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(-)

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