checkers/dune

Summary:
Needed to move a bunch of files around to make this happen. Notably,
moving "preanal.ml" outside of checkers/ into backend/ since it needs to
modify the proc desc in the summary. Also hoisting goes to cost/.

Reviewed By: skcho

Differential Revision: D21407069

fbshipit-source-id: ebb9b78ec

infer/src/backend/preanal.ml

@@ -234,11 +234,7 @@ module Liveness = struct
         (* can't take the address of a variable in Java *)
       else
         let initial = AddressTaken.Domain.empty in
-        match
+        match AddressTaken.Analyzer.compute_post () ~initial (Summary.get_proc_desc summary) with
-          AddressTaken.Analyzer.compute_post
-            {ProcData.summary; tenv; extras= ()}
-            ~initial (Summary.get_proc_desc summary)
-        with
         | Some post ->
             post
         | None ->
@@ -306,10 +302,9 @@ module Liveness = struct
 end
 
 module FunctionPointerSubstitution = struct
-  let process summary tenv =
+  let process proc_desc =
-    let updated = FunctionPointers.substitute_function_pointers summary tenv in
+    let updated = FunctionPointers.substitute_function_pointers proc_desc in
-    let pdesc = Summary.get_proc_desc summary in
+    if updated then Attributes.store ~proc_desc:(Some proc_desc) (Procdesc.get_attributes proc_desc)
-    if updated then Attributes.store ~proc_desc:(Some pdesc) (Procdesc.get_attributes pdesc)
 end
 
 (** pre-analysis to cut control flow after calls to functions whose type indicates they do not
@@ -381,7 +376,7 @@ let do_preanalysis exe_env pdesc =
   let proc_name = Procdesc.get_proc_name pdesc in
   if Procname.is_java proc_name then InlineJavaSyntheticMethods.process pdesc ;
   if Config.function_pointer_specialization && not (Procname.is_java proc_name) then
-    FunctionPointerSubstitution.process summary tenv ;
+    FunctionPointerSubstitution.process pdesc ;
   Liveness.process summary tenv ;
   AddAbstractionInstructions.process pdesc ;
   NoReturn.process tenv pdesc ;

infer/src/checkers/NullabilityPreanalysis.ml

@@ -20,7 +20,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = FieldsAssignedInConstructors
 
-  type analysis_data = Exp.t Ident.Hash.t ProcData.t
+  type analysis_data = Exp.t Ident.Hash.t
 
   let exp_is_null ids_map exp =
     match exp with
@@ -38,18 +38,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     with Caml.Not_found -> false
 
 
-  let exec_instr astate (proc_data : Exp.t Ident.Hash.t ProcData.t) _ instr =
+  let exec_instr astate id_table _ instr =
     match instr with
     | Sil.Load {id; e= exp} ->
-        Ident.Hash.add proc_data.extras id exp ;
+        Ident.Hash.add id_table id exp ; astate
-        astate
     | Sil.Store {e1= Exp.Lfield (Exp.Var lhs_id, name, typ); typ= exp_typ; e2= rhs} -> (
       match exp_typ.Typ.desc with
       (* block field of a ObjC class *)
       | Typ.Tptr ({desc= Tfun}, _)
-        when Typ.is_objc_class typ && is_self proc_data.extras lhs_id
+        when Typ.is_objc_class typ && is_self id_table lhs_id
              && (* lhs is self, rhs is not null *)
-             not (exp_is_null proc_data.extras rhs) ->
+             not (exp_is_null id_table rhs) ->
           FieldsAssignedInConstructors.add (name, typ) astate
       | _ ->
           astate )
@@ -94,9 +93,7 @@ let analysis cfg tenv =
   let f proc_name pdesc domain =
     if Procdesc.is_defined pdesc && Procname.is_constructor proc_name then
       match
-        FieldsAssignedInConstructorsChecker.compute_post ~initial
+        FieldsAssignedInConstructorsChecker.compute_post ~initial (Ident.Hash.create 10) pdesc
-          {ProcData.summary= Summary.OnDisk.reset pdesc; tenv; extras= Ident.Hash.create 10}
-          pdesc
       with
       | Some new_domain ->
           FieldsAssignedInConstructors.union new_domain domain

infer/src/checkers/SelfInBlock.ml

@@ -329,7 +329,7 @@ module TransferFunctions = struct
       | _ ->
           domain
     in
-    let proc_desc_opt = Ondemand.get_proc_desc pname in
+    let proc_desc_opt = AnalysisCallbacks.get_proc_desc pname in
     let annotations = get_annotations proc_desc_opt in
     let args =
       if is_objc_instance proc_desc_opt then match args with _ :: rest -> rest | [] -> []

infer/src/checkers/SimpleChecker.ml

@@ -31,7 +31,7 @@ module type Spec = sig
 end
 
 module type S = sig
-  val checker : Callbacks.proc_callback_t
+  val checker : IntraproceduralAnalysis.t -> unit
   (** add YourChecker.checker to registerCallbacks.ml to run your checker *)
 end
 
@@ -60,14 +60,13 @@ module Make (Spec : Spec) : S = struct
     module CFG = CFG
     module Domain = Domain
 
-    type analysis_data = unit ProcData.t
+    type analysis_data = IntraproceduralAnalysis.t
 
-    let exec_instr astate_set proc_data node instr =
+    let exec_instr astate_set {IntraproceduralAnalysis.proc_desc; tenv} node instr =
       let node_kind = CFG.Node.kind node in
-      let pname = Summary.get_proc_name proc_data.ProcData.summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       Domain.fold
-        (fun astate acc ->
+        (fun astate acc -> Domain.add (Spec.exec_instr astate instr node_kind pname tenv) acc)
-          Domain.add (Spec.exec_instr astate instr node_kind pname proc_data.ProcData.tenv) acc )
         astate_set Domain.empty
 
 
@@ -76,10 +75,8 @@ module Make (Spec : Spec) : S = struct
 
   module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))
 
-  let checker {Callbacks.exe_env; summary} : Summary.t =
+  let checker ({IntraproceduralAnalysis.proc_desc} as analysis_data) =
-    let proc_desc = Summary.get_proc_desc summary in
     let proc_name = Procdesc.get_proc_name proc_desc in
-    let tenv = Exe_env.get_tenv exe_env proc_name in
     let nodes = Procdesc.get_nodes proc_desc in
     let do_reporting node_id state =
       let astate_set = state.AbstractInterpreter.State.post in
@@ -94,9 +91,6 @@ module Make (Spec : Spec) : S = struct
           (fun astate -> Spec.report astate (ProcCfg.Exceptional.Node.loc node) proc_name)
           astate_set
     in
-    let inv_map =
+    let inv_map = Analyzer.exec_pdesc analysis_data ~initial:Domain.empty proc_desc in
-      Analyzer.exec_pdesc {ProcData.summary; tenv; extras= ()} ~initial:Domain.empty proc_desc
+    Analyzer.InvariantMap.iter do_reporting inv_map
-    in
-    Analyzer.InvariantMap.iter do_reporting inv_map ;
-    summary
 end

infer/src/checkers/SimpleChecker.mli

@@ -20,7 +20,7 @@ module type Spec = sig
 end
 
 module type S = sig
-  val checker : Callbacks.proc_callback_t
+  val checker : IntraproceduralAnalysis.t -> unit
 end
 
 module Make (Spec : Spec) : S

infer/src/checkers/addressTaken.ml

@@ -17,7 +17,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type analysis_data = unit ProcData.t
+  type analysis_data = unit
 
   let rec add_address_taken_pvars exp astate =
     match exp with
@@ -35,7 +35,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         astate
 
 
-  let exec_instr astate _ _ = function
+  let exec_instr astate () _ = function
     | Sil.Store {typ= {desc= Tptr _}; e2= rhs_exp} ->
         add_address_taken_pvars rhs_exp astate
     | Sil.Call (_, _, actuals, _, _) ->

infer/src/checkers/dune

@@ -0,0 +1,14 @@
+; Copyright (c) Facebook, Inc. and its affiliates.
+;
+; This source code is licensed under the MIT license found in the
+; LICENSE file in the root directory of this source tree.
+
+(library
+ (name checkers)
+ (public_name infer.checkers)
+ (flags
+  (:standard -open Core -open OpenSource -open InferIR -open InferStdlib -open IStd -open InferGenerated
+    -open InferBase -open Absint -open Biabduction -open Bo -open Pulselib))
+ (libraries base64 core ocamlgraph InferStdlib InferGenerated InferBase InferIR absint biabduction bo pulselib)
+ (preprocess (pps ppx_compare))
+)

infer/src/checkers/functionPointers.ml

@@ -21,9 +21,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type analysis_data = unit ProcData.t
+  type analysis_data = unit
 
