smtgcc translation validation

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

Re: CLZ when CLZ_DEFINED_VALUE_AT_ZERO is false

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

CLZ when CLZ_DEFINED_VALUE_AT_ZERO is false

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

Re: semantics of uninitialized values in GIMPLE

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

Re: semantics of uninitialized values in GIMPLE

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

Re: semantics of uninitialized values in GIMPLE

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

Re: semantics of uninitialized values in GIMPLE

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

semantics of uninitialized values in GIMPLE

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

Re: types in GIMPLE IR

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

Re: types in GIMPLE IR

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

types in GIMPLE IR

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;

Re: CLOBBER(eol)

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

CLOBBER(eol)

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

Re: Translation validation

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

Translation validation

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

Re: GIMPLE undefined behavior

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

GIMPLE undefined behavior

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

Re: [PATCH] target/58397: add host_hooks for NetBSD to make precompiled headers work

On Sun, 25 Nov 2018, Maya Rashish wrote: gcc/config.host | 4 ++ gcc/config/host-netbsd.c | 85 gcc/config/x-netbsd | 4 ++ 3 files changed, 93 insertions(+) create mode 100644 gcc/config/host-netbsd.c create mode 100644 gcc/config/x-netbsd

Re: [PATCH] Add netbsd-stdint.h to several netbsd targets

On Sun, Sep 3, 2017 at 5:16 PM, Maya Rashish wrote: > grouping netbsd.h netbsd-stdint.h netbsd-elf.h as "nbsd_tm_file", > similar to freebsd. I found a small bug in the patch -- the NetBSD stdint.h have different definitions for 8- and 16-bit "fast" types than what is in the

[committed] Fix PR 39570 - cabs/cabsf named differently on NetBSD

-netbsd6.1. /Krister 2017-09-26 Krister Walfridsson <krister.walfrids...@gmail.com> PR target/39570 * gcc/config/netbsd-protos.h: New file. * gcc/config/netbsd.c: New file. * gcc/config/netbsd.h (SUBTARGET_INIT_BUILTINS): Define. * gcc/conf

[committed] Always assume NetBSD provides __cxa_atexit

I have committed the attached patch to remove checks for obsolete NetBSD releases from the 1990s that do not provide __cxa_atexit. Bootstrapped and tested on i386-unknown-netbsdelf6.1 and x86_64-unknown-netbsd6.1. /Krister 2017-07-23 Krister Walfridsson <krister.walfrids...@gmail.

committed: Always assume NetBSD support pthreads

I have committed the attached patch to remove checks for obsolete NetBSD releases from the 1990s that do not support pthreads. Bootstrapped and tested on i386-unknown-netbsdelf6.1 and x86_64-unknown-netbsd6.1. /Krister 2017-07-09 Krister Walfridsson <krister.walfrids...@gmail.

committed: Remove libgcc/config.host check for aout NetBSD releases

I have committed the attached patch to remove a check for obsolete NetBSD aout releases from the 1990s. Bootstrapped and tested on i386-unknown-netbsdelf6.1 and x86_64-unknown-netbsd6.1. /Krister 2017-07-09 Krister Walfridsson <krister.walfrids...@gmail.com> * confi

Re: committed: Fix NetBSD problem PR80600

On Mon, 15 May 2017, Krister Walfridsson wrote: I have committed the attached patch to make NetBSD handle -lgcc correctly for shared libraries. gcc/ChangeLog: PR target/80600 * config/netbsd.h (NETBSD_LIBGCC_SPEC): Always add -lgcc. libgcc/ChangeLog: PR target/80600

committed: Fix NetBSD problem PR80600

I have committed the attached patch to make NetBSD handle -lgcc correctly for shared libraries. gcc/ChangeLog: PR target/80600 * config/netbsd.h (NETBSD_LIBGCC_SPEC): Always add -lgcc. libgcc/ChangeLog: PR target/80600 * config.host (*-*-netbsd*): Add

Re: Use a specfile that actually allows building programs on NetBSD

On Mon, 9 Jan 2017, co...@sdf.org wrote: 3 month ping, 1 week ping (trying again), etc... Apologies for not getting back to you sooner. Like most operating systems, NetBSD has a libc which contains stuff it needs for most programs to work, and people expect it to be linked without

committed: define LINK_EH_SPEC for NetBSD

I have committed the attached to add a LINK_EH_SPEC enabling --eh-frame-hdr in the NetBSD config. Bootstrapped and tested on x86_64-unknown-netbsd6.1. /Krister 2016-12-19 Krister Walfridsson <krister.walfrids...@gmail.com> * config/netbsd.h (LINK_EH_SPEC): Define.Inde

