From d5e9b22e4101c7df97c2b0297e6065e20d73b534 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Fri, 5 May 2017 11:28:29 -0700 Subject: [PATCH] [infer][checkers] remove the code for the checkers that are not being run in prod Summary: While working on making the AI framework simpler to use, it become hard to change the shared API while keeping these unused checkers compiling, and even harder to keep their functionality since there is no tests for them. Also, these checkers are not useful as proof of concept since using the AI framework is the preferred way to write new kinds of analysis now. Reviewed By: sblackshear Differential Revision: D4999387 fbshipit-source-id: 497284b --- infer/src/checkers/checkDeadCode.ml | 118 ----- infer/src/checkers/checkDeadCode.mli | 13 - infer/src/checkers/checkTraceCallSequence.ml | 346 ------------ infer/src/checkers/checkTraceCallSequence.mli | 14 - infer/src/checkers/checkers.ml | 493 ------------------ infer/src/checkers/checkers.mli | 16 - infer/src/checkers/registerCheckers.ml | 17 +- infer/src/checkers/sqlChecker.ml | 74 --- infer/src/checkers/sqlChecker.mli | 12 - 9 files changed, 1 insertion(+), 1102 deletions(-) delete mode 100644 infer/src/checkers/checkDeadCode.ml delete mode 100644 infer/src/checkers/checkDeadCode.mli delete mode 100644 infer/src/checkers/checkTraceCallSequence.ml delete mode 100644 infer/src/checkers/checkTraceCallSequence.mli delete mode 100644 infer/src/checkers/sqlChecker.ml delete mode 100644 infer/src/checkers/sqlChecker.mli diff --git a/infer/src/checkers/checkDeadCode.ml b/infer/src/checkers/checkDeadCode.ml deleted file mode 100644 index f6b5fc8da..000000000 --- a/infer/src/checkers/checkDeadCode.ml +++ /dev/null @@ -1,118 +0,0 @@ -(* - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -module L = Logging -module F = Format -open Dataflow - -(** Simple check for dead code. *) - -let verbose = false - -module State = struct - type t = - { - visited : Procdesc.NodeSet.t; - } - - let initial = - { - visited = Procdesc.NodeSet.empty; - } - - let equal t1 t2 = - Procdesc.NodeSet.equal t1.visited t2.visited - - let join t1 t2 = - { - visited = Procdesc.NodeSet.union t1.visited t2.visited - } - - let add_visited node t = - { - visited = Procdesc.NodeSet.add node t.visited; - } - - let get_visited t = - t.visited - - let pp fmt t = - F.fprintf fmt "visited: %a" - (Pp.seq Procdesc.Node.pp) (Procdesc.NodeSet.elements t.visited) - - let num_visited t = - Procdesc.NodeSet.cardinal t.visited -end - -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)@." - Procdesc.Node.pp node - State.pp s'; - [s'], [s'] - - -(** Report an error. *) -let report_error tenv description pn pd loc = - if verbose then L.stderr "ERROR: %s@." description; - Checkers.ST.report_error tenv pn pd Localise.checkers_dead_code loc description - - -(** Check the final state at the end of the analysis. *) -let check_final_state tenv proc_name proc_desc final_s = - let proc_nodes = Procdesc.get_nodes proc_desc in - let tot_nodes = List.length proc_nodes in - let tot_visited = State.num_visited final_s in - if verbose then L.stderr "TOT nodes: %d (visited: %n)@." tot_nodes tot_visited; - if tot_nodes <> tot_visited then - begin - let not_visited = - List.filter - ~f:(fun n -> not (Procdesc.NodeSet.mem n (State.get_visited final_s))) - proc_nodes in - let do_node n = - let loc = Procdesc.Node.get_loc n in - let description = Format.sprintf "Node not visited: %d" (Procdesc.Node.get_id n :> int) in - let report = match Procdesc.Node.get_kind n with - | Procdesc.Node.Join_node -> false - | k when Procdesc.Node.equal_nodekind k Procdesc.Node.exn_sink_kind -> false - | _ -> true in - if report - then report_error tenv description proc_name proc_desc loc in - List.iter ~f:do_node not_visited - end - -(** Simple check for dead code. *) -let callback_check_dead_code { Callbacks.proc_desc; tenv; summary } = - let proc_name = Procdesc.get_proc_name proc_desc in - - let module DFDead = MakeDF(struct - type t = State.t - let equal = State.equal - let join = State.join - let do_node = do_node - let proc_throws _ = DontKnow - end) in - - let do_check () = - begin - if verbose then L.stderr "@.--@.PROC: %a@." Typ.Procname.pp proc_name; - let transitions = DFDead.run tenv proc_desc State.initial in - let exit_node = Procdesc.get_exit_node proc_desc in - match transitions exit_node with - | DFDead.Transition (pre_final_s, _, _) -> - let final_s = State.add_visited exit_node pre_final_s in - check_final_state tenv proc_name proc_desc final_s - | DFDead.Dead_state -> () - end in - - do_check (); - summary diff --git a/infer/src/checkers/checkDeadCode.mli b/infer/src/checkers/checkDeadCode.mli deleted file mode 100644 index 60adad47d..000000000 --- a/infer/src/checkers/checkDeadCode.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -(** Simple check for dead code. *) -val callback_check_dead_code: Callbacks.proc_callback_t diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml deleted file mode 100644 index fd9cbf29e..000000000 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ /dev/null @@ -1,346 +0,0 @@ -(* - * Copyright (c) 2016 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -module L = Logging -module F = Format -open Dataflow - -(** Check the sequence of calls to tracing APIs in a method (intraprocedural). *) - -let verbose = false - -let widening_threshold = 10 - - -(** Tracing methods of the form (package name, class name, begin name, end name). *) -let tracing_methods = - let for_testing = - [ - "", "TraceCallSequence", "begin", "end"; - "", "TraceCallSequence", "beginWrapper", "endWrapper"; - ] in - for_testing @ FbTraceCalls.tracing_methods - - -(** Boolean variables to be tracked. *) -let boolean_variables = - [ - "shouldTrace"; - ] - -(** Report a warning in the spec file of the procedure. *) -let report_warning tenv description pn pd loc = - if verbose then L.stderr "ERROR: %s@." description; - Checkers.ST.report_error tenv pn pd Localise.checkers_trace_calls_sequence loc description - - -(** Tracing APIs. *) -module APIs = struct - let method_match pn pkgname cname mname = - match pn with - | Typ.Procname.Java pn_java -> - String.equal (Typ.Procname.java_get_method pn_java) mname - && - (match pkgname with - | "" -> - String.equal (Typ.Procname.java_get_simple_class_name pn_java) cname - | _ -> - String.equal (Typ.Procname.java_get_class_name pn_java) (pkgname ^ "." ^ cname)) - | _ -> - false - let is_begin pn = - let filter (pkgname, cname, begin_name, _) = method_match pn pkgname cname begin_name in - List.exists ~f:filter tracing_methods - let is_end pn = - let filter (pkgname, cname, _, end_name) = method_match pn pkgname cname end_name in - List.exists ~f:filter tracing_methods - let is_begin_or_end pn = - is_begin pn || is_end pn -end - - -(** Environment for boolean variables. *) -module Env = struct - type t = bool String.Map.t [@@deriving compare] - let empty = String.Map.empty - let add key data map = String.Map.add ~key ~data map - let remove key map = String.Map.remove map key - let get map name = String.Map.find map name - let pp fmt map = - let pp_elem fmt (s, b) = F.fprintf fmt "%s:%b" s b in - let l = String.Map.to_alist map in - if l <> [] then F.fprintf fmt "%a" (Pp.seq pp_elem) l -end - -(** Element for the set domain: an integer (for pending traces), and an environment. *) -module Elem = struct - type t = int * Env.t [@@deriving compare] - let pp fmt (i, env) = F.fprintf fmt "(%d %a)" i Env.pp env - let zero = (0, Env.empty) - let is_consistent (i, _) = i >= 0 - let get_int (i, _) = i - let get_env (_, env) = env - let set_env (i, _) env' = (i, env') - let incr (i, env) = (i + 1, env) - let decr (i, env) = (i - 1, env) -end - - -module ElemSet = Caml.Set.Make(Elem) - - -module State = struct - (** Each number represents the difference between begin() and end() on some path. *) - type t = ElemSet.t - - let to_string n = - let pp_intset fmt s = - ElemSet.iter (fun d -> F.fprintf fmt "%a " Elem.pp d) s in - let pp fmt = - Format.fprintf fmt "{%a}" pp_intset n in - F.asprintf "%t" pp - - (** Initial balanced state with empty environment. *) - let balanced = ElemSet.singleton Elem.zero - - (** State is balanced. *) - let is_balanced s = - ElemSet.for_all (fun elem -> Int.equal (Elem.get_int elem) 0) s - - let equal = ElemSet.equal - - let has_zero s = ElemSet.exists (fun elem -> Int.equal (Elem.get_int elem) 0) s - - (** Map a function to the elements of the set, and filter out inconsistencies. *) - let map2 (f : Elem.t -> Elem.t list) (s : t) : t = - let l = ElemSet.elements s in - let l' = List.filter ~f:Elem.is_consistent (List.concat_map ~f:f l) in - List.fold_right ~f:ElemSet.add l' ~init:ElemSet.empty - - let map (f : Elem.t -> Elem.t) s = - map2 (fun elem -> [f elem]) s - - (** Increment the number of begin/start. *) - let incr s = - map Elem.incr s - - (** Decrement the number of begin/start. *) - let decr s = - map Elem.decr s - - (** Max value of the set. *) - let max s = - ElemSet.max_elt s - - (** Prune the value of name w.r.t. boolean b. *) - let prune s name b = - let f elem = - let env = Elem.get_env elem in - match Env.get env name with - | None -> - let env' = Env.add name b env in - let elem' = Elem.set_env elem env' in - [elem'] - | Some b' -> - if Bool.equal b b' then [elem] - else [] in - map2 f s - - (** Set name to the given bool, or nondeterministic if None. *) - let set_bool s name b_opt = - let f elem = - let env = Elem.get_env elem in - let env' = match b_opt with - | None -> Env.remove name env - | Some b -> Env.add name b env in - Elem.set_env elem env' in - map f s - - (** Stop growing sets if they go beyond a threshold. *) - let widening s_before s_after = - if ElemSet.cardinal s_after <= widening_threshold - then s_after - else s_before - - (** Join two states and perform widening if necessary. *) - let join s1 s2 = - let s' = ElemSet.union s1 s2 in - let s'' = widening s1 s' in - if verbose then L.stderr " join %s %s --> %s@." (to_string s1) (to_string s2) (to_string s''); - s'' -end - -(** Abstract domain for automata whose state transitions are triggered by calls. *) -module Automaton = struct - - (** Transfer function for a procedure call. *) - let do_call tenv caller_pn caller_pd callee_pn (s : State.t) loc : State.t = - let method_name () = match callee_pn with - | Typ.Procname.Java pname_java -> - Typ.Procname.java_get_method pname_java - | _ -> - Typ.Procname.to_simplified_string callee_pn in - if APIs.is_begin callee_pn then - begin - if verbose then L.stderr " calling %s@." (method_name ()); - State.incr s - end - else if APIs.is_end callee_pn then - begin - if verbose then L.stderr " calling %s@." (method_name ()); - if State.has_zero s then report_warning tenv "too many end/stop" caller_pn caller_pd loc; - State.decr s - end - else s - - (** Transfer function for an instruction. *) - let do_instr tenv pn pd (instr : Sil.instr) (state : State.t) : State.t = - match instr with - | Sil.Call (_, Exp.Const (Const.Cfun callee_pn), _, loc, _) -> - do_call tenv pn pd callee_pn state loc - | _ -> state - - (** Check if the final state contains any numbers other than zero (balanced). *) - let check_final_state tenv pn pd exit_node (s : State.t) : unit = - if verbose then L.stderr "@.Final: %s@." (State.to_string s); - if not (State.is_balanced s) then - begin - let description = Printf.sprintf "%d missing end/stop" (Elem.get_int (State.max s)) in - let loc = Procdesc.Node.get_loc exit_node in - report_warning tenv description pn pd loc - end - -end - - -(** Abstract domain to track the value of specific boolean variables. *) -module BooleanVars = struct - - (** Check if the expression exp is one of the listed boolean variables. *) - let exp_boolean_var exp = match exp with - | Exp.Lvar pvar when Pvar.is_local pvar -> - let name = Mangled.to_string (Pvar.get_name pvar) in - if List.mem ~equal:String.equal boolean_variables name - then Some name - else None - | _ -> None - - (** Transfer function for an instruction. *) - let do_instr _ _ idenv (instr : Sil.instr) (state : State.t) : State.t = - (* Normalize a boolean condition. *) - let normalize_condition cond_e = - match cond_e with - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) -> - Exp.BinOp (Binop.Ne, e1, e2) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne, e1, e2), _) -> - Exp.BinOp (Binop.Eq, e1, e2) - | _ -> cond_e in - - (* Normalize an instruction. *) - let normalize_instr = function - | Sil.Prune (cond_e, loc, tb, ik) -> - let cond_e' = normalize_condition cond_e in - Sil.Prune (cond_e', loc, tb, ik) - | instr -> instr in - - match normalize_instr instr with - | Sil.Prune (Exp.BinOp (Binop.Eq, _cond_e, Exp.Const (Const.Cint i)), _, _, _) - when IntLit.iszero i -> - let cond_e = Idenv.expand_expr idenv _cond_e in - let state' = match exp_boolean_var cond_e with - | Some name -> - if verbose then L.stderr " prune false on %s@." name; - State.prune state name false - | None -> state in - state' - | Sil.Prune (Exp.BinOp (Binop.Ne, _cond_e, Exp.Const (Const.Cint i)), _, _, _) - when IntLit.iszero i -> - let cond_e = Idenv.expand_expr idenv _cond_e in - let state' = match exp_boolean_var cond_e with - | Some name -> - if verbose then L.stderr " prune true on %s@." name; - State.prune state name true - | None -> state in - state' - | Sil.Store (_e1, _, e2, _) -> - let e1 = Idenv.expand_expr idenv _e1 in - let state' = match exp_boolean_var e1 with - | Some name -> - let b_opt = match e2 with - | Exp.Const (Const.Cint i) -> Some (not (IntLit.iszero i)) - | _ -> None in - if verbose then - begin - let b_str = match b_opt with - | None -> "nondet" - | Some b -> string_of_bool b in - L.stderr " setting %s to %s@." name b_str - end; - State.set_bool state name b_opt - | None -> state in - state' - | _ -> state - - let check_final_state _ _ _ _ = - () - -end - - -(** State transformation for a cfg node. *) -let do_node tenv pn pd idenv _ node (s : State.t) : (State.t list) * (State.t list) = - if verbose then L.stderr "N:%d S:%s@." (Procdesc.Node.get_id node :> int) (State.to_string s); - - let curr_state = ref s in - - let do_instr instr : unit = - let state1 = Automaton.do_instr tenv pn pd instr !curr_state in - let state2 = BooleanVars.do_instr pn pd idenv instr state1 in - curr_state := state2 in - - List.iter ~f:do_instr (Procdesc.Node.get_instrs node); - [!curr_state], [!curr_state] - -(** Check the final state at the end of the analysis. *) -let check_final_state tenv proc_name proc_desc exit_node final_s = - Automaton.check_final_state tenv proc_name proc_desc exit_node final_s; - BooleanVars.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; idenv; tenv; summary } = - let proc_name = Procdesc.get_proc_name proc_desc in - - let module DFTrace = MakeDF(struct - type t = State.t - let equal = State.equal - let join = State.join - let do_node = do_node tenv proc_name proc_desc idenv - let proc_throws pn = - if APIs.is_begin_or_end pn - then DoesNotThrow (* assume the tracing function do not throw *) - else DontKnow - end) in - - let do_check () = - begin - if verbose then L.stderr "@.--@.PROC: %a@." Typ.Procname.pp proc_name; - let transitions = DFTrace.run tenv proc_desc State.balanced in - let exit_node = Procdesc.get_exit_node proc_desc in - match transitions exit_node with - | DFTrace.Transition (final_s, _, _) -> - check_final_state tenv proc_name proc_desc exit_node final_s - | DFTrace.Dead_state -> () - end in - - if not (APIs.is_begin_or_end proc_name) then do_check (); - summary diff --git a/infer/src/checkers/checkTraceCallSequence.mli b/infer/src/checkers/checkTraceCallSequence.mli deleted file mode 100644 index c33cf0047..000000000 --- a/infer/src/checkers/checkTraceCallSequence.mli +++ /dev/null @@ -1,14 +0,0 @@ -(* - * Copyright (c) 2016 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -(** Check the sequence of calls to tracing APIs in a method (intraprocedural). *) - -val callback_check_trace_call_sequence: Callbacks.proc_callback_t diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index b9fbc5a48..f06ddebcd 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -32,28 +32,6 @@ end (* PP *) (** State that persists in the .specs files. *) module ST = struct - let add summary key value = - ProcAttributes.proc_flags_add summary.Specs.attributes.ProcAttributes.proc_flags key value - - let pname_add proc_name key value = - let summary = Specs.get_summary_unsafe "ST.pname_add" proc_name in - add summary key value - - let files_open = ref Typ.Procname.Set.empty - - let pname_find proc_name key = - if Typ.Procname.Set.mem proc_name !files_open then - let summary = Specs.get_summary_unsafe "ST.pname_find" proc_name in - ProcAttributes.proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key - else begin - match Specs.get_summary proc_name with - | None -> raise Not_found - | Some summary -> - begin - files_open := Typ.Procname.Set.add proc_name !files_open; - ProcAttributes.proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key - end - end let report_error tenv proc_name @@ -144,474 +122,3 @@ module ST = struct Reporting.log_error proc_name ~loc ~ltr:trace exn end end - -let report_calls_and_accesses tenv callback proc_desc instr = - let proc_name = Procdesc.get_proc_name proc_desc in - let callee = Typ.Procname.to_string proc_name in - match PatternMatch.get_java_field_access_signature instr with - | Some (bt, fn, ft) -> - ST.report_error tenv - proc_name - proc_desc - callback - (Procdesc.get_loc proc_desc) - (Format.sprintf "field access %s.%s:%s in %s@." bt fn ft callee) - | None -> - match PatternMatch.get_java_method_call_formal_signature instr with - | Some (bt, fn, _, rt) -> - ST.report_error tenv - proc_name - proc_desc - callback - (Procdesc.get_loc proc_desc) - (Format.sprintf "method call %s.%s(%s):%s in %s@." bt fn "..." rt callee) - | None -> () - -(** Report all field accesses and method calls of a procedure. *) -let callback_check_access { Callbacks.tenv; proc_desc; summary } = - Procdesc.iter_instrs - (fun _ instr -> report_calls_and_accesses tenv Localise.proc_callback proc_desc instr) - proc_desc; - summary - - -(** Report all field accesses and method calls of a class. *) -let callback_check_cluster_access exe_env all_procs get_proc_desc _ = - List.iter ~f:(fun proc_name -> - match get_proc_desc proc_name with - | Some proc_desc -> - let tenv = Exe_env.get_tenv exe_env proc_name in - Procdesc.iter_instrs - (fun _ instr -> - report_calls_and_accesses tenv Localise.cluster_callback proc_desc instr) - proc_desc - | _ -> - () - ) all_procs - -(** Looks for writeToParcel methods and checks whether read is in reverse *) -let callback_check_write_to_parcel_java - pname_java { Callbacks.tenv; proc_desc; idenv; get_proc_desc } = - let proc_name = Procdesc.get_proc_name proc_desc in - let verbose = ref false in - - let is_write_to_parcel this_expr this_type = - let method_match () = - String.equal (Typ.Procname.java_get_method pname_java) "writeToParcel" in - let expr_match () = Exp.is_this this_expr in - let type_match () = - let class_name = Typ.Name.Java.from_string "android.os.Parcelable" in - match this_type.Typ.desc with - | Typ.Tptr ({desc=Tstruct name}, _) | Tstruct name -> - PatternMatch.is_immediate_subtype tenv name class_name - | _ -> false in - method_match () && expr_match () && type_match () in - - let is_parcel_constructor proc_name = - Typ.Procname.is_constructor proc_name && - PatternMatch.has_formal_method_argument_type_names - proc_desc pname_java ["android.os.Parcel"] in - - let parcel_constructors tenv typ = - match typ.Typ.desc with - | Typ.Tptr ({desc=Tstruct name}, _) -> ( - match Tenv.lookup tenv name with - | Some { methods } -> List.filter ~f:is_parcel_constructor methods - | None -> [] - ) - | _ -> [] in - - let check r_desc w_desc = - - let is_serialization_node node = - match Procdesc.Node.get_callees node with - | [] -> false - | [Typ.Procname.Java pname_java] -> - let class_name = Typ.Procname.java_get_class_name pname_java in - let method_name = Typ.Procname.java_get_method pname_java in - (try - String.equal class_name "android.os.Parcel" && - (String.equal (String.sub method_name ~pos:0 ~len:5) "write" - || - String.equal (String.sub method_name ~pos:0 ~len:4) "read") - with Invalid_argument _ -> false) - | _ -> assert false in - - let is_inverse rc_ wc_ = match rc_, wc_ with - | Typ.Procname.Java rc, Typ.Procname.Java wc -> - let rn = Typ.Procname.java_get_method rc in - let wn = Typ.Procname.java_get_method wc in - let postfix_length = String.length wn - 5 in (* covers writeList <-> readArrayList etc. *) - (try - String.equal - (String.sub rn ~pos:(String.length rn - postfix_length) ~len:postfix_length) - (String.sub wn ~pos:5 ~len:postfix_length) - with Invalid_argument _ -> false) - | _ -> - false in - - let node_to_call_desc node = - match Procdesc.Node.get_callees node with - | [desc] -> desc - | _ -> assert false in - - let r_call_descs = - List.map ~f:node_to_call_desc - (List.filter ~f:is_serialization_node - (Procdesc.get_sliced_slope r_desc is_serialization_node)) in - let w_call_descs = - List.map ~f:node_to_call_desc - (List.filter ~f:is_serialization_node - (Procdesc.get_sliced_slope w_desc is_serialization_node)) in - - let rec check_match = function - | rc:: rcs, wc:: wcs -> - if not (is_inverse rc wc) then - L.stdout "Serialization missmatch in %a for %a and %a@." - Typ.Procname.pp proc_name - Typ.Procname.pp rc - Typ.Procname.pp wc - else - check_match (rcs, wcs) - | rc:: _, [] -> - L.stdout "Missing write in %a: for %a@." - Typ.Procname.pp proc_name Typ.Procname.pp rc - | _, wc:: _ -> - L.stdout "Missing read in %a: for %a@." - Typ.Procname.pp proc_name Typ.Procname.pp wc - | _ -> - () in - - check_match (r_call_descs, w_call_descs) in - - let do_instr _ instr = match instr with - | Sil.Call (_, Exp.Const (Const.Cfun _), (_this_exp, this_type):: _, _, _) -> - let this_exp = Idenv.expand_expr idenv _this_exp in - if is_write_to_parcel this_exp this_type then begin - if !verbose then - L.stdout "Serialization check for %a@." - Typ.Procname.pp proc_name; - try - match parcel_constructors tenv this_type with - | x :: _ -> - (match get_proc_desc x with - | Some x_proc_desc -> check x_proc_desc proc_desc - | None -> raise Not_found) - | _ -> - L.stdout "No parcel constructor found for %a@." - Typ.Procname.pp proc_name - with Not_found -> - if !verbose then L.stdout "Methods not available@." - end - | _ -> () in - Procdesc.iter_instrs do_instr proc_desc - -(** Looks for writeToParcel methods and checks whether read is in reverse *) -let callback_check_write_to_parcel ({ Callbacks.summary } as args) = - begin - match Specs.get_proc_name summary with - | Typ.Procname.Java pname_java -> - callback_check_write_to_parcel_java pname_java args - | _ -> () - end; - summary - -(** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *) -let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; summary } = - let proc_name = Procdesc.get_proc_name proc_desc in - let verbose = ref false in - - let class_formal_names = lazy ( - let formals = Procdesc.get_formals proc_desc in - let class_formals = - let is_class_type (p, typ) = - match typ.Typ.desc with - | Typ.Tptr _ when String.equal (Mangled.to_string p) "this" -> - false (* no need to null check 'this' *) - | Typ.Tstruct _ -> true - | Typ.Tptr ({desc=Tstruct _}, _) -> true - | _ -> false in - List.filter ~f:is_class_type formals in - List.map ~f:fst class_formals) in - let equal_formal_param exp formal_name = match exp with - | Exp.Lvar pvar -> - let name = Pvar.get_name pvar in - Mangled.equal name formal_name - | _ -> false in - - let is_formal_param exp = - List.exists ~f:(equal_formal_param exp) (Lazy.force class_formal_names) in - - let is_nullcheck pn = match pn with - | Typ.Procname.Java pn_java -> - PatternMatch.java_proc_name_with_class_method - pn_java "com.google.common.base.Preconditions" "checkNotNull" - | _ -> - false in - - let checks_to_formals = ref Exp.Set.empty in - - let handle_check_of_formal e = - let repeated = Exp.Set.mem e !checks_to_formals in - if repeated && !verbose then L.stdout "Repeated Null Check of Formal: %a@." Exp.pp e - else begin - checks_to_formals := Exp.Set.add e !checks_to_formals; - if !verbose then L.stdout "Null Check of Formal: %a@." Exp.pp e - end in - - let summary_checks_of_formals () = - let formal_names = Lazy.force class_formal_names in - let nchecks = Exp.Set.cardinal !checks_to_formals in - let nformals = List.length formal_names in - if (nchecks > 0 && nchecks < nformals) then - begin - let was_not_found formal_name = - not (Exp.Set.exists (fun exp -> equal_formal_param exp formal_name) !checks_to_formals) in - let missing = List.filter ~f:was_not_found formal_names in - let loc = Procdesc.get_loc proc_desc in - let pp_file_loc fmt () = - F.fprintf fmt "%a:%d" SourceFile.pp loc.Location.file loc.Location.line in - L.stdout "Null Checks of Formal Parameters: "; - L.stdout "%d out of %d parameters checked (missing checks on: %a)[%a]@." - nchecks nformals (Pp.seq Mangled.pp) missing pp_file_loc (); - - let linereader = Printer.LineReader.create () in - L.stdout "%a@." (PP.pp_loc_range linereader 10 10) loc - end in - - let do_instr _ instr = match instr with - | Sil.Call (_, Exp.Const (Const.Cfun pn), (_arg1, _):: _, _, _) when is_nullcheck pn -> - let arg1 = Idenv.expand_expr idenv _arg1 in - if is_formal_param arg1 then handle_check_of_formal arg1; - if !verbose then - (match proc_name with - | Typ.Procname.Java pname_java -> - L.stdout "call in %s %s: %a with first arg: %a@." - (Typ.Procname.java_get_class_name pname_java) - (Typ.Procname.java_get_method pname_java) - (Sil.pp_instr Pp.text) instr - Exp.pp arg1 - | _ -> - ()) - | _ -> () in - Procdesc.iter_instrs do_instr proc_desc; - summary_checks_of_formals (); - summary - -(** Test persistent state. *) -let callback_test_state { Callbacks.summary } = - let proc_name = Specs.get_proc_name summary in - ST.pname_add proc_name "somekey" "somevalue"; - summary - -(** Check the uses of VisibleForTesting *) -let callback_checkVisibleForTesting { Callbacks.proc_desc; summary } = - if Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting then - begin - let loc = Procdesc.get_loc proc_desc in - let linereader = Printer.LineReader.create () in - L.stdout "%a@." (PP.pp_loc_range linereader 10 10) loc - end; - summary - -(** Check for readValue and readValueAs json deserialization *) -let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; summary } = - let proc_name = Procdesc.get_proc_name proc_desc in - let verbose = true in - - let ret_const_key = "return_const" in - - let reverse_find_instr f node = - (* this is not really sound but for the moment a sufficient approximation *) - let has_instr node = - List.exists ~f (Procdesc.Node.get_instrs node) in - let preds = - Procdesc.Node.get_generated_slope - node - (fun n -> Procdesc.Node.get_sliced_preds n has_instr) in - let instrs = - List.concat - (List.map ~f:(fun n -> List.rev (Procdesc.Node.get_instrs n)) preds) in - List.find ~f instrs in - - let get_return_const proc_name' = - try - ST.pname_find proc_name' ret_const_key - with Not_found -> - match get_proc_desc proc_name' with - Some proc_desc' -> - let is_return_instr = function - | Sil.Store (Exp.Lvar p, _, _, _) - when Pvar.equal p (Procdesc.get_ret_var proc_desc') -> true - | _ -> false in - (match reverse_find_instr is_return_instr (Procdesc.get_exit_node proc_desc') with - | Some (Sil.Store (_, _, Exp.Const (Const.Cclass n), _)) -> Ident.name_to_string n - | _ -> "<" ^ (Typ.Procname.to_string proc_name') ^ ">") - | None -> "?" in - - let get_actual_arguments node instr = match instr with - | Sil.Call (_, Exp.Const (Const.Cfun _), _:: args, _, _) -> - (try - let find_const exp = - let expanded = Idenv.expand_expr idenv exp in - match expanded with - | Exp.Const (Const.Cclass n) -> Ident.name_to_string n - | Exp.Lvar _ -> ( - let is_call_instr set call = match set, call with - | Sil.Store (_, _, Exp.Var (i1), _), Sil.Call (Some (i2, _), _, _, _, _) - when Ident.equal i1 i2 -> true - | _ -> false in - let is_set_instr = function - | Sil.Store (e1, _, _, _) when Exp.equal expanded e1 -> true - | _ -> false in - match reverse_find_instr is_set_instr node with - (* Look for ivar := tmp *) - | Some s -> ( - match reverse_find_instr (is_call_instr s) node with - (* Look for tmp := foo() *) - | Some (Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _)) -> - get_return_const pn - | _ -> "?") - | _ -> "?") - | _ -> "?" in - let arg_name (exp, _) = find_const exp in - Some (List.map ~f:arg_name args) - with _ -> None) - | _ -> None in - - let process_result instr result = - if verbose then ( - let linereader = Printer.LineReader.create () in - L.stdout "%a@." (PP.pp_loc_range linereader 2 2) (Sil.instr_get_loc instr); - ); - match result with - | str when (Str.string_match (Str.regexp "<\\(.*\\)>") str 0) -> ( - let missing_proc_name = Str.matched_group 1 str in - L.stdout "Deserialization of %s requires 2nd phase: " str; - L.stdout "missing: %s@." missing_proc_name) - | "?" -> L.stdout "Unable to resolve deserialization\n\n@." - | _ -> L.stdout "Deserialization of %s\n\n@." result in - - let do_instr node instr = - match PatternMatch.get_java_method_call_formal_signature instr with - | Some (_, "readValue", _, _) -> ( - match get_actual_arguments node instr with - | Some [_; cl] -> process_result instr cl - | _ -> process_result instr "?") - | Some (_, "readValueAs", _, _) -> ( - match get_actual_arguments node instr with - | Some [cl] -> process_result instr cl - | _ -> process_result instr "?") - | _ -> () in - - let store_return () = - let ret_const = get_return_const proc_name in - ST.pname_add proc_name ret_const_key ret_const in - - store_return (); - Procdesc.iter_instrs do_instr proc_desc; - summary - -(** Check field accesses. *) -let callback_check_field_access { Callbacks.proc_desc; summary } = - let rec do_exp is_read = function - | Exp.Var _ -> () - | Exp.UnOp (_, e, _) -> - do_exp is_read e - | Exp.BinOp (_, e1, e2) -> - do_exp is_read e1; - do_exp is_read e2 - | Exp.Exn _ -> () - | Exp.Closure _ -> () - | Exp.Const _ -> () - | Exp.Cast (_, e) -> - do_exp is_read e - | Exp.Lvar _ -> () - | Exp.Lfield (e, fn, _) -> - if not (Fieldname.java_is_outer_instance fn) then - L.stdout "field %s %s@." (Fieldname.to_string fn) (if is_read then "reading" else "writing"); - do_exp is_read e - | Exp.Lindex (e1, e2) -> - do_exp is_read e1; - do_exp is_read e2 - | Exp.Sizeof _ -> () in - let do_read_exp = do_exp true in - let do_write_exp = do_exp false in - let do_instr _ = function - | Sil.Load (_, e, _, _) -> - do_read_exp e - | Sil.Store (e1, _, e2, _) -> - do_write_exp e1; - do_read_exp e2 - | Sil.Prune (e, _, _, _) -> - do_read_exp e - | Sil.Call (_, e, etl, _, _) -> - do_read_exp e; - List.iter ~f:(fun (e, _) -> do_read_exp e) etl - | Sil.Nullify _ - | Sil.Abstract _ - | Sil.Remove_temps _ - | Sil.Declare_locals _ -> - () in - Procdesc.iter_instrs do_instr proc_desc; - summary - -(** Print c method calls. *) -let callback_print_c_method_calls { Callbacks.tenv; proc_desc; summary } = - let proc_name = Procdesc.get_proc_name proc_desc in - let do_instr node = function - | Sil.Call (_, Exp.Const (Const.Cfun pn), (e, _):: _, loc, _) - when Typ.Procname.is_c_method pn -> - let receiver = match Errdesc.exp_rv_dexp tenv node e with - | Some de -> DecompiledExp.to_string de - | None -> "?" in - let description = - Printf.sprintf "['%s' %s]" receiver (Typ.Procname.to_string pn) in - ST.report_error tenv - proc_name - proc_desc - Localise.checkers_print_objc_method_calls - loc - description - | Sil.Call (_, Exp.Const (Const.Cfun pn), _, loc, _) -> - let description = - Printf.sprintf "call to %s" (Typ.Procname.to_string pn) in - ST.report_error tenv - proc_name - proc_desc - Localise.checkers_print_c_call - loc - description - | _ -> () in - Procdesc.iter_instrs do_instr proc_desc; - summary - -(** Print access to globals. *) -let callback_print_access_to_globals { Callbacks.tenv; proc_desc; summary } = - let proc_name = Procdesc.get_proc_name proc_desc in - let do_pvar is_read pvar loc = - let description = - Printf.sprintf "%s of global %s" - (if is_read then "read" else "write") - (Pvar.to_string pvar) in - ST.report_error tenv - proc_name - proc_desc - Localise.checkers_access_global - loc - description in - let rec get_global_var = function - | Exp.Lvar pvar when Pvar.is_global pvar -> - Some pvar - | Exp.Lfield (e, _, _) -> - get_global_var e - | _ -> - None in - let do_instr _ = function - | Sil.Load (_, e, _, loc) when get_global_var e <> None -> - Option.iter ~f:(fun pvar -> do_pvar true pvar loc) (get_global_var e) - | Sil.Store (e, _, _, loc) when get_global_var e <> None -> - Option.iter ~f:(fun pvar -> do_pvar false pvar loc) (get_global_var e) - | _ -> () in - Procdesc.iter_instrs do_instr proc_desc; - summary diff --git a/infer/src/checkers/checkers.mli b/infer/src/checkers/checkers.mli index e67e131dc..7250a784a 100644 --- a/infer/src/checkers/checkers.mli +++ b/infer/src/checkers/checkers.mli @@ -14,11 +14,6 @@ open! IStd (** State that persists in the .specs files. *) module ST : sig - (** Add a key/value pair. *) - val pname_add : Typ.Procname.t -> string -> string -> unit - - (** Find the value associated to the key. Raise Not_found if it does not exist. *) - val pname_find: Typ.Procname.t -> string -> string (** Report an error. *) val report_error: @@ -42,14 +37,3 @@ module PP : sig and [nafter] lines after [loc] *) val pp_loc_range : Printer.LineReader.t -> int -> int -> Format.formatter -> Location.t -> unit end (* PP *) - -val callback_check_access : Callbacks.proc_callback_t -val callback_check_cluster_access : Callbacks.cluster_callback_t -val callback_monitor_nullcheck : Callbacks.proc_callback_t -val callback_test_state : Callbacks.proc_callback_t -val callback_checkVisibleForTesting : Callbacks.proc_callback_t -val callback_check_write_to_parcel : Callbacks.proc_callback_t -val callback_find_deserialization : Callbacks.proc_callback_t -val callback_check_field_access : Callbacks.proc_callback_t -val callback_print_c_method_calls : Callbacks.proc_callback_t -val callback_print_access_to_globals : Callbacks.proc_callback_t diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 81def7dbd..934609692 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -20,20 +20,10 @@ let active_procedure_checkers () = let java_checkers = let l = [ - Checkers.callback_check_access, false; - Checkers.callback_monitor_nullcheck, false; - Checkers.callback_test_state , false; - Checkers.callback_checkVisibleForTesting, false; - Checkers.callback_check_write_to_parcel, false; - Checkers.callback_find_deserialization, false; - CheckTraceCallSequence.callback_check_trace_call_sequence, false; - Dataflow.callback_test_dataflow, false; FragmentRetainsViewChecker.callback_fragment_retains_view, Config.checkers_enabled; - SqlChecker.callback_sql, false; Eradicate.callback_eradicate, Config.eradicate; BoundedCallTree.checker, Config.crashcontext; JavaTaintAnalysis.checker, Config.quandary; - Checkers.callback_check_field_access, false; ImmutableChecker.callback_check_immutable_cast, Config.checkers_enabled; RepeatedCallsChecker.callback_check_repeated_calls, Config.checkers_repeated_calls; PrintfArgs.callback_printf_args, Config.checkers_enabled; @@ -47,9 +37,6 @@ let active_procedure_checkers () = let c_cpp_checkers = let l = [ - Checkers.callback_print_c_method_calls, false; - CheckDeadCode.callback_check_dead_code, false; - Checkers.callback_print_access_to_globals, false; ClangTaintAnalysis.checker, Config.quandary; Siof.checker, Config.siof; ThreadSafety.analyze_procedure, Config.threadsafety; @@ -61,9 +48,7 @@ let active_procedure_checkers () = java_checkers @ c_cpp_checkers let active_cluster_checkers () = - [(Checkers.callback_check_cluster_access, false, Some Config.Java); - (ThreadSafety.file_analysis, Config.threadsafety || Config.checkers_enabled, Some Config.Java) - ] + [(ThreadSafety.file_analysis, Config.threadsafety || Config.checkers_enabled, Some Config.Java)] let register () = let register registry (callback, active, language_opt) = diff --git a/infer/src/checkers/sqlChecker.ml b/infer/src/checkers/sqlChecker.ml deleted file mode 100644 index 630d0b5d0..000000000 --- a/infer/src/checkers/sqlChecker.ml +++ /dev/null @@ -1,74 +0,0 @@ -(* - * Copyright (c) 2014 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -module L = Logging - - -(** Find SQL statements in string concatenations *) -let callback_sql { Callbacks.proc_desc; tenv; summary } : Specs.summary = - let proc_name = Procdesc.get_proc_name proc_desc in - let verbose = false in - - (* Case insensitive SQL statement patterns *) - let sql_start = - let _sql_start = [ - "select.*from.*"; - "insert into.*"; - "update .* set.*"; - "delete .* from.*"; - ] in - List.map ~f:Str.regexp_case_fold _sql_start in - - (* Check for SQL string concatenations *) - let do_instr const_map node instr = - let do_call pn_java i1 i2 l = - if String.equal (Typ.Procname.java_get_class_name pn_java) "java.lang.StringBuilder" - && String.equal (Typ.Procname.java_get_method pn_java) "append" - then - begin - let rvar1 = Exp.Var i1 in - let rvar2 = Exp.Var i2 in - begin - let matches s r = Str.string_match r s 0 in - match const_map node rvar1, const_map node rvar2 with - | Some (Const.Cstr ""), Some (Const.Cstr s2) -> - if List.exists ~f:(matches s2) sql_start then - begin - L.stdout - "%s%s@." - "Possible SQL query using string concatenation. " - "Please consider using a prepared statement instead."; - let linereader = Printer.LineReader.create () in - L.stdout "%a@." (Checkers.PP.pp_loc_range linereader 2 2) l - end - | _ -> () - end - end in - - match instr with - | Sil.Call (_, Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: (Exp.Var i2, _):: [], l, _) -> - begin - match pn with - | Typ.Procname.Java pn_java -> - do_call pn_java i1 i2 l - | _ -> - () - end - | _ -> () in - - begin - try - let const_map = ConstantPropagation.build_const_map tenv proc_desc in - if verbose then L.stdout "Analyzing %a...\n@." Typ.Procname.pp proc_name; - Procdesc.iter_instrs (do_instr const_map) proc_desc - with _ -> () - end; - summary diff --git a/infer/src/checkers/sqlChecker.mli b/infer/src/checkers/sqlChecker.mli deleted file mode 100644 index 6474fab0a..000000000 --- a/infer/src/checkers/sqlChecker.mli +++ /dev/null @@ -1,12 +0,0 @@ -(* - * Copyright (c) 2014 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - *) - -open! IStd - -val callback_sql : Callbacks.proc_callback_t