Skip to content

Commit

Permalink
Changes to X86_64 verification. (#2013)
Browse files Browse the repository at this point in the history 
* Changes to X86_64 verification.

* Address comments.
  • Loading branch information
@andreistefanescu
andreistefanescu authored Jan 18, 2024
1 parent 0a8fdf5 commit 8561a21
Show file tree
Hide file tree
Showing 2 changed files with 81 additions and 73 deletions.
86 changes: 48 additions & 38 deletions src/SAWScript/Crucible/LLVM/Builtins.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,8 +83,10 @@ module SAWScript.Crucible.LLVM.Builtins
, checkSpecReturnType
, verifyPrestate
, verifyPoststate
, getPoststateObligations
, withCfgAndBlockId
, registerOverride
, lookupMemGlobal
) where

import Prelude hiding (fail)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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


--------------------------------------------------------------------------------
Expand Down Expand Up @@ -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) ->
Expand All @@ -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 ::
Expand Down
68 changes: 33 additions & 35 deletions src/SAWScript/Crucible/LLVM/X86.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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"
Expand All @@ -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
Expand Down

0 comments on commit 8561a21

Please sign in to comment.