-  let exec_instr astate _ _ = function
+  let exec_instr astate () _ = function
     | Sil.Load {id= lhs_id} when Ident.is_none lhs_id ->
         astate
     | Sil.Load {id= lhs_id; e= Exp.Lvar rhs_pvar; typ= Typ.{desc= Tptr ({desc= Tfun}, _)}} ->
@@ -90,13 +90,12 @@ let substitute_function_ptrs ~function_pointers node instr =
       instr
 
 
-let get_function_pointers summary tenv =
+let get_function_pointers proc_desc =
-  let proc_data = {ProcData.summary; tenv; extras= ()} in
+  let cfg = CFG.from_pdesc proc_desc in
-  let cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in
+  Analyzer.exec_cfg cfg () ~initial:Domain.empty
-  Analyzer.exec_cfg cfg proc_data ~initial:Domain.empty
 
 
-let substitute_function_pointers summary tenv =
+let substitute_function_pointers proc_desc =
-  let function_pointers = get_function_pointers summary tenv in
+  let function_pointers = get_function_pointers proc_desc in
   let f = substitute_function_ptrs ~function_pointers in
-  Procdesc.replace_instrs (Summary.get_proc_desc summary) ~f
+  Procdesc.replace_instrs proc_desc ~f

infer/src/checkers/uninit.ml

@@ -86,7 +86,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let is_array t = match t.Typ.desc with Typ.Tarray _ -> true | _ -> false
 
-  let get_formals pname = Ondemand.get_proc_desc pname |> Option.map ~f:Procdesc.get_formals
+  let get_formals pname =
+    AnalysisCallbacks.get_proc_desc pname |> Option.map ~f:Procdesc.get_formals
+
 
   let should_report_var pdesc tenv maybe_uninit_vars access_expr =
     let base = HilExp.AccessExpression.get_base access_expr in

infer/src/deadcode/Makefile

@@ -50,8 +50,8 @@ endif
 # Note that we run find under _build directory. Since we copy some
 # sources from subfolders to src/ folder to avoid duplicates we use
 # $(DEPTH_ONE) and iteration over main and library folders.
-LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./biabduction ./bufferoverrun ./c_stubs ./istd ./nullsafe ./pulse ./scripts
+LIBRARY_FOLDERS = . ./IR ./absint ./atd ./base ./biabduction ./bufferoverrun ./c_stubs ./checkers ./istd ./nullsafe ./pulse ./scripts
-INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I biabduction -I bufferoverrun -I c_stubs -I istd -I nullsafe -I pulse -I scripts
+INCLUDE_FOLDERS = -I absint -I IR -I atd -I base -I biabduction -I bufferoverrun -I c_stubs -I checkers -I istd -I nullsafe -I pulse -I scripts
 
 ml_src_files:=$(shell \
 	cd $(INFER_BUILD_DIR); \

infer/src/dune.in

@@ -13,7 +13,6 @@ let source_dirs =
   (if clang then ["al"; "clang"; "unit" ^/ "clang"] else ["clang_stubs"; "unit" ^/ "clang_stubs"])
   @ [ (if java then "java" else "java_stubs")
     ; "backend"
-    ; "checkers"
     ; "concurrency"
     ; "cost"
     ; "integration"
@@ -60,6 +59,8 @@ let infer_cflags =
   ; "-open"
   ; "Pulselib"
   ; "-open"
+  ; "Checkers"
+  ; "-open"
   ; "Absint"
   ; "-open"
   ; "OpenSource"
@@ -93,7 +94,14 @@ let main_lib_stanza =
     infer_cflags
     (String.concat " "
        ( common_libraries
-       @ ["InferIR"; "InferCStubs"; "absint"; "biabduction"; "nullsafe"; "bo"; "pulselib"] ))
+       @ [ "InferIR"
+         ; "InferCStubs"
+         ; "absint"
+         ; "biabduction"
+         ; "nullsafe"
+         ; "bo"
+         ; "pulselib"
+         ; "checkers" ] ))
     (String.concat " " infer_binaries)
 
 

infer/src/unit/addressTakenTests.ml

@@ -57,8 +57,6 @@ let tests =
         ; invariant "{ &b, &d }"
         ; var_assign_addrof_var ~rhs_typ:int_ptr_typ "e" "f"
         ; invariant "{ &b, &f, &d }" ] ) ]
-    |> TestInterpreter.create_tests
+    |> TestInterpreter.create_tests (fun _summary -> ()) ~initial:AddressTaken.Domain.empty
-         (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()})
-         ~initial:AddressTaken.Domain.empty
   in
   "address_taken_suite" >::: test_list