Merge branch 'feature/eva/sign-bitwise' into 'master'

[Eva] Implements bitwise and logical C forward operators in the sign values

See merge request frama-c/frama-c!2731

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

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

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

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

src/plugins/value/utils/unit_tests.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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 ()

src/plugins/value/utils/unit_tests.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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

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 =

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

tests/float/fval_test.i

 /* 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:

tests/value/oracle/unit_tests.res.oracle

+[kernel] Parsing tests/value/unit_tests.i (no preprocessing)
+[eva] Runs unit tests: only faulty operations will be printed.

tests/value/unit_tests.i

+/* run.config
+   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT:
+*/
+/* run.config*
+   DONTRUN:
+*/

tests/value/unit_tests.ml

+(* Programmatic tests of Eva, run by unit_tests.i. *)
+
+let () = Db.Main.extend Eva.Unit_tests.run