synth failure

[FSY369]

Version

Yosys 0.48+47 (git sha1 cbb95cb, clang++ 18.1.8 -fPIC -O3)

On which OS did this happen?

Linux

Reproduction Steps

1. Enter yosys in the terminal
2. read the rtl.v file, read_verilog rtl.v
3. synthesize the command, synth
4. synthesis failed

rtl.v.log

Expected Behavior

Synthesize Success

Actual Behavior

synthesis failed，2.5. Executing CHECK pass (checking for obvious problems).
Checking module module128...
Checking module module150...
浮点数例外 (核心已转储)

[whitequark]

You are submitting a bug report produced using fuzzing tools. With such bug reports, it is often hard to tell whether the issue reported is an issue in Yosys or an issue with the test harness.

You were instructed how to submit such bug reports properly and you are not following the instructions. As such I am closing your report as invalid.

[FSY369]

Sorry, I uploaded the wrong file, here is the minimal test case, the problem occurs with the assignment of reg161 thus causing the synthesis to fail.

rtl.v.log

[whitequark]

Thanks. For other readers, it seems that:

浮点数例外 (核心已转储)

means

Floating point exception (core dumped)

[whitequark]

I have reduced your testcase further using C-Reduce. Here is the actually minimal testcase:

module a(b, c, d);
	output b;
	input c;
	input d;
	always b <= $signed(f) << (0 ? 0 : g);
endmodule

I have done this by putting your code into issue4844.v, writing a shell script issue4844.sh that checks for a floating point error (code 136) being returned:

#!/bin/sh
yosys issue4844.v -p synth
[ $? -eq 136 ]

and running C-Reduce as:

$ creduce --not-c issue4844.sh issue4844.v

[whitequark]

What happens is that in the following code:

yosys/kernel/celledges.cc

Lines 250 to 257 in 6225abe

	for (int k = 0; k < b_width; k++) {
	// left shifts
	if (cell->type.in(ID($shl), ID($sshl))) {
	if (a_width == 1 && is_signed) {
	int skip = 1 << (k + 1);
	int base = skip -1;
	if (i % skip != base && i - a_width + 2 < 1 << b_width)
	db->add_edge(cell, ID::B, k, ID::Y, i, -1);

skip becomes 0 as k becomes 31. This actually seems like it would happen pretty much every time there is a signed left shift by a 32-bit value; I'm surprised it doesn't trigger more often.

I'm not actually sure what exactly this code is doing so I'll let someone else fix it.

[whitequark]

Oh also 1 << b_width triggers UB on each iteration of the loop when b_width == 32 (C99 §6.5.7.3):

The integer promotions are performed on each of the operands. The type of the result is that of the promoted left operand. If the value of the right operand is negative or is greater than or equal to the width of the promoted left operand, the behavior is undefined.

[whitequark]

@povik @nakengelhardt It looks like this bug was introduced in #3972. Not to put too fine a point on it, but the nondeterminism that I complained about two years ago was (almost certainly) caused by invoking UB, apparently, every single time that we had code akin to $signed(1) << 1, and it should have been investigated then instead of making excuses for it. The reason I thought it would be the case is because I get the crash with -Og but not with -O0, but after going through this issue and that one one more time it looks like the way codegen works out for this instance of UB is that it would deterministically produce the same result.

[whitequark]

By setting SANITIZER = undefined in Makefile.conf and setting the variable UBSAN_OPTIONS=halt_on_error=1 I am able to get it to crash in the sanitizer:

Checking module a...
kernel/celledges.cc:256:50: runtime error: shift exponent 32 is too large for 32-bit type 'int'
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior kernel/celledges.cc:256:50 in 

I think we should run ubsan on CI and I've filed #4845 to do that.

I ran the testsuite with UBSan enabled and got this:

SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior frontends/ast/simplify.cc:2939:21 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior kernel/celledges.cc:254:19 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior kernel/celledges.cc:255:22 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior kernel/celledges.cc:256:50 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior kernel/celledges.cc:259:30 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior kernel/celledges.cc:262:30 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:227:5 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:227:5 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:370:5 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:370:5 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:372:5 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:372:5 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:512:11 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:512:18 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:513:11 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:513:18 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:514:11 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:514:18 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:515:11 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:515:18 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:518:11 in
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior libs/fst/fastlz.cc:518:18 in

Aside from the issue in astsimplify introduced in 2cab4ff, all of the instances of UB are either in celledges.cc, or in fastlz.cc for unaligned loads/stores that we should probably add to the exclusion list.

[FSY369]

So, it's really a flaw in yosys isn't it?

[whitequark]

Yes, definitely, and a fairly important one in my opinion.