Merge pull request #955 from GaloisInc/crucible-jvm

Remove "crucible_" prefix from JVM verification commands

doc/manual/manual.md

@@ -1245,7 +1245,7 @@ techniques that do not require significant computation.
 
 * `assume_unsat : ProofScript SatResult` indicates that the current goal
 should be assumed to be unsatisfiable. At the moment,
-`crucible_jvm_verify` and `crucible_llvm_verify` (described below) run
+`jvm_verify` and `crucible_llvm_verify` (described below) run
 their proofs in a satisfiability-checking (negated) context, so
 `assume_unsat` indicates that the property being checked should be
 assumed to be true. This is likely to change in the future.
@@ -1845,7 +1845,7 @@ A similar command for JVM programs is available if `enable_experimental`
 has been run.
 
 ~~~~
-crucible_jvm_verify :
+jvm_verify :
   JavaClass ->
   String ->
   [JVMMethodSpec] ->
@@ -2011,11 +2011,11 @@ of properties we have already proved about its callees rather than
 analyzing them anew. This enables us to reason about much larger
 and more complex systems than otherwise possible.
 
-The `crucible_llvm_verify` and `crucible_jvm_verify` functions return
-values of type `CrucibleMethodSpec` and `JVMMethodSpec`, respectively.
-These values are opaque objects that internally contain both the
-information provided in the associated `JVMSetup` or `CrucibleSetup`
-blocks and the results of the verification process.
+The `crucible_llvm_verify` and `jvm_verify` functions return values of
+type `CrucibleMethodSpec` and `JVMMethodSpec`, respectively. These
+values are opaque objects that internally contain both the information
+provided in the associated `JVMSetup` or `CrucibleSetup` blocks and
+the results of the verification process.
 
 Any of these `MethodSpec` objects can be passed in via the third
 argument of the `..._verify` functions. For any function or method
@@ -2330,7 +2330,7 @@ crucible_llvm_unsafe_assume_spec :
 Or, in the experimental JVM implementation:
 
 ~~~
-crucible_jvm_unsafe_assume_spec :
+jvm_unsafe_assume_spec :
   JavaClass -> String -> JVMSetup () -> TopLevel JVMMethodSpec
 ~~~
 

doc/tutorial/code/java_add.saw

@@ -13,6 +13,6 @@ let dbl_spec = do {
 };
 
 cls <- java_load_class "Add";
-ms <- crucible_jvm_verify cls "add" [] false add_spec abc;
-ms' <- crucible_jvm_verify cls "dbl" [ms] false dbl_spec abc;
+ms <- jvm_verify cls "add" [] false add_spec abc;
+ms' <- jvm_verify cls "dbl" [ms] false dbl_spec abc;
 print "Done.";

doc/tutorial/tutorial.md

@@ -387,13 +387,13 @@ inline). Because Java methods can operate on references, as well, which
 do not exist in Cryptol, Cryptol expressions must be translated to JVM
 values with `jvm_term`.
 
-To make use of these setup blocks, the `crucible_jvm_verify` command
-analyzes the method corresponding to the class and method name provided,
-using the setup block passed in as a parameter. It then returns an
-object that describes the proof it has just performed. This object can
-be passed into later instances of `java_verify` to indicate that calls
-to the analyzed method do not need to be followed, and the previous
-proof about that method can be used instead of re-analyzing it.
+To make use of these setup blocks, the `jvm_verify` command analyzes
+the method corresponding to the class and method name provided, using
+the setup block passed in as a parameter. It then returns an object
+that describes the proof it has just performed. This object can be
+passed into later instances of `jvm_verify` to indicate that calls to
+the analyzed method do not need to be followed, and the previous proof
+about that method can be used instead of re-analyzing it.
 
 Interactive Interpreter
 =======================

examples/ecdsa/ecdsa-crucible.saw

@@ -264,15 +264,15 @@ c <- java_load_class ecc_class;
 let method_prove name specs setup tac =
   time do {
     print (str_concat "Verifying " name);
-    crucible_jvm_verify c name specs false setup tac;
+    jvm_verify c name specs false setup tac;
   };
 
 let method_assume name specs setup tac = method_prove name specs setup assume_unsat;
 
 let method_skip name _specs setup _tac =
   time do {
     print (str_concat "Skipping verification of " name);
-    crucible_jvm_unsafe_assume_spec c name setup;
+    jvm_unsafe_assume_spec c name setup;
   };
 
 let method = method_prove;

intTests/test_issue108/refarray.saw

@@ -11,5 +11,5 @@ let test2_spec : JVMSetup() = do {
   jvm_execute_func [r, jvm_term x];
   jvm_return (jvm_term x);
 };
