Make eradicate work in the absence of procdescs for callees.

Summary:public
Eradicate need the procedure attributes for callees.
It relies on the java front-end to create proc descs for callees that are declared but not defined.
This diff remove that needs, and when a callee without prodedure attributes is found, it creates one on the fly. The attribute created is similar to what the Java front-end would do, except
that the number and types of arguments are part of the call instruction, so they can
be used to create the formal parameters.

Reviewed By: jeremydubreil

Differential Revision: D3073904

fb-gh-sync-id: 381ff67
fbshipit-source-id: 381ff67

infer/lib/python/inferlib/jwlib.py

@@ -257,10 +257,6 @@ class AnalyzerWithFrontendWrapper(analyze.AnalyzerWrapper):
         if self.args.android_harness:
             infer_cmd.append('-harness')
 
-        if self.args.android_harness or \
-           self.args.analyzer in [config.ANALYZER_ERADICATE,
-                                  config.ANALYZER_CAPTURE]:
-            os.environ['INFER_CREATE_CALLEE_PDESC'] = 'Y'
 
         return analyze.run_command(
             infer_cmd,

infer/src/backend/iList.ml

@@ -100,6 +100,15 @@ let append l1 l2 =
 let map f l =
   rev (rev_map f l)
 
+(** tail-recursive variant of List.mapi *)
+let mapi f l =
+  let i = ref 0 in
+  rev (rev_map
+         (fun x ->
+            incr i;
+            f (!i - 1) x)
+         l)
+
 (** Remove consecutive equal elements from a list (according to the given comparison functions) *)
 let remove_duplicates compare l =
   let rec remove compare acc = function

infer/src/backend/iList.mli

@@ -45,6 +45,9 @@ val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 (** tail-recursive variant of List.map *)
 val map : ('a -> 'b) -> 'a list -> 'b list
 
+(** tail-recursive variant of List.mapi *)
+val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
+
 (** Like List.mem but without builtin equality *)
 val mem : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
 

infer/src/backend/interproc.ml

@@ -478,7 +478,7 @@ let do_symbolic_execution handle_exn tenv
   let pdesc = Cfg.Node.get_proc_desc node in
   State.mark_execution_start node;
   (* build the const map lazily *)
-  State.set_const_map (ConstantPropagation.build_const_map pdesc);
+  State.set_const_map (ConstantPropagation.build_const_map tenv pdesc);
   check_assignement_guard node;
   let instrs = Cfg.Node.get_instrs node in
   (* fresh normal vars must be fresh w.r.t. instructions *)

infer/src/backend/symExec.mli

@@ -10,6 +10,9 @@
 
 (** Symbolic Execution *)
 
+(** Lookup Java types by name. *)
+val lookup_java_typ_from_string :  Sil.tenv -> string -> Sil.typ
+
 (** print the builtin functions and exit *)
 val print_builtins : unit -> unit
 

infer/src/checkers/checkDeadCode.ml

@@ -50,7 +50,7 @@ module State = struct
     Cfg.NodeSet.cardinal t.visited
 end
 
-let do_node node (s : State.t) : (State.t list) * (State.t list) =
+let do_node _ node (s : State.t) : (State.t list) * (State.t list) =
   let s' = State.add_visited node s in
   if verbose then L.stderr "  N:%a (#visited: %a)@."
       Cfg.Node.pp node
@@ -87,7 +87,7 @@ let check_final_state proc_name proc_desc final_s =
     end
 
 (** Simple check for dead code. *)
-let callback_check_dead_code { Callbacks.proc_desc; proc_name } =
+let callback_check_dead_code { Callbacks.proc_desc; proc_name; tenv } =
 
   let module DFDead = MakeDF(struct
       type t = State.t
@@ -100,7 +100,7 @@ let callback_check_dead_code { Callbacks.proc_desc; proc_name } =
   let do_check () =
     begin
       if verbose then L.stderr "@.--@.PROC: %a@." Procname.pp proc_name;
-      let transitions = DFDead.run proc_desc State.initial in
+      let transitions = DFDead.run tenv proc_desc State.initial in
       let exit_node = Cfg.Procdesc.get_exit_node proc_desc in
       match transitions exit_node with
       | DFDead.Transition (pre_final_s, _, _) ->

infer/src/checkers/checkTraceCallSequence.ml

@@ -300,7 +300,7 @@ end
 
 
 (** State transformation for a cfg node. *)
-let do_node pn pd idenv node (s : State.t) : (State.t list) * (State.t list) =
+let do_node pn pd idenv _ node (s : State.t) : (State.t list) * (State.t list) =
   if verbose then L.stderr "N:%d S:%s@." (Cfg.Node.get_id node) (State.to_string s);
 
   let curr_state = ref s in
@@ -321,7 +321,7 @@ let check_final_state proc_name proc_desc exit_node final_s =
 (** Check that the trace calls are balanced.
     This is done by using the most general control flow including exceptions.
     The begin() and end() function are assumed not to throw exceptions. *)
-let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv } : unit =
+let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv; tenv } : unit =
 
   let module DFTrace = MakeDF(struct
       type t = State.t
@@ -337,7 +337,7 @@ let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv }
   let do_check () =
     begin
       if verbose then L.stderr "@.--@.PROC: %a@." Procname.pp proc_name;
