32-bit modulo now uses sign extend then call to the 64-bit function

5 files changed, 60 insertions, 27 deletions

diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 3529a36f..991dd3f0 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -181,3 +181,39 @@ Proof.
   pose proof modulus_fits_64.
   omega.
 Qed.
+  
+Theorem modu_is_modlu: forall v1 v2 : val,
+    Val.modu v1 v2 =
+    match Val.modlu (Val.longofintu v1) (Val.longofintu v2) with
+    | None => None
+    | Some q => Some (Val.loword q)
+    end.
+Proof.
+  intros.
+  destruct v1; simpl; trivial.
+  destruct v2; simpl; trivial.
+  destruct i as [i_val i_range].
+  destruct i0 as [i0_val i0_range].
+  simpl.
+  unfold Int.eq, Int64.eq, Int.zero, Int64.zero.
+  simpl.
+  rewrite Int.unsigned_repr by (compute; split; discriminate).
+  rewrite (Int64.unsigned_repr 0) by (compute; split; discriminate).
+  rewrite (unsigned64_repr i0_val) by assumption.
+  destruct (zeq i0_val 0) as [ | Hnot0]; simpl; trivial.
+  f_equal. f_equal.
+  unfold Int.modu, Int64.modu. simpl.
+  rewrite (unsigned64_repr i_val) by assumption.
+  rewrite (unsigned64_repr i0_val) by assumption.
+  unfold Int64.loword.
+  rewrite Int64.unsigned_repr.
+  reflexivity.
+  assert((i_val mod i0_val) < i0_val).
+  apply Z_mod_lt.
+  omega.
+  split.
+  { apply Z_mod_lt.
+    omega. }
+  pose proof modulus_fits_64.
+  omega.
+Qed.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index c4b01d89..aac3010e 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -430,7 +430,11 @@ Definition divu_base (e1: expr) (e2: expr) :=
       :::Enil).
   
 Definition modu_base (e1: expr) (e2: expr) :=
-  Eexternal i32_umod sig_ii_i (e1 ::: e2 ::: Enil).
+  Eop Olowlong
+     ((Eexternal i64_umod sig_ll_l
+       ((Eop Ocast32unsigned (e1 ::: Enil)):::
+       (Eop Ocast32unsigned (e2 ::: Enil))::: Enil))
+      :::Enil).
 
 Definition shrximm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 2730ee91..d22725d5 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -899,8 +899,24 @@ Theorem eval_modu_base:
     Val.modu x y = Some z ->
     exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold modu_base.
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  intros until z.
+  intros Hax Hby Hmod. unfold modu_base.
+  pose proof (modu_is_modlu x y) as MODU.
+  destruct (Val.modlu (Val.longofintu x) (Val.longofintu y))
+    as [ ql | ] eqn:Emod.
+  { TrivialExists.
+    { econstructor. eapply eval_helper_2; eauto.
+      { econstructor. econstructor. eassumption.
+       constructor. simpl. reflexivity. }
+      { econstructor. econstructor. eassumption.
+        constructor. simpl. reflexivity. }
+      { DeclHelper. }
+      { UseHelper. }
+      constructor. }
+    simpl.
+    congruence.
+  }
+  congruence.
 Qed.
 
 Theorem eval_shrximm:
diff --git a/runtime/mppa_k1c/i64_umod.c b/runtime/mppa_k1c/i64_umod.c
index f6fed4c4..e69de29b 100644
--- a/runtime/mppa_k1c/i64_umod.c
+++ b/runtime/mppa_k1c/i64_umod.c
@@ -1,23 +0,0 @@
-#ifdef COMPLIQUE
-unsigned long long
-udivmoddi4(unsigned long long num, unsigned long long den, int modwanted);
-
-unsigned long long
-i64_umod (unsigned long long a, unsigned long long b)
-{
-  return udivmoddi4 (a, b, 1);
-}
-
-#else
-extern unsigned long __umoddi3 (unsigned long a, unsigned long b);
-
-unsigned long i64_umod (unsigned long a, unsigned long b)
-{
-  return __umoddi3 (a, b);
-}
-
-unsigned int i32_umod (unsigned int a, unsigned int b)
-{
-  return __umoddi3 (a, b);
-}
-#endif
diff --git a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c b/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c
index 4dc333dd..6a4db4c3 100644
--- a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c
+++ b/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c
@@ -58,7 +58,7 @@ DM_INLINE void Lustre_arrow_3_step(_real i1[50],_real i2[50],_real out[50]/*out*
 } // End of Lustre_arrow_3_step
 
 // Step function(s) for Lustre_hat_ctx
-void Lustre_hat_step(_real i1,_real out[50]/*out*/){
+DM_INLINE void Lustre_hat_step(_real i1,_real out[50]/*out*/){
   out[0] = i1;
   out[1] = i1;
   out[2] = i1;