Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work

1 files changed, 107 insertions, 0 deletions

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 00b49bc1..97f3ff61 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -86,6 +86,39 @@ 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 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 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
@@ -210,6 +243,11 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2)
   | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2)
   | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2)
+  | 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
+  | Oselectl, vb::vt::vf::nil => select01_long vb vt vf
   | _, _ => Vbot
   end.
 
@@ -221,6 +259,75 @@ 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.
+
+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.
+
+  
+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,
   list_forall2 (vmatch bc) vargs aargs ->