-      let transitions = DFTrace.run proc_desc State.balanced in
+      let transitions = DFTrace.run tenv proc_desc State.balanced in
       let exit_node = Cfg.Procdesc.get_exit_node proc_desc in
       match transitions exit_node with
       | DFTrace.Transition (final_s, _, _) ->

infer/src/checkers/constantPropagation.ml

@@ -45,7 +45,7 @@ module ConstantFlow = Dataflow.MakeDF(struct
 
     let proc_throws _ = Dataflow.DontKnow
 
-    let do_node node constants =
+    let do_node _ node constants =
 
       let do_instr constants instr =
         try
@@ -125,8 +125,8 @@ module ConstantFlow = Dataflow.MakeDF(struct
       [constants], [constants]
   end)
 
-let run proc_desc =
+let run tenv proc_desc =
-  let transitions = ConstantFlow.run proc_desc ConstantMap.empty in
+  let transitions = ConstantFlow.run tenv proc_desc ConstantMap.empty in
   let get_constants node =
     match transitions node with
     | ConstantFlow.Transition (_, post_states, _) -> ConstantFlow.join post_states ConstantMap.empty
@@ -136,8 +136,8 @@ let run proc_desc =
 type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
 
 (** Build a const map lazily. *)
-let build_const_map pdesc =
+let build_const_map tenv pdesc =
-  let const_map = lazy (run pdesc) in
+  let const_map = lazy (run tenv pdesc) in
   let f node exp =
     try
       let map = (Lazy.force const_map) node in

infer/src/checkers/constantPropagation.mli

@@ -10,4 +10,4 @@
 type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
 
 (** Build a const map lazily. *)
-val build_const_map : Cfg.Procdesc.t -> const_map
+val build_const_map : Sil.tenv -> Cfg.Procdesc.t -> const_map

infer/src/checkers/dataflow.ml

@@ -21,7 +21,7 @@ module type DFStateType = sig
   val join : t -> t -> t (** Join two states (the old one is the first parameter). *)
 
   (** Perform a state transition on a node. *)
-  val do_node : Cfg.Node.t -> t -> (t list) * (t list)
+  val do_node : Sil.tenv -> Cfg.Node.t -> t -> (t list) * (t list)
 
   val proc_throws : Procname.t -> throws (** Can proc throw an exception? *)
 end
@@ -35,7 +35,7 @@ module type DF = sig
     | Transition of state * state list * state list
 
   val join : state list -> state -> state
-  val run : Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition)
+  val run : Sil.tenv -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition)
 end
 
 (** Determine if the node can throw an exception. *)
@@ -126,7 +126,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
     H.replace t.exn_states node states_exn
 
   (** Run the worklist-based dataflow algorithm. *)
-  let run proc_desc state =
+  let run tenv proc_desc state =
 
     let t =
       let start_node = Cfg.Procdesc.get_start_node proc_desc in
@@ -148,7 +148,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
         t.worklist <- S.remove node t.worklist;
         try
           let state = H.find t.pre_states node in
-          let states_succ, states_exn = St.do_node node state in
+          let states_succ, states_exn = St.do_node tenv node state in
           propagate t node states_succ states_exn (node_throws node St.proc_throws)
         with Not_found -> ()
       done in
