Some minor UX fixes

saw-script.cabal

@@ -221,7 +221,7 @@ executable saw
     , cryptol-saw-core
     , aig
 
-  GHC-options: -O2 -Wall -Werror -threaded -fno-ignore-asserts -fno-spec-constr-count
+  GHC-options: -O2 -Wall -Werror -threaded -fno-ignore-asserts -fno-spec-constr-count -rtsopts
 
 test-suite integration_tests
   type: exitcode-stdio-1.0

src/SAWScript/Builtins.hs

@@ -30,6 +30,7 @@ import Data.Monoid
 import Control.Monad.Except (MonadError(..))
 import Control.Monad.State
 import qualified Control.Exception as Ex
+import Data.Char (toLower)
 import qualified Data.ByteString as StrictBS
 import qualified Data.ByteString.Lazy as BS
 import qualified Data.ByteString.Lazy.UTF8 as B
@@ -116,6 +117,7 @@ import SAWScript.ImportAIG
 import SAWScript.AST (getVal, pShow, Located(..))
 import SAWScript.Options as Opts
 import SAWScript.Proof
+import SAWScript.Crucible.Common (PathSatSolver(..))
 import SAWScript.TopLevel
 import qualified SAWScript.Value as SV
 import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork)
@@ -424,15 +426,40 @@ print_term_depth d t =
      output <- liftIO $ scShowTerm sc opts' t
      printOutLnTop Info output
 
+goalSummary :: ProofGoal -> String
+goalSummary goal = unlines $
+  [ ("Goal " ++ goalName goal ++ " (goal number " ++ (show $ goalNum goal) ++ "): " ++ goalType goal) ++ " at " ++ goalLoc goal ] ++
+  if null (goalDesc goal) then [] else [ goalDesc goal ]
+
+
+write_goal :: String -> ProofScript ()
+write_goal fp =
+  execTactic $ tacticId $ \goal ->
+  do opts <- getTopLevelPPOpts
+     sc <- getSharedContext
+     liftIO $ do
+       output <- liftIO (scShowTerm sc opts =<< propToTerm sc (goalProp goal))
+       writeFile fp (unlines [goalSummary goal, output])
+
 print_goal :: ProofScript ()
 print_goal =
   execTactic $ tacticId $ \goal ->
   do opts <- getTopLevelPPOpts
      sc <- getSharedContext
      output <- liftIO (scShowTerm sc opts =<< propToTerm sc (goalProp goal))
-     printOutLnTop Info ("Goal " ++ goalName goal ++ " (goal number " ++ (show $ goalNum goal) ++ "):")
+     printOutLnTop Info (goalSummary goal)
      printOutLnTop Info output
 
+print_goal_summary :: ProofScript ()
+print_goal_summary =
+  execTactic $ tacticId $ \goal ->
+    printOutLnTop Info (goalSummary goal)
+
+goal_num :: ProofScript Int
+goal_num =
+  execTactic $ tacticId $ \goal ->
+    return (goalNum goal)
+
 print_goal_depth :: Int -> ProofScript ()
 print_goal_depth n =
   execTactic $ tacticId $ \goal ->
@@ -915,7 +942,15 @@ provePrim script t = do
   io $ checkBooleanSchema (ttType t)
   sc <- getSharedContext
   prop <- io $ predicateToProp sc Universal (ttTerm t)
-  let goal = ProofGoal 0 "prove" "prove" prop
+  pos <- SV.getPosition
+  let goal = ProofGoal
+             { goalNum  = 0
+             , goalType = "prove"
+             , goalName = "prove_prim"
+             , goalLoc  = show pos
+             , goalDesc = ""
+             , goalProp = prop
+             }
   res <- SV.runProofScript script goal Nothing "prove_prim"
   case res of
     UnfinishedProof pst ->
@@ -925,15 +960,24 @@ provePrim script t = do
   return res
 
 proveHelper ::
+  String ->
   ProofScript () ->
   TypedTerm ->
   (Term -> TopLevel Prop) ->
   TopLevel Theorem
-proveHelper script t f = do
+proveHelper nm script t f = do
   prop <- f $ ttTerm t
-  let goal = ProofGoal 0 "prove" "prove" prop
+  pos <- SV.getPosition
+  let goal = ProofGoal
+             { goalNum = 0
+             , goalType = "prove"
+             , goalName = nm
+             , goalLoc  = show pos
+             , goalDesc = ""
+             , goalProp = prop
+             }
   opts <- rwPPOpts <$> getTopLevelRW
-  res <- SV.runProofScript script goal Nothing "prove_print_prim"
+  res <- SV.runProofScript script goal Nothing (Text.pack nm)
   let failProof pst =
          fail $ "prove: " ++ show (length (psGoals pst)) ++ " unsolved subgoal(s)\n"
                           ++ SV.showsProofResult opts res ""
