[Eva] Emits alarms on a%b when a/b overflows.

According to the C standard, section 6.5.5 §6:
"If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a;
otherwise, the behavior of both a/b and a%b is undefined."

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
 

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 *)
 

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) =

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;

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}

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

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}) }}