pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[cost] Refactoring: Avoid using functors that are used only once

Browse Source 
Summary:
This diff avoids some usages of functors when they are applied only once in `polynomials.ml`.  While
functor is in general helpful to abstract data and make code cleaner, it makes us hard to understand
code, eg `merlin-locate` does not give an actual definition point of terms when it is from a module
parameter.

Reviewed By: ngorogiannis

Differential Revision: D23991164

fbshipit-source-id: c61289e84
master
Sungkeun Cho 4 years ago committed by Facebook GitHub Bot
parent 1154a2673a
commit 5ec6bc7a09
2 changed files with 79 additions and 104 deletions
Show Stats Download Patch File Download Diff File

180
infer/src/bufferoverrun/polynomials.ml
Unescape View File

@ -7,8 +7,8 @@
open! IStd
open! AbstractDomain.Types
module Bound = Bounds.Bound
open Ints
open Bounds
module DegreeKind = struct
type t = Linear | Log [@@deriving compare]
@ -51,104 +51,63 @@ module Degree = struct
F.fprintf f " + %a%slog" NonNegativeInt.pp d.log SpecialChars.dot_operator
end
module type NonNegativeSymbol = sig
type t [@@deriving compare]
val classify : t -> (Ints.NonNegativeInt.t, t, Bounds.BoundTrace.t) Bounds.valclass
val int_lb : t -> NonNegativeInt.t
val int_ub : t -> NonNegativeInt.t option
val mask_min_max_constant : t -> t
val subst :
Procname.t
-> Location.t
-> t
-> Bound.eval_sym
-> (NonNegativeInt.t, t, Bounds.BoundTrace.t) Bounds.valclass
val pp : hum:bool -> F.formatter -> t -> unit
val split_mult : t -> (t * t) option
val make_err_trace : t -> string * Errlog.loc_trace
end
module type NonNegativeSymbolWithDegreeKind = sig
type t0
include NonNegativeSymbol
val make : DegreeKind.t -> t0 -> t
val degree_kind : t -> DegreeKind.t
val symbol : t -> t0
val split_mult : t -> (t * t) option
val make_err_trace_symbol : t0 -> string * Errlog.loc_trace
end
module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
NonNegativeSymbolWithDegreeKind with type t0 = S.t = struct
type t0 = S.t [@@deriving compare]
type t = {degree_kind: DegreeKind.t; symbol: t0} [@@deriving compare]
module NonNegativeBoundWithDegreeKind = struct
type t = {degree_kind: DegreeKind.t; symbol: NonNegativeBound.t} [@@deriving compare]
let classify ({degree_kind; symbol} as self) =
match S.classify symbol with
match NonNegativeBound.classify symbol with
| Constant c ->
Bounds.Constant (DegreeKind.compute degree_kind c)
Constant (DegreeKind.compute degree_kind c)
| Symbolic _ ->
Bounds.Symbolic self
Symbolic self
| ValTop trace ->
Bounds.ValTop trace
ValTop trace
let mask_min_max_constant {degree_kind; symbol} =
{degree_kind; symbol= S.mask_min_max_constant symbol}
{degree_kind; symbol= NonNegativeBound.mask_min_max_constant symbol}
let make degree_kind symbol = {degree_kind; symbol}
let int_lb {degree_kind; symbol} = S.int_lb symbol |> DegreeKind.compute degree_kind
let int_lb {degree_kind; symbol} =
NonNegativeBound.int_lb symbol |> DegreeKind.compute degree_kind
let int_ub {degree_kind; symbol} =
S.int_ub symbol |> Option.map ~f:(DegreeKind.compute degree_kind)
NonNegativeBound.int_ub symbol |> Option.map ~f:(DegreeKind.compute degree_kind)
let subst callee_pname location {degree_kind; symbol} eval =
match S.subst callee_pname location symbol eval with
match NonNegativeBound.subst callee_pname location symbol eval with
| Constant c ->
Bounds.Constant (DegreeKind.compute degree_kind c)
Constant (DegreeKind.compute degree_kind c)
| Symbolic symbol ->
Bounds.Symbolic {degree_kind; symbol}
Symbolic {degree_kind; symbol}
| ValTop trace ->
Logging.d_printfln_escaped "subst(%a) became top." (S.pp ~hum:false) symbol ;
Bounds.ValTop trace
Logging.d_printfln_escaped "subst(%a) became top." (NonNegativeBound.pp ~hum:false) symbol ;
ValTop trace
let pp ~hum f {degree_kind; symbol} =
DegreeKind.pp_hole (NonNegativeBound.pp ~hum) f degree_kind symbol
let pp ~hum f {degree_kind; symbol} = DegreeKind.pp_hole (S.pp ~hum) f degree_kind symbol
let degree_kind {degree_kind} = degree_kind
let symbol {symbol} = symbol
let split_mult {degree_kind; symbol} =
Option.map (S.split_mult symbol) ~f:(fun (s1, s2) -> (make degree_kind s1, make degree_kind s2))
Option.map (NonNegativeBound.split_mult symbol) ~f:(fun (s1, s2) ->
(make degree_kind s1, make degree_kind s2) )
let make_err_trace {symbol} = S.make_err_trace symbol
let make_err_trace_symbol symbol = S.make_err_trace symbol
let make_err_trace_symbol symbol = NonNegativeBound.make_err_trace symbol
end
module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
module NonNegativeNonTopPolynomial = struct
module M = struct
include Caml.Map.Make (S)
include Caml.Map.Make (NonNegativeBoundWithDegreeKind)
let increasing_union ~f m1 m2 = union (fun _ v1 v2 -> Some (f v1 v2)) m1 m2
@ -218,14 +177,16 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
- symbols in terms are only symbolic values *)
type poly = {const: NonNegativeInt.t; terms: poly M.t} [@@deriving compare]
type t = {poly: poly; autoreleasepool_trace: Bounds.BoundTrace.t option} [@@deriving compare]
type t = {poly: poly; autoreleasepool_trace: BoundTrace.t option} [@@deriving compare]
let get_autoreleasepool_trace {autoreleasepool_trace} = autoreleasepool_trace
let rec degree_poly {terms} =
M.fold
(fun t p cur_max ->
let degree_term = Degree.succ (S.degree_kind t) (degree_poly p) in
let degree_term =
Degree.succ (NonNegativeBoundWithDegreeKind.degree_kind t) (degree_poly p)
in
if Degree.compare degree_term cur_max > 0 then degree_term else cur_max )
terms Degree.zero
@ -237,7 +198,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
let poly_of_non_negative_int : NonNegativeInt.t -> poly = fun const -> {const; terms= M.empty}
let of_non_negative_int : ?autoreleasepool_trace:Bounds.BoundTrace.t -> NonNegativeInt.t -> t =
let of_non_negative_int : ?autoreleasepool_trace:BoundTrace.t -> NonNegativeInt.t -> t =
fun ?autoreleasepool_trace const -> {poly= poly_of_non_negative_int const; autoreleasepool_trace}
@ -249,7 +210,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
let one ?autoreleasepool_trace () = of_non_negative_int ?autoreleasepool_trace NonNegativeInt.one
let of_int_exn : ?autoreleasepool_trace:Bounds.BoundTrace.t -> int -> t =
let of_int_exn : ?autoreleasepool_trace:BoundTrace.t -> int -> t =
fun ?autoreleasepool_trace i ->
i |> NonNegativeInt.of_int_exn |> of_non_negative_int ?autoreleasepool_trace
@ -301,7 +262,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
(* (c + r * R + s * S + t * T) x s
= 0 + r * (R x s) + s * (c + s * S + t * T) *)
let rec mult_symb_poly : poly -> S.t -> poly =
let rec mult_symb_poly : poly -> NonNegativeBoundWithDegreeKind.t -> poly =
fun {const; terms} s ->
let less_than_s, equal_s_opt, greater_than_s = M.split s terms in
let less_than_s = M.map (fun p -> mult_symb_poly p s) less_than_s in
@ -319,7 +280,9 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
{const= NonNegativeInt.zero; terms}
let mult_symb : t -> S.t -> t = fun x s -> {x with poly= mult_symb_poly x.poly s}
let mult_symb : t -> NonNegativeBoundWithDegreeKind.t -> t =
fun x s -> {x with poly= mult_symb_poly x.poly s}
let rec mult_poly : poly -> poly -> poly =
fun p1 p2 ->
@ -350,20 +313,24 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
body )
let rec of_valclass : (NonNegativeInt.t, S.t, 't) Bounds.valclass -> ('t, t, 't) below_above =
let rec of_valclass :
(NonNegativeInt.t, NonNegativeBoundWithDegreeKind.t, 't) valclass -> ('t, t, 't) below_above =
function
| ValTop trace ->
Above trace
| Constant i ->
Val (of_non_negative_int i)
| Symbolic s -> (
match S.split_mult s with
match NonNegativeBoundWithDegreeKind.split_mult s with
| None ->
Val
{ poly= {const= NonNegativeInt.zero; terms= M.singleton s one_poly}
; autoreleasepool_trace= None }
| Some (s1, s2) -> (
match (of_valclass (S.classify s1), of_valclass (S.classify s2)) with
match
( of_valclass (NonNegativeBoundWithDegreeKind.classify s1)
, of_valclass (NonNegativeBoundWithDegreeKind.classify s2) )
with
| Val s1, Val s2 ->
Val (mult s1 s2)
| Below _, _ | _, Below _ ->
@ -375,7 +342,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
let rec int_lb {const; terms} =
M.fold
(fun symbol polynomial acc ->
let s_lb = S.int_lb symbol in
let s_lb = NonNegativeBoundWithDegreeKind.int_lb symbol in
let p_lb = int_lb polynomial in
NonNegativeInt.((s_lb * p_lb) + acc) )
terms const
@ -385,7 +352,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
M.fold
(fun symbol polynomial acc ->
Option.bind acc ~f:(fun acc ->
Option.bind (S.int_ub symbol) ~f:(fun s_ub ->
Option.bind (NonNegativeBoundWithDegreeKind.int_ub symbol) ~f:(fun s_ub ->
Option.map (int_ub polynomial) ~f:(fun p_ub -> NonNegativeInt.((s_ub * p_ub) + acc)) ) )
)
terms (Some const)
@ -419,7 +386,8 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
M.fold
(fun s p acc ->
let p' = mask_min_max_constant_poly p in
M.update (S.mask_min_max_constant s)
M.update
(NonNegativeBoundWithDegreeKind.mask_min_max_constant s)
(function
| None -> Some p' | Some p -> if leq_poly ~lhs:p ~rhs:p' then Some p' else Some p )
acc )
@ -442,12 +410,12 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
let subst callee_pname location =
let exception ReturnTop of (S.t * Bounds.BoundTrace.t) in
let exception ReturnTop of (NonNegativeBoundWithDegreeKind.t * BoundTrace.t) in
(* avoids top-lifting everything *)
let rec subst_poly {const; terms} eval_sym =
M.fold
(fun s p acc ->
match S.subst callee_pname location s eval_sym with
match NonNegativeBoundWithDegreeKind.subst callee_pname location s eval_sym with
| Constant c -> (
match PositiveInt.of_big_int (c :> Z.t) with
| None ->
@ -467,7 +435,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
match subst_poly poly eval_sym with
| poly ->
let autoreleasepool_trace =
Option.map autoreleasepool_trace ~f:(Bounds.BoundTrace.call ~callee_pname ~location)
Option.map autoreleasepool_trace ~f:(BoundTrace.call ~callee_pname ~location)
in
Val {poly; autoreleasepool_trace}
| exception ReturnTop s_trace ->
@ -481,7 +449,9 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
M.fold
(fun t p cur_max ->
let d, p' = degree_with_term_poly p in
let degree_term = (Degree.succ (S.degree_kind t) d, mult_symb p' t) in
let degree_term =
(Degree.succ (NonNegativeBoundWithDegreeKind.degree_kind t) d, mult_symb p' t)
in
if [%compare: Degree.t * t] degree_term cur_max > 0 then degree_term else cur_max )
terms
(Degree.zero, one ())
@ -496,7 +466,8 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
let pp_poly : hum:bool -> F.formatter -> poly -> unit =
let add_symb s (((last_s, last_occ) as last), others) =
if Int.equal 0 (S.compare s last_s) then ((last_s, PositiveInt.succ last_occ), others)
if Int.equal 0 (NonNegativeBoundWithDegreeKind.compare s last_s) then
((last_s, PositiveInt.succ last_occ), others)
else ((s, PositiveInt.one), last :: others)
in
let pp_coeff fmt (c : NonNegativeInt.t) =
@ -510,7 +481,9 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
let s = F.asprintf "%a" pp x in
if String.contains s ' ' then F.fprintf fmt "(%s)" s else F.pp_print_string fmt s
in
let pp_symb ~hum fmt symb = pp_magic_parentheses (S.pp ~hum) fmt symb in
let pp_symb ~hum fmt symb =
pp_magic_parentheses (NonNegativeBoundWithDegreeKind.pp ~hum) fmt symb
in
let pp_symb_exp ~hum fmt (symb, exp) = F.fprintf fmt "%a%a" (pp_symb ~hum) symb pp_exp exp in
let pp_symbs ~hum fmt (last, others) =
List.rev_append others [last] |> Pp.seq ~sep:multiplication_sep (pp_symb_exp ~hum) fmt
@ -545,37 +518,37 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
let pp : hum:bool -> F.formatter -> t -> unit = fun ~hum fmt {poly} -> pp_poly ~hum fmt poly
let get_symbols p : S.t0 list =
let get_symbols p : NonNegativeBound.t list =
let rec get_symbols_sub {terms} acc =
M.fold (fun s p acc -> get_symbols_sub p (S.symbol s :: acc)) terms acc
M.fold
(fun s p acc -> get_symbols_sub p (NonNegativeBoundWithDegreeKind.symbol s :: acc))
terms acc
in
get_symbols_sub p.poly []
let polynomial_traces ?(is_autoreleasepool_trace = false) p =
let traces = get_symbols p |> List.map ~f:S.make_err_trace_symbol in
let traces =
get_symbols p |> List.map ~f:NonNegativeBoundWithDegreeKind.make_err_trace_symbol
in
if is_autoreleasepool_trace then
traces
@ Option.value_map (get_autoreleasepool_trace p) ~default:[] ~f:(fun trace ->
[("autorelease", Bounds.BoundTrace.make_err_trace ~depth:0 trace)] )
[("autorelease", BoundTrace.make_err_trace ~depth:0 trace)] )
else traces
end
module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNegativeBound)
module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind)
module TopTrace = struct
module S = NonNegativeBoundWithDegreeKind
type t =
| UnboundedLoop of {bound_trace: Bounds.BoundTrace.t}
| UnboundedSymbol of {location: Location.t; symbol: S.t; bound_trace: Bounds.BoundTrace.t}
| UnboundedLoop of {bound_trace: BoundTrace.t}
| UnboundedSymbol of
{location: Location.t; symbol: NonNegativeBoundWithDegreeKind.t; bound_trace: BoundTrace.t}
| Call of {location: Location.t; callee_pname: Procname.t; callee_trace: t}
[@@deriving compare]
let rec length = function
| UnboundedLoop {bound_trace} | UnboundedSymbol {bound_trace} ->
1 + Bounds.BoundTrace.length bound_trace
1 + BoundTrace.length bound_trace
| Call {callee_trace} ->
1 + length callee_trace
@ -592,10 +565,11 @@ module TopTrace = struct
let rec pp f = function
| UnboundedLoop {bound_trace} ->
F.fprintf f "%a -> UnboundedLoop" Bounds.BoundTrace.pp bound_trace
F.fprintf f "%a -> UnboundedLoop" BoundTrace.pp bound_trace
| UnboundedSymbol {location; symbol; bound_trace} ->
F.fprintf f "%a -> UnboundedSymbol (%a): %a" Bounds.BoundTrace.pp bound_trace Location.pp
location (S.pp ~hum:false) symbol
F.fprintf f "%a -> UnboundedSymbol (%a): %a" BoundTrace.pp bound_trace Location.pp location
(NonNegativeBoundWithDegreeKind.pp ~hum:false)
symbol
| Call {callee_pname; callee_trace; location} ->
F.fprintf f "%a -> Call `%a` (%a)" pp callee_trace Procname.pp callee_pname Location.pp
location
@ -604,12 +578,14 @@ module TopTrace = struct
let rec make_err_trace ~depth trace =
match trace with
| UnboundedLoop {bound_trace} ->
let bound_err_trace = Bounds.BoundTrace.make_err_trace ~depth bound_trace in
let bound_err_trace = BoundTrace.make_err_trace ~depth bound_trace in
[("Unbounded loop", bound_err_trace)] |> Errlog.concat_traces
| UnboundedSymbol {location; symbol; bound_trace} ->
let desc = F.asprintf "Unbounded value %a" (S.pp ~hum:true) symbol in
let desc =
F.asprintf "Unbounded value %a" (NonNegativeBoundWithDegreeKind.pp ~hum:true) symbol
in
Errlog.make_trace_element depth location desc []
:: Bounds.BoundTrace.make_err_trace ~depth bound_trace
:: BoundTrace.make_err_trace ~depth bound_trace
| Call {location; callee_pname; callee_trace} ->
let desc = F.asprintf "Call to %a" Procname.pp callee_pname in
Errlog.make_trace_element depth location desc []

3
infer/src/bufferoverrun/polynomials.mli
Unescape View File

@ -6,7 +6,6 @@
*)
open! IStd
module Bound = Bounds.Bound
module DegreeKind : sig
type t = Linear | Log
@ -83,7 +82,7 @@ module NonNegativePolynomial : sig
val min_default_left : t -> t -> t
val subst : Procname.t -> Location.t -> t -> Bound.eval_sym -> t
val subst : Procname.t -> Location.t -> t -> Bounds.Bound.eval_sym -> t
val degree : t -> Degree.t option

Write Preview
Loading…
Cancel
Save