Merge pull request #808 from goblint/limit_string_pointers

Limit address sets to include at most one string pointer

Author: michael-schwarz

conf/examples/very-precise.json

@@ -55,7 +55,8 @@
       },
       "structs" : {
         "domain" : "combined-sk"
-      }
+      },
+      "limit-string-addresses": false
     }
   },
   "exp": {

src/cdomains/lval.ml

@@ -178,12 +178,22 @@ struct
   type field = fieldinfo
   type idx = Idx.t
   module Offs = OffsetPrintable (Idx)
+
   type t =
     | 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 (** 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
+    | StrPtr _ ->
+      if GobConfig.get_bool "ana.base.limit-string-addresses" then
+        13859
+      else
+        hash x
+    | _ -> hash x
+
   include Printable.Std
   let name () = "Normal Lvals"
 
@@ -210,9 +220,9 @@ struct
     | _      -> None
 
   (* strings *)
-  let from_string x = StrPtr x
+  let from_string x = StrPtr (Some x)
   let to_string = function
-    | StrPtr x -> Some x
+    | StrPtr (Some x) -> Some x
     | _        -> None
 
   let rec short_offs = function
@@ -228,7 +238,8 @@ struct
 
   let show = function
     | Addr (x, o)-> short_addr (x, o)
-    | StrPtr x   -> "\"" ^ x ^ "\""
+    | StrPtr (Some x)   -> "\"" ^ x ^ "\""
+    | StrPtr None -> "(unknown string)"
     | UnknownPtr -> "?"
     | NullPtr    -> "NULL"
 
@@ -277,7 +288,8 @@ struct
     in
     match x with
     | Addr (v,o) -> AddrOf (Var v, to_cil o)
-    | StrPtr x -> mkString x
+    | StrPtr (Some x) -> mkString x
+    | StrPtr None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.")
     | NullPtr -> integer 0
     | UnknownPtr -> raise Lattice.TopValue
   let rec add_offsets x y = match x with
@@ -303,24 +315,46 @@ struct
   module Offs = Offset (Idx)
 
   let is_definite = function
-    | NullPtr | StrPtr _ -> true
+    | NullPtr -> true
     | Addr (v,o) when Offs.is_definite o -> true
     | _ -> false
 
   let leq x y = match x, y with
-    | StrPtr a  , StrPtr b   -> a = b
+    | StrPtr _, StrPtr None -> true
+    | StrPtr a, StrPtr b   -> a = b
     | Addr (x,o), Addr (y,u) -> CilType.Varinfo.equal x y && Offs.leq o u
     | _                      -> x = y
 
   let drop_ints = function
     | Addr (x, o) -> Addr (x, Offs.drop_ints o)
     | x -> x
 
+  let join_string_ptr x y = match x, y with
+    | None, _
+    | _, 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
+        raise Lattice.Uncomparable
+
+  let meet_string_ptr 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 *) -> raise Lattice.Uncomparable
+
   let merge cop x y =
     match x, y with
     | UnknownPtr, UnknownPtr -> UnknownPtr
     | NullPtr   , NullPtr -> NullPtr
-    | StrPtr a  , StrPtr b when a=b -> StrPtr a
+    | StrPtr a, StrPtr b ->
+      StrPtr
+        begin match cop with
+          |`Join | `Widen -> join_string_ptr a b
+          |`Meet | `Narrow -> meet_string_ptr a b
+        end
     | Addr (x,o), Addr (y,u) when CilType.Varinfo.equal x y -> Addr (x, Offs.merge cop o u)
     | _ -> raise Lattice.Uncomparable
 

src/util/options.schema.json

@@ -606,6 +606,12 @@
               },
               "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
+            },
             "partition-arrays": {
               "title": "ana.base.partition-arrays",
               "type": "object",

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

@@ -0,0 +1,37 @@
+//PARAM: --enable 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!
+
+    // This is unknown due to only keeping one string pointer in abstract address sets
+    __goblint_check(ptr != str4); //UNKNOWN
+
+    char *ptr2 = unknown_function();
+
+    __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;
+}