From 0eb1e1e6dd80154fb9841697b2c19482ece2f7da Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 30 Jan 2021 15:52:21 +0100
Subject: select through bitwise operations

---
 riscV/ExtValues.v | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 riscV/ExtValues.v

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
new file mode 100644
index 00000000..0f29e837
--- /dev/null
+++ b/riscV/ExtValues.v
@@ -0,0 +1,40 @@
+Require Import Coqlib.
+Require Import Integers.
+Require Import Values.
+Require Import Floats.
+
+Definition bitwise_select_int b vtrue vfalse :=
+  Val.or (Val.and (Val.neg b) vtrue)
+         (Val.and (Val.sub b Vone) vfalse).
+
+Lemma bitwise_select_int_true :
+  forall vtrue vfalse,
+    bitwise_select_int (Val.of_optbool (Some true)) (Vint vtrue) (Vint vfalse)
+    = Vint vtrue.
+Proof.
+  intros. cbn. f_equal.
+  change (Int.neg Int.one) with Int.mone.
+  rewrite Int.and_commut.
+  rewrite Int.and_mone.
+  rewrite Int.sub_idem.
+  rewrite Int.and_commut.
+  rewrite Int.and_zero.
+  apply Int.or_zero.
+Qed.
+
+Lemma bitwise_select_int_false :
+  forall vtrue vfalse,
+    bitwise_select_int (Val.of_optbool (Some false)) (Vint vtrue) (Vint vfalse)
+    = Vint vfalse.
+Proof.
+  intros. cbn. f_equal.
+  rewrite Int.neg_zero.
+  rewrite Int.and_commut.
+  rewrite Int.and_zero.
+  rewrite Int.sub_zero_r.
+  change (Int.neg Int.one) with Int.mone.
+  rewrite Int.and_commut.
+  rewrite Int.and_mone.
+  rewrite Int.or_commut.
+  apply Int.or_zero.
+Qed.
-- 
cgit 


From e3c6f0702765bd076f3319257651a85f727a0598 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 30 Jan 2021 16:07:26 +0100
Subject: select_long

---
 riscV/ExtValues.v | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 0f29e837..5e6ebf02 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -38,3 +38,41 @@ Proof.
   rewrite Int.or_commut.
   apply Int.or_zero.
 Qed.
