Skip to content

Latest commit

 

History

History
112 lines (107 loc) · 8.92 KB

BugList.md

File metadata and controls

112 lines (107 loc) · 8.92 KB
Raw

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. LIVM 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)

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)