Skip to content

Commit d5163c9

Browse files
sim642sim642
authored
Merge pull request #1208 from goblint/string-unit-domain
Add `ana.base.strings.domain` option and unit string domain
2 parents 0fdea44 + d01ef63 commit d5163c9

File tree

14 files changed

+216
-84
lines changed

14 files changed

+216
-84
lines changed

‎conf/examples/very-precise.json‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,9 @@
6161
"structs" : {
6262
"domain" : "combined-sk"
6363
},
64-
"limit-string-addresses": false
64+
"strings": {
65+
"domain": "disjoint"
66+
}
6567
}
6668
},
6769
"exp": {

‎src/cdomains/addressDomain.ml‎

Lines changed: 19 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ open IntOps
55

66
module M = Messages
77
module Mval_outer = Mval
8+
module SD = StringDomain
89

910

1011
module AddressBase (Mval: Printable.S) =
@@ -14,23 +15,14 @@ struct
1415
| Addr of Mval.t
1516
| NullPtr
1617
| UnknownPtr
17-
| StrPtr of string option
18+
| StrPtr of SD.t
1819
[@@deriving eq, ord, hash] (* TODO: StrPtr equal problematic if the same literal appears more than once *)
1920

2021
let name () = Format.sprintf "address (%s)" (Mval.name ())
2122

22-
let hash x = match x with
23-
| StrPtr _ ->
24-
if GobConfig.get_bool "ana.base.limit-string-addresses" then
25-
13859
26-
else
27-
hash x
28-
| _ -> hash x
29-
3023
let show = function
3124
| Addr m -> Mval.show m
32-
| StrPtr (Some x) -> "\"" ^ x ^ "\""
33-
| StrPtr None -> "(unknown string)"
25+
| StrPtr s -> StringDomain.show s
3426
| UnknownPtr -> "?"
3527
| NullPtr -> "NULL"
3628

@@ -42,31 +34,18 @@ struct
4234
)
4335

4436
(* strings *)
45-
let of_string x = StrPtr (Some x)
37+
let of_string x = StrPtr (SD.of_string x)
4638
let to_string = function
47-
| StrPtr (Some x) -> Some x
39+
| StrPtr s -> SD.to_string s
4840
| _ -> None
49-
(* only keep part before first null byte *)
5041
let to_c_string = function
51-
| StrPtr (Some x) ->
52-
begin match String.split_on_char '\x00' x with
53-
| s::_ -> Some s
54-
| [] -> None
55-
end
42+
| StrPtr s -> SD.to_c_string s
5643
| _ -> None
57-
let to_n_c_string n x =
58-
match to_c_string x with
59-
| Some x ->
60-
if n > String.length x then
61-
Some x
62-
else if n < 0 then
63-
None
64-
else
65-
Some (String.sub x 0 n)
44+
let to_n_c_string n = function
45+
| StrPtr s -> SD.to_n_c_string n s
6646
| _ -> None
67-
let to_string_length x =
68-
match to_c_string x with
69-
| Some x -> Some (String.length x)
47+
let to_string_length = function
48+
| StrPtr s -> SD.to_string_length s
7049
| _ -> None
7150

7251
let arbitrary () = QCheck.always UnknownPtr (* S TODO: non-unknown *)
@@ -101,8 +80,7 @@ struct
10180
(* TODO: seems to be unused *)
10281
let to_exp = function
10382
| Addr m -> AddrOf (Mval.to_cil m)
104-
| StrPtr (Some x) -> mkString x
105-
| StrPtr None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.")
83+
| StrPtr s -> SD.to_exp s
10684
| NullPtr -> integer 0
10785
| UnknownPtr -> raise Lattice.TopValue
10886
(* TODO: unused *)
@@ -123,9 +101,7 @@ struct
123101

124102
let semantic_equal x y = match x, y with
125103
| Addr x, Addr y -> Mval.semantic_equal x y
126-
| StrPtr None, StrPtr _
127-
| StrPtr _, StrPtr None -> Some true
128-
| StrPtr (Some a), StrPtr (Some b) -> if a = b then None else Some false
104+
| StrPtr s1, StrPtr s2 -> SD.semantic_equal s1 s2
129105
| NullPtr, NullPtr -> Some true
130106
| UnknownPtr, UnknownPtr
131107
| UnknownPtr, Addr _
@@ -135,35 +111,14 @@ struct
135111
| _, _ -> Some false
136112

137113
let leq x y = match x, y with
138-
| StrPtr _, StrPtr None -> true
139-
| StrPtr a, StrPtr b -> a = b
114+
| StrPtr s1, StrPtr s2 -> SD.leq s1 s2
140115
| Addr x, Addr y -> Mval.leq x y
141116
| _ -> x = y
142117

143118
let top_indices = function
144119
| Addr x -> Addr (Mval.top_indices x)
145120
| x -> x
146121

147-
let join_string_ptr x y = match x, y with
148-
| None, _
149-
| _, None -> None
150-
| Some a, Some b when a = b -> Some a
151-
| Some a, Some b (* when a <> b *) ->
152-
if GobConfig.get_bool "ana.base.limit-string-addresses" then
153-
None
154-
else
155-
raise Lattice.Uncomparable
156-
157-
let meet_string_ptr x y = match x, y with
158-
| None, a
159-
| a, None -> a
160-
| Some a, Some b when a = b -> Some a
161-
| Some a, Some b (* when a <> b *) ->
162-
if GobConfig.get_bool "ana.base.limit-string-addresses" then
163-
raise Lattice.BotValue
164-
else
165-
raise Lattice.Uncomparable
166-
167122
let merge mop sop x y =
168123
match x, y with
169124
| UnknownPtr, UnknownPtr -> UnknownPtr
@@ -172,10 +127,10 @@ struct
172127
| Addr x, Addr y -> Addr (mop x y)
173128
| _ -> raise Lattice.Uncomparable
174129

175-
let join = merge Mval.join join_string_ptr
176-
let widen = merge Mval.widen join_string_ptr
177-
let meet = merge Mval.meet meet_string_ptr
178-
let narrow = merge Mval.narrow meet_string_ptr
130+
let join = merge Mval.join SD.join
131+
let widen = merge Mval.widen SD.join
132+
let meet = merge Mval.meet SD.meet
133+
let narrow = merge Mval.narrow SD.meet
179134

180135
include Lattice.NoBotTop
181136

@@ -194,8 +149,7 @@ struct
194149

195150
let of_elt (x: elt): t = match x with
196151
| Addr (v, o) -> Addr v
197-
| StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
198-
| StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *)
152+
| StrPtr s -> StrPtr (SD.repr s)
199153
| NullPtr -> NullPtr
200154
| UnknownPtr -> UnknownPtr
201155
end
@@ -211,8 +165,7 @@ struct
211165

212166
let of_elt (x: elt): t = match x with
213167
| Addr (v, o) -> Addr (v, Offset.Unit.of_offs o) (* addrs grouped by var and part of offset *)
214-
| StrPtr _ when GobConfig.get_bool "ana.base.limit-string-addresses" -> StrPtr None (* all strings together if limited *)
215-
| StrPtr x -> StrPtr x (* everything else is kept separate, including strings if not limited *)
168+
| StrPtr s -> StrPtr (SD.repr s)
216169
| NullPtr -> NullPtr
217170
| UnknownPtr -> UnknownPtr
218171
end

‎src/cdomains/addressDomain_intf.ml‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ sig
77
| Addr of Mval.t (** Pointer to mvalue. *)
88
| NullPtr (** NULL pointer. *)
99
| UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *)
10-
| StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *)
10+
| StrPtr of StringDomain.t (** String literal pointer. [StrPtr None] abstracts any string pointer *)
1111
include Printable.S with type t := t (** @closed *)
1212

1313
val of_string: string -> t
@@ -16,8 +16,6 @@ sig
1616
val to_string: t -> string option
1717
(** Convert {!StrPtr} to string if possible. *)
1818

19-
(** 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. *)
20-
2119
val to_c_string: t -> string option
2220
(** Convert {!StrPtr} to C string if possible. *)
2321

@@ -71,7 +69,7 @@ sig
7169
- Each {!Addr}, modulo precise index expressions in the offset, is a sublattice with ordering induced by {!Mval}.
7270
- {!NullPtr} is a singleton sublattice.
7371
- {!UnknownPtr} is a singleton sublattice.
74-
- 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. *)
72+
- 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. *)
7573
module AddressLattice (Mval: Mval.Lattice):
7674
sig
7775
include module type of AddressPrintable (Mval)

