On Wed, Jul 31, 2024 at 12:42 PM Mariam Arutunian
<[email protected]> wrote:
>
> Gives an opportunity to execute the code on bit level,
> assigning symbolic values to the variables which don't have initial values.
> Supports only CRC specific operations.
>
> Example:
>
> uint8_t crc;
> uint8_t pol = 1;
> crc = crc ^ pol;
>
> during symbolic execution crc's value will be:
> crc(8), crc(7), ... crc(1), crc(0) ^ 1
There seem to be quite some functions without a function comment.
I see
+enum value_type {
+ SYMBOLIC_BIT,
+ BIT,
+ BIT_XOR_EXPRESSION,
+ BIT_AND_EXPRESSION,
+ BIT_OR_EXPRESSION,
+ BIT_COMPLEMENT_EXPRESSION,
+ SHIFT_RIGHT_EXPRESSION,
+ SHIFT_LEFT_EXPRESSION,
+ ADD_EXPRESSION,
+ SUB_EXPRESSION,
+ BIT_CONDITION
+};
is there a specific reason to make the expressions not use enum tree_code?
The main API (?) has
+ /* Does bit-level XOR operation for given variables. */
+ bool do_xor (tree arg1, tree arg2, tree dest);
+
+ /* Does bit-level AND operation for given variables. */
+ bool do_and (tree arg1, tree arg2, tree dest);
+
+ /* Does bit-level OR operation for given variables. */
+ bool do_or (tree arg1, tree arg2, tree dest);
+
...
that could better be
bool do (enum tree_code, tree, tree, tree);
so symbolic execution of a set of GIMPLE stmts would not require
"indirection"?
How is this all used and what are the constraints? It does look like
a generic framework which means documentation in the internals
manual would be useful to be had.
We have some crude symbolic execution in gimple-ssa-store-merging.cc
for the purpose of detecting byte-swaps. That operates on a byte level.
It is quite efficient. I assume that the new symbolic execution framework
could be used to replace that or am I mis-characterizing what it does?
Richard.
> Author: Matevos Mehrabyan <[email protected]>
>
> gcc/
>
> * Makefile.in (OBJS): Add sym-exec/expression.o,
> sym-exec/state.o, sym-exec/condition.o.
> * configure (sym-exec): New subdir.
>
> gcc/sym-exec/
>
> * condition.cc: New file.
> * condition.h: New file.
> * expression-is-a-helper.h: New file.
> * expression.cc: New file.
> * expression.h: New file.
> * state.cc: New file.
> * state.h: New file.
>
> Signed-off-by: Mariam Arutunian <[email protected]>
