[hil] add HIL wrapper for abstract interpreter

Summary:
Before this change, analyses using HIL needed to pass `IdAcessPathMapDomain.empty` to abstract interpreter, and would get back the map as part of the post.
This is a confusing API and was a pain point for Dino in trying to use HIL.

This diff adds a HIL wrapper around the abstract interpreter that hides these details.
It replaces `LowerHIL.makeDefault` as the new "simplest possible way" to use HIL.

Reviewed By: jberdine

Differential Revision: D6125597

fbshipit-source-id: 560856b

infer/src/absint/LowerHil.ml

@@ -60,5 +60,15 @@ struct
 
 end
 
-module MakeDefault (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) =
+module MakeAbstractInterpreter
-  Make (MakeTransferFunctions) (DefaultConfig) (CFG)
+    (CFG : ProcCfg.S)
+    (MakeTransferFunctions : TransferFunctions.MakeHIL) =
+struct
+  module Interpreter =
+    AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig))
+
+  let compute_post ?(debug= Config.debug_mode) proc_data ~initial =
+    let initial' = (initial, IdAccessPathMapDomain.empty) in
+    Option.map ~f:fst (Interpreter.compute_post ~debug proc_data ~initial:initial')
+
+end

infer/src/absint/LowerHil.mli

@@ -33,6 +33,17 @@ module Make
   val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate
 end
 
-module MakeDefault (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) : sig
+(** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *)
-  include module type of Make (MakeTransferFunctions) (DefaultConfig) (CFG)
+module MakeAbstractInterpreter
+    (CFG : ProcCfg.S)
+    (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig
+  module Interpreter :
+      module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig))
+
+  val compute_post :
+    ?debug:bool -> Interpreter.TransferFunctions.extras ProcData.t
+    -> initial:MakeTransferFunctions(CFG).Domain.astate
+    -> MakeTransferFunctions(CFG).Domain.astate option
+  (** compute and return the postcondition for the given procedure starting from [initial]. If
+      [debug] is true, print html debugging output. *)
 end

infer/src/checkers/NullabilityCheck.ml

@@ -114,12 +114,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 end
 
-module Analyzer =
+module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions)
-  AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions))
 
 let checker {Callbacks.summary; proc_desc; tenv} =
-  let initial = (Domain.empty, IdAccessPathMapDomain.empty) in
+  let initial = Domain.empty in
   let proc_data = ProcData.make proc_desc tenv summary in
   ignore (Analyzer.compute_post proc_data ~initial ~debug:false) ;
   summary
-

infer/src/checkers/NullabilitySuggest.ml

@@ -104,8 +104,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 end
 
-module Analyzer =
+module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions)
-  AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.MakeDefault (TransferFunctions))
 
 let make_error_trace astate ap ud =
   let name_of ap =
@@ -184,11 +183,10 @@ let checker {Callbacks.summary; proc_desc; tenv} =
     summary
   else
     (* Assume all fields are not null in the beginning *)
-    let initial = (Domain.empty, IdAccessPathMapDomain.empty) in
+    let initial = Domain.empty in
     let proc_data = ProcData.make_default proc_desc tenv in
     match Analyzer.compute_post proc_data ~initial ~debug:false with
-    | Some (post, _) ->
+    | Some post ->
         report post proc_data ; summary
     | None ->
         L.(die InternalError) "Analyzer failed to compute post for %a" Typ.Procname.pp proc_name
-

infer/src/checkers/uninit.ml

@@ -74,7 +74,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 end
 
 module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Normal)
-module Analyzer = AbstractInterpreter.Make (CFG) (LowerHil.MakeDefault (TransferFunctions))
+module Analyzer =
+  AbstractInterpreter.Make (CFG) (LowerHil.Make (TransferFunctions) (LowerHil.DefaultConfig))
 
 let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
   let cfg = CFG.from_pdesc proc_desc in

infer/src/concurrency/RacerD.ml

@@ -967,8 +967,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 end
 
-module Analyzer =
+module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions)
-  AbstractInterpreter.Make (ProcCfg.Normal) (LowerHil.MakeDefault (TransferFunctions))
 
 (* Methods in @ThreadConfined classes and methods annotated with @ThreadConfined are assumed to all
    run on the same thread. For the moment we won't warn on accesses resulting from use of such
@@ -1131,7 +1130,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
           (* express that the constructor owns [this] *)
         in
         let ownership = List.fold ~f:add_owned_formal owned_formals ~init:own_locals_in_cpp in
-        ({RacerDDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty)
+        {RacerDDomain.empty with ownership; threads}
       else
         (* add Owned(formal_index) predicates for each formal to indicate that each one is owned if
            it is owned in the caller *)
@@ -1143,10 +1142,10 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
             (FormalMap.get_formals_indexes formal_map)
             ~init:own_locals_in_cpp
         in
-        ({RacerDDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty)
+        {RacerDDomain.empty with ownership; threads}
     in
     match Analyzer.compute_post proc_data ~initial ~debug:false with
-    | Some ({threads; locks; accesses; ownership; attribute_map}, _) ->
+    | Some {threads; locks; accesses; ownership; attribute_map} ->
         let return_var_ap =
           AccessPath.of_pvar
             (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))

infer/src/labs/ResourceLeaks.ml

@@ -93,12 +93,12 @@ end
 
 (* Create an intraprocedural abstract interpreter from the transfer functions we defined *)
 module Analyzer =
-  AbstractInterpreter.Make
+  LowerHil.MakeAbstractInterpreter
     (* Type of CFG to analyze--Exceptional to follow exceptional control-flow edges, Normal to
        ignore them *)
     (ProcCfg.Normal)
     (* 5(a) *)
-    (LowerHil.Make (TransferFunctions) (LowerHil.DefaultConfig))
+    (TransferFunctions)
 
 (* Callback for invoking the checker from the outside--registered in RegisterCheckers *)
 let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary =
@@ -118,9 +118,8 @@ let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary =
   in
   let extras = FormalMap.make proc_desc in
   let proc_data = ProcData.make proc_desc tenv extras in
-  let initial = (ResourceLeakDomain.initial, IdAccessPathMapDomain.empty) in
+  match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial ~debug:false with
-  match Analyzer.compute_post proc_data ~initial ~debug:false with
+  | Some post ->
-  | Some (post, _) ->
       (* 1(f) *)
       report post proc_data ;
       Summary.update_summary (convert_to_summary post) summary

infer/src/unit/TaintTests.ml

@@ -60,7 +60,9 @@ module MockTaintAnalysis = TaintAnalysis.Make (struct
 end)
 
 module TestInterpreter =
-  AnalyzerTester.Make (ProcCfg.Normal) (LowerHil.MakeDefault (MockTaintAnalysis.TransferFunctions))
+  AnalyzerTester.Make
+    (ProcCfg.Normal)
+    (LowerHil.Make (MockTaintAnalysis.TransferFunctions) (LowerHil.DefaultConfig))
 
 let tests =
   let open OUnit2 in