From 041e16343a8e8a63ce7b383ff93e2db0ad489478 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 3 Oct 2024 10:15:37 +0200
Subject: [PATCH] [Eva] Adds tests for the emission of overflow alarms on
division and modulo.
---
tests/value/div.i | 54 +++++++++++++++-
tests/value/modulo.i | 43 +++++++++++++
tests/value/oracle/div.res.oracle | 93 +++++++++++++++++++++++++++-
tests/value/oracle/modulo.res.oracle | 63 +++++++++++++++----
4 files changed, 236 insertions(+), 17 deletions(-)
diff --git a/tests/value/div.i b/tests/value/div.i
index a57ddb2084..74d9eb4233 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -2,13 +2,13 @@
STDOPT: #""
*/
-
+volatile int nondet;
int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
int a,b,d1,d2,d0,e;
int t[5]={1,2,3};
int *p;
-void main (void) {
+void test (void) {
int i;
volatile int c=0;
while (c+1)
@@ -36,3 +36,53 @@ void main (void) {
d0 = 100 / (int)(&X);
e = - (int) &X;
}
+
+/* Tests the emission of overflow alarms on a division x/y only if [x] may be
+ equal to MIN_INT and [y] may be equal to -1. Also tests the reduction of the
+ possible values of [x] or [y] when possible. Similar test in file modulo.i. */
+void test_overflow_alarms (void) {
+ int min_int = -2147483648;
+ int min_one = -1;
+ int a = nondet ? min_int : 10;
+ int b = nondet ? -1 : 2;
+ int x = nondet;
+ int y = nondet;
+ int r = 0;
+ if (nondet) {
+ r = a / b; // Overflow alarm.
+ // No reduction as [a] and [b] cannot be reduced simultaneously.
+ Frama_C_show_each(a, b);
+ }
+ if (nondet) {
+ r = a / min_one; // Overflow alarm.
+ r = a / min_one; // No alarm if [a] has been reduced.
+ Frama_C_show_each_ten(a); // Check the reduction of [a].
+ }
+ if (nondet) {
+ r = min_int / b; // Overflow alarm.
+ r = min_int / b; // No alarm if [b] has been reduced.
+ Frama_C_show_each_two(b); // Check the reduction of [b]
+ }
+ if (nondet) {
+ r = x / min_one; // Overflow alarm.
+ r = x / min_one; // No alarm if [x] has been reduced.
+ Frama_C_show_each(x); // All integers except MIN_INT.
+ }
+ if (nondet) {
+ r = min_int / x; // Overflow alarm and division by zero alarm.
+ // All integers except -1 and 0, but not representable as an interval.
+ Frama_C_show_each(x);
+ }
+ if (nondet) {
+ r = min_int / min_one; // Invalid alarm.
+ Frama_C_show_each_BOTTOM(min_int, min_one);
+ }
+ // Overflow alarm and division by zero alarm,
+ // no possible reduction: [x] and [y] must be top_int as the end.
+ r = x / y;
+}
+
+void main (void) {
+ test();
+ test_overflow_alarms();
+}
diff --git a/tests/value/modulo.i b/tests/value/modulo.i
index dc7bc118ff..37fa7c2eff 100644
--- a/tests/value/modulo.i
+++ b/tests/value/modulo.i
@@ -161,6 +161,48 @@ void address_modulo(void) {
r = uaddr % i;
}
+/* Tests the emission of overflow alarms on operation x%y only if [x] may be
+ equal to MIN_INT and [y] may be equal to -1. Also tests the reduction of the
+ possible values of [x] or [y] when possible. Similar test in file div.i. */
+void test_overflow_alarms (void) {
+ int min_int = -2147483648;
+ int min_one = -1;
+ int a = v ? min_int : 10;
+ int b = v ? -1 : 2;
+ int x = v;
+ int y = v;
+ int r = 0;
+ if (v) {
+ r = a % b; // Overflow alarm.
+ // No reduction as [a] and [b] cannot be reduced simultaneously.
+ Frama_C_show_each(a, b);
+ }
+ if (v) {
+ r = a % min_one; // Overflow alarm.
+ r = a % min_one; // No alarm if [a] has been reduced.
+ Frama_C_show_each_ten(a); // Check the reduction of [a].
+ }
+ if (v) {
+ r = min_int % b; // Overflow alarm.
+ r = min_int % b; // No alarm if [b] has been reduced.
+ Frama_C_show_each_two(b); // Check the reduction of [b]
+ }
+ if (v) {
+ r = x % min_one; // Overflow alarm.
+ r = x % min_one; // No alarm if [x] has been reduced.
+ Frama_C_show_each(x); // All integers except MIN_INT.
+ }
+ if (v) {
+ r = min_int % x; // Overflow alarm and division by zero alarm.
+ // All integers except -1 and 0, but not representable as an interval.
+ Frama_C_show_each(x);
+ }
+ if (v) {
+ r = min_int % min_one; // Invalid alarm.
+ Frama_C_show_each_BOTTOM(min_int, min_one);
+ }
+}
+
void main() {
if (v) { pgcd1(a, b); }
if (v) { pgcd2(a, b); }
@@ -172,4 +214,5 @@ void main() {
extract_bits_modulo();
pos_rem();
address_modulo();
+ test_overflow_alarms();
}
diff --git a/tests/value/oracle/div.res.oracle b/tests/value/oracle/div.res.oracle
index bf467409f1..4b8b6e318c 100644
--- a/tests/value/oracle/div.res.oracle
+++ b/tests/value/oracle/div.res.oracle
@@ -3,6 +3,7 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
X ∈ {0}
Y ∈ {0}
Z1 ∈ {0}
@@ -24,6 +25,8 @@
[2] ∈ {3}
[3..4] ∈ {0}
p ∈ {0}
+[eva] computing for function test <- main.
+ Called from div.i:86.
[eva:alarm] div.i:14: Warning: signed overflow. assert c + 1 ≤ 2147483647;
[eva:alarm] div.i:17: Warning: signed overflow. assert c + 2 ≤ 2147483647;
[eva] div.i:14: starting to merge loop iterations
@@ -58,11 +61,37 @@
signed overflow. assert -((int)(&X)) ≤ 2147483647;
[eva:garbled-mix:write] div.i:37:
Assigning imprecise value to e because of arithmetic operation on addresses.
+[eva] Recording results for test
+[eva] Done for function test
+[eva] computing for function test_overflow_alarms <- main.
+ Called from div.i:87.
+[eva:alarm] div.i:52: Warning: signed overflow. assert a_0 / b_0 ≤ 2147483647;
+[eva] div.i:54: Frama_C_show_each: {-2147483648; 10}, {-1; 2}
+[eva:alarm] div.i:57: Warning:
+ signed overflow. assert a_0 / min_one ≤ 2147483647;
+[eva] div.i:59: Frama_C_show_each_ten: {10}
+[eva:alarm] div.i:62: Warning:
+ signed overflow. assert min_int / b_0 ≤ 2147483647;
+[eva] div.i:64: Frama_C_show_each_two: {2}
+[eva:alarm] div.i:67: Warning:
+ signed overflow. assert x / min_one ≤ 2147483647;
+[eva] div.i:69: Frama_C_show_each: [-2147483647..2147483647]
+[eva:alarm] div.i:72: Warning: division by zero. assert x ≢ 0;
+[eva:alarm] div.i:72: Warning:
+ signed overflow. assert min_int / x ≤ 2147483647;
+[eva] div.i:74: Frama_C_show_each: [-2147483648..2147483647]
+[eva:alarm] div.i:77: Warning:
+ signed overflow. assert min_int / min_one ≤ 2147483647;
+[eva:alarm] div.i:82: Warning: division by zero. assert y ≢ 0;
+[eva:alarm] div.i:82: Warning: signed overflow. assert x / y ≤ 2147483647;
+[eva] Recording results for test_overflow_alarms
+[eva] Done for function test_overflow_alarms
[eva] Recording results for main
[eva] Done for function main
+[eva] div.i:77: assertion 'Eva,signed_overflow' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
+[eva:final-states] Values at end of function test:
X ∈ [--..--]
Y ∈ [-126..333],9%27
Z1 ∈ [-42..111],3%9
@@ -81,10 +110,60 @@
e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
p ∈ {{ &t[3] }}
c ∈ [--..--]
+[eva:final-states] Values at end of function test_overflow_alarms:
+ min_int ∈ {-2147483648}
+ min_one ∈ {-1}
+ a_0 ∈ {-2147483648; 10}
+ b_0 ∈ {-1; 2}
+ x ∈ [--..--]
+ y ∈ [--..--]
+ r ∈ [--..--]
+[eva:final-states] Values at end of function main:
+ X ∈ [--..--]
+ Y ∈ [-126..333],9%27
+ Z1 ∈ [-42..111],3%9
+ Z2 ∈ [-25..66]
+ T ∈ [34..493],7%27
+ U1 ∈ [11..164],2%9
+ U2 ∈ [6..98]
+ V ∈ [-125..334],10%27
+ W1 ∈ [-41..111]
+ W2 ∈ [-25..66]
+ a ∈ [-40000..40000]
+ b ∈ {{ garbled mix of &{Z2} (origin: Arithmetic {div.i:33}) }}
+ d1 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:35}) }}
+ d2 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:34}) }}
+ d0 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:36}) }}
+ e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
+ p ∈ {{ &t[3] }}
+[from] Computing for function test
+[from] Done for function test
+[from] Computing for function test_overflow_alarms
+[from] Done for function test_overflow_alarms
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function test:
+ X FROM X (and SELF)
+ Y FROM X
+ Z1 FROM X
+ Z2 FROM X
+ T FROM X
+ U1 FROM X
+ U2 FROM X
+ V FROM X
+ W1 FROM X
+ W2 FROM X
+ a FROM X
+ b FROM X
+ d1 FROM \nothing
+ d2 FROM \nothing
+ d0 FROM \nothing
+ e FROM \nothing
+ p FROM \nothing
+[from] Function test_overflow_alarms:
+ NO EFFECTS
[from] Function main:
X FROM X (and SELF)
Y FROM X
@@ -104,7 +183,15 @@
e FROM \nothing
p FROM \nothing
[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main:
+[inout] Out (internal) for function test:
X; Y; Z1; Z2; T; U1; U2; V; W1; W2; a; b; d1; d2; d0; e; p; c
-[inout] Inputs for function main:
+[inout] Inputs for function test:
X; Y; Z2; T; V
+[inout] Out (internal) for function test_overflow_alarms:
+ min_int; min_one; a_0; tmp; b_0; tmp_0; x; y; r
+[inout] Inputs for function test_overflow_alarms:
+ nondet
+[inout] Out (internal) for function main:
+ X; Y; Z1; Z2; T; U1; U2; V; W1; W2; a; b; d1; d2; d0; e; p
+[inout] Inputs for function main:
+ nondet; X; Y; Z2; T; V
diff --git a/tests/value/oracle/modulo.res.oracle b/tests/value/oracle/modulo.res.oracle
index 6159974336..bd53257d35 100644
--- a/tests/value/oracle/modulo.res.oracle
+++ b/tests/value/oracle/modulo.res.oracle
@@ -26,8 +26,8 @@
b ∈ [--..--]
i2 ∈ [--..--]
[eva] computing for function pgcd1 <- main.
- Called from modulo.i:165.
-[eva:alarm] modulo.i:165: Warning:
+ Called from modulo.i:207.
+[eva:alarm] modulo.i:207: Warning:
function pgcd1: precondition got status unknown.
[eva] modulo.i:37: loop invariant got status valid.
[eva] modulo.i:38: loop invariant got status valid.
@@ -40,8 +40,8 @@
[eva] Recording results for pgcd1
[eva] Done for function pgcd1
[eva] computing for function pgcd2 <- main.
- Called from modulo.i:166.
-[eva:alarm] modulo.i:166: Warning:
+ Called from modulo.i:208.
+[eva:alarm] modulo.i:208: Warning:
function pgcd2: precondition got status unknown.
[eva] modulo.i:50: loop invariant got status valid.
[eva] modulo.i:53: Frama_C_show_each_2: [-10..10], [1..10], [-9..9]
@@ -49,15 +49,15 @@
[eva] Recording results for pgcd2
[eva] Done for function pgcd2
[eva] computing for function pgcd3 <- main.
- Called from modulo.i:167.
-[eva:alarm] modulo.i:167: Warning:
+ Called from modulo.i:209.
+[eva:alarm] modulo.i:209: Warning:
function pgcd3: precondition got status unknown.
[eva:alarm] modulo.i:63: Warning: division by zero. assert b_0 ≢ 0;
[eva] modulo.i:64: Frama_C_show_each_3: [-10..10], [-10..10], [-9..9]
[eva] Recording results for pgcd3
[eva] Done for function pgcd3
[eva] computing for function main2 <- main.
- Called from modulo.i:169.
+ Called from modulo.i:211.
[eva:alarm] modulo.i:9: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
[eva:alarm] modulo.i:9: Warning: signed overflow. assert 4 * i ≤ 2147483647;
[eva:alarm] modulo.i:10: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
@@ -69,12 +69,12 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function simultaneous_congruences <- main.
- Called from modulo.i:170.
+ Called from modulo.i:212.
[eva:alarm] modulo.i:76: Warning: assertion got status unknown.
[eva] Recording results for simultaneous_congruences
[eva] Done for function simultaneous_congruences
[eva] computing for function shift_modulo <- main.
- Called from modulo.i:171.
+ Called from modulo.i:213.
[eva:alarm] modulo.i:100: Warning: assertion got status unknown.
[eva:alarm] modulo.i:103: Warning:
signed overflow. assert (int)((int)(i * 12) + 5) << 25 ≤ 2147483647;
@@ -83,19 +83,19 @@
[eva] Recording results for shift_modulo
[eva] Done for function shift_modulo
[eva] computing for function extract_bits_modulo <- main.
- Called from modulo.i:172.
+ Called from modulo.i:214.
[eva:alarm] modulo.i:109: Warning: assertion got status unknown.
[eva] Recording results for extract_bits_modulo
[eva] Done for function extract_bits_modulo
[eva] computing for function pos_rem <- main.
- Called from modulo.i:173.
+ Called from modulo.i:215.
[eva:alarm] modulo.i:137: Warning: assertion got status unknown.
[eva:alarm] modulo.i:142: Warning: assertion got status unknown.
[eva:alarm] modulo.i:146: Warning: assertion got status unknown.
[eva] Recording results for pos_rem
[eva] Done for function pos_rem
[eva] computing for function address_modulo <- main.
- Called from modulo.i:174.
+ Called from modulo.i:216.
[eva:garbled-mix:write] modulo.i:158:
Assigning imprecise value to r because of arithmetic operation on addresses.
[eva:alarm] modulo.i:159: Warning: division by zero. assert i ≢ 0;
@@ -111,8 +111,31 @@
Assigning imprecise value to r because of arithmetic operation on addresses.
[eva] Recording results for address_modulo
[eva] Done for function address_modulo
+[eva] computing for function test_overflow_alarms <- main.
+ Called from modulo.i:217.
+[eva:alarm] modulo.i:176: Warning:
+ signed overflow. assert a_0 / b_0 ≤ 2147483647;
+[eva] modulo.i:178: Frama_C_show_each: {-2147483648; 10}, {-1; 2}
+[eva:alarm] modulo.i:181: Warning:
+ signed overflow. assert a_0 / min_one ≤ 2147483647;
+[eva] modulo.i:183: Frama_C_show_each_ten: {10}
+[eva:alarm] modulo.i:186: Warning:
+ signed overflow. assert min_int / b_0 ≤ 2147483647;
+[eva] modulo.i:188: Frama_C_show_each_two: {2}
+[eva:alarm] modulo.i:191: Warning:
+ signed overflow. assert x / min_one ≤ 2147483647;
+[eva] modulo.i:193: Frama_C_show_each: [-2147483647..2147483647]
+[eva:alarm] modulo.i:196: Warning: division by zero. assert x ≢ 0;
+[eva:alarm] modulo.i:196: Warning:
+ signed overflow. assert min_int / x ≤ 2147483647;
+[eva] modulo.i:198: Frama_C_show_each: [-2147483648..2147483647]
+[eva:alarm] modulo.i:201: Warning:
+ signed overflow. assert min_int / min_one ≤ 2147483647;
+[eva] Recording results for test_overflow_alarms
+[eva] Done for function test_overflow_alarms
[eva] Recording results for main
[eva] Done for function main
+[eva] modulo.i:201: assertion 'Eva,signed_overflow' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function address_modulo:
@@ -187,6 +210,14 @@
o1 ∈ [11..268435451],11%24
o2 ∈ [11..268435451],11%24
o3 ∈ [11..268435451],11%24
+[eva:final-states] Values at end of function test_overflow_alarms:
+ min_int ∈ {-2147483648}
+ min_one ∈ {-1}
+ a_0 ∈ {-2147483648; 10}
+ b_0 ∈ {-1; 2}
+ x ∈ [--..--]
+ y ∈ [--..--]
+ r ∈ [-2147483647..0]
[eva:final-states] Values at end of function main:
A ∈ {0}
B ∈ {-3; 1}
@@ -223,6 +254,8 @@
[from] Done for function shift_modulo
[from] Computing for function simultaneous_congruences
[from] Done for function simultaneous_congruences
+[from] Computing for function test_overflow_alarms
+[from] Done for function test_overflow_alarms
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -261,6 +294,8 @@
NO EFFECTS
[from] Function simultaneous_congruences:
NO EFFECTS
+[from] Function test_overflow_alarms:
+ NO EFFECTS
[from] Function main:
A FROM v
B FROM v
@@ -317,6 +352,10 @@
n1; n2; n3; m1; m2; o1; o2; o3
[inout] Inputs for function simultaneous_congruences:
i2
+[inout] Out (internal) for function test_overflow_alarms:
+ min_int; min_one; a_0; tmp; b_0; tmp_0; x; y; r
+[inout] Inputs for function test_overflow_alarms:
+ v
[inout] Out (internal) for function main:
A; B; C; D; E; F; G; H; I; J; K; L; M; N; O; P; Q
[inout] Inputs for function main:
--
GitLab