From 6f7e4a33721baf98363f0cf889a192e379f66fb4 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 3 Dec 2021 01:56:41 +0100
Subject: [PATCH] [Eva] multidim: limit the size of the segmentation to 10
---
.../abstract_interp/abstract_memory.ml | 38 +++++++++-
tests/value/multidim.c | 36 ++++++++-
tests/value/oracle/multidim.res.oracle | 74 +++++++++++++++++--
3 files changed, 137 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index 2f3e1be7fa3..e848f1dc018 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -633,7 +633,7 @@ struct
Bound.upper_const ~oracle b
let born b = b, Integer.zero
- let _age (_,a) = a
+ let age (_,a) = a
let operators oracle : (module Operators with type t = t) =
operators (cmp ~oracle)
end
@@ -920,6 +920,40 @@ struct
| `Bottom -> assert false (* TODO: ensure that with typing *)
| `Value v -> v
+ let segments_limit = 10
+
+ let oldest_inner_bound m =
+ match m.segments with (* ignore m.start bound *)
+ | [] -> None
+ | (_,b) :: t ->
+ let rec aux acc = function
+ | [] -> None
+ | [_] -> Some acc (* ignore last bound *)
+ | (_,b) :: t -> aux (min acc (B.age b)) t
+ in
+ aux (B.age b) t
+
+ let remove_oldest_bounds ~oracle m =
+ match oldest_inner_bound m with
+ | None -> m (* no inner bounds, should not happen if segments_limit > 2 *)
+ | Some oldest_age ->
+ (* Remvoe all bounds of this age *)
+ let rec aux acc l = function
+ | ([] | [_]) as t -> List.rev (t @ acc)
+ | ((v,u) :: t) as s ->
+ if B.age u = oldest_age then
+ aux acc l (merge_first ~oracle l s)
+ else
+ aux ((v,u) :: acc) u t
+ in
+ { m with segments = aux [] m.start m.segments }
+
+ let limit_size ~oracle m =
+ let rec aux m n =
+ if n <= 0 then m else aux (remove_oldest_bounds ~oracle m) (n - 1)
+ in
+ aux m (List.length m.segments - segments_limit)
+
(* TODO: partitioning strategies
1. reinforcement without loss
2. weak update without singularization
@@ -985,7 +1019,7 @@ struct
age;
}
in
- aux_before m.start m.segments
+ limit_size ~oracle (aux_before m.start m.segments)
let incr_bound ~oracle vi x m =
let incr = B.incr_or_constantify ~oracle vi x in
diff --git a/tests/value/multidim.c b/tests/value/multidim.c
index bc3e62d3e8a..dda9e95f2a7 100644
--- a/tests/value/multidim.c
+++ b/tests/value/multidim.c
@@ -73,7 +73,8 @@ void main3(void) {
Frama_C_domain_show_each(z, r);
}
-void main4(void) { // How trace partitioning changes array partitioning ?
+void main4(void) {
+ // How trace partitioning changes array partitioning ?
int t[N];
//@ loop unroll 1;
@@ -83,6 +84,37 @@ void main4(void) { // How trace partitioning changes array partitioning ?
t[j] = 42;
}
}
+
+ Frama_C_domain_show_each(t);
+}
+
+void main5(void) {
+ // Array partitioning hints
+ int t[20] = {0};
+
+ //@ array_partition t, 0, 10, 20;
+ for (int i = 0; i < 20; i++) {
+ //@ split i < 9;
+ //@ split i == 9;
+ if (i < 10)
+ t[i] = 1;
+ else
+ t[i] = 2;
+ //@ array_partition t, 0, 10, 20;
+ }
+
+ Frama_C_domain_show_each(t);
+}
+
+void main6(void) {
+ // Limit on the number of bounds in a segmentation
+ int t[100];
+
+ //@ loop unroll 100;
+ for (int i = 0; i < 100; i++) {
+ t[i] = 0;
+ }
+
Frama_C_domain_show_each(t);
}
@@ -91,4 +123,6 @@ void main(s x) {
main2();
main3();
main4();
+ main5();
+ main6();
}
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index 83818a8f1c6..343affc156a 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing multidim.c (with preprocessing)
+[kernel] multidim.c:96: Warning:
+ Ignoring previous annotation relative to next statement effects
[eva:experimental] Warning: The multidim domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -7,7 +9,7 @@
z[0..3] ∈ {0}
nondet ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from multidim.c:90.
+ Called from multidim.c:122.
[eva] multidim.c:39:
Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
@@ -84,7 +86,7 @@
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from multidim.c:91.
+ Called from multidim.c:123.
[eva] multidim.c:55: starting to merge loop iterations
[eva:alarm] multidim.c:58: Warning: check got status unknown.
[eva] multidim.c:59:
@@ -94,7 +96,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from multidim.c:92.
+ Called from multidim.c:124.
[eva] multidim.c:64: starting to merge loop iterations
[eva] multidim.c:63: starting to merge loop iterations
[kernel] multidim.c:65:
@@ -135,16 +137,51 @@
[kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from multidim.c:93.
-[eva:loop-unroll:partial] multidim.c:80: loop not completely unrolled
-[eva] multidim.c:80: starting to merge loop iterations
-[eva] multidim.c:82: starting to merge loop iterations
-[eva] multidim.c:86:
+ Called from multidim.c:125.
+[eva:loop-unroll:partial] multidim.c:81: loop not completely unrolled
+[eva] multidim.c:81: starting to merge loop iterations
+[eva] multidim.c:83: starting to merge loop iterations
+[eva] multidim.c:88:
Frama_C_domain_show_each:
t : # cvalue: {42}
# multidim: { [0] = {42}, [1] = {42}, [2] = {42}, [3] = {42} }
[eva] Recording results for main4
[eva] Done for function main4
+[eva] computing for function main5 <- main.
+ Called from multidim.c:126.
+[eva] multidim.c:96: starting to merge loop iterations
+[eva] multidim.c:106:
+ Frama_C_domain_show_each:
+ t : # cvalue: [0..9] ∈ {0; 1}
+ [10..19] ∈ {0; 2}
+ # multidim: {
+ [0 .. 17] = {1; 2},
+ [18] = {1; 2},
+ [19] = {2},
+ [20 .. 19] = {0}
+ }
+[eva] Recording results for main5
+[eva] Done for function main5
+[eva] computing for function main6 <- main.
+ Called from multidim.c:127.
+[eva] multidim.c:114: Trace partitioning superposing up to 100 states
+[eva] multidim.c:118:
+ Frama_C_domain_show_each:
+ t : # cvalue: {0}
+ # multidim: {
+ [0 .. 90] = {0},
+ [91] = {0},
+ [92] = {0},
+ [93] = {0},
+ [94] = {0},
+ [95] = {0},
+ [96] = {0},
+ [97] = {0},
+ [98] = {0},
+ [99] = {0}
+ }
+[eva] Recording results for main6
+[eva] Done for function main6
[eva] Recording results for main
[eva] done for function main
[kernel] multidim.c:50: more than 1(28) elements to enumerate. Approximating.
@@ -165,6 +202,11 @@
r ∈ [--..--]
[eva:final-states] Values at end of function main4:
t[0..3] ∈ {42}
+[eva:final-states] Values at end of function main5:
+ t[0..9] ∈ {0; 1}
+ [10..19] ∈ {0; 2}
+[eva:final-states] Values at end of function main6:
+ t[0..99] ∈ {0}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
z[0..3] ∈ [--..--]
@@ -182,6 +224,10 @@
[from] Done for function main3
[from] Computing for function main4
[from] Done for function main4
+[from] Computing for function main5
+[from] Done for function main5
+[from] Computing for function main6
+[from] Done for function main6
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -200,6 +246,10 @@
z{[0..2]; [3].t1[0..3]} FROM \nothing (and SELF)
[from] Function main4:
NO EFFECTS
+[from] Function main5:
+ NO EFFECTS
+[from] Function main6:
+ NO EFFECTS
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
z[0..3] FROM \nothing
@@ -220,6 +270,14 @@
t[0..3]; i; j
[inout] Inputs for function main4:
\nothing
+[inout] Out (internal) for function main5:
+ t[0..19]; i
+[inout] Inputs for function main5:
+ \nothing
+[inout] Out (internal) for function main6:
+ t[0..99]; i
+[inout] Inputs for function main6:
+ \nothing
[inout] Out (internal) for function main:
Frama_C_entropy_source; z[0..3]
[inout] Inputs for function main:
--
GitLab