Commit 3d4a9844 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Michael Sammler
Browse files

More support comparing pointers with 0 in the front end + rules for if and assert on pointers.

parent 6db380fd
Pipeline #51699 passed with stage
in 14 minutes and 8 seconds
......@@ -92,3 +92,34 @@ void test_logical(){
if(INT_MAX) { assert(1); } else { assert(0); }
assert(UINT_MAX);
}
[[rc::returns("void")]]
void test_not_ptr(){
int i;
int *pi = &i;
if(!pi){
assert(0);
}
if(pi){
assert(1);
} else {
assert(0);
}
assert(pi);
void *p = NULL;
if(p){
assert(0);
}
if(!p){
assert(1);
} else {
assert(0);
}
assert(!p);
}
......@@ -158,30 +158,43 @@ let rec pp_expr : Coq_ast.expr pp = fun ff e ->
| BinOp(op,ty1,ty2,e1,e2) ->
begin
match (ty1, ty2, op) with
(* Comma operator. *)
| (_ , _ , CommaOp) ->
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
(* Pointer offset operations. *)
| (OpPtr(l), OpInt(_), AddOp ) ->
pp "(%a) at_offset{%a, PtrOp, %a} (%a)" pp_expr e1
(pp_layout false) l pp_op_type ty2 pp_expr e2
| (OpPtr(l), OpInt(_), SubOp ) ->
pp "(%a) at_neg_offset{%a, PtrOp, %a} (%a)" pp_expr e1
(pp_layout false) l pp_op_type ty2 pp_expr e2
(* Pointer difference. *)
| (OpPtr(l1), OpPtr(l2), SubOp) ->
pp "(%a) sub_ptr{%a, PtrOp, PtrOp} (%a)" pp_expr e1
(pp_layout false) l1 pp_expr e2
| (OpPtr(_), OpInt(_), _ ) ->
panic_no_pos "Binop [%a] not supported on pointers."
pp_bin_op op
(* Pointer compared to 0 (Cerberus rejects non-0 integer values). *)
| (OpInt(_) , OpPtr(l) , (EqOp | NeOp)) ->
let e1 = {e1 with elt = UnOp(CastOp(ty2), ty1, e1)} in
pp "(%a) %a{PtrOp, PtrOp, i32} (%a)" pp_expr e1
pp_bin_op op pp_expr e2
| (OpPtr(l) , OpInt(_) , (EqOp | NeOp)) ->
let e2 = {e2 with elt = UnOp(CastOp(ty1), ty2, e2)} in
pp "(%a) %a{PtrOp, PtrOp, i32} (%a)" pp_expr e1
pp_bin_op op pp_expr e2
(* Invalid operations mixing an integer and a pointer. *)
| (OpPtr(_), OpInt(_), _ )
| (OpInt(_), OpPtr(_), _ ) ->
panic_no_pos "Wrong ordering of integer pointer binop [%a]."
pp_bin_op op
| _ when is_bool_result_op op ->
pp "(%a) %a{%a, %a, i32} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
let loc = Location.to_cerb_loc e.loc in
panic loc "Invalid use of binary operation [%a]." pp_bin_op op
(* All other operations are defined. *)
| _ ->
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
if is_bool_result_op op then
pp "(%a) %a{%a, %a, i32} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
else
pp "(%a) %a{%a, %a} (%a)" pp_expr e1 pp_bin_op op
pp_op_type ty1 pp_op_type ty2 pp_expr e2
end
| Deref(atomic,ty,e) ->
if atomic then
......
......@@ -59,3 +59,13 @@ let pp_loc : t pp = fun ff (key, pool) ->
| None -> Format.fprintf ff "unknown"
type 'a located = { elt : 'a ; loc : t }
let to_cerb_loc : t -> Location_ocaml.t = fun (key, pool) ->
match Pool.get pool key with
| None -> Location_ocaml.unknown
| Some(d) ->
let pos_fname = d.loc_file in
let {loc_line1=l1; loc_col1=c1; loc_line2=l2; loc_col2=c2; _} = d in
let p1 = Lexing.{pos_fname; pos_lnum=l1; pos_bol=0; pos_cnum=c1} in
let p2 = Lexing.{pos_fname; pos_lnum=l2; pos_bol=0; pos_cnum=c2} in
Location_ocaml.region (p1, p2) None
......@@ -26,3 +26,5 @@ val pp_data : loc_data pp
val pp_loc : t pp
type 'a located = { elt : 'a ; loc : t }
val to_cerb_loc : t -> Location_ocaml.t
......@@ -388,7 +388,8 @@ Section loc_in_bounds.
rewrite loc_in_bounds_eq.
iIntros "Hb ((?&?&Hctx&?)&?)". iDestruct "Hb" as (id al ????) "Hb".
iDestruct (alloc_range_lookup with "Hctx Hb") as %[al' [?[??]]].
iExists id, al'. iPureIntro. unfold al_end in *. naive_solver lia.
iExists id, al'. iPureIntro. unfold allocation_in_range, al_end in *.
naive_solver lia.
Qed.
Lemma loc_in_bounds_ptr_in_range l n:
......
......@@ -238,6 +238,7 @@ Definition heap_state_loc_in_bounds (l : loc) (n : nat) (st : heap_state) : Prop
alloc_id al,
l.1 = ProvAlloc (Some alloc_id)
st.(hs_allocs) !! alloc_id = Some al
allocation_in_range al
al.(al_start) l.2
l.2 + n al_end al.
......@@ -246,6 +247,10 @@ Definition heap_state_loc_in_bounds (l : loc) (n : nat) (st : heap_state) : Prop
Definition valid_ptr (l : loc) (st : heap_state) : Prop :=
block_alive l st heap_state_loc_in_bounds l 0 st.
Lemma valid_ptr_in_allocation_range l σ:
valid_ptr l σ min_alloc_start l.2 max_alloc_end.
Proof. move => [_][?][?][]?[]?[[]]???. lia. Qed.
Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : Prop :=
alloc, st.(hs_allocs) !! aid = Some alloc a alloc.
......
......@@ -496,6 +496,10 @@ comparing pointers? (see lambda rust) *)
| IfES v it e1 e2 n σ:
val_to_Z v it = Some n
expr_step (IfE (IntOp it) (Val v) e1 e2) σ [] (if bool_decide (n 0) then e1 else e2) σ []
| IfESP v e1 e2 l σ:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then heap_state_loc_in_bounds l 0%nat σ.(st_heap) else True)
expr_step (IfE PtrOp (Val v) e1 e2) σ [] (if bool_decide (l NULL_loc) then e1 else e2) σ []
(* no rule for StuckE *)
.
......@@ -513,6 +517,10 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set →
| IfSS it v s1 s2 rf σ n:
val_to_Z v it = Some n
stmt_step (IfS (IntOp it) (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if bool_decide (n 0) then s1 else s2))) σ []
| IfSSP v s1 s2 rf σ l:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then heap_state_loc_in_bounds l 0%nat σ.(st_heap) else True)
stmt_step (IfS PtrOp (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if bool_decide (l NULL_loc) then s1 else s2))) σ []
| SwitchS rf σ v n m bs s def it :
val_to_Z v it = Some n
( i : nat, m !! n = Some i is_Some (bs !! i))
......
......@@ -441,6 +441,22 @@ Proof.
iModIntro. iMod "HE". by iFrame.
Qed.
Lemma wp_cast_int_null Φ v E it:
val_to_Z v it = Some 0
Φ (val_of_loc NULL_loc) -
WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv) "HΦ".
iApply wp_unop_det_pure; [|done].
move => ??. split.
- inversion 1; simplify_eq => //. case_bool_decide; last done. exfalso.
revert select (valid_ptr _ _) => /valid_ptr_in_allocation_range []/=.
rewrite /min_alloc_start //.
- move => ->. econstructor => //. case_bool_decide; last done. exfalso.
revert select (valid_ptr _ _) => /valid_ptr_in_allocation_range []/=.
rewrite /min_alloc_start //.
Qed.
Lemma wp_copy_alloc_id Φ it a l v1 v2:
val_to_Z v1 it = Some a
val_to_loc v2 = Some l
......@@ -628,6 +644,24 @@ Proof.
iSplit => //. iFrame. by case_bool_decide.
Qed.
Lemma wp_if_ptr Φ v e1 e2 l:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then loc_in_bounds l 0 else True) -
(if bool_decide (l NULL_loc) then WP e1 {{ Φ }} else WP e2 {{ Φ }}) -
WP IfE PtrOp (Val v) e1 e2 {{ Φ }}.
Proof.
iIntros (?) "Hlib HΦ".
iApply wp_lift_expr_step; auto.
iIntros (σ1) "Hσ1". iModIntro. case_bool_decide.
- iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hσ1") as %Hlib.
iSplit. { iPureIntro; repeat eexists _; apply IfESP; rewrite ?bool_decide_true //. }
iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
iSplit => //. iFrame. by case_bool_decide.
- iSplit. { iPureIntro; repeat eexists _; apply IfESP; rewrite ?bool_decide_false //. eauto. }
iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
iSplit => //. iFrame. by case_bool_decide.
Qed.
Lemma wp_skip Φ v E:
Φ v - WP SkipE (Val v) @ E {{ Φ }}.
Proof.
......@@ -955,6 +989,23 @@ Proof.
iFrame "Hσ". case_bool_decide; by iApply "Hs".
Qed.
Lemma wps_if_ptr Q Ψ v s1 s2 l:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then loc_in_bounds l 0 else True) -
(if bool_decide (l NULL_loc) then WPs s1 {{ Q, Ψ }} else WPs s2 {{ Q, Ψ }}) -
WPs (if{PtrOp}: (Val v) then s1 else s2) {{ Q , Ψ }}.
Proof.
iIntros (Hl) "Hlib Hs". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
iApply wp_lift_stmt_step. iIntros (σ1) "Hσ1". case_bool_decide.
- iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hσ1") as %Hlib.
iModIntro. iSplit. { iPureIntro; repeat eexists _; apply IfSSP; rewrite ?bool_decide_true //. }
iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
iFrame "Hσ1". rewrite bool_decide_true; last done. by iApply "Hs".
- iModIntro. iSplit. { iPureIntro; repeat eexists _; apply IfSSP; rewrite ?bool_decide_false //. eauto. }
iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
iFrame "Hσ1". rewrite bool_decide_false; last eauto. by iApply "Hs".
Qed.
Lemma wps_assert Q Ψ it v s n:
val_to_Z v it = Some n n 0
WPs s {{ Q, Ψ }} -
......@@ -964,6 +1015,16 @@ Proof.
iApply wps_if => //. by case_decide.
Qed.
Lemma wps_assert_ptr Q Ψ v s l:
val_to_loc v = Some l l NULL_loc
loc_in_bounds l 0 -
WPs s {{ Q, Ψ }} -
WPs (assert{PtrOp}: Val v; s) {{ Q , Ψ }}.
Proof.
iIntros (Hv Hl) "#Hlib Hs". rewrite /notation.Assert.
iApply wps_if_ptr; rewrite ?bool_decide_true => //.
Qed.
Definition wps_block (P : iProp Σ) (b : label) (Q : gmap label stmt) (Ψ : val iProp Σ) : iProp Σ :=
( (P - WPs Goto b {{ Q, Ψ }})).
......
......@@ -62,7 +62,7 @@ Ltac convert_to_i2p_tac P ::=
| typed_call ?v ?P ?vl ?tys ?T => uconstr:(((_ : TypedCall _ _ _ _) _).(i2p_proof))
| typed_copy_alloc_id ?v1 ?ty1 ?v2 ?ty2 ?ot ?T => uconstr:(((_ : TypedCopyAllocId _ _ _ _ _) _).(i2p_proof))
| typed_place ?P ?l1 ?β1 ?ty1 ?T => uconstr:(((_ : TypedPlace _ _ _ _) _).(i2p_proof))
| typed_if ?ot ?v ?ty ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _).(i2p_proof))
| typed_if ?ot ?v ?P ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _).(i2p_proof))
| typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _).(i2p_proof))
| typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _).(i2p_proof))
| typed_read_end ?a ?E ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _ _) _).(i2p_proof))
......
......@@ -333,8 +333,7 @@ Section programs.
typed_if (IntOp it) v (v ◁ᵥ n @ int it) T1 T2.
Proof.
unfold destruct_hint. iIntros "Hs %Hb" => /=.
iExists it, n. iSplit; first done. iSplit; first done.
by do !case_decide.
iExists n. iSplit; first done. by do !case_decide.
Qed.
Global Instance type_if_int_inst n v it : TypedIf (IntOp it) v (v ◁ᵥ n @ int it)%I :=
λ T1 T2, i2p (type_if_int it n v T1 T2).
......@@ -342,7 +341,7 @@ Section programs.
Lemma type_assert_int it n s Q fn ls R v :
(n 0 typed_stmt s fn ls R Q) -
typed_assert (IntOp it) v (v ◁ᵥ n @ int it) s fn ls R Q.
Proof. iIntros "[% Hs] %Hb". iExists it, _. by iFrame. Qed.
Proof. iIntros "[% Hs] %Hb". iExists _. by iFrame. Qed.
Global Instance type_assert_int_inst it n v : TypedAssert (IntOp it) v (v ◁ᵥ n @ int it)%I :=
λ s fn ls R Q, i2p (type_assert_int _ _ _ _ _ _ _ _).
......@@ -507,7 +506,7 @@ Section programs.
typed_if (IntOp it) v (v ◁ᵥ b @ boolean it) T1 T2.
Proof.
unfold destruct_hint. iIntros "Hs %Hb".
iExists _, _. do 2 iSplit => //. by destruct b.
iExists _. iSplit; first done. by destruct b.
Qed.
Global Instance type_if_bool_inst it b v : TypedIf (IntOp it) v (v ◁ᵥ b @ boolean it)%I :=
λ T1 T2, i2p (type_if_bool it b v T1 T2).
......@@ -516,8 +515,8 @@ Section programs.
(b typed_stmt s fn ls R Q) -
typed_assert (IntOp it) v (v ◁ᵥ b @ boolean it) s fn ls R Q.
Proof.
iIntros "[% Hs] %Hb". iExists it, _. iFrame "Hs".
do 2 (iSplit; first done). by destruct b.
iIntros "[% Hs] %Hb". iExists _. iFrame "Hs".
iSplit; first done. by destruct b.
Qed.
Global Instance type_assert_bool_inst it b v : TypedAssert (IntOp it) v (v ◁ᵥ b @ boolean it)%I :=
λ s fn ls R Q, i2p (type_assert_bool _ _ _ _ _ _ _ _).
......
......@@ -187,6 +187,38 @@ Section own.
TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp PtrOp) PtrOp :=
λ T, i2p (type_cast_ptr_ptr p β ty T).
Lemma type_if_ptr l β ty T1 T2 n `{!LocInBounds ty β n}:
(l ◁ₗ{β} ty - T1) -
typed_if PtrOp l (l ◁ₗ{β} ty) T1 T2.
Proof.
iIntros "HT1 Hl".
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hlib".
iDestruct (loc_in_bounds_has_alloc_id with "Hlib") as %[? H].
iExists l. iSplit; first by rewrite val_to_of_loc.
rewrite bool_decide_true; last by move: l H => [??] /= -> //.
iSplit. { iApply loc_in_bounds_shorten; last done. lia. }
by iApply "HT1".
Qed.
Global Instance type_if_ptr_inst (l : loc) β ty n `{!LocInBounds ty β n}:
TypedIf PtrOp l (l ◁ₗ{β} ty)%I :=
λ T1 T2, i2p (type_if_ptr l β ty T1 T2 n).
Lemma type_assert_ptr l β ty n `{!LocInBounds ty β n} s fn ls R Q:
(l ◁ₗ{β} ty - typed_stmt s fn ls R Q) -
typed_assert PtrOp l (l ◁ₗ{β} ty) s fn ls R Q.
Proof.
iIntros "HT Hl".
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hlib".
iDestruct (loc_in_bounds_has_alloc_id with "Hlib") as %[? H].
iExists l. iSplit; first by rewrite val_to_of_loc.
iSplit. { iPureIntro. move: l H => [??] /= -> //. }
iSplit. { iApply loc_in_bounds_shorten; last done. lia. }
by iApply "HT".
Qed.
Global Instance type_assert_ptr_inst (l : loc) β ty n `{!LocInBounds ty β n}:
TypedAssert PtrOp l (l ◁ₗ{β} ty)%I :=
λ s fn ls R Q, i2p (type_assert_ptr l β ty n s fn ls R Q).
Lemma type_place_cast_ptr_ptr K l ty β T:
typed_place K l β ty T -
typed_place (UnOpPCtx (CastOp PtrOp) :: K) l β ty T.
......@@ -213,7 +245,7 @@ Section own.
iIntros (i') "!>". by iApply ("HΦ" with "[] HT").
Qed.
Global Instance type_cast_int_ptr_inst n v it:
TypedUnOp v (v ◁ᵥ n @ int it)%I (CastOp PtrOp) (IntOp it) :=
TypedUnOp v (v ◁ᵥ n @ int it)%I (CastOp PtrOp) (IntOp it) | 50 :=
λ T, i2p (type_cast_int_ptr n v it T).
Lemma type_copy_aid v a it l β ty T:
......@@ -504,7 +536,19 @@ Section null.
move => Hlib ?. have [??]:= heap_state_loc_in_bounds_has_alloc_id _ _ _ Hlib.
destruct p; simplify_eq/=. destruct b => //; split => Heq; subst.
1, 3: inversion Heq; unfold NULL in *; rewrite ->?val_to_of_loc in *; simplify_eq; done.
all: econstructor; rewrite ?val_to_of_loc /val_of_bool/i2v ?Heq //.
all: eapply RelOpPNull => //; rewrite val_to_of_loc //.
Qed.
Lemma eval_bin_op_null_ptr (b : bool) op h (p : loc) v:
heap_state_loc_in_bounds p 0 h.(st_heap)
(if b then op = NeOp i32 else op = EqOp i32)
eval_bin_op op PtrOp PtrOp h NULL p v
val_of_Z (Z_of_bool b) i32 None = Some v.
Proof.
move => Hlib ?. have [??]:= heap_state_loc_in_bounds_has_alloc_id _ _ _ Hlib.
destruct p; simplify_eq/=. destruct b => //; split => Heq; subst.
1, 3: inversion Heq; unfold NULL in *; rewrite ->?val_to_of_loc in *; simplify_eq; done.
all: eapply RelOpNullP => //; rewrite val_to_of_loc //.
Qed.
Lemma eval_bin_op_null_null (b : bool) op h v:
......@@ -535,10 +579,10 @@ Section null.
TypedBinOp v1 (v1 ◁ᵥ null) v2 (v2 ◁ᵥ null) op PtrOp PtrOp :=
λ T, i2p (type_binop_null_null v1 v2 op T).
Lemma type_binop_ptr_null v2 op T (l : loc) ty β n `{!LocInBounds ty β n}:
(match op with | EqOp rit | NeOp rit => rit = i32 | _ => False end v, l ◁ₗ{β} ty -
T v (t2mt ((if op is EqOp i32 then false else true) @ boolean i32))) -
typed_bin_op l (l ◁ₗ{β} ty) v2 (v2 ◁ᵥ null) op PtrOp PtrOp T.
Lemma type_binop_ptr_null v op (l : loc) ty β n `{!LocInBounds ty β n} T:
(match op with EqOp rit | NeOp rit => rit = i32 | _ => False end v, l ◁ₗ{β} ty -
T v (t2mt ((if op is EqOp _ then false else true) @ boolean i32))) -
typed_bin_op l (l ◁ₗ{β} ty) v (v ◁ᵥ null) op PtrOp PtrOp T.
Proof.
iIntros "[% HT] Hl" (-> Φ) "HΦ".
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hb".
......@@ -554,9 +598,32 @@ Section null.
iModIntro. iMod "HE". iModIntro. iFrame.
iApply "HΦ". 2: by iApply "HT". by destruct op.
Qed.
Global Instance type_binop_ptr_null_inst v2 op (l : loc) ty β n `{!LocInBounds ty β n}:
TypedBinOp l (l ◁ₗ{β} ty) v2 (v2 ◁ᵥ null) op PtrOp PtrOp :=
λ T, i2p (type_binop_ptr_null v2 op T l ty β n).
Global Instance type_binop_ptr_null_inst v op (l : loc) ty β n `{!LocInBounds ty β n}:
TypedBinOp l (l ◁ₗ{β} ty) v (v ◁ᵥ null) op PtrOp PtrOp :=
λ T, i2p (type_binop_ptr_null v op l ty β n T).
Lemma type_binop_null_ptr v op (l : loc) ty β n `{!LocInBounds ty β n} T:
(match op with EqOp rit | NeOp rit => rit = i32 | _ => False end v, l ◁ₗ{β} ty -
T v (t2mt ((if op is EqOp _ then false else true) @ boolean i32))) -
typed_bin_op v (v ◁ᵥ null) l (l ◁ₗ{β} ty) op PtrOp PtrOp T.
Proof.
iIntros "[% HT] -> Hl %Φ HΦ".
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hb".
iDestruct (loc_in_bounds_shorten _ _ 0 with "Hb") as "#Hb0"; first by lia.
have ?:= val_of_Z_bool (if op is EqOp _ then false else true) i32.
iApply (wp_binop_det (i2v (Z_of_bool (if op is EqOp _ then false else true)) i32)).
iIntros (σ) "Hctx". iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
iSplit. {
iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hb0 Hctx") as %?.
iPureIntro => ?.
rewrite (eval_bin_op_null_ptr (if op is EqOp _ then false else true)); destruct op => //; naive_solver.
}
iModIntro. iMod "HE". iModIntro. iFrame.
iApply "HΦ". 2: by iApply "HT". by destruct op.
Qed.
Global Instance type_binop_null_ptr_inst v op (l : loc) ty β n `{!LocInBounds ty β n}:
TypedBinOp v (v ◁ᵥ null) l (l ◁ₗ{β} ty) op PtrOp PtrOp :=
λ T, i2p (type_binop_null_ptr v op l ty β n T).
Lemma type_cast_null_int it v T:
(T (i2v 0 it) (t2mt (0 @ int it))) -
......@@ -571,6 +638,30 @@ Section null.
Global Instance type_cast_null_int_inst v it:
TypedUnOpVal v null (CastOp (IntOp it)) PtrOp :=
λ T, i2p (type_cast_null_int it v T).
Lemma type_cast_zero_ptr v it T:
(T (val_of_loc NULL_loc) (t2mt null)) -
typed_un_op v (v ◁ᵥ 0 @ int it) (CastOp PtrOp) (IntOp it) T.
Proof.
iIntros "HT" (Hv Φ) "HΦ".
iApply wp_cast_int_null; first done.
iModIntro. by iApply ("HΦ" with "[] HT").
Qed.
Global Instance type_cast_zero_ptr_inst v it:
TypedUnOpVal v (0 @ int it) (CastOp PtrOp) (IntOp it) | 10 :=
λ T, i2p (type_cast_zero_ptr v it T).
Lemma type_if_null v T1 T2:
T2 -
typed_if PtrOp v (v ◁ᵥ null) T1 T2.
Proof.
iIntros "HT2 ->". iExists NULL_loc.
rewrite val_to_of_loc bool_decide_false; last eauto.
by iFrame.
Qed.
Global Instance type_if_null_inst v:
TypedIf PtrOp v (v ◁ᵥ null)%I :=
λ T1 T2, i2p (type_if_null v T1 T2).
End null.
Section optionable.
......
......@@ -65,7 +65,14 @@ Section judgements.
Definition typed_if (ot : op_type) (v : val) (P : iProp Σ) (T1 T2 : iProp Σ) : iProp Σ :=
(* TODO: generalize this to PtrOp *)
(P - it z, ot = IntOp it val_to_Z v it = Some z (if bool_decide (z 0) then T1 else T2)).
(P -
match ot with
| IntOp it => z, val_to_Z v it = Some z (if bool_decide (z 0) then T1 else T2)
| PtrOp => l, val_to_loc v = Some l
(if bool_decide (l NULL_loc) then loc_in_bounds l 0 else True)
(if bool_decide (l NULL_loc) then T1 else T2)
| _ => False
end).
Class TypedIf (ot : op_type) (v : val) (P : iProp Σ) : Type :=
typed_if_proof T1 T2 : iProp_to_Prop (typed_if ot v P T1 T2).
......@@ -89,9 +96,15 @@ Section judgements.
typed_switch_proof m ss def fn ls R Q : iProp_to_Prop (typed_switch v ty it m ss def fn ls R Q).
Definition typed_assert (ot : op_type) (v : val) (P : iProp Σ) (s : stmt) (fn : function) (ls : list loc) (R : val mtype iProp Σ) (Q : gmap label stmt) : iProp Σ :=
(P - it z, ot = IntOp it val_to_Z v it = Some z z 0 typed_stmt s fn ls R Q)%I.
(P -
match ot with
| IntOp it => z, val_to_Z v it = Some z z 0 typed_stmt s fn ls R Q
| PtrOp => l, val_to_loc v = Some l l NULL_loc loc_in_bounds l 0 typed_stmt s fn ls R Q
| _ => False
end)%I.
Class TypedAssert (ot : op_type) (v : val) (P : iProp Σ) : Type :=
typed_assert_proof s fn ls R Q : iProp_to_Prop (typed_assert ot v P s fn ls R Q).
(*** expressions *)
Definition typed_val_expr (e : expr) (T : val mtype iProp Σ) : iProp Σ :=
( Φ, ( v (ty : mtype), v ◁ᵥ ty - T v ty - Φ v) - WP e {{ Φ }}).
......@@ -332,7 +345,7 @@ Global Hint Mode SubsumeVal + + + + ! + ! : typeclass_instances.
Global Hint Mode SimpleSubsumePlace + + + ! - : typeclass_instances.
Global Hint Mode SimpleSubsumePlaceR + + + ! + ! - : typeclass_instances.
Global Hint Mode SimpleSubsumeVal + + + ! + ! - : typeclass_instances.
Global Hint Mode TypedIf + + + + : typeclass_instances.
Global Hint Mode TypedIf + + + + + : typeclass_instances.
Global Hint Mode TypedAssert + + + + + : typeclass_instances.
Global Hint Mode TypedValue + + + : typeclass_instances.
Global Hint Mode TypedBinOp + + + + + + + + + : typeclass_instances.
......@@ -407,10 +420,12 @@ Section proper.
((T1 - T1') (T2 - T2')) -
typed_if ot v P T1' T2'.
Proof.
iIntros "Hif HT Hv". iDestruct ("Hif" with "Hv") as (it z ? ?) "HC".
iExists _, _. iSplit; [done|]. iSplit; [done|]. case_decide.
- iDestruct "HT" as "[_ HT]". by iApply "HT".
- iDestruct "HT" as "[HT _]". by iApply "HT".
iIntros "Hif HT Hv". iDestruct ("Hif" with "Hv") as "Hif".
destruct ot => //; iDestruct "Hif" as (zorl ?) "HC"; iExists zorl.
all: try iDestruct "HC" as "[$ HC]".
all: iSplit; first done.
all: case_decide; [iDestruct "HT" as "[_ HT]" | iDestruct "HT" as "[HT _]"].
all: by iApply "HT".
Qed.
Lemma typed_bin_op_wand v1 P1 Q1 v2 P2 Q2 op ot1 ot2 T:
......@@ -1013,7 +1028,7 @@ Section typing.
iIntros "Hs Hv". iDestruct (i2p_proof with "Hs Hv") as (Q) "[HQ HT]" => /=. simpl in *.
iApply ("HT" with "HQ").
Qed.
Global Instance typed_if_simplify_inst ot v (P : iProp Σ) n {SH : SimplifyHyp P (Some n)}:
Global Instance typed_if_simplify_inst ot v P n {SH : SimplifyHyp P (Some n)}:
TypedIf ot v P | 1000 :=
λ T1 T2, i2p (typed_if_simplify ot v P T1 T2 n).
......@@ -1074,15 +1089,19 @@ Section typing.
all: by iApply ("HT" with "Hl").
Qed.
Lemma type_if Q it e s1 s2 fn ls R:
typed_val_expr e (λ v ty, typed_if (IntOp it) v (v ◁ᵥ ty)
Lemma type_if Q ot e s1 s2 fn ls R:
typed_val_expr e (λ v ty, typed_if ot v (v ◁ᵥ ty)