From d76d20a9ca6b8056bcd055ca5019cd324164b73b Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 16 Feb 2018 11:08:59 -0800 Subject: [PATCH] [ownership] prototype of ownership analysis for tracking reads/moves Summary: A simple intraprocedural analysis that tracks when a storage location is read or deleted. For now, this works only with local variable storage locations; field and array accesses are ignored. In order to test this, I added a new "use-after-lifetime" warning. It complains when a variable is read or deleted after it has already been deleted. Reviewed By: jeremydubreil Differential Revision: D6961314 fbshipit-source-id: 75e95a2 --- infer/src/IR/Typ.ml | 1 - infer/src/base/Config.ml | 5 + infer/src/base/Config.mli | 2 + infer/src/base/IssueType.ml | 2 + infer/src/base/IssueType.mli | 2 + infer/src/checkers/Ownership.ml | 151 ++++++++++++++++++ infer/src/checkers/Ownership.mli | 12 ++ infer/src/checkers/registerCheckers.ml | 3 + .../codetoanalyze/cpp/ownership/Makefile | 20 +++ .../codetoanalyze/cpp/ownership/issues.exp | 8 + .../cpp/ownership/use_after_delete.cpp | 100 ++++++++++++ 11 files changed, 305 insertions(+), 1 deletion(-) create mode 100644 infer/src/checkers/Ownership.ml create mode 100644 infer/src/checkers/Ownership.mli create mode 100644 infer/tests/codetoanalyze/cpp/ownership/Makefile create mode 100644 infer/tests/codetoanalyze/cpp/ownership/issues.exp create mode 100644 infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 889b9264e..ed1ec8599 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -1057,7 +1057,6 @@ module Procname = struct | _ -> QualifiedCppName.empty - (** Convert a proc name to a filename *) let to_concrete_filename ?crc_only pname = (* filenames for clang procs are REVERSED qualifiers with '#' as separator *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 173b5ec1d..dd8290d6a 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -679,6 +679,7 @@ and ( annotation_reachability , linters , litho , liveness + , ownership , printf_args , quandary , racerd @@ -720,6 +721,7 @@ and ( annotation_reachability and litho = mk_checker ~long:"litho" "Experimental checkers supporting the Litho framework" and liveness = mk_checker ~long:"liveness" ~default:true "the detection of dead stores and unused variables" + and ownership = mk_checker ~long:"ownership" ~default:true "the detection of C++ lifetime bugs" and printf_args = mk_checker ~long:"printf-args" ~default:true "the detection of mismatch between the Java printf format strings and the argument types For, example, this checker will warn about the type error in `printf(\"Hello %d\", \"world\")`" @@ -781,6 +783,7 @@ and ( annotation_reachability , linters , litho , liveness + , ownership , printf_args , quandary , racerd @@ -2485,6 +2488,8 @@ and only_footprint = !only_footprint and only_show = !only_show +and ownership = !ownership + and passthroughs = !passthroughs and patterns_modeled_expensive = match patterns_modeled_expensive with k, r -> (k, !r) diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 27d1a2dd5..21d7fcc40 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -496,6 +496,8 @@ val only_footprint : bool val only_show : bool +val ownership : bool + val pmd_xml : bool val precondition_stats : bool diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 6ce214f25..8d39fdb6e 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -333,6 +333,8 @@ let unsafe_guarded_by_access = from_string "UNSAFE_GUARDED_BY_ACCESS" let use_after_free = from_string "USE_AFTER_FREE" +let use_after_lifetime = from_string "USE_AFTER_LIFETIME" + let user_controlled_sql_risk = from_string "USER_CONTROLLED_SQL_RISK" let untrusted_deserialization = from_string "UNTRUSTED_DESERIALIZATION" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 3e82a15dc..497caaaba 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -246,6 +246,8 @@ val unsafe_guarded_by_access : t val use_after_free : t +val use_after_lifetime : t + val untrusted_deserialization : t val untrusted_file : t diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml new file mode 100644 index 000000000..3d9732d39 --- /dev/null +++ b/infer/src/checkers/Ownership.ml @@ -0,0 +1,151 @@ +(* + * Copyright (c) 2018 - 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 F = Format +module L = Logging + +type permission = + | TransferOwnership + (** permission to permanently transfer ownership (e.g. call a destructor, delete, or free) *) + | Read (** permission to read *) + +module Permission = struct + type astate = permission + + let ( <= ) ~lhs ~rhs = + match (lhs, rhs) with + | Read, TransferOwnership -> + true + | Read, Read | TransferOwnership, TransferOwnership -> + true + | TransferOwnership, Read -> + false + + + let join astate1 astate2 = + match (astate1, astate2) with + | Read, Read -> + Read + | TransferOwnership, _ | _, TransferOwnership -> + TransferOwnership + + + let widen ~prev ~next ~num_iters:_ = join prev next + + let pp fmt = function + | TransferOwnership -> + F.fprintf fmt "TransferOwnership" + | Read -> + F.fprintf fmt "Read" +end + +(** map from variable to permission required based on the way the variable is used. for example, if + we see delete x, then x needs permission "TransferOwnership" *) +module Domain = struct + include AbstractDomain.Map (Var) (Permission) + + let log_use_after_lifetime var loc summary = + let message = F.asprintf "Variable %a is used after its lifetime has ended" Var.pp var in + let ltr = [Errlog.make_trace_element 0 loc "Use of invalid variable" []] in + let exn = Exceptions.Checkers (IssueType.use_after_lifetime, Localise.verbatim_desc message) in + Reporting.log_error summary ~loc ~ltr exn + + + (* don't allow strong updates via add; only remove *) + let add var new_permission loc summary astate = + let permission = + try + let old_permission = find var astate in + ( match (old_permission, new_permission) with + | TransferOwnership, (Read | TransferOwnership) -> + log_use_after_lifetime var loc summary + | _ -> + () ) ; + Permission.join new_permission old_permission + with Not_found -> new_permission + in + add var permission astate + + + let access_path_add_read ((base_var, _), _) loc summary astate = + add base_var Read loc summary astate + + + let exp_add_reads exp loc summary astate = + List.fold + ~f:(fun acc access_path -> access_path_add_read access_path loc summary acc) + (HilExp.get_access_paths exp) ~init:astate + + + let actuals_add_reads actuals loc summary astate = + (* TODO: handle reads in actuals + return values properly. This is nontrivial because the + frontend sometimes chooses to translate return as pass-by-ref on a dummy actual *) + List.fold actuals + ~f:(fun acc actual_exp -> exp_add_reads actual_exp loc summary acc) + ~init:astate + + + (* handle assigning directly to a base var *) + let handle_var_assign lhs_var rhs_exp loc summary astate = + exp_add_reads rhs_exp loc summary astate |> remove lhs_var +end + +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain + + type extras = Specs.summary + + let transfers_ownership pname = + (* TODO: support delete[], free, and destructors *) + Typ.Procname.equal pname BuiltinDecl.__delete + + + let exec_instr (astate: Domain.astate) (proc_data: extras ProcData.t) _ (instr: HilInstr.t) = + let summary = proc_data.extras in + match instr with + | Assign (Base (lhs_var, _), rhs_exp, loc) -> + Domain.handle_var_assign lhs_var rhs_exp loc summary astate + | Assign (lhs_access_exp, rhs_exp, loc) -> + (* assign to field, array, indirectly with &/*, or a combination *) + Domain.exp_add_reads rhs_exp loc summary astate + |> Domain.access_path_add_read (AccessExpression.to_access_path lhs_access_exp) loc summary + | Call (_, Direct callee_pname, [(AccessExpression Base (lhs_var, _))], _, loc) + when transfers_ownership callee_pname -> + Domain.add lhs_var TransferOwnership loc summary astate + | Call (_, Direct callee_pname, [(AccessExpression Base (lhs_var, _)); rhs_exp], _, loc) + when String.equal (Typ.Procname.get_method callee_pname) "operator=" -> + Domain.handle_var_assign lhs_var rhs_exp loc summary astate + | Call (None, Direct callee_pname, lhs_exp :: actuals, _, loc) + when Typ.Procname.is_constructor callee_pname -> + (* frontend translates constructors as assigning-by-ref to first actual *) + let constructed_var = + match lhs_exp with + | AccessExpression Base (var, _) -> + var + | _ -> + L.die InternalError "Unexpected: constructor called on %a" HilExp.pp lhs_exp + in + Domain.actuals_add_reads actuals loc summary astate |> Domain.remove constructed_var + | Call (ret_opt, _, actuals, _, loc) + -> ( + let astate' = Domain.actuals_add_reads actuals loc summary astate in + match ret_opt with Some (base_var, _) -> Domain.remove base_var astate' | None -> astate' ) + | Assume (assume_exp, _, _, loc) -> + Domain.exp_add_reads assume_exp loc summary astate +end + +module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) + +let checker {Callbacks.proc_desc; tenv; summary} = + let proc_data = ProcData.make proc_desc tenv summary in + let initial = Domain.empty in + ignore (Analyzer.compute_post proc_data ~initial) ; + summary diff --git a/infer/src/checkers/Ownership.mli b/infer/src/checkers/Ownership.mli new file mode 100644 index 000000000..eb08fda49 --- /dev/null +++ b/infer/src/checkers/Ownership.mli @@ -0,0 +1,12 @@ +(* + * Copyright (c) 2018 - 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 checker : Callbacks.proc_callback_t diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 8c37f8df6..2662572d7 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -71,6 +71,9 @@ let all_checkers = ; callbacks= [ (Procedure NullabilitySuggest.checker, Language.Java) ; (Procedure NullabilitySuggest.checker, Language.Clang) ] } + ; { name= "ownership" + ; active= Config.ownership + ; callbacks= [(Procedure Ownership.checker, Language.Clang)] } ; { name= "quandary" ; active= Config.quandary ; callbacks= diff --git a/infer/tests/codetoanalyze/cpp/ownership/Makefile b/infer/tests/codetoanalyze/cpp/ownership/Makefile new file mode 100644 index 000000000..ca1658779 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/ownership/Makefile @@ -0,0 +1,20 @@ +# Copyright (c) 2018 - 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. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +# see explanations in cpp/errors/Makefile for the custom isystem +CLANG_OPTIONS = -x c++ -std=c++14 -Wc++1z-extensions -nostdinc++ -isystem$(MODELS_DIR)/cpp/include -isystem$(CLANG_INCLUDES)/c++/v1/ -c +INFER_OPTIONS = --ownership-only --ml-buckets cpp --debug-exceptions --project-root $(TESTS_DIR) +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.cpp) + +include $(TESTS_DIR)/clang.make + +infer-out/report.json: $(MAKEFILE_LIST) diff --git a/infer/tests/codetoanalyze/cpp/ownership/issues.exp b/infer/tests/codetoanalyze/cpp/ownership/issues.exp new file mode 100644 index 000000000..b2065ae95 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/ownership/issues.exp @@ -0,0 +1,8 @@ +codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, [Use of invalid variable] +codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, [Use of invalid variable] +codetoanalyze/cpp/ownership/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_LIFETIME, [Use of invalid variable] +codetoanalyze/cpp/ownership/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_LIFETIME, [Use of invalid variable] +codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_LIFETIME, [Use of invalid variable] +codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, [Use of invalid variable] +codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, [Use of invalid variable] +codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, [Use of invalid variable] diff --git a/infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp new file mode 100644 index 000000000..19e50dfb9 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/ownership/use_after_delete.cpp @@ -0,0 +1,100 @@ +/* + * Copyright (c) 2018 - 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. + */ + +#include +#include + +struct S { + int f; +}; + +void deref_deleted_bad() { + auto s = new S{1}; + delete s; + S tmp = *s; +} + +S* return_deleted_bad() { + auto s = new S{1}; + delete s; + return s; +} + +S* reassign_deleted_ok() { + auto s = new S{1}; + delete s; + s = new S{2}; + return s; +} + +void reassign_field_of_deleted_bad() { + auto s = new S{1}; + delete s; + s->f = 7; +} + +void reassign_field_of_reinitialized_ok(S* tmp) { + auto s = new S{1}; + delete s; + s = tmp; + s->f = 7; +} + +void double_delete_bad() { + auto s = new S{1}; + delete s; + delete s; +} + +S* delete_in_branch_bad(bool b) { + auto s = new S{1}; + if (b) { + delete s; + } + return s; +} + +void delete_in_branch_ok(bool b) { + auto s = new S{1}; + if (b) { + delete s; + } else { + delete s; + } +} + +void use_in_branch_bad(bool b) { + auto s = new S{1}; + delete s; + if (b) { + auto tmp = *s; + } +} + +void delete_in_loop_bad() { + auto s = new S{1}; + for (int i = 0; i < 10; i++) { + delete s; + } +} + +void delete_in_loop_ok() { + for (int i = 0; i < 10; i++) { + auto s = new S{1}; + delete s; + } +} + +void use_in_loop_bad() { + auto s = new S{1}; + delete s; + for (int i = 0; i < 10; i++) { + s->f = i; + } +}