Merge pull request #435 from GaloisInc/at-396-remove-lss

This removes all connections to the old LSS (llvm-verifier) code now that the Crucible-based equivalent is sufficiently robust. The one downside is that llvm_symexec no longer exists. We may want to implement something with similar but better functionality eventually.

Fixes #396.

cabal.project

@@ -12,7 +12,6 @@ packages:
     deps/saw-core-what4
     deps/cryptol-verifier
     deps/jvm-verifier
-    deps/llvm-verifier
     deps/crucible/what4
     deps/crucible/what4-abc
     deps/crucible/crucible

doc/tutorial/code/double.saw

@@ -1,7 +1,6 @@
-enable_deprecated;
 l <- llvm_load_module "double.bc";
-double_imp <- llvm_extract l "double_imp" llvm_pure;
-double_ref <- llvm_extract l "double_ref" llvm_pure;
+double_imp <- crucible_llvm_extract l "double_imp";
+double_ref <- crucible_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,12 +1,11 @@
-enable_deprecated;
 import "ffs.cry";
 j <- java_load_class "FFS";
-java_ffs_ref <- java_extract j "ffs_ref" java_pure;
-java_ffs_imp <- java_extract j "ffs_imp" java_pure;
+java_ffs_ref <- crucible_java_extract j "ffs_ref";
+java_ffs_imp <- crucible_java_extract j "ffs_imp";
 
 l <- llvm_load_module "ffs.bc";
-c_ffs_ref <- llvm_extract l "ffs_ref" llvm_pure;
-c_ffs_imp <- llvm_extract l "ffs_imp" llvm_pure;
+c_ffs_ref <- crucible_llvm_extract l "ffs_ref";
+c_ffs_imp <- crucible_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,10 +1,9 @@
-enable_deprecated;
 cls <- java_load_class "FFS";
 bc <- llvm_load_module "ffs.bc";
-java_ffs_ref <- java_extract cls "ffs_ref" java_pure;
-java_ffs_imp <- java_extract cls "ffs_imp" java_pure;
-c_ffs_ref <- llvm_extract bc "ffs_ref" llvm_pure;
-c_ffs_imp <- llvm_extract bc "ffs_imp" llvm_pure;
+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";
 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,10 +1,9 @@
-enable_deprecated;
 print "Extracting reference term";
 j <- java_load_class "FFS";
-ffs_ref <- java_extract j "ffs_ref" java_pure;
+ffs_ref <- crucible_java_extract j "ffs_ref";
 
 print "Extracting implementation term";
-ffs_imp <- java_extract j "ffs_imp" java_pure;
+ffs_imp <- crucible_java_extract j "ffs_imp";
 
 print "Proving equivalence";
 let thm1 = {{ \x -> ffs_ref x == ffs_imp x }};

doc/tutorial/code/ffs_java_crucible.saw

@@ -1,4 +1,3 @@
-enable_deprecated;
 print "Extracting reference term";
 j <- java_load_class "FFS";
 ffs_ref <- crucible_java_extract j "ffs_ref";

doc/tutorial/code/ffs_llvm.saw

@@ -1,16 +1,15 @@
-enable_deprecated;
 print "Extracting reference term: ffs_ref";
 l <- llvm_load_module "ffs.bc";
-ffs_ref <- llvm_extract l "ffs_ref" llvm_pure;
+ffs_ref <- crucible_llvm_extract l "ffs_ref";
 
 print "Extracting implementation term: ffs_imp";
-ffs_imp <- llvm_extract l "ffs_imp" llvm_pure;
+ffs_imp <- crucible_llvm_extract l "ffs_imp";
 
 print "Extracting implementation term: ffs_musl";
-ffs_musl <- llvm_extract l "ffs_musl" llvm_pure;
+ffs_musl <- crucible_llvm_extract l "ffs_musl";
 
 print "Extracting buggy term: ffs_bug";
-ffs_bug <- llvm_extract l "ffs_bug" llvm_pure;
+ffs_bug <- crucible_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,7 +1,6 @@
-enable_deprecated;
 l <- llvm_load_module "double.bc";
-double_imp <- llvm_extract l "double_imp" llvm_pure;
-double_ref <- llvm_extract l "double_ref" llvm_pure;
+double_imp <- crucible_llvm_extract l "double_imp";
+double_ref <- crucible_llvm_extract l "double_ref";
 let thm = {{ \x -> double_ref x == double_imp x }};
 
 let picosat = external_cnf_solver "picosat" ["%f"];

examples/chacha20/chacha20.saw

@@ -7,26 +7,36 @@ import "../../deps/cryptol-specs/Primitive/Symmetric/Cipher/Stream/chacha20.cry"
 print "loading LLVM bitcode...";
 mod <- llvm_load_module "chacha20.bc";
 
