Skip to content

Commit

Permalink
Attempts towards simplification
Browse files Browse the repository at this point in the history
  • Loading branch information
@michael-schwarz
michael-schwarz committed Nov 24, 2023
1 parent a50b1b8 commit 86b7c35
Show file tree
Hide file tree
Showing 2 changed files with 84 additions and 37 deletions.
89 changes: 53 additions & 36 deletions src/cdomains/arrayDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1000,6 +1000,7 @@ module NullByte (Val: LatticeWithNull) (Idx: IntDomain.Z): Str with type value =
struct
module MustSet = NullByteSet.MustSet
module MaySet = NullByteSet.MaySet
module Nulls = NullByteSet.MustMaySet

(* (Must Null Set, May Null Set, Array Size) *)
include Lattice.Prod3 (MustSet) (MaySet) (Idx)
Expand All @@ -1019,6 +1020,7 @@ struct
| _ -> None

let get (ask: VDQ.t) (must_nulls_set, may_nulls_set, size) (e, i) =
let nulls = (must_nulls_set, may_nulls_set) in
let min interval = match Idx.minimal interval with
| Some min_num when Z.geq min_num Z.zero -> min_num
| _ -> Z.zero in (* assume worst case minimal natural number *)
Expand All @@ -1031,34 +1033,37 @@ struct
(* if there is no maximum value in index interval *)
| None, _ ->
(* ... return NotNull if no i >= min_i in may_nulls_set *)
if not (MaySet.exists (Z.leq min_i) may_nulls_set) then
if not (Nulls.may_exist (Z.leq min_i) nulls) then
NotNull
(* ... else return Top *)
else
Top
(* if there is no maximum size *)
| Some max_i, None when Z.geq max_i Z.zero ->
(* ... and maximum value in index interval < minimal size, return Null if all numbers in index interval are in must_nulls_set *)
if Z.lt max_i min_size && MustSet.interval_mem (min_i,max_i) must_nulls_set then
if Z.lt max_i min_size && Nulls.must_mem_interval (min_i,max_i) nulls then
Null
(* ... return NotNull if no number in index interval is in may_nulls_set *)
else if not (MaySet.exists (fun x -> Z.geq x min_i && Z.leq x max_i) may_nulls_set) then
else if not (Nulls.may_exist (fun x -> Z.geq x min_i && Z.leq x max_i) nulls) then
NotNull
else
Top
| Some max_i, Some max_size when Z.geq max_i Z.zero ->
(* if maximum value in index interval < minimal size, return Null if all numbers in index interval are in must_nulls_set *)
if Z.lt max_i min_size && MustSet.interval_mem (min_i,max_i) must_nulls_set then
if Z.lt max_i min_size && Nulls.must_mem_interval (min_i, max_i) nulls then
Null
(* if maximum value in index interval < maximal size, return NotNull if no number in index interval is in may_nulls_set *)
else if Z.lt max_i max_size && not (MaySet.exists (fun x -> Z.geq x min_i && Z.leq x max_i) may_nulls_set) then
else if Z.lt max_i max_size && not (Nulls.may_exist (fun x -> Z.geq x min_i && Z.leq x max_i) nulls) then
NotNull
else
Top
(* if maximum number in interval is invalid, i.e. negative, return Top of value *)
| _ -> Top

let set (ask: VDQ.t) (must_nulls_set, may_nulls_set, size) (e, i) v =
let uf ((a,b),c) = (a,b,c)

let set (ask: VDQ.t) ((must_nulls_set, may_nulls_set, size) as x) (e, i) v =
let nulls = (must_nulls_set, may_nulls_set) in
let rec add_indexes i max may_nulls_set =
if Z.gt i max then
may_nulls_set
Expand Down Expand Up @@ -1144,30 +1149,37 @@ struct
(if Val.is_null v && idx_maximal size = None then
match idx_maximal size with
(* ... and there is no maximal size, modify may_nulls_set to top *)
| None -> (must_nulls_set, MaySet.top (), size)
| None -> uf @@ (Nulls.forget_may nulls, size)
(* ... and there is a maximal size, add all i from minimal index to maximal size to may_nulls_set *)
| Some max_size -> (must_nulls_set, add_indexes min_i (Z.pred max_size) may_nulls_set, size)
| Some max_size -> uf @@ (Nulls.add_may_interval (min_i, Z.pred max_size) nulls, size)
(* ... and value <> null, only keep indexes < minimal index in must_nulls_set *)
else if Val.is_not_null v then
(MustSet.filter (Z.gt min_i) must_nulls_set min_size, may_nulls_set, size)
uf @@ (Nulls.filter_musts (Z.gt min_i) min_size nulls, size)
(*..., value unknown *)
else
match Idx.minimal size, idx_maximal size with
(* ... and size unknown, modify both sets to top *)
| None, None -> (MustSet.top (), MaySet.top (), size)
| None, None -> uf @@ (Nulls.top (), size)
(* ... and only minimal size known, remove all indexes < minimal size from must_nulls_set and modify may_nulls_set to top *)
| Some min_size, None -> (MustSet.filter (Z.gt min_size) must_nulls_set min_size, MaySet.top (), size)
| Some min_size, None ->
let nulls = Nulls.forget_may nulls in
uf @@ (Nulls.filter_musts (Z.gt min_size) min_size nulls, size)
(* ... and only maximal size known, modify must_nulls_set to top and add all i from minimal index to maximal size to may_nulls_set *)
| None, Some max_size -> (MustSet.top (), add_indexes min_i (Z.pred max_size) may_nulls_set, size)
| None, Some max_size ->
let nulls = Nulls.forget_must nulls in
uf @@ (Nulls.add_may_interval (min_i, Z.pred max_size) nulls, size)
(* ... and size is known, remove all indexes < minimal size from must_nulls_set and add all i from minimal index to maximal size to may_nulls_set *)
| Some min_size, Some max_size -> (MustSet.filter (Z.gt min_size) must_nulls_set min_size, add_indexes min_i (Z.pred max_size) may_nulls_set, size))
| Some min_size, Some max_size ->
let nulls = Nulls.filter_musts (Z.gt min_size) min_size nulls in
uf @@ (Nulls.add_may_interval (min_i, Z.pred max_size) nulls, size)
)
| Some max_i when Z.geq max_i Z.zero ->
if Z.equal min_i max_i then
set_exact min_i
else
(set_interval_must min_i max_i, set_interval_may min_i max_i, size)
(* if maximum number in interval is invalid, i.e. negative, return tuple unmodified *)
| _ -> (must_nulls_set, may_nulls_set, size)
| _ -> x

let make ?(varAttr=[]) ?(typAttr=[]) i v =
let min_i, max_i = match Idx.minimal i, idx_maximal i with
Expand Down Expand Up @@ -1240,20 +1252,21 @@ struct
(set, set, Idx.of_int ILong (Z.succ last_null))

(** Returns an abstract value with at most one null byte marking the end of the string *)
let to_string (must_nulls_set, may_nulls_set, size) =
let to_string ((must_nulls_set, may_nulls_set, size) as x) =
let nulls = (must_nulls_set, may_nulls_set) in
(* if must_nulls_set and min_nulls_set empty, definitely no null byte in array => warn about certain buffer overflow and return tuple unchanged *)
if MustSet.is_empty must_nulls_set && MaySet.is_empty may_nulls_set then
(M.error ~category:ArrayOobMessage.past_end "Array access past end: buffer overflow";
(must_nulls_set, may_nulls_set, size))
if Nulls.must_be_empty nulls then
(M.error ~category:ArrayOobMessage.past_end "Array access past end: buffer overflow"; x)
(* if only must_nulls_set empty, no certainty about array containing null byte => warn about potential buffer overflow and return tuple unchanged *)
else if MustSet.is_empty must_nulls_set then
(M.warn ~category:ArrayOobMessage.past_end "May access array past end: potential buffer overflow";
(must_nulls_set, may_nulls_set, size))
else if Nulls.may_be_empty nulls then
(M.warn ~category:ArrayOobMessage.past_end "May access array past end: potential buffer overflow"; x)
else
let min_must_null = MustSet.min_elt must_nulls_set in
let min_must_null = Nulls.min_must_elem nulls in
let min_may_null = Nulls.min_may_elem nulls in
(* if smallest index in sets coincides, only this null byte is kept in both sets *)
if Z.equal min_must_null (MaySet.min_elt may_nulls_set) then
(MustSet.singleton min_must_null, MaySet.singleton min_must_null, Idx.of_int ILong (Z.succ min_must_null))
if Z.equal min_must_null min_may_null then
let (must,may) = Nulls.precise_singleton min_must_null in
(must, may, Idx.of_int ILong (Z.succ min_must_null))
(* else return empty must_nulls_set and keep every index up to smallest index of must_nulls_set included in may_nulls_set *)
else
match idx_maximal size with
Expand All @@ -1273,6 +1286,7 @@ struct
* marking the end of the string and if needed followed by further null bytes to obtain
* an n bytes string. *)
let to_n_string (must_nulls_set, may_nulls_set, size) n =
let nulls = (must_nulls_set, may_nulls_set) in
let rec add_indexes i max set =
if Z.geq i max then
set
Expand Down Expand Up @@ -1316,7 +1330,7 @@ struct
| None, None -> ());

(* if definitely no null byte in array, i.e. must_nulls_set = may_nulls_set = empty set *)
if MustSet.is_empty must_nulls_set && MaySet.is_empty may_nulls_set then
if Nulls.must_be_empty nulls then
(M.warn ~category:ArrayOobMessage.past_end
"Resulting string might not be null-terminated because src doesn't contain a null byte";
match idx_maximal size with
Expand All @@ -1325,13 +1339,13 @@ struct
| _ -> (must_nulls_set, may_nulls_set, Idx.of_int ILong (Z.of_int n)))
(* if only must_nulls_set empty, remove indexes >= n from may_nulls_set and add all indexes from minimal may null index to n - 1;
* warn as in any case, resulting array not guaranteed to contain null byte *)
else if MustSet.is_empty must_nulls_set then
let min_may_null = MaySet.min_elt may_nulls_set in
else if Nulls.may_be_empty nulls then
let min_may_null = Nulls.min_may_elem nulls in
warn_no_null Z.zero false min_may_null;
(must_nulls_set, update_may_indexes min_may_null may_nulls_set, Idx.of_int ILong (Z.of_int n))
else
let min_must_null = MustSet.min_elt must_nulls_set in
let min_may_null = MaySet.min_elt may_nulls_set in
let min_must_null = Nulls.min_must_elem nulls in
let min_may_null = Nulls.min_may_elem nulls in
(* warn if resulting array may not contain null byte *)
warn_no_null min_must_null true min_may_null;
(* if min_must_null = min_may_null, remove indexes >= n and add all indexes from minimal must/may null to n - 1 in the sets *)
Expand All @@ -1341,19 +1355,21 @@ struct
(MustSet.top (), update_may_indexes min_may_null may_nulls_set, Idx.of_int ILong (Z.of_int n)))

