Heapster: improved bitvector and automation support

heapster-saw/doc/Permissions.md

@@ -53,6 +53,7 @@ Any crucible type can have a variable of that type, and that thing is an express
 | `n`                          | `nat`              | A literal natural number |
 | `n`                          | `bv w`             | A literal bitvector |
 | `b1 + b2`                    | `bv w`             | Sum of two bitvectors |
+| `-b`                         | `bv w`             | 2's complement negation of a bitvector |
 | `b1 * b2`                    | `bv w`             | Linear multiplication of two bitvectors, meaning that one of the operands must be a constant |
 | `struct(e1,..,en)`           | `struct(a1,..,an)` | A (crucible) struct is a tuple of expressions for each argument of the struct type. Crucible structs are different from C structs, and we only use crucible structs when we need to, otherwise C structs are described manually as pointers into chunks of memory |
 | `llvmword(e)`                | `llvmptr(w)`       | An LLVM value that represents a word, i.e. whose region identifier is 0, given a bitvector expression `e:bv w` |

heapster-saw/examples/linked_list_proofs.v

@@ -16,37 +16,17 @@ Require Import Examples.linked_list_gen.
 Import linked_list.
 
 
-(* QOL: nicer names for bitvector and list arguments *)
-#[local] Hint Extern 901 (IntroArg Any (bitvector _) _) =>
-  let e := fresh "x" in IntroArg_intro e : refines prepostcond. 
+(* QOL: nicer names for list arguments *)
 #[local] Hint Extern 901 (IntroArg Any (list _) _) =>
   let e := fresh "l" in IntroArg_intro e : refines prepostcond. 
 #[local] Hint Extern 901 (IntroArg Any (List_def _) _) =>
   let e := fresh "l" in IntroArg_intro e : refines prepostcond. 
-
-#[local] Hint Extern 901 (IntroArg RetAny (bitvector _) _) =>
-  let e := fresh "r_x" in IntroArg_intro e : refines prepostcond. 
 #[local] Hint Extern 901 (IntroArg RetAny list _) =>
   let e := fresh "r_l" in IntroArg_intro e : refines prepostcond. 
 #[local] Hint Extern 901 (IntroArg RetAny List_def _) =>
   let e := fresh "r_l" in IntroArg_intro e : refines prepostcond.
 
 
-(* bitvector (in)equality automation *)
-
-Lemma simpl_llvm_bool_eq (b : bool) :
-  negb (bvEq 1 (if b then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = b.
-Proof. destruct b; eauto. Qed.
-
-Definition simpl_llvm_bool_eq_IntroArg n (b1 b2 : bool) (goal : Prop) :
-  IntroArg n (b1 = b2) (fun _ => goal) ->
-  IntroArg n (negb (bvEq 1 (if b1 then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = b2) (fun _ => goal).
-Proof. rewrite simpl_llvm_bool_eq; eauto. Defined.
-
-#[local] Hint Extern 101 (IntroArg _ (negb (bvEq 1 (if _ then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = _) _) =>
-  simple eapply simpl_llvm_bool_eq_IntroArg : refines.
-
-
 (* List destruction automation *)
 
 Arguments FunsTo_Nil {a}.

heapster-saw/examples/mbox_proofs.v

@@ -26,201 +26,7 @@ Require Import Examples.mbox_gen.
 Import mbox.
 
 
-
-(* QOL: nicer names for bitvector and mbox arguments *)
-#[local] Hint Extern 901 (IntroArg Any (bitvector _) _) =>
-  let e := fresh "x" in IntroArg_intro e : refines prepostcond.
-#[local] Hint Extern 901 (IntroArg Any Mbox _) =>
-  let e := fresh "m" in IntroArg_intro e : refines prepostcond.
-#[local] Hint Extern 901 (IntroArg Any Mbox_def _) =>
-  let e := fresh "m" in IntroArg_intro e : refines prepostcond.
-
-#[local] Hint Extern 901 (IntroArg RetAny (bitvector _) _) =>
-  let e := fresh "r_x" in IntroArg_intro e : refines prepostcond.
-#[local] Hint Extern 901 (IntroArg RetAny Mbox _) =>
-  let e := fresh "r_m" in IntroArg_intro e : refines prepostcond.
-#[local] Hint Extern 901 (IntroArg RetAny Mbox_def _) =>
-  let e := fresh "r_m" in IntroArg_intro e : refines prepostcond.
-
-
-(* Maybe automation - FIXME move to EnTree.Automation *)
-
-Lemma spec_refines_maybe_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  RR A t1 k1 mb (t2 : SpecM E2 Γ2 R2) :
-  (mb = Nothing _ -> spec_refines RPre RPost RR t1 t2) ->
-  (forall a, mb = Just _ a -> spec_refines RPre RPost RR (k1 a) t2) ->
-  spec_refines RPre RPost RR (maybe A (SpecM E1 Γ1 R1) t1 k1 mb) t2.
-Proof. destruct mb; intros; eauto. Qed.
-
-Lemma spec_refines_maybe_r (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  RR (t1 : SpecM E1 Γ1 R1) A t2 k2 mb :
-  (mb = Nothing _ -> spec_refines RPre RPost RR t1 t2) ->
-  (forall a, mb = Just _ a -> spec_refines RPre RPost RR t1 (k2 a)) ->
-  spec_refines RPre RPost RR t1 (maybe A (SpecM E2 Γ2 R2) t2 k2 mb).
-Proof. destruct mb; intros; eauto. Qed.
-
-Definition spec_refines_maybe_l_IntroArg (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  RR A t1 k1 mb (t2 : SpecM E2 Γ2 R2) :
-  (IntroArg Hyp (mb = Nothing _) (fun _ => spec_refines RPre RPost RR t1 t2)) ->
-  (IntroArg Any A (fun a => IntroArg Hyp (mb = Just _ a) (fun _ =>
-   spec_refines RPre RPost RR (k1 a) t2))) ->
-  spec_refines RPre RPost RR (maybe A (SpecM E1 Γ1 R1) t1 k1 mb) t2 :=
-  spec_refines_maybe_l E1 E2 Γ1 Γ2 R1 R2 RPre RPost RR A t1 k1 mb t2.
-
-Definition spec_refines_maybe_r_IntroArg (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  RR (t1 : SpecM E1 Γ1 R1) A t2 k2 mb :
-  (IntroArg Hyp (mb = Nothing _) (fun _ => spec_refines RPre RPost RR t1 t2)) ->
-  (IntroArg Any A (fun a => IntroArg Hyp (mb = Just _ a) (fun _ =>
-   spec_refines RPre RPost RR t1 (k2 a)))) ->
-  spec_refines RPre RPost RR t1 (maybe A (SpecM E2 Γ2 R2) t2 k2 mb) :=
-  spec_refines_maybe_r E1 E2 Γ1 Γ2 R1 R2 RPre RPost RR t1 A t2 k2 mb.
-
-#[global] Hint Extern 101 (spec_refines _ _ _ (maybe _ _ _ _ _) _) =>
-  simple apply spec_refines_maybe_l_IntroArg : refines.
-#[global] Hint Extern 101 (spec_refines _ _ _ _ (maybe _ _ _ _ _)) =>
-  simple apply spec_refines_maybe_r_IntroArg : refines.
-
-Lemma IntroArg_eq_Nothing_const n A (goal : Prop)
-  : goal -> IntroArg n (Nothing A = Nothing A) (fun _ => goal).
-Proof. intros H eq; eauto. Qed.
-Lemma IntroArg_eq_Just_const n A (x y : A) (goal : Prop)
-  : IntroArg n (x = y) (fun _ => goal) ->
-    IntroArg n (Just A x = Just A y) (fun _ => goal).
-Proof. intros H eq; apply H; injection eq; eauto. Qed.
-Lemma IntroArg_eq_Nothing_Just n A (x : A) goal
-  : IntroArg n (Nothing A = Just A x) goal.
-Proof. intros eq; discriminate eq. Qed.
-Lemma IntroArg_eq_Just_Nothing n A (x : A) goal
-  : IntroArg n (Just A x = Nothing A) goal.
-Proof. intros eq; discriminate eq. Qed.
-
-#[global] Hint Extern 101 (IntroArg _ (Nothing _ = Nothing _) _) =>
-  simple apply IntroArg_eq_Nothing_const : refines.
-#[global] Hint Extern 101 (IntroArg _ (Just _ _ = Just _ _) _) =>
-  simple apply IntroArg_eq_Just_const : refines.
-#[global] Hint Extern 101 (IntroArg _ (Nothing _ = Just _ _) _) =>
-  apply IntroArg_eq_Nothing_Just : refines.
-#[global] Hint Extern 101 (IntroArg _ (Just _ _ = Nothing _) _) =>
-  apply IntroArg_eq_Just_Nothing : refines.
-
-
-(* sawLet automation *)
-
-Definition spec_refines_sawLet_const_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  (RR : Rel R1 R2) A (x : A) t1 t2 :
-  spec_refines RPre RPost RR t1 t2 ->
-  spec_refines RPre RPost RR (sawLet_def _ _ x (fun _ => t1)) t2 := fun pf => pf.
-Definition spec_refines_sawLet_const_r (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  (RR : Rel R1 R2) A (x : A) t1 t2 :
-  spec_refines RPre RPost RR t1 t2 ->
-  spec_refines RPre RPost RR t1 (sawLet_def _ _ x (fun _ => t2)) := fun pf => pf.
-
-Definition spec_refines_sawLet_bv_l_IntroArg (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  (RR : Rel R1 R2) w (x : bitvector w) k1 t2 :
-  IntroArg Any _ (fun a => IntroArg SAWLet (a = x) (fun _ =>
-    spec_refines RPre RPost RR (k1 a) t2)) ->
-  spec_refines RPre RPost RR (sawLet_def _ _ x k1) t2.
-Proof. intro H; eapply H; eauto. Qed.
-Definition spec_refines_sawLet_bv_r_IntroArg (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  (RR : Rel R1 R2) w (x : bitvector w) t1 k2 :
-  IntroArg Any _ (fun a => IntroArg SAWLet (a = x) (fun _ =>
-    spec_refines RPre RPost RR t1 (k2 a))) ->
-  spec_refines RPre RPost RR t1 (sawLet_def _ _ x k2).
-Proof. intro H; eapply H; eauto. Qed.
-
-Definition spec_refines_sawLet_unfold_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  (RR : Rel R1 R2) A (x : A) k1 t2 :
-  spec_refines RPre RPost RR (k1 x) t2 ->
-  spec_refines RPre RPost RR (sawLet_def _ _ x k1) t2 := fun pf => pf.
-Definition spec_refines_sawLet_unfold_r (E1 E2 : EvType) Γ1 Γ2 R1 R2
-  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
-  (RR : Rel R1 R2) A (x : A) t1 k2 :
-  spec_refines RPre RPost RR t1 (k2 x) ->
-  spec_refines RPre RPost RR t1 (sawLet_def _ _ x k2) := fun pf => pf.
-
-Ltac spec_refines_sawLet_l :=
-  first [ simple apply spec_refines_sawLet_const_l
-        | simple apply spec_refines_sawLet_bv_l_IntroArg
-        | simple apply spec_refines_sawLet_unfold_l ].
-Ltac spec_refines_sawLet_r :=
-  first [ simple apply spec_refines_sawLet_const_r
-        | simple apply spec_refines_sawLet_bv_r_IntroArg
-        | simple apply spec_refines_sawLet_unfold_r ].
-
-#[global] Hint Extern 101 (spec_refines _ _ _ (sawLet_def _ _ _ _) _) =>
-  spec_refines_sawLet_l : refines.
-#[global] Hint Extern 101 (spec_refines _ _ _ _ (sawLet_def _ _ _ _ )) =>
-  spec_refines_sawLet_r : refines.
-
-
-(* bitvector (in)equality automation *)
-
-Lemma simpl_llvm_bool_eq (b : bool) :
-  negb (bvEq 1 (if b then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = b.
-Proof. destruct b; eauto. Qed.
-
-Definition simpl_llvm_bool_eq_IntroArg n (b1 b2 : bool) (goal : Prop) :
-  IntroArg n (b1 = b2) (fun _ => goal) ->
-  IntroArg n (negb (bvEq 1 (if b1 then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = b2) (fun _ => goal).
-Proof. rewrite simpl_llvm_bool_eq; eauto. Defined.
-
-#[local] Hint Extern 101 (IntroArg _ (negb (bvEq 1 (if _ then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = _) _) =>
-  simple eapply simpl_llvm_bool_eq_IntroArg : refines.
-
-Polymorphic Lemma bvuleWithProof_not :
-  forall w a b,
-  bvuleWithProof w a b = Nothing _ <-> ~ (isBvule w a b).
-Proof.
-  unfold bvuleWithProof, isBvule.
-  split.
-  - intros H0 H1.
-    rewrite H1 in H0. simpl.
-    discriminate.
-  - intros H.
-    destruct (bvule w a b).
-      + contradiction.
-      + reflexivity.
-Qed.
-
-Polymorphic Lemma bvuleWithProof_not_IntroArg n w a b goal :
-  IntroArg n (~ (isBvule w a b)) (fun _ => goal) ->
-  IntroArg n (bvuleWithProof w a b = Nothing _) (fun _ => goal).
-Proof. intros H eq; apply H; apply bvuleWithProof_not; eauto. Qed.
-
-#[local] Hint Extern 101 (IntroArg _ (bvuleWithProof _ _ _ = Nothing _) _) =>
-  simple apply bvuleWithProof_not_IntroArg || shelve : refines.
-
-Polymorphic Lemma bvultWithProof_not :
-  forall w a b,
-  bvultWithProof w a b = Nothing _ <-> ~ (isBvult w a b).
-Proof.
-  unfold bvultWithProof, isBvult.
-  split.
-  - intros H0 H1.
-    rewrite H1 in H0. simpl.
-    discriminate.
-  - intros H.
-    destruct (bvult w a b).
-      + contradiction.
-      + reflexivity.
-Qed.
-
-Polymorphic Lemma bvultWithProof_not_IntroArg n w a b goal :
-  IntroArg n (~ (isBvult w a b)) (fun _ => goal) ->
-  IntroArg n (bvultWithProof w a b = Nothing _) (fun _ => goal).
-Proof. intros H eq; apply H; apply bvultWithProof_not; eauto. Qed.
-
-#[local] Hint Extern 101 (IntroArg _ (bvultWithProof _ _ _ = Nothing _) _) =>
-  apply bvultWithProof_not_IntroArg : refines.
+(* Bitvector lemmas *)
 
 Lemma bvAdd_Sub_cancel w a b :
       bvAdd w a (bvSub w b a) = b.
@@ -336,6 +142,17 @@ Program Global Instance QuantType_Mbox : QuantType Mbox :=
     quantEnumSurjective := QuantType_Mbox_surjective }.
 
 
+(* QOL: nicer names for mbox arguments *)
+#[local] Hint Extern 901 (IntroArg Any Mbox _) =>
+  let e := fresh "m" in IntroArg_intro e : refines prepostcond.
+#[local] Hint Extern 901 (IntroArg Any Mbox_def _) =>
+  let e := fresh "m" in IntroArg_intro e : refines prepostcond.
+#[local] Hint Extern 901 (IntroArg RetAny Mbox _) =>
+  let e := fresh "r_m" in IntroArg_intro e : refines prepostcond.
+#[local] Hint Extern 901 (IntroArg RetAny Mbox_def _) =>
+  let e := fresh "r_m" in IntroArg_intro e : refines prepostcond.
+
+
 (* Mbox destruction automation *)
 
 Arguments FunsTo_Nil {a}.

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

@@ -5519,8 +5519,8 @@ permIndicesForProvingOffset ps _ _
 permIndicesForProvingOffset ps imprecise_p off =
   let ixs_holdss = flip findMaybeIndices ps $ \p ->
         case llvmPermContainsOffset off p of
-          Just (_, True) -> Just True
-          Just _ | llvmPermContainsArray p && imprecise_p -> Just False
+          Just (_, holds) | holds || imprecise_p -> Just holds
+          -- Just _ | llvmPermContainsArray p && imprecise_p -> Just False
           _ -> Nothing in
   case find (\(_,holds) -> holds) ixs_holdss of
     Just (i,_) -> [i]

heapster-saw/src/Verifier/SAW/Heapster/Lexer.x

@@ -27,6 +27,7 @@ $white+                         ;
 "."                             { token_ TDot           }
 ","                             { token_ TComma         }
 "+"                             { token_ TPlus          }
+"-"                             { token_ TMinus         }
 "*"                             { token_ TStar          }
 "@"                             { token_ TAt            }
 "-o"                            { token_ TLoli          }

heapster-saw/src/Verifier/SAW/Heapster/Parser.y

@@ -37,6 +37,7 @@ import Verifier.SAW.Heapster.UntypedAST
 '.'             { Located $$ TDot                       }
 ','             { Located $$ TComma                     }
 '+'             { Located $$ TPlus                      }
+'-'             { Located $$ TMinus                     }
 '*'             { Located $$ TStar                      }
 '@'             { Located $$ TAt                        }
 '-o'            { Located $$ TLoli                      }
@@ -135,6 +136,7 @@ expr ::                                         { AstExpr }
   | NAT                                         { ExNat (pos $1) (locThing $1) }
   | 'unit'                                      { ExUnit (pos $1) }
   | expr '+' expr                               { ExAdd (pos $2) $1 $3 }
+  | '-' expr                                    { ExNeg (pos $1) $2 }
   | expr '*' expr                               { ExMul (pos $2) $1 $3 }
   | 'struct' '(' list(expr) ')'                 { ExStruct (pos $1) $3 }
   | lifetime 'array' '(' expr ',' expr ',' '<' expr ',' '*' expr ',' expr ')'

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

@@ -2870,14 +2870,20 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
          m
 
   [nuMP| SImpl_LLVMArrayEmpty x mb_ap |] ->
-    do (w_term, _, elem_tp, ap_tp_trans) <- translateLLVMArrayPerm mb_ap
-       let arr_term =
-             applyOpenTermMulti (globalOpenTerm "Prelude.emptyBVVec")
-             [w_term, elem_tp]
-       withPermStackM (:>: translateVar x)
-         (\pctx ->
-           pctx :>:
-           PTrans_Conj [APTrans_LLVMArray $ typeTransF ap_tp_trans [arr_term]])
+    do (w_tm, _, elem_tp, ap_tp_trans) <- translateLLVMArrayPerm mb_ap
+       -- First we build a term of type Vec 0 elem_tp using EmptyVec
+       let vec_tm = applyGlobalOpenTerm "Prelude.EmptyVec" [elem_tp]
+       -- Next, we build a computation that casts it to BVVec w 0x0 elem_tp
+       let w = fromIntegral $ natVal2 mb_ap
+       let bvZero_nat_tm =
+             applyGlobalOpenTerm "Prelude.bvToNat"
+             [w_tm, bvLitOpenTerm (replicate w False)]
+       vec_cast_m <-
+         applyNamedSpecOpM "Prelude.castVecS" [elem_tp, natOpenTerm 0,
+                                               bvZero_nat_tm, vec_tm]
+       bindSpecMTransM vec_cast_m ap_tp_trans "empty_vec" $ \ptrans_arr ->
+         withPermStackM (:>: translateVar x)
+         (\pctx -> pctx :>: PTrans_Conj [APTrans_LLVMArray ptrans_arr])
          m
 
 -- translate1/translateClosed ( zeroOfType <- get the default element )

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

@@ -22,6 +22,7 @@ data Token
   | TSemicolon          -- ^ symbol @;@
   | TComma              -- ^ symbol @,@
   | TPlus               -- ^ symbol @+@
+  | TMinus              -- ^ symbol @-@
   | TStar               -- ^ symbol @*@
   | TAt                 -- ^ symbol @\@@
   | TLoli               -- ^ symbol @-o@
@@ -105,6 +106,7 @@ describeToken t =
     TComma              -> "','"
     TSemicolon          -> "';'"
     TPlus               -> "'+'"
+    TMinus              -> "'-'"
     TStar               -> "'*'"
     TAt                 -> "'@'"
     TLoli               -> "'-o'"