[HIL] make it easier to customize-specialized abstract interpreter

Reviewed By: jeremydubreil

Differential Revision: D6299382

fbshipit-source-id: 0722a56

infer/src/absint/LowerHil.ml

@@ -87,12 +87,12 @@ struct
 
 end
 
-module MakeAbstractInterpreter
+module MakeAbstractInterpreterWithConfig
+    (HilConfig : HilConfig)
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeHIL) =
 struct
-  module Interpreter =
+  module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig))
-    AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig))
 
   let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial =
     if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv ;
@@ -100,3 +100,5 @@ struct
     Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial')
 
 end
+
+module MakeAbstractInterpreter = MakeAbstractInterpreterWithConfig (DefaultConfig)

infer/src/absint/LowerHil.mli

@@ -34,11 +34,12 @@ module Make
 end
 
 (** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *)
-module MakeAbstractInterpreter
+module MakeAbstractInterpreterWithConfig
+    (HilConfig : HilConfig)
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig
   module Interpreter :
-      module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig))
+      module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig))
 
   val compute_post :
     Interpreter.TransferFunctions.extras ProcData.t
@@ -47,3 +48,11 @@ module MakeAbstractInterpreter
   (** compute and return the postcondition for the given procedure starting from [initial]. If
       [debug] is true, print html debugging output. *)
 end
+
+(** Simpler version of the above wrapper that uses the default HIL config *)
+module MakeAbstractInterpreter
+    (CFG : ProcCfg.S)
+    (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig
+  include module type of
+    MakeAbstractInterpreterWithConfig (DefaultConfig) (CFG) (MakeTransferFunctions)
+end

infer/src/quandary/TaintAnalysis.ml

@@ -708,7 +708,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
   end
 
   module Analyzer =
-    AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make (TransferFunctions) (HilConfig))
+    LowerHil.MakeAbstractInterpreterWithConfig (HilConfig) (ProcCfg.Exceptional)
+      (TransferFunctions)
 
   (* sanity checks for summaries. should only be used in developer mode *)
   let check_invariants access_tree =
@@ -828,21 +829,18 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     (* bind parameters to a trace with a tainted source (if applicable) *)
     let make_initial pdesc =
       let pname = Procdesc.get_proc_name pdesc in
-      let access_tree =
+      List.fold
-        List.fold
+        ~f:(fun acc (name, typ, taint_opt) ->
-          ~f:(fun acc (name, typ, taint_opt) ->
+          match taint_opt with
-            match taint_opt with
+          | Some source ->
-            | Some source ->
+              let base_ap =
-                let base_ap =
+                AccessPath.Abs.Abstracted (AccessPath.of_pvar (Pvar.mk name pname) typ)
-                  AccessPath.Abs.Abstracted (AccessPath.of_pvar (Pvar.mk name pname) typ)
+              in
-                in
+              TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc
-                TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc
+          | None ->
-            | None ->
+              acc)
-                acc)
+        ~init:TaintDomain.empty
-          ~init:TaintDomain.empty
+        (TraceDomain.Source.get_tainted_formals pdesc tenv)
-          (TraceDomain.Source.get_tainted_formals pdesc tenv)
-      in
-      (access_tree, IdAccessPathMapDomain.empty)
     in
     Preanal.do_dynamic_dispatch proc_desc (Cg.create (SourceFile.invalid __FILE__)) tenv ;
     let initial = make_initial proc_desc in
@@ -851,8 +849,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       {formal_map; summary}
     in
     let proc_data = ProcData.make proc_desc tenv extras in
-    match Analyzer.compute_post proc_data ~initial ~debug:false with
+    match Analyzer.compute_post proc_data ~initial with
-    | Some (access_tree, _) ->
+    | Some access_tree ->
         Summary.update_summary (make_summary proc_data access_tree) summary
     | None ->
         if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (