On Fri, 11 Jul 2025, Filip Kastl wrote:
Please let me know if there are additional configurations you would like me
to include in the testing.
Seems like work on smtgcc is going nicely. Good to hear!
Have you considered -Ofast or some subset of the flags it enables? Perhaps
that would uncov
On Wed, 2 Jul 2025, Sam James wrote:
Please let me know if there are additional configurations you would
like me to include in the testing.
We sometimes get interesting bugs, especially with UBSAN
(-fsanitize=undefined), with SAVE_EXPR. PR120471 is one example and
PR120837 is another.
These
I have continued working on my translation validator, smtgcc [1]. Here is
an update of what I have done since the end-of-year update.
smtgcc-tv-backend
-
The main focus has been improving the smtgcc-tv-backend tool which checks
that the generated assembly is a refinement of the
I'm working on ensuring that the GIMPLE semantics used by smtgcc are
correct, and I have a lot of questions about the details. I'll be sending
a series of emails with these questions. This first one is about pointers
in general.
Each section starts with a description of the semantics I've impl
On Thu, 3 Apr 2025, Richard Biener wrote:
On Thu, Apr 3, 2025 at 2:23 AM Krister Walfridsson via Gcc
wrote:
I have more questions about GIMPLE memory semantics for smtgcc.
As before, each section starts with a description of the semantics I've
implemented (or plan to implement), follow
I have more questions about GIMPLE memory semantics for smtgcc.
As before, each section starts with a description of the semantics I've
implemented (or plan to implement), followed by concrete questions if
relevant. Let me know if the described semantics are incorrect or
incomplete.
Accessi
On Thu, 20 Mar 2025, Richard Biener wrote:
Pointer arithmetic -- POINTER_DIFF_EXPR
---
Subtracting a pointer q from a pointer p is done using POINTER_DIFF_EXPR.
* It is UB if the difference does not fit in a signed integer with the
same precision as the
On Fri, 21 Mar 2025, Richard Biener wrote:
Issues
--
The semantics I've described above result in many reports of
miscompilations that I haven't reported yet.
As mentioned earlier, the vectorizer can use POINTER_PLUS_EXPR to generate
pointers that extend up to a vector length past the objec
On Thu, 2 Jan 2025, Andi Kleen wrote:
Krister Walfridsson via Gcc writes:
But running smtgcc on the test suite is not the best use case for the
tool -- it only detects bugs where the test triggers an unrelated bug
compared to what the test is checking, which should be uncommon. I
therefore
I have continued working on my translation validator, smtgcc [1], over the
last few months. Here's an update on what has happened since my talk at
the GNU Tools Cauldron [2].
Improvements
The main focus has been improving the smtgcc-tv-backend tool which checks
that the generated
On Sun, 18 Aug 2024, Gerald Pfeifer wrote:
On Sat, 30 Sep 2023, Krister Walfridsson via Gcc wrote:
I have now released the new implementation for translation validation I talked
about at the GNU Tools Cauldron last week:
https://github.com/kristerw/smtgcc
Wouldn't it be appropriate/ni
I have now released the new implementation for translation validation I
talked about at the GNU Tools Cauldron last week:
https://github.com/kristerw/smtgcc
/Krister
On Fri, 1 Sep 2023, Richard Biener wrote:
The value of .CLZ (0) is undefined then. I belive your analysis is correct in
that both 63 - _35 might overflow and that dom3 (thus ranger) mis-computes
the range for _35. I wonder why we don't elide _36 ? _31 : 1 with that info
(possibly no range-op f
My translation validation tool reports some miscompilations related to the
internal call CLZ(0) when CLZ_DEFINED_VALUE_AT_ZERO is false, but I am not
sure I use the correct semantics...
I started by modeling CLZ(0) as undefined behavior, but that made the tool
report a miscompilation for gcc.c
On Tue, 11 Jul 2023, Krister Walfridsson wrote:
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 recen
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 Cauld
On Tue, 11 Jul 2023, Richard Biener wrote:
With "plain copies", do you mean treating it as it is always defined? That
would prevent optimizations such as transforming
int t;
if (1)
t = *p;
else
t = 0;
return t + 1;
to the equivalent of
return *p + 1;
because the latt
On Fri, 7 Jul 2023, Richard Biener wrote:
I have implemented support for uninitialized memory in my translation
validator. But I am not sure how well this corresponds to the GIMPLE
semantics, so I have some questions...
My implementation tracks uninitialized bits. Use of uninitialized bits is
i
I have implemented support for uninitialized memory in my translation
validator. But I am not sure how well this corresponds to the GIMPLE
semantics, so I have some questions...
My implementation tracks uninitialized bits. Use of uninitialized bits is
in general treated as UB (for example, `x
On Thu, 29 Jun 2023, Richard Biener wrote:
IIRC we have some simplification rules that turn bit operations into
arithmetics. Arithmetic is allowed if it keeps the values inside
[-1,0] for signed bools or [0, 1] for unsigned bools.
I have now verified that all cases seems to be just one operat
On Thu, 29 Jun 2023, Richard Biener wrote:
The thing with signed bools is that the two relevant values are -1 (true)
and 0 (false), those are used for vector bool components where we also
need them to be of wider type (32bits in this case).
My main confusion comes from seeing IR doing arithmet
I have some random questions concerning types in the GIMPLE IR that I
would appreciate some clarification on.
Type safety
---
Some transformations treat 1-bit types as a synonym of _Bool and mix the
types in expressions, such as:
_2;
_Bool _3;
_Bool _4;
...
_4 = _2 ^ _3;
On Tue, 27 Jun 2023, Richard Biener wrote:
I think this is a bug in NRV, yes, is special but the above would
allow to DSE the three stores.
Can you open a bugreport?
Done! https://gcc.gnu.org/bugzilla/show_bug.cgi?id=110434
I'm working on an updated version of my translation validator [*], and I
have some problems with CLOBBER(eol).
I currently treat CLOBBER(eol) as making the memory invalid (i.e. all
subsequent accesses is undefined behavior), but the tool reports
miscompilation for a few cases where the tree-nr
On Wed, 14 Sep 2022, Richard Biener wrote:
Note that the folding/peephole optimizations done early can be avoided
when you separate opportunities in the source to multiple statements,
like change
int a, b;
a = b + 1 - b;
to
a = b + 1;
a = a - b;
note that parts of the folding optimizations
I have implemented a tool for translation validation (similar to Alive2
for LLVM). The tool takes GIMPLE IR for two functions and checks that the
second is a refinement of the first. That is,
* The returned value is the same for both functions for all input that
does not invoke undefined beh
On Thu, 1 Sep 2022, Richard Biener wrote:
It's generally poorly documented what is considered 'undefined behavior'.
We desparately need a section in the internals manual for this.
For the {L,R}SHIFT_EXPR case we assume the shift operand is
in range of [0, precision - 1], so in theory value-range
I'm implementing a tool for translation validation (similar to Alive2 for
LLVM). The tool uses an SMT solver to verify for each GIMPLE pass that the
output IR is a refinement of the input IR:
* That each compiled function returns an identical result before/after
the pass (for input that does
28 matches
Mail list logo
