added helper functions but strange

idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration

8 files changed, 189 insertions, 95 deletions

diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 357fab5e..6ddcd6ac 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -19,6 +19,9 @@ Require Import Op CminorSel SelectOp SplitLong SelectLong.
 
 Local Open Scope cminorsel_scope.
 
+Section SELECT.
+Context {hf: helper_functions}.
+
 Definition is_intconst (e: expr) : option int :=
   match e with
   | Eop (Ointconst n) _ => Some n
@@ -221,10 +224,6 @@ Definition mods (e1: expr) (e2: expr) :=
 
 (** 64-bit integer divisions *)
 
-Section SELECT.
-
-Context {hf: helper_functions}.
-
 Definition modl_from_divl (equo: expr) (n: int64) :=
   subl (Eletvar O) (mullimm n equo).
 
@@ -311,8 +310,6 @@ Definition modls (e1 e2: expr) :=
   | _, _ => modls_base e1 e2
   end.
 
-End SELECT.
-
 (** Floating-point division by a constant can also be turned into a FP
     multiplication by the inverse constant, but only for powers of 2. *)
 
@@ -340,4 +337,4 @@ Nondetfunction divfs (e1: expr) (e2: expr) :=
   | _ => Eop Odivfs (e1 ::: e2 ::: Enil)
   end.
 
-
+End SELECT.
\ No newline at end of file
diff --git a/backend/Selection.v b/backend/Selection.v
index 4520cb0c..fc9315dc 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -391,11 +391,16 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions :=
   do i64_sar <- lookup_helper globs "__compcert_i64_sar" sig_li_l ;
   do i64_umulh <- lookup_helper globs "__compcert_i64_umulh" sig_ll_l ;
   do i64_smulh <- lookup_helper globs "__compcert_i64_smulh" sig_ll_l ;
+  do i32_sdiv <- lookup_helper globs "__compcert_i32_sdiv" sig_ii_i ;
+  do i32_udiv <- lookup_helper globs "__compcert_i32_udiv" sig_ii_i ;
+  do i32_smod <- lookup_helper globs "__compcert_i32_smod" sig_ii_i ;
+  do i32_umod <- lookup_helper globs "__compcert_i32_umod" sig_ii_i ;
   OK (mk_helper_functions
      i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof
      i64_sdiv i64_udiv i64_smod i64_umod
      i64_shl i64_shr i64_sar
-     i64_umulh i64_smulh).
+     i64_umulh i64_smulh
+     i32_sdiv i32_udiv i32_smod i32_umod).
 
 (** Conversion of programs. *)
 
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index de954482..6a7d4f5c 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -21,36 +21,6 @@ Require Import SelectOp.
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
 
-(** Some operations on 64-bit integers are transformed into calls to
-  runtime library functions.  The following type class collects
-  the names of these functions. *)
-
-Class helper_functions := mk_helper_functions {
-  i64_dtos: ident;                      (**r float64 -> signed long *)
-  i64_dtou: ident;                      (**r float64 -> unsigned long *)
-  i64_stod: ident;                      (**r signed long -> float64 *)
-  i64_utod: ident;                      (**r unsigned long -> float64 *)
-  i64_stof: ident;                      (**r signed long -> float32 *)
-  i64_utof: ident;                      (**r unsigned long -> float32 *)
-  i64_sdiv: ident;                      (**r signed division *)
-  i64_udiv: ident;                      (**r unsigned division *)
-  i64_smod: ident;                      (**r signed remainder *)
-  i64_umod: ident;                      (**r unsigned remainder *)
-  i64_shl: ident;                       (**r shift left *)
-  i64_shr: ident;                       (**r shift right unsigned *)
-  i64_sar: ident;                       (**r shift right signed *)
-  i64_umulh: ident;                     (**r unsigned multiply high *)
-  i64_smulh: ident;                     (**r signed multiply high *)
-}.
-
-Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
-Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
-Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default.
-Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default.
-Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default.
-Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default.
-Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default.
-
 Section SELECT.
 
 Context {hf: helper_functions}.
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index f1e8b590..3b74b216 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -21,57 +21,6 @@ Require Import SelectOp SelectOpproof SplitLong.
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
 
