New Analysis combining Linear Two-Variable Equalities with other domains

conf/svcomp25_testing.json

@@ -0,0 +1,123 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "lin2vareq_p"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "lin2vareq_p": {
+      "inequalities" : "coeffs_threshold"
+    },
+    "autotune": {
+      "enabled": false,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ],
+      "extraTerminationDomain": "lin2vareq_p"
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

conf/svcomp25_testing2.json

@@ -0,0 +1,119 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "lin2vareq"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": false,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.apron.ml

@@ -0,0 +1,40 @@
+(** {{!RelationAnalysis} Relational integer value analysis} using an OCaml implementation of the linear two-variable equalities domain ([lin2vareq]).
+
+    @see <http://doi.acm.org/10.1145/2049706.2049710> A. Flexeder, M. Petter, and H. Seidl Fast Interprocedural Linear Two-Variable Equalities. *)
+
+open Analyses
+include RelationAnalysis
+
+module NoIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.NoInequalties)
+module PentagonIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.PentagonCoeffs))
+module PentagonOffsetIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.PentagonOffsetCoeffs))
+module FullIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.TwoVarInequalitySet))
+
+let spec_module: (module MCPSpec) Lazy.t =
+  lazy (
+    let (module AD) = match GobConfig.get_string "ana.lin2vareq_p.inequalities" with 
+      | "none" -> (module NoIneq : RelationDomain.RD)
+      | "pentagon" -> (module PentagonIneq : RelationDomain.RD)
+      | "pentagon_offset" -> (module PentagonOffsetIneq : RelationDomain.RD)
+      | _ ->  (module FullIneq : RelationDomain.RD) (*Other options differ only in the limit function*)
+    in
+    let module Priv = (val RelationPriv.get_priv ()) in
+    let module Spec =
+    struct
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
+      let name () = "lin2vareq_p"
+    end
+    in
+    (module Spec)
+  )
+
+let get_spec (): (module MCPSpec) =
+  Lazy.force spec_module
+
+let after_config () =
+  let module Spec = (val get_spec ()) in
+  MCP.register_analysis (module Spec : MCPSpec);
+  GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
+
+let _ =
+  AfterConfig.register after_config

src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.no-apron.ml

@@ -0,0 +1,3 @@
+(* This analysis is empty on purpose. It serves only as an alternative dependency
+   in cases where the actual domain can't be used because of a missing library.
+   It was added because we don't want to fully depend on Apron. *)

src/autoTune.ml

@@ -248,12 +248,12 @@ let focusOnMemSafetySpecification () =
 let focusOnTermination (spec: Svcomp.Specification.t) =
   match spec with
   | Termination ->
-    let terminationAnas = ["threadflag"; "apron"] in
+    let terminationAnas = ["threadflag"; get_string "ana.autotune.extraTerminationDomain"] in
     enableAnalyses "Specification: Termination" "termination analyses" terminationAnas;
     set_string "sem.int.signed_overflow" "assume_none";
     set_bool "ana.int.interval" true;
-    set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
-    ()
+    if get_string "ana.autotune.extraTerminationDomain" = "apron" then 
+      set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
   | _ -> ()
 
 let focusOnTermination () =

src/cdomain/value/cdomains/int/congruenceDomain.ml

@@ -1,8 +1,11 @@
 open IntDomain0
 open GoblintCil
 
+module type Norm = sig
+  val normalize : ikind -> (Z.t * Z.t) option -> (Z.t * Z.t) option
+end
 
-module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option =
+module CongruenceFunctor (Norm : Norm): S with type int_t = Z.t and type t = (Z.t * Z.t) option =
 struct
   let name () = "congruences"
   type int_t = Z.t
@@ -24,22 +27,7 @@ struct
   let ( |: ) a b =
     if a =: Z.zero then false else (b %: a) =: Z.zero
 
-  let normalize ik x =
-    match x with
-    | None -> None
-    | Some (c, m) ->
-      if m =: Z.zero then
-        if should_wrap ik then
-          Some (Size.cast ik c, m)
-        else
-          Some (c, m)
-      else
-        let m' = Z.abs m in
-        let c' = c %: m' in
-        if c' <: Z.zero then
-          Some (c' +: m', m')
-        else
-          Some (c' %: m', m')
+  let normalize = Norm.normalize
 
   let range ik = Size.range ik
 
@@ -540,3 +528,52 @@ struct
 
   let project ik p t = t
 end
+
+module Wrapping : Norm = struct
+
+  let (%:) = Z.rem
+  let (=:) = Z.equal
+  let (+:) = Z.add
+  let (<:) x y = Z.compare x y < 0
+
+  let normalize ik x =
+    match x with
+    | None -> None
+    | Some (c, m) ->
+      if m =: Z.zero then
+        if should_wrap ik then
+          Some (Size.cast ik c, m)
+        else
+          Some (c, m)
+      else
+        let m' = Z.abs m in
+        let c' = c %: m' in
+        if c' <: Z.zero then
+          Some (c' +: m', m')
+        else
+          Some (c' %: m', m')
+end
+
+module NoWrapping : Norm = struct
+
+  let (%:) = Z.rem
+  let (=:) = Z.equal
+  let (+:) = Z.add
+  let (<:) x y = Z.compare x y < 0
+
+  let normalize ik x =
+    match x with
+    | None -> None
+    | Some (c, m) ->
+      if m =: Z.zero then
+        Some (c, m)
+      else
+        let m' = Z.abs m in
+        let c' = c %: m' in
+        if c' <: Z.zero then
+          Some (c' +: m', m')
+        else
+          Some (c' %: m', m')
+end
+
+module Congruence = CongruenceFunctor(Wrapping)