From bdffee831a5a8b038191d503dc94ccbda80fad5b Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 9 Apr 2018 12:37:54 -0700 Subject: [PATCH] [inferbo][easy] Rename SubstMap to SymbolMap Reviewed By: jvillard Differential Revision: D7551674 fbshipit-source-id: 5b2681f --- infer/src/bufferoverrun/arrayBlk.ml | 4 ++-- infer/src/bufferoverrun/bufferOverrunDomain.ml | 5 +++-- .../src/bufferoverrun/bufferOverrunProofObligations.ml | 4 ++-- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 8 ++++---- infer/src/bufferoverrun/itv.ml | 10 +++++----- infer/src/bufferoverrun/itv.mli | 6 +++--- 6 files changed, 19 insertions(+), 18 deletions(-) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 45f01efa3..e9a5d263c 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -57,7 +57,7 @@ module ArrInfo = struct let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset - let subst : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t = + let subst : t -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t = fun arr subst_map -> {arr with offset= Itv.subst arr.offset subst_map; size= Itv.subst arr.size subst_map} @@ -138,7 +138,7 @@ let get_pow_loc : astate -> PowLoc.t = fold pow_loc_of_allocsite array PowLoc.bot -let subst : astate -> Itv.Bound.t bottom_lifted Itv.SubstMap.t -> astate = +let subst : astate -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> astate = fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 913e2b9e6..f3235a5ed 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -213,14 +213,15 @@ module Val = struct let subst - : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Location.t + : t -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t -> Location.t -> t = fun x (bound_map, trace_map) location -> let symbols = get_symbols x in let traces_caller = List.fold symbols ~f:(fun traces symbol -> - try TraceSet.join (Itv.SubstMap.find symbol trace_map) traces with Not_found -> traces ) + try TraceSet.join (Itv.SymbolMap.find symbol trace_map) traces with Not_found -> traces + ) ~init:TraceSet.empty in let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 854dede05..8f517410e 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -235,7 +235,7 @@ module ArrayAccessCondition = struct {report_issue_type; propagate= is_symbolic} - let subst : Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t -> t option = + let subst : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t -> t option = fun bound_map c -> match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with | NonBottom idx, NonBottom size -> @@ -450,7 +450,7 @@ module ConditionSet = struct | Some cond -> let traces_caller = List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol -> - match Itv.SubstMap.find symbol trace_map with + match Itv.SymbolMap.find symbol trace_map with | symbol_trace -> ValTraceSet.join symbol_trace val_traces | exception Not_found -> diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 1fc1edcb4..c1d2409d8 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -548,15 +548,15 @@ let get_matching_pairs let subst_map_of_pairs : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list - -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t = + -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t = fun pairs -> let add_pair (bound_map, trace_map) (formal, actual, traces) = if Itv.Bound.is_const formal |> Option.is_some then (bound_map, trace_map) else let symbol = Itv.Bound.get_one_symbol formal in - (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) + (Itv.SymbolMap.add symbol actual bound_map, Itv.SymbolMap.add symbol traces trace_map) in - List.fold ~f:add_pair ~init:(Itv.SubstMap.empty, Itv.SubstMap.empty) pairs + List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs let rec list_fold2_def @@ -576,7 +576,7 @@ let rec list_fold2_def let get_subst_map : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> callee_ret_alias:AliasTarget.t option - -> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) + -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t) * AliasTarget.t option = fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias -> let add_pair (formal, typ) actual (l, ret_alias) = diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5bb9dfb9f..fb80c8147 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -53,7 +53,7 @@ module Symbol = struct let is_unsigned : t -> bool = fun x -> x.unsigned end -module SubstMap = Caml.Map.Make (Symbol) +module SymbolMap = PrettyPrintable.MakePPMap (Symbol) module NonZeroInt : sig type t = private int [@@deriving compare] @@ -721,7 +721,7 @@ module Bound = struct (* substitution symbols in ``x'' with respect to ``map'' *) - let subst : subst_pos:subst_pos_t -> t -> t bottom_lifted SubstMap.t -> t bottom_lifted = + let subst : subst_pos:subst_pos_t -> t -> t bottom_lifted SymbolMap.t -> t bottom_lifted = fun ~subst_pos x map -> let subst_helper s y x = let y' = @@ -733,7 +733,7 @@ module Bound = struct in subst1 ~subst_pos x s y' in - SubstMap.fold subst_helper map (NonBottom x) + SymbolMap.fold subst_helper map (NonBottom x) let subst_lb x map = subst ~subst_pos:SubstLowerBound x map @@ -885,7 +885,7 @@ module ItvPure = struct let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false - let subst : t -> Bound.t bottom_lifted SubstMap.t -> t bottom_lifted = + let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted = fun x map -> match (Bound.subst_lb (lb x) map, Bound.subst_ub (ub x) map) with | NonBottom l, NonBottom u -> @@ -1407,7 +1407,7 @@ let prune_eq : t -> t -> t = lift2_opt ItvPure.prune_eq let prune_ne : t -> t -> t = lift2_opt ItvPure.prune_ne -let subst : t -> Bound.t bottom_lifted SubstMap.t -> t = +let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t = fun x map -> match x with NonBottom x' -> ItvPure.subst x' map | _ -> x diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 885ed79c7..c57f05fef 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -23,7 +23,7 @@ module Symbol : sig type t end -module SubstMap : Caml.Map.S with type key = Symbol.t +module SymbolMap : PrettyPrintable.PPMap with type key = Symbol.t module Bound : sig type t [@@deriving compare] @@ -133,7 +133,7 @@ module ItvPure : sig val get_symbols : t -> Symbol.t list - val subst : t -> Bound.t bottom_lifted SubstMap.t -> t bottom_lifted + val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted end include module type of AbstractDomain.BottomLifted (ItvPure) @@ -235,4 +235,4 @@ val prune_eq : t -> t -> t val prune_ne : t -> t -> t -val subst : t -> Bound.t bottom_lifted SubstMap.t -> t +val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t