Update ARM port. Not tested yet.

3 files changed, 8 insertions, 7 deletions

diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 41db3c70..3180a55d 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -713,7 +713,8 @@ Lemma eval_modl_from_divl:
 Proof.
   unfold modl_from_divl; intros.
   exploit eval_mullimm; eauto. instantiate (1 := n). intros (v1 & A1 & B1).
-  exploit (eval_subl prog sp e m le (Eletvar O)). constructor; eauto. eexact A1.
+  assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)) by (constructor; auto).
+  exploit eval_subl; auto. eexact A0. eexact A1.
   intros (v2 & A2 & B2).
   simpl in B1; inv B1. simpl in B2; inv B2. exact A2.
 Qed.
@@ -798,7 +799,7 @@ Proof.
   assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)).
   { constructor; auto. }
   exploit eval_mullhs. eauto. eexact A0. instantiate (1 := Int64.repr M).  intros (v1 & A1 & B1).
-  exploit eval_addl. eexact A1. eexact A0. intros (v2 & A2 & B2).
+  exploit eval_addl; auto. eexact A1. eexact A0. intros (v2 & A2 & B2).
   exploit eval_shrluimm. eauto. eexact A0. instantiate (1 := Int.repr 63). intros (v3 & A3 & B3).
   set (a4 := if zlt M Int64.half_modulus
              then mullhs (Eletvar 0) (Int64.repr M)
@@ -807,7 +808,7 @@ Proof.
   assert (A4: eval_expr ge sp e m le a4 v4). 
   { unfold a4, v4; destruct (zlt M Int64.half_modulus); auto. }
   exploit eval_shrlimm. eauto. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5).
-  exploit eval_addl. eexact A5. eexact A3. intros (v6 & A6 & B6).
+  exploit eval_addl; auto. eexact A5. eexact A3. intros (v6 & A6 & B6).
   assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true).
   { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto.
     assert (64 < Int.max_unsigned) by (compute; auto). omega. }
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index f7eeebd0..60d8e4c4 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -241,7 +241,7 @@ Definition mull_base (e1 e2: expr) :=
              (mul (lift h1) (lift l2)))
         (Eop Olowlong (Eletvar O ::: Enil)))).
 
-Definition mullimm (e: expr) (n: int64) :=
+Definition mullimm (n: int64) (e: expr) :=
   if Int64.eq n Int64.zero then longconst Int64.zero else
   if Int64.eq n Int64.one then e else
   match Int64.is_power2' n with
@@ -252,8 +252,8 @@ Definition mullimm (e: expr) (n: int64) :=
 Definition mull (e1 e2: expr) :=
   match is_longconst e1, is_longconst e2 with
   | Some n1, Some n2 => longconst (Int64.mul n1 n2)
-  | Some n1, _ => mullimm e2 n1
-  | _, Some n2 => mullimm e1 n2
+  | Some n1, _ => mullimm n1 e2
+  | _, Some n2 => mullimm n2 e1
   | _, _ => mull_base e1 e2
   end.
 
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index 31f5db67..07759dc9 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -791,7 +791,7 @@ Proof.
 Qed.
 
 Lemma eval_mullimm:
-  forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)).
+  forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)).
 Proof.
   unfold mullimm; red; intros.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.