@@ -950,15 +994,15 @@ provePrintPrim ::
   TopLevel Theorem
 provePrintPrim script t = do
   sc <- getSharedContext
-  proveHelper script t $ io . predicateToProp sc Universal
+  proveHelper "prove_print" script t $ io . predicateToProp sc Universal
 
 provePropPrim ::
   ProofScript () ->
   TypedTerm ->
   TopLevel Theorem
 provePropPrim script t = do
   sc <- getSharedContext
-  proveHelper script t $ io . termToProp sc
+  proveHelper "prove_extcore" script t $ io . termToProp sc
 
 satPrim ::
   ProofScript () ->
@@ -968,7 +1012,15 @@ satPrim script t =
   do io $ checkBooleanSchema (ttType t)
      sc <- getSharedContext
      prop <- io $ predicateToProp sc Existential (ttTerm t)
-     let goal = ProofGoal 0 "sat" "sat" prop
+     pos <- SV.getPosition
+     let goal = ProofGoal
+                { goalNum = 0
+                , goalType = "sat"
+                , goalName = "sat"
+                , goalLoc  = show pos
+                , goalDesc = ""
+                , goalProp = prop
+                }
      res <- SV.runProofScript script goal Nothing "sat"
      case res of
        InvalidProof stats cex _ -> return (SV.Sat stats cex)
@@ -1439,8 +1491,17 @@ prove_core script input =
   do sc <- getSharedContext
      t <- parseCore input
      p <- io (termToProp sc t)
+     pos <- SV.getPosition
      opts <- rwPPOpts <$> getTopLevelRW
-     res <- SV.runProofScript script (ProofGoal 0 "prove" "prove" p) Nothing "prove_core"
+     let goal = ProofGoal
+                { goalNum = 0
+                , goalType = "prove"
+                , goalName = "prove_core"
+                , goalLoc  = show pos
+                , goalDesc = ""
+                , goalProp = p
+                }
+     res <- SV.runProofScript script goal Nothing "prove_core"
      let failProof pst =
             fail $ "prove_core: " ++ show (length (psGoals pst)) ++ " unsolved subgoal(s)\n"
                                   ++ SV.showsProofResult opts res ""
@@ -1683,6 +1744,13 @@ approxmc t = do
     [l] -> io $ putStrLn l
     _ -> fail $ "Garbled result from approxmc\n\n" ++ out
 
+set_path_sat_solver :: String -> TopLevel ()
+set_path_sat_solver nm =
+  case map toLower nm of
+    "z3"    -> modify (\rw -> rw{ rwPathSatSolver = PathSat_Z3 })
+    "yices" -> modify (\rw -> rw{ rwPathSatSolver = PathSat_Yices })
+    _ -> fail $ "Unknown path sat solver: " ++ show nm
+
 summarize_verification :: TopLevel ()
 summarize_verification =
   do values <- rwProofs <$> getTopLevelRW

src/SAWScript/Crucible/Common.hs

@@ -18,6 +18,7 @@ module SAWScript.Crucible.Common
   , IsSymBackend(..)
   , HasSymInterface(..)
   , OnlineSolver(..)
+  , PathSatSolver(..)
   , setupProfiling
   , SAWCruciblePersonality(..)
   , newSAWCoreExprBuilder
@@ -38,6 +39,7 @@ import           Lang.Crucible.Backend.Online (OnlineBackend, newOnlineBackend)
 import qualified Data.Parameterized.Nonce as Nonce
 import           What4.Protocol.Online (OnlineSolver(..))
 import qualified What4.Solver.Z3 as Z3
+import qualified What4.Solver.Yices as Yices
 import qualified What4.Protocol.SMTLib2 as SMT2
 
 import qualified What4.Config as W4
@@ -54,6 +56,12 @@ import qualified Prettyprinter as PP
 import Verifier.SAW.SharedTerm as SC
 import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState, newSAWCoreState)
 
+data PathSatSolver
+  = PathSat_Z3
+  | PathSat_Yices
+ deriving (Eq, Ord, Show)
+
+
 -- | The symbolic backend we use for SAW verification
 type Sym = W4.ExprBuilder Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.FloatReal)
 type Backend solver = OnlineBackend solver Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.FloatReal)
@@ -75,11 +83,18 @@ newSAWCoreExprBuilder sc =
 defaultSAWCoreBackendTimeout :: Integer
 defaultSAWCoreBackendTimeout = 10000
 
