ercoppa

The current implementation of `visitSelectInst` is: ``` void Symbolizer::visitSelectInst(SelectInst &I) { // Select is like the ternary operator ("?:") in C. We push the (potentially // negated) condition to the...

Consider this example (inspired by a real-world code): ``` #include #include #include int bar(unsigned char a) { if (a == 0xCA) return -1; else return 0; } int main() {...

Consider the following example (inspired by a real-world program): ``` int main(int argc, char *argv[]) { char c[8]; ssize_t nbytes = read(STDIN_FILENO, c, 1); if (nbytes != 1) return 1;...

The current implementation of `_sym_get_input_byte` in the simple backend is: ``` Z3_ast _sym_get_input_byte(size_t offset, uint8_t) { static std::vector stdinBytes; if (offset < stdinBytes.size()) return stdinBytes[offset]; auto varName = "stdin" +...

Support for variadic functions

1

Consider this function: ``` int variadic_foo(int count, ...) { va_list args; int i; va_start(args, count); int sum = 0; for (i = 0; i < count; i++) sum += va_arg(args,...

fix notify bb site_id

1

See issue #21

Setcond handling

3

For instance, let us consider the handling of `setcond_i32`: ``` tcg_gen_op4i_i32(INDEX_op_setcond_i32, ret, arg1, arg2, cond); TCGv_i32 cond_temp = tcg_const_i32(cond); gen_helper_sym_setcond_i32( tcgv_i32_expr(ret), cpu_env, arg1, tcgv_i32_expr(arg1), arg2, tcgv_i32_expr(arg2), cond_temp, ret); tcg_temp_free_i32(cond_temp); ```...

Muluh symbolic value is concretized

1

Symqemu defines a symbolic helper for `muluh_i64`: ``` void *HELPER(sym_muluh_i64)(uint64_t arg1, void *arg1_expr, uint64_t arg2, void *arg2_expr) { BINARY_HELPER_ENSURE_EXPRESSIONS; assert(_sym_bits_helper(arg1_expr) == 64 && _sym_bits_helper(arg2_expr) == 64); void *full_result = _sym_build_mul(_sym_build_zext(arg1_expr,...

Symbolization of QEMU helpers with SymCC

1

SymQEMU ignores the effects of most QEMU helpers. Some of them, especially on i386/x86_64, are quite common when analyzing real-world programs. Manually writing symbolic helpers is quite hard in several...

Wrong site_id in notify BB

1

The current code in `gen_tb_start`: ``` TCGv_i64 block = tcg_const_i64((uint64_t)tb); ``` uses as `site_id` the address of struct TB. This address does not reflect the address of the original BB....