[Eva] multidim: remove obviously empty slices after bound replacement

- many cases where equality/inclusions are verified

src/kernel_services/abstract_interp/abstract_memory.ml

@@ -885,8 +885,9 @@ struct
   let hash (b,_a) = Bound.hash b
   let compare (b1,_a1) (b2,_a2) =
     Bound.compare b1 b2
-  let equal (b1,_a1) (b2,_a2) =
+  let equal_regardless_age (b1,_a1) (b2,_a2) =
     Bound.equal b1 b2
+  let equal = equal_regardless_age
   let _of_integer i a = Bound.of_integer i, a
   let _of_exp e a = Bound.of_exp e, a
   let _succ (b,a) = (Bound.succ b, a)
@@ -954,6 +955,8 @@ struct
     padding: bit; (* padding at the left and right of the segmentation *)
   }
 
+  type segments = (M.t * B.t) list
+
   let _pretty_debug fmt (l,s) : unit =
     Format.fprintf fmt " {%a} " B.pretty l;
     let pp fmt (v,u) =
@@ -1311,6 +1314,24 @@ struct
     aging >>-:
     limit_size ~oracle
 
+  let remove_empty_segments m =
+    let unify_head_age (b' : B.t) : segments -> segments = function
+      | [] -> [] (* Start of segmentation, age is 0, do nothing *)
+      | (v,b) :: t -> (v, B.unify_age ~other:b' b) :: t
+    in
+    let rec aux l acc = function
+      | [] -> List.rev acc
+      | (v,u) :: t ->
+        (* Oracle cannot be used in case of incr here as it represents the
+           value of the bounds before the instruction, while we iterate
+           here over a segmentation interpreted after the instruction. *)
+        if B.equal_regardless_age l u then (* empty segment, remove v *)
+          aux l (unify_head_age u acc) t
+        else
+          aux u ((v,u) :: acc) t
+    in
+    { m with segments = check_segments (aux m.start [] m.segments) }
+
   let incr_bound ~oracle vi x m =
     let incr = B.incr_or_constantify ~oracle vi x in
     let rec aux acc = function
@@ -1337,7 +1358,8 @@ struct
           and v = M.smash ~oracle (M.of_raw m.padding) v in
           l, (v,u) :: t
     in
-    { m with start ; segments = check_segments (List.rev (aux [] segments)) }
+    { m with start ; segments = check_segments (List.rev (aux [] segments)) } |>
+    remove_empty_segments
 
   let map f m =
     { m with segments = check_segments (List.map (fun (v,u) -> f v, u) m.segments) }

tests/value/oracle/multidim.res.oracle

@@ -92,7 +92,7 @@
 [eva] multidim.c:59: 
   Frama_C_domain_show_each:
   t : # cvalue: {0; 1}
-      # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} }
+      # multidim: [0 .. 9] = {1}
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
@@ -154,12 +154,7 @@
   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}
-                  }
+      # multidim: { [0 .. 17] = {1; 2}, [18] = {1; 2}, [19] = {2} }
 [eva] Recording results for main5
 [eva] Done for function main5
 [eva] computing for function main6 <- main.
@@ -195,12 +190,9 @@
   Frama_C_domain_show_each:
   t : # cvalue: [0].typ ∈ {1; 2} or UNINITIALIZED
                 {[0].val; [1..999]} ∈ [--..--] or UNINITIALIZED
-      # multidim: {
-                    [0 .. 999] = {
-                      { .typ = {1}, .val.i = {42} } or 
-                      { .typ = {2}, .val.f = {42.} }
-                    },
-                    [1000 .. 999] = UNINITIALIZED
+      # multidim: [0 .. 999] = {
+                    { .typ = {1}, .val.i = {42} } or 
+                    { .typ = {2}, .val.f = {42.} }
                   }
 [eva] computing for function Frama_C_interval <- main7 <- main.
   Called from multidim.c:147.
@@ -219,7 +211,7 @@
 [eva] multidim.c:169: 
   Frama_C_domain_show_each:
   t : # cvalue: {0; 1}
-      # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} }
+      # multidim: [0 .. 9] = {1}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.