[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

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

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)
 

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

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 =

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

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

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]. *)
 

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]

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 <stdlib.h>
+
+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;
+  }
+}