Add Interval Set domain for Interval Set analysis

docs/user-guide/annotating.md

@@ -21,10 +21,13 @@ The attribute `goblint_context` can be used to fine-tune function contexts.
 The following string arguments are supported:
 
 1. `base.interval`/`base.no-interval` to override the `ana.base.context.interval` option.
-2. `base.int`/`base.no-int` to override the `ana.base.context.interval` option.
-3. `base.non-ptr`/`base.no-non-ptr` to override the `ana.base.context.non-ptr` option.
-4. `relation.context`/`relation.no-context` to override the `ana.relation.context` option.
-5. `widen`/`no-widen` to override the `ana.context.widen` option.
+2. `base.interval_set`/`base.no-interval_set` to override the `ana.base.context.interval_set` option.
+3. `base.int`/`base.no-int` to override the `ana.base.context.interval` option.
+4. `base.non-ptr`/`base.no-non-ptr` to override the `ana.base.context.non-ptr` option.
+5. `relation.context`/`relation.no-context` to override the `ana.relation.context` option.
+6. `widen`/`no-widen` to override the `ana.context.widen` option.
+
+
 
 ### Apron attributes
 The Apron library can be set to only track variables with the attribute `goblint_apron_track`

src/analyses/base.ml

@@ -595,6 +595,8 @@ struct
 
   let drop_interval = CPA.map (function `Int x -> `Int (ID.no_interval x) | x -> x)
 
+  let drop_intervalSet = CPA.map (function `Int x -> `Int (ID.no_intervalSet x) | x -> x )
+
   let context (fd: fundec) (st: store): store =
     let f keep drop_fn (st: store) = if keep then st else { st with cpa = drop_fn st.cpa} in
     st |>
@@ -604,6 +606,7 @@ struct
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.non-ptr" ~removeAttr:"base.no-non-ptr" ~keepAttr:"base.non-ptr" fd) drop_non_ptrs
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.int" ~removeAttr:"base.no-int" ~keepAttr:"base.int" fd) drop_ints
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval" ~removeAttr:"base.no-interval" ~keepAttr:"base.interval" fd) drop_interval
+    %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval_set" ~removeAttr:"base.no-interval_set" ~keepAttr:"base.interval_set" fd) drop_intervalSet
 
   let context_cpa fd (st: store) = (context fd st).cpa
 

src/autoTune.ml

@@ -129,8 +129,8 @@ let disableIntervalContextsInRecursiveFunctions () =
   ResettableLazy.force functionCallMaps |> fun (x,_,_) -> x |> FunctionCallMap.iter (fun f set ->
       (*detect direct recursion and recursion with one indirection*)
       if FunctionSet.mem f set || (not @@ FunctionSet.disjoint (calledFunctions f) (callingFunctions f)) then (
-        print_endline ("function " ^ (f.vname) ^" is recursive, disable interval context");
-        f.vattr <- addAttributes (f.vattr) [Attr ("goblint_context",[AStr "base.no-interval"; AStr "relation.no-context"])];
+        print_endline ("function " ^ (f.vname) ^" is recursive, disable interval and intervalSet contexts");
+        f.vattr <- addAttributes (f.vattr) [Attr ("goblint_context",[AStr "base.no-interval"; AStr "base.no-interval_set"; AStr "relation.no-context"])];
       )
     )
 

src/cdomains/intDomain.mli

@@ -273,6 +273,37 @@ sig
 end
 (** Interface of IntDomain implementations taking an ikind for arithmetic operations *)
 
+module type SOverFlow = 
+sig
+
+  include S
+
+  val add : ?no_ov:bool -> Cil.ikind ->  t -> t -> t * bool * bool * bool
+
+  val sub : ?no_ov:bool -> Cil.ikind ->  t -> t -> t * bool * bool * bool
+
+  val mul : ?no_ov:bool -> Cil.ikind ->  t -> t -> t * bool * bool * bool
+
+  val div : ?no_ov:bool -> Cil.ikind ->  t -> t -> t * bool * bool * bool
+
+  val neg : ?no_ov:bool -> Cil.ikind ->  t -> t * bool * bool * bool
+
+  val cast_to : ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * bool * bool * bool
+
+  val of_int : Cil.ikind -> int_t -> t * bool * bool * bool
+
+  val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t * bool  * bool * bool
+
+  val starting : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t * bool  * bool * bool
+  val ending : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t * bool * bool * bool
+
+  val shift_left : Cil.ikind -> t -> t -> t * bool * bool * bool
+
+  val shift_right: Cil.ikind -> t -> t -> t * bool * bool * bool
+
+
+end
+
 module OldDomainFacade (Old : IkindUnawareS with type int_t = int64) : S with type int_t = IntOps.BigIntOps.t and type t = Old.t
 (** Facade for IntDomain implementations that do not implement the interface where arithmetic functions take an ikind parameter. *)
 
@@ -320,6 +351,7 @@ module IntDomWithDefaultIkind (I: Y) (Ik: Ikind) : Y with type t = I.t and type
 module IntDomTuple : sig
   include Z
   val no_interval: t -> t