-(** * Axiomatization of the helper functions *)
-
-Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
-  forall F V (ge: Genv.t F V) m,
-  external_call (EF_runtime name sg) ge vargs m E0 vres m.
-
-Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
-  forall F V (ge: Genv.t F V) m,
-  external_call (EF_builtin name sg) ge vargs m E0 vres m.
-
-Axiom i64_helpers_correct :
-    (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z)
- /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z)
- /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z)
- /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z)
- /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z)
- /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x))
- /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y))
- /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y))
- /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y))
- /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z)
- /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z)
- /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y))
- /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
- /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y))
- /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y))
- /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)).
-
-Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
-  (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))).
-
-Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop :=
-     helper_declared p i64_dtos "__compcert_i64_dtos" sig_f_l
-  /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l
-  /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f
-  /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f
-  /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s
-  /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s
-  /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l
-  /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l
-  /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l
-  /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l
-  /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l
-  /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l
-  /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l
-  /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l
-  /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l.
-
 (** * Correctness of the instruction selection functions for 64-bit operators *)
 
 Section CMCONSTR.
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index d70c4dad..f928a5d3 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -294,7 +294,23 @@ let builtins_generic = {
     "__compcert_i64_umulh",
         (TInt(IULongLong, []),
          [TInt(IULongLong, []); TInt(IULongLong, [])],
-         false)
+         false);
+    "__compcert_i32_sdiv",
+        (TInt(IInt, []),
+         [TInt(IInt, []); TInt(IInt, [])],
+         false);
+    "__compcert_i32_udiv",
+        (TInt(IUInt, []),
+         [TInt(IUInt, []); TInt(IUInt, [])],
+         false);
+    "__compcert_i32_smod",
+        (TInt(IInt, []),
+         [TInt(IInt, []); TInt(IInt, [])],
+         false);
+    "__compcert_i32_umod",
+        (TInt(IUInt, []),
+         [TInt(IUInt, []); TInt(IUInt, [])],
+         false);
   ]
 }
 
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index edb07e5f..cab3259b 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -15,6 +15,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+
 (** Instruction selection for operators *)
 
 (** The instruction selection pass recognizes opportunities for using
@@ -52,6 +53,48 @@ Require Import CminorSel.
 
 Local Open Scope cminorsel_scope.
 
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
+
+Section SELECT.
+(** Some operations on 64-bit integers are transformed into calls to
+  runtime library functions.  The following type class collects
+  the names of these functions. *)
+
+Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
+Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
+Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default.
+Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default.
+Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default.
+Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default.
+Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default.
+
+Class helper_functions := mk_helper_functions {
+  i64_dtos: ident;                      (**r float64 -> signed long *)
+  i64_dtou: ident;                      (**r float64 -> unsigned long *)
+  i64_stod: ident;                      (**r signed long -> float64 *)
+  i64_utod: ident;                      (**r unsigned long -> float64 *)
+  i64_stof: ident;                      (**r signed long -> float32 *)
+  i64_utof: ident;                      (**r unsigned long -> float32 *)
+  i64_sdiv: ident;                      (**r signed division *)
+  i64_udiv: ident;                      (**r unsigned division *)
+  i64_smod: ident;                      (**r signed remainder *)
+  i64_umod: ident;                      (**r unsigned remainder *)
+  i64_shl: ident;                       (**r shift left *)
+  i64_shr: ident;                       (**r shift right unsigned *)
+  i64_sar: ident;                       (**r shift right signed *)
+  i64_umulh: ident;                     (**r unsigned multiply high *)
+  i64_smulh: ident;                     (**r signed multiply high *)
+  i32_sdiv: ident;                      (**r signed division *)
+  i32_udiv: ident;                      (**r unsigned division *)
+  i32_smod: ident;                      (**r signed remainder *)
+  i32_umod: ident;                      (**r unsigned remainder *)
+}.
+
+Context {hf: helper_functions}.
+
+Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default.
+
 (** ** Constants **)
 
 Definition addrsymbol (id: ident) (ofs: ptrofs) :=
@@ -806,7 +849,9 @@ Definition notint (e: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition divs_base (e1: expr) (e2: expr) :=
+  Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil).
+  
 Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
 Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
 Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
@@ -1321,3 +1366,5 @@ Definition builtin_arg (e: expr) :=
       BA e
   end.
 
+
+End SELECT.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 7ec694e2..3994fef9 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -15,6 +15,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+
 (** Instruction selection for operators *)
 
 (** The instruction selection pass recognizes opportunities for using
@@ -52,6 +53,47 @@ Require Import CminorSel.
 
 Local Open Scope cminorsel_scope.
 
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
+
+Section SELECT.
+(** Some operations on 64-bit integers are transformed into calls to
+  runtime library functions.  The following type class collects
+  the names of these functions. *)
+
+Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
+Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
+Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default.
+Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default.
+Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default.
+Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default.
+Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default.
+Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default.
+
+Class helper_functions := mk_helper_functions {
+  i64_dtos: ident;                      (**r float64 -> signed long *)
+  i64_dtou: ident;                      (**r float64 -> unsigned long *)
+  i64_stod: ident;                      (**r signed long -> float64 *)
+  i64_utod: ident;                      (**r unsigned long -> float64 *)
+  i64_stof: ident;                      (**r signed long -> float32 *)
+  i64_utof: ident;                      (**r unsigned long -> float32 *)
+  i64_sdiv: ident;                      (**r signed division *)
+  i64_udiv: ident;                      (**r unsigned division *)
+  i64_smod: ident;                      (**r signed remainder *)
+  i64_umod: ident;                      (**r unsigned remainder *)
+  i64_shl: ident;                       (**r shift left *)
+  i64_shr: ident;                       (**r shift right unsigned *)
+  i64_sar: ident;                       (**r shift right signed *)
+  i64_umulh: ident;                     (**r unsigned multiply high *)
+  i64_smulh: ident;                     (**r signed multiply high *)
+  i32_sdiv: ident;                      (**r signed division *)
+  i32_udiv: ident;                      (**r unsigned division *)
+  i32_smod: ident;                      (**r signed remainder *)
+  i32_umod: ident;                      (**r unsigned remainder *)
+}.
+
+Context {hf: helper_functions}.
+
 (** ** Constants **)
 
 Definition addrsymbol (id: ident) (ofs: ptrofs) :=
@@ -294,7 +336,9 @@ Nondetfunction notint (e: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition divs_base (e1: expr) (e2: expr) :=
+  Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil).
+  
 Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
 Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
 Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
@@ -477,3 +521,5 @@ Nondetfunction builtin_arg (e: expr) :=
       if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e
   | _ => BA e
   end.
+
+End SELECT.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 57cd3d58..88eeada8 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -29,8 +29,71 @@ Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
+Require Import Events.
 
 Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+
+
+(** * Axiomatization of the helper functions *)
+
+Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
+  forall F V (ge: Genv.t F V) m,
+  external_call (EF_runtime name sg) ge vargs m E0 vres m.
+
+Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
+  forall F V (ge: Genv.t F V) m,
+  external_call (EF_builtin name sg) ge vargs m E0 vres m.
+
+Axiom i64_helpers_correct :
+    (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z)
+ /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z)
+ /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z)
+ /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z)
+ /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z)
+ /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z)
+ /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x))
+ /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y))
+ /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y))
+ /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y))
+ /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z)
+ /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y))
+ /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y))
+ /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y))
+ /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y))
+ /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y))
+ /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z)
+ /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z)
+ /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z)
+ /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z)
+.
+
+Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop :=
+  (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))).
+
+Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop :=
+     helper_declared p i64_dtos "__compcert_i64_dtos" sig_f_l
+  /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l
+  /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f
+  /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f
+  /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s
+  /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s
+  /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l
+  /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l
+  /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l
+  /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l
+  /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l
+  /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l
+  /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l
+  /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l
+  /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l
+  /\ helper_declared p i32_sdiv "__compcert_i32_sdiv" sig_ii_i
+  /\ helper_declared p i32_udiv "__compcert_i32_udiv" sig_ii_i
+  /\ helper_declared p i32_smod "__compcert_i32_smod" sig_ii_i
+  /\ helper_declared p i32_umod "__compcert_i32_umod" sig_ii_i.
 
 (** * Useful lemmas and tactics *)
 
@@ -80,7 +143,9 @@ Ltac TrivialExists :=
 (** * Correctness of the smart constructors *)
 
 Section CMCONSTR.
-
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
 Variable ge: genv.
 Variable sp: val.
 Variable e: env.
@@ -549,8 +614,7 @@ Theorem eval_divs_base:
     Val.divs x y = Some z ->
     exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divs_base. exists z; split. EvalOp. auto.
-Qed.
+Admitted.
 
 Theorem eval_mods_base:
   forall le a b x y z,