Commit 4865b710 authored by Hai Dang's avatar Hai Dang

Fix retag semantics:

- single retag on references
- retagging with Sum (enum) does not look at the memory in the case with UnsafeCell
- cleanups
parent e5bcee56
......@@ -182,82 +182,59 @@ Definition unsafe_action
Section blah.
Context {A: Type}.
Equations visit_freeze_sensitive'
(h: mem) (l: loc) (f: A loc nat bool option A)
(l: loc) (f: A loc nat bool option A)
(a: A) (last cur_dist: nat) (T: type) : option (A * (nat * nat)) :=
visit_freeze_sensitive' h l f a last cur_dist (FixedSize n) :=
visit_freeze_sensitive' l f a last cur_dist (FixedSize n) :=
(* consider frozen, simply extend the distant by n *)
Some (a, (last, cur_dist + n)%nat) ;
visit_freeze_sensitive' h l f a last cur_dist (Reference _ _) :=
visit_freeze_sensitive' l f a last cur_dist (Reference _ _) :=
(* consider frozen, extend the distant by 1 *)
Some (a, (last, S cur_dist)) ;
visit_freeze_sensitive' h l f a last cur_dist (Unsafe T) :=
visit_freeze_sensitive' l f a last cur_dist (Unsafe T) :=
(* reach an UnsafeCell, apply the action `f` and return new `last` and
`cur_dist` *)
unsafe_action f a l last cur_dist (tsize T) ;
visit_freeze_sensitive' h l f a last cur_dist (Union Ts) :=
visit_freeze_sensitive' l f a last cur_dist (Union Ts) :=
(* If it's a union, look at the type to see if there is UnsafeCell *)
if is_freeze (Union Ts)
(* No UnsafeCell, consider the whole block frozen and simply extend the
distant. *)
then Some (a, (last, cur_dist + (tsize (Union Ts)))%nat)
(* There can be UnsafeCell, consider the whole block unfrozen and perform
`f a _ _ false` on the whole block. `unsafe_action` will return the
offsets for the following visit. *)
(* There can be UnsafeCell, consider the whole block of [Union Ts]
unfrozen and perform `f a _ _ false` on the whole block.
`unsafe_action` will return the offsets for the following visit. *)
else unsafe_action f a l last cur_dist (tsize (Union Ts)) ;
visit_freeze_sensitive' h l f a last cur_dist (Product Ts) :=
visit_freeze_sensitive' l f a last cur_dist (Product Ts) :=
(* Try a shortcut *)
if is_freeze (Product Ts)
(* No UnsafeCell, consider the whole block frozen and simply extend the
distant. *)
then Some (a, (last, cur_dist + (tsize (Product Ts)))%nat)
(* This implements left-to-right search on the type, which guarantees
(* Perform a left-to-right search on [Product Ts], which guarantees
that the offsets are increasing. *)
else visit_LR a last cur_dist Ts
where visit_LR (a: A) (last cur_dist: nat) (Ts: list type)
: option (A * (nat * nat)) :=
{ visit_LR a last cur_dist [] := Some (a, (last, cur_dist)) ;
visit_LR a last cur_dist (T' :: Ts') :=
alc visit_freeze_sensitive' h l f a last cur_dist T' ;
alc visit_freeze_sensitive' l f a last cur_dist T' ;
visit_LR alc.1 alc.2.1 alc.2.2 Ts' } ;
visit_freeze_sensitive' h l f a last cur_dist (Sum Ts) :=
visit_freeze_sensitive' l f a last cur_dist (Sum Ts) :=
(* Try a shortcut *)
if is_freeze (Sum Ts)
(* No UnsafeCell, consider the whole block frozen and simply extend the
distant. *)
then Some (a, (last, cur_dist + (tsize (Sum Ts)))%nat)
else
match h !! (l + (last + cur_dist)) with
(* This looks up the current state to see which discriminant currently
is active (which is an integer) and redirect the visit for the type
of that discriminant. Note that this consitutes a read-access, and
should adhere to the access checks. But we are skipping them here.
FIXME *)
| Some (ScInt i) =>
if decide (O i)
then (* the discriminant is well-defined, visit with the
corresponding type *)
alc visit_lookup Ts (Z.to_nat i) ;
(* Anything in the padding is considered frozen and will be
applied with the action by the following visit.
`should_offset` presents the offset that the visit SHOULD
arrive at after the visit. If there are padding bytes left,
they will be added to the cur_dist. *)
let should_offset := (last + cur_dist + tsize (Sum Ts))%nat in
Some (alc.1, (alc.2.1, (should_offset - alc.2.1)%nat))
else None
| _ => None
end
where visit_lookup (Ts: list type) (i: nat) : option (A * (nat * nat)) :=
{ visit_lookup [] _ := None ;
visit_lookup (T :: _) O :=
visit_freeze_sensitive' h l f a last (S cur_dist) T ;
visit_lookup (T :: Ts) (S i) := visit_lookup Ts i }
(* There can be UnsafeCell, consider the whole block of [Sum Ts] unfrozen
and perform `f a _ _ false` on the whole block. `unsafe_action` will
return the offsets for the following visit. *)
else unsafe_action f a l last cur_dist (tsize (Sum Ts))
.
End blah.
Definition visit_freeze_sensitive {A: Type}
h (l: loc) (T: type) (f: A loc nat bool option A) (a: A) : option A :=
match visit_freeze_sensitive' h l f a O O T with
(l: loc) (T: type) (f: A loc nat bool option A) (a: A) : option A :=
match visit_freeze_sensitive' l f a O O T with
| Some (a', (last', cur_dist')) =>
(* the last block is frozen *)
f a' (l + last') cur_dist' true
......@@ -310,13 +287,13 @@ Definition reborrowN α cids l n old_tag new_tag pm prot :=
(* This implements EvalContextPrivExt::reborrow *)
(* TODO?: alloc.check_bounds(this, ptr, size)?; *)
Definition reborrow h α cids l (old_tag: tag) T (kind: ref_kind)
Definition reborrow α cids l (old_tag: tag) T (kind: ref_kind)
(new_tag: tag) (protector: option call_id) :=
match kind with
| SharedRef | RawRef false =>
(* for shared refs and const raw pointer, treat Unsafe as SharedReadWrite
and Freeze as SharedReadOnly *)
visit_freeze_sensitive h l T
visit_freeze_sensitive l T
(λ α' l' sz frozen,
(* If is in Unsafe, use SharedReadWrite, otherwise SharedReadOnly *)
let perm := if frozen then SharedReadOnly else SharedReadWrite in
......@@ -331,11 +308,12 @@ Definition reborrow h α cids l (old_tag: tag) T (kind: ref_kind)
(* Retag one pointer *)
(* This implements EvalContextPrivExt::retag_reference *)
Definition retag_ref h α cids (nxtp: ptr_id) l (old_tag: tag) T
Definition retag_ref α cids (nxtp: ptr_id) l (old_tag: tag) T
(kind: ref_kind) (protector: option call_id)
: option (tag * stacks * ptr_id) :=
match tsize T with
| O => (* Nothing to do for zero-sized types *)
(* TODO: this can be handled by reborrow *)
Some (old_tag, α, nxtp)
| _ =>
let new_tag := match kind with
......@@ -343,7 +321,7 @@ Definition retag_ref h α cids (nxtp: ptr_id) l (old_tag: tag) T
| _ => Tagged nxtp
end in
(* reborrow old_tag with new_tag *)
α' reborrow h α cids l old_tag T kind new_tag protector;
α' reborrow α cids l old_tag T kind new_tag protector;
Some (new_tag, α', S nxtp)
end.
......@@ -352,8 +330,7 @@ Definition adding_protector (kind: retag_kind) (c: call_id) : option call_id :=
(* This *partly* implements EvalContextExt::retag *)
(* Assumption: ct cids *)
Definition retag1
h α (nxtp: ptr_id) (cids: call_id_stack) (ct: call_id)
Definition retag α (nxtp: ptr_id) (cids: call_id_stack) (ct: call_id)
(l: loc) (otag: tag) (kind: retag_kind) pk Tr :
option (tag * stacks * ptr_id) :=
let qualify : option (ref_kind * option call_id) :=
......@@ -371,62 +348,11 @@ Definition retag1
| RawPtr _, _ => None
end in
match qualify with
| Some (rkind, protector) => retag_ref h α cids nxtp l otag Tr rkind protector
| Some (rkind, protector) => retag_ref α cids nxtp l otag Tr rkind protector
| None => Some (otag, α, nxtp)
end
.
Equations retag
(h: mem) α (nxtp: ptr_id) (cids: call_id_stack) (ct: call_id) (x: loc) (kind: retag_kind) T :
option (mem * stacks * ptr_id) :=
retag h α nxtp cids ct x kind (FixedSize _) := Some (h, α, nxtp) ;
retag h α nxtp cids ct x kind (Union _) := Some (h, α, nxtp) ;
retag h α nxtp cids ct x kind (Unsafe T) := retag h α nxtp cids ct x kind T ;
retag h α nxtp cids ct x kind (Reference pk Tr) with h !! x :=
{ | Some (ScPtr l otag) :=
let qualify : option (ref_kind * option call_id) :=
match pk, kind with
(* Mutable reference *)
| RefPtr Mutable, _ =>
Some (UniqueRef (is_two_phase kind), adding_protector kind ct)
(* Immutable reference *)
| RefPtr Immutable, _ => Some (SharedRef, adding_protector kind ct)
(* If is both raw ptr and Raw retagging, no protector *)
| RawPtr mut, RawRt => Some (RawRef (bool_decide (mut = Mutable)), None)
(* Box pointer, no protector *)
| BoxPtr, _ => Some (UniqueRef false, None)
(* Ignore Raw pointer otherwise *)
| RawPtr _, _ => None
end in
match qualify with
| Some (rkind, protector) =>
bac retag_ref h α cids nxtp l otag Tr rkind protector ;
Some (<[x := ScPtr l bac.1.1]>h, bac.1.2, bac.2)
| None => Some (h, α, nxtp)
end ;
| _ := None } ;
retag h α nxtp cids ct x kind (Product Ts) := visit_LR h α nxtp x Ts
(* left-to-right visit to retag *)
where visit_LR h α (nxtp: ptr_id) (x: loc) (Ts: list type)
: option (mem * stacks * ptr_id) :=
{ visit_LR h α nxtp x [] := Some (h, α, nxtp) ;
visit_LR h α nxtp x (T :: Ts) :=
hac retag h α nxtp cids ct x kind T ;
visit_LR hac.1.1 hac.1.2 hac.2 (x + (tsize T)) Ts } ;
retag h α nxtp cids ct x kind (Sum Ts) with h !! x :=
{ | Some (ScInt i) :=
if decide (O i < length Ts)
then (* the discriminant is well-defined, visit with the
corresponding type *)
visit_lookup Ts (Z.to_nat i)
else None
where visit_lookup (Ts: list type) (i: nat) : option (mem * stacks * ptr_id) :=
{ visit_lookup [] i := None ;
visit_lookup (T :: Ts) O := retag h α nxtp cids ct (x + 1) kind T ;
visit_lookup (T :: Ts) (S i) := visit_lookup Ts i } ;
| _ := None }
.
Definition tag_included (tg: tag) (nxtp: ptr_id) : Prop :=
match tg with
| Tagged t => (t < nxtp)%nat
......@@ -439,7 +365,7 @@ Infix "<<t" := tag_values_included (at level 60, no associativity).
(** Instrumented step for the stacked borrows *)
(* This ignores CAS for now. *)
Inductive bor_step h α (cids: call_id_stack) (nxtp: ptr_id) (nxtc: call_id):
Inductive bor_step α (cids: call_id_stack) (nxtp: ptr_id) (nxtc: call_id):
event stacks call_id_stack ptr_id call_id Prop :=
(* | SysCallIS id :
bor_step h α β nxtp (SysCallEvt id) h α β nxtp *)
......@@ -447,7 +373,7 @@ Inductive bor_step h α (cids: call_id_stack) (nxtp: ptr_id) (nxtc: call_id):
| AllocIS x T :
(* Tagged nxtp is the first borrow of the variable x,
used when accessing x directly (not through another pointer) *)
bor_step h α cids nxtp nxtc
bor_step α cids nxtp nxtc
(AllocEvt x (Tagged nxtp) T)
(init_stacks α x (tsize T) (Tagged nxtp)) cids (S nxtp) nxtc
(* This implements AllocationExtra::memory_read. *)
......@@ -455,23 +381,23 @@ Inductive bor_step h α (cids: call_id_stack) (nxtp: ptr_id) (nxtc: call_id):
(ACC: memory_read α cids l lbor (tsize T) = Some α')
(* This comes from wellformedness, but for convenience we require it here *)
(BOR: vl <<t nxtp):
bor_step h α cids nxtp nxtc (CopyEvt l lbor T vl) α' cids nxtp nxtc
bor_step α cids nxtp nxtc (CopyEvt l lbor T vl) α' cids nxtp nxtc
(* This implements AllocationExtra::memory_written. *)
| WriteIS α' l lbor T vl
(ACC: memory_written α cids l lbor (tsize T) = Some α')
(* This comes from wellformedness, but for convenience we require it here *)
(BOR: vl <<t nxtp) :
bor_step h α cids nxtp nxtc (WriteEvt l lbor T vl) α' cids nxtp nxtc
bor_step α cids nxtp nxtc (WriteEvt l lbor T vl) α' cids nxtp nxtc
(* This implements AllocationExtra::memory_deallocated. *)
| DeallocIS α' l lbor T
(ACC: memory_deallocated α cids l lbor (tsize T) = Some α') :
bor_step h α cids nxtp nxtc (DeallocEvt l lbor T) α' cids nxtp nxtc
bor_step α cids nxtp nxtc (DeallocEvt l lbor T) α' cids nxtp nxtc
| InitCallIS :
bor_step h α cids nxtp nxtc (InitCallEvt nxtc) α (nxtc :: cids) nxtp (S nxtc)
bor_step α cids nxtp nxtc (InitCallEvt nxtc) α (nxtc :: cids) nxtp (S nxtc)
| EndCallIS c cids' v
(TOP: cids = c :: cids') :
bor_step h α cids nxtp nxtc (EndCallEvt c v) α cids' nxtp nxtc
bor_step α cids nxtp nxtc (EndCallEvt c v) α cids' nxtp nxtc
| RetagIS α' nxtp' l otag ntag T kind pkind c cids'
(TOP: cids = c :: cids')
(RETAG: retag1 h α nxtp cids c l otag kind pkind T = Some (ntag, α', nxtp')) :
bor_step h α cids nxtp nxtc (RetagEvt l otag ntag pkind T kind) α' cids nxtp' nxtc.
(RETAG: retag α nxtp cids c l otag kind pkind T = Some (ntag, α', nxtp')) :
bor_step α cids nxtp nxtc (RetagEvt l otag ntag pkind T kind) α' cids nxtp' nxtc.
......@@ -70,25 +70,6 @@ Lemma of_result_list_expr (vl: list value) :
(of_result <$> (ValR <$> vl)) = Val <$> vl.
Proof. induction vl as [|v vl IH]; [done|]. by rewrite 3!fmap_cons IH. Qed.
(* Lemma subst_is_closed X x es e :
is_closed X es is_closed (x::X) e is_closed X (subst x es e).
Proof.
revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
try naive_solver; rewrite ?andb_True; intros.
- set_solver.
- split; first naive_solver. induction el; naive_solver.
- (* eauto using is_closed_weaken with set_solver. *)
- eapply is_closed_weaken; first done.
destruct (decide (BNamed x = f)), (decide (BNamed x xl)); set_solver.
- induction el; naive_solver.
- split; first naive_solver. induction el; naive_solver.
Qed.
Lemma subst'_is_closed X b es e :
is_closed X es is_closed (b:b:X) e is_closed X (subst' b es e).
Proof. destruct b; first done. apply subst_is_closed. Qed.
*)
(** Equality and other typeclass stuff *)
Instance bin_op_eq_dec : EqDecision bin_op.
......@@ -354,7 +335,7 @@ Inductive head_step :
: head_step e σ [ev] e' σ []
| HeadImpureS σ e e' ev h' α' cids' nxtp' nxtc'
(ExprStep : mem_expr_step σ.(shp) e ev h' e')
(InstrStep: bor_step h' σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(InstrStep: bor_step σ.(sst) σ.(scs) σ.(snp) σ.(snc)
ev α' cids' nxtp' nxtc')
: head_step e σ [ev] e' (mkState h' α' cids' nxtp' nxtc') [].
......@@ -413,7 +394,6 @@ Definition new_place T (v: expr) : expr :=
Definition retag_place
(p: expr) (pk: pointer_kind) (T: type) (kind: retag_kind) : expr :=
let: "p" := p in
(* read the current tag of the place [p] *)
let: "o" := & "p" in
(* retag and update with new tag *)
"p" <- Retag "o" pk T kind.
(* read the current pointer stored in the place [p] *)
(* retag and update [p] with the pointer with new tag *)
"p" <- Retag (Copy "p") pk T kind.
......@@ -21,7 +21,7 @@ Ltac inv_head_step :=
inversion H ; subst; clear H
| H : pure_expr_step _ _ _ _ _ |- _ =>
inversion H ; subst; clear H
| H : bor_step _ _ _ _ _ _ _ _ _ _ |- _ =>
| H : bor_step _ _ _ _ _ _ _ _ _ |- _ =>
inversion H ; subst; clear H
end.
......@@ -867,20 +867,22 @@ Proof.
- subst K. by exists (Ki :: K0).
Qed.
Lemma tstep_retag_inv l otg T pk rk e' σ σ'
(STEP: (Retag #[ScPtr l otg] pk T rk, σ) ~{fns}~> (e', σ')) :
c cids ntg α' nxtp',
Lemma tstep_retag_inv (ptr: result) T pk rk e' σ σ'
(STEP: (Retag ptr pk T rk, σ) ~{fns}~> (e', σ')) :
l otg c cids ntg α' nxtp',
ptr = ValR [ScPtr l otg]
σ.(scs) = c :: cids
retag1 σ.(shp) σ.(sst) σ.(snp) σ.(scs) c l otg rk pk T
= Some (ntg, α', nxtp')
retag σ.(sst) σ.(snp) σ.(scs) c l otg rk pk T = Some (ntg, α', nxtp')
e' = #[ScPtr l ntg]%V
σ' = mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc).
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_retag_decompose _ _ _ _ _ _ Eq) as [[]|[K' [? Eq']]]; subst.
- clear Eq. simpl in HS. inv_head_step. naive_solver.
- clear Eq. simpl in HS. inv_head_step.
have Eq1 := to_of_result ptr. rewrite -H0 /to_result in Eq1. simplify_eq.
naive_solver.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq'. by eexists.
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
Qed.
......
This diff is collapsed.
This diff is collapsed.
......@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
Definition ex1_unopt : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in (* put argument into place *)
Retag "x" Default ;;
retag_place "x" (RefPtr Mutable) int Default ;;
Call #[ScFnPtr "f"] [] ;;
*{int} "x" <- #[42] ;;
Call #[ScFnPtr "g"] [] ;;
......@@ -20,7 +20,7 @@ Definition ex1_unopt : function :=
Definition ex1_opt : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" Default ;;
retag_place "x" (RefPtr Mutable) int Default ;;
Call #[ScFnPtr "f"] [] ;;
*{int} "x" <- #[42] ;;
let: "v" := Copy *{int} "x" in
......@@ -43,13 +43,24 @@ Proof.
intros sarg ->.
sim_apply sim_simple_let=>/=.
apply: sim_simple_result.
(* Retag local *)
(* Retag a local place *)
sim_apply sim_simple_let=>/=.
destruct args as [|args args']; first by inversion AREL.
apply Forall2_cons_inv in AREL as [AREL ATAIL].
destruct args' as [|]; last by inversion ATAIL. clear ATAIL.
sim_apply sim_simple_retag_local; [simpl; lia|solve_sim..|].
move=>l_i tg_i hplt /= Hl_i.
sim_apply sim_simple_let=>/=.
(* Copy local place *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply: sim_simple_result. simpl.
(* Retag *)
destruct args as [|args args']; first by inversion AREL.
apply Forall2_cons_inv in AREL as [AREL ATAIL].
destruct args' as [|]; last by inversion ATAIL. clear ATAIL.
have AREL': arel rarg sarg sarg.
{ have AREL':=(arel_eq _ _ _ AREL). by subst args. }
sim_apply sim_simple_retag_mut_ref; [simpl; lia| |eauto|..]; [solve_sim|].
move=>l_i tg_i tg_n hplt /= ? IS_i. subst sarg.
specialize (IS_i O ltac:(lia)). rewrite shift_loc_0_nat in IS_i.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros s ?. simplify_eq.
(* Call *)
sim_apply sim_simple_let=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
......@@ -98,7 +109,7 @@ Proof.
sim_apply sim_simple_let=>/=.
sim_apply sim_simple_free_public.
{ simpl. constructor; [|by constructor].
assert (args = sarg). { by revert AREL; apply arel_eq. } subst args.
assert (args = ScPtr l' tg_i). { by revert AREL; apply arel_eq. } subst args.
revert AREL. apply arel_mono; [|solve_res].
apply (cmra_valid_included _ _ Hval).
do 3 apply cmra_mono_r. apply cmra_included_l. } simpl.
......
......@@ -8,17 +8,19 @@ Set Default Proof Using "Type".
Definition ex1_down : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in (* put argument into place *)
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex1_down_opt : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i" ;;
Copy *{int} "x"
.
......
......@@ -8,19 +8,22 @@ Set Default Proof Using "Type".
Definition ex2 : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" Default ;;
retag_place "x" (RefPtr Immutable) int Default ;;
Copy *{int} "x" ;;
Call #[ScFnPtr "f"] ["x"] ;;
Copy *{int} "x"
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
"v"
.
Definition ex2_opt : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" Default ;;
retag_place "x" (RefPtr Immutable) int Default ;;
Copy *{int} "x" ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] ["x"] ;;
Free "x" ;; Free "i" ;;
"v"
.
......
......@@ -8,18 +8,21 @@ Set Default Proof Using "Type".
Definition ex2_down : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Immutable) int FnEntry ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] ["x"] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex2_down_opt : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Immutable) int FnEntry ;;
Call #[ScFnPtr "f"] ["x"] ;;
Copy *{int} "x"
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
"v"
.
......
......@@ -4,32 +4,36 @@ Set Default Proof Using "Type".
(** Moving a write to a mutable reference up across unknown code. *)
(* TODO: check if Free is in the right place *)
(* Assuming x : &mut i32 *)
Definition ex3 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[42] ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex3_opt_1 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[42] ;;
*{int} "x" <- #[13] ;;
Call #[ScFnPtr "f"] []
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i"
.
Definition ex3_opt_2 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[13] ;;
Call #[ScFnPtr "f"] []
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i"
.
Lemma ex3_sim_fun : ⊨ᶠ ex3 ex3_opt_1.
......
......@@ -8,29 +8,32 @@ Set Default Proof Using "Type".
Definition ex3_down : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[42] ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex3_down_opt_1 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[42] ;;
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex3_down_opt_2 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
......
From stbor.lang Require Import steps_retag.
From stbor.lang Require Import steps_retag steps_progress.
From stbor.sim Require Export instance.
Set Default Proof Using "Type".
......
......@@ -27,7 +27,7 @@ Fixpoint expr_wf (e: expr) : Prop :=
| Val v => value_wf v