Skip to content

Commit

Permalink
Added instrumentation of vector TCG operations (#38)
Browse files Browse the repository at this point in the history
* add util function for vec expr
* instrument tcg_gen_mov_vec
* instrumented tcg_gen_ld_vec
* add tcgv_vec_expr util function
* simplify sym_store_host helper
* instrumented tcg_gen_st_vec
* instrument tcg_gen_stl_vec
* add malloc and free helper functions
* util functions for vector instrumentation
* instrumented tcg_gen_and_vec
* implemented sym helper for and vec
* generalized sym_and_vec implementation
* instrumented vec or, xor, add, sub,mul
* make vector operations andc, orc, nand, nor, eqv be built with instrumented operations
* make vector operations not and neg be built with instrumented operations
* make vector operations abs be built with instrumented operations
* add build_symbol_for_vector_int32_op function
* instrumented vec vec shifts and rotates ops
* instrumented vec i32 shifts and rotates ops
* instrumented vec immediate shifts and rotates ops
* add support of helper functions with 8 and 9 args
* instrumented tcg_gen_cmp_vec
* concretize not yet instrumented vec ops results to avoid a crash
* instrumented saturating signed/unsigned sub/add vec instructions
* make sure cmpsel and bitsel instructions are generated using already instrumented instructions
* instrumented tcg_gen_dup_i64_vec, tcg_gen_dup_i32_vec functions
* instrumented min max functions
* instrumented tcg_gen_dup_mem_vec
* fix wrong assert in sym_load_and_duplicate_into_vec
* put vec helpers in a separate file
* TODO: some indirectly instrumented instructions could have better performance with direct instrumentation 
* TODO: returning expressions instead of pushing path constraints
* Add asprintf test program
This target program resulted in incorrect results before the vector instructions were instrumented
* Update SymQEMU unit tests (check-sym-runtime.c)
"helper_sym_store_host_i64" and "helper_sym_store_host_i32" were
replaced by helper_sym_store_host, adjusting the unit tests
accordingly

---------

Co-authored-by: Aurelien Francillon <[email protected]>
  • Loading branch information
damienmaier and aurelf authored Feb 22, 2024
1 parent 3763b2f commit 5c00e64
Show file tree
Hide file tree
Showing 78 changed files with 1,249 additions and 114 deletions.
16 changes: 9 additions & 7 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -146,13 +146,15 @@ Also, refer to [QEMU's own tests suite documentation](https://www.qemu.org/docs/
## Documentation
The [paper](http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html)
contains details on how SymQEMU works. A large part of the implementation is the
run-time support in `accel/tcg/tcg-runtime-sym.{c,h}` (which delegates any
actual symbolic computation to SymCC's symbolic backend), and we have modified
most code-generating functions in `tcg/tcg-op.c` to emit calls to the runtime.
For development, configure with `--enable-debug` for run-time assertions; there
are tests for the symbolic run-time support in `tests/check-sym-runtime.c`.
The [paper](http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html) contains
details on how SymQEMU works. A large part of the implementation is the run-time support
in `accel/tcg/tcg-runtime-sym.{c,h}` and `accel/tcg/tcg-runtime-sym-vec.{c,h}` (which
delegates any actual symbolic computation to SymCC's symbolic backend), and we have
modified most code-generating functions in `tcg/tcg-op.c`, `tcg/tcg-op-vec.c` and
`include/tcg/tcg-op-common.h` to emit calls to the runtime.
For development, configure with `--enable-debug` for run-time assertions; there are tests
for the symbolic run-time support in `tests/check-sym-runtime.c`.
More information about the port to QEMU 8 and internals of (Sym)QEMU
can be found in the QEMU 8 merge commit message
Expand Down
2 changes: 2 additions & 0 deletions accel/tcg/meson.build
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ tcg_ss.add(files(
'tcg-runtime-gvec.c',
'tcg-runtime.c',
'tcg-runtime-sym.c',
'tcg-runtime-sym-vec.c',
'tcg-runtime-sym-common.c',
'translate-all.c',
'translator.c',
))
Expand Down
95 changes: 95 additions & 0 deletions accel/tcg/tcg-runtime-sym-common.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
#include "qemu/osdep.h"
#include "cpu.h"
#include "exec/helper-proto.h"
#include "exec/cpu_ldst.h"
#include "qemu/qemu-print.h"
#include "tcg/tcg.h"
#include "exec/translation-block.h"

#include "accel/tcg/tcg-runtime-sym-common.h"

/* Include the symbolic backend, using void* as expression type. */

#define SymExpr void*
#include "RuntimeCommon.h"

void *build_and_push_path_constraint(CPUArchState *env, void *arg1_expr, void *arg2_expr, uint32_t comparison_operator, uint8_t is_taken){
void *(*handler)(void *, void*);
switch (comparison_operator) {
case TCG_COND_EQ:
handler = _sym_build_equal;
break;
case TCG_COND_NE:
handler = _sym_build_not_equal;
break;
case TCG_COND_LT:
handler = _sym_build_signed_less_than;
break;
case TCG_COND_GE:
handler = _sym_build_signed_greater_equal;
break;
case TCG_COND_LE:
handler = _sym_build_signed_less_equal;
break;
case TCG_COND_GT:
handler = _sym_build_signed_greater_than;
break;
case TCG_COND_LTU:
handler = _sym_build_unsigned_less_than;
break;
case TCG_COND_GEU:
handler = _sym_build_unsigned_greater_equal;
break;
case TCG_COND_LEU:
handler = _sym_build_unsigned_less_equal;
break;
case TCG_COND_GTU:
handler = _sym_build_unsigned_greater_than;
break;
default:
g_assert_not_reached();
}

void *condition_symbol = handler(arg1_expr, arg2_expr);
_sym_push_path_constraint(condition_symbol, is_taken, get_pc(env));

return condition_symbol;
}

/* Architecture-independent way to get the program counter */
target_ulong get_pc(CPUArchState *env)
{
target_ulong pc, cs_base;
uint32_t flags;

cpu_get_tb_cpu_state(env, &pc, &cs_base, &flags);

return pc;
}

void *sym_rotate_left(void *arg1_expr, void *arg2_expr) {
/* The implementation follows the alternative implementation of
* tcg_gen_rotl_i64 in tcg-op.c (which handles architectures that don't
* support rotl directly). */

uint8_t bits = _sym_bits_helper(arg1_expr);
return _sym_build_or(
_sym_build_shift_left(arg1_expr, arg2_expr),
_sym_build_logical_shift_right(
arg1_expr,
_sym_build_sub(_sym_build_integer(bits, bits), arg2_expr)));
}

void *sym_rotate_right(void *arg1_expr, void *arg2_expr) {

/* The implementation follows the alternative implementation of
* tcg_gen_rotr_i64 in tcg-op.c (which handles architectures that don't
* support rotr directly). */

uint8_t bits = _sym_bits_helper(arg1_expr);
return _sym_build_or(
_sym_build_logical_shift_right(arg1_expr, arg2_expr),
_sym_build_shift_left(
arg1_expr,
_sym_build_sub(_sym_build_integer(bits, bits), arg2_expr)));
}
4 changes: 4 additions & 0 deletions accel/tcg/tcg-runtime-sym-common.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
void *build_and_push_path_constraint(CPUArchState *env, void *arg1_expr, void *arg2_expr, uint32_t comparison_operator, uint8_t is_taken);
target_ulong get_pc(CPUArchState *env);
void *sym_rotate_left(void *arg1_expr, void *arg2_expr);
void *sym_rotate_right(void *arg1_expr, void *arg2_expr);
Loading

0 comments on commit 5c00e64

Please sign in to comment.