let to_string_length (must_nulls_set, may_nulls_set, size) =
let nulls = (must_nulls_set, may_nulls_set) in
(* if must_nulls_set and min_nulls_set empty, definitely no null byte in array => return interval [size, inf) and warn *)
if MustSet.is_empty must_nulls_set && MaySet.is_empty may_nulls_set then
(* TODO: check of must set really needed? *)
if Nulls.must_be_empty nulls then
(M.error ~category:ArrayOobMessage.past_end "Array doesn't contain a null byte: buffer overflow";
match Idx.minimal size with
| Some min_size -> Idx.starting !Cil.kindOfSizeOf min_size
| None -> Idx.starting !Cil.kindOfSizeOf Z.zero)
(* if only must_nulls_set empty, no guarantee that null ever encountered in array => return interval [minimal may null, inf) and *)
else if MustSet.is_empty must_nulls_set then
else if Nulls.may_be_empty nulls then
(M.warn ~category:ArrayOobMessage.past_end "Array might not contain a null byte: potential buffer overflow";
Idx.starting !Cil.kindOfSizeOf (MaySet.min_elt may_nulls_set))
Idx.starting !Cil.kindOfSizeOf (Nulls.min_may_elem nulls))
(* else return interval [minimal may null, minimal must null] *)
else
Idx.of_interval !Cil.kindOfSizeOf (MaySet.min_elt may_nulls_set, MustSet.min_elt must_nulls_set)
Idx.of_interval !Cil.kindOfSizeOf (Nulls.min_may_elem nulls, Nulls.min_must_elem nulls)

let string_copy (must_nulls_set1, may_nulls_set1, size1) (must_nulls_set2, may_nulls_set2, size2) n =
(* filter out indexes before strlen(src) from dest sets and after strlen(src) from src sets and build union, keep size of dest *)
Expand Down Expand Up @@ -1599,13 +1615,14 @@ struct
compute_concat must_nulls_set2' may_nulls_set2'
| _ -> (MustSet.top (), MaySet.top (), size1)

let substring_extraction haystack (must_nulls_set_needle, may_nulls_set_needle, size_needle) =
let substring_extraction haystack ((must_needle, may_needle, size_needle) as needle) =
let nulls_needle = (must_needle, may_needle) in
(* if needle is empty string, i.e. certain null byte at index 0, return value of strstr is pointer to haystack *)
if MustSet.mem Z.zero must_nulls_set_needle then
if Nulls.must_mem Z.zero nulls_needle then
IsSubstrAtIndex0
else
let haystack_len = to_string_length haystack in
let needle_len = to_string_length (must_nulls_set_needle, may_nulls_set_needle, size_needle) in
let needle_len = to_string_length needle in
match idx_maximal haystack_len, Idx.minimal needle_len with
| Some haystack_max, Some needle_min ->
(* if strlen(haystack) < strlen(needle), needle can never be substring of haystack => return None *)
Expand Down
32 changes: 31 additions & 1 deletion src/cdomains/nullByteSet.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ module MustSet = struct
else
M.min_elt must_nulls_set


let interval_mem (l,u) set =
if M.is_bot set then
true
Expand Down Expand Up @@ -63,3 +62,34 @@ module MaySet = struct
else
M.min_elt may_nulls_set
end

module MustMaySet = struct
include Lattice.Prod (MustSet) (MaySet)

let must_mem i (musts, mays) = MustSet.mem i musts
let must_mem_interval (l,u) (musts, mays) = MustSet.interval_mem (l,u) musts

let may_be_empty (musts, mays) = MustSet.is_empty musts
let must_be_empty (musts, mays) = MaySet.is_empty mays

let min_may_elem (musts, mays) = MaySet.min_elt mays
let min_must_elem (musts, mays) = MustSet.min_elt musts

let add_may_interval (l,u) (musts, mays) =
let rec add_indexes i max set =
if Z.gt i max then
set
else
add_indexes (Z.succ i) max (MaySet.add i set)
in
(musts, add_indexes l u mays)

let precise_singleton i =
(MustSet.singleton i, MaySet.singleton i)

let may_exist f (musts, mays) = MaySet.exists f mays

let forget_may (musts, mays) = (musts, MaySet.top ())
let forget_must (musts, mays) = (MustSet.top (), mays)
let filter_musts f min_size (musts, mays) = (MustSet.filter f musts min_size, mays)
end

0 comments on commit 86b7c35

Please sign in to comment.