[pulse] remember equalities found in branches

Summary:
When we make the decision to go into a branch "v = N" where some
abstract value is compared to a constant, remember the corresponding
equality. This allows to prune simple infeasible paths
intra-procedurally.

Further work is needed to make this useful interprocedurally, for
instance either or both of these ideas could be explored:

- abduce v=N in the precondition and do not apply summaries when the
  equalities in the pre are not satisfied

- prune post-conditions that lead to unsat states where a value has to
  be equal to several different constants

Reviewed By: skcho

Differential Revision: D17906166

fbshipit-source-id: 5cc84abc2

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

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

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

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

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<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,invalid access occurs here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass<int>::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]