On Tue, 11 Jul 2023, Richard Biener wrote:
I'll update my implementation, and will come back with a more detailed
proposal in a few weeks when I have tried some more things.
Thanks! I've also taken the opportunity given by your work at the recent
bugs to propose a talk at this years GNU Cauldron about undefined
behavior on GCC and hope to at least start on documenting the state of
art^WGCC in the internals manual for this. If you have any pointers to
your work / research I'd be happy to point to it, learn from it (and maybe
steal a word or two ;)).
Nice!
No, I have not published anything since the original release of 'pysmtgcc'
last year -- I was planning to document it in detail, but found out that
nothing worked, and I did not really understand what I was doing... And
the Python prototype started to be annoying, so I threw all away and wrote
a new tool in C++.
The new implementation now handles most of GIMPLE (but it still does not
handle loops or function calls). I also have support for checking that the
generated assembly has the same semantics as the optimized GIMPLE (only
partial support for RISC-V for now). I plan to publish a write-up of the
memory model soon in a series of blog posts -- I'll send you the link when
it is available.
And FWIW, I'm also planning to submit a talk to GNU Cauldron. :)
My proposal is about "Analyzing IR and Assembly Using SMT Solvers". The
translation validation stuff is actually just a test case for my analysis
engine -- I have more ideas for how it can be used...
/Krister
