Support specifying ProofScripts during x86 verification (#753)

* Support specifying ProofScripts during x86 verification

* Change .travis.yml s2n commit to HEAD of saw-travis-branch

Author: chameco

.travis.yml

@@ -84,7 +84,7 @@ jobs:
         - mkdir -p s2n/test-deps/saw/bin
         - cp bin/saw s2n/test-deps/saw/bin
         - cd s2n
-        - git checkout 28ea0fea9ab7dc710c9424d9b869b39ca3804d79
+        - git checkout cd7282102bf5e65cc8b324c4127c7943c71c8513
       before_script:
         - export TESTS=sawHMAC
       script:

intTests/test_llvm_x86_01/test.saw

@@ -11,7 +11,7 @@ let foo_setup = do {
   val <- crucible_fresh_var "val'" (llvm_int 64);
   crucible_points_to ptr (crucible_term val);
 };
-foo_method_spec <- crucible_llvm_verify_x86 m "./test" "foo" [] false foo_setup;
+foo_method_spec <- crucible_llvm_verify_x86 m "./test" "foo" [] false foo_setup w4;
 
 let bar_setup = do {
   crucible_execute_func [];

intTests/test_llvm_x86_02/test.saw

@@ -11,4 +11,4 @@ let increment_setup = do {
   crucible_points_to ptr (crucible_term valprime);
   crucible_postcond {{ valprime == val }};
 };
-fails (crucible_llvm_verify_x86 m "./test" "increment" [] false increment_setup);
+fails (crucible_llvm_verify_x86 m "./test" "increment" [] false increment_setup w4);

intTests/test_llvm_x86_03/test.saw

@@ -6,4 +6,4 @@ let test_setup = do {
   crucible_execute_func [];
   crucible_return (crucible_term {{ 1 : [64] }});
 };
-fails (crucible_llvm_verify_x86 m "./test" "foo" [] false test_setup);
+fails (crucible_llvm_verify_x86 m "./test" "foo" [] false test_setup w4);

intTests/test_llvm_x86_04/test.saw

@@ -16,4 +16,4 @@ let addvar_setup = do {
   valprime <- crucible_fresh_var "_val" (llvm_int 64);
   crucible_points_to ptr (crucible_term valprime);
 };
-crucible_llvm_verify_x86 m "./test" "addvar" [] false addvar_setup;
+crucible_llvm_verify_x86 m "./test" "addvar" [] false addvar_setup w4;

src/SAWScript/Crucible/LLVM/X86.hs

@@ -29,7 +29,7 @@ module SAWScript.Crucible.LLVM.X86
 import Control.Lens.TH (makeLenses)
 
 import System.IO (stdout)
-import Control.Exception (catch, throw)
+import Control.Exception (throw)
 import Control.Lens (view, use, (&), (^.), (.~), (.=))
 import Control.Monad.ST (stToIO)
 import Control.Monad.State
@@ -54,11 +54,12 @@ import Data.Parameterized.NatRepr
 import Data.Parameterized.Context hiding (view)
 import Data.Parameterized.Nonce
 
+import Verifier.SAW.FiniteValue
 import Verifier.SAW.Recognizer
 import Verifier.SAW.Term.Functor
 import Verifier.SAW.TypedTerm
 
-import SAWScript.Prover.SBV
+import SAWScript.Proof
 import SAWScript.Prover.SolverStats
 import SAWScript.TopLevel
 import SAWScript.Value
@@ -187,8 +188,9 @@ crucible_llvm_verify_x86 ::
   [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} ->
   Bool {-^ Whether to enable path satisfiability checking (currently ignored) -} ->
   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
+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
@@ -278,7 +280,7 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl
         C.AbortedResult{} -> printOutLn opts Warn "Warning: function never returns"
         C.TimeoutResult{} -> fail "Execution timed out"
 
-      liftIO . void $ runX86Sim preState checkGoals
+      checkGoals sym opts sc tactic
 
       pure $ SomeLLVM methodSpec
   | otherwise = fail "LLVM module must be 64-bit"
@@ -700,29 +702,35 @@ assertPointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr texpected) = do
 
 -- | Gather and run the solver on goals from the simulator.
 checkGoals ::
-  X86Sim ()
-checkGoals = do
-  sym <- use x86Sym
-  opts <- use x86Options
-  sc <- use x86SharedContext
+  Sym ->
+  Options ->
+  SharedContext ->
+  ProofScript SatResult ->
+  TopLevel ()
+checkGoals sym opts sc tactic = do
   gs <- liftIO $ getGoals sym
   liftIO . printOutLn opts Info $ mconcat
     [ "Simulation finished, running solver on "
     , show $ length gs
     , " goals"
     ]
-  liftIO . forM_ gs $ \g ->
-    do
-      term <- gGoal sc g
-      (mb, stats) <- proveUnintSBV z3 [] Nothing sc term
-      printOutLn opts Info $ ppStats stats
-      case mb of
-        Nothing -> printOutLn opts Info "Goal succeeded"
-        Just ex -> do
-          fail $ mconcat
-            ["Failure (", show $ gLoc g
-            , "): ", show $ gMessage g
-            , "\nCounterexample: " <> show ex
-            ]
-    `catch` \(X86Error e) -> fail $ "Failure, error: " <> e
+  forM_ (zip [0..] gs) $ \(n, g) -> do
+    term <- liftIO $ gGoal sc g
+    let proofgoal = ProofGoal n "vc" (show $ gMessage g) term
+    r <- evalStateT tactic $ startProof proofgoal
+    case r of
+      Unsat stats -> do
+        liftIO . printOutLn opts Info $ ppStats stats
+      SatMulti stats vals -> do
+        printOutLnTop Info $ unwords ["Subgoal failed:", show $ gMessage g]
+        printOutLnTop Info (show stats)
+        printOutLnTop OnlyCounterExamples "----------Counterexample----------"
+        ppOpts <- sawPPOpts . rwPPOpts <$> getTopLevelRW
+        case vals of
+          [] -> printOutLnTop OnlyCounterExamples "<<All settings of the symbolic variables constitute a counterexample>>"
+          _ -> let showAssignment (name, val) =
+                     mconcat [ " ", name, ": ", show $ ppFirstOrderValue ppOpts val ]
+               in mapM_ (printOutLnTop OnlyCounterExamples . showAssignment) vals
+        printOutLnTop OnlyCounterExamples "----------------------------------"
+        throwTopLevel "Proof failed."
   liftIO $ printOutLn opts Info "All goals succeeded"

src/SAWScript/Interpreter.hs

@@ -1986,7 +1986,7 @@ primitives = Map.fromList
     ]
 
   , prim "crucible_llvm_verify_x86"
-    "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> CrucibleSetup () -> TopLevel CrucibleMethodSpec"
+    "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> CrucibleSetup () -> ProofScript SatResult -> TopLevel CrucibleMethodSpec"
     (bicVal crucible_llvm_verify_x86)
     Experimental
     [ "Verify an x86 function from an ELF file for use as an override in an"