Merge pull request #1545 from GaloisInc/heapster/sawLet

[Heapster] Don't use Coq let-bindings in Heapster specs

heapster-saw/examples/_CoqProject

@@ -28,7 +28,9 @@ arrays_gen.v
 arrays_proofs.v
 clearbufs_gen.v
 clearbufs_proofs.v
+exp_explosion_gen.v
+exp_explosion_proofs.v
 mbox_gen.v
 mbox_proofs.v
-#sha512_gen.v
+sha512_gen.v
 #sha512_proofs.v

heapster-saw/examples/arrays_proofs.v

@@ -237,7 +237,7 @@ Proof.
   unfold even_odd_sums_diff_invar, noErrorsSpec.
   time "even_odd_sums_diff" prove_refinement.
   all: try assumption.
-  - enough (isBvult 64 (bvSub 64 a4 (intToBv 64 1)) (bvMul 64 (intToBv 64 2) a1))
+  - enough (isBvult 64 a2 (bvMul 64 (intToBv 64 2) a1))
       by (rewrite H in e_maybe; discriminate e_maybe).
     rewrite <- e_if.
     assert (isBvsle 64 (intToBv 64 0) a4) by (apply isBvslt_to_isBvsle; eauto).
@@ -246,7 +246,8 @@ Proof.
       (* apply isBvsle_bvSub_inj_pos. *)
       (* I give up I'm done messing around manually with bitvectors for now *)
       admit.
-    + apply isBvslt_pred_l; eauto.
+    + rewrite e_let.
+      apply isBvslt_pred_l; eauto.
       rewrite <- e_assuming; reflexivity.
   - (* (e_if4 is a contradiction) *)
     admit.

heapster-saw/examples/exp_explosion.c

@@ -0,0 +1,23 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+#define op(x,y) x ^ (y << 1)
+
+int64_t exp_explosion(int64_t x0) {
+  int64_t x1 = op(x0, x0);
+  int64_t x2 = op(x1, x1);
+  int64_t x3 = op(x2, x2);
+  int64_t x4 = op(x3, x3);
+  int64_t x5 = op(x4, x4);
+  int64_t x6 = op(x5, x5);
+  int64_t x7 = op(x6, x6);
+  int64_t x8 = op(x7, x7);
+  int64_t x9 = op(x8, x8);
+  int64_t x10 = op(x9, x9);
+  int64_t x11 = op(x10, x10);
+  int64_t x12 = op(x11, x11);
+  int64_t x13 = op(x12, x12);
+  int64_t x14 = op(x13, x13);
+  int64_t x15 = op(x14, x14);
+  return x15;
+}

heapster-saw/examples/exp_explosion.saw

@@ -0,0 +1,9 @@
+enable_experimental;
+env <- heapster_init_env "exp_explosion" "exp_explosion.bc";
+
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+heapster_typecheck_fun env "exp_explosion"
+  "(). arg0:int64<> -o arg0:int64<>, ret:int64<>";
+
+heapster_export_coq env "exp_explosion_gen.v";

heapster-saw/examples/exp_explosion_proofs.v

@@ -0,0 +1,20 @@
+From Coq          Require Import Lists.List.
+From Coq          Require Import String.
+From Coq          Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+From CryptolToCoq Require Import SAWCoreBitvectors.
+
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import CompMExtra.
+
+Require Import Examples.exp_explosion_gen.
+Import exp_explosion.
+
+Import SAWCorePrelude.
+
+Lemma no_errors_explosion : refinesFun exp_explosion (fun _ => noErrorsSpec).
+Proof.
+  unfold exp_explosion, exp_explosion__tuple_fun, noErrorsSpec.
+  time "no_errors_exp_explosion" prove_refinement.
+Qed.

heapster-saw/examples/linked_list_proofs.v

@@ -22,7 +22,7 @@ Qed.
 
 Lemma no_errors_is_elem_manual : refinesFun is_elem (fun _ _ => noErrorsSpec).
 Proof.
-  unfold is_elem, is_elem__tuple_fun.
+  unfold is_elem, is_elem__tuple_fun, sawLet_def.
   unfold noErrorsSpec.
   apply refinesFun_multiFixM_fst; intros x l.
   apply refinesM_letRecM_Nil_l.
@@ -62,7 +62,7 @@ Qed.
 
 Lemma is_elem_fun_ref_manual : refinesFun is_elem is_elem_fun.
 Proof.
-  unfold is_elem, is_elem__tuple_fun, is_elem_fun.
+  unfold is_elem, is_elem__tuple_fun, is_elem_fun, sawLet_def.
   apply refinesFun_multiFixM_fst; intros x l.
   apply refinesM_letRecM_Nil_l.
   apply refinesM_either_l; intros [] e_either.

heapster-saw/examples/sha512.c

@@ -2,103 +2,6 @@
 #include <stdint.h>
 #include <string.h>
 
-// First simplication of sha512_block_data_order
-
-static inline uint64_t SIMPL1_CRYPTO_load_u64_be(const void *ptr) {
-  uint64_t ret;
-  memcpy(&ret, ptr, sizeof(ret));
-  return ret;
-}
-
-static const uint64_t SIMPL1_K512[80] = {
-    UINT64_C(0x428a2f98d728ae22), UINT64_C(0x7137449123ef65cd),
-    UINT64_C(0xb5c0fbcfec4d3b2f), UINT64_C(0xe9b5dba58189dbbc),
-    UINT64_C(0x3956c25bf348b538), UINT64_C(0x59f111f1b605d019),
-    UINT64_C(0x923f82a4af194f9b), UINT64_C(0xab1c5ed5da6d8118),
-    UINT64_C(0xd807aa98a3030242), UINT64_C(0x12835b0145706fbe),
-    UINT64_C(0x243185be4ee4b28c), UINT64_C(0x550c7dc3d5ffb4e2),
-    UINT64_C(0x72be5d74f27b896f), UINT64_C(0x80deb1fe3b1696b1),
-    UINT64_C(0x9bdc06a725c71235), UINT64_C(0xc19bf174cf692694),
-    UINT64_C(0xe49b69c19ef14ad2), UINT64_C(0xefbe4786384f25e3),
-    UINT64_C(0x0fc19dc68b8cd5b5), UINT64_C(0x240ca1cc77ac9c65),
-    UINT64_C(0x2de92c6f592b0275), UINT64_C(0x4a7484aa6ea6e483),
-    UINT64_C(0x5cb0a9dcbd41fbd4), UINT64_C(0x76f988da831153b5),
-    UINT64_C(0x983e5152ee66dfab), UINT64_C(0xa831c66d2db43210),
-    UINT64_C(0xb00327c898fb213f), UINT64_C(0xbf597fc7beef0ee4),
-    UINT64_C(0xc6e00bf33da88fc2), UINT64_C(0xd5a79147930aa725),
-    UINT64_C(0x06ca6351e003826f), UINT64_C(0x142929670a0e6e70),
-    UINT64_C(0x27b70a8546d22ffc), UINT64_C(0x2e1b21385c26c926),
-    UINT64_C(0x4d2c6dfc5ac42aed), UINT64_C(0x53380d139d95b3df),
-    UINT64_C(0x650a73548baf63de), UINT64_C(0x766a0abb3c77b2a8),
-    UINT64_C(0x81c2c92e47edaee6), UINT64_C(0x92722c851482353b),
-    UINT64_C(0xa2bfe8a14cf10364), UINT64_C(0xa81a664bbc423001),
-    UINT64_C(0xc24b8b70d0f89791), UINT64_C(0xc76c51a30654be30),
-    UINT64_C(0xd192e819d6ef5218), UINT64_C(0xd69906245565a910),
-    UINT64_C(0xf40e35855771202a), UINT64_C(0x106aa07032bbd1b8),
-    UINT64_C(0x19a4c116b8d2d0c8), UINT64_C(0x1e376c085141ab53),
-    UINT64_C(0x2748774cdf8eeb99), UINT64_C(0x34b0bcb5e19b48a8),
-    UINT64_C(0x391c0cb3c5c95a63), UINT64_C(0x4ed8aa4ae3418acb),
-    UINT64_C(0x5b9cca4f7763e373), UINT64_C(0x682e6ff3d6b2b8a3),
-    UINT64_C(0x748f82ee5defb2fc), UINT64_C(0x78a5636f43172f60),
-    UINT64_C(0x84c87814a1f0ab72), UINT64_C(0x8cc702081a6439ec),
-    UINT64_C(0x90befffa23631e28), UINT64_C(0xa4506cebde82bde9),
-    UINT64_C(0xbef9a3f7b2c67915), UINT64_C(0xc67178f2e372532b),
-    UINT64_C(0xca273eceea26619c), UINT64_C(0xd186b8c721c0c207),
-    UINT64_C(0xeada7dd6cde0eb1e), UINT64_C(0xf57d4f7fee6ed178),
-    UINT64_C(0x06f067aa72176fba), UINT64_C(0x0a637dc5a2c898a6),
-    UINT64_C(0x113f9804bef90dae), UINT64_C(0x1b710b35131c471b),
-    UINT64_C(0x28db77f523047d84), UINT64_C(0x32caab7b40c72493),
-    UINT64_C(0x3c9ebe0a15c9bebc), UINT64_C(0x431d67c49c100d4c),
-    UINT64_C(0x4cc5d4becb3e42b6), UINT64_C(0x597f299cfc657e2a),
-    UINT64_C(0x5fcb6fab3ad6faec), UINT64_C(0x6c44198c4a475817),
-};
-
-#define SIMPL1_ROUND_00_01(i, a, b) \
-  do {                              \
-    T1 += a + SIMPL1_K512[i];       \
-    a += T1;                        \
-    b += T1;                        \
-  } while (0)
-
-#define SIMPL1_ROUND_02_10(i, j, a, b) \
-  do {                                 \
-    SIMPL1_ROUND_00_01(i + j, a, b);   \
-  } while (0)
-
-void simpl1_return_state(uint64_t *state) {
-
-}
-
-uint64_t sha512_block_data_order_simpl1(uint64_t *state, const uint8_t *in, size_t num) {
-  uint64_t a, b, T1;
-  int i;
-
-  while (num--) {
-
-    a = state[0];
-    b = state[1];
-    simpl1_return_state(state);
-
-    T1 = SIMPL1_CRYPTO_load_u64_be(in);
-    SIMPL1_ROUND_00_01(0, a, b);
-    T1 = SIMPL1_CRYPTO_load_u64_be(in + 8);
-    SIMPL1_ROUND_00_01(1, a, b);
-
-    for (i = 2; i < 10; i += 2) {
-      SIMPL1_ROUND_02_10(i, 0, a, b);
-      SIMPL1_ROUND_02_10(i, 1, a, b);
-    }
-
-    state[0] += a;
-    state[1] += b;
-
-    in += 2 * 8;
-  }
-  return a;
-}
-
-// sha512_block_data_order
-
 static inline void *OPENSSL_memcpy(void *dst, const void *src, size_t n) {
   if (n == 0) {
     return dst;
@@ -196,9 +99,7 @@ static const uint64_t K512[80] = {
     ROUND_00_15(i + j, a, b, c, d, e, f, g, h);        \
   } while (0)
 
-void return_state(uint64_t *state) {
-
-}
+void return_state(uint64_t *state) { }
 
 static void sha512_block_data_order(uint64_t *state, const uint8_t *in,
                                     size_t num) {
@@ -216,7 +117,7 @@ static void sha512_block_data_order(uint64_t *state, const uint8_t *in,
     f = state[5];
     g = state[6];
     h = state[7];
-    return_state(state);
+    return_state(state); // for Heapster
 
     T1 = X[0] = CRYPTO_load_u64_be(in);
     ROUND_00_15(0, a, b, c, d, e, f, g, h);
@@ -283,6 +184,7 @@ static void sha512_block_data_order(uint64_t *state, const uint8_t *in,
   }
 }
 
+// needed for Heapster to be able to see the static function above
 void dummy(uint64_t *state, const uint8_t *in, size_t num) {
   sha512_block_data_order(state, in, num);
 }

heapster-saw/examples/sha512.saw

@@ -1,60 +1,12 @@
 enable_experimental;
 env <- heapster_init_env "SHA512" "sha512.bc";
 
-heapster_set_debug_level env 1;
+// heapster_set_debug_level env 1;
 
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))";
 heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
 
-heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
-  "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, \
-   \ b:llvmblock 64, len:bv 64). \
-  \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), \
-  \ arg2:eq(llvmword(len)) -o \
-  \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))"
-  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
-
-/*
-heapster_typecheck_fun env "SIMPL1_CRYPTO_load_u64_be"
-  "(). arg0:ptr((R,0) |-> int64<>) -o \
-     \ arg0:ptr((R,0) |-> int64<>), ret:int64<>";
-
-heapster_typecheck_fun env "simpl1_return_state"
-  "(). arg0:array(W,0,<2,*8,fieldsh(int64<>)) -o \
-     \ arg0:array(W,0,<2,*8,fieldsh(int64<>))";
-
-heapster_typecheck_fun env "sha512_block_data_order_simpl1"
-  "(num:bv 64). arg0:array(W,0,<2,*8,fieldsh(int64<>)), \
-              \ arg1:array(R,0,<2*num,*8,fieldsh(int64<>)), \
-              \ arg2:eq(llvmword(num)) -o \
-              \ arg0:array(W,0,<2,*8,fieldsh(int64<>)), \
-              \ arg1:array(R,0,<2*num,*8,fieldsh(int64<>)), \
-              \ arg2:true, ret:true";
-// arg0:array(W,0,<1,*8,fieldsh(int64<>))
-*/
-
-/*
-// A copy of the permissions for memcpy
-heapster_assume_fun env "OPENSSL_memcpy"
-  "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, \
-   \ b:llvmblock 64, len:bv 64). \
-  \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), \
-  \ arg2:eq(llvmword(len)) -o \
-  \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))"
-  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
-
-heapster_typecheck_fun env "CRYPTO_bswap4"
-  "(). arg0:int32<> -o arg0:int32<>, ret:int32<>";
-
-heapster_typecheck_fun env "CRYPTO_bswap8"
-  "(). arg0:int64<> -o arg0:int64<>, ret:int64<>";
-
-heapster_typecheck_fun env "CRYPTO_load_u64_be"
-  "(). arg0:ptr((R,0) |-> int64<>) -o \
-     \ arg0:ptr((R,0) |-> int64<>), ret:int64<>";
-*/
-
 heapster_assume_fun env "CRYPTO_load_u64_be"
   "(). arg0:ptr((R,0) |-> int64<>) -o \
      \ arg0:ptr((R,0) |-> int64<>), ret:int64<>"
@@ -73,5 +25,4 @@ heapster_typecheck_fun env "sha512_block_data_order"
               \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \
               \ arg2:true, ret:true";
 
-
 heapster_export_coq env "sha512_gen.v";

heapster-saw/examples/sha512_proofs.v

@@ -14,8 +14,14 @@ Import SAWCorePrelude.
 Require Import Examples.sha512_gen.
 Import SHA512.
 
-Lemma no_errors_sha512_block_data_order_simpl1 :
-  refinesFun sha512_block_data_order_simpl1 (fun _ _ _ => noErrorsSpec).
+Definition sha512_block_data_order_precond num := isBvslt 64 (intToBv 64 0) num.
+
+Lemma no_errors_sha512_block_data_order :
+  refinesFun sha512_block_data_order
+             (fun num _ _ => assumingM (sha512_block_data_order_precond num) noErrorsSpec).
 Proof.
-  unfold sha512_block_data_order_simpl1, sha512_block_data_order_simpl1__tuple_fun.
-  Set Printing Depth 1000.
+  unfold sha512_block_data_order, sha512_block_data_order__tuple_fun.
+  (* time "sha512_block_data_order (1)" prove_refinement_match_letRecM_l. *)
+  (* 1-2: intros; apply noErrorsSpec. *)
+  (* time "sha512_block_data_order (2)" prove_refinement. *)
+Admitted.

heapster-saw/examples/xor_swap_proofs.v

@@ -41,6 +41,6 @@ Qed.
 Lemma xor_swap_correct : refinesFun xor_swap xor_swap_spec.
 Proof.
   prove_refinement.
-  rewrite bvXor_twice_r. rewrite bvXor_twice_l.
+  subst. rewrite bvXor_twice_r. rewrite bvXor_twice_l.
   reflexivity.
 Qed.

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

@@ -318,13 +318,13 @@ inExtMultiTransM MNil m = m
 inExtMultiTransM (ctx :>: etrans) m =
   inExtMultiTransM ctx $ inExtTransM etrans m
 
--- | Run a translation computation in an extended context, where we let-bind any
+-- | Run a translation computation in an extended context, where we sawLet-bind any
 -- term in the supplied expression translation
-inExtTransLetBindM :: TransInfo info => TypeTrans (ExprTrans tp) ->
-                      ExprTrans tp -> TransM info (ctx :> tp) OpenTerm ->
-                      TransM info ctx OpenTerm
-inExtTransLetBindM tp_trans etrans m =
-  letTransMultiM "z" (typeTransTypes tp_trans) (transTerms etrans) $ \var_tms ->
+inExtTransSAWLetBindM :: TransInfo info => TypeTrans (ExprTrans tp) -> OpenTerm ->
+                         ExprTrans tp -> TransM info (ctx :> tp) OpenTerm ->
+                         TransM info ctx OpenTerm
+inExtTransSAWLetBindM tp_trans tp_ret etrans m =
+  sawLetTransMultiM "z" (typeTransTypes tp_trans) tp_ret (transTerms etrans) $ \var_tms ->
   inExtTransM (typeTransF tp_trans var_tms) m
 
 -- | Run a translation computation in context @(ctx1 :++: ctx2) :++: ctx2@ by
@@ -424,17 +424,27 @@ letTransM x tp rhs_m body_m =
      return $
        letOpenTerm (pack x) tp (runTransM rhs_m r) (\x' -> runTransM (body_m x') r)
 
--- | Build 0 or more let-bindings in a translation monad, using the same
+-- | Build a sawLet-binding in a translation monad
+sawLetTransM :: String -> OpenTerm -> OpenTerm -> TransM info ctx OpenTerm ->
+                (OpenTerm -> TransM info ctx OpenTerm) ->
+                TransM info ctx OpenTerm
+sawLetTransM x tp tp_ret rhs_m body_m =
+  do r <- ask
+     return $
+       sawLetOpenTerm (pack x) tp tp_ret (runTransM rhs_m r)
+                      (\x' -> runTransM (body_m x') r)
+
+-- | Build 0 or more sawLet-bindings in a translation monad, using the same
 -- variable name