-crucible_jvm_verify Test_class "test1" [] false test1_spec abc;
-crucible_jvm_verify Test_class "test2" [] false test2_spec abc;
+jvm_verify Test_class "test1" [] false test1_spec abc;
+jvm_verify Test_class "test2" [] false test2_spec abc;

intTests/test_jvm_method_names/test.saw

@@ -2,7 +2,7 @@ enable_experimental;
 c <- java_load_class "Test";
 print c;
 
-crucible_jvm_verify c "get" [] false
+jvm_verify c "get" [] false
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -16,7 +16,7 @@ crucible_jvm_verify c "get" [] false
 print "********************************************************************************";
 print "<init>";
 fails (
-crucible_jvm_verify c "<init>" [] false
+jvm_verify c "<init>" [] false
   do {
     this <- jvm_alloc_object "Test";
     jvm_execute_func [this];
@@ -26,7 +26,7 @@ crucible_jvm_verify c "<init>" [] false
 
 print "********************************************************************************";
 print "<init>(J)V";
-crucible_jvm_verify c "<init>(J)V" [] false
+jvm_verify c "<init>(J)V" [] false
   do {
     this <- jvm_alloc_object "Test";
     x <- jvm_fresh_var "x" java_long;
@@ -37,7 +37,7 @@ crucible_jvm_verify c "<init>(J)V" [] false
 
 print "********************************************************************************";
 print "<init>(I)V";
-crucible_jvm_verify c "<init>(I)V" [] false
+jvm_verify c "<init>(I)V" [] false
   do {
     this <- jvm_alloc_object "Test";
     x <- jvm_fresh_var "x" java_int;
@@ -48,7 +48,7 @@ crucible_jvm_verify c "<init>(I)V" [] false
 
 print "********************************************************************************";
 print "<init>()V";
-crucible_jvm_verify c "<init>()V" [] false
+jvm_verify c "<init>()V" [] false
   do {
     this <- jvm_alloc_object "Test";
     jvm_execute_func [this];
@@ -59,7 +59,7 @@ crucible_jvm_verify c "<init>()V" [] false
 print "********************************************************************************";
 print "increment";
 fails (
-crucible_jvm_verify c "increment" [] false
+jvm_verify c "increment" [] false
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -71,7 +71,7 @@ crucible_jvm_verify c "increment" [] false
 
 print "********************************************************************************";
 print "increment()V";
-crucible_jvm_verify c "increment()V" [] false
+jvm_verify c "increment()V" [] false
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -83,7 +83,7 @@ crucible_jvm_verify c "increment()V" [] false
 
 print "********************************************************************************";
 print "increment(J)V";
-crucible_jvm_verify c "increment(J)V" [] false
+jvm_verify c "increment(J)V" [] false
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -96,7 +96,7 @@ crucible_jvm_verify c "increment(J)V" [] false
 
 print "********************************************************************************";
 print "increment(I)V";
-crucible_jvm_verify c "increment(I)V" [] false
+jvm_verify c "increment(I)V" [] false
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -109,7 +109,7 @@ crucible_jvm_verify c "increment(I)V" [] false
 
 print "********************************************************************************";
 print "increment(LTest;)V";
-crucible_jvm_verify c "increment(LTest;)V" [] false
+jvm_verify c "increment(LTest;)V" [] false
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;

intTests/test_jvm_setup_errors/test.saw

@@ -2,10 +2,10 @@
 
 This file is intended to test the error checking for ill-formed
 `JVMSetup` blocks. All setup blocks will be tested with
-`crucible_jvm_unsafe_assume_spec`, in order to make sure that the
-errors are caught at the early phase when the setup block is
-processed, and that we do not rely on run-time errors during symbolic
-simulation to catch problems.
+`jvm_unsafe_assume_spec`, in order to make sure that the errors are
+caught at the early phase when the setup block is processed, and that
+we do not rely on run-time errors during symbolic simulation to catch
+problems.
 
 This file is necessarily incomplete, and should be extended with new
 additional tests as we add new checks to the SAW/JVM code.
@@ -21,7 +21,7 @@ test <- java_load_class "Test";
 print test;
 
 let check_fails cls name spec =
-  fails (crucible_jvm_unsafe_assume_spec cls name spec);
+  fails (jvm_unsafe_assume_spec cls name spec);
 
 let KNOWN_FALSE_POSITIVE cls name spec =
   do {
@@ -30,7 +30,7 @@ let KNOWN_FALSE_POSITIVE cls name spec =
   };
 
 print "Working spec for method 'get'";
-crucible_jvm_verify test "get" [] false
+jvm_verify test "get" [] false
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -121,7 +121,7 @@ check_fails test "get"
   };
 
 print "Working spec for method 'lookup'";
-crucible_jvm_verify test "lookup" [] false
+jvm_verify test "lookup" [] false
   do {
     arr <- jvm_alloc_array 8 java_long;
     let idx = {{ 2 : [32] }};
@@ -234,7 +234,7 @@ check_fails test "lookup"
   };
 
 print "Working spec for method 'lookup' (jvm_array_is)";
-crucible_jvm_verify test "lookup" [] false
+jvm_verify test "lookup" [] false
   do {
     arr <- jvm_alloc_array 8 java_long;
     xs <- jvm_fresh_var "xs" (java_array 8 java_long);
@@ -357,7 +357,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
   };
 
 print "Working spec for method 'set'";
-crucible_jvm_verify test "set" [] false
+jvm_verify test "set" [] false
   do {
     this <- jvm_alloc_object "Test";
     x <- jvm_fresh_var "x" java_long;

saw-remote-api/src/SAWServer/JVMVerify.hs

@@ -43,9 +43,9 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc
               VerifyContract -> do
                 lemmas <- mapM getJVMMethodSpecIR lemmaNames
                 proofScript <- interpretProofScript script
-                tl $ crucible_jvm_verify cls fun lemmas checkSat setup proofScript
+                tl $ jvm_verify cls fun lemmas checkSat setup proofScript
               AssumeContract ->
-                tl $ crucible_jvm_unsafe_assume_spec cls fun setup
+                tl $ jvm_unsafe_assume_spec cls fun setup
             dropTask
             setServerVal lemmaName res
             ok

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -25,8 +25,8 @@ Stability   : provisional
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module SAWScript.Crucible.JVM.Builtins
-    ( crucible_jvm_verify
-    , crucible_jvm_unsafe_assume_spec
+    ( jvm_verify
+    , jvm_unsafe_assume_spec
     , jvm_return
     , jvm_execute_func
     , jvm_postcond
@@ -180,15 +180,15 @@ excludedRefs = Set.fromList
   , "java/lang/invoke/MethodHandleInfo"
   ]
 
-crucible_jvm_verify ::
+jvm_verify ::
   J.Class ->
   String {- ^ method name -} ->
   [CrucibleMethodSpecIR] {- ^ overrides -} ->
   Bool {- ^ path sat checking -} ->
   JVMSetupM () ->
   ProofScript SatResult ->
   TopLevel CrucibleMethodSpecIR
-crucible_jvm_verify cls nm lemmas checkSat setup tactic =
+jvm_verify cls nm lemmas checkSat setup tactic =
   do cb <- getJavaCodebase
      opts <- getOptions
      -- allocate all of the handles/static vars that are referenced
@@ -205,7 +205,7 @@ crucible_jvm_verify cls nm lemmas checkSat setup tactic =
      let loc = SS.toW4Loc "_SAW_verify_prestate" pos
 
      profFile <- rwProfilingFile <$> getTopLevelRW
-     (writeFinalProfile, pfs) <- io $ Common.setupProfiling sym "crucible_jvm_verify" profFile
+     (writeFinalProfile, pfs) <- io $ Common.setupProfiling sym "jvm_verify" profFile
 
      (cls', method) <- io $ findMethod cb pos nm cls -- TODO: switch to crucible-jvm version
      let st0 = initialCrucibleSetupState cc (cls', method) loc
@@ -224,7 +224,7 @@ crucible_jvm_verify cls nm lemmas checkSat setup tactic =
      frameIdent <- io $ Crucible.pushAssumptionFrame sym
 
      -- run the symbolic execution
-     top_loc <- SS.toW4Loc "crucible_jvm_verify" <$> getPosition
+     top_loc <- SS.toW4Loc "jvm_verify" <$> getPosition
      (ret, globals3) <-
        io $ verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals2 checkSat
 
@@ -241,12 +241,12 @@ crucible_jvm_verify cls nm lemmas checkSat setup tactic =
      returnProof (methodSpec & MS.csSolverStats .~ stats)
 
 
-crucible_jvm_unsafe_assume_spec ::
+jvm_unsafe_assume_spec ::
   J.Class          ->
   String          {- ^ Name of the method -} ->
   JVMSetupM () {- ^ Boundary specification -} ->
   TopLevel CrucibleMethodSpecIR
-crucible_jvm_unsafe_assume_spec cls nm setup =
+jvm_unsafe_assume_spec cls nm setup =
   do cc <- setupCrucibleContext cls
      cb <- getJavaCodebase
      pos <- getPosition