Pipe condition metadata through the X86 verification modes.

Author: robdockins

src/SAWScript/Crucible/LLVM/X86.hs

@@ -41,6 +41,7 @@ import Control.Monad.Catch (MonadThrow)
 
 import qualified Data.BitVector.Sized as BV
 import Data.Foldable (foldlM)
+import           Data.IORef
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Vector as Vector
 import qualified Data.Text as Text
@@ -79,6 +80,7 @@ import SAWScript.Options
 import SAWScript.X86 hiding (Options)
 import SAWScript.X86Spec
 import SAWScript.Crucible.Common
+import SAWScript.Crucible.Common.Override (MetadataMap)
 
 import qualified SAWScript.Crucible.Common as Common
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
@@ -350,6 +352,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
       basic_ss <- getBasicSS
       rw <- getTopLevelRW
       sym <- liftIO $ newSAWCoreExprBuilder sc
+      mdMap <- liftIO $ newIORef mempty
       SomeOnlineBackend bak <- liftIO $
         newSAWCoreBackendWithTimeout pathSatSolver sym $ rwCrucibleTimeout rw
       cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms $ W4.getConfiguration sym
@@ -487,7 +490,8 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
                 }
           liftIO $ printOutLn opts Info
             "Examining specification to determine postconditions"
-          liftIO . void . runX86Sim finalState $ assertPost globals' env (preState ^. x86Mem) (preState ^. x86Regs)
+          liftIO . void . runX86Sim finalState $
+            assertPost globals' env (preState ^. x86Mem) (preState ^. x86Regs) mdMap
           pure $ C.regValue r
 
       liftIO $ printOutLn opts Info "Simulating function"
@@ -521,7 +525,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
             ar
         C.TimeoutResult{} -> fail "Execution timed out"
 
-      (stats,thms) <- checkGoals bak opts nm sc tactic
+      (stats,thms) <- checkGoals bak opts nm sc tactic mdMap
 
       end <- io getCurrentTime
       let diff = diffUTCTime end start
@@ -1020,8 +1024,9 @@ assertPost ::
   Map MS.AllocIndex Ptr ->
   Mem {- ^ The state of memory before simulation -} ->
   Regs {- ^ The state of the registers before simulation -} ->
+  IORef MetadataMap {- ^ metadata map -} ->
   X86Sim ()
-assertPost globals env premem preregs = do
+assertPost globals env premem preregs mdMap = do
   SomeOnlineBackend bak <- use x86Backend
   sym <- use x86Sym
   opts <- use x86Options
@@ -1109,9 +1114,10 @@ assertPost globals env premem preregs = do
     Right (_, st) -> pure st
   liftIO . forM_ (view O.osAssumes st) $ \(_md, asum) ->
     C.addAssumption bak $ C.GenericAssumption (st ^. O.osLocation) "precondition" asum
