From 3ac8e270625130f4d37d952b0ad93f444653b074 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 15 Oct 2019 03:36:49 -0700 Subject: [PATCH] [pulse] use constant equality to prune unfeasible paths Summary: When we know "x = 3" and we have a condition "x != 3" we know we can prune the corresponding path. Reviewed By: skcho Differential Revision: D17665472 fbshipit-source-id: 988958ea6 --- infer/src/pulse/Pulse.ml | 13 ++-- infer/src/pulse/PulseAbductiveDomain.ml | 2 + infer/src/pulse/PulseAbductiveDomain.mli | 2 + infer/src/pulse/PulseDomain.ml | 16 +++++ infer/src/pulse/PulseDomain.mli | 2 + infer/src/pulse/PulseOperations.ml | 57 +++++++++++++++ infer/src/pulse/PulseOperations.mli | 7 ++ .../tests/codetoanalyze/cpp/pulse/issues.exp | 4 ++ .../tests/codetoanalyze/cpp/pulse/values.cpp | 71 +++++++++++++++++++ 9 files changed, 170 insertions(+), 4 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/values.cpp diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index c439e5c42..052f98cd3 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -185,10 +185,15 @@ module PulseTransferFunctions = struct Ok astate in [check_error summary result] - | Prune (condition, loc, _is_then_branch, _if_kind) -> - (* ignored for now *) - let post = PulseOperations.eval loc condition astate |> check_error summary |> fst in - [post] + | Prune (condition, loc, _is_then_branch, _if_kind) -> ( + let post, cond_satisfiable = + PulseOperations.eval_cond loc condition astate |> check_error summary + in + match (cond_satisfiable : PulseOperations.TBool.t) with + | False -> + (* [condition] is known to be unsatisfiable: prune path *) [] + | True | Top -> + (* [condition] is true or unknown value: go into the branch *) [post] ) | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call summary ret call_exp actuals loc call_flags astate |> check_error summary | Metadata (ExitScope (vars, location)) -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 109168ac9..d515bc2ad 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -209,6 +209,8 @@ module Memory = struct BaseMemory.get_closure_proc_name addr (astate.post :> base_domain).heap + let get_constant addr astate = BaseMemory.get_constant addr (astate.post :> base_domain).heap + let std_vector_reserve addr astate = map_post_heap astate ~f:(fun heap -> BaseMemory.std_vector_reserve addr heap) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 8256c7ab1..7cf77765a 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -75,6 +75,8 @@ module Memory : sig val eval_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t (** [eval_edge addr access astate] follows the edge [addr --access--> .] in memory and returns what it points to or creates a fresh value if that edge didn't exist. *) + + val get_constant : AbstractAddress.t -> t -> Const.t option end val is_local : Var.t -> t -> bool diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index af42b0a77..467a1b9c2 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -287,6 +287,8 @@ module Attribute = struct let std_vector_reserve_rank = Variants.to_rank StdVectorReserve + let const_rank = Variants.to_rank (Constant (Const.Cint IntLit.zero)) + let pp f = function | AddressOfCppTemporary (var, history) -> F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history @@ -359,6 +361,13 @@ module Attributes = struct || Option.is_some (Set.find_rank attrs Attribute.invalid_rank) + let get_constant attrs = + Set.find_rank attrs Attribute.const_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.Constant c) = attr in + c ) + + include Set end @@ -469,6 +478,8 @@ module Memory : sig val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val get_constant : AbstractAddress.t -> t -> Const.t option + val std_vector_reserve : AbstractAddress.t -> t -> t val is_std_vector_reserved : AbstractAddress.t -> t -> bool @@ -541,6 +552,11 @@ end = struct |> Option.bind ~f:(fun attributes -> Attributes.get_closure_proc_name attributes) + let get_constant address memory = + Graph.find_opt address (snd memory) + |> Option.bind ~f:(fun attributes -> Attributes.get_constant attributes) + + let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory let is_std_vector_reserved address memory = diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 7db9cca01..50bb3507e 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -186,6 +186,8 @@ module Memory : sig val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option + val get_constant : AbstractAddress.t -> t -> Const.t option + val std_vector_reserve : AbstractAddress.t -> t -> t val is_std_vector_reserved : AbstractAddress.t -> t -> bool diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index d32016d1b..e6eed4135 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -157,6 +157,63 @@ let eval location exp0 astate = eval exp0 astate +type eval_result = + | EvalConst of Const.t + | EvalAddr of AbstractAddress.t + | EvalError of PulseDiagnostic.t + +let eval_to_const location exp astate = + match (exp : Exp.t) with + | Const c -> + EvalConst c + | exp -> ( + match eval location exp astate with + | Error err -> + EvalError err + | Ok (astate, (addr, _)) -> ( + match Memory.get_constant addr astate with Some c -> EvalConst c | None -> EvalAddr addr ) ) + + +let eval_binop (bop : Binop.t) c1 c2 = + match bop with Eq -> Const.equal c1 c2 | Ne -> not (Const.equal c1 c2) | _ -> true + + +module TBool = struct + (** booleans with \top *) + type t = True | False | Top + + let negate = function True -> False | False -> True | Top -> Top + + let of_bool b = if b then True else False +end + +let negate_cond result = Result.map result ~f:(fun (astate, b) -> (astate, TBool.negate b)) + +let rec eval_cond location exp astate = + match (exp : Exp.t) with + | BinOp (bop, e1, e2) -> ( + match eval_to_const location e1 astate with + | EvalError err -> + Error err + | EvalAddr _ -> + (* TODO: might want to remember [addr = const] and other kinds of pure facts *) + Ok (astate, TBool.Top) + | EvalConst c1 -> ( + match eval_to_const location e2 astate with + | EvalError err -> + Error err + | EvalAddr _ -> + (* TODO: might want to remember [addr = const] and other kinds of pure facts *) + Ok (astate, TBool.Top) + | EvalConst c2 -> + Ok (astate, eval_binop bop c1 c2 |> TBool.of_bool) ) ) + | UnOp (LNot, exp', _) -> + negate_cond (eval_cond location exp' astate) + | exp -> + let zero = Exp.Const (Cint IntLit.zero) in + eval_cond location (Exp.BinOp (Ne, exp, zero)) astate + + let eval_deref location exp astate = eval location exp astate >>= fun (astate, addr_trace) -> diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 6fc11a270..b1c49b8d8 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -25,6 +25,13 @@ val eval : Location.t -> Exp.t -> t -> (t * PulseDomain.AddrTracePair.t) access_ Return an error state if it traverses some known invalid address or if the end destination is known to be invalid. *) +module TBool : sig + (** booleans with \top *) + type t = True | False | Top +end + +val eval_cond : Location.t -> Exp.t -> t -> (t * TBool.t) access_result + val eval_deref : Location.t -> Exp.t -> t -> (t * PulseDomain.AddrTracePair.t) access_result (** Like [eval] but evaluates [*exp]. *) diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 07aafca52..3024899ce 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -46,6 +46,10 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `invalidate_local_ok` here,memory is the address of a stack variable `t` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,assigned,returned from call to `invalidate_local_ok`,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/values.cpp b/infer/tests/codetoanalyze/cpp/pulse/values.cpp new file mode 100644 index 000000000..f5e3d7bd4 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/values.cpp @@ -0,0 +1,71 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +void error_under_true_conditionals_bad(int* x) { + if (1) { + free(x); + } + if (2 == 2) { + *x = 42; + } +} + +void simple_infeasible_error_path_ok(int* x) { + free(x); + if (0 == 1) { + *x = 42; + } + + int y = 0; + if (y == 1) { + *x = 42; + } + if (y) { + *x = 42; + } + if (y != 0) { + *x = 42; + } + if (!(y == 0)) { + *x = 42; + } + if (!(!(y != 0))) { + *x = 42; + } + if (!(!(!(0 == y)))) { + *x = 42; + } +} + +void free_if(int* x, int b) { + if (b) { + free(x); + } +} + +void FP_no_free_if_ok(int* x) { + free_if(x, 0); + *x = 42; +} + +void free_if_deref_bad(int* x) { + free_if(x, 1); + *x = 42; +} + +// Document some limitations, although there are so many for now that +// it's not really worth it. Add more tests when/if the analysis gets +// smarter than just constants. +void FP_infeasible_tricky_ok(int* x) { + free_if(x, x == x); + int y = 42; + if (2 * y != y << 1) { + free(x); + *x = 42; + } +}