Categorize exp options

conf/incremental.json

@@ -9,6 +9,9 @@
     },
     "opt": {
       "hashcons": false
+    },
+    "base": {
+      "privatization": "none"
     }
   },
   "incremental": {
@@ -19,7 +22,6 @@
   },
   "exp": {
     "earlyglobs": true,
-    "privatization": "none",
     "solver": {
       "td3": {
         "term": true,

conf/svcomp.json

@@ -1,5 +1,10 @@
 {
   "ana": {
+    "base": {
+      "partition-arrays": {
+        "enabled": true
+      }
+    },
     "sv-comp": {
       "enabled": true,
       "functions": true
@@ -26,17 +31,7 @@
     ],
     "context": {
       "widen": false
-    }
-  },
-  "exp": {
-    "witness": {
-      "id": "enumerate",
-      "unknown": false
-    },
-    "partition-arrays": {
-      "enabled": true
     },
-    "region-offsets": true,
     "malloc": {
       "wrappers": [
         "kmalloc",
@@ -58,6 +53,13 @@
       ]
     }
   },
+  "exp": {
+    "region-offsets": true,
+  },
+  "witness": {
+    "id": "enumerate",
+    "unknown": false
+  },
   "solver": "td3",
   "sem": {
     "unknown_function": {

conf/svcomp21.json

@@ -1,5 +1,10 @@
 {
   "ana": {
+    "base": {
+      "partition-arrays": {
+        "enabled": true
+      }
+    },
     "sv-comp": {
       "enabled": true,
       "functions": true
@@ -25,16 +30,7 @@
     ],
     "context": {
       "widen": false
-    }
-  },
-  "exp": {
-    "witness": {
-      "id": "enumerate"
     },
-    "partition-arrays": {
-      "enabled": true
-    },
-    "region-offsets": true,
     "malloc": {
       "wrappers": [
         "kmalloc",
@@ -52,10 +48,16 @@
       ]
     }
   },
+  "exp": {
+    "region-offsets": true
+  },
   "solver": "td3",
   "sem": {
     "unknown_function": {
       "spawn": false
     }
+  },
+  "witness": {
+    "id": "enumerate"
   }
 }

conf/svcomp22.json

@@ -1,5 +1,10 @@
 {
   "ana": {
+    "base": {
+      "partition-arrays": {
+        "enabled": true
+      }
+    },
     "sv-comp": {
       "enabled": true,
       "functions": true
@@ -25,17 +30,7 @@
     ],
     "context": {
       "widen": false
-    }
-  },
-  "exp": {
-    "witness": {
-      "id": "enumerate",
-      "unknown": false
     },
-    "partition-arrays": {
-      "enabled": true
-    },
-    "region-offsets": true,
     "malloc": {
       "wrappers": [
         "kmalloc",
@@ -53,6 +48,9 @@
       ]
     }
   },
+  "exp": {
+    "region-offsets": true
+  },
   "solver": "td3",
   "sem": {
     "unknown_function": {
@@ -61,5 +59,9 @@
     "int": {
       "signed_overflow": "assume_none"
     }
+  },
+  "witness": {
+    "id": "enumerate",
+    "unknown": false
   }
 }

conf/traces-rel.json

@@ -7,22 +7,7 @@
     },
     "exp": {
 
-    }
-  },
-  "sem": {
-    "unknown_function": {
-      "invalidate": {
-        "globals": false
-      },
-      "spawn": true
     },
-    "builtin_unreachable": {
-      "dead_code": true
-    }
-  },
-  "exp": {
-    "privatization": "mutex-meet",
-    "priv-distr-init": false,
     "malloc": {
       "wrappers": [
         "kmalloc",
@@ -43,6 +28,23 @@
         "ldv_calloc"
       ]
     },
+    "base" : {
+      "privatization": "mutex-meet"
+    }
+  },
+  "sem": {
+    "unknown_function": {
+      "invalidate": {
+        "globals": false
+      },
+      "spawn": true
+    },
+    "builtin_unreachable": {
+      "dead_code": true
+    }
+  },
+  "exp": {
+    "priv-distr-init": false,
     "solver" : {
       "td3": {
         "side_widen" : "sides-pp"

docs/artifact-descriptions/sas21.md

@@ -95,7 +95,7 @@ presented in the paper quickly.
         or
 
     * Run some of the regression tests in `tests/regression/13-privatized` by calling `./regtest.sh 13 xx` where `xx` is the number of the test. Especially `xx > 16` are interesting, these were added with the paper and highlight
-      differences between different approaches. Use the `--set exp.privatization chosenname` option to choose which thread-modular analysis to use.
+      differences between different approaches. Use the `--set ana.base.privatization chosenname` option to choose which thread-modular analysis to use.
 
 ### Outline of how the code is structured
 Lastly, we give a general outline of how code in the Goblint framework is organized:

docs/developer-guide/testing.md

@@ -20,7 +20,7 @@ Regression tests can be run with various granularity:
 
 To pass additional options to Goblint with `update_suite.rb`, use the `gobopt` environment variable, e.g.:
 ```
-gobopt='--set exp.privatization write+lock' ./scripts/update_suite.rb
+gobopt='--set ana.base.privatization write+lock' ./scripts/update_suite.rb
 ```
 
 ### Writing

src/analyses/apron/apronPriv.apron.ml

@@ -813,7 +813,7 @@ struct
     let thread x = `Right x
   end
 
-  let name () = "PerMutexMeetPrivTID(" ^ (Cluster.name ()) ^ (if GobConfig.get_bool "exp.apron.priv.must-joined" then  ",join"  else "") ^ ")"
+  let name () = "PerMutexMeetPrivTID(" ^ (Cluster.name ()) ^ (if GobConfig.get_bool "ana.apron.priv.must-joined" then  ",join"  else "") ^ ")"
 
 
   let compatible (ask:Q.ask) current must_joined other =
@@ -836,7 +836,7 @@ struct
           not @@ List.mem other (ConcDomain.ThreadSet.elements must_joined)
         with _ -> true
       in
-      not_self_read && (not (GobConfig.get_bool "exp.apron.priv.not-started") || (may_be_running ())) && (not (GobConfig.get_bool "exp.apron.priv.must-joined") || (may_not_be_joined ()))
+      not_self_read && (not (GobConfig.get_bool "ana.apron.priv.not-started") || (may_be_running ())) && (not (GobConfig.get_bool "ana.apron.priv.must-joined") || (may_not_be_joined ()))
     | _ -> true
 
   let get_relevant_writes (ask:Q.ask) m v =
@@ -1166,7 +1166,7 @@ end
 let priv_module: (module S) Lazy.t =
   lazy (
     let module Priv: S =
-      (val match get_string "exp.apron.privatization" with
+      (val match get_string "ana.apron.privatization" with
          | "dummy" -> (module Dummy : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
@@ -1176,7 +1176,7 @@ let priv_module: (module S) Lazy.t =
          | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2)))
          | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ArbitraryCluster (ClusteringMax)))
          | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (ClusteringPower)))
-         | _ -> failwith "exp.apron.privatization: illegal value"
+         | _ -> failwith "ana.apron.privatization: illegal value"
       )
     in
     let module Priv = TracingPriv (Priv)  in

src/analyses/base.ml

@@ -1293,7 +1293,7 @@ struct
       in
       let effect_on_array arr st =
         let v = CPA.find arr st in
-        let nval = VD.affect_move ~replace_with_const:(get_bool ("exp.partition-arrays.partition-by-const-on-return")) a v x (fun _ -> None) in (* Having the function for movement return None here is equivalent to forcing the partitioning to be dropped *)
+        let nval = VD.affect_move ~replace_with_const:(get_bool ("ana.base.partition-arrays.partition-by-const-on-return")) a v x (fun _ -> None) in (* Having the function for movement return None here is equivalent to forcing the partitioning to be dropped *)
         update_variable arr arr.vtype nval st
       in
       { st with cpa = List.fold_left (fun x y -> effect_on_array y x) st.cpa affected_arrays }
@@ -2236,7 +2236,7 @@ struct
         match lv with
         | Some lv ->
           let heap_var =
-            if (get_bool "exp.malloc.fail")
+            if (get_bool "sem.malloc.fail")
             then AD.join (AD.from_var (heap_var ctx)) AD.null_ptr
             else AD.from_var (heap_var ctx)
           in
@@ -2250,7 +2250,7 @@ struct
         | Some lv -> (* array length is set to one, as num*size is done when turning into `Calloc *)
           let heap_var = heap_var ctx in
           let add_null addr =
-            if get_bool "exp.malloc.fail"
+            if get_bool "sem.malloc.fail"
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
             else addr in
           (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)

src/analyses/basePriv.ml

@@ -1382,7 +1382,7 @@ struct
     (* LVH.iter (fun (l, x) v ->
         ignore (Pretty.printf "%a %a = %a\n" CilType.Location.pretty l d_varinfo x VD.pretty v)
       ) lvh; *)
-    Marshal.output f ({name = get_string "exp.privatization"; results = lvh}: result);
+    Marshal.output f ({name = get_string "ana.base.privatization"; results = lvh}: result);
     close_out_noerr f
 
   let finalize () =
@@ -1497,7 +1497,7 @@ end
 let priv_module: (module S) Lazy.t =
   lazy (
     let module Priv: S =
-      (val match get_string "exp.privatization" with
+      (val match get_string "ana.base.privatization" with
         | "none" -> (module NonePriv: S)
         | "protection-old" -> (module ProtectionBasedOldPriv)
         | "mutex-oplus" -> (module PerMutexOplusPriv)
@@ -1512,7 +1512,7 @@ let priv_module: (module S) Lazy.t =
         | "lock" -> (module LockCenteredPriv)
         | "write" -> (module WriteCenteredPriv)
         | "write+lock" -> (module WriteAndLockCenteredPriv)
-        | _ -> failwith "exp.privatization: illegal value"
+        | _ -> failwith "ana.base.privatization: illegal value"
       )
     in
     let module Priv = PrecisionDumpPriv (Priv) in

src/analyses/libraryFunctions.ml

@@ -70,12 +70,12 @@ let classify' fn exps =
   | "mutex_lock" | "mutex_lock_interruptible" | "_write_lock" | "_raw_write_lock"
   | "pthread_rwlock_wrlock" | "GetResource" | "_raw_spin_lock"
   | "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave"
-    -> `Lock (get_bool "exp.failing-locks", true, true)
+    -> `Lock (get_bool "sem.lock.fail", true, true)
   | "pthread_mutex_lock" | "__pthread_mutex_lock"
-    -> `Lock (get_bool "exp.failing-locks", true, false)
+    -> `Lock (get_bool "sem.lock.fail", true, false)
   | "pthread_rwlock_tryrdlock" | "pthread_rwlock_rdlock" | "_read_lock"  | "_raw_read_lock"
   | "down_read"
-    -> `Lock (get_bool "exp.failing-locks", false, true)
+    -> `Lock (get_bool "sem.lock.fail", false, true)
   | "LAP_Se_SignalSemaphore"
   | "__raw_read_unlock" | "__raw_write_unlock"  | "raw_spin_unlock"
   | "_spin_unlock" | "spin_unlock" | "_spin_unlock_irqrestore" | "_spin_unlock_bh"

src/analyses/mallocWrapperAnalysis.ml

@@ -88,7 +88,7 @@ struct
     | _ -> Queries.Result.top q
 
   let init marshal =
-    List.iter (fun wrapper -> Hashtbl.replace wrappers wrapper ()) (get_string_list "exp.malloc.wrappers");
+    List.iter (fun wrapper -> Hashtbl.replace wrappers wrapper ()) (get_string_list "ana.malloc.wrappers");
     NodeVarinfoMap.unmarshal marshal
 
   let finalize () =

src/analyses/malloc_null.ml

@@ -229,7 +229,7 @@ struct
   let exitstate  v = D.empty ()
 
   let init marshal =
-    set_bool "exp.malloc.fail" true;
+    set_bool "sem.malloc.fail" true;
     return_addr_ :=  Addr.from_var (Goblintutil.create_var @@ makeVarinfo false "RETURN" voidType)
 end
 

src/cdomains/arrayDomain.ml

@@ -306,7 +306,7 @@ struct
       (Expp.top(), (r, r, r)))
     else
       normalize @@
-      let use_last = get_string "exp.partition-arrays.keep-expr" = "last" in
+      let use_last = get_string "ana.base.partition-arrays.keep-expr" = "last" in
       let exp_value e =
         match e with
         | `Lifted e' ->
@@ -463,7 +463,7 @@ struct
     | `Lifted e1e, `Lifted e2e when Basetype.CilExp.equal e1e e2e ->
       (e1, (op xl1 xl2, op xm1 xm2, op xr1 xr2))
     | `Lifted e1e, `Lifted e2e ->
-      if get_string "exp.partition-arrays.keep-expr" = "last" || get_bool "exp.partition-arrays.smart-join" then
+      if get_string "ana.base.partition-arrays.keep-expr" = "last" || get_bool "ana.base.partition-arrays.smart-join" then
         let op = Val.join in (* widen between different components isn't called validly *)
         let over_all_x1 = op (op xl1 xm1) xr1 in
         let over_all_x2 = op (op xl2 xm2) xr2 in
@@ -729,9 +729,9 @@ struct
   let update_length newl x = unop_to_t (P.update_length newl) (T.update_length newl) x
 
   (* Functions that make use of the configuration flag *)
-  let name () = "FlagConfiguredArrayDomain: " ^ if get_bool "exp.partition-arrays.enabled" then P.name () else T.name ()
+  let name () = "FlagConfiguredArrayDomain: " ^ if get_bool "ana.base.partition-arrays.enabled" then P.name () else T.name ()
 
-  let partition_enabled () = get_bool "exp.partition-arrays.enabled"
+  let partition_enabled () = get_bool "ana.base.partition-arrays.enabled"
 
   let bot () =
     if partition_enabled () then

src/cdomains/arrayDomain.mli

@@ -76,4 +76,4 @@ module PartitionedWithLength (Val: LatticeWithSmartOps) (Idx:IntDomain.Z): S wit
 (** Like partitioned but additionally manages the length of the array. *)
 
 module FlagConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t
-(** Switches between PartitionedWithLength and TrivialWithLength based on the value of exp.partition-arrays. *)
+(** Switches between PartitionedWithLength and TrivialWithLength based on the value of ana.base.partition-arrays. *)