No crucible prefix

CHANGES.md

@@ -66,6 +66,19 @@ The new `cryptol_add_path` command adds a directory to the search path
 used when loading Cryptol modules (and following imports within
 explicitly-loaded modules).
 
+New, shorter names are available for all LLVM commands starting with
+the `crucible_` prefix. The new names use the `llvm_` prefix instead.
+The top-level function `crucible_llvm_verify` is now `llvm_verify`,
+and `crucible_llvm_unsafe_assume_spec` is `llvm_unsafe_assume_spec`.
+The old names are still supported for now. The in-REPL documentation
+(`:? <command>`) gives the new name for each command.
+
+Shorter names are available for some saw-script types: `CrucibleSetup`
+is now `LLVMSetup`, `CrucibleMethodSpec` is now simply `LLVMSpec`, and
+`JVMMethodSpec` is `JVMSpec`. The old type names are still supported
+for backward compatibility.
+
+
 ## Bug Fixes
 
 * Catch more exceptions at the REPL (issues #138, #560, #745, and #814).

doc/tutorial/code/dotprod.saw

@@ -1,25 +1,25 @@
 import "dotprod.cry";
 
 let alloc_init ty v = do {
-    p <- crucible_alloc ty;
-    crucible_points_to p v;
+    p <- llvm_alloc ty;
+    llvm_points_to p v;
     return p;
 };
 
 let ptr_to_fresh n ty = do {
-    x <- crucible_fresh_var n ty;
-    p <- alloc_init ty (crucible_term x);
+    x <- llvm_fresh_var n ty;
+    p <- alloc_init ty (llvm_term x);
     return (x, p);
 };
 
 let dotprod_spec n = do {
-    let nt = crucible_term {{ `n : [32] }};
+    let nt = llvm_term {{ `n : [32] }};
     (xs, xsp) <- ptr_to_fresh "xs" (llvm_array n (llvm_int 32));
     (ys, ysp) <- ptr_to_fresh "ys" (llvm_array n (llvm_int 32));
-    crucible_execute_func [xsp, ysp, nt];
-    crucible_return (crucible_term {{ dotprod xs ys }});
+    llvm_execute_func [xsp, ysp, nt];
+    llvm_return (llvm_term {{ dotprod xs ys }});
 };
 
 m <- llvm_load_module "dotprod.bc";
 
-dotprod_ov <- crucible_llvm_verify m "dotprod" [] true (dotprod_spec 10) z3;
+dotprod_ov <- llvm_verify m "dotprod" [] true (dotprod_spec 10) z3;

doc/tutorial/code/double.saw

@@ -1,6 +1,6 @@
 l <- llvm_load_module "double.bc";
-double_imp <- crucible_llvm_extract l "double_imp";
-double_ref <- crucible_llvm_extract l "double_ref";
+double_imp <- llvm_extract l "double_imp";
+double_ref <- llvm_extract l "double_ref";
 let thm = {{ \x -> double_ref x == double_imp x }};
 
 r <- prove abc thm;

doc/tutorial/code/ffs_compare.saw

@@ -1,11 +1,11 @@
 import "ffs.cry";
 j <- java_load_class "FFS";
-java_ffs_ref <- crucible_java_extract j "ffs_ref";
-java_ffs_imp <- crucible_java_extract j "ffs_imp";
+java_ffs_ref <- jvm_extract j "ffs_ref";
+java_ffs_imp <- jvm_extract j "ffs_imp";
 
 l <- llvm_load_module "ffs.bc";
-c_ffs_ref <- crucible_llvm_extract l "ffs_ref";
-c_ffs_imp <- crucible_llvm_extract l "ffs_imp";
+c_ffs_ref <- llvm_extract l "ffs_ref";
+c_ffs_imp <- llvm_extract l "ffs_imp";
 
 print "java ref <-> java imp";
 let thm1 = {{ \x -> java_ffs_ref x == java_ffs_imp x }};

doc/tutorial/code/ffs_gen_aig.saw

@@ -1,9 +1,9 @@
 cls <- java_load_class "FFS";
 bc <- llvm_load_module "ffs.bc";
-java_ffs_ref <- crucible_java_extract cls "ffs_ref";
-java_ffs_imp <- crucible_java_extract cls "ffs_imp";
-c_ffs_ref <- crucible_llvm_extract bc "ffs_ref";
-c_ffs_imp <- crucible_llvm_extract bc "ffs_imp";
+java_ffs_ref <- jvm_extract cls "ffs_ref";
+java_ffs_imp <- jvm_extract cls "ffs_imp";
+c_ffs_ref <- llvm_extract bc "ffs_ref";
+c_ffs_imp <- llvm_extract bc "ffs_imp";
 write_aig "java_ffs_ref.aig" java_ffs_ref;
 write_aig "java_ffs_imp.aig" java_ffs_imp;
 write_aig "c_ffs_ref.aig" c_ffs_ref;

doc/tutorial/code/ffs_java.saw

@@ -1,9 +1,9 @@
 print "Extracting reference term";
 j <- java_load_class "FFS";
-ffs_ref <- crucible_java_extract j "ffs_ref";
+ffs_ref <- jvm_extract j "ffs_ref";
 
 print "Extracting implementation term";
-ffs_imp <- crucible_java_extract j "ffs_imp";
+ffs_imp <- jvm_extract j "ffs_imp";
 
 print "Proving equivalence";
 let thm1 = {{ \x -> ffs_ref x == ffs_imp x }};

doc/tutorial/code/ffs_java_crucible.saw

@@ -1,9 +1,9 @@
 print "Extracting reference term";
 j <- java_load_class "FFS";
-ffs_ref <- crucible_java_extract j "ffs_ref";
+ffs_ref <- jvm_extract j "ffs_ref";
 
 print "Extracting implementation term";
-ffs_imp <- crucible_java_extract j "ffs_imp";
+ffs_imp <- jvm_extract j "ffs_imp";
 
 print "Proving equivalence";
 let thm1 = {{ \x -> ffs_ref x == ffs_imp x }};

doc/tutorial/code/ffs_llvm.saw

@@ -2,16 +2,16 @@ set_base 16;
 
 print "Extracting reference term: ffs_ref";
 l <- llvm_load_module "ffs.bc";
-ffs_ref <- crucible_llvm_extract l "ffs_ref";
+ffs_ref <- llvm_extract l "ffs_ref";
 
 print "Extracting implementation term: ffs_imp";
-ffs_imp <- crucible_llvm_extract l "ffs_imp";
+ffs_imp <- llvm_extract l "ffs_imp";
 
 print "Extracting implementation term: ffs_musl";
-ffs_musl <- crucible_llvm_extract l "ffs_musl";
+ffs_musl <- llvm_extract l "ffs_musl";
 
 print "Extracting buggy term: ffs_bug";
-ffs_bug <- crucible_llvm_extract l "ffs_bug";
+ffs_bug <- llvm_extract l "ffs_bug";
 
 print "Proving equivalence: ffs_ref == ffs_imp";
 let thm1 = {{ \x -> ffs_ref x == ffs_imp x }};

doc/tutorial/code/picosat.saw

@@ -1,6 +1,6 @@
 l <- llvm_load_module "double.bc";
-double_imp <- crucible_llvm_extract l "double_imp";
-double_ref <- crucible_llvm_extract l "double_ref";
+double_imp <- llvm_extract l "double_imp";
+double_ref <- llvm_extract l "double_ref";
 let thm = {{ \x -> double_ref x == double_imp x }};
 
 let picosat = external_cnf_solver "picosat" ["%f"];

doc/tutorial/tutorial.md

@@ -139,7 +139,7 @@ $include all code/ffs_llvm.saw
 ```
 
 In this script, the `print` commands simply display text for the user.
-The `crucible_llvm_extract` command instructs the SAWScript interpreter
+The `llvm_extract` command instructs the SAWScript interpreter
 to perform symbolic simulation of the given C function (e.g., `ffs_ref`)
 from a given bitcode file (e.g., `ffs.bc`), and return a term
 representing the semantics of the function.
@@ -254,10 +254,10 @@ Now we can do the proof both within and across languages (from
 $include all code/ffs_compare.saw
 ```
 
-Here, the `crucible_java_extract` function works like
-`crucible_llvm_extract`, but on a Java class and method name. The
-`prove_print` command works similarly to the `prove` followed by `print`
-combination used for the LLVM example above.
+Here, the `jvm_extract` function works like `llvm_extract`, but on a
+Java class and method name. The `prove_print` command works similarly
+to the `prove` followed by `print` combination used for the LLVM
+example above.
 
 Using SMT-Lib Solvers
 =====================
@@ -378,7 +378,7 @@ In this example, the definitions of `add_spec` and `dbl_spec` provide
 extra information about how to configure the symbolic simulator when
 analyzing Java code. In this case, the setup blocks provide explicit
 descriptions of the implicit configuration used by
-`crucible_java_extract` (used in the earlier Java FFS example and in the
+`jvm_extract` (used in the earlier Java FFS example and in the
 next section). The `jvm_fresh_var` commands instruct the simulator to
 create fresh symbolic inputs to correspond to the Java variables `x` and
 `y`. Then, the `jvm_return` commands indicate the expected return value

examples/chacha20/chacha20-crucible.saw

@@ -4,16 +4,16 @@ import "../../deps/cryptol-specs/Primitive/Symmetric/Cipher/Stream/chacha20.cry"
 
 // Allocate a pointer of type 'ty', referring to the value 'v'
 let alloc_init ty v = do {
-  p <- crucible_alloc ty;
-  crucible_points_to p v;
+  p <- llvm_alloc ty;
+  llvm_points_to p v;
   return p;
 };
 
 // Allocate a pointer to a fresh symbolic value
 // Returns a pair of the symbolic variable and the pointer
 let ptr_to_fresh n ty = do {
-  x <- crucible_fresh_var n ty;
-  p <- alloc_init ty (crucible_term x);
+  x <- llvm_fresh_var n ty;
+  p <- alloc_init ty (llvm_term x);
   return (x, p);
 };
 
@@ -33,26 +33,26 @@ crypto_stream_chacha20(unsigned char* out,
 
   (_, out_p)       <- ptr_to_fresh       "out"     (llvm_array 256 (llvm_int 8));
   let olen         =                                            {{ 256 : [64] }};
-  counter          <- crucible_fresh_var "counter"                 (llvm_int 32);
+  counter          <- llvm_fresh_var     "counter"                 (llvm_int 32);
   (nonce, nonce_p) <- ptr_to_fresh       "nonce"   (llvm_array 12  (llvm_int 8));
   (key, key_p)     <- ptr_to_fresh       "key"     (llvm_array 32  (llvm_int 8));
 
   // symbolically executing the function
 
-  crucible_execute_func
+  llvm_execute_func
     [ out_p
-    , crucible_term olen
-    , crucible_term counter
+    , llvm_term olen
+    , llvm_term counter
     , nonce_p
     , key_p
     ];
 
   // assert the specification
 
   let spec_result =
-    crucible_term {{ chacha20::stream key counter nonce : [256][8] }};
+    llvm_term {{ chacha20::stream key counter nonce : [256][8] }};
 
-  crucible_points_to out_p spec_result;
+  llvm_points_to out_p spec_result;
 
 };
 
@@ -62,4 +62,4 @@ mod <- llvm_load_module "chacha20.bc";
 let solver = abc;
 
 print "Testing equality...";
-time (crucible_llvm_verify mod "crypto_stream_chacha20" [] false chacha20_setup solver);
+time (llvm_verify mod "crypto_stream_chacha20" [] false chacha20_setup solver);

examples/chacha20/chacha20.saw

@@ -8,35 +8,35 @@ print "loading LLVM bitcode...";
 mod <- llvm_load_module "chacha20.bc";
 
 let alloc_init ty v = do {
-    p <- crucible_alloc ty;
-    crucible_points_to p v;
+    p <- llvm_alloc ty;
+    llvm_points_to p v;
     return p;
 };
 
 let ptr_to_fresh n ty = do {
-    x <- crucible_fresh_var n ty;
-    p <- alloc_init ty (crucible_term x);
+    x <- llvm_fresh_var n ty;
+    p <- alloc_init ty (llvm_term x);
     return (x, p);
 };
 
 let i8 = llvm_int 8;
 let i32 = llvm_int 32;
 
 let stream_spec len = do {
-  outp <- crucible_alloc (llvm_array len i8);
+  outp <- llvm_alloc (llvm_array len i8);
   (key, keyp) <- ptr_to_fresh "key" (llvm_array 32 i8);
   (nonce, noncep) <- ptr_to_fresh "nonce" (llvm_array 12 i8);
-  counter <- crucible_fresh_var "counter" i32;
+  counter <- llvm_fresh_var "counter" i32;
 
-  crucible_execute_func [ outp
-                        , crucible_term {{ `len : [64] }}
-                        , crucible_term counter
-                        , noncep
-                        , keyp
-                        ];
+  llvm_execute_func [ outp
+                    , llvm_term {{ `len : [64] }}
+                    , llvm_term counter
+                    , noncep
+                    , keyp
+                    ];
 
-  crucible_points_to outp (crucible_term {{ chacha20::stream key counter nonce : [len][8] }});
+  llvm_points_to outp (llvm_term {{ chacha20::stream key counter nonce : [len][8] }});
 };
 
 print "running verification...";
-time (crucible_llvm_verify mod "crypto_stream_chacha20" [] true (stream_spec 256) abc);
+time (llvm_llvm_verify mod "crypto_stream_chacha20" [] true (stream_spec 256) abc);

examples/fresh-post/fresh-post-bad.saw

@@ -1,15 +1,15 @@
 let whoknows_spec : CrucibleSetup () = do {
-  crucible_execute_func [];
-  y <- crucible_fresh_var "y" (llvm_int 32);
-  crucible_postcond {{ y < 0x0000FFFF }};
-  crucible_return (crucible_term y);
+  llvm_execute_func [];
+  y <- llvm_fresh_var "y" (llvm_int 32);
+  llvm_postcond {{ y < 0x0000FFFF }};
+  llvm_return (llvm_term y);
 };
 
 let bad_spec : CrucibleSetup () = do {
-  crucible_execute_func [];
-  crucible_return (crucible_term {{0:[32]}});
+  llvm_execute_func [];
+  llvm_return (llvm_term {{0:[32]}});
 };
 
 m <- llvm_load_module "source.bc";
-whoknows <- crucible_llvm_unsafe_assume_spec m "whoknows" whoknows_spec;
-fails (crucible_llvm_verify m "bad" [whoknows] false bad_spec abc);
+whoknows <- llvm_unsafe_assume_spec m "whoknows" whoknows_spec;
+fails (llvm_verify m "bad" [whoknows] false bad_spec abc);

examples/fresh-post/fresh-post-good.saw

@@ -1,25 +1,25 @@
 let whoknows_spec : CrucibleSetup () = do {
-  crucible_execute_func [];
-  y <- crucible_fresh_var "y" (llvm_int 32);
-  crucible_return (crucible_term y);
+  llvm_execute_func [];
+  y <- llvm_fresh_var "y" (llvm_int 32);
+  llvm_return (llvm_term y);
 };
 
 let example_spec : CrucibleSetup () = do {
-  crucible_execute_func [];
-  crucible_return (crucible_term {{0:[32]}});
+  llvm_execute_func [];
+  llvm_return (llvm_term {{0:[32]}});
 };
 
 let one_spec : CrucibleSetup () = do {
-  crucible_execute_func [];
-  x <- crucible_fresh_var "x" (llvm_int 32);
-  crucible_return (crucible_term x);
+  llvm_execute_func [];
+  x <- llvm_fresh_var "x" (llvm_int 32);
+  llvm_return (llvm_term x);
 };
 
 let main : TopLevel () = do {
 
     m <- llvm_load_module "source.bc";
-    whoknows <- crucible_llvm_unsafe_assume_spec m "whoknows" whoknows_spec;
-    crucible_llvm_verify m "example" [whoknows] false example_spec abc;
-    crucible_llvm_verify m "one" [] false one_spec ( do { print_goal; abc; } );
+    whoknows <- llvm_unsafe_assume_spec m "whoknows" whoknows_spec;
+    llvm_verify m "example" [whoknows] false example_spec abc;
+    llvm_verify m "one" [] false one_spec ( do { print_goal; abc; } );
     print "done";
 };

examples/ghost/ghost.saw

@@ -1,26 +1,26 @@
 let next_spec counter : CrucibleSetup () = do {
-  n <- crucible_fresh_var "n" (llvm_int 32);
-  crucible_ghost_value counter n;
-  crucible_execute_func [];
-  crucible_ghost_value counter {{n+1}};
-  crucible_return (crucible_term {{n}});
+  n <- llvm_fresh_var "n" (llvm_int 32);
+  llvm_ghost_value counter n;
+  llvm_execute_func [];
+  llvm_ghost_value counter {{n+1}};
+  llvm_return (llvm_term {{n}});
 };
 
 let example_spec counter : CrucibleSetup () = do {
-  n <- crucible_fresh_var "nm" (llvm_int 32);
-  crucible_precond {{n < 2}};
-  crucible_ghost_value counter n;
-  crucible_execute_func [];
-  crucible_ghost_value counter {{n+3}};
-  crucible_return (crucible_term {{n+2}});
+  n <- llvm_fresh_var "nm" (llvm_int 32);
+  llvm_precond {{n < 2}};
+  llvm_ghost_value counter n;
+  llvm_execute_func [];
+  llvm_ghost_value counter {{n+3}};
+  llvm_return (llvm_term {{n+2}});
 };
 
 let main : TopLevel () = do {
-    counter <- crucible_declare_ghost_state "ctr";
+    counter <- llvm_declare_ghost_state "ctr";
 
     m <- llvm_load_module "simple.bc";
-    next <- crucible_llvm_unsafe_assume_spec m "next" (next_spec counter);
-    crucible_llvm_verify m "example" [next] false (example_spec counter)
+    next <- llvm_unsafe_assume_spec m "next" (next_spec counter);
+    llvm_verify m "example" [next] false (example_spec counter)
                 (do { print_goal; z3;} );
     print "done";
 };