diff options
| -rw-r--r-- | aarch64/Asmblock.v | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index b37b6e27..193941aa 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1443,6 +1443,21 @@ Definition arith_prepare_comparison_p i v := | Pfcmp0 D => (v, (Vfloat Float.zero)) end. +Definition arith_comparison_pp_compare i := + match i with + | Pcmpext _ | Pcmnext _ => compare_long + | Pfcmp S => compare_single + | Pfcmp D => compare_float + end. + +Definition arith_comparison_p_compare i := + match i with + | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int + | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long + | Pfcmp0 S => compare_single + | Pfcmp0 D => compare_float + end. + Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithP i d => rs#d <- (arith_eval_p i) @@ -1466,23 +1481,14 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithComparisonPP i s1 s2 => let (v1, v2) := arith_prepare_comparison_pp i rs#s1 rs#s2 in - (match i with - | Pcmpext _ | Pcmnext _ => compare_long rs v1 v2 - | Pfcmp S => compare_single rs v1 v2 - | Pfcmp D => compare_float rs v1 v2 - end) + arith_comparison_pp_compare i rs v1 v2 | PArithComparisonR0R i s1 s2 => let is := arith_comparison_r0r_isize i in let (v1, v2) := arith_prepare_comparison_r0r i (ir0 is rs s1) rs#s2 in (if is (* is W *) then compare_int else compare_long) rs v1 v2 | PArithComparisonP i s => let (v1, v2) := arith_prepare_comparison_p i rs#s in - (match i with - | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => compare_int rs v1 v2 - | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => compare_long rs v1 v2 - | Pfcmp0 S => compare_single rs v1 v2 - | Pfcmp0 D => compare_float rs v1 v2 - end) + arith_comparison_p_compare i rs v1 v2 end. (* basic exec *) |