Skip to content
Snippets Groups Projects
Commit ce0892a2 authored by xleroy's avatar xleroy
Browse files

Strengthen chunktype inference and use it to remove some useless casts. 

Finished proof of chunktype_compat, which was incomplete.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1335 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 48fe0e54
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
.depend
+ 1
− 1
View file @ ce0892a2
......@@ -20,7 +20,7 @@ common/Smallstep.vo: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Event
common/Determinism.vo: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo
common/Switch.vo: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo
backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo
$(ARCH)/Op.vo: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo
$(ARCH)/Op.vo: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo
backend/CminorSel.vo: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo
$(ARCH)/SelectOp.vo: $(ARCH)/SelectOp.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo
backend/Selection.vo: backend/Selection.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
......
cfrontend/Cminorgen.v
+ 42
− 9
View file @ ce0892a2
......@@ -70,7 +70,10 @@ Definition compilenv := PMap.t var_info.
Definition chunktype_const (c: Csharpminor.constant) :=
match c with
| Csharpminor.Ointconst n => Mint32
| Csharpminor.Ointconst n =>
if Int.ltu n (Int.repr 256) then Mint8unsigned
else if Int.ltu n (Int.repr 65536) then Mint16unsigned
else Mint32
| Csharpminor.Ofloatconst n => Mfloat64
end.
......@@ -81,7 +84,7 @@ Definition chunktype_unop (op: unary_operation) :=
| Ocast16unsigned => Mint16unsigned
| Ocast16signed => Mint16signed
| Onegint => Mint32
| Onotbool => Mint32
| Onotbool => Mint8unsigned
| Onotint => Mint32
| Onegf => Mfloat64
| Oabsf => Mfloat64
......@@ -92,7 +95,16 @@ Definition chunktype_unop (op: unary_operation) :=
| Ofloatofintu => Mfloat64
end.
Definition chunktype_binop (op: binary_operation) :=
Definition chunktype_logical_op (chunk1 chunk2: memory_chunk) :=
match chunk1, chunk2 with
| Mint8unsigned, Mint8unsigned => Mint8unsigned
| Mint8unsigned, Mint16unsigned => Mint16unsigned
| Mint16unsigned, Mint8unsigned => Mint16unsigned
| Mint16unsigned, Mint16unsigned => Mint16unsigned
| _, _ => Mint32
end.
Definition chunktype_binop (op: binary_operation) (chunk1 chunk2: memory_chunk) :=
match op with
| Oadd => Mint32
| Osub => Mint32
......@@ -101,9 +113,9 @@ Definition chunktype_binop (op: binary_operation) :=
| Odivu => Mint32
| Omod => Mint32
| Omodu => Mint32
| Oand => Mint32
| Oor => Mint32
| Oxor => Mint32
| Oand => chunktype_logical_op chunk1 chunk2
| Oor => chunktype_logical_op chunk1 chunk2
| Oxor => chunktype_logical_op chunk1 chunk2
| Oshl => Mint32
| Oshr => Mint32
| Oshru => Mint32
......@@ -119,7 +131,7 @@ Definition chunktype_binop (op: binary_operation) :=
Definition chunktype_compat (src dst: memory_chunk) : bool :=
match src, dst with
| Mint8unsigned, (Mint8unsigned|Mint16unsigned|Mint16signed|Mint32) => true
| Mint8signed, (Mint8signed|Mint16unsigned|Mint16signed|Mint32) => true
| Mint8signed, (Mint8signed|Mint16signed|Mint32) => true
| Mint16unsigned, (Mint16unsigned|Mint32) => true
| Mint16signed, (Mint16signed|Mint32) => true
| Mint32, Mint32 => true
......@@ -158,7 +170,9 @@ Fixpoint chunktype_expr (cenv: compilenv) (e: Csharpminor.expr)
| Csharpminor.Eunop op e1 =>
OK (chunktype_unop op)
| Csharpminor.Ebinop op e1 e2 =>
OK (chunktype_binop op)
do chunk1 <- chunktype_expr cenv e1;
do chunk2 <- chunktype_expr cenv e2;
OK (chunktype_binop op chunk1 chunk2)
| Csharpminor.Eload chunk e =>
OK chunk
| Csharpminor.Econdition e1 e2 e3 =>
......@@ -219,6 +233,18 @@ Definition make_stackaddr (ofs: Z): expr :=
Definition make_globaladdr (id: ident): expr :=
Econst (Oaddrsymbol id Int.zero).
(** Auxiliary to remove useless conversions. *)
Definition unop_is_cast (op: unary_operation) : option memory_chunk :=
match op with
| Ocast8unsigned => Some Mint8unsigned
| Ocast8signed => Some Mint8signed
| Ocast16unsigned => Some Mint16unsigned
| Ocast16signed => Some Mint16signed
| Osingleoffloat => Some Mfloat32
| _ => None
end.
(** Generation of a Cminor expression for reading a Csharpminor variable. *)
Definition var_get (cenv: compilenv) (id: ident): res expr :=
......@@ -308,7 +334,14 @@ Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
OK (Econst (transl_constant cst))
| Csharpminor.Eunop op e1 =>
do te1 <- transl_expr cenv e1;
OK (Eunop op te1)
match unop_is_cast op with
| None => OK (Eunop op te1)
| Some chunk =>
do chunk1 <- chunktype_expr cenv e1;
if chunktype_compat chunk1 chunk
then OK te1
else OK (Eunop op te1)
end
| Csharpminor.Ebinop op e1 e2 =>
do te1 <- transl_expr cenv e1;
do te2 <- transl_expr cenv e2;
......
cfrontend/Cminorgenproof.v
+ 99
− 14
View file @ ce0892a2
......@@ -215,13 +215,48 @@ Proof.
contradiction || reflexivity.
Qed.
Lemma chunktype_compat_correct:
forall src dst v,
chunktype_compat src dst = true ->
val_normalized v src -> val_normalized v dst.
Proof.
unfold val_normalized; intros. rewrite <- H0.
assert (A: 0 < 8 < Z_of_nat Int.wordsize). compute; auto.
assert (B: 0 < 16 < Z_of_nat Int.wordsize). compute; auto.
assert (C: 8 <= 16 < Z_of_nat Int.wordsize). omega.
destruct src; destruct dst; simpl in H; try discriminate; auto;
destruct v; simpl; auto.
rewrite Int.sign_ext_idem; auto.
rewrite Int.sign_ext_widen; auto.
rewrite Int.zero_ext_idem; auto.
rewrite Int.sign_zero_ext_widen; auto.
rewrite Int.zero_ext_widen; auto.
rewrite Int.sign_ext_widen; auto. omega.
rewrite Int.zero_ext_idem; auto.
rewrite Float.singleoffloat_idem; auto.
Qed.
Remark int_zero_ext_small:
forall x n,
0 <= Int.unsigned x < two_p n ->
Int.zero_ext n x = x.
Proof.
intros. unfold Int.zero_ext. rewrite Zmod_small; auto. apply Int.repr_unsigned.
Qed.
Lemma chunktype_const_correct:
forall c v,
Csharpminor.eval_constant c = Some v ->
val_normalized v (chunktype_const c).
Proof.
unfold Csharpminor.eval_constant; intros.
destruct c; inv H; unfold val_normalized; auto.
destruct c; inv H; unfold val_normalized; simpl.
case_eq (Int.ltu i (Int.repr 256)); intros.
simpl. decEq. apply int_zero_ext_small. exact (Int.ltu_inv _ _ H).
case_eq (Int.ltu i (Int.repr 65536)); intros.
simpl. decEq. apply int_zero_ext_small. exact (Int.ltu_inv _ _ H0).
simpl; auto.
auto.
Qed.
Lemma chunktype_unop_correct:
......@@ -246,10 +281,42 @@ Proof.
destruct v1; inv H; auto.
Qed.
Lemma chunktype_logical_op_correct:
forall (logop: int -> int -> int)
(DISTR: forall a b c, logop (Int.and a c) (Int.and b c) =
Int.and (logop a b) c)
n1 c1 n2 c2,
val_normalized (Vint n1) c1 -> val_normalized (Vint n2) c2 ->
val_normalized (Vint (logop n1 n2)) (chunktype_logical_op c1 c2).
Proof.
intros. set (c := chunktype_logical_op c1 c2).
assert (val_normalized (Vint n1) c /\ val_normalized (Vint n2) c).
unfold c, chunktype_logical_op.
destruct c1; destruct c2; split; try (auto; unfold val_normalized; reflexivity).
apply chunktype_compat_correct with Mint8unsigned; auto.
apply chunktype_compat_correct with Mint8unsigned; auto.
destruct H1.
assert (c = Mint8unsigned \/ c = Mint16unsigned \/ c = Mint32).
unfold c. destruct c1; auto; destruct c2; auto.
destruct H3 as [A | [A | A]]; rewrite A in *.
unfold val_normalized in *. simpl in *.
assert (0 < 8 < Z_of_nat Int.wordsize). compute; auto.
rewrite Int.zero_ext_and in *; auto.
set (m := Int.repr (two_p 8 - 1)) in *.
rewrite <- DISTR. congruence.
unfold val_normalized in *. simpl in *.
assert (0 < 16 < Z_of_nat Int.wordsize). compute; auto.
rewrite Int.zero_ext_and in *; auto.
set (m := Int.repr (two_p 16 - 1)) in *.
rewrite <- DISTR. congruence.
red. auto.
Qed.
Lemma chunktype_binop_correct:
forall op v1 v2 m v,
forall op v1 v2 c1 c2 m v,
Csharpminor.eval_binop op v1 v2 m = Some v ->
val_normalized v (chunktype_binop op).
val_normalized v1 c1 -> val_normalized v2 c2 ->
val_normalized v (chunktype_binop op c1 c2).
Proof.
intros; destruct op; simpl in *; unfold val_normalized;
destruct v1; destruct v2; try (inv H; reflexivity).
......@@ -258,6 +325,15 @@ Proof.
destruct (Int.eq i0 Int.zero); inv H; auto.
destruct (Int.eq i0 Int.zero); inv H; auto.
destruct (Int.eq i0 Int.zero); inv H; auto.
inv H. apply chunktype_logical_op_correct; auto.
intros. repeat rewrite Int.and_assoc. decEq.
rewrite (Int.and_commut b c). rewrite <- Int.and_assoc. rewrite Int.and_idem. auto.
inv H. apply chunktype_logical_op_correct; auto.
intros. rewrite (Int.and_commut a c). rewrite (Int.and_commut b c).
rewrite <- Int.and_or_distrib. apply Int.and_commut.
inv H. apply chunktype_logical_op_correct; auto.
intros. rewrite (Int.and_commut a c). rewrite (Int.and_commut b c).
rewrite <- Int.and_xor_distrib. apply Int.and_commut.
destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
......@@ -269,21 +345,11 @@ Proof.
destruct (Mem.valid_pointer m b (Int.signed i) &&
Mem.valid_pointer m b0 (Int.signed i0)).
destruct (eq_block b b0); inv H. destruct (Int.cmp c i i0); auto.
destruct c; inv H1; auto. inv H.
destruct c; inv H3; auto. inv H.
inv H. destruct (Int.cmpu c i i0); auto.
inv H. destruct (Float.cmp c f f0); auto.
Qed.
Lemma chunktype_compat_correct:
forall src dst v,
chunktype_compat src dst = true ->
val_normalized v src -> val_normalized v dst.
Proof.
unfold val_normalized; intros. rewrite <- H0.
destruct src; destruct dst; simpl in H; try discriminate; auto;
destruct v; simpl; auto.
Admitted.
Lemma chunktype_merge_correct:
forall c1 c2 c v,
chunktype_merge c1 c2 = OK c ->
......@@ -301,6 +367,7 @@ Proof.
rewrite e. apply val_normalized_has_type. auto.
Qed.
(** * Correspondence between Csharpminor's and Cminor's environments and memory states *)
(** In Csharpminor, every variable is stored in a separate memory block.
......@@ -1482,6 +1549,14 @@ Proof.
eapply eval_Econst. simpl. rewrite H. auto.
Qed.
Lemma unop_is_cast_correct:
forall op chunk v,
unop_is_cast op = Some chunk ->
Csharpminor.eval_unop op v = Some (Val.load_result chunk v).
Proof.
intros. destruct op; simpl in H; inv H; reflexivity.
Qed.
(** Correctness of [make_store]. *)
Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=
......@@ -2394,6 +2469,16 @@ Proof.
(* Eunop *)
exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
exploit eval_unop_compat; eauto. intros [tv [EVAL INJ]].
revert EQ0. case_eq (unop_is_cast op); intros; monadInv EQ0.
revert EQ2. case_eq (chunktype_compat x0 m0); intros; monadInv EQ2.
exploit unop_is_cast_correct; eauto. instantiate (1 := v1); intros.
assert (val_normalized v1 m0).
eapply chunktype_compat_correct; eauto.
eapply chunktype_expr_correct; eauto.
red in H4.
assert (v = v1) by congruence. subst v.
exists tv1; auto.
exists tv; split. econstructor; eauto. auto.
exists tv; split. econstructor; eauto. auto.
(* Ebinop *)
exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment