Changes to X86_64 verification.

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -83,8 +83,10 @@ module SAWScript.Crucible.LLVM.Builtins
     , checkSpecReturnType
     , verifyPrestate
     , verifyPoststate
+    , getPoststateObligations
     , withCfgAndBlockId
     , registerOverride
+    , lookupMemGlobal
     ) where
 
 import Prelude hiding (fail)
@@ -616,10 +618,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
      -- set up the LLVM memory with a pristine heap
      let globals = cc^.ccLLVMGlobals
      let mvar = Crucible.llvmMemVar (ccLLVMContext cc)
-     mem0 <-
-       case Crucible.lookupGlobal mvar globals of
-         Nothing   -> fail "internal error: LLVM Memory global not found"
-         Just mem0 -> return mem0
+     let mem0 = lookupMemGlobal mvar globals
      -- push a memory stack frame if starting from a breakpoint
      let mem = case methodSpec^.csParentName of
                Just parent -> mem0
@@ -727,10 +726,7 @@ refineMethodSpec cc methodSpec lemmas tactic =
      -- set up the LLVM memory with a pristine heap
      let globals = cc^.ccLLVMGlobals
      let mvar = Crucible.llvmMemVar (ccLLVMContext cc)
-     mem <-
-       case Crucible.lookupGlobal mvar globals of
-         Nothing   -> fail "internal error: LLVM Memory global not found"
-         Just mem0 -> return mem0
+     let mem = lookupMemGlobal mvar globals
 
      let globals1 = Crucible.llvmGlobals mvar mem
 
@@ -947,10 +943,7 @@ verifyPrestate opts cc mspec globals =
      liftIO $ W4.setCurrentProgramLoc sym prestateLoc
 
      let lvar = Crucible.llvmMemVar (ccLLVMContext cc)