+
+Definition bitwise_select_long b vtrue vfalse :=
+  let b' := Val.longofint b in
+  Val.orl (Val.andl (Val.negl b') vtrue)
+          (Val.andl (Val.subl b' (Vlong Int64.one)) vfalse).
+
+Lemma bitwise_select_long_true :
+  forall vtrue vfalse,
+    bitwise_select_long (Val.of_optbool (Some true)) (Vlong vtrue) (Vlong vfalse)
+    = Vlong vtrue.
+Proof.
+  intros. cbn. f_equal.
+  change (Int64.neg Int64.one) with Int64.mone.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_mone.
+  rewrite Int64.sub_idem.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_zero.
+  apply Int64.or_zero.
+Qed.
+
+Lemma bitwise_select_long_false :
+  forall vtrue vfalse,
+    bitwise_select_long (Val.of_optbool (Some false)) (Vlong vtrue) (Vlong vfalse)
+    = Vlong vfalse.
+Proof.
+  intros. cbn. f_equal.
+  change (Int64.repr (Int.signed Int.zero)) with Int64.zero.
+  rewrite Int64.neg_zero.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_zero.
+  rewrite Int64.sub_zero_r.
+  change (Int64.neg Int64.one) with Int64.mone.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_mone.
+  rewrite Int64.or_commut.
+  apply Int64.or_zero.
+Qed.
-- 
cgit 


From 6eabac7e12de09dc4b2a32fa2458e3b91fb34471 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 14:34:30 +0100
Subject: define some semantics in Asm

---
 riscV/Asm.v       | 10 +++++++---
 riscV/ExtValues.v | 17 +++++++++++++++++
 2 files changed, 24 insertions(+), 3 deletions(-)

(limited to 'riscV')

diff --git a/riscV/Asm.v b/riscV/Asm.v
index dc410a3b..599002e7 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -30,6 +30,7 @@ Require Import Smallstep.
 Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
+Require ExtValues.
 
 (** * Abstract syntax *)
 
@@ -918,6 +919,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.floatofsingle rs#s))) m
   | Pfcvtsd d s =>
       Next (nextinstr (rs#d <- (Val.singleoffloat rs#s))) m
+          
+  | Pfmvxs d s =>
+      Next (nextinstr (rs#d <- (ExtValues.bits_of_single rs#s))) m
+  | Pfmvxd d s =>
+      Next (nextinstr (rs#d <- (ExtValues.bits_of_float rs#s))) m
+
 
 (** Pseudo-instructions *)
   | Pallocframe sz pos =>
@@ -968,9 +975,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       so we do not model them. *)
   | Pfence
 
-  | Pfmvxs _ _
-  | Pfmvxd _ _
-
   | Pfmins _ _ _
   | Pfmaxs _ _ _
   | Pfsqrts _ _
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 5e6ebf02..4edd2e3d 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -3,6 +3,18 @@ Require Import Integers.
 Require Import Values.
 Require Import Floats.
 
+Definition bits_of_float x :=
+  match x with
+  | Vfloat f => Vlong (Float.to_bits f)
+  | _ => Vundef
+  end.
+
+Definition bits_of_single x :=
+  match x with
+  | Vsingle f => Vint (Float32.to_bits f)
+  | _ => Vundef
+  end.
+
 Definition bitwise_select_int b vtrue vfalse :=
   Val.or (Val.and (Val.neg b) vtrue)
          (Val.and (Val.sub b Vone) vfalse).
@@ -76,3 +88,8 @@ Proof.
   rewrite Int64.or_commut.
   apply Int64.or_zero.
 Qed.
+
+(*
+Compute (Int.unsigned (Float32.to_bits (Float32.of_int (Int.repr 4200)))).
+Compute (Int64.unsigned (Float.to_bits (Float.of_int (Int.repr 4233)))).
+*)
-- 
cgit 


From d2dc422b91ed628f0f8d6286a23f6f4fb9869248 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 15:07:46 +0100
Subject: Obits_of_single etc

---
 riscV/NeedOp.v   |  2 ++
 riscV/Op.v       | 19 ++++++++++++++++---
 riscV/ValueAOp.v | 28 ++++++++++++++++++++++++++++
 3 files changed, 46 insertions(+), 3 deletions(-)

(limited to 'riscV')

diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 117bbcb4..9a406b6f 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -87,6 +87,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
   | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
   | Ocmp c => needs_of_condition c
+  | Obits_of_single => op1 (default nv)
+  | Obits_of_float => op1 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
diff --git a/riscV/Op.v b/riscV/Op.v
index 2271ecd2..160e4412 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -32,6 +32,7 @@
 Require Import BoolEqual Coqlib.
 Require Import AST Integers Floats.
 Require Import Values Memory Globalenvs Events.
+Require ExtValues.
 
 Set Implicit Arguments.
 
@@ -152,7 +153,9 @@ Inductive operation : Type :=
   | Osingleoflong            (**r [rd = float32_of_signed_long(r1)] *)
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
-  | Ocmp (cond: condition).  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Ocmp (cond: condition)  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Obits_of_single
+  | Obits_of_float.
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -317,6 +320,8 @@ Definition eval_operation
   | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1))
   | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
+  | Obits_of_single, v1::nil => Some (ExtValues.bits_of_single v1)
+  | Obits_of_float, v1::nil => Some (ExtValues.bits_of_float v1)
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   | _, _ => None
   end.
@@ -348,9 +353,9 @@ Qed.
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
-      destruct x; simpl in H; FuncInv
+      destruct x; cbn in H; FuncInv
   | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ =>
-      destruct v; simpl in H; FuncInv
+      destruct v; cbn in H; FuncInv
   | H: (if Archi.ptr64 then _ else _) = Some _ |- _ =>
       destruct Archi.ptr64 eqn:?; FuncInv
   | H: (Some _ = Some _) |- _ =>
@@ -474,6 +479,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Osingleoflongu => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
+  | Obits_of_single => (Tsingle :: nil, Tint)
+  | Obits_of_float => (Tfloat :: nil, Tlong)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -680,6 +687,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
+  (* Bits_of_single, float *)
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -1246,6 +1256,9 @@ Proof.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
     destruct b; simpl; constructor.
     simpl; constructor.
+  (* Bits_of_single, double *)
+  - inv H4; simpl; auto.
+  - inv H4; simpl; auto.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index f4b7b4d6..e1ba878e 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -42,6 +42,18 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
   | _, _ => Vbot
   end.
 
+Definition bits_of_single (v : aval) : aval :=
+  match v with
+  | FS f => I (Float32.to_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition bits_of_float (v : aval) : aval :=
+  match v with
+  | F f => L (Float.to_bits f)
+  | _ => ntop1 v
+  end.
+
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -137,6 +149,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | Obits_of_single, v1::nil => bits_of_single v1
+  | Obits_of_float, v1::nil => bits_of_float v1
   | _, _ => Vbot
   end.
 
@@ -148,6 +162,20 @@ Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
 Hypothesis STACK: bc sp = BCstack.
 
+Lemma bits_of_single_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_single v) (bits_of_single x).
+Proof.
+  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
+Qed.
+
+Lemma bits_of_float_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_float v) (bits_of_float x).
+Proof.
+  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
+Qed.
+
+Hint Resolve bits_of_single_sound bits_of_float_sound : va.
+
 Theorem eval_static_condition_sound:
   forall cond vargs m aargs,
   list_forall2 (vmatch bc) vargs aargs ->
-- 
cgit 


From 52f602db7f306441cfa509cee7cce8cf8567ddc1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 16:09:31 +0100
Subject: adding builtins

---
 riscV/Builtins1.v     | 19 +++++++++++++++----
 riscV/CBuiltins.ml    |  4 ++++
 riscV/SelectOp.vp     |  5 ++++-
 riscV/SelectOpproof.v |  5 ++++-
 4 files changed, 27 insertions(+), 6 deletions(-)

(limited to 'riscV')

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.
-- 
cgit 


From 21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 18:53:04 +0100
Subject: bits to float

---
 riscV/Asm.v            | 11 +++++++++--
 riscV/Builtins1.v      | 10 +++++++++-
 riscV/CBuiltins.ml     |  4 ++++
 riscV/ExtValues.v      | 12 ++++++++++++
 riscV/NeedOp.v         |  2 ++
 riscV/Op.v             | 14 +++++++++++++-
 riscV/SelectOp.vp      |  2 ++
 riscV/TargetPrinter.ml |  4 ++++
 riscV/ValueAOp.v       | 28 +++++++++++++++++++++++++++-
 9 files changed, 82 insertions(+), 5 deletions(-)

(limited to 'riscV')

diff --git a/riscV/Asm.v b/riscV/Asm.v
index 599002e7..d1946a06 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -256,8 +256,10 @@ Inductive instruction : Type :=
 
   (* floating point register move *)
   | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
-  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
-  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
+  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r bitwise move FP single to integer register *)
+  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r bitwise move FP double to integer register *)
+  | Pfmvsx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP single *)
+  | Pfmvdx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP double*)
 
   (* 32-bit (single-precision) floating point *)
   | Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
@@ -924,6 +926,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (ExtValues.bits_of_single rs#s))) m
   | Pfmvxd d s =>
       Next (nextinstr (rs#d <- (ExtValues.bits_of_float rs#s))) m
+          
+  | Pfmvsx d s =>
+      Next (nextinstr (rs#d <- (ExtValues.single_of_bits rs#s))) m
+  | Pfmvdx d s =>
+      Next (nextinstr (rs#d <- (ExtValues.float_of_bits rs#s))) m
 
 
 (** Pseudo-instructions *)
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index 86bcb2ac..47bacffa 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.v
@@ -22,23 +22,31 @@ Require ExtValues.
 
 Inductive platform_builtin : Type :=
 | BI_bits_of_float
-| BI_bits_of_double.
+| BI_bits_of_double
+| BI_float_of_bits
+| BI_double_of_bits.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
      ("__builtin_bits_of_float", BI_bits_of_float)
   :: ("__builtin_bits_of_double", BI_bits_of_double)
+  :: ("__builtin_float_of_bits", BI_float_of_bits)
+  :: ("__builtin_double_of_bits", BI_double_of_bits)
   :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
   match b with
   | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default
   | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default
+  | BI_float_of_bits => mksignature (Tint :: nil) Tsingle cc_default
+  | BI_double_of_bits => mksignature (Tlong :: nil) Tfloat cc_default
   end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
   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
+  | BI_float_of_bits => mkbuiltin_n1t Tint Tsingle Float32.of_bits
+  | BI_double_of_bits => mkbuiltin_n1t Tlong Tfloat Float.of_bits
   end.
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index 55b6bbd5..00b44fd5 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -50,6 +50,10 @@ let builtins = {
       (TInt(IULong, []), [TFloat(FDouble, [])], false);
     "__builtin_bits_of_float",
       (TInt(IUInt, []), [TFloat(FFloat, [])], false);
+    "__builtin_double_of_bits",
+      (TFloat(FDouble, []), [TInt(IULong, [])], false);
+    "__builtin_float_of_bits",
+      (TFloat(FFloat, []), [TInt(IUInt, [])], false);
   ]
 }
 
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 4edd2e3d..39070e7b 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -15,6 +15,18 @@ Definition bits_of_single x :=
   | _ => Vundef
   end.
 
+Definition float_of_bits x :=
+  match x with
+  | Vlong f => Vfloat (Float.of_bits f)
+  | _ => Vundef
+  end.
+
+Definition single_of_bits x :=
+  match x with
+  | Vint f => Vsingle (Float32.of_bits f)
+  | _ => Vundef
+  end.
+
 Definition bitwise_select_int b vtrue vfalse :=
   Val.or (Val.and (Val.neg b) vtrue)
          (Val.and (Val.sub b Vone) vfalse).
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 9a406b6f..136c157f 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -89,6 +89,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ocmp c => needs_of_condition c
   | Obits_of_single => op1 (default nv)
   | Obits_of_float => op1 (default nv)
+  | Osingle_of_bits => op1 (default nv)
+  | Ofloat_of_bits => op1 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
diff --git a/riscV/Op.v b/riscV/Op.v
index 160e4412..21de7787 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -155,7 +155,9 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp (cond: condition)  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
   | Obits_of_single
-  | Obits_of_float.
+  | Obits_of_float
+  | Osingle_of_bits
+  | Ofloat_of_bits.
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -322,6 +324,8 @@ Definition eval_operation
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
   | Obits_of_single, v1::nil => Some (ExtValues.bits_of_single v1)
   | Obits_of_float, v1::nil => Some (ExtValues.bits_of_float v1)
+  | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1)
+  | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1)
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   | _, _ => None
   end.
@@ -481,6 +485,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocmp c => (type_of_condition c, Tint)
   | Obits_of_single => (Tsingle :: nil, Tint)
   | Obits_of_float => (Tfloat :: nil, Tlong)
+  | Osingle_of_bits => (Tint :: nil, Tsingle)
+  | Ofloat_of_bits => (Tlong :: nil, Tfloat)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -690,6 +696,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* Bits_of_single, float *)
   - destruct v0; cbn; trivial.
   - destruct v0; cbn; trivial.
+  (* single, float of bits *)
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -1259,6 +1268,9 @@ Proof.
   (* Bits_of_single, double *)
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
+  (* single, double of bits *)
+  - inv H4; simpl; auto.
+  - inv H4; simpl; auto.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 87e3af05..7714f12d 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -465,4 +465,6 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   match b with
   | BI_bits_of_float => Some (Eop Obits_of_single args)
   | BI_bits_of_double => Some (Eop Obits_of_float args)
+  | BI_float_of_bits => Some (Eop Osingle_of_bits args)
+  | BI_double_of_bits => Some (Eop Ofloat_of_bits args)
   end.
\ No newline at end of file
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 1f02ca71..4bcfa6af 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -396,6 +396,10 @@ module Target : TARGET =
          fprintf oc "	fmv.x.s	%a, %a\n"     ireg rd freg fs
       | Pfmvxd (rd,fs) ->
          fprintf oc "	fmv.x.d	%a, %a\n"     ireg rd freg fs
+      | Pfmvsx (fd,rs) ->
+         fprintf oc "	fmv.s.x	%a, %a\n"     freg fd ireg rs
+      | Pfmvdx (fd,rs) ->
+         fprintf oc "	fmv.d.x	%a, %a\n"     freg fd ireg rs
 
       (* 32-bit (single-precision) floating point *)
       | Pfls (fd, ra, ofs) ->
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index e1ba878e..f94669a2 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -54,6 +54,18 @@ Definition bits_of_float (v : aval) : aval :=
   | _ => ntop1 v
   end.
 
+Definition single_of_bits (v : aval) : aval :=
+  match v with
+  | I f => FS (Float32.of_bits f)
+  | _ => ntop1 v
+  end.
+
+Definition float_of_bits (v : aval) : aval :=
+  match v with
+  | L f => F (Float.of_bits f)
+  | _ => ntop1 v
+  end.
+
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -151,6 +163,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
   | Obits_of_single, v1::nil => bits_of_single v1
   | Obits_of_float, v1::nil => bits_of_float v1
+  | Osingle_of_bits, v1::nil => single_of_bits v1
+  | Ofloat_of_bits, v1::nil => float_of_bits v1
   | _, _ => Vbot
   end.
 
@@ -174,7 +188,19 @@ Proof.
   unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
 Qed.
 
-Hint Resolve bits_of_single_sound bits_of_float_sound : va.
+Lemma single_of_bits_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.single_of_bits v) (single_of_bits x).
+Proof.
+  unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor.
+Qed.
+
+Lemma float_of_bits_sound:
+  forall v x, vmatch bc v x -> vmatch bc (ExtValues.float_of_bits v) (float_of_bits x).
+Proof.
+  unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
+Qed.
+
+Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound : va.
 
 Theorem eval_static_condition_sound:
   forall cond vargs m aargs,
-- 
cgit 


From 10dbecd69cb985841a85b8b62efdf29c3242967f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 18:58:16 +0100
Subject: Asmgen for bits / float

---
 riscV/Asmgen.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'riscV')

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index b431d63d..debe1928 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -705,6 +705,19 @@ Definition transl_op
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
 
+  | Obits_of_single, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfmvxs rd rs :: k)
+  | Obits_of_float, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfmvxd rd rs :: k)
+  | Osingle_of_bits, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfmvsx rd rs :: k)
+  | Ofloat_of_bits, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pfmvdx rd rs :: k)
+                               
   | Ocmp cmp, _ =>
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
-- 
cgit 


