From f5786c444b0ebdd1fe2948051e1278d6bfa42c05 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 26 Oct 2018 07:30:14 -0700 Subject: [PATCH] [pulse] use after free Summary: Model `free` like `delete`. Reviewed By: mbouaziz, skcho Differential Revision: D10509332 fbshipit-source-id: fe4249601 --- infer/src/checkers/PulseDomain.ml | 6 +++++- infer/src/checkers/PulseInvalidation.ml | 6 ++++++ infer/src/checkers/PulseInvalidation.mli | 1 + infer/src/checkers/PulseModels.ml | 11 +++++++++++ infer/tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../tests/codetoanalyze/cpp/pulse/use_after_free.cpp | 12 ++++++++++++ 6 files changed, 36 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 9e5cff411..b2b9489fc 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -155,7 +155,11 @@ module Domain : AbstractDomain.S with type astate = t = struct let compare_size _ _ = 0 - let merge ~from ~to_ = if Config.debug_mode then to_ := Set.union !from !to_ + let merge ~from ~to_ = + (* building the actual set is only useful to display what equalities where discovered in the + HTML debug output *) + if Config.debug_mode then to_ := Set.union !from !to_ + let pp f x = Set.pp f !x end diff --git a/infer/src/checkers/PulseInvalidation.ml b/infer/src/checkers/PulseInvalidation.ml index 7147e441f..db9392d82 100644 --- a/infer/src/checkers/PulseInvalidation.ml +++ b/infer/src/checkers/PulseInvalidation.ml @@ -11,6 +11,7 @@ module L = Logging type cause = | CppDelete of AccessExpression.t | CppDestructor of Typ.Procname.t * AccessExpression.t + | CFree of AccessExpression.t | StdVectorPushBack of AccessExpression.t [@@deriving compare] @@ -21,6 +22,8 @@ let issue_type_of_cause = function IssueType.use_after_delete | CppDestructor _ -> IssueType.use_after_lifetime + | CFree _ -> + IssueType.use_after_free | StdVectorPushBack _ -> IssueType.use_after_lifetime @@ -33,6 +36,9 @@ let pp f ({cause; location}[@warning "+9"]) = | CppDestructor (proc_name, access_expr) -> F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name AccessExpression.pp access_expr Location.pp location + | CFree access_expr -> + F.fprintf f "invalidated by call to `free(%a)` at %a" AccessExpression.pp access_expr + Location.pp location | StdVectorPushBack access_expr -> F.fprintf f "potentially invalidated by call to `std::vector::push_back(%a, ..)` at %a" AccessExpression.pp access_expr Location.pp location diff --git a/infer/src/checkers/PulseInvalidation.mli b/infer/src/checkers/PulseInvalidation.mli index e0bd169b4..44f36aa21 100644 --- a/infer/src/checkers/PulseInvalidation.mli +++ b/infer/src/checkers/PulseInvalidation.mli @@ -9,6 +9,7 @@ open! IStd type cause = | CppDelete of AccessExpression.t | CppDestructor of Typ.Procname.t * AccessExpression.t + | CFree of AccessExpression.t | StdVectorPushBack of AccessExpression.t [@@deriving compare] diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index f83b526fb..825ef135d 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -16,6 +16,16 @@ type exec_fun = type model = exec_fun +module C = struct + let free : model = + fun location ~ret:_ ~actuals astate -> + match actuals with + | [AccessExpression deleted_access] -> + PulseDomain.invalidate (CFree deleted_access) location deleted_access astate + | _ -> + Ok astate +end + module Cplusplus = struct let delete : model = fun location ~ret:_ ~actuals astate -> @@ -89,6 +99,7 @@ end let builtins_dispatcher = let builtins = [ (BuiltinDecl.__delete, Cplusplus.delete) + ; (BuiltinDecl.free, C.free) ; (BuiltinDecl.__placement_new, Cplusplus.placement_new) ] in let builtins_map = diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 1d640f60c..7e8dec71d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -28,4 +28,5 @@ codetoanalyze/cpp/ownership/use_after_destructor.cpp, reinit_after_explicit_dest codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `S_~S(&(s))` at line 61, column 3 here,accessed `*(s.f)` here] codetoanalyze/cpp/ownership/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidated by destructor call `C_~C(&(c))` at line 186, column 3 here,accessed `pc->f` here] codetoanalyze/cpp/pulse/join.cpp, visit_list, 11, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here] +codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(x), ..)` at line 13, column 3 here,accessed `*(y)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp new file mode 100644 index 000000000..2672b045d --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp @@ -0,0 +1,12 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +int use_after_free_simple_bad(int* x) { + free(x); + return *x; +}