diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 052f98cd3..57a2ead6a 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -187,7 +187,7 @@ module PulseTransferFunctions = struct [check_error summary result] | Prune (condition, loc, _is_then_branch, _if_kind) -> ( let post, cond_satisfiable = - PulseOperations.eval_cond loc condition astate |> check_error summary + PulseOperations.assert_is_true loc ~condition astate |> check_error summary in match (cond_satisfiable : PulseOperations.TBool.t) with | False -> diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index e6eed4135..7188105df 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -157,62 +157,65 @@ let eval location exp0 astate = eval exp0 astate -type eval_result = - | EvalConst of Const.t - | EvalAddr of AbstractAddress.t - | EvalError of PulseDiagnostic.t +type eval_result = EvalConst of Const.t | EvalAddr of AbstractAddress.t let eval_to_const location exp astate = match (exp : Exp.t) with | Const c -> - EvalConst c + Ok (astate, 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 ) ) + eval location exp astate + >>| fun (astate, (addr, _)) -> + match Memory.get_constant addr astate with + | Some c -> + (astate, EvalConst c) + | None -> + (astate, 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 +let eval_binop ~negated (bop : Binop.t) c1 c2 = + match (bop, negated) with + | Eq, false | Ne, true -> + Const.equal c1 c2 + | Eq, true | Ne, false -> + 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 = +let rec eval_cond ~negated 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) ) ) + eval_to_const location e1 astate + >>= fun (astate, eval1) -> + eval_to_const location e2 astate + >>| fun (astate, eval2) -> + match (eval1, eval2) with + | EvalConst c1, EvalConst c2 -> + (astate, eval_binop ~negated bop c1 c2 |> TBool.of_bool) + | EvalAddr _, EvalAddr _ -> + (astate, TBool.Top) + | EvalAddr v, EvalConst c | EvalConst c, EvalAddr v -> ( + match (bop, negated) with + | Eq, false | Ne, true -> + (Memory.add_attribute v (Constant c) astate, TBool.True) + | _ -> + (astate, TBool.Top) ) ) | UnOp (LNot, exp', _) -> - negate_cond (eval_cond location exp' astate) + eval_cond ~negated:(not negated) location exp' astate | exp -> let zero = Exp.Const (Cint IntLit.zero) in - eval_cond location (Exp.BinOp (Ne, exp, zero)) astate + eval_cond ~negated location (Exp.BinOp (Ne, exp, zero)) astate + +let assert_is_true location ~condition astate = eval_cond ~negated:false location condition astate let eval_deref location exp astate = eval location exp astate diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index b1c49b8d8..7d5b06ae0 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -30,7 +30,7 @@ module TBool : sig type t = True | False | Top end -val eval_cond : Location.t -> Exp.t -> t -> (t * TBool.t) access_result +val assert_is_true : Location.t -> condition: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/conditionals.cpp b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp new file mode 100644 index 000000000..b59473323 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp @@ -0,0 +1,26 @@ +/* + * 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 unreachable_eq_then_ne_ok(int* x, int y) { + if (y == 0) { + free(x); + } + if (y != 0) { + free(x); + } +} + +// pulse only tracks equality for now, not disequality +void FP_unreachable_ne_then_eq_ok(int* x, int y) { + if (y != 0) { + free(x); + } + if (y == 0) { + free(x); + } +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 3024899ce..d4076d326 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -5,6 +5,7 @@ codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_b codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,value captured as `&s`,invalid access occurs here] +codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_ne_then_eq_ok, 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/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function<_Bool>` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,invalid access occurs here]