for floats and doubles, asmgen support

1 files changed, 35 insertions, 6 deletions

diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index da108ada..122249a4 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -59,6 +59,24 @@ Definition selectl (v0 v1 vselect : aval) : aval :=
     else binop_long (fun x0 x1 => x1) v0 v1
   | _ => Vtop
   end.
+
+Definition selectf (v0 v1 vselect : aval) : aval :=
+  match vselect with
+  | I iselect =>
+    if Int.eq Int.zero iselect
+    then binop_float (fun x0 x1 => x0) v0 v1
+    else binop_float (fun x0 x1 => x1) v0 v1
+  | _ => Vtop
+  end.
+
+Definition selectfs (v0 v1 vselect : aval) : aval :=
+  match vselect with
+  | I iselect =>
+    if Int.eq Int.zero iselect
+    then binop_single (fun x0 x1 => x0) v0 v1
+    else binop_single (fun x0 x1 => x1) v0 v1
+  | _ => Vtop
+  end.
   
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
@@ -186,6 +204,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
   | Oselect, v0::v1::vselect::nil => select v0 v1 vselect
   | Oselectl, v0::v1::vselect::nil => selectl v0 v1 vselect               
+  | Oselectf, v0::v1::vselect::nil => selectf v0 v1 vselect
+  | Oselectfs, v0::v1::vselect::nil => selectfs v0 v1 vselect               
   | _, _ => Vbot
   end.
 
@@ -265,18 +285,27 @@ Proof.
   (* select *)
   - inv H2; simpl; try constructor.
     + destruct (Int.eq _ _); apply binop_int_sound; trivial.
-    + destruct (Int.eq _ _);
-      destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _);
-      destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _);
-      destruct a1; destruct a0; eauto; constructor.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
   (* selectl *)
   - inv H2; simpl; try constructor.
     + destruct (Int.eq _ _); apply binop_long_sound; trivial.
     + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
     + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
     + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+  (* selectf *)
+  - inv H2; simpl; try constructor.
+    + destruct (Int.eq _ _); apply binop_float_sound; trivial.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+  (* selectfs *)
+  - inv H2; simpl; try constructor.
+    + destruct (Int.eq _ _); apply binop_single_sound; trivial.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
 Qed.
 
 End SOUNDNESS.