diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json index 84cbf53585..2197335eaf 100644 --- a/conf/examples/very-precise.json +++ b/conf/examples/very-precise.json @@ -61,7 +61,9 @@ "structs" : { "domain" : "combined-sk" }, - "limit-string-addresses": false + "strings": { + "domain": "disjoint" + } } }, "exp": { diff --git a/src/cdomains/addressDomain_intf.ml b/src/cdomains/addressDomain_intf.ml index 0ef3d6dd8d..f86dee29c4 100644 --- a/src/cdomains/addressDomain_intf.ml +++ b/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) diff --git a/src/cdomains/stringDomain.ml b/src/cdomains/stringDomain.ml index c888663c7c..6c398cf9fd 100644 --- a/src/cdomains/stringDomain.ml +++ b/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,10 +70,10 @@ 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 @@ -77,13 +81,13 @@ let meet x y = | 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 *) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 1b9c7d3fd5..330506958a 100644 --- a/src/util/options.schema.json +++ b/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", diff --git a/tests/regression/02-base/88-string-ptrs-limited.c b/tests/regression/02-base/88-string-ptrs-limited.c index ab8b2fefe8..c4f39dc711 100644 --- a/tests/regression/02-base/88-string-ptrs-limited.c +++ b/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 #include diff --git a/tests/regression/02-base/89-string-ptrs-not-limited.c b/tests/regression/02-base/89-string-ptrs-not-limited.c index 96100d230d..ab30e21fd8 100644 --- a/tests/regression/02-base/89-string-ptrs-not-limited.c +++ b/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 #include diff --git a/tests/regression/73-strings/01-string_literals.c b/tests/regression/73-strings/01-string_literals.c index 36e4ed121c..42086e07b6 100644 --- a/tests/regression/73-strings/01-string_literals.c +++ b/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 #include @@ -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 diff --git a/tests/regression/73-strings/02-string_literals_with_null.c b/tests/regression/73-strings/02-string_literals_with_null.c index 75d000bbb8..cc41e9e287 100644 --- a/tests/regression/73-strings/02-string_literals_with_null.c +++ b/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 #include diff --git a/tests/regression/73-strings/03-string_basics.c b/tests/regression/73-strings/03-string_basics.c index db196c64b4..a9d02d5e8b 100644 --- a/tests/regression/73-strings/03-string_basics.c +++ b/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 #include diff --git a/tests/regression/73-strings/05-string-unit-domain.c b/tests/regression/73-strings/05-string-unit-domain.c index 521e2f3ec5..70e6bed5bf 100644 --- a/tests/regression/73-strings/05-string-unit-domain.c +++ b/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 #include