Merge pull request #1208 from goblint/string-unit-domain

Add `ana.base.strings.domain` option and unit string 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.ml

@@ -5,6 +5,7 @@ open IntOps
 
 module M = Messages
 module Mval_outer = Mval
+module SD = StringDomain
 
 
 module AddressBase (Mval: Printable.S) =
@@ -14,23 +15,14 @@ struct
     | Addr of Mval.t
     | NullPtr
     | UnknownPtr
-    | StrPtr of string option
+    | StrPtr of SD.t
   [@@deriving eq, ord, hash] (* TODO: StrPtr equal problematic if the same literal appears more than once *)
 
   let name () = Format.sprintf "address (%s)" (Mval.name ())
 
-  let hash x = match x with
-    | StrPtr _ ->
-      if GobConfig.get_bool "ana.base.limit-string-addresses" then
-        13859
-      else
-        hash x
-    | _ -> hash x
-
   let show = function
     | Addr m -> Mval.show m
-    | StrPtr (Some x)   -> "\"" ^ x ^ "\""
-    | StrPtr None -> "(unknown string)"
+    | StrPtr s   -> StringDomain.show s
     | UnknownPtr -> "?"
     | NullPtr    -> "NULL"
 
@@ -42,31 +34,18 @@ struct
     )
 
   (* strings *)
-  let of_string x = StrPtr (Some x)
+  let of_string x = StrPtr (SD.of_string x)
   let to_string = function
-    | StrPtr (Some x) -> Some x
+    | StrPtr s -> SD.to_string s
     | _        -> None
-  (* only keep part before first null byte *)
   let to_c_string = function
-    | StrPtr (Some x) ->
-      begin match String.split_on_char '\x00' x with
-        | s::_ -> Some s
-        | [] -> None
-      end
+    | StrPtr s -> SD.to_c_string s
     | _ -> None
-  let to_n_c_string n x =
-    match to_c_string x with
-    | Some x ->
-      if n > String.length x then
-        Some x
-      else if n < 0 then
-        None
-      else
-        Some (String.sub x 0 n)
+  let to_n_c_string n = function
+    | StrPtr s -> SD.to_n_c_string n s
     | _ -> None
-  let to_string_length x =
-    match to_c_string x with
-    | Some x -> Some (String.length x)
+  let to_string_length = function
+    | StrPtr s -> SD.to_string_length s
     | _ -> None
 
   let arbitrary () = QCheck.always UnknownPtr (* S TODO: non-unknown *)
@@ -101,8 +80,7 @@ struct
   (* TODO: seems to be unused *)
   let to_exp = function
     | Addr m -> AddrOf (Mval.to_cil m)
-    | StrPtr (Some x) -> mkString x
-    | StrPtr None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.")
+    | StrPtr s -> SD.to_exp s
     | NullPtr -> integer 0
     | UnknownPtr -> raise Lattice.TopValue
   (* TODO: unused *)
@@ -123,9 +101,7 @@ struct
 
   let semantic_equal x y = match x, y with
     | Addr x, Addr y -> Mval.semantic_equal x y
-    | StrPtr None, StrPtr _
-    | StrPtr _, StrPtr None -> Some true
-    | StrPtr (Some a), StrPtr (Some b) -> if a = b then None else Some false
+    | StrPtr s1, StrPtr s2 -> SD.semantic_equal s1 s2
     | NullPtr, NullPtr -> Some true
     | UnknownPtr, UnknownPtr
     | UnknownPtr, Addr _
@@ -135,35 +111,14 @@ struct
     | _, _ -> Some false
 
   let leq x y = match x, y with
-    | StrPtr _, StrPtr None -> true
-    | StrPtr a, StrPtr b   -> a = b
+    | StrPtr s1, StrPtr s2   -> SD.leq s1 s2
     | Addr x, Addr y -> Mval.leq x y
     | _                      -> x = y
 
   let top_indices = function
     | Addr x -> Addr (Mval.top_indices x)
     | 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 *) ->
-      if GobConfig.get_bool "ana.base.limit-string-addresses" then
-        raise Lattice.BotValue
-      else
-        raise Lattice.Uncomparable
-
   let merge mop sop x y =
     match x, y with
     | UnknownPtr, UnknownPtr -> UnknownPtr
@@ -172,10 +127,10 @@ struct
     | Addr x, Addr y -> Addr (mop x y)
     | _ -> raise Lattice.Uncomparable
 
-  let join = merge Mval.join join_string_ptr
-  let widen = merge Mval.widen join_string_ptr
-  let meet = merge Mval.meet meet_string_ptr
-  let narrow = merge Mval.narrow meet_string_ptr
+  let join = merge Mval.join SD.join
+  let widen = merge Mval.widen SD.join
+  let meet = merge Mval.meet SD.meet
+  let narrow = merge Mval.narrow SD.meet
 
   include Lattice.NoBotTop
 
@@ -194,8 +149,7 @@ struct
 
     let of_elt (x: elt): t = match x with
       | Addr (v, o) -> Addr v
-      | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
-      | StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *)
+      | StrPtr s -> StrPtr (SD.repr s)
       | NullPtr -> NullPtr
       | UnknownPtr -> UnknownPtr
   end
@@ -211,8 +165,7 @@ struct
 
     let of_elt (x: elt): t = match x with
       | Addr (v, o) -> Addr (v, Offset.Unit.of_offs o) (* addrs grouped by var and part of offset *)
-      | StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
-      | StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *)
+      | StrPtr s -> StrPtr (SD.repr s)
       | NullPtr -> NullPtr
       | UnknownPtr -> UnknownPtr
   end

src/cdomains/addressDomain_intf.ml

@@ -7,7 +7,7 @@ sig
       | Addr of Mval.t (** Pointer to mvalue. *)
       | NullPtr (** NULL pointer. *)
       | UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *)
-      | StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *)
+      | StrPtr of StringDomain.t (** String literal pointer. [StrPtr None] abstracts any string pointer *)
     include Printable.S with type t := t (** @closed *)
 
     val of_string: string -> t
@@ -16,8 +16,6 @@ sig
     val to_string: t -> string option
     (** Convert {!StrPtr} to string if possible. *)
 
-    (** C strings are different from OCaml strings as they are not processed after the first [NUL] byte, even though the OCaml string (and a C string literal) may be longer. *)
-
     val to_c_string: t -> string option
     (** Convert {!StrPtr} to C string if possible. *)
 
@@ -71,7 +69,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

@@ -0,0 +1,114 @@
+include Printable.StdLeaf
+
+let name () = "string"
+
+type string_domain = Unit | Disjoint | Flat
+
+let string_domain: string_domain ResettableLazy.t =
+  ResettableLazy.from_fun (fun () ->
+      match GobConfig.get_string "ana.base.strings.domain" with
+      | "unit" -> Unit
+      | "disjoint" -> Disjoint
+      | "flat" -> Flat
+      | _ -> failwith "ana.base.strings.domain: illegal value"
+    )
+
+let get_string_domain () = ResettableLazy.force string_domain
+
+let reset_lazy () =
+  ResettableLazy.reset string_domain
+
+
+type t = string option [@@deriving eq, ord, hash]
+
+let hash x =
+  if get_string_domain () = Disjoint then
+    hash x
+  else
+    13859
+
+let show = function
+  | Some x -> "\"" ^ x ^ "\""
+  | None -> "(unknown string)"
+
+include Printable.SimpleShow (
+  struct
+    type nonrec t = t
+    let show = show
+  end
+  )
+
+let of_string x =
+  if get_string_domain () = Unit then
+    None
+  else
+    Some x
+let to_string x = x
+
+(* only keep part before first null byte *)
+let to_c_string = function
+  | Some x ->
+    begin match String.split_on_char '\x00' x with
+      | s::_ -> Some s
+      | [] -> None
+    end
+  | None -> None
+
+let to_n_c_string n x =
+  match to_c_string x with
+  | Some x ->
+    if n > String.length x then
+      Some x
+    else if n < 0 then
+      None
+    else
+      Some (String.sub x 0 n)
+  | None -> None
+
+let to_string_length x =
+  match to_c_string x with
+  | Some x -> Some (String.length x)
+  | None -> None
+
+let to_exp = function
+  | Some x -> GoblintCil.mkString x
+  | None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.")
+
+let semantic_equal x y =
+  match x, y with
+  | None, _
+  | _, None -> Some true
+  | Some a, Some b -> if a = b then None else Some false
+
+let leq x y =
+  match x, y with
+  | _, None -> true
+  | a, b   -> a = b
+
+let join 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 get_string_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 get_string_domain () = Disjoint then
+      raise Lattice.Uncomparable
+    else
+      raise Lattice.BotValue
+
+let repr x =
+  if get_string_domain () = Disjoint then
+    x (* everything else is kept separate, including strings if not limited *)
+  else
+    None (* all strings together if limited *)

src/cdomains/stringDomain.mli

@@ -0,0 +1,40 @@
+(** String literals domain. *)
+
+include Printable.S
+
+val reset_lazy: unit -> unit
+(** Reset the cached configuration of the string domain. *)
+
+val of_string: string -> t
+(** Convert from string. *)
+
+val to_string: t -> string option
+(** Convert to string if possible. *)
+
+(** C strings are different from OCaml strings as they are not processed after the first [NUL] byte, even though the OCaml string (and a C string literal) may be longer. *)
+
+val to_c_string: t -> string option
+(** Convert to C string if possible. *)
+
+val to_n_c_string: int -> t -> string option
+(** Convert to C string of given maximum length if possible. *)
+
+val to_string_length: t -> int option
+(** Find length of C string if possible. *)
+
+val to_exp: t -> GoblintCil.exp
+(** Convert to CIL expression. *)
+
+val semantic_equal: t -> t -> bool option
+(** Check semantic equality of two strings.
+
+    @return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *)
+
+(** Some {!Lattice.S} operations. *)
+
+val leq: t -> t -> bool
+val join: t -> t -> t
+val meet: t -> t -> t
+
+val repr : t -> t
+(** Representative for address lattice. *)

src/common/util/options.schema.json

@@ -655,11 +655,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",

src/goblint_lib.ml

@@ -213,6 +213,7 @@ module FloatDomain = FloatDomain
 
 module Mval = Mval
 module Offset = Offset
+module StringDomain = StringDomain
 module AddressDomain = AddressDomain
 
 (** {5 Complex} *)