portugalfuturista/rizin
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

librz/arch/x86: fix ADC, AND, OR, SBB RzIL lifting (#6524)

Browse source 
* Cast operands for AND and OR instructions to the correct width
* Add missing operand casts for SBB and ADC.
* Add flawed instructions to asm tests

---------

Co-authored-by: Dhruv Maroo <dhruvmaru007@gmail.com>
This commit is contained in:
Rot127 2026-06-18 03:07:43 +00:00 committed by GitHub
parent b9d2a03be3
commit 110c812219
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 907 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
librz/arch/isa/x86/il_fp_ops.inc
View file

@ -568,6 +568,7 @@ RzILOpEffect *fcom_helper(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis, Rz
} else if (ins->structure->operand_count_visible == 1) {
op1 = x86_il_get_floating_op(0);
} else {
rz_il_op_pure_free(st0);
st0 = x86_il_get_floating_op(0);
op1 = x86_il_get_floating_op(1);
}

32
librz/arch/isa/x86/il_ops.inc
View file

@ -154,16 +154,20 @@ IL_LIFTER(aas) {
* - RM
*/
IL_LIFTER(adc) {
RzILOpEffect *op1 = SETL("op1", x86_il_get_op(0));
RzILOpEffect *op2 = SETL("op2", x86_il_get_op(1));
RzILOpEffect *set_op1 = SETL("_op1", x86_il_get_op(0));
RzILOpPure *op2 = x86_il_get_op(1);
if (ins->operands[0].size != ins->operands[1].size) {
op2 = CAST(ins->operands[0].size * BITS_PER_BYTE, IL_FALSE, op2);
}
RzILOpEffect *set_op2 = SETL("_op2", op2);
RzILOpPure *cf = VARG(EFLAGS(CF));
RzILOpEffect *sum = SETL("sum", ADD(ADD(VARL("op1"), VARL("op2")), BOOL_TO_BV(cf, ins->operands[0].size * BITS_PER_BYTE)));
RzILOpEffect *sum = SETL("sum", ADD(ADD(VARL("_op1"), VARL("_op2")), BOOL_TO_BV(cf, ins->operands[0].size * BITS_PER_BYTE)));
RzILOpEffect *set_dest = x86_il_set_op(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);
RzILOpEffect *set_arith_flags = x86_il_set_arithmetic_flags(VARL("sum"), VARL("_op1"), VARL("_op2"), true);
return SEQ6(op1, op2, sum, set_dest, set_res_flags, set_arith_flags);
return SEQ6(set_op1, set_op2, sum, set_dest, set_res_flags, set_arith_flags);
}
/**
@ -203,6 +207,10 @@ IL_LIFTER(add) {
IL_LIFTER(and) {
RzILOpPure *op1 = x86_il_get_op(0);
RzILOpPure *op2 = x86_il_get_op(1);
if (ins->operands[0].size != ins->operands[1].size) {
op2 = CAST(ins->operands[0].size * BITS_PER_BYTE, IL_FALSE, op2);
}
RzILOpEffect *and = SETL("and_", LOGAND(op1, op2));
RzILOpEffect *set_dest = x86_il_set_op(0, VARL("and_"));
@ -1501,6 +1509,10 @@ IL_LIFTER(not) {
IL_LIFTER(or) {
RzILOpPure *op1 = x86_il_get_op(0);
RzILOpPure *op2 = x86_il_get_op(1);
if (ins->operands[0].size != ins->operands[1].size) {
op2 = CAST(ins->operands[0].size * BITS_PER_BYTE, IL_FALSE, op2);
}
RzILOpEffect * or = SETL("_or", LOGOR(op1, op2));
RzILOpEffect *set_dest = x86_il_set_op(0, VARL("_or"));
@ -1985,8 +1997,12 @@ IL_LIFTER(shr) {
* Encoding: I, MI, MR, RM
*/
IL_LIFTER(sbb) {
RzILOpEffect *op1 = SETL("_op1", x86_il_get_op(0));
RzILOpEffect *op2 = SETL("_op2", x86_il_get_op(1));
RzILOpEffect *set_op1 = SETL("_op1", x86_il_get_op(0));
RzILOpPure *op2 = x86_il_get_op(1);
if (ins->operands[0].size != ins->operands[1].size) {
op2 = CAST(ins->operands[0].size * BITS_PER_BYTE, IL_FALSE, op2);
}
RzILOpEffect *set_op2 = SETL("_op2", op2);
RzILOpPure *cf = VARG(EFLAGS(CF));
RzILOpEffect *diff = SETL("_diff", SUB(SUB(VARL("_op1"), VARL("_op2")), BOOL_TO_BV(cf, ins->operands[0].size * BITS_PER_BYTE)));
@ -1994,7 +2010,7 @@ IL_LIFTER(sbb) {
RzILOpEffect *set_res_flags = x86_il_set_result_flags(VARL("_diff"));
RzILOpEffect *set_arith_flags = x86_il_set_arithmetic_flags(VARL("_diff"), VARL("_op1"), VARL("_op2"), false);
return SEQ6(op1, op2, diff, set_dest, set_res_flags, set_arith_flags);
return SEQ6(set_op1, set_op2, diff, set_dest, set_res_flags, set_arith_flags);
}
RzILOpEffect *x86_il_scas_helper(const X86ILIns *ins, ut64 pc, RzAnalysis *analysis, ut8 size) {

4
librz/il/il_graph.c
View file

@ -784,7 +784,7 @@ static void il_op_effect_graph_resolve(RzILOpEffect *op, RzGraph /*<RzGraphNodeI
*/
RZ_API RZ_OWN RzGraph /*<RzGraphNodeInfo *, NULL *>*/ *rz_il_op_pure_graph(RZ_NONNULL RzILOpPure *op, RZ_NULLABLE const char *name) {
rz_return_val_if_fail(op, NULL);
RzGraph *graph = rz_graph_new(RZ_GRAPH_IMPL_LIST, NULL, NULL, NULL);
RzGraph *graph = rz_graph_new(RZ_GRAPH_IMPL_LIST, NULL, rz_graph_free_node_info, NULL);
if (!graph) {
return NULL;
}
@ -801,7 +801,7 @@ RZ_API RZ_OWN RzGraph /*<RzGraphNodeInfo *, NULL *>*/ *rz_il_op_pure_graph(RZ_NO
*/
RZ_API RZ_OWN RzGraph /*<RzGraphNodeInfo *, NULL *>*/ *rz_il_op_effect_graph(RZ_NONNULL RzILOpEffect *op, RZ_NULLABLE const char *name) {
rz_return_val_if_fail(op, NULL);
RzGraph *graph = rz_graph_new(RZ_GRAPH_IMPL_LIST, NULL, NULL, NULL);
RzGraph *graph = rz_graph_new(RZ_GRAPH_IMPL_LIST, NULL, rz_graph_free_node_info, NULL);
if (!graph) {
return NULL;
}

10
test/db/asm/x86_32
View file

@ -5,11 +5,11 @@ d "aad 0x69" d569 0x0 (seq (set temp_al (cast 8 false (var eax))) (set temp_ah (
d "aam 0x0a" 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 (mod (var temp_al) (bv 8 0xa))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var adjusted)))) (set _result (var adjusted)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
d "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 (mod (var temp_al) (bv 8 0x42))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var adjusted)))) (set _result (var adjusted)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
d "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, 0x00" 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 pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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 (var eax))) (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 pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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 (var eax))) (set op2 (cast 8 false (var eax))) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (storew 0 (var eax) (var sum)) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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))) (set op2 (var eax)) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))) (storew 0 (var eax) (var sum)) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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))) (set sum (+ (+ (var op1) (var op2)) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))) (set eax (var sum)) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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, 0x00" 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 pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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 (var eax))) (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 pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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 (var eax))) (set _op2 (cast 8 false (var eax))) (set sum (+ (+ (var _op1) (var _op2)) (ite (var cf) (bv 8 0x1) (bv 8 0x0)))) (storew 0 (var eax) (var sum)) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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))) (set _op2 (var eax)) (set sum (+ (+ (var _op1) (var _op2)) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))) (storew 0 (var eax) (var sum)) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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))) (set sum (+ (+ (var _op1) (var _op2)) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))) (set eax (var sum)) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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, 0x00" 0400 0x0 (seq (set op1 (cast 8 false (var eax))) (set op2 (bv 8 0x0)) (set sum (+ (var op1) (var op2))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var sum)))) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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, byte [eax]" 0200 0x0 (seq (set op1 (cast 8 false (var eax))) (set op2 (loadw 0 8 (var eax))) (set sum (+ (var op1) (var op2))) (set eax (| (& (var eax) (~ (bv 32 0xff))) (cast 32 false (var sum)))) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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 byte [bx+si*1], al" 670000 0x0 (seq (set op1 (loadw 0 8 (+ (cast 32 false (cast 16 false (var ebx))) (* (cast 32 false (cast 16 false (var esi))) (bv 32 0x1))))) (set op2 (cast 8 false (var eax))) (set sum (+ (var op1) (var op2))) (storew 0 (+ (cast 32 false (cast 16 false (var ebx))) (* (cast 32 false (cast 16 false (var esi))) (bv 32 0x1))) (var sum)) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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))))))))

