diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-12-15 00:01:30 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2017-12-15 00:01:30 +0100 |
| commit | 73ab7968d862c4d4d883fb3d3215353eba905b0f (patch) | |
| tree | ed09a92dc480a54eb26987e66d3dfb83fbe03de7 /arm/Asm.v | |
| parent | cdf6681b3450baa1489c6a62e1903a450c0e2c3f (diff) | |
| download | compcert-kvx-73ab7968d862c4d4d883fb3d3215353eba905b0f.tar.gz compcert-kvx-73ab7968d862c4d4d883fb3d3215353eba905b0f.zip | |
Introduce 'cmn' instruction and optimize compare-with-immediate when negated immediates can be encoded.
Diffstat (limited to 'arm/Asm.v')
| -rw-r--r-- | arm/Asm.v | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -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 => |