Cost/inferbo: move range to numerical abstract domain

Reviewed By: ddino

Differential Revision: D7843351

fbshipit-source-id: 92a8f94

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -317,6 +317,14 @@ module Heap = struct
    fun mem ->
     let mem = filter (fun l _ -> Loc.is_return l) mem in
     if is_empty mem then Val.bot else snd (choose mem)
+
+
+  let range : filter_loc:(Loc.t -> bool) -> astate -> Itv.Bound.t =
+   fun ~filter_loc mem ->
+    fold
+      (fun loc v acc ->
+        if filter_loc loc then v |> Val.get_itv |> Itv.range |> Itv.Bound.mult acc else acc )
+      mem Itv.Bound.one
 end
 
 module AliasTarget = struct
@@ -758,6 +766,10 @@ module MemReach = struct
         add_from_locs heap reachable_locs (PowLoc.add loc acc)
     in
     fun locs m -> add_from_locs m.heap locs PowLoc.empty
+
+
+  let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.Bound.t =
+   fun ~filter_loc {heap} -> Heap.range ~filter_loc heap
 end
 
 module Mem = struct

infer/src/checkers/cost.ml

@@ -110,37 +110,23 @@ module BoundMap = struct
     L.(debug Analysis Medium) "@\n******* END Bound Map ITV **** @\n\n"
 
 
-  let convert (mem: BufferOverrunDomain.Mem.astate) : CostDomain.EnvDomainBO.astate =
-    let open AbstractDomain.Types in
-    match mem with
-    | Bottom ->
-        L.internal_error
-          "@\n\
-           [COST ANALYSIS INTERNAL WARNING:] Found Bottom when converting mem, returning No env \n" ;
-        Bottom
-    | NonBottom {BufferOverrunDomain.MemReach.heap} ->
-        let env =
-          BufferOverrunDomain.Heap.fold
-            (fun loc data acc ->
-              match loc with
-              | AbsLoc.Loc.Var (Var.LogicalVar id) ->
-                  let key = Exp.Var id in
-                  CostDomain.EnvMap.add key (BufferOverrunDomain.Val.get_itv data) acc
-              | AbsLoc.Loc.Var (Var.ProgramVar v) ->
-                  let key = Exp.Lvar v in
-                  CostDomain.EnvMap.add key (BufferOverrunDomain.Val.get_itv data) acc
+  let filter_loc formal_pvars vars_to_keep = function
+    | AbsLoc.Loc.Var (Var.LogicalVar _) ->
+        false
+    | AbsLoc.Loc.Var (Var.ProgramVar pvar) when List.mem formal_pvars pvar ~equal:Pvar.equal ->
+        false
+    | AbsLoc.Loc.Var var when Control.VarSet.mem var vars_to_keep ->
+        true
     | _ ->
-                  acc )
-            heap CostDomain.EnvMap.empty
-        in
-        NonBottom env
+        false
 
 
   let compute_upperbound_map node_cfg inferbo_invariant_map data_invariant_map
       control_invariant_map =
-    let fparam = Procdesc.get_formals node_cfg in
     let pname = Procdesc.get_proc_name node_cfg in
-    let fparam' = List.map ~f:(fun (m, _) -> Exp.Lvar (Pvar.mk m pname)) fparam in
+    let formal_pvars =
+      Procdesc.get_formals node_cfg |> List.map ~f:(fun (m, _) -> Pvar.mk m pname)
+    in
     let compute_node_upper_bound bound_map node =
       let node_id = NodeCFG.id node in
       match Procdesc.Node.get_kind node with
@@ -162,39 +148,17 @@ module BoundMap = struct
                 Control.VarSet.pp all_deps ;
               (* bound = env(v1) *... * env(vn) *)
               let bound =
-                match convert entry_mem with
+                match entry_mem with
                 | Bottom ->
-                    (* We get None by converting Bottom *)
                     L.internal_error
                       "@\n\
                        [COST ANALYSIS INTERNAL WARNING:] No 'env' found. This location is \
                        unreachable returning cost 0 \n" ;
                     Itv.Bound.zero
-                | NonBottom env ->
-                    CostDomain.EnvMap.fold
-                      (fun exp itv acc ->
-                        let itv' =
-                          match exp with
-                          | Exp.Var _ ->
-                              Itv.one
-                          (* For temp var we give [1,1] so it doesn't count*)
-                          | Exp.Lvar _
-                            when List.mem fparam' exp ~equal:Exp.equal ->
-                              Itv.one
-                          | Exp.Lvar pvar when Control.VarSet.mem (Var.of_pvar pvar) all_deps ->
-                              itv
-                          | Exp.Lvar _ ->
-                              (* For a var that doesn't affect control flow directly or indirectly, we give [1,1] so it doesn't count *)
-                              Itv.one
-                          | _ ->
-                              assert false
-                        in
-                        let range = Itv.range itv' in
-                        L.(debug Analysis Medium)
-                          "@\n>>>For node = %a :  exp=%a  itv=%a   range =%a @\n\n" Node.pp_id
-                          node_id Exp.pp exp Itv.pp itv' Itv.Bound.pp range ;
-                        Itv.Bound.mult acc range )
-                      env Itv.Bound.one
+                | NonBottom mem ->
+                    BufferOverrunDomain.MemReach.heap_range
+                      ~filter_loc:(filter_loc formal_pvars all_deps)
+                      mem
               in
               L.(debug Analysis Medium)
                 "@\n>>>Setting bound for node = %a  to %a@\n\n" Node.pp_id node_id Itv.Bound.pp

infer/src/checkers/costDomain.ml

@@ -12,8 +12,6 @@ module F = Format
 
 (** Map (node,instr) -> basic cost  *)
 module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (Itv.Bound)
-module EnvMap = AbstractDomain.Map (Exp) (Itv)
-module EnvDomainBO = AbstractDomain.BottomLifted (EnvMap)
 
 type summary = {post: Itv.Bound.t}