4
test/db/asm/x86_64
View file

@ -1140,3 +1140,7 @@ d "cvttss2si rax, xmm0" f3480f2cc0 0x0 (set rax (fcast_sint 64 rtz (float 0 (cas
d "cvttss2si eax, xmm0" f30f2cc0 0x0 (set rax (cast 64 false (fcast_sint 32 rtz (float 0 (cast 32 false (var xmm0)) ))))
d "cvtsd2ss xmm0, xmm1" f20f5ac1 0x0 (set xmm0 (| (<< (>> (var xmm0) (bv 8 0x20) false) (bv 8 0x20) false) (cast 128 false (fbits (fconvert ieee754-bin32 rne (float 1 (cast 64 false (var xmm1)) ))))))
d "cvtss2sd xmm0, xmm1" f30f5ac1 0x0 (set xmm0 (| (<< (>> (var xmm0) (bv 8 0x40) false) (bv 8 0x40) false) (cast 128 false (fbits (fconvert ieee754-bin64 rne (float 0 (cast 32 false (var xmm1)) ))))))
d "and rcx, 0xfffffffffffffff0" 4883e1f0 0x0 (seq (set and_ (& (var rcx) (bv 64 0xfffffffffffffff0))) (set rcx (var and_)) (set of false) (set cf false) (set _result (var and_)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
d "or r8d, 0x01" 4183c801 0x0 (seq (set _or (| (cast 32 false (var r8)) (cast 32 false (bv 8 0x1)))) (set r8 (cast 64 false (var _or))) (set of false) (set cf false) (set _result (var _or)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
d "adc esi, 0x00" 83d600 0x0 (seq (set _op1 (cast 32 false (var rsi))) (set _op2 (cast 32 false (bv 8 0x0))) (set sum (+ (+ (var _op1) (var _op2)) (ite (var cf) (bv 32 0x1) (bv 32 0x0)))) (set rsi (cast 64 false (var sum))) (set _result (var sum)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (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 "sbb qword [rsp+0x30], 0xffffffffffffffff" 48835c2430ff 0x0 (seq (set _op1 (loadw 0 64 (+ (var rsp) (bv 64 0x30)))) (set _op2 (cast 64 false (bv 8 0xff))) (set _diff (- (- (var _op1) (var _op2)) (ite (var cf) (bv 64 0x1) (bv 64 0x0)))) (storew 0 (+ (var rsp) (bv 64 0x30)) (var _diff)) (set _result (var _diff)) (set pf (! (lsb (let _val (cast 8 false (var _result)) (let _c4 (^ (var _val) (>> (var _val) (bv 8 0x4) false)) (let _c2 (^ (var _c4) (>> (var _c4) (bv 8 0x2) false)) (^ (var _c2) (>> (var _c2) (bv 8 0x1) false)))))))) (set zf (is_zero (var _result))) (set sf (msb (var _result))) (set _result (var _diff)) (set _x (var _op1)) (set _y (var _op2)) (set cf (|| (|| (&& (! (msb (var _x))) (msb (var _y))) (&& (msb (var _y)) (msb (var _result)))) (&& (msb (var _result)) (! (msb (var _x)))))) (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 _y))) (msb (cast 4 false (var _result))))) (&& (msb (cast 4 false (var _result))) (! (msb (cast 4 false (var _x))))))))

871
test/db/rzil/x86
View file

@ -171,4 +171,875 @@ xmm0 = 0x00000000000000004010000000000000
rax = 0x0000000000000003
xmm0 = 0x0000000000000000401800003fc00000
EOF
NAME=Missing casting of arguments and register write issue test
FILE==
CMDS=<<EOF
e asm.arch=x86
e asm.bits=64
echo "\n====="
wx 4883e1f0
pi 1
aoip
echo "\n====="
wx 4183c801
pi 1
aoip
echo "\n====="
wx 83d600
pi 1
aoip
echo "\n====="
wx 48835c2430ff
pi 1
aoip
echo "\n====="
wx 838db4000000
pi 1
aoip
echo "\n====="
wx 48834f1008
pi 1
aoip
echo "\n====="
wx 4883d803
pi 1
aoip
echo "\n====="
wx 834b100c
pi 1
aoip
echo "\n====="
wx 83ce10
pi 1
aoip
echo "\n====="
wx 4183ceff
pi 1
aoip
EOF
EXPECT=<<EOF
=====
and rcx, 0xfffffffffffffff0
0x0
(seq
(set and_
(&
(var rcx)
(bv 64 0xfffffffffffffff0)))
(set rcx
(var and_))
(set of
false)
(set cf
false)
(set _result
(var and_))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result))))
=====
or r8d, 0x01
0x0
(seq
(set _or
(|
(cast 32
false
(var r8))
(cast 32
false
(bv 8 0x1))))
(set r8
(cast 64
false
(var _or)))
(set of
false)
(set cf
false)
(set _result
(var _or))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result))))
=====
adc esi, 0x00
0x0
(seq
(set _op1
(cast 32
false
(var rsi)))
(set _op2
(cast 32
false
(bv 8 0x0)))
(set sum
(+
(+
(var _op1)
(var _op2))
(ite
(var cf)
(bv 32 0x1)
(bv 32 0x0))))
(set rsi
(cast 64
false
(var sum)))
(set _result
(var sum))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(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))))))))
=====
sbb qword [rsp+0x30], 0xffffffffffffffff
0x0
(seq
(set _op1
(loadw 0 64
(+
(var rsp)
(bv 64 0x30))))
(set _op2
(cast 64
false
(bv 8 0xff)))
(set _diff
(-
(-
(var _op1)
(var _op2))
(ite
(var cf)
(bv 64 0x1)
(bv 64 0x0))))
(storew 0
(+
(var rsp)
(bv 64 0x30))
(var _diff))
(set _result
(var _diff))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result)))
(set _result
(var _diff))
(set _x
(var _op1))
(set _y
(var _op2))
(set cf
(||
(||
(&&
(!
(msb
(var _x)))
(msb
(var _y)))
(&&
(msb
(var _y))
(msb
(var _result))))
(&&
(msb
(var _result))
(!
(msb
(var _x))))))
(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 _y)))
(msb
(cast 4
false
(var _result)))))
(&&
(msb
(cast 4
false
(var _result)))
(!
(msb
(cast 4
false
(var _x))))))))
=====
or dword [rbp+0xb4], 0x00
0x0
(seq
(set _or
(|
(loadw 0 32
(+
(var rbp)
(bv 64 0xb4)))
(cast 32
false
(bv 8 0x0))))
(storew 0
(+
(var rbp)
(bv 64 0xb4))
(var _or))
(set of
false)
(set cf
false)
(set _result
(var _or))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result))))
=====
or qword [rdi+0x10], 0x08
0x0
(seq
(set _or
(|
(loadw 0 64
(+
(var rdi)
(bv 64 0x10)))
(cast 64
false
(bv 8 0x8))))
(storew 0
(+
(var rdi)
(bv 64 0x10))
(var _or))
(set of
false)
(set cf
false)
(set _result
(var _or))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result))))
=====
sbb rax, 0x03
0x0
(seq
(set _op1
(var rax))
(set _op2
(cast 64
false
(bv 8 0x3)))
(set _diff
(-
(-
(var _op1)
(var _op2))
(ite
(var cf)
(bv 64 0x1)
(bv 64 0x0))))
(set rax
(var _diff))
(set _result
(var _diff))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result)))
(set _result
(var _diff))
(set _x
(var _op1))
(set _y
(var _op2))
(set cf
(||
(||
(&&
(!
(msb
(var _x)))
(msb
(var _y)))
(&&
(msb
(var _y))
(msb
(var _result))))
(&&
(msb
(var _result))
(!
(msb
(var _x))))))
(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 _y)))
(msb
(cast 4
false
(var _result)))))
(&&
(msb
(cast 4
false
(var _result)))
(!
(msb
(cast 4
false
(var _x))))))))
=====
or dword [rbx+0x10], 0x0c
0x0
(seq
(set _or
(|
(loadw 0 32
(+
(var rbx)
(bv 64 0x10)))
(cast 32
false
(bv 8 0xc))))
(storew 0
(+
(var rbx)
(bv 64 0x10))
(var _or))
(set of
false)
(set cf
false)
(set _result
(var _or))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result))))
=====
or esi, 0x10
0x0
(seq
(set _or
(|
(cast 32
false
(var rsi))
(cast 32
false
(bv 8 0x10))))
(set rsi
(cast 64
false
(var _or)))
(set of
false)
(set cf
false)
(set _result
(var _or))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result))))
=====
or r14d, 0xffffffff
0x0
(seq
(set _or
(|
(cast 32
false
(var r14))
(cast 32
false
(bv 8 0xff))))
(set r14
(cast 64
false
(var _or)))
(set of
false)
(set cf
false)
(set _result
(var _or))
(set pf
(!
(lsb
(let _val
(cast 8
false
(var _result))
(let _c4
(^
(var _val)
(>>
(var _val)
(bv 8 0x4)
false))
(let _c2
(^
(var _c4)
(>>
(var _c4)
(bv 8 0x2)
false))
(^
(var _c2)
(>>
(var _c2)
(bv 8 0x1)
false))))))))
(set zf
(is_zero
(var _result)))
(set sf
(msb
(var _result))))
EOF
EXPECT_ERR=
RUN