Change ana.base.limit-string-addresses to ana.base.strings.domain

conf/examples/very-precise.json

@@ -61,7 +61,9 @@
       "structs" : {
         "domain" : "combined-sk"
       },
-      "limit-string-addresses": false
+      "strings": {
+        "domain": "disjoint"
+      }
     }
   },
   "exp": {

src/cdomains/addressDomain_intf.ml

@@ -71,7 +71,7 @@ sig
       - Each {!Addr}, modulo precise index expressions in the offset, is a sublattice with ordering induced by {!Mval}.
       - {!NullPtr} is a singleton sublattice.
       - {!UnknownPtr} is a singleton sublattice.
-      - If [ana.base.limit-string-addresses] is enabled, then all {!StrPtr} are together in one sublattice with flat ordering. If [ana.base.limit-string-addresses] is disabled, then each {!StrPtr} is a singleton sublattice. *)
+      - If [ana.base.strings.domain] is disjoint, then each {!StrPtr} is a singleton sublattice. Otherwise, all {!StrPtr} are together in one sublattice with flat ordering. *)
   module AddressLattice (Mval: Mval.Lattice):
   sig
     include module type of AddressPrintable (Mval)

src/cdomains/stringDomain.ml

@@ -1,10 +1,10 @@
 type t = string option [@@deriving eq, ord, hash]
 
 let hash x =
-  if GobConfig.get_bool "ana.base.limit-string-addresses" then
-    13859
-  else
+  if GobConfig.get_string "ana.base.strings.domain" = "disjoint" then
     hash x
+  else
+    13859
 
 let show = function
   | Some x -> "\"" ^ x ^ "\""
@@ -17,7 +17,11 @@ include Printable.SimpleShow (
   end
   )
 
-let of_string x = Some x
+let of_string x =
+  if GobConfig.get_string "ana.base.strings.domain" = "unit" then
+    None
+  else
+    Some x
 let to_string x = x
 
 (* only keep part before first null byte *)
@@ -66,24 +70,24 @@ let join x y =
   | _, None -> None
   | Some a, Some b when a = b -> Some a
   | Some a, Some b (* when a <> b *) ->
-    if GobConfig.get_bool "ana.base.limit-string-addresses" then
-      None
-    else
+    if GobConfig.get_string "ana.base.strings.domain" = "disjoint" then
       raise Lattice.Uncomparable
+    else
+      None
 
 let meet x y =
   match x, y with
   | None, a
   | a, None -> a
   | Some a, Some b when a = b -> Some a
   | Some a, Some b (* when a <> b *) ->
-    if GobConfig.get_bool "ana.base.limit-string-addresses" then
-      raise Lattice.BotValue
-    else
+    if GobConfig.get_string "ana.base.strings.domain" = "disjoint" then
       raise Lattice.Uncomparable
+    else
+      raise Lattice.BotValue
 
 let repr x =
-  if GobConfig.get_bool "ana.base.limit-string-addresses" then
-    None (* all strings together if limited *)
-  else
+  if GobConfig.get_string "ana.base.strings.domain" = "disjoint" then
     x (* everything else is kept separate, including strings if not limited *)
+  else
+    None (* all strings together if limited *)

src/util/options.schema.json

@@ -619,11 +619,19 @@
               },
               "additionalProperties": false
             },
-            "limit-string-addresses": {
-              "title": "ana.base.limit-string-addresses",
-              "description": "Limit abstract address sets to keep at most one distinct string pointer.",
-              "type": "boolean",
-              "default": true
+            "strings": {
+              "title": "ana.base.strings",
+              "type": "object",
+              "properties": {
+                "domain": {
+                  "title": "ana.base.strings.domain",
+                  "description": "Domain for string literals.",
+                  "type": "string",
+                  "enum": ["unit", "flat", "disjoint"],
+                  "default": "flat"
+                }
+              },
+              "additionalProperties": false
             },
             "partition-arrays": {
               "title": "ana.base.partition-arrays",

tests/regression/02-base/88-string-ptrs-limited.c

@@ -1,4 +1,4 @@
-//PARAM: --enable ana.base.limit-string-addresses
+//PARAM: --set ana.base.strings.domain flat
 #include <stdlib.h>
 #include <goblint.h>
 

tests/regression/02-base/89-string-ptrs-not-limited.c

@@ -1,4 +1,4 @@
-//PARAM: --disable ana.base.limit-string-addresses
+//PARAM: --set ana.base.strings.domain disjoint
 #include <stdlib.h>
 #include <goblint.h>
 

tests/regression/73-strings/01-string_literals.c

@@ -1,4 +1,4 @@
-// PARAM: --disable ana.base.limit-string-addresses --enable ana.int.interval
+// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval
 
 #include <goblint.h>
 #include <string.h>
@@ -21,7 +21,7 @@ int main() {
     char* s1 = "abcde";
     char* s2 = "abcdfg";
     char* s3 = hello_world();
-    
+
     int i = strlen(s1);
     __goblint_check(i == 5);
 
@@ -96,10 +96,10 @@ int main() {
         #define STRNCAT strncat(s1, "hi", 1)
     #endif
     STRNCAT; // WARN
-        
+
     #ifdef __APPLE__
         // do nothing => no warning
-    #else  
+    #else
         char s4[] = "hello";
         strcpy(s4, s2); // NOWARN
         strncpy(s4, s3, 2); // NOWARN

tests/regression/73-strings/02-string_literals_with_null.c

@@ -1,4 +1,4 @@
-// PARAM: --disable ana.base.limit-string-addresses --enable ana.int.interval
+// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval
 
 #include <goblint.h>
 #include <string.h>

tests/regression/73-strings/03-string_basics.c

@@ -1,4 +1,4 @@
-// PARAM: --disable ana.base.limit-string-addresses --enable ana.int.interval
+// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval
 
 #include <goblint.h>
 #include <string.h>

tests/regression/73-strings/05-string-unit-domain.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.base.limit-string-addresses
+// PARAM: --set ana.base.strings.domain unit
 #include <string.h>
 #include <goblint.h>