Skip to content

Commit

Permalink
Heapster: improved bitvector and automation support (#1792)
Browse files Browse the repository at this point in the history 
* Heapster: Support negating bitvector permission expressions

This adds the necessary tweaks to `heapster-saw` to support parsing and
typechecking permission expressions of the form `-b`, which represents the
2's complement negation of the bitvector `b`.

Fixes #1780.

* added castVecS

* fixed the translation of the SImpl_LLVMArrayEmpty rule to produce a well-typed term

* changed implication prover for field permissions so that a field can be proved by a block that could contain its offset, rather that requiring it to definitely contain its offset

* add maybe automation to SpecMExtra

Co-authored-by: Eddy Westbrook <[email protected]>
Co-authored-by: Matthew Yacavone <[email protected]>
  • Loading branch information
@RyanGlScott @m-yac
3 people authored Jan 3, 2023
1 parent b4ecd82 commit 7a6c8e1
Show file tree
Hide file tree
Showing 12 changed files with 271 additions and 233 deletions.
1 change: 1 addition & 0 deletions heapster-saw/doc/Permissions.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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` |
Expand Down
22 changes: 1 addition & 21 deletions heapster-saw/examples/linked_list_proofs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}.
Expand Down
207 changes: 12 additions & 195 deletions heapster-saw/examples/mbox_proofs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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}.
Expand Down
4 changes: 2 additions & 2 deletions heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
1 change: 1 addition & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Lexer.x
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ $white+ ;
"." { token_ TDot }
"," { token_ TComma }
"+" { token_ TPlus }
"-" { token_ TMinus }
"*" { token_ TStar }
"@" { token_ TAt }
"-o" { token_ TLoli }
Expand Down
2 changes: 2 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Parser.y
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ import Verifier.SAW.Heapster.UntypedAST
'.' { Located $$ TDot }
',' { Located $$ TComma }
'+' { Located $$ TPlus }
'-' { Located $$ TMinus }
'*' { Located $$ TStar }
'@' { Located $$ TAt }
'-o' { Located $$ TLoli }
Expand Down Expand Up @@ -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 ')'
Expand Down
22 changes: 14 additions & 8 deletions heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
Expand Down
2 changes: 2 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Token.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ data Token
| TSemicolon -- ^ symbol @;@
| TComma -- ^ symbol @,@
| TPlus -- ^ symbol @+@
| TMinus -- ^ symbol @-@
| TStar -- ^ symbol @*@
| TAt -- ^ symbol @\@@
| TLoli -- ^ symbol @-o@
Expand Down Expand Up @@ -105,6 +106,7 @@ describeToken t =
TComma -> "','"
TSemicolon -> "';'"
TPlus -> "'+'"
TMinus -> "'-'"
TStar -> "'*'"
TAt -> "'@'"
TLoli -> "'-o'"
Expand Down
Loading

0 comments on commit 7a6c8e1

Please sign in to comment.