261 lines
38 KiB
Text
261 lines
38 KiB
Text
ad "adc r0, r1" 011C 0x0 (seq (set RES (+ (+ (var r0) (var r1)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set hf (! (is_zero (& (| (| (& (var r0) (var r1)) (& (var r1) (~ (var RES)))) (& (~ (var RES)) (var r0))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r0) (var r1)) (~ (var RES))) (& (& (~ (var r0)) (~ (var r1))) (var RES))))) (set nf (msb (var RES))) (set zf (is_zero (var RES))) (set cf (msb (| (| (& (var r0) (var r1)) (& (var r1) (~ (var RES)))) (& (~ (var RES)) (var r0))))) (set sf (^^ (var nf) (var vf))) (set r0 (var RES)))
|
|
ad "adc r21, r25" 591f 0x0 (seq (set RES (+ (+ (var r21) (var r25)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set hf (! (is_zero (& (| (| (& (var r21) (var r25)) (& (var r25) (~ (var RES)))) (& (~ (var RES)) (var r21))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r21) (var r25)) (~ (var RES))) (& (& (~ (var r21)) (~ (var r25))) (var RES))))) (set nf (msb (var RES))) (set zf (is_zero (var RES))) (set cf (msb (| (| (& (var r21) (var r25)) (& (var r25) (~ (var RES)))) (& (~ (var RES)) (var r21))))) (set sf (^^ (var nf) (var vf))) (set r21 (var RES)))
|
|
ad "add r0, r1" 010C 0x0 (seq (set RES (+ (var r0) (var r1))) (set hf (! (is_zero (& (| (| (& (var r0) (var r1)) (& (var r1) (~ (var RES)))) (& (~ (var RES)) (var r0))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r0) (var r1)) (~ (var RES))) (& (& (~ (var r0)) (~ (var r1))) (var RES))))) (set nf (msb (var RES))) (set zf (is_zero (var RES))) (set cf (msb (| (| (& (var r0) (var r1)) (& (var r1) (~ (var RES)))) (& (~ (var RES)) (var r0))))) (set sf (^^ (var nf) (var vf))) (set r0 (var RES)))
|
|
ad "add r20, r24" 480f 0x0 (seq (set RES (+ (var r20) (var r24))) (set hf (! (is_zero (& (| (| (& (var r20) (var r24)) (& (var r24) (~ (var RES)))) (& (~ (var RES)) (var r20))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r20) (var r24)) (~ (var RES))) (& (& (~ (var r20)) (~ (var r24))) (var RES))))) (set nf (msb (var RES))) (set zf (is_zero (var RES))) (set cf (msb (| (| (& (var r20) (var r24)) (& (var r24) (~ (var RES)))) (& (~ (var RES)) (var r20))))) (set sf (^^ (var nf) (var vf))) (set r20 (var RES)))
|
|
ad "adiw r25:r24, 0x00" 0096 0x0 (seq (set IND (+ (append (var r25) (var r24)) (bv 16 0x0))) (set r25 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r24 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (! (msb (var r25))) (msb (var IND)))) (set nf (msb (var IND))) (set cf (&& (! (msb (var IND))) (msb (var r25)))) (set sf (^^ (var nf) (var vf))))
|
|
ad "adiw r25:r24, 0x01" 0196 0x0 (seq (set IND (+ (append (var r25) (var r24)) (bv 16 0x1))) (set r25 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r24 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (! (msb (var r25))) (msb (var IND)))) (set nf (msb (var IND))) (set cf (&& (! (msb (var IND))) (msb (var r25)))) (set sf (^^ (var nf) (var vf))))
|
|
ad "adiw r27:r26, 0x01" 1196 0x0 (seq (set IND (+ (append (var r27) (var r26)) (bv 16 0x1))) (set r27 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r26 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (! (msb (var r27))) (msb (var IND)))) (set nf (msb (var IND))) (set cf (&& (! (msb (var IND))) (msb (var r27)))) (set sf (^^ (var nf) (var vf))))
|
|
ad "adiw r27:r26, 0x3f" df96 0x0 (seq (set IND (+ (append (var r27) (var r26)) (bv 16 0x3f))) (set r27 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r26 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (! (msb (var r27))) (msb (var IND)))) (set nf (msb (var IND))) (set cf (&& (! (msb (var IND))) (msb (var r27)))) (set sf (^^ (var nf) (var vf))))
|
|
a "adiw r24, 0x00" 0096
|
|
a "adiw r24, 0x01" 0196
|
|
a "adiw r26, 0x01" 1196
|
|
a "adiw r26, 63" df96
|
|
ad "and r0, r1" 0120 0x0 (seq (set r0 (& (var r0) (var r1))) (set vf false) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))))
|
|
ad "andi r16, 0x00" 0070 0x0 (seq (set r16 (& (var r16) (bv 8 0x0))) (set vf false) (set nf (msb (var r16))) (set zf (is_zero (var r16))) (set sf (^^ (var nf) (var vf))))
|
|
ad "andi r24, 0xef" 8f7e 0x0 (seq (set r24 (& (var r24) (bv 8 0xef))) (set vf false) (set nf (msb (var r24))) (set zf (is_zero (var r24))) (set sf (^^ (var nf) (var vf))))
|
|
ad "asr r0" 0594 0x0 (seq (set cf (lsb (var r0))) (set r0 (>> (var r0) (bv 32 0x1) (msb (var r0)))) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))) (set vf (^^ (var nf) (var cf))))
|
|
a "bclr 7" f894
|
|
a "bclr 2" a894
|
|
ad "bld r0, 0" 00F8 0x0 (set r0 (ite (var tf) (| (var r0) (bv 8 0x1)) (& (var r0) (bv 8 0xfe))))
|
|
ad "bld r14, 1" e1f8 0x0 (set r14 (ite (var tf) (| (var r14) (bv 8 0x2)) (& (var r14) (bv 8 0xfd))))
|
|
a "brbc 5, 2" 05f4
|
|
a "brbc 5, 0xffffffffffffff84" 0df6
|
|
a "brbs 5, 2" 05f0
|
|
a "brbs 5, 0xffffffffffffff84" 0df2
|
|
ad "brcc 0x2" 00F4 0x0 (branch (var cf) nop (jmp (bv 32 0x2)))
|
|
ad "brcc 0x4" 08f4 0x0 (branch (var cf) nop (jmp (bv 32 0x4)))
|
|
ad "brcc 0xffffffffffffff84" 08f6 0x0 (branch (var cf) nop (jmp (bv 32 0xff84)))
|
|
ad "brcs 0x2" 00F0 0x0 (branch (var cf) (jmp (bv 32 0x2)) nop)
|
|
ad "brcs 0x4" 08f0 0x0 (branch (var cf) (jmp (bv 32 0x4)) nop)
|
|
ad "brcs 0xffffffffffffff84" 08f2 0x0 (branch (var cf) (jmp (bv 32 0xff84)) nop)
|
|
ad "break" 9895 0x0 nop
|
|
ad "breq 0x2" 01F0 0x0 (branch (var zf) (jmp (bv 32 0x2)) nop)
|
|
ad "breq 0x6" 09f0 2 (branch (var zf) (jmp (bv 32 0x6)) nop)
|
|
ad "breq 0xffffffffffffff84" 09f2 0x0 (branch (var zf) (jmp (bv 32 0xff84)) nop)
|
|
ad "brge 0x2" 04F4 0x0 (branch (^^ (var nf) (var vf)) nop (jmp (bv 32 0x2)))
|
|
ad "brge 0xc" 0cf4 8 (branch (^^ (var nf) (var vf)) nop (jmp (bv 32 0xc)))
|
|
ad "brge 0xffffffffffffff84" 0cf6 0x0 (branch (^^ (var nf) (var vf)) nop (jmp (bv 32 0xff84)))
|
|
ad "brhc 0x2" 05F4 0x0 (branch (var hf) nop (jmp (bv 32 0x2)))
|
|
ad "brhc 0xe" 0df4 0xa (branch (var hf) nop (jmp (bv 32 0xe)))
|
|
ad "brhc 0xffffffffffffff84" 0df6 0x0 (branch (var hf) nop (jmp (bv 32 0xff84)))
|
|
ad "brhs 0x2" 05F0 0x0 (branch (var hf) (jmp (bv 32 0x2)) nop)
|
|
ad "brhs 0xe" 0df0 0xa (branch (var hf) (jmp (bv 32 0xe)) nop)
|
|
ad "brhs 0xffffffffffffff84" 0df2 0x0 (branch (var hf) (jmp (bv 32 0xff84)) nop)
|
|
ad "brid 0x12" 0ff4 0xe (branch (var if) nop (jmp (bv 32 0x12)))
|
|
ad "brid 0x2" 07F4 0x0 (branch (var if) nop (jmp (bv 32 0x2)))
|
|
ad "brid 0xffffffffffffff84" 0ff6 0x0 (branch (var if) nop (jmp (bv 32 0xff84)))
|
|
ad "brie 0x12" 0ff0 0xe (branch (var if) (jmp (bv 32 0x12)) nop)
|
|
ad "brie 0x2" 07F0 0x0 (branch (var if) (jmp (bv 32 0x2)) nop)
|
|
ad "brie 0xffffffffffffff84" 0ff2 0x0 (branch (var if) (jmp (bv 32 0xff84)) nop)
|
|
ad "brlt 0x2" 04F0 0x0 (branch (^^ (var nf) (var vf)) (jmp (bv 32 0x2)) nop)
|
|
ad "brlt 0xc" 0cf0 8 (branch (^^ (var nf) (var vf)) (jmp (bv 32 0xc)) nop)
|
|
ad "brlt 0xffffffffffffff84" 0cf2 0x0 (branch (^^ (var nf) (var vf)) (jmp (bv 32 0xff84)) nop)
|
|
ad "brmi 0x2" 02F0 0x0 (branch (var nf) (jmp (bv 32 0x2)) nop)
|
|
ad "brmi 0x8" 0af0 4 (branch (var nf) (jmp (bv 32 0x8)) nop)
|
|
ad "brmi 0xffffffffffffff84" 0af2 0x0 (branch (var nf) (jmp (bv 32 0xff84)) nop)
|
|
ad "brne 0x2" 01F4 0x0 (branch (var zf) nop (jmp (bv 32 0x2)))
|
|
ad "brne 0x6" 09f4 2 (branch (var zf) nop (jmp (bv 32 0x6)))
|
|
ad "brne 0xffffffffffffff84" 09f6 0x0 (branch (var zf) nop (jmp (bv 32 0xff84)))
|
|
ad "brpl 0x2" 02F4 0x0 (branch (var nf) nop (jmp (bv 32 0x2)))
|
|
ad "brpl 0x8" 0af4 4 (branch (var nf) nop (jmp (bv 32 0x8)))
|
|
ad "brpl 0xffffffffffffff84" 0af6 0x0 (branch (var nf) nop (jmp (bv 32 0xff84)))
|
|
ad "brtc 0x10" 0ef4 0xc (branch (var tf) nop (jmp (bv 32 0x10)))
|
|
ad "brtc 0x2" 06F4 0x0 (branch (var tf) nop (jmp (bv 32 0x2)))
|
|
ad "brtc 0xffffffffffffff84" 0ef6 0x0 (branch (var tf) nop (jmp (bv 32 0xff84)))
|
|
ad "brts 0x10" 0ef0 0xc (branch (var tf) (jmp (bv 32 0x10)) nop)
|
|
ad "brts 0x2" 06F0 0x0 (branch (var tf) (jmp (bv 32 0x2)) nop)
|
|
ad "brts 0xffffffffffffff84" 0ef2 0x0 (branch (var tf) (jmp (bv 32 0xff84)) nop)
|
|
ad "brvc 0x2" 03F4 0x0 (branch (var vf) nop (jmp (bv 32 0x2)))
|
|
ad "brvc 0xa" 0bf4 6 (branch (var vf) nop (jmp (bv 32 0xa)))
|
|
ad "brvc 0xffffffffffffff84" 0bf6 0x0 (branch (var vf) nop (jmp (bv 32 0xff84)))
|
|
ad "brvs 0x2" 03F0 0x0 (branch (var vf) (jmp (bv 32 0x2)) nop)
|
|
ad "brvs 0xa" 0bf0 6 (branch (var vf) (jmp (bv 32 0xa)) nop)
|
|
ad "brvs 0xffffffffffffff84" 0bf2 0x0 (branch (var vf) (jmp (bv 32 0xff84)) nop)
|
|
a "bset 7" 7894
|
|
a "bset 2" 2894
|
|
ad "bst r0, 0" 00FA 0x0 (set tf (! (is_zero (& (var r0) (bv 8 0x1)))))
|
|
ad "bst r0, 4" 04FA 0x0 (set tf (! (is_zero (& (var r0) (bv 8 0x10)))))
|
|
ad "call 0x0" 0E940000 0x0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x4)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x0)))
|
|
ad "call 0x16" 0e940b00 0x2d0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x2d4)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x16)))
|
|
ad "call 0x2016" 0e940b10 0x0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x4)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x2016)))
|
|
ad "call 0x3ffffe" FF94FFFF 0x0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x4)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x3ffffe)))
|
|
ad "cbi 0x00, 0" 0098 0x0 (set r0 (& (bv 8 0xfe) (var r0)))
|
|
ad "cbi 0x10, 4" 8498 0x0 (set r16 (& (bv 8 0xef) (var r16)))
|
|
a "cbr r16, 0xf0" 0f70
|
|
a "cbr r18, 1" 2e7f
|
|
ad "clc" 8894 0x0 (set cf false)
|
|
ad "clh" D894 0x0 (set hf false)
|
|
ad "cli" f894 0x0 (set if false)
|
|
ad "cli" F894 0x0 (set if false)
|
|
ad "cln" A894 0x0 (set nf false)
|
|
ad "clr r15" ff24 0x0 (seq (set r15 (bv 8 0x0)) (set sf false) (set vf false) (set nf false) (set zf true))
|
|
ad "cls" C894 0x0 (set sf false)
|
|
ad "clt" E894 0x0 (set tf false)
|
|
ad "clv" B894 0x0 (set vf false)
|
|
ad "clz" 9894 0x0 (set zf false)
|
|
ad "com r0" 0094 0x0 (seq (set r0 (- (bv 8 0xff) (var r0))) (set cf true) (set vf false) (set zf (is_zero (var r0))) (set nf (! (is_zero (& (var r0) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "com r24" 8095 0x0 (seq (set r24 (- (bv 8 0xff) (var r24))) (set cf true) (set vf false) (set zf (is_zero (var r24))) (set nf (! (is_zero (& (var r24) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "cp r0, r1" 0114 0x0 (seq (set RES (- (var r0) (var r1))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r0)) (var r1)) (& (var r1) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r0) (~ (var r1))) (~ (var RES))) (& (& (~ (var r0)) (var r1)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r0)) (var r1)) (& (var r1) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "cp r18, r24" 2817 0x0 (seq (set RES (- (var r18) (var r24))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r18)) (var r24)) (& (var r24) (var RES))) (& (var RES) (~ (var r18)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r18) (~ (var r24))) (~ (var RES))) (& (& (~ (var r18)) (var r24)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r18)) (var r24)) (& (var r24) (var RES))) (& (var RES) (~ (var r18)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "cpc r0, r1" 0104 0x0 (seq (set RES (- (- (var r0) (var r1)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set zf (&& (is_zero (var RES)) (var zf))) (set hf (! (is_zero (& (| (| (& (~ (var r0)) (var r1)) (& (var r1) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r0) (~ (var r1))) (~ (var RES))) (& (& (~ (var r0)) (var r1)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r0)) (var r1)) (& (var r1) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "cpc r25, r18" 9207 0x0 (seq (set RES (- (- (var r25) (var r18)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set zf (&& (is_zero (var RES)) (var zf))) (set hf (! (is_zero (& (| (| (& (~ (var r25)) (var r18)) (& (var r18) (var RES))) (& (var RES) (~ (var r25)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r25) (~ (var r18))) (~ (var RES))) (& (& (~ (var r25)) (var r18)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r25)) (var r18)) (& (var r18) (var RES))) (& (var RES) (~ (var r25)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "cpi r16, 0x00" 0030 0x0 (seq (set RES (- (var r16) (bv 8 0x0))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r16)) (bv 8 0x0)) (& (bv 8 0x0) (var RES))) (& (var RES) (~ (var r16)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r16) (~ (bv 8 0x0))) (~ (var RES))) (& (& (~ (var r16)) (bv 8 0x0)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r16)) (bv 8 0x0)) (& (bv 8 0x0) (var RES))) (& (var RES) (~ (var r16)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "cpi r24, 0xf5" 853f 0x0 (seq (set RES (- (var r24) (bv 8 0xf5))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r24)) (bv 8 0xf5)) (& (bv 8 0xf5) (var RES))) (& (var RES) (~ (var r24)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r24) (~ (bv 8 0xf5))) (~ (var RES))) (& (& (~ (var r24)) (bv 8 0xf5)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r24)) (bv 8 0xf5)) (& (bv 8 0xf5) (var RES))) (& (var RES) (~ (var r24)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))))
|
|
|
|
# this instruction is expecting to have an extra instruction after it but we cannot test this.
|
|
# the result is anyway correct because all jumps are (PC - 2) since the next instruction is of size 0
|
|
ad "cpse r0, r0" 0010 0x10 (branch (== (var r0) (var r0)) (jmp (bv 32 0x10)) nop)
|
|
|
|
ad "dec r0" 0a94 0x0 (seq (set vf (== (var r0) (bv 8 0x80))) (set r0 (- (var r0) (bv 8 0x1))) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))))
|
|
ad "dec r8" 8A94 0x0 (seq (set vf (== (var r8) (bv 8 0x80))) (set r8 (- (var r8) (bv 8 0x1))) (set nf (msb (var r8))) (set zf (is_zero (var r8))) (set sf (^^ (var nf) (var vf))))
|
|
ad "des 0x00" 0B94 0x0
|
|
ad "eicall" 1995 0x0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x2)) (set sp (- (var sp) (bv 16 0x4))) (jmp (<< (cast 32 false (append (var eind) (append (var r31) (var r30)))) (bv 32 0x1) false)))
|
|
ad "eijmp" 1994 0x0 (jmp (<< (cast 32 false (append (var eind) (append (var r31) (var r30)))) (bv 32 0x1) false))
|
|
ad "elpm r0, Z" 0690 0x0 (set r0 (loadw 0 8 (cast 32 false (append (var rampz) (append (var r31) (var r30))))))
|
|
ad "elpm r1, Z+" 1790 0x0 (seq (set r1 (loadw 0 8 (cast 32 false (append (var rampz) (append (var r31) (var r30)))))) (set RES (+ (cast 32 false (append (var rampz) (append (var r31) (var r30)))) (bv 32 0x1))) (set rampz (cast 8 false (>> (var RES) (bv 32 0x10) false))) (set r31 (cast 8 false (>> (var RES) (bv 32 0x8) false))) (set r30 (cast 8 false (var RES))))
|
|
ad "elpm r16, Z+" 0791 0x0 (seq (set r16 (loadw 0 8 (cast 32 false (append (var rampz) (append (var r31) (var r30)))))) (set RES (+ (cast 32 false (append (var rampz) (append (var r31) (var r30)))) (bv 32 0x1))) (set rampz (cast 8 false (>> (var RES) (bv 32 0x10) false))) (set r31 (cast 8 false (>> (var RES) (bv 32 0x8) false))) (set r30 (cast 8 false (var RES))))
|
|
ad "elpm" D895 0x0
|
|
ad "eor r0, r1" 0124 0x0 (seq (set r0 (^ (var r0) (var r1))) (set vf false) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))))
|
|
ad "eor r24, r25" 8927 0x0 (seq (set r24 (^ (var r24) (var r25))) (set vf false) (set nf (msb (var r24))) (set zf (is_zero (var r24))) (set sf (^^ (var nf) (var vf))))
|
|
ad "fmul r16, r16" 0803 0x0 (seq (set IND (* (cast 16 false (var r16)) (cast 16 false (var r16)))) (set RES (<< (ite (! (ule (var IND) (bv 16 0x7fff))) (- (var IND) (bv 16 0x8000)) (var IND)) (bv 8 0x1) false)) (set r1 (cast 8 false (>> (var RES) (bv 32 0x8) false))) (set r0 (cast 8 false (var RES))) (set zf (is_zero (var RES))) (set cf (msb (var RES))))
|
|
ad "fmuls r16, r16" 8003 0x0 (seq (set IND (* (cast 16 false (ite (! (ule (var r16) (bv 8 0x7f))) (- (bv 8 0x0) (var r16)) (var r16))) (cast 16 false (ite (! (ule (var r16) (bv 8 0x7f))) (- (bv 8 0x0) (var r16)) (var r16))))) (set RES (<< (ite (! (ule (var IND) (bv 16 0x3fff))) (- (var IND) (bv 16 0x4000)) (var IND)) (bv 8 0x1) false)) (set r1 (cast 8 false (>> (ite (^^ (msb (var r16)) (msb (var r16))) (- (bv 16 0x0) (var RES)) (var RES)) (bv 32 0x8) false))) (set r0 (cast 8 false (ite (^^ (msb (var r16)) (msb (var r16))) (- (bv 16 0x0) (var RES)) (var RES)))) (set zf (&& (is_zero (var r0)) (is_zero (var r1)))) (set cf (msb (var r1))))
|
|
ad "fmulsu r16, r16" 8803 0x0 (seq (set IND (* (ite (! (ule (cast 16 false (var r16)) (bv 16 0x7f))) (- (cast 16 false (var r16)) (bv 16 0x80)) (cast 16 false (var r16))) (cast 16 false (var r16)))) (set RES (<< (ite (! (ule (var IND) (bv 16 0x3fff))) (- (var IND) (bv 16 0x4000)) (var IND)) (bv 8 0x1) false)) (set r1 (cast 8 false (>> (ite (msb (var r16)) (- (bv 16 0x0) (var RES)) (var RES)) (bv 32 0x8) false))) (set r0 (cast 8 false (ite (msb (var r16)) (- (bv 16 0x0) (var RES)) (var RES)))) (set zf (&& (is_zero (var r0)) (is_zero (var r1)))) (set cf (msb (var r1))))
|
|
ad "icall" 0995 0x0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x2)) (set sp (- (var sp) (bv 16 0x4))) (jmp (<< (cast 32 false (append (var r31) (var r30))) (bv 32 0x1) false)))
|
|
ad "ijmp" 0994 0x0 (jmp (<< (cast 32 false (append (var r31) (var r30))) (bv 32 0x1) false))
|
|
ad "in r0, 0x00" 00B0 0x0 (set r0 (var r0))
|
|
ad "in r16, 0x16" 06b3 0x0 (set r16 (var r22))
|
|
ad "in r28, 0x3d" cdb7 0x0 (set r28 (loadw 0 8 (bv 32 0x3d)))
|
|
ad "inc r0" 0394 0x0 (seq (set vf (== (var r0) (bv 8 0x7f))) (set r0 (+ (var r0) (bv 8 0x1))) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))))
|
|
ad "inc r14" e394 0x0 (seq (set vf (== (var r14) (bv 8 0x7f))) (set r14 (+ (var r14) (bv 8 0x1))) (set nf (msb (var r14))) (set zf (is_zero (var r14))) (set sf (^^ (var nf) (var vf))))
|
|
ad "jmp 0x0" 0C940000 0x0 (jmp (bv 32 0x0))
|
|
ad "jmp 0x20246" 0d942301 0x0 (jmp (bv 32 0x20246))
|
|
ad "jmp 0x246" 0c942301 0x0 (jmp (bv 32 0x246))
|
|
ad "jmp 0x2c0246" bc942301 0x0 (jmp (bv 32 0x2c0246))
|
|
ad "jmp 0x400246" 0c952301 0x0 (jmp (bv 32 0x400246))
|
|
ad "lac Z, r0" 0692 0x0 (seq (set RES (- (bv 8 0xff) (var r0))) (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (storew 0 (cast 32 false (append (var r31) (var r30))) (var RES)))
|
|
ad "las Z, r0" 0592 0x0 (seq (set RES (var r0)) (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (storew 0 (cast 32 false (append (var r31) (var r30))) (var RES)))
|
|
ad "lat Z, r0" 0792 0x0 (seq (set RES (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (storew 0 (cast 32 false (append (var r31) (var r30))) (^ (var RES) (var r0))) (set r0 (var RES)))
|
|
ad "ld r0, -X" 0E90 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r27) (var r26))))) (set IND (append (var r27) (var r26))) (set r27 (cast 8 false (>> (- (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r26 (cast 8 false (- (var IND) (bv 16 0x1)))))
|
|
ad "ld r0, -Y" 0A90 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r29) (var r28))))) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (- (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r28 (cast 8 false (- (var IND) (bv 16 0x1)))))
|
|
ad "ld r0, -Z" 0290 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (- (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (- (var IND) (bv 16 0x1)))))
|
|
ad "ld r0, X" 0C90 0x0 (set r0 (loadw 0 8 (cast 32 false (append (var r27) (var r26)))))
|
|
ad "ld r0, X+" 0D90 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r27) (var r26))))) (set IND (append (var r27) (var r26))) (set r27 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r26 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "ld r0, Y" 0880 0x0 (set r0 (loadw 0 8 (cast 32 false (append (var r29) (var r28)))))
|
|
ad "ld r0, Y+" 0990 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r29) (var r28))))) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r28 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "ld r0, Z" 0080 0x0 (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30)))))
|
|
ad "ld r0, Z+" 0190 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "ld r24, Z" 8081 0x0 (set r24 (loadw 0 8 (cast 32 false (append (var r31) (var r30)))))
|
|
ad "ldd r0, Y+63" 0FAC 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r29) (var r28))))) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (+ (var IND) (bv 16 0x3f)) (bv 32 0x8) false))) (set r28 (cast 8 false (+ (var IND) (bv 16 0x3f)))))
|
|
ad "ldd r0, Y+7" 0F80 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r29) (var r28))))) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (+ (var IND) (bv 16 0x7)) (bv 32 0x8) false))) (set r28 (cast 8 false (+ (var IND) (bv 16 0x7)))))
|
|
ad "ldd r0, Z+48" 00A8 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x30)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x30)))))
|
|
ad "ldd r0, Z+63" 07AC 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x3f)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x3f)))))
|
|
ad "ldd r0, Z+7" 0780 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x7)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x7)))))
|
|
ad "ldd r9, Z+1" 9180 0x0 (seq (set r9 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "ldi r16, 0x00" 00E0 0x0 (set r16 (bv 8 0x0))
|
|
ad "ldi r25, 0x07" 97e0 0x0 (set r25 (bv 8 0x7))
|
|
ad "lds r0, 0x00" 00900000 0x0 (set r0 (loadw 0 8 (bv 32 0x0)))
|
|
ad "lds r24, 0x102" 80910201 0x0 (set r24 (loadw 0 8 (bv 32 0x102)))
|
|
ad "lpm r0, Z" 0490 0x0 (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30)))))
|
|
ad "lpm r0, Z+" 0590 0x0 (seq (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "lpm" C895 0x0 (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30)))))
|
|
ad "lsl r24" 880f 0x0 (seq (set hf (! (is_zero (& (var r24) (bv 8 0x8))))) (set cf (msb (var r24))) (set r24 (+ (var r24) (var r24))) (set nf (msb (var r24))) (set zf (is_zero (var r24))) (set sf (^^ (var nf) (var vf))) (set vf (^^ (var nf) (var cf))))
|
|
ad "lsr r0" 0694 0x0 (seq (set cf (lsb (var r0))) (set nf false) (set r0 (>> (var r0) (bv 32 0x1) false)) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))) (set vf (^^ (var nf) (var cf))))
|
|
ad "mov r0, r0" 002C 0x0 (set r0 (var r0))
|
|
ad "mov r0, r31" 0f2e 0x0 (set r0 (var r31))
|
|
ad "movw r0, r0" 0001 0x0 (seq (set IND (append (var r1) (var r0))) (set r1 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r0 (cast 8 false (var IND))))
|
|
ad "movw r22, r18" b901 0x0 (seq (set IND (append (var r19) (var r18))) (set r23 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r22 (cast 8 false (var IND))))
|
|
ad "mul r0, r0" 009C 0x0 (seq (set RES (* (cast 16 false (var r0)) (cast 16 false (var r0)))) (set r1 (cast 8 false (>> (var RES) (bv 32 0x8) false))) (set r0 (cast 8 false (var RES))) (set zf (is_zero (var RES))) (set cf (msb (var RES))))
|
|
ad "muls r16, r16" 0002 0x0 (seq (set RES (* (cast 16 (msb (var r16)) (var r16)) (cast 16 (msb (var r16)) (var r16)))) (set r1 (cast 8 false (>> (var RES) (bv 32 0x8) false))) (set r0 (cast 8 false (var RES))) (set zf (is_zero (var RES))) (set cf (msb (var RES))))
|
|
ad "mulsu r16, r16" 0003 0x0 (seq (set RES (* (cast 16 (msb (var r16)) (var r16)) (cast 16 false (var r16)))) (set r1 (cast 8 false (>> (var RES) (bv 32 0x8) false))) (set r0 (cast 8 false (var RES))) (set zf (is_zero (var RES))) (set cf (msb (var RES))))
|
|
ad "muls r16, r17" 0102 0x0 (seq (set RES (* (cast 16 (msb (var r16)) (var r16)) (cast 16 (msb (var r17)) (var r17)))) (set r1 (cast 8 false (>> (var RES) (bv 32 0x8) false))) (set r0 (cast 8 false (var RES))) (set zf (is_zero (var RES))) (set cf (msb (var RES))))
|
|
ad "neg r0" 0194 0x0 (seq (set IND (var r0)) (set r0 (ite (== (var r0) (bv 8 0x80)) (var r0) (- (bv 8 0x0) (var r0)))) (set hf (! (is_zero (& (| (var r0) (var IND)) (bv 8 0x8))))) (set vf (== (var r0) (bv 8 0x80))) (set nf (msb (var r0))) (set cf (! (is_zero (var r0)))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))))
|
|
ad "nop" 0000 0x0 nop
|
|
ad "or r0, r0" 0028 0x0 (seq (set r0 (| (var r0) (var r0))) (set vf false) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))))
|
|
ad "ori r16, 0x00" 0060 0x0 (seq (set r16 (| (var r16) (bv 8 0x0))) (set vf false) (set nf (msb (var r16))) (set zf (is_zero (var r16))) (set sf (^^ (var nf) (var vf))))
|
|
ad "ori r24, 0x01" 8160 0x0 (seq (set r24 (| (var r24) (bv 8 0x1))) (set vf false) (set nf (msb (var r24))) (set zf (is_zero (var r24))) (set sf (^^ (var nf) (var vf))))
|
|
ad "out 0x00, r0" 00B8 0x0 (set r0 (var r0))
|
|
ad "out 0x3e, r25" 9ebf 0x0 (storew 0 (bv 32 0x3e) (var r25))
|
|
ad "pop r0" 0F90 0x0 (seq (set sp (+ (var sp) (bv 16 0x1))) (set r0 (loadw 0 8 (cast 32 false (var sp)))))
|
|
ad "pop r28" cf91 0x0 (seq (set sp (+ (var sp) (bv 16 0x1))) (set r28 (loadw 0 8 (cast 32 false (var sp)))))
|
|
ad "push r0" 0F92 0x0 (seq (storew 0 (cast 32 false (var sp)) (var r0)) (set sp (- (var sp) (bv 16 0x1))))
|
|
ad "push r29" df93 0x0 (seq (storew 0 (cast 32 false (var sp)) (var r29)) (set sp (- (var sp) (bv 16 0x1))))
|
|
ad "rcall 0x12" 08D0 0x0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x2)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x12)))
|
|
ad "rcall 0x14" 09D0 0x0 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x2)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x14)))
|
|
ad "rcall 0x12" 00D0 0x10 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x12)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x12)))
|
|
ad "rcall 0x14" 01D0 0x10 (seq (storew 0 (- (cast 32 false (var sp)) (bv 32 0x3)) (bv 32 0x12)) (set sp (- (var sp) (bv 16 0x4))) (jmp (bv 32 0x14)))
|
|
ad "ret" 0895 0x0 (seq (set sp (+ (var sp) (bv 16 0x4))) (jmp (loadw 0 32 (- (cast 32 false (var sp)) (bv 32 0x3)))))
|
|
ad "reti" 1895 0x0 (seq (set sp (+ (var sp) (bv 16 0x4))) (jmp (loadw 0 32 (- (cast 32 false (var sp)) (bv 32 0x3)))))
|
|
ad "rjmp 0x12" 08C0 0x0 (jmp (bv 32 0x12))
|
|
ad "rjmp 0x14" 09c0 0x0 (jmp (bv 32 0x14))
|
|
ad "rjmp 0x12" 00C0 0x10 (jmp (bv 32 0x12))
|
|
ad "rjmp 0x14" 01c0 0x10 (jmp (bv 32 0x14))
|
|
ad "rjmp 0x375a6" 1fc0 0x37566 (jmp (bv 32 0x375a6))
|
|
ad "rjmp 0xfffffffffffff002" 00c8 0x0 (jmp (bv 32 0xfffff002))
|
|
ad "rjmp 0xfffffffffffff004" 01c8 0x0 (jmp (bv 32 0xfffff004))
|
|
ad "rjmp 0xfffffffffffff0fe" 7ec8 0x0 (jmp (bv 32 0xfffff0fe))
|
|
ad "rjmp 0xfffffffffffff100" 7fc8 0x0 (jmp (bv 32 0xfffff100))
|
|
ad "rjmp 0xfffffffffffff102" 80c8 0x0 (jmp (bv 32 0xfffff102))
|
|
ad "rjmp 0xfffffffffffff104" 81c8 0x0 (jmp (bv 32 0xfffff104))
|
|
ad "rol r25" 991f 0x0 (seq (set RES (var cf)) (set hf (! (is_zero (& (var r25) (bv 8 0x8))))) (set cf (msb (var r25))) (set r25 (<< (var r25) (bv 32 0x1) (var RES))) (set nf (msb (var r25))) (set zf (is_zero (var r25))) (set sf (^^ (var nf) (var vf))) (set vf (^^ (var nf) (var cf))))
|
|
ad "ror r0" 0794 0x0 (seq (set RES (var cf)) (set cf (lsb (var r0))) (set r0 (>> (var r0) (bv 32 0x1) (var RES))) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))) (set vf (^^ (var nf) (var cf))))
|
|
ad "sbc r0, r0" 0008 0x0 (seq (set RES (- (- (var r0) (var r0)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set zf (&& (is_zero (var RES)) (var zf))) (set hf (! (is_zero (& (| (| (& (~ (var r0)) (var r0)) (& (var r0) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r0) (~ (var r0))) (~ (var RES))) (& (& (~ (var r0)) (var r0)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r0)) (var r0)) (& (var r0) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r0 (var RES)))
|
|
ad "sbc r19, r25" 390b 0x0 (seq (set RES (- (- (var r19) (var r25)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set zf (&& (is_zero (var RES)) (var zf))) (set hf (! (is_zero (& (| (| (& (~ (var r19)) (var r25)) (& (var r25) (var RES))) (& (var RES) (~ (var r19)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r19) (~ (var r25))) (~ (var RES))) (& (& (~ (var r19)) (var r25)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r19)) (var r25)) (& (var r25) (var RES))) (& (var RES) (~ (var r19)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r19 (var RES)))
|
|
ad "sbci r16, 0x00" 0040 0x0 (seq (set RES (- (- (var r16) (bv 8 0x0)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set zf (&& (is_zero (var RES)) (var zf))) (set hf (! (is_zero (& (| (| (& (~ (var r16)) (bv 8 0x0)) (& (bv 8 0x0) (var RES))) (& (var RES) (~ (var r16)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r16) (~ (bv 8 0x0))) (~ (var RES))) (& (& (~ (var r16)) (bv 8 0x0)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r16)) (bv 8 0x0)) (& (bv 8 0x0) (var RES))) (& (var RES) (~ (var r16)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r16 (var RES)))
|
|
ad "sbci r19, 0xff" 3f4f 0x0 (seq (set RES (- (- (var r19) (bv 8 0xff)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set zf (&& (is_zero (var RES)) (var zf))) (set hf (! (is_zero (& (| (| (& (~ (var r19)) (bv 8 0xff)) (& (bv 8 0xff) (var RES))) (& (var RES) (~ (var r19)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r19) (~ (bv 8 0xff))) (~ (var RES))) (& (& (~ (var r19)) (bv 8 0xff)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r19)) (bv 8 0xff)) (& (bv 8 0xff) (var RES))) (& (var RES) (~ (var r19)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r19 (var RES)))
|
|
ad "sbi 0x00, 0" 009A 0x0 (set r0 (| (bv 8 0x1) (var r0)))
|
|
ad "sbic 0x00, 0" 0099 0x0 (branch (is_zero (& (bv 8 0xfe) (var r0))) (jmp (bv 32 0x0)) nop)
|
|
ad "sbis 0x00, 0" 009B 0x0 (branch (is_zero (& (bv 8 0xfe) (var r0))) nop (jmp (bv 32 0x0)))
|
|
ad "sbiw r25:r24, 0x00" 0097 0x0 (seq (set IND (- (append (var r25) (var r24)) (bv 16 0x0))) (set r25 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r24 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (msb (var r25)) (! (msb (var IND))))) (set nf (msb (var IND))) (set cf (&& (msb (var IND)) (! (msb (var r25))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "sbiw r25:r24, 0x01" 0197 0x0 (seq (set IND (- (append (var r25) (var r24)) (bv 16 0x1))) (set r25 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r24 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (msb (var r25)) (! (msb (var IND))))) (set nf (msb (var IND))) (set cf (&& (msb (var IND)) (! (msb (var r25))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "sbiw r27:r26, 0x01" 1197 0x0 (seq (set IND (- (append (var r27) (var r26)) (bv 16 0x1))) (set r27 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r26 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (msb (var r27)) (! (msb (var IND))))) (set nf (msb (var IND))) (set cf (&& (msb (var IND)) (! (msb (var r27))))) (set sf (^^ (var nf) (var vf))))
|
|
ad "sbiw r27:r26, 0x3f" df97 0x0 (seq (set IND (- (append (var r27) (var r26)) (bv 16 0x3f))) (set r27 (cast 8 false (>> (var IND) (bv 32 0x8) false))) (set r26 (cast 8 false (var IND))) (set zf (is_zero (var IND))) (set vf (&& (msb (var r27)) (! (msb (var IND))))) (set nf (msb (var IND))) (set cf (&& (msb (var IND)) (! (msb (var r27))))) (set sf (^^ (var nf) (var vf))))
|
|
a "sbiw r24, 0x00" 0097
|
|
a "sbiw r24, 0x01" 0197
|
|
a "sbiw r26, 0x01" 1197
|
|
a "sbiw r26, 63" df97
|
|
ad "sbrc r0, 0" 00FC 0x0 (branch (is_zero (& (bv 8 0xfe) (var r0))) (jmp (bv 32 0x0)) nop)
|
|
ad "sbrs r0, 0" 00FE 0x0 (branch (is_zero (& (bv 8 0xfe) (var r0))) nop (jmp (bv 32 0x0)))
|
|
ad "sec" 0894 0x0 (set cf true)
|
|
ad "seh" 5894 0x0 (set hf true)
|
|
ad "sei" 7894 0x0 (set if true)
|
|
ad "sei" 7894 0x0 (set if true)
|
|
ad "sen" 2894 0x0 (set nf true)
|
|
ad "ser r16" 0FEF 0x0 (set r16 (bv 8 0xff))
|
|
ad "ser r24" 8fef 0x0 (set r24 (bv 8 0xff))
|
|
ad "ses" 4894 0x0 (set sf true)
|
|
ad "set" 6894 0x0 (set tf true)
|
|
ad "sev" 3894 0x0 (set vf true)
|
|
ad "sez" 1894 0x0 (set zf true)
|
|
ad "sleep" 8895 0x0 nop
|
|
ad "spm Z+" F895 0x0
|
|
ad "spm" E895 0x0
|
|
ad "st -X, r0" 0E92 0x0 (seq (storew 0 (cast 32 false (append (var r27) (var r26))) (var r0)) (set IND (append (var r27) (var r26))) (set r27 (cast 8 false (>> (- (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r26 (cast 8 false (- (var IND) (bv 16 0x1)))))
|
|
ad "st -Y, r0" 0A92 0x0 (seq (storew 0 (cast 32 false (append (var r29) (var r28))) (var r0)) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (- (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r28 (cast 8 false (- (var IND) (bv 16 0x1)))))
|
|
ad "st -Z, r0" 0292 0x0 (seq (storew 0 (cast 32 false (append (var r31) (var r30))) (var r0)) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (- (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (- (var IND) (bv 16 0x1)))))
|
|
ad "st X+1, r0" 0D92 0x0 (seq (storew 0 (cast 32 false (append (var r27) (var r26))) (var r0)) (set IND (append (var r27) (var r26))) (set r27 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r26 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "st X, r0" 0C92 0x0 (storew 0 (cast 32 false (append (var r27) (var r26))) (var r0))
|
|
ad "st Y+1, r0" 0992 0x0 (seq (storew 0 (cast 32 false (append (var r29) (var r28))) (var r0)) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r28 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "st Y, r0" 0882 0x0 (storew 0 (cast 32 false (append (var r29) (var r28))) (var r0))
|
|
ad "st Y, r15" F882 0x0 (storew 0 (cast 32 false (append (var r29) (var r28))) (var r15))
|
|
ad "st Z+1, r0" 0192 0x0 (seq (storew 0 (cast 32 false (append (var r31) (var r30))) (var r0)) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "st Z, r0" 0082 0x0 (storew 0 (cast 32 false (append (var r31) (var r30))) (var r0))
|
|
ad "st Z, r1" 1082 0x0 (storew 0 (cast 32 false (append (var r31) (var r30))) (var r1))
|
|
ad "std Y+1, r0" 0982 0x0 (seq (storew 0 (cast 32 false (append (var r29) (var r28))) (var r0)) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r28 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "std Y+63, r0" 0FAE 0x0 (seq (storew 0 (cast 32 false (append (var r29) (var r28))) (var r0)) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (+ (var IND) (bv 16 0x3f)) (bv 32 0x8) false))) (set r28 (cast 8 false (+ (var IND) (bv 16 0x3f)))))
|
|
ad "std Y+7, r0" 0F82 0x0 (seq (storew 0 (cast 32 false (append (var r29) (var r28))) (var r0)) (set IND (append (var r29) (var r28))) (set r29 (cast 8 false (>> (+ (var IND) (bv 16 0x7)) (bv 32 0x8) false))) (set r28 (cast 8 false (+ (var IND) (bv 16 0x7)))))
|
|
ad "std Z+1, r0" 0182 0x0 (seq (storew 0 (cast 32 false (append (var r31) (var r30))) (var r0)) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "std Z+1, r1" 1182 0x0 (seq (storew 0 (cast 32 false (append (var r31) (var r30))) (var r1)) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x1)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x1)))))
|
|
ad "std Z+63, r0" 07AE 0x0 (seq (storew 0 (cast 32 false (append (var r31) (var r30))) (var r0)) (set IND (append (var r31) (var r30))) (set r31 (cast 8 false (>> (+ (var IND) (bv 16 0x3f)) (bv 32 0x8) false))) (set r30 (cast 8 false (+ (var IND) (bv 16 0x3f)))))
|
|
ad "sts 0x00, r0" 00920000 0x0 (storew 0 (bv 32 0x0) (var r0))
|
|
ad "sts 0x7c0, r25" 9093c007 0x0 (storew 0 (bv 32 0x7c0) (var r25))
|
|
ad "sub r0, r0" 0018 0x0 (seq (set RES (- (var r0) (var r0))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r0)) (var r0)) (& (var r0) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r0) (~ (var r0))) (~ (var RES))) (& (& (~ (var r0)) (var r0)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r0)) (var r0)) (& (var r0) (var RES))) (& (var RES) (~ (var r0)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r0 (var RES)))
|
|
ad "sub r18, r24" 281b 0x0 (seq (set RES (- (var r18) (var r24))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r18)) (var r24)) (& (var r24) (var RES))) (& (var RES) (~ (var r18)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r18) (~ (var r24))) (~ (var RES))) (& (& (~ (var r18)) (var r24)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r18)) (var r24)) (& (var r24) (var RES))) (& (var RES) (~ (var r18)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r18 (var RES)))
|
|
ad "subi r16, 0x00" 0050 0x0 (seq (set RES (- (var r16) (bv 8 0x0))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r16)) (bv 8 0x0)) (& (bv 8 0x0) (var RES))) (& (var RES) (~ (var r16)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r16) (~ (bv 8 0x0))) (~ (var RES))) (& (& (~ (var r16)) (bv 8 0x0)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r16)) (bv 8 0x0)) (& (bv 8 0x0) (var RES))) (& (var RES) (~ (var r16)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r16 (var RES)))
|
|
ad "subi r18, 0xff" 2f5f 0x0 (seq (set RES (- (var r18) (bv 8 0xff))) (set zf (is_zero (var RES))) (set hf (! (is_zero (& (| (| (& (~ (var r18)) (bv 8 0xff)) (& (bv 8 0xff) (var RES))) (& (var RES) (~ (var r18)))) (bv 8 0x8))))) (set vf (msb (| (& (& (var r18) (~ (bv 8 0xff))) (~ (var RES))) (& (& (~ (var r18)) (bv 8 0xff)) (var RES))))) (set nf (msb (var RES))) (set cf (! (is_zero (& (| (| (& (~ (var r18)) (bv 8 0xff)) (& (bv 8 0xff) (var RES))) (& (var RES) (~ (var r18)))) (bv 8 0x80))))) (set sf (^^ (var nf) (var vf))) (set r18 (var RES)))
|
|
ad "swap r0" 0294 0x0 (seq (set RES (var r0)) (set r0 (| (<< (var r0) (bv 32 0x4) false) (>> (var RES) (bv 32 0x4) false))))
|
|
ad "tst r0" 0020 0x0 (seq (set r0 (& (var r0) (var r0))) (set vf false) (set nf (msb (var r0))) (set zf (is_zero (var r0))) (set sf (^^ (var nf) (var vf))))
|
|
ad "tst r24" 8823 0x0 (seq (set r24 (& (var r24) (var r24))) (set vf false) (set nf (msb (var r24))) (set zf (is_zero (var r24))) (set sf (^^ (var nf) (var vf))))
|
|
ad "wdr" A895 0x0 nop
|
|
ad "xch Z, r0" 0492 0x0 (seq (set RES (var r0)) (set r0 (loadw 0 8 (cast 32 false (append (var r31) (var r30))))) (storew 0 (cast 32 false (append (var r31) (var r30))) (var RES)))
|
|
d "invalid" 0e 0x0
|
|
d "invalid" ffff 2
|