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