@@ -164,18 +164,18 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
 end (* MakeDF *)
 
 (** Example dataflow callback: compute the the distance from a node to the start node. *)
-let callback_test_dataflow { Callbacks.proc_desc } =
+let callback_test_dataflow { Callbacks.proc_desc; tenv } =
   let verbose = false in
   let module DFCount = MakeDF(struct
       type t = int
       let equal = int_equal
       let join n m = if n = 0 then m else n
-      let do_node n s =
+      let do_node _ n s =
         if verbose then L.stdout "visiting node %a with state %d@." Cfg.Node.pp n s;
         [s + 1], [s + 1]
       let proc_throws _ = DoesNotThrow
     end) in
-  let transitions = DFCount.run proc_desc 0 in
+  let transitions = DFCount.run tenv proc_desc 0 in
   let do_node node =
     match transitions node with
     | DFCount.Transition _ -> ()

infer/src/checkers/dataflow.mli

@@ -19,7 +19,7 @@ module type DFStateType = sig
   val join : t -> t -> t (** Join two states (the old one is the first parameter). *)
 
   (** Perform a state transition on a node. *)
-  val do_node : Cfg.Node.t -> t -> (t list) * (t list)
+  val do_node : Sil.tenv -> Cfg.Node.t -> t -> (t list) * (t list)
 
   val proc_throws : Procname.t -> throws (** Can proc throw an exception? *)
 end
@@ -34,7 +34,7 @@ module type DF = sig
   val join : state list -> state -> state
   (** Run the dataflow analysis on a procedure starting from the given state.
       Returns a function to lookup the results of the analysis on every node *)
-  val run : Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition)
+  val run : Sil.tenv -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition)
 end
 
 (** Functor to create an instance of a dataflow analysis. *)

infer/src/checkers/repeatedCallsChecker.ml

@@ -62,7 +62,7 @@ struct
   (** Check if the procedure performs an allocation operation.
       If [paths] is AllPaths, check if an allocation happens on all paths.
       If [paths] is SomePath, check if a path with an allocation exists. *)
-  let proc_performs_allocation pdesc paths : Location.t option =
+  let proc_performs_allocation tenv pdesc paths : Location.t option =
 
     let node_allocates node : Location.t option =
       let found = ref None in
@@ -90,7 +90,7 @@ struct
           | Some loc1, Some _ ->
               Some loc1 (* left priority *)
         let join = _join paths
-        let do_node node lo1 =
+        let do_node _ node lo1 =
           let lo2 = node_allocates node in
           let lo' = (* use left priority join to implement transfer function *)
             _join SomePath lo1 lo2 in
@@ -98,13 +98,13 @@ struct
         let proc_throws _ = Dataflow.DontKnow
       end) in
 
-    let transitions = DFAllocCheck.run pdesc None in
+    let transitions = DFAllocCheck.run tenv pdesc None in
     match transitions (Cfg.Procdesc.get_exit_node pdesc) with
     | DFAllocCheck.Transition (loc, _, _) -> loc
     | DFAllocCheck.Dead_state -> None
 
   (** Check repeated calls to the same procedure. *)
-  let check_instr get_proc_desc curr_pname curr_pdesc extension instr normalized_etl =
+  let check_instr tenv get_proc_desc curr_pname curr_pdesc extension instr normalized_etl =
 
     (** Arguments are not temporary variables. *)
     let arguments_not_temp args =
@@ -128,7 +128,7 @@ struct
           match get_old_call instr_normalized_args extension with
           | Some (Sil.Call (_, _, _, loc_old, _)) ->
               begin
-                match proc_performs_allocation proc_desc AllPaths with
+                match proc_performs_allocation tenv proc_desc AllPaths with
                 | Some alloc_loc ->
                     let description =
                       Printf.sprintf "call to %s seen before on line %d (may allocate at %s:%n)"

infer/src/checkers/sqlChecker.ml

@@ -11,7 +11,7 @@ module L = Logging
 
 
 (** Find SQL statements in string concatenations *)
-let callback_sql { Callbacks.proc_desc; proc_name } =
+let callback_sql { Callbacks.proc_desc; proc_name; tenv } =
   let verbose = false in
 
   (* Case insensitive SQL statement patterns *)
@@ -62,7 +62,7 @@ let callback_sql { Callbacks.proc_desc; proc_name } =
     | _ -> () in
 
   try
