diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index d31f8e6f1f..ca4ae24655 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/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 :: diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index d0ced45957..26aca27d81 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/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