Merge pull request #873 from GaloisInc/path-sat-fix

Path sat fix

Author: robdockins

deps/crucible

@@ -0,0 +1,23 @@
+#include <stdint.h>
+
+uint64_t g1(uint64_t x) {
+  int i = 0;
+  uint64_t r = x;
+  do {
+    r = r+1;
+  } while ( i++ < 3 && r == 0 );
+  return r;
+}
+
+// NB the termination of the following loop
+// is a bit tricky because of the interaction
+// between short-cutting '&&' and the 'i++'
+// expression.
+uint64_t g2(uint64_t x) {
+  int i = 0;
+  uint64_t r = x;
+  do {
+    r = r+1;
+  } while ( r == 0 && i++ < 3 );
+  return r;
+}

deps/what4

@@ -0,0 +1,12 @@
+m <- llvm_load_module "termination.bc";
+
+let g_spec = do {
+  x <- crucible_fresh_var "x" (llvm_int 64);
+  crucible_execute_func [crucible_term x];
+  };
+
+crucible_llvm_verify m "g1" [] false g_spec z3;
+
+// NB: path sat checking is required for this
+// to terminate in a reasonable time
+crucible_llvm_verify m "g2" [] true g_spec z3;

intTests/test0061_path_sat/termination.bc

@@ -0,0 +1 @@
+$SAW test.saw

intTests/test0061_path_sat/termination.c

@@ -707,6 +707,10 @@ setupCrucibleContext bic opts jclass =
      let gen = globalNonceGenerator
      sym <- io $ Crucible.newSAWCoreBackend W4.FloatRealRepr sc gen
      io $ CJ.setSimulatorVerbosity (simVerbose opts) sym