-newSAWCoreBackend :: Sym -> IO SomeOnlineBackend
-newSAWCoreBackend sym = newSAWCoreBackendWithTimeout sym 0
+newSAWCoreBackend :: PathSatSolver -> Sym -> IO SomeOnlineBackend
+newSAWCoreBackend pss sym = newSAWCoreBackendWithTimeout pss sym 0
+
+newSAWCoreBackendWithTimeout :: PathSatSolver -> Sym -> Integer -> IO SomeOnlineBackend
+newSAWCoreBackendWithTimeout PathSat_Yices sym timeout =
+  do bak <- newOnlineBackend sym Yices.yicesDefaultFeatures
+     W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
+     yicesTimeoutSetting <- W4.getOptionSetting Yices.yicesGoalTimeout (W4.getConfiguration sym)
+     _ <- W4.setOpt yicesTimeoutSetting timeout
+     return (SomeOnlineBackend (bak :: Backend Yices.Connection))
 
-newSAWCoreBackendWithTimeout :: Sym -> Integer -> IO SomeOnlineBackend
-newSAWCoreBackendWithTimeout sym timeout =
+newSAWCoreBackendWithTimeout PathSat_Z3 sym timeout =
   do bak <- newOnlineBackend sym (SMT2.defaultFeatures Z3.Z3)
      W4.extendConfig Z3.z3Options (W4.getConfiguration sym)
      z3TimeoutSetting <- W4.getOptionSetting Z3.z3Timeout (W4.getConfiguration sym)

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -31,6 +31,7 @@ module SAWScript.Crucible.JVM.Builtins
     , jvm_execute_func
     , jvm_postcond
     , jvm_precond
+    , jvm_assert
     , jvm_modifies_field
     , jvm_modifies_static_field
     , jvm_modifies_elem
@@ -290,7 +291,14 @@ verifyObligations cc mspec tactic assumes asserts =
        goal   <- io $ scImplies sc assume assert
        goal'  <- io $ boolToProp sc [] goal -- TODO, generalize over inputs
        let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
-           proofgoal = ProofGoal n "vc" goalname goal'
+           proofgoal = ProofGoal
+                       { goalNum = n
+                       , goalType = "vc"
+                       , goalName = nm
+                       , goalLoc  = show ploc
+                       , goalDesc = msg
+                       , goalProp = goal'
+                       }
        res <- runProofScript tactic proofgoal (Just ploc) $ Text.unwords
                  ["JVM verification condition:", Text.pack (show n), Text.pack goalname]
        case res of
@@ -717,6 +725,13 @@ verifyPoststate cc mspec env0 globals ret =
      poststateLoc <- SS.toW4Loc "_SAW_verify_poststate" <$> getPosition
      io $ W4.setCurrentProgramLoc sym poststateLoc
 
+     -- This discards all the obligations generated during
+     -- symbolic execution itself, i.e., which are not directly
+     -- generated from specification postconditions. This
+     -- is, in general, unsound.
+     skipSafetyProofs <- gets rwSkipSafetyProofs
+     when skipSafetyProofs (io (Crucible.clearProofObligations bak))
+
      let ecs0 = Map.fromList
            [ (ecVarIndex ec, ec)
            | tt <- mspec ^. MS.csPreState . MS.csFreshVars
@@ -763,8 +778,9 @@ setupCrucibleContext jclass =
      jc <- getJVMTrans
      cb <- getJavaCodebase
      sc <- getSharedContext
+     pathSatSolver <- gets rwPathSatSolver
      sym <- io $ newSAWCoreExprBuilder sc
-     bak <- io $ newSAWCoreBackend sym
+     bak <- io $ newSAWCoreBackend pathSatSolver sym
      opts <- getOptions
      io $ CJ.setSimulatorVerbosity (simVerbose opts) sym
 
@@ -1248,6 +1264,11 @@ generic_array_is ptr mval =
        X.throwM $ JVMArrayModifyPrestate ptr'
      Setup.addPointsTo pt
 
+jvm_assert :: TypedTerm -> JVMSetupM ()
+jvm_assert term = JVMSetupM $ do
+  loc <- SS.toW4Loc "jvm_assert" <$> lift getPosition
+  Setup.addCondition (MS.SetupCond_Pred loc term)
+
 jvm_precond :: TypedTerm -> JVMSetupM ()
 jvm_precond term = JVMSetupM $ do
   loc <- SS.toW4Loc "jvm_precond" <$> lift getPosition

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -138,6 +138,7 @@ jvm_extract c mname = do
   sc <- getSharedContext
   cb <- getJavaCodebase
   opts <- getOptions
+  pathSatSolver <- gets rwPathSatSolver
   let verbosity = simVerbose opts
   let gen       = Nonce.globalNonceGenerator
 
@@ -159,7 +160,7 @@ jvm_extract c mname = do
 
   io $ do -- only the IO monad, nothing else
           sym <- newSAWCoreExprBuilder sc
-          SomeOnlineBackend bak <- newSAWCoreBackend sym
+          SomeOnlineBackend bak <- newSAWCoreBackend pathSatSolver sym
           st  <- sawCoreState sym
           CJ.setSimulatorVerbosity verbosity sym