From 73ab7968d862c4d4d883fb3d3215353eba905b0f Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Fri, 15 Dec 2017 00:01:30 +0100 Subject: Introduce 'cmn' instruction and optimize compare-with-immediate when negated immediates can be encoded. --- arm/Asm.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index c05ec3e9..184dbc9b 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -148,6 +148,7 @@ Inductive instruction : Type := | Pblreg: ireg -> signature -> instruction (**r computed branch and link *) | Pbic: ireg -> ireg -> shift_op -> instruction (**r bitwise bit-clear *) | Pcmp: ireg -> shift_op -> instruction (**r integer comparison *) + | Pcmn: ireg -> shift_op -> instruction (**r integer comparison with opposite *) | Peor: ireg -> ireg -> shift_op -> instruction (**r bitwise exclusive or *) | Pldr: ireg -> ireg -> shift_op -> instruction (**r int32 load *) | Pldr_a: ireg -> ireg -> shift_op -> instruction (**r any32 load to int register *) @@ -608,6 +609,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr_nf (rs#r1 <- (Val.and rs#r2 (Val.notint (eval_shift_op so rs))))) m | Pcmp r1 so => Next (nextinstr (compare_int rs rs#r1 (eval_shift_op so rs) m)) m + | Pcmn r1 so => + Next (nextinstr (compare_int rs rs#r1 (Val.neg (eval_shift_op so rs)) m)) m | Peor r1 r2 so => Next (nextinstr_nf (rs#r1 <- (Val.xor rs#r2 (eval_shift_op so rs)))) m | Pldr r1 r2 sa => -- cgit