summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-18 15:52:24 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-18 15:52:24 +0000
commit165407527b1be7df6a376791719321c788e55149 (patch)
tree35c2eb9603f007b033fced56f21fa49fd105562f
parent1346309fd03e19da52156a700d037c348f27af0d (diff)
Simplification de Cminor: les affectations de variables locales ne sont
plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat
-rw-r--r--backend/Cmconstr.v1
-rw-r--r--backend/Cmconstrproof.v580
-rw-r--r--backend/Cminor.v160
-rw-r--r--backend/RTLgen.v147
-rw-r--r--backend/RTLgenproof.v463
-rw-r--r--backend/RTLgenproof1.v218
-rw-r--r--caml/CMparser.mly2
-rw-r--r--caml/CMtypecheck.ml17
-rw-r--r--cfrontend/Cminorgen.v4
-rw-r--r--cfrontend/Cminorgenproof.v166
-rw-r--r--test/cminor/aes.cmp15
11 files changed, 792 insertions, 981 deletions
diff --git a/backend/Cmconstr.v b/backend/Cmconstr.v
index f3a63fa..2cc947c 100644
--- a/backend/Cmconstr.v
+++ b/backend/Cmconstr.v
@@ -46,7 +46,6 @@ Open Scope cminor_scope.
Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr :=
match a with
| Evar id => Evar id
- | Eassign id b => Eassign id (lift_expr p b)
| Eop op bl => Eop op (lift_exprlist p bl)
| Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl)
| Estore chunk addr bl c =>
diff --git a/backend/Cmconstrproof.v b/backend/Cmconstrproof.v
index b9976ee..35b3d8a 100644
--- a/backend/Cmconstrproof.v
+++ b/backend/Cmconstrproof.v
@@ -67,38 +67,38 @@ Scheme eval_expr_ind_3 := Minimality for eval_expr Sort Prop
with eval_condexpr_ind_3 := Minimality for eval_condexpr Sort Prop
with eval_exprlist_ind_3 := Minimality for eval_exprlist Sort Prop.
-Hint Resolve eval_Evar eval_Eassign eval_Eop eval_Eload eval_Estore
+Hint Resolve eval_Evar eval_Eop eval_Eload eval_Estore
eval_Ecall eval_Econdition eval_Ealloc
eval_Elet eval_Eletvar
eval_CEtrue eval_CEfalse eval_CEcond
eval_CEcondition eval_Enil eval_Econs: evalexpr.
Lemma eval_list_one:
- forall sp le e1 m1 a t e2 m2 v,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
- eval_exprlist ge sp le e1 m1 (a ::: Enil) t e2 m2 (v :: nil).
+ forall sp le e m1 a t m2 v,
+ eval_expr ge sp le e m1 a t m2 v ->
+ eval_exprlist ge sp le e m1 (a ::: Enil) t m2 (v :: nil).
Proof.
intros. econstructor. eauto. constructor. traceEq.
Qed.
Lemma eval_list_two:
- forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 t,
- eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 ->
- eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 ->
+ forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 t,
+ eval_expr ge sp le e m1 a1 t1 m2 v1 ->
+ eval_expr ge sp le e m2 a2 t2 m3 v2 ->
t = t1 ** t2 ->
- eval_exprlist ge sp le e1 m1 (a1 ::: a2 ::: Enil) t e3 m3 (v1 :: v2 :: nil).
+ eval_exprlist ge sp le e m1 (a1 ::: a2 ::: Enil) t m3 (v1 :: v2 :: nil).
Proof.
intros. econstructor. eauto. econstructor. eauto. constructor.
reflexivity. traceEq.
Qed.
Lemma eval_list_three:
- forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 a3 t3 e4 m4 v3 t,
- eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 ->
- eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 ->
- eval_expr ge sp le e3 m3 a3 t3 e4 m4 v3 ->
+ forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 a3 t3 m4 v3 t,
+ eval_expr ge sp le e m1 a1 t1 m2 v1 ->
+ eval_expr ge sp le e m2 a2 t2 m3 v2 ->
+ eval_expr ge sp le e m3 a3 t3 m4 v3 ->
t = t1 ** t2 ** t3 ->
- eval_exprlist ge sp le e1 m1 (a1 ::: a2 ::: a3 ::: Enil) t e4 m4 (v1 :: v2 :: v3 :: nil).
+ eval_exprlist ge sp le e m1 (a1 ::: a2 ::: a3 ::: Enil) t m4 (v1 :: v2 :: v3 :: nil).
Proof.
intros. econstructor. eauto. econstructor. eauto. econstructor. eauto. constructor.
reflexivity. reflexivity. traceEq.
@@ -107,22 +107,22 @@ Qed.
Hint Resolve eval_list_one eval_list_two eval_list_three: evalexpr.
Lemma eval_lift_expr:
- forall w sp le e1 m1 a t e2 m2 v,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
+ forall w sp le e m1 a t m2 v,
+ eval_expr ge sp le e m1 a t m2 v ->
forall p le', insert_lenv le p w le' ->
- eval_expr ge sp le' e1 m1 (lift_expr p a) t e2 m2 v.
+ eval_expr ge sp le' e m1 (lift_expr p a) t m2 v.
Proof.
intros w.
apply (eval_expr_ind_3 ge
- (fun sp le e1 m1 a t e2 m2 v =>
+ (fun sp le e m1 a t m2 v =>
forall p le', insert_lenv le p w le' ->
- eval_expr ge sp le' e1 m1 (lift_expr p a) t e2 m2 v)
- (fun sp le e1 m1 a t e2 m2 vb =>
+ eval_expr ge sp le' e m1 (lift_expr p a) t m2 v)
+ (fun sp le e m1 a t m2 vb =>
forall p le', insert_lenv le p w le' ->
- eval_condexpr ge sp le' e1 m1 (lift_condexpr p a) t e2 m2 vb)
- (fun sp le e1 m1 al t e2 m2 vl =>
+ eval_condexpr ge sp le' e m1 (lift_condexpr p a) t m2 vb)
+ (fun sp le e m1 al t m2 vl =>
forall p le', insert_lenv le p w le' ->
- eval_exprlist ge sp le' e1 m1 (lift_exprlist p al) t e2 m2 vl));
+ eval_exprlist ge sp le' e m1 (lift_exprlist p al) t m2 vl));
simpl; intros; eauto with evalexpr.
destruct v1; eapply eval_Econdition;
@@ -139,9 +139,9 @@ Proof.
Qed.
Lemma eval_lift:
- forall sp le e1 m1 a t e2 m2 v w,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
- eval_expr ge sp (w::le) e1 m1 (lift a) t e2 m2 v.
+ forall sp le e m1 a t m2 v w,
+ eval_expr ge sp le e m1 a t m2 v ->
+ eval_expr ge sp (w::le) e m1 (lift a) t m2 v.
Proof.
intros. unfold lift. eapply eval_lift_expr.
eexact H. apply insert_lenv_0.
@@ -160,69 +160,69 @@ Ltac TrivialOp cstr :=
of operator applications. *)
Lemma inv_eval_Eop_0:
- forall sp le e1 m1 op t e2 m2 v,
- eval_expr ge sp le e1 m1 (Eop op Enil) t e2 m2 v ->
- t = E0 /\ e2 = e1 /\ m2 = m1 /\ eval_operation ge sp op nil = Some v.
+ forall sp le e m1 op t m2 v,
+ eval_expr ge sp le e m1 (Eop op Enil) t m2 v ->
+ t = E0 /\ m2 = m1 /\ eval_operation ge sp op nil = Some v.
Proof.
intros. inversion H. inversion H6.
intuition. congruence.
Qed.
Lemma inv_eval_Eop_1:
- forall sp le e1 m1 op t a1 e2 m2 v,
- eval_expr ge sp le e1 m1 (Eop op (a1 ::: Enil)) t e2 m2 v ->
+ forall sp le e m1 op t a1 m2 v,
+ eval_expr ge sp le e m1 (Eop op (a1 ::: Enil)) t m2 v ->
exists v1,
- eval_expr ge sp le e1 m1 a1 t e2 m2 v1 /\
+ eval_expr ge sp le e m1 a1 t m2 v1 /\
eval_operation ge sp op (v1 :: nil) = Some v.
Proof.
intros.
- inversion H. inversion H6. inversion H19.
+ inversion H. inversion H6. inversion H18.
subst. exists v1; intuition. rewrite E0_right. auto.
Qed.
Lemma inv_eval_Eop_2:
- forall sp le e1 m1 op a1 a2 t3 e3 m3 v,
- eval_expr ge sp le e1 m1 (Eop op (a1 ::: a2 ::: Enil)) t3 e3 m3 v ->
- exists t1, exists t2, exists e2, exists m2, exists v1, exists v2,
- eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 /\
- eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 /\
+ forall sp le e m1 op a1 a2 t3 m3 v,
+ eval_expr ge sp le e m1 (Eop op (a1 ::: a2 ::: Enil)) t3 m3 v ->
+ exists t1, exists t2, exists m2, exists v1, exists v2,
+ eval_expr ge sp le e m1 a1 t1 m2 v1 /\
+ eval_expr ge sp le e m2 a2 t2 m3 v2 /\
t3 = t1 ** t2 /\
eval_operation ge sp op (v1 :: v2 :: nil) = Some v.
Proof.
intros.
inversion H. subst. inversion H6. subst. inversion H8. subst.
- inversion H10. subst.
- exists t1; exists t0; exists e0; exists m0; exists v0; exists v1.
+ inversion H11. subst.
+ exists t1; exists t0; exists m0; exists v0; exists v1.
intuition. traceEq.
Qed.
Ltac SimplEval :=
match goal with
- | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op Enil) ?t ?e2 ?m2 ?v) -> _] =>
+ | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op Enil) ?t ?m2 ?v) -> _] =>
intro XX1;
- generalize (inv_eval_Eop_0 sp le e1 m1 op t e2 m2 v XX1);
+ generalize (inv_eval_Eop_0 sp le e m1 op t m2 v XX1);
clear XX1;
- intros [XX1 [XX2 [XX3 XX4]]];
- subst t e2 m2; simpl in XX4;
- try (simplify_eq XX4; clear XX4;
+ intros [XX1 [XX2 XX3]];
+ subst t m2; simpl in XX3;
+ try (simplify_eq XX3; clear XX3;
let EQ := fresh "EQ" in (intro EQ; rewrite EQ))
- | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op (?a1 ::: Enil)) ?t ?e2 ?m2 ?v) -> _] =>
+ | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: Enil)) ?t ?m2 ?v) -> _] =>
intro XX1;
- generalize (inv_eval_Eop_1 sp le e1 m1 op t a1 e2 m2 v XX1);
+ generalize (inv_eval_Eop_1 sp le e m1 op t a1 m2 v XX1);
clear XX1;
let v1 := fresh "v" in let EV := fresh "EV" in
let EQ := fresh "EQ" in
(intros [v1 [EV EQ]]; simpl in EQ)
- | [ |- (eval_expr _ ?sp ?le ?e1 ?m1 (Eop ?op (?a1 ::: ?a2 ::: Enil)) ?t ?e2 ?m2 ?v) -> _] =>
+ | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: ?a2 ::: Enil)) ?t ?m2 ?v) -> _] =>
intro XX1;
- generalize (inv_eval_Eop_2 sp le e1 m1 op a1 a2 t e2 m2 v XX1);
+ generalize (inv_eval_Eop_2 sp le e m1 op a1 a2 t m2 v XX1);
clear XX1;
let t1 := fresh "t" in let t2 := fresh "t" in
- let e := fresh "e" in let m := fresh "m" in
+ let m := fresh "m" in
let v1 := fresh "v" in let v2 := fresh "v" in
let EV1 := fresh "EV" in let EV2 := fresh "EV" in
let EQ := fresh "EQ" in let TR := fresh "TR" in
- (intros [t1 [t2 [e [m [v1 [v2 [EV1 [EV2 [TR EQ]]]]]]]]]; simpl in EQ)
+ (intros [t1 [t2 [m [v1 [v2 [EV1 [EV2 [TR EQ]]]]]]]]; simpl in EQ)
| _ => idtac
end.
@@ -245,57 +245,57 @@ Ltac InvEval H :=
*)
Theorem eval_negint:
- forall sp le e1 m1 a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (negint a) t e2 m2 (Vint (Int.neg x)).
+ forall sp le e m1 a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (negint a) t m2 (Vint (Int.neg x)).
Proof.
TrivialOp negint.
Qed.
Theorem eval_negfloat:
- forall sp le e1 m1 a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vfloat x) ->
- eval_expr ge sp le e1 m1 (negfloat a) t e2 m2 (Vfloat (Float.neg x)).
+ forall sp le e m1 a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vfloat x) ->
+ eval_expr ge sp le e m1 (negfloat a) t m2 (Vfloat (Float.neg x)).
Proof.
TrivialOp negfloat.
Qed.
Theorem eval_absfloat:
- forall sp le e1 m1 a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vfloat x) ->
- eval_expr ge sp le e1 m1 (absfloat a) t e2 m2 (Vfloat (Float.abs x)).
+ forall sp le e m1 a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vfloat x) ->
+ eval_expr ge sp le e m1 (absfloat a) t m2 (Vfloat (Float.abs x)).
Proof.
TrivialOp absfloat.
Qed.
Theorem eval_intoffloat:
- forall sp le e1 m1 a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vfloat x) ->
- eval_expr ge sp le e1 m1 (intoffloat a) t e2 m2 (Vint (Float.intoffloat x)).
+ forall sp le e m1 a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vfloat x) ->
+ eval_expr ge sp le e m1 (intoffloat a) t m2 (Vint (Float.intoffloat x)).
Proof.
TrivialOp intoffloat.
Qed.
Theorem eval_floatofint:
- forall sp le e1 m1 a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (floatofint a) t e2 m2 (Vfloat (Float.floatofint x)).
+ forall sp le e m1 a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (floatofint a) t m2 (Vfloat (Float.floatofint x)).
Proof.
TrivialOp floatofint.
Qed.
Theorem eval_floatofintu:
- forall sp le e1 m1 a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (floatofintu a) t e2 m2 (Vfloat (Float.floatofintu x)).
+ forall sp le e m1 a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (floatofintu a) t m2 (Vfloat (Float.floatofintu x)).
Proof.
TrivialOp floatofintu.
Qed.
Theorem eval_notint:
- forall sp le e1 m1 a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (notint a) t e2 m2 (Vint (Int.not x)).
+ forall sp le e m1 a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (notint a) t m2 (Vint (Int.not x)).
Proof.
unfold notint; intros until x; case (notint_match a); intros.
InvEval H. FuncInv. EvalOp. simpl. congruence.
@@ -310,10 +310,10 @@ Proof.
Qed.
Lemma eval_notbool_base:
- forall sp le e1 m1 a t e2 m2 v b,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
+ forall sp le e m1 a t m2 v b,
+ eval_expr ge sp le e m1 a t m2 v ->
Val.bool_of_val v b ->
- eval_expr ge sp le e1 m1 (notbool_base a) t e2 m2 (Val.of_bool (negb b)).
+ eval_expr ge sp le e m1 (notbool_base a) t m2 (Val.of_bool (negb b)).
Proof.
TrivialOp notbool_base. simpl.
inversion H0.
@@ -326,10 +326,10 @@ Hint Resolve Val.bool_of_true_val Val.bool_of_false_val
Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof.
Theorem eval_notbool:
- forall a sp le e1 m1 t e2 m2 v b,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
+ forall a sp le e m1 t m2 v b,
+ eval_expr ge sp le e m1 a t m2 v ->
Val.bool_of_val v b ->
- eval_expr ge sp le e1 m1 (notbool a) t e2 m2 (Val.of_bool (negb b)).
+ eval_expr ge sp le e m1 (notbool a) t m2 (Val.of_bool (negb b)).
Proof.
assert (N1: forall v b, Val.is_false v -> Val.bool_of_val v b -> Val.is_true (Val.of_bool (negb b))).
intros. inversion H0; simpl; auto; subst v; simpl in H.
@@ -341,33 +341,33 @@ Proof.
induction a; simpl; intros; try (eapply eval_notbool_base; eauto).
destruct o; try (eapply eval_notbool_base; eauto).
- destruct e. InvEval H. injection XX4; clear XX4; intro; subst v.
+ destruct e. InvEval H. injection XX3; clear XX3; intro; subst v.
inversion H0. rewrite Int.eq_false; auto.
simpl; eauto with evalexpr.
rewrite Int.eq_true; simpl; eauto with evalexpr.
eapply eval_notbool_base; eauto.
inversion H. subst.
- simpl in H12. eapply eval_Eop; eauto.
+ simpl in H11. eapply eval_Eop; eauto.
simpl. caseEq (eval_condition c vl); intros.
- rewrite H1 in H12.
+ rewrite H1 in H11.
assert (b0 = b).
- destruct b0; inversion H12; subst v; inversion H0; auto.
+ destruct b0; inversion H11; subst v; inversion H0; auto.
subst b0. rewrite (Op.eval_negate_condition _ _ H1).
destruct b; reflexivity.
- rewrite H1 in H12; discriminate.
+ rewrite H1 in H11; discriminate.
inversion H; eauto 10 with evalexpr valboolof.
inversion H; eauto 10 with evalexpr valboolof.
- inversion H. subst. eapply eval_Econdition with (t2 := t8). eexact H36.
+ inversion H. subst. eapply eval_Econdition with (t2 := t8). eexact H34.
destruct v4; eauto. auto.
Qed.
Theorem eval_addimm:
- forall sp le e1 m1 n a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (addimm n a) t e2 m2 (Vint (Int.add x n)).
+ forall sp le e m1 n a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (addimm n a) t m2 (Vint (Int.add x n)).
Proof.
unfold addimm; intros until x.
generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro.
@@ -376,16 +376,16 @@ Proof.
InvEval H0. EvalOp. simpl. rewrite Int.add_commut. auto.
InvEval H0. destruct (Genv.find_symbol ge s); discriminate.
InvEval H0.
- destruct sp; simpl in XX4; discriminate.
+ destruct sp; simpl in XX3; discriminate.
InvEval H0. FuncInv. EvalOp. simpl. subst x.
rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut.
EvalOp.
Qed.
Theorem eval_addimm_ptr:
- forall sp le e1 m1 n t a e2 m2 b ofs,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vptr b ofs) ->
- eval_expr ge sp le e1 m1 (addimm n a) t e2 m2 (Vptr b (Int.add ofs n)).
+ forall sp le e m1 n t a m2 b ofs,
+ eval_expr ge sp le e m1 a t m2 (Vptr b ofs) ->
+ eval_expr ge sp le e m1 (addimm n a) t m2 (Vptr b (Int.add ofs n)).
Proof.
unfold addimm; intros until ofs.
generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro.
@@ -396,8 +396,8 @@ Proof.
destruct (Genv.find_symbol ge s).
rewrite Int.add_commut. congruence.
discriminate.
- InvEval H0. destruct sp; simpl in XX4; try discriminate.
- inversion XX4. EvalOp. simpl. decEq. decEq.
+ InvEval H0. destruct sp; simpl in XX3; try discriminate.
+ inversion XX3. EvalOp. simpl. decEq. decEq.
rewrite Int.add_assoc. decEq. apply Int.add_commut.
InvEval H0. FuncInv. subst b0; subst ofs. EvalOp. simpl.
rewrite (Int.add_commut n m). rewrite Int.add_assoc. auto.
@@ -405,10 +405,10 @@ Proof.
Qed.
Theorem eval_add:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (add a b) (t1**t2) e3 m3 (Vint (Int.add x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vint (Int.add x y)).
Proof.
intros until y. unfold add; case (add_match a b); intros.
InvEval H. rewrite Int.add_commut. apply eval_addimm.
@@ -432,10 +432,10 @@ Proof.
Qed.
Theorem eval_add_ptr:
- forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (add a b) (t1**t2) e3 m3 (Vptr p (Int.add x y)).
+ forall sp le e m1 a t1 m2 p x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add x y)).
Proof.
intros until y. unfold add; case (add_match a b); intros.
InvEval H.
@@ -457,10 +457,10 @@ Proof.
Qed.
Theorem eval_add_ptr_2:
- forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p y) ->
- eval_expr ge sp le e1 m1 (add a b) (t1**t2) e3 m3 (Vptr p (Int.add y x)).
+ forall sp le e m1 a t1 m2 p x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vptr p y) ->
+ eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add y x)).
Proof.
intros until y. unfold add; case (add_match a b); intros.
InvEval H.
@@ -484,10 +484,10 @@ Proof.
Qed.
Theorem eval_sub:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (sub a b) (t1**t2) e3 m3 (Vint (Int.sub x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)).
Proof.
intros until y.
unfold sub; case (sub_match a b); intros.
@@ -512,10 +512,10 @@ Proof.
Qed.
Theorem eval_sub_ptr_int:
- forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (sub a b) (t1**t2) e3 m3 (Vptr p (Int.sub x y)).
+ forall sp le e m1 a t1 m2 p x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vptr p (Int.sub x y)).
Proof.
intros until y.
unfold sub; case (sub_match a b); intros.
@@ -541,10 +541,10 @@ Proof.
Qed.
Theorem eval_sub_ptr_ptr:
- forall sp le e1 m1 a t1 e2 m2 p x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p y) ->
- eval_expr ge sp le e1 m1 (sub a b) (t1**t2) e3 m3 (Vint (Int.sub x y)).
+ forall sp le e m1 a t1 m2 p x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vptr p y) ->
+ eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)).
Proof.
intros until y.
unfold sub; case (sub_match a b); intros.
@@ -571,9 +571,9 @@ Proof.
Qed.
Lemma eval_rolm:
- forall sp le e1 m1 a amount mask t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (rolm a amount mask) t e2 m2 (Vint (Int.rolm x amount mask)).
+ forall sp le e m1 a amount mask t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (rolm a amount mask) t m2 (Vint (Int.rolm x amount mask)).
Proof.
intros until x. unfold rolm; case (rolm_match a); intros.
InvEval H. eauto with evalexpr.
@@ -590,10 +590,10 @@ Proof.
Qed.
Theorem eval_shlimm:
- forall sp le e1 m1 a n t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
+ forall sp le e m1 a n t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
Int.ltu n (Int.repr 32) = true ->
- eval_expr ge sp le e1 m1 (shlimm a n) t e2 m2 (Vint (Int.shl x n)).
+ eval_expr ge sp le e m1 (shlimm a n) t m2 (Vint (Int.shl x n)).
Proof.
intros. unfold shlimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
@@ -604,10 +604,10 @@ Proof.
Qed.
Theorem eval_shruimm:
- forall sp le e1 m1 a n t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
+ forall sp le e m1 a n t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
Int.ltu n (Int.repr 32) = true ->
- eval_expr ge sp le e1 m1 (shruimm a n) t e2 m2 (Vint (Int.shru x n)).
+ eval_expr ge sp le e m1 (shruimm a n) t m2 (Vint (Int.shru x n)).
Proof.
intros. unfold shruimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
@@ -618,9 +618,9 @@ Proof.
Qed.
Lemma eval_mulimm_base:
- forall sp le e1 m1 a t n e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (mulimm_base n a) t e2 m2 (Vint (Int.mul x n)).
+ forall sp le e m1 a t n m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (mulimm_base n a) t m2 (Vint (Int.mul x n)).
Proof.
intros; unfold mulimm_base.
generalize (Int.one_bits_decomp n).
@@ -633,7 +633,7 @@ Proof.
rewrite Int.add_zero. rewrite <- Int.shl_mul.
apply eval_shlimm. auto. auto with coqlib.
destruct l.
- intros. apply eval_Elet with t e2 m2 (Vint x) E0. auto.
+ intros. apply eval_Elet with t m2 (Vint x) E0. auto.
rewrite H1. simpl. rewrite Int.add_zero.
rewrite Int.mul_add_distr_r.
rewrite <- Int.shl_mul.
@@ -650,9 +650,9 @@ Proof.
Qed.
Theorem eval_mulimm:
- forall sp le e1 m1 a n t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (mulimm n a) t e2 m2 (Vint (Int.mul x n)).
+ forall sp le e m1 a n t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (mulimm n a) t m2 (Vint (Int.mul x n)).
Proof.
intros until x; unfold mulimm.
generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro.
@@ -670,10 +670,10 @@ Proof.
Qed.
Theorem eval_mul:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (mul a b) (t1**t2) e3 m3 (Vint (Int.mul x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (mul a b) (t1**t2) m3 (Vint (Int.mul x y)).
Proof.
intros until y.
unfold mul; case (mul_match a b); intros.
@@ -684,11 +684,11 @@ Proof.
Qed.
Theorem eval_divs:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
y <> Int.zero ->
- eval_expr ge sp le e1 m1 (divs a b) (t1**t2) e3 m3 (Vint (Int.divs x y)).
+ eval_expr ge sp le e m1 (divs a b) (t1**t2) m3 (Vint (Int.divs x y)).
Proof.
TrivialOp divs. simpl.
predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto.
@@ -700,11 +700,11 @@ Lemma eval_mod_aux:
y <> Int.zero ->
eval_operation ge sp divop (Vint x :: Vint y :: nil) =
Some (Vint (semdivop x y))) ->
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
y <> Int.zero ->
- eval_expr ge sp le e1 m1 (mod_aux divop a b) (t1**t2) e3 m3
+ eval_expr ge sp le e m1 (mod_aux divop a b) (t1**t2) m3
(Vint (Int.sub x (Int.mul (semdivop x y) y))).
Proof.
intros; unfold mod_aux.
@@ -726,11 +726,11 @@ Proof.
Qed.
Theorem eval_mods:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
y <> Int.zero ->
- eval_expr ge sp le e1 m1 (mods a b) (t1**t2) e3 m3 (Vint (Int.mods x y)).
+ eval_expr ge sp le e m1 (mods a b) (t1**t2) m3 (Vint (Int.mods x y)).
Proof.
intros; unfold mods.
rewrite Int.mods_divs.
@@ -740,22 +740,22 @@ Proof.
Qed.
Lemma eval_divu_base:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
y <> Int.zero ->
- eval_expr ge sp le e1 m1 (Eop Odivu (a ::: b ::: Enil)) (t1**t2) e3 m3 (Vint (Int.divu x y)).
+ eval_expr ge sp le e m1 (Eop Odivu (a ::: b ::: Enil)) (t1**t2) m3 (Vint (Int.divu x y)).
Proof.
intros. EvalOp. simpl.
predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto.
Qed.
Theorem eval_divu:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
y <> Int.zero ->
- eval_expr ge sp le e1 m1 (divu a b) (t1**t2) e3 m3 (Vint (Int.divu x y)).
+ eval_expr ge sp le e m1 (divu a b) (t1**t2) m3 (Vint (Int.divu x y)).
Proof.
intros until y.
unfold divu; case (divu_match b); intros.
@@ -768,11 +768,11 @@ Proof.
Qed.
Theorem eval_modu:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
y <> Int.zero ->
- eval_expr ge sp le e1 m1 (modu a b) (t1**t2) e3 m3 (Vint (Int.modu x y)).
+ eval_expr ge sp le e m1 (modu a b) (t1**t2) m3 (Vint (Int.modu x y)).
Proof.
intros until y; unfold modu; case (divu_match b); intros.
InvEval H0. caseEq (Int.is_power2 y).
@@ -789,9 +789,9 @@ Proof.
Qed.
Theorem eval_andimm:
- forall sp le e1 m1 n a t e2 m2 x,
- eval_expr ge sp le e1 m1 a t e2 m2 (Vint x) ->
- eval_expr ge sp le e1 m1 (andimm n a) t e2 m2 (Vint (Int.and x n)).
+ forall sp le e m1 n a t m2 x,
+ eval_expr ge sp le e m1 a t m2 (Vint x) ->
+ eval_expr ge sp le e m1 (andimm n a) t m2 (Vint (Int.and x n)).
Proof.
intros. unfold andimm. case (Int.is_rlw_mask n).
rewrite <- Int.rolm_zero. apply eval_rolm; auto.
@@ -799,10 +799,10 @@ Proof.
Qed.
Theorem eval_and:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (and a b) (t1**t2) e3 m3 (Vint (Int.and x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (and a b) (t1**t2) m3 (Vint (Int.and x y)).
Proof.
intros until y; unfold and; case (mul_match a b); intros.
InvEval H. rewrite Int.and_commut.
@@ -812,11 +812,11 @@ Proof.
Qed.
Remark eval_same_expr_pure:
- forall a1 a2 sp le e1 m1 t1 e2 m2 v1 t2 e3 m3 v2,
+ forall a1 a2 sp le e m1 t1 m2 v1 t2 m3 v2,
same_expr_pure a1 a2 = true ->
- eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 ->
- eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 ->
- t1 = E0 /\ t2 = E0 /\ a2 = a1 /\ v2 = v1 /\ e2 = e1 /\ m2 = m1.
+ eval_expr ge sp le e m1 a1 t1 m2 v1 ->
+ eval_expr ge sp le e m2 a2 t2 m3 v2 ->
+ t1 = E0 /\ t2 = E0 /\ a2 = a1 /\ v2 = v1 /\ m2 = m1.
Proof.
intros until v2.
destruct a1; simpl; try (intros; discriminate).
@@ -828,18 +828,18 @@ Proof.
Qed.
Lemma eval_or:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (or a b) (t1**t2) e3 m3 (Vint (Int.or x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (or a b) (t1**t2) m3 (Vint (Int.or x y)).
Proof.
intros until y; unfold or; case (or_match a b); intros.
generalize (Int.eq_spec amount1 amount2); case (Int.eq amount1 amount2); intro.
case (Int.is_rlw_mask (Int.or mask1 mask2)).
caseEq (same_expr_pure t0 t3); intro.
simpl. InvEval H. FuncInv. InvEval H0. FuncInv.
- generalize (eval_same_expr_pure _ _ _ _ _ _ _ _ _ _ _ _ _ _ H2 EV EV0).
- intros [EQ1 [EQ2 [EQ3 [EQ4 [EQ5 EQ6]]]]].
+ generalize (eval_same_expr_pure _ _ _ _ _ _ _ _ _ _ _ _ H2 EV EV0).
+ intros [EQ1 [EQ2 [EQ3 [EQ4 EQ5]]]].
injection EQ4; intro EQ7. subst.
EvalOp. simpl. rewrite Int.or_rolm. auto.
simpl. EvalOp.
@@ -849,18 +849,18 @@ Proof.
Qed.
Theorem eval_xor:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (xor a b) (t1**t2) e3 m3 (Vint (Int.xor x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (xor a b) (t1**t2) m3 (Vint (Int.xor x y)).
Proof. TrivialOp xor. Qed.
Theorem eval_shl:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
Int.ltu y (Int.repr 32) = true ->
- eval_expr ge sp le e1 m1 (shl a b) (t1**t2) e3 m3 (Vint (Int.shl x y)).
+ eval_expr ge sp le e m1 (shl a b) (t1**t2) m3 (Vint (Int.shl x y)).
Proof.
intros until y; unfold shl; case (shift_match b); intros.
InvEval H0. rewrite E0_right. apply eval_shlimm; auto.
@@ -868,21 +868,21 @@ Proof.
Qed.
Theorem eval_shr:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
Int.ltu y (Int.repr 32) = true ->
- eval_expr ge sp le e1 m1 (shr a b) (t1**t2) e3 m3 (Vint (Int.shr x y)).
+ eval_expr ge sp le e m1 (shr a b) (t1**t2) m3 (Vint (Int.shr x y)).
Proof.
TrivialOp shr. simpl. rewrite H1. auto.
Qed.
Theorem eval_shru:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
Int.ltu y (Int.repr 32) = true ->
- eval_expr ge sp le e1 m1 (shru a b) (t1**t2) e3 m3 (Vint (Int.shru x y)).
+ eval_expr ge sp le e m1 (shru a b) (t1**t2) m3 (Vint (Int.shru x y)).
Proof.
intros until y; unfold shru; case (shift_match b); intros.
InvEval H0. rewrite E0_right; apply eval_shruimm; auto.
@@ -890,10 +890,10 @@ Proof.
Qed.
Theorem eval_addf:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) ->
- eval_expr ge sp le e1 m1 (addf a b) (t1**t2) e3 m3 (Vfloat (Float.add x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vfloat x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vfloat y) ->
+ eval_expr ge sp le e m1 (addf a b) (t1**t2) m3 (Vfloat (Float.add x y)).
Proof.
intros until y; unfold addf; case (addf_match a b); intros.
InvEval H. FuncInv. EvalOp.
@@ -909,10 +909,10 @@ Proof.
Qed.
Theorem eval_subf:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) ->
- eval_expr ge sp le e1 m1 (subf a b) (t1**t2) e3 m3 (Vfloat (Float.sub x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vfloat x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vfloat y) ->
+ eval_expr ge sp le e m1 (subf a b) (t1**t2) m3 (Vfloat (Float.sub x y)).
Proof.
intros until y; unfold subf; case (subf_match a b); intros.
InvEval H. FuncInv. EvalOp.
@@ -922,23 +922,23 @@ Proof.
Qed.
Theorem eval_mulf:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) ->
- eval_expr ge sp le e1 m1 (mulf a b) (t1**t2) e3 m3 (Vfloat (Float.mul x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vfloat x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vfloat y) ->
+ eval_expr ge sp le e m1 (mulf a b) (t1**t2) m3 (Vfloat (Float.mul x y)).
Proof. TrivialOp mulf. Qed.
Theorem eval_divf:
- forall sp le e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) ->
- eval_expr ge sp le e1 m1 (divf a b) (t1**t2) e3 m3 (Vfloat (Float.div x y)).
+ forall sp le e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vfloat x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vfloat y) ->
+ eval_expr ge sp le e m1 (divf a b) (t1**t2) m3 (Vfloat (Float.div x y)).
Proof. TrivialOp divf. Qed.
Theorem eval_cast8signed:
- forall sp le e1 m1 a t e2 m2 v,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
- eval_expr ge sp le e1 m1 (cast8signed a) t e2 m2 (Val.cast8signed v).
+ forall sp le e m1 a t m2 v,
+ eval_expr ge sp le e m1 a t m2 v ->
+ eval_expr ge sp le e m1 (cast8signed a) t m2 (Val.cast8signed v).
Proof.
intros until v; unfold cast8signed; case (cast8signed_match a); intros.
replace (Val.cast8signed v) with v. auto.
@@ -947,9 +947,9 @@ Proof.
Qed.
Theorem eval_cast8unsigned:
- forall sp le e1 m1 a t e2 m2 v,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
- eval_expr ge sp le e1 m1 (cast8unsigned a) t e2 m2 (Val.cast8unsigned v).
+ forall sp le e m1 a t m2 v,
+ eval_expr ge sp le e m1 a t m2 v ->
+ eval_expr ge sp le e m1 (cast8unsigned a) t m2 (Val.cast8unsigned v).
Proof.
intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros.
replace (Val.cast8unsigned v) with v. auto.
@@ -958,9 +958,9 @@ Proof.
Qed.
Theorem eval_cast16signed:
- forall sp le e1 m1 a t e2 m2 v,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
- eval_expr ge sp le e1 m1 (cast16signed a) t e2 m2 (Val.cast16signed v).
+ forall sp le e m1 a t m2 v,
+ eval_expr ge sp le e m1 a t m2 v ->
+ eval_expr ge sp le e m1 (cast16signed a) t m2 (Val.cast16signed v).
Proof.
intros until v; unfold cast16signed; case (cast16signed_match a); intros.
replace (Val.cast16signed v) with v. auto.
@@ -969,9 +969,9 @@ Proof.
Qed.
Theorem eval_cast16unsigned:
- forall sp le e1 m1 a t e2 m2 v,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
- eval_expr ge sp le e1 m1 (cast16unsigned a) t e2 m2 (Val.cast16unsigned v).
+ forall sp le e m1 a t m2 v,
+ eval_expr ge sp le e m1 a t m2 v ->
+ eval_expr ge sp le e m1 (cast16unsigned a) t m2 (Val.cast16unsigned v).
Proof.
intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros.
replace (Val.cast16unsigned v) with v. auto.
@@ -980,9 +980,9 @@ Proof.
Qed.
Theorem eval_singleoffloat:
- forall sp le e1 m1 a t e2 m2 v,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
- eval_expr ge sp le e1 m1 (singleoffloat a) t e2 m2 (Val.singleoffloat v).
+ forall sp le e m1 a t m2 v,
+ eval_expr ge sp le e m1 a t m2 v ->
+ eval_expr ge sp le e m1 (singleoffloat a) t m2 (Val.singleoffloat v).
Proof.
intros until v; unfold singleoffloat; case (singleoffloat_match a); intros.
replace (Val.singleoffloat v) with v. auto.
@@ -991,42 +991,42 @@ Proof.
Qed.
Theorem eval_cmp:
- forall sp le c e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 (Val.of_bool (Int.cmp c x y)).
+ forall sp le c e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 (Val.of_bool (Int.cmp c x y)).
Proof.
TrivialOp cmp.
simpl. case (Int.cmp c x y); auto.
Qed.
Theorem eval_cmp_null_r:
- forall sp le c e1 m1 a t1 e2 m2 p x b t2 e3 m3 v,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint Int.zero) ->
+ forall sp le c e m1 a t1 m2 p x b t2 m3 v,
+ eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint Int.zero) ->
(c = Ceq /\ v = Vfalse) \/ (c = Cne /\ v = Vtrue) ->
- eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 v.
+ eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 v.
Proof.
TrivialOp cmp.
simpl. elim H1; intros [EQ1 EQ2]; subst c; subst v; reflexivity.
Qed.
Theorem eval_cmp_null_l:
- forall sp le c e1 m1 a t1 e2 m2 p x b t2 e3 m3 v,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint Int.zero) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p x) ->
+ forall sp le c e m1 a t1 m2 p x b t2 m3 v,
+ eval_expr ge sp le e m1 a t1 m2 (Vint Int.zero) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vptr p x) ->
(c = Ceq /\ v = Vfalse) \/ (c = Cne /\ v = Vtrue) ->
- eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 v.
+ eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 v.
Proof.
TrivialOp cmp.
simpl. elim H1; intros [EQ1 EQ2]; subst c; subst v; reflexivity.
Qed.
Theorem eval_cmp_ptr:
- forall sp le c e1 m1 a t1 e2 m2 p x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vptr p x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vptr p y) ->
- eval_expr ge sp le e1 m1 (cmp c a b) (t1**t2) e3 m3 (Val.of_bool (Int.cmp c x y)).
+ forall sp le c e m1 a t1 m2 p x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vptr p x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vptr p y) ->
+ eval_expr ge sp le e m1 (cmp c a b) (t1**t2) m3 (Val.of_bool (Int.cmp c x y)).
Proof.
TrivialOp cmp.
simpl. unfold eq_block. rewrite zeq_true.
@@ -1034,32 +1034,32 @@ Proof.
Qed.
Theorem eval_cmpu:
- forall sp le c e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vint x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vint y) ->
- eval_expr ge sp le e1 m1 (cmpu c a b) (t1**t2) e3 m3 (Val.of_bool (Int.cmpu c x y)).
+ forall sp le c e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vint x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vint y) ->
+ eval_expr ge sp le e m1 (cmpu c a b) (t1**t2) m3 (Val.of_bool (Int.cmpu c x y)).
Proof.
TrivialOp cmpu.
simpl. case (Int.cmpu c x y); auto.
Qed.
Theorem eval_cmpf:
- forall sp le c e1 m1 a t1 e2 m2 x b t2 e3 m3 y,
- eval_expr ge sp le e1 m1 a t1 e2 m2 (Vfloat x) ->
- eval_expr ge sp le e2 m2 b t2 e3 m3 (Vfloat y) ->
- eval_expr ge sp le e1 m1 (cmpf c a b) (t1**t2) e3 m3 (Val.of_bool (Float.cmp c x y)).
+ forall sp le c e m1 a t1 m2 x b t2 m3 y,
+ eval_expr ge sp le e m1 a t1 m2 (Vfloat x) ->
+ eval_expr ge sp le e m2 b t2 m3 (Vfloat y) ->
+ eval_expr ge sp le e m1 (cmpf c a b) (t1**t2) m3 (Val.of_bool (Float.cmp c x y)).
Proof.
TrivialOp cmpf.
simpl. case (Float.cmp c x y); auto.
Qed.
Lemma eval_base_condition_of_expr:
- forall sp le a e1 m1 t e2 m2 v (b: bool),
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
+ forall sp le a e m1 t m2 v (b: bool),
+ eval_expr ge sp le e m1 a t m2 v ->
Val.bool_of_val v b ->
- eval_condexpr ge sp le e1 m1
+ eval_condexpr ge sp le e m1
(CEcond (Ccompuimm Cne Int.zero) (a ::: Enil))
- t e2 m2 b.
+ t m2 b.
Proof.
intros.
eapply eval_CEcond. eauto with evalexpr.
@@ -1067,60 +1067,60 @@ Proof.
Qed.
Lemma eval_condition_of_expr:
- forall a sp le e1 m1 t e2 m2 v (b: bool),
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
+ forall a sp le e m1 t m2 v (b: bool),
+ eval_expr ge sp le e m1 a t m2 v ->
Val.bool_of_val v b ->
- eval_condexpr ge sp le e1 m1 (condexpr_of_expr a) t e2 m2 b.
+ eval_condexpr ge sp le e m1 (condexpr_of_expr a) t m2 b.
Proof.
induction a; simpl; intros;
try (eapply eval_base_condition_of_expr; eauto; fail).
destruct o; try (eapply eval_base_condition_of_expr; eauto; fail).
- destruct e. InvEval H. inversion XX4; subst v.
+ destruct e. InvEval H. inversion XX3; subst v.
inversion H0.
rewrite Int.eq_false; auto. constructor.
subst i; rewrite Int.eq_true. constructor.
eapply eval_base_condition_of_expr; eauto.
- inversion H. subst. eapply eval_CEcond; eauto. simpl in H12.
+ inversion H. subst. eapply eval_CEcond; eauto. simpl in H11.
destruct (eval_condition c vl); try discriminate.
- destruct b0; inversion H12; subst; inversion H0; congruence.
+ destruct b0; inversion H11; subst; inversion H0; congruence.
inversion H. subst.
destruct v1; eauto with evalexpr.
Qed.
Theorem eval_conditionalexpr_true:
- forall sp le e1 m1 a1 t1 e2 m2 v1 t2 a2 e3 m3 v2 a3,
- eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 ->
+ forall sp le e m1 a1 t1 m2 v1 t2 a2 m3 v2 a3,
+ eval_expr ge sp le e m1 a1 t1 m2 v1 ->
Val.is_true v1 ->
- eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 ->
- eval_expr ge sp le e1 m1 (conditionalexpr a1 a2 a3) (t1**t2) e3 m3 v2.
+ eval_expr ge sp le e m2 a2 t2 m3 v2 ->
+ eval_expr ge sp le e m1 (conditionalexpr a1 a2 a3) (t1**t2) m3 v2.
Proof.
intros; unfold conditionalexpr.
- apply eval_Econdition with t1 e2 m2 true t2; auto.
+ apply eval_Econdition with t1 m2 true t2; auto.
eapply eval_condition_of_expr; eauto with valboolof.
Qed.
Theorem eval_conditionalexpr_false:
- forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 a3,
- eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 ->
+ forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 a3,
+ eval_expr ge sp le e m1 a1 t1 m2 v1 ->
Val.is_false v1 ->
- eval_expr ge sp le e2 m2 a3 t2 e3 m3 v2 ->
- eval_expr ge sp le e1 m1 (conditionalexpr a1 a2 a3) (t1**t2) e3 m3 v2.
+ eval_expr ge sp le e m2 a3 t2 m3 v2 ->
+ eval_expr ge sp le e m1 (conditionalexpr a1 a2 a3) (t1**t2) m3 v2.
Proof.
intros; unfold conditionalexpr.
- apply eval_Econdition with t1 e2 m2 false t2; auto.
+ apply eval_Econdition with t1 m2 false t2; auto.
eapply eval_condition_of_expr; eauto with valboolof.
Qed.
Lemma eval_addressing:
- forall sp le e1 m1 a t e2 m2 v b ofs,
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
+ forall sp le e m1 a t m2 v b ofs,
+ eval_expr ge sp le e m1 a t m2 v ->
v = Vptr b ofs ->
match addressing a with (mode, args) =>
exists vl,
- eval_exprlist ge sp le e1 m1 args t e2 m2 vl /\
+ eval_exprlist ge sp le e m1 args t m2 vl /\
eval_addressing ge sp mode vl = Some v
end.
Proof.
@@ -1151,54 +1151,54 @@ Proof.
Qed.
Theorem eval_load:
- forall sp le e1 m1 a t e2 m2 v chunk v',
- eval_expr ge sp le e1 m1 a t e2 m2 v ->
+ forall sp le e m1 a t m2 v chunk v',
+ eval_expr ge sp le e m1 a t m2 v ->
Mem.loadv chunk m2 v = Some v' ->
- eval_expr ge sp le e1 m1 (load chunk a) t e2 m2 v'.
+ eval_expr ge sp le e m1 (load chunk a) t m2 v'.
Proof.
intros. generalize H0; destruct v; simpl; intro; try discriminate.
unfold load.
- generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ _ H (refl_equal _)).
+ generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)).
destruct (addressing a). intros [vl [EV EQ]].
eapply eval_Eload; eauto.
Qed.
Theorem eval_store:
- forall sp le e1 m1 a1 t1 e2 m2 v1 a2 t2 e3 m3 v2 chunk m4,
- eval_expr ge sp le e1 m1 a1 t1 e2 m2 v1 ->
- eval_expr ge sp le e2 m2 a2 t2 e3 m3 v2 ->
+ forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 chunk m4,
+ eval_expr ge sp le e m1 a1 t1 m2 v1 ->
+ eval_expr ge sp le e m2 a2 t2 m3 v2 ->
Mem.storev chunk m3 v1 v2 = Some m4 ->
- eval_expr ge sp le e1 m1 (store chunk a1 a2) (t1**t2) e3 m4 v2.
+ eval_expr ge sp le e m1 (store chunk a1 a2) (t1**t2) m4 v2.
Proof.
intros. generalize H1; destruct v1; simpl; intro; try discriminate.
unfold store.
- generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ _ H (refl_equal _)).
+ generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)).
destruct (addressing a1). intros [vl [EV EQ]].
eapply eval_Estore; eauto.
Qed.
Theorem exec_ifthenelse_true:
- forall sp e1 m1 a t1 e2 m2 v ifso ifnot t2 e3 m3 out,
- eval_expr ge sp nil e1 m1 a t1 e2 m2 v ->
+ forall sp e m1 a t1 m2 v ifso ifnot t2 e3 m3 out,
+ eval_expr ge sp nil e m1 a t1 m2 v ->
Val.is_true v ->
- exec_stmt ge sp e2 m2 ifso t2 e3 m3 out ->
- exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out.
+ exec_stmt ge sp e m2 ifso t2 e3 m3 out ->
+ exec_stmt ge sp e m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out.
Proof.
intros. unfold ifthenelse.
- apply exec_Sifthenelse with t1 e2 m2 true t2.
+ apply exec_Sifthenelse with t1 m2 true t2.
eapply eval_condition_of_expr; eauto with valboolof.
auto. auto.
Qed.
Theorem exec_ifthenelse_false:
- forall sp e1 m1 a t1 e2 m2 v ifso ifnot t2 e3 m3 out,
- eval_expr ge sp nil e1 m1 a t1 e2 m2 v ->
+ forall sp e m1 a t1 m2 v ifso ifnot t2 e3 m3 out,
+ eval_expr ge sp nil e m1 a t1 m2 v ->
Val.is_false v ->
- exec_stmt ge sp e2 m2 ifnot t2 e3 m3 out ->
- exec_stmt ge sp e1 m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out.
+ exec_stmt ge sp e m2 ifnot t2 e3 m3 out ->
+ exec_stmt ge sp e m1 (ifthenelse a ifso ifnot) (t1**t2) e3 m3 out.
Proof.
intros. unfold ifthenelse.
- apply exec_Sifthenelse with t1 e2 m2 false t2.
+ apply exec_Sifthenelse with t1 m2 false t2.
eapply eval_condition_of_expr; eauto with valboolof.
auto. auto.
Qed.
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 6fdf602..9ed5e19 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -15,7 +15,7 @@ Require Import Globalenvs.
(** Cminor is a low-level imperative language structured in expressions,
statements, functions and programs. Expressions include
- reading and writing local variables, reading and writing store locations,
+ reading local variables, reading and writing store locations,
arithmetic operations, function calls, and conditional expressions
(similar to [e1 ? e2 : e3] in C). The [Elet] and [Eletvar] constructs
enable sharing the computations of subexpressions. De Bruijn notation
@@ -28,7 +28,6 @@ Require Import Globalenvs.
Inductive expr : Set :=
| Evar : ident -> expr
- | Eassign : ident -> expr -> expr
| Eop : operation -> exprlist -> expr
| Eload : memory_chunk -> addressing -> exprlist -> expr
| Estore : memory_chunk -> addressing -> exprlist -> expr -> expr
@@ -48,14 +47,15 @@ with exprlist : Set :=
| Enil: exprlist
| Econs: expr -> exprlist -> exprlist.
-(** Statements include expression evaluation, an if/then/else conditional,
- infinite loops, blocks and early block exits, and early function returns.
- [Sexit n] terminates prematurely the execution of the [n+1] enclosing
- [Sblock] statements. *)
+(** Statements include expression evaluation, assignment to local variables,
+ an if/then/else conditional, infinite loops, blocks and early block
+ exits, and early function returns. [Sexit n] terminates prematurely
+ the execution of the [n+1] enclosing [Sblock] statements. *)
Inductive stmt : Set :=
| Sskip: stmt
| Sexpr: expr -> stmt
+ | Sassign : ident -> expr -> stmt
| Sseq: stmt -> stmt -> stmt
| Sifthenelse: condexpr -> stmt -> stmt -> stmt
| Sloop: stmt -> stmt
@@ -154,126 +154,120 @@ Section RELSEM.
Variable ge: genv.
-(** Evaluation of an expression: [eval_expr ge sp le e m a e' m' v]
+(** Evaluation of an expression: [eval_expr ge sp le e m a m' v]
states that expression [a], in initial local environment [e] and
- memory state [m], evaluates to value [v]. [e'] and [m'] are the final
- local environment and memory state, respectively, reflecting variable
- assignments and memory stores possibly performed by [a]. [ge] and
- [le] are the global environment and let environment respectively, and
- are unchanged during evaluation. [sp] is the pointer to the memory
- block allocated for this function (stack frame).
+ memory state [m], evaluates to value [v]. [m'] is the final
+ memory state, reflecting memory stores possibly performed by [a].
+ Expressions do not assign variables, therefore the local environment
+ [e] is unchanged. [ge] and [le] are the global environment and let
+ environment respectively, and are unchanged during evaluation. [sp]
+ is the pointer to the memory block allocated for this function
+ (stack frame).
*)
Inductive eval_expr:
- val -> letenv ->
- env -> mem -> expr -> trace ->
- env -> mem -> val -> Prop :=
+ val -> letenv -> env ->
+ mem -> expr -> trace -> mem -> val -> Prop :=
| eval_Evar:
forall sp le e m id v,
PTree.get id e = Some v ->
- eval_expr sp le e m (Evar id) E0 e m v
- | eval_Eassign:
- forall sp le e m id a t e1 m1 v,
- eval_expr sp le e m a t e1 m1 v ->
- eval_expr sp le e m (Eassign id a) t (PTree.set id v e1) m1 v
+ eval_expr sp le e m (Evar id) E0 m v
| eval_Eop:
- forall sp le e m op al t e1 m1 vl v,
- eval_exprlist sp le e m al t e1 m1 vl ->
+ forall sp le e m op al t m1 vl v,
+ eval_exprlist sp le e m al t m1 vl ->
eval_operation ge sp op vl = Some v ->
- eval_expr sp le e m (Eop op al) t e1 m1 v
+ eval_expr sp le e m (Eop op al) t m1 v
| eval_Eload:
- forall sp le e m chunk addr al t e1 m1 v vl a,
- eval_exprlist sp le e m al t e1 m1 vl ->
+ forall sp le e m chunk addr al t m1 v vl a,
+ eval_exprlist sp le e m al t m1 vl ->
eval_addressing ge sp addr vl = Some a ->
Mem.loadv chunk m1 a = Some v ->
- eval_expr sp le e m (Eload chunk addr al) t e1 m1 v
+ eval_expr sp le e m (Eload chunk addr al) t m1 v
| eval_Estore:
- forall sp le e m chunk addr al b t t1 e1 m1 vl t2 e2 m2 m3 v a,
- eval_exprlist sp le e m al t1 e1 m1 vl ->
- eval_expr sp le e1 m1 b t2 e2 m2 v ->
+ forall sp le e m chunk addr al b t t1 m1 vl t2 m2 m3 v a,
+ eval_exprlist sp le e m al t1 m1 vl ->
+ eval_expr sp le e m1 b t2 m2 v ->
eval_addressing ge sp addr vl = Some a ->
Mem.storev chunk m2 a v = Some m3 ->
t = t1 ** t2 ->
- eval_expr sp le e m (Estore chunk addr al b) t e2 m3 v
+ eval_expr sp le e m (Estore chunk addr al b) t m3 v
| eval_Ecall:
- forall sp le e m sig a bl t t1 e1 m1 t2 e2 m2 t3 m3 vf vargs vres f,
- eval_expr sp le e m a t1 e1 m1 vf ->
- eval_exprlist sp le e1 m1 bl t2 e2 m2 vargs ->
+ forall sp le e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f,
+ eval_expr sp le e m a t1 m1 vf ->
+ eval_exprlist sp le e m1 bl t2 m2 vargs ->
Genv.find_funct ge vf = Some f ->
funsig f = sig ->
eval_funcall m2 f vargs t3 m3 vres ->
t = t1 ** t2 ** t3 ->
- eval_expr sp le e m (Ecall sig a bl) t e2 m3 vres
+ eval_expr sp le e m (Ecall sig a bl) t m3 vres
| eval_Econdition:
- forall sp le e m a b c t t1 e1 m1 v1 t2 e2 m2 v2,
- eval_condexpr sp le e m a t1 e1 m1 v1 ->
- eval_expr sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 ->
+ forall sp le e m a b c t t1 m1 v1 t2 m2 v2,
+ eval_condexpr sp le e m a t1 m1 v1 ->
+ eval_expr sp le e m1 (if v1 then b else c) t2 m2 v2 ->
t = t1 ** t2 ->
- eval_expr sp le e m (Econdition a b c) t e2 m2 v2
+ eval_expr sp le e m (Econdition a b c) t m2 v2
| eval_Elet:
- forall sp le e m a b t t1 e1 m1 v1 t2 e2 m2 v2,
- eval_expr sp le e m a t1 e1 m1 v1 ->
- eval_expr sp (v1::le) e1 m1 b t2 e2 m2 v2 ->
+ forall sp le e m a b t t1 m1 v1 t2 m2 v2,
+ eval_expr sp le e m a t1 m1 v1 ->
+ eval_expr sp (v1::le) e m1 b t2 m2 v2 ->
t = t1 ** t2 ->
- eval_expr sp le e m (Elet a b) t e2 m2 v2
+ eval_expr sp le e m (Elet a b) t m2 v2
| eval_Eletvar:
forall sp le e m n v,
nth_error le n = Some v ->
- eval_expr sp le e m (Eletvar n) E0 e m v
+ eval_expr sp le e m (Eletvar n) E0 m v
| eval_Ealloc:
- forall sp le e m a t e1 m1 n m2 b,
- eval_expr sp le e m a t e1 m1 (Vint n) ->
+ forall sp le e m a t m1 n m2 b,
+ eval_expr sp le e m a t m1 (Vint n) ->
Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
- eval_expr sp le e m (Ealloc a) t e1 m2 (Vptr b Int.zero)
+ eval_expr sp le e m (Ealloc a) t m2 (Vptr b Int.zero)
(** Evaluation of a condition expression:
- [eval_condexpr ge sp le e m a e' m' b]
+ [eval_condexpr ge sp le e m a m' b]
states that condition expression [a] evaluates to the boolean value [b].
The other parameters are as in [eval_expr].
*)
with eval_condexpr:
- val -> letenv ->
- env -> mem -> condexpr -> trace ->
- env -> mem -> bool -> Prop :=
+ val -> letenv -> env ->
+ mem -> condexpr -> trace -> mem -> bool -> Prop :=
| eval_CEtrue:
forall sp le e m,
- eval_condexpr sp le e m CEtrue E0 e m true
+ eval_condexpr sp le e m CEtrue E0 m true
| eval_CEfalse:
forall sp le e m,
- eval_condexpr sp le e m CEfalse E0 e m false
+ eval_condexpr sp le e m CEfalse E0 m false
| eval_CEcond:
- forall sp le e m cond al t1 e1 m1 vl b,
- eval_exprlist sp le e m al t1 e1 m1 vl ->
+ forall sp le e m cond al t1 m1 vl b,
+ eval_exprlist sp le e m al t1 m1 vl ->
eval_condition cond vl = Some b ->
- eval_condexpr sp le e m (CEcond cond al) t1 e1 m1 b
+ eval_condexpr sp le e m (CEcond cond al) t1 m1 b
| eval_CEcondition:
- forall sp le e m a b c t t1 e1 m1 vb1 t2 e2 m2 vb2,
- eval_condexpr sp le e m a t1 e1 m1 vb1 ->
- eval_condexpr sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 ->
+ forall sp le e m a b c t t1 m1 vb1 t2 m2 vb2,
+ eval_condexpr sp le e m a t1 m1 vb1 ->
+ eval_condexpr sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
t = t1 ** t2 ->
- eval_condexpr sp le e m (CEcondition a b c) t e2 m2 vb2
+ eval_condexpr sp le e m (CEcondition a b c) t m2 vb2
(** Evaluation of a list of expressions:
- [eval_exprlist ge sp le al m a e' m' vl]
+ [eval_exprlist ge sp le al m a m' vl]
states that the list [al] of expressions evaluate
to the list [vl] of values.
The other parameters are as in [eval_expr].
*)
with eval_exprlist:
- val -> letenv ->
- env -> mem -> exprlist -> trace ->
- env -> mem -> list val -> Prop :=
+ val -> letenv -> env ->
+ mem -> exprlist -> trace -> mem -> list val -> Prop :=
| eval_Enil:
forall sp le e m,
- eval_exprlist sp le e m Enil E0 e m nil
+ eval_exprlist sp le e m Enil E0 m nil
| eval_Econs:
- forall sp le e m a bl t t1 e1 m1 v t2 e2 m2 vl,
- eval_expr sp le e m a t1 e1 m1 v ->
- eval_exprlist sp le e1 m1 bl t2 e2 m2 vl ->
+ forall sp le e m a bl t t1 m1 v t2 m2 vl,
+ eval_expr sp le e m a t1 m1 v ->
+ eval_exprlist sp le e m1 bl t2 m2 vl ->
t = t1 ** t2 ->
- eval_exprlist sp le e m (Econs a bl) t e2 m2 (v :: vl)
+ eval_exprlist sp le e m (Econs a bl) t m2 (v :: vl)
(** Evaluation of a function invocation: [eval_funcall ge m f args m' res]
means that the function [f], applied to the arguments [args] in
@@ -307,13 +301,17 @@ with exec_stmt:
forall sp e m,
exec_stmt sp e m Sskip E0 e m Out_normal
| exec_Sexpr:
- forall sp e m a t e1 m1 v,
- eval_expr sp nil e m a t e1 m1 v ->
- exec_stmt sp e m (Sexpr a) t e1 m1 Out_normal
+ forall sp e m a t m1 v,
+ eval_expr sp nil e m a t m1 v ->
+ exec_stmt sp e m (Sexpr a) t e m1 Out_normal
+ | exec_Sassign:
+ forall sp e m id a t m1 v,
+ eval_expr sp nil e m a t m1 v ->
+ exec_stmt sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal
| exec_Sifthenelse:
- forall sp e m a s1 s2 t t1 e1 m1 v1 t2 e2 m2 out,
- eval_condexpr sp nil e m a t1 e1 m1 v1 ->
- exec_stmt sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out ->
+ forall sp e m a s1 s2 t t1 m1 v1 t2 e2 m2 out,
+ eval_condexpr sp nil e m a t1 m1 v1 ->
+ exec_stmt sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
t = t1 ** t2 ->
exec_stmt sp e m (Sifthenelse a s1 s2) t e2 m2 out
| exec_Sseq_continue:
@@ -346,17 +344,17 @@ with exec_stmt:
forall sp e m n,
exec_stmt sp e m (Sexit n) E0 e m (Out_exit n)
| exec_Sswitch:
- forall sp e m a cases default t1 e1 m1 n,
- eval_expr sp nil e m a t1 e1 m1 (Vint n) ->
+ forall sp e m a cases default t1 m1 n,
+ eval_expr sp nil e m a t1 m1 (Vint n) ->
exec_stmt sp e m (Sswitch a cases default)
- t1 e1 m1 (Out_exit (switch_target n default cases))
+ t1 e m1 (Out_exit (switch_target n default cases))
| exec_Sreturn_none:
forall sp e m,
exec_stmt sp e m (Sreturn None) E0 e m (Out_return None)
| exec_Sreturn_some:
- forall sp e m a t e1 m1 v,
- eval_expr sp nil e m a t e1 m1 v ->
- exec_stmt sp e m (Sreturn (Some a)) t e1 m1 (Out_return (Some v)).
+ forall sp e m a t m1 v,
+ eval_expr sp nil e m a t m1 v ->
+ exec_stmt sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)).
End RELSEM.
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index a5c3ae7..b38964d 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -10,42 +10,6 @@ Require Import Registers.
Require Import Cminor.
Require Import RTL.
-(** * Mutated variables *)
-
-(** The following functions compute the list of local Cminor variables
- possibly modified during the evaluation of the given expression.
- It is used in the [alloc_reg] function to avoid unnecessary
- register-to-register moves in the generated RTL. *)
-
-Fixpoint mutated_expr (a: expr) : list ident :=
- match a with
- | Evar id => nil
- | Eassign id b => id :: mutated_expr b
- | Eop op bl => mutated_exprlist bl
- | Eload _ _ bl => mutated_exprlist bl
- | Estore _ _ bl c => mutated_exprlist bl ++ mutated_expr c
- | Ecall _ b cl => mutated_expr b ++ mutated_exprlist cl
- | Econdition b c d => mutated_condexpr b ++ mutated_expr c ++ mutated_expr d
- | Elet b c => mutated_expr b ++ mutated_expr c
- | Eletvar n => nil
- | Ealloc b => mutated_expr b
- end
-
-with mutated_condexpr (a: condexpr) : list ident :=
- match a with
- | CEtrue => nil
- | CEfalse => nil
- | CEcond cond bl => mutated_exprlist bl
- | CEcondition b c d =>
- mutated_condexpr b ++ mutated_condexpr c ++ mutated_condexpr d
- end
-
-with mutated_exprlist (l: exprlist) : list ident :=
- match l with
- | Enil => nil
- | Econs a bl => mutated_expr a ++ mutated_exprlist bl
- end.
-
(** * Translation environments and state *)
(** The translation functions are parameterized by the following
@@ -239,37 +203,32 @@ Definition find_letvar (map: mapping) (idx: nat) : mon reg :=
(** ** Optimized temporary generation *)
-(** [alloc_reg map mut a] returns the RTL register where the evaluation
+(** [alloc_reg map a] returns the RTL register where the evaluation
of expression [a] should leave its result -- the ``target register''
for evaluating [a]. In general, this is a
fresh temporary register. Exception: if [a] is a let-bound variable
- or a non-mutated local variable, we return the RTL register associated
+ or a local variable, we return the RTL register associated
with that variable instead. Returning a fresh temporary in all cases
would be semantically correct, but would generate less efficient
RTL code. *)
-Definition alloc_reg (map: mapping) (mut: list ident) (a: expr) : mon reg :=
+Definition alloc_reg (map: mapping) (a: expr) : mon reg :=
match a with
- | Evar id =>
- if In_dec ident_eq id mut
- then new_reg
- else find_var map id
- | Eletvar n =>
- find_letvar map n
- | _ =>
- new_reg
+ | Evar id => find_var map id
+ | Eletvar n => find_letvar map n
+ | _ => new_reg
end.
(** [alloc_regs] is similar, but for a list of expressions. *)
-Fixpoint alloc_regs (map: mapping) (mut:list ident) (al: exprlist)
+Fixpoint alloc_regs (map: mapping) (al: exprlist)
{struct al}: mon (list reg) :=
match al with
| Enil =>
ret nil
| Econs a bl =>
- do rl <- alloc_regs map mut bl;
- do r <- alloc_reg map mut a;
+ do rl <- alloc_regs map bl;
+ do r <- alloc_reg map a;
ret (r :: rl)
end.
@@ -287,52 +246,46 @@ Definition add_move (rs rd: reg) (nd: node) : mon node :=
to compute the value of Cminor expression [a], leave its result
in register [rd], and branch to node [nd]. It returns the node
of the first instruction in this sequence. [map] is the compile-time
- translation environment, and [mut] is an over-approximation of
- the set of local variables possibly modified during
- the evaluation of [a]. *)
+ translation environment. *)
-Fixpoint transl_expr (map: mapping) (mut: list ident)
- (a: expr) (rd: reg) (nd: node)
+Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
{struct a}: mon node :=
match a with
| Evar v =>
do r <- find_var map v; add_move r rd nd
- | Eassign v b =>
- do r <- find_var map v;
- do no <- add_move rd r nd; transl_expr map mut b rd no
| Eop op al =>
- do rl <- alloc_regs map mut al;
+ do rl <- alloc_regs map al;
do no <- add_instr (Iop op rl rd nd);
- transl_exprlist map mut al rl no
+ transl_exprlist map al rl no
| Eload chunk addr al =>
- do rl <- alloc_regs map mut al;
+ do rl <- alloc_regs map al;
do no <- add_instr (Iload chunk addr rl rd nd);
- transl_exprlist map mut al rl no
+ transl_exprlist map al rl no
| Estore chunk addr al b =>
- do rl <- alloc_regs map mut al;
+ do rl <- alloc_regs map al;
do no <- add_instr (Istore chunk addr rl rd nd);
- do ns <- transl_expr map mut b rd no;
- transl_exprlist map mut al rl ns
+ do ns <- transl_expr map b rd no;
+ transl_exprlist map al rl ns
| Ecall sig b cl =>
- do rf <- alloc_reg map mut b;
- do rargs <- alloc_regs map mut cl;
+ do rf <- alloc_reg map b;
+ do rargs <- alloc_regs map cl;
do n1 <- add_instr (Icall sig (inl _ rf) rargs rd nd);
- do n2 <- transl_exprlist map mut cl rargs n1;
- transl_expr map mut b rf n2
+ do n2 <- transl_exprlist map cl rargs n1;
+ transl_expr map b rf n2
| Econdition b c d =>
- do nfalse <- transl_expr map mut d rd nd;
- do ntrue <- transl_expr map mut c rd nd;
- transl_condition map mut b ntrue nfalse
+ do nfalse <- transl_expr map d rd nd;
+ do ntrue <- transl_expr map c rd nd;
+ transl_condition map b ntrue nfalse
| Elet b c =>
do r <- new_reg;
- do nc <- transl_expr (add_letvar map r) mut c rd nd;
- transl_expr map mut b r nc
+ do nc <- transl_expr (add_letvar map r) c rd nd;
+ transl_expr map b r nc
| Eletvar n =>
do r <- find_letvar map n; add_move r rd nd
| Ealloc a =>
- do r <- alloc_reg map mut a;
+ do r <- alloc_reg map a;
do no <- add_instr (Ialloc r rd nd);
- transl_expr map mut a r no
+ transl_expr map a r no
end
(** Translation of a conditional expression. Similar to [transl_expr],
@@ -340,8 +293,7 @@ Fixpoint transl_expr (map: mapping) (mut: list ident)
code branches to one of two possible continuation nodes [ntrue] or
[nfalse] depending on the truth value of [a]. *)
-with transl_condition (map: mapping) (mut: list ident)
- (a: condexpr) (ntrue nfalse: node)
+with transl_condition (map: mapping) (a: condexpr) (ntrue nfalse: node)
{struct a}: mon node :=
match a with
| CEtrue =>
@@ -349,26 +301,25 @@ with transl_condition (map: mapping) (mut: list ident)
| CEfalse =>
ret nfalse
| CEcond cond bl =>
- do rl <- alloc_regs map mut bl;
+ do rl <- alloc_regs map bl;
do nt <- add_instr (Icond cond rl ntrue nfalse);
- transl_exprlist map mut bl rl nt
+ transl_exprlist map bl rl nt
| CEcondition b c d =>
- do nd <- transl_condition map mut d ntrue nfalse;
- do nc <- transl_condition map mut c ntrue nfalse;
- transl_condition map mut b nc nd
+ do nd <- transl_condition map d ntrue nfalse;
+ do nc <- transl_condition map c ntrue nfalse;
+ transl_condition map b nc nd
end
(** Translation of a list of expressions. The expressions are evaluated
left-to-right, and their values left in the given list of registers. *)
-with transl_exprlist (map: mapping) (mut: list ident)
- (al: exprlist) (rl: list reg) (nd: node)
+with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
{struct al} : mon node :=
match al, rl with
| Enil, nil =>
ret nd
| Econs b bs, r :: rs =>
- do no <- transl_exprlist map mut bs rs nd; transl_expr map mut b r no
+ do no <- transl_exprlist map bs rs nd; transl_expr map b r no
| _, _ =>
error node
end.
@@ -419,21 +370,24 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
| Sskip =>
ret nd
| Sexpr a =>
- let mut := mutated_expr a in
- do r <- alloc_reg map mut a; transl_expr map mut a r nd
+ do r <- alloc_reg map a; transl_expr map a r nd
+ | Sassign v b =>
+ do rv <- find_var map v;
+ do rt <- alloc_reg map b;
+ do no <- add_move rt rv nd;
+ transl_expr map b rt no
| Sseq s1 s2 =>
do ns <- transl_stmt map s2 nd nexits nret rret;
transl_stmt map s1 ns nexits nret rret
| Sifthenelse a strue sfalse =>
- let mut := mutated_condexpr a in
- (if more_likely a strue sfalse then
+ if more_likely a strue sfalse then
do nfalse <- transl_stmt map sfalse nd nexits nret rret;
do ntrue <- transl_stmt map strue nd nexits nret rret;
- transl_condition map mut a ntrue nfalse
- else
+ transl_condition map a ntrue nfalse
+ else
do ntrue <- transl_stmt map strue nd nexits nret rret;
do nfalse <- transl_stmt map sfalse nd nexits nret rret;
- transl_condition map mut a ntrue nfalse)
+ transl_condition map a ntrue nfalse
| Sloop sbody =>
do nloop <- reserve_instr;
do nbody <- transl_stmt map sbody nloop nexits nret rret;
@@ -444,14 +398,13 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
| Sexit n =>
transl_exit nexits n
| Sswitch a cases default =>
- let mut := mutated_expr a in
- do r <- alloc_reg map mut a;
+ do r <- alloc_reg map a;
do ns <- transl_switch r nexits cases default;
- transl_expr map mut a r ns
+ transl_expr map a r ns
| Sreturn opt_a =>
match opt_a, rret with
| None, None => ret nret
- | Some a, Some r => transl_expr map (mutated_expr a) a r nret
+ | Some a, Some r => transl_expr map a r nret
| _, _ => error node
end
end.
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 24cc41b..2ce961b 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -133,57 +133,48 @@ Qed.
Definition transl_expr_correct
(sp: val) (le: letenv) (e: env) (m: mem) (a: expr)
- (t: trace) (e': env) (m': mem) (v: val) : Prop :=
- forall map mut rd nd s ns s' rs
+ (t: trace) (m': mem) (v: val) : Prop :=
+ forall map rd nd s ns s' rs
(MWF: map_wf map s)
- (TE: transl_expr map mut a rd nd s = OK ns s')
+ (TE: transl_expr map a rd nd s = OK ns s')
(ME: match_env map e le rs)
- (MUT: incl (mutated_expr a) mut)
- (TRG: target_reg_ok s map mut a rd),
+ (TRG: target_reg_ok s map a rd),
exists rs',
exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
- /\ match_env map e' le rs'
+ /\ match_env map e le rs'
/\ rs'#rd = v
/\ (forall r,
- reg_valid r s -> ~(mutated_reg map mut r) ->
- reg_in_map map r \/ r <> rd ->
- rs'#r = rs#r).
+ reg_valid r s -> reg_in_map map r \/ r <> rd -> rs'#r = rs#r).
(** The simulation properties for lists of expressions and for
conditional expressions are similar. *)
Definition transl_exprlist_correct
(sp: val) (le: letenv) (e: env) (m: mem) (al: exprlist)
- (t: trace) (e': env) (m': mem) (vl: list val) : Prop :=
- forall map mut rl nd s ns s' rs
+ (t: trace) (m': mem) (vl: list val) : Prop :=
+ forall map rl nd s ns s' rs
(MWF: map_wf map s)
- (TE: transl_exprlist map mut al rl nd s = OK ns s')
+ (TE: transl_exprlist map al rl nd s = OK ns s')
(ME: match_env map e le rs)
- (MUT: incl (mutated_exprlist al) mut)
- (TRG: target_regs_ok s map mut al rl),
+ (TRG: target_regs_ok s map al rl),
exists rs',
exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
- /\ match_env map e' le rs'
+ /\ match_env map e le rs'
/\ rs'##rl = vl
/\ (forall r,
- reg_valid r s -> ~(mutated_reg map mut r) ->
- reg_in_map map r \/ ~(In r rl) ->
- rs'#r = rs#r).
+ reg_valid r s -> reg_in_map map r \/ ~(In r rl) -> rs'#r = rs#r).
Definition transl_condition_correct
(sp: val) (le: letenv) (e: env) (m: mem) (a: condexpr)
- (t: trace) (e': env) (m': mem) (vb: bool) : Prop :=
- forall map mut ntrue nfalse s ns s' rs
+ (t: trace) (m': mem) (vb: bool) : Prop :=
+ forall map ntrue nfalse s ns s' rs
(MWF: map_wf map s)
- (TE: transl_condition map mut a ntrue nfalse s = OK ns s')
- (ME: match_env map e le rs)
- (MUT: incl (mutated_condexpr a) mut),
+ (TE: transl_condition map a ntrue nfalse s = OK ns s')
+ (ME: match_env map e le rs),
exists rs',
exec_instrs tge s'.(st_code) sp ns rs m t (if vb then ntrue else nfalse) rs' m'
- /\ match_env map e' le rs'
- /\ (forall r,
- reg_valid r s -> ~(mutated_reg map mut r) ->
- rs'#r = rs#r).
+ /\ match_env map e le rs'
+ /\ (forall r, reg_valid r s -> rs'#r = rs#r).
(** For statements, we define the following auxiliary predicates
relating the outcome of the Cminor execution with the final node
@@ -283,7 +274,7 @@ Definition transl_function_correct
Lemma transl_expr_Evar_correct:
forall (sp: val) (le: letenv) (e: env) (m: mem) (id: ident) (v: val),
e!id = Some v ->
- transl_expr_correct sp le e m (Evar id) E0 e m v.
+ transl_expr_correct sp le e m (Evar id) E0 m v.
Proof.
intros; red; intros. monadInv TE. intro.
generalize EQ; unfold find_var. caseEq (map_vars map)!id.
@@ -294,43 +285,40 @@ Proof.
(* Exec *)
split. assumption.
(* Match-env *)
- split. inversion TRG.
+ split. inversion TRG; subst.
(* Optimized case rd = r *)
- rewrite MV in H5; injection H5; intro; subst r.
+ rewrite MV in H3; injection H3; intro; subst r.
apply match_env_exten with rs.
intros. case (Reg.eq r rd); intro.
subst r; assumption. apply OTHER1; assumption.
assumption.
(* General case rd is temp *)
apply match_env_invariant with rs.
- assumption. intros. apply OTHER1. red; intro; subst r1. contradiction.
+ assumption. intros. apply OTHER1. congruence.
(* Result value *)
split. rewrite RES1. eauto with rtlg.
(* Other regs *)
- intros. case (Reg.eq rd r0); intro.
- subst r0. inversion TRG.
- rewrite MV in H8; injection H8; intro; subst r. apply RES1.
- byContradiction. tauto.
- apply OTHER1; auto.
+ intros. destruct (Reg.eq rd r0).
+ subst r0. inversion TRG; subst.
+ congruence.
+ byContradiction. tauto.
+ auto.
intro; monadSimpl.
Qed.
Lemma transl_expr_Eop_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation)
- (al : exprlist) (t: trace) (e1 : env) (m1 : mem) (vl : list val)
+ (al : exprlist) (t: trace) (m1 : mem) (vl : list val)
(v: val),
- eval_exprlist ge sp le e m al t e1 m1 vl ->
- transl_exprlist_correct sp le e m al t e1 m1 vl ->
+ eval_exprlist ge sp le e m al t m1 vl ->
+ transl_exprlist_correct sp le e m al t m1 vl ->
eval_operation ge sp op vl = Some v ->
- transl_expr_correct sp le e m (Eop op al) t e1 m1 v.
+ transl_expr_correct sp le e m (Eop op al) t m1 v.
Proof.
intros until v. intros EEL TEL EOP. red; intros.
simpl in TE. monadInv TE. intro EQ1.
- simpl in MUT.
- assert (TRG': target_regs_ok s1 map mut al l); eauto with rtlg.
- assert (MWF': map_wf map s1). eauto with rtlg.
- generalize (TEL _ _ _ _ _ _ _ _ MWF' EQ1 ME MUT TRG').
+ exploit TEL. 2: eauto. eauto with rtlg. eauto. eauto with rtlg.
intros [rs1 [EX1 [ME1 [RR1 RO1]]]].
exists (rs1#rd <- v).
(* Exec *)
@@ -347,74 +335,31 @@ Proof.
split. apply Regmap.gss.
(* Other regs *)
intros. rewrite Regmap.gso.
- apply RO1. eauto with rtlg. assumption.
- case (In_dec Reg.eq r l); intro.
- left. elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro.
- assumption. byContradiction; eauto with rtlg.
- right; assumption.
+ apply RO1. eauto with rtlg.
+ destruct (In_dec Reg.eq r l).
+ left. elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro.
+ auto. byContradiction; eauto with rtlg.
+ right; auto.
red; intro; subst r.
- elim H1; intro. inversion TRG. contradiction.
+ elim H0; intro. inversion TRG. contradiction.
tauto.
Qed.
-Lemma transl_expr_Eassign_correct:
- forall (sp: val) (le : letenv) (e : env) (m : mem)
- (id : ident) (a : expr) (t: trace) (e1 : env) (m1 : mem)
- (v : val),
- eval_expr ge sp le e m a t e1 m1 v ->
- transl_expr_correct sp le e m a t e1 m1 v ->
- transl_expr_correct sp le e m (Eassign id a) t (PTree.set id v e1) m1 v.
-Proof.
- intros; red; intros.
- simpl in TE. monadInv TE. intro EQ1.
- simpl in MUT.
- assert (MWF0: map_wf map s1). eauto with rtlg.
- assert (MUTa: incl (mutated_expr a) mut).
- red. intros. apply MUT. simpl. tauto.
- assert (TRGa: target_reg_ok s1 map mut a rd).
- inversion TRG. apply target_reg_other; eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME MUTa TRGa).
- intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
- generalize (add_move_correct _ _ sp _ _ _ _ rs1 m1 EQ0).
- intros [rs2 [EX2 [RES2 OTHER2]]].
- exists rs2.
-(* Exec *)
- split. eapply exec_trans. eexact EX1.
- apply exec_instrs_incr with s1. eauto with rtlg.
- eexact EX2. traceEq.
-(* Match-env *)
- split.
- apply match_env_update_var with rs1 r s s0; auto.
- congruence.
-(* Result *)
- split. case (Reg.eq rd r); intro.
- subst r. congruence.
- rewrite OTHER2; auto.
-(* Other regs *)
- intros. transitivity (rs1#r0).
- apply OTHER2. red; intro; subst r0.
- apply H2. red. exists id. split. apply MUT. red; tauto.
- generalize EQ; unfold find_var.
- destruct ((map_vars map)!id); monadSimpl. congruence.
- apply OTHER1. eauto with rtlg. assumption. assumption.
-Qed.
-
Lemma transl_expr_Eload_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
(chunk : memory_chunk) (addr : addressing)
- (al : exprlist) (t: trace) (e1 : env) (m1 : mem) (v : val)
+ (al : exprlist) (t: trace) (m1 : mem) (v : val)
(vl : list val) (a: val),
- eval_exprlist ge sp le e m al t e1 m1 vl ->
- transl_exprlist_correct sp le e m al t e1 m1 vl ->
+ eval_exprlist ge sp le e m al t m1 vl ->
+ transl_exprlist_correct sp le e m al t m1 vl ->
eval_addressing ge sp addr vl = Some a ->
Mem.loadv chunk m1 a = Some v ->
- transl_expr_correct sp le e m (Eload chunk addr al) t e1 m1 v.
+ transl_expr_correct sp le e m (Eload chunk addr al) t m1 v.
Proof.
intros; red; intros. simpl in TE. monadInv TE. intro EQ1. clear TE.
- simpl in MUT.
assert (MWF1: map_wf map s1). eauto with rtlg.
- assert (TRG1: target_regs_ok s1 map mut al l). eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT TRG1).
+ assert (TRG1: target_regs_ok s1 map al l). eauto with rtlg.
+ generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
exists (rs1#rd <- v).
(* Exec *)
@@ -429,9 +374,9 @@ Proof.
split. apply Regmap.gss.
(* Other regs *)
intros. rewrite Regmap.gso. apply OTHER1.
- eauto with rtlg. assumption.
+ eauto with rtlg.
case (In_dec Reg.eq r l); intro.
- elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro.
+ elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro.
tauto. byContradiction. eauto with rtlg.
tauto.
red; intro; subst r. inversion TRG. tauto.
@@ -440,34 +385,31 @@ Qed.
Lemma transl_expr_Estore_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
(chunk : memory_chunk) (addr : addressing)
- (al : exprlist) (b : expr) (t t1: trace) (e1 : env) (m1 : mem)
- (vl : list val) (t2: trace) (e2 : env) (m2 m3 : mem)
+ (al : exprlist) (b : expr) (t t1: trace) (m1 : mem)
+ (vl : list val) (t2: trace) (m2 m3 : mem)
(v : val) (a: val),
- eval_exprlist ge sp le e m al t1 e1 m1 vl ->
- transl_exprlist_correct sp le e m al t1 e1 m1 vl ->
- eval_expr ge sp le e1 m1 b t2 e2 m2 v ->
- transl_expr_correct sp le e1 m1 b t2 e2 m2 v ->
+ eval_exprlist ge sp le e m al t1 m1 vl ->
+ transl_exprlist_correct sp le e m al t1 m1 vl ->
+ eval_expr ge sp le e m1 b t2 m2 v ->
+ transl_expr_correct sp le e m1 b t2 m2 v ->
eval_addressing ge sp addr vl = Some a ->
Mem.storev chunk m2 a v = Some m3 ->
t = t1 ** t2 ->
- transl_expr_correct sp le e m (Estore chunk addr al b) t e2 m3 v.
+ transl_expr_correct sp le e m (Estore chunk addr al b) t m3 v.
Proof.
intros; red; intros. simpl in TE; monadInv TE. intro EQ2; clear TE.
- simpl in MUT.
assert (MWF2: map_wf map s2).
apply map_wf_incr with s.
apply state_incr_trans2 with s0 s1; eauto with rtlg.
assumption.
- assert (MUT2: incl (mutated_exprlist al) mut). eauto with coqlib.
- assert (TRG2: target_regs_ok s2 map mut al l).
+ assert (TRG2: target_regs_ok s2 map al l).
apply target_regs_ok_incr with s0; eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWF2 EQ2 ME MUT2 TRG2).
+ generalize (H0 _ _ _ _ _ _ _ MWF2 EQ2 ME TRG2).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
assert (MWF1: map_wf map s1). eauto with rtlg.
- assert (MUT1: incl (mutated_expr b) mut). eauto with coqlib.
- assert (TRG1: target_reg_ok s1 map mut b rd).
+ assert (TRG1: target_reg_ok s1 map b rd).
inversion TRG. apply target_reg_other; eauto with rtlg.
- generalize (H2 _ _ _ _ _ _ _ _ MWF1 EQ1 ME1 MUT1 TRG1).
+ generalize (H2 _ _ _ _ _ _ _ MWF1 EQ1 ME1 TRG1).
intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
exists rs2.
(* Exec *)
@@ -479,7 +421,7 @@ Proof.
assert (rs2##l = rs1##l).
apply list_map_exten. intros r' IN. symmetry. apply OTHER2.
eauto with rtlg. eauto with rtlg.
- elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r' IN); intro.
+ elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r' IN); intro.
tauto. right. apply sym_not_equal.
apply valid_fresh_different with s. inversion TRG; assumption.
assumption.
@@ -495,55 +437,53 @@ Proof.
(* Other regs *)
intro r'; intros. transitivity (rs1#r').
apply OTHER2. apply reg_valid_incr with s; eauto with rtlg.
- assumption. assumption.
+ assumption.
apply OTHER1. apply reg_valid_incr with s.
apply state_incr_trans2 with s0 s1; eauto with rtlg. assumption.
- assumption. case (In_dec Reg.eq r' l); intro.
- elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r' i); intro.
+ case (In_dec Reg.eq r' l); intro.
+ elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r' i); intro.
tauto. byContradiction; eauto with rtlg. tauto.
Qed.
Lemma transl_expr_Ecall_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
(sig : signature) (a : expr) (bl : exprlist) (t t1: trace)
- (e1: env) (m1: mem) (t2: trace) (e2 : env) (m2 : mem)
+ (m1: mem) (t2: trace) (m2 : mem)
(t3: trace) (m3: mem) (vf : val)
(vargs : list val) (vres : val) (f : Cminor.fundef),
- eval_expr ge sp le e m a t1 e1 m1 vf ->
- transl_expr_correct sp le e m a t1 e1 m1 vf ->
- eval_exprlist ge sp le e1 m1 bl t2 e2 m2 vargs ->
- transl_exprlist_correct sp le e1 m1 bl t2 e2 m2 vargs ->
+ eval_expr ge sp le e m a t1 m1 vf ->
+ transl_expr_correct sp le e m a t1 m1 vf ->
+ eval_exprlist ge sp le e m1 bl t2 m2 vargs ->
+ transl_exprlist_correct sp le e m1 bl t2 m2 vargs ->
Genv.find_funct ge vf = Some f ->
Cminor.funsig f = sig ->
eval_funcall ge m2 f vargs t3 m3 vres ->
transl_function_correct m2 f vargs t3 m3 vres ->
t = t1 ** t2 ** t3 ->
- transl_expr_correct sp le e m (Ecall sig a bl) t e2 m3 vres.
+ transl_expr_correct sp le e m (Ecall sig a bl) t m3 vres.
Proof.
intros. red; simpl; intros.
monadInv TE. intro EQ3. clear TE.
- assert (MUTa: incl (mutated_expr a) mut). eauto with coqlib.
- assert (MUTbl: incl (mutated_exprlist bl) mut). eauto with coqlib.
assert (MWFa: map_wf map s3).
apply map_wf_incr with s.
apply state_incr_trans3 with s0 s1 s2; eauto with rtlg.
assumption.
- assert (TRGr: target_reg_ok s3 map mut a r).
+ assert (TRGr: target_reg_ok s3 map a r).
apply target_reg_ok_incr with s0.
apply state_incr_trans2 with s1 s2; eauto with rtlg.
eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWFa EQ3 ME MUTa TRGr).
+ generalize (H0 _ _ _ _ _ _ _ MWFa EQ3 ME TRGr).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
- clear MUTa MWFa TRGr.
+ clear MWFa TRGr.
assert (MWFbl: map_wf map s2).
apply map_wf_incr with s.
apply state_incr_trans2 with s0 s1; eauto with rtlg.
assumption.
- assert (TRGl: target_regs_ok s2 map mut bl l).
+ assert (TRGl: target_regs_ok s2 map bl l).
apply target_regs_ok_incr with s1; eauto with rtlg.
- generalize (H2 _ _ _ _ _ _ _ _ MWFbl EQ2 ME1 MUTbl TRGl).
+ generalize (H2 _ _ _ _ _ _ _ MWFbl EQ2 ME1 TRGl).
intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
- clear MUTbl MWFbl TRGl.
+ clear MWFbl TRGl.
generalize (functions_translated vf f H3). intros [tf [TFIND TF]].
generalize (H6 tf TF). intro EXF.
@@ -554,11 +494,9 @@ Proof.
eauto with rtlg. simpl. replace (rs2#r) with vf. eexact TFIND.
rewrite <- RES1. symmetry. apply OTHER2.
apply reg_valid_incr with s0; eauto with rtlg.
- apply target_reg_not_mutated with s0 a.
- eauto with rtlg. eauto with rtlg.
assert (MWFs0: map_wf map s0). eauto with rtlg.
case (In_dec Reg.eq r l); intro.
- elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWFs0 EQ0 r i); intro.
+ elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWFs0 EQ0 r i); intro.
tauto. byContradiction. apply valid_fresh_absurd with r s0.
eauto with rtlg. assumption.
tauto.
@@ -584,10 +522,9 @@ Proof.
apply reg_valid_incr with s.
apply state_incr_trans2 with s0 s1; eauto with rtlg.
assumption.
- assumption.
assert (MWFs0: map_wf map s0). eauto with rtlg.
case (In_dec Reg.eq r0 l); intro.
- elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWFs0 EQ0 r0 i); intro.
+ elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWFs0 EQ0 r0 i); intro.
tauto. byContradiction. apply valid_fresh_absurd with r0 s0.
eauto with rtlg. assumption.
tauto.
@@ -595,10 +532,9 @@ Proof.
apply reg_valid_incr with s.
apply state_incr_trans3 with s0 s1 s2; eauto with rtlg.
assumption.
- assumption.
case (Reg.eq r0 r); intro.
subst r0.
- elim (alloc_reg_fresh_or_in_map _ _ _ _ _ _ MWF EQ); intro.
+ elim (alloc_reg_fresh_or_in_map _ _ _ _ _ MWF EQ); intro.
tauto. byContradiction; eauto with rtlg.
tauto.
red; intro; subst r0.
@@ -607,30 +543,27 @@ Qed.
Lemma transl_expr_Econdition_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
- (a : condexpr) (b c : expr) (t t1: trace) (e1 : env) (m1 : mem)
- (v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (v2 : val),
- eval_condexpr ge sp le e m a t1 e1 m1 v1 ->
- transl_condition_correct sp le e m a t1 e1 m1 v1 ->
- eval_expr ge sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 ->
- transl_expr_correct sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 ->
+ (a : condexpr) (b c : expr) (t t1: trace) (m1 : mem)
+ (v1 : bool) (t2: trace) (m2 : mem) (v2 : val),
+ eval_condexpr ge sp le e m a t1 m1 v1 ->
+ transl_condition_correct sp le e m a t1 m1 v1 ->
+ eval_expr ge sp le e m1 (if v1 then b else c) t2 m2 v2 ->
+ transl_expr_correct sp le e m1 (if v1 then b else c) t2 m2 v2 ->
t = t1 ** t2 ->
- transl_expr_correct sp le e m (Econdition a b c) t e2 m2 v2.
+ transl_expr_correct sp le e m (Econdition a b c) t m2 v2.
Proof.
intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
- simpl in MUT.
assert (MWF1: map_wf map s1).
apply map_wf_incr with s. eauto with rtlg. assumption.
- assert (MUT1: incl (mutated_condexpr a) mut). eauto with coqlib.
- generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1).
+ generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME).
intros [rs1 [EX1 [ME1 OTHER1]]].
destruct v1.
assert (MWF0: map_wf map s0). eauto with rtlg.
- assert (MUT0: incl (mutated_expr b) mut). eauto with coqlib.
- assert (TRG0: target_reg_ok s0 map mut b rd).
+ assert (TRG0: target_reg_ok s0 map b rd).
inversion TRG. apply target_reg_other; eauto with rtlg.
- generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUT0 TRG0).
+ generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1 TRG0).
intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
exists rs2.
(* Exec *)
@@ -647,10 +580,9 @@ Proof.
apply OTHER1; auto. apply reg_valid_incr with s.
apply state_incr_trans with s0; eauto with rtlg. assumption.
- assert (MUTc: incl (mutated_expr c) mut). eauto with coqlib.
- assert (TRGc: target_reg_ok s map mut c rd).
+ assert (TRGc: target_reg_ok s map c rd).
inversion TRG. apply target_reg_other; auto.
- generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc TRGc).
+ generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 TRGc).
intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
exists rs2.
(* Exec *)
@@ -670,38 +602,35 @@ Qed.
Lemma transl_expr_Elet_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
- (a b : expr) (t t1: trace) (e1 : env) (m1 : mem) (v1 : val)
- (t2: trace) (e2 : env) (m2 : mem) (v2 : val),
- eval_expr ge sp le e m a t1 e1 m1 v1 ->
- transl_expr_correct sp le e m a t1 e1 m1 v1 ->
- eval_expr ge sp (v1 :: le) e1 m1 b t2 e2 m2 v2 ->
- transl_expr_correct sp (v1 :: le) e1 m1 b t2 e2 m2 v2 ->
+ (a b : expr) (t t1: trace) (m1 : mem) (v1 : val)
+ (t2: trace) (m2 : mem) (v2 : val),
+ eval_expr ge sp le e m a t1 m1 v1 ->
+ transl_expr_correct sp le e m a t1 m1 v1 ->
+ eval_expr ge sp (v1 :: le) e m1 b t2 m2 v2 ->
+ transl_expr_correct sp (v1 :: le) e m1 b t2 m2 v2 ->
t = t1 ** t2 ->
- transl_expr_correct sp le e m (Elet a b) t e2 m2 v2.
+ transl_expr_correct sp le e m (Elet a b) t m2 v2.
Proof.
intros; red; intros.
simpl in TE; monadInv TE. intro EQ1.
- simpl in MUT.
assert (MWF1: map_wf map s1). eauto with rtlg.
- assert (MUT1: incl (mutated_expr a) mut). eauto with coqlib.
- assert (TRG1: target_reg_ok s1 map mut a r).
+ assert (TRG1: target_reg_ok s1 map a r).
eapply target_reg_other; eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1).
+ generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
assert (MWF2: map_wf (add_letvar map r) s0).
apply add_letvar_wf; eauto with rtlg.
- assert (MUT2: incl (mutated_expr b) mut). eauto with coqlib.
- assert (ME2: match_env (add_letvar map r) e1 (v1 :: le) rs1).
+ assert (ME2: match_env (add_letvar map r) e (v1 :: le) rs1).
apply match_env_letvar; assumption.
- assert (TRG2: target_reg_ok s0 (add_letvar map r) mut b rd).
+ assert (TRG2: target_reg_ok s0 (add_letvar map r) b rd).
inversion TRG. apply target_reg_other.
unfold reg_in_map, add_letvar; simpl. red; intro.
- elim H11; intro. apply H4. left. assumption.
- elim H12; intro. apply valid_fresh_absurd with rd s.
- assumption. rewrite <- H13. eauto with rtlg.
+ elim H10; intro. apply H4. left. assumption.
+ elim H11; intro. apply valid_fresh_absurd with rd s.
+ assumption. rewrite <- H12. eauto with rtlg.
apply H4. right. assumption.
eauto with rtlg.
- generalize (H2 _ _ _ _ _ _ _ _ MWF2 EQ0 ME2 MUT2 TRG2).
+ generalize (H2 _ _ _ _ _ _ _ MWF2 EQ0 ME2 TRG2).
intros [rs2 [EX2 [ME3 [RES2 OTHER2]]]].
exists rs2.
(* Exec *)
@@ -716,22 +645,20 @@ Proof.
(* Other regs *)
intros. transitivity (rs1#r0).
apply OTHER2. eauto with rtlg.
- unfold mutated_reg. unfold add_letvar; simpl. assumption.
- elim H6; intro. left.
+ elim H5; intro. left.
unfold reg_in_map, add_letvar; simpl.
- unfold reg_in_map in H7; tauto.
+ unfold reg_in_map in H6; tauto.
tauto.
apply OTHER1. eauto with rtlg.
- assumption.
right. red; intro. apply valid_fresh_absurd with r0 s.
- assumption. rewrite H7. eauto with rtlg.
+ assumption. rewrite H6. eauto with rtlg.
Qed.
Lemma transl_expr_Eletvar_correct:
forall (sp: val) (le : list val) (e : env)
(m : mem) (n : nat) (v : val),
nth_error le n = Some v ->
- transl_expr_correct sp le e m (Eletvar n) E0 e m v.
+ transl_expr_correct sp le e m (Eletvar n) E0 m v.
Proof.
intros; red; intros.
simpl in TE; monadInv TE. intro EQ1.
@@ -766,19 +693,18 @@ Qed.
Lemma transl_expr_Ealloc_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
- (a : expr) (t: trace) (e1 : env) (m1 : mem) (n: int)
+ (a : expr) (t: trace) (m1 : mem) (n: int)
(m2: mem) (b: block),
- eval_expr ge sp le e m a t e1 m1 (Vint n) ->
- transl_expr_correct sp le e m a t e1 m1 (Vint n) ->
+ eval_expr ge sp le e m a t m1 (Vint n) ->
+ transl_expr_correct sp le e m a t m1 (Vint n) ->
Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
- transl_expr_correct sp le e m (Ealloc a) t e1 m2 (Vptr b Int.zero).
+ transl_expr_correct sp le e m (Ealloc a) t m2 (Vptr b Int.zero).
Proof.
intros until b; intros EE TEC ALLOC; red; intros.
simpl in TE. monadInv TE. intro EQ1.
- simpl in MUT.
- assert (TRG': target_reg_ok s1 map mut a r); eauto with rtlg.
+ assert (TRG': target_reg_ok s1 map a r); eauto with rtlg.
assert (MWF': map_wf map s1). eauto with rtlg.
- generalize (TEC _ _ _ _ _ _ _ _ MWF' EQ1 ME MUT TRG').
+ generalize (TEC _ _ _ _ _ _ _ MWF' EQ1 ME TRG').
intros [rs1 [EX1 [ME1 [RR1 RO1]]]].
exists (rs1#rd <- (Vptr b Int.zero)).
(* Exec *)
@@ -792,18 +718,18 @@ Proof.
split. apply Regmap.gss.
(* Other regs *)
intros. rewrite Regmap.gso.
- apply RO1. eauto with rtlg. assumption.
+ apply RO1. eauto with rtlg.
case (Reg.eq r0 r); intro.
- subst r0. left. elim (alloc_reg_fresh_or_in_map _ _ _ _ _ _ MWF EQ); intro.
+ subst r0. left. elim (alloc_reg_fresh_or_in_map _ _ _ _ _ MWF EQ); intro.
auto. byContradiction; eauto with rtlg.
right; assumption.
- elim H1; intro. red; intro. subst r0. inversion TRG. contradiction.
+ elim H0; intro. red; intro. subst r0. inversion TRG. contradiction.
auto.
Qed.
Lemma transl_condition_CEtrue_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem),
- transl_condition_correct sp le e m CEtrue E0 e m true.
+ transl_condition_correct sp le e m CEtrue E0 m true.
Proof.
intros; red; intros. simpl in TE; monadInv TE. subst ns.
exists rs. split. apply exec_refl. split. auto. auto.
@@ -811,7 +737,7 @@ Qed.
Lemma transl_condition_CEfalse_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem),
- transl_condition_correct sp le e m CEfalse E0 e m false.
+ transl_condition_correct sp le e m CEfalse E0 m false.
Proof.
intros; red; intros. simpl in TE; monadInv TE. subst ns.
exists rs. split. apply exec_refl. split. auto. auto.
@@ -819,19 +745,17 @@ Qed.
Lemma transl_condition_CEcond_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
- (cond : condition) (al : exprlist) (t1: trace) (e1 : env)
+ (cond : condition) (al : exprlist) (t1: trace)
(m1 : mem) (vl : list val) (b : bool),
- eval_exprlist ge sp le e m al t1 e1 m1 vl ->
- transl_exprlist_correct sp le e m al t1 e1 m1 vl ->
+ eval_exprlist ge sp le e m al t1 m1 vl ->
+ transl_exprlist_correct sp le e m al t1 m1 vl ->
eval_condition cond vl = Some b ->
- transl_condition_correct sp le e m (CEcond cond al) t1 e1 m1 b.
+ transl_condition_correct sp le e m (CEcond cond al) t1 m1 b.
Proof.
intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
assert (MWF1: map_wf map s1). eauto with rtlg.
- simpl in MUT.
- assert (TRG: target_regs_ok s1 map mut al l).
- eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT TRG).
+ assert (TRG: target_regs_ok s1 map al l). eauto with rtlg.
+ generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
exists rs1.
(* Exec *)
@@ -847,35 +771,32 @@ Proof.
(* Match-env *)
split. assumption.
(* Regs *)
- intros. apply OTHER1. eauto with rtlg. assumption.
+ intros. apply OTHER1. eauto with rtlg.
case (In_dec Reg.eq r l); intro.
- elim (alloc_regs_fresh_or_in_map _ _ _ _ _ _ MWF EQ r i); intro.
+ elim (alloc_regs_fresh_or_in_map _ _ _ _ _ MWF EQ r i); intro.
tauto. byContradiction; eauto with rtlg.
tauto.
Qed.
Lemma transl_condition_CEcondition_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
- (a b c : condexpr) (t t1: trace) (e1 : env) (m1 : mem)
- (vb1 : bool) (t2: trace) (e2 : env) (m2 : mem) (vb2 : bool),
- eval_condexpr ge sp le e m a t1 e1 m1 vb1 ->
- transl_condition_correct sp le e m a t1 e1 m1 vb1 ->
- eval_condexpr ge sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 ->
- transl_condition_correct sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 ->
+ (a b c : condexpr) (t t1: trace) (m1 : mem)
+ (vb1 : bool) (t2: trace) (m2 : mem) (vb2 : bool),
+ eval_condexpr ge sp le e m a t1 m1 vb1 ->
+ transl_condition_correct sp le e m a t1 m1 vb1 ->
+ eval_condexpr ge sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
+ transl_condition_correct sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
t = t1 ** t2 ->
- transl_condition_correct sp le e m (CEcondition a b c) t e2 m2 vb2.
+ transl_condition_correct sp le e m (CEcondition a b c) t m2 vb2.
Proof.
intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
- simpl in MUT.
assert (MWF1: map_wf map s1). eauto with rtlg.
- assert (MUTa: incl (mutated_condexpr a) mut). eauto with coqlib.
- generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUTa).
+ generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME).
intros [rs1 [EX1 [ME1 OTHER1]]].
destruct vb1.
assert (MWF0: map_wf map s0). eauto with rtlg.
- assert (MUTb: incl (mutated_condexpr b) mut). eauto with coqlib.
- generalize (H2 _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 MUTb).
+ generalize (H2 _ _ _ _ _ _ _ MWF0 EQ0 ME1).
intros [rs2 [EX2 [ME2 OTHER2]]].
exists rs2.
split. eapply exec_trans. eexact EX1.
@@ -886,8 +807,7 @@ Proof.
apply OTHER2; eauto with rtlg.
apply OTHER1; eauto with rtlg.
- assert (MUTc: incl (mutated_condexpr c) mut). eauto with coqlib.
- generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUTc).
+ generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1).
intros [rs2 [EX2 [ME2 OTHER2]]].
exists rs2.
split. eapply exec_trans. eexact EX1.
@@ -901,7 +821,7 @@ Qed.
Lemma transl_exprlist_Enil_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem),
- transl_exprlist_correct sp le e m Enil E0 e m nil.
+ transl_exprlist_correct sp le e m Enil E0 m nil.
Proof.
intros; red; intros.
generalize TE. simpl. destruct rl; monadSimpl.
@@ -914,26 +834,23 @@ Qed.
Lemma transl_exprlist_Econs_correct:
forall (sp: val) (le : letenv) (e : env) (m : mem)
- (a : expr) (bl : exprlist) (t t1: trace) (e1 : env) (m1 : mem)
- (v : val) (t2: trace) (e2 : env) (m2 : mem) (vl : list val),
- eval_expr ge sp le e m a t1 e1 m1 v ->
- transl_expr_correct sp le e m a t1 e1 m1 v ->
- eval_exprlist ge sp le e1 m1 bl t2 e2 m2 vl ->
- transl_exprlist_correct sp le e1 m1 bl t2 e2 m2 vl ->
+ (a : expr) (bl : exprlist) (t t1: trace) (m1 : mem)
+ (v : val) (t2: trace) (m2 : mem) (vl : list val),
+ eval_expr ge sp le e m a t1 m1 v ->
+ transl_expr_correct sp le e m a t1 m1 v ->
+ eval_exprlist ge sp le e m1 bl t2 m2 vl ->
+ transl_exprlist_correct sp le e m1 bl t2 m2 vl ->
t = t1 ** t2 ->
- transl_exprlist_correct sp le e m (Econs a bl) t e2 m2 (v :: vl).
+ transl_exprlist_correct sp le e m (Econs a bl) t m2 (v :: vl).
Proof.
intros. red. intros.
inversion TRG.
- rewrite <- H11 in TE. simpl in TE. monadInv TE. intro EQ1.
- simpl in MUT.
- assert (MUT1: incl (mutated_expr a) mut); eauto with coqlib.
- assert (MUT2: incl (mutated_exprlist bl) mut); eauto with coqlib.
+ rewrite <- H10 in TE. simpl in TE. monadInv TE. intro EQ1.
assert (MWF1: map_wf map s1); eauto with rtlg.
- assert (TRG1: target_reg_ok s1 map mut a r); eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1).
+ assert (TRG1: target_reg_ok s1 map a r); eauto with rtlg.
+ generalize (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
- generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUT2 H12).
+ generalize (H2 _ _ _ _ _ _ _ MWF EQ ME1 H11).
intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
exists rs2.
(* Exec *)
@@ -947,13 +864,12 @@ Proof.
reflexivity.
eauto with rtlg.
eauto with rtlg.
- assumption.
(* Other regs *)
simpl. intros.
transitivity (rs1#r0).
apply OTHER2; auto. tauto.
apply OTHER1; auto. eauto with rtlg.
- elim H15; intro. left; assumption. right; apply sym_not_equal; tauto.
+ elim H13; intro. left; assumption. right; apply sym_not_equal; tauto.
Qed.
Lemma transl_funcall_internal_correct:
@@ -1084,36 +1000,65 @@ Qed.
Lemma transl_stmt_Sexpr_correct:
forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
- (e1 : env) (m1 : mem) (v : val),
- eval_expr ge sp nil e m a t e1 m1 v ->
- transl_expr_correct sp nil e m a t e1 m1 v ->
- transl_stmt_correct sp e m (Sexpr a) t e1 m1 Out_normal.
+ (m1 : mem) (v : val),
+ eval_expr ge sp nil e m a t m1 v ->
+ transl_expr_correct sp nil e m a t m1 v ->
+ transl_stmt_correct sp e m (Sexpr a) t e m1 Out_normal.
Proof.
intros; red; intros.
simpl in OUT. subst nd.
unfold transl_stmt in TE. monadInv TE. intro EQ1.
assert (MWF0: map_wf map s0). eauto with rtlg.
- assert (TRG: target_reg_ok s0 map (mutated_expr a) a r). eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ _ MWF0 EQ1 ME (incl_refl (mutated_expr a)) TRG).
+ assert (TRG: target_reg_ok s0 map a r). eauto with rtlg.
+ generalize (H0 _ _ _ _ _ _ _ MWF0 EQ1 ME TRG).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
exists rs1; simpl; tauto.
Qed.
+Lemma transl_stmt_Sassign_correct:
+ forall (sp: val) (e : env) (m : mem)
+ (id : ident) (a : expr) (t: trace) (m1 : mem) (v : val),
+ eval_expr ge sp nil e m a t m1 v ->
+ transl_expr_correct sp nil e m a t m1 v ->
+ transl_stmt_correct sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal.
+Proof.
+ intros; red; intros.
+ simpl in TE. monadInv TE. intro EQ2.
+ assert (MWF0: map_wf map s2).
+ apply map_wf_incr with s. eauto 6 with rtlg. auto.
+ assert (TRGa: target_reg_ok s2 map a r0). eauto 6 with rtlg.
+ generalize (H0 _ _ _ _ _ _ _ MWF0 EQ2 ME TRGa).
+ intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
+ generalize (add_move_correct _ _ sp _ _ _ _ rs1 m1 EQ1).
+ intros [rs2 [EX2 [RES2 OTHER2]]].
+ exists rs2.
+(* Exec *)
+ split. inversion OUT; subst. eapply exec_trans. eexact EX1.
+ apply exec_instrs_incr with s2. eauto with rtlg.
+ eexact EX2. traceEq.
+(* Match-env *)
+ split.
+ apply match_env_update_var with rs1 r s s0; auto.
+ congruence.
+(* Outcome *)
+ simpl; auto.
+Qed.
+
Lemma transl_stmt_Sifthenelse_correct:
forall (sp: val) (e : env) (m : mem) (a : condexpr)
- (s1 s2 : stmt) (t t1: trace) (e1 : env) (m1 : mem)
+ (s1 s2 : stmt) (t t1: trace) (m1 : mem)
(v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (out : outcome),
- eval_condexpr ge sp nil e m a t1 e1 m1 v1 ->
- transl_condition_correct sp nil e m a t1 e1 m1 v1 ->
- exec_stmt ge sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out ->
- transl_stmt_correct sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out ->
+ eval_condexpr ge sp nil e m a t1 m1 v1 ->
+ transl_condition_correct sp nil e m a t1 m1 v1 ->
+ exec_stmt ge sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
+ transl_stmt_correct sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
t = t1 ** t2 ->
transl_stmt_correct sp e m (Sifthenelse a s1 s2) t e2 m2 out.
Proof.
intros; red; intros until rs; intro MWF.
simpl. case (more_likely a s1 s2); monadSimpl; intro EQ2; intros.
assert (MWF1: map_wf map s3). eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)).
+ generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME).
intros [rs1 [EX1 [ME1 OTHER1]]].
destruct v1.
assert (MWF0: map_wf map s0). eauto with rtlg.
@@ -1132,7 +1077,7 @@ Proof.
tauto.
assert (MWF1: map_wf map s3). eauto with rtlg.
- generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)).
+ generalize (H0 _ _ _ _ _ _ rs MWF1 EQ2 ME).
intros [rs1 [EX1 [ME1 OTHER1]]].
destruct v1.
generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG).
@@ -1291,10 +1236,10 @@ Qed.
Lemma transl_stmt_Sswitch_correct:
forall (sp : val) (e : env) (m : mem) (a : expr)
(cases : list (int * nat)) (default : nat)
- (t1 : trace) (e1 : env) (m1 : mem) (n : int),
- eval_expr ge sp nil e m a t1 e1 m1 (Vint n) ->
- transl_expr_correct sp nil e m a t1 e1 m1 (Vint n) ->
- transl_stmt_correct sp e m (Sswitch a cases default) t1 e1 m1
+ (t1 : trace) (m1 : mem) (n : int),
+ eval_expr ge sp nil e m a t1 m1 (Vint n) ->
+ transl_expr_correct sp nil e m a t1 m1 (Vint n) ->
+ transl_stmt_correct sp e m (Sswitch a cases default) t1 e m1
(Out_exit (switch_target n default cases)).
Proof.
intros; red; intros. monadInv TE. clear TE; intros EQ1.
@@ -1303,8 +1248,8 @@ Proof.
red in H0.
assert (MWF1: map_wf map s1). eauto with rtlg.
- assert (TRG1: target_reg_ok s1 map (mutated_expr a) a r). eauto with rtlg.
- destruct (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME (incl_refl _) TRG1)
+ assert (TRG1: target_reg_ok s1 map a r). eauto with rtlg.
+ destruct (H0 _ _ _ _ _ _ _ MWF1 EQ1 ME TRG1)
as [rs' [EXEC1 [ME1 [RES1 OTHER1]]]].
simpl. exists rs'.
(* execution *)
@@ -1327,16 +1272,16 @@ Qed.
Lemma transl_stmt_Sreturn_some_correct:
forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
- (e1 : env) (m1 : mem) (v : val),
- eval_expr ge sp nil e m a t e1 m1 v ->
- transl_expr_correct sp nil e m a t e1 m1 v ->
- transl_stmt_correct sp e m (Sreturn (Some a)) t e1 m1 (Out_return (Some v)).
+ (m1 : mem) (v : val),
+ eval_expr ge sp nil e m a t m1 v ->
+ transl_expr_correct sp nil e m a t m1 v ->
+ transl_stmt_correct sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)).
Proof.
intros; red; intros. generalize TE; simpl.
destruct rret. intro EQ.
- assert (TRG: target_reg_ok s map (mutated_expr a) a r).
+ assert (TRG: target_reg_ok s map a r).
inversion RRG. apply target_reg_other; auto.
- generalize (H0 _ _ _ _ _ _ _ _ MWF EQ ME (incl_refl _) TRG).
+ generalize (H0 _ _ _ _ _ _ _ MWF EQ ME TRG).
intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
simpl in OUT. subst nd. exists rs1. tauto.
@@ -1366,7 +1311,6 @@ Proof
transl_stmt_correct
transl_expr_Evar_correct
- transl_expr_Eassign_correct
transl_expr_Eop_correct
transl_expr_Eload_correct
transl_expr_Estore_correct
@@ -1385,6 +1329,7 @@ Proof
transl_funcall_external_correct
transl_stmt_Sskip_correct
transl_stmt_Sexpr_correct
+ transl_stmt_Sassign_correct
transl_stmt_Sifthenelse_correct
transl_stmt_Sseq_continue_correct
transl_stmt_Sseq_stop_correct
diff --git a/backend/RTLgenproof1.v b/backend/RTLgenproof1.v
index 8b14901..8e12e79 100644
--- a/backend/RTLgenproof1.v
+++ b/backend/RTLgenproof1.v
@@ -402,20 +402,6 @@ Proof.
Qed.
Hint Resolve reg_in_map_valid: rtlg.
-(** A register is mutated if it is associated with a Cminor local variable
- that belongs to the given set of mutated variables. *)
-
-Definition mutated_reg (map: mapping) (mut: list ident) (r: reg) : Prop :=
- exists id, In id mut /\ map.(map_vars)!id = Some r.
-
-Lemma mutated_reg_in_map:
- forall map mut r, mutated_reg map mut r -> reg_in_map map r.
-Proof.
- intros. elim H. intros id [IN EQ].
- left. exists id; auto.
-Qed.
-Hint Resolve mutated_reg_in_map: rtlg.
-
(** * Properties of basic operations over the state *)
(** Properties of [add_instr]. *)
@@ -538,16 +524,6 @@ Proof.
Qed.
Hint Resolve new_reg_not_in_map: rtlg.
-Lemma new_reg_not_mutated:
- forall s1 s2 m mut r,
- new_reg s1 = OK r s2 -> map_wf m s1 -> ~(mutated_reg m mut r).
-Proof.
- unfold not; intros.
- generalize (mutated_reg_in_map _ _ _ H1); intro.
- exact (new_reg_not_in_map _ _ _ _ H H0 H2).
-Qed.
-Hint Resolve new_reg_not_mutated: rtlg.
-
(** * Properties of operations over compilation environments *)
Lemma init_mapping_wf:
@@ -592,21 +568,6 @@ Proof.
Qed.
Hint Resolve find_var_valid: rtlg.
-Lemma find_var_not_mutated:
- forall s1 s2 map name r mut,
- find_var map name s1 = OK r s2 ->
- map_wf map s1 ->
- ~(In name mut) ->
- ~(mutated_reg map mut r).
-Proof.
- intros until mut. unfold find_var; caseEq (map.(map_vars)!name).
- intros r0 EQ. monadSimpl; intros; subst r0.
- red; unfold mutated_reg; intros [id [IN EQ2]].
- assert (name = id). eauto with rtlg.
- subst id. contradiction.
- intro; monadSimpl.
-Qed.
-Hint Resolve find_var_not_mutated: rtlg.
(** Properties of [find_letvar]. *)
@@ -641,20 +602,6 @@ Proof.
Qed.
Hint Resolve find_letvar_valid: rtlg.
-Lemma find_letvar_not_mutated:
- forall s1 s2 map idx mut r,
- find_letvar map idx s1 = OK r s2 ->
- map_wf map s1 ->
- ~(mutated_reg map mut r).
-Proof.
- intros until r. unfold find_letvar.
- caseEq (nth_error (map_letvars map) idx).
- intros r' NTH. monadSimpl. unfold not; unfold mutated_reg.
- intros MWF (id, (IN, MV)). subst r'. eauto with rtlg coqlib.
- intro; monadSimpl.
-Qed.
-Hint Resolve find_letvar_not_mutated: rtlg.
-
(** Properties of [add_var]. *)
Lemma add_var_valid:
@@ -781,38 +728,34 @@ Qed.
(** * Properties of [alloc_reg] and [alloc_regs] *)
Lemma alloc_reg_incr:
- forall a s1 s2 map mut r,
- alloc_reg map mut a s1 = OK r s2 -> state_incr s1 s2.
+ forall a s1 s2 map r,
+ alloc_reg map a s1 = OK r s2 -> state_incr s1 s2.
Proof.
intros until r. unfold alloc_reg.
case a; eauto with rtlg.
- intro i; case (In_dec ident_eq i mut); eauto with rtlg.
Qed.
Hint Resolve alloc_reg_incr: rtlg.
Lemma alloc_reg_valid:
- forall a s1 s2 map mut r,
+ forall a s1 s2 map r,
map_wf map s1 ->
- alloc_reg map mut a s1 = OK r s2 -> reg_valid r s2.
+ alloc_reg map a s1 = OK r s2 -> reg_valid r s2.
Proof.
intros until r. unfold alloc_reg.
case a; eauto with rtlg.
- intro i; case (In_dec ident_eq i mut); eauto with rtlg.
Qed.
Hint Resolve alloc_reg_valid: rtlg.
Lemma alloc_reg_fresh_or_in_map:
- forall map mut a s r s',
+ forall map a s r s',
map_wf map s ->
- alloc_reg map mut a s = OK r s' ->
+ alloc_reg map a s = OK r s' ->
reg_in_map map r \/ reg_fresh r s.
Proof.
intros until s'. unfold alloc_reg.
- destruct a; try (right; eauto with rtlg; fail).
- case (In_dec ident_eq i mut); intros.
- right; eauto with rtlg.
+ destruct a; intros; try (right; eauto with rtlg; fail).
+ left; eauto with rtlg.
left; eauto with rtlg.
- intros; left; eauto with rtlg.
Qed.
Lemma add_vars_letenv:
@@ -830,74 +773,57 @@ Qed.
(** A register is an adequate target for holding the value of an
expression if
- either the register is associated with a Cminor let-bound variable
- or a Cminor local variable that is not modified;
+ or a Cminor local variable;
- or the register is valid and not associated with any Cminor variable. *)
-Inductive target_reg_ok: state -> mapping -> list ident -> expr -> reg -> Prop :=
- | target_reg_immut_var:
- forall s map mut id r,
- ~(In id mut) -> map.(map_vars)!id = Some r ->
- target_reg_ok s map mut (Evar id) r
+Inductive target_reg_ok: state -> mapping -> expr -> reg -> Prop :=
+ | target_reg_var:
+ forall s map id r,
+ map.(map_vars)!id = Some r ->
+ target_reg_ok s map (Evar id) r
| target_reg_letvar:
- forall s map mut idx r,
+ forall s map idx r,
nth_error map.(map_letvars) idx = Some r ->
- target_reg_ok s map mut (Eletvar idx) r
+ target_reg_ok s map (Eletvar idx) r
| target_reg_other:
- forall s map mut a r,
+ forall s map a r,
~(reg_in_map map r) ->
reg_valid r s ->
- target_reg_ok s map mut a r.
+ target_reg_ok s map a r.
Lemma target_reg_ok_incr:
- forall s1 s2 map mut e r,
+ forall s1 s2 map e r,
state_incr s1 s2 ->
- target_reg_ok s1 map mut e r ->
- target_reg_ok s2 map mut e r.
+ target_reg_ok s1 map e r ->
+ target_reg_ok s2 map e r.
Proof.
intros. inversion H0.
- apply target_reg_immut_var; auto.
+ apply target_reg_var; auto.
apply target_reg_letvar; auto.
apply target_reg_other; eauto with rtlg.
Qed.
Hint Resolve target_reg_ok_incr: rtlg.
Lemma target_reg_valid:
- forall s map mut e r,
+ forall s map e r,
map_wf map s ->
- target_reg_ok s map mut e r ->
+ target_reg_ok s map e r ->
reg_valid r s.
Proof.
intros. inversion H0; eauto with rtlg coqlib.
Qed.
Hint Resolve target_reg_valid: rtlg.
-Lemma target_reg_not_mutated:
- forall s map mut e r,
- map_wf map s ->
- target_reg_ok s map mut e r ->
- ~(mutated_reg map mut r).
-Proof.
- unfold not; unfold mutated_reg; intros until r.
- intros MWF TRG [id [IN MV]].
- inversion TRG.
- assert (id = id0); eauto with rtlg. subst id0. contradiction.
- assert (In r (map_letvars map)). eauto with coqlib. eauto with rtlg.
- apply H. red. left; exists id; assumption.
-Qed.
-Hint Resolve target_reg_not_mutated: rtlg.
-
Lemma alloc_reg_target_ok:
- forall a s1 s2 map mut r,
+ forall a s1 s2 map r,
map_wf map s1 ->
- alloc_reg map mut a s1 = OK r s2 ->
- target_reg_ok s2 map mut a r.
+ alloc_reg map a s1 = OK r s2 ->
+ target_reg_ok s2 map a r.
Proof.
intros until r; intro MWF. unfold alloc_reg.
case a; intros; try (eapply target_reg_other; eauto with rtlg; fail).
- generalize H; case (In_dec ident_eq i mut); intros.
- apply target_reg_other; eauto with rtlg.
- apply target_reg_immut_var; auto.
- generalize H0; unfold find_var.
+ apply target_reg_var.
+ generalize H; unfold find_var.
case (map_vars map)!i.
intro. monadSimpl. congruence.
monadSimpl.
@@ -910,8 +836,8 @@ Qed.
Hint Resolve alloc_reg_target_ok: rtlg.
Lemma alloc_regs_incr:
- forall al s1 s2 map mut rl,
- alloc_regs map mut al s1 = OK rl s2 -> state_incr s1 s2.
+ forall al s1 s2 map rl,
+ alloc_regs map al s1 = OK rl s2 -> state_incr s1 s2.
Proof.
induction al; simpl; intros.
monadInv H. subst s2. eauto with rtlg.
@@ -920,9 +846,9 @@ Qed.
Hint Resolve alloc_regs_incr: rtlg.
Lemma alloc_regs_valid:
- forall al s1 s2 map mut rl,
+ forall al s1 s2 map rl,
map_wf map s1 ->
- alloc_regs map mut al s1 = OK rl s2 ->
+ alloc_regs map al s1 = OK rl s2 ->
forall r, In r rl -> reg_valid r s2.
Proof.
induction al; simpl; intros.
@@ -935,9 +861,9 @@ Qed.
Hint Resolve alloc_regs_valid: rtlg.
Lemma alloc_regs_fresh_or_in_map:
- forall map mut al s rl s',
+ forall map al s rl s',
map_wf map s ->
- alloc_regs map mut al s = OK rl s' ->
+ alloc_regs map al s = OK rl s' ->
forall r, In r rl -> reg_in_map map r \/ reg_fresh r s.
Proof.
induction al; simpl; intros.
@@ -945,28 +871,28 @@ Proof.
monadInv H0. subst rl. elim (in_inv H1); intro.
subst r.
assert (MWF: map_wf map s0). eauto with rtlg.
- elim (alloc_reg_fresh_or_in_map map mut e s0 r0 s1 MWF EQ0); intro.
+ elim (alloc_reg_fresh_or_in_map map e s0 r0 s1 MWF EQ0); intro.
left; assumption. right; eauto with rtlg.
eauto with rtlg.
Qed.
-Inductive target_regs_ok: state -> mapping -> list ident -> exprlist -> list reg -> Prop :=
+Inductive target_regs_ok: state -> mapping -> exprlist -> list reg -> Prop :=
| target_regs_nil:
- forall s map mut,
- target_regs_ok s map mut Enil nil
+ forall s map,
+ target_regs_ok s map Enil nil
| target_regs_cons:
- forall s map mut a r al rl,
+ forall s map a r al rl,
reg_in_map map r \/ ~(In r rl) ->
- target_reg_ok s map mut a r ->
- target_regs_ok s map mut al rl ->
- target_regs_ok s map mut (Econs a al) (r :: rl).
+ target_reg_ok s map a r ->
+ target_regs_ok s map al rl ->
+ target_regs_ok s map (Econs a al) (r :: rl).
Lemma target_regs_ok_incr:
- forall s1 map mut al rl,
- target_regs_ok s1 map mut al rl ->
+ forall s1 map al rl,
+ target_regs_ok s1 map al rl ->
forall s2,
state_incr s1 s2 ->
- target_regs_ok s2 map mut al rl.
+ target_regs_ok s2 map al rl.
Proof.
induction 1; intros.
apply target_regs_nil.
@@ -975,8 +901,8 @@ Qed.
Hint Resolve target_regs_ok_incr: rtlg.
Lemma target_regs_valid:
- forall s map mut al rl,
- target_regs_ok s map mut al rl ->
+ forall s map al rl,
+ target_regs_ok s map al rl ->
map_wf map s ->
forall r, In r rl -> reg_valid r s.
Proof.
@@ -988,31 +914,18 @@ Proof.
Qed.
Hint Resolve target_regs_valid: rtlg.
-Lemma target_regs_not_mutated:
- forall s map mut el rl,
- target_regs_ok s map mut el rl ->
- map_wf map s ->
- forall r, In r rl -> ~(mutated_reg map mut r).
-Proof.
- induction 1; simpl; intros.
- contradiction.
- elim H3; intro. subst r0. eauto with rtlg.
- auto.
-Qed.
-Hint Resolve target_regs_not_mutated: rtlg.
-
Lemma alloc_regs_target_ok:
- forall al s1 s2 map mut rl,
+ forall al s1 s2 map rl,
map_wf map s1 ->
- alloc_regs map mut al s1 = OK rl s2 ->
- target_regs_ok s2 map mut al rl.
+ alloc_regs map al s1 = OK rl s2 ->
+ target_regs_ok s2 map al rl.
Proof.
induction al; simpl; intros.
monadInv H0. subst rl; apply target_regs_nil.
monadInv H0. subst s0; subst rl.
apply target_regs_cons; eauto 6 with rtlg.
assert (MWF: map_wf map s). eauto with rtlg.
- elim (alloc_reg_fresh_or_in_map map mut e s r s2 MWF EQ0); intro.
+ elim (alloc_reg_fresh_or_in_map map e s r s2 MWF EQ0); intro.
left; assumption. right; red; intro; eauto with rtlg.
Qed.
Hint Resolve alloc_regs_target_ok: rtlg.
@@ -1306,7 +1219,6 @@ Lemma expr_condexpr_exprlist_ind:
forall (P : expr -> Prop) (P0 : condexpr -> Prop)
(P1 : exprlist -> Prop),
(forall i : ident, P (Evar i)) ->
- (forall (i : ident) (e : expr), P e -> P (Eassign i e)) ->
(forall (o : operation) (e : exprlist), P1 e -> P (Eop o e)) ->
(forall (m : memory_chunk) (a : addressing) (e : exprlist),
P1 e -> P (Eload m a e)) ->
@@ -1341,14 +1253,14 @@ Proof.
Qed.
Definition transl_expr_incr_pred (a: expr) : Prop :=
- forall map mut rd nd s ns s',
- transl_expr map mut a rd nd s = OK ns s' -> state_incr s s'.
+ forall map rd nd s ns s',
+ transl_expr map a rd nd s = OK ns s' -> state_incr s s'.
Definition transl_condition_incr_pred (c: condexpr) : Prop :=
- forall map mut ntrue nfalse s ns s',
- transl_condition map mut c ntrue nfalse s = OK ns s' -> state_incr s s'.
+ forall map ntrue nfalse s ns s',
+ transl_condition map c ntrue nfalse s = OK ns s' -> state_incr s s'.
Definition transl_exprlist_incr_pred (al: exprlist) : Prop :=
- forall map mut rl nd s ns s',
- transl_exprlist map mut al rl nd s = OK ns s' -> state_incr s s'.
+ forall map rl nd s ns s',
+ transl_exprlist map al rl nd s = OK ns s' -> state_incr s s'.
Lemma transl_expr_condition_exprlist_incr:
(forall a, transl_expr_incr_pred a) /\
@@ -1377,18 +1289,18 @@ Proof.
Qed.
Lemma transl_expr_incr:
- forall a map mut rd nd s ns s',
- transl_expr map mut a rd nd s = OK ns s' -> state_incr s s'.
+ forall a map rd nd s ns s',
+ transl_expr map a rd nd s = OK ns s' -> state_incr s s'.
Proof (proj1 transl_expr_condition_exprlist_incr).
Lemma transl_condition_incr:
- forall a map mut ntrue nfalse s ns s',
- transl_condition map mut a ntrue nfalse s = OK ns s' -> state_incr s s'.
+ forall a map ntrue nfalse s ns s',
+ transl_condition map a ntrue nfalse s = OK ns s' -> state_incr s s'.
Proof (proj1 (proj2 transl_expr_condition_exprlist_incr)).
Lemma transl_exprlist_incr:
- forall al map mut rl nd s ns s',
- transl_exprlist map mut al rl nd s = OK ns s' -> state_incr s s'.
+ forall al map rl nd s ns s',
+ transl_exprlist map al rl nd s = OK ns s' -> state_incr s s'.
Proof (proj2 (proj2 transl_expr_condition_exprlist_incr)).
Hint Resolve transl_expr_incr transl_condition_incr transl_exprlist_incr: rtlg.
@@ -1431,6 +1343,8 @@ Proof.
monadInv H. eauto with rtlg.
+ monadInv H. intro. apply state_incr_trans3 with s0 s1 s2; eauto with rtlg.
+
monadInv H. eauto with rtlg.
generalize H. case (more_likely c a1 a2); monadSimpl; eauto 6 with rtlg.
diff --git a/caml/CMparser.mly b/caml/CMparser.mly
index 2df44fb..d9a8187 100644
--- a/caml/CMparser.mly
+++ b/caml/CMparser.mly
@@ -216,6 +216,7 @@ var_declaration:
stmt:
expr SEMICOLON { Sexpr $1 }
+ | IDENT EQUAL expr SEMICOLON { Sassign($1, $3) }
| IF LPAREN expr RPAREN stmts ELSE stmts { Cmconstr.ifthenelse $3 $5 $7 }
| IF LPAREN expr RPAREN stmts { Cmconstr.ifthenelse $3 $5 Sskip }
| LOOP stmts { Sloop($2) }
@@ -241,7 +242,6 @@ stmt_list:
expr:
LPAREN expr RPAREN { $2 }
| IDENT { Evar $1 }
- | IDENT EQUAL expr { Eassign($1, $3) }
| INTLIT { intconst $1 }
| FLOATLIT { Eop(Ofloatconst $1, Enil) }
| STRINGLIT { Eop(Oaddrsymbol($1, Int.zero), Enil) }
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml
index 4e700d7..a926039 100644
--- a/caml/CMtypecheck.ml
+++ b/caml/CMtypecheck.ml
@@ -219,15 +219,6 @@ let rec type_expr env lenv e =
match e with
| Evar id ->
type_var env id
- | Eassign(id, e1) ->
- let tid = type_var env id in
- let te1 = type_expr env lenv e1 in
- begin try
- unify tid te1
- with Error s ->
- raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s))
- end;
- tid
| Eop(op, el) ->
let tel = type_exprlist env lenv el in
let (targs, tres) = type_operation op in
@@ -325,6 +316,14 @@ let rec type_stmt env blk ret s =
| Sskip -> ()
| Sexpr e ->
ignore (type_expr env [] e)
+ | Sassign(id, e1) ->
+ let tid = type_var env id in
+ let te1 = type_expr env [] e1 in
+ begin try
+ unify tid te1
+ with Error s ->
+ raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s))
+ end
| Sseq(s1, s2) ->
type_stmt env blk ret s1;
type_stmt env blk ret s2
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 30832e8..27aa453 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -168,7 +168,7 @@ Definition var_get (cenv: compilenv) (id: ident): option expr :=
Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option stmt :=
match PMap.get id cenv with
| Var_local chunk =>
- Some(Sexpr(Eassign id (make_cast chunk rhs)))
+ Some(Sassign id (make_cast chunk rhs))
| Var_stack_scalar chunk ofs =>
Some(make_store chunk (make_stackaddr ofs) rhs)
| Var_global_scalar chunk =>
@@ -397,7 +397,7 @@ Fixpoint store_parameters
| (id, chunk) :: rem =>
match PMap.get id cenv with
| Var_local chunk =>
- Sseq (Sexpr (Eassign id (make_cast chunk (Evar id))))
+ Sseq (Sassign id (make_cast chunk (Evar id)))
(store_parameters cenv rem)
| Var_stack_scalar chunk ofs =>
Sseq (make_store chunk (make_stackaddr ofs) (Evar id))
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 66d0eff..f700f82 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -851,14 +851,14 @@ Qed.
provided arguments match pairwise ([val_list_inject f] hypothesis). *)
Lemma make_op_correct:
- forall al a op vl m2 v sp le te1 tm1 t te2 tm2 tvl f,
+ forall al a op vl m2 v sp le te tm1 t tm2 tvl f,
make_op op al = Some a ->
Csharpminor.eval_operation op vl m2 = Some v ->
- eval_exprlist tge (Vptr sp Int.zero) le te1 tm1 al t te2 tm2 tvl ->
+ eval_exprlist tge (Vptr sp Int.zero) le te tm1 al t tm2 tvl ->
val_list_inject f vl tvl ->
mem_inject f m2 tm2 ->
exists tv,
- eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 tv
+ eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 tv
/\ val_inject f v tv.
Proof.
intros.
@@ -867,7 +867,7 @@ Proof.
[idtac | destruct al as [ | a3 al]]];
simpl in H; try discriminate.
(* Constant operators *)
- inversion H1. subst sp0 le0 e m te2 tm1 tvl.
+ inversion H1. subst sp0 le0 e m tm1 tvl.
inversion H2. subst vl.
destruct op; simplify_eq H; intro; subst a;
simpl in H0; injection H0; intro; subst v.
@@ -965,13 +965,12 @@ Qed.
normalized according to the given memory chunk. *)
Lemma make_cast_correct:
- forall f sp le te1 tm1 a t te2 tm2 v chunk tv,
- eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 tv ->
+ forall f sp le te tm1 a t tm2 v chunk tv,
+ eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 tv ->
val_inject f v tv ->
exists tv',
eval_expr tge (Vptr sp Int.zero) le
- te1 tm1 (make_cast chunk a)
- t te2 tm2 tv'
+ te tm1 (make_cast chunk a) t tm2 tv'
/\ val_inject f (Val.load_result chunk v) tv'.
Proof.
intros. destruct chunk.
@@ -1009,7 +1008,7 @@ Lemma make_stackaddr_correct:
forall sp le te tm ofs,
eval_expr tge (Vptr sp Int.zero) le
te tm (make_stackaddr ofs)
- E0 te tm (Vptr sp (Int.repr ofs)).
+ E0 tm (Vptr sp (Int.repr ofs)).
Proof.
intros; unfold make_stackaddr.
eapply eval_Eop. econstructor. simpl. decEq. decEq.
@@ -1021,7 +1020,7 @@ Lemma make_globaladdr_correct:
Genv.find_symbol tge id = Some b ->
eval_expr tge (Vptr sp Int.zero) le
te tm (make_globaladdr id)
- E0 te tm (Vptr b Int.zero).
+ E0 tm (Vptr b Int.zero).
Proof.
intros; unfold make_globaladdr.
eapply eval_Eop. econstructor. simpl. rewrite H. auto.
@@ -1030,28 +1029,28 @@ Qed.
(** Correctness of [make_load] and [make_store]. *)
Lemma make_load_correct:
- forall sp le te1 tm1 a t te2 tm2 va chunk v,
- eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 va ->
+ forall sp le te tm1 a t tm2 va chunk v,
+ eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 va ->
Mem.loadv chunk tm2 va = Some v ->
eval_expr tge (Vptr sp Int.zero) le
- te1 tm1 (make_load chunk a)
- t te2 tm2 v.
+ te tm1 (make_load chunk a)
+ t tm2 v.
Proof.
intros; unfold make_load.
eapply eval_load; eauto.
Qed.
Lemma store_arg_content_inject:
- forall f sp le te1 tm1 a t te2 tm2 v va chunk,
- eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 va ->
+ forall f sp le te tm1 a t tm2 v va chunk,
+ eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 va ->
val_inject f v va ->
exists vb,
- eval_expr tge (Vptr sp Int.zero) le te1 tm1 (store_arg chunk a) t te2 tm2 vb
+ eval_expr tge (Vptr sp Int.zero) le te tm1 (store_arg chunk a) t tm2 vb
/\ val_content_inject f (mem_chunk chunk) v vb.
Proof.
intros.
assert (exists vb,
- eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 vb
+ eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 vb
/\ val_content_inject f (mem_chunk chunk) v vb).
exists va; split. assumption. constructor. assumption.
inversion H; clear H; subst; simpl; trivial.
@@ -1070,20 +1069,20 @@ Proof.
Qed.
Lemma make_store_correct:
- forall f sp te1 tm1 addr te2 tm2 tvaddr rhs te3 tm3 tvrhs
+ forall f sp te tm1 addr tm2 tvaddr rhs tm3 tvrhs
chunk vrhs m3 vaddr m4 t1 t2,
eval_expr tge (Vptr sp Int.zero) nil
- te1 tm1 addr t1 te2 tm2 tvaddr ->
+ te tm1 addr t1 tm2 tvaddr ->
eval_expr tge (Vptr sp Int.zero) nil
- te2 tm2 rhs t2 te3 tm3 tvrhs ->
+ te tm2 rhs t2 tm3 tvrhs ->
Mem.storev chunk m3 vaddr vrhs = Some m4 ->
mem_inject f m3 tm3 ->
val_inject f vaddr tvaddr ->
val_inject f vrhs tvrhs ->
exists tm4,
exec_stmt tge (Vptr sp Int.zero)
- te1 tm1 (make_store chunk addr rhs)
- (t1**t2) te3 tm4 Out_normal
+ te tm1 (make_store chunk addr rhs)
+ (t1**t2) te tm4 Out_normal
/\ mem_inject f m4 tm4
/\ nextblock tm4 = nextblock tm3.
Proof.
@@ -1112,7 +1111,7 @@ Lemma var_get_correct:
eval_var_ref prog e id b chunk ->
load chunk m b 0 = Some v ->
exists tv,
- eval_expr tge (Vptr sp Int.zero) le te tm a E0 te tm tv /\
+ eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\
val_inject f v tv.
Proof.
unfold var_get; intros.
@@ -1155,7 +1154,7 @@ Lemma var_addr_correct:
var_addr cenv id = Some a ->
eval_var_addr prog e id b ->
exists tv,
- eval_expr tge (Vptr sp Int.zero) le te tm a E0 te tm tv /\
+ eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\
val_inject f (Vptr b Int.zero) tv.
Proof.
unfold var_addr; intros.
@@ -1189,24 +1188,24 @@ Proof.
Qed.
Lemma var_set_correct:
- forall cenv id rhs a f e te2 sp lo hi m2 cs tm2 te1 tm1 tv b chunk v m3 t,
+ forall cenv id rhs a f e te sp lo hi m2 cs tm2 tm1 tv b chunk v m3 t,
var_set cenv id rhs = Some a ->
- match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 ->
- eval_expr tge (Vptr sp Int.zero) nil te1 tm1 rhs t te2 tm2 tv ->
+ match_callstack f (mkframe cenv e te sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 ->
+ eval_expr tge (Vptr sp Int.zero) nil te tm1 rhs t tm2 tv ->
val_inject f v tv ->
mem_inject f m2 tm2 ->
eval_var_ref prog e id b chunk ->
store chunk m2 b 0 v = Some m3 ->
exists te3, exists tm3,
- exec_stmt tge (Vptr sp Int.zero) te1 tm1 a t te3 tm3 Out_normal /\
+ exec_stmt tge (Vptr sp Int.zero) te tm1 a t te3 tm3 Out_normal /\
mem_inject f m3 tm3 /\
match_callstack f (mkframe cenv e te3 sp lo hi :: cs) m3.(nextblock) tm3.(nextblock) m3.
Proof.
unfold var_set; intros.
assert (NEXTBLOCK: nextblock m3 = nextblock m2).
exploit store_inv; eauto. simpl; tauto.
- inversion H0. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m.
- assert (match_var f id e m2 te2 sp cenv!!id). inversion H19; auto.
+ inversion H0. subst.
+ assert (match_var f id e m2 te sp cenv!!id). inversion H19; auto.
inversion H6; subst; rewrite <- H7 in H; inversion H; subst; clear H.
(* var_local *)
inversion H4; [subst|congruence].
@@ -1214,8 +1213,8 @@ Proof.
assert (chunk0 = chunk). congruence. subst chunk0.
exploit make_cast_correct; eauto.
intros [tv' [EVAL INJ]].
- exists (PTree.set id tv' te2); exists tm2.
- split. eapply exec_Sexpr. eapply eval_Eassign. eauto.
+ exists (PTree.set id tv' te); exists tm2.
+ split. eapply exec_Sassign. eauto.
split. eapply store_unmapped_inject; eauto.
rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto.
(* var_stack_scalar *)
@@ -1227,7 +1226,7 @@ Proof.
eapply make_stackaddr_correct.
eauto. eauto. eauto. eauto. eauto.
rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]].
- exists te2; exists tm3.
+ exists te; exists tm3.
split. auto. split. auto.
rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
eapply match_callstack_mapped; eauto.
@@ -1242,7 +1241,7 @@ Proof.
eapply make_globaladdr_correct; eauto.
eauto. eauto. eauto. eauto. eauto.
rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]].
- exists te2; exists tm3.
+ exists te; exists tm3.
split. auto. split. auto.
rewrite NEXTBLOCK; rewrite TNEXTBLOCK.
eapply match_callstack_mapped; eauto. congruence.
@@ -1586,8 +1585,7 @@ Proof.
exists te3; exists tm3.
(* execution *)
split. apply exec_Sseq_continue with E0 te2 tm1 E0.
- econstructor. unfold te2. constructor. eassumption.
- assumption. traceEq.
+ unfold te2. constructor. eassumption. assumption. traceEq.
(* meminj & match_callstack *)
tauto.
@@ -1784,38 +1782,38 @@ Ltac monadInv H :=
Definition eval_expr_prop
(le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (t: trace) (m2: mem) (v: val) : Prop :=
- forall cenv ta f1 tle te1 tm1 sp lo hi cs
+ forall cenv ta f1 tle te tm1 sp lo hi cs
(TR: transl_expr cenv a = Some ta)
(LINJ: val_list_inject f1 le tle)
(MINJ: mem_inject f1 m1 tm1)
(MATCH: match_callstack f1
- (mkframe cenv e te1 sp lo hi :: cs)
+ (mkframe cenv e te sp lo hi :: cs)
m1.(nextblock) tm1.(nextblock) m1),
- exists f2, exists te2, exists tm2, exists tv,
- eval_expr tge (Vptr sp Int.zero) tle te1 tm1 ta t te2 tm2 tv
+ exists f2, exists tm2, exists tv,
+ eval_expr tge (Vptr sp Int.zero) tle te tm1 ta t tm2 tv
/\ val_inject f2 v tv
/\ mem_inject f2 m2 tm2
/\ inject_incr f1 f2
/\ match_callstack f2
- (mkframe cenv e te2 sp lo hi :: cs)
+ (mkframe cenv e te sp lo hi :: cs)
m2.(nextblock) tm2.(nextblock) m2.
Definition eval_exprlist_prop
(le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (t: trace) (m2: mem) (vl: list val) : Prop :=
- forall cenv tal f1 tle te1 tm1 sp lo hi cs
+ forall cenv tal f1 tle te tm1 sp lo hi cs
(TR: transl_exprlist cenv al = Some tal)
(LINJ: val_list_inject f1 le tle)
(MINJ: mem_inject f1 m1 tm1)
(MATCH: match_callstack f1
- (mkframe cenv e te1 sp lo hi :: cs)
+ (mkframe cenv e te sp lo hi :: cs)
m1.(nextblock) tm1.(nextblock) m1),
- exists f2, exists te2, exists tm2, exists tvl,
- eval_exprlist tge (Vptr sp Int.zero) tle te1 tm1 tal t te2 tm2 tvl
+ exists f2, exists tm2, exists tvl,
+ eval_exprlist tge (Vptr sp Int.zero) tle te tm1 tal t tm2 tvl
/\ val_list_inject f2 vl tvl
/\ mem_inject f2 m2 tm2
/\ inject_incr f1 f2
/\ match_callstack f2
- (mkframe cenv e te2 sp lo hi :: cs)
+ (mkframe cenv e te sp lo hi :: cs)
m2.(nextblock) tm2.(nextblock) m2.
Definition eval_funcall_prop
@@ -1876,7 +1874,7 @@ Proof.
intros; red; intros. unfold transl_expr in TR.
exploit var_get_correct; eauto.
intros [tv [EVAL VINJ]].
- exists f1; exists te1; exists tm1; exists tv; intuition eauto.
+ exists f1; exists tm1; exists tv; intuition eauto.
Qed.
Lemma transl_expr_Eaddrof_correct:
@@ -1889,7 +1887,7 @@ Proof.
intros; red; intros. simpl in TR.
exploit var_addr_correct; eauto.
intros [tv [EVAL VINJ]].
- exists f1; exists te1; exists tm1; exists tv. intuition eauto.
+ exists f1; exists tm1; exists tv. intuition eauto.
Qed.
Lemma transl_expr_Eop_correct:
@@ -1903,10 +1901,10 @@ Lemma transl_expr_Eop_correct:
Proof.
intros; red; intros. monadInv TR; intro EQ0.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]].
+ intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
exploit make_op_correct; eauto.
intros [tv [EVAL2 VINJ2]].
- exists f2; exists te2; exists tm2; exists tv. intuition.
+ exists f2; exists tm2; exists tv. intuition.
Qed.
Lemma transl_expr_Eload_correct:
@@ -1921,10 +1919,10 @@ Proof.
intros; red; intros.
monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
exploit loadv_inject; eauto.
intros [tv [TLOAD VINJ]].
- exists f2; exists te2; exists tm2; exists tv.
+ exists f2; exists tm2; exists tv.
intuition.
subst ta. eapply make_load_correct; eauto.
Qed.
@@ -1948,10 +1946,10 @@ Lemma transl_expr_Ecall_correct:
Proof.
intros;red;intros. monadInv TR. subst ta.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
exploit H2.
eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
- intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]].
+ intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
assert (tv1 = vf).
elim (Genv.find_funct_inv H3). intros bf VF. rewrite VF in H3.
rewrite Genv.find_funct_find_funct_ptr in H3.
@@ -1964,7 +1962,7 @@ Proof.
subst tv1. elim (functions_translated _ _ H3). intros tf [FIND TRF].
exploit H6; eauto.
intros [f4 [tm4 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]].
- exists f4; exists te3; exists tm4; exists tres. intuition.
+ exists f4; exists tm4; exists tres. intuition.
eapply eval_Ecall; eauto.
rewrite <- H4. apply sig_preserved; auto.
apply inject_incr_trans with f2; auto.
@@ -1985,11 +1983,11 @@ Lemma transl_expr_Econdition_true_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
exploit H3.
eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
- intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]].
- exists f3; exists te3; exists tm3; exists tv2.
+ intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
+ exists f3; exists tm3; exists tv2.
intuition.
rewrite <- H6. subst t; eapply eval_conditionalexpr_true; eauto.
inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto.
@@ -2010,11 +2008,11 @@ Lemma transl_expr_Econdition_false_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
exploit H3.
eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
- intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]].
- exists f3; exists te3; exists tm3; exists tv2.
+ intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
+ exists f3; exists tm3; exists tv2.
intuition.
rewrite <- H6. subst t; eapply eval_conditionalexpr_false; eauto.
inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto.
@@ -2034,13 +2032,13 @@ Lemma transl_expr_Elet_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]].
exploit H2.
eauto.
constructor. eauto. eapply val_list_inject_incr; eauto.
eauto. eauto.
- intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]].
- exists f3; exists te3; exists tm3; exists tv2.
+ intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]].
+ exists f3; exists tm3; exists tv2.
intuition.
subst ta; eapply eval_Elet; eauto.
eapply inject_incr_trans; eauto.
@@ -2065,7 +2063,7 @@ Lemma transl_expr_Eletvar_correct:
Proof.
intros; red; intros. monadInv TR.
exploit val_list_inject_nth; eauto. intros [tv [A B]].
- exists f1; exists te1; exists tm1; exists tv.
+ exists f1; exists tm1; exists tv.
intuition.
subst ta. eapply eval_Eletvar; auto.
Qed.
@@ -2080,7 +2078,7 @@ Lemma transl_expr_Ealloc_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
inversion VINJ1. subst tv1 i.
caseEq (alloc tm2 0 (Int.signed n)). intros tm3 tb TALLOC.
assert (LB: Int.min_signed <= 0). compute. congruence.
@@ -2089,7 +2087,7 @@ Proof.
exploit alloc_parallel_inject; eauto.
intros [MINJ3 INCR3].
exists (extend_inject b (Some (tb, 0)) f2);
- exists te2; exists tm3; exists (Vptr tb Int.zero).
+ exists tm3; exists (Vptr tb Int.zero).
split. subst ta; econstructor; eauto.
split. econstructor. unfold extend_inject, eq_block. rewrite zeq_true. reflexivity.
reflexivity.
@@ -2103,7 +2101,7 @@ Lemma transl_exprlist_Enil_correct:
eval_exprlist_prop le e m Csharpminor.Enil E0 m nil.
Proof.
intros; red; intros. monadInv TR.
- exists f1; exists te1; exists tm1; exists (@nil val).
+ exists f1; exists tm1; exists (@nil val).
intuition. subst tal; constructor.
Qed.
@@ -2121,11 +2119,11 @@ Lemma transl_exprlist_Econs_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
exploit H2.
eauto. eapply val_list_inject_incr; eauto. eauto. eauto.
- intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]].
- exists f3; exists te3; exists tm3; exists (tv1 :: tv2).
+ intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]].
+ exists f3; exists tm3; exists (tv1 :: tv2).
intuition. subst tal; econstructor; eauto.
constructor. eapply val_inject_incr; eauto. auto.
eapply inject_incr_trans; eauto.
@@ -2226,8 +2224,8 @@ Lemma transl_stmt_Sexpr_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
- exists f2; exists te2; exists tm2; exists Out_normal.
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
+ exists f2; exists te1; exists tm2; exists Out_normal.
intuition. subst ts. econstructor; eauto.
constructor.
Qed.
@@ -2244,7 +2242,7 @@ Lemma transl_stmt_Sassign_correct:
Proof.
intros; red; intros. monadInv TR; intro EQ0.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]].
exploit var_set_correct; eauto.
intros [te3 [tm3 [EVAL2 [MINJ2 MATCH2]]]].
exists f2; exists te3; exists tm3; exists Out_normal.
@@ -2266,17 +2264,17 @@ Lemma transl_stmt_Sstore_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
exploit H2.
eauto.
eapply val_list_inject_incr; eauto.
eauto. eauto.
- intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]].
+ intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]].
exploit make_store_correct.
eexact EVAL1. eexact EVAL2. eauto. eauto.
eapply val_inject_incr; eauto. eauto.
intros [tm4 [EVAL [MINJ4 NEXTBLOCK]]].
- exists f3; exists te3; exists tm4; exists Out_normal.
+ exists f3; exists te1; exists tm4; exists Out_normal.
rewrite <- H6. subst t3. intuition.
constructor.
eapply inject_incr_trans; eauto.
@@ -2340,7 +2338,7 @@ Lemma transl_stmt_Sifthenelse_true_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
exploit H3; eauto.
intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]].
exists f3; exists te3; exists tm3; exists tout.
@@ -2365,7 +2363,7 @@ Lemma transl_stmt_Sifthenelse_false_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]].
+ intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]].
exploit H3; eauto.
intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]].
exists f3; exists te3; exists tm3; exists tout.
@@ -2454,8 +2452,8 @@ Lemma transl_stmt_Sswitch_correct:
Proof.
intros; red; intros. monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]].
- exists f2; exists te2; exists tm2;
+ intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
+ exists f2; exists te1; exists tm2;
exists (Out_exit (switch_target n default cases)). intuition.
subst ts. constructor. inversion VINJ1. subst tv1. assumption.
constructor.
@@ -2481,8 +2479,8 @@ Lemma transl_stmt_Sreturn_some_correct:
Proof.
intros; red; intros; monadInv TR.
exploit H0; eauto.
- intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]].
- exists f2; exists te2; exists tm2; exists (Out_return (Some tv1)).
+ intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]].
+ exists f2; exists te1; exists tm2; exists (Out_return (Some tv1)).
intuition. subst ts; econstructor; eauto. constructor; auto.
Qed.
diff --git a/test/cminor/aes.cmp b/test/cminor/aes.cmp
index 35eabc4..11a253c 100644
--- a/test/cminor/aes.cmp
+++ b/test/cminor/aes.cmp
@@ -42,7 +42,8 @@
rk(5) = rk(1) ^ rk(4);
rk(6) = rk(2) ^ rk(5);
rk(7) = rk(3) ^ rk(6);
- if ((i = i + 1) == 10) {
+ i = i + 1;
+ if (i == 10) {
return 10;
}
rk_ = rk_ + 4 * 4;
@@ -62,7 +63,8 @@
rk( 7) = rk( 1) ^ rk( 6);
rk( 8) = rk( 2) ^ rk( 7);
rk( 9) = rk( 3) ^ rk( 8);
- if ((i = i + 1) == 8) {
+ i = i + 1;
+ if (i == 8) {
return 12;
}
rk(10) = rk( 4) ^ rk( 9);
@@ -84,7 +86,8 @@
rk( 9) = rk( 1) ^ rk( 8);
rk(10) = rk( 2) ^ rk( 9);
rk(11) = rk( 3) ^ rk(10);
- if ((i = i + 1) == 7) {
+ i = i + 1;
+ if (i == 7) {
return 14;
}
temp = rk(11);
@@ -198,7 +201,8 @@
rk(7);
rk_ = rk_ + 8 * 4;
- if ((r = r - 1) == 0) exit;
+ r = r - 1;
+ if (r == 0) exit;
s0 =
Te0((t0 >>u 24) ) ^
@@ -302,7 +306,8 @@
rk(7);
rk_ = rk_ + 8 * 4;
- if ((r = r - 1) == 0) exit;
+ r = r - 1;
+ if (r == 0) exit;
s0 =
Td0((t0 >>u 24) ) ^
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 03:57:18 +0000