diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index ff2cac7f0..9f9adb39c 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -340,7 +340,6 @@ let process_cluster_cmdline fname = let () = print_prolog (); RegisterCheckers.register (); - Facebook.register_checkers (); if !allow_specs_cleanup = true && !cluster_cmdline = None then DB.Results_dir.clean_specs_dir (); diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml new file mode 100644 index 000000000..4f3081045 --- /dev/null +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -0,0 +1,337 @@ +(* + * 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. + *) + +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 description pn pd loc = + if verbose then L.stderr "ERROR: %s@." description; + Checkers.ST.report_error pn pd "CHECKERS_TRACE_CALLS_SEQUENCE" loc description + + +(** Tracing APIs. *) +module APIs = struct + let method_match pn pkgname cname mname = + Procname.is_java pn && + Procname.java_get_method pn = mname && + (match pkgname with + | "" -> Procname.java_get_simple_class pn = cname + | _ -> Procname.java_get_class pn = pkgname ^ "." ^ cname) + let is_begin pn = + let filter (pkgname, cname, begin_name, _) = method_match pn pkgname cname begin_name in + IList.exists filter tracing_methods + let is_end pn = + let filter (pkgname, cname, _, end_name) = method_match pn pkgname cname end_name in + IList.exists 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 StringMap.t + let empty = StringMap.empty + let compare = StringMap.compare bool_compare + let add = StringMap.add + let remove = StringMap.remove + let get map name = + try Some (StringMap.find name map) + with Not_found -> None + let pp fmt map = + let pp_elem fmt (s, b) = F.fprintf fmt "%s:%b" s b in + let l = StringMap.bindings 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 + let compare (i1, env1) (i2, env2) = + let n = int_compare i1 i2 in + if n <> 0 then n else Env.compare env1 env2 + 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 = 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 + pp_to_string 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 -> Elem.get_int elem = 0) s + + let equal = ElemSet.equal + + let has_zero s = ElemSet.exists (fun elem -> 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' = IList.filter Elem.is_consistent (IList.flatten (IList.map f l)) in + IList.fold_right ElemSet.add l' 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 caller_pn caller_pd callee_pn (s : State.t) loc : State.t = + if APIs.is_begin callee_pn then + begin + if verbose then L.stderr " calling %s@." (Procname.java_get_method callee_pn); + State.incr s + end + else if APIs.is_end callee_pn then + begin + if verbose then L.stderr " calling %s@." (Procname.java_get_method callee_pn); + if State.has_zero s then report_warning "too many end/stop" caller_pn caller_pd loc; + State.decr s + end + else s + + (** Transfer function for an instruction. *) + let do_instr pn pd (instr : Sil.instr) (state : State.t) : State.t = + match instr with + | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, loc, _) -> + do_call pn pd callee_pn state loc + | _ -> state + + (** Check if the final state contains any numbers other than zero (balanced). *) + let check_final_state 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 = Cfg.Node.get_loc exit_node in + report_warning 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 + | Sil.Lvar pvar when Sil.pvar_is_local pvar -> + let name = Mangled.to_string (Sil.pvar_get_name pvar) in + if IList.mem string_equal name boolean_variables + 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 + | Sil.UnOp (Sil.LNot, Sil.BinOp (Sil.Eq, e1, e2), _) -> + Sil.BinOp (Sil.Ne, e1, e2) + | Sil.UnOp (Sil.LNot, Sil.BinOp (Sil.Ne, e1, e2), _) -> + Sil.BinOp (Sil.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 (Sil.BinOp (Sil.Eq, _cond_e, Sil.Const (Sil.Cint i)), _, _, _) + when Sil.Int.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 (Sil.BinOp (Sil.Ne, _cond_e, Sil.Const (Sil.Cint i)), _, _, _) + when Sil.Int.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.Set (_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 + | Sil.Const (Sil.Cint i) -> Some (not (Sil.Int.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 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 + + let do_instr instr : unit = + let state1 = Automaton.do_instr pn pd instr !curr_state in + let state2 = BooleanVars.do_instr pn pd idenv instr state1 in + curr_state := state2 in + + IList.iter do_instr (Cfg.Node.get_instrs node); + [!curr_state], [!curr_state] + +(** Check the final state at the end of the analysis. *) +let check_final_state proc_name proc_desc exit_node final_s = + Automaton.check_final_state 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; proc_name; idenv } : unit = + + let module DFTrace = MakeDF(struct + type t = State.t + let equal = State.equal + let join = State.join + let do_node = do_node 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@." Procname.pp proc_name; + let transitions = DFTrace.run 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, _, _) -> + check_final_state 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 () diff --git a/infer/src/checkers/checkTraceCallSequence.mli b/infer/src/checkers/checkTraceCallSequence.mli new file mode 100644 index 000000000..221965659 --- /dev/null +++ b/infer/src/checkers/checkTraceCallSequence.mli @@ -0,0 +1,12 @@ +(* + * 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. + *) + +(** 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/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index caafea4c8..0c2ada52d 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -26,6 +26,7 @@ let active_procedure_checkers () = 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, checkers_enabled; SqlChecker.callback_sql, false; diff --git a/infer/src/opensource/facebook.ml b/infer/src/opensource/fbTraceCalls.ml similarity index 77% rename from infer/src/opensource/facebook.ml rename to infer/src/opensource/fbTraceCalls.ml index 5750b06e4..8c1cb8edd 100644 --- a/infer/src/opensource/facebook.ml +++ b/infer/src/opensource/fbTraceCalls.ml @@ -1,5 +1,5 @@ (* - * Copyright (c) 2014 - present Facebook, Inc. + * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * * This source code is licensed under the BSD style license found in the @@ -7,4 +7,4 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -let register_checkers () = () +let tracing_methods = [] diff --git a/infer/src/opensource/fbTraceCalls.mli b/infer/src/opensource/fbTraceCalls.mli new file mode 100644 index 000000000..c45238366 --- /dev/null +++ b/infer/src/opensource/fbTraceCalls.mli @@ -0,0 +1,10 @@ +(* + * 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. + *) + +val tracing_methods : (string * string * string * string) list