From 9c03320dd809295239a9cdf71cd8726f02df0d33 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 20:37:49 +0100
Subject: int64_of_value

---
 riscV/ExtValues.v | 77 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 39070e7b..d79604f7 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -2,7 +2,84 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 Require Import Floats.
+Require Import Memory.
+Require Import Lia.
 
+Axiom address_of_ptr : mem -> block -> ptrofs -> int64.
+Axiom ptr_of_address : mem -> int64 -> option (block*ptrofs).
+Axiom ptr_address_correct :
+  forall m b ofs, (ptr_of_address m (address_of_ptr m b ofs)) = Some (b, ofs).
+
+Definition int64_of_value m v : int64 :=
+  match v with
+  | Vint x => Int64.repr (Int.signed x)
+  | Vlong x => x
+  | Vsingle x => Int64.repr (Int.signed (Float32.to_bits x))
+  | Vfloat x => Float.to_bits x
+  | Vptr b ofs => address_of_ptr m b ofs
+  | Vundef => Int64.zero
+  end.
+
+Inductive vtype := VTint | VTlong | VTsingle | VTfloat | VTptr | VTundef.
+
+Definition vtype_of v :=
+  match v with
+  | Vint _ => VTint
+  | Vlong _ => VTlong
+  | Vfloat _ => VTfloat
+  | Vsingle _ => VTsingle
+  | Vptr _ _ => VTptr
+  | Vundef => VTundef
+  end.
+
+Definition value_of_int64 (ty : vtype) (m : mem) (l : int64) : val :=
+  match ty with
+  | VTint => Vint (Int.repr (Int64.signed l))
+  | VTlong => Vlong l
+  | VTsingle => Vsingle (Float32.of_bits (Int.repr (Int64.signed l)))
+  | VTfloat => Vfloat (Float.of_bits l)
+  | VTptr => match ptr_of_address m l with
+                | Some(b, ofs) => Vptr b ofs
+                | None => Vundef
+             end
+  | VTundef => Vundef
+  end.
+
+Remark min_signed_order: Int64.min_signed <= Int.min_signed.
+Proof.
+  cbv. discriminate.
+Qed.
+
+Remark max_signed_order: Int.max_signed <= Int64.max_signed.
+Proof.
+  cbv. discriminate.
+Qed.
+
+Lemma int64_of_value_correct :
+  forall m v,
+    value_of_int64 (vtype_of v) m (int64_of_value m v) = v.
+Proof.
+  destruct v; cbn; trivial; f_equal.
+  - rewrite Int64.signed_repr.
+    apply Int.repr_signed. 
+    pose proof (Int.signed_range i) as RANGE.
+    pose proof min_signed_order.
+    pose proof max_signed_order.
+    lia.
+  - apply Float.of_to_bits.
+  - rewrite Int64.signed_repr.
+    { rewrite Int.repr_signed.
+      apply Float32.of_to_bits. }
+    pose proof (Int.signed_range (Float32.to_bits f)) as RANGE.
+    pose proof min_signed_order.
+    pose proof max_signed_order.
+    lia.
+  - pose proof (ptr_address_correct m b i).
+    destruct (ptr_of_address m (address_of_ptr m b i)).
+    + inv H. trivial.
+    + discriminate.
+Qed.
+    
 Definition bits_of_float x :=
   match x with
   | Vfloat f => Vlong (Float.to_bits f)
-- 
cgit 


From 485952d5513a9de25f7e3ee3ca7a35442f154d04 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 20:53:06 +0100
Subject: int64_of_value some more

---
 riscV/ExtValues.v | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index d79604f7..f9996a97 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -104,6 +104,7 @@ Definition single_of_bits x :=
   | _ => Vundef
   end.
 
+(*
 Definition bitwise_select_int b vtrue vfalse :=
   Val.or (Val.and (Val.neg b) vtrue)
          (Val.and (Val.sub b Vone) vfalse).
@@ -139,18 +140,18 @@ Proof.
   rewrite Int.or_commut.
   apply Int.or_zero.
 Qed.
+ *)
 
 Definition bitwise_select_long b vtrue vfalse :=
