Skip to content

Commit

Permalink
Add tests for ADC instructions
Browse files Browse the repository at this point in the history 
  * Properly cast `LOADW` and `STOREW` values
  • Loading branch information
@DMaroo
DMaroo committed Aug 25, 2022
1 parent 1bbeb10 commit 70bfd16
Show file tree
Hide file tree
Showing 2 changed files with 38 additions and 28 deletions.
56 changes: 33 additions & 23 deletions librz/analysis/arch/x86/x86_il.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -525,24 +525,36 @@ static RzILOpEffect *x86_il_set_reg_bits(X86Reg reg, RzILOpPure *val, int bits)

#define x86_il_set_reg(reg, val) x86_il_set_reg_bits(reg, val, analysis->bits)

static RzILOpPure *x86_il_get_memaddr_bits(X86Mem mem, int bits) {
static RzILOpPure *x86_il_get_memaddr_bits(X86Mem mem, int analysis_bits, ut8 size) {
RzILOpPure *offset = NULL;
if (mem.base != X86_REG_INVALID) {
if (!offset) {
offset = x86_il_get_reg_bits(mem.base, bits);
offset = x86_il_get_reg_bits(mem.base, analysis_bits);
if (analysis_bits != size) {
/* Need to cast the value to the correct size */
offset = UNSIGNED(size, offset);
}
}
}
if (mem.index != X86_REG_INVALID) {
if (!offset) {
offset = MUL(x86_il_get_reg_bits(mem.index, bits), U64(mem.scale));
RzILOpPure *reg = x86_il_get_reg_bits(mem.index, analysis_bits);
if (analysis_bits != size) {
reg = UNSIGNED(size, reg);
}
offset = MUL(reg, UN(size, mem.scale));
} else {
offset = ADD(offset, MUL(x86_il_get_reg_bits(mem.index, bits), U64(mem.scale)));
RzILOpPure *reg = x86_il_get_reg_bits(mem.index, analysis_bits);
if (analysis_bits != size) {
reg = UNSIGNED(size, reg);
}
offset = ADD(offset, MUL(reg, UN(size, mem.scale)));
}
}
if (!offset) {
offset = U64(mem.disp);
offset = UN(size, mem.disp);
} else {
offset = ADD(offset, U64(mem.disp));
offset = ADD(offset, UN(size, mem.disp));
}

RzILOpPure *ret = NULL;
Expand All @@ -556,10 +568,8 @@ static RzILOpPure *x86_il_get_memaddr_bits(X86Mem mem, int bits) {
return ret;
}

#define x86_il_get_memaddr(mem) x86_il_get_memaddr_bits(mem, analysis->bits)

static RzILOpEffect *x86_il_set_mem_bits(X86Mem mem, RzILOpPure *val, int bits) {
return STOREW(x86_il_get_memaddr_bits(mem, bits), val);
static RzILOpEffect *x86_il_set_mem_bits(X86Mem mem, RzILOpPure *val, int analysis_bits, ut8 size) {
return STOREW(x86_il_get_memaddr_bits(mem, analysis_bits, size), val);
}

#define x86_il_set_mem(mem, val) x86_il_set_mem_bits(mem, val, analysis->bits)
Expand All @@ -577,7 +587,7 @@ static RzILOpPure *x86_il_get_operand_bits(X86Op op, int analysis_bits) {
ret = SN(op.size * BITS_PER_BYTE, op.imm);
break;
case X86_OP_MEM:
ret = LOADW(BITS_PER_BYTE * op.size, x86_il_get_memaddr_bits(op.mem, op.size * BITS_PER_BYTE));
ret = LOADW(BITS_PER_BYTE * op.size, x86_il_get_memaddr_bits(op.mem, analysis_bits, op.size * BITS_PER_BYTE));
}
return ret;
}
Expand All @@ -591,7 +601,7 @@ static RzILOpEffect *x86_il_set_operand_bits(X86Op op, RzILOpPure *val, int bits
ret = x86_il_set_reg_bits(op.reg, val, bits);
break;
case X86_OP_MEM:
ret = x86_il_set_mem_bits(op.mem, val, bits);
ret = x86_il_set_mem_bits(op.mem, val, bits, op.size * BITS_PER_BYTE);
break;
case X86_OP_IMM:
RZ_LOG_ERROR("x86: RzIL: Cannot set an immediate operand\n");
Expand All @@ -605,7 +615,7 @@ static RzILOpEffect *x86_il_set_operand_bits(X86Op op, RzILOpPure *val, int bits

#define x86_il_set_operand(op, val) x86_il_set_operand_bits(op, val, analysis->bits)

static inline RzILOpBool *x86_il_is_add_carry(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
static RzILOpBool *x86_il_is_add_carry(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
// res = x + y
RzILOpBool *xmsb = MSB(x);
RzILOpBool *ymsb = MSB(y);
Expand All @@ -618,16 +628,16 @@ static inline RzILOpBool *x86_il_is_add_carry(RZ_OWN RzILOpPure *res, RZ_OWN RzI
// !res & y
RzILOpBool *ry = AND(nres, DUP(ymsb));
// x & !res
RzILOpBool *xr = AND(DUP(xmsb), nres);
RzILOpBool *xr = AND(DUP(xmsb), DUP(nres));

// bit = xy | ry | xr
RzILOpBool * or = OR(xy, ry);
or = OR(or, xr);

return NON_ZERO(or);
return or ;
}

static inline RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
static RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
// res = x - y
RzILOpBool *xmsb = MSB(x);
RzILOpBool *ymsb = MSB(y);
Expand All @@ -640,16 +650,16 @@ static inline RzILOpBool *x86_il_is_sub_borrow(RZ_OWN RzILOpPure *res, RZ_OWN Rz
// y & res
RzILOpBool *rny = AND(DUP(ymsb), resmsb);
// res & !x
RzILOpBool *rnx = AND(DUP(resmsb), nx);
RzILOpBool *rnx = AND(DUP(resmsb), DUP(nx));

// bit = nxy | rny | rnx
RzILOpBool * or = OR(nxy, rny);
or = OR(or, rnx);

return NON_ZERO(or);
return or ;
}

static inline RzILOpBool *x86_il_is_add_overflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
static RzILOpBool *x86_il_is_add_overflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
// res = x + y
RzILOpBool *xmsb = MSB(x);
RzILOpBool *ymsb = MSB(y);
Expand All @@ -662,10 +672,10 @@ static inline RzILOpBool *x86_il_is_add_overflow(RZ_OWN RzILOpPure *res, RZ_OWN
// or = nrxy | rnxny
RzILOpBool * or = OR(nrxy, rnxny);

return NON_ZERO(or);
return or ;
}

static inline RzILOpBool *x86_il_is_sub_underflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
static RzILOpBool *x86_il_is_sub_underflow(RZ_OWN RzILOpPure *res, RZ_OWN RzILOpPure *x, RZ_OWN RzILOpPure *y) {
// res = x - y
RzILOpBool *xmsb = MSB(x);
RzILOpBool *ymsb = MSB(y);
Expand All @@ -678,7 +688,7 @@ static inline RzILOpBool *x86_il_is_sub_underflow(RZ_OWN RzILOpPure *res, RZ_OWN
// or = nrxny | rnxy
RzILOpBool * or = OR(nrxny, rnxy);

return NON_ZERO(or);
return or ;
}

static RzILOpBitVector *x86_bool_to_bv(RzILOpBool *b, unsigned int bits) {
Expand Down Expand Up @@ -900,7 +910,7 @@ static RzILOpEffect *x86_il_adc(const X86ILIns *ins, ut64 pc, RzAnalysis *analys
RzILOpEffect *op2 = SETL("op2", x86_il_get_operand(ins->structure->operands[1]));
RzILOpPure *cf = VARG(x86_eflags_registers[X86_EFLAGS_CF]);

RzILOpEffect *sum = SETL("sum", ADD(ADD(VARL("op1"), VARL("op2")), cf));
RzILOpEffect *sum = SETL("sum", ADD(ADD(VARL("op1"), VARL("op2")), x86_bool_to_bv(cf, ins->structure->operands[0].size * BITS_PER_BYTE)));
RzILOpEffect *set_dest = x86_il_set_operand(ins->structure->operands[0], VARL("sum"));
RzILOpEffect *set_res_flags = x86_il_set_result_flags(VARL("sum"));
RzILOpEffect *set_arith_flags = x86_il_set_arithmetic_flags(VARL("sum"), VARL("op1"), VARL("op2"), true);
Expand Down
10 changes: 5 additions & 5 deletions test/db/asm/x86_32
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@ ad "aad 0x69" d569 0x0 (seq (set temp_al (cast 8 false (var eax))) (set temp_ah
ad "aam" d40a 0x0 (seq (set temp_al (cast 8 false (var eax))) (set eax (| (& (var eax) (~ (bv 32 0xff00))) (<< (cast 32 false (div (var temp_al) (bv 8 0xa))) (bv 8 0x8) false))) (set adjusted (smod (var temp_al) (bv 8 0xa))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var adjusted)))) (set _result (var adjusted)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (is_zero (var _val)) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (smod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
ad "aam 0x42" d442 0x0 (seq (set temp_al (cast 8 false (var eax))) (set eax (| (& (var eax) (~ (bv 32 0xff00))) (<< (cast 32 false (div (var temp_al) (bv 8 0x42))) (bv 8 0x8) false))) (set adjusted (smod (var temp_al) (bv 8 0x42))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var adjusted)))) (set _result (var adjusted)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (is_zero (var _val)) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (smod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
ad "aas" 3f 0x0 (seq (branch (|| (! (ule (& (cast 8 false (var eax)) (bv 8 0xf)) (bv 8 0x9))) (var af)) (seq (set eax (| (& (var eax) (~ (bv 32 0xffff))) (cast 32 false (- (cast 16 false (var eax)) (bv 16 0x6))))) (set eax (| (& (var eax) (~ (bv 32 0xff00))) (<< (cast 32 false (- (cast 8 false (>> (var eax) (bv 8 0x8) false)) (bv 8 0x1))) (bv 8 0x8) false))) (set af true) (set cf true)) (seq (set af false) (set cf false))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (& (cast 8 false (var eax)) (bv 8 0xf))))))
d "adc al, 0" 1400
d "adc al, byte [eax]" 1200
d "adc byte [eax], al" 1000
d "adc dword [eax], eax" 1100
d "adc eax, dword [eax]" 1300
d "adc al, 0" 1400 0x0 (seq (set op1 (cast 8 false (var eax))) (set op2 (bv 8 0x0)) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var sum)))) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (is_zero (var _val)) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (smod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))))
d "adc al, byte [eax]" 1200 0x0 (seq (set op1 (cast 8 false (var eax))) (set op2 (loadw 0 8 (+ (cast 8 false (var eax)) (bv 8 0x0)))) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var sum)))) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (is_zero (var _val)) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (smod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))))
d "adc byte [eax], al" 1000 0x0 (seq (set op1 (loadw 0 8 (+ (cast 8 false (var eax)) (bv 8 0x0)))) (set op2 (cast 8 false (var eax))) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (storew 0 (+ (cast 8 false (var eax)) (bv 8 0x0)) (var sum)) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (is_zero (var _val)) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (smod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))))
d "adc dword [eax], eax" 1100 0x0 (seq (set op1 (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set op2 (var eax)) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))) (storew 0 (+ (var eax) (bv 32 0x0)) (var sum)) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (is_zero (var _val)) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (smod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))))
d "adc eax, dword [eax]" 1300 0x0 (seq (set op1 (var eax)) (set op2 (loadw 0 32 (+ (var eax) (bv 32 0x0)))) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))) (set eax (var sum)) (set _result (var sum)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (is_zero (var _val)) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (smod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var sum)) (set _x (var op1)) (set _y (var op2)) (set cf (|| (|| (&& (msb (var _x)) (msb (var _y))) (&& (! (msb (var _result))) (msb (var _y)))) (&& (msb (var _x)) (! (msb (var _result)))))) (set of (|| (&& (&& (! (msb (var _result))) (msb (var _x))) (msb (var _y))) (&& (&& (msb (var _result)) (! (msb (var _x)))) (! (msb (var _y)))))) (set af (|| (|| (&& (msb (cast 4 false (var _x))) (msb (cast 4 false (var _y)))) (&& (! (msb (cast 4 false (var _result)))) (msb (cast 4 false (var _y))))) (&& (msb (cast 4 false (var _x))) (! (msb (cast 4 false (var _result))))))))
d "add al, 0" 0400
d "add al, byte [eax]" 0200
d "add byte [bx + si], al" 670000
Expand Down

0 comments on commit 70bfd16

Please sign in to comment.