Skip to content

Latest commit

 

History

History
172 lines (166 loc) · 14.7 KB

BugList.md

File metadata and controls

172 lines (166 loc) · 14.7 KB

Bugs Found by Alive2

This document lists the bugs found so far by Alive2 in LLVM & Z3. Please contact us or submit a PR if something is missing or inaccurate.

Bugs found in LLVM

  1. Incorrect fold of 'x & (-1 >> y) s>= x' (https://llvm.org/PR39861)
  2. Incorrect instcombine fold for icmp sgt (https://llvm.org/PR42198)
  3. Instsimplify: uadd_overflow(X, undef) is not undef (https://llvm.org/PR42209)
  4. CVP: adding nuw flags not correct in the presence of undef (https://llvm.org/PR42618)
  5. DivRemPairs is incorrect in the presence of undef (https://llvm.org/PR42619)
  6. EmitGEPOffset() incorrectly adds NUW to multiplications (https://llvm.org/PR42699)
  7. Incorrect fold of uadd.with.overflow with undef (https://llvm.org/PR43188)
  8. Incorrect transformation of bitcast->gep inbounds (https://llvm.org/PR43501)
  9. globalopt leaves store to a constant global (https://llvm.org/PR43616)
  10. Incorrect fold of ashr+xor -> lshr w/ vectors (https://llvm.org/PR43665)
  11. Incorrect 'icmp sle' -> 'icmp slt' w/ vectors (https://llvm.org/PR43730)
  12. expandmemcmp generates loads with incorrect alignment (https://llvm.org/PR43880)
  13. Shuffle undef mask on vectors with poison elements (https://llvm.org/PR43958)
  14. Can't remove shufflevector if input might be poison (https://llvm.org/PR44185)
  15. Incorrect instcombine transform: urem -> icmp+zext with vectors (https://llvm.org/PR44186)
  16. InstCombine incorrectly shrinks the size of store (https://llvm.org/PR44306)
  17. InstCombine incorrectly folds 'gep(bitcast ptr), idx' into 'gep ptr, idx' (https://llvm.org/PR44321)
  18. Instcombine: incorrect transformation 'x > (x & undef)' -> 'x > undef' (https://llvm.org/PR44383)
  19. memcpyopt adds incorrect align to memset (https://llvm.org/PR44388)
  20. Folding 'gep p, (q - p)' to q should check it is never used for loads & stores (https://llvm.org/PR44403)
  21. StraightLineStrengthReduce can introduce UB when optimizing 2-dim array gep (https://llvm.org/PR44533)
  22. SLPVectorizer should drop nsw flags from add (https://llvm.org/PR44536)
  23. InstCombine doesn't propagate correct alignment (https://llvm.org/PR44543)
  24. DSE not checking decl of libcalls (https://github.com/llvm/llvm-project/commit/87407fc03c82d880cc42330a8e230e7a48174e3c & https://github.com/llvm/llvm-project/commit/7f903873b8a937acec2e2cc232e70cba53061352)
  25. InstCombine incorrectly rewrites indices of gep inbounds (https://llvm.org/PR44861)
  26. InstCombine incorrectly transforms store i64 -> store double (https://llvm.org/PR45152)
  27. Incorrect optimization of gep without inbounds + load -> icmp eq (https://llvm.org/PR45210)
  28. gep(ptr, undef) isn't undef (https://llvm.org/PR45445)
  29. Incorrect transformation: (undef u>> a) ^ -1 -> undef >> a, when a != 0 (https://llvm.org/PR45447)
  30. Invalid undef splat in instcombine (https://llvm.org/PR45455)
  31. Incorrect transformation of minnum with nnan (https://llvm.org/PR45478)
  32. Can't remove insertelement undef (https://llvm.org/PR45481)
  33. InstSimplify: fadd (nsz op), +0 incorrectly removed (https://llvm.org/PR45778)
  34. Incorrect instcombine fold of control-flow to umul.with.overflow (https://llvm.org/PR45952)
  35. Incorrect instcombine fold of vector ult -> sgt (https://llvm.org/PR45954)
  36. Jumpthreading introduces jump on poison (https://llvm.org/PR45956)
  37. X86InterleavedAccess introduces misaligned loads (https://llvm.org/PR45957)
  38. load-store-vectorizer vectorizes non consecutive loads (https://llvm.org/PR46591)
  39. Incorrect transformation: mul foo, undef -> shl foo, undef (https://llvm.org/PR47133)
  40. Incorrect transformation: (llvm.maximum undef, %x) -> undef (https://llvm.org/PR47567)
  41. LoopReroll incorrectly reorders stores across loads when they may alias (https://llvm.org/PR47658)
  42. InstCombine: incorrect select operand simplification with undef (https://llvm.org/PR47696)
  43. MemCpyOpt: uses sext instead of zext for memcpy/memset size subtraction (https://llvm.org/PR47697)
  44. SCEVExpander introduces branch on poison (https://llvm.org/PR47769)
  45. Incorrect transformation of fabs with nnan flag (https://llvm.org/PR47960)
  46. Loop peeling introduces OOB stores (https://llvm.org/PR48125)
  47. Loop vectorizer introduces gep inbounds with negative offset (https://llvm.org/PR48126)
  48. DSE incorrectly removes store in function that only triggers UB in one of the branches (https://llvm.org/PR48521)
  49. Incorrect swap of fptrunc with fast-math instructions (https://llvm.org/PR49080)
  50. Incorrect propagation of nsz from fneg to fdiv (https://llvm.org/PR49654)
  51. Incorrect offset calculation when adding align to load from assume (https://reviews.llvm.org/D98759)
  52. InstSimplify: incorrect fold of pointer comparison between globals (https://llvm.org/PR50208)
  53. ConstraintElimination: incorrect fold of pointer comparison (https://llvm.org/PR50280)
  54. InstCombine: incorrect select fast-math folds (https://llvm.org/PR50281)
  55. LoopIdiomRecognize: Overflow in ctlz shifting loop (https://llvm.org/PR51669)
  56. LoopUnroll: runtime check introduces branch on poison if fn call doesn't return (https://llvm.org/PR51670)
  57. MergeICmps reorders comparisons and introduces UB (https://llvm.org/PR51845)
  58. Sink: moves calls that may not return (https://llvm.org/PR51846)
  59. LLVM introduces load in writeonly function (https://llvm.org/PR51906)
  60. InstSimplify incorrectly folds signed comparisons of 'gep inbounds' (https://llvm.org/PR52429)
  61. LoadStoreVectorizer assumes non-willreturn calls always return (https://llvm.org/PR52950)
  62. SROA sub-vector memcpy w/subsequent load loses the store (https://llvm.org/PR52971)
  63. NewGVN miscompiles with equal instructions modulo attributes (https://llvm.org/PR53218)
  64. InstCombine miscompiles combination of signed comparisons (https://llvm.org/PR53252)
  65. InstCombine propagates nsz flag from select to fneg incorrectly (https://llvm.org/PR54077)
  66. SLPVectorizer replaces add nsw undef with add poison (https://llvm.org/PR55653)
  67. InstCombine swaps inbounds geps originating OOB pointer (https://llvm.org/PR55722)
  68. SLP vectorizer's reduce_and formation introduces poison (https://llvm.org/PR55734)
  69. IRCE introduces UB by changing order of condition checks (https://llvm.org/PR57523)
  70. LoopIdiomRecognizer creates memset_pattern16 with incorrect size type with custom dl (https://llvm.org/PR57679)
  71. InstSimplify: xor pattern miscompiles undef lane (https://llvm.org/PR58977)
  72. llvm.canonicalize() folding incorrect for denormals (https://llvm.org/PR59245)
  73. InstCombine: incorrect fabs formation (https://llvm.org/PR59279)
  74. InstCombine: incorrect select + fast-math swap (https://llvm.org/PR59451)
  75. SCEV expander introduces poison when hoisting IV (https://llvm.org/PR59777)
  76. InstCombine: incorrect overflow check simplification (https://llvm.org/PR59836)
  77. Loop reroll creates incorrect IV increment (https://llvm.org/PR59841)
  78. InstCombine: incorrect transformation of smul_overflow with i1 (https://llvm.org/PR59876)
  79. CVP: incorrect transformation of abs (https://llvm.org/PR59887)
  80. InstCombine generates incorrect range metadata for ctpop (https://llvm.org/PR59888)
  81. InstCombine introduces UB when moving rem instructions (https://llvm.org/PR60906)
  82. SimpleLoopUnswitch reverses branch condition incorrectly (https://llvm.org/PR63962)
  83. Vectorization of loop reduction introduces an aligned store incorrectly (https://llvm.org/PR65212)
  84. InstCombine: incorrect sink of FP math through select changes NaN payload (https://llvm.org/PR74297)
  85. InstCombine: fold of shuffle into fadd changes NaN payload (https://llvm.org/PR74326)
  86. Attributor & Function-attrs mark function as noundef incorrectly due to return value not in range (https://llvm.org/PR88026)
  87. InstCombine: incorrect vector fshr->shl transformation (https://llvm.org/PR89338)
  88. VectorCombine: shufflevector reorder leads to srem by poison (https://llvm.org/PR89390)
  89. InstCombine: incorrect srem rewrite (https://llvm.org/PR89516)
  90. InstCombine: incorrect swap of select vector operands (https://llvm.org/PR89669)
  91. SimplifyCFG: coalesced store retains the wrong alignment (https://llvm.org/PR89672)
  92. LoopVectorize introduces division by zero (https://llvm.org/PR89958)
  93. InstCombine: align attribute doesn't dereferenceability (https://llvm.org/PR90446)
  94. Reassociate: invalid propagation of overflow attributes at low bit-width (https://llvm.org/PR91417)
  95. InstCombine: removes a select, making the code more poisonous (https://llvm.org/PR91691)
  96. DSE removes store before free() incorrectly (https://llvm.org/PR97956)
  97. GlobalOpt breaks !callees metadata (https://llvm.org/PR121265)

Bugs found in Z3

  1. Incorrect bitblast for fprem (Z3Prover/z3#2369)
  2. Bug in FPA w/ quantifiers (Z3Prover/z3#2596)
  3. Bug in FPA w/ quantifiers (Z3Prover/z3#2631)
  4. Crash in partial model mode (Z3Prover/z3#2652)
  5. Crash when printing multi-precision integer (Z3Prover/z3#2761)
  6. Bug with lambdas and quantified variables (Z3Prover/z3#2792)
  7. Bug in MBQI (Z3Prover/z3#2822)
  8. Bug with equality of arrays w/ lambdas (https://github.com/Z3Prover/z3/commit/0b14f1b6f6bb33b555bace93d644163987b0c54f)
  9. Crash in FPA model construction (Z3Prover/z3#2865)
  10. Crash in BV theory assertion (Z3Prover/z3#2878)
  11. Assertion violation in SMT equality propagation (Z3Prover/z3#2879)
  12. Assertion violation in qe_lite (https://github.com/Z3Prover/z3/commit/bb5edb7c653f9351fe674630d63cdd2b10338277)
  13. SMT internalize doesn't respect the timeout (Z3Prover/z3#4192)
  14. Unsoundness with smt.bv.size_reduce=true (Z3Prover/z3#6314)
  15. Incorrect sort after lambda rewrite (Z3Prover/z3#6340)
  16. Incorrect BV rewrite (Z3Prover/z3#6426)
  17. Crash with FP<->BV conversions (Z3Prover/z3#6460)
  18. Integer overflow (https://github.com/Z3Prover/z3/commit/a96f5a9b425b6f5ba7e8ce1c1a75db6683c4bdc9)
  19. Memory leak with arrays on timeout (https://github.com/Z3Prover/z3/commit/dda0c8ff4200faa6a441855716b47ec7f93e026e)
  20. Unsoundness in elim-uncnstr2 (Z3Prover/z3#6488)
  21. Unsoundness in elim-uncnstr2 (Z3Prover/z3#6506)
  22. Unsound NaN encoding (Z3Prover/z3#6972)
  23. fp.roundToIntegral gives invalid zero_extend application (Z3Prover/z3#7056)

Miscompilation bugs found in ARM64 Backend

  1. GlobalIsel miscompiles an llvm.fshl instruction (llvm/llvm-project#55003)
  2. GlobalIsel miscompiles a zero-extended logical shift right (llvm/llvm-project#55129)
  3. Incorrect optimization of sitofp/fptosi roundtrip (llvm/llvm-project#55150)
  4. Miscompilation on a shift followed by an icmp instruction (llvm/llvm-project#55178)
  5. Miscompilation when backend attempts to lower to a rotate instruction (llvm/llvm-project#55201)
  6. Miscompilation with urem and undef (llvm/llvm-project#55271)
  7. or followed by and miscompile with global isel on arm64 (llvm/llvm-project#55284)
  8. urem and udiv miscompile with global isel set on arm64 (llvm/llvm-project#55287)
  9. fshl-related miscompile by arm64 and x86-64 backends (llvm/llvm-project#55296)
  10. Miscompilation of arithmetic binops with constant params (llvm/llvm-project#55342)
  11. Miscompilation in multiple backends including arm64 and x86-64 (llvm/llvm-project#55484)
  12. Miscompilation involving arithmentic binops (llvm/llvm-project#55490)
  13. Miscompilation of non-canonical add+icmp (llvm/llvm-project#55627)
  14. Miscompilation of smul.with.overflow.i2 (llvm/llvm-project#55644)
  15. Funnel shift related miscompile by ARM64 backend with global isel (llvm/llvm-project#56664)
  16. Possible miscompile of signext-of-i1 by aarch64 backend (llvm/llvm-project#57181)
  17. GlobalIsel backend miscompiles funnel shift with undef amount (llvm/llvm-project#57256)
  18. Miscompile of code involving a usub.sat by AArch64 backend (llvm/llvm-project#58109)
  19. Miscompilation of a frozen poison by AArch64 backend (llvm/llvm-project#58321)
  20. AArch64 backend miscompile of some funnel shifts (llvm/llvm-project#59898)
  21. Miscompile by AArch64 backend related to smax.i64 (llvm/llvm-project#59902)
  22. miscompile from AArch64 global isel backend (llvm/llvm-project#61008)
  23. AArch64 miscompile of i1 arithmetic with global isel (llvm/llvm-project#72475)
  24. backends will turn OOB InsertElement into OOB store (llvm/llvm-project#74248)
  25. another OOB InsertElement -> OOB store (llvm/llvm-project#75557)
  26. likely miscompile of vector code by AArch64 backend (llvm/llvm-project#76769)
  27. srem-related vector miscompile on AArch64 (llvm/llvm-project#77169)
  28. AArch64 with global isel turns OOB extractelement into OOB load (llvm/llvm-project#78383)
  29. AArch64 with global isel miscompile (llvm/llvm-project#78477)
  30. miscompilation of trivial but non-canonical arithmetic by AArch64 backend (llvm/llvm-project#84718)
  31. AArch64 backend: extractelement with poison index leads to OOB memory load (llvm/llvm-project#88959)
  32. AArch64 backend incorrectly selecting uabdl (llvm/llvm-project#88784)
  33. AArch64 backend miscompilation related to sshl.sat (llvm/llvm-project#88950)
  34. incorrect coalescing of stores by AArch64 global isel backend (llvm/llvm-project#90242)
  35. scalar/integer miscompile from global isel for AArch64 (llvm/llvm-project#90245)
  36. miscompile of non-canonical IR by AArch64 global isel backend (llvm/llvm-project#90532)
  37. miscompile related to coalescing stores in AArch64 SDAG backend (llvm/llvm-project#90936)
  38. arithmetic miscompile from AArch64 backend (llvm/llvm-project#96366)
  39. vector miscompile from AArch64 backend (llvm/llvm-project#121372)
  40. vector miscompile from AArch64 backend (llvm/llvm-project#125989)