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 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 diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 7eccaba3f1..76c15dd351 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_x86_with_invariant , defaultStackBaseAlign ) where @@ -60,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 @@ -69,6 +71,7 @@ import Verifier.SAW.Prelude import Verifier.SAW.Recognizer import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm +import Verifier.SAW.SCTypeCheck (scTypeCheck) import Verifier.SAW.Simulator.What4.ReturnTrip @@ -86,7 +89,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 +108,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 +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.SimpleLoopInvariant as SimpleInvariant import qualified Lang.Crucible.LLVM.Translation as C.LLVM import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM @@ -308,7 +312,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 +328,29 @@ 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_x86_with_invariant :: + 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, 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_x86_with_invariant llvmModule path nm globsyms checkSat (loopName,loopNum,f) = + llvm_verify_x86_common llvmModule path nm globsyms checkSat + (SimpleInvariant loopName loopNum f) + +data FixpointSelect + = NoFixpoint + | SimpleFixpoint TypedTerm + | SimpleInvariant String Integer TypedTerm llvm_verify_x86_common :: Some LLVMModule {- ^ Module to associate with method spec -} -> @@ -332,11 +358,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 +542,23 @@ 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] + SimpleInvariant loopFixpointSymbol loopNum 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 let printFn = printOutLn opts Info + f <- liftIO (setupSimpleLoopInvariantFeature sym printFn loopNum + sc sawst mdMap loopcfg mvar func) + return [f] let execFeatures = simpleLoopFixpointFeature ++ psatf @@ -553,6 +591,7 @@ setupSimpleLoopFixpointFeature :: , C.IsSymInterface sym , ?memOpts::C.LLVM.MemOptions , C.LLVM.HasLLVMAnn sym + , C.IsSyntaxExtension ext ) => sym -> SharedContext -> @@ -619,6 +658,117 @@ 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 + , n ~ GlobalNonceGenerator + , ?memOpts::C.LLVM.MemOptions + , C.LLVM.HasLLVMAnn sym + , C.IsSyntaxExtension ext + ) => + sym -> + (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 {- ^ user-provided invariant term -} -> + IO (C.ExecutionFeature p sym ext rtp) + +setupSimpleLoopInvariantFeature sym printFn loopNum sc sawst mdMap cfg mvar func = + SimpleInvariant.simpleLoopInvariant sym loopNum cfg mvar invariant_func + + where + invariant_func phase implicit_params invariant_substitution = + 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) + && 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 + initial_exprs <- + forM subst_pairs $ + \ (MapF.Pair _var (SimpleInvariant.InvariantEntry initVal _current)) -> + toSC sym sawst initVal + current_exprs <- + forM subst_pairs $ + \ (MapF.Pair _var (SimpleInvariant.InvariantEntry _init current)) -> + toSC sym sawst current + + 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 -> + do printFn (show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts x)) + 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 + 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 invariant must return a boolean value, but got:" + , show (ppTerm Verifier.SAW.SharedTerm.defaultPPOpts tp) + -- TODO, get ppOpts from the right place + ] + b <- bindSAWTerm sym sawst W4.BaseBoolRepr inv + + -- Add goal metadata for the initial and inductive invariants + case phase of + SimpleInvariant.HypotheticalInvariant -> return b + SimpleInvariant.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' + SimpleInvariant.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 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 1ff78d2d61..b8f92b2c99 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3180,6 +3180,41 @@ primitives = Map.fromList , "the live variables in the loop evolve as the loop computes." ] + , prim "llvm_verify_x86_with_invariant" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Int, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" + (pureVal llvm_verify_x86_with_invariant) + Experimental + [ "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. 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." + ] + , prim "enable_x86_what4_hash_consing" "TopLevel ()" (pureVal enable_x86_what4_hash_consing) Experimental