From 248f120de81b16c3e16e126eac3ef103abc8886c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 2 Oct 2024 14:01:15 +0200
Subject: [PATCH] [Eva] Evaluation engine: more precise alarms about division
overflows.
Only emits overflow alarms on [a/b] when [a] may be equal to [min_int] AND
[b] may be equal to [-1]. Also reduces the values of [a] and [b] when possible.
---
src/plugins/eva/engine/evaluation.ml | 79 +++++++++++++------
src/plugins/eva/utils/eval_typ.ml | 7 ++
src/plugins/eva/utils/eval_typ.mli | 4 +
tests/value/oracle/addition.res.oracle | 8 --
tests/value/oracle/div.0.res.oracle | 14 ----
tests/value/oracle/div.1.res.oracle | 14 ----
tests/value/oracle/modulo.res.oracle | 6 --
.../value/oracle_equality/addition.res.oracle | 14 ++--
8 files changed, 74 insertions(+), 72 deletions(-)
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index c6a940037fe..5b3ef361dd5 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -342,6 +342,12 @@ module Make
Forward Operations, Alarms and Reductions
------------------------------------------------------------------------ *)
+ (* Applies function [f] on the optional value in a truth. *)
+ let apply_on_truth f = function
+ | `Unknown v -> `Unknown (f v)
+ | `TrueReduced v -> `TrueReduced (f v)
+ | `True | `False | `Unreachable as x -> x
+
(* Handles the result of an [assume] function from value abstractions (see
abstract_values.mli for more details), applied to the initial [value].
If the value could have been reduced, [reduce] is applied on the new value.
@@ -369,22 +375,37 @@ module Make
let reduce = reduce_argument (expr, value) in
process_truth ~reduce ~alarm value truth
- (* Processes the results of assume_comparable, that affects both arguments of
- the comparison. *)
- let reduce_by_double_truth ~alarm (e1, v1) (e2, v2) truth =
+ (* Interprets a [truth] about a pair of values (v1, v2), and reduce both
+ values accordingly. Used on the result of [Value.assume_comparable], which
+ affects both arguments of the comparison. *)
+ let reduce_both_by_truth ~alarm (e1, v1) (e2, v2) truth =
let reduce (new_value1, new_value2) =
Option.iter (fun e1 -> reduce_argument (e1, v1) new_value1) e1;
reduce_argument (e2, v2) new_value2;
in
process_truth ~reduce ~alarm (v1, v2) truth
+ (* Creates a disjunctive truth about the pair of values (v1, v2). *)
+ let disjunctive_truth (v1, truth1) (v2, truth2) =
+ match truth1, truth2 with
+ | (`True | `TrueReduced _), _
+ | _, (`True | `TrueReduced _) -> `True
+ | `Unreachable, _ | _, `Unreachable -> `Unreachable
+ | `False, `False -> `False
+ | `False, `Unknown v2 -> `Unknown (v1, v2)
+ | `Unknown v1, `False -> `Unknown (v1, v2)
+ | `Unknown _, `Unknown _ ->
+ (* [v1] (resp. [v2]) cannot be reduced as [truth2] (resp. [truth1])
+ might be true for some values. *)
+ `Unknown (v1, v2)
+
let is_true = function
| `True | `TrueReduced _ -> true
| _ -> false
+ (* Overflow of div is processed separately in [assume_valid_div]. *)
let may_overflow = function
- | Shiftlt | Mult | MinusPP | MinusPI | PlusPI
- | PlusA | MinusA | Div -> true
+ | Shiftlt | Mult | MinusPP | MinusPI | PlusPI | PlusA | MinusA -> true
| _ -> false
let truncate_bound overflow_kind bound bound_kind expr value =
@@ -541,19 +562,33 @@ module Make
let truth = Value.assume_bounded Alarms.Upper_bound size_int value in
reduce_by_truth ~alarm (index_expr, value) truth
- (* 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
+ (* If [typ] is a signed integer type, emits an alarm for a division overflow
+ if [v1] can be equal to min_int AND [v2] can be equal to [-1].
+ Also reduces the values of [v1] or [v2] accordingly when possible. *)
+ let assume_valid_div context typ (e1, v1) (e2, v2) =
+ match Eval_typ.integer_range ~ptr:false typ with
+ | Some range when range.i_signed ->
+ let min_int = Eval_typ.range_lower_bound range in
+ let max_int = Eval_typ.range_upper_bound range in
+ let alarm () =
+ let expr = Eva_ast.Build.div e1 e2 in
+ let cil_expr = Eva_ast.to_cil_exp expr in
+ Alarms.(Overflow (Signed, cil_expr, max_int, Upper_bound))
+ in
+ let forward_binop = Value.forward_binop context typ in
+ (* Bottom should never happen on addition or subtraction. *)
+ let add v1 v2 = Bottom.non_bottom (forward_binop PlusA v1 v2) in
+ let sub v1 v2 = Bottom.non_bottom (forward_binop MinusA v1 v2) in
+ let assume_non_equal value i =
+ let v_i = Value.inject_int typ i in
+ let truth = Value.assume_non_zero (sub value v_i) in
+ apply_on_truth (fun value -> add value v_i) truth
+ in
+ let truth1 = assume_non_equal v1 min_int in
+ let truth2 = assume_non_equal v2 Integer.minus_one in
+ let truth = disjunctive_truth (v1, truth1) (v2, truth2) in
+ reduce_both_by_truth ~alarm (Some e1, v1) (e2, v2) truth
+ | _ -> return (v1, v2)
let assume_valid_binop context typ (e1, v1 as arg1) op (e2, v2 as arg2) =
let open Evaluated.Operators in
@@ -563,9 +598,7 @@ module Make
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
- if op = Mod
- then assume_valid_mod context typ (e1, v1) (e2, v2)
- else return (v1, v2)
+ assume_valid_div context typ (e1, v1) (e2, v2)
| Shiftrt ->
let warn_negative = Kernel.RightShiftNegative.get () in
reduce_shift ~warn_negative typ arg1 arg2
@@ -579,7 +612,7 @@ module Make
Alarms.Differing_blocks (Eva_ast.to_cil_exp e1, Eva_ast.to_cil_exp e2)
in
let arg1 = Some e1, v1 in
- reduce_by_double_truth ~alarm arg1 arg2 truth
+ reduce_both_by_truth ~alarm arg1 arg2 truth
| _ -> return (v1, v2)
else return (v1, v2)
@@ -603,7 +636,7 @@ module Make
if warn_pointer_comparison typ then
if propagate_all
then `Value (v1, v2), snd (interpret_truth ~alarm (v1, v2) truth)
- else reduce_by_double_truth ~alarm (e1, v1) (e2, v2) truth
+ else reduce_both_by_truth ~alarm (e1, v1) (e2, v2) truth
else `Value (v1, v2), Alarmset.none
in
let result = let* v1, v2 = args in compute v1 v2 in
diff --git a/src/plugins/eva/utils/eval_typ.ml b/src/plugins/eva/utils/eval_typ.ml
index 69649a738b3..9781c483f5f 100644
--- a/src/plugins/eva/utils/eval_typ.ml
+++ b/src/plugins/eva/utils/eval_typ.ml
@@ -191,6 +191,13 @@ let classify_as_scalar typ =
| TFloat (fk, _) -> Some (TSFloat fk)
| _ -> None
+let integer_range ~ptr typ =
+ match Cil.unrollType typ with
+ | TInt (ik, attrs) | TEnum ({ekind=ik}, attrs) ->
+ Some (ik_attrs_range ik attrs)
+ | TPtr _ when ptr -> Some (pointer_range ())
+ | _ -> None
+
let need_cast t1 t2 =
match classify_as_scalar t1, classify_as_scalar t2 with
| None, None -> Cil.need_cast t1 t2
diff --git a/src/plugins/eva/utils/eval_typ.mli b/src/plugins/eva/utils/eval_typ.mli
index f00f1829f7e..62757358602 100644
--- a/src/plugins/eva/utils/eval_typ.mli
+++ b/src/plugins/eva/utils/eval_typ.mli
@@ -86,3 +86,7 @@ type scalar_typ =
(* Classifies a cil type as a scalar type; returns None for non-scalar types. *)
val classify_as_scalar: typ -> scalar_typ option
+
+(* Returns the range of a cil integer type; returns None for non-integer types.
+ Pointers are considered as integer types if [ptr] is true. *)
+val integer_range: ptr:bool -> typ -> integer_range option
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index 8e49b33bc5d..38e7399ccb3 100644
--- a/tests/value/oracle/addition.res.oracle
+++ b/tests/value/oracle/addition.res.oracle
@@ -102,10 +102,6 @@
assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
[eva:alarm] addition.i:50: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
-[eva:alarm] addition.i:50: Warning:
- signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
-[eva:alarm] addition.i:50: Warning:
- signed overflow. assert (int)(&p1) / 2 ≤ 2147483647;
[eva:garbled-mix:write] addition.i:50: Warning:
Assigning imprecise value to p9 because of arithmetic operation on addresses.
[eva:alarm] addition.i:52: Warning:
@@ -345,10 +341,6 @@
assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
[eva:alarm] addition.i:50: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
-[eva:alarm] addition.i:50: Warning:
- signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
-[eva:alarm] addition.i:50: Warning:
- signed overflow. assert (int)(&p1) / 2 ≤ 2147483647;
[eva:alarm] addition.i:52: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] addition.i:56: Warning:
diff --git a/tests/value/oracle/div.0.res.oracle b/tests/value/oracle/div.0.res.oracle
index 5595ff6926a..bf467409f16 100644
--- a/tests/value/oracle/div.0.res.oracle
+++ b/tests/value/oracle/div.0.res.oracle
@@ -33,8 +33,6 @@
[eva:alarm] div.i:33: Warning: division by zero. assert Z2 ≢ 0;
[eva:alarm] div.i:33: Warning:
pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
-[eva:alarm] div.i:33: Warning:
- signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
[eva:alarm] div.i:33: Warning:
signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
[eva:garbled-mix:write] div.i:33:
@@ -42,26 +40,14 @@
[eva:alarm] div.i:34: Warning:
pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
[eva:alarm] div.i:34: Warning: division by zero. assert (int)(&X + 2) ≢ 0;
-[eva:alarm] div.i:34: Warning:
- signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 2);
-[eva:alarm] div.i:34: Warning:
- signed overflow. assert 100 / (int)(&X + 2) ≤ 2147483647;
[eva:garbled-mix:write] div.i:34:
Assigning imprecise value to d2 because of arithmetic operation on addresses.
[eva:alarm] div.i:35: Warning:
pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
-[eva:alarm] div.i:35: Warning:
- signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
-[eva:alarm] div.i:35: Warning:
- signed overflow. assert 100 / (int)(&X + 1) ≤ 2147483647;
[eva:garbled-mix:write] div.i:35:
Assigning imprecise value to d1 because of arithmetic operation on addresses.
[eva:alarm] div.i:36: Warning:
pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
-[eva:alarm] div.i:36: Warning:
- signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
-[eva:alarm] div.i:36: Warning:
- signed overflow. assert 100 / (int)(&X) ≤ 2147483647;
[eva:garbled-mix:write] div.i:36:
Assigning imprecise value to d0 because of arithmetic operation on addresses.
[eva:alarm] div.i:37: Warning:
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
index d2a683468cb..6cc6efc9056 100644
--- a/tests/value/oracle/div.1.res.oracle
+++ b/tests/value/oracle/div.1.res.oracle
@@ -55,8 +55,6 @@
[eva:alarm] div.i:33: Warning: division by zero. assert Z2 ≢ 0;
[eva:alarm] div.i:33: Warning:
pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
-[eva:alarm] div.i:33: Warning:
- signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
[eva:alarm] div.i:33: Warning:
signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
[eva:garbled-mix:write] div.i:33:
@@ -68,10 +66,6 @@
[eva:alarm] div.i:34: Warning:
pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
[eva:alarm] div.i:34: Warning: division by zero. assert (int)(&X + 2) ≢ 0;
-[eva:alarm] div.i:34: Warning:
- signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 2);
-[eva:alarm] div.i:34: Warning:
- signed overflow. assert 100 / (int)(&X + 2) ≤ 2147483647;
[eva:garbled-mix:write] div.i:34:
Assigning imprecise value to d2 because of arithmetic operation on addresses.
[eva:alarm] div.i:35: Warning:
@@ -79,10 +73,6 @@
[eva] div.i:35: assertion 'rte,division_by_zero' got status valid.
[eva:alarm] div.i:35: Warning:
pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
-[eva:alarm] div.i:35: Warning:
- signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
-[eva:alarm] div.i:35: Warning:
- signed overflow. assert 100 / (int)(&X + 1) ≤ 2147483647;
[eva:garbled-mix:write] div.i:35:
Assigning imprecise value to d1 because of arithmetic operation on addresses.
[eva:alarm] div.i:36: Warning:
@@ -90,10 +80,6 @@
[eva] div.i:36: assertion 'rte,division_by_zero' got status valid.
[eva:alarm] div.i:36: Warning:
pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
-[eva:alarm] div.i:36: Warning:
- signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
-[eva:alarm] div.i:36: Warning:
- signed overflow. assert 100 / (int)(&X) ≤ 2147483647;
[eva:garbled-mix:write] div.i:36:
Assigning imprecise value to d0 because of arithmetic operation on addresses.
[eva:alarm] div.i:37: Warning:
diff --git a/tests/value/oracle/modulo.res.oracle b/tests/value/oracle/modulo.res.oracle
index af30cb8df0c..6159974336e 100644
--- a/tests/value/oracle/modulo.res.oracle
+++ b/tests/value/oracle/modulo.res.oracle
@@ -96,15 +96,9 @@
[eva] Done for function pos_rem
[eva] computing for function address_modulo <- main.
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:
- 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:
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 27a80490220..65ebb74096e 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -1,30 +1,30 @@
-129,134d128
+125,130d124
< [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;
< [eva:garbled-mix:write] addition.i:61: Warning:
< Assigning imprecise value to p14 because of misaligned read of addresses.
-142a137,141
+138a133,137
> [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
+140c139
< [scope:rm_asserts] removing 9 assertion(s)
---
> [scope:rm_asserts] removing 7 assertion(s)
-168c167
+164c163
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
-362,365d360
+354,357d352
< [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;
-373c368,373
+365c360,365
< [scope:rm_asserts] removing 9 assertion(s)
---
> [eva:garbled-mix:summary] Warning:
@@ -33,7 +33,7 @@
> (read in 1 statement, propagated through 2 statements)
> garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
-398c398
+390c390
< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
--
GitLab