Skip to content
Snippets Groups Projects
Commit 248f120d authored by David Bühler's avatar David Bühler
Browse files

[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.
parent 5d48c248
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 74 additions and 72 deletions
src/plugins/eva/engine/evaluation.ml
+ 56
− 23
View file @ 248f120d
......@@ -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
......
src/plugins/eva/utils/eval_typ.ml
+ 7
− 0
View file @ 248f120d
......@@ -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
......
src/plugins/eva/utils/eval_typ.mli
+ 4
− 0
View file @ 248f120d
......@@ -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
tests/value/oracle/addition.res.oracle
+ 0
− 8
View file @ 248f120d
......@@ -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:
......
tests/value/oracle/div.0.res.oracle
+ 0
− 14
View file @ 248f120d
......@@ -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:
......
tests/value/oracle/div.1.res.oracle
+ 0
− 14
View file @ 248f120d
......@@ -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:
......
tests/value/oracle/modulo.res.oracle
+ 0
− 6
View file @ 248f120d
......@@ -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:
......
tests/value/oracle_equality/addition.res.oracle
+ 7
− 7
View file @ 248f120d
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}) }}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment