Merge branch 'feature/eva/bitwise-small-sets-precision' into 'master'

[ival] improve the precision of the computed small sets for bitwise operators

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

src/kernel_services/abstract_interp/int_set.ml

@@ -318,7 +318,7 @@ let apply_bin_1_strict_decr f x (s : Integer.t array) =
   in
   c 0
 
-let apply2_n f (s1 : Integer.t array) (s2 : Integer.t array) =
+let apply2 f (s1 : Integer.t array) (s2 : Integer.t array) =
   let ps = ref empty_ps in
   let l1 = Array.length s1 in
   let l2 = Array.length s2 in
@@ -588,7 +588,7 @@ let add_singleton = apply_bin_1_strict_incr Int.add
 let add s1 s2 =
   match s1, s2 with
   | [| x |], s | s, [| x |] -> `Set (apply_bin_1_strict_incr Int.add x s)
-  | _, _ -> apply2_n Int.add s1 s2
+  | _, _ -> apply2 Int.add s1 s2
 
 let add_under s1 s2 =
   match s1, s2 with
@@ -619,7 +619,7 @@ let scale f s =
 let mul s1 s2 =
   match s1, s2 with
   | s, [| x |] | [| x |], s -> `Set (scale x s)
-  | _, _ -> apply2_n Int.mul s1 s2
+  | _, _ -> apply2 Int.mul s1 s2
 
 let scale_div ~pos f s =
   assert (not (Int.is_zero f));

src/kernel_services/abstract_interp/int_set.mli

