diff --git a/Makefile b/Makefile
index d6d044aebe2a88c183a3477078b4574087e5699d..5ff002277f9313e9675975904459bdca593ddb92 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 7fdecae8316b409d5dc49098688c2cf5cd52f1a9..d43eeffc48af86d043e959faf807147e54c171e7 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 799ccedfc3f67f9507b9bcb5b89893eeb0bb109a..0af283e70bf755cd874fc5ea3bc51725fd8007d6 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 4de6198ed1a43b3c1d4a9c2d0a344b378eee5dc6..a11a0dca9aa2bab2ab56cfc918b2dbb915cd0c8e 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 0000000000000000000000000000000000000000..043a2a726fa93a52dba15278fa6a4ca2881935e0
--- /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 0000000000000000000000000000000000000000..8783260b33accee3d55c8edf0a5002e41d3ed89b
--- /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.ml b/src/plugins/value/values/sign_value.ml
index 74c45a2c26862947e8909f5d0997dbf695722b5a..93051f60d086a6613c33d8327a049d52343fb9f8 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -125,17 +125,28 @@ let assume_comparable _ v1 v2 = `Unknown (v1, v2)
(** {2 Forward transfer functions} *)
-(* The three functions below are forward transformers for the mathematical
- operations +, *, /, and the unary negation -. The potential overflows for the
- operations on machine integers are taken into account by the functions
- [truncate_integer] and [rewrap_integer]. *)
+(* Functions [neg_unop], [plus], [mul] and [div] below are forward transformers
+ for the mathematical operations -, +, *, /. The potential overflows and
+ wrappings for the operations on machine integers are taken into account by
+ the functions [truncate_integer] and [rewrap_integer]. *)
let neg_unop v = { v with neg = v.pos; pos = v.neg }
-let forward_unop _ op v =
+let bitwise_not typ v =
+ match Cil.unrollType typ with
+ | TInt (ikind, _) | TEnum ({ekind=ikind}, _) ->
+ if Cil.isSigned ikind
+ then { pos = v.neg; neg = v.pos || v.zero; zero = v.neg }
+ else { pos = v.pos || v.zero; neg = false; zero = v.pos }
+ | _ -> top
+
+let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
+
+let forward_unop typ op v =
match op with
| Neg -> `Value (neg_unop v)
- | _ -> `Value top
+ | BNot -> `Value (bitwise_not typ v)
+ | LNot -> `Value (logical_not v)
let plus v1 v2 =
let neg = v1.neg || v2.neg in
@@ -158,12 +169,69 @@ let div v1 v2 =
let zero = true in (* zero can appear with large enough v2 *)
{ neg; pos; zero }
+(* The implementation of the bitwise operators below relies on this table
+ giving the sign of the result according to the sign of both operands.
+
+ v1 v2 v1&v2 v1|v2 v1^v2
+ -----------------------------------
+ | + + +0 + +0
+ | + 0 0 + +
+ | + - +0 - -
+ | 0 + 0 + +
+ | 0 0 0 0 0
+ | 0 - 0 - -
+ | - + +0 - -
+ | - 0 0 - -
+ | - - - - +0
+*)
+
+let bitwise_and v1 v2 =
+ let pos = (v1.pos && (v2.pos || v2.neg)) || (v2.pos && v1.neg) in
+ let neg = v1.neg && v2.neg in
+ let zero = v1.zero || v1.pos || v2.zero || v2.pos in
+ { neg; pos; zero }
+
+let bitwise_or v1 v2 =
+ let pos = (v1.pos && (v2.pos || v2.zero)) || (v1.zero && v2.pos) in
+ let neg = v1.neg || v2.neg in
+ let zero = v1.zero && v2.zero in
+ { neg; pos; zero }
+
+let bitwise_xor v1 v2 =
+ let pos =
+ (v1.pos && v2.pos) || (v1.pos && v2.zero) || (v1.zero && v2.pos)
+ || (v1.neg && v2.neg)
+ in
+ let neg =
+ (v1.neg && (v2.pos || v2.zero)) ||
+ (v2.neg && (v1.pos || v1.zero))
+ in
+ let zero = (v1.zero && v2.zero) || (v1.pos && v2.pos) || (v1.neg && v2.neg) in
+ { neg; pos; zero }
+
+let logical_and v1 v2 =
+ let pos = (v1.pos || v1.neg) && (v2.pos || v2.neg) in
+ let neg = false in
+ let zero = v1.zero || v2.zero in
+ { pos; neg; zero }
+
+let logical_or v1 v2 =
+ let pos = v1.pos || v1.neg || v2.pos || v2.neg in
+ let neg = false in
+ let zero = v1.zero && v2.zero in
+ { pos; neg; zero }
+
let forward_binop _ op v1 v2 =
match op with
| PlusA -> `Value (plus v1 v2)
| MinusA -> `Value (plus v1 (neg_unop v2))
| Mult -> `Value (mul v1 v2)
| Div -> if equal zero v2 then `Bottom else `Value (div v1 v2)
+ | BAnd -> `Value (bitwise_and v1 v2)
+ | BOr -> `Value (bitwise_or v1 v2)
+ | BXor -> `Value (bitwise_xor v1 v2)
+ | LAnd -> `Value (logical_and v1 v2)
+ | LOr -> `Value (logical_or v1 v2)
| _ -> `Value top
let rewrap_integer range v =
diff --git a/src/plugins/value/values/sign_value.mli b/src/plugins/value/values/sign_value.mli
index 055794019f7c3ace0d52ffd9652037f60c978d4e..94dd0faa8383c843fc97a7e8093f992c51f74bd5 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/float/fval_test.i b/tests/float/fval_test.i
index cabb28768924493f9964d6329934d0356b2e5143..f480093ba099eda06a2fdca943402b02945c5cce 100644
--- a/tests/float/fval_test.i
+++ b/tests/float/fval_test.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT:
*/
/* run.config*
DONTRUN:
diff --git a/tests/value/oracle/unit_tests.res.oracle b/tests/value/oracle/unit_tests.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..35ce0d1ac58fd2746a03ac9dc7555281595b0f8e
--- /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 0000000000000000000000000000000000000000..f480093ba099eda06a2fdca943402b02945c5cce
--- /dev/null
+++ b/tests/value/unit_tests.i
@@ -0,0 +1,7 @@
+/* run.config
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT:
+*/
+/* run.config*
+ DONTRUN:
+*/
diff --git a/tests/value/unit_tests.ml b/tests/value/unit_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..48e3b3405bcb13af995b3a50f15aebaa64b09b54
--- /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