+  val no_intervalSet: t -> t
   val ikind: t -> ikind
 end
 
@@ -369,7 +401,9 @@ module FlattenedBI : IkindUnawareS with type t = [`Top | `Lifted of IntOps.BigIn
 module Lifted : IkindUnawareS with type t = [`Top | `Lifted of int64 | `Bot] and type int_t = int64
 (** Artificially bounded integers in their natural ordering. *)
 
-module IntervalFunctor(Ints_t : IntOps.IntOps): S with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option
+module IntervalFunctor(Ints_t : IntOps.IntOps): SOverFlow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option
+
+module IntervalSetFunctor(Ints_t : IntOps.IntOps): SOverFlow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list
 
 module Interval32 :Y with (* type t = (IntOps.Int64Ops.t * IntOps.Int64Ops.t) option and *) type int_t = IntOps.Int64Ops.t
 
@@ -379,7 +413,9 @@ module BigInt:
     val cast_to: Cil.ikind -> Z.t -> Z.t
   end
 
-module Interval : S with type int_t = IntOps.BigIntOps.t
+module Interval : SOverFlow with type int_t = IntOps.BigIntOps.t
+
+module IntervalSet : SOverFlow with type int_t = IntOps.BigIntOps.t
 
 module Congruence : S with type int_t = IntOps.BigIntOps.t
 

src/util/options.schema.json

@@ -357,7 +357,13 @@
             "interval": {
               "title": "ana.int.interval",
               "description":
-                "Use IntDomain.Interval32: (int64 * int64) option.",
+                "Use IntDomain.Interval32: (Z.t * Z.t) option.",
+              "type": "boolean",
+              "default": false
+            },
+            "interval_set": {
+              "title": "ana.int.interval_set",
+              "description": "Use IntDomain.IntervalSet: (Z.t * Z.t) list.",
               "type": "boolean",
               "default": false
             },
@@ -589,6 +595,13 @@
                     "Integer values of the Interval domain in function contexts.",
                   "type": "boolean",
                   "default": true
+                },
+                "interval_set": {
+                  "title": "ana.base.context.interval_set",
+                  "description":
+                    "Integer values of the IntervalSet domain in function contexts.",
+                  "type": "boolean",
+                  "default": true
                 }
               },
               "additionalProperties": false
@@ -1430,7 +1443,7 @@
             "type": "array",
             "items": {
               "type": "string",
-              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.interval", "relation.no-context", "relation.context", "no-widen", "widen"]
+              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set","base.interval", "base.interval_set","relation.no-context", "relation.context", "no-widen", "widen"]
             },
             "default": []
           }

src/util/precisionUtil.ml

@@ -1,19 +1,20 @@
 (* We define precision by the number of IntDomains activated.
- * We currently have 4 types: DefExc, Interval, Enums, Congruence *)
-type int_precision = (bool * bool * bool * bool)
+ * We currently have 5 types: DefExc, Interval, Enums, Congruence, IntervalSet *)
+type int_precision = (bool * bool * bool * bool * bool)
 (* Same applies for FloatDomain
  * We currently have only an interval type analysis *)
 type float_precision = (bool)
 
 
 (* Thus for maximum precision we activate all Domains *)
-let max_int_precision : int_precision = (true, true, true, true)
+let max_int_precision : int_precision = (true, true, true, true, true)
 let max_float_precision : float_precision = (true)
 let int_precision_from_fundec (fd: GoblintCil.fundec): int_precision =
   ((ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.int.def_exc" ~removeAttr:"no-def_exc" ~keepAttr:"def_exc" fd),
    (ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.int.interval" ~removeAttr:"no-interval" ~keepAttr:"interval" fd),
    (ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.int.enums" ~removeAttr:"no-enums" ~keepAttr:"enums" fd),
-   (ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.int.congruence" ~removeAttr:"no-congruence" ~keepAttr:"congruence" fd))
+   (ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.int.congruence" ~removeAttr:"no-congruence" ~keepAttr:"congruence" fd),
+   (ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.int.interval_set" ~removeAttr:"no-interval_set" ~keepAttr:"interval_set" fd))
 
 let float_precision_from_fundec (fd: GoblintCil.fundec): float_precision =
   ((ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.float.interval" ~removeAttr:"no-float-interval" ~keepAttr:"float-interval" fd))
@@ -22,7 +23,7 @@ let int_precision_from_node (): int_precision =
   | Some n -> int_precision_from_fundec (Node.find_fundec n)
   | _ -> max_int_precision (* In case a Node is None we have to handle Globals, i.e. we activate all IntDomains (TODO: verify this assumption) *)
 
-let is_congruence_active (_, _, _, c: int_precision): bool = c
+let is_congruence_active (_, _, _, c,_: int_precision): bool = c
 
 let float_precision_from_node (): float_precision =
   match !MyCFG.current_node with
@@ -34,7 +35,7 @@ let int_precision_from_node_or_config (): int_precision =
     int_precision_from_node ()
   else
     let f n = GobConfig.get_bool ("ana.int."^n) in
-    (f "def_exc", f "interval", f "enums", f "congruence")
+    (f "def_exc", f "interval", f "enums", f "congruence", f "interval_set")
 
 let float_precision_from_node_or_config (): float_precision =
   if GobConfig.get_bool "annotation.float.enabled" then

tests/regression/66-interval-set-one/00-was_problematic_2.c

@@ -0,0 +1,24 @@
+// PARAM: --enable ana.int.interval_set  --set ana.base.arrays.domain partitioned
+int main(void)
+{
+  int arr[260];
+  int n;
+
+  n = 5;
+  arr[0] = 0;
+
+  while (n > 1) { //here
+    arr[1] = 7;
+    n--;
+  }
+
+  int arr2[260];
+
+  n = 5;
+  arr2[259] = 0;
+
+  while (n > 1) {
+    arr2[258] = 7;
+    n--;
+  }
+}

tests/regression/66-interval-set-one/01-dynamically-sized-array-oob-access.c

@@ -0,0 +1,33 @@
+// PARAM: --enable ana.arrayoob --enable ana.int.interval_set --enable ana.int.interval_set --enable ana.int.enums
+
+// Variable sized array: oob access
+
+#include <stdio.h>
+#include <stdlib.h>
+int main() {
+  int top;
+  int N;
+// The if statement is needed, so the size is actually dynamic
+  if (top) {
+    N = 5;
+  } else {
+    N = 10;
+  }
+  int arr[N];
+  arr[0] = 1;
+  arr[1] = 2;
+  arr[2] = 3;
+  arr[3] = 4;
+  arr[4] = 5;   // NOWARN
+  arr[-1] = 10; // WARN
+  for (int i = 0; i < 5; ++i) {
+    arr[i] = 5; // NOWARN
+  }
+  for (int i = 0; i <= 5; ++i) {
+    arr[i] = 5; // WARN
+  }
+  for (int i = -2; i < 5; ++i) {
+    arr[i] = 5; // WARN
+  }
+  return 0;
+}

tests/regression/66-interval-set-one/02-continue.c

@@ -0,0 +1,20 @@
+// PARAM: --enable ana.int.interval_set --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5
+// Simple example
+#include <goblint.h>
+
+void main(void)
+{
+    int j = 0;
+
+    for(int i=0;i < 50;i++) {
+        if(i < 2) {
+            continue;
+        }
+        if(i>4) {
+            break;
+        }
+        j++;
+    }
+
+    __goblint_check(j==3);
+}

tests/regression/66-interval-set-one/03-was_problematic_3.c

@@ -0,0 +1,52 @@
+// PARAM: --enable ana.int.interval_set  --set ana.base.arrays.domain partitioned
+struct some_struct
+{
+    int dir[7];
+    int length;
+    double coeff;
+    double forwback;
+};
+
+struct some_struct q_paths[200];
+int num_q_paths;
+
+int add_basic_path(int length, double coeff)
+{
+    int ir[4];
+    int j;
+    int flag;
+
+    ir[2] = 0;
+    while (ir[2] < 2)
+    {
+        ir[3] = 0;
+        while (ir[3] < 2)
+        {
+            j = 0;
+            while (j < num_q_paths)
+            {
+                if (flag == 1)
+                {
+                    break;
+                }
+                j++;
+            }
+
+            q_paths[num_q_paths].length = length;
+
+            num_q_paths++;
+
+            (ir[3])++;
+        }
+        (ir[2])++;
+    }
+
+    return 42;
+}
+
+int main(int argc, char **argv)
+{
+    double this_coeff;
+    int pl;
+    add_basic_path(pl, this_coeff);
+}

tests/regression/66-interval-set-one/04-interval-overflow.c

@@ -0,0 +1,44 @@
+// PARAM: --enable ana.int.interval_set --enable ana.int.congruence --disable ana.int.def_exc
+// Overflow information should be passed from the interval domain to congruences
+#include <goblint.h>
+#include <stdio.h>
+
+int main(){
+  signed char r;
+
+  if (r) {
+    r = -68;
+  } else {
+    r = -63;
+  }
+
+  signed char k = r - 80;
+  __goblint_check(k == 0); //UNKNOWN!
+
+  signed char non_ov = r - 10;
+  __goblint_check(non_ov == -78); //UNKNOWN!
+
+  signed char m = r * 2;
+
+  __goblint_check(m == 0); //UNKNOWN!
+
+  signed char l = r + (-80);
+  __goblint_check(l == 0); //UNKNOWN!
+
+  int g;
+
+  if (g) {
+    g = -126;
+  } else {
+    g = -128;
+  }
+
+  signed char f = g / (-1);
+  __goblint_check(f == 1); //UNKNOWN!
+
+  signed char d = -g;
+  __goblint_check(d == 1); //UNKNOWN!
+
+  return 0;
+
+}