From 703cec791d199e33710be8bc05f854b2365f4572 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 14 Dec 2018 05:07:11 -0800 Subject: [PATCH] [inferbo] Restore type models Reviewed By: skcho, jvillard Differential Revision: D13449623 fbshipit-source-id: feebe58f1 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 17 ++--- .../src/bufferoverrun/bufferOverrunDomain.ml | 34 +++++++--- .../bufferoverrun/bufferOverrunOndemandEnv.ml | 14 ++++- .../bufferoverrun/bufferOverrunTypModels.ml | 62 ++----------------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 57 ----------------- .../src/bufferoverrun/bufferOverrunUtils.mli | 29 --------- infer/src/bufferoverrun/itv.ml | 2 - infer/src/bufferoverrun/itv.mli | 2 - 8 files changed, 53 insertions(+), 164 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 828978a16..fc8175c7a 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -32,8 +32,7 @@ type extras = Dom.OndemandEnv.t module CFG = ProcCfg.NormalOneInstrPerNode module Init = struct - let initial_state {ProcData.pdesc; tenv; extras= {Dom.OndemandEnv.integer_type_widths} as oenv} - start_node = + let initial_state {ProcData.pdesc; tenv; extras= oenv} start_node = let node_hash = CFG.Node.hash start_node in let location = CFG.Node.loc start_node in let pname = Procdesc.get_proc_name pdesc in @@ -46,12 +45,14 @@ module Init = struct ?stride ~inst_num ~represents_multiple_values ~dimension mem | Typ.Tstruct typname -> ( match TypModels.dispatch tenv typname with - | Some {TypModels.declare_local} -> - let model_env = - Models.mk_model_env pname node_hash location tenv integer_type_widths - in - declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values - ~dimension mem + | Some typ_model -> ( + match typ_model with + | Array {element_typ; length} -> + BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc element_typ + ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem + | JavaCollection -> + BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num + ~represents_multiple_values ~dimension mem ) | None -> (mem, inst_num) ) | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 6d795654f..cf52cc6b9 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -339,7 +339,7 @@ module Val = struct let is_mone x = Itv.is_mone (get_itv x) - let of_path ~may_last_field integer_type_widths location typ path = + let of_path tenv ~may_last_field integer_type_widths location typ path = let is_java = Language.curr_language_is Java in L.d_printfln "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ (if may_last_field then ", may_last_field" else "") @@ -374,10 +374,26 @@ module Val = struct ArrayBlk.make allocsite ~stride ~offset ~size in {bot with arrayblk; traces} - | Tstruct _ -> - let l = Loc.of_path path in - let traces = TraceSet.singleton location (Trace.Parameter l) in - of_loc ~traces l + | Tstruct typename -> ( + match BufferOverrunTypModels.dispatch tenv typename with + | Some typ_model -> ( + match typ_model with + | Array {deref_kind; length} -> + let deref_path = SPath.deref ~deref_kind path in + let l = Loc.of_path deref_path in + let traces = TraceSet.singleton location (Trace.Parameter l) in + let allocsite = Allocsite.make_symbol deref_path in + let offset = Itv.zero in + let size = Itv.of_int_lit length in + of_array_alloc allocsite ~stride:None ~offset ~size ~traces + | JavaCollection -> + let l = Loc.of_path path in + let traces = TraceSet.singleton location (Trace.Parameter l) in + of_itv ~traces (Itv.of_normal_path ~unsigned:true path) ) + | None -> + let l = Loc.of_path path in + let traces = TraceSet.singleton location (Trace.Parameter l) in + of_loc ~traces l ) | Tarray {length; stride} -> let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in let l = Loc.of_path deref_path in @@ -400,7 +416,7 @@ module Val = struct let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t = - fun ~default {typ_of_param_path; may_last_field; entry_location; integer_type_widths} l -> + fun ~default {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} l -> match Loc.get_path l with | None -> L.d_printfln "Val.on_demand for %a -> no path" Loc.pp l ; @@ -414,7 +430,7 @@ module Val = struct L.d_printfln "Val.on_demand for %a" Loc.pp l ; let may_last_field = may_last_field path in let path = OndemandEnv.canonical_path typ_of_param_path path in - of_path ~may_last_field integer_type_widths entry_location typ path ) + of_path tenv ~may_last_field integer_type_widths entry_location typ path ) module Itv = struct @@ -1114,7 +1130,9 @@ module Mem = struct let forget_locs : PowLoc.t -> t -> t = fun locs -> map ~f:(MemReach.forget_locs locs) - let init_param_relation : Loc.t -> t -> t = fun loc -> map ~f:(MemReach.init_param_relation loc) + let[@warning "-32"] init_param_relation : Loc.t -> t -> t = + fun loc -> map ~f:(MemReach.init_param_relation loc) + let init_array_relation : Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index 4cd06ad55..e334edc18 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -11,7 +11,8 @@ module SPath = Symb.SymbolPath module FormalTyps = Caml.Map.Make (Pvar) type t = - { typ_of_param_path: SPath.partial -> Typ.t option + { tenv: Tenv.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 } @@ -34,6 +35,15 @@ let mk pdesc = elt | Tvoid -> Typ.void + | Tstruct typename -> ( + match BufferOverrunTypModels.dispatch tenv typename with + | Some (Array {element_typ}) -> + element_typ + | Some _ -> + L.(die InternalError) + "Deref of non-array modeled type `%a`" Typ.Name.pp typename + | None -> + L.(die InternalError) "Deref of unmodeled type `%a`" Typ.Name.pp typename ) | _ -> L.(die InternalError) "Untyped expression is given." ) | SPath.Field (fn, x) -> @@ -61,7 +71,7 @@ let mk pdesc = 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} + {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} let canonical_path typ_of_param_path path = diff --git a/infer/src/bufferoverrun/bufferOverrunTypModels.ml b/infer/src/bufferoverrun/bufferOverrunTypModels.ml index ce3925a76..2efdbbb20 100644 --- a/infer/src/bufferoverrun/bufferOverrunTypModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunTypModels.ml @@ -6,53 +6,13 @@ *) open! IStd -open AbsLoc -module BoUtils = BufferOverrunUtils -module Dom = BufferOverrunDomain -type model_env = BufferOverrunModels.model_env = - { pname: Typ.Procname.t - ; node_hash: int - ; location: Location.t - ; tenv: Tenv.t - ; integer_type_widths: Typ.IntegerWidths.t } +type typ_model = + | Array of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t} + | JavaCollection -type declare_local_fun = - decl_local:BoUtils.Exec.decl_local - -> model_env - -> Loc.t - -> inst_num:int - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int - -type declare_symbolic_fun = - decl_sym_val:BoUtils.Exec.decl_sym_val - -> Itv.SymbolPath.partial - -> model_env - -> depth:int - -> Loc.t - -> Dom.Mem.t - -> Dom.Mem.t - -type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} - -let std_array typ length = - let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num - ~represents_multiple_values ~dimension mem = - (* should this be deferred to the constructor? *) - let length = Some (IntLit.of_int64 length) in - BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num - ~represents_multiple_values ~dimension mem - in - let declare_symbolic ~decl_sym_val path {pname; tenv; location} ~depth loc mem = - let offset = Itv.zero in - let size = Itv.of_int64 length in - BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname path tenv - location ~depth loc typ ~offset ~size mem - in - {declare_local; declare_symbolic} +let std_array element_typ length = + Array {element_typ; deref_kind= Symb.SymbolPath.Deref_ArrayIndex; length= IntLit.of_int64 length} (* Java's Collections are represented by their size. We don't care about the elements. @@ -60,17 +20,7 @@ let std_array typ length = - each time we add an element, we increase the length of the array - each time we delete an element, we decrease the length of the array *) -let collection = - let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num - ~represents_multiple_values ~dimension mem = - BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num - ~represents_multiple_values ~dimension mem - in - let declare_symbolic ~decl_sym_val:_ path {location} ~depth:_ loc mem = - BoUtils.Exec.decl_sym_collection path location loc mem - in - {declare_local; declare_symbolic} - +let collection = JavaCollection let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher = let open ProcnameDispatcher.TypName in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index fdb1c90fc..843c93e16 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -118,63 +118,6 @@ module Exec = struct (mem, inst_num + 1) - type decl_sym_val = - Typ.Procname.t - -> Itv.SymbolPath.partial - -> Tenv.t - -> Location.t - -> depth:int - -> Loc.t - -> Typ.t - -> Dom.Mem.t - -> Dom.Mem.t - - let decl_sym_arr : - decl_sym_val:decl_sym_val - -> Symb.SymbolPath.deref_kind - -> Typ.Procname.t - -> Itv.SymbolPath.partial - -> Tenv.t - -> Location.t - -> depth:int - -> Loc.t - -> Typ.t - -> ?offset:Itv.t - -> ?size:Itv.t - -> ?stride:int - -> Dom.Mem.t - -> Dom.Mem.t = - fun ~decl_sym_val deref_kind pname path tenv location ~depth loc typ ?offset ?size ?stride mem -> - let offset = IOption.value_default_f offset ~f:(fun () -> Itv.of_offset_path path) in - let size = IOption.value_default_f size ~f:(fun () -> Itv.of_length_path path) in - let deref_path = Itv.SymbolPath.deref ~deref_kind path in - let allocsite = Allocsite.make_symbol deref_path in - let mem = - let arr = - let traces = Trace.(Set.singleton location (Parameter loc)) in - let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in - Dom.Val.of_array_alloc allocsite ~stride ~offset ~size ~traces - |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values - in - mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc - |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None - in - let deref_loc = Loc.of_allocsite allocsite in - decl_sym_val pname deref_path tenv location ~depth deref_loc typ mem - - - let decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t - = - fun path location loc mem -> - let size = - let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in - let traces = Trace.(Set.singleton location (Parameter loc)) in - Itv.of_length_path path |> Dom.Val.of_itv ~traces - |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values - in - Dom.Mem.add_heap loc size mem - - let init_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem = let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 977fde459..9d6fca5ab 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -56,35 +56,6 @@ module Exec : sig -> Dom.Mem.t -> Dom.Mem.t * int - type decl_sym_val = - Typ.Procname.t - -> Itv.SymbolPath.partial - -> Tenv.t - -> Location.t - -> depth:int - -> Loc.t - -> Typ.t - -> Dom.Mem.t - -> Dom.Mem.t - - val decl_sym_arr : - decl_sym_val:decl_sym_val - -> Symb.SymbolPath.deref_kind - -> Typ.Procname.t - -> Itv.SymbolPath.partial - -> Tenv.t - -> Location.t - -> depth:int - -> Loc.t - -> Typ.t - -> ?offset:Itv.t - -> ?size:Itv.t - -> ?stride:int - -> Dom.Mem.t - -> Dom.Mem.t - - val decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t - val init_array_fields : Tenv.t -> Typ.IntegerWidths.t diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 79ed339dc..ba1266f3f 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -498,8 +498,6 @@ let of_big_int : Z.t -> t = fun n -> NonBottom (ItvPure.of_big_int n) let of_int_lit : IntLit.t -> t = fun n -> of_big_int (IntLit.to_big_int n) -let of_int64 : Int64.t -> t = fun n -> of_big_int (Z.of_int64 n) - let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false let le : lhs:t -> rhs:t -> bool = ( <= ) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 9b0db3b53..516285351 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -133,8 +133,6 @@ val of_big_int : Z.t -> t val of_int_lit : IntLit.t -> t -val of_int64 : Int64.t -> t - val is_const : t -> Z.t option val is_one : t -> bool