@@ -97,6 +97,9 @@ type set_or_top =
 
 type set_or_top_or_bottom = [ `Bottom | set_or_top ]
 
+(** [apply2 f s1 s2] applies [f i1 i2] for all integers i1 in s1 and i2 in s2. *)
+val apply2: (Integer.t -> Integer.t -> Integer.t) -> t -> t -> set_or_top
+
 (** {2 Lattice structure.} *)
 
 val is_included: t -> t -> bool

src/kernel_services/abstract_interp/int_val.ml

@@ -660,6 +660,8 @@ end
 
 module type BitOperator =
 sig
+  (* Concrete version of the bitwise operator *)
+  val concrete_bitwise : Int.t -> Int.t -> Int.t
   (* Printable version of the operator *)
   val representation : string
   (* forward is given here as the lifted function of some bit operator op
@@ -682,6 +684,8 @@ end
 
 module And : BitOperator =
 struct
+  let concrete_bitwise = Int.logand
+
   let representation = "&"
 
   let forward v1 v2 =
@@ -701,6 +705,8 @@ end
 
 module Or : BitOperator =
 struct
+  let concrete_bitwise = Int.logor
+
   let representation = "|"
 
   let forward v1 v2 =
@@ -720,6 +726,8 @@ end
 
 module Xor : BitOperator =
 struct
+  let concrete_bitwise = Int.logxor
+
   let representation = "^"
 
   let forward v1 v2 =
@@ -893,7 +901,15 @@ struct
       acc := List.fold_left (set_bit (Bit i)) [] !acc;
       if List.length !acc > small_cardinal () then raise Do_not_fit_small_sets
     done;
-    let list = List.map (fun (r, _, _) -> r) !acc in
+    (* Keep only values that can actually be obtained *)
+    let is_admissible (r, v1, v2) =
+      match v1, v2 with
+      | Set s1, Set s2 ->
+        let op = Op.concrete_bitwise in
+        Int_set.(exists (fun i1 -> exists (fun i2 -> op i1 i2 = r) s2) s1)
+      | _, _ -> true
+    in
+    let list = Extlib.filter_map is_admissible (fun (r, _, _) -> r) !acc in
     Set (Int_set.inject_list list)
 
   (* If lower is true (resp. false), compute the lower (resp. upper) bound of
@@ -936,18 +952,22 @@ struct
     bound
 
   let bitwise_forward (v1 : t) (v2 : t) : t =
-    let r, modu = compute_modulo v1 v2 in
-    match result_size v1 v2 with
-    | None ->
-      (* We could do better here, as one of the bound may be finite. However,
-         this case should occur rarely or not at all. *)
-      inject_interval None None r modu
-    | Some size ->
-      try compute_small_set ~size v1 v2 r modu
-      with Do_not_fit_small_sets ->
-        let min = compute_bound ~size v1 v2 true
-        and max = compute_bound ~size v1 v2 false in
-        inject_interval (Some min) (Some max) r modu
+    match v1, v2 with
+    | Set s1, Set s2 ->
+      inject_set_or_top (Int_set.apply2 Op.concrete_bitwise s1 s2)
+    | _, _ ->
+      let r, modu = compute_modulo v1 v2 in
+      match result_size v1 v2 with
+      | None ->
+        (* We could do better here, as one of the bound may be finite. However,
+           this case should occur rarely or not at all. *)
+        inject_interval None None r modu
+      | Some size ->
+        try compute_small_set ~size v1 v2 r modu
+        with Do_not_fit_small_sets ->
+          let min = compute_bound ~size v1 v2 true
+          and max = compute_bound ~size v1 v2 false in
+          inject_interval (Some min) (Some max) r modu
 end
 
 let bitwise_or = let module M = BitwiseOperator (Or) in M.bitwise_forward

tests/value/bitwise.i

@@ -2,11 +2,16 @@
    STDOPT: +"-big-ints-hex 256"
 */
 
-/*@ assigns \result \from min, max;
-    ensures min <= \result <= max ;
+/*@ assigns \result \from a, b;
+    ensures result_a_or_b: \result == a || \result == b ;
  */
-int Frama_C_interval(int min, int max);
+extern int Frama_C_nondet(int a, int b);
 
+/*@ requires order: min <= max;
+    assigns \result \from min, max;
+    ensures result_bounded: min <= \result <= max ;
+ */
+extern int Frama_C_interval(int min, int max);
 
 volatile long v;
 volatile unsigned char input[3];
@@ -67,13 +72,22 @@ int test4(void)
   if (something & 0x80000000) {
     Frama_C_show_each_true(something);
     return 0;
-  } 
+  }
   else {
     Frama_C_show_each_false(something);
     return 1;
   }
 }
 
+void test5(void)
+{
+  int x = Frama_C_nondet(-1, 0);
+  int y = Frama_C_nondet(-1, 0);
+  int a = x & y;
+  int b = x | y;
+  int c = x ^ y;
+}
+
 void and_or_rel(void)
 {
   long x, r1, r2, r3;
@@ -150,6 +164,7 @@ void main(void) {
   test2();
   test3();
   test4();
+  test5();
   and_or_rel();
   double_neg();
   bug1();

tests/value/oracle/bitwise.res.oracle

@@ -7,76 +7,95 @@
   input[0..2] ∈ [--..--]
   s ∈ [--..--]
 [eva] computing for function test1 <- main.
-  Called from tests/value/bitwise.i:149.
+  Called from tests/value/bitwise.i:163.
 [eva] computing for function Frama_C_interval <- test1 <- main.
-  Called from tests/value/bitwise.i:23.
+  Called from tests/value/bitwise.i:28.
 [eva] using specification for function Frama_C_interval
+[eva] tests/value/bitwise.i:28: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test1 <- main.
-  Called from tests/value/bitwise.i:24.
+  Called from tests/value/bitwise.i:29.
+[eva] tests/value/bitwise.i:29: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test1 <- main.
-  Called from tests/value/bitwise.i:25.
+  Called from tests/value/bitwise.i:30.
+[eva] tests/value/bitwise.i:30: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] Recording results for test1
 [eva] Done for function test1
 [eva] computing for function test2 <- main.
-  Called from tests/value/bitwise.i:150.
+  Called from tests/value/bitwise.i:164.
 [eva] computing for function Frama_C_interval <- test2 <- main.
-  Called from tests/value/bitwise.i:50.
+  Called from tests/value/bitwise.i:55.
+[eva] tests/value/bitwise.i:55: 
+  function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] Recording results for test2
 [eva] Done for function test2
 [eva] computing for function test3 <- main.
-  Called from tests/value/bitwise.i:151.
+  Called from tests/value/bitwise.i:165.
 [eva] Recording results for test3
 [eva] Done for function test3
 [eva] computing for function test4 <- main.
-  Called from tests/value/bitwise.i:152.
-[eva] tests/value/bitwise.i:62: assertion got status valid.
-[eva] tests/value/bitwise.i:64: 
+  Called from tests/value/bitwise.i:166.
+[eva] tests/value/bitwise.i:67: assertion got status valid.
+[eva] tests/value/bitwise.i:69: 
   Frama_C_show_each_1: [0x80000000..0xFFFFFFFF], {0x80000000}
-[eva] tests/value/bitwise.i:64: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
-[eva] tests/value/bitwise.i:66: 
+[eva] tests/value/bitwise.i:69: Frama_C_show_each_1: [0..0x7FFFFFFF], {0}
+[eva] tests/value/bitwise.i:71: 
   Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0x80000000}
-[eva] tests/value/bitwise.i:66: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
-[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
-[eva] tests/value/bitwise.i:72: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] tests/value/bitwise.i:71: Frama_C_show_each_2: [0..0x7FFFFFFF], {0}, {0}
+[eva] tests/value/bitwise.i:77: Frama_C_show_each_false: [0..0x7FFFFFFF]
+[eva] tests/value/bitwise.i:77: Frama_C_show_each_false: [0..0x7FFFFFFF]
 [eva] Recording results for test4
 [eva] Done for function test4
+[eva] computing for function test5 <- main.
+  Called from tests/value/bitwise.i:167.
+[eva] computing for function Frama_C_nondet <- test5 <- main.
+  Called from tests/value/bitwise.i:84.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] computing for function Frama_C_nondet <- test5 <- main.
+  Called from tests/value/bitwise.i:85.
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for test5
+[eva] Done for function test5
 [eva] computing for function and_or_rel <- main.
-  Called from tests/value/bitwise.i:153.
-[eva:alarm] tests/value/bitwise.i:87: Warning: assertion got status unknown.
+  Called from tests/value/bitwise.i:168.
+[eva:alarm] tests/value/bitwise.i:101: Warning: assertion got status unknown.
 [eva] Recording results for and_or_rel
 [eva] Done for function and_or_rel
 [eva] computing for function double_neg <- main.
-  Called from tests/value/bitwise.i:154.
+  Called from tests/value/bitwise.i:169.
 [eva] Recording results for double_neg
 [eva] Done for function double_neg
 [eva] computing for function bug1 <- main.
-  Called from tests/value/bitwise.i:155.
+  Called from tests/value/bitwise.i:170.
 [eva] Recording results for bug1
 [eva] Done for function bug1
 [eva] computing for function bug2 <- main.
-  Called from tests/value/bitwise.i:156.
-[eva] tests/value/bitwise.i:114: Frama_C_show_each_then:
-[eva] tests/value/bitwise.i:114: Frama_C_show_each_else:
+  Called from tests/value/bitwise.i:171.
+[eva] tests/value/bitwise.i:128: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:128: Frama_C_show_each_else:
 [eva] Recording results for bug2
 [eva] Done for function bug2
 [eva] computing for function bug3 <- main.
-  Called from tests/value/bitwise.i:157.
-[eva] tests/value/bitwise.i:121: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
+  Called from tests/value/bitwise.i:172.
+[eva] tests/value/bitwise.i:135: Frama_C_show_each: {0x41F656F}, {0xFBE09A91}
 [eva] Recording results for bug3
 [eva] Done for function bug3
 [eva] computing for function bug4 <- main.
-  Called from tests/value/bitwise.i:158.
-[eva] tests/value/bitwise.i:131: Frama_C_show_each_then:
-[eva] tests/value/bitwise.i:133: Frama_C_show_each_else:
+  Called from tests/value/bitwise.i:173.
+[eva] tests/value/bitwise.i:145: Frama_C_show_each_then:
+[eva] tests/value/bitwise.i:147: Frama_C_show_each_else:
 [eva] Recording results for bug4
 [eva] Done for function bug4
 [eva] computing for function bug5 <- main.
-  Called from tests/value/bitwise.i:159.
-[eva] tests/value/bitwise.i:144: Frama_C_show_each_dead: {0}
+  Called from tests/value/bitwise.i:174.
+[eva] tests/value/bitwise.i:158: Frama_C_show_each_dead: {0}
 [eva] Recording results for bug5
 [eva] Done for function bug5
 [eva] Recording results for main
@@ -136,6 +155,12 @@
   something ∈ [0..0x7FFFFFFF]
   topBitOnly ∈ {0; 0x80000000}
   __retres ∈ {1}
+[eva:final-states] Values at end of function test5:
+  x ∈ {-1; 0}
+  y ∈ {-1; 0}
+  a ∈ {-1; 0}
+  b ∈ {-1; 0}
+  c ∈ {-1; 0}
 [eva:final-states] Values at end of function main:
   
 [from] Computing for function and_or_rel
@@ -162,12 +187,18 @@
 [from] Done for function test3
 [from] Computing for function test4
 [from] Done for function test4
+[from] Computing for function test5
+[from] Computing for function Frama_C_nondet <-test5
+[from] Done for function Frama_C_nondet
+[from] Done for function test5
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
 [from] Function Frama_C_interval:
   \result FROM min; max
+[from] Function Frama_C_nondet:
+  \result FROM a; b
 [from] Function and_or_rel:
   NO EFFECTS
 [from] Function bug1:
@@ -190,6 +221,8 @@
   NO EFFECTS
 [from] Function test4:
   \result FROM v
+[from] Function test5:
+  NO EFFECTS
 [from] Function main:
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
@@ -238,6 +271,10 @@
     something; topBitOnly; __retres
 [inout] Inputs for function test4:
     v
+[inout] Out (internal) for function test5:
+    x; y; a; b; c
+[inout] Inputs for function test5:
+    \nothing
 [inout] Out (internal) for function main:
     \nothing
 [inout] Inputs for function main: