[inferbo] Refactor pretty print of alias domain

Summary:
This diff is to refactoring some stuffs for the following diff.

* revised pretty print of the alias domain
* moved `eval_array_locs_length` to `BufferOverrunSemantics`.

Reviewed By: jvillard

Differential Revision: D17667123

fbshipit-source-id: c95611df5

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -411,7 +411,11 @@ module Val = struct
 
   let prune_ge_one : t -> t = lift_prune1 Itv.prune_ge_one
 
-  let prune_length_eq_zero : t -> t = lift_prune_length1 Itv.prune_eq_zero
+  let prune_length_eq : t -> Itv.t -> t =
+   fun x y -> lift_prune_length1 (fun x -> Itv.prune_eq x y) x
+
+
+  let prune_length_eq_zero : t -> t = fun x -> prune_length_eq x Itv.zero
 
   let prune_length_ge_one : t -> t = lift_prune_length1 Itv.prune_ge_one
 
@@ -842,28 +846,27 @@ module AliasTarget = struct
 
   let equal = [%compare.equal: t]
 
-  let pp =
-    let intlit_pp fmt i =
-      if IntLit.isnegative i then F.fprintf fmt "-%a" IntLit.pp (IntLit.neg i)
-      else F.fprintf fmt "+%a" IntLit.pp i
+  let pp_with_key pp_key =
+    let pp_intlit fmt i =
+      if not (IntLit.iszero i) then
+        if IntLit.isnegative i then F.fprintf fmt "-%a" IntLit.pp (IntLit.neg i)
+        else F.fprintf fmt "+%a" IntLit.pp i
     in
-    let java_tmp_pp fmt java_tmp = Option.iter java_tmp ~f:(F.fprintf fmt "=%a" Loc.pp) in
+    let pp_java_tmp fmt java_tmp = Option.iter java_tmp ~f:(F.fprintf fmt "=%a" Loc.pp) in
     fun fmt -> function
       | Simple {l; i; java_tmp} ->
-          Loc.pp fmt l ;
-          if not (IntLit.iszero i) then intlit_pp fmt i ;
-          java_tmp_pp fmt java_tmp
+          F.fprintf fmt "%t%a=%a%a" pp_key pp_java_tmp java_tmp Loc.pp l pp_intlit i
       | Empty l ->
-          F.fprintf fmt "empty(%a)" Loc.pp l
+          F.fprintf fmt "%t=empty(%a)" pp_key Loc.pp l
       | Size {l; i; java_tmp} ->
-          F.fprintf fmt "size(%a)" Loc.pp l ;
-          if not (IntLit.iszero i) then intlit_pp fmt i ;
-          java_tmp_pp fmt java_tmp
+          F.fprintf fmt "%t%a=size(%a)%a" pp_key pp_java_tmp java_tmp Loc.pp l pp_intlit i
       | Fgets l ->
-          F.fprintf fmt "fgets(%a)" Loc.pp l
+          F.fprintf fmt "%t=fgets(%a)" pp_key Loc.pp l
       | Top ->
-          F.fprintf fmt "T"
+          F.fprintf fmt "%t=?" pp_key
+
 
+  let pp = pp_with_key (fun fmt -> F.pp_print_string fmt "_")
 
   let fgets l = Fgets l
 
@@ -948,7 +951,7 @@ module AliasMap = struct
    fun fmt x ->
     if not (is_empty x) then
       let pp_sep fmt () = F.fprintf fmt ", @," in
-      let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Key.pp k AliasTarget.pp v in
+      let pp1 fmt (k, v) = AliasTarget.pp_with_key (fun fmt -> Key.pp fmt k) fmt v in
       F.pp_print_list ~pp_sep pp1 fmt (bindings x)
 
 
@@ -1591,7 +1594,7 @@ module MemReach = struct
     PowLoc.fold find_join locs Val.bot
 
 
-  let find_alias : Ident.t -> _ t0 -> AliasTarget.t option = fun k m -> Alias.find_id k m.alias
+  let find_alias_id : Ident.t -> _ t0 -> AliasTarget.t option = fun k m -> Alias.find_id k m.alias
 
   let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t option) option =
    fun k m ->
@@ -1922,8 +1925,8 @@ module Mem = struct
    fun k -> f_lift_default ~default:None (MemReach.find_opt k)
 
 
-  let find_alias : Ident.t -> _ t0 -> AliasTarget.t option =
-   fun k -> f_lift_default ~default:None (MemReach.find_alias k)
+  let find_alias_id : Ident.t -> _ t0 -> AliasTarget.t option =
+   fun k -> f_lift_default ~default:None (MemReach.find_alias_id k)
 
 
   let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t option) option =

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -378,15 +378,6 @@ let infer_print e =
   {exec; check= no_check}
 
 
-let eval_array_locs_length arr_locs mem =
-  if PowLoc.is_empty arr_locs then Dom.Val.Itv.top
-  else
-    let arr = Dom.Mem.find_set arr_locs mem in
-    let traces = Dom.Val.get_traces arr in
-    let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in
-    Dom.Val.of_itv ~traces length
-
-
 let load_size_alias id arr_locs mem =
   match PowLoc.is_singleton_or_more arr_locs with
   | IContainer.Singleton loc ->
@@ -399,7 +390,7 @@ let load_size_alias id arr_locs mem =
 let get_array_length array_exp =
   let exec _ ~ret:(ret_id, _) mem =
     let arr_locs = Sem.eval_locs array_exp mem in
