08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
40 lines
1.4 KiB
Text
40 lines
1.4 KiB
Text
/-!
|
|
# Signed integer division overflow test
|
|
|
|
On x86_64, INT_MIN / -1 and INT_MIN % -1 cause a SIGFPE (floating point exception)
|
|
because the result overflows the destination register. This test verifies the fix.
|
|
|
|
The expected behavior (per BitVec.sdiv semantics): return minValue (wrapped result) for div,
|
|
and 0 for mod.
|
|
-/
|
|
|
|
-- Test that signed division handles overflow correctly
|
|
-- INT_MIN / -1 should return INT_MIN (wrapped)
|
|
|
|
#guard (Int8.minValue / -1 : Int8) == Int8.minValue
|
|
#guard (Int16.minValue / -1 : Int16) == Int16.minValue
|
|
#guard (Int32.minValue / -1 : Int32) == Int32.minValue
|
|
#guard (Int64.minValue / -1 : Int64) == Int64.minValue
|
|
#guard (ISize.minValue / -1 : ISize) == ISize.minValue
|
|
|
|
-- Test that signed mod handles overflow correctly
|
|
-- INT_MIN % -1 should return 0
|
|
|
|
#guard (Int8.minValue % -1 : Int8) == 0
|
|
#guard (Int16.minValue % -1 : Int16) == 0
|
|
#guard (Int32.minValue % -1 : Int32) == 0
|
|
#guard (Int64.minValue % -1 : Int64) == 0
|
|
#guard (ISize.minValue % -1 : ISize) == 0
|
|
|
|
-- Also test via #eval to exercise the C runtime
|
|
#eval (Int8.minValue / -1 : Int8)
|
|
#eval (Int16.minValue / -1 : Int16)
|
|
#eval (Int32.minValue / -1 : Int32)
|
|
#eval (Int64.minValue / -1 : Int64)
|
|
#eval (ISize.minValue / -1 : ISize)
|
|
|
|
#eval (Int8.minValue % -1 : Int8)
|
|
#eval (Int16.minValue % -1 : Int16)
|
|
#eval (Int32.minValue % -1 : Int32)
|
|
#eval (Int64.minValue % -1 : Int64)
|
|
#eval (ISize.minValue % -1 : ISize)
|