Commit 41be1439 authored by Michael Sammler's avatar Michael Sammler
Browse files

try substituting lists

parent 51eb4150
......@@ -785,25 +785,25 @@ Fixpoint subst (x : var_name) (v : val) (e : expr) : expr :=
| StuckE => StuckE
end.
Fixpoint subst_l (xs : list var_name) (vs : list val) (e : expr) : expr :=
match xs, vs with
| x::xs', v::vs' => subst x v (subst_l xs' vs' e)
| _, _ => e
Fixpoint subst_l (xs : list (var_name * val)) (e : expr) : expr :=
match xs with
| (x, v)::xs' => subst_l xs' (subst x v e)
| _ => e
end.
Fixpoint subst_stmt (xs : list var_name) (vs : list val) (s : stmt) : stmt :=
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
match s with
| Goto b => Goto b
| Return e => Return (subst_l xs vs e)
| Switch it e m' bs def => Switch it (subst_l xs vs e) m' (subst_stmt xs vs <$> bs) (subst_stmt xs vs def)
| Assign o ly e1 e2 s => Assign o ly (subst_l xs vs e1) (subst_l xs vs e2) (subst_stmt xs vs s)
| SkipS s => SkipS (subst_stmt xs vs s)
| Return e => Return (subst_l xs e)
| Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
| Assign o ly e1 e2 s => Assign o ly (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
| SkipS s => SkipS (subst_stmt xs s)
| StuckS => StuckS
| ExprS e s => ExprS (subst_l xs vs e) (subst_stmt xs vs s)
| ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
end.
Definition subst_function (xs : list var_name) (vs : list val) (f : function) : function := {|
f_code := (subst_stmt xs vs) <$> f.(f_code);
Definition subst_function (xs : list (var_name * val)) (f : function) : function := {|
f_code := (subst_stmt xs) <$> f.(f_code);
f_args := f.(f_args); f_init := f.(f_init); f_local_vars := f.(f_local_vars);
|}.
......@@ -1005,7 +1005,7 @@ comparing pointers? (see lambda rust) *)
length lsa = length fn.(f_args)
length lsv = length fn.(f_local_vars)
(* substitute the variables in fn with the corresponding locations *)
fn' = subst_function (fn.(f_args).*1 ++ fn.(f_local_vars).*1) (val_of_loc <$> (lsa ++ lsv)) fn
fn' = subst_function (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1) (val_of_loc <$> (lsa ++ lsv))) fn
(* check the layout of the arguments *)
Forall2 has_layout_val vs fn.(f_args).*2
(* ensure that locations are aligned *)
......@@ -1323,5 +1323,5 @@ Canonical Structure allocationO := leibnizO allocation.
(*** Tests *)
Example simpl_subst :
subst_stmt (["y"; "x"]) [[MPoison; MPoison]; [MPoison]] (Return (BinOp AddOp PtrOp PtrOp (Var "x") (Var "y"))) = Return (BinOp AddOp PtrOp PtrOp (Val [MPoison]) (Val [MPoison; MPoison])).
subst_stmt ([("y", [MPoison; MPoison]); ("x", [MPoison])]) (Return (BinOp AddOp PtrOp PtrOp (Var "x") (Var "y"))) = Return (BinOp AddOp PtrOp PtrOp (Val [MPoison]) (Val [MPoison; MPoison])).
Proof. simpl. done. Abort.
......@@ -579,8 +579,8 @@ Lemma wp_call vf vl f fn Φ:
Forall2 has_layout_val vl (f_args fn).*2
fntbl_entry f fn - ( lsa lsv, Forall2 has_layout_loc lsa (f_args fn).*2 -
([ list] l; v lsa; vl, lv) - ([ list] l; v lsv; fn.(f_local_vars), l|v.2|) - Ψ',
WPs Goto fn.(f_init) {{ (subst_stmt (fn.(f_args).*1 ++ fn.(f_local_vars).*1)
(val_of_loc <$> (lsa ++ lsv))) <$> fn.(f_code), Ψ' }}
WPs Goto fn.(f_init) {{ (subst_stmt (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1)
(val_of_loc <$> (lsa ++ lsv)))) <$> fn.(f_code), Ψ' }}
( v, Ψ' v -
([ list] l; v lsa; fn.(f_args), l|v.2|)
([ list] l; v lsv; fn.(f_local_vars), l|v.2|)
......
......@@ -491,45 +491,38 @@ Proof.
Qed.
(*** Substitution *)
Fixpoint subst (x : var_name) (v : val) (e : expr) : expr :=
Fixpoint subst_l (xs : list (var_name * val)) (e : expr) : expr :=
match e with
| Var y => if bool_decide (y = x) then (Val v) else Var y
| Var y => if list_find (λ x, x.1 = y) xs is Some (_, (_, v)) then Val v else Var y
| Loc l => Loc l
| Val v => Val v
| UnOp op ot e => UnOp op ot (subst x v e)
| BinOp op ot1 ot2 e1 e2 => BinOp op ot1 ot2 (subst x v e1) (subst x v e2)
| CopyAllocId e1 e2 => CopyAllocId (subst x v e1) (subst x v e2)
| Deref o l e => Deref o l (subst x v e)
| CAS ot e1 e2 e3 => CAS ot (subst x v e1) (subst x v e2) (subst x v e3)
| Call f args => Call (subst x v f) (subst x v <$> args)
| Concat es => Concat (subst x v <$> es)
| SkipE e => SkipE (subst x v e)
| UnOp op ot e => UnOp op ot (subst_l xs e)
| BinOp op ot1 ot2 e1 e2 => BinOp op ot1 ot2 (subst_l xs e1) (subst_l xs e2)
| CopyAllocId e1 e2 => CopyAllocId (subst_l xs e1) (subst_l xs e2)
| Deref o l e => Deref o l (subst_l xs e)
| CAS ot e1 e2 e3 => CAS ot (subst_l xs e1) (subst_l xs e2) (subst_l xs e3)
| Call f args => Call (subst_l xs f) (subst_l xs <$> args)
| Concat es => Concat (subst_l xs <$> es)
| SkipE e => SkipE (subst_l xs e)
| StuckE => StuckE
| Use o ly e => Use o ly (subst x v e)
| AddrOf e => AddrOf (subst x v e)
| LValue e => LValue (subst x v e)
| AnnotExpr n a e => AnnotExpr n a (subst x v e)
| LocInfoE a e => LocInfoE a (subst x v e)
| StructInit ly fs => StructInit ly (prod_map id (subst x v) <$> fs)
| GetMember e s m => GetMember (subst x v e) s m
| GetMemberUnion e ul m => GetMemberUnion (subst x v e) ul m
| Use o ly e => Use o ly (subst_l xs e)
| AddrOf e => AddrOf (subst_l xs e)
| LValue e => LValue (subst_l xs e)
| AnnotExpr n a e => AnnotExpr n a (subst_l xs e)
| LocInfoE a e => LocInfoE a (subst_l xs e)
| StructInit ly fs => StructInit ly (prod_map id (subst_l xs) <$> fs)
| GetMember e s m => GetMember (subst_l xs e) s m
| GetMemberUnion e ul m => GetMemberUnion (subst_l xs e) ul m
| OffsetOf s m => OffsetOf s m
| OffsetOfUnion ul m => OffsetOfUnion ul m
| MacroE m es wf => MacroE m (subst x v <$> es) wf
| Expr e => Expr (lang.subst x v e)
| MacroE m es wf => MacroE m (subst_l xs <$> es) wf
| Expr e => Expr (lang.subst_l xs e)
end.
Fixpoint subst_l (xs : list var_name) (vs : list val) (e : expr) : expr :=
match xs, vs with
| x::xs', v::vs' => subst x v (subst_l xs' vs' e)
| _, _ => e
end.
Lemma to_expr_subst x v e :
to_expr (subst x v e) = lang.subst x v (to_expr e).
to_expr (subst_l [(x, v)] e) = lang.subst x v (to_expr e).
Proof.
elim: e => *//; cbn -[notation.GetMember]; (repeat case_bool_decide) => //=; f_equal; eauto.
elim: e => *//; cbn -[notation.GetMember]; (repeat case_bool_decide) => //=; f_equal; eauto; try by case_decide.
- (** Call *)
rewrite -!list_fmap_compose. apply list_fmap_ext' => //. by apply Forall_forall.
- (** Concat *)
......@@ -562,28 +555,48 @@ Proof.
rewrite -!list_fmap_compose. apply list_fmap_ext' => //. by apply Forall_forall.
Qed.
Lemma to_expr_subst_l xs vs e :
to_expr (subst_l xs vs e) = lang.subst_l xs vs (to_expr e).
Proof. elim: xs vs e => //= x xs IH [|v vs] // e. by rewrite to_expr_subst IH. Qed.
Lemma Forall_eq_fmap {A B} (xs : list A) (f1 f2 : A B) :
Forall (λ x, f1 x = f2 x) xs f1 <$> xs = f2 <$> xs.
Proof. elim => //. csimpl. congruence. Qed.
Lemma fmap_snd_prod_map {A B C} (l : list (A * B)) (f1 f2 : B C) :
f1 <$> l.*2 = f2 <$> l.*2
prod_map id f1 <$> l = prod_map id f2 <$> l.
Proof. elim: l => // -[??] ? IH. csimpl => -[??]. rewrite IH //. congruence. Qed.
Lemma to_expr_subst_l xs e :
to_expr (subst_l xs e) = lang.subst_l xs (to_expr e).
Proof.
elim: xs e => //=.
- elim => //= >; try congruence; try move => ->.
all: try move => /Forall_eq_fmap; try move/fmap_snd_prod_map.
all: by move => <-; by rewrite -list_fmap_compose.
- move => [x v] xs IH e. rewrite -to_expr_subst -IH. f_equal.
elim: e => //= >; try congruence; try move => ->.
all: try move => /Forall_eq_fmap; try move/fmap_snd_prod_map.
all: try by move => ->; by rewrite -list_fmap_compose.
case_decide => //. rewrite /subst_l.
by match goal with | |- context [list_find ?f ?xs] => destruct (list_find f xs) as [[?[??]]|] end.
Qed.
Fixpoint subst_stmt (xs : list var_name) (vs : list val) (s : stmt) : stmt :=
Fixpoint subst_stmt (xs : list (var_name * val)) (s : stmt) : stmt :=
match s with
| Goto b => Goto b
| Return e => Return (subst_l xs vs e)
| Switch it e m' bs def => Switch it (subst_l xs vs e) m' (subst_stmt xs vs <$> bs) (subst_stmt xs vs def)
| Assign o ly e1 e2 s => Assign o ly (subst_l xs vs e1) (subst_l xs vs e2) (subst_stmt xs vs s)
| SkipS s => SkipS (subst_stmt xs vs s)
| Return e => Return (subst_l xs e)
| Switch it e m' bs def => Switch it (subst_l xs e) m' (subst_stmt xs <$> bs) (subst_stmt xs def)
| Assign o ly e1 e2 s => Assign o ly (subst_l xs e1) (subst_l xs e2) (subst_stmt xs s)
| SkipS s => SkipS (subst_stmt xs s)
| StuckS => StuckS
| ExprS e s => ExprS (subst_l xs vs e) (subst_stmt xs vs s)
| If e s1 s2 => If (subst_l xs vs e) (subst_stmt xs vs s1) (subst_stmt xs vs s2)
| Assert e s => Assert (subst_l xs vs e) (subst_stmt xs vs s)
| AnnotStmt n a s => AnnotStmt n a (subst_stmt xs vs s)
| LocInfoS a s => LocInfoS a (subst_stmt xs vs s)
| Stmt s => Stmt (lang.subst_stmt xs vs s)
| ExprS e s => ExprS (subst_l xs e) (subst_stmt xs s)
| If e s1 s2 => If (subst_l xs e) (subst_stmt xs s1) (subst_stmt xs s2)
| Assert e s => Assert (subst_l xs e) (subst_stmt xs s)
| AnnotStmt n a s => AnnotStmt n a (subst_stmt xs s)
| LocInfoS a s => LocInfoS a (subst_stmt xs s)
| Stmt s => Stmt (lang.subst_stmt xs s)
end.
Lemma to_stmt_subst xs vs s :
to_stmt (subst_stmt xs vs s) = lang.subst_stmt xs vs (to_stmt s).
Lemma to_stmt_subst xs s :
to_stmt (subst_stmt xs s) = lang.subst_stmt xs (to_stmt s).
Proof.
elim: s => * //=; repeat rewrite to_expr_subst_l //; repeat f_equal => //; repeat rewrite -list_fmap_compose.
- by apply Forall_fmap_ext_1.
......
......@@ -59,9 +59,9 @@ Ltac convert_to_i2p_tac P ::=
Section automation.
Context `{!typeG Σ}.
Lemma tac_simpl_subst {B} xs vs s fn ls Q (fr : B _):
typed_stmt (W.to_stmt (W.subst_stmt xs vs s)) fn ls fr Q -
typed_stmt (subst_stmt xs vs (W.to_stmt s)) fn ls fr Q.
Lemma tac_simpl_subst {B} xs s fn ls Q (fr : B _):
typed_stmt (W.to_stmt (W.subst_stmt xs s)) fn ls fr Q -
typed_stmt (subst_stmt xs (W.to_stmt s)) fn ls fr Q.
Proof. by rewrite W.to_stmt_subst. Qed.
Lemma tac_typed_single_block_rec {B} P b Q fn ls (fr : B _) s:
......@@ -123,10 +123,10 @@ Ltac liRStmt :=
lazymatch goal with
| |- envs_entails ?Δ (typed_stmt ?s ?fn ?ls ?fr ?Q) =>
lazymatch s with
| subst_stmt ?xs ?vs ?s =>
| subst_stmt ?xs ?s =>
let s' := W.of_stmt s in
change (subst_stmt xs vs s) with (subst_stmt xs vs (W.to_stmt s'));
refine (tac_fast_apply (tac_simpl_subst _ _ _ _ _ _ _) _); simpl; unfold W.to_stmt, W.to_expr
change (subst_stmt xs s) with (subst_stmt xs (W.to_stmt s'));
refine (tac_fast_apply (tac_simpl_subst _ _ _ _ _ _) _); simpl; unfold W.to_stmt, W.to_expr
| _ =>
let s' := W.of_stmt s in
lazymatch s' with
......
......@@ -20,8 +20,8 @@ Section function.
(lsa : vec loc (length (fp x).(fp_atys))) (lsv : vec loc (length fn.(f_local_vars))),
let Qinit := ([list] l;tlsa;(fp x).(fp_atys), l ◁ₗ (t:mtype))
([list] l;plsv;fn.(f_local_vars), l ◁ₗ uninit (p.2)) (fp x).(fp_Pa) in
let Q := (subst_stmt (fn.(f_args).*1 ++ fn.(f_local_vars).*1)
(val_of_loc <$> (lsa ++ lsv))) <$> fn.(f_code) in
let Q := (subst_stmt (zip (fn.(f_args).*1 ++ fn.(f_local_vars).*1)
(val_of_loc <$> (lsa ++ lsv)))) <$> fn.(f_code) in
Qinit - typed_stmt (Goto fn.(f_init)) fn (lsa ++ lsv) (fp x).(fp_fr) Q
)%I.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment