Carl Friedrich Bolz-Tereick pushed to branch branch/default at PyPy / pypy
Commits:
cba4ba4f by Carl Friedrich Bolz-Tereick at 2022-10-15T14:28:30+02:00
(cfbolz, NiRit100 around): #3832 be more careful in handling bound
addition/subtraction in the presence of overflows
--HG--
branch : fix-intutils-ovf-bug
- - - - -
350a1e9c by Carl Friedrich Bolz-Tereick at 2022-10-15T15:24:27+02:00
int_neg also has a bug
also add some consistency checks between the methods
--HG--
branch : fix-intutils-ovf-bug
- - - - -
ca0788f3 by Carl Friedrich Bolz-Tereick at 2022-10-15T19:02:42+02:00
get rid of has_upper and has_lower completely
Their meaning was basically never super obvious, and you need to be careful to
understand it correctly everywhere. Instead, we now have:
- methods that check whether overflow is known to not occur for certain
operations (add/sub/.._bound_cannot_overflow)
- the default add/sub/mul/..._bound methods will return result bounds that are
correct whether overflow happens or not.
- for int_add_ovf/guard_no_overflow there is another new method on the bounds,
add_bound_no_overflow that returns the tighter range that applies if we know
from the guard that overflow has not occurred.
--HG--
branch : fix-intutils-ovf-bug
- - - - -
92e91d51 by Carl Friedrich Bolz-Tereick at 2022-10-15T19:41:08+02:00
another incorrect test, about int_neg:
the following implication is wrong in the presence of overflow:
-x <= 0 ⇒ x >= 0
with the (only) counterexample of x = MININT
the inverse one holds:
-x >= 0 ⇒ x <= 0
in practice, int_neg is mostly preceded by int_eq(x, MINIT), guard_false, so
make things work in that case
--HG--
branch : fix-intutils-ovf-bug
- - - - -
fe37c69e by Carl Friedrich Bolz-Tereick at 2022-10-15T22:04:30+02:00
add a new file with test_optimize*-style tests but specifically for those cases
that relate to intbounds (the other ones are getting way too huge)
--HG--
branch : fix-intutils-ovf-bug
- - - - -
e6e6 by Carl Friedrich Bolz-Tereick at 2022-10-17T13:37:01+02:00
add some somewhat experimental code that uses the Z3 SMT solver to check that
the optimizer produces a valid output. only works for a small amount of integer
operations so far
--HG--
branch : fix-intutils-ovf-bug
- - - - -
71a68c2b by Carl Friedrich Bolz-Tereick at 2022-10-17T20:36:49+02:00
put widening logic into one spot
--HG--
branch : fix-intutils-ovf-bug
- - - - -
be5ab5e7 by Carl Friedrich Bolz-Tereick at 2022-10-17T20:54:27+02:00
support of int_add_ovf, guard_no_overflow
--HG--
branch : fix-intutils-ovf-bug
- - - - -
b19b73e8 by Carl Friedrich Bolz-Tereick at 2022-10-17T22:48:05+02:00
move int tests into a file and support them in z3
--HG--
branch : fix-intutils-ovf-bug
- - - - -
b2a468a0 by Carl Friedrich Bolz-Tereick at 2022-10-18T10:32:42+02:00
support for signext
--HG--
branch : fix-intutils-ovf-bug
- - - - -
67010878 by Carl Friedrich Bolz-Tereick at 2022-10-18T10:39:38+02:00
test and fix: known_ge_const was unused, untested, and thus broken
--HG--
branch : fix-intutils-ovf-bug
- - - - -
cb49de15 by Carl Friedrich Bolz-Tereick at 2022-10-18T12:28:44+02:00
support for uint_mul_high
--HG--
branch : fix-intutils-ovf-bug
- - - - -
fdaa1225 by Carl Friedrich Bolz-Tereick at 2022-10-18T12:29:53+02:00
start randomly generating traces, optimizing them, and checking with z3
--HG--
branch : fix-intutils-ovf-bug
- - - - -
83b9b414 by Carl Friedrich Bolz-Tereick at 2022-10-18T13:05:13+02:00
ability to set a z3 timeout, plus print the rng state
--HG--
branch : fix-intutils-ovf-bug
- - - - -
4a7f7700 by Carl Friedrich Bolz-Tereick at 2022-10-18T13:34:39+02:00
fix propagate_bounds_INT_MUL, which is not always valid, only if no overflow
occurs
--HG--
branch : fix-intutils-ovf-bug
- - - - -
0a06a2f0 by Carl Friedrich Bolz-Tereick at 2022-10-18T13:54:20+02:00
equivalent bug for lshift
--HG--
branch : fix-intutils-ovf-bug
- - - - -
4627ff02 by Carl Friedrich Bolz-Tereick at 2022-10-18T22:09:29+02:00
test and fix: wrong api usage in int_add chaining logic
--HG--
branch : fix-intutils-ovf-bug
- - - - -
2440591f by Carl Friedrich Bolz-Tereick at 2022-10-18T22:09:42+02:00
comment out the pdb
--HG--
branch : fix-intutils-ovf-bug
- - - - -
aab30f47 by Carl Friedrich Bolz-Tereick at 2022-10-18T22:15:46+02:00
make it pass with z3
--HG--
branch : fix-intutils-ovf-bug
- - - - -
01a0f381 by Carl Friedrich Bolz-Tereick at 2022-10-19T11:58:00+02:00
start fixing the shift test mess
--HG--
branch : fix-intutils-ovf-bug
- - - - -
99bb8114 by Carl Friedrich Bolz-Tereick at 2022-10-19T12:16:46+02:00
some cleanups. the idea of checking the textual expected output cannot work
--HG--
branch : fix-intutils-ovf-bug
- - - - -
58402933 by Carl Friedrich Bolz-Tereick at 2022-10-19T22:11:06+02:00
print nicer debug output when stuff goes wrong
--HG--
branch : fix-intutils-ovf-bug
- - - - -
0cb67cdc by Carl Friedrich Bolz-Tereick at 2022-10-19T22:11:27+02:00
test and fix: we can't reuse results of non-ovfche
