Commit 7b52a054 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Adds unit testing of the sign values semantics.

Unit tests are in the new file utils/unit_tests.ml, and are run by the new test
file tests/value/unit_tests.i through the exported function Eva.Unit_tests.test.
parent d1c267e2
......@@ -910,6 +910,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
utils/unit_tests \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
......
......@@ -1367,6 +1367,8 @@ src/plugins/value/utils/state_import.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/state_import.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_perf.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_perf.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_results.ml: CEA_LGPL_OR_PROPRIETARY
......
......@@ -42,7 +42,7 @@ val non_bottom: 'a or_bottom -> 'a
val equal: ('a -> 'a -> bool) -> 'a or_bottom -> 'a or_bottom -> bool
val compare: ('a -> 'a -> int) -> 'a or_bottom -> 'a or_bottom -> int
val is_included: ('a -> 'a -> bool) -> 'a or_bottom -> 'a or_bottom -> bool
val is_included: ('a -> 'b -> bool) -> 'a or_bottom -> 'b or_bottom -> bool
val join: ('a -> 'a -> 'a) -> 'a or_bottom -> 'a or_bottom -> 'a or_bottom
val join_list: ('a -> 'a -> 'a) -> 'a or_bottom list -> 'a or_bottom
val narrow: ('a -> 'a -> 'a or_bottom) -> 'a or_bottom -> 'a or_bottom -> 'a or_bottom
......
......@@ -60,3 +60,9 @@ module Eval_terms: sig
@return None on either an evaluation error or on unsupported construct. *)
val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
end
module Unit_tests: sig
(** Runs the unit tests of Eva. *)
val run: unit -> unit
end
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2020 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Cil_types
(* If true, prints each operation performed for the tests. Otherwise, only
prints wrong operations. *)
let print = false
let report bug format =
if print || bug
then Value_parameters.result ("%s" ^^ format) (if bug then "BUG " else "")
else Format.ifprintf Format.std_formatter format
(* Tests the semantics of sign values, by comparison with the Ival semantics. *)
module Sign = struct
module Sign = struct
include Sign_value
let zero = zero
let pos = one
let neg = inject_int Cil.uintType Integer.minus_one
let pos_or_zero = join zero pos
let neg_or_zero = join zero neg
let pos_neg = join pos neg
end
module Ival = struct
include Ival
let positive = inject_range (Some Integer.one) None
let negative = inject_range None (Some Integer.minus_one)
let pos irange =
let max = Eval_typ.range_upper_bound irange in
inject_range (Some Integer.one) (Some max)
let neg irange =
let min = Eval_typ.range_lower_bound irange in
inject_range (Some min) (Some Integer.minus_one)
end
module Cval = Main_values.CVal
(* List of pairs (ival, sign) such that γ(ival) ⊆ γ(sign) and all values in
γ(sign) are in the range of [ikind]. *)
let test_values ikind =
let irange = Eval_typ.ik_range ikind in
let list =
[ Ival.zero, Sign.zero;
Ival.pos irange, Sign.pos;
Ival.zero, Sign.pos_or_zero;
Ival.pos irange, Sign.pos_or_zero; ]
in
if not irange.Eval_typ.i_signed
then list
else
list @
[ Ival.neg irange, Sign.neg;
Ival.zero, Sign.neg_or_zero;
Ival.neg irange, Sign.neg_or_zero;
Ival.pos irange, Sign.pos_neg;
Ival.neg irange, Sign.pos_neg; ]
let make_cvalue values =
List.map (fun (ival, sign) -> Cvalue.V.inject_ival ival, sign) values
(* Checks whether γ(ival) ⊆ γ(sign). *)
let is_included cvalue sign =
try
let ival = Cvalue.V.project_ival cvalue in
(not (Ival.contains_zero ival) || sign.Sign.zero) &&
(Ival.(is_bottom (narrow ival positive)) || sign.Sign.pos) &&
(Ival.(is_bottom (narrow ival negative)) || sign.Sign.neg)
with Cvalue.V.Not_based_on_null -> Sign.(equal sign top)
let test_unop unop typ values =
let test (cval, sign) =
let cval_res = Cval.forward_unop typ unop cval in
let sign_res = Sign.forward_unop typ unop sign in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a = %a while %a %a = %a"
Printer.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
Printer.pp_unop unop Sign.pretty sign (Bottom.pretty Sign.pretty) sign_res
in
List.iter test values
let test_binop binop typ values =
let test (cval1, sign1) (cval2, sign2) =
let cval_res = Cval.forward_binop typ binop cval1 cval2 in
let sign_res = Sign.forward_binop typ binop sign1 sign2 in
let bug = not (Bottom.is_included is_included cval_res sign_res) in
report bug "%a %a %a = %a while %a %a %a = %a"
Cval.pretty cval1 Printer.pp_binop binop Cval.pretty cval2
(Bottom.pretty Cval.pretty) cval_res
Sign.pretty sign1 Printer.pp_binop binop Sign.pretty sign2
(Bottom.pretty Sign.pretty) sign_res
in
List.iter (fun x -> List.iter (test x) values) values
let test_typ ikind =
let typ = TInt (ikind, [])
and values = make_cvalue (test_values ikind) in
let apply f op = f op typ values in
List.iter (apply test_unop) [Neg; BNot; LNot];
List.iter (apply test_binop)
[PlusA; MinusA; Mult; Div; BAnd; BOr; BXor; LAnd; LOr]
let test () = List.iter test_typ [IInt; IUInt]
end
(** Runs all tests. *)
let run () =
Value_parameters.result "Runs unit tests: %s."
(if print
then "all operations will be printed"
else "only faulty operations will be printed");
Sign.test ()
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2020 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(** Currently tested by this file:
- semantics of sign values. *)
(** Runs some programmatic tests on Eva. *)
val run: unit -> unit
......@@ -22,6 +22,12 @@
(** Sign domain: abstraction of integer numerical values by their signs. *)
include Abstract_value.Leaf
type signs = {
pos: bool; (** true: maybe positive, false: never positive *)
zero: bool; (** true: maybe zero, false: never zero *)
neg: bool; (** true: maybe negative, false: never negative *)
}
include Abstract_value.Leaf with type t = signs
val pretty_debug: t Pretty_utils.formatter
[kernel] Parsing tests/value/unit_tests.i (no preprocessing)
[eva] Runs unit tests: only faulty operations will be printed.
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: -load-module @PTEST_DIR@/@PTEST_NAME@
*/
/* run.config*
DONTRUN:
*/
(* Programmatic tests of Eva, run by unit_tests.i. *)
let () = Db.Main.extend Eva.Unit_tests.run
Markdown is supported
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