Merge pull request #1553 from GaloisInc/simple-loop-fixpoint2

Simple loop fixpoint2

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

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

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
 

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,19 +48,23 @@ 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
 
 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
 

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