6 files changed, 43 insertions, 4 deletions
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index ce5c67f6..14c75155 100644
--- a/arm/Machregsaux.ml
+++ b/arm/Machregsaux.ml
@@ -33,3 +33,8 @@ let register_by_name s =
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/arm/Machregsaux.mli
+++ b/arm/Machregsaux.mli
@@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
 val can_reserve_register: Machregs.mreg -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/arm/SelectLong.vp b/arm/SelectLong.vp
index cc7a38f6..b4cdd0e3 100644
--- a/arm/SelectLong.vp
+++ b/arm/SelectLong.vp
@@ -16,6 +16,6 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
-Require Import SelectOp SplitLong.
+Require Import OpHelpers SelectOp SplitLong.
 
 (** This file is empty because we use the default implementation provided in [SplitLong]. *)
diff --git a/arm/SelectLongproof.v b/arm/SelectLongproof.v
index a82c082c..a65a38d4 100644
--- a/arm/SelectLongproof.v
+++ b/arm/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/arm/SelectOp.vp b/arm/SelectOp.vp
index 1220abc4..5506157c 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -39,7 +39,7 @@
 Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats Builtins.
-Require Import Op CminorSel.
+Require Import Op OpHelpers CminorSel.
 
 Local Open Scope cminorsel_scope.
 
@@ -516,6 +516,13 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => 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).
+
 (** Platform-specific known builtins *)
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 5d54d94f..75d32ea3 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -17,6 +17,7 @@ Require Import AST Integers Floats.
 Require Import Values Memory Builtins Globalenvs.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 Local Transparent Archi.ptr64.
@@ -69,8 +70,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.
@@ -902,6 +905,27 @@ 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.
+
 (** Platform-specific known builtins *)
 
 Theorem eval_platform_builtin: