diff --git a/src/plugins/eva/ast/eva_ast_builder.ml b/src/plugins/eva/ast/eva_ast_builder.ml
index 1faa1e6f1dc9af1562e723b2e979439ee994ff4b..6b8f061985b4b973e1746bfe692491f51f4501be 100644
--- a/src/plugins/eva/ast/eva_ast_builder.ml
+++ b/src/plugins/eva/ast/eva_ast_builder.ml
@@ -202,6 +202,7 @@ struct
| _ -> invalid_arg "unsupported construction"
let add = binop PlusA
+ let div = binop Div
let eq = binop Eq
let ne = binop Ne
diff --git a/src/plugins/eva/ast/eva_ast_builder.mli b/src/plugins/eva/ast/eva_ast_builder.mli
index 7a7bdcdcdc614698b005d31bd49cca0ec52bc539..448da7c1e6af41fccbf4959492dc1a7605b235ea 100644
--- a/src/plugins/eva/ast/eva_ast_builder.mli
+++ b/src/plugins/eva/ast/eva_ast_builder.mli
@@ -73,6 +73,7 @@ sig
val cast: typ -> exp -> exp (* (typ)x *)
val add: exp -> exp -> exp (* x + y *)
+ val div: exp -> exp -> exp (* x / y *)
val eq: exp -> exp -> exp (* x == y *)
val ne: exp -> exp -> exp (* x != y *)
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index cbb95ced117ad297b74bf51bc738689398b55540..c6a940037fead7e93263663590fbceead7d3f2e3 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -541,15 +541,31 @@ module Make
let truth = Value.assume_bounded Alarms.Upper_bound size_int value in
reduce_by_truth ~alarm (index_expr, value) truth
- let assume_valid_binop typ (e1, v1 as arg1) op (e2, v2 as arg2) =
+ (* The behavior of a%b is undefined if the quotient a/b overflows
+ (according to 6.5.5,§6 in the C standard). This is checked here. *)
+ let assume_valid_mod context typ (e1, v1) (e2, v2) =
+ let expr = Eva_ast.Build.div e1 e2 in
+ let value = Value.forward_binop context typ Div v1 v2 in
+ let check_overflow value =
+ let open Evaluated.Operators in
+ (* Check overflow alarms, but the reduced value of a/b is useless here. *)
+ let+ _v = handle_overflow ~may_overflow:true context expr typ value in
+ (* We could probably reduce [v1] or [v2] in some cases. *)
+ v1, v2
+ in
+ Bottom.fold ~bottom:(return (v1, v2)) check_overflow value
+
+ let assume_valid_binop context typ (e1, v1 as arg1) op (e2, v2 as arg2) =
let open Evaluated.Operators in
if Cil.isIntegralType typ then
match op with
| Div | Mod ->
let truth = Value.assume_non_zero v2 in
let alarm () = Alarms.Division_by_zero (Eva_ast.to_cil_exp e2) in
- let+ v2 = reduce_by_truth ~alarm arg2 truth in
- v1, v2
+ let* v2 = reduce_by_truth ~alarm arg2 truth in
+ if op = Mod
+ then assume_valid_mod context typ (e1, v1) (e2, v2)
+ else return (v1, v2)
| Shiftrt ->
let warn_negative = Kernel.RightShiftNegative.get () in
reduce_shift ~warn_negative typ arg1 arg2
@@ -616,7 +632,7 @@ module Make
let e1 = if Eva_ast.is_zero_ptr e1 then None else Some e1 in
forward_comparison ~compute typ_e1 kind (e1, v1) arg2
| None ->
- let& v1, v2 = assume_valid_binop typ arg1 op arg2 in
+ let& v1, v2 = assume_valid_binop context typ arg1 op arg2 in
Value.forward_binop context typ_e1 op v1 v2
let forward_unop context unop (e, v as arg) =
diff --git a/tests/value/modulo.i b/tests/value/modulo.i
index e802427c601e40b1b4eeb7ef6856a121ecb1a95c..dc7bc118ff839f8957828e481a0aca454e188560 100644
--- a/tests/value/modulo.i
+++ b/tests/value/modulo.i
@@ -147,7 +147,9 @@ void pos_rem(void) {
int l = (int)*(signed char*)&n; // Best rem is ([0..72] \cup {255})%255, we approximate by [-128..127]
}
-/* No overflow alarms should be emitted on mod operations, even on addresses. */
+/* On modulo, overflow alarms should only be emitted on INT_MIN % -1, which
+ is not possible on addresses. However, garbled mixes on arithmetic operations
+ involving addresses currently lose all precision and lead to false alarms. */
void address_modulo(void) {
int* ptr = v ? &A : &B;
unsigned int uaddr = (unsigned int) ptr;
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index 394936b8b9df05a61b4935cb721c0e66380efa36..8e49b33bc5d9199023561d3a7cf7ddf7716ceff9 100644
--- a/tests/value/oracle/addition.res.oracle
+++ b/tests/value/oracle/addition.res.oracle
@@ -136,8 +136,11 @@
out of bounds read. assert \valid_read(*((int **)45));
[eva] addition.i:87: Frama_C_show_each_1: [-10..15]
[eva] addition.i:88: assertion got status valid.
+[eva:alarm] addition.i:98: Warning:
+ signed overflow. assert p17 / (int)(-1) ≤ 2147483647;
[eva] Recording results for main
[eva] Done for function main
+[eva] addition.i:98: assertion 'Eva,signed_overflow' got final status invalid.
[scope:rm_asserts] removing 9 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -165,7 +168,7 @@
{{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
p15 ∈ {-1}
p16 ∈ {2949122}
- p17 ∈ {-2147483648; 0}
+ p17 ∈ {-2147483648}
u1 ∈ {8}
q1 ∈ {{ &p1 }}
quo1 ∈ {3}
@@ -363,6 +366,8 @@
[eva:alarm] addition.i:66: Warning:
out of bounds read. assert \valid_read(*((int **)45));
[eva] addition.i:87: Frama_C_show_each_1: [-10..15]
+[eva:alarm] addition.i:98: Warning:
+ signed overflow. assert p17 / (int)(-1) ≤ 2147483647;
[eva] Recording results for main
[eva] Done for function main
[scope:rm_asserts] removing 9 assertion(s)
@@ -393,7 +398,7 @@
{{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
p15 ∈ {-1}
p16 ∈ {2; 2949122; 3014658}
- p17 ∈ {-2147483648; 0}
+ p17 ∈ {-2147483648}
u1 ∈ {8}
q1 ∈ {{ &p1 }}
quo1 ∈ {3}
diff --git a/tests/value/oracle/modulo.res.oracle b/tests/value/oracle/modulo.res.oracle
index 2735d95852af1642e100d42a180b75add289acd7..af30cb8df0c8dfda0300fb88381c97c172f0131f 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:163.
-[eva:alarm] modulo.i:163: Warning:
+ Called from modulo.i:165.
+[eva:alarm] modulo.i:165: 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:164.
-[eva:alarm] modulo.i:164: Warning:
+ Called from modulo.i:166.
+[eva:alarm] modulo.i:166: 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:165.
-[eva:alarm] modulo.i:165: Warning:
+ Called from modulo.i:167.
+[eva:alarm] modulo.i:167: 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:167.
+ Called from modulo.i:169.
[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:168.
+ Called from modulo.i:170.
[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:169.
+ Called from modulo.i:171.
[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,30 +83,38 @@
[eva] Recording results for shift_modulo
[eva] Done for function shift_modulo
[eva] computing for function extract_bits_modulo <- main.
- Called from modulo.i:170.
+ Called from modulo.i:172.
[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:171.
+ Called from modulo.i:173.
[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:172.
-[eva:garbled-mix:write] modulo.i:156:
- Assigning imprecise value to r because of arithmetic operation on addresses.
-[eva:alarm] modulo.i:157: Warning: division by zero. assert i ≢ 0;
-[eva:garbled-mix:write] modulo.i:157:
- Assigning imprecise value to r because of arithmetic operation on addresses.
+ Called from modulo.i:174.
+[eva:alarm] modulo.i:158: Warning:
+ signed overflow. assert -2147483648 ≤ addr / 16;
+[eva:alarm] modulo.i:158: Warning:
+ signed overflow. assert addr / 16 ≤ 2147483647;
[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;
[eva:alarm] modulo.i:159: Warning:
- division by zero. assert (unsigned int)i ≢ 0;
+ signed overflow. assert -2147483648 ≤ addr / i;
+[eva:alarm] modulo.i:159: Warning:
+ signed overflow. assert addr / i ≤ 2147483647;
[eva:garbled-mix:write] modulo.i:159:
Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:garbled-mix:write] modulo.i:160:
+ Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:alarm] modulo.i:161: Warning:
+ division by zero. assert (unsigned int)i ≢ 0;
+[eva:garbled-mix:write] modulo.i:161:
+ Assigning imprecise value to r because of arithmetic operation on addresses.
[eva] Recording results for address_modulo
[eva] Done for function address_modulo
[eva] Recording results for main
@@ -118,7 +126,7 @@
uaddr ∈ {{ (unsigned int)&A ; (unsigned int)&B }}
addr ∈ {{ (int)&A ; (int)&B }}
i ∈ [-99..99]
- r ∈ {{ garbled mix of &{A; B} (origin: Arithmetic {modulo.i:159}) }}
+ r ∈ {{ garbled mix of &{A; B} (origin: Arithmetic {modulo.i:161}) }}
[eva:final-states] Values at end of function extract_bits_modulo:
i ∈ [0..10]
aa1 ∈ [1291..32011],1291%3072
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index cfbd463cdffd29c09f0e53feed5f870850e73e5c..27a80490220c3faa309e2febd15c8abdfec54e72 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -5,25 +5,26 @@
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
< [eva:garbled-mix:write] addition.i:61: Warning:
< Assigning imprecise value to p14 because of misaligned read of addresses.
-141c135,140
-< [scope:rm_asserts] removing 9 assertion(s)
----
+142a137,141
> [eva:garbled-mix:summary] Warning:
> Origins of garbled mix generated during analysis:
> addition.i:59: misaligned read of addresses
> (read in 1 statement, propagated through 2 statements)
> garbled mix of &{p1}
+144c143
+< [scope:rm_asserts] removing 9 assertion(s)
+---
> [scope:rm_asserts] removing 7 assertion(s)
-165c164
+168c167
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
-359,362d357
+362,365d360
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-368c363,368
+373c368,373
< [scope:rm_asserts] removing 9 assertion(s)
---
> [eva:garbled-mix:summary] Warning:
@@ -32,7 +33,7 @@
> (read in 1 statement, propagated through 2 statements)
> garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
-393c393
+398c398
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}