[inferbo] Preparing for one-value symbols

Reviewed By: skcho

Differential Revision: D13071832

fbshipit-source-id: d978eead0

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -335,25 +335,21 @@ let eval_sympath params sympath mem =
 
 
 let mk_eval_sym_trace callee_pdesc actual_exps caller_mem =
-  let formals = get_formals callee_pdesc in
-  let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) actual_exps in
-  let params = ParamBindings.make formals actuals in
-  let eval_sym_traced s =
+  let params =
+    let formals = get_formals callee_pdesc in
+    let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) actual_exps in
+    ParamBindings.make formals actuals
+  in
+  let eval_sym s =
+    let sympath = Symb.Symbol.path s in
+    let itv, _ = eval_sympath params sympath caller_mem in
+    Itv.get_bound itv (Symb.Symbol.bound_end s)
+  in
+  let trace_of_sym s =
     let sympath = Symb.Symbol.path s in
     let itv, traces = eval_sympath params sympath caller_mem in
-    if Itv.eq itv Itv.bot then (Bottom, TraceSet.empty)
-    else
-      let get_bound =
-        match Symb.Symbol.bound_end s with
-        | Symb.BoundEnd.LowerBound ->
-            Itv.lb
-        | Symb.BoundEnd.UpperBound ->
-            Itv.ub
-      in
-      (NonBottom (get_bound itv), traces)
+    if Itv.eq itv Itv.bot then TraceSet.empty else traces
   in
-  let eval_sym s = fst (eval_sym_traced s) in
-  let trace_of_sym s = snd (eval_sym_traced s) in
   let eval_locpath partial = eval_locpath params partial caller_mem in
   ((eval_sym, trace_of_sym), eval_locpath)
 

infer/src/bufferoverrun/itv.ml

@@ -539,9 +539,9 @@ module ItvPure = struct
     if Bound.equal l u then Bound.pp fmt l
     else
       match Bound.is_same_symbol l u with
-      | Some symbol ->
+      | Some symbol when Config.bo_debug < 3 ->
           Symb.SymbolPath.pp fmt symbol
-      | None ->
+      | _ ->
           F.fprintf fmt "[%a, %a]" Bound.pp l Bound.pp u
 
 
@@ -889,6 +889,16 @@ let ub : t -> Bound.t = function
       L.(die InternalError) "upper bound of bottom"
 
 
+let get_bound itv (be : Symb.BoundEnd.t) =
+  match (itv, be) with
+  | Bottom, _ ->
+      Bottom
+  | NonBottom x, LowerBound ->
+      NonBottom (ItvPure.lb x)
+  | NonBottom x, UpperBound ->
+      NonBottom (ItvPure.ub x)
+
+
 let false_sem = NonBottom ItvPure.false_sem
 
 let m1_255 = NonBottom ItvPure.m1_255

infer/src/bufferoverrun/itv.mli

@@ -193,6 +193,8 @@ val lb : t -> Bound.t
 
 val ub : t -> Bound.t
 
+val get_bound : t -> Symb.BoundEnd.t -> Bound.t bottom_lifted
+
 val is_false : t -> bool
 
 val neg : t -> t