[preanalysis] more conservative and efficient devirtualizers

Summary:
Move from Map to SafeInvertedMap:
- joining two branches where only one branch had the variable set to a
  given closure or type should *not* keep that information around: now
  we correctly get Top instead
- the "Safe" part is an optimisation that doesn't store Top values in
  the map, which is important as most values are not closures so we
  don't care about storing the fact that we don't know anything about
  them

Reviewed By: ngorogiannis

Differential Revision: D24418560

fbshipit-source-id: 0ac701502

infer/src/backend/ClosureSubstSpecializedMethod.ml

@@ -14,7 +14,7 @@ module PPPVar = struct
 end
 
 module VDom = AbstractDomain.Flat (PPPVar)
-module Domain = AbstractDomain.Map (Ident) (VDom)
+module Domain = AbstractDomain.SafeInvertedMap (Ident) (VDom)
 
 module TransferFunctions = struct
   module CFG = CFG
@@ -28,9 +28,9 @@ module TransferFunctions = struct
     | Load {id; e= Exp.Lvar pvar} ->
         Domain.add id (VDom.v pvar) astate
     | Load {id} ->
-        Domain.add id VDom.bottom astate
+        Domain.add id VDom.top astate
     | Call ((id, _), _, _, _, _) ->
-        Domain.add id VDom.bottom astate
+        Domain.add id VDom.top astate
     | _ ->
         astate
 

infer/src/backend/ClosuresSubstitution.ml

@@ -25,13 +25,13 @@ end
 
 module VDom = AbstractDomain.Flat (ExpClosure)
 module CFG = ProcCfg.Normal
-module Domain = AbstractDomain.Map (Var) (VDom)
+module Domain = AbstractDomain.SafeInvertedMap (Var) (VDom)
 
-let get_var (astate : Domain.t) (v : Var.t) : VDom.t =
+let get_var (astate : Domain.t) (v : Var.t) =
-  match Domain.find_opt v astate with Some ab -> ab | None -> VDom.bottom
+  match Domain.find_opt v astate with Some c -> c | None -> VDom.top
 
 
-let rec eval_expr (astate : Domain.t) (expr : Exp.t) : VDom.t =
+let rec eval_expr (astate : Domain.t) (expr : Exp.t) =
   match expr with
   | Var id ->
       get_var astate (Var.of_id id)
@@ -75,12 +75,9 @@ end
 
 module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions)
 
-let get_invariant_at_node (map : Analyzer.invariant_map) node : Domain.t =
+let get_invariant_at_node (map : Analyzer.invariant_map) node =
-  match Analyzer.InvariantMap.find_opt (Procdesc.Node.get_id node) map with
+  Analyzer.InvariantMap.find_opt (Procdesc.Node.get_id node) map
-  | Some abstate ->
+  |> Option.value_map ~default:Domain.top ~f:(fun abstate -> abstate.AbstractInterpreter.State.pre)
-      abstate.pre
-  | None ->
-      Domain.bottom
 
 
 let replace_closure_call node (astate : Domain.t) (instr : Sil.instr) : Sil.instr =
@@ -90,8 +87,7 @@ let replace_closure_call node (astate : Domain.t) (instr : Sil.instr) : Sil.inst
       match instr with
       | Call (ret_id_typ, Var id, actual_params, loc, call_flags) -> (
           L.d_printfln "call  %a " (Sil.pp_instr Pp.text ~print_types:true) instr ;
-          let aval = eval_expr astate (Var id) in
+          match eval_expr astate (Var id) |> VDom.get with
-          match VDom.get aval with
           | None ->
               L.d_printfln "(no closure found)" ;
               instr
@@ -126,7 +122,7 @@ let replace_closure_param node (astate : Domain.t) (instr : Sil.instr) : Sil.ins
           | Exp.Closure _ ->
               param
           | _ -> (
-            match VDom.get (eval_expr astate exp) with
+            match eval_expr astate exp |> VDom.get with
             | None ->
                 param
             | Some c ->

infer/src/backend/Devirtualizer.ml

@@ -18,10 +18,10 @@ module L = Logging
 module VDom = AbstractDomain.Flat (JavaClassName)
 
 module CFG = ProcCfg.Normal
-module Domain = AbstractDomain.Map (Var) (VDom)
+module Domain = AbstractDomain.SafeInvertedMap (Var) (VDom)
 
 let get_var (astate : Domain.t) (v : Var.t) : VDom.t =
-  match Domain.find_opt v astate with Some ab -> ab | None -> VDom.bottom
+  match Domain.find_opt v astate with Some ab -> ab | None -> VDom.top
 
 
 let rec eval_expr (astate : Domain.t) (expr : Exp.t) : VDom.t =
@@ -93,7 +93,7 @@ let analyze_at_node (map : Analyzer.invariant_map) node : Domain.t =
   | Some abstate ->
       abstate.pre
   | None ->
-      Domain.bottom
+      Domain.top
 
 
 (* inspired from biabduction/Symexec.ml, function resolve_method  *)