begin implementing select

8 files changed, 114 insertions, 6 deletions

diff --git a/configure b/configure
index f93605de..812ad6f7 100755
--- a/configure
+++ b/configure
@@ -844,6 +844,7 @@ fi
 
 if [ "$arch" = "riscV" ] ; then
 cat >> Makefile.config <<EOF
+EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq
 BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v
 EOF
 fi
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 ->