[Eva] multidim: limit the size of the segmentation to 10

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

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();
 }

tests/value/oracle/multidim.res.oracle

 [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: