[Eva] multidim: fix a non termination bug

- Unification doesn't keep empty slices anymore so they can't accumulate
- Fix the conversion of bounds to constants

src/kernel_services/abstract_interp/abstract_memory.ml

@@ -509,6 +509,16 @@ struct
     | Exp (e, i) -> Ival.add_singleton_int i (oracle e)
     | Ptroffset _ -> raise Not_implemented
 
+  let to_const ~oracle = function
+    | Const i -> Some i
+    | Exp (e, i) ->
+      begin try
+          Some (Integer.add (Ival.project_int (oracle e)) i)
+        with Ival.Not_Singleton_Int ->
+          None
+      end
+    | Ptroffset _ -> raise Not_implemented
+
   let succ = function
     | Const i -> Const (Integer.succ i)
     | Exp (e, i) -> Exp (e, Integer.succ i)
@@ -535,6 +545,11 @@ struct
         else Option.map (fun i -> Ptroffset (e, base, Integer.(sub j (mul l i)))) i
     with NonLinear -> None
 
+  let incr_or_constantify ~oracle vi i b =
+    match incr vi i b with
+    | Some v -> Some v
+    | None -> Option.map (fun c -> Const c) (to_const ~oracle b)
+
   let cmp_int i1 i2 =
     let r = Integer.sub i1 i2 in
     if Integer.is_zero r
@@ -597,11 +612,13 @@ struct
     Bound.compare b1 b2 <?> (Integer.compare, a1, a2)
   let equal (b1,a1) (b2,a2) =
     Bound.equal b1 b2 && Integer.equal a1 a2
-  let of_integer i a = Bound.of_integer i, a
+  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)
   let pred (b,a) = (Bound.pred b, a)
-  let incr vi i (b,a) = Bound.incr vi i b |> Option.map (fun b -> b,a)
+  let _incr vi i (b,a) = Bound.incr vi i b |> Option.map (fun b -> b,a)
+  let incr_or_constantify ~oracle vi i (b,a) =
+    Bound.incr_or_constantify ~oracle vi i b |> Option.map (fun b -> b,a)
   let _to_ival ~oracle (b,_a) = Bound.to_ival ~oracle b
   let cmp ~oracle (b1,_a1) (b2,_a2) = Bound.cmp ~oracle b1 b2
   let eq ?oracle (b1,_a1) (b2,_a2) = Bound.eq ?oracle b1 b2
@@ -615,7 +632,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
@@ -823,9 +840,15 @@ struct
       in
       match left_slice_emerges, right_slice_emerges with
       | Some (v1,u1,t1), None -> (* left slice emerges *)
-        aux u1 t1 s2 ((v1,u1) :: acc)
+        if equals Left l u1 then (* actually empty both sides*)
+          aux l t1 s2 acc
+        else
+          aux u1 t1 s2 ((v1,u1) :: acc)
       | None, Some (v2,u2,t2) -> (* right slice emerges *)
-        aux u2 s1 t2 ((v2,u2) :: acc)
+        if equals Right l u2 then (* actually empty both sides *)
+          aux l s1 t2 acc
+        else
+          aux u2 s1 t2 ((v2,u2) :: acc)
       | Some _, Some _ (* both emerges, can't choose *)
       | None, None -> (* none emerges *)
         match s1, s2 with (* Are we done yet ? *)
@@ -960,16 +983,7 @@ struct
     aux_before m.start m.segments
 
   let incr_bound ~oracle vi x m =
-    let incr b =
-      match B.incr vi x b with
-      | Some b -> Some b
-      | None ->
-        try
-          let i = Ival.project_int (oracle (Cil.evar vi)) in
-          Some (B.of_integer i (B.age b))
-        with Ival.Not_Singleton_Int ->
-          None
-    in
+    let incr = B.incr_or_constantify ~oracle vi x in
     let rec aux acc = function
       | [] -> acc
       | (v,u) :: t ->

tests/value/multidim.c

@@ -2,6 +2,7 @@
    STDOPT: #"-main main -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
    STDOPT: #"-main main2 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
    STDOPT: #"-main main3 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
+   STDOPT: #"-main main4 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
 */
 #include "__fc_builtin.h"
 #define N 4
@@ -27,7 +28,7 @@ s z[M];
 /*@ assigns z[..] \from \nothing;
     ensures \are_finite(z[..].t1[..].f) && \are_finite(z[..].t2[..].f);
   */
-void f();
+void f(void);
 
 volatile int nondet;
 
@@ -57,8 +58,8 @@ void main2(void) {
   for (int i = 0 ; i < 10 ; i++) {
     t[i] = 1;
   }
-  Frama_C_domain_show_each(t);
   //@ check t[0..9] == 1;
+  Frama_C_domain_show_each(t);
 }
 
 void main3(void) {
@@ -69,10 +70,21 @@ void main3(void) {
     }
   }
   
-  Frama_C_domain_show_each(z);
-
   int a = Frama_C_interval(0,M-1);
   int b = Frama_C_interval(0,N-1);
   t r = z[a].t1[b];
-  Frama_C_domain_show_each(r);
+  Frama_C_domain_show_each(z, r);
+}
+
+void main4(void) { // How trace partitioning changes array partitioning ?
+  int t[N];
+
+  //@ loop unroll 1;
+  for (int i = 0; i < M; i++) {
+    //@ loop unroll N;
+    for (int j = 0; j < N; j++) {
+      t[j] = 42;
+    }
+  }
+  Frama_C_domain_show_each(t);
 }

tests/value/oracle/multidim.0.res.oracle

 [kernel] Parsing multidim.c (with preprocessing)
-[kernel:typing:no-proto] multidim.c:49: Warning: 
-  Calling function f that is declared without prototype.
-  Its formals will be inferred from actual arguments
 [eva:experimental] Warning: The multidim domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
@@ -9,7 +6,7 @@
 [eva:initial-state] Values of globals at initialization
   z[0..3] ∈ {0}
   nondet ∈ [--..--]
-[eva] multidim.c:41: 
+[eva] multidim.c:42: 
   Frama_C_domain_show_each:
   x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
                 .t1[0].i ∈ [--..--]
@@ -44,7 +41,7 @@
        # multidim: { .t1[0] = { .f = {4.} } }
   z : # cvalue: {0}
       # multidim: 0
-[eva] multidim.c:47: 
+[eva] multidim.c:48: 
   Frama_C_domain_show_each:
   x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
                 .t1[0].i ∈ [--..--]
@@ -63,29 +60,29 @@
                 .t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
                 .t2[3].i ∈ [--..--]
       # multidim: {
-                    .t1[0 .. 4] = { .f = {{ ANYTHING }} },
-                    .t2[0 .. 4] = { .f = {{ ANYTHING }} }
+                    .t1[0 .. 3] = { .f = {{ ANYTHING }} },
+                    .t2[0 .. 3] = { .f = {{ ANYTHING }} }
                   }
 [eva] computing for function f <- main.
-  Called from multidim.c:49.
+  Called from multidim.c:50.
 [eva] using specification for function f
 [eva] Done for function f
-[eva] multidim.c:50: 
+[eva] multidim.c:51: 
   Frama_C_domain_show_each:
   z : # cvalue: [--..--]
-      # multidim: [0 .. 4] = {
-                    .t1[0 .. 4] = {
+      # multidim: [0 .. 3] = {
+                    .t1[0 .. 3] = {
                       .f = [-3.40282346639e+38 .. 3.40282346639e+38]
                     },
-                    .t2[0 .. 4] = {
+                    .t2[0 .. 3] = {
                       .f = [-3.40282346639e+38 .. 3.40282346639e+38]
                     }
                   }
-[eva:alarm] multidim.c:52: Warning: check got status unknown.
+[eva:alarm] multidim.c:53: Warning: check got status unknown.
 [eva] Recording results for main
 [eva] done for function main
-[kernel] multidim.c:52: more than 1(28) elements to enumerate. Approximating.
-[kernel] multidim.c:52: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:53: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:53: more than 1(28) elements to enumerate. Approximating.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   z[0..3] ∈ [--..--]

tests/value/oracle/multidim.1.res.oracle

 [kernel] Parsing multidim.c (with preprocessing)
-[kernel:typing:no-proto] multidim.c:49: Warning: 
-  Calling function f that is declared without prototype.
-  Its formals will be inferred from actual arguments
 [eva:experimental] Warning: The multidim domain is experimental.
 [eva] Analyzing a complete application starting at main2
 [eva] Computing initial state
@@ -9,12 +6,12 @@
 [eva:initial-state] Values of globals at initialization
   z[0..3] ∈ {0}
   nondet ∈ [--..--]
-[eva] multidim.c:57: starting to merge loop iterations
-[eva] multidim.c:60: 
+[eva] multidim.c:58: starting to merge loop iterations
+[eva:alarm] multidim.c:61: Warning: check got status unknown.
+[eva] multidim.c:62: 
   Frama_C_domain_show_each:
   t : # cvalue: {0; 1}
       # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} }
-[eva:alarm] multidim.c:61: Warning: check got status unknown.
 [eva] Recording results for main2
 [eva] done for function main2
 [eva] ====== VALUES COMPUTED ======

tests/value/oracle/multidim.2.res.oracle

 [kernel] Parsing multidim.c (with preprocessing)
-[kernel:typing:no-proto] multidim.c:49: Warning: 
-  Calling function f that is declared without prototype.
-  Its formals will be inferred from actual arguments
 [eva:experimental] Warning: The multidim domain is experimental.
 [eva] Analyzing a complete application starting at main3
 [eva] Computing initial state
@@ -9,47 +6,40 @@
 [eva:initial-state] Values of globals at initialization
   z[0..3] ∈ {0}
   nondet ∈ [--..--]
+[eva] multidim.c:67: starting to merge loop iterations
 [eva] multidim.c:66: starting to merge loop iterations
-[eva] multidim.c:65: starting to merge loop iterations
-[kernel] multidim.c:67: 
-  more than 1(20) locations to update in array. Approximating.
 [kernel] multidim.c:68: 
   more than 1(20) locations to update in array. Approximating.
-[kernel] multidim.c:67: 
-  more than 1(28) locations to update in array. Approximating.
+[kernel] multidim.c:69: 
+  more than 1(20) locations to update in array. Approximating.
 [kernel] multidim.c:68: 
   more than 1(28) locations to update in array. Approximating.
-[eva] multidim.c:72: 
-  Frama_C_domain_show_each:
-  z : # cvalue: [0].t1[0].f ∈ [0. .. 2.]
-                {[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
-                [--..--]
-                [3].t1[3].i ∈ {0; 2}
-                [3].t2[0..3] ∈ {0}
-      # multidim: [0 .. 3] = {
-                    .t1{
-                      [0 .. 3] = { .f = [0. .. 2.], .i = {0; 2} },
-                      [4 .. 3] = 0
-                    }
-                  }
+[kernel] multidim.c:69: 
+  more than 1(28) locations to update in array. Approximating.
 [eva] computing for function Frama_C_interval <- main3.
-  Called from multidim.c:74.
+  Called from multidim.c:73.
 [eva] using specification for function Frama_C_interval
-[eva] multidim.c:74: 
+[eva] multidim.c:73: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- main3.
-  Called from multidim.c:75.
-[eva] multidim.c:75: 
+  Called from multidim.c:74.
+[eva] multidim.c:74: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] multidim.c:77: 
+[eva] multidim.c:76: 
   Frama_C_domain_show_each:
+  z : # cvalue: [0].t1[0].f ∈ [0. .. 2.]
+                {[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
+                [--..--]
+                [3].t1[3].i ∈ {0; 2}
+                [3].t2[0..3] ∈ {0}
+      # multidim: [0 .. 3] = { .t1[0 .. 3] = { .f = [0. .. 2.], .i = {0; 2} } }
   r : # cvalue: [--..--]
       # multidim: { .f = [0. .. 2.], .i = {0; 2} }
 [eva] Recording results for main3
-[kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
 [kernel] multidim.c:68: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:69: more than 1(28) elements to enumerate. Approximating.
 [eva] done for function main3
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main3:
@@ -63,8 +53,8 @@
   b ∈ {0; 1; 2; 3}
   r ∈ [--..--]
 [from] Computing for function main3
-[kernel] multidim.c:67: more than 1(28) dependencies to update. Approximating.
 [kernel] multidim.c:68: more than 1(28) dependencies to update. Approximating.
+[kernel] multidim.c:69: more than 1(28) dependencies to update. Approximating.
 [from] Computing for function Frama_C_interval <-main3
 [from] Done for function Frama_C_interval
 [from] Done for function main3

tests/value/oracle/multidim.3.res.oracle

+[kernel] Parsing multidim.c (with preprocessing)
+[eva:experimental] Warning: The multidim domain is experimental.
+[eva] Analyzing a complete application starting at main4
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  z[0..3] ∈ {0}
+  nondet ∈ [--..--]
+[eva:loop-unroll:partial] multidim.c:83: loop not completely unrolled
+[eva] multidim.c:83: starting to merge loop iterations
+[eva] multidim.c:85: starting to merge loop iterations
+[eva] multidim.c:89: 
+  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] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main4:
+  t[0..3] ∈ {42}
+[from] Computing for function main4
+[from] Done for function main4
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function main4:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main4:
+    t[0..3]; i; j
+[inout] Inputs for function main4:
+    \nothing