-    let const_map = ConstantPropagation.build_const_map proc_desc in
+    let const_map = ConstantPropagation.build_const_map tenv proc_desc in
     if verbose then L.stdout "Analyzing %a...\n@." Procname.pp proc_name;
     Cfg.Procdesc.iter_instrs (do_instr const_map) proc_desc
   with _ -> ()

infer/src/eradicate/eradicate.ml

@@ -69,7 +69,7 @@ struct
     | None -> ()
 
   let callback1
-      find_canonical_duplicate calls_this checks get_proc_desc idenv curr_pname
+      tenv find_canonical_duplicate calls_this checks get_proc_desc idenv curr_pname
       curr_pdesc annotated_signature linereader proc_loc
     : bool * Extension.extension TypeState.t option =
     let mk_pvar s = Sil.mk_pvar s curr_pname in
@@ -117,11 +117,11 @@ struct
         type t = Extension.extension TypeState.t
         let equal = TypeState.equal
         let join = TypeState.join Extension.ext
-        let do_node node typestate =
+        let do_node tenv node typestate =
           State.set_node node;
           let typestates_succ, typestates_exn =
             TypeCheck.typecheck_node
-              Extension.ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc
+              tenv Extension.ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc
               find_canonical_duplicate annotated_signature typestate node linereader in
           if trace then
             IList.iter (fun typestate_succ ->
@@ -135,7 +135,7 @@ struct
       end) in
     let initial_typestate = get_initial_typestate () in
     do_before_dataflow initial_typestate;
-    let transitions = DFTypeCheck.run curr_pdesc initial_typestate in
+    let transitions = DFTypeCheck.run tenv curr_pdesc initial_typestate in
     match transitions (Cfg.Procdesc.get_exit_node curr_pdesc) with
     | DFTypeCheck.Transition (final_typestate, _, _) ->
         do_after_dataflow find_canonical_duplicate final_typestate;
@@ -180,7 +180,7 @@ struct
             check_ret_type = [];
           }, ref false in
       callback1
-        find_canonical_duplicate calls_this' checks' get_proc_desc idenv_pn
+        tenv find_canonical_duplicate calls_this' checks' get_proc_desc idenv_pn
         pname pdesc ann_sig linereader loc in
 
     let module Initializers = struct
@@ -375,7 +375,7 @@ struct
   type extension = unit
   let ext =
     let empty = () in
-    let check_instr _ _ _ ext _ _ = ext in
+    let check_instr _ _ _ _ ext _ _ = ext in
     let join () () = () in
     let pp _ () = () in
     {

infer/src/eradicate/typeCheck.ml

@@ -236,7 +236,8 @@ let rec typecheck_expr
   | _ -> tr_default
 
 (** Typecheck an instruction. *)
-let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc curr_pname
+let typecheck_instr
+    tenv ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc curr_pname
     curr_pdesc find_canonical_duplicate annotated_signature instr_ref linereader typestate instr =
   (* let print_current_state () = *)
   (*   L.stdout "Current Typestate in node %a@\n%a@." *)
@@ -558,15 +559,42 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
         typestate
   | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _) when SymExec.function_is_builtin pn ->
       typestate (* skip othe builtins *)
-  | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags)
+  | Sil.Call
-    when Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname <> None ->
+      (ret_ids,
+       Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
+       etl_,
+       loc,
+       cflags)
+    ->
       Ondemand.analyze_proc_name ~propagate_exceptions:true curr_pdesc callee_pname;
       let callee_attributes =
         match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with
-        | Some proc_attributes -> proc_attributes
+        | Some proc_attributes ->
-        | None -> assert false in
+            proc_attributes
+        | None ->
+            let formals =
+              IList.mapi
+                (fun i (_, typ) ->
+                   let arg =
+                     if i = 0 &&
+                        not (Procname.java_is_static callee_pname)
+                     then "this"
+                     else Printf.sprintf "arg%d" i in
+                   (Mangled.from_string arg, typ))
+                etl_ in
+            let ret_typ_str = Procname.java_get_return_type callee_pname_java in
+            let ret_type =
+              match SymExec.lookup_java_typ_from_string tenv ret_typ_str with
+              | Sil.Tstruct _ as typ -> Sil.Tptr (typ, Sil.Pk_pointer)
+              | typ -> typ in
+            let proc_attributes =
+              { (ProcAttributes.default callee_pname Config.Java) with
+                ProcAttributes.formals;
+                ret_type;
+              } in
+            proc_attributes in
 
