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
