diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index e3035af16..99b641e61 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -127,8 +127,64 @@ module Allocsite = struct end module Loc = struct - type t = Var of Var.t | Allocsite of Allocsite.t | Field of t * Typ.Fieldname.t - [@@deriving compare] + include (* Enforce invariants on Field and StarField, see Symb.mli *) ( + struct + type t = + | Var of Var.t + | Allocsite of Allocsite.t + | Field of t * Typ.Fieldname.t + | StarField of {prefix: t; last_field: Typ.Fieldname.t} + [@@deriving compare] + + let of_var v = Var v + + let of_allocsite a = Allocsite a + + let append_field l0 ~fn = + let rec aux = function + | Var _ | Allocsite _ -> + Field (l0, fn) + | StarField {last_field} as l when Typ.Fieldname.equal fn last_field -> + l + | StarField {prefix} -> + StarField {prefix; last_field= fn} + | Field (_, fn') when Typ.Fieldname.equal fn fn' -> + StarField {prefix= l0; last_field= fn} + | Field (l, _) -> + aux l + in + aux l0 + + + let append_star_field l0 ~fn = + let rec aux = function + | Var _ | Allocsite _ -> + StarField {prefix= l0; last_field= fn} + | StarField {last_field} as l when Typ.Fieldname.equal fn last_field -> + l + | StarField {prefix} -> + StarField {prefix; last_field= fn} + | Field (l, _) -> + aux l + in + aux l0 + end : + sig + type t = private + | Var of Var.t + | Allocsite of Allocsite.t + | Field of t * Typ.Fieldname.t + | StarField of {prefix: t; last_field: Typ.Fieldname.t} + [@@deriving compare] + + val of_var : Var.t -> t + + val of_allocsite : Allocsite.t -> t + + val append_field : t -> fn:Typ.Fieldname.t -> t + + val append_star_field : t -> fn:Typ.Fieldname.t -> t + end ) let equal = [%compare.equal: t] @@ -136,14 +192,14 @@ module Loc = struct match (l1, l2) with Allocsite as1, Allocsite as2 -> Allocsite.eq as1 as2 | _ -> Boolean.Top - let unknown = Allocsite Allocsite.unknown + let unknown = of_allocsite Allocsite.unknown let rec is_unknown = function | Var _ -> false | Allocsite a -> Allocsite.is_unknown a - | Field (x, _) -> + | Field (x, _) | StarField {prefix= x} -> is_unknown x @@ -172,7 +228,12 @@ module Loc = struct | Field (l, f) -> BufferOverrunField.pp ~pp_lhs:(pp_paren ~paren:true) ~pp_lhs_alone:(pp_paren ~paren) ~sep:"." fmt l f + | StarField {prefix; last_field} -> + BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~pp_lhs_alone:(pp_star ~paren) ~sep:"." + fmt prefix last_field + + and pp_star ~paren fmt l = pp_paren ~paren fmt l ; F.pp_print_string fmt ".*" let pp = pp_paren ~paren:false @@ -192,31 +253,27 @@ module Loc = struct true | Allocsite a -> Allocsite.is_pretty a - | Field (loc, _) -> + | Field (loc, _) | StarField {prefix= loc} -> is_pretty loc - let of_var v = Var v - - let of_allocsite a = Allocsite a + let of_c_strlen loc = append_field loc ~fn:(BufferOverrunField.c_strlen ()) - let of_c_strlen loc = Field (loc, BufferOverrunField.c_strlen ()) + let of_pvar pvar = of_var (Var.of_pvar pvar) - let of_pvar pvar = Var (Var.of_pvar pvar) - - let of_id id = Var (Var.of_id id) + let of_id id = of_var (Var.of_id id) let rec of_path path = match path with | Symb.SymbolPath.Pvar pvar -> of_pvar pvar | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Callsite _ -> - Allocsite (Allocsite.make_symbol path) + of_allocsite (Allocsite.make_symbol path) | Symb.SymbolPath.Field (fn, path) -> - Field (of_path path, fn) - + append_field (of_path path) ~fn + | Symb.SymbolPath.StarField {last_field= fn; prefix} -> + append_star_field (of_path prefix) ~fn - let append_field l ~fn = Field (l, fn) let is_return = function | Var (Var.ProgramVar x) -> @@ -225,7 +282,9 @@ module Loc = struct false - let is_field_of ~loc ~field_loc = match field_loc with Field (l, _) -> equal loc l | _ -> false + let is_field_of ~loc ~field_loc = + match field_loc with Field (l, _) | StarField {prefix= l} -> equal loc l | _ -> false + let is_literal_string = function Allocsite a -> Allocsite.is_literal_string a | _ -> None @@ -241,7 +300,7 @@ module Loc = struct Pvar.is_global pvar | Var (Var.LogicalVar _) | Allocsite _ -> false - | Field (loc, _) -> + | Field (loc, _) | StarField {prefix= loc} -> is_global loc @@ -254,6 +313,8 @@ module Loc = struct Allocsite.get_path allocsite | Field (l, fn) -> Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn) + | StarField {prefix; last_field} -> + get_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.star_field p last_field) let rec get_param_path = function @@ -263,6 +324,8 @@ module Loc = struct Allocsite.get_param_path allocsite | Field (l, fn) -> Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn) + | StarField {prefix; last_field} -> + get_param_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.star_field p last_field) let rec represents_multiple_values = function @@ -272,6 +335,8 @@ module Loc = struct Allocsite.represents_multiple_values allocsite | Field (l, _) -> represents_multiple_values l + | StarField _ -> + true let rec exists_pvar ~f = function @@ -281,7 +346,7 @@ module Loc = struct f pvar | Allocsite allocsite -> Allocsite.exists_pvar ~f allocsite - | Field (l, _) -> + | Field (l, _) | StarField {prefix= l} -> exists_pvar ~f l @@ -303,6 +368,11 @@ module PowLoc = struct else fold (fun l -> add (Loc.append_field l ~fn)) ploc empty + let append_star_field ploc ~fn = + if is_bot ploc then singleton Loc.unknown + else fold (fun l -> add (Loc.append_star_field l ~fn)) ploc empty + + let lift_cmp cmp_loc ploc1 ploc2 = match (is_singleton_or_more ploc1, is_singleton_or_more ploc2) with | IContainer.Singleton loc1, IContainer.Singleton loc2 -> diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index 0aa504e5b..b8e85a22b 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -56,6 +56,8 @@ let mk pdesc = Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn) | some_typ -> some_typ ) + | SPath.StarField {last_field} -> + BufferOverrunField.get_type last_field | SPath.Callsite {ret_typ} -> Some ret_typ in @@ -66,7 +68,7 @@ let mk pdesc = let rec may_last_field = function | SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ -> true - | SPath.Field (fn, x) -> + | SPath.Field (fn, x) | SPath.StarField {last_field= fn; prefix= x} -> may_last_field x && Option.value_map ~default:true (typ_of_param_path x) ~f:(fun parent_typ -> match parent_typ.Typ.desc with @@ -91,7 +93,7 @@ let canonical_path typ_of_param_path path = let module KnownFields = Caml.Map.Make (K) in let rec helper path = match path with - | SPath.Pvar _ | SPath.Callsite _ -> + | SPath.Pvar _ | SPath.Callsite _ | SPath.StarField _ -> (None, KnownFields.empty) | SPath.Deref (deref_kind, ptr) -> let ptr_opt, known_fields = helper ptr in diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 6824f0cfe..317b485de 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -400,7 +400,7 @@ let rec eval_sympath_partial ~mode params p mem = Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem | EvalPOCond | EvalPOReachability -> Val.Itv.top ) - | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ -> + | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ | Symb.SymbolPath.StarField _ -> let locs = eval_locpath ~mode params p mem in Mem.find_set locs mem @@ -417,6 +417,9 @@ and eval_locpath ~mode params p mem = | Symb.SymbolPath.Field (fn, p) -> let locs = eval_locpath ~mode params p mem in PowLoc.append_field ~fn locs + | Symb.SymbolPath.StarField {last_field= fn; prefix} -> + let locs = eval_locpath ~mode params prefix mem in + PowLoc.append_star_field ~fn locs in if PowLoc.is_empty res then ( match mode with diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index d815e100c..af2017378 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -26,12 +26,70 @@ module SymbolPath = struct let compare_deref_kind _ _ = 0 - type partial = - | Pvar of Pvar.t - | Deref of deref_kind * partial - | Field of Typ.Fieldname.t * partial - | Callsite of {ret_typ: Typ.t; cs: CallSite.t} - [@@deriving compare] + include (* Enforce invariants on Field and StarField *) ( + struct + type partial = + | Pvar of Pvar.t + | Deref of deref_kind * partial + | Field of Typ.Fieldname.t * partial + | Callsite of {ret_typ: Typ.t; cs: CallSite.t} + | StarField of {last_field: Typ.Fieldname.t; prefix: partial} + [@@deriving compare] + + let of_pvar pvar = Pvar pvar + + let of_callsite ~ret_typ cs = Callsite {ret_typ; cs} + + let deref ~deref_kind p = Deref (deref_kind, p) + + let star_field p0 fn = + let rec aux = function + | Pvar _ | Callsite _ -> + StarField {last_field= fn; prefix= p0} + | Deref (_, p) | Field (_, p) -> + aux p + | StarField {last_field} as p when Typ.Fieldname.equal fn last_field -> + p + | StarField {prefix} -> + StarField {last_field= fn; prefix} + in + aux p0 + + + let field p0 fn = + let rec aux = function + | Pvar _ | Callsite _ -> + Field (fn, p0) + | Field (fn', _) when Typ.Fieldname.equal fn fn' -> + StarField {last_field= fn; prefix= p0} + | Field (_, p) | Deref (_, p) -> + aux p + | StarField {last_field} as p when Typ.Fieldname.equal fn last_field -> + p + | StarField {prefix} -> + StarField {last_field= fn; prefix} + in + aux p0 + end : + sig + type partial = private + | Pvar of Pvar.t + | Deref of deref_kind * partial + | Field of Typ.Fieldname.t * partial + | Callsite of {ret_typ: Typ.t; cs: CallSite.t} + | StarField of {last_field: Typ.Fieldname.t; prefix: partial} + [@@deriving compare] + + val of_pvar : Pvar.t -> partial + + val of_callsite : ret_typ:Typ.t -> CallSite.t -> partial + + val deref : deref_kind:deref_kind -> partial -> partial + + val field : partial -> Typ.Fieldname.t -> partial + + val star_field : partial -> Typ.Fieldname.t -> partial + end ) type t = Normal of partial | Offset of partial | Length of partial | Modeled of partial [@@deriving compare] @@ -40,14 +98,6 @@ module SymbolPath = struct let equal_partial = [%compare.equal: partial] - let of_pvar pvar = Pvar pvar - - let of_callsite ~ret_typ cs = Callsite {ret_typ; cs} - - let field p fn = Field (fn, p) - - let deref ~deref_kind p = Deref (deref_kind, p) - let normal p = Normal p let offset p = Offset p @@ -61,7 +111,7 @@ module SymbolPath = struct let rec get_pvar = function | Pvar pvar -> Some pvar - | Deref (_, partial) | Field (_, partial) -> + | Deref (_, partial) | Field (_, partial) | StarField {prefix= partial} -> get_pvar partial | Callsite _ -> None @@ -84,6 +134,9 @@ module SymbolPath = struct ~pp_lhs_alone:(pp_partial_paren ~paren) ~sep:"." fmt p fn | Callsite {cs} -> F.fprintf fmt "%s" (Typ.Procname.to_simplified_string ~withclass:true (CallSite.pname cs)) + | StarField {last_field; prefix} -> + BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~pp_lhs_alone:(pp_star ~paren) ~sep:"." + fmt prefix last_field and pp_pointer ~paren fmt p = @@ -92,6 +145,8 @@ module SymbolPath = struct if paren then F.fprintf fmt ")" + and pp_star ~paren fmt p = pp_partial_paren ~paren fmt p ; F.pp_print_string fmt ".*" + let pp_partial = pp_partial_paren ~paren:false let pp fmt = function @@ -111,7 +166,7 @@ module SymbolPath = struct (* TODO depending on the result, the call might represent multiple values *) | Callsite _ | Pvar _ -> false - | Deref (Deref_ArrayIndex, _) -> + | Deref (Deref_ArrayIndex, _) | StarField _ -> true | Deref (Deref_CPointer, p) (* Deref_CPointer is unsound here but avoids many FPs for non-array pointers *) @@ -121,7 +176,7 @@ module SymbolPath = struct let rec represents_multiple_values_sound = function - | Callsite _ -> + | Callsite _ | StarField _ -> true | Pvar _ -> false @@ -136,14 +191,14 @@ module SymbolPath = struct true | Pvar _ -> false - | Deref (_, p) | Field (_, p) -> + | Deref (_, p) | Field (_, p) | StarField {prefix= p} -> represents_callsite_sound_partial p let rec exists_pvar_partial ~f = function | Pvar pvar -> f pvar - | Deref (_, p) | Field (_, p) -> + | Deref (_, p) | Field (_, p) | StarField {prefix= p} -> exists_pvar_partial ~f p | Callsite _ -> false @@ -154,7 +209,7 @@ module SymbolPath = struct f (Pvar.to_string pvar) | Deref (_, x) -> exists_str_partial ~f x - | Field (fld, x) -> + | Field (fld, x) | StarField {last_field= fld; prefix= x} -> f (Typ.Fieldname.to_string fld) || exists_str_partial ~f x | Callsite _ -> false diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index b785fab0b..be846196e 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -27,6 +27,15 @@ module SymbolPath : sig | Deref of deref_kind * partial | Field of Typ.Fieldname.t * partial | Callsite of {ret_typ: Typ.t; cs: CallSite.t} + | StarField of {last_field: Typ.Fieldname.t; prefix: partial} + (** + Represents a path starting with [prefix] and ending with the field [last_field], + the middle can be anything. + Invariants: + - There is at most one StarField + - StarField excluded, there are no duplicate fieldnames + - StarField can only be followed by Deref elements + *) [@@deriving compare] type t = private Normal of partial | Offset of partial | Length of partial | Modeled of partial @@ -49,6 +58,8 @@ module SymbolPath : sig val field : partial -> Typ.Fieldname.t -> partial + val star_field : partial -> Typ.Fieldname.t -> partial + val normal : partial -> t val offset : partial -> t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/cast.c b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c index 86e7b1fdf..9194fe035 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/cast.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c @@ -89,3 +89,25 @@ void cast_float_to_int_Bad_FN() { arr[y] = 0; } } + +/* + Testing that the analyzer doesn't run infinitely on these cases +*/ +typedef struct s_cast { + char* data; + struct s_cast* another; + char* data2; +} t_cast; + +char cast_field_to_struct(struct s_cast* s, int i0) { + for (int i = i0; i > 0; i--) { + s = (struct s_cast*)(&s->data); + } + s = s->another; + for (int i = i0; i > 0; i--) { + s = (struct s_cast*)(&s->data); + s = (struct s_cast*)((unsigned char*)(void*)(s->data2) - + offsetof(s->data2)); + } + return *s->data; +}