diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 078799bea6..993df9a26a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1417,7 +1417,7 @@ struct (** [set st addr val] returns a state where [addr] is set to [val] * it is always ok to put None for lval_raw and rval_raw, this amounts to not using/maintaining * precise information about arrays. *) - let set (a: Q.ask) ~(ctx: _ ctx) ?(invariant=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = + let set (a: Q.ask) ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = let update_variable x t y z = if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\n\n" x.vname VD.pretty y CPA.pretty z; let r = update_variable x t y z in (* refers to defintion that is outside of set *) @@ -1450,7 +1450,7 @@ struct let update_offset old_value = (* Projection globals to highest Precision *) let projected_value = project_val (Queries.to_value_domain_ask a) None None value (is_global a x) in - let new_value = VD.update_offset (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in + let new_value = VD.update_offset ~blob_destructive (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in if WeakUpdates.mem x st.weak then VD.join old_value new_value else if invariant then ( @@ -2189,24 +2189,90 @@ struct (* do nothing if all characters are needed *) | _ -> None in - let string_manipulation s1 s2 lv all op = - let s1_a, s1_typ = addr_type_of_exp s1 in - let s2_a, s2_typ = addr_type_of_exp s2 in - match lv, op with - | Some lv_val, Some f -> - (* when whished types coincide, compute result of operation op, otherwise use top *) - let lv_a = eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val in - let lv_typ = Cilfacade.typeOfLval lv_val in - if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *) - lv_a, lv_typ, (f s1_a s2_a) - else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *) - lv_a, lv_typ, (f s1_a s2_a) - else - lv_a, lv_typ, (VD.top_value (unrollType lv_typ)) - | _ -> - (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *) - let _ = AD.string_writing_defined s1_a in - s1_a, s1_typ, VD.top_value (unrollType s1_typ) + let address_from_value (v:value) = match v with + | Address a -> + (* TODO: is it fine to just drop the last index unconditionally? https://github.com/goblint/analyzer/pull/1076#discussion_r1408975611 *) + let rec lo = function + | `Index (i, `NoOffset) -> `NoOffset + | `NoOffset -> `NoOffset + | `Field (f, o) -> `Field (f, lo o) + | `Index (i, o) -> `Index (i, lo o) in + let rmLastOffset = function + | Addr.Addr (v, o) -> Addr.Addr (v, lo o) + | other -> other in + AD.map rmLastOffset a + | _ -> raise (Failure "String function: not an address") + in + let string_manipulation s1 s2 lv all op_addr op_array = + let s1_v = eval_rv (Analyses.ask_of_ctx ctx) gs st s1 in + let s1_a = address_from_value s1_v in + let s1_typ = AD.type_of s1_a in + let s2_v = eval_rv (Analyses.ask_of_ctx ctx) gs st s2 in + let s2_a = address_from_value s2_v in + let s2_typ = AD.type_of s2_a in + (* compute value in string literals domain if s1 and s2 are both string literals *) + (* TODO: is this reliable? there could be a char* which isn't StrPtr *) + if CilType.Typ.equal s1_typ charPtrType && CilType.Typ.equal s2_typ charPtrType then + begin match lv, op_addr with + | Some lv_val, Some f -> + (* when whished types coincide, compute result of operation op_addr, otherwise use top *) + let lv_a = eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val in + let lv_typ = Cilfacade.typeOfLval lv_val in + if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *) + set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a) + else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *) + set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (f s1_a s2_a) + else + set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + | _ -> + (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *) + let _ = AD.string_writing_defined s1_a in + set ~ctx (Analyses.ask_of_ctx ctx) gs st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + end + (* else compute value in array domain *) + else + let lv_a, lv_typ = match lv with + | Some lv_val -> eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val, Cilfacade.typeOfLval lv_val + | None -> s1_a, s1_typ in + begin match (get (Analyses.ask_of_ctx ctx) gs st s1_a None), get (Analyses.ask_of_ctx ctx) gs st s2_a None with + | Array array_s1, Array array_s2 -> set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + | Array array_s1, _ when CilType.Typ.equal s2_typ charPtrType -> + let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in + let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in + set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + | Bot, Array array_s2 -> + (* If we have bot inside here, we assume the blob is used as a char array and create one inside *) + let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in + let size = ctx.ask (Q.BlobSize {exp = s1; base_address = false}) in + let s_id = + try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size + with Failure _ -> ID.top_of ptrdiff_ik in + let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in + set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2) + | Bot , _ when CilType.Typ.equal s2_typ charPtrType -> + (* If we have bot inside here, we assume the blob is used as a char array and create one inside *) + let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in + let size = ctx.ask (Q.BlobSize {exp = s1; base_address = false}) in + let s_id = + try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size + with Failure _ -> ID.top_of ptrdiff_ik in + let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in + let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in + let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in + set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2) + | _, Array array_s2 when CilType.Typ.equal s1_typ charPtrType -> + (* if s1 is string literal, str(n)cpy and str(n)cat are undefined *) + if op_addr = None then + (* triggers warning, function only evaluated for side-effects *) + let _ = AD.string_writing_defined s1_a in + set ~ctx (Analyses.ask_of_ctx ctx) gs st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + else + let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in + let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in + set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + | _ -> + set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + end in let st = match desc.special args, f.vname with | Memset { dest; ch; count; }, _ -> @@ -2229,53 +2295,51 @@ struct set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value | Memcpy { dest = dst; src; n; }, _ -> (* TODO: use n *) memory_copying dst src (Some n) - (* strcpy(dest, src); *) - | Strcpy { dest = dst; src; n = None }, _ -> - let dest_a, dest_typ = addr_type_of_exp dst in - (* when dest surely isn't a string literal, try copying src to dest *) - if AD.string_writing_defined dest_a then - memory_copying dst src None - else - (* else return top (after a warning was issued) *) - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (VD.top_value (unrollType dest_typ)) - (* strncpy(dest, src, n); *) - | Strcpy { dest = dst; src; n }, _ -> - begin match eval_n n with - | Some num -> - let dest_a, dest_typ, value = string_manipulation dst src None false None in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value - | None -> failwith "already handled in case above" - end - | Strcat { dest = dst; src; n }, _ -> - let dest_a, dest_typ, value = string_manipulation dst src None false None in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value + | Strcpy { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_copy ar1 ar2 (eval_n n))) + | Strcat { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_concat ar1 ar2 (eval_n n))) | Strlen s, _ -> begin match lv with | Some lv_val -> let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val in let dest_typ = Cilfacade.typeOfLval lv_val in - let lval = mkMem ~addr:(Cil.stripCasts s) ~off:NoOffset in - let address = eval_lv (Analyses.ask_of_ctx ctx) gs st lval in - let (value:value) = Int(AD.to_string_length address) in + let v = eval_rv (Analyses.ask_of_ctx ctx) gs st s in + let a = address_from_value v in + let value:value = + (* if s string literal, compute strlen in string literals domain *) + (* TODO: is this reliable? there could be a char* which isn't StrPtr *) + if CilType.Typ.equal (AD.type_of a) charPtrType then + Int (AD.to_string_length a) + (* else compute strlen in array domain *) + else + begin match get (Analyses.ask_of_ctx ctx) gs st a None with + | Array array_s -> Int (CArrays.to_string_length array_s) + | _ -> VD.top_value (unrollType dest_typ) + end in set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value | None -> st end | Strstr { haystack; needle }, _ -> begin match lv with - | Some _ -> - (* when haystack, needle and dest type coincide, check if needle is a substring of haystack: - if that is the case, assign the substring of haystack starting at the first occurrence of needle to dest, - else use top *) - let dest_a, dest_typ, value = string_manipulation haystack needle lv true (Some (fun h_a n_a -> Address(AD.substring_extraction h_a n_a))) in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value + | Some lv_val -> + (* check if needle is a substring of haystack in string literals domain if haystack and needle are string literals, + else check in null bytes domain if both haystack and needle are / can be transformed to an array domain representation; + if needle is substring, assign the substring of haystack starting at the first occurrence of needle to dest, + if it surely isn't, assign a null_ptr *) + string_manipulation haystack needle lv true (Some (fun h_a n_a -> Address (AD.substring_extraction h_a n_a))) + (fun h_ar n_ar -> match CArrays.substring_extraction h_ar n_ar with + | CArrays.IsNotSubstr -> Address (AD.null_ptr) + | CArrays.IsSubstrAtIndex0 -> Address (eval_lv (Analyses.ask_of_ctx ctx) gs st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset)) + | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv (Analyses.ask_of_ctx ctx) gs st + (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr))) | None -> st end | Strcmp { s1; s2; n }, _ -> begin match lv with | Some _ -> - (* when s1 and s2 type coincide, compare both both strings completely or their first n characters, otherwise use top *) - let dest_a, dest_typ, value = string_manipulation s1 s2 lv false (Some (fun s1_a s2_a -> Int(AD.string_comparison s1_a s2_a (eval_n n)))) in - set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value + (* when s1 and s2 are string literals, compare both completely or their first n characters in the string literals domain; + else compare them in the null bytes array domain if they are / can be transformed to an array domain representation *) + string_manipulation s1 s2 lv false (Some (fun s1_a s2_a -> Int (AD.string_comparison s1_a s2_a (eval_n n)))) + (fun s1_ar s2_ar -> Int (CArrays.string_comparison s1_ar s2_ar (eval_n n))) | None -> st end | Abort, _ -> raise Deadcode diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index 2f91e47663..6c47f1e87a 100644 --- a/src/cdomains/arrayDomain.ml +++ b/src/cdomains/arrayDomain.ml @@ -39,15 +39,12 @@ let get_domain ~varAttr ~typAttr = let can_recover_from_top x = x <> TrivialDomain -module type S = +module type S0 = sig include Lattice.S type idx type value - val domain_of_t: t -> domain - - val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value val set: VDQ.t -> t -> Basetype.CilExp.t option * idx -> value -> t val make: ?varAttr:attributes -> ?typAttr:attributes -> idx -> value -> t val length: t -> idx option @@ -60,20 +57,76 @@ sig val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool val update_length: idx -> t -> t + val project: ?varAttr:attributes -> ?typAttr:attributes -> VDQ.t -> t -> t val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t end -module type LatticeWithSmartOps = +module type S = +sig + include S0 + + val domain_of_t: t -> domain + val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value +end + +module type Str = +sig + include S0 + + type ret = Null | NotNull | Maybe + type substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr + + val get: VDQ.t -> t -> Basetype.CilExp.t option * idx -> ret + + val to_null_byte_domain: string -> t + val to_string_length: t -> idx + val string_copy: t -> t -> int option -> t + val string_concat: t -> t -> int option -> t + val substring_extraction: t -> t -> substr + val string_comparison: t -> t -> int option -> idx +end + +module type StrWithDomain = +sig + include Str + include S with type t := t and type idx := idx +end + +module type LatticeWithInvalidate = sig include Lattice.S + val invalidate_abstract_value: t -> t +end + +module type LatticeWithSmartOps = +sig + include LatticeWithInvalidate val smart_join: (Cil.exp -> BI.t option) -> (Cil.exp -> BI.t option) -> t -> t -> t val smart_widen: (Cil.exp -> BI.t option) -> (Cil.exp -> BI.t option) -> t -> t -> t val smart_leq: (Cil.exp -> BI.t option) -> (Cil.exp -> BI.t option) -> t -> t -> bool end +module type Null = +sig + type t + type retnull = Null | NotNull | Maybe + + val null: unit -> t + val is_null: t -> retnull + + val get_ikind: t -> Cil.ikind option + val zero_of_ikind: Cil.ikind -> t + val not_zero_of_ikind: Cil.ikind -> t +end + +module type LatticeWithNull = +sig + include LatticeWithSmartOps + include Null with type t := t +end -module Trivial (Val: Lattice.S) (Idx: Lattice.S): S with type value = Val.t and type idx = Idx.t = +module Trivial (Val: LatticeWithInvalidate) (Idx: Lattice.S): S with type value = Val.t and type idx = Idx.t = struct include Val let name () = "trivial arrays" @@ -105,6 +158,7 @@ struct let smart_widen _ _ = widen let smart_leq _ _ = leq let update_length _ x = x + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t let invariant ~value_invariant ~offset ~lval x = @@ -128,7 +182,7 @@ let factor () = | 0 -> failwith "ArrayDomain: ana.base.arrays.unrolling-factor needs to be set when using the unroll domain" | x -> x -module Unroll (Val: Lattice.S) (Idx:IntDomain.Z): S with type value = Val.t and type idx = Idx.t = +module Unroll (Val: LatticeWithInvalidate) (Idx:IntDomain.Z): S with type value = Val.t and type idx = Idx.t = struct module Factor = struct let x () = (get_int "ana.base.arrays.unrolling-factor") end module Base = Lattice.ProdList (Val) (Factor) @@ -804,7 +858,7 @@ let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) else () -module TrivialWithLength (Val: Lattice.S) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t = +module TrivialWithLength (Val: LatticeWithInvalidate) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t = struct module Base = Trivial (Val) (Idx) include Lattice.Prod (Base) (Idx) @@ -902,7 +956,7 @@ struct let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ] end -module UnrollWithLength (Val: Lattice.S) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t = +module UnrollWithLength (Val: LatticeWithInvalidate) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t = struct module Base = Unroll (Val) (Idx) include Lattice.Prod (Base) (Idx) @@ -946,6 +1000,674 @@ struct let to_yojson (x, y) = `Assoc [ (Base.name (), Base.to_yojson x); ("length", Idx.to_yojson y) ] end +module NullByte (Val: LatticeWithNull) (Idx: IntDomain.Z): Str with type value = Val.t and type idx = Idx.t = +struct + module MustSet = NullByteSet.MustSet + module MaySet = NullByteSet.MaySet + module Nulls = NullByteSet.MustMaySet + + let (<.) = Z.lt + let (<=.) = Z.leq + let (>.) = Z.gt + let (>=.) = Z.geq + let (=.) = Z.equal + let (+.) = Z.add + + (* (Must Null Set, May Null Set, Array Size) *) + include Lattice.Prod (Nulls) (Idx) + + let name () = "arrays containing null bytes" + type idx = Idx.t + type value = Val.t + + type ret = Null | NotNull | Maybe + + type substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr + + module ArrayOobMessage = M.Category.Behavior.Undefined.ArrayOutOfBounds + let warn_past_end = M.error ~category:ArrayOobMessage.past_end + + let min_nat_of_idx i = Z.max Z.zero (BatOption.default Z.zero (Idx.minimal i)) + + let get (ask: VDQ.t) (nulls, size) (e, i) = + let min_i = min_nat_of_idx i in + let max_i = Idx.maximal i in + let min_size = min_nat_of_idx size in + + match max_i, Idx.maximal size with + (* if there is no maximum value in index interval *) + | None, _ when not (Nulls.exists Possibly ((<=.) min_i) nulls) -> + (* ... return NotNull if no i >= min_i in may_nulls_set *) + NotNull + | None, _ -> + (* ... else return Top *) + Maybe + (* if there is no maximum size *) + | Some max_i, None when 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 max_i <. min_size && Nulls.interval_mem Definitely (min_i,max_i) nulls then + Null + (* ... return NotNull if no number in index interval is in may_nulls_set *) + else if not (Nulls.exists Possibly (fun x -> x >=. min_i && x <=. max_i) nulls) then + NotNull + else + Maybe + | Some max_i, Some max_size when 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 max_i <. min_size && Nulls.interval_mem Definitely (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 max_i <. max_size && not (Nulls.exists Possibly (fun x -> x >=. min_i && x <=. max_i) nulls) then + NotNull + else + Maybe + (* if maximum number in interval is invalid, i.e. negative, return Top of value *) + | _ -> Maybe + + let set (ask: VDQ.t) (nulls, size) (e, i) v = + let min_size = min_nat_of_idx size in + let min_i = min_nat_of_idx i in + let max_i = Idx.maximal i in + + let set_exact_nulls i = + match Idx.maximal size with + (* if size has no upper limit *) + | None -> + (match Val.is_null v with + | NotNull -> + Nulls.remove (if Nulls.is_full_set Possibly nulls then Possibly else Definitely) i nulls min_size + (* ... and value <> null, remove i from must_nulls_set and also from may_nulls_set if not top *) + | Null -> + Nulls.add (if i <. min_size then Definitely else Possibly) i nulls + (* i < minimal size and value = null, add i to must_nulls_set and may_nulls_set *) + (* i >= minimal size and value = null, add i only to may_nulls_set *) + | Maybe -> + let removed = Nulls.remove Possibly i nulls min_size in + Nulls.add Possibly i removed) + | Some max_size -> + (match Val.is_null v with + | NotNull -> + Nulls.remove Definitely i nulls min_size + (* if value <> null, remove i from must_nulls_set and may_nulls_set *) + | Null when i <. min_size -> + Nulls.add Definitely i nulls + | Null when i <. max_size -> + Nulls.add Possibly i nulls + | Maybe when i <. max_size -> + let removed = Nulls.remove Possibly i nulls min_size in + Nulls.add Possibly i removed + | _ -> nulls + ) + in + + let set_interval min_i max_i = + (* Update max_i so it is capped at the maximum size *) + let max_i = BatOption.map_default (fun x -> Z.min max_i @@ Z.pred x) max_i (Idx.maximal size) in + match Val.is_null v with + | NotNull -> Nulls.remove_interval Possibly (min_i, max_i) min_size nulls + | Null -> Nulls.add_interval ~maxfull:(Idx.maximal size) Possibly (min_i, max_i) nulls + | Maybe -> + let nulls = Nulls.add_interval ~maxfull:(Idx.maximal size) Possibly (min_i, max_i) nulls in + Nulls.remove_interval Possibly (min_i, max_i) min_size nulls + in + + (* warn if index is (potentially) out of bounds *) + array_oob_check (module Idx) (Nulls.get_set Possibly, size) (e, i); + let nulls = match max_i with + (* if no maximum number in index interval *) + | None -> + (* ..., value = null *) + (if Val.is_null v = Null && Idx.maximal size = None then + match Idx.maximal size with + (* ... and there is no maximal size, modify may_nulls_set to top *) + | None -> Nulls.add_all Possibly nulls + (* ... and there is a maximal size, add all i from minimal index to maximal size to may_nulls_set *) + | Some max_size -> Nulls.add_interval Possibly (min_i, Z.pred max_size) nulls + (* ... and value <> null, only keep indexes < minimal index in must_nulls_set *) + else if Val.is_null v = NotNull then + Nulls.filter_musts (Z.gt min_i) min_size nulls + (*..., value unknown *) + else + match Idx.minimal size, Idx.maximal size with + (* ... and size unknown, modify both sets to top *) + | None, None -> Nulls.top () + (* ... 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 -> + let nulls = Nulls.add_all Possibly nulls in + Nulls.filter_musts (Z.gt min_size) min_size nulls + (* ... 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 -> + let nulls = Nulls.remove_all Possibly nulls in + Nulls.add_interval Possibly (min_i, Z.pred max_size) nulls + (* ... 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 -> + let nulls = Nulls.filter_musts (Z.gt min_size) min_size nulls in + Nulls.add_interval Possibly (min_i, Z.pred max_size) nulls + ) + | Some max_i when max_i >=. Z.zero -> + if min_i =. max_i then + set_exact_nulls min_i + else + set_interval min_i max_i + (* if maximum number in interval is invalid, i.e. negative, return tuple unmodified *) + | _ -> nulls + in + (nulls, size) + + + let make ?(varAttr=[]) ?(typAttr=[]) i v = + let min_i, max_i = match Idx.minimal i, Idx.maximal i with + | Some min_i, Some max_i -> + if min_i <. Z.zero && max_i <. Z.zero then + (M.error ~category:ArrayOobMessage.before_start "Tries to create an array of negative size"; + Z.zero, Some Z.zero) + else if min_i <. Z.zero then + (M.warn ~category:ArrayOobMessage.before_start "May try to create an array of negative size"; + Z.zero, Some max_i) + else + min_i, Some max_i + | None, Some max_i -> + if max_i <. Z.zero then + (M.error ~category:ArrayOobMessage.before_start "Tries to create an array of negative size"; + Z.zero, Some Z.zero) + else + Z.zero, Some max_i + | Some min_i, None -> + if min_i <. Z.zero then + (M.warn ~category:ArrayOobMessage.before_start "May try to create an array of negative size"; + Z.zero, None) + else + min_i, None + | None, None -> Z.zero, None + in + let size = BatOption.map_default (fun max -> Idx.of_interval ILong (min_i, max)) (Idx.starting ILong min_i) max_i in + match Val.is_null v with + | Null -> (Nulls.make_all_must (), size) + | NotNull -> (Nulls.empty (), size) + | Maybe -> (Nulls.top (), size) + + + let length (_, size) = Some size + + let move_if_affected ?(replace_with_const=false) _ x _ _ = x + + let get_vars_in_e _ = [] + + let map f (nulls, size) = + (* if f(null) = null, all values in must_nulls_set still are surely null; + * assume top for may_nulls_set as checking effect of f for every possible value is unfeasbile *) + match Val.is_null (f (Val.null ())) with + | Null -> (Nulls.add_all Possibly nulls, size) + | _ -> (Nulls.top (), size) (* else also return top for must_nulls_set *) + + let fold_left f acc _ = f acc (Val.top ()) + + let smart_join _ _ = join + let smart_widen _ _ = widen + let smart_leq _ _ = leq + + (* string functions *) + + let to_null_byte_domain s = + let last_null = Z.of_int (String.length s) in + let rec build_set i set = + if (Z.of_int i) >=. last_null then + Nulls.Set.add last_null set + else + match String.index_from_opt s i '\x00' with + | Some i -> build_set (i + 1) (Nulls.Set.add (Z.of_int i) set) + | None -> Nulls.Set.add last_null set in + let set = build_set 0 (Nulls.Set.empty ()) in + (Nulls.precise_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 ((nulls, size) as x:t):t = + (* 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 Nulls.is_empty Definitely nulls then + (warn_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 Nulls.is_empty Possibly nulls then + (warn_past_end "May access array past end: potential buffer overflow"; x) + else + let min_must_null = Nulls.min_elem Definitely nulls in + let new_size = Idx.of_int ILong (Z.succ min_must_null) in + let min_may_null = Nulls.min_elem Possibly nulls in + (* if smallest index in sets coincides, only this null byte is kept in both sets *) + let nulls = + if min_must_null =. min_may_null then + Nulls.precise_singleton 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 + | Some max_size -> + let nulls' = Nulls.remove_all Possibly nulls in + Nulls.filter ~max_size (Z.leq min_must_null) nulls' + | None when not (Nulls.may_can_benefit_from_filter nulls) -> + Nulls.add_interval Possibly (Z.zero, min_must_null) (Nulls.empty ()) + | None -> + let nulls' = Nulls.remove_all Possibly nulls in + Nulls.filter (Z.leq min_must_null) nulls' + in + (nulls, new_size) + + (** [to_n_string index_set n] returns an abstract value with a potential null byte + * marking the end of the string and if needed followed by further null bytes to obtain + * an n bytes string. *) + let to_n_string (nulls, size) n:t = + if n < 0 then + (Nulls.top (), Idx.top_of ILong) + else + let n = Z.of_int n in + let warn_no_null min_must_null min_may_null = + if Z.geq min_may_null n then + M.warn "Resulting string might not be null-terminated because src doesn't contain a null byte in the first n bytes" + else + (match min_must_null with + | Some min_must_null when not (min_must_null >=. n || min_must_null >. min_may_null) -> () + | _ -> + M.warn "Resulting string might not be null-terminated because src might not contain a null byte in the first n bytes" + ) + in + (match Idx.minimal size, Idx.maximal size with + | Some min_size, Some max_size -> + if n >. max_size then + warn_past_end "Array size is smaller than n bytes; can cause a buffer overflow" + else if n >. min_size then + warn_past_end "Array size might be smaller than n bytes; can cause a buffer overflow" + | Some min_size, None -> + if n >. min_size then + warn_past_end "Array size might be smaller than n bytes; can cause a buffer overflow" + | None, Some max_size -> + if n >. max_size then + warn_past_end "Array size is smaller than n bytes; can cause a buffer overflow" + | None, None -> ()); + let nulls = + (* if definitely no null byte in array, i.e. must_nulls_set = may_nulls_set = empty set *) + if Nulls.is_empty Definitely nulls then + (warn_past_end + "Resulting string might not be null-terminated because src doesn't contain a null byte"; + match Idx.maximal size with + (* ... there *may* be null bytes from maximal size to n - 1 if maximal size < n (i.e. past end) *) + | Some max_size when Z.geq max_size Z.zero -> Nulls.add_interval Possibly (max_size, Z.pred n) nulls + | _ -> nulls) + (* 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 Nulls.is_empty Possibly nulls then + let min_may_null = Nulls.min_elem Possibly nulls in + warn_no_null None min_may_null; + if min_may_null =. Z.zero then + Nulls.add_all Possibly nulls + else + let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in + Nulls.filter (fun x -> x <. n) nulls + else + let min_must_null = Nulls.min_elem Definitely nulls in + let min_may_null = Nulls.min_elem Possibly nulls in + (* warn if resulting array may not contain null byte *) + warn_no_null (Some min_must_null) 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 *) + if min_must_null =. min_may_null then + if min_must_null =. Z.zero then + Nulls.full_set () + else + let nulls = Nulls.add_interval Definitely (min_must_null, Z.pred n) nulls in + let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in + Nulls.filter (fun x -> x <. n) nulls + else if min_may_null =. Z.zero then + Nulls.top () + else + let nulls = Nulls.remove_all Possibly nulls in + let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in + Nulls.filter (fun x -> x <. n) nulls + in + (nulls, Idx.of_int ILong n) + + let to_string_length (nulls, size) = + (* if must_nulls_set and min_nulls_set empty, definitely no null byte in array => return interval [size, inf) and warn *) + if Nulls.is_empty Definitely nulls then + (warn_past_end "Array doesn't contain a null byte: buffer overflow"; + Idx.starting !Cil.kindOfSizeOf (BatOption.default Z.zero (Idx.minimal size)) + ) + (* if only must_nulls_set empty, no guarantee that null ever encountered in array => return interval [minimal may null, inf) and *) + else if Nulls.is_empty Possibly nulls then + (warn_past_end "Array might not contain a null byte: potential buffer overflow"; + Idx.starting !Cil.kindOfSizeOf (Nulls.min_elem Possibly nulls)) + (* else return interval [minimal may null, minimal must null] *) + else + Idx.of_interval !Cil.kindOfSizeOf (Nulls.min_elem Possibly nulls, Nulls.min_elem Definitely nulls) + + let string_copy (dstnulls, dstsize) ((srcnulls, srcsize) as src) n = + let must_nulls_set1, may_nulls_set1 = dstnulls in + (* filter out indexes before strlen(src) from dest sets and after strlen(src) from src sets and build union, keep size of dest *) + let update_sets (truncatednulls, truncatedsize) len2 = + let must_nulls_set2',may_nulls_set2' = truncatednulls in + match Idx.minimal dstsize, Idx.maximal dstsize, Idx.minimal len2, Idx.maximal len2 with + | Some min_dstsize, Some max_dstsize, Some min_srclen, Some max_srclen -> + (if max_dstsize <. min_srclen then + warn_past_end "The length of string src is greater than the allocated size for dest" + else if min_dstsize <. max_srclen then + warn_past_end "The length of string src may be greater than the allocated size for dest"); + let must_nulls_set_result = + let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in + (* get must nulls from src string < minimal size of dest *) + MustSet.filter ~min_size:min_size2 (Z.gt min_dstsize) must_nulls_set2' + (* and keep indexes of dest >= maximal strlen of src *) + |> MustSet.union (MustSet.filter ~min_size:min_dstsize (Z.leq max_srclen) must_nulls_set1) in + let may_nulls_set_result = + let max_size2 = BatOption.default max_dstsize (Idx.maximal truncatedsize) in + (* get may nulls from src string < maximal size of dest *) + MaySet.filter ~max_size:max_size2 (Z.gt max_dstsize) may_nulls_set2' + (* and keep indexes of dest >= minimal strlen of src *) + |> MaySet.union (MaySet.filter ~max_size:max_dstsize (Z.leq min_srclen) may_nulls_set1) in + ((must_nulls_set_result, may_nulls_set_result), dstsize) + + + | Some min_size1, None, Some min_len2, Some max_len2 -> + (if min_size1 <. max_len2 then + warn_past_end "The length of string src may be greater than the allocated size for dest"); + let must_nulls_set_result = + let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in + MustSet.filter ~min_size: min_size2 (Z.gt min_size1) must_nulls_set2' + |> MustSet.union (MustSet.filter ~min_size:min_size1 (Z.leq max_len2) must_nulls_set1) in + let may_nulls_set_result = + (* get all may nulls from src string as no maximal size of dest *) + may_nulls_set2' + |> MaySet.union (MaySet.filter ~max_size:(Z.succ min_len2) (Z.leq min_len2) may_nulls_set1) in + ((must_nulls_set_result, may_nulls_set_result), dstsize) + | Some min_size1, Some max_size1, Some min_len2, None -> + (if max_size1 <. min_len2 then + warn_past_end "The length of string src is greater than the allocated size for dest" + else if min_size1 <. min_len2 then + warn_past_end"The length of string src may be greater than the allocated size for dest"); + (* do not keep any index of dest as no maximal strlen of src *) + let must_nulls_set_result = + let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in + MustSet.filter ~min_size:min_size2 (Z.gt min_size1) must_nulls_set2' in + let may_nulls_set_result = + let max_size2 = BatOption.default max_size1 (Idx.maximal truncatedsize) in + MaySet.filter ~max_size:max_size2 (Z.gt max_size1) may_nulls_set2' + |> MaySet.union (MaySet.filter ~max_size:max_size1 (Z.leq min_len2) may_nulls_set1) in + ((must_nulls_set_result, may_nulls_set_result), dstsize) + | Some min_size1, None, Some min_len2, None -> + (if min_size1 <. min_len2 then + warn_past_end "The length of string src may be greater than the allocated size for dest"); + (* do not keep any index of dest as no maximal strlen of src *) + let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in + let truncatednulls = Nulls.remove_interval Possibly (Z.zero, min_size1) min_size2 truncatednulls in + let filtered_dst = Nulls.filter ~max_size:(Z.succ min_len2) (Z.leq min_len2) dstnulls in + (* get all may nulls from src string as no maximal size of dest *) + (Nulls.union_mays truncatednulls filtered_dst, dstsize) + (* any other case shouldn't happen as minimal index is always >= 0 *) + | _ -> (Nulls.top (), dstsize) in + + (* warn if size of dest is (potentially) smaller than size of src and the latter (potentially) has no null byte at index < size of dest *) + let sizes_warning srcsize = + (match Idx.minimal dstsize, Idx.maximal dstsize, Idx.minimal srcsize, Idx.maximal srcsize with + | Some min_dstsize, _, Some min_srcsize, _ when min_dstsize <. min_srcsize -> + if not (Nulls.exists Possibly (Z.gt min_dstsize) srcnulls) then + warn_past_end "src doesn't contain a null byte at an index smaller than the size of dest" + else if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then + warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + | Some min_dstsize, _, _, Some max_srcsize when min_dstsize <. max_srcsize -> + if not (Nulls.exists Possibly (Z.gt min_dstsize) srcnulls) then + warn_past_end "src doesn't contain a null byte at an index smaller than the size of dest" + else if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then + warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + | Some min_dstsize, _, _, None -> + if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then + warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + | _, Some mac_dstsize, _, Some max_srcsize when mac_dstsize <. max_srcsize -> + if not (Nulls.exists Definitely (Z.gt mac_dstsize) srcnulls) then + warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + |_, Some max_dstsize, _, None -> + if not (Nulls.exists Definitely (Z.gt max_dstsize) srcnulls) then + warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + | _ -> ()) in + + match n with + (* strcpy *) + | None -> + sizes_warning srcsize; + let truncated = to_string src in + update_sets truncated (to_string_length src) + (* strncpy = exactly n bytes from src are copied to dest *) + | Some n when n >= 0 -> + sizes_warning (Idx.of_int ILong (Z.of_int n)); + let truncated = to_n_string src n in + update_sets truncated (Idx.of_int !Cil.kindOfSizeOf (Z.of_int n)) + | _ -> (Nulls.top (), dstsize) + + let string_concat (nulls1, size1) (nulls2, size2) n = + let update_sets min_size1 max_size1 minlen1 maxlen1 minlen2 (maxlen2: Z.t option) nulls2' = + (* track any potential buffer overflow and issue warning if needed *) + (if GobOption.exists (fun x -> x <=. (minlen1 +. minlen2)) max_size1 then + warn_past_end + "The length of the concatenation of the strings in src and dest is greater than the allocated size for dest" + else + (match maxlen1, maxlen2 with + | Some maxlen1, Some maxlen2 when min_size1 >. (maxlen1 +. maxlen2) -> () + | _ -> warn_past_end + "The length of the concatenation of the strings in src and dest may be greater than the allocated size for dest") + ); + (* if any must_nulls_set empty, result must_nulls_set also empty; + * for all i1, i2 in may_nulls_set1, may_nulls_set2: add i1 + i2 if it is <= strlen(dest) + strlen(src) to new may_nulls_set + * and keep indexes > minimal strlen(dest) + strlen(src) of may_nulls_set *) + if Nulls.is_empty Possibly nulls1 || Nulls.is_empty Possibly nulls2 then + match max_size1 with + | Some max_size1 -> + let nulls1_no_must = Nulls.remove_all Possibly nulls1 in + let pred = match maxlen1, maxlen2 with + | Some maxlen1, Some maxlen2 -> (fun x -> x <=. (maxlen1 +. maxlen2)) + | _ -> (fun _ -> true) + in + let r = + nulls1_no_must + (* filter ensures we have the concete representation *) + |> Nulls.filter ~max_size:max_size1 pred + |> Nulls.elements ~max_size:max_size1 Possibly + |> BatList.cartesian_product (Nulls.elements ~max_size:max_size1 Possibly nulls2') + |> List.map (fun (i1, i2) -> i1 +. i2) + |> (fun x -> Nulls.add_list Possibly x (Nulls.filter ~max_size:max_size1 (Z.lt (minlen1 +. minlen2)) nulls1_no_must)) + |> Nulls.filter (Z.gt max_size1) + in + (r, size1) + | None when Nulls.may_can_benefit_from_filter nulls1 && Nulls.may_can_benefit_from_filter nulls2 -> + (match maxlen1, maxlen2 with + | Some maxlen1, Some maxlen2-> + let nulls1_no_must = Nulls.remove_all Possibly nulls1 in + let r = + nulls1_no_must + (* filter ensures we have the concete representation *) + |> Nulls.filter (fun x -> x <=. (maxlen1 +. maxlen2)) + |> Nulls.elements Possibly + |> BatList.cartesian_product (Nulls.elements Possibly nulls2') + |> List.map (fun (i1, i2) -> i1 +. i2) + |> (fun x -> Nulls.add_list Possibly x (Nulls.filter (Z.lt (minlen1 +. minlen2)) nulls1_no_must)) + in + (r, size1) + | _ -> (Nulls.top (), size1)) + | _ -> (Nulls.top (), size1) + (* if minimal must null = minimal may null in ar1 and ar2, add them together and keep indexes > strlen(dest) + strlen(src) of ar1 *) + else if Nulls.min_elem_precise nulls1 && Nulls.min_elem_precise nulls2' then + let min_i1 = Nulls.min_elem Definitely nulls1 in + let min_i2 = Nulls.min_elem Definitely nulls2' in + let min_i = min_i1 +. min_i2 in + let (must_nulls_set1, may_nulls_set1) = nulls1 in + let must_nulls_set_result = + MustSet.filter ~min_size:min_size1 (Z.lt min_i) must_nulls_set1 + |> MustSet.add min_i + |> MustSet.M.filter (Z.gt min_size1) in + let may_nulls_set_result = + match max_size1 with + | Some max_size1 -> + MaySet.filter ~max_size:max_size1 (Z.lt min_i) may_nulls_set1 + |> MaySet.add min_i + |> MaySet.M.filter (fun x -> max_size1 >. x) + | _ -> MaySet.top () + in + ((must_nulls_set_result, may_nulls_set_result), size1) + (* else only add all may nulls together <= strlen(dest) + strlen(src) *) + else + let min_i2 = Nulls.min_elem Definitely nulls2' in + let (must_nulls_set1, may_nulls_set1) = nulls1 in + let (must_nulls_set2', may_nulls_set2') = nulls2' in + let may_nulls_set2'_until_min_i2 = + match Idx.maximal size2 with + | Some max_size2 -> MaySet.filter ~max_size:max_size2 (Z.geq min_i2) may_nulls_set2' + | None -> MaySet.filter ~max_size:(Z.succ min_i2) (Z.geq min_i2) may_nulls_set2' in + let must_nulls_set_result = + let pred = match maxlen1, maxlen2 with + | Some maxlen1, Some maxlen2 -> (fun x -> (maxlen1 +. maxlen2) <. x) + | _ -> (fun _ -> false) + in + MustSet.filter ~min_size:min_size1 pred must_nulls_set1 + in + let may_nulls_set_result = + let pred = match maxlen1, maxlen2 with + | Some maxlen1, Some maxlen2 -> (fun x -> x <=. (maxlen1 +. maxlen2)) + | _ -> (fun _ -> true) + in + match max_size1 with + | Some max_size1 -> + MaySet.filter ~max_size:max_size1 pred may_nulls_set1 + |> MaySet.elements + |> BatList.cartesian_product (MaySet.elements may_nulls_set2'_until_min_i2) + |> List.map (fun (i1, i2) -> i1 +. i2) + |> MaySet.of_list + |> MaySet.union (MaySet.filter ~max_size:max_size1 (Z.lt (minlen1 +. minlen2)) may_nulls_set1) + |> MaySet.M.filter (fun x -> max_size1 >. x) + | None when not (MaySet.is_top may_nulls_set1) -> + MaySet.M.filter pred may_nulls_set1 + |> MaySet.elements + |> BatList.cartesian_product (MaySet.elements may_nulls_set2'_until_min_i2) + |> List.map (fun (i1, i2) -> i1 +. i2) + |> MaySet.of_list + |> MaySet.union (MaySet.M.filter (Z.lt (minlen1 +. minlen2)) may_nulls_set1) + | _ -> + MaySet.top () in + ((must_nulls_set_result, may_nulls_set_result), size1) in + + let compute_concat nulls2' = + let strlen1 = to_string_length (nulls1, size1) in + let strlen2 = to_string_length (nulls2', size2) in + match Idx.minimal size1, Idx.minimal strlen1, Idx.minimal strlen2 with + | Some min_size1, Some minlen1, Some minlen2 -> + begin + let f = update_sets min_size1 (Idx.maximal size1) minlen1 in + match Idx.maximal strlen1, Idx.maximal strlen2 with + | (Some _ as maxlen1), (Some _ as maxlen2) -> f maxlen1 minlen2 maxlen2 nulls2' + | _ -> f None minlen2 None nulls2' + end + (* any other case shouldn't happen as minimal index is always >= 0 *) + | _ -> (Nulls.top (), size1) in + + match n with + (* strcat *) + | None -> + let nulls2', _ = to_string (nulls2, size2) in + compute_concat nulls2' + (* strncat *) + | Some n when n >= 0 -> + let n = Z.of_int n in + (* take at most n bytes from src; if no null byte among them, add null byte at index n *) + let nulls2' = + let (nulls2, size2) = to_string (nulls2, size2) in + if not (Nulls.exists Possibly (Z.gt n) nulls2) then + Nulls.precise_singleton n + else if not (Nulls.exists Definitely (Z.gt n) nulls2) then + let max_size = BatOption.default (Z.succ n) (Idx.maximal size2) in + let nulls2 = Nulls.remove_all Possibly nulls2 in + let nulls2 = Nulls.filter ~max_size (Z.geq n) nulls2 in + Nulls.add Possibly n nulls2 + else + let min_size = BatOption.default Z.zero (Idx.minimal size2) in + let max_size = BatOption.default n (Idx.maximal size2) in + Nulls.filter ~max_size ~min_size (Z.gt n) nulls2 + in + compute_concat nulls2' + | _ -> (Nulls.top (), size1) + + let substring_extraction haystack ((nulls_needle, size_needle) as needle) = + (* if needle is empty string, i.e. certain null byte at index 0, return value of strstr is pointer to haystack *) + if Nulls.mem Definitely Z.zero nulls_needle then + IsSubstrAtIndex0 + else + let haystack_len = to_string_length haystack 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 when haystack_max <. needle_min -> + (* if strlen(haystack) < strlen(needle), needle can never be substring of haystack => return None *) + IsNotSubstr + | _ -> IsMaybeSubstr + + let string_comparison (nulls1, size1) (nulls2, size2) n = + let cmp n = + (* if s1 = s2 = empty string, i.e. certain null byte at index 0, or n = 0, return 0 *) + if (Nulls.mem Definitely Z.zero nulls1 && Nulls.mem Definitely Z.zero nulls2) || (BatOption.map_default (Z.equal Z.zero) false n) then + Idx.of_int IInt Z.zero + (* if only s1 = empty string, return negative integer *) + else if Nulls.mem Definitely Z.zero nulls1 && not (Nulls.mem Possibly Z.zero nulls2) then + Idx.ending IInt Z.minus_one + (* if only s2 = empty string, return positive integer *) + else if Nulls.mem Definitely Z.zero nulls2 then + Idx.starting IInt Z.one + else + try + let min_must1 = Nulls.min_elem Definitely nulls1 in + let min_must2 = Nulls.min_elem Definitely nulls2 in + if not (min_must1 =. min_must2) + && min_must1 =.(Nulls.min_elem Possibly nulls1) + && min_must2 =. (Nulls.min_elem Possibly nulls2) + && (BatOption.map_default (fun x -> min_must1 <. x || min_must2 <. x) true n) + then + (* if first null bytes are certain, have different indexes and are before index n if n present, return integer <> 0 *) + Idx.of_excl_list IInt [Z.zero] + else + Idx.top_of IInt + with Not_found -> Idx.top_of IInt + in + + match n with + (* strcmp *) + | None -> + (* track any potential buffer overflow and issue warning if needed *) + let warn_missing_nulls nulls name = + if Nulls.is_empty Definitely nulls then + warn_past_end "Array of string %s doesn't contain a null byte: buffer overflow" name + else if Nulls.is_empty Possibly nulls then + warn_past_end "Array of string %s might not contain a null byte: potential buffer overflow" name + in + warn_missing_nulls nulls1 "1"; + warn_missing_nulls nulls2 "2"; + (* compute abstract value for result of strcmp *) + cmp None + (* strncmp *) + | Some n when n >= 0 -> + let n = Z.of_int n in + let warn_size size name = + let min = min_nat_of_idx size in + match Idx.maximal size with + | Some max when n >. max -> + warn_past_end "The size of the array of string %s is smaller than n bytes" name + | Some max when n >. min -> + warn_past_end "The size of the array of string %s might be smaller than n bytes" name + | None when n >. min -> + warn_past_end "The size of the array of string %s might be smaller than n bytes" name + | _ -> () + in + warn_size size1 "1"; + warn_size size2 "2"; + (* compute abstract value for result of strncmp *) + cmp (Some n) + | _ -> Idx.top_of IInt + + let update_length new_size (nulls, size) = (nulls, new_size) + + let project ?(varAttr=[]) ?(typAttr=[]) _ t = t + + let invariant ~value_invariant ~offset ~lval x = Invariant.none +end + module AttributeConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t = struct module P = PartitionedWithLength(Val)(Idx) @@ -999,7 +1721,7 @@ struct let smart_widen f g = binop_to_t' (P.smart_widen f g) (T.smart_widen f g) (U.smart_widen f g) let smart_leq f g = binop' (P.smart_leq f g) (T.smart_leq f g) (U.smart_leq f g) let update_length newl x = unop_to_t' (P.update_length newl) (T.update_length newl) (U.update_length newl) x - let name () = "AttributeConfiguredArrayDomain" + let name () = "FlagHelperAttributeConfiguredArrayDomain" let bot () = to_t @@ match get_domain ~varAttr:[] ~typAttr:[] with | PartitionedDomain -> (Some (P.bot ()), None, None) @@ -1067,3 +1789,91 @@ struct (T.invariant ~value_invariant ~offset ~lval) (U.invariant ~value_invariant ~offset ~lval) end + +module AttributeConfiguredAndNullByteArrayDomain (Val: LatticeWithNull) (Idx: IntDomain.Z): StrWithDomain with type value = Val.t and type idx = Idx.t = +struct + module A = AttributeConfiguredArrayDomain (Val) (Idx) + module N = NullByte (Val) (Idx) + + include Lattice.Prod (A) (N) + + let name () = "AttributeConfiguredAndNullByteArrayDomain" + type idx = Idx.t + type value = Val.t + + type ret = Null | NotNull | Maybe + type substr = N.substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr + + let domain_of_t (t_f, _) = A.domain_of_t t_f + + let get ?(checkBounds=true) (ask: VDQ.t) (t_f, t_n) i = + let f_get = A.get ~checkBounds ask t_f i in + if get_bool "ana.base.arrays.nullbytes" then + let n_get = N.get ask t_n i in + match Val.get_ikind f_get, n_get with + | Some ik, Null -> Val.meet f_get (Val.zero_of_ikind ik) + | Some ik, NotNull -> Val.meet f_get (Val.not_zero_of_ikind ik) + | _ -> f_get + else + f_get + + let construct a n = + if get_bool "ana.base.arrays.nullbytes" then + (a, n ()) + else + (a, N.top ()) + + let set (ask:VDQ.t) (t_f, t_n) i v = construct (A.set ask t_f i v) (fun () -> N.set ask t_n i v) + let make ?(varAttr=[]) ?(typAttr=[]) i v = construct (A.make ~varAttr ~typAttr i v) (fun () -> N.make ~varAttr ~typAttr i v) + let map f (t_f, t_n) = construct (A.map f t_f) (fun () -> N.map f t_n) + let update_length newl (t_f, t_n) = construct (A.update_length newl t_f) (fun () -> N.update_length newl t_n) + + let smart_binop op_a op_n x y (t_f1, t_n1) (t_f2, t_n2) = construct (op_a x y t_f1 t_f2) (fun () -> op_n x y t_n1 t_n2) + + let smart_join = smart_binop A.smart_join N.smart_join + let smart_widen = smart_binop A.smart_widen N.smart_widen + + let string_op op (t_f1, t_n1) (_, t_n2) n = construct (A.map Val.invalidate_abstract_value t_f1) (fun () -> op t_n1 t_n2 n) + let string_copy = string_op N.string_copy + let string_concat = string_op N.string_concat + + let extract op default (_, t_n1) (_, t_n2) n = + if get_bool "ana.base.arrays.nullbytes" then + op t_n1 t_n2 n + else + (* Hidden behind unit, as constructing defaults may happen to early otherwise *) + (* e.g. for Idx.top_of IInt *) + default () + + let substring_extraction x y = extract (fun x y _ -> N.substring_extraction x y) (fun () -> IsMaybeSubstr) x y None + let string_comparison = extract N.string_comparison (fun () -> Idx.top_of IInt) + + let length (t_f, t_n) = + if get_bool "ana.base.arrays.nullbytes" then + N.length t_n + else + A.length t_f + let move_if_affected ?(replace_with_const=false) (ask:VDQ.t) (t_f, t_n) v f = (A.move_if_affected ~replace_with_const ask t_f v f, N.move_if_affected ~replace_with_const ask t_n v f) + let get_vars_in_e (t_f, _) = A.get_vars_in_e t_f + let fold_left f acc (t_f, _) = A.fold_left f acc t_f + + let smart_leq x y (t_f1, t_n1) (t_f2, t_n2) = + if get_bool "ana.base.arrays.nullbytes" then + A.smart_leq x y t_f1 t_f2 && N.smart_leq x y t_n1 t_n2 + else + A.smart_leq x y t_f1 t_f2 + + let to_null_byte_domain s = + if get_bool "ana.base.arrays.nullbytes" then + (A.make (Idx.top_of ILong) (Val.meet (Val.not_zero_of_ikind IChar) (Val.zero_of_ikind IChar)), N.to_null_byte_domain s) + else + (A.top (), N.top ()) + let to_string_length (_, t_n) = + if get_bool "ana.base.arrays.nullbytes" then + N.to_string_length t_n + else + Idx.top_of !Cil.kindOfSizeOf + + let project ?(varAttr=[]) ?(typAttr=[]) ask (t_f, t_n) = (A.project ~varAttr ~typAttr ask t_f, N.project ~varAttr ~typAttr ask t_n) + let invariant ~value_invariant ~offset ~lval (t_f, _) = A.invariant ~value_invariant ~offset ~lval t_f +end diff --git a/src/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli index ebf265ac0b..9b5a713859 100644 --- a/src/cdomains/arrayDomain.mli +++ b/src/cdomains/arrayDomain.mli @@ -12,8 +12,7 @@ val get_domain: varAttr:Cil.attributes -> typAttr:Cil.attributes -> domain val can_recover_from_top: domain -> bool (** Some domains such as Trivial cannot recover from their value ever being top. {!ValueDomain} handles intialization differently for these *) -(** Abstract domains representing arrays. *) -module type S = +module type S0 = sig include Lattice.S type idx @@ -22,12 +21,6 @@ sig type value (** The abstract domain of values stored in the array. *) - val domain_of_t: t -> domain - (* Returns the domain used for the array*) - - val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value - (** Returns the element residing at the given index. *) - val set: VDQ.t -> t -> Basetype.CilExp.t option * idx -> value -> t (** Returns a new abstract value, where the given index is replaced with the * given element. *) @@ -57,25 +50,104 @@ sig val smart_widen: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> t val smart_leq: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> bool val update_length: idx -> t -> t - val project: ?varAttr:Cil.attributes -> ?typAttr:Cil.attributes -> VDQ.t -> t -> t val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t end -module type LatticeWithSmartOps = +(** Abstract domains representing arrays. *) +module type S = +sig + include S0 + + val domain_of_t: t -> domain + (* Returns the domain used for the array*) + + val get: ?checkBounds:bool -> VDQ.t -> t -> Basetype.CilExp.t option * idx -> value + (** Returns the element residing at the given index. *) +end + +(** Abstract domains representing strings a.k.a. null-terminated char arrays. *) +module type Str = +sig + include S0 + + type ret = Null | NotNull | Maybe + type substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr + + val get: VDQ.t -> t -> Basetype.CilExp.t option * idx -> ret + (* overwrites get of module S *) + + val to_null_byte_domain: string -> t + (* Converts a string to its abstract value in the NullByte domain *) + + val to_string_length: t -> idx + (** Returns length of string represented by input abstract value *) + + val string_copy: t -> t -> int option -> t + (** [string_copy dest src n] returns an abstract value representing the copy of string [src] + * into array [dest], taking at most [n] bytes of [src] if present *) + + val string_concat: t -> t -> int option -> t + (** [string_concat s1 s2 n] returns a new abstract value representing the string + * concatenation of the input abstract values [s1] and [s2], taking at most [n] bytes of + * [s2] if present *) + + val substring_extraction: t -> t -> substr + (** [substring_extraction haystack needle] returns {!IsNotSubstr} if the string represented by + * the abstract value [needle] surely isn't a substring of [haystack], {!IsSubstrAtIndex0} if + * [needle] is the empty string, else {!IsMaybeSubstr} *) + + val string_comparison: t -> t -> int option -> idx + (** [string_comparison s1 s2 n] returns a negative / positive idx element if the string + * represented by [s1] is less / greater than the one by [s2] or zero if they are equal; + * only compares the first [n] bytes if present *) +end + +module type StrWithDomain = +sig + include Str + include S with type t := t and type idx := idx +end + +module type LatticeWithInvalidate = sig include Lattice.S + val invalidate_abstract_value: t -> t +end + +module type LatticeWithSmartOps = +sig + include LatticeWithInvalidate val smart_join: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> t val smart_widen: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> t val smart_leq: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> bool end -module Trivial (Val: Lattice.S) (Idx: Lattice.S): S with type value = Val.t and type idx = Idx.t +module type Null = +sig + type t + type retnull = Null | NotNull | Maybe + + val null: unit -> t + val is_null: t -> retnull + + val get_ikind: t -> Cil.ikind option + val zero_of_ikind: Cil.ikind -> t + val not_zero_of_ikind: Cil.ikind -> t +end + +module type LatticeWithNull = +sig + include LatticeWithSmartOps + include Null with type t := t +end + +module Trivial (Val: LatticeWithInvalidate) (Idx: Lattice.S): S with type value = Val.t and type idx = Idx.t (** This functor creates a trivial single cell representation of an array. The * indexing type is taken as a parameter to satisfy the type system, it is not * used in the implementation. *) -module TrivialWithLength (Val: Lattice.S) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t +module TrivialWithLength (Val: LatticeWithInvalidate) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t (** This functor creates a trivial single cell representation of an array. The * indexing type is also used to manage the length. *) @@ -90,5 +162,18 @@ module Partitioned (Val: LatticeWithSmartOps) (Idx: IntDomain.Z): S with type va module PartitionedWithLength (Val: LatticeWithSmartOps) (Idx:IntDomain.Z): S with type value = Val.t and type idx = Idx.t (** Like partitioned but additionally manages the length of the array. *) -module AttributeConfiguredArrayDomain(Val: LatticeWithSmartOps) (Idx:IntDomain.Z):S with type value = Val.t and type idx = Idx.t +module NullByte (Val: LatticeWithNull) (Idx: IntDomain.Z): Str with type value = Val.t and type idx = Idx.t +(** This functor creates an array representation by the indexes of all null bytes + * the array must and may contain. This is useful to analyze strings, i.e. null- + * terminated char arrays, and particularly to determine if operations on strings + * could lead to a buffer overflow. Concrete values from Val are not interesting + * for this domain. It additionally tracks the array size. +*) + +module AttributeConfiguredArrayDomain (Val: LatticeWithSmartOps) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t (** Switches between PartitionedWithLength, TrivialWithLength and Unroll based on variable, type, and flag. *) + +module AttributeConfiguredAndNullByteArrayDomain (Val: LatticeWithNull) (Idx: IntDomain.Z): StrWithDomain with type value = Val.t and type idx = Idx.t +(** Like FlagHelperAttributeConfiguredArrayDomain but additionally runs NullByte + * in parallel if flag "ana.base.arrays.nullbytes" is set. +*) diff --git a/src/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml new file mode 100644 index 0000000000..38fe5cbda9 --- /dev/null +++ b/src/cdomains/nullByteSet.ml @@ -0,0 +1,200 @@ +module MustSet = struct + module M = SetDomain.Reverse (SetDomain.ToppedSet (IntDomain.BigInt) (struct let topname = "All Null" end)) + include M + + let compute_set len = + List.init (Z.to_int len) Z.of_int + |> of_list + + let remove i must_nulls_set min_size = + if M.is_bot must_nulls_set then + M.remove i (compute_set min_size) + else + M.remove i must_nulls_set + + let filter ?min_size cond must_nulls_set = + if M.is_bot must_nulls_set then + match min_size with + | Some min_size -> M.filter cond (compute_set min_size) + | _ -> M.empty () + else + M.filter cond must_nulls_set + + let min_elt must_nulls_set = + if M.is_bot must_nulls_set then + Z.zero + else + M.min_elt must_nulls_set + + let interval_mem (l,u) set = + if M.is_bot set then + true + else if Z.lt (Z.of_int (M.cardinal set)) (Z.sub u l) then + false + else + let rec check_all_indexes i = + if Z.gt i u then + true + else if M.mem i set then + check_all_indexes (Z.succ i) + else + false in + check_all_indexes l +end + +module MaySet = struct + module M = SetDomain.ToppedSet (IntDomain.BigInt) (struct let topname = "All Null" end) + include M + + let elements ?max_size may_nulls_set = + if M.is_top may_nulls_set then + match max_size with + | Some max_size -> M.elements @@ MustSet.compute_set max_size + | _ -> failwith "top and no max size supplied" + else + M.elements may_nulls_set + + let remove i may_nulls_set max_size = + if M.is_top may_nulls_set then + M.remove i (MustSet.compute_set max_size) + else + M.remove i may_nulls_set + + let filter ?max_size cond may_nulls_set = + if M.is_top may_nulls_set then + match max_size with + | Some max_size -> M.filter cond (MustSet.compute_set max_size) + | _ -> may_nulls_set + else + M.filter cond may_nulls_set + + let min_elt may_nulls_set = + if M.is_top may_nulls_set then + Z.zero + else + M.min_elt may_nulls_set +end + +module MustMaySet = struct + include Lattice.Prod (MustSet) (MaySet) + + module Set = SetDomain.Make (IntDomain.BigInt) + + type mode = Definitely | Possibly + + let empty () = (MustSet.top (), MaySet.bot ()) + + let full_set () = (MustSet.bot (), MaySet.top ()) + + let is_empty mode (musts, mays) = + match mode with + | Definitely -> MaySet.is_empty mays + | Possibly -> MustSet.is_empty musts + + let min_elem mode (musts, mays) = + match mode with + | Definitely -> MustSet.min_elt musts + | Possibly -> MaySet.min_elt mays + + let min_elem_precise x = + Z.equal (min_elem Definitely x) (min_elem Possibly x) + + let mem mode i (musts, mays) = + match mode with + | Definitely -> MustSet.mem i musts + | Possibly -> MaySet.mem i mays + + let interval_mem mode (l,u) (musts, mays) = + match mode with + | Definitely -> MustSet.interval_mem (l,u) musts + | Possibly -> failwith "not implemented" + + let remove mode i (musts, mays) min_size = + match mode with + | Definitely -> (MustSet.remove i musts min_size, MaySet.remove i mays min_size) + | Possibly -> (MustSet.remove i musts min_size, mays) + + let add mode i (musts, mays) = + match mode with + | Definitely -> (MustSet.add i musts, MaySet.add i mays) + | Possibly -> (musts, MaySet.add i mays) + + let add_list mode l (musts, mays) = + match mode with + | Definitely -> failwith "todo" + | Possibly -> (musts, MaySet.union (MaySet.of_list l) mays) + + let add_interval ?maxfull mode (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 + let mays = + match maxfull with + | Some Some maxfull when Z.equal l Z.zero && Z.geq u maxfull -> + MaySet.top () + | _ -> + add_indexes l u mays + in + match mode with + | Definitely -> (add_indexes l u musts, mays) + | Possibly -> (musts, mays) + + let remove_interval mode (l,u) min_size (musts, mays) = + match mode with + | Definitely -> failwith "todo" + | Possibly -> + if Z.equal l Z.zero && Z.geq u min_size then + (MustSet.top (), mays) + else + (MustSet.filter ~min_size (fun x -> (Z.lt x l || Z.gt x u) && Z.lt x min_size) musts, mays) + + let add_all mode (musts, mays) = + match mode with + | Definitely -> failwith "todo" + | Possibly -> (musts, MaySet.top ()) + + let remove_all mode (musts, mays) = + match mode with + | Possibly -> (MustSet.top (), mays) + | Definitely -> empty () + + let is_full_set mode (musts, mays) = + match mode with + | Definitely -> MustSet.is_bot musts + | Possibly -> MaySet.is_top mays + + let get_set mode (musts, mays) = + match mode with + | Definitely -> musts + | Possibly -> mays + + let elements ?max_size ?min_size mode (musts, mays) = + match mode with + | Definitely ->failwith "todo" + | Possibly -> MaySet.elements ?max_size mays + + let union_mays (must,mays) (_,mays2) = (must, MaySet.join mays mays2) + + + let precise_singleton i = + (MustSet.singleton i, MaySet.singleton i) + + let precise_set (s:Set.t):t = (`Lifted s,`Lifted s) + + let make_all_must () = (MustSet.bot (), MaySet.top ()) + + let may_can_benefit_from_filter (musts, mays) = not (MaySet.is_top mays) + + let exists mode f (musts, mays) = + match mode with + | Definitely -> MustSet.exists f musts + | Possibly -> MaySet.exists f mays + + let filter ?min_size ?max_size f (must, mays):t = + (MustSet.filter ?min_size f must, MaySet.filter ?max_size f mays) + + let filter_musts f min_size (musts, mays) = (MustSet.filter ~min_size f musts, mays) +end diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index e90f07aa0c..d1b81dcb08 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -19,11 +19,12 @@ sig include Lattice.S type offs val eval_offset: VDQ.t -> (AD.t -> t) -> t-> offs -> exp option -> lval option -> typ -> t - val update_offset: VDQ.t -> t -> offs -> t -> exp option -> lval -> typ -> t + val update_offset: ?blob_destructive:bool -> VDQ.t -> t -> offs -> t -> exp option -> lval -> typ -> t val update_array_lengths: (exp -> t) -> t -> Cil.typ -> t val affect_move: ?replace_with_const:bool -> VDQ.t -> t -> varinfo -> (exp -> int option) -> t val affecting_vars: t -> varinfo list val invalidate_value: VDQ.t -> typ -> t -> t + val invalidate_abstract_value: t -> t val is_safe_cast: typ -> typ -> bool val cast: ?torg:typ -> typ -> t -> t val smart_join: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t @@ -38,6 +39,8 @@ sig val is_top_value: t -> typ -> bool val zero_init_value: ?varAttr:attributes -> typ -> t + include ArrayDomain.Null with type t := t + val project: VDQ.t -> int_precision option-> ( attributes * attributes ) option -> t -> t val mark_jmpbufs_as_copied: t -> t end @@ -49,6 +52,7 @@ sig type origin include Lattice.S with type t = value * size * origin + val map: (value -> value) -> t -> t val value: t -> value val invalidate_value: VDQ.t -> typ -> t -> t end @@ -68,6 +72,7 @@ struct type size = Size.t type origin = ZeroInit.t + let map f (v, s, o) = f v, s, o let value (a, b, c) = a let relift (a, b, c) = Value.relift a, b, c let invalidate_value ask t (v, s, o) = Value.invalidate_value ask t v, s, o @@ -250,7 +255,6 @@ struct let tag_name : t -> string = function | Top -> "Top" | Int _ -> "Int" | Float _ -> "Float" | Address _ -> "Address" | Struct _ -> "Struct" | Union _ -> "Union" | Array _ -> "Array" | Blob _ -> "Blob" | Thread _ -> "Thread" | Mutex -> "Mutex" | MutexAttr _ -> "MutexAttr" | JmpBuf _ -> "JmpBuf" | Bot -> "Bot" - include Printable.Std let name () = "compound" @@ -264,6 +268,22 @@ struct let is_top x = x = Top let top_name = "Unknown" + let null () = Int (ID.of_int IChar Z.zero) + + type retnull = Null | NotNull | Maybe + let is_null = function + | Int n when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> Null + | Int n -> + let zero_ik = ID.of_int (ID.ikind n) Z.zero in + if ID.to_bool (ID.ne n zero_ik) = Some true then NotNull else Maybe + | _ -> Maybe + + let get_ikind = function + | Int n -> Some (ID.ikind n) + | _ -> None + let zero_of_ikind ik = Int(ID.of_int ik Z.zero) + let not_zero_of_ikind ik = Int(ID.of_excl_list ik [Z.zero]) + let pretty () state = match state with | Int n -> ID.pretty () n @@ -709,6 +729,22 @@ struct | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *) | t , _ -> top_value t + (* TODO: why is this separately needed? *) + let rec invalidate_abstract_value = function + | Top -> Top + | Int i -> Int (ID.top_of (ID.ikind i)) + | Float f -> Float (FD.top_of (FD.get_fkind f)) + | Address _ -> Address (AD.top_ptr) + | Struct s -> Struct (Structs.map invalidate_abstract_value s) + | Union u -> Union (Unions.top ()) (* More precise invalidate does not make sense, as it is not clear which component is accessed. *) + | Array a -> Array (CArrays.map invalidate_abstract_value a) + | Blob b -> Blob (Blobs.map invalidate_abstract_value b) + | Thread _ -> Thread (Threads.top ()) + | JmpBuf _ -> JmpBuf (JmpBufs.top ()) + | Mutex -> Mutex + | MutexAttr _ -> MutexAttr (MutexAttrDomain.top ()) + | Bot -> Bot + (* take the last offset in offset and move it over to left *) let shift_one_over left offset = @@ -894,7 +930,7 @@ struct in do_eval_offset ask f x offs exp l o v t - let update_offset (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t = + let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t = let rec do_update_offset (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t = if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value; let mu = function Blob (Blob (y, s', orig), s, orig2) -> Blob (y, ID.join s s',orig) | x -> x in @@ -942,9 +978,11 @@ struct | (Var var, _) -> let blob_size_opt = ID.to_int s in not @@ ask.is_multiple var - && not @@ Cil.isVoidType t (* Size of value is known *) && Option.is_some blob_size_opt (* Size of blob is known *) - && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t) + && (( + not @@ Cil.isVoidType t (* Size of value is known *) + && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t) + ) || blob_destructive) | _ -> false end in @@ -1230,7 +1268,7 @@ and Structs: StructDomain.S with type field = fieldinfo and type value = Compoun and Unions: UnionDomain.S with type t = UnionDomain.Field.t * Compound.t and type value = Compound.t = UnionDomain.Simple (Compound) -and CArrays: ArrayDomain.S with type value = Compound.t and type idx = ArrIdxDomain.t = ArrayDomain.AttributeConfiguredArrayDomain(Compound)(ArrIdxDomain) +and CArrays: ArrayDomain.StrWithDomain with type value = Compound.t and type idx = ArrIdxDomain.t = ArrayDomain.AttributeConfiguredAndNullByteArrayDomain(Compound)(ArrIdxDomain) and Blobs: Blob with type size = ID.t and type value = Compound.t and type origin = ZeroInit.t = Blob (Compound) (ID) diff --git a/src/common/util/xmlUtil.ml b/src/common/util/xmlUtil.ml index e33be1b215..c0eaa074e9 100644 --- a/src/common/util/xmlUtil.ml +++ b/src/common/util/xmlUtil.ml @@ -11,4 +11,5 @@ let escape (x:string):string = Str.global_replace (Str.regexp "\"") """ |> Str.global_replace (Str.regexp "'") "'" |> Str.global_replace (Str.regexp "[\x0b\001\x0c\x0f\x0e\x05]") "" |> (* g2html just cannot handle from some kernel benchmarks, even when escaped... *) - Str.global_replace (Str.regexp "[\x1b]") "" (* g2html cannot handle from chrony *) + Str.global_replace (Str.regexp "[\x1b]") "" |> (* g2html cannot handle from chrony *) + Str.global_replace (Str.regexp "\x00") "\\\\0" (* produces \\0, is needed if an example contains \0 *) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 4d9546a9ca..30bc4f3d8c 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -689,6 +689,12 @@ "description": "Indicates how many values will the unrolled part of the unrolled array domain contain.", "type": "integer", "default": 0 + }, + "nullbytes": { + "title": "ana.base.arrays.nullbytes", + "description": "Whether the Null Byte array domain should be activated.", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/tests/regression/73-strings/01-string_literals.c b/tests/regression/73-strings/01-string_literals.c index 42086e07b6..4a43590bf5 100644 --- a/tests/regression/73-strings/01-string_literals.c +++ b/tests/regression/73-strings/01-string_literals.c @@ -2,6 +2,7 @@ #include #include +#include char* hello_world() { return "Hello world!"; @@ -10,28 +11,49 @@ char* hello_world() { void id(char* s) { char* ptr = NULL; // future usage of cmp should warn: workaround for macOS test #ifdef __APPLE__ - #define ID int i = strcmp(ptr, "trigger warning") + #define ID int i = *ptr #else #define ID strcpy(s, s) #endif ID; // WARN } -int main() { +void example1() { + char* s1 = "bc\0test"; + char* s2 = "bc"; + char* s3; + if (rand()) + s3 = "aabbcc"; + else + s3 = "ebcdf"; + + int i = strcmp(s1, s2); + __goblint_check(i == 0); + + char* s4 = strstr(s3, s1); + __goblint_check(s4 != NULL); + + size_t len = strlen(s4); + __goblint_check(len >= 3); + __goblint_check(len <= 4); + __goblint_check(len == 3); // UNKNOWN! +} + +void example2() { char* s1 = "abcde"; char* s2 = "abcdfg"; char* s3 = hello_world(); + + size_t len = strlen(s1); + __goblint_check(len == 5); - int i = strlen(s1); - __goblint_check(i == 5); - - i = strlen(s2); - __goblint_check(i == 6); + len = strlen(s2); + __goblint_check(len == 6); - i = strlen(s3); - __goblint_check(i == 12); + len = strlen(s3); + __goblint_check(len == 12); - i = strcmp(s1, s2); + int i = strcmp(s1, s2); __goblint_check(i < 0); i = strcmp(s2, "abcdfg"); @@ -70,28 +92,28 @@ int main() { cmp = NULL; // future usage of cmp should warn: workaround for macOS test #ifdef __APPLE__ - #define STRCPY i = strcmp(cmp, "trigger warning") + #define STRCPY i = *cmp #else #define STRCPY strcpy(s1, "hi"); #endif STRCPY; // WARN #ifdef __APPLE__ - #define STRNCPY i = strcmp(cmp, "trigger warning") + #define STRNCPY i = *cmp #else # define STRNCPY strncpy(s1, "hi", 1) #endif STRNCPY; // WARN #ifdef __APPLE__ - #define STRCAT i = strcmp(cmp, "trigger warning") + #define STRCAT i = *cmp #else #define STRCAT strcat(s1, "hi") #endif STRCAT; // WARN #ifdef __APPLE__ - #define STRNCAT i = strcmp(cmp, "trigger warning") + #define STRNCAT i = *cmp #else #define STRNCAT strncat(s1, "hi", 1) #endif @@ -101,13 +123,18 @@ int main() { // do nothing => no warning #else char s4[] = "hello"; - strcpy(s4, s2); // NOWARN + strcpy(s4, s2); // NOWARN -> null byte array domain not enabled strncpy(s4, s3, 2); // NOWARN char s5[13] = "hello"; strcat(s5, " world"); // NOWARN strncat(s5, "! some further text", 1); // NOWARN #endif +} + +int main() { + example1(); + example2(); return 0; } 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 cc41e9e287..610390701a 100644 --- a/tests/regression/73-strings/02-string_literals_with_null.c +++ b/tests/regression/73-strings/02-string_literals_with_null.c @@ -9,10 +9,10 @@ int main() { char* s3 = "hello world!"; char* s4 = "\0 i am the empty string"; - int i = strlen(s1); - __goblint_check(i == 5); + size_t len = strlen(s1); + __goblint_check(len == 5); - i = strcmp(s1, s2); + int i = strcmp(s1, s2); __goblint_check(i == 0); i = strcmp(s3, s1); diff --git a/tests/regression/73-strings/03-string_basics.c b/tests/regression/73-strings/03-string_basics.c index a9d02d5e8b..e4d6c5c5e4 100644 --- a/tests/regression/73-strings/03-string_basics.c +++ b/tests/regression/73-strings/03-string_basics.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval +// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval --enable ana.base.arrays.nullbytes #include #include @@ -13,35 +13,49 @@ void concat_1(char* s, int i) { } int main() { - char* s1 = malloc(40); - strcpy(s1, "hello "); + char s1[40] = "hello "; char s2[] = "world!"; char s3[10] = "abcd"; char s4[20] = "abcdf"; + char* s5 = malloc(40); + strcpy(s5, "hello"); - int i = strlen(s1); - __goblint_check(i == 6); // UNKNOWN + size_t len = strlen(s1); + __goblint_check(len == 6); - i = strlen(s2); - __goblint_check(i == 6); // UNKNOWN + len = strlen(s2); + __goblint_check(len == 6); - i = strlen(s3); - __goblint_check(i == 4); // UNKNOWN + len = strlen(s3); + __goblint_check(len == 4); + + len = strlen(s5); + __goblint_check(len == 5); strcat(s1, s2); - i = strcmp(s1, "hello world!"); + len = strlen(s1); + int i = strcmp(s1, "hello world!"); + __goblint_check(len == 12); __goblint_check(i == 0); // UNKNOWN strcpy(s1, "hi "); + strncpy(s1, s3, 3); // WARN + len = strlen(s1); + __goblint_check(len == 3); + + char tmp[] = "hi "; + len = strlen(tmp); + __goblint_check(len == 3); + strcpy(s1, tmp); strncpy(s1, s3, 3); - i = strlen(s1); - __goblint_check(i == 3); // UNKNOWN + len = strlen(s1); + __goblint_check(len == 3); strcat(s1, "ababcd"); char* cmp = strstr(s1, "bab"); __goblint_check(cmp != NULL); // UNKNOWN - i = strcmp(cmp, "babcd"); // WARN: no check if cmp != NULL (even if it obviously is != NULL) + i = strcmp(cmp, "babcd"); // NOWARN: cmp != NULL __goblint_check(i == 0); // UNKNOWN i = strncmp(s4, s3, 4); @@ -50,15 +64,27 @@ int main() { i = strncmp(s4, s3, 5); __goblint_check(i > 0); // UNKNOWN - strncpy(s1, "", 20); + strncpy(s1, "", 20); // WARN + strcpy(tmp, "\0hi"); + i = strcmp(s1, tmp); + __goblint_check(i == 0); + + char tmp2[] = ""; + strcpy(s1, tmp2); + i = strcmp(s1, tmp2); + __goblint_check(i == 0); + + i = strcmp(s1, tmp); + __goblint_check(i == 0); + concat_1(s1, 30); - i = strlen(s1); - __goblint_check(i == 30); // UNKNOWN + len = strlen(s1); + __goblint_check(len == 30); cmp = strstr(s1, "0"); __goblint_check(cmp == NULL); // UNKNOWN - free(s1); + free(s5); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/73-strings/06-juliet.c b/tests/regression/73-strings/06-juliet.c new file mode 100644 index 0000000000..a198c62948 --- /dev/null +++ b/tests/regression/73-strings/06-juliet.c @@ -0,0 +1,166 @@ +// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval --set ana.base.arrays.domain partitioned --enable ana.base.arrays.nullbytes + +#include +#include +#include + +// TODO: tackle memset -> map it to for loop with set for each cell + +int main() { + CWE121_Stack_Based_Buffer_Overflow__src_char_declare_cpy_01_bad(); + CWE126_Buffer_Overread__CWE170_char_loop_01_bad(); + CWE126_Buffer_Overread__CWE170_char_strncpy_01_bad(); + CWE126_Buffer_Overread__char_declare_loop_01_bad(); + CWE571_Expression_Always_True__string_equals_01_bad(); + CWE665_Improper_Initialization__char_cat_01_bad(); + CWE665_Improper_Initialization__char_ncat_11_bad(); + + return 0; +} + +void CWE121_Stack_Based_Buffer_Overflow__src_char_declare_cpy_01_bad() +{ + char * data; + char dataBuffer[100]; + data = dataBuffer; + /* FLAW: Initialize data as a large buffer that is larger than the small buffer used in the sink */ + /* memset(data, 'A', 100-1); // fill with 'A's -- memset not supported currently, replaced with for-loop */ + for (size_t i = 0; i < 100-1; i++) + data[i] = 'A'; + data[100-1] = '\0'; /* null terminate */ + __goblint_check(data[42] == 'A'); + { + char dest[50] = ""; + /* POTENTIAL FLAW: Possible buffer overflow if data is larger than dest */ + strcpy(dest, data); // WARN + } +} + +void CWE126_Buffer_Overread__CWE170_char_loop_01_bad() +{ + { + char src[150], dest[100]; + int i; + /* Initialize src */ + /* memset(src, 'A', 149); */ + for (i = 0; i < 149; i++) + src[i] = 'A'; + src[149] = '\0'; + for(i=0; i < 99; i++) + { + dest[i] = src[i]; + } + /* FLAW: do not explicitly null terminate dest after the loop */ + __goblint_check(dest[42] != '\0'); // UNKNOWN + __goblint_check(dest[99] != '\0'); // UNKNOWN + } +} + +void CWE126_Buffer_Overread__CWE170_char_strncpy_01_bad() +{ + { + char data[150], dest[100]; + /* Initialize data */ + /* memset(data, 'A', 149); */ + for (size_t i = 0; i < 149; i++) + data[i] = 'A'; + data[149] = '\0'; + /* strncpy() does not null terminate if the string in the src buffer is larger than + * the number of characters being copied to the dest buffer */ + strncpy(dest, data, 99); // WARN + /* FLAW: do not explicitly null terminate dest after the use of strncpy() */ + } +} + +void CWE126_Buffer_Overread__char_declare_loop_01_bad() +{ + char * data; + char dataBadBuffer[50]; + char dataGoodBuffer[100]; + /* memset(dataBadBuffer, 'A', 50-1); // fill with 'A's */ + for (size_t i = 0; i < 50-1; i++) + dataBadBuffer[i] = 'A'; + dataBadBuffer[50-1] = '\0'; /* null terminate */ + /* memset(dataGoodBuffer, 'A', 100-1); // fill with 'A's */ + for (size_t i = 0; i < 100-1; i++) + dataGoodBuffer[i] = 'A'; + dataGoodBuffer[100-1] = '\0'; /* null terminate */ + /* FLAW: Set data pointer to a small buffer */ + data = dataBadBuffer; + { + size_t i, destLen; + char dest[100]; + /* memset(dest, 'C', 100-1); */ + for (i = 0; i < 100-1; i++) + dest[i] = 'C'; + dest[100-1] = '\0'; /* null terminate */ + destLen = strlen(dest); + __goblint_check(destLen <= 99); + /* POTENTIAL FLAW: using length of the dest where data + * could be smaller than dest causing buffer overread */ + for (i = 0; i < destLen; i++) + { + dest[i] = data[i]; + } + dest[100-1] = '\0'; + } +} + +void CWE665_Improper_Initialization__char_cat_01_bad() +{ + char * data; + char dataBuffer[100]; + data = dataBuffer; + /* FLAW: Do not initialize data */ + ; /* empty statement needed for some flow variants */ + { + char source[100]; + /* memset(source, 'C', 100-1); // fill with 'C's */ + for (size_t i = 0; i < 100-1; i++) + source[i] = 'C'; + source[100-1] = '\0'; /* null terminate */ + /* POTENTIAL FLAW: If data is not initialized properly, strcat() may not function correctly */ + strcat(data, source); // WARN + } +} + +void CWE571_Expression_Always_True__string_equals_01_bad() +{ + char charString[10] = "true"; + int cmp = strcmp(charString, "true"); + __goblint_check(cmp == 0); // UNKNOWN + + /* FLAW: This expression is always true */ + if (cmp == 0) + { + printf("always prints"); + } +} + +void CWE665_Improper_Initialization__char_ncat_11_bad() +{ + char * data; + char dataBuffer[100]; + data = dataBuffer; + if(rand()) + { + /* FLAW: Do not initialize data */ + ; /* empty statement needed for some flow variants */ + } + { + size_t sourceLen; + char source[100]; + /* memset(source, 'C', 100-1); // fill with 'C's */ + for (size_t i = 0; i < 100-1; i++) + source[i] = 'C'; + source[100-1] = '\0'; /* null terminate */ + sourceLen = strlen(source); + __goblint_check(sourceLen <= 99); + /* POTENTIAL FLAW: If data is not initialized properly, strncat() may not function correctly */ + #ifdef __APPLE__ + ; + #else + strncat(data, source, sourceLen); // NOWARN because sourceLen is not exactly known => array domain not consulted + #endif + } +} diff --git a/tests/regression/73-strings/07-larger_example.c b/tests/regression/73-strings/07-larger_example.c new file mode 100644 index 0000000000..9e9c2985ce --- /dev/null +++ b/tests/regression/73-strings/07-larger_example.c @@ -0,0 +1,41 @@ +// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval --enable ana.base.arrays.nullbytes + +#include +#include +#include + +int main() { + char* user; + if (rand()) + user = "Alice"; + else + user = "Bob"; + + if (strcmp(user, "Alice") == 0) + strcpy(user, "++++++++"); // WARN + + __goblint_check(strcmp(user, "Alice") == 0); // UNKNOWN + __goblint_check(strcmp(user, "Bob") == 0); // UNKNOWN + __goblint_check(strcmp(user, "Eve") != 0); + + char pwd_gen[20]; + for (size_t i = 12; i < 20; i++) + pwd_gen[i] = (char) (rand() % 123); + + char* p1 = "hello"; + char* p2 = "12345"; + strcat(pwd_gen, p1); // WARN + strncpy(pwd_gen, p2, 6); + __goblint_check(pwd_gen[5] == '\0'); + strncat(pwd_gen, p1, 4); + __goblint_check(pwd_gen[5] != '\0'); + + int cmp = strcmp(pwd_gen, "12345hello"); + __goblint_check(cmp != 0); + + char* pwd = strstr(pwd_gen, p2); + size_t pwd_len = strlen(pwd_gen); + __goblint_check(pwd_len == 9); + + return 0; +} diff --git a/tests/regression/73-strings/08-cursed.c b/tests/regression/73-strings/08-cursed.c new file mode 100644 index 0000000000..836b744da5 --- /dev/null +++ b/tests/regression/73-strings/08-cursed.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval --enable ana.base.arrays.nullbytes --set ana.malloc.unique_address_count 1 + +#include +#include +#include + +int main() { + // These should behave identically + char s1[40]; + char* s5 = malloc(40); + char* s6 = malloc(40); + + strcpy(s1, "hello"); + strcpy(s5, "hello"); + + int len = strlen(s5); + __goblint_check(len == 5); + + int len2 = strlen(s1); + __goblint_check(len2 == 5); + + strcpy(s6,s5); + int len3 = strlen(s6); + __goblint_check(len3 == 5); + + strcpy(s5, "badabingbadaboom"); + int len2 = strlen(s5); + __goblint_check(len2 == 16); + + return 0; +} diff --git a/tests/regression/73-strings/09-malloc.c b/tests/regression/73-strings/09-malloc.c new file mode 100644 index 0000000000..126872c682 --- /dev/null +++ b/tests/regression/73-strings/09-malloc.c @@ -0,0 +1,16 @@ +// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval --enable ana.base.arrays.nullbytes +#include +#include +#include + +int main () { + char* s1 = malloc(50); + s1[0] = 'a'; + + char s2[50]; + s2[0] = 'a'; + + // Use size_t to avoid integer warnings hiding the lack of string warnings + size_t len1 = strlen(s1); //TODO + size_t len2 = strlen(s2); //WARN +} diff --git a/tests/regression/73-strings/10-char_arrays.c b/tests/regression/73-strings/10-char_arrays.c new file mode 100644 index 0000000000..2454f2811b --- /dev/null +++ b/tests/regression/73-strings/10-char_arrays.c @@ -0,0 +1,383 @@ +// PARAM: --set ana.base.strings.domain disjoint --enable ana.int.interval --enable ana.base.arrays.nullbytes + +#include +#include +#include + +int main() { + example1(); + example2(); + example3(); + example4(); + example5(); + example6(); + example7(); + example8(); + example9(); + example10(); + example11(); + example12(); + example13(); + example14(); + example15(); + example16(); + example17(); + example18(); + + return 0; +} + +void example1() { + char s1[] = "user1_"; // must and may null at 6 and 7 + char s2[] = "pwd:\0abc"; // must and may null at 4 and 8 + char s3[20]; // no must nulls, all may nulls + + strcpy(s3, s1); // must null at 6, may nulls starting from 6 + + if (rand()) { + s2[4] = ' '; + strncat(s3, s2, 10); // must null at 14, may nulls starting from 14 + } else + strcat(s3, s2); // must null at 10, may nulls starting from 10 + + // s3: no must nulls, may nulls starting from 10 + + s3[14] = '\0'; // must null at 14, may nulls starting from 10 + + size_t len = strlen(s3); + __goblint_check(len >= 10); + __goblint_check(len <= 14); + __goblint_check(len == 10); // UNKNOWN! + + strcpy(s1, s3); // WARN +} + +void example2() { + char s1[42]; + char s2[20] = "testing"; // must null at 7, may null starting from 7 + + strcpy(s1, s2); // must null and may null at 7 + + size_t len = strlen(s1); + __goblint_check(len == 7); + + strcat(s1, s2); // "testingtesting" + + len = strlen(s1); + __goblint_check(len == 14); +} + +void example3() { + char s1[42]; + char s2[20] = "testing"; // must null at 7, may null starting from 7 + + if (rand() == 42) + s2[1] = '\0'; + + strcpy(s1, s2); // may null at 1 and starting from 7 + + size_t len = strlen(s1); // WARN: no must null in s1 + __goblint_check(len >= 1); + __goblint_check(len <= 7); // UNKNOWN + + strcpy(s2, s1); // WARN: no must null in s1 +} + +void example4() { + char s1[5] = "abc\0d"; // must and may null at 3 + char s2[] = "a"; // must and may null at 1 + + strcpy(s1, s2); // "a\0c\0d" + + size_t len = strlen(s1); + __goblint_check(len == 1); + + s1[1] = 'b'; // "abc\0d" + len = strlen(s1); + __goblint_check(len == 3); +} + +void example5() { + char s1[7] = "hello!"; // must and may null at 6 + char s2[8] = "goblint"; // must and may null at 7 + + strncpy(s1, s2, 7); // WARN + + size_t len = strlen(s1); // WARN + __goblint_check(len >= 7); // no null byte in s1 +} + +void example6() { + char s1[42] = "a string, i.e. null-terminated char array"; // must and may null at 42 + for (int i = 0; i < 42; i += 3) { + if (rand() != 42) + s1[i] = '\0'; + } + s1[41] = '.'; // no must nulls, only may null a 0, 3, 6... + + char s2[42] = "actually containing some text"; // must and may null at 29 + char s3[60] = "text: "; // must and may null at 6 + + strcat(s3, s1); // WARN: no must nulls, may nulls at 6, 9, 12... + + size_t len = strlen(s3); // WARN + __goblint_check(len >= 6); + __goblint_check(len > 6); // UNKNOWN + + strncat(s2, s3, 10); // WARN: no must nulls, may nulls at 35 and 38 + + len = strlen(s2); // WARN + __goblint_check(len >= 35); + __goblint_check(len > 40); // UNKNOWN +} + +void example7() { + char s1[50] = "hello"; // must and may null at 5 + char s2[] = " world!"; // must and may null at 7 + char s3[] = " goblint."; // must and may null at 9 + + if (rand() < 42) + strcat(s1, s2); // "hello world!" -> must and may null at 12 + else + strncat(s1, s3, 8); // "hello goblint" -> must and may null at 13 + + char s4[20]; + strcpy(s4, s1); // WARN: no must nulls, may nulls at 12 and 13 + + size_t len = strlen(s4); + __goblint_check(len >= 12); + __goblint_check(len == 13); // UNKNOWN + + s4[14] = '\0'; // must null at 14, may nulls at 12, 13 and 14 + len = strlen(s4); + __goblint_check(len >= 12); + __goblint_check(len <= 14); + + char s5[20]; + strncpy(s5, s4, 16); // WARN: no must nulls, may nulls at 12, 13, 14, 15... + len = strlen(s5); // WARN + __goblint_check(len >= 12); + __goblint_check(len <= 14); // UNKNOWN + __goblint_check(len < 20); // UNKNOWN +} + +void example8() { + char s1[6] = "abc"; // must and may null at 3 + if (rand() == 42) + s1[5] = '\0'; // must null at 3, may nulls at 3 and 5 + + char s2[] = "hello world"; // must and may null at 11 + + strncpy(s2, s1, 8); // WARN: 8 > size of s1 -- must and may nulls at 3, 4, 5, 6 and 7 + + size_t len = strlen(s2); + __goblint_check(len == 3); + + s2[3] = 'a'; // must and may nulls at 4, 5, 6 and 7 + len = strlen(s2); + __goblint_check(len == 4); + + for (int i = 4; i <= 7; i++) + s2[i] = 'a'; + s2[11] = 'a'; // no must nulls, may nulls at 4, 5, 6 and 7 + + len = strlen(s2); // WARN + __goblint_check(len >= 12); // UNKNOWN: loop transformed to interval + + s2[4] = 'a'; + s2[5] = 'a'; + s2[6] = 'a'; + s2[7] = 'a'; + len = strlen(s2); // WARN: no must nulls and may nulls + __goblint_check(len >= 12); +} + +void example9() { + char empty[] = ""; + char s1[] = "hello world"; // must and may null at 11 + char s2[] = "test"; // must and may null at 4 + + char cmp[50]; + #ifdef __APPLE__ + size_t len = 11; + #else + strcpy(cmp, strstr(s1, empty)); // NOWARN: strstr(s1, empty) != NULL + size_t len = strlen(cmp); + #endif + __goblint_check(len == 11); + + char* cmp_ptr = strstr(s2, s1); + __goblint_check(cmp_ptr == NULL); +} + +void example10() { + char empty1[] = ""; + char empty2[] = "\0 also empty"; + char s1[] = "hi"; + char s2[] = "hello"; + + int i = strcmp(empty1, empty2); + __goblint_check(i == 0); + + i = strcmp(empty1, s1); + __goblint_check(i < 0); + + i = strcmp(s1, empty1); + __goblint_check(i > 0); + + i = strcmp(s1, s2); + __goblint_check(i != 0); + + i = strncmp(s1, s2, 2); + __goblint_check(i != 0); // UNKNOWN + + s1[2] = 'a'; + + i = strcmp(s1, s2); // WARN + __goblint_check(i != 0); // UNKNOWN + + i = strncmp(s1, s2, 10); // WARN + __goblint_check(i != 0); // UNKNOWN +} + +void example11() { + size_t i; + if (rand()) + i = 0; + else + i = 1; + + char s1[50] = "goblint"; // must null at 7, may nulls starting from 7 + __goblint_check(s1[i] != '\0'); + + char s2[6] = "\0\0\0\0\0"; // all must and may nulls + __goblint_check(s2[i] == '\0'); + + strcpy(s1, s2); // must null at 0 and 7, mays nulls at 0 and starting from 7 + __goblint_check(s1[i] == '\0'); // UNKNOWN + + s1[i] = 'a'; // must null at 7, mays nulls at 0 and starting from 7 + + size_t len = strlen(s1); + __goblint_check(len >= 0); + __goblint_check(len > 0); // UNKNOWN + __goblint_check(len <= 7); + + s2[0] = 'a'; // all must and may null >= 1 + __goblint_check(s2[i] == '\0'); // UNKNOWN +} + +void example12() { + char s1[50]; + for (size_t i = 0; i < 50; i++) + s1[i] = '\0'; + __goblint_check(s1[0] == '\0'); // no must null, all may nulls + __goblint_check(s1[1] == '\0'); // known by trivial array domain + + char s2[5]; + s2[0] = 'a'; s2[1] = 'a'; s2[2] = 'a'; s2[3] = 'a'; s2[4] ='a'; + __goblint_check(s2[10] != '\0'); // no must null and may nulls + + strcpy(s1, s2); // WARN: no must nulls, may nulls >= 5 + strcpy(s2, "definite buffer overflow"); // WARN + + s2[4] = '\0'; // must and may null at 4 + + strncpy(s1, s2, 4); // WARN +} + +void example13() { + char s1[10]; // no must null, all may nulls + char s2[10]; // no must null, all may nulls + strncpy(s1, s2, 4); // WARN: no must null, all may nulls + __goblint_check(s1[3] == '\0'); // UNKNOWN + + s1[0] = 'a'; + s1[1] = 'b'; // no must null, may nulls >= 2 + + strcat(s1, s2); // WARN: no must null, may nulls >= 2 + __goblint_check(s1[1] != '\0'); + __goblint_check(s1[2] == '\0'); // UNKNOWN + + int cmp = strncmp(s1, s2, 0); + __goblint_check(cmp == 0); +} + +void example14() { + size_t size; + if (rand()) + size = 15; + else + size = 20; + + char* s = malloc(size); + + strcpy(s, ""); // must null at 0, all may null + + strcat(s, "123456789012345678"); // WARN +} + +example15() { + char* s1 = malloc(8); + strcpy(s1, "goblint"); // must and may null at 7 + + char s2[42] = "static"; // must null at 6, may null >= 6 + + strcat(s2, s1); // must null at 13, may null >= 13 + __goblint_check(s2[12] != '\0'); + __goblint_check(s2[13] == '\0'); + __goblint_check(s2[14] == '\0'); // UNKNOWN + + char* s3 = strstr(s1, s2); + __goblint_check(s3 == NULL); +} + +example16() { + size_t i; + if (rand()) + i = 3; + else + i = 4; + + char s[5] = "abab"; + __goblint_check(s[i] != '\0'); // UNKNOWN + + s[4] = 'a'; + __goblint_check(s[i] != '\0'); + + s[4] = '\0'; + s[i] = '\0'; + __goblint_check(s[4] == '\0'); + __goblint_check(s[3] == '\0'); // UNKNOWN + + s[i] = 'a'; + __goblint_check(s[4] == '\0'); // UNKNOWN +} + +example17() { + char s1[20]; + char s2[10]; + strcat(s1, s2); // WARN + __goblint_check(s1[0] == '\0'); // UNKNOWN + __goblint_check(s1[5] == '\0'); // UNKNOWN + __goblint_check(s1[12] == '\0'); // UNKNOWN +} + +example18() { + char s1[20] = "hello"; + char s2[10] = "world"; + + size_t i; + if (rand()) + i = 1; + else + i = 2; + s1[i] = '\0'; + + strcat(s1, s2); + __goblint_check(s1[1] != '\0'); + __goblint_check(s1[6] == '\0'); // UNKNOWN + __goblint_check(s1[7] == '\0'); // UNKNOWN + __goblint_check(s1[8] != '\0'); // UNKNOWN because might still be uninitialized + __goblint_check(s1[10] == '\0'); // UNKNOWN +}