‎src/cdomains/stringDomain.ml‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
include Printable.StdLeaf
2+
3+
let name () = "string"
4+
5+
type string_domain = Unit | Disjoint | Flat
6+
7+
let string_domain: string_domain ResettableLazy.t =
8+
ResettableLazy.from_fun (fun () ->
9+
match GobConfig.get_string "ana.base.strings.domain" with
10+
| "unit" -> Unit
11+
| "disjoint" -> Disjoint
12+
| "flat" -> Flat
13+
| _ -> failwith "ana.base.strings.domain: illegal value"
14+
)
15+
16+
let get_string_domain () = ResettableLazy.force string_domain
17+
18+
let reset_lazy () =
19+
ResettableLazy.reset string_domain
20+
21+
22+
type t = string option [@@deriving eq, ord, hash]
23+
24+
let hash x =
25+
if get_string_domain () = Disjoint then
26+
hash x
27+
else
28+
13859
29+
30+
let show = function
31+
| Some x -> "\"" ^ x ^ "\""
32+
| None -> "(unknown string)"
33+
34+
include Printable.SimpleShow (
35+
struct
36+
type nonrec t = t
37+
let show = show
38+
end
39+
)
40+
41+
let of_string x =
42+
if get_string_domain () = Unit then
43+
None
44+
else
45+
Some x
46+
let to_string x = x
47+
48+
(* only keep part before first null byte *)
49+
let to_c_string = function
50+
| Some x ->
51+
begin match String.split_on_char '\x00' x with
52+
| s::_ -> Some s
53+
| [] -> None
54+
end
55+
| None -> None
56+
57+
let to_n_c_string n x =
58+
match to_c_string x with
59+
| Some x ->
60+
if n > String.length x then
61+
Some x
62+
else if n < 0 then
63+
None
64+
else
65+
Some (String.sub x 0 n)
66+
| None -> None
67+
68+
let to_string_length x =
69+
match to_c_string x with
70+
| Some x -> Some (String.length x)
71+
| None -> None
72+
73+
let to_exp = function
74+
| Some x -> GoblintCil.mkString x
75+
| None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.")
76+
77+
let semantic_equal x y =
78+
match x, y with
79+
| None, _
80+
| _, None -> Some true
81+
| Some a, Some b -> if a = b then None else Some false
82+
83+
let leq x y =
84+
match x, y with
85+
| _, None -> true
86+
| a, b -> a = b
87+
88+
let join x y =
89+
match x, y with
90+
| None, _
91+
| _, None -> None
92+
| Some a, Some b when a = b -> Some a
93+
| Some a, Some b (* when a <> b *) ->
94+
if get_string_domain () = Disjoint then
95+
raise Lattice.Uncomparable
96+
else
97+
None
98+
99+
let meet x y =
100+
match x, y with
101+
| None, a
102+
| a, None -> a
103+
| Some a, Some b when a = b -> Some a
104+
| Some a, Some b (* when a <> b *) ->
105+
if get_string_domain () = Disjoint then
106+
raise Lattice.Uncomparable
107+
else
108+
raise Lattice.BotValue
109+
110+
let repr x =
111+
if get_string_domain () = Disjoint then
112+
x (* everything else is kept separate, including strings if not limited *)
113+
else
114+
None (* all strings together if limited *)

‎src/cdomains/stringDomain.mli‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
(** String literals domain. *)
2+
3+
include Printable.S
4+
5+
val reset_lazy: unit -> unit
6+
(** Reset the cached configuration of the string domain. *)
7+
8+
val of_string: string -> t
9+
(** Convert from string. *)
10+
11+
val to_string: t -> string option
12+
(** Convert to string if possible. *)
13+
14+
(** 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. *)
15+
16+
val to_c_string: t -> string option
17+
(** Convert to C string if possible. *)
18+
19+
val to_n_c_string: int -> t -> string option
20+
(** Convert to C string of given maximum length if possible. *)
21+
22+
val to_string_length: t -> int option
23+
(** Find length of C string if possible. *)
24+
25+
val to_exp: t -> GoblintCil.exp
26+
(** Convert to CIL expression. *)
27+
28+
val semantic_equal: t -> t -> bool option
29+
(** Check semantic equality of two strings.
30+
31+
@return [Some true] if definitely equal, [Some false] if definitely not equal, [None] if unknown. *)
32+
33+
(** Some {!Lattice.S} operations. *)
34+
35+
val leq: t -> t -> bool
36+
val join: t -> t -> t
37+
val meet: t -> t -> t
38+
39+
val repr : t -> t
40+
(** Representative for address lattice. *)

‎src/common/util/options.schema.json‎

Lines changed: 13 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -655,11 +655,19 @@
655655
},
656656
"additionalProperties": false
657657
},
658-
"limit-string-addresses": {
659-
"title": "ana.base.limit-string-addresses",
660-
"description": "Limit abstract address sets to keep at most one distinct string pointer.",
661-
"type": "boolean",
662-
"default": true
658+
"strings": {
659+
"title": "ana.base.strings",
660+
"type": "object",
661+
"properties": {
662+
"domain": {
663+
"title": "ana.base.strings.domain",
664+
"description": "Domain for string literals.",
665+
"type": "string",
666+
"enum": ["unit", "flat", "disjoint"],
667+
"default": "flat"
668+
}
669+
},
670+
"additionalProperties": false
663671
},
664672
"partition-arrays": {
665673
"title": "ana.base.partition-arrays",

‎src/goblint_lib.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -213,6 +213,7 @@ module FloatDomain = FloatDomain
213213

214214
module Mval = Mval
215215
module Offset = Offset
216+
module StringDomain = StringDomain
216217
module AddressDomain = AddressDomain
217218

218219
(** {5 Complex} *)

0 commit comments

Comments
 (0)