Asmblock: Add instructions with conditional execution

1 files changed, 41 insertions, 6 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index e98eeadd..14613fd3 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -285,9 +285,9 @@ Inductive arith_r : Type :=
 (* TODO matching case in ar_instruction *)
 Inductive arith_name_c_r : Type :=
   (** Conditional data processing *)
-  | Pcset (c: testcond)                                    (**r set to 1/0 if cond is true/false *)
+  | Pcset                                       (**r set to 1/0 if cond is true/false *)
 (*
-  | Pcsetm (c: testcond)                                   (**r set to -1/0 if cond is true/false *)
+  | Pcsetm                                      (**r set to -1/0 if cond is true/false *)
 *)
 .
 
@@ -412,7 +412,7 @@ Inductive arith_name_rrr : Type :=
 (* TODO matching case in ar_instruction *)
 Inductive arith_name_c_rrr : Type :=
   (** Conditional data processing *)
-  | Pcsel (c: testcond)                               (**r int conditional move *)
+  | Pcsel                                             (**r int conditional move *)
 .
 
 Inductive arith_name_rsprspr : Type :=
@@ -458,7 +458,7 @@ Inductive arith_name_fff : Type :=
 (* TODO matching case in ar_instruction *)
 Inductive arith_name_c_fff : Type :=
   (** Floating-point conditional select *)
-  | Pfsel (cond: testcond)
+  | Pfsel
 .
 
 Inductive arith_name_rsprsp : Type :=
@@ -527,9 +527,11 @@ Inductive arith_name_aaffff : Type :=
  *)
 Inductive ar_instruction : Type :=
   | PArithR (i : arith_r) (rd : ireg)
+  | PArithCR (i : arith_name_c_r) (rd : ireg) (c : testcond)
   | PArithRR (i : arith_name_rr) (rd rs : ireg)
   | PArithRF (i : arith_name_rf) (rd : ireg) (rs : freg)
   | PArithRRR (i : arith_name_rrr) (rd r1 r2 : ireg)
+  | PArithCRRR (i : arith_name_c_rrr) (rd r1 r2 : ireg) (c : testcond)
   | PArithWRR0R (i : arith_name_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithXRR0R (i : arith_name_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
   | PArithWRR0 (i : arith_name_w_rr0) (rd : ireg) (r1 : ireg0)
@@ -544,6 +546,7 @@ Inductive ar_instruction : Type :=
   | PArithSWFR0 (i : arith_name_sw_fr0) (rd : freg) (rs : ireg0)
   | PArithDXFR0 (i : arith_name_dx_fr0) (rd : freg) (rs : ireg0)
   | PArithFFF (i : arith_name_fff) (rd r1 r2 : freg)
+  | PArithCFFF (i : arith_name_c_fff) (rd r1 r2 : freg) (c : testcond)
   | PArithAFFF (i : arith_name_afff) (rd r1 r2 : freg)
   (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm
   | PArithAFFFF (i : arith_name_affff) (rd r1 r2 r3 : freg) *)
@@ -1295,6 +1298,16 @@ Definition arith_eval_r (i:arith_r): val :=
   | Pmovk X pos => insert_in_long rs#rd n pos 16 *)
   end.
 
+Definition arith_eval_c_r (i : arith_name_c_r) (c : option bool) : val :=
+  match i with
+  | Pcset =>
+    (match c with
+    | Some true => Vint Int.one
+    | Some false =>  Vint Int.zero
+    | None => Vundef
+    end)
+  end.
+
 Definition arith_eval_rr n v :=
   match n with
   | Pmov => v
@@ -1341,6 +1354,16 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pudiv X => Val.maketotal (Val.divlu v1 v2)
   end.
 
+Definition arith_eval_c_rrr (i : arith_name_c_rrr) (v1 v2 : val) (c : option bool) :=
+  match i with
+  | Pcsel =>
+    (match c with
+    | Some true => v1
+    | Some false => v2
+    | None => Vundef
+    end)
+  end.
+
 (* obtain v1 by rs##r1 *)
 Definition arith_eval_w_rr0r n v1 v2 :=
   match n with
@@ -1464,6 +1487,16 @@ Definition arith_eval_fff n v1 v2 :=
   | Pfsub D => Val.subf v1 v2
   end.
 
+Definition arith_eval_c_fff (i : arith_name_c_fff) (v1 v2 : val) (c : option bool) :=
+  match i with
+  | Pfsel =>
+    (match c with
+    | Some true => v1
+    | Some false => v2
+    | None => Vundef
+    end)
+  end.
+
 Definition arith_eval_afff n v1 v2 :=
   match n with
   | Pfnmul S => Val.negfs (Val.mulfs v1 v2)
@@ -1515,9 +1548,11 @@ Definition arith_prepare_comparison_ff n (v1 v2 : val) :=
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithR i d => rs#d <- (arith_eval_r i)
+  | PArithCR i d c => rs#d <- (arith_eval_c_r i (eval_testcond c rs))
   | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s)
   | PArithRF n d s => rs#d <- (arith_eval_rf n rs#s)
   | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2)
+  | PArithCRRR n d s1 s2 c => rs#d <- (arith_eval_c_rrr n rs#s1 rs#s2 (eval_testcond c rs))
 
   | PArithWRR0R n d s1 s2 => rs#d <- (arith_eval_w_rr0r n rs##s1 rs#s2)
   | PArithXRR0R n d s1 s2 => rs#d <- (arith_eval_x_rr0r n rs###s1 rs#s2)
@@ -1539,6 +1574,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithDXFR0 n d s => rs#d <- (arith_eval_dx_fr0 n rs###s)
 
   | PArithFFF n d s1 s2 => rs#d <- (arith_eval_fff n rs#s1 rs#s2)
+  | PArithCFFF n d s1 s2 c => rs#d <- (arith_eval_c_fff n rs#s1 rs#s2 (eval_testcond c rs))
   | PArithAFFF n d s1 s2 => rs#d <- (arith_eval_afff n rs#s1 rs#s2)
 
   | PArithComparisonRR n s1 s2 =>
@@ -1855,8 +1891,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#rd <- v)) m
   | Pcset rd cond =>
       let v :=
-        match 
- cond rs with
+        match cond rs with
         | Some true => Vint Int.one
         | Some false => Vint Int.zero
         | None => Vundef