From 7b52a054bf63f3b2fe85b8b91f4863c1ff8ebcaa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 25 Jun 2020 15:08:51 +0200
Subject: [PATCH] [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.
---
Makefile | 1 +
headers/header_spec.txt | 2 +
.../abstract_interp/bottom.mli | 2 +-
src/plugins/value/Eva.mli | 6 +
src/plugins/value/utils/unit_tests.ml | 135 ++++++++++++++++++
src/plugins/value/utils/unit_tests.mli | 27 ++++
src/plugins/value/values/sign_value.mli | 8 +-
tests/value/oracle/unit_tests.res.oracle | 2 +
tests/value/unit_tests.i | 7 +
tests/value/unit_tests.ml | 3 +
10 files changed, 191 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/value/utils/unit_tests.ml
create mode 100644 src/plugins/value/utils/unit_tests.mli
create mode 100644 tests/value/oracle/unit_tests.res.oracle
create mode 100644 tests/value/unit_tests.i
create mode 100644 tests/value/unit_tests.ml
diff --git a/Makefile b/Makefile
index d6d044aebe2..5ff002277f9 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7fdecae8316..d43eeffc48a 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -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
diff --git a/src/kernel_services/abstract_interp/bottom.mli b/src/kernel_services/abstract_interp/bottom.mli
index 799ccedfc3f..0af283e70bf 100644
--- a/src/kernel_services/abstract_interp/bottom.mli
+++ b/src/kernel_services/abstract_interp/bottom.mli
@@ -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
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 4de6198ed1a..a11a0dca9aa 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -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
diff --git a/src/plugins/value/utils/unit_tests.ml b/src/plugins/value/utils/unit_tests.ml
new file mode 100644
index 00000000000..043a2a726fa
--- /dev/null
+++ b/src/plugins/value/utils/unit_tests.ml
@@ -0,0 +1,135 @@
+(**************************************************************************)
+(* *)
+(* 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 ()
diff --git a/src/plugins/value/utils/unit_tests.mli b/src/plugins/value/utils/unit_tests.mli
new file mode 100644
index 00000000000..8783260b33a
--- /dev/null
+++ b/src/plugins/value/utils/unit_tests.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/plugins/value/values/sign_value.mli b/src/plugins/value/values/sign_value.mli
index 055794019f7..94dd0faa838 100644
--- a/src/plugins/value/values/sign_value.mli
+++ b/src/plugins/value/values/sign_value.mli
@@ -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
diff --git a/tests/value/oracle/unit_tests.res.oracle b/tests/value/oracle/unit_tests.res.oracle
new file mode 100644
index 00000000000..35ce0d1ac58
--- /dev/null
+++ b/tests/value/oracle/unit_tests.res.oracle
@@ -0,0 +1,2 @@
+[kernel] Parsing tests/value/unit_tests.i (no preprocessing)
+[eva] Runs unit tests: only faulty operations will be printed.
diff --git a/tests/value/unit_tests.i b/tests/value/unit_tests.i
new file mode 100644
index 00000000000..cabb2876892
--- /dev/null
+++ b/tests/value/unit_tests.i
@@ -0,0 +1,7 @@
+/* run.config
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@
+*/
+/* run.config*
+ DONTRUN:
+*/
diff --git a/tests/value/unit_tests.ml b/tests/value/unit_tests.ml
new file mode 100644
index 00000000000..48e3b3405bc
--- /dev/null
+++ b/tests/value/unit_tests.ml
@@ -0,0 +1,3 @@
+(* Programmatic tests of Eva, run by unit_tests.i. *)
+
+let () = Db.Main.extend Eva.Unit_tests.run
--
GitLab