From 5e63f22311b240350c1e179acb3c98e5446e6fc8 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 25 May 2020 16:31:32 -0400 Subject: [PATCH 1/4] Properly match points-to and return value assertions in x86 --- src/SAWScript/Crucible/LLVM/Override.hs | 1 + src/SAWScript/Crucible/LLVM/X86.hs | 107 ++++++++++++++++-------- 2 files changed, 74 insertions(+), 34 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 181ae699cb..605c8550b8 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -36,6 +36,7 @@ module SAWScript.Crucible.LLVM.Override , termSub , learnCond + , learnSetupCondition , matchArg , methodSpecHandler , valueToSC diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 4d19346497..80fda27463 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -53,6 +53,7 @@ import Data.Parameterized.NatRepr import Data.Parameterized.Context hiding (view) import Data.Parameterized.Nonce +import Verifier.SAW.Recognizer import Verifier.SAW.Term.Functor import Verifier.SAW.TypedTerm @@ -65,15 +66,18 @@ import SAWScript.X86 hiding (Options) import SAWScript.X86Spec import qualified SAWScript.Crucible.Common.MethodSpec as MS +import qualified SAWScript.Crucible.Common.Override as O import qualified SAWScript.Crucible.Common.Setup.Type as Setup import SAWScript.Crucible.LLVM.Builtins import SAWScript.Crucible.LLVM.MethodSpecIR import SAWScript.Crucible.LLVM.ResolveSetupValue +import qualified SAWScript.Crucible.LLVM.Override as LO import qualified What4.Expr as W4 import qualified What4.FunctionName as W4 import qualified What4.Interface as W4 +import qualified What4.LabeledPred as W4 import qualified What4.ProgramLoc as W4 import qualified Lang.Crucible.Analysis.Postdom as C @@ -114,11 +118,16 @@ import qualified Data.ElfEdit as Elf type LLVMArch = C.LLVM.X86 64 type LLVM = C.LLVM.LLVM LLVMArch +type LLVMOverrideMatcher = O.OverrideMatcher LLVM type Regs = Assignment (C.RegValue' Sym) (Macaw.MacawCrucibleRegTypes Macaw.X86_64) type Register = Macaw.X86Reg (Macaw.BVType 64) type Mem = C.LLVM.MemImpl Sym type Ptr = C.LLVM.LLVMPtr Sym 64 -type X86Constraints = (C.LLVM.HasPtrWidth (C.LLVM.ArchWidth LLVMArch), C.LLVM.HasLLVMAnn Sym) +type X86Constraints = + ( C.LLVM.HasPtrWidth (C.LLVM.ArchWidth LLVMArch) + , C.LLVM.HasLLVMAnn Sym + , ?lc :: C.LLVM.TypeContext + ) newtype X86Sim a = X86Sim { unX86Sim :: StateT X86State IO a } deriving (Functor, Applicative, Monad, MonadIO, MonadState X86State, MonadThrow) @@ -187,7 +196,8 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl let ?badBehaviorMap = bbMapRef sym <- liftIO $ C.newSAWCoreBackend W4.FloatRealRepr sc globalNonceGenerator halloc <- getHandleAlloc - mvar <- liftIO $ C.LLVM.mkMemVar halloc + -- mvar <- liftIO $ C.LLVM.mkMemVar halloc + let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule sfs <- liftIO $ Macaw.newSymFuns sym (C.SomeCFG cfg, elf, relf, addr) <- liftIO $ buildCFG opts halloc path nm @@ -219,6 +229,8 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl liftIO $ printOutLn opts Info "Examining specification to determine preconditions" methodSpec <- buildMethodSpec bic opts llvmModule nm (show addr) setup + let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx + emptyState <- liftIO $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr (env, preState) <- liftIO . runX86Sim emptyState $ setupMemory globsyms @@ -248,14 +260,16 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl $ Macaw.crucGenArchConstraints Macaw.x86_64MacawSymbolicFns $ do 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 env (preState ^. x86Mem) (preState ^. x86Regs) + liftIO . void . runX86Sim finalState $ assertPost globals' env (preState ^. x86Mem) (preState ^. x86Regs) pure $ C.regValue r liftIO $ printOutLn opts Info "Simulating function" @@ -322,8 +336,9 @@ buildMethodSpec :: buildMethodSpec bic opts lm nm loc setup = setupLLVMCrucibleContext bic opts lm $ \cc -> do let methodId = LLVMMethodId nm Nothing - let programLoc = W4.mkProgramLoc (W4.functionNameFromText $ Text.pack nm) - . W4.OtherPos $ Text.pack loc + let programLoc = + W4.mkProgramLoc (W4.functionNameFromText $ Text.pack nm) + . W4.OtherPos $ Text.pack loc let lc = modTrans lm ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx (args, ret) <- case llvmSignature opts lm nm of Left err -> fail $ mconcat ["Could not find declaration for \"", nm, "\": ", err] @@ -434,9 +449,9 @@ setupMemory globsyms = do tyenv = ms ^. MS.csPreState . MS.csAllocs nameEnv = MS.csTypeNames ms - env <- foldlM executeAllocation Map.empty . Map.assocs $ tyenv + env <- foldlM assumeAllocation Map.empty . Map.assocs $ tyenv - mapM_ (executePointsTo env tyenv nameEnv) $ ms ^. MS.csPreState . MS.csPointsTos + mapM_ (assumePointsTo env tyenv nameEnv) $ ms ^. MS.csPreState . MS.csPointsTos setArgs env tyenv nameEnv . fmap snd . Map.elems $ ms ^. MS.csArgBindings @@ -502,12 +517,12 @@ allocateStack szInt = do -- | Process a crucible_alloc statement, allocating the requested memory and -- associating a pointer to that memory with the appropriate index. -executeAllocation :: +assumeAllocation :: X86Constraints => Map MS.AllocIndex Ptr -> (MS.AllocIndex, LLVMAllocSpec) {- ^ crucible_alloc statement -} -> X86Sim (Map MS.AllocIndex Ptr) -executeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc) = do +assumeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc) = do sym <- use x86Sym mem <- use x86Mem sz' <- liftIO $ W4.bvLit sym knownNat $ C.LLVM.bytesToInteger sz @@ -517,14 +532,14 @@ executeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc) = do pure $ Map.insert i ptr env -- | Process a crucible_points_to statement, writing some SetupValue to a pointer. -executePointsTo :: +assumePointsTo :: X86Constraints => Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> LLVMPointsTo LLVMArch {- ^ crucible_points_to statement from the precondition -} -> X86Sim () -executePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tval) = do +assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tval) = do when (isJust cond) $ throwX86 "unsupported x86_64 command: crucible_conditional_points_to" sym <- use x86Sym cc <- use x86CrucibleContext @@ -596,18 +611,21 @@ setArgs env tyenv nameEnv args -- | 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 -} -> X86Sim () -assertPost env premem preregs = do +assertPost globals env premem preregs = do sym <- use x86Sym + opts <- use x86Options + sc <- use x86SharedContext + cc <- use x86CrucibleContext ms <- use x86MethodSpec postregs <- use x86Regs - let tyenv = ms ^. MS.csPreState . MS.csAllocs - nameEnv = MS.csTypeNames ms - forM_ (ms ^. MS.csPostState . MS.csPointsTos) - $ assertPointsTo env tyenv nameEnv + let + tyenv = ms ^. MS.csPreState . MS.csAllocs + nameEnv = MS.csTypeNames ms prersp <- getReg Macaw.RSP preregs expectedIP <- liftIO $ C.LLVM.doLoad sym premem prersp (C.LLVM.bitvectorType 8) @@ -623,7 +641,38 @@ assertPost env premem preregs = do liftIO $ C.addAssertion sym . C.LabeledPred correctStack . C.SimError W4.initializationLoc $ C.AssertFailureSimError "Stack not preserved" "" - -- TODO: Match return value in RAX + pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) + $ assertPointsTo env tyenv nameEnv + + returnMatches <- case (ms ^. MS.csRetValue, ms ^. MS.csRet) of + (Just expectedRet, Just retTy) -> do + postRAX <- C.LLVM.ptrToPtrVal <$> getReg Macaw.RAX postregs + pure [LO.matchArg opts sc cc ms MS.PostState postRAX retTy expectedRet] + _ -> pure [] + + let setupConditionMatches = LO.learnSetupCondition opts sc cc ms MS.PostState + <$> (ms ^. MS.csPostState . MS.csConditions) + + let + initialTerms = Map.fromList + [ (ecVarIndex ec, ttTerm tt) + | tt <- ms ^. MS.csPreState . MS.csFreshVars + , let Just ec = asExtCns (ttTerm tt) + ] + initialFree = Set.fromList $ LO.termId . ttTerm <$> ms ^. MS.csPostState . MS.csFreshVars + + result <- liftIO + . O.runOverrideMatcher sym globals env initialTerms initialFree (ms ^. MS.csLoc) + . sequence_ $ mconcat + [ returnMatches + , pointsToMatches + , setupConditionMatches + ] + st <- case result of + Left err -> throwX86 $ show err + Right (_, st) -> pure st + liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) -> + C.addAssertion sym $ C.LabeledPred p r -- | Assert that a points-to postcondition holds. assertPointsTo :: @@ -632,31 +681,21 @@ assertPointsTo :: Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> LLVMPointsTo LLVMArch {- ^ crucible_points_to statement from the precondition -} -> - X86Sim () + X86Sim (LLVMOverrideMatcher md ()) assertPointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr texpected) = do when (isJust cond) $ throwX86 "unsupported x86_64 command: crucible_conditional_points_to" sym <- use x86Sym opts <- use x86Options + sc <- use x86SharedContext cc <- use x86CrucibleContext + ms <- use x86MethodSpec mem <- use x86Mem ptr <- liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) =<< resolveSetupVal cc mem env tyenv Map.empty tptr - storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv texpected - _actual <- liftIO $ C.LLVM.assertSafe sym =<< C.LLVM.loadRaw sym mem ptr storTy C.LLVM.noAlignment - -- TODO: actually do matching between actual and expected - -- For now, we only make sure we can load the memory - if | MS.SetupTerm expected <- texpected - , FTermF (ExtCns ec) <- unwrapTermF $ ttTerm expected - , ('_':_) <- ecName ec - -> pure () - | otherwise -> liftIO . printOutLn opts Warn $ mconcat - [ "During x86 verification, attempted to match against a term that is not " - , "a fresh variable with an underscore-prefixed name. " - , "Note that crucible_points_to only asserts that memory is readable. " - , "Matching against concrete values is potentially unsound." - ] - - pure () + memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv texpected + storTy <- liftIO $ C.LLVM.toStorableType memTy + actual <- liftIO $ C.LLVM.assertSafe sym =<< C.LLVM.loadRaw sym mem ptr storTy C.LLVM.noAlignment + pure $ LO.matchArg opts sc cc ms MS.PostState actual memTy texpected -- | Gather and run the solver on goals from the simulator. checkGoals :: From b0add5fb78ed60f75b5aa091c36b231c25138e91 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Thu, 18 Jun 2020 11:20:36 -0400 Subject: [PATCH 2/4] Address comments --- src/SAWScript/Crucible/LLVM/X86.hs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 80fda27463..e27e29aa0c 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -196,7 +196,6 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl let ?badBehaviorMap = bbMapRef sym <- liftIO $ C.newSAWCoreBackend W4.FloatRealRepr sc globalNonceGenerator halloc <- getHandleAlloc - -- mvar <- liftIO $ C.LLVM.mkMemVar halloc let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule sfs <- liftIO $ Macaw.newSymFuns sym @@ -641,17 +640,18 @@ assertPost globals env premem preregs = do liftIO $ C.addAssertion sym . C.LabeledPred correctStack . C.SimError W4.initializationLoc $ C.AssertFailureSimError "Stack not preserved" "" - pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) - $ assertPointsTo env tyenv nameEnv - returnMatches <- case (ms ^. MS.csRetValue, ms ^. MS.csRet) of (Just expectedRet, Just retTy) -> do postRAX <- C.LLVM.ptrToPtrVal <$> getReg Macaw.RAX postregs pure [LO.matchArg opts sc cc ms MS.PostState postRAX retTy expectedRet] _ -> pure [] - let setupConditionMatches = LO.learnSetupCondition opts sc cc ms MS.PostState - <$> (ms ^. MS.csPostState . MS.csConditions) + pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) + $ assertPointsTo env tyenv nameEnv + + let setupConditionMatches = fmap + (LO.learnSetupCondition opts sc cc ms MS.PostState) + $ ms ^. MS.csPostState . MS.csConditions let initialTerms = Map.fromList @@ -659,7 +659,7 @@ assertPost globals env premem preregs = do | tt <- ms ^. MS.csPreState . MS.csFreshVars , let Just ec = asExtCns (ttTerm tt) ] - initialFree = Set.fromList $ LO.termId . ttTerm <$> ms ^. MS.csPostState . MS.csFreshVars + initialFree = Set.fromList . fmap (LO.termId . ttTerm) $ ms ^. MS.csPostState . MS.csFreshVars result <- liftIO . O.runOverrideMatcher sym globals env initialTerms initialFree (ms ^. MS.csLoc) From b32a4e78388eaa154c415f3b772a8a1b5d78d7f1 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Thu, 18 Jun 2020 11:36:26 -0400 Subject: [PATCH 3/4] Fix and enable previously-disabled x86 tests. --- intTests/disabled_tests.txt | 4 ---- intTests/test_llvm_x86_01/test.saw | 2 +- intTests/test_llvm_x86_02/test.saw | 2 +- intTests/test_llvm_x86_03/test.saw | 2 +- intTests/test_llvm_x86_04/test.saw | 2 +- 5 files changed, 4 insertions(+), 8 deletions(-) diff --git a/intTests/disabled_tests.txt b/intTests/disabled_tests.txt index 41a8c64a6b..3ca52f7a7f 100644 --- a/intTests/disabled_tests.txt +++ b/intTests/disabled_tests.txt @@ -12,7 +12,3 @@ test0010_jss_cnf_exp # Missing LLVM intrinsic test0039_rust - -# Current limitations of crucible_llvm_verify_x86 -test_llvm_x86_02 -test_llvm_x86_03 diff --git a/intTests/test_llvm_x86_01/test.saw b/intTests/test_llvm_x86_01/test.saw index 6550344cd5..55a6c203a2 100644 --- a/intTests/test_llvm_x86_01/test.saw +++ b/intTests/test_llvm_x86_01/test.saw @@ -11,7 +11,7 @@ let foo_setup = do { val <- crucible_fresh_var "val'" (llvm_int 64); crucible_points_to ptr (crucible_term val); }; -foo_method_spec <- crucible_llvm_verify_x86 m "./test" "foo" [] false foo_setup; +foo_method_spec <- crucible_llvm_verify_x86 m "./test" "foo" [] false foo_setup w4; let bar_setup = do { crucible_execute_func []; diff --git a/intTests/test_llvm_x86_02/test.saw b/intTests/test_llvm_x86_02/test.saw index 33408348ba..682ff36449 100644 --- a/intTests/test_llvm_x86_02/test.saw +++ b/intTests/test_llvm_x86_02/test.saw @@ -11,4 +11,4 @@ let increment_setup = do { crucible_points_to ptr (crucible_term valprime); crucible_postcond {{ valprime == val }}; }; -fails (crucible_llvm_verify_x86 m "./test" "increment" [] false increment_setup); \ No newline at end of file +fails (crucible_llvm_verify_x86 m "./test" "increment" [] false increment_setup w4); \ No newline at end of file diff --git a/intTests/test_llvm_x86_03/test.saw b/intTests/test_llvm_x86_03/test.saw index c3e28f62a1..d44a3e3adb 100644 --- a/intTests/test_llvm_x86_03/test.saw +++ b/intTests/test_llvm_x86_03/test.saw @@ -6,4 +6,4 @@ let test_setup = do { crucible_execute_func []; crucible_return (crucible_term {{ 1 : [64] }}); }; -fail (crucible_llvm_verify_x86 m "./test" "foo" [] false test_setup); \ No newline at end of file +fails (crucible_llvm_verify_x86 m "./test" "foo" [] false test_setup w4); \ No newline at end of file diff --git a/intTests/test_llvm_x86_04/test.saw b/intTests/test_llvm_x86_04/test.saw index 2b6e06befb..f5c6fbf544 100644 --- a/intTests/test_llvm_x86_04/test.saw +++ b/intTests/test_llvm_x86_04/test.saw @@ -16,4 +16,4 @@ let addvar_setup = do { valprime <- crucible_fresh_var "_val" (llvm_int 64); crucible_points_to ptr (crucible_term valprime); }; -crucible_llvm_verify_x86 m "./test" "addvar" [] false addvar_setup; \ No newline at end of file +crucible_llvm_verify_x86 m "./test" "addvar" [] false addvar_setup w4; \ No newline at end of file From f679f1a943dcdb833fb2fa6bd9c9df1c2cece726 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Thu, 18 Jun 2020 15:57:57 -0400 Subject: [PATCH 4/4] No tactics in x86 tests, yet --- intTests/test_llvm_x86_01/test.saw | 2 +- intTests/test_llvm_x86_02/test.saw | 2 +- intTests/test_llvm_x86_03/test.saw | 2 +- intTests/test_llvm_x86_04/test.saw | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/intTests/test_llvm_x86_01/test.saw b/intTests/test_llvm_x86_01/test.saw index 55a6c203a2..6550344cd5 100644 --- a/intTests/test_llvm_x86_01/test.saw +++ b/intTests/test_llvm_x86_01/test.saw @@ -11,7 +11,7 @@ let foo_setup = do { val <- crucible_fresh_var "val'" (llvm_int 64); crucible_points_to ptr (crucible_term val); }; -foo_method_spec <- crucible_llvm_verify_x86 m "./test" "foo" [] false foo_setup w4; +foo_method_spec <- crucible_llvm_verify_x86 m "./test" "foo" [] false foo_setup; let bar_setup = do { crucible_execute_func []; diff --git a/intTests/test_llvm_x86_02/test.saw b/intTests/test_llvm_x86_02/test.saw index 682ff36449..33408348ba 100644 --- a/intTests/test_llvm_x86_02/test.saw +++ b/intTests/test_llvm_x86_02/test.saw @@ -11,4 +11,4 @@ let increment_setup = do { crucible_points_to ptr (crucible_term valprime); crucible_postcond {{ valprime == val }}; }; -fails (crucible_llvm_verify_x86 m "./test" "increment" [] false increment_setup w4); \ No newline at end of file +fails (crucible_llvm_verify_x86 m "./test" "increment" [] false increment_setup); \ No newline at end of file diff --git a/intTests/test_llvm_x86_03/test.saw b/intTests/test_llvm_x86_03/test.saw index d44a3e3adb..56bc887a9d 100644 --- a/intTests/test_llvm_x86_03/test.saw +++ b/intTests/test_llvm_x86_03/test.saw @@ -6,4 +6,4 @@ let test_setup = do { crucible_execute_func []; crucible_return (crucible_term {{ 1 : [64] }}); }; -fails (crucible_llvm_verify_x86 m "./test" "foo" [] false test_setup w4); \ No newline at end of file +fails (crucible_llvm_verify_x86 m "./test" "foo" [] false test_setup); \ No newline at end of file diff --git a/intTests/test_llvm_x86_04/test.saw b/intTests/test_llvm_x86_04/test.saw index f5c6fbf544..2b6e06befb 100644 --- a/intTests/test_llvm_x86_04/test.saw +++ b/intTests/test_llvm_x86_04/test.saw @@ -16,4 +16,4 @@ let addvar_setup = do { valprime <- crucible_fresh_var "_val" (llvm_int 64); crucible_points_to ptr (crucible_term valprime); }; -crucible_llvm_verify_x86 m "./test" "addvar" [] false addvar_setup w4; \ No newline at end of file +crucible_llvm_verify_x86 m "./test" "addvar" [] false addvar_setup; \ No newline at end of file