Skip to content
Snippets Groups Projects
Commit 7efda0af authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

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

parent 06b7167f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_services/abstract_interp/int_val.ml
+ 17
− 1
View file @ 7efda0af
......@@ -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
......
tests/value/bitwise.i
+ 19
− 4
View file @ 7efda0af
......@@ -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
+ 66
− 29
View file @ 7efda0af
......@@ -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:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment