Merge pull request #1625 from CopperCableIsolator/master

Sparsification of Affine Equality Matrix

Author: DrMichaelPetter

dune-project

@@ -1,4 +1,4 @@
-(lang dune 3.7)
+(lang dune 3.13)
 (using dune_site 0.1)
 (cram enable)
 (name goblint)

goblint.opam

@@ -35,7 +35,7 @@ homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
-  "dune" {>= "3.7"}
+  "dune" {>= "3.13"}
   "ocaml" {>= "4.14"}
   "goblint-cil" {>= "2.0.5"}
   "batteries" {>= "3.5.1"}

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -4,11 +4,30 @@
 
 open Analyses
 
+open SparseVector
+open ListMatrix
+
+open ArrayVector
+open ArrayMatrix
+
 include RelationAnalysis
 
+(* There are two versions of the affeq domain.
+   1. Sparse without side effects
+   2. Dense Array with side effects
+   Default: sparse implementation
+   The array implementation with side effects of the affeq domain is used when the --disable ana.affeq.sparse option is set *)
+let get_domain: (module RelationDomain.RD) Lazy.t =
+  lazy (
+    if GobConfig.get_bool "ana.affeq.sparse" then
+      (module AffineEqualityDomain.D2 (SparseVector) (ListMatrix))
+    else
+      (module AffineEqualityDenseDomain.D2 (ArrayVector) (ArrayMatrix))
+  )
+
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
-    let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
+    let module AD = (val Lazy.force get_domain) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct