Merge pull request #1546 from GaloisInc/heapster/unify-unit-variables

Unify unit variables in heapster

heapster-saw/examples/_CoqProject

@@ -32,5 +32,7 @@ exp_explosion_gen.v
 exp_explosion_proofs.v
 mbox_gen.v
 mbox_proofs.v
+global_var_gen.v
+global_var_proofs.v
 sha512_gen.v
 #sha512_proofs.v

heapster-saw/examples/global_var.c

@@ -0,0 +1,56 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+/* A very simple acquire/release lock for some shared data */
+
+int64_t shared_data = 0;
+int64_t lock = 0;
+
+/* A spin lock; returns 1 after acquireing lock, otherwise runs forever.
+   (Not robust to concurrent semantics) */
+int64_t acquire_lock(int64_t** data) {
+  while (lock != 0) {
+    continue;
+ }
+  lock = 1;
+  *data = &shared_data;
+  return 1;
+}
+
+/* To be called after a thread is done accessing the shared data. */ 
+void release_lock(void) {
+  lock = 0;
+  return;
+}
+
+
+int64_t acquire_release_acquire_release(void) {
+
+  int64_t* data;
+  acquire_lock(&data);
+  *data = 42;
+  release_lock();
+
+  acquire_lock(&data);
+  if (data == NULL) {
+    return -1;
+  }
+  int64_t val = *data;
+  release_lock();
+  return val;
+}
+
+int64_t acquire_release_fail(void) {
+  int64_t* data;
+  acquire_lock(&data);
+  *data = 42;
+  release_lock();
+
+  *data = 84;
+
+  // shared data should still be 42
+  acquire_lock(&data);
+  int64_t val = *data;
+  release_lock();
+  return val;
+}

heapster-saw/examples/global_var.saw

@@ -0,0 +1,73 @@
+enable_experimental;
+env <- heapster_init_env_from_file "global_var.sawcore" "global_var.bc";
+
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+
+// Demonstrates one technique for dealing with global variables and environment
+// permissions like locks
+
+
+
+// A heapster type for the lock global variable"
+//
+// The rwmodality makes the permission not copyable when provided the write
+// modality.
+//
+// When extracted to Coq, u:has_lock_perm<W> and u:can_lock_perm<W> are
+// bitvectors representing the value stored in the shared_data variable
+heapster_define_opaque_perm env "has_lock_perm"
+    "rw:rwmodality, dat:llvmptr 64"
+    "unit"
+    "Vec 64 Bool";
+
+heapster_define_opaque_perm env "can_lock_perm"
+    "rw:rwmodality"
+    "unit"
+    "Vec 64 Bool";
+
+// Need to axiomatize acquire_lock because it touches the global variables
+heapster_assume_fun env
+    "acquire_lock"
+
+    "(u:unit). \
+    \ arg0:ptr((W,0) |-> true), \
+    \ u:can_lock_perm<W> \
+    \ -o \
+    \ (dat:llvmptr 64). \
+    \ ret:eq(llvmword(1)), \
+    \ arg0:ptr((W,0) |-> eq(dat)), \
+    \ dat:ptr((W,0) |-> int64<>), \
+    \ u:has_lock_perm<W,dat>"
+
+    "acquireLockM";
+
+heapster_assume_fun env
+    "release_lock"
+
+    "(u:unit, dat:llvmptr 64). \
+    \ u:has_lock_perm<W,dat>, \
+    \ dat:ptr((W,0) |-> int64<>) \
+    \ -o \
+    \ ret:true, \
+    \ u:can_lock_perm<W>"
+
+    "releaseLockM";
+
+
+
+heapster_typecheck_fun env
+    "acquire_release_acquire_release"
+    "(u:unit). u:can_lock_perm<W> \
+    \ -o \
+    \ ret:int64<>, u:can_lock_perm<W>";
+
+heapster_typecheck_fun env
+    "acquire_release_fail"
+    "(u:unit). u:can_lock_perm<W> \
+    \ -o \
+    \ ret:int64<>, u:can_lock_perm<W>";
+
+
+heapster_export_coq env "global_var_gen.v";

heapster-saw/examples/global_var.sawcore

@@ -0,0 +1,10 @@
+module GlobalVar where
+
+import Prelude;
+
+acquireLockM : Vec 64 Bool -> CompM (Vec 64 Bool * Vec 64 Bool);
+acquireLockM u = returnM (Vec 64 Bool * Vec 64 Bool)
+			 (u,u);
+
+releaseLockM : Vec 64 Bool -> Vec 64 Bool -> CompM (Vec 64 Bool);
+releaseLockM u new_u = returnM (Vec 64 Bool) new_u;

heapster-saw/examples/global_var_proofs.v

@@ -0,0 +1,56 @@
+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.global_var_gen.
+Import GlobalVar.
+
+Import SAWCorePrelude.
+
+Lemma no_errors_acquire_release_acquire_release :
+    refinesFun acquire_release_acquire_release (fun _ => noErrorsSpec).
+Proof.
+    unfold acquire_release_acquire_release,
+           acquire_release_acquire_release__tuple_fun,
+           noErrorsSpec,
+           acquireLockM, releaseLockM.
+    prove_refinement.
+Qed.
+
+
+Definition acquire_release_acquire_release_spec (x : bitvector 64)
+    : CompM (can_lock_perm * bitvector 64) :=
+    returnM (intToBv 64 42, intToBv 64 42).
+
+Lemma spec_acquire_release_acquire_release :
+        refinesFun acquire_release_acquire_release
+                   acquire_release_acquire_release_spec.
+Proof.
+    unfold acquire_release_acquire_release,
+           acquire_release_acquire_release__tuple_fun,
+           acquire_release_acquire_release_spec,
+           acquireLockM, releaseLockM,
+           projT2.
+    prove_refinement.
+Qed.
+
+
+Definition errorSpec {A} : CompM A := existsM (fun (s : string) => errorM s).
+
+Lemma errors_acquire_release_fail : refinesFun acquire_release_fail
+                                               (fun _ => errorSpec).
+Proof.
+    unfold acquire_release_fail, acquire_release_fail__tuple_fun,
+           errorSpec,
+           acquireLockM, releaseLockM,
+           projT2.
+    prove_refinement.
+Qed.
+

heapster-saw/examples/mbox_proofs.v

@@ -382,8 +382,8 @@ Proof.
   (* Most of the remaining cases are taken care of with just bvAdd_id_l and bvAdd_id_r *)
   all: try rewrite bvAdd_id_r; try rewrite bvAdd_id_l; try reflexivity.
   (* The remaining case just needs a few more rewrites *)
-  - rewrite bvAdd_assoc, bvAdd_comm, bvAdd_assoc; reflexivity.
-  - cbn; rewrite transMbox_Mbox_nil_r; reflexivity.
+  - simpl. f_equal. rewrite bvAdd_assoc. f_equal. rewrite bvAdd_comm. f_equal.
+    simpl. rewrite transMbox_Mbox_nil_r. reflexivity.
 Time Qed.
 
 
@@ -467,6 +467,7 @@ Proof.
   - rewrite e_forall0 in e_maybe0.
     discriminate e_maybe0.
   (* TODO Add the sort of reasoning in the next two cases back into the automation? *)
+
   - rewrite a in e_maybe1.
     discriminate e_maybe1.
   - rewrite a1 in e_maybe2.