-    let result = eval_array_locs_length arr_locs mem in
+    let result = Sem.eval_array_locs_length arr_locs mem in
     model_by_value result ret_id mem |> load_size_alias ret_id arr_locs
   in
   {exec; check= no_check}
@@ -558,11 +549,13 @@ module ArrObjCommon = struct
     Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths exp mem) |> PowLoc.append_field ~fn
 
 
-  let eval_size model_env exp ~fn mem = eval_array_locs_length (deref_of model_env exp ~fn mem) mem
+  let eval_size model_env exp ~fn mem =
+    Sem.eval_array_locs_length (deref_of model_env exp ~fn mem) mem
+
 
   let size_exec exp ~fn model_env ~ret:(id, _) mem =
     let arr_locs = deref_of model_env exp ~fn mem in
-    let mem = Dom.Mem.add_stack (Loc.of_id id) (eval_array_locs_length arr_locs mem) mem in
+    let mem = Dom.Mem.add_stack (Loc.of_id id) (Sem.eval_array_locs_length arr_locs mem) mem in
     load_size_alias id arr_locs mem
 
 
@@ -694,7 +687,9 @@ module StdVector = struct
     let exec model_env ~ret:_ mem =
       let arr_locs = deref_of model_env elt_typ vec_arg mem in
       let mem =
-        let new_size = Dom.Val.plus_a (eval_array_locs_length arr_locs mem) (Dom.Val.of_int 1) in
+        let new_size =
+          Dom.Val.plus_a (Sem.eval_array_locs_length arr_locs mem) (Dom.Val.of_int 1)
+        in
         set_size model_env arr_locs new_size mem
       in
       let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set arr_locs mem) in
@@ -845,7 +840,7 @@ module Collection = struct
 
   let eval_collection_length coll_exp mem =
     let arr_locs = eval_collection_internal_array_locs coll_exp mem in
-    eval_array_locs_length arr_locs mem
+    Sem.eval_array_locs_length arr_locs mem
 
 
   let change_size_by ~size_f coll_id {location} ~ret:_ mem =
@@ -1027,7 +1022,7 @@ module JavaString = struct
         (Dom.Val.of_int (String.length s), Dom.Val.of_itv (get_char_range s))
     | _ ->
         let arr_locs = deref_of model_env exp mem in
-        let length = eval_array_locs_length arr_locs mem in
+        let length = Sem.eval_array_locs_length arr_locs mem in
         let elem =
           let arr_locs = Dom.Val.get_all_locs (Dom.Mem.find_set arr_locs mem) in
           Dom.Mem.find_set arr_locs mem

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -28,7 +28,7 @@ let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool =
  fun e1 e2 m ->
   match (e1, e2) with
   | Exp.Var x1, Exp.Var x2 -> (
-    match (Mem.find_alias x1 m, Mem.find_alias x2 m) with
+    match (Mem.find_alias_id x1 m, Mem.find_alias_id x2 m) with
     | Some x1', Some x2' ->
         AliasTarget.equal x1' x2'
         && PowLoc.for_all (fun l -> not (Mem.is_rep_multi_loc l m)) (AliasTarget.get_locs x1')
@@ -313,7 +313,7 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
  fun integer_type_widths exp mem ->
   match exp with
   | Exp.Var id -> (
-    match Mem.find_alias id mem with
+    match Mem.find_alias_id id mem with
     | Some (AliasTarget.Simple {l= loc; i}) when IntLit.iszero i ->
         Mem.find loc mem
     | Some
@@ -502,6 +502,15 @@ let get_offset_sym_f integer_type_widths mem e =
 
 let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_type_widths e mem)
 
+let eval_array_locs_length arr_locs mem =
+  if PowLoc.is_empty arr_locs then Val.Itv.top
+  else
+    let arr = Mem.find_set arr_locs mem in
+    let traces = Val.get_traces arr in
+    let length = Val.get_array_blk arr |> ArrayBlk.sizeof in
+    Val.of_itv ~traces length
+
+
 module Prune = struct
   type t = {prune_pairs: PrunePairs.t; mem: Mem.t}
 
@@ -515,7 +524,7 @@ module Prune = struct
    fun e ({mem} as astate) ->
     match e with
     | Exp.Var x -> (
-      match Mem.find_alias x mem with
+      match Mem.find_alias_id x mem with
       | Some (AliasTarget.Simple {l= lv; i}) when IntLit.iszero i ->
           let v = Mem.find lv mem in
           let v' = Val.prune_ne_zero v in
@@ -531,7 +540,7 @@ module Prune = struct
       | Some (AliasTarget.Simple _ | AliasTarget.Size _ | Top) | None ->
           astate )
     | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> (
-      match Mem.find_alias x mem with
+      match Mem.find_alias_id x mem with
       | Some (AliasTarget.Simple {l= lv; i}) when IntLit.iszero i ->
           let v = Mem.find lv mem in
           let v' = Val.prune_eq_zero v in

infer/src/checkers/costModels.ml

@@ -17,7 +17,7 @@ end
 
 module Array : S = struct
   let length arr_exp inferbo_mem =
-    BufferOverrunModels.eval_array_locs_length
+    BufferOverrunSemantics.eval_array_locs_length
       (BufferOverrunSemantics.eval_locs arr_exp inferbo_mem)
       inferbo_mem
 end