On Fri, Aug 16, 2024 at 4:33 PM Jeff Law <jeffreya...@gmail.com> wrote: > > > > 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.
I'm fine with documenting in the .cc file. > 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. So the store-merging variant IIRC tracks a single overall source only (unless it was extended and I missed that) and operates at a byte granularity. I did want to extend it to support vector shuffles at one point (with two sources then), but didn't get to it. The current implementation manages to be quite efficient - mainly due to the restriction to a single source I guess. How does that compare to the symbolic execution engine? What can the symbolic execution engine handle? The store-merging machinery can only handle plain copies, can the symbolic execution engine tell that for example bits 3-7 are bits 1-5 from A plus constant 9 with appropriately truncated result? Note we should always have an eye on compile-time complexity, GCC does get used on multi-megabyte machine-generated sources that tend to look very uniform - variants with loops and bit operations supported by symbolic execution would not catch me in surprise. Richard. > Jeff
