asmgen Oselectl

2 files changed, 11 insertions, 0 deletions

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