+
+     -- TODO! there's a lot of options setup we need to replicate
+     --  from SAWScript.Crucible.LLVM.Builtins
+
      return JVMCrucibleContext { _jccJVMClass = jclass
                                , _jccCodebase = cb
                                , _jccBackend = sym

intTests/test0061_path_sat/test.saw

@@ -132,6 +132,7 @@ import qualified What4.Expr.Builder as W4
 
 -- crucible
 import qualified Lang.Crucible.Backend as Crucible
+import qualified Lang.Crucible.Backend.Online as Crucible
 import qualified Lang.Crucible.Backend.SAWCore as CrucibleSAW
 import qualified Lang.Crucible.CFG.Core as Crucible
 import qualified Lang.Crucible.CFG.Extension as Crucible
@@ -269,7 +270,7 @@ crucible_llvm_verify ::
   TopLevel (SomeLLVM MS.CrucibleMethodSpecIR)
 crucible_llvm_verify bic opts (Some lm) nm lemmas checkSat setup tactic =
   do lemmas' <- checkModuleCompatibility lm lemmas
-     withMethodSpec bic opts lm nm setup $ \cc method_spec ->
+     withMethodSpec bic opts checkSat lm nm setup $ \cc method_spec ->
        do (res_method_spec, _) <- verifyMethodSpec bic opts cc method_spec lemmas' checkSat tactic Nothing
           returnProof $ SomeLLVM res_method_spec
 
@@ -281,7 +282,7 @@ crucible_llvm_unsafe_assume_spec ::
   LLVMCrucibleSetupM () {- ^ Boundary specification -} ->
   TopLevel (SomeLLVM MS.CrucibleMethodSpecIR)
 crucible_llvm_unsafe_assume_spec bic opts (Some lm) nm setup =
-  withMethodSpec bic opts lm nm setup $ \_ method_spec ->
+  withMethodSpec bic opts False lm nm setup $ \_ method_spec ->
   do printOutLnTop Info $
        unwords ["Assume override", (method_spec ^. csName)]
      returnProof $ SomeLLVM method_spec
@@ -298,7 +299,7 @@ crucible_llvm_array_size_profile ::
 crucible_llvm_array_size_profile assume bic opts (Some lm) nm lemmas setup = do
   cell <- io $ newIORef (Map.empty :: Map Text.Text [Crucible.FunctionProfile])
   lemmas' <- checkModuleCompatibility lm lemmas
-  withMethodSpec bic opts lm nm setup $ \cc ms -> do
+  withMethodSpec bic opts False lm nm setup $ \cc ms -> do
     void . verifyMethodSpec bic opts cc ms lemmas' True assume $ Just cell
     profiles <- io $ readIORef cell
     pure . fmap (\(fnm, prof) -> (Text.unpack fnm, prof)) $ Map.toList profiles
@@ -310,13 +311,13 @@ crucible_llvm_compositional_extract ::
   String ->
   String ->
   [SomeLLVM MS.CrucibleMethodSpecIR] ->
-  Bool ->
+  Bool {- ^ check sat -} ->
   LLVMCrucibleSetupM () ->
   ProofScript SatResult ->
   TopLevel (SomeLLVM MS.CrucibleMethodSpecIR)
 crucible_llvm_compositional_extract bic opts (Some lm) nm func_name lemmas checkSat setup tactic =
   do lemmas' <- checkModuleCompatibility lm lemmas
-     withMethodSpec bic opts lm nm setup $ \cc method_spec ->
+     withMethodSpec bic opts checkSat lm nm setup $ \cc method_spec ->
        do let value_input_parameters = mapMaybe
                 (\(_, setup_value) -> setupValueAsExtCns setup_value)
                 (Map.elems $ method_spec ^. MS.csArgBindings)
@@ -447,13 +448,14 @@ checkModuleCompatibility llvmModule = foldM step []
 withMethodSpec ::
   BuiltinContext   ->
   Options          ->
+  Bool {- ^ path sat -} ->
   LLVMModule arch ->
   String            {- ^ Name of the function -} ->
   LLVMCrucibleSetupM () {- ^ Boundary specification -} ->
   ((?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
    LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> TopLevel a) ->
   TopLevel a
-withMethodSpec bic opts lm nm setup action =
+withMethodSpec bic opts pathSat lm nm setup action =
   do (nm', parent) <- resolveSpecName nm
      let edef = findDefMaybeStatic (modAST lm) nm'
      let edecl = findDecl (modAST lm) nm'
@@ -468,7 +470,7 @@ withMethodSpec bic opts lm nm setup action =
 
      Crucible.llvmPtrWidth (mtrans ^. Crucible.transContext) $ \_ ->
        fmap NE.head $ forM defOrDecls $ \defOrDecl ->
-         setupLLVMCrucibleContext bic opts lm $ \cc ->
+         setupLLVMCrucibleContext bic opts pathSat lm $ \cc ->
            do let sym = cc^.ccBackend
 
               pos <- getPosition
@@ -1204,11 +1206,12 @@ verifyPoststate opts sc cc mspec env0 globals ret =
 setupLLVMCrucibleContext ::
   BuiltinContext ->
   Options ->
+  Bool {- ^ enable path sat checking -} ->
   LLVMModule arch ->
   ((?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
    LLVMCrucibleContext arch -> TopLevel a) ->
   TopLevel a
-setupLLVMCrucibleContext bic opts lm action =
+setupLLVMCrucibleContext bic opts pathSat lm action =
   do halloc <- getHandleAlloc
      let llvm_mod = modAST lm
      let mtrans = modTrans lm
@@ -1234,6 +1237,10 @@ setupLLVMCrucibleContext bic opts lm action =
                cacheTermsSetting <- W4.getOptionSetting W4.cacheTerms cfg
                _ <- W4.setOpt cacheTermsSetting what4HashConsing
 
+               -- enable online solver interactions if path sat checking is on
+               enableOnlineSetting <- W4.getOptionSetting Crucible.enableOnlineBackend cfg
+               _ <- W4.setOpt enableOnlineSetting pathSat
+
                W4.extendConfig
                  [ W4.opt
                      enableSMTArrayMemoryModel
@@ -1447,7 +1454,7 @@ crucible_llvm_extract bic opts (Some lm) fn_name =
             when (any L.isAlias defTypes) $
               throwTopLevel "Type aliases are not supported by `crucible_llvm_extract`."
        Left err -> throwTopLevel (displayVerifExceptionOpts opts err)
-     setupLLVMCrucibleContext bic opts lm $ \cc ->
+     setupLLVMCrucibleContext bic opts False lm $ \cc ->
        case Map.lookup (fromString fn_name) (Crucible.cfgMap (ccLLVMModuleTrans cc)) of
          Nothing  -> throwTopLevel $ unwords ["function", fn_name, "not found"]
          Just (_,cfg) -> io $ extractFromLLVMCFG opts (biSharedContext bic) cc cfg
@@ -1461,7 +1468,7 @@ crucible_llvm_cfg ::
 crucible_llvm_cfg bic opts (Some lm) fn_name =
   do let ctx = modTrans lm ^. Crucible.transContext
      let ?lc = ctx^.Crucible.llvmTypeCtx
-     setupLLVMCrucibleContext bic opts lm $ \cc ->
+     setupLLVMCrucibleContext bic opts False lm $ \cc ->
        case Map.lookup (fromString fn_name) (Crucible.cfgMap (ccLLVMModuleTrans cc)) of
          Nothing  -> throwTopLevel $ unwords ["function", fn_name, "not found"]
          Just (_,cfg) -> return (LLVM_CFG cfg)

intTests/test0061_path_sat/test.sh

@@ -120,6 +120,7 @@ import           Data.Parameterized.Some (Some(Some))
 import qualified Data.Parameterized.Map as MapF
 
 import qualified What4.Expr.Builder as B
+import           What4.Protocol.Online (OnlineSolver)
 import           What4.ProgramLoc (ProgramLoc)
 
 import qualified Lang.Crucible.Backend.SAWCore as Crucible
@@ -140,6 +141,7 @@ import           Verifier.SAW.Rewriter (Simpset)
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.TypedTerm
 
+
 --------------------------------------------------------------------------------
 -- ** Language features
 
@@ -291,7 +293,8 @@ showLLVMModule (LLVMModule name m _) =
 --------------------------------------------------------------------------------
 -- ** Ghost state
 
-instance Crucible.IntrinsicClass (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) MS.GhostValue where
+instance OnlineSolver solver =>
+    Crucible.IntrinsicClass (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) MS.GhostValue where
   type Intrinsic (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) MS.GhostValue ctx = TypedTerm
   muxIntrinsic sym _ _namerep _ctx prd thn els =
     do when (ttSchema thn /= ttSchema els) $ fail $ unlines $

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -94,6 +94,7 @@ import qualified Lang.Crucible.Simulator.Operations as C
 import qualified Lang.Crucible.Simulator.OverrideSim as C
 import qualified Lang.Crucible.Simulator.RegMap as C
 import qualified Lang.Crucible.Simulator.SimError as C
+import qualified Lang.Crucible.Simulator.PathSatisfiability as C
 
 import qualified Lang.Crucible.LLVM.DataLayout as C.LLVM
 import qualified Lang.Crucible.LLVM.Extension as C.LLVM
@@ -226,11 +227,11 @@ crucible_llvm_verify_x86 ::
   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 (currently ignored) -} ->
+  Bool {- ^ Whether to enable path satisfiability checking -} ->
   LLVMCrucibleSetupM () {- ^ Specification to verify against -} ->
   ProofScript SatResult {- ^ Tactic used to use when discharging goals -} ->
   TopLevel (SomeLLVM MS.CrucibleMethodSpecIR)
-crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm globsyms _checkSat setup tactic
+crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic
   | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @64) . C.LLVM.llvmArch
                  $ modTrans llvmModule ^. C.LLVM.transContext = do
       let ?ptrWidth = knownNat @64
@@ -277,7 +278,7 @@ 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
+      methodSpec <- buildMethodSpec bic opts llvmModule nm (show addr) checkSat setup
 
       let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx
 
@@ -346,13 +347,23 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl
           pure $ C.regValue r
 
       liftIO $ printOutLn opts Info "Simulating function"
-      liftIO $ C.executeCrucible [] initial >>= \case
+
+      psatf <-
+         if checkSat then
+           do f <- liftIO (C.pathSatisfiabilityFeature sym (C.considerSatisfiability sym))
+              pure [C.genericToExecutionFeature f]
+         else
+           pure []
+
+      let execFeatures = psatf
+
+      liftIO $ C.executeCrucible execFeatures initial >>= \case
         C.FinishedResult{} -> pure ()
         C.AbortedResult{} -> printOutLn opts Warn "Warning: function never returns"
         C.TimeoutResult{} -> fail "Execution timed out"
 
       stats <- checkGoals sym opts sc tactic
- 
+
       returnProof $ SomeLLVM (methodSpec & MS.csSolverStats .~ stats)
   | otherwise = fail "LLVM module must be 64-bit"
 
@@ -424,10 +435,11 @@ buildMethodSpec ::
   LLVMModule LLVMArch ->
   String {- ^ Name of method -} ->
   String {- ^ Source location for method spec (here, we use the address) -} ->
+  Bool {- ^ check sat -} ->
   LLVMCrucibleSetupM () ->
   TopLevel (MS.CrucibleMethodSpecIR LLVM)
-buildMethodSpec bic opts lm nm loc setup =
-  setupLLVMCrucibleContext bic opts lm $ \cc -> do
+buildMethodSpec bic opts lm nm loc checkSat setup =
+  setupLLVMCrucibleContext bic opts checkSat lm $ \cc -> do
     let methodId = LLVMMethodId nm Nothing
     let programLoc =
           W4.mkProgramLoc (W4.functionNameFromText $ Text.pack nm)