[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

@@ -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 *)

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)

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

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"

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

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

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

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=

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)

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]

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 <memory>
+#include <string>
+
+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;
+  }
+}