Sparsification of Affine Equality Matrix

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -14,15 +14,15 @@ include RelationAnalysis
 
 (* There are two versions of the affeq domain.
    1. Sparse without side effects
-   2. Array with 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 --enable ana.affeq.side_effects option is set *)
+   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.side_effects" then
-      (module AffineEqualityDomainSideEffects.D2 (ArrayVector) (ArrayMatrix))
-    else
+    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 =

src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml

@@ -30,7 +30,7 @@ sig
   val append_matrices: t -> t -> t
 end
 
-(** Some functions inside have the suffix _with, which means that the function has side effects. *)
+(** Some functions inside have the suffix _with, which means that the function is not purely functional. *)
 module type ArrayMatrixFunctor =
   functor (A: RatOps) (V: ArrayVectorFunctor) ->
   sig
@@ -40,7 +40,8 @@ module type ArrayMatrixFunctor =
 (** Array-based matrix implementation.
     It provides a normalization function to reduce a matrix into reduced row echelon form.
     Operations exploit that the input matrix/matrices are in reduced row echelon form already. *)
-(* The functions that have the suffix _with have side effects and were used in a previous version of the affineEqualityDomain.
+(* The functions that have the suffix _with are not purely functional and affect the program state beyond their return value.
+    They were used in a previous version of the affineEqualityDomain.
     These calls were removed to transition to list-based matrices.*)
 module ArrayMatrix: ArrayMatrixFunctor =
   functor (A: RatOps) (V: ArrayVectorFunctor) ->
@@ -180,7 +181,7 @@ module ArrayMatrix: ArrayMatrixFunctor =
 
     let del_cols m cols = timing_wrap "del_cols" (del_cols m) cols
 
-    (* This does NOT have the same semantics (minus side effects) as map2i_with. While map2i_with can deal with m and v having different lenghts, map2i will raise Invalid_argument in that case*)
+    (* This does NOT have the same semantics as map2i_with. While map2i_with can deal with m and v having different lenghts, map2i will raise Invalid_argument in that case*)
     let map2i f m v =
       let f' x (i,y) = V.to_array @@ f i (V.of_array x) y in
       let range_array = Array.init (V.length v) Fun.id in

src/cdomains/apron/affineEqualityDomainSideEffects.apron.ml → src/cdomains/apron/affineEqualityDenseDomain.apron.ml

@@ -3,7 +3,7 @@
     @see <https://doi.org/10.1007/BF00268497> Karr, M. Affine relationships among variables of a program. *)
 
 (** There are two versions of the AffineEqualityDomain.
-    This version here is based on side effects, thus it uses Matrix and Vector functions marked with "_with" which use side effects.
+    This version here is based on a dense implementation that is not purely functional, thus it uses Matrix and Vector functions marked with "_with".
     Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment.
     Matrices are modeled as proposed by Karr: Each variable is assigned to a column and each row represents a linear affine relationship that must hold at the corresponding program point.
     The apron environment is hereby used to organize the order of columns and variables. *)

src/config/options.schema.json

@@ -1203,11 +1203,11 @@
           "title": "ana.affeq",
           "type": "object",
           "properties": {
-            "side_effects": {
-              "title": "ana.affeq.side_effects",
-              "description": "Use side effect Affine Equality analysis (array implementation). Default is false (sparse implementation)",
+            "sparse": {
+              "title": "ana.affeq.sparse",
+              "description": "Use sparse implementation of Affine Equality analysis (using lists). If set to false, the dense version is used (using arrays). Default is true (sparse implementation)",
               "type": "boolean",
-              "default": false
+              "default": true
             }
           },
           "additionalProperties": false

src/dune

@@ -35,9 +35,9 @@
       (apron -> affineEqualityDomain.apron.ml)
       (-> affineEqualityDomain.no-apron.ml)
     )
-    (select affineEqualityDomainSideEffects.ml from
-      (apron -> affineEqualityDomainSideEffects.apron.ml)
-      (-> affineEqualityDomainSideEffects.no-apron.ml)
+    (select affineEqualityDenseDomain.ml from
+      (apron -> affineEqualityDenseDomain.apron.ml)
+      (-> affineEqualityDenseDomain.no-apron.ml)
     )
     (select linearTwoVarEqualityAnalysis.ml from
       (apron -> linearTwoVarEqualityAnalysis.apron.ml)

src/goblint_lib.ml

@@ -260,7 +260,7 @@ module ValueDomainQueries = ValueDomainQueries
 module RelationDomain = RelationDomain
 module ApronDomain = ApronDomain
 module AffineEqualityDomain = AffineEqualityDomain
-module AffineEqualityDomainSideEffects = AffineEqualityDomainSideEffects
+module AffineEqualityDomainDense = AffineEqualityDenseDomain
 module LinearTwoVarEqualityDomain = LinearTwoVarEqualityDomain
 
 (** {3 Concurrency} *)