Commit 8f7320ba authored by Lennard Gäher's avatar Lennard Gäher
Browse files

add blocked_shr

parent c8e540dd
From refinedc.lang Require Export lang.
Set Default Proof Using "Type".
Coercion val_of_loc : loc >-> val.
Coercion Val : val >-> expr.
Coercion Var : var_name >-> expr.
Definition string_to_varname (s : string) : var_name := s.
Coercion string_to_varname : string >-> var_name.
Coercion it_layout : int_type >-> layout.
Notation "☠" := MPoison : val_scope.
Notation "!{ ot , o } e" := (Deref o ot e%E) (at level 9, format "!{ ot , o } e") : expr_scope.
Notation "!{ ot } e" := (Deref Na1Ord ot e%E) (at level 9, format "!{ ot } e") : expr_scope.
(* − is a unicode minus, not the normal minus to prevent parsing conflicts *)
Notation "'−' '{' ot } e" := (UnOp NegOp ot e%E)
(at level 40, format "'−' '{' ot } e") : expr_scope.
Notation "e1 '+' '{' ot1 , ot2 } e2" := (BinOp AddOp ot1 ot2 e1%E e2%E)
(at level 50, left associativity, format "e1 '+' '{' ot1 , ot2 } e2") : expr_scope.
(* This conflicts with rewrite -{2}(app_nil_r vs). *)
Notation "e1 '-' '{' ot1 , ot2 } e2" := (BinOp SubOp ot1 ot2 e1%E e2%E)
(at level 50, left associativity, format "e1 '-' '{' ot1 , ot2 } e2") : expr_scope.
Notation "e1 '=' '{' ot1 , ot2 , rit } e2" := (BinOp (EqOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 '=' '{' ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 '!=' '{' ot1 , ot2 , rit } e2" := (BinOp (NeOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 '!=' '{' ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 ≤{ ot1 , ot2 , rit } e2" := (BinOp (LeOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ≤{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 <{ ot1 , ot2 , rit } e2" := (BinOp (LtOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 <{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 ≥{ ot1 , ot2 , rit } e2" := (BinOp (GeOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ≥{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 >{ ot1 , ot2 , rit } e2" := (BinOp (GtOp rit) ot1 ot2 e1%E e2%E)
(at level 70, format "e1 >{ ot1 , ot2 , rit } e2") : expr_scope.
Notation "e1 ×{ ot1 , ot2 } e2" := (BinOp MulOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ×{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 /{ ot1 , ot2 } e2" := (BinOp DivOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 /{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 %{ ot1 , ot2 } e2" := (BinOp ModOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 %{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 <<{ ot1 , ot2 } e2" := (BinOp ShlOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 <<{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 >>{ ot1 , ot2 } e2" := (BinOp ShrOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 >>{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 &{ ot1 , ot2 } e2" := (BinOp AndOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 &{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 |{ ot1 , ot2 } e2" := (BinOp OrOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 |{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 ^{ ot1 , ot2 } e2" := (BinOp XorOp ot1 ot2 e1%E e2%E)
(at level 70, format "e1 ^{ ot1 , ot2 } e2") : expr_scope.
Notation "e1 ,{ ot1 , ot2 } e2" := (BinOp Comma ot1 ot2 e1%E e2%E)
(at level 30, format "e1 ,{ ot1 , ot2 } e2") : expr_scope.
(* The offset must be evaluated first for the type system to work, thus the order is switched here. *)
Notation "e1 'at_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrOffsetOp ly) ot2 ot1 e2%E e1%E)
(at level 70, format "e1 at_offset{ ly , ot1 , ot2 } e2") : expr_scope.
Notation "e1 'at_neg_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrNegOffsetOp ly) ot2 ot1 e2%E e1%E)
(at level 70, format "e1 at_neg_offset{ ly , ot1 , ot2 } e2") : expr_scope.
Notation "e1 'sub_ptr{' ly , ot1 , ot2 } e2" := (BinOp (PtrDiffOp ly) ot2 ot1 e1%E e2%E)
(at level 70, format "e1 sub_ptr{ ly , ot1 , ot2 } e2") : expr_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <-{ ot , o } e2 ; s" := (Assign o ot e1%E e2%E s%E)
(at level 80, s at level 200, format "'[v' e1 '<-{' ot ',' o '}' e2 ';' '/' s ']'") : expr_scope.
Notation "e1 <-{ ot } e2 ; s" := (Assign Na1Ord ot e1%E e2%E s%E)
(at level 80, s at level 200, format "'[v' e1 '<-{' ot '}' e2 ';' '/' s ']'") : expr_scope.
Notation "'if{' ot '}' ':' e1 'then' s1 'else' s2" := (IfS ot e1%E s1%E s2%E)
(at level 102, e1, s1, s2 at level 150, format "'[v' 'if{' ot '}' ':' e1 'then' '/ ' s1 '/' 'else' '/ ' s2 ']'") : expr_scope.
Notation "'expr:' e ; s" := (ExprS e%E s%E)
(at level 80, s at level 200, format "'[v' 'expr:' e ';' '/' s ']'") : expr_scope.
Definition LogicalAnd (ot1 ot2 : op_type) rit (e1 e2 : expr) : expr :=
(IfE ot1 e1 (IfE ot2 e2 (i2v 1 rit) (i2v 0 rit)) (i2v 0 rit)).
Notation "e1 &&{ ot1 , ot2 , rit } e2" := (LogicalAnd ot1 ot2 rit e1 e2)
(at level 70, format "e1 &&{ ot1 , ot2 , rit } e2") : expr_scope.
Arguments LogicalAnd : simpl never.
Typeclasses Opaque LogicalAnd.
Definition LogicalOr (ot1 ot2 : op_type) rit (e1 e2 : expr) : expr :=
(IfE ot1 e1 (i2v 1 rit) (IfE ot2 e2 (i2v 1 rit) (i2v 0 rit))).
Notation "e1 ||{ ot1 , ot2 , rit } e2" := (LogicalOr ot1 ot2 rit e1 e2)
(at level 70, format "e1 ||{ ot1 , ot2 , rit } e2") : expr_scope.
Arguments LogicalOr : simpl never.
Typeclasses Opaque LogicalOr.
Definition Assert (ot : op_type) (e : expr) (s : stmt) : stmt := (if{ ot }: e then s else StuckS)%E.
Notation "'assert{' ot '}' ':' e ; s" := (Assert ot e%E s%E)
(at level 80, s at level 200, format "'[v' 'assert{' ot '}' ':' e ';' '/' s ']'") : expr_scope.
Arguments Assert : simpl never.
Typeclasses Opaque Assert.
Definition Use (o : order) (ot : op_type) (e : expr) := Deref o ot e.
Notation "'use{' ot , o } e" := (Use o ot e%E) (at level 9, format "'use{' ot , o } e") : expr_scope.
Notation "'use{' ot } e" := (Use Na1Ord ot e%E) (at level 9, format "'use{' ot } e") : expr_scope.
Arguments Use : simpl never.
Typeclasses Opaque Use.
Definition AddrOf (e : expr) := e.
(* TODO: this breaks the sigT notation { A : Type & (A -> nat) }. See if we can do something about it. *)
Notation "& e" := (AddrOf e%E) (at level 9, format "& e") : expr_scope.
Arguments AddrOf : simpl never.
Typeclasses Opaque AddrOf.
Definition LValue (e : expr) := e.
Arguments LValue : simpl never.
Typeclasses Opaque LValue.
Definition AnnotExpr (n : nat) {A} (a : A) (e : expr) := Nat.iter n SkipE e.
Arguments AnnotExpr : simpl never.
Typeclasses Opaque AnnotExpr.
Definition AnnotStmt (n : nat) {A} (a : A) (s : stmt) := Nat.iter n SkipS s.
Notation "'annot:' a ; s" := (AnnotStmt 0%nat a s%E)
(at level 80, s at level 200, format "'annot:' a ; s") : expr_scope.
Arguments AnnotStmt : simpl never.
Typeclasses Opaque AnnotStmt.
Inductive location_info :=
| LocationInfo (file : string) (line_start column_start line_end column_end : Z).
Definition LocInfo {B} (a : location_info) (b : B) := b.
Arguments LocInfo : simpl never.
Typeclasses Opaque LocInfo.
Notation "'locinfo:' a ; b" := (LocInfo (B:=stmt) a b%E)
(at level 80, b at level 200, format "'[v' 'locinfo:' a ';' '/' b ']'") : expr_scope.
Notation LocInfoE := (LocInfo (B:=expr)).
Definition MacroE (m : list expr expr) (es : list expr) := m es.
Arguments MacroE : simpl never.
Typeclasses Opaque MacroE.
(* One could probably get rid of this type class by swallowing the
substitutions in MacroE, i.e. make it parametrized by a list of names
and a list of expressions which are substituted in m. (Then one can
maybe also get rid of es?) *)
Class MacroWfSubst (m : list expr expr) : Prop :=
macro_wf_subst x v es: subst x v (m es) = m (subst x v <$> es)
.
(* Like [MacroE m es] but checks that [m es] is equal to [e] *)
Notation CheckedMacroE m es e := (ltac:(
let rec get_head e := match e with
| ?f ?a => get_head f
| ?x => x
end in
let mhead := get_head constr:(m%function) in
let munf := (eval unfold mhead in (m%function)) in
let esunf := (eval unfold LocInfo in (es%list)) in
let eunf := (eval unfold LocInfo in e) in
(* idtac munf; *)
unify (munf esunf) eunf with typeclass_instances;
exact (MacroE m es))) (only parsing).
Lemma annot_expr_S {A} n (a : A) e:
AnnotExpr (S n) a e = SkipE (AnnotExpr n a e).
Proof. done. Qed.
Lemma annot_expr_S_r {A} n (a : A) e:
AnnotExpr (S n) a e = (AnnotExpr n a (SkipE e)).
Proof. by rewrite /AnnotExpr Nat_iter_S_r. Qed.
Lemma annot_stmt_S {A} n (a : A) s:
AnnotStmt (S n) a s = SkipS (AnnotStmt n a s).
Proof. done. Qed.
Lemma annot_stmt_S_r {A} n (a : A) s:
AnnotStmt (S n) a s = (AnnotStmt n a (SkipS s)).
Proof. by rewrite /AnnotStmt Nat_iter_S_r. Qed.
(*** Layouts and structs *)
Definition StructInit (ly : struct_layout) (fs : list (string * expr)) : expr :=
let fs : gmap string expr := list_to_map fs in
let fn idly := default (Val (replicate (ly_size idly.2) MPoison)) (x idly.1; fs !! x) in
Concat (fn <$> sl_members ly).
Typeclasses Opaque StructInit.
Arguments StructInit : simpl never.
Definition GetMember (e : expr) (s : struct_layout) (m : var_name) : expr :=
(e at_offset{u8, PtrOp, IntOp size_t} Val (default [MPoison] (offset_of s.(sl_members) m = (λ m, val_of_Z (Z.of_nat m) size_t None))))%E.
Notation "e 'at{' s } m" := (GetMember e%E s m) (at level 10, format "e 'at{' s } m") : expr_scope.
Typeclasses Opaque GetMember.
Arguments GetMember : simpl never.
Definition OffsetOf (s : struct_layout) (m : var_name) : expr :=
(default StuckE (Val <$> (offset_of s.(sl_members) m) = (λ m, val_of_Z (Z.of_nat m) size_t None)))%E.
Typeclasses Opaque OffsetOf.
Arguments OffsetOf : simpl never.
Definition GetMemberUnion (e : expr) (ul : union_layout) (m : var_name) : expr := (e)%E.
Notation "e 'at_union{' ul } m" := (GetMemberUnion e%E ul m) (at level 10, format "e 'at_union{' ul } m") : expr_scope.
Typeclasses Opaque GetMemberUnion.
Arguments GetMemberUnion : simpl never.
Definition OffsetOfUnion (ul : union_layout) (m : var_name) : expr := (i2v 0 size_t).
Typeclasses Opaque OffsetOfUnion.
Arguments OffsetOfUnion : simpl never.
(*** Tests *)
Example test1 (l : loc) ly ot :
(l <-{ly} use{ot}(&l +{PtrOp, IntOp size_t} (l ={PtrOp, PtrOp, i32} l)); ExprS (Call l [ (l : expr); (l : expr)]) (l <-{ly, ScOrd} l; Goto "a"))%E =
(Assign Na1Ord ly l (Use Na1Ord ot (BinOp AddOp PtrOp (IntOp size_t) (AddrOf l) (BinOp (EqOp i32) PtrOp PtrOp l l))))
(ExprS (Call l [ Val (val_of_loc l); Val (val_of_loc l)]) ((Assign ScOrd ly l l) (Goto "a"))).
Proof. simpl. reflexivity. Abort.
Example test_get_member (l : loc) (s : struct_layout) ot :
(!{ot} (!{ot, ScOrd} l) at{s} "a")%E = GetMember (Deref Na1Ord ot (Deref ScOrd ot l%E)) s "a".
Proof. simpl. reflexivity. Abort.
From refinedc.lang Require Import lang notation.
Definition unit_layout : layout := {| ly_size := 1; ly_align_log := 0 |}.
Definition ref_layout := void_ptr.
(* move = copy, make old thing invalid (poison?) *)
(* [e2] should be side-effect free, otherwise we evaluate it multiple times... *)
Definition Move (e1 : expr) (e2 : expr) ot (s : stmt) : stmt :=
(e1 <-{ot} use{ot} e2;
(*e2 <-{ot} Val $ replicate (ot_layout ot).(ly_size) MPoison;*)
s)%E.
Notation "e1 'move{' ot '}' e2 ; s" := (Move e1%E e2%E ot s%E) (at level 80, s at level 200,
format "e1 'move{' ot '}' e2 ; s"
) : expr_scope.
Arguments Move : simpl never.
Typeclasses Opaque Move.
Inductive mutability := | Mut | Shr.
Inductive ptr_kind := | PRaw | PRef.
Definition Ref (m : mutability) (κ: string) (e : expr) := e.
Definition Raw (m : mutability) (e : expr) := e.
Notation "'&ref{' mut , κ '}' e" := (Ref mut κ e) (at level 9, format "&ref{ mut , κ } e") : expr_scope.
Notation "'&raw{' mut '}' e" := (Raw mut e) (at level 9, format "&raw{ mut } e") : expr_scope.
Arguments Ref : simpl never.
Typeclasses Opaque Ref.
Arguments Raw : simpl never.
Typeclasses Opaque Raw.
(* override the Caesium notation to get one later *)
Notation "'annot:' a ; s" := (AnnotStmt 1%nat a s%E)
(at level 80, s at level 200, format "'annot:' a ; s") : expr_scope.
From stdpp Require Import fin_maps.
From refinedc.lang Require Export notation rust.
From refinedc.lang Require Export notation.
Set Default Proof Using "Type".
Module W.
......@@ -115,7 +115,7 @@ Fixpoint to_expr (e : expr) : lang.expr :=
| OffsetOf s m => notation.OffsetOf s m
| OffsetOfUnion ul m => notation.OffsetOfUnion ul m
| MacroE m es _ => notation.MacroE m (to_expr <$> es)
| Borrow m κn e => rust.Ref m κn (to_expr e)
| Borrow m κn e => notation.Ref m κn (to_expr e)
| Expr e => e
end.
......@@ -136,7 +136,7 @@ Ltac of_expr e :=
let e := of_expr e in constr:(AnnotExpr n a e)
| notation.MacroE ?m ?es =>
let es := of_expr es in constr:(MacroE m es _)
| rust.Ref ?m ?κn ?e =>
| notation.Ref ?m ?κn ?e =>
let e := of_expr e in constr:(Borrow m κn e)
| notation.LocInfo ?a ?e =>
let e := of_expr e in constr:(LocInfoE a e)
......@@ -417,13 +417,13 @@ Fixpoint to_stmt (s : stmt) : lang.stmt :=
match s with
| Goto b => lang.Goto b
| Return e => lang.Return (to_expr e)
| IfS ot e s1 s2 => (if{ot}: to_expr e then to_stmt s1 else to_stmt s2)%E
| IfS ot e s1 s2 => lang.IfS ot (to_expr e) (to_stmt s1) (to_stmt s2)
| Switch it e m bs def => lang.Switch it (to_expr e) m (to_stmt <$> bs) (to_stmt def)
| Assign o ot e1 e2 s => lang.Assign o ot (to_expr e1) (to_expr e2) (to_stmt s)
| SkipS s => lang.SkipS (to_stmt s)
| StuckS => lang.StuckS
| ExprS e s => lang.ExprS (to_expr e) (to_stmt s)
| Assert ot e s => (assert{ot}: to_expr e; to_stmt s)%E
| Assert ot e s => notation.Assert ot (to_expr e) (to_stmt s)
| AnnotStmt n a s => notation.AnnotStmt n a (to_stmt s)
| LocInfoS a s => notation.LocInfo a (to_stmt s)
| Stmt s => s
......@@ -443,11 +443,11 @@ Ltac of_stmt s :=
| notation.LocInfo ?a ?s =>
let s := of_stmt s in
constr:(LocInfoS a s)
| (assert{?ot}: ?e ; ?s)%E =>
| notation.Assert ?ot ?e ?s =>
let e := of_expr e in
let s := of_stmt s in
constr:(Assert ot e s)
| (if{?ot}: ?e then ?s1 else ?s2)%E =>
| IfS ?ot ?e ?s1 ?s2 =>
let e := of_expr e in
let s1 := of_stmt s1 in
let s2 := of_stmt s2 in
......
......@@ -9,10 +9,10 @@ Set Default Proof Using "Type".
Module W.
Local Unset Elimination Schemes.
Section bla.
Context `{typeGS Σ}.
Context `{typeGS Σ}.
(* TODO place_wrap *)
Inductive ty : Type Type :=
Inductive ty : Type Type :=
| Atom (rt : Type) (t : type rt) : ty rt
| MutRef (rt : Type) (H : ghost_varG Σ rt) (t : ty rt) (κ : lft) : ty (rt * gname)%type
| ShrRef (rt : Type) (t : ty rt) (κ : lft) : ty rt
......@@ -28,9 +28,9 @@ Inductive lty : Type → Type :=
(*| BoxLty (rt : Type) (lt : lty rt) : lty rt*)
.
Fixpoint to_type {rt} (t : ty rt) : type rt :=
Fixpoint to_type {rt} (t : ty rt) : type rt :=
match t with
| Atom _ t => t
| Atom _ t => t
| MutRef rt _ t κ => mut_ref (to_type t) κ
| ShrRef _ t κ => shr_ref (to_type t) κ
(*| Box _ t => *)
......@@ -44,14 +44,14 @@ Fixpoint to_ltype {rt} (lt : lty rt) : ltype rt :=
| ShrLty _ _ lt κ => shr_ltype κ (to_ltype lt)
end.
(**
(**
Unfold the [OfTy] conversion by one step, if there is [OfTy] at the head.
Return [Some(lty, b)] if the conversion can be done, where [lty] is the new ltype
Return [Some(lty, b)] if the conversion can be done, where [lty] is the new ltype
and [b] indicates that an unfolding had to be done.
*)
Program Definition unfold_step {rt} (lt : lty rt) : option ((lty rt) * bool) :=
Program Definition unfold_step {rt} (lt : lty rt) : option ((lty rt) * bool) :=
match lt in lty T return option (lty T * bool) with
| OfTy _ H t =>
| OfTy _ H t =>
match t in (ty T) return (ghost_varG Σ T option (lty T * bool)) with
| Atom _ _ => λ _, None
| MutRef _ _ t κ =>
......@@ -65,10 +65,10 @@ Program Definition unfold_step {rt} (lt : lty rt) : option ((lty rt) * bool) :=
end
.
Fixpoint unfold_lty {rt} (lt : lty rt) (K : list place_ectx_item) : option (lty rt * bool) :=
match K with
Fixpoint unfold_lty {rt} (lt : lty rt) (K : list place_ectx_item) : option (lty rt * bool) :=
match K with
| [] => Some (lt, false)
| Ki :: K =>
| Ki :: K =>
match Ki with
| DerefPCtx _ _ =>
'(lt, changed) unfold_step lt;
......@@ -87,9 +87,9 @@ Fixpoint unfold_lty {rt} (lt : lty rt) (K : list place_ectx_item) : option (lty
end.
Fixpoint is_ty_strongly_writable {rt} (t : ty rt) (K : list place_ectx_item) : option bool :=
match K with
match K with
| [] => Some true
| Ki :: K =>
| Ki :: K =>
match Ki with
| DerefPCtx _ _ =>
match t with
......@@ -97,7 +97,7 @@ Fixpoint is_ty_strongly_writable {rt} (t : ty rt) (K : list place_ectx_item) : o
Some false
| ShrRef _ t κ =>
Some false
| _ =>
| _ =>
None
end
| _ => None
......@@ -105,9 +105,9 @@ Fixpoint is_ty_strongly_writable {rt} (t : ty rt) (K : list place_ectx_item) : o
end.
Fixpoint is_lty_strongly_writable {rt} (lt : lty rt) (K : list place_ectx_item) : option bool :=
match K with
match K with
| [] => Some true
| Ki :: K =>
| Ki :: K =>
match Ki with
| DerefPCtx _ _ =>
'(lt, _) unfold_step lt;
......@@ -116,28 +116,13 @@ Fixpoint is_lty_strongly_writable {rt} (lt : lty rt) (K : list place_ectx_item)
Some false
| ShrLty _ _ lt κ =>
Some false
| _ =>
| _ =>
None
end
| _ => None
end
end.
(* TODO: find out a good way to check for equality of lt1' and lt2' in the mut case.
is there a better way to do this than using an equality decider?
*)
(*
Fixpoint fold_lty {rt} (lt : lty rt) : lty rt :=
match lt in lty T return lty T with
| OfTy rt _ t => OfTy rt _ t
| MutLty rt _ _ lt1 lt2 κ =>
let lt1' := fold_lty lt1 in
let lt2' := fold_lty lt2 in
match lt1', lt2' with
| OfTy _ _ t1, OfTy _ _ t2 =>
end.
end.
*)
End bla.
Section test.
......@@ -145,10 +130,10 @@ Section test.
Definition folded_ty := (MutRef _ _ (MutRef _ _ (Atom Z (int i32)) static) static).
Definition folded_lty := OfTy _ _ (MutRef _ _ (MutRef _ _ (Atom Z (int i32)) static) static).
Eval cbn in (unfold_lty folded_lty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).
Eval cbn in (is_lty_strongly_writable folded_lty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).
Eval cbn in (is_ty_strongly_writable folded_ty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).
Eval cbn in (is_ty_strongly_writable folded_ty []).
(*Eval cbn in (unfold_lty folded_lty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).*)
(*Eval cbn in (is_lty_strongly_writable folded_lty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).*)
(*Eval cbn in (is_ty_strongly_writable folded_ty [DerefPCtx Na1Ord (IntOp i32); DerefPCtx Na1Ord (IntOp i32)]).*)
(*Eval cbn in (is_ty_strongly_writable folded_ty []).*)
End test.
......@@ -156,35 +141,35 @@ End W.
Ltac of_type t :=
lazymatch t with
| @mut_ref _ _ ?rt ?t ?H ?κ =>
| @mut_ref _ _ ?rt ?t ?H ?κ =>
let t := of_type t in
constr:(W.MutRef rt H t κ)
| @shr_ref _ _ ?rt ?t ?κ =>
| @shr_ref _ _ ?rt ?t ?κ =>
let t := of_type t in
constr:(W.ShrRef rt t κ)
| _ => constr:(W.Atom _ t)
end.
Ltac of_ltype lt :=
Ltac of_ltype lt :=
lazymatch lt with
| @lty_of_ty _ _ ?rt ?t ?H =>
| @lty_of_ty _ _ ?rt ?t ?H =>
let t := of_type t in
constr:(W.OfTy rt H t)
| @mut_ltype _ _ ?rt ?H ?lt1 ?κ ?lt2 => constr:(W.MutLty rt H _ lt1 lt2 κ)
| @shr_ltype _ _ ?rt ?H ?κ ?lt => constr:(W.ShrLty rt H lt κ)
| @blocked _ _ ?rt ?t ?H ?κ ?γ => constr:(W.BlockedLty rt H t κ γ)
| @blocked _ _ ?rt ?t ?H ?κ ?γ => constr:(W.BlockedLty rt H t κ γ)
end.
(* Reshape a place by unfolding [lty_of_ty] to ltypes *)
Ltac liRReshapePlace :=
Ltac liRReshapePlace :=
lazymatch goal with
| |- envs_entails ?Δ (typed_place ?π ?E ?L ?l ?lty ?r ?b ?K ?T) =>
let reified_lty := of_ltype lty in
let unfolded := eval cbn in (W.unfold_lty reified_lty K) in
match unfolded with
| Some (?unfolded, ?needs_unfold) =>
| Some (?unfolded, ?needs_unfold) =>
match needs_unfold with
| true =>
| true =>
let lty2 := eval cbn in (W.to_ltype unfolded) in
refine (tac_fast_apply (place_eqltype _ _ _ _ lty2 _ _ _ _ _) _); simpl
| false =>
......@@ -254,7 +239,10 @@ Ltac convert_to_i2p_tac P ::=
| typed_switch ?E ?L ?v ?rt ?ty ?r ?it ?m ?ss ?def ?fn ?ls ?R ?Q ?π => uconstr:(((_ : TypedSwitch E L v rt ty r it π) m ss def fn ls R Q).(i2p_proof))
| typed_assert ?E ?L ?ot ?v ?rt ?ty ?r ?s ?fn ?ls ?R ?Q ?π => uconstr:(((_ : TypedAssert E L ot v rt ty r π) s fn ls R Q).(i2p_proof))
| typed_read_end ?E ?L ?π ?l ?rt ?ty ?r ?b2 ?bmin ?ot ?T => uconstr:(((_ : TypedReadEnd E L π l ty r b2 bmin ot) T).(i2p_proof))
| typed_write_end ?E ?L ?π ?ot ?v1 ?rt1 ?ty1 ?r1 ?b2 ?bmin ?l2 ?rt2 ?lty2 ?r2 ?T => uconstr:(((_ : TypedWriteEnd E L π ot v1 rt1 ty1 r1 b2 bmin l2 rt2 lty2 r2) T).(i2p_proof))
| typed_write_end ?E ?L ?π ?ot ?v1 ?rt1 ?ty1 ?r1 ?b2 ?bmin ?l2 ?rt2 ?lty2 ?r2 ?T => uconstr:(((_ : TypedWriteEnd E L π ot v1 ty1 r1 b2 bmin l2 lty2 r2) T).(i2p_proof))
| typed_borrow_mut_end ?E ?L ?π ?κ ?l ?ty ?r ?b2 ?bmin ?T => uconstr:(((_ : TypedBorrowMutEnd E L π κ l ty r b2 bmin) T).(i2p_proof))
| typed_borrow_shr_end ?E ?L ?π ?κ ?l ?ty ?r ?b2 ?bmin ?T => uconstr:(((_ : TypedBorrowShrEnd E L π κ l ty r b2 bmin) T).(i2p_proof))
| cast_ltype_to_type ?E ?L ?lty ?T => uconstr:(((_ : CastLtypeToType E L lty) T).(i2p_proof))
(*| typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _).(i2p_proof))*)
(*| typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _).(i2p_proof))*)
(*| typed_annot_expr ?n ?a ?v ?P ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) .(i2p_proof))*)
......@@ -378,9 +366,8 @@ Ltac liRExpr :=
| W.Val _ => notypeclasses refine (tac_fast_apply (type_val E L _ π T) _)
| W.Loc _ => notypeclasses refine (tac_fast_apply (type_val E L _ π T) _)
| W.Use _ _ _ => notypeclasses refine (tac_fast_apply (type_use E L _ T _ _ π) _)
| W.Borrow Mut _ _ => notypeclasses refine (tac_fast_apply (type_mut_bor E L T _ π _ _ _) _)
(* TODO *)
(*| W.Borrow Shr _ _ => *)
| W.Borrow Mut _ _ => notypeclasses refine (tac_fast_apply (type_mut_bor E L T _ π _) _)
| W.Borrow Shr _ _ => notypeclasses refine (tac_fast_apply (type_shr_bor E L T _ π _) _)
(*| W.AddrOf _ => notypeclasses refine (tac_fast_apply (type_addr_of _ _) _)*)
| W.BinOp _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_bin_op E L _ _ _ _ _ π T) _)
| W.UnOp _ _ _ => notypeclasses refine (tac_fast_apply (type_un_op E L _ _ _ π T) _)
......@@ -398,59 +385,35 @@ Ltac liRExpr :=
end
end.
(* NOTE: this currently cannot support BinOp/UnOp (as find_place_ctx does), since we cannot evaluate here.
This seems to be a relatively fundamental limitation.
Possibly completely switch to type_write_strong? (and generalize type_place_strong to only determine later on in the checking process if we can do a strong update)
*)
Fixpoint decompose_place_ctx `{typeGS Σ} (e : W.expr) : option (list place_ectx_item * loc)%type :=
match e with
| W.Loc l => Some ([], l)
| W.Deref o ot e => '(K, l) decompose_place_ctx e; Some (K ++ [DerefPCtx o ot], l)
| W.GetMember e sl m => '(K, l) decompose_place_ctx e; Some (K ++ [GetMemberPCtx sl m], l)
| W.AnnotExpr n x e => '(K, l) decompose_place_ctx e; Some (K ++ [AnnotExprPCtx n x], l)
| W.LocInfoE a e => decompose_place_ctx e
| _ => None
end.
(* TODO: this is broken. we don't even know the type of the location at that point.
To solve these problems, we should really pick a common definition for writing.
i.e.: set up lemmas for typed_place_strong that also allows the possibility that it is not strongly writable after all.
Then have one common lemma that always works. *)
(*
Ltac liRWrite :=
Ltac liRWriteTo :=
lazymatch goal with
| |- envs_entails ?Δ (typed_write ?E ?L ?e ?ot ?v ?rt ?ty ?r ?π ?T) =>
let reified_ty := of_type ty in
let e' := W.of_expr e in
let K0 := eval cbn in (decompose_place_ctx e') in
match K0 with
| Some (?K, ?l) =>
idtac K;
let writable := eval cbn in (W.is_ty_strongly_writable reified_ty K) in
idtac writable;
match writable with
| Some true =>
notypeclasses refine (tac_fast_apply (type_write_strong E L T _ _ _ _ rt ty r π _) _); [ solve [refine _ ] |]