Merge pull request #1373 from GaloisInc/heapster-improved-ptr-impls

Improved ptr permission implications

heapster-saw/examples/Makefile

@@ -52,3 +52,6 @@ rust_lifetimes.bc: rust_lifetimes.rs
 
 rust_lifetimes.v: rust_lifetimes.bc rust_lifetimes.saw
 	$(SAW) rust_lifetimes.saw
+
+clearbufs.v: clearbufs.bc clearbufs.saw clearbufs.sawcore
+	$(SAW) clearbufs.saw

heapster-saw/examples/_CoqProject

@@ -23,3 +23,5 @@ rust_data_proofs.v
 rust_lifetimes.v
 rust_lifetimes_proofs.v
 arrays.v
+clearbufs.v
+clearbufs_proofs.v

heapster-saw/examples/clearbufs.c

@@ -0,0 +1,32 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+typedef struct bufs {
+  struct bufs * next;
+  int64_t len;
+  int64_t data [];
+} bufs;
+
+void clearbufs (bufs * lst)
+{
+  // NOTE: the input value of lst is stored in a stack-allocated variable, which
+  // is also called lst below, but is called lp in the paper. This is sort-of
+  // like the following code, except that the following would actually make a
+  // second stack slot for variable lp, unlike the paper example.
+  //
+  // bufs **lp = alloca(8)
+  // *lp = lst;
+
+  while (1) {
+    // NOTE: reading lst here and testing for NULL 
+    //
+    // bufs *l = lst = *lp
+    // if (l == NULL) { ... }
+    if (lst == NULL) {
+      return;
+    } else {
+      lst->data[0] = 0;
+      lst = lst->next;
+    }
+  }
+}

heapster-saw/examples/clearbufs.saw

@@ -0,0 +1,13 @@
+enable_experimental;
+env <- heapster_init_env_from_file "clearbufs.sawcore" "clearbufs.bc";
+
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+heapster_define_reachability_perm env "Bufs" "x:llvmptr 64" "llvmptr 64" "exists len:(bv 64).ptr((W,0) |-> Bufs<x>) * ptr((W,8) |-> eq(llvmword(len))) * array(16, <len, *8, [(W,0) |-> int64<>])" "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
+
+heapster_block_entry_hint env "clearbufs" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:Bufs<ghost>, arg0:ptr((W,0) |-> eq(ghost)), ghost:Bufs<llvmword(0)>,frm:llvmframe [arg0:8]";
+
+heapster_typecheck_fun env "clearbufs" "().arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
+
+heapster_export_coq env "clearbufs.v";

heapster-saw/examples/clearbufs.sawcore

@@ -0,0 +1,63 @@
+
+module clearbufs where
+
+import Prelude;
+
+BV64 : sort 0;
+BV64 = Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #());
+
+V64 : sort 0;
+V64 = Vec 64 Bool;
+
+-- Harcoded 64 length bitvector value 16, used for mbox definitions
+bv64_16 : Vec 64 Bool;
+bv64_16 = [False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,True,False,False,False,False];
+
+data Mbox : sort 0 where {
+  Mbox_nil : Mbox;
+  Mbox_cons : Mbox -> (len : Vec 64 Bool) -> BVVec 64 len BV64 -> Mbox;
+}
+
+-- A definition for the Mbox datatype; currently needed as a workaround in Heapster
+Mbox_def : sort 0;
+Mbox_def = Mbox;
+
+{- Mbox__rec : (P : Mbox -> sort 0) ->
+            (P Mbox_nil) ->
+            ((m:Mbox) -> P m -> (len:BV64) -> (d:BVVec 64 bv64_16 BV64) -> P (Mbox_cons m len d)) ->
+            (m:Mbox) -> P m;
+Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}
+
+--unfoldMbox : Mbox -> Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #());
+primitive
+unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len BV64 * #()));
+
+{-unfoldMbox m =
+  Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()))
+  (Left #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()) ())
+  (\ (m:Mbox) (_:Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #())) (len:BV64) (d:BVVec 64 bv64_16 BV64) ->
+     Right #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()) (m, len, d, ()))
+  m;
+  -}
+
+primitive
+foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len BV64 * #())) -> Mbox;
+
+--(Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #()) -> Mbox;
+{-
+foldMbox =
+  either #() (Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #()) Mbox
+         (\ (_:#()) -> Mbox_nil)
+         (\ (tup : (Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #())) ->
+            Mbox_cons tup.1 tup.2 tup.3);
+			-}
+
+primitive
+transMbox : Mbox -> Mbox -> Mbox;
+{-
+transMbox m1 m2 =
+  Mbox__rec (\ (_ : Mbox) -> Mbox)
+  m2
+  (\ (_ : Mbox) (rec:Mbox) (len : BV64) (vec : BVVec 64 bv64_16 BV64) -> Mbox_cons rec len vec)
+  m1;
+-}

heapster-saw/examples/clearbufs_proofs.v

@@ -0,0 +1,14 @@
+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.clearbufs.
+Import clearbufs.
+
+(* Eval cbn in clearbufs__tuple_fun. *)

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

@@ -5865,8 +5865,13 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
     partialSubstForceM (fmap llvmFieldOffset mb_fp) "proveVarPtrPerms" >>>= \off ->
     foldMapWithDefault implCatchM
     (proveVarAtomicImplUnfoldOrFail x ps mb_p)
-    (\(i,_) -> proveVarLLVMField x ps i off mb_fp)
-    (findMaybeIndices (llvmPermContainsOffset off) ps)
+    (\(i,_) -> proveVarLLVMField x ps i off mb_fp) $
+    -- If there are any permissions that definitely contain off, use those, and
+    -- otherwise iterate through all those that could contain off
+    let ixs_props = findMaybeIndices (llvmPermContainsOffset off) ps in
+    case filter (\(_,props) -> all bvPropHolds props) ixs_props of
+      [] -> ixs_props
+      ixs_props_hold -> ixs_props_hold
 
   [nuMP| Perm_LLVMArray mb_ap |] ->
     partialSubstForceM mb_ap "proveVarPtrPerms" >>>= \ap ->