From 86b7c35bb981b5b7264ade4ef0073b226518b8fc Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 24 Nov 2023 23:54:16 +0100 Subject: [PATCH] Attempts towards simplification --- src/cdomains/arrayDomain.ml | 89 ++++++++++++++++++++++--------------- src/cdomains/nullByteSet.ml | 32 ++++++++++++- 2 files changed, 84 insertions(+), 37 deletions(-) diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index bb304af85e..741207c9e4 100644 --- a/src/cdomains/arrayDomain.ml +++ b/src/cdomains/arrayDomain.ml @@ -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) @@ -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 *) @@ -1031,7 +1033,7 @@ 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 @@ -1039,26 +1041,29 @@ struct (* 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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 *) @@ -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 *) @@ -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 *) diff --git a/src/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml index 5977023b8e..3fc3889ffc 100644 --- a/src/cdomains/nullByteSet.ml +++ b/src/cdomains/nullByteSet.ml @@ -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 @@ -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 \ No newline at end of file