From 73f3eee9cd7bb0b0f26305498170a1a80ffa4cb5 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 20 Jul 2017 14:16:30 -0700 Subject: [PATCH] [checkers] use liveness analysis to create dead store checker Summary: Pretty basic: warn when we see an assignment instruction `x = ...` and `x` is not live in the post of the instruction. Only enabled for Clang at the moment because linters already warn on this for Java. But we can enable it later if we want to (should be fully generic). Reviewed By: jeremydubreil Differential Revision: D5450439 fbshipit-source-id: 693514c --- Makefile | 2 +- infer/src/IR/Localise.ml | 2 + infer/src/IR/Localise.mli | 2 + infer/src/base/Config.ml | 8 ++ infer/src/base/Config.mli | 2 + infer/src/checkers/liveness.ml | 31 +++++- infer/src/checkers/registerCheckers.ml | 1 + .../codetoanalyze/c/bufferoverrun/Makefile | 2 +- .../codetoanalyze/cpp/bufferoverrun/Makefile | 2 +- .../tests/codetoanalyze/cpp/liveness/Makefile | 20 ++++ .../cpp/liveness/dead_stores.cpp | 96 +++++++++++++++++++ .../codetoanalyze/cpp/liveness/issues.exp | 6 ++ .../codetoanalyze/cpp/quandary/pointers.cpp | 2 + 13 files changed, 171 insertions(+), 5 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/liveness/Makefile create mode 100644 infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp create mode 100644 infer/tests/codetoanalyze/cpp/liveness/issues.exp diff --git a/Makefile b/Makefile index be2b347d0..54b6637d5 100644 --- a/Makefile +++ b/Makefile @@ -32,7 +32,7 @@ BUILD_SYSTEMS_TESTS += \ DIRECT_TESTS += \ c_biabduction c_bufferoverrun c_errors c_frontend \ - cpp_bufferoverrun cpp_errors cpp_frontend cpp_quandary cpp_siof cpp_threadsafety \ + cpp_bufferoverrun cpp_errors cpp_frontend cpp_liveness cpp_quandary cpp_siof cpp_threadsafety \ ifneq ($(BUCK),no) BUILD_SYSTEMS_TESTS += buck-clang-db buck_flavors buck_flavors_deterministic diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 13cfe6aa4..a93fb114b 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -77,6 +77,8 @@ let context_leak = from_string "CONTEXT_LEAK" let dangling_pointer_dereference = from_string "DANGLING_POINTER_DEREFERENCE" +let dead_store = from_string "DEAD_STORE" + let deallocate_stack_variable = from_string "DEALLOCATE_STACK_VARIABLE" let deallocate_static_memory = from_string "DEALLOCATE_STATIC_MEMORY" diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 6ab412c2b..069a1b32c 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -69,6 +69,8 @@ val context_leak : t val dangling_pointer_dereference : t +val dead_store : t + val deallocate_stack_variable : t val deallocate_static_memory : t diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index df05bbefb..06ae6cb50 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -559,6 +559,7 @@ and ( annotation_reachability , eradicate , fragment_retains_view , immutable_cast + , liveness , printf_args , quandary , repeated_calls @@ -596,6 +597,10 @@ and ( annotation_reachability ~in_help:CLOpt.([(Analyze, manual_generic)]) ~default:true "the detection of object cast from immutable type to mutable type. For instance, it will detect cast from ImmutableList to List, ImmutableMap to Map, and ImmutableSet to Set." + and liveness = + CLOpt.mk_bool ~long:"liveness" + ~in_help:CLOpt.([(Analyze, manual_generic)]) + ~default:true "the detection of dead stores and unused variables" and printf_args = CLOpt.mk_bool ~long:"printf-args" ~in_help:CLOpt.([(Analyze, manual_generic)]) @@ -643,6 +648,7 @@ and ( annotation_reachability , eradicate , fragment_retains_view , immutable_cast + , liveness , printf_args , quandary , repeated_calls @@ -1971,6 +1977,8 @@ and linters_developer_mode = !linters_developer_mode and linters_ignore_clang_failures = !linters_ignore_clang_failures +and liveness = !liveness + and load_average = match !load_average with None when !buck -> Some (float_of_int ncpu) | _ -> !load_average diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 0accd7543..7d6886585 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -471,6 +471,8 @@ val linters_developer_mode : bool val linters_ignore_clang_failures : bool +val liveness : bool + val load_analysis_results : string option val log_file : string diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 905b1842b..94633a195 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -56,5 +56,32 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> astate end -module Analyzer = - AbstractInterpreter.Make (ProcCfg.Backward (ProcCfg.Exceptional)) (TransferFunctions) +module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional)) +module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions) + +let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = + let cfg = CFG.from_pdesc proc_desc in + let invariant_map = + Analyzer.exec_cfg cfg (ProcData.make_default proc_desc tenv) ~initial:Domain.empty ~debug:true + in + let report_dead_store live_vars = function + | Sil.Store (Lvar pvar, _, _, loc) + when not + ( Pvar.is_frontend_tmp pvar || Pvar.is_return pvar || Pvar.is_global pvar + || Domain.mem (Var.of_pvar pvar) live_vars ) + -> let issue_id = Localise.to_issue_id Localise.dead_store in + let message = F.asprintf "The value written to %a is never used" (Pvar.pp Pp.text) pvar in + let ltr = [Errlog.make_trace_element 0 loc "Write of unused value" []] in + let exn = Exceptions.Checkers (issue_id, Localise.verbatim_desc message) in + Reporting.log_error summary ~loc ~ltr exn + | _ + -> () + in + List.iter (CFG.nodes cfg) ~f:(fun node -> + (* note: extract_pre grabs the post, since the analysis is backward *) + match Analyzer.extract_pre (CFG.id node) invariant_map with + | Some live_vars + -> List.iter ~f:(report_dead_store live_vars) (CFG.instrs node) + | None + -> () ) ; + summary diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 481144bcc..b9dcbef82 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -39,6 +39,7 @@ let checkers = ; ( "immutable cast" , Config.immutable_cast , [(Procedure ImmutableChecker.callback_check_immutable_cast, Config.Java)] ) + ; ("liveness", Config.liveness, [(Procedure Liveness.checker, Config.Clang)]) ; ("printf args", Config.printf_args, [(Procedure PrintfArgs.callback_printf_args, Config.Java)]) ; ( "nullable suggestion" , Config.suggest_nullable diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/Makefile b/infer/tests/codetoanalyze/c/bufferoverrun/Makefile index aeedafc44..33f9f6477 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/Makefile +++ b/infer/tests/codetoanalyze/c/bufferoverrun/Makefile @@ -12,7 +12,7 @@ TESTS_DIR = ../../.. ANALYZER = checkers CLANG_OPTIONS = -c -INFER_OPTIONS = --bufferoverrun -F --project-root $(TESTS_DIR) --no-failures-allowed +INFER_OPTIONS = -F --project-root $(TESTS_DIR) --no-failures-allowed --no-liveness --bufferoverrun INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.c) diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile b/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile index 69352c75f..92b63476e 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile @@ -11,7 +11,7 @@ ANALYZER = checkers # see explanations in cpp/errors/Makefile for the custom isystem CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(MODELS_DIR)/cpp/include -isystem$(CLANG_INCLUDES)/c++/v1/ -c INFER_OPTIONS = --bufferoverrun --ml-buckets cpp --no-filtering --debug-exceptions \ - --project-root $(TESTS_DIR) --no-failures-allowed + --project-root $(TESTS_DIR) --no-failures-allowed --no-liveness INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.cpp) diff --git a/infer/tests/codetoanalyze/cpp/liveness/Makefile b/infer/tests/codetoanalyze/cpp/liveness/Makefile new file mode 100644 index 000000000..3943f3d6b --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/liveness/Makefile @@ -0,0 +1,20 @@ +# 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. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +# see explanations in cpp/errors/Makefile for the custom isystem +CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(MODELS_DIR)/cpp/include -isystem$(CLANG_INCLUDES)/c++/v1/ -c +INFER_OPTIONS = --ml-buckets cpp --debug-exceptions --project-root $(TESTS_DIR) --no-failures-allowed +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/liveness/dead_stores.cpp b/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp new file mode 100644 index 000000000..2ce2f29b1 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/liveness/dead_stores.cpp @@ -0,0 +1,96 @@ +/* + * Copyright (c) 2017 - 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. + */ + +namespace dead_stores { + +void easy_bad() { int x = 5; } + +void reassign_param_bad(int x) { x = 5; } + +int dead_then_live_bad() { + int x = 5; + x = 3; + return x; +} + +int use_then_dead_bad() { + int x = 5; + int y = x; + x = 7; + return y; +} + +void dead_pointer_bad() { + int num = 2; + int* x = # +} + +int return_ok() { + int x = 5; + return x; +} + +int branch_ok(bool b) { + int x = 5; + int y = 3; + if (b) { + y = x; + } + return y; +} + +int loop_ok(bool b) { + int x = 5; + int y = 3; + while (b) { + y = x; + b = false; + } + return y; +} + +int loop_break_ok(bool b) { + int x = 5; + while (b) { + x = 3; + break; + } + return x; +} + +int loop_continue_ok(bool b) { + int x = 5; + int y = 2; + while (b) { + y = x; + x = 3; + continue; + } + return y; +} + +void assign_pointer1_ok(int* ptr) { *ptr = 7; } + +int* assign_pointer2_ok() { + int num = 2; + int* ptr = # + return ptr; +} + +void by_ref_ok(int& ref) { ref = 7; } + +char* global; + +void FP_assign_array_tricky_ok() { + char arr[1]; + global = arr; + *(int*)arr = 123; // think this is a bug in the frontend... this instruction + // looks like &arr:int = 123 +} +} diff --git a/infer/tests/codetoanalyze/cpp/liveness/issues.exp b/infer/tests/codetoanalyze/cpp/liveness/issues.exp new file mode 100644 index 000000000..5fed35731 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/liveness/issues.exp @@ -0,0 +1,6 @@ +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::FP_assign_array_tricky_ok, 3, DEAD_STORE, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::dead_pointer_bad, 2, DEAD_STORE, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::dead_then_live_bad, 1, DEAD_STORE, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::easy_bad, 0, DEAD_STORE, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::reassign_param_bad, 0, DEAD_STORE, [Write of unused value] +codetoanalyze/cpp/liveness/dead_stores.cpp, dead_stores::use_then_dead_bad, 3, DEAD_STORE, [Write of unused value] diff --git a/infer/tests/codetoanalyze/cpp/quandary/pointers.cpp b/infer/tests/codetoanalyze/cpp/quandary/pointers.cpp index 287839759..6c9959c50 100644 --- a/infer/tests/codetoanalyze/cpp/quandary/pointers.cpp +++ b/infer/tests/codetoanalyze/cpp/quandary/pointers.cpp @@ -8,6 +8,7 @@ */ #include +#include extern std::string* __infer_taint_source(); extern void __infer_taint_sink(std::string); @@ -56,6 +57,7 @@ void assign_source_by_reference_bad3() { void reuse_pointer_as_local(std::string* pointer) { pointer = __infer_taint_source(); + std::cout << *pointer; } // need to understand that assigning a reference doesn't change the value in the