-  let b' := Val.longofint b in
-  Val.orl (Val.andl (Val.negl b') vtrue)
-          (Val.andl (Val.subl b' (Vlong Int64.one)) vfalse).
+  let b' := Int64.repr (Int64.unsigned b) in
+  Int64.or (Int64.and (Int64.neg b') vtrue)
+           (Int64.and (Int64.sub b' Int64.one) vfalse).
 
 Lemma bitwise_select_long_true :
   forall vtrue vfalse,
-    bitwise_select_long (Val.of_optbool (Some true)) (Vlong vtrue) (Vlong vfalse)
-    = Vlong vtrue.
+    bitwise_select_long Int64.one vtrue vfalse = vtrue.
 Proof.
-  intros. cbn. f_equal.
+  intros. unfold bitwise_select_long. cbn.
   change (Int64.neg Int64.one) with Int64.mone.
   rewrite Int64.and_commut.
   rewrite Int64.and_mone.
@@ -162,11 +163,10 @@ Qed.
 
 Lemma bitwise_select_long_false :
   forall vtrue vfalse,
-    bitwise_select_long (Val.of_optbool (Some false)) (Vlong vtrue) (Vlong vfalse)
-    = Vlong vfalse.
+    bitwise_select_long Int64.zero vtrue vfalse = vfalse.
 Proof.
-  intros. cbn. f_equal.
-  change (Int64.repr (Int.signed Int.zero)) with Int64.zero.
+  intros. unfold bitwise_select_long. cbn.
+  change (Int64.repr (Int64.unsigned Int64.zero)) with Int64.zero.
   rewrite Int64.neg_zero.
   rewrite Int64.and_commut.
   rewrite Int64.and_zero.
@@ -178,7 +178,8 @@ Proof.
   apply Int64.or_zero.
 Qed.
 
-(*
-Compute (Int.unsigned (Float32.to_bits (Float32.of_int (Int.repr 4200)))).
-Compute (Int64.unsigned (Float.to_bits (Float.of_int (Int.repr 4233)))).
-*)
+Definition bitwise_select_value vt m b vtrue vfalse :=
+  value_of_int64 vt m (bitwise_select_long b
+                                        (int64_of_value m vtrue)
+                                        (int64_of_value m vfalse)).
+
-- 
cgit 


From 325b9f028f91b65e191d48dc8482da8d1ccb5d2b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 21:02:18 +0100
Subject: bitwise_select_value_correct

---
 riscV/ExtValues.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index f9996a97..591507ed 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -183,3 +183,15 @@ Definition bitwise_select_value vt m b vtrue vfalse :=
                                         (int64_of_value m vtrue)
                                         (int64_of_value m vfalse)).
 
+Theorem bitwise_select_value_correct :
+  forall m (b : bool) vtrue vfalse,
+    bitwise_select_value (vtype_of (if b then vtrue else vfalse))
+                         m (if b then Int64.one else Int64.zero) vtrue vfalse =
+    if b then vtrue else vfalse.
+Proof.
+  intros. unfold bitwise_select_value. destruct b.
+  - rewrite bitwise_select_long_true.
+    apply int64_of_value_correct.
+  - rewrite bitwise_select_long_false.
+    apply int64_of_value_correct.
+Qed.
-- 
cgit 


From 91899d674a333c429ed6cdaf6aeb24baa7cd8532 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 21:09:24 +0100
Subject: repr etc.

---
 riscV/ExtValues.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 591507ed..0ba3b0ea 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -143,9 +143,8 @@ Qed.
  *)
 
 Definition bitwise_select_long b vtrue vfalse :=
-  let b' := Int64.repr (Int64.unsigned b) in
-  Int64.or (Int64.and (Int64.neg b') vtrue)
-           (Int64.and (Int64.sub b' Int64.one) vfalse).
+  Int64.or (Int64.and (Int64.neg b) vtrue)
+           (Int64.and (Int64.sub b Int64.one) vfalse).
 
 Lemma bitwise_select_long_true :
   forall vtrue vfalse,
@@ -166,7 +165,6 @@ Lemma bitwise_select_long_false :
     bitwise_select_long Int64.zero vtrue vfalse = vfalse.
 Proof.
   intros. unfold bitwise_select_long. cbn.
-  change (Int64.repr (Int64.unsigned Int64.zero)) with Int64.zero.
   rewrite Int64.neg_zero.
   rewrite Int64.and_commut.
   rewrite Int64.and_zero.
-- 
cgit 


From e0f1a90c2dcf7c43137064470ce4b12368b8435d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 1 Feb 2021 21:38:12 +0100
Subject: select01_long

---
 riscV/ExtValues.v | 140 ++++--------------------------------------------------
 1 file changed, 10 insertions(+), 130 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 0ba3b0ea..e0557de4 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -4,81 +4,6 @@ Require Import Values.
 Require Import Floats.
 Require Import Memory.
 Require Import Lia.
-
-Axiom address_of_ptr : mem -> block -> ptrofs -> int64.
-Axiom ptr_of_address : mem -> int64 -> option (block*ptrofs).
-Axiom ptr_address_correct :
-  forall m b ofs, (ptr_of_address m (address_of_ptr m b ofs)) = Some (b, ofs).
-
-Definition int64_of_value m v : int64 :=
-  match v with
-  | Vint x => Int64.repr (Int.signed x)
-  | Vlong x => x
-  | Vsingle x => Int64.repr (Int.signed (Float32.to_bits x))
-  | Vfloat x => Float.to_bits x
-  | Vptr b ofs => address_of_ptr m b ofs
-  | Vundef => Int64.zero
-  end.
-
-Inductive vtype := VTint | VTlong | VTsingle | VTfloat | VTptr | VTundef.
-
-Definition vtype_of v :=
-  match v with
-  | Vint _ => VTint
-  | Vlong _ => VTlong
-  | Vfloat _ => VTfloat
-  | Vsingle _ => VTsingle
-  | Vptr _ _ => VTptr
-  | Vundef => VTundef
-  end.
-
-Definition value_of_int64 (ty : vtype) (m : mem) (l : int64) : val :=
-  match ty with
-  | VTint => Vint (Int.repr (Int64.signed l))
-  | VTlong => Vlong l
-  | VTsingle => Vsingle (Float32.of_bits (Int.repr (Int64.signed l)))
-  | VTfloat => Vfloat (Float.of_bits l)
-  | VTptr => match ptr_of_address m l with
-                | Some(b, ofs) => Vptr b ofs
-                | None => Vundef
-             end
-  | VTundef => Vundef
-  end.
-
-Remark min_signed_order: Int64.min_signed <= Int.min_signed.
-Proof.
-  cbv. discriminate.
-Qed.
-
-Remark max_signed_order: Int.max_signed <= Int64.max_signed.
-Proof.
-  cbv. discriminate.
-Qed.
-
-Lemma int64_of_value_correct :
-  forall m v,
-    value_of_int64 (vtype_of v) m (int64_of_value m v) = v.
-Proof.
-  destruct v; cbn; trivial; f_equal.
-  - rewrite Int64.signed_repr.
-    apply Int.repr_signed. 
-    pose proof (Int.signed_range i) as RANGE.
-    pose proof min_signed_order.
-    pose proof max_signed_order.
-    lia.
-  - apply Float.of_to_bits.
-  - rewrite Int64.signed_repr.
-    { rewrite Int.repr_signed.
-      apply Float32.of_to_bits. }
-    pose proof (Int.signed_range (Float32.to_bits f)) as RANGE.
-    pose proof min_signed_order.
-    pose proof max_signed_order.
-    lia.
-  - pose proof (ptr_address_correct m b i).
-    destruct (ptr_of_address m (address_of_ptr m b i)).
-    + inv H. trivial.
-    + discriminate.
-Qed.
     
 Definition bits_of_float x :=
   match x with
@@ -104,44 +29,6 @@ Definition single_of_bits x :=
   | _ => Vundef
   end.
 
-(*
-Definition bitwise_select_int b vtrue vfalse :=
-  Val.or (Val.and (Val.neg b) vtrue)
-         (Val.and (Val.sub b Vone) vfalse).
-
-Lemma bitwise_select_int_true :
-  forall vtrue vfalse,
-    bitwise_select_int (Val.of_optbool (Some true)) (Vint vtrue) (Vint vfalse)
-    = Vint vtrue.
-Proof.
-  intros. cbn. f_equal.
-  change (Int.neg Int.one) with Int.mone.
-  rewrite Int.and_commut.
-  rewrite Int.and_mone.
-  rewrite Int.sub_idem.
-  rewrite Int.and_commut.
-  rewrite Int.and_zero.
-  apply Int.or_zero.
-Qed.
-
-Lemma bitwise_select_int_false :
-  forall vtrue vfalse,
-    bitwise_select_int (Val.of_optbool (Some false)) (Vint vtrue) (Vint vfalse)
-    = Vint vfalse.
-Proof.
-  intros. cbn. f_equal.
-  rewrite Int.neg_zero.
-  rewrite Int.and_commut.
-  rewrite Int.and_zero.
-  rewrite Int.sub_zero_r.
-  change (Int.neg Int.one) with Int.mone.
-  rewrite Int.and_commut.
-  rewrite Int.and_mone.
-  rewrite Int.or_commut.
-  apply Int.or_zero.
-Qed.
- *)
-
 Definition bitwise_select_long b vtrue vfalse :=
   Int64.or (Int64.and (Int64.neg b) vtrue)
            (Int64.and (Int64.sub b Int64.one) vfalse).
@@ -176,20 +63,13 @@ Proof.
   apply Int64.or_zero.
 Qed.
 
-Definition bitwise_select_value vt m b vtrue vfalse :=
-  value_of_int64 vt m (bitwise_select_long b
-                                        (int64_of_value m vtrue)
-                                        (int64_of_value m vfalse)).
-
-Theorem bitwise_select_value_correct :
-  forall m (b : bool) vtrue vfalse,
-    bitwise_select_value (vtype_of (if b then vtrue else vfalse))
-                         m (if b then Int64.one else Int64.zero) vtrue vfalse =
-    if b then vtrue else vfalse.
-Proof.
-  intros. unfold bitwise_select_value. destruct b.
-  - rewrite bitwise_select_long_true.
-    apply int64_of_value_correct.
-  - rewrite bitwise_select_long_false.
-    apply int64_of_value_correct.
-Qed.
+Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val :=
+  match vb with
+  | (Vint b) =>
+    if Int.eq b Int.one
+    then vtrue
+    else if Int.eq b Int.zero
+         then vfalse
+         else Vundef
+  | _ => Vundef
+  end.
-- 
cgit 


From d2159e300b2d5e017a3144c747d34949b2ff2769 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 10:21:17 +0100
Subject: begin implementing select

---
 riscV/Asm.v            |  8 +++++--
 riscV/Asmexpand.ml     | 15 ++++++++++++-
 riscV/ExtValues.v      | 10 +++++++++
 riscV/NeedOp.v         | 11 ++++++++++
 riscV/Op.v             | 16 +++++++++++++-
 riscV/TargetPrinter.ml |  2 ++
 riscV/ValueAOp.v       | 57 ++++++++++++++++++++++++++++++++++++++++++++++++--
 7 files changed, 113 insertions(+), 6 deletions(-)

(limited to 'riscV')

diff --git a/riscV/Asm.v b/riscV/Asm.v
index d1946a06..9a4b2a57 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -63,10 +63,10 @@ Inductive freg: Type :=
   | F24: freg | F25: freg | F26: freg | F27: freg
   | F28: freg | F29: freg | F30: freg | F31: freg.
 
-Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
+Definition ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
-Lemma ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}.
+Definition ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}.
 Proof. decide equality. apply ireg_eq. Defined.
 
 Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
@@ -348,6 +348,7 @@ Inductive instruction : Type :=
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
               -> builtin_res preg -> instruction    (**r built-in function (pseudo) *)
+  | Pselectl (rd: ireg) (rb: ireg0) (rt: ireg0) (rf: ireg0)
   | Pnop : instruction.                             (**r nop instruction *)
 
 
@@ -954,6 +955,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
           | _ => Stuck
           end
       end
+  | Pselectl rd rb rt rf =>
+    Next (nextinstr (rs#rd <- (ExtValues.select01_long
+                                (rs###rb) (rs###rt) (rs###rf)))) m
   | Plabel lbl =>
       Next (nextinstr rs) m
   | Ploadsymbol rd s ofs =>
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 810514a3..9dd8cac9 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -582,9 +582,22 @@ let expand_builtin_inline name args res =
      raise (Error ("unrecognized builtin " ^ name))
 
 (* Expansion of instructions *)
-
+                                 
 let expand_instruction instr =
   match instr with
+  | Pselectl(rd, rb, rt, rf) ->
+      if not (ireg0_eq rt rf)
+      then
+        if (ireg0_eq (X rd) rt) || (ireg0_eq (X rd) rf)
+        then failwith "Pselectl"
+        else
+          begin
+            emit (Psubl(X31, X0, rb));
+            emit (Paddil(rd, rb, Int64.mone));
+            emit (Pandl(X31, X X31, rt));
+            emit (Pandl(rd, X rd, rf));
+            emit (Porl(rd, X rd, X X31))
+          end
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (X30, X2));
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index e0557de4..81688ca6 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -73,3 +73,13 @@ Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val :=
          else Vundef
   | _ => Vundef
   end.
+
+Lemma normalize_select01:
+  forall x y z, Val.normalize (select01_long x y z) AST.Tlong = select01_long x (Val.normalize y AST.Tlong) (Val.normalize z AST.Tlong).
+Proof.
+  unfold select01_long.
+  intros.
+  destruct x; cbn; trivial.
+  destruct (Int.eq i Int.one); trivial.
+  destruct (Int.eq i Int.zero); trivial.
+Qed.
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 136c157f..9e1ad004 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -91,6 +91,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Obits_of_float => op1 (default nv)
   | Osingle_of_bits => op1 (default nv)
   | Ofloat_of_bits => op1 (default nv)
+  | Oselectl => All :: nv :: nv :: nil
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -158,6 +159,16 @@ Proof.
 - apply shlimm_sound; auto.
 - apply shrimm_sound; auto.
 - apply shruimm_sound; auto.
+- (* selectl *)
+  unfold ExtValues.select01_long.
+  destruct v0; auto with na.
+  assert (Val.lessdef (Vint i) v4) as LESSDEF by auto with na.
+  inv LESSDEF.
+  destruct (Int.eq i Int.one).
+  { apply normalize_sound; auto. }
+  destruct (Int.eq i Int.zero).
+  { apply normalize_sound; auto. }
+  cbn. auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/riscV/Op.v b/riscV/Op.v
index 21de7787..64d5e4c9 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -157,7 +157,8 @@ Inductive operation : Type :=
   | Obits_of_single
   | Obits_of_float
   | Osingle_of_bits
-  | Ofloat_of_bits.
+  | Ofloat_of_bits
+  | Oselectl.
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -327,6 +328,7 @@ Definition eval_operation
   | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1)
   | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1)
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
+  | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
   | _, _ => None
   end.
 
@@ -487,6 +489,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Obits_of_float => (Tfloat :: nil, Tlong)
   | Osingle_of_bits => (Tint :: nil, Tsingle)
   | Ofloat_of_bits => (Tlong :: nil, Tfloat)
+  | Oselectl => (Tint :: Tlong :: Tlong :: nil, Tlong)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -699,6 +702,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* single, float of bits *)
   - destruct v0; cbn; trivial.
   - destruct v0; cbn; trivial.
+  (* selectl *)
+  - destruct v0; cbn; trivial.
+    destruct Int.eq; cbn.
+    apply Val.normalize_type.
+    destruct Int.eq; cbn; trivial.
+    apply Val.normalize_type.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -1271,6 +1280,11 @@ Proof.
   (* single, double of bits *)
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
+  (* selectl *)
+  - inv H4; trivial. cbn.
+    destruct (Int.eq i Int.one).
+    + auto using Val.normalize_inject.
+    + destruct (Int.eq i Int.zero); cbn; auto using Val.normalize_inject.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 4bcfa6af..1f00c440 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -529,6 +529,8 @@ module Target : TARGET =
          fprintf oc "	fcvt.s.d	%a, %a\n" freg fd freg fs
 
       (* Pseudo-instructions expanded in Asmexpand *)
+      | Pselectl(_, _, _, _) ->
+         assert false
       | Pallocframe(sz, ofs) ->
          assert false
       | Pfreeframe(sz, ofs) ->
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index f94669a2..e779b114 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -66,6 +66,15 @@ Definition float_of_bits (v : aval) : aval :=
   | _ => ntop1 v
   end.
 
+Definition select01_long (vb : aval) (vt : aval) (vf : aval) :=
+  match vb with
+  | I b =>
+    if Int.eq b Int.one then add_undef vt
+    else if Int.eq b Int.zero then add_undef vf
+         else add_undef (vlub vt vf)
+  | _ => add_undef (vlub vt vf)
+  end.
+
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -165,6 +174,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Obits_of_float, v1::nil => bits_of_float v1
   | Osingle_of_bits, v1::nil => single_of_bits v1
   | Ofloat_of_bits, v1::nil => float_of_bits v1
+  | Oselectl, vb::vt::vf::nil => select01_long vb vt vf
   | _, _ => Vbot
   end.
 
@@ -200,7 +210,50 @@ Proof.
   unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor.
 Qed.
 
-Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound : va.
+  
+Lemma select01_long_sound:
+  forall vb xb vt xt vf xf
+         (MATCH_b : vmatch bc vb xb)
+         (MATCH_t : vmatch bc vt xt)
+         (MATCH_f : vmatch bc vf xf),
+    vmatch bc (Val.normalize (ExtValues.select01_long vb vt vf) Tlong)
+              (select01_long xb xt xf).
+Proof.
+  intros.
+  inv MATCH_b; cbn; try apply add_undef_undef.
+  - destruct (Int.eq i Int.one). { apply add_undef_normalize; trivial. }
+    destruct (Int.eq i Int.zero). { apply add_undef_normalize; trivial. }
+    cbn. apply add_undef_undef.
+  - destruct (Int.eq i Int.one).
+    { apply add_undef_normalize.
+      apply vmatch_lub_l.
+      trivial. }
+    destruct (Int.eq i Int.zero).
+    { apply add_undef_normalize.
+      apply vmatch_lub_r.
+      trivial. }
+    cbn. apply add_undef_undef.
+  - destruct (Int.eq i Int.one).
+    { apply add_undef_normalize.
+      apply vmatch_lub_l.
+      trivial. }
+    destruct (Int.eq i Int.zero).
+    { apply add_undef_normalize.
+      apply vmatch_lub_r.
+      trivial. }
+    cbn. apply add_undef_undef.
+  - destruct (Int.eq i Int.one).
+    { apply add_undef_normalize.
+      apply vmatch_lub_l.
+      trivial. }
+    destruct (Int.eq i Int.zero).
+    { apply add_undef_normalize.
+      apply vmatch_lub_r.
+      trivial. }
+    cbn. apply add_undef_undef.
+Qed.
+
+Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound select01_long_sound : va.
 
 Theorem eval_static_condition_sound:
   forall cond vargs m aargs,
@@ -254,7 +307,7 @@ Proof.
   destruct addr; InvHyps; eauto with va.
   rewrite Ptrofs.add_zero_l; eauto with va.
 Qed.
-
+  
 Theorem eval_static_operation_sound:
   forall op vargs m vres aargs,
   eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
-- 
cgit 


From 5dfa2de0e1ba0acd36584983afefd9af1f5c2262 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 10:36:49 +0100
Subject: asmgen Oselectl

---
 riscV/Asmgen.v       | 7 +++++++
 riscV/Asmgenproof1.v | 4 ++++
 2 files changed, 11 insertions(+)

(limited to 'riscV')

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index debe1928..b87d2692 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -722,6 +722,13 @@ Definition transl_op
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
 
+  | Oselectl, b::t::f::nil =>
+      do rd <- ireg_of res;
+      do rb <- ireg_of b;
+      do rt <- ireg_of t;
+      do rf <- ireg_of f;
+      OK (Pselectl rd rb rt rf :: k)
+         
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index d2255e66..5940802c 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1138,6 +1138,10 @@ Opaque Int.eq.
 - (* cond *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
+- (* select *)
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl.
+  apply Val.lessdef_normalize.
 Qed.
 
 (** Memory accesses *)
-- 
cgit 


From 5afebe369cea7f2746dec7c64514822562e9100e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 11:22:59 +0100
Subject: begin synthesizing select

---
 riscV/ExtValues.v     | 18 ++++++++++++++++++
 riscV/SelectOp.vp     |  6 +++++-
 riscV/SelectOpproof.v | 12 +++++++++++-
 3 files changed, 34 insertions(+), 2 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 81688ca6..3f283cdc 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -83,3 +83,21 @@ Proof.
   destruct (Int.eq i Int.one); trivial.
   destruct (Int.eq i Int.zero); trivial.
 Qed.
+
+Lemma select01_long_true:
+  forall vt vf,
+    select01_long Vtrue vt vf = vt.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true. reflexivity.
+Qed.
+
+Lemma select01_long_false:
+  forall vt vf,
+    select01_long Vfalse vt vf = vf.
+Proof.
+  intros. unfold select01_long. cbn.
+  rewrite Int.eq_true.
+  rewrite Int.eq_false. reflexivity.
+  cbv. discriminate.
+Qed.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 7714f12d..0596ebf6 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -421,7 +421,11 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
    : option expr
-   := None.
+   := match ty with
+      | Tlong => Some (Eop Oselectl
+                       ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil))
+      | _ => None
+      end.
  
 (** ** Recognition of addressing modes for load and store operations *)
 
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 1d713010..9dfe9b6e 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -886,7 +886,17 @@ Theorem eval_select:
      eval_expr ge sp e m le a v
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
-  unfold select; intros; discriminate.
+  unfold select; intros.
+  destruct ty; cbn in *; try discriminate.
+  inv H.
+  TrivialExists.
+  - cbn. constructor.
+    { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
+    constructor. eassumption. constructor. eassumption. constructor.
+  - cbn. f_equal. rewrite ExtValues.normalize_select01.
+    destruct b.
+    + rewrite ExtValues.select01_long_true. reflexivity.
+    + rewrite ExtValues.select01_long_false. reflexivity.
 Qed.
 
 Theorem eval_addressing:
-- 
cgit 


From 7afc85c95aaec5cc0935733cac487e13f114cc46 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 13:07:56 +0100
Subject: cmov on integers

---
 riscV/SelectOp.vp     | 10 ++++--
 riscV/SelectOpproof.v | 89 +++++++++++++++++++++++++++++++++++++++++++++------
 2 files changed, 88 insertions(+), 11 deletions(-)

(limited to 'riscV')

diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 0596ebf6..0e82f8ba 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -421,11 +421,17 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
    : option expr
-   := match ty with
+   := if Archi.ptr64 then
+      match ty with
       | Tlong => Some (Eop Oselectl
                        ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil))
+      | Tint => Some (Eop Olowlong ((Eop Oselectl
+                       ((Eop (Ocmp cond) args) :::
+		         (Eop Ocast32signed (e1 ::: Enil)) :::
+			 (Eop Ocast32signed (e2 ::: Enil)) ::: Enil)) ::: Enil))
       | _ => None
-      end.
+      end
+      else None.
  
 (** ** Recognition of addressing modes for load and store operations *)
 
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 9dfe9b6e..7f7474b6 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -24,6 +24,7 @@ Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 Require Import OpHelpers.
 Require Import OpHelpersproof.
+Require Import Lia.
 
 Local Open Scope cminorsel_scope.
 
@@ -875,6 +876,58 @@ Proof.
   red; intros. unfold floatofsingle. TrivialExists.
 Qed.
 
+Lemma mod_small_negative:
+  forall a modulus,
+    modulus > 0 -> -modulus < a < 0 -> a mod modulus = a + modulus.
+Proof.
+  intros.
+  replace (a mod modulus) with ((a + modulus) mod modulus).
+  apply Z.mod_small.
+  lia.
+  rewrite <- Zplus_mod_idemp_r.
+  rewrite Z.mod_same by lia.
+  rewrite Z.add_0_r.
+  reflexivity.
+Qed.
+
+Remark normalize_low_long: forall
+  (PTR64 : Archi.ptr64 = true) v1,
+    Val.loword (Val.normalize (Val.longofint v1) Tlong) = Val.normalize v1 Tint.
+Proof.
+  intros.
+  destruct v1; cbn; try rewrite PTR64; trivial.
+  f_equal.
+  unfold Int64.loword.
+  unfold Int.signed.
+  destruct zlt.
+  { rewrite Int64.int_unsigned_repr.
+    apply Int.repr_unsigned.
+  }
+  pose proof (Int.unsigned_range i).
+  rewrite Int64.unsigned_repr_eq.
+  replace ((Int.unsigned i - Int.modulus) mod Int64.modulus)
+    with (Int64.modulus + Int.unsigned i - Int.modulus).
+  {
+    rewrite <- (Int.repr_unsigned i) at 2.
+    apply Int.eqm_samerepr.
+    unfold Int.eqm, eqmod.
+    change Int.modulus with 4294967296 in *.
+    change Int64.modulus with 18446744073709551616 in *.
+    exists 4294967295.
+    lia.
+  }
+  { rewrite mod_small_negative.
+    lia.
+    constructor.
+    constructor.
+    change Int.modulus with 4294967296 in *.
+    change Int.half_modulus with 2147483648 in *.
+    change Int64.modulus with 18446744073709551616 in *.
+    lia.
+    lia.
+  }
+Qed.
+
 Theorem eval_select:
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
@@ -887,16 +940,34 @@ Theorem eval_select:
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
   unfold select; intros.
+  destruct Archi.ptr64 eqn:PTR64.
+  2: discriminate.
   destruct ty; cbn in *; try discriminate.
-  inv H.
-  TrivialExists.
-  - cbn. constructor.
-    { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
-    constructor. eassumption. constructor. eassumption. constructor.
-  - cbn. f_equal. rewrite ExtValues.normalize_select01.
-    destruct b.
-    + rewrite ExtValues.select01_long_true. reflexivity.
-    + rewrite ExtValues.select01_long_false. reflexivity.
+  - inv H. TrivialExists.
+    + cbn. constructor.
+      { econstructor.
+        { constructor.
+          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
+          constructor. econstructor. constructor. eassumption.
+          constructor. cbn. reflexivity.
+          constructor. econstructor. constructor. eassumption. constructor.
+          cbn. reflexivity. constructor.
+        }
+        constructor.
+      }
+      constructor.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      destruct b.
+      * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
+      * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
+  - inv H. TrivialExists.
+    + cbn. constructor.
+      { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
+      constructor. eassumption. constructor. eassumption. constructor.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      destruct b.
+      * rewrite ExtValues.select01_long_true. reflexivity.
+      * rewrite ExtValues.select01_long_false. reflexivity.
 Qed.
 
 Theorem eval_addressing:
-- 
cgit 


From a47d709fd9251f58032444fde27a3ad7e947c26d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 13:33:43 +0100
Subject: Pselectd

---
 riscV/ExtValues.v     | 10 ++++++++++
 riscV/SelectOp.vp     |  4 ++++
 riscV/SelectOpproof.v | 19 +++++++++++++++++++
 3 files changed, 33 insertions(+)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 3f283cdc..aebbe5c5 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -101,3 +101,13 @@ Proof.
   rewrite Int.eq_false. reflexivity.
   cbv. discriminate.
 Qed.
+
+Lemma float_bits_normalize:
+  forall v1,
+  ExtValues.float_of_bits (Val.normalize (ExtValues.bits_of_float v1) AST.Tlong) =
+  Val.normalize v1 AST.Tfloat.
+Proof.
+  destruct v1; cbn; trivial.
+  f_equal.
+  apply Float.of_to_bits.
+Qed.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 0e82f8ba..b6720e40 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -429,6 +429,10 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
                        ((Eop (Ocmp cond) args) :::
 		         (Eop Ocast32signed (e1 ::: Enil)) :::
 			 (Eop Ocast32signed (e2 ::: Enil)) ::: Enil)) ::: Enil))
+      | Tfloat => Some (Eop Ofloat_of_bits ((Eop Oselectl
+                       ((Eop (Ocmp cond) args) :::
+		         (Eop Obits_of_float (e1 ::: Enil)) :::
+			 (Eop Obits_of_float (e2 ::: Enil)) ::: Enil)) ::: Enil))
       | _ => None
       end
       else None.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 7f7474b6..c313fbaf 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -960,6 +960,25 @@ Proof.
       destruct b.
       * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
       * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
+  - inv H. TrivialExists.
+    + cbn. constructor.
+      { econstructor.
+        { constructor.
+          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
+          constructor. econstructor. constructor. eassumption.
+          constructor. cbn. reflexivity.
+          constructor. econstructor. constructor. eassumption. constructor.
+          cbn. reflexivity. constructor.
+        }
+        constructor.
+      }
+      constructor.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      destruct b.
+      * rewrite ExtValues.select01_long_true.
+        apply ExtValues.float_bits_normalize.
+      * rewrite ExtValues.select01_long_false.
+        apply ExtValues.float_bits_normalize.
   - inv H. TrivialExists.
     + cbn. constructor.
       { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
-- 
cgit 


From 3a3e6f61db092f0f81849af6970c771c70df8bce Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 13:43:44 +0100
Subject: some more cases implemented

---
 riscV/Asmexpand.ml | 37 +++++++++++++++++++++++++------------
 1 file changed, 25 insertions(+), 12 deletions(-)

(limited to 'riscV')

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 9dd8cac9..f23db36e 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -586,18 +586,31 @@ let expand_builtin_inline name args res =
 let expand_instruction instr =
   match instr with
   | Pselectl(rd, rb, rt, rf) ->
-      if not (ireg0_eq rt rf)
-      then
-        if (ireg0_eq (X rd) rt) || (ireg0_eq (X rd) rf)
-        then failwith "Pselectl"
-        else
-          begin
-            emit (Psubl(X31, X0, rb));
-            emit (Paddil(rd, rb, Int64.mone));
-            emit (Pandl(X31, X X31, rt));
-            emit (Pandl(rd, X rd, rf));
-            emit (Porl(rd, X rd, X X31))
-          end
+     if not Archi.ptr64
+     then failwith "Pselectl not available on RV32, only on RV64"
+     else
+       if not (ireg0_eq rt rf)
+       then
+         if (ireg0_eq (X rd) rt) 
+         then failwith "Pselectl rd=rt"
+         else
+           if (ireg0_eq (X rd) rf)
+           then
+             begin
+               emit (Paddil(X31, rb, Int64.mone));
+               emit (Pandl(X31, X X31, rf));
+               emit (Psubl(rd, X0, rb));
+               emit (Pandl(rd, X rd, rt));
+               emit (Porl(rd, X rd, X X31))
+             end  
+           else
+             begin
+               emit (Psubl(X31, X0, rb));
+               emit (Paddil(rd, rb, Int64.mone));
+               emit (Pandl(X31, X X31, rt));
+               emit (Pandl(rd, X rd, rf));
+               emit (Porl(rd, X rd, X X31))
+             end
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (X30, X2));
-- 
cgit 


From 225e51bcf9bfe4029e0d9ca5617ad288326e68c9 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 15:44:38 +0100
Subject: implement for another register configuration

---
 riscV/Asmexpand.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'riscV')

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index f23db36e..1f6597d1 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -592,7 +592,14 @@ let expand_instruction instr =
        if not (ireg0_eq rt rf)
        then
          if (ireg0_eq (X rd) rt) 
-         then failwith "Pselectl rd=rt"
+         then
+           begin
+             emit (Psubl(X31, X0, rb));
+             emit (Pandl(X31, X X31, rt));
+             emit (Paddil(rd, rb, Int64.mone));
+             emit (Pandl(rd, X rd, rf));
+             emit (Porl(rd, X rd, X X31))
+           end
          else
            if (ireg0_eq (X rd) rf)
            then
-- 
cgit 


From 11018c3d46845722daf73883ce3959afdd6ac92f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 16:34:28 +0100
Subject: Cmov Tsingle

---
 riscV/ExtValues.v     | 10 +++++++++
 riscV/SelectOp.vp     |  7 ++++++
 riscV/SelectOpproof.v | 59 +++++++++++++++++++++++----------------------------
 3 files changed, 43 insertions(+), 33 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index aebbe5c5..edf359ef 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -111,3 +111,13 @@ Proof.
   f_equal.
   apply Float.of_to_bits.
 Qed.
+
+Lemma single_bits_normalize:
+  forall v1,
+  ExtValues.single_of_bits (Val.normalize (ExtValues.bits_of_single v1) AST.Tint) =
+  Val.normalize v1 AST.Tsingle.
+Proof.
+  destruct v1; cbn; trivial.
+  f_equal.
+  apply Float32.of_to_bits.
+Qed.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index b6720e40..bc169006 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -433,6 +433,13 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
                        ((Eop (Ocmp cond) args) :::
 		         (Eop Obits_of_float (e1 ::: Enil)) :::
 			 (Eop Obits_of_float (e2 ::: Enil)) ::: Enil)) ::: Enil))
+      | Tsingle => Some
+         (Eop Osingle_of_bits
+           ((Eop Olowlong ((Eop Oselectl
+             ((Eop (Ocmp cond) args) :::
+         (Eop Ocast32signed ((Eop Obits_of_single (e1 ::: Enil)) ::: Enil)) :::
+	 (Eop Ocast32signed ((Eop Obits_of_single (e2 ::: Enil)) ::: Enil))
+	 ::: Enil)) ::: Enil)) ::: Enil))
       | _ => None
       end
       else None.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index c313fbaf..1fe4e662 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -943,50 +943,43 @@ Proof.
   destruct Archi.ptr64 eqn:PTR64.
   2: discriminate.
   destruct ty; cbn in *; try discriminate.
-  - inv H. TrivialExists.
-    + cbn. constructor.
-      { econstructor.
-        { constructor.
-          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
-          constructor. econstructor. constructor. eassumption.
-          constructor. cbn. reflexivity.
-          constructor. econstructor. constructor. eassumption. constructor.
-          cbn. reflexivity. constructor.
-        }
-        constructor.
-      }
-      constructor.
+  - (* Tint *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
     + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      destruct b.
+      rewrite H3. destruct b.
       * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
       * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
-  - inv H. TrivialExists.
-    + cbn. constructor.
-      { econstructor.
-        { constructor.
-          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
-          constructor. econstructor. constructor. eassumption.
-          constructor. cbn. reflexivity.
-          constructor. econstructor. constructor. eassumption. constructor.
-          cbn. reflexivity. constructor.
-        }
-        constructor.
-      }
-      constructor.
+        
+  - (* Tfloat *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
     + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      destruct b.
+      rewrite H3. destruct b.
       * rewrite ExtValues.select01_long_true.
         apply ExtValues.float_bits_normalize.
       * rewrite ExtValues.select01_long_false.
         apply ExtValues.float_bits_normalize.
-  - inv H. TrivialExists.
-    + cbn. constructor.
-      { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
-      constructor. eassumption. constructor. eassumption. constructor.
+
+  - (* Tlong *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
     + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      destruct b.
+      rewrite H3. destruct b.
       * rewrite ExtValues.select01_long_true. reflexivity.
       * rewrite ExtValues.select01_long_false. reflexivity.
+
+  - (* Tsingle *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      rewrite H3. destruct b.
+      * rewrite ExtValues.select01_long_true.
+        rewrite normalize_low_long by assumption.
+        apply ExtValues.single_bits_normalize.
+      * rewrite ExtValues.select01_long_false.
+        rewrite normalize_low_long by assumption.
+        apply ExtValues.single_bits_normalize.
 Qed.
 
 Theorem eval_addressing:
-- 
cgit 


From afe54de36234834449e72d9dc891a90291aadcb1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 18:19:01 +0100
Subject: fix problem if rt = rf

---
 riscV/Asmexpand.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'riscV')

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 1f6597d1..14407bba 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -589,10 +589,13 @@ let expand_instruction instr =
      if not Archi.ptr64
      then failwith "Pselectl not available on RV32, only on RV64"
      else
-       if not (ireg0_eq rt rf)
-       then
-         if (ireg0_eq (X rd) rt) 
-         then
+       if ireg0_eq rt rf then
+         begin
+           if not (ireg0_eq (X rd) rt) then
+             emit (Paddil(rd, rt, Int64.zero))
+         end
+       else
+         if (ireg0_eq (X rd) rt) then
            begin
              emit (Psubl(X31, X0, rb));
              emit (Pandl(X31, X X31, rt));
@@ -601,8 +604,7 @@ let expand_instruction instr =
              emit (Porl(rd, X rd, X X31))
            end
          else
-           if (ireg0_eq (X rd) rf)
-           then
+           if (ireg0_eq (X rd) rf) then
              begin
                emit (Paddil(X31, rb, Int64.mone));
                emit (Pandl(X31, X X31, rf));
-- 
cgit 


From 90493ef36faa2925dbb107a994a57f010424fcbd Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 18:25:47 +0100
Subject: fix code generation for select(b, r, r)

---
 riscV/Asmexpand.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'riscV')

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 14407bba..c5cd6817 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -591,8 +591,13 @@ let expand_instruction instr =
      else
        if ireg0_eq rt rf then
          begin
-           if not (ireg0_eq (X rd) rt) then
-             emit (Paddil(rd, rt, Int64.zero))
+           if ireg0_eq (X rd) rt then
+             begin
+             end
+           else
+             begin
+               emit (Paddl(rd, X0, rt))
+             end
          end
        else
          if (ireg0_eq (X rd) rt) then
-- 
cgit 


From 48d2d8755ec840cc15cfab9663f0e1e1ef47d65f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 19:00:55 +0100
Subject: detect redundant cmov

---
 riscV/SelectOp.vp     | 15 ++++++++++++---
 riscV/SelectOpproof.v | 22 ++++++++++++++++++++++
 2 files changed, 34 insertions(+), 3 deletions(-)

(limited to 'riscV')

diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index bc169006..9932aaf8 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -419,9 +419,18 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 (** ** Selection *)
 
+Definition same_expr_pure (e1 e2: expr) :=
+  match e1, e2 with
+  | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false
+  | _, _ => false
+  end.
+
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
-   : option expr
-   := if Archi.ptr64 then
+  : option expr :=
+  if same_expr_pure e1 e2
+  then Some e1
+  else
+     if Archi.ptr64 then
       match ty with
       | Tlong => Some (Eop Oselectl
                        ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil))
@@ -488,4 +497,4 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   | BI_bits_of_double => Some (Eop Obits_of_float args)
   | BI_float_of_bits => Some (Eop Osingle_of_bits args)
   | BI_double_of_bits => Some (Eop Ofloat_of_bits args)
-  end.
\ No newline at end of file
+  end.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 1fe4e662..ce80fc57 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -928,6 +928,19 @@ Proof.
   }
 Qed.
 
+Lemma same_expr_pure_correct:
+  forall le a1 a2 v1 v2
+    (PURE : same_expr_pure a1 a2 = true)
+    (EVAL1 : eval_expr ge sp e m le a1 v1)
+    (EVAL2 : eval_expr ge sp e m le a2 v2),
+    v1 = v2.
+Proof.
+  intros.
+  destruct a1; destruct a2; cbn in *; try discriminate.
+  inv EVAL1. inv EVAL2.
+  destruct (ident_eq i i0); congruence.
+Qed.
+  
 Theorem eval_select:
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
@@ -940,6 +953,15 @@ Theorem eval_select:
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
   unfold select; intros.
+  pose proof (same_expr_pure_correct le a1 a2 v1 v2) as PURE.
+  destruct (same_expr_pure a1 a2).
+  { rewrite <- PURE by auto.
+    inv H.
+    exists v1. split. assumption.
+    unfold Val.select.
+    destruct b; apply Val.lessdef_normalize.
+  }
+  clear PURE.
   destruct Archi.ptr64 eqn:PTR64.
   2: discriminate.
   destruct ty; cbn in *; try discriminate.
-- 
cgit 


From 6c72e95b59f07e7356c05d95b3015df01a4389cf Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 3 Feb 2021 14:29:33 +0100
Subject: écrase X31
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 riscV/Asm.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'riscV')

diff --git a/riscV/Asm.v b/riscV/Asm.v
index 9a4b2a57..5d3518f2 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -957,7 +957,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       end
   | Pselectl rd rb rt rf =>
     Next (nextinstr (rs#rd <- (ExtValues.select01_long
-                                (rs###rb) (rs###rt) (rs###rf)))) m
+                                 (rs###rb) (rs###rt) (rs###rf)))
+                     #X31 <- Vundef) m
   | Plabel lbl =>
       Next (nextinstr rs) m
   | Ploadsymbol rd s ofs =>
-- 
cgit 


From a9763cd4327e12316d62e80648122f122581cca4 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 25 Feb 2021 11:43:20 +0100
Subject: Adding missing operators in PrintOp for debugging

---
 riscV/PrintOp.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'riscV')

diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 9ec474b3..7e78283e 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -156,6 +156,11 @@ let print_operation reg pp = function
   | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1
   | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1
   | Ocmp c, args -> print_condition reg pp (c, args)
+  | Obits_of_single, [r1] -> fprintf pp "bits_of_single(%a)" reg r1
+  | Obits_of_float, [r1] -> fprintf pp "bits_of_float(%a)" reg r1
+  | Osingle_of_bits, [r1] -> fprintf pp "single_of_bits(%a)" reg r1
+  | Ofloat_of_bits, [r1] -> fprintf pp "float_of_bits(%a)" reg r1
+  | Oselectl, [rb;rt;rf] -> fprintf pp "selectl(b:%a, t:%a, f:%a)" reg rb reg rt reg rf
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function
-- 
cgit