[inferbo][easy] Rename SubstMap to SymbolMap

Reviewed By: jvillard

Differential Revision: D7551674

fbshipit-source-id: 5b2681f

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
 
 

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

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 ->

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) =

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
 
 

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