ça recompile sur x86

15 files changed, 166 insertions, 110 deletions

diff --git a/Makefile b/Makefile
index ed9059db..d8cd428a 100644
--- a/Makefile
+++ b/Makefile
@@ -72,7 +72,7 @@ COMMON=Errors.v AST.v Linking.v \
 # Back-end modules (in backend/, $(ARCH)/)
 
 BACKEND=\
-  Cminor.v Op.v CminorSel.v \
+  Cminor.v Op.v CminorSel.v OpHelpers.v OpHelpersproof.v \
   SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \
   SelectOpproof.v SelectDivproof.v SplitLongproof.v \
   SelectLongproof.v Selectionproof.v \
diff --git a/backend/OpHelpers.v b/backend/OpHelpers.v
new file mode 100644
index 00000000..53414dab
--- /dev/null
+++ b/backend/OpHelpers.v
@@ -0,0 +1,42 @@
+Require Import Coqlib.
+Require Import AST Integers Floats.
+Require Import Op CminorSel.
+
+(** Some arithmetic operations 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.
+Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default.
+Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) 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 *)
+  f64_div: ident;                       (**float division*)
+  f32_div: ident;                       (**float division*)
+}.
diff --git a/backend/OpHelpersproof.v b/backend/OpHelpersproof.v
new file mode 100644
index 00000000..63040c5f
--- /dev/null
+++ b/backend/OpHelpersproof.v
@@ -0,0 +1,78 @@
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Cminor.
+Require Import Op.
+Require Import CminorSel.
+Require Import Events.
+Require Import OpHelpers.
+
+(** * 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 arith_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.divs x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z)
+ /\ (forall x y z, Val.divu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z)
+ /\ (forall x y z, Val.mods x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z)
+ /\ (forall x y z, Val.modu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z)
+ /\ (forall x y z, Val.divfs x y = z -> external_implements "__compcert_f32_div" sig_ss_s (x::y::nil) z)
+ /\ (forall x y z, Val.divf x y = z -> external_implements "__compcert_f64_div" sig_ff_f (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
+  /\ helper_declared p f32_div  "__compcert_f32_div"  sig_ss_s
+  /\ helper_declared p f64_div  "__compcert_f64_div"  sig_ff_f
+.
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 7241d028..9f852616 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -15,7 +15,7 @@
 Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats.
-Require Import Op CminorSel SelectOp SplitLong SelectLong.
+Require Import Op CminorSel OpHelpers SelectOp SplitLong SelectLong.
 
 Local Open Scope cminorsel_scope.
 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index dbd3f58d..e2249ddb 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -15,6 +15,7 @@
 Require Import Zquot Coqlib.
 Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv.
 
 Local Open Scope cminorsel_scope.
diff --git a/backend/Selection.v b/backend/Selection.v
index aba84049..05a06abf 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -26,7 +26,7 @@ Require String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Globalenvs Switch.
 Require Cminor.
-Require Import Op CminorSel.
+Require Import Op CminorSel OpHelpers.
 Require Import SelectOp SplitLong SelectLong SelectDiv.
 Require Machregs.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 5a0fafaf..50ff377a 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -16,6 +16,7 @@ Require Import FunInd.
 Require Import Coqlib Maps.
 Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep.
 Require Import Switch Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectDiv SplitLong SelectLong Selection.
 Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof.
 
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index 6a7d4f5c..dfe42df0 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -16,6 +16,7 @@ Require String.
 Require Import Coqlib.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
+Require Import OpHelpers.
 Require Import SelectOp.
 
 Local Open Scope cminorsel_scope.
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index a74276c7..6718ba5b 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -16,6 +16,7 @@ Require Import String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Floats.
 Require Import Values Memory Globalenvs Events Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong.
 
 Local Open Scope cminorsel_scope.
@@ -33,7 +34,7 @@ Variable sp: val.
 Variable e: env.
 Variable m: mem.
 
-Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto.
+Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto.
 Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.
 
 Lemma eval_helper:
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 19712d2f..f6605c11 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -50,6 +50,7 @@ Require Import Integers.
 Require Import Floats.
 Require Import Op.
 Require Import CminorSel.
+Require Import OpHelpers.
 
 Local Open Scope cminorsel_scope.
 
@@ -57,44 +58,6 @@ 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.
-Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default.
-Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) 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 *)
-  f64_div: ident;                       (**float division*)
-  f32_div: ident;                       (**float division*)
-}.
 
 Context {hf: helper_functions}.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index a4a5f72b..111c08e4 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -35,71 +35,6 @@ 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.divs x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z)
- /\ (forall x y z, Val.divu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z)
- /\ (forall x y z, Val.mods x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z)
- /\ (forall x y z, Val.modu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z)
- /\ (forall x y z, Val.divfs x y = z -> external_implements "__compcert_f32_div" sig_ss_s (x::y::nil) z)
- /\ (forall x y z, Val.divf x y = z -> external_implements "__compcert_f64_div" sig_ff_f (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
-  /\ helper_declared p f32_div  "__compcert_f32_div"  sig_ss_s
-  /\ helper_declared p f64_div  "__compcert_f64_div"  sig_ff_f
-.
-
 (** * Useful lemmas and tactics *)
 
 (** The following are trivial lemmas and custom tactics that help
diff --git a/x86/SelectLong.vp b/x86/SelectLong.vp
index b213e23f..4f9fb518 100644
--- a/x86/SelectLong.vp
+++ b/x86/SelectLong.vp
@@ -16,7 +16,7 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
-Require Import SelectOp SplitLong.
+Require Import OpHelpers SelectOp SplitLong.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v
index 3bef632d..f008f39e 100644
--- a/x86/SelectLongproof.v
+++ b/x86/SelectLongproof.v
@@ -16,6 +16,7 @@ Require Import String Coqlib Maps Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
 
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index a1583600..eadda093 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -40,6 +40,7 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
+Require Import OpHelpers.
 
 Local Open Scope cminorsel_scope.
 
@@ -540,3 +541,10 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
   | _ => BA e
   end.
+
+(* floats *)
+Definition divf_base (e1: expr) (e2: expr) :=
+  Eop Odivf (e1 ::: e2 ::: Enil).
+
+Definition divfs_base (e1: expr) (e2: expr) :=
+  Eop Odivfs (e1 ::: e2 ::: Enil).
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index fdbadaa8..1eeb5906 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -23,6 +23,8 @@ Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 
@@ -74,8 +76,10 @@ Ltac TrivialExists :=
 (** * Correctness of the smart constructors *)
 
 Section CMCONSTR.
-
-Variable ge: genv.
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
@@ -984,4 +988,25 @@ Proof.
 - constructor; auto.
 Qed.
 
+
+(* floating-point division without HELPERS *)
+Theorem eval_divf_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v.
+Proof.
+  intros; unfold divf_base.
+  TrivialExists.
+Qed.
+
+Theorem eval_divfs_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+  intros; unfold divfs_base.
+  TrivialExists.
+Qed.
 End CMCONSTR.