adding builtins

4 files changed, 27 insertions, 6 deletions

diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index 53c83d7e..86bcb2ac 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.v
@@ -18,16 +18,27 @@
 Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
+Require ExtValues.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+| BI_bits_of_float
+| BI_bits_of_double.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+     ("__builtin_bits_of_float", BI_bits_of_float)
+  :: ("__builtin_bits_of_double", BI_bits_of_double)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  match b with
+  | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default
+  | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default
+  end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  match b with
+  | BI_bits_of_float => mkbuiltin_n1t Tsingle Tint Float32.to_bits
+  | BI_bits_of_double => mkbuiltin_n1t Tfloat Tlong Float.to_bits
+  end.
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index a2087cb7..55b6bbd5 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -46,6 +46,10 @@ let builtins = {
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmin",
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+    "__builtin_bits_of_double",
+      (TInt(IULong, []), [TFloat(FDouble, [])], false);
+    "__builtin_bits_of_float",
+      (TInt(IUInt, []), [TFloat(FFloat, [])], false);
   ]
 }
 
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index e9920e46..87e3af05 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -462,4 +462,7 @@ Definition divfs_base (e1: expr) (e2: expr) :=
 (** Platform-specific known builtins *)
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
-  None.
+  match b with
+  | BI_bits_of_float => Some (Eop Obits_of_single args)
+  | BI_bits_of_double => Some (Eop Obits_of_float args)
+  end.
\ No newline at end of file
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 1d13702a..1d713010 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -969,7 +969,10 @@ Theorem eval_platform_builtin:
   platform_builtin_sem bf vl = Some v ->
   exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
 Proof.
-  intros. discriminate.
+  destruct bf; intros until le; intro Heval.
+  all: try (inversion Heval; subst a; clear Heval;
+       exists v; split; trivial;
+       repeat (try econstructor; try eassumption)).
 Qed.
 
 End CMCONSTR.