From fc8f28be257464c7b169a61b079ba19675f08e35 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 25 Oct 2016 17:27:48 +0200
Subject: 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.
---
 ia32/SelectLong.vp     |  4 +++-
 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.
-- 
cgit