-  liftIO . forM_ (view LO.osAsserts st) $ \(_md, W4.LabeledPred p r) ->
-    -- TODO, use assertion metadata
-    C.addAssertion bak $ C.LabeledPred p r
+  liftIO . forM_ (view LO.osAsserts st) $ \(md, W4.LabeledPred p r) ->
+       do (ann,p') <- W4.annotateTerm sym p
+          modifyIORef mdMap (Map.insert ann md)
+          C.addAssertion bak (W4.LabeledPred p' r)
 
 -- | Assert that a points-to postcondition holds.
 assertPointsTo ::
@@ -1160,9 +1166,10 @@ checkGoals ::
   String ->
   SharedContext ->
   ProofScript () ->
+  IORef MetadataMap {- ^ metadata map -} ->
   TopLevel (SolverStats, Set TheoremNonce)
-checkGoals bak opts nm sc tactic = do
-  gs <- liftIO $ getGoals (SomeBackend bak)
+checkGoals bak opts nm sc tactic mdMap = do
+  gs <- liftIO $ getGoals (SomeBackend bak) mdMap
   liftIO . printOutLn opts Info $ mconcat
     [ "Simulation finished, running solver on "
     , show $ length gs
@@ -1172,12 +1179,12 @@ checkGoals bak opts nm sc tactic = do
     term <- liftIO $ gGoal sc g
     let proofgoal = ProofGoal
                     { goalNum  = n
-                    , goalType = "vc"
+                    , goalType = MS.conditionType (gMd g)
                     , goalName = nm
-                    , goalLoc  = show $ gLoc g
+                    , goalLoc  = show $ MS.conditionLoc (gMd g)
                     , goalDesc = show $ gMessage g
                     , goalProp = term
-                    , goalTags = mempty -- TODO! propagate tags
+                    , goalTags = MS.conditionTags (gMd g)
                     }
     res <- runProofScript tactic proofgoal (Just (gLoc g)) $ Text.unwords
               ["X86 verification condition", Text.pack (show n), Text.pack (show (gMessage g))]

src/SAWScript/X86.hs

@@ -12,6 +12,7 @@ module SAWScript.X86
   , Fun(..)
   , Goal(..)
   , gGoal
+  , gLoc
   , getGoals
   , X86Error(..)
   , X86Unsupported(..)
@@ -35,11 +36,12 @@ import qualified Data.BitVector.Sized as BV
 import           Data.ByteString (ByteString)
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BSC
+import           Data.IORef
 import qualified Data.Map as Map
 import qualified Data.Text as Text
 import           Data.Text.Encoding(decodeUtf8)
 import           System.IO(hFlush,stdout)
-import           Data.Maybe(mapMaybe)
+import           Data.Maybe(mapMaybe, fromMaybe)
 
 -- import Text.PrettyPrint.ANSI.Leijen(pretty)
 
@@ -135,6 +137,8 @@ import Verifier.SAW.Cryptol.Prelude(scLoadPreludeModule,scLoadCryptolModule)
 -- SAWScript
 import SAWScript.X86Spec hiding (Prop)
 import SAWScript.Proof(boolToProp, Prop)
+import SAWScript.Crucible.Common.MethodSpec (ConditionMetadata(..))
+import SAWScript.Crucible.Common.Override (MetadataMap)
 import SAWScript.Crucible.Common
   ( newSAWCoreBackend, newSAWCoreExprBuilder
   , sawCoreState, SomeOnlineBackend(..)
@@ -405,6 +409,9 @@ translate opts elf fun =
   do let name = funName fun
      sayLn ("Translating function: " ++ BSC.unpack name)
 
+     -- TODO? do we need to pass in the mdMap into more places in this mode?
+     mdMap <- newIORef mempty
+
      let ?memOpts = Crucible.defaultMemOptions
      let ?recordLLVMAnnotation = \_ _ _ -> return ()
 
@@ -426,7 +433,7 @@ translate opts elf fun =
 
      addr <- doSim opts elf sfs name globs st checkPost
 
-     gs <- getGoals bak
+     gs <- getGoals bak mdMap
      sc <- saw_ctx <$> sawCoreState sym
      return (sc, addr, gs)
 
@@ -549,10 +556,13 @@ makeCFG opts elf name addr =
 data Goal = Goal
   { gAssumes :: [ Term ]              -- ^ Assuming these
   , gShows   :: Term                  -- ^ We need to show this
-  , gLoc     :: ProgramLoc            -- ^ The goal came from here
+  , gMd      :: ConditionMetadata     -- ^ Metadata about the goal
   , gMessage :: SimErrorReason        -- ^ We should say this if the proof fails
   }
 
+gLoc :: Goal -> ProgramLoc
+gLoc = conditionLoc . gMd
+
 -- | The proposition that needs proving (i.e., assumptions imply conclusion)
 gGoal :: SharedContext -> Goal -> IO Prop
 gGoal sc g0 = boolToProp sc [] =<< go (gAssumes g)
@@ -575,21 +585,31 @@ gGoal sc g0 = boolToProp sc [] =<< go (gAssumes g)
             []     -> return (gShows g)
             a : as -> scImplies sc a =<< go as
 
-getGoals :: SomeBackend Sym -> IO [Goal]
-getGoals (SomeBackend bak) =
-  do obls <- maybe [] goalsToList <$> getProofObligations bak
+getGoals :: SomeBackend Sym -> IORef MetadataMap -> IO [Goal]
+getGoals (SomeBackend bak) mdMap =
+  do finalMdMap <- readIORef mdMap
+     obls <- maybe [] goalsToList <$> getProofObligations bak
      st <- sawCoreState sym
-     mapM (toGoal st) obls
+     mapM (toGoal st finalMdMap) obls
   where
   sym = backendGetSym bak
 
-  toGoal st (ProofGoal asmps g) =
+  toGoal st finalMdMap (ProofGoal asmps g) =
     do a1 <- toSC sym st =<< assumptionsPred sym asmps
        p  <- toSC sym st (g ^. labeledPred)
        let SimError loc msg = g^.labeledPredMsg
+       let defaultMd = ConditionMetadata
+                       { conditionLoc = loc
+                       , conditionTags = mempty
+                       , conditionType = "safety assertion"
+                       , conditionContext = ""
+                       }
+       let md = fromMaybe defaultMd $
+                  do ann <- W4.getAnnotation sym (g^.labeledPred)
+                     Map.lookup ann finalMdMap
        return Goal { gAssumes = [a1]
                    , gShows   = p
-                   , gLoc     = loc
+                   , gMd      = md
                    , gMessage = msg
                    }