From 4d53251d4e9a07da1170f4be9b04b5d44381c9ed Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 22 Mar 2019 10:16:16 +0100
Subject: Risc-V works again (32/64).

---
 riscV/SelectLong.vp     |  2 +-
 riscV/SelectLongproof.v |  1 +
 riscV/SelectOp.vp       |  7 +++++++
 riscV/SelectOpproof.v   | 29 +++++++++++++++++++++++++++--
 4 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/riscV/SelectLong.vp b/riscV/SelectLong.vp
index b3e07bf5..0ccc4725 100644
--- a/riscV/SelectLong.vp
+++ b/riscV/SelectLong.vp
@@ -21,7 +21,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/riscV/SelectLongproof.v b/riscV/SelectLongproof.v
index 78a1935d..d47b6d64 100644
--- a/riscV/SelectLongproof.v
+++ b/riscV/SelectLongproof.v
@@ -21,6 +21,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/riscV/SelectOp.vp b/riscV/SelectOp.vp
index bb8af2ed..181b9d05 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -448,3 +448,10 @@ Nondetfunction builtin_arg (e: expr) :=
       if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e
   | _ => 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/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 90f077db..9966305c 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -29,6 +29,8 @@ Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 
@@ -80,8 +82,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.
@@ -922,4 +926,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.
-- 
cgit