-letTransMultiM :: String -> [OpenTerm] -> [OpenTerm] ->
+sawLetTransMultiM :: String -> [OpenTerm] -> OpenTerm -> [OpenTerm] ->
                   ([OpenTerm] -> TransM info ctx OpenTerm) ->
                   TransM info ctx OpenTerm
-letTransMultiM _ [] [] f = f []
-letTransMultiM x (tp:tps) (rhs:rhss) f =
-  letTransM x tp (return rhs) $ \var_tm ->
-  letTransMultiM x tps rhss (\var_tms -> f (var_tm:var_tms))
-letTransMultiM _ _ _ _ =
-  error "letTransMultiM: numbers of types and right-hand sides disagree"
+sawLetTransMultiM _ [] _ [] f = f []
+sawLetTransMultiM x (tp:tps) ret_tp (rhs:rhss) f =
+  sawLetTransM x tp ret_tp (return rhs) $ \var_tm ->
+  sawLetTransMultiM x tps ret_tp rhss (\var_tms -> f (var_tm:var_tms))
+sawLetTransMultiM _ _ _ _ _ =
+  error "sawLetTransMultiM: numbers of types and right-hand sides disagree"
 
 -- | Build a bitvector type in a translation monad
 bitvectorTransM :: TransM info ctx OpenTerm -> TransM info ctx OpenTerm
@@ -4210,9 +4220,10 @@ translateStmt :: PermCheckExtC ext =>
 translateStmt loc mb_stmt m = case mbMatch mb_stmt of
   [nuMP| TypedSetReg tp e |] ->
     do tp_trans <- translate tp
+       tp_ret <- compReturnTypeM
        etrans <- tpTransM $ translate e
        let ptrans = exprOutPerm e
-       inExtTransLetBindM tp_trans etrans $
+       inExtTransSAWLetBindM tp_trans tp_ret etrans $
          withPermStackM (:>: Member_Base) (:>: extPermTrans ptrans) m
 
   [nuMP| TypedSetRegPermExpr _ e |] ->