committed: add t-eh-dw2-dip to NetBSD libgcc tmake_file

I have committed the attached patch to add t-eh-dw2-dip to NetBSD libgcc tmake_file. Bootstrapped and tested on i386-unknown-netbsdelf6.1 and x86_64-unknown-netbsd6.1. /Krister 2016-12-19 Krister Walfridsson <krister.walfrids...@gmail.com> * config.host (*-*-netbsd*): Ad

committed: make i486 default arch for x86 NetBSD

I have committed the attached patch to make i486 the default arch on NetBSD in the same way as for FreeBSD, as 386 CPUs are not supported on any maintained version of NetBSD. Bootstrapped and tested on i386-unknown-netbsdelf6.1 /Krister 2016-12-10 Krister Walfridsson <krister.walfr

committed: add i386/t-crtstuff to i[34567]86-*-netbsdelf tmake_file

I have committed the attached patch to add i386/t-crtstuff to tmake_file for i[34567]86-*-netbsdelf*. Bootstrapped and tested on i386-unknown-netbsdelf6.1 (fixes 29378 failures) /Krister 2016-12-10 Krister Walfridsson <krister.walfrids...@gmail.com> * config.host (i[34

Re: [PATCH] Fix NetBSD bootstrap

ng mode) or "provide" (always use GCC's header). I committed the following to set it to "wrap" (which is consistent with how the other BSDs handle it). Bootstrapped and tested on x86_64-unknown-netbsd6.1. /Krister 2016-11-19 Krister Walfridsson <krister.walfrids...@g

Re: [PATCH] Fix NetBSD bootstrap

On Wed, 16 Nov 2016, Mike Stump wrote: Looks reasonable. The biggest issue would be if any of those values changed through time, and the current version works for older netbsd releases, the patch could break them. Of course, I don't have any visibility into how any of those values might

[PATCH] Fix NetBSD bootstrap

maintainer, so I belive I don't need approval to commit this. But I have been absent for a long time, so it makes sense for someone to review at least this first patch. Bootstrapped and tested on i386-unknown-netbsdelf6.1 and x86_64-unknown-netbsd6.1. OK to commit? /Krister 2016-11-16 Krister

Re: 33 unknowns left

On Wed, 26 Aug 2015, Joseph Myers wrote: kristerw = kristerw Krister Walfridsson <krister.walfrids...@gmail.com> Yes, this is my current address (the "cato@" address mentioned in some other mail is obsolete). [I have been away from GCC development for a long time, but

Re: Re: PR39570 (gfortran) cabs and cabsf are named differently on NetBSD 5

Apologies for the slow response. On Mon, 26 Jan 2015, Kai-Uwe Eckhardt wrote: according to gcc/MAINTAINERS Jason and Krister are NetBSD maintainers for GCC and can approve patches like yours, so let me copy them. (Should this be applied now, at least the copyright years need to be adjusted to

Re: [Bug fortran/48244] iso-c-binding support missing on NetBSD (with patch)

--- Comment #1 from Dominique d'Humieres dominiq at lps dot ens.fr --- Is there still maintainers/users of NetBSD? There are still users. But my paperwork is not in order since I changed employer some years ago, so I am not allowed to commit anything... :( /Krister

Re: [patch] PR 51006 fix bootstrap failure on NetBSD

On Mon, Jan 2, 2012 at 1:06 PM, Jonathan Wakely jwakely@gmail.com wrote: libgcc/ChangeLog 2012-01-02  Jonathan Wakely  jwakely@gmail.com        PR bootstrap/51006        * enable-execute-stack-mprotect.c (getpagesize): Do not define        for NetBSD. This removes the definition of

Re: gnat1 huge time

On Fri, 30 Nov 2007, Joel Sherrill wrote: Krister Walfridsson wrote: On Wed, 28 Nov 2007, Joel Sherrill wrote: I am trying to get the SVN head built locally again and back at work on the GNAT/RTEMS work I was doing. Unfortunately, I have tripped across something that is quite bad. Compiling

Re: gnat1 huge time

On Wed, 28 Nov 2007, Joel Sherrill wrote: I am trying to get the SVN head built locally again and back at work on the GNAT/RTEMS work I was doing. Unfortunately, I have tripped across something that is quite bad. Compiling on Linux x86 targeting the PowerPC or SPARC leads to a huge

Re: Krister Walfridsson appointed NetBSD OS port maintainer

On Thu, 30 Aug 2007, David Edelsohn wrote: I am pleased to announce that the GCC Steering Committee has appointed Krister Walfridsson as NetBSD OS port maintainer. Please join me in congratulating Krister on his new role. Krister, please update your listing in the MAINTAINERS