google / xls

XLS: Accelerated HW Synthesis
http://google.github.io/xls/
Apache License 2.0
1.2k stars 177 forks source link

Invalid narrowing optimization, fuzzer crasher d9e2 #1184

Closed meheff closed 11 months ago

meheff commented 11 months ago

Found by the fuzzer. Minimized IR:

package sample

top fn __sample__main(x0: bits[36], x1: bits[4], x2: bits[57]) -> bits[1] {
  bit_slice.624: bits[1] = bit_slice(x2, start=0, width=1, id=624)
  zero_ext.606: bits[2] = zero_ext(bit_slice.624, new_bit_count=2, id=606)
  one_hot.141: bits[3] = one_hot(zero_ext.606, lsb_prio=true, id=141)
  literal.134: bits[27] = literal(value=134217727, id=134, pos=[(0,43,59)])
  literal.519: bits[27] = literal(value=0, id=519, pos=[(0,44,27)])
  literal.139: bits[27] = literal(value=99846409, id=139, pos=[(0,45,21)])
  x4: bits[27] = one_hot_sel(one_hot.141, cases=[literal.134, literal.519, literal.139], id=142)
  literal.158: bits[27] = literal(value=127305941, id=158, pos=[(0,52,16)])
  ret sge.160: bits[1] = sge(x4, literal.158, id=160, pos=[(0,52,16)])
}

Repro:

$ xls/tools/eval_ir_main --eval_after_each_pass --input="bits[36]:0xa_aaaa_aaaa;bits[4]:0xa;bits[57]:0x8000_0000_0000" minimized.ir --optimize_ir
...
// Evaluating entry function after pass: narrow
bits[1]:0x1
Error: INVALID_ARGUMENT: Miscompare for input[0] "bits[36]:0xa_aaaa_aaaa; bits[4]:0xa; bits[57]:0x8000_0000_0000"
  narrow: bits[1]:0x1
  before optimizations: bits[1]:0x0; [after 'Narrowing' pass, dynamic pass #309]
=== Source Location Trace: ===
xls/passes/pass_base.h:289
ericastor commented 11 months ago

Simplified a bit further, after cutting down params, taking the IR right before the actual invalid optimization, and then encouraging the minimizer to simplify the concat a bit with a bit of manual help... plus removing unneeded pos info and renumbering.

package sample

top fn __sample__main(x0: bits[2]) -> bits[1] {
  literal.1: bits[1] = literal(value=1, id=1)
  bit_slice.2: bits[1] = bit_slice(x0, start=0, width=1, id=2)
  literal.3: bits[25] = literal(value=32508169, id=3)
  concat.4: bits[27] = concat(literal.1, bit_slice.2, literal.3, id=4)
  literal.5: bits[27] = literal(value=127305941, id=5)
  ret sge.6: bits[1] = sge(concat.4, literal.5, id=6)
}
ericastor commented 11 months ago

I've confirmed this was introduced in https://github.com/google/xls/commit/85249d232e5a93998d2de616eedd1c1d325b03b5

grebe commented 11 months ago

I understand the problem and have a fix incoming.

To summarize, signed comparisons with operands of the form 0XXXX can unconditionally be narrowed to unsigned comparisons with the MSB trimmed, but if the operands are of the form 1XXXX you can't. 10XXXX can be, though (flipping the order of the comparison). I'm adding a check that the next-most MSB is known 0.

grebe commented 11 months ago

This explanation was wrong, the real problem is that I shouldn't flip the operands. I mistakenly thought that dropping the MSB flipped the sign like multiplying by -1, but it's really just adding a fixed offset to both sides when you drop the MSB. This fixed offset doesn't change the direction of the comparison. The correct behavior is to drop MSBs in common and switch to unsigned comparisons. It's actually a lot simpler!