-     mem <-
-       case Crucible.lookupGlobal lvar globals of
-         Nothing  -> fail "internal error: LLVM Memory global not found"
-         Just mem -> pure mem
+     let mem = lookupMemGlobal lvar globals
 
      -- Allocate LLVM memory for each 'llvm_alloc'
      (env, mem') <- runStateT
@@ -1253,6 +1246,12 @@ doAlloc cc i (LLVMAllocSpec mut _memTy alignment sz md fresh initialization)
 
 --------------------------------------------------------------------------------
 
+lookupMemGlobal :: Crucible.GlobalVar tp -> Crucible.SymGlobalState sym -> Crucible.RegValue sym tp
+lookupMemGlobal mvar globals =
+  fromMaybe
+    (panic "SAWScript.Crucible.LLVM.X86.pushFreshReturnAddress" ["LLVM Memory global not found"])
+    (Crucible.lookupGlobal mvar globals)
+
 ppAbortedResult :: LLVMCrucibleContext arch
                 -> Crucible.AbortedResult Sym a
                 -> Doc ann
@@ -1264,9 +1263,7 @@ ppGlobalPair :: LLVMCrucibleContext arch
 ppGlobalPair cc gp =
   let mvar = Crucible.llvmMemVar (ccLLVMContext cc)
       globals = gp ^. Crucible.gpGlobals in
-  case Crucible.lookupGlobal mvar globals of
-    Nothing -> "LLVM Memory global variable not initialized"
-    Just mem -> Crucible.ppMem (Crucible.memImplHeap mem)
+  Crucible.ppMem $ Crucible.memImplHeap $ lookupMemGlobal mvar globals
 
 
 --------------------------------------------------------------------------------
@@ -1673,34 +1670,12 @@ verifyPoststate cc mspec env0 globals ret mdMap =
           modifyIORef mdMap (Map.insert ann md)
           Crucible.addAssertion bak (Crucible.LabeledPred p' r)
 
-     obligations <- io $
-       do obls <- Crucible.getProofObligations bak
-          Crucible.clearProofObligations bak
-          return (maybe [] Crucible.goalsToList obls)
-
-     finalMdMap <- io $ readIORef mdMap
-     sc_obligations <- io $ mapM (verifyObligation sc finalMdMap) obligations
+     sc_obligations <- io $ getPoststateObligations sc bak mdMap
      return (sc_obligations, st)
 
   where
     sym = cc^.ccSym
 
-    verifyObligation sc finalMdMap (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) =
-      do st <- Common.sawCoreState sym
-         hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps
-         conclTerm  <- toSC sym st concl
-         obligation <- scImplies sc hypTerm conclTerm
-         let defaultMd = MS.ConditionMetadata
-                         { MS.conditionLoc = loc
-                         , MS.conditionTags = mempty
-                         , MS.conditionType = "safety assertion"
-                         , MS.conditionContext = ""
-                         }
-         let md = fromMaybe defaultMd $
-                    do ann <- W4.getAnnotation sym concl
-                       Map.lookup ann finalMdMap
-         return (show err, md, obligation)
-
     matchResult opts sc =
       case (ret, mspec ^. MS.csRetValue) of
         (Just (rty,r), Just expect) ->
@@ -1715,6 +1690,41 @@ verifyPoststate cc mspec env0 globals ret mdMap =
           fail "verifyPoststate: unexpected llvm_return specification"
         _ -> return ()
 
+-- | Translate the proof obligations from the Crucible backend into SAWCore
+-- terms. For each proof oblication, return a triple consisting of the error
+-- message, the metadata, and the SAWCore.
+getPoststateObligations ::
+  Crucible.IsSymBackend Sym bak =>
+  SharedContext ->
+  bak ->
+  IORef MetadataMap ->
+  IO [(String, MS.ConditionMetadata, Term)]
+getPoststateObligations sc bak mdMap =
+  do obligations <- maybe [] Crucible.goalsToList <$> Crucible.getProofObligations bak
+     Crucible.clearProofObligations bak
+
+     finalMdMap <- readIORef mdMap
+     mapM (verifyObligation finalMdMap) obligations
+
+  where
+    sym = Crucible.backendGetSym bak
+
+    verifyObligation finalMdMap (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) =
+      do st <- Common.sawCoreState sym
+         hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps
+         conclTerm <- toSC sym st concl
+         obligation <- scImplies sc hypTerm conclTerm
+         let defaultMd = MS.ConditionMetadata
+                         { MS.conditionLoc = loc
+                         , MS.conditionTags = mempty
+                         , MS.conditionType = "safety assertion"
+                         , MS.conditionContext = ""
+                         }
+         let md = fromMaybe defaultMd $
+                    do ann <- W4.getAnnotation sym concl
+                       Map.lookup ann finalMdMap
+         return (show err, md, obligation)
+
 --------------------------------------------------------------------------------
 
 setupLLVMCrucibleContext ::

src/SAWScript/Crucible/LLVM/X86.hs

@@ -527,19 +527,8 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
                  let loc = MS.conditionLoc md
                  C.addAssumption bak
                    (C.GenericAssumption loc reason expr)
-          r <- C.callCFG cfg . C.RegMap . singleton . C.RegEntry macawStructRepr $ preState ^. x86Regs
-          globals' <- C.readGlobals
-          mem' <- C.readGlobal mvar
-          let finalState = preState
-                { _x86Mem = mem'
-                , _x86Regs = C.regValue r
-                , _x86CrucibleContext = cc & ccLLVMGlobals .~ globals'
-                }
-          liftIO $ printOutLn opts Info
-            "Examining specification to determine postconditions"
-          liftIO . void . runX86Sim finalState $
-            assertPost globals' env (preState ^. x86Mem) (preState ^. x86Regs) mdMap
-          pure $ C.regValue r
+          C.regValue <$>
+            (C.callCFG cfg . C.RegMap . singleton . C.RegEntry macawStructRepr $ preState ^. x86Regs)
 
       liftIO $ printOutLn opts Info "Simulating function"
 
@@ -571,19 +560,29 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
 
       let execFeatures = simpleLoopFixpointFeature ++ psatf
 
-      liftIO $ C.executeCrucible execFeatures initial >>= \case
-        C.FinishedResult{} -> pure ()
+      finalState <- liftIO $ C.executeCrucible execFeatures initial >>= \case
+        C.FinishedResult _ pr -> do
+          gp <- getGlobalPair opts pr
+          let mem' = lookupMemGlobal mvar $ gp ^. C.gpGlobals
+          return $ preState
+            { _x86Mem = mem'
+            , _x86Regs = C.regValue $ gp ^. C.gpValue
+            , _x86CrucibleContext = cc & ccLLVMGlobals .~ (gp ^. C.gpGlobals)
+            }
         C.AbortedResult _ ar -> do
-          printOutLn opts Warn "Warning: function never returns"
-          print $ Common.ppAbortedResult
-            ( \gp ->
-                case C.lookupGlobal mvar $ gp ^. C.gpGlobals of
-                  Nothing -> "LLVM memory global variable not initialized"
-                  Just mem -> C.LLVM.ppMem $ C.LLVM.memImplHeap mem
-            )
-            ar
+          let resultDoc = Common.ppAbortedResult
+                (\gp ->  C.LLVM.ppMem $ C.LLVM.memImplHeap $ lookupMemGlobal mvar $ gp ^. C.gpGlobals)
+                ar
+          fail $ unlines [ "Execution failed: function never returns."
+                         , show resultDoc
+                         ]
         C.TimeoutResult{} -> fail "Execution timed out"
 
+      liftIO $ printOutLn opts Info
+        "Examining specification to determine postconditions"
+      liftIO $ void $ runX86Sim finalState $
+        assertPost env (preState ^. x86Mem) (preState ^. x86Regs) mdMap
+
       (stats,vcstats) <- checkGoals bak opts nm sc tactic mdMap
 
       end <- io getCurrentTime
@@ -1247,13 +1246,12 @@ argRegs = [Macaw.RDI, Macaw.RSI, Macaw.RDX, Macaw.RCX, Macaw.R8, Macaw.R9]
 -- | Assert the postcondition for the spec, given the final memory and register map.
 assertPost ::
   X86Constraints =>
-  C.SymGlobalState Sym ->
   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 mdMap = do
+assertPost env premem preregs mdMap = do
   SomeOnlineBackend bak <- use x86Backend
   sym <- use x86Sym
   opts <- use x86Options
@@ -1264,6 +1262,7 @@ assertPost globals env premem preregs mdMap = do
   let
     tyenv = ms ^. MS.csPreState . MS.csAllocs
     nameEnv = MS.csTypeNames ms
+    globals = cc ^. ccLLVMGlobals
 
   prersp <- getReg Macaw.RSP preregs
   expectedIP <- liftIO $ C.LLVM.doLoad bak premem prersp (C.LLVM.bitvectorType 8)
@@ -1390,15 +1389,14 @@ checkGoals ::
   IORef MetadataMap {- ^ metadata map -} ->
   TopLevel (SolverStats, [MS.VCStats])
 checkGoals bak opts nm sc tactic mdMap = do
-  gs <- liftIO $ getGoals (SomeBackend bak) mdMap
+  gs <- liftIO $ getPoststateObligations sc bak mdMap
   liftIO . printOutLn opts Info $ mconcat
     [ "Simulation finished, running solver on "
     , show $ length gs
     , " goals"
     ]
-  outs <- forM (zip [0..] gs) $ \(n, g) -> do
-    term <- liftIO $ gGoal sc g
-    let md = gMd g
+  outs <- forM (zip [0..] gs) $ \(n, (msg, md, term)) -> do
+    g <- liftIO $ boolToProp sc [] term
     let ploc = MS.conditionLoc md
     let gloc = (unwords [show (W4.plSourceLoc ploc)
                        ,"in"
@@ -1410,24 +1408,24 @@ checkGoals bak opts nm sc tactic mdMap = do
                     , goalType = MS.conditionType md
                     , goalName = nm
                     , goalLoc  = gloc
-                    , goalDesc = show $ gMessage g
-                    , goalSequent = propToSequent term
+                    , goalDesc = msg
+                    , goalSequent = propToSequent g
                     , goalTags = MS.conditionTags md
                     }
-    res <- runProofScript tactic term proofgoal (Just (gLoc g))
+    res <- runProofScript tactic g proofgoal (Just ploc)
              (Text.unwords
-              ["X86 verification condition", Text.pack (show n), Text.pack (show (gMessage g))])
+              ["X86 verification condition", Text.pack (show n), Text.pack msg])
              False -- do not record this theorem in the database
              False -- TODO! useSequentGoals
     case res of
       ValidProof stats thm ->
         return (stats, MS.VCStats md stats (thmSummary thm) (thmNonce thm) (thmDepends thm) (thmElapsedTime thm))
       UnfinishedProof pst -> do
-        printOutLnTop Info $ unwords ["Subgoal failed:", show $ gMessage g]
+        printOutLnTop Info $ unwords ["Subgoal failed:", msg]
         printOutLnTop Info (show (psStats pst))
         throwTopLevel $ "Proof failed: " ++ show (length (psGoals pst)) ++ " goals remaining."
       InvalidProof stats vals _pst -> do
-        printOutLnTop Info $ unwords ["Subgoal failed:", show $ gMessage g]
+        printOutLnTop Info $ unwords ["Subgoal failed:", msg]
         printOutLnTop Info (show stats)
         printOutLnTop OnlyCounterExamples "----------Counterexample----------"
         ppOpts <- sawPPOpts . rwPPOpts <$> getTopLevelRW