On 8/12/24 5:13 AM, Matevos Mehrabyan wrote:

    On Fri, Aug 2, 2024, 14:25 Richard Biener
    <richard.guent...@gmail.com <mailto:richard.guent...@gmail.com>> wrote:
     > On Wed, Jul 31, 2024 at 12:42 PM Mariam Arutunian
     > <mariamarutun...@gmail.com <mailto: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.
Right. IIRC we need to track that a given bit has some same value as some other bit. We could probably fake it by finding a tree code in the same neighborhood as SYMBOLIC_BIT and BIT, but I'm not sure doing so really helps maintenance in any notable way.


;

    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.
Right. It could potentially be useful to for other bitwise analysis. It's got a pretty limited set of operations, but they could always be extended.

I'd kind of hoped we could extend the existing symbolic execution and propagation engines rather than adding another. But that never really panned out the way I'd hoped -- in particular I think we could use those existing mechanisms for the polynomial extraction, but they'd need significant work for the validation step IIRC.


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?
I'm torn. We end to document in the .cc files which just encourages folks to look at the implementation rather than defining crisp APIs that can be understood and used solely from looking at headers. I've never liked that approach.

But I also don't want to have a module like the bitwise symbolic execution do something significantly differently than what we do elsewhere. So document in the appropriate .cc file.

I think the question to Richi is whether or not converting the store merging code to this new symbolic execution engine (or using the store-merging symbolic execution engine in the CRC validator) is a requirement to move forward.

Jeff

Reply via email to