diff --git a/CHANGES.md b/CHANGES.md index fdc01b341a..3fe9085243 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -40,6 +40,13 @@ as with `llvm_field`, debug symbols are required for `llvm_union` to work correctly. +* A new highly experimental `llvm_verify_fixpoint_x86` function that + allows partial correctness verification of loops using loop + invariants instead of full symbolic unrolling. Only certain very simple + styles of loops can currently be accommodated, and the user is + required to provide a term that describes how the live variables in + the loop evolve over an iteration. + # Version 0.9 ## New Features diff --git a/deps/crucible b/deps/crucible index e1308319ee..d18505d1ad 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5 +Subproject commit d18505d1ad1fe03e142371359852b5f52ea0b1f0 diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index 7f5267fb45..d05b6f99ed 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -7,7 +7,7 @@ WORKDIR /saw-script RUN mkdir -p /saw-script && \ git clone https://github.com/GaloisInc/aws-lc-verification.git && \ cd aws-lc-verification && \ - git checkout 7acbcfadd2e040b63cc33e8143e3f8e972408288 && \ + git checkout 1dcf4258305ce17592fb5b90a1c7b638e6bdff9e && \ git config --file=.gitmodules submodule.src.url https://github.com/awslabs/aws-lc && \ git submodule sync && \ git submodule update --init diff --git a/s2nTests/scripts/awslc-entrypoint.sh b/s2nTests/scripts/awslc-entrypoint.sh index 62ca1eb26f..afe2953913 100755 --- a/s2nTests/scripts/awslc-entrypoint.sh +++ b/s2nTests/scripts/awslc-entrypoint.sh @@ -3,6 +3,7 @@ set -xe cd /saw-script/aws-lc-verification/SAW ./scripts/install.sh +rm bin/saw cp /saw-bin/saw bin/saw cp /saw-bin/abc bin/abc diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 24770eda78..e95786b426 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -22,9 +22,11 @@ Stability : provisional {-# Language ConstraintKinds #-} {-# Language GeneralizedNewtypeDeriving #-} {-# Language TemplateHaskell #-} +{-# Language ViewPatterns #-} module SAWScript.Crucible.LLVM.X86 ( llvm_verify_x86 + , llvm_verify_fixpoint_x86 , defaultStackBaseAlign ) where @@ -46,6 +48,7 @@ import qualified Data.Set as Set import Data.Text (Text) import Data.Text.Encoding (decodeUtf8, encodeUtf8) import Data.Time.Clock (getCurrentTime, diffUTCTime) +import qualified Data.List as List import qualified Data.Map as Map import Data.Map (Map) import Data.Maybe @@ -53,12 +56,15 @@ import Data.Maybe 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.Context hiding (view) +import Data.Parameterized.Context hiding (view, zipWithM) import Verifier.SAW.CryptolEnv import Verifier.SAW.FiniteValue import Verifier.SAW.Name (toShortName) +import Verifier.SAW.Prelude +import Verifier.SAW.Recognizer import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm @@ -113,6 +119,7 @@ import qualified Lang.Crucible.LLVM.Extension as C.LLVM 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.Translation as C.LLVM import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM @@ -297,7 +304,36 @@ llvm_verify_x86 :: LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> ProofScript () {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.ProvedSpec) -llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic +llvm_verify_x86 llvmModule path nm globsyms checkSat = + llvm_verify_x86_common llvmModule path nm globsyms checkSat Nothing + +-- | 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 :: + 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 -} -> + TypedTerm {- ^ 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 llvmModule path nm globsyms checkSat f = + llvm_verify_x86_common llvmModule path nm globsyms checkSat (Just f) + +llvm_verify_x86_common :: + 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 -} -> + Maybe TypedTerm -> + 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 | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @64) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do start <- io getCurrentTime @@ -460,7 +496,14 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se else pure [] - let execFeatures = psatf + simpleLoopFixpointFeature <- + case maybeFixpointFunc of + Nothing -> return [] + Just func -> + do f <- liftIO (setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func) + return [f] + + let execFeatures = simpleLoopFixpointFeature ++ psatf liftIO $ C.executeCrucible execFeatures initial >>= \case C.FinishedResult{} -> pure () @@ -484,6 +527,79 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se | otherwise = fail "LLVM module must be 64-bit" + + +setupSimpleLoopFixpointFeature :: + ( sym ~ W4.B.ExprBuilder n st fs + , C.IsSymInterface sym + , ?memOpts::C.LLVM.MemOptions + , C.LLVM.HasLLVMAnn sym + ) => + sym -> + SharedContext -> + SAWCoreState n -> + C.CFG ext blocks init ret -> + C.GlobalVar C.LLVM.Mem -> + TypedTerm -> + IO (C.ExecutionFeature p sym ext rtp) + +setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func = + Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar fixpoint_func + + where + fixpoint_func fixpoint_substitution condition = + do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution + let body_exprs = map (mapSome $ Crucible.LLVM.Fixpoint.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.Fixpoint.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.Fixpoint.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 2b11857fb3..93dc3e3118 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -2728,6 +2728,15 @@ primitives = Map.fromList Experimental [ "Legacy alternative name for `llvm_verify_x86`." ] + , prim "llvm_verify_fixpoint_x86" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> Term -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec" + (pureVal llvm_verify_fixpoint_x86) + 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