From 7efda0affb3be984cb2f9ca247840e56ab52f205 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 29 Jun 2020 11:41:55 +0200
Subject: [PATCH] [ival] improve the precision of the computed small sets for
bitwise operators
---
.../abstract_interp/int_val.ml | 18 +++-
tests/value/bitwise.i | 23 ++++-
tests/value/oracle/bitwise.res.oracle | 95 +++++++++++++------
3 files changed, 102 insertions(+), 34 deletions(-)
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index a98c8c40fee..e1afac0cf11 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/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
diff --git a/tests/value/bitwise.i b/tests/value/bitwise.i
index 10db311b22c..92a3bc59753 100644
--- a/tests/value/bitwise.i
+++ b/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();
diff --git a/tests/value/oracle/bitwise.res.oracle b/tests/value/oracle/bitwise.res.oracle
index 5bd9c79813b..20f6783fe65 100644
--- a/tests/value/oracle/bitwise.res.oracle
+++ b/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:
--
GitLab