From cae993aae0a03c5ddb5c9d3ce7a4ff67205d14c7 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 9 Oct 2019 06:14:47 -0700 Subject: [PATCH] [cost] Add FB-specific cost model Reviewed By: ezgicicek Differential Revision: D17788476 fbshipit-source-id: 7fd34eb8d --- infer/src/checkers/costModels.ml | 22 +++------------------- infer/src/checkers/costUtils.ml | 17 +++++++++++++++++ 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml index 2b65d1645..4ac574c2f 100644 --- a/infer/src/checkers/costModels.ml +++ b/infer/src/checkers/costModels.ml @@ -9,22 +9,6 @@ open! IStd module BasicCost = CostDomain.BasicCost open BufferOverrunUtils.ModelEnv -module type S = sig - val length : Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t -end - -module Array : S = struct - let length arr_exp inferbo_mem = - BufferOverrunSemantics.eval_array_locs_length - (BufferOverrunSemantics.eval_locs arr_exp inferbo_mem) - inferbo_mem -end - -module Collection : S = struct - let length coll_exp inferbo_mem = - BufferOverrunModels.Collection.eval_collection_length coll_exp inferbo_mem -end - let linear exp ~of_function {integer_type_widths; location} ~ret:_ inferbo_mem = let itv = BufferOverrunSemantics.eval integer_type_widths exp inferbo_mem @@ -40,7 +24,7 @@ let modeled ~of_function {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t = CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location -module BoundsOf (Container : S) = struct +module BoundsOf (Container : CostUtils.S) = struct let of_length exp {location} ~ret:_ mem ~of_function ~degree_kind = let itv = Container.length exp mem |> BufferOverrunDomain.Val.get_itv in CostUtils.of_itv ~itv ~degree_kind ~of_function location @@ -118,8 +102,8 @@ module JavaString = struct BasicCost.mult n m end -module BoundsOfCollection = BoundsOf (Collection) -module BoundsOfArray = BoundsOf (Array) +module BoundsOfCollection = BoundsOf (CostUtils.Collection) +module BoundsOfArray = BoundsOf (CostUtils.Array) module Call = struct let dispatch : (Tenv.t, CostUtils.model) ProcnameDispatcher.Call.dispatcher = diff --git a/infer/src/checkers/costUtils.ml b/infer/src/checkers/costUtils.ml index 407332d4e..fd5f98f8b 100644 --- a/infer/src/checkers/costUtils.ml +++ b/infer/src/checkers/costUtils.ml @@ -32,3 +32,20 @@ let string_len_range_itv model_env exp ~from mem = in Itv.minus itv start_itv ) |> Itv.set_lb_zero + + +module type S = sig + val length : Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t +end + +module Array : S = struct + let length arr_exp inferbo_mem = + BufferOverrunSemantics.eval_array_locs_length + (BufferOverrunSemantics.eval_locs arr_exp inferbo_mem) + inferbo_mem +end + +module Collection : S = struct + let length coll_exp inferbo_mem = + BufferOverrunModels.Collection.eval_collection_length coll_exp inferbo_mem +end