-      let etl = drop_unchecked_params calls_this callee_attributes _etl in
+      let etl = drop_unchecked_params calls_this callee_attributes etl_ in
       let call_params, typestate1 =
         let handle_et (e1, t1) (etl1, typestate1) =
           typecheck_expr_for_errors typestate e1 loc;
@@ -798,7 +826,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
                 let extension = TypeState.get_extension typestate1 in
                 let extension' =
                   ext.TypeState.check_instr
-                    get_proc_desc curr_pname curr_pdesc extension instr etl' in
+                    tenv get_proc_desc curr_pname curr_pdesc extension instr etl' in
                 TypeState.set_extension typestate1 extension'
               else typestate1 in
             let has_method pn name = match pn with
@@ -1043,7 +1071,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
 
 (** Typecheck the instructions in a cfg node. *)
 let typecheck_node
-    ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc
+    tenv ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc
     find_canonical_duplicate annotated_signature typestate node linereader =
 
   let instrs = Cfg.Node.get_instrs node in
@@ -1074,7 +1102,8 @@ let typecheck_node
     let instr_ref = (* keep unique instruction reference per-node *)
       TypeErr.InstrRef.gen instr_ref_gen in
     let instr' =
-      typecheck_instr ext calls_this checks node idenv get_proc_desc curr_pname curr_pdesc
+      typecheck_instr
+        tenv ext calls_this checks node idenv get_proc_desc curr_pname curr_pdesc
         find_canonical_duplicate annotated_signature instr_ref linereader typestate instr in
     handle_exceptions typestate instr;
     instr' in

infer/src/eradicate/typeCheck.mli

@@ -25,7 +25,7 @@ type checks =
   }
 
 val typecheck_node :
-  'a TypeState.ext ->
+  Sil.tenv -> 'a TypeState.ext ->
   bool ref -> checks -> Idenv.t ->
   get_proc_desc -> Procname.t -> Cfg.Procdesc.t ->
   find_canonical_duplicate -> Annotations.annotated_signature -> 'a TypeState.t ->

infer/src/eradicate/typeState.ml

@@ -23,7 +23,8 @@ type 'a ext =
   {
     empty : 'a; (** empty extension *)
     check_instr : (** check the extension for an instruction *)
-      get_proc_desc -> Procname.t -> Cfg.Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a;
+      Sil.tenv -> get_proc_desc -> Procname.t ->
+      Cfg.Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a;
     join : 'a -> 'a -> 'a; (** join two extensions *)
     pp : Format.formatter -> 'a -> unit (** pretty print an extension *)
   }

infer/src/eradicate/typeState.mli

@@ -19,7 +19,8 @@ type 'a ext =
   {
     empty : 'a; (** empty extension *)
     check_instr : (** check the extension for an instruction *)
-      get_proc_desc -> Procname.t -> Cfg.Procdesc.t ->'a -> Sil.instr -> parameters -> 'a;
+      Sil.tenv -> get_proc_desc -> Procname.t ->
+      Cfg.Procdesc.t ->'a -> Sil.instr -> parameters -> 'a;
     join : 'a -> 'a -> 'a; (** join two extensions *)
     pp : Format.formatter -> 'a -> unit (** pretty print an extension *)
   }

infer/src/java/jConfig.ml

@@ -146,7 +146,3 @@ let translate_checks = ref false
 
 (* Generate harness for Android code *)
 let create_harness = ref false
-
-(* Create a procedure description of callees *)
-let create_callee_procdesc =
-  Config.from_env_variable "INFER_CREATE_CALLEE_PDESC"

infer/src/java/jTrans.ml

@@ -551,11 +551,8 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
                 end in
     loop cn cn in
   let cn' = resolve_method context cn ms in
-  let cfg = JContext.get_cfg context in
   let tenv = JContext.get_tenv context in
   let program = JContext.get_program context in
-  if JConfig.create_callee_procdesc then
-    ignore (get_method_procdesc program cfg tenv cn' ms method_kind);
   let cf_virtual, cf_interface = match invoke_code with
     | I_Virtual -> (true, false)
     | I_Interface -> (true, true)