diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 17:27:48 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 17:27:48 +0200 |
| commit | fc8f28be257464c7b169a61b079ba19675f08e35 (patch) | |
| tree | 05535928e3d87e0741c9c81026aea1dc72e09473 | |
| parent | 65ab86a0e3df080ca9a1c37631904d8d02c07596 (diff) | |
| download | compcert-fc8f28be257464c7b169a61b079ba19675f08e35.tar.gz compcert-fc8f28be257464c7b169a61b079ba19675f08e35.zip | |
x86-32: make sure is_longconst and mullimm work correctly in 32 bits
SelectLong.is_longconst was always returning 'false' in 32 bits.
SelectLong.mullimm was generating a Omullimm insn even in 32 bits.
Both functions are used by SelectDiv.
| -rw-r--r-- | ia32/SelectLong.vp | 4 | ||||
| -rw-r--r-- | ia32/SelectLongproof.v | 16 |
2 files changed, 11 insertions, 9 deletions
diff --git a/ia32/SelectLong.vp b/ia32/SelectLong.vp index 2869f823..b213e23f 100644 --- a/ia32/SelectLong.vp +++ b/ia32/SelectLong.vp @@ -29,6 +29,7 @@ Definition longconst (n: int64) : expr := if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil. Definition is_longconst (e: expr) := + if Archi.splitlong then SplitLong.is_longconst e else match e with | Eop (Olongconst n) Enil => Some n | _ => None @@ -269,7 +270,8 @@ Definition mullimm_base (n1: int64) (e2: expr) := end. Nondetfunction mullimm (n1: int64) (e2: expr) := - if Int64.eq n1 Int64.zero then longconst Int64.zero + if Archi.splitlong then SplitLong.mullimm n1 e2 + else if Int64.eq n1 Int64.zero then longconst Int64.zero else if Int64.eq n1 Int64.one then e2 else match e2 with | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2) diff --git a/ia32/SelectLongproof.v b/ia32/SelectLongproof.v index 14b0bcce..a3d2bb19 100644 --- a/ia32/SelectLongproof.v +++ b/ia32/SelectLongproof.v @@ -66,17 +66,15 @@ Proof. EvalOp. Qed. -Lemma is_longconst_sound_1: - forall a n, is_longconst a = Some n -> a = Eop (Olongconst n) Enil. -Proof with (try discriminate). - unfold is_longconst; intros. destruct a... destruct o... destruct e0... congruence. -Qed. - Lemma is_longconst_sound: forall v a n le, is_longconst a = Some n -> eval_expr ge sp e m le a v -> v = Vlong n. -Proof. - intros. rewrite (is_longconst_sound_1 _ _ H) in H0. InvEval. auto. +Proof with (try discriminate). + intros. unfold is_longconst in *. destruct Archi.splitlong. + eapply SplitLongproof.is_longconst_sound; eauto. + assert (a = Eop (Olongconst n) Enil). + { destruct a... destruct o... destruct e0... congruence. } + subst a. InvEval. auto. Qed. Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword. @@ -401,6 +399,8 @@ Qed. Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). Proof. unfold mullimm. intros; red; intros. + destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_mullimm; eauto. predSpec Int64.eq Int64.eq_spec n Int64.zero. exists (Vlong Int64.zero); split. apply eval_longconst. destruct x; simpl; auto. subst n; rewrite Int64.mul_zero; auto. |