From 3a64f77a81f769ed2b9e38977f1f7cbe8d7ae748 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 8 Aug 2022 15:02:26 -0700 Subject: [PATCH 01/12] bump crucible to current master --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 8ab240b1e4..7501d6b62b 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 8ab240b1e45aae393d8685a5a914c6f611857b57 +Subproject commit 7501d6b62be53fec0a1da4d92749c300c19da23a From 4042b5367da658df113c1f760c03b271731670cb Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Thu, 14 Jul 2022 10:49:57 -0700 Subject: [PATCH 02/12] WIP, install the new loop fixpoint feature --- src/SAWScript/Crucible/LLVM/X86.hs | 170 +++++++++++++++++++++++++++-- src/SAWScript/Interpreter.hs | 9 ++ 2 files changed, 171 insertions(+), 8 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 7eccaba3f1..c49722f512 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -27,6 +27,7 @@ Stability : provisional module SAWScript.Crucible.LLVM.X86 ( llvm_verify_x86 , llvm_verify_fixpoint_x86 + , llvm_verify_fixpoint_x86_ex , defaultStackBaseAlign ) where @@ -69,6 +70,7 @@ import Verifier.SAW.Prelude import Verifier.SAW.Recognizer import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm +import Verifier.SAW.SCTypeCheck (scTypeCheckError) import Verifier.SAW.Simulator.What4.ReturnTrip @@ -86,7 +88,6 @@ import qualified SAWScript.Crucible.Common as Common 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 hiding (LLVM) import SAWScript.Crucible.LLVM.ResolveSetupValue @@ -106,6 +107,7 @@ import qualified Lang.Crucible.Analysis.Postdom as C import qualified Lang.Crucible.Backend as C import qualified Lang.Crucible.Backend.Online as C import qualified Lang.Crucible.CFG.Core as C +import qualified Lang.Crucible.CFG.Extension as C import qualified Lang.Crucible.FunctionHandle as C import qualified Lang.Crucible.Simulator.EvalStmt as C import qualified Lang.Crucible.Simulator.ExecutionTree as C @@ -123,6 +125,7 @@ import qualified Lang.Crucible.LLVM.Intrinsics as C.LLVM import qualified Lang.Crucible.LLVM.MemModel as C.LLVM import qualified Lang.Crucible.LLVM.MemType as C.LLVM import qualified Lang.Crucible.LLVM.SimpleLoopFixpoint as Crucible.LLVM.Fixpoint +import qualified Lang.Crucible.LLVM.SimpleLoopFixpoint2 as Crucible.LLVM.Fixpoint2 import qualified Lang.Crucible.LLVM.Translation as C.LLVM import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM @@ -308,7 +311,7 @@ llvm_verify_x86 :: ProofScript () {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.ProvedSpec) llvm_verify_x86 llvmModule path nm globsyms checkSat = - llvm_verify_x86_common llvmModule path nm globsyms checkSat Nothing + llvm_verify_x86_common llvmModule path nm globsyms checkSat NoFixpoint -- | Verify that an x86_64 function (following the System V AMD64 ABI) conforms -- to an LLVM specification. This allows for compositional verification of LLVM @@ -324,7 +327,28 @@ llvm_verify_fixpoint_x86 :: ProofScript () {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.ProvedSpec) llvm_verify_fixpoint_x86 llvmModule path nm globsyms checkSat f = - llvm_verify_x86_common llvmModule path nm globsyms checkSat (Just f) + llvm_verify_x86_common llvmModule path nm globsyms checkSat (SimpleFixpoint f) + +-- | Verify that an x86_64 function (following the System V AMD64 ABI) conforms +-- to an LLVM specification. This allows for compositional verification of LLVM +-- functions that call x86_64 functions (but not the other way around). +llvm_verify_fixpoint_x86_ex :: + Some LLVMModule {- ^ Module to associate with method spec -} -> + FilePath {- ^ Path to ELF file -} -> + String {- ^ Function's symbol in ELF file -} -> + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + Bool {- ^ Whether to enable path satisfiability checking -} -> + (String, TypedTerm) {- ^ Name of the looping symbol, and function specifying the loop -} -> + LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> + ProofScript () {- ^ Tactic used to use when discharging goals -} -> + TopLevel (SomeLLVM MS.ProvedSpec) +llvm_verify_fixpoint_x86_ex llvmModule path nm globsyms checkSat (loopnm,f) = + llvm_verify_x86_common llvmModule path nm globsyms checkSat (SimpleFixpoint2 loopnm f) + +data FixpointSelect + = NoFixpoint + | SimpleFixpoint TypedTerm + | SimpleFixpoint2 String TypedTerm llvm_verify_x86_common :: Some LLVMModule {- ^ Module to associate with method spec -} -> @@ -332,11 +356,11 @@ llvm_verify_x86_common :: String {- ^ Function's symbol in ELF file -} -> [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> Bool {- ^ Whether to enable path satisfiability checking -} -> - Maybe TypedTerm -> + FixpointSelect -> LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> ProofScript () {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.ProvedSpec) -llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat maybeFixpointFunc setup tactic +llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat fixpointSelect setup tactic | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @64) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do start <- io getCurrentTime @@ -516,11 +540,21 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec pure [] simpleLoopFixpointFeature <- - case maybeFixpointFunc of - Nothing -> return [] - Just func -> + case fixpointSelect of + NoFixpoint -> return [] + SimpleFixpoint func -> do f <- liftIO (setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func) return [f] + SimpleFixpoint2 loopFixpointSymbol func -> + do (loopaddr :: Macaw.MemSegmentOff 64) <- + case findSymbols (symMap relf) . encodeUtf8 $ Text.pack loopFixpointSymbol of + (loopaddr:_) -> pure loopaddr + _ -> fail $ mconcat ["Could not find symbol \"", nm, "\""] + case Map.lookup loopaddr cfgs of + Nothing -> throwX86 $ "Unable to discover looping CFG from address " <> show loopaddr + Just (C.SomeCFG loopcfg) -> + do f <- liftIO (setupSimpleLoopFixpointFeature2 sym sc sawst loopcfg mvar func) + return [f] let execFeatures = simpleLoopFixpointFeature ++ psatf @@ -553,6 +587,7 @@ setupSimpleLoopFixpointFeature :: , C.IsSymInterface sym , ?memOpts::C.LLVM.MemOptions , C.LLVM.HasLLVMAnn sym + , C.IsSyntaxExtension ext ) => sym -> SharedContext -> @@ -619,6 +654,125 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = return (result_substitution, result_condition) +setupSimpleLoopFixpointFeature2 :: + ( sym ~ W4.B.ExprBuilder n st fs + , C.IsSymInterface sym + , ?memOpts::C.LLVM.MemOptions + , C.LLVM.HasLLVMAnn sym + , C.IsSyntaxExtension ext + ) => + sym -> + SharedContext -> + SAWCoreState n -> + C.CFG ext blocks init ret -> + C.GlobalVar C.LLVM.Mem -> + TypedTerm -> + IO (C.ExecutionFeature p sym ext rtp) + +setupSimpleLoopFixpointFeature2 sym sc sawst cfg mvar func = + Crucible.LLVM.Fixpoint2.simpleLoopFixpoint sym cfg mvar invariant_func + + where + invariant_func implicit_params invariant_substitution = + do let subst_pairs = reverse (MapF.toList invariant_substitution) + let filtered_implicit_params = filter + (\(Some variable) -> + not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)) + implicit_params + body_tms <- mapM (viewSome $ toSC sym sawst) filtered_implicit_params + implicit_params' <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet body_tms + initial_exprs <- + forM subst_pairs $ + \ (MapF.Pair _var (Crucible.LLVM.Fixpoint2.FixpointEntry initVal _current)) -> + toSC sym sawst initVal + current_exprs <- + forM subst_pairs $ + \ (MapF.Pair _var (Crucible.LLVM.Fixpoint2.FixpointEntry _init current)) -> + toSC sym sawst current + + initial_tuple <- scTuple sc initial_exprs + current_tuple <- scTuple sc current_exprs + + putStrLn "Loop invariant implicit parameters!" + forM_ implicit_params' (\x -> putStrLn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts x))) + + inv <- scApplyAll sc (ttTerm func) (implicit_params' ++ [initial_tuple, current_tuple]) + + -- check that the produced term is type-correct + tp <- scTypeCheckError sc inv + ok <- scConvertible sc True tp =<< scBoolType sc + unless ok $ + fail $ unlines [ "Loop invaraiant must return a boolean value, but got:" + , show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp) -- TODO, get ppOpts from the right place + ] + bindSAWTerm sym sawst W4.BaseBoolRepr inv + +{- +putStrLn "Invariant types!" + forM_ (MapF.toList fixpoint_substitution) $ \(MapF.Pair hd _body) -> + putStrLn (show (W4.exprType hd)) + b <- W4.freshConstant sym (W4.safeSymbol "loop_invariant") W4.BaseBoolRepr + return b +-} + +{- + + do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution + let body_exprs = map (mapSome $ Crucible.LLVM.Fixpoint2.bodyValue) (MapF.elems fixpoint_substitution) + let uninterpreted_constants = foldMap + (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) + (Some condition : body_exprs) + let filtered_uninterpreted_constants = Set.toList $ Set.filter + (\(Some variable) -> + not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)) + uninterpreted_constants + body_tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants + implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet body_tms + + arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> + toSC sym sawst $ Crucible.LLVM.Fixpoint2.headerValue fixpoint_entry + applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ arguments + applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i -> + scTupleSelector sc applied_func i (length fixpoint_substitution_as_list) + result_substitution <- MapF.fromList <$> zipWithM + (\(MapF.Pair variable _) applied_func_selector -> + MapF.Pair variable <$> bindSAWTerm sym sawst (W4.exprType variable) applied_func_selector) + fixpoint_substitution_as_list + applied_func_selectors + + explicit_parameters <- forM fixpoint_substitution_as_list $ \(MapF.Pair variable _) -> + toSC sym sawst variable + inner_func <- case asConstant (ttTerm func) of + Just (_, Just (asApplyAll -> (isGlobalDef "Prelude.fix" -> Just (), [_, inner_func]))) -> + return inner_func + _ -> fail $ "not Prelude.fix: " ++ showTerm (ttTerm func) + func_body <- betaNormalize sc + =<< scApplyAll sc inner_func ((ttTerm func) : (implicit_parameters ++ explicit_parameters)) + + step_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> + toSC sym sawst $ Crucible.LLVM.Fixpoint2.bodyValue fixpoint_entry + tail_applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ step_arguments + explicit_parameters_tuple <- scTuple sc explicit_parameters + let lhs = Prelude.last step_arguments + w <- scNat sc 64 + rhs <- scBvMul sc w (head implicit_parameters) =<< scBvNat sc w =<< scNat sc 128 + loop_condition <- scBvULt sc w lhs rhs + output_tuple_type <- scTupleType sc =<< mapM (scTypeOf sc) explicit_parameters + loop_body <- scIte sc output_tuple_type loop_condition tail_applied_func explicit_parameters_tuple + + induction_step_condition <- scEq sc loop_body func_body + result_condition <- bindSAWTerm sym sawst W4.BaseBoolRepr induction_step_condition + + return (result_substitution, result_condition) +-} + + -------------------------------------------------------------------------------- -- ** Computing the CFG diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 1ff78d2d61..c154c0b053 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3180,6 +3180,15 @@ primitives = Map.fromList , "the live variables in the loop evolve as the loop computes." ] + , prim "llvm_verify_fixpoint_x86_ex" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" + (pureVal llvm_verify_fixpoint_x86_ex) + Experimental + [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties" + , "involving simple loops with the help of a user-provided term that describes how" + , "the live variables in the loop evolve as the loop computes." + ] + , prim "enable_x86_what4_hash_consing" "TopLevel ()" (pureVal enable_x86_what4_hash_consing) Experimental From 8157e0f26ff44a4feb648504e0e3d528fc002327 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Wed, 20 Jul 2022 09:48:44 -0700 Subject: [PATCH 03/12] Tweaks to the simple loop fixpoint2 feature --- src/SAWScript/Crucible/LLVM/X86.hs | 33 +++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 10 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index c49722f512..406d13aae5 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -70,7 +70,7 @@ import Verifier.SAW.Prelude import Verifier.SAW.Recognizer import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm -import Verifier.SAW.SCTypeCheck (scTypeCheckError) +import Verifier.SAW.SCTypeCheck (scTypeCheck) import Verifier.SAW.Simulator.What4.ReturnTrip @@ -676,11 +676,13 @@ setupSimpleLoopFixpointFeature2 sym sc sawst cfg mvar func = invariant_func implicit_params invariant_substitution = do let subst_pairs = reverse (MapF.toList invariant_substitution) let filtered_implicit_params = filter - (\(Some variable) -> + (\ (Some variable) -> not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) - && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)) + && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cnoSatisfyingWrite" $ show $ W4.printSymExpr variable) + ) implicit_params body_tms <- mapM (viewSome $ toSC sym sawst) filtered_implicit_params implicit_params' <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet body_tms @@ -697,17 +699,28 @@ setupSimpleLoopFixpointFeature2 sym sc sawst cfg mvar func = current_tuple <- scTuple sc current_exprs putStrLn "Loop invariant implicit parameters!" - forM_ implicit_params' (\x -> putStrLn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts x))) + forM_ implicit_params' $ \x -> + do putStrLn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts x)) + tp <- scTypeOf sc x + putStrLn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp)) inv <- scApplyAll sc (ttTerm func) (implicit_params' ++ [initial_tuple, current_tuple]) -- check that the produced term is type-correct - tp <- scTypeCheckError sc inv - ok <- scConvertible sc True tp =<< scBoolType sc - unless ok $ - fail $ unlines [ "Loop invaraiant must return a boolean value, but got:" - , show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp) -- TODO, get ppOpts from the right place - ] + res <- scTypeCheck sc Nothing inv + case res of + Left _tcErr -> + do tpType <- scTypeOf sc initial_tuple + fail $ unlines [ "Loop invariant has incorrect type! State tuple has type:" + , show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tpType) + ] + Right tp -> + do ok <- scConvertible sc True tp =<< scBoolType sc + unless ok $ + fail $ unlines [ "Loop invaraiant must return a boolean value, but got:" + , show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp) + -- TODO, get ppOpts from the right place + ] bindSAWTerm sym sawst W4.BaseBoolRepr inv {- From 7a45455e08eb51476cf74813181ca7b2672c08ac Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Mon, 25 Jul 2022 13:06:17 -0700 Subject: [PATCH 04/12] Add tags to goals resulting from the loop invariant feature. Delete some dead code. --- src/SAWScript/Crucible/LLVM/X86.hs | 100 ++++++++++------------------- 1 file changed, 33 insertions(+), 67 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 406d13aae5..6b1cb83b52 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -61,6 +61,7 @@ import qualified Text.LLVM.AST as LLVM import Data.Parameterized.Some import qualified Data.Parameterized.Map as MapF import Data.Parameterized.NatRepr +import Data.Parameterized.Nonce (GlobalNonceGenerator) import Data.Parameterized.Context hiding (view, zipWithM) import Verifier.SAW.CryptolEnv @@ -553,7 +554,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec case Map.lookup loopaddr cfgs of Nothing -> throwX86 $ "Unable to discover looping CFG from address " <> show loopaddr Just (C.SomeCFG loopcfg) -> - do f <- liftIO (setupSimpleLoopFixpointFeature2 sym sc sawst loopcfg mvar func) + do f <- liftIO (setupSimpleLoopFixpointFeature2 sym sc sawst mdMap loopcfg mvar func) return [f] let execFeatures = simpleLoopFixpointFeature ++ psatf @@ -657,6 +658,7 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = setupSimpleLoopFixpointFeature2 :: ( sym ~ W4.B.ExprBuilder n st fs , C.IsSymInterface sym + , n ~ GlobalNonceGenerator , ?memOpts::C.LLVM.MemOptions , C.LLVM.HasLLVMAnn sym , C.IsSyntaxExtension ext @@ -664,16 +666,17 @@ setupSimpleLoopFixpointFeature2 :: sym -> SharedContext -> SAWCoreState n -> + IORef MetadataMap -> C.CFG ext blocks init ret -> C.GlobalVar C.LLVM.Mem -> TypedTerm -> IO (C.ExecutionFeature p sym ext rtp) -setupSimpleLoopFixpointFeature2 sym sc sawst cfg mvar func = +setupSimpleLoopFixpointFeature2 sym sc sawst mdMap cfg mvar func = Crucible.LLVM.Fixpoint2.simpleLoopFixpoint sym cfg mvar invariant_func where - invariant_func implicit_params invariant_substitution = + invariant_func phase implicit_params invariant_substitution = do let subst_pairs = reverse (MapF.toList invariant_substitution) let filtered_implicit_params = filter (\ (Some variable) -> @@ -721,70 +724,33 @@ setupSimpleLoopFixpointFeature2 sym sc sawst cfg mvar func = , show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp) -- TODO, get ppOpts from the right place ] - bindSAWTerm sym sawst W4.BaseBoolRepr inv - -{- -putStrLn "Invariant types!" - forM_ (MapF.toList fixpoint_substitution) $ \(MapF.Pair hd _body) -> - putStrLn (show (W4.exprType hd)) - b <- W4.freshConstant sym (W4.safeSymbol "loop_invariant") W4.BaseBoolRepr - return b --} - -{- - - do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution - let body_exprs = map (mapSome $ Crucible.LLVM.Fixpoint2.bodyValue) (MapF.elems fixpoint_substitution) - let uninterpreted_constants = foldMap - (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) - (Some condition : body_exprs) - let filtered_uninterpreted_constants = Set.toList $ Set.filter - (\(Some variable) -> - not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) - && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) - && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) - && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable)) - uninterpreted_constants - body_tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants - implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet body_tms - - arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> - toSC sym sawst $ Crucible.LLVM.Fixpoint2.headerValue fixpoint_entry - applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ arguments - applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i -> - scTupleSelector sc applied_func i (length fixpoint_substitution_as_list) - result_substitution <- MapF.fromList <$> zipWithM - (\(MapF.Pair variable _) applied_func_selector -> - MapF.Pair variable <$> bindSAWTerm sym sawst (W4.exprType variable) applied_func_selector) - fixpoint_substitution_as_list - applied_func_selectors - - explicit_parameters <- forM fixpoint_substitution_as_list $ \(MapF.Pair variable _) -> - toSC sym sawst variable - inner_func <- case asConstant (ttTerm func) of - Just (_, Just (asApplyAll -> (isGlobalDef "Prelude.fix" -> Just (), [_, inner_func]))) -> - return inner_func - _ -> fail $ "not Prelude.fix: " ++ showTerm (ttTerm func) - func_body <- betaNormalize sc - =<< scApplyAll sc inner_func ((ttTerm func) : (implicit_parameters ++ explicit_parameters)) - - step_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) -> - toSC sym sawst $ Crucible.LLVM.Fixpoint2.bodyValue fixpoint_entry - tail_applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ step_arguments - explicit_parameters_tuple <- scTuple sc explicit_parameters - let lhs = Prelude.last step_arguments - w <- scNat sc 64 - rhs <- scBvMul sc w (head implicit_parameters) =<< scBvNat sc w =<< scNat sc 128 - loop_condition <- scBvULt sc w lhs rhs - output_tuple_type <- scTupleType sc =<< mapM (scTypeOf sc) explicit_parameters - loop_body <- scIte sc output_tuple_type loop_condition tail_applied_func explicit_parameters_tuple - - induction_step_condition <- scEq sc loop_body func_body - result_condition <- bindSAWTerm sym sawst W4.BaseBoolRepr induction_step_condition - - return (result_substitution, result_condition) --} - + b <- bindSAWTerm sym sawst W4.BaseBoolRepr inv + + -- Add goal metadata for the initial and inductive invariants + case phase of + Crucible.LLVM.Fixpoint2.HypotheticalInvariant -> return b + Crucible.LLVM.Fixpoint2.InitialInvariant -> + do (ann,b') <- W4.annotateTerm sym b + loc <- W4.getCurrentProgramLoc sym + let md = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = Set.singleton "initial loop invariant" + , MS.conditionType = "initial loop invariant" + , MS.conditionContext = "" + } + modifyIORef mdMap (Map.insert ann md) + return b' + Crucible.LLVM.Fixpoint2.InductiveInvariant -> + do (ann,b') <- W4.annotateTerm sym b + loc <- W4.getCurrentProgramLoc sym + let md = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = Set.singleton "inductive loop invariant" + , MS.conditionType = "inductive loop invariant" + , MS.conditionContext = "" + } + modifyIORef mdMap (Map.insert ann md) + return b' -------------------------------------------------------------------------------- -- ** Computing the CFG From 9d8daac354aa6739ba809f54ace320b0b692b668 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Tue, 26 Jul 2022 13:57:38 -0700 Subject: [PATCH 05/12] Pipe in the additional integer argument for the loop invariant feature. This allows users to select which (of potentially several) loops within a function they wish to install a loop invariant for. --- src/SAWScript/Crucible/LLVM/X86.hs | 18 ++++++++++-------- src/SAWScript/Interpreter.hs | 2 +- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 6b1cb83b52..84993e3c5c 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -339,17 +339,18 @@ llvm_verify_fixpoint_x86_ex :: String {- ^ Function's symbol in ELF file -} -> [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> Bool {- ^ Whether to enable path satisfiability checking -} -> - (String, TypedTerm) {- ^ Name of the looping symbol, and function specifying the loop -} -> + (String, Integer, TypedTerm) {- ^ Name of the looping symbol, and function specifying the loop -} -> LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> ProofScript () {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.ProvedSpec) -llvm_verify_fixpoint_x86_ex llvmModule path nm globsyms checkSat (loopnm,f) = - llvm_verify_x86_common llvmModule path nm globsyms checkSat (SimpleFixpoint2 loopnm f) +llvm_verify_fixpoint_x86_ex llvmModule path nm globsyms checkSat (loopName,loopNum,f) = + llvm_verify_x86_common llvmModule path nm globsyms checkSat + (SimpleFixpoint2 loopName loopNum f) data FixpointSelect = NoFixpoint | SimpleFixpoint TypedTerm - | SimpleFixpoint2 String TypedTerm + | SimpleFixpoint2 String Integer TypedTerm llvm_verify_x86_common :: Some LLVMModule {- ^ Module to associate with method spec -} -> @@ -546,7 +547,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec SimpleFixpoint func -> do f <- liftIO (setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func) return [f] - SimpleFixpoint2 loopFixpointSymbol func -> + SimpleFixpoint2 loopFixpointSymbol loopNum func -> do (loopaddr :: Macaw.MemSegmentOff 64) <- case findSymbols (symMap relf) . encodeUtf8 $ Text.pack loopFixpointSymbol of (loopaddr:_) -> pure loopaddr @@ -554,7 +555,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec case Map.lookup loopaddr cfgs of Nothing -> throwX86 $ "Unable to discover looping CFG from address " <> show loopaddr Just (C.SomeCFG loopcfg) -> - do f <- liftIO (setupSimpleLoopFixpointFeature2 sym sc sawst mdMap loopcfg mvar func) + do f <- liftIO (setupSimpleLoopFixpointFeature2 sym loopNum sc sawst mdMap loopcfg mvar func) return [f] let execFeatures = simpleLoopFixpointFeature ++ psatf @@ -664,6 +665,7 @@ setupSimpleLoopFixpointFeature2 :: , C.IsSyntaxExtension ext ) => sym -> + Integer -> SharedContext -> SAWCoreState n -> IORef MetadataMap -> @@ -672,8 +674,8 @@ setupSimpleLoopFixpointFeature2 :: TypedTerm -> IO (C.ExecutionFeature p sym ext rtp) -setupSimpleLoopFixpointFeature2 sym sc sawst mdMap cfg mvar func = - Crucible.LLVM.Fixpoint2.simpleLoopFixpoint sym cfg mvar invariant_func +setupSimpleLoopFixpointFeature2 sym loopNum sc sawst mdMap cfg mvar func = + Crucible.LLVM.Fixpoint2.simpleLoopFixpoint sym loopNum cfg mvar invariant_func where invariant_func phase implicit_params invariant_substitution = diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index c154c0b053..b892c1c12c 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3181,7 +3181,7 @@ primitives = Map.fromList ] , prim "llvm_verify_fixpoint_x86_ex" - "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Int, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" (pureVal llvm_verify_fixpoint_x86_ex) Experimental [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties" From de470992fe3c9e46a109442eef1e35bc48da634e Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 8 Aug 2022 15:30:55 -0700 Subject: [PATCH 06/12] Rename the functions binding to the new simple loop invariant feature. --- src/SAWScript/Crucible/LLVM/X86.hs | 32 +++++++++++++++--------------- src/SAWScript/Interpreter.hs | 8 ++++---- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 84993e3c5c..adfc0ac332 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -27,7 +27,7 @@ Stability : provisional module SAWScript.Crucible.LLVM.X86 ( llvm_verify_x86 , llvm_verify_fixpoint_x86 - , llvm_verify_fixpoint_x86_ex + , llvm_verify_x86_with_invariant , defaultStackBaseAlign ) where @@ -126,7 +126,7 @@ import qualified Lang.Crucible.LLVM.Intrinsics as C.LLVM import qualified Lang.Crucible.LLVM.MemModel as C.LLVM import qualified Lang.Crucible.LLVM.MemType as C.LLVM import qualified Lang.Crucible.LLVM.SimpleLoopFixpoint as Crucible.LLVM.Fixpoint -import qualified Lang.Crucible.LLVM.SimpleLoopFixpoint2 as Crucible.LLVM.Fixpoint2 +import qualified Lang.Crucible.LLVM.SimpleLoopInvariant as SimpleInvariant import qualified Lang.Crucible.LLVM.Translation as C.LLVM import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM @@ -333,7 +333,7 @@ llvm_verify_fixpoint_x86 llvmModule path nm globsyms checkSat f = -- | Verify that an x86_64 function (following the System V AMD64 ABI) conforms -- to an LLVM specification. This allows for compositional verification of LLVM -- functions that call x86_64 functions (but not the other way around). -llvm_verify_fixpoint_x86_ex :: +llvm_verify_x86_with_invariant :: Some LLVMModule {- ^ Module to associate with method spec -} -> FilePath {- ^ Path to ELF file -} -> String {- ^ Function's symbol in ELF file -} -> @@ -343,14 +343,14 @@ llvm_verify_fixpoint_x86_ex :: LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> ProofScript () {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.ProvedSpec) -llvm_verify_fixpoint_x86_ex llvmModule path nm globsyms checkSat (loopName,loopNum,f) = +llvm_verify_x86_with_invariant llvmModule path nm globsyms checkSat (loopName,loopNum,f) = llvm_verify_x86_common llvmModule path nm globsyms checkSat - (SimpleFixpoint2 loopName loopNum f) + (SimpleInvariant loopName loopNum f) data FixpointSelect = NoFixpoint | SimpleFixpoint TypedTerm - | SimpleFixpoint2 String Integer TypedTerm + | SimpleInvariant String Integer TypedTerm llvm_verify_x86_common :: Some LLVMModule {- ^ Module to associate with method spec -} -> @@ -547,7 +547,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec SimpleFixpoint func -> do f <- liftIO (setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func) return [f] - SimpleFixpoint2 loopFixpointSymbol loopNum func -> + SimpleInvariant loopFixpointSymbol loopNum func -> do (loopaddr :: Macaw.MemSegmentOff 64) <- case findSymbols (symMap relf) . encodeUtf8 $ Text.pack loopFixpointSymbol of (loopaddr:_) -> pure loopaddr @@ -555,7 +555,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec case Map.lookup loopaddr cfgs of Nothing -> throwX86 $ "Unable to discover looping CFG from address " <> show loopaddr Just (C.SomeCFG loopcfg) -> - do f <- liftIO (setupSimpleLoopFixpointFeature2 sym loopNum sc sawst mdMap loopcfg mvar func) + do f <- liftIO (setupSimpleLoopInvariantFeature sym loopNum sc sawst mdMap loopcfg mvar func) return [f] let execFeatures = simpleLoopFixpointFeature ++ psatf @@ -656,7 +656,7 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = return (result_substitution, result_condition) -setupSimpleLoopFixpointFeature2 :: +setupSimpleLoopInvariantFeature :: ( sym ~ W4.B.ExprBuilder n st fs , C.IsSymInterface sym , n ~ GlobalNonceGenerator @@ -674,8 +674,8 @@ setupSimpleLoopFixpointFeature2 :: TypedTerm -> IO (C.ExecutionFeature p sym ext rtp) -setupSimpleLoopFixpointFeature2 sym loopNum sc sawst mdMap cfg mvar func = - Crucible.LLVM.Fixpoint2.simpleLoopFixpoint sym loopNum cfg mvar invariant_func +setupSimpleLoopInvariantFeature sym loopNum sc sawst mdMap cfg mvar func = + SimpleInvariant.simpleLoopInvariant sym loopNum cfg mvar invariant_func where invariant_func phase implicit_params invariant_substitution = @@ -693,11 +693,11 @@ setupSimpleLoopFixpointFeature2 sym loopNum sc sawst mdMap cfg mvar func = implicit_params' <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet body_tms initial_exprs <- forM subst_pairs $ - \ (MapF.Pair _var (Crucible.LLVM.Fixpoint2.FixpointEntry initVal _current)) -> + \ (MapF.Pair _var (SimpleInvariant.InvariantEntry initVal _current)) -> toSC sym sawst initVal current_exprs <- forM subst_pairs $ - \ (MapF.Pair _var (Crucible.LLVM.Fixpoint2.FixpointEntry _init current)) -> + \ (MapF.Pair _var (SimpleInvariant.InvariantEntry _init current)) -> toSC sym sawst current initial_tuple <- scTuple sc initial_exprs @@ -730,8 +730,8 @@ setupSimpleLoopFixpointFeature2 sym loopNum sc sawst mdMap cfg mvar func = -- Add goal metadata for the initial and inductive invariants case phase of - Crucible.LLVM.Fixpoint2.HypotheticalInvariant -> return b - Crucible.LLVM.Fixpoint2.InitialInvariant -> + SimpleInvariant.HypotheticalInvariant -> return b + SimpleInvariant.InitialInvariant -> do (ann,b') <- W4.annotateTerm sym b loc <- W4.getCurrentProgramLoc sym let md = MS.ConditionMetadata @@ -742,7 +742,7 @@ setupSimpleLoopFixpointFeature2 sym loopNum sc sawst mdMap cfg mvar func = } modifyIORef mdMap (Map.insert ann md) return b' - Crucible.LLVM.Fixpoint2.InductiveInvariant -> + SimpleInvariant.InductiveInvariant -> do (ann,b') <- W4.annotateTerm sym b loc <- W4.getCurrentProgramLoc sym let md = MS.ConditionMetadata diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index b892c1c12c..cdfbc98e33 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3180,13 +3180,13 @@ primitives = Map.fromList , "the live variables in the loop evolve as the loop computes." ] - , prim "llvm_verify_fixpoint_x86_ex" + , prim "llvm_verify_x86_with_invariant" "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Int, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" - (pureVal llvm_verify_fixpoint_x86_ex) + (pureVal llvm_verify_x86_with_invariant) Experimental [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties" - , "involving simple loops with the help of a user-provided term that describes how" - , "the live variables in the loop evolve as the loop computes." + , "involving simple loops with the help of a user-provided loop invariant describes" + , "how the live variables in the loop evolve as the loop computes." ] , prim "enable_x86_what4_hash_consing" "TopLevel ()" From 0ee1edac1789c030fba9fcba04b5eedb8cf5d20b Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Fri, 26 Aug 2022 15:57:31 -0700 Subject: [PATCH 07/12] Better output handling for the simple loop invariant feature. The discovered implicit arguments are now printed using the correct functions, and only on verbosity level `info` or higher. --- src/SAWScript/Crucible/LLVM/X86.hs | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index adfc0ac332..9bc825e799 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -555,7 +555,9 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec case Map.lookup loopaddr cfgs of Nothing -> throwX86 $ "Unable to discover looping CFG from address " <> show loopaddr Just (C.SomeCFG loopcfg) -> - do f <- liftIO (setupSimpleLoopInvariantFeature sym loopNum sc sawst mdMap loopcfg mvar func) + do let printFn = printOutLn opts Info + f <- liftIO (setupSimpleLoopInvariantFeature sym printFn loopNum + sc sawst mdMap loopcfg mvar func) return [f] let execFeatures = simpleLoopFixpointFeature ++ psatf @@ -665,6 +667,7 @@ setupSimpleLoopInvariantFeature :: , C.IsSyntaxExtension ext ) => sym -> + (String -> IO ()) -> Integer -> SharedContext -> SAWCoreState n -> @@ -674,7 +677,7 @@ setupSimpleLoopInvariantFeature :: TypedTerm -> IO (C.ExecutionFeature p sym ext rtp) -setupSimpleLoopInvariantFeature sym loopNum sc sawst mdMap cfg mvar func = +setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func = SimpleInvariant.simpleLoopInvariant sym loopNum cfg mvar invariant_func where @@ -703,11 +706,12 @@ setupSimpleLoopInvariantFeature sym loopNum sc sawst mdMap cfg mvar func = initial_tuple <- scTuple sc initial_exprs current_tuple <- scTuple sc current_exprs - putStrLn "Loop invariant implicit parameters!" - forM_ implicit_params' $ \x -> - do putStrLn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts x)) - tp <- scTypeOf sc x - putStrLn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp)) + when (phase == SimpleInvariant.InitialInvariant) $ + do printFn "Loop invariant implicit parameters!" + forM_ implicit_params' $ \x -> + do printFn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts x)) + tp <- scTypeOf sc x + printFn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp)) inv <- scApplyAll sc (ttTerm func) (implicit_params' ++ [initial_tuple, current_tuple]) From 2867e1d1bd367b559b73c0d23f078cf150156c38 Mon Sep 17 00:00:00 2001 From: robdockins Date: Sat, 27 Aug 2022 16:22:28 -0700 Subject: [PATCH 08/12] Apply suggestions from code review Co-authored-by: Ryan Scott --- src/SAWScript/Interpreter.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index cdfbc98e33..1e6f31bddb 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3185,7 +3185,7 @@ primitives = Map.fromList (pureVal llvm_verify_x86_with_invariant) Experimental [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties" - , "involving simple loops with the help of a user-provided loop invariant describes" + , "involving simple loops with the help of a user-provided loop invariant that describes" , "how the live variables in the loop evolve as the loop computes." ] From 00d9ba37093cfbb9f7e6373d93602e269efed8d9 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Mon, 29 Aug 2022 03:55:57 -0700 Subject: [PATCH 09/12] More extensive help documentation for `llvm_verify_x86_with_invariant`. --- src/SAWScript/Interpreter.hs | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 1e6f31bddb..1ffe05217e 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3184,9 +3184,34 @@ primitives = Map.fromList "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Int, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" (pureVal llvm_verify_x86_with_invariant) Experimental - [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties" + [ "An experimental extension of 'llvm_verify_x86'. This extension can prove some properties" , "involving simple loops with the help of a user-provided loop invariant that describes" , "how the live variables in the loop evolve as the loop computes." + , "" + , "The loop invariant is provided by the tuple argument, which indicates what symbol the loop" + , "appears in (which might differ from the function the specification is for), which loop within" + , "that function to reason about (starts counting from 0), and a term that desribes the loop invariant" + , "itself. For this verification command to succeed, the loop in question must have a single entry-point," + , "must have a single back-edge, and must have a constant memory footprint." + , "" + , "The SAWCore type expected of the loop invariant will depend on the results of an analysis done" + , "on the indicated loop, which will attempt to discover what are all the loop-carried dependencies." + , "The result of this analysis will be packaged into a tuple, and any relevant top-level specification" + , "variables will be found. The expected type of the loop invariant will then be a function over all" + , "the implicit variables found, and two tuples consisting of the initial values of the loop-carried" + , "dependencies, and the current value of the loop-carried dependencies. The function should return Bool." + , "Some trial-and-error will generally be required to match the results of the analysis with a sutiable" + , "function." + , "" + , "As part of the verification process, the loop invariant will be used in several ways. First, a proof" + , "obligation will be issued upon first entry to the loop, establishing the loop invariant holds at the" + , "beginning of the loop. Second, the loop invariant is used when starting execution from the loop head" + , "to make a generic assumption that the invariant holds. Finally, the invariant is used when execution" + , "once again reaches the loop head to assert that the invariant holds inductively across the execution" + , "of the loop body." + , "" + , "Provided all the generated verification conditions are discharged, this results in a partial" + , "correctness proof for the indicated function. Note that termination is not proved via this procedure." ] , prim "enable_x86_what4_hash_consing" "TopLevel ()" From 71f15ad12438188c4c99b8327387fae9306dff21 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Mon, 29 Aug 2022 04:09:14 -0700 Subject: [PATCH 10/12] Additional comments --- src/SAWScript/Crucible/LLVM/X86.hs | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 9bc825e799..67d6d2212f 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -658,6 +658,10 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = return (result_substitution, result_condition) +-- | This procedure sets up the simple loop fixpoint feature. +-- Its main task is to massage the user-provided invariant +-- term into the form expected by the Crucible exeuction +-- feature. setupSimpleLoopInvariantFeature :: ( sym ~ W4.B.ExprBuilder n st fs , C.IsSymInterface sym @@ -667,14 +671,14 @@ setupSimpleLoopInvariantFeature :: , C.IsSyntaxExtension ext ) => sym -> - (String -> IO ()) -> - Integer -> + (String -> IO ()) {- ^ logging function -} -> + Integer {- ^ Which loop are we targeting? -} -> SharedContext -> SAWCoreState n -> IORef MetadataMap -> C.CFG ext blocks init ret -> C.GlobalVar C.LLVM.Mem -> - TypedTerm -> + TypedTerm {- ^ user-provided invariant term -} -> IO (C.ExecutionFeature p sym ext rtp) setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func = @@ -685,6 +689,10 @@ setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func do let subst_pairs = reverse (MapF.toList invariant_substitution) let filtered_implicit_params = filter (\ (Some variable) -> + -- We filter variables with the following special names from appearing as + -- implicit arguments to the loop invariant. These are basically all various + -- kinds of underspecification appearing from various underlying components + -- and don't make sense as arguments to the loop invariant. not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable) @@ -706,6 +714,8 @@ setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func initial_tuple <- scTuple sc initial_exprs current_tuple <- scTuple sc current_exprs + -- use the provided logging function to print the discovered + -- implicit parameters when (phase == SimpleInvariant.InitialInvariant) $ do printFn "Loop invariant implicit parameters!" forM_ implicit_params' $ \x -> @@ -713,6 +723,7 @@ setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func tp <- scTypeOf sc x printFn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp)) + -- actually apply the arguments to the given term inv <- scApplyAll sc (ttTerm func) (implicit_params' ++ [initial_tuple, current_tuple]) -- check that the produced term is type-correct From 207b0682f5da946c6b133f75a4cf34592f14bcd0 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Mon, 29 Aug 2022 13:47:44 -0700 Subject: [PATCH 11/12] typo, improved helpstring --- src/SAWScript/Crucible/LLVM/X86.hs | 2 +- src/SAWScript/Interpreter.hs | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 67d6d2212f..76c15dd351 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -737,7 +737,7 @@ setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func Right tp -> do ok <- scConvertible sc True tp =<< scBoolType sc unless ok $ - fail $ unlines [ "Loop invaraiant must return a boolean value, but got:" + fail $ unlines [ "Loop invariant must return a boolean value, but got:" , show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp) -- TODO, get ppOpts from the right place ] diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 1ffe05217e..b8f92b2c99 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3208,7 +3208,8 @@ primitives = Map.fromList , "beginning of the loop. Second, the loop invariant is used when starting execution from the loop head" , "to make a generic assumption that the invariant holds. Finally, the invariant is used when execution" , "once again reaches the loop head to assert that the invariant holds inductively across the execution" - , "of the loop body." + , "of the loop body. The produced proof obligations will be tagged with either the tag" + , "'initial loop invariant' or 'inductive loop invariant'." , "" , "Provided all the generated verification conditions are discharged, this results in a partial" , "correctness proof for the indicated function. Note that termination is not proved via this procedure." From 37e9f9723b922ab67f1e0633b6f5bfc682d1ee87 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Mon, 29 Aug 2022 13:57:35 -0700 Subject: [PATCH 12/12] update changelog --- CHANGES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 9bb19507d3..686d137c21 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -86,6 +86,10 @@ * The experimental and rarely-used `goal_assume` tactic has been removed. The use case it was targeting is better solved via sequents. +* A new experimental `llvm_verify_x86_with_invariant` command that + allows verification certain kinds of simple loops by using a + user-provided loop invariant. + # Version 0.9 ## New Features