Skip to content

Commit

Permalink
Improve StringDomain type safety by matching all domains
Browse files Browse the repository at this point in the history
This is more robust against changes to the possible choices of domain.
It would have avoided issue #1594.
  • Loading branch information
sim642 committed Oct 18, 2024
1 parent eed1e27 commit 2284da8
Showing 1 changed file with 17 additions and 18 deletions.
35 changes: 17 additions & 18 deletions src/cdomain/value/cdomains/stringDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,9 @@ type t = string option [@@deriving eq, ord, hash]
(** [None] means top. *)

let hash x =
if get_string_domain () <> Unit then
hash x
else
13859
match get_string_domain () with
| Disjoint | Flat -> hash x
| Unit -> 13859

let show = function
| Some x -> "\"" ^ x ^ "\""
Expand All @@ -40,10 +39,9 @@ include Printable.SimpleShow (
)

let of_string x =
if get_string_domain () = Unit then
None
else
Some x
match get_string_domain () with
| Unit -> None
| Disjoint | Flat -> Some x
let to_string x = x

(* only keep part before first null byte *)
Expand Down Expand Up @@ -92,24 +90,25 @@ let join x y =
| _, 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
match get_string_domain () with
| Disjoint -> raise Lattice.Uncomparable
| Flat -> None
| Unit -> assert false

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
match get_string_domain () with
| Disjoint -> raise Lattice.Uncomparable
| Flat -> raise Lattice.BotValue
| Unit -> assert false

let repr x =
if get_string_domain () = Disjoint then
match get_string_domain () with
| Disjoint ->
x (* everything else is kept separate, including strings if not limited *)
else
| Flat | Unit ->
None (* all strings together if limited *)

0 comments on commit 2284da8

Please sign in to comment.