Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve flat string domain hash #1602

Merged
merged 2 commits into from
Oct 24, 2024
Merged

Improve flat string domain hash #1602

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
eed1e27
Improve flat string domain hash
sim642 Oct 18, 2024
2284da8
Improve StringDomain type safety by matching all domains
sim642 Oct 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 18 additions & 18 deletions src/cdomain/value/cdomains/stringDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@ let reset_lazy () =


type t = string option [@@deriving eq, ord, hash]
(** [None] means top. *)

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

let show = function
| Some x -> "\"" ^ x ^ "\""
Expand All @@ -39,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 @@ -91,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 *)
Loading