>
>
> On Fri, Aug 2, 2024, 14:25 Richard Biener <richard.guent...@gmail.com>
> wrote:
> > On Wed, Jul 31, 2024 at 12:42 PM Mariam Arutunian
> > <mariamarutun...@gmail.com> 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 added more comments for functions in the new patch.
> 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?
>
>
This enum is used for inner purposes. It represents a single bit. It is
used by 'is_a_helper<>'
for type checking and some printing. As you can see it also has values such
as 'BIT'
and 'SYMBOLIC_BIT' that represents constant and symbolic bits. 'tree_code'
doesn't have
such similar values. At most, I can remove Expression values from it and
use both 'value_type'
and 'tree_code', but it wouldn't be handy.
> 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"?
>
>
I have updated the API. Now, it has the following form:
bool do_operation (enum tree_code, tree, tree, tree);
> 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.
>
>
Currently, this is only used for CRC candidate functions. It supports
limited expressions
that we met while analyzing CRC functions, but can be extended. New
expressions must be
represented at the bit level as the symbolic executor operates on the bit
level.
I can add documentation for this version. In which section should this be
added or I should add
the documentation in the source file as it's done for
gimple-ssa-store-merging.cc?
> 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?
>
>
I think this symbolic executor can be used there too. Bits' positions and
their origins are saved for
each bit making it easy to understand where each bit came from.
> Richard.
>
>
> > Author: Matevos Mehrabyan <matevosmehrab...@gmail.com>
> >
> > 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 <mariamarutun...@gmail.com>
>
Best Regards,
Matevos.
