diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 99528e9c4..a6dc9a593 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -12,6 +12,7 @@ open AbsLoc open! AbstractDomain.Types module F = Format module L = Logging +module OndemandEnv = BufferOverrunOndemandEnv module Relation = BufferOverrunDomainRelation module SPath = Symb.SymbolPath module Trace = BufferOverrunTrace @@ -22,90 +23,6 @@ type eval_sym_trace = ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t ; eval_locpath: PowLoc.eval_locpath } -module OndemandEnv = struct - module FormalTyps = Caml.Map.Make (Pvar) - - type t = - { typ_of_param_path: SPath.partial -> Typ.t option - ; may_last_field: SPath.partial -> bool - ; entry_location: Location.t - ; integer_type_widths: Typ.IntegerWidths.t } - - let mk pdesc = - let formal_typs = - List.fold (Procdesc.get_pvar_formals pdesc) ~init:FormalTyps.empty - ~f:(fun acc (formal, typ) -> FormalTyps.add formal typ acc ) - in - fun tenv integer_type_widths -> - let rec typ_of_param_path = function - | SPath.Pvar x -> - FormalTyps.find_opt x formal_typs - | SPath.Deref (_, x) -> - Option.map (typ_of_param_path x) ~f:(fun typ -> - match typ.Typ.desc with - | Tptr (typ, _) -> - typ - | Tarray {elt} -> - elt - | Tvoid -> - Typ.void - | _ -> - L.(die InternalError) "Untyped expression is given." ) - | SPath.Field (fn, x) -> - let lookup = Tenv.lookup tenv in - Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn) - | SPath.Callsite {ret_typ} -> - Some ret_typ - in - let is_last_field fn (fields : Typ.Struct.field list) = - Option.value_map (List.last fields) ~default:false ~f:(fun (last_fn, _, _) -> - Typ.Fieldname.equal fn last_fn ) - in - let rec may_last_field = function - | SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ -> - true - | SPath.Field (fn, 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 - | Tstruct typename -> - let opt_struct = Tenv.lookup tenv typename in - Option.value_map opt_struct ~default:false ~f:(fun str -> - is_last_field fn str.Typ.Struct.fields ) - | _ -> - true ) - in - let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in - {typ_of_param_path; may_last_field; entry_location; integer_type_widths} - - - let canonical_path typ_of_param_path path = - let module KnownFields = Caml.Map.Make (struct - type t = Typ.t option * Typ.Fieldname.t [@@deriving compare] - end) in - let rec helper path = - match path with - | SPath.Pvar _ | SPath.Callsite _ -> - (None, KnownFields.empty) - | SPath.Deref (deref_kind, ptr) -> - let ptr_opt, known_fields = helper ptr in - (Option.map ptr_opt ~f:(fun ptr -> SPath.deref ~deref_kind ptr), known_fields) - | SPath.Field (fn, struct_path) -> ( - let struct_path_opt, known_fields = helper struct_path in - let key = (typ_of_param_path (Option.value ~default:struct_path struct_path_opt), fn) in - match KnownFields.find_opt key known_fields with - | Some _ as canonicalized -> - (canonicalized, known_fields) - | None -> - let field_path = - Option.value_map struct_path_opt ~default:path ~f:(fun struct_path -> - SPath.field struct_path fn ) - in - (None, KnownFields.add key field_path known_fields) ) - in - Option.value (helper path |> fst) ~default:path -end - module Val = struct type t = { itv: Itv.t diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml new file mode 100644 index 000000000..4cd06ad55 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -0,0 +1,91 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module L = Logging +module SPath = Symb.SymbolPath +module FormalTyps = Caml.Map.Make (Pvar) + +type t = + { typ_of_param_path: SPath.partial -> Typ.t option + ; may_last_field: SPath.partial -> bool + ; entry_location: Location.t + ; integer_type_widths: Typ.IntegerWidths.t } + +let mk pdesc = + let formal_typs = + List.fold (Procdesc.get_pvar_formals pdesc) ~init:FormalTyps.empty ~f:(fun acc (formal, typ) -> + FormalTyps.add formal typ acc ) + in + fun tenv integer_type_widths -> + let rec typ_of_param_path = function + | SPath.Pvar x -> + FormalTyps.find_opt x formal_typs + | SPath.Deref (_, x) -> + Option.map (typ_of_param_path x) ~f:(fun typ -> + match typ.Typ.desc with + | Tptr (typ, _) -> + typ + | Tarray {elt} -> + elt + | Tvoid -> + Typ.void + | _ -> + L.(die InternalError) "Untyped expression is given." ) + | SPath.Field (fn, x) -> + let lookup = Tenv.lookup tenv in + Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn) + | SPath.Callsite {ret_typ} -> + Some ret_typ + in + let is_last_field fn (fields : Typ.Struct.field list) = + Option.value_map (List.last fields) ~default:false ~f:(fun (last_fn, _, _) -> + Typ.Fieldname.equal fn last_fn ) + in + let rec may_last_field = function + | SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ -> + true + | SPath.Field (fn, 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 + | Tstruct typename -> + let opt_struct = Tenv.lookup tenv typename in + Option.value_map opt_struct ~default:false ~f:(fun str -> + is_last_field fn str.Typ.Struct.fields ) + | _ -> + true ) + in + let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in + {typ_of_param_path; may_last_field; entry_location; integer_type_widths} + + +let canonical_path typ_of_param_path path = + let module KnownFields = Caml.Map.Make (struct + type t = Typ.t option * Typ.Fieldname.t [@@deriving compare] + end) in + let rec helper path = + match path with + | SPath.Pvar _ | SPath.Callsite _ -> + (None, KnownFields.empty) + | SPath.Deref (deref_kind, ptr) -> + let ptr_opt, known_fields = helper ptr in + (Option.map ptr_opt ~f:(fun ptr -> SPath.deref ~deref_kind ptr), known_fields) + | SPath.Field (fn, struct_path) -> ( + let struct_path_opt, known_fields = helper struct_path in + let key = (typ_of_param_path (Option.value ~default:struct_path struct_path_opt), fn) in + match KnownFields.find_opt key known_fields with + | Some _ as canonicalized -> + (canonicalized, known_fields) + | None -> + let field_path = + Option.value_map struct_path_opt ~default:path ~f:(fun struct_path -> + SPath.field struct_path fn ) + in + (None, KnownFields.add key field_path known_fields) ) + in + Option.value (helper path |> fst) ~default:path