From 1a3c8d42aa760a0dc30552d9375db3fdf1a48d20 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Tue, 7 Jul 2020 10:51:47 +0200 Subject: Inline Pcset in ar_instruction --- aarch64/Asmblock.v | 20 ++++---------------- 1 file changed, 4 insertions(+), 16 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index e0815890..90ca7e05 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -284,15 +284,6 @@ Inductive arith_p : Type := | Pfmovimmd (f: float) (**r load float64 constant *) . -(* Arithmetic instructions with conditional execution *) -Inductive arith_c_p : Type := - (** Conditional data processing *) - | Pcset (**r set to 1/0 if cond is true/false *) -(* - | Pcsetm (**r set to -1/0 if cond is true/false *) -*) -. - Inductive arith_comparison_p : Type := (** Floating-point comparison *) | Pfcmp0 (sz: fsize) (**r compare [r1] and [+0.0] *) @@ -451,7 +442,6 @@ Inductive arith_appp : Type := *) Inductive ar_instruction : Type := | PArithP (i : arith_p) (rd : preg) - | PArithCP (i : arith_c_p) (rd : preg) (c : testcond) | PArithPP (i : arith_pp) (rd rs : preg) | PArithPPP (i : arith_ppp) (rd r1 r2 : preg) | PArithCPPP (i : arith_c_ppp) (rd r1 r2 : preg) (c : testcond) @@ -467,6 +457,9 @@ Inductive ar_instruction : Type := | PArithComparisonPP (i : arith_comparison_pp) (r1 r2 : preg) | PArithComparisonR0R (i : arith_comparison_r0r) (r1 : ireg0) (r2 : ireg) | PArithComparisonP (i : arith_comparison_p) (r1 : preg) + (* Instructions without indirection sine they would be the only ones *) + (* PArithCP: Pcsetm is commented out by aarch64/Asm, so Pcset is alone *) + | Pcset (rd : preg) (c : testcond) . Inductive basic : Type := @@ -1211,11 +1204,6 @@ Definition if_opt_bool_val (c: option bool) v1 v2: val := | None => Vundef end. -Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val := - match i with - | Pcset => if_opt_bool_val c (Vint Int.one) (Vint Int.zero) - end. - Definition arith_eval_pp i v := match i with | Pmov => v @@ -1444,7 +1432,6 @@ Definition arith_comparison_p_compare i := Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithP i d => rs#d <- (arith_eval_p i) - | PArithCP i d c => rs#d <- (arith_eval_c_p i (eval_testcond c rs)) | PArithPP i d s => rs#d <- (arith_eval_pp i rs#s) | PArithPPP i d s1 s2 => rs#d <- (arith_eval_ppp i rs#s1 rs#s2) | PArithCPPP i d s1 s2 c => rs#d <- (arith_eval_c_ppp i rs#s1 rs#s2 (eval_testcond c rs)) @@ -1470,6 +1457,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithComparisonP i s => let (v1, v2) := arith_prepare_comparison_p i rs#s in arith_comparison_p_compare i rs v1 v2 + | Pcset d c => rs#d <- (if_opt_bool_val (eval_testcond c rs) (Vint Int.one) (Vint Int.zero)) end. (* basic exec *) -- cgit