Limit address sets to include at most one string pointer

src/cdomains/lval.ml

@@ -183,7 +183,7 @@ struct
     | Addr of CilType.Varinfo.t * Offs.t (** Pointer to offset of a variable. *)
     | NullPtr (** NULL pointer. *)
     | UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *)
-    | StrPtr of string option (** String literal pointer. *)
+    | StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *)
   [@@deriving eq, ord, hash] (* TODO: StrPtr equal problematic if the same literal appears more than once *)
 
   let hash x = match x with
@@ -328,10 +328,14 @@ struct
     | None, _
     | _, None -> None
     | Some a, Some b when a = b -> Some a
-    | Some a, Some b (* when a <> b *) -> None
+    | Some a, Some b (* when a <> b *) ->
+      if GobConfig.get_bool "ana.base.limit-string-addresses" then
+        None
+      else
+        raise Lattice.Uncomparable
 
   let meet_string_ptr x y = match x, y with
-    | None, a -> a
+    | None, a
     | a, None -> a
     | Some a, Some b when a = b -> Some a
     | Some a, Some b (* when a <> b *) -> raise Lattice.Uncomparable

src/util/options.schema.json

@@ -606,6 +606,11 @@
               },
               "additionalProperties": false
             },
+            "limit-string-addresses": {
+              "title": "ana.base.limit-string-addresses",
+              "type": "boolean",
+              "default": true
+            },
             "partition-arrays": {
               "title": "ana.base.partition-arrays",
               "type": "object",

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

@@ -1,6 +1,8 @@
-#include <assert.h>
+//PARAM: --enable ana.base.limit-string-addresses
 #include <stdlib.h>
 
+char *unknown_function();
+
 int main(){
     char* str = "Hello";
     char* str2 = "Hello";
@@ -21,15 +23,15 @@ int main(){
     } else {
         ptr = str3;
     }
-    __goblint_check(*ptr == *str); //UNKNOWN
+    __goblint_check(ptr == str); //UNKNOWN!
 
     // This is unknwon due to only keeping one string pointer in abstract address sets
-    __goblint_check(*ptr == *str4); //UNKNOWN
+    __goblint_check(ptr != str4); //UNKNOWN
 
-    char *ptr2 = unknown_function(); 
+    char *ptr2 = unknown_function();
 
-    __goblint_check(ptr == ptr2); //UNKNOWN
-    __goblint_check(ptr2 == str); //UNKNOWN
+    __goblint_check(ptr2 == str); //UNKNOWN!
+    __goblint_check(ptr2 == ptr); //UNKNOWN!
 
     return 0;
 }

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

@@ -0,0 +1,36 @@
+//PARAM: --disable ana.base.limit-string-addresses
+#include <stdlib.h>
+
+char *unknown_function();
+
+int main(){
+    char* str = "Hello";
+    char* str2 = "Hello";
+    char* str3 = "hi";
+    char* str4 = "other string";
+
+    // Unknown since the there may be multiple copies of the same string
+    __goblint_check(str != str2); // UNKNOWN!
+
+    __goblint_check(str == str);
+    __goblint_check(str != str3);
+
+    char *ptr = NULL;
+    int top = rand();
+
+    if(top){
+        ptr = str2;
+    } else {
+        ptr = str3;
+    }
+    __goblint_check(ptr == str); //UNKNOWN!
+
+    __goblint_check(ptr != str4);
+
+    char *ptr2 = unknown_function();
+
+    __goblint_check(ptr2 == str); //UNKNOWN!
+    __goblint_check(ptr2 == ptr); //UNKNOWN!
+
+    return 0;
+}