Skip to content

Commit

Permalink
sync BugList with Alive2
Browse files Browse the repository at this point in the history
  • Loading branch information
spica authored and spica committed Nov 8, 2023
1 parent ed3f224 commit d27abfb
Showing 1 changed file with 0 additions and 20 deletions.
20 changes: 0 additions & 20 deletions BugList.md
Original file line number Diff line number Diff line change
Expand Up @@ -107,25 +107,5 @@ Please contact us or submit a PR if something is missing or inaccurate.
15. Incorrect sort after lambda rewrite (https://github.com/Z3Prover/z3/issues/6340)
16. Incorrect BV rewrite (https://github.com/Z3Prover/z3/issues/6426)
17. Crash with FP<->BV conversions (https://github.com/Z3Prover/z3/issues/6460)
<<<<<<< HEAD
18. Integer overflow (https://github.com/Z3Prover/z3/commit/a96f5a9b425b6f5ba7e8ce1c1a75db6683c4bdc9)
19. Memory leak with arrays on timeout (https://github.com/Z3Prover/z3/commit/dda0c8ff4200faa6a441855716b47ec7f93e026e)
=======


### Mutation bugs
This section is outdated. All bugs are maintained at alive-mutateBuglist.md (under the same folder) instead

#### Confirmed bugs
1. InstCombine: 2 related logic bugs from over-generalizing "lshr" to "any shr" (https://llvm.org/PR51351)
2. Inbounds: might cause problem in signed GEP instruction (https://bugs.llvm.org/show_bug.cgi?id=52429)
3. NUW and NSW flag in InstSimplify (https://reviews.llvm.org/D116322)

#### Suspected bugs
1. This bug combines vectors, UB, and non-standard FP (https://alive2.llvm.org/ce/z/jwZ7uS)
2. LLVM bug. briefly, uitofp(undef) is more defined than undef, the transformation tries to replace uiofp(undef) with undef (in 2nd lane) (https://alive2.llvm.org/ce/z/CYafMt)
3. Alive2 Bug. bitcast should not change any bits (cite: langref), bitcast in Alive2 (from float to BV) doesn’t follow this rule. (https://alive2.llvm.org/ce/z/CYafMt )
4. LLVM bug. For the second lane, with the input from cexp, the source evaluates a result with two possible values (either 0x80000000 or 0x00010000, depends on what the undef in %t2 freezes to); the tgt is undef free but it evaluates to a whole different value 0x00000000. (https://alive2.llvm.org/ce/z/_RDXK-)
5. Alive2 Bug. Alive2 should limit the parapmeter used in malloc. (https://alive2.llvm.org/ce/z/rEGMoF)
6. Alive2 Bug. Alive2 is not handing nsz correct for fcmp (https://alive2.llvm.org/ce/z/RWA-EG)
>>>>>>> Mutation bugs section added

0 comments on commit d27abfb

Please sign in to comment.