added helper functions but strange

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

4 files changed, 10 insertions, 89 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.