-c <- fresh_symbolic "out"     {| [256][8] |};
-k <- fresh_symbolic "key"     {| [32][8]  |};
-n <- fresh_symbolic "nonce"   {| [12][8]  |};
-i <- fresh_symbolic "counter" {| [32] |};
-
-let allocs = [ ("out",   256)
-             , ("key",   32)
-             , ("nonce", 12)
-             ];
-let inits = [ ("*out",   c, 256)
-            , ("olen", {{ 256:[64] }}, 1)
-            , ("counter", i, 1)
-            , ("*key",   k, 32)
-            , ("*nonce", n, 12)
-            ];
-let results = [ ("*out", 256) ];
-
-print "extracting stream function...";
-cstream <- time (llvm_symexec mod "crypto_stream_chacha20" allocs inits results true);
-
-print "checking equality...";
-thm <- abstract_symbolic {{ cstream == chacha20::stream k i n }};
-time (prove_print abc thm);
+let alloc_init ty v = do {
+    p <- crucible_alloc ty;
+    crucible_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);
+    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);
+  (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;
+
+  crucible_execute_func [ outp
+                        , crucible_term {{ `len : [64] }}
+                        , crucible_term counter
+                        , noncep
+                        , keyp
+                        ];
+
+  crucible_points_to outp (crucible_term {{ chacha20::stream key counter nonce : [len][8] }});
+};
+
+print "running verification...";
+time (crucible_llvm_verify mod "crypto_stream_chacha20" [] true (stream_spec 256) abc);

examples/java/javatoaig.saw

@@ -1,5 +1,5 @@
 enable_deprecated;
 c <- java_load_class "Double";
-t <- java_extract c "f" java_pure;
+t <- crucible_java_extract c "f";
 print_term t;
 write_aig "java_f.aig" t;

examples/llvm/assert-null.saw

@@ -1,17 +1,14 @@
-enable_deprecated;
-let f_spec = do {
-    llvm_ptr "x" (llvm_int 32);
-    llvm_assert_null "x";
-    llvm_return {{ 1 : [32] }};
-    llvm_verify_tactic abc;
+let f_spec1 = do {
+    p <- crucible_alloc (llvm_int 32);
+    crucible_execute_func [p];
+    crucible_return (crucible_term {{ 0 : [32] }});
 };
 
 let f_spec2 = do {
-    llvm_ptr "x" (llvm_int 32);
-    llvm_return {{ 0 : [32] }};
-    llvm_verify_tactic abc;
+    crucible_execute_func [crucible_null];
+    crucible_return (crucible_term {{ 1 : [32] }});
 };
 
 m <- llvm_load_module "assert-null.bc";
-llvm_verify m "f" [] f_spec;
-llvm_verify m "f" [] f_spec2;
+crucible_llvm_verify m "f" [] false f_spec1 abc;
+crucible_llvm_verify m "f" [] false f_spec2 abc;

examples/llvm/assert.c

@@ -0,0 +1,5 @@
+#include <assert.h>
+
+void f(int x) {
+    assert(x != 0);
+}

examples/llvm/assert.saw

@@ -0,0 +1,8 @@
+let f_spec = do {
+  x <- crucible_fresh_var "x" (llvm_int 32);
+  crucible_precond {{ x > 0 }};
+  crucible_execute_func [crucible_term x];
+};
+
+m <- llvm_load_module "assert.bc";
+crucible_llvm_verify m "f" [] true f_spec abc;

examples/llvm/basic.saw

@@ -1,20 +1,17 @@
-enable_deprecated;
-let add_setup : LLVMSetup () = do {
-    x <- llvm_var "x" (llvm_int 32);
-    y <- llvm_var "y" (llvm_int 32);
-    llvm_return {{ x + y : [32] }};
-    llvm_verify_tactic abc;
+let add_setup = do {
+    x <- crucible_fresh_var "x" (llvm_int 32);
+    y <- crucible_fresh_var "y" (llvm_int 32);
+    crucible_execute_func [crucible_term x, crucible_term y];
+    crucible_return (crucible_term {{ x + y : [32] }});
 };
 
-let dbl_setup : LLVMSetup () = do {
-    x <- llvm_var "x" (llvm_int 32);
-    llvm_return {{ x + x : [32] }};
-    llvm_verify_tactic abc;
+let dbl_setup = do {
+    x <- crucible_fresh_var "x" (llvm_int 32);
+    crucible_execute_func [crucible_term x];
+    crucible_return (crucible_term {{ x + x : [32] }});
 };
 
-let main : TopLevel () = do {
-    m <- llvm_load_module "basic.bc";
-    add_ms <- llvm_verify m "add" [] add_setup;
-    llvm_verify m "dbl" [add_ms] dbl_setup;
-    print "Done.";
-};
+m <- llvm_load_module "basic.bc";
+add_ms <- crucible_llvm_verify m "add" [] false add_setup abc;
+crucible_llvm_verify m "dbl" [add_ms] false dbl_setup abc;
+print "Done.";

examples/llvm/dotprod_struct.saw

@@ -1,55 +1,30 @@
-enable_deprecated;
 import "dotprod.cry";
-m <- llvm_load_module "dotprod_struct.bc";
-xs <- fresh_symbolic "xs" {| [2][32] |};
-ys <- fresh_symbolic "ys" {| [2][32] |};
-let allocs = [ ("x", 1), ("y", 1), ("x->0", 2), ("y->0", 2) ];
-let inputs = [ ("*(x->0)", {{ xs }}, 2)
-             , ("*(y->0)", {{ ys }}, 2)
-             , ("x->1", {{ 2:[32] }}, 1)
-             , ("y->1", {{ 2:[32] }}, 1)
-             ];
-let outputs = [("return", 1)];
-t <- llvm_symexec m "dotprod_struct" allocs inputs outputs true;
-thm <- abstract_symbolic {{ t == dotprod xs ys }};
-prove_print abc thm;
 
-let dotprod_spec = do {
-    llvm_ptr "x" (llvm_struct "struct.vec_t");
-    llvm_ptr "y" (llvm_struct "struct.vec_t");
-    llvm_ptr "x->0" (llvm_array 2 (llvm_int 32));
-    llvm_ptr "y->0" (llvm_array 2 (llvm_int 32));
-    xs <- llvm_var "*(x->0)" (llvm_array 2 (llvm_int 32));
-    xn <- llvm_var "x->1" (llvm_int 32);
-    ys <- llvm_var "*(y->0)" (llvm_array 2 (llvm_int 32));
-    yn <- llvm_var "y->1" (llvm_int 32);
-    llvm_sat_branches true;
-    llvm_assert_eq "x->1" {{ 2:[32] }};
-    llvm_assert_eq "y->1" {{ 2:[32] }};
-    llvm_return {{ dotprod xs ys }};
-    llvm_verify_tactic abc;
+let alloc_init ty v = do {
+    p <- crucible_alloc ty;
+    crucible_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);
+    return (x, p);
 };
 
-let dotprod_wrap_spec = do {
-    llvm_ptr "x" (llvm_struct "struct.vec_t");
-    llvm_ptr "y" (llvm_struct "struct.vec_t");
-    llvm_ptr "x->0" (llvm_array 2 (llvm_int 32));
-    llvm_ptr "y->0" (llvm_array 2 (llvm_int 32));
-    xs <- llvm_var "*(x->0)" (llvm_array 2 (llvm_int 32));
-    xn <- llvm_var "x->1" (llvm_int 32);
-    ys <- llvm_var "*(y->0)" (llvm_array 2 (llvm_int 32));
-    yn <- llvm_var "y->1" (llvm_int 32);
-    llvm_assert_eq "x->1" {{ 2:[32] }};
-    llvm_assert_eq "y->1" {{ 2:[32] }};
-    llvm_return {{ dotprod xs ys }};
-    llvm_verify_tactic do {
-      simplify (add_cryptol_defs ["ecEq"] (cryptol_ss ()));
-      simplify (add_prelude_defs ["implies"] basic_ss);
-      simplify (add_prelude_eqs ["bvEq_refl"] basic_ss);
-      simplify (add_prelude_eqs ["or_True1"] basic_ss);
-      trivial;
-    };
+let dotprod_spec n = do {
+    let nt = crucible_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));
+    let xval = crucible_struct [ xsp, nt ];
+    let yval = crucible_struct [ ysp, nt ];
+    xp <- alloc_init (llvm_struct "struct.vec_t") xval;
+    yp <- alloc_init (llvm_struct "struct.vec_t") yval;
+    crucible_execute_func [xp, yp];
+    crucible_return (crucible_term {{ dotprod xs ys }});
 };
 
-dotprod_ov <- llvm_verify m "dotprod_struct" [] dotprod_spec;
-llvm_verify m "dotprod_wrap" [dotprod_ov] dotprod_wrap_spec;
+m <- llvm_load_module "dotprod_struct.bc";
+
+dotprod_ov <- crucible_llvm_verify m "dotprod_struct" [] true (dotprod_spec 2) z3;
+crucible_llvm_verify m "dotprod_wrap" [dotprod_ov] true (dotprod_spec 2) z3;