7 files changed, 56 insertions, 6 deletions
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index 646c4afb..35d555f9 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -15,6 +15,7 @@
 
 Require Import Coqlib Decidableplus.
 Require Import AST Machregs Locations.
+Require Import Errors.
 
 (** * Classification of machine registers *)
 
@@ -26,7 +27,7 @@ Require Import AST Machregs Locations.
   We follow the x86-32 and x86-64 application binary interfaces (ABI)
   in our choice of callee- and caller-save registers.
 *)
-
+  
 Definition is_callee_save (r: mreg) : bool :=
   match r with
   | AX | CX | DX => false
diff --git a/x86/Machregsaux.ml b/x86/Machregsaux.ml
index 473e0602..80066b00 100644
--- a/x86/Machregsaux.ml
+++ b/x86/Machregsaux.ml
@@ -14,9 +14,9 @@
 
 open Camlcoq
 open Machregs
-
+   
 let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
+                                              
 let _ =
   List.iter
     (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
@@ -31,3 +31,8 @@ let register_by_name s =
   Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
 
 let can_reserve_register r = Conventions1.is_callee_save r
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/x86/Machregsaux.mli b/x86/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/x86/Machregsaux.mli
+++ b/x86/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/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 31be8c32..d734ecc6 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -40,7 +40,11 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats Builtins.
 Require Import Op CminorSel.
+<<<<<<< HEAD
+Require Import OpHelpers.
+=======
 Require Archi.
+>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 
 Local Open Scope cminorsel_scope.
 
@@ -576,7 +580,16 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => BA e
   end.
 
+<<<<<<< HEAD
+(* 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 :=
   None.
+>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index a1bb0703..b59f4a87 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -17,6 +17,8 @@ Require Import AST Integers Floats.
 Require Import Values Memory Builtins Globalenvs.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 
@@ -68,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.
@@ -1012,6 +1016,29 @@ Proof.
 - constructor; auto.
 Qed.
 
+<<<<<<< HEAD
+
+(* 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:
@@ -1024,4 +1051,5 @@ Proof.
   intros. discriminate.
 Qed.
 
+>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 End CMCONSTR.