[pulse] arithmetic operations

Summary: Model +/- when we know the concrete interval for a value.

Reviewed By: skcho

Differential Revision: D18528535

fbshipit-source-id: 7c67a7a54

infer/src/pulse/PulseArithmetic.ml

@@ -4,8 +4,10 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  *)
+
 open! IStd
 module F = Format
+module L = Logging
 
 module Bound = struct
   type t = Int of IntLit.t | MinusInfinity | PlusInfinity [@@deriving compare]
@@ -83,6 +85,27 @@ module Bound = struct
         false
     | _ ->
         le b1 b2
+
+
+  let add b1 b2 =
+    match (b1, b2) with
+    | MinusInfinity, (MinusInfinity | Int _) | Int _, MinusInfinity ->
+        MinusInfinity
+    | PlusInfinity, (PlusInfinity | Int _) | Int _, PlusInfinity ->
+        PlusInfinity
+    | Int i1, Int i2 ->
+        Int (IntLit.add i1 i2)
+    | MinusInfinity, PlusInfinity | PlusInfinity, MinusInfinity ->
+        L.die InternalError "cannot add %a and %a" pp b1 pp b2
+
+
+  let minus = function
+    | MinusInfinity ->
+        PlusInfinity
+    | Int i ->
+        Int (IntLit.neg i)
+    | PlusInfinity ->
+        MinusInfinity
 end
 
 module Unsafe : sig
@@ -396,3 +419,50 @@ let abduce_binop_is_true ~negated bop v1 v2 =
       let a1 = Option.value v1 ~default:unknown in
       let a2 = Option.value v2 ~default:unknown in
       abduce_binop_constraints ~negated bop a1 a2
+
+
+let add a1 a2 =
+  match (a1, a2) with
+  | Between (lower1, upper1), Between (lower2, upper2) ->
+      Some (between (Bound.add lower1 lower2) (Bound.add upper1 upper2))
+  | _ ->
+      None
+
+
+let minus = function
+  | Between (lower, upper) ->
+      Some (between (Bound.minus upper) (Bound.minus lower))
+  | Outside (l, u) ->
+      Some (outside (IntLit.neg u) (IntLit.neg l))
+
+
+let binop (bop : Binop.t) a_lhs a_rhs =
+  let open Option.Monad_infix in
+  match bop with
+  | PlusA _ ->
+      add a_lhs a_rhs
+  | MinusA _ ->
+      minus a_rhs >>= add a_lhs
+  | PlusPI
+  | MinusPI
+  | MinusPP
+  | Mult _
+  | Div
+  | Mod
+  | Shiftlt
+  | Shiftrt
+  | Lt
+  | Gt
+  | Le
+  | Ge
+  | Eq
+  | Ne
+  | BAnd
+  | BXor
+  | BOr
+  | LAnd
+  | LOr ->
+      None
+
+
+let unop (unop : Unop.t) a = match unop with Neg -> minus a | BNot | LNot -> None

infer/src/pulse/PulseArithmetic.mli

@@ -35,3 +35,7 @@ val abduce_binop_is_true : negated:bool -> Binop.t -> t option -> t option -> ab
 
     If [negated] then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.
 *)
+
+val binop : Binop.t -> t -> t -> t option
+
+val unop : Unop.t -> t -> t option

infer/src/pulse/PulseOperations.ml

@@ -142,7 +142,43 @@ let eval location exp0 astate =
                (ConstantDereference i) location
         in
         Ok (astate, (addr, []))
-    | Const _ | Sizeof _ | UnOp _ | BinOp _ | Exn _ ->
+    | UnOp (unop, exp, _typ) -> (
+        eval exp astate
+        >>| fun (astate, (addr, hist)) ->
+        let unop_addr = AbstractValue.mk_fresh () in
+        match
+          Memory.get_arithmetic addr astate
+          |> Option.bind ~f:(function a, _ -> Arithmetic.unop unop a)
+        with
+        | None ->
+            (astate, (unop_addr, (* TODO history *) []))
+        | Some unop_a ->
+            let unop_hist = (* TODO: add event *) hist in
+            let unop_trace = Trace.Immediate {location; history= unop_hist} in
+            let astate = Memory.add_attribute unop_addr (Arithmetic (unop_a, unop_trace)) astate in
+            (astate, (unop_addr, unop_hist)) )
+    | BinOp (bop, e_lhs, e_rhs) -> (
+        eval e_lhs astate
+        >>= fun (astate, (addr_lhs, hist_lhs)) ->
+        eval e_rhs astate
+        >>| fun (astate, (addr_rhs, _hist_rhs)) ->
+        let binop_addr = AbstractValue.mk_fresh () in
+        match
+          Option.both
+            (Memory.get_arithmetic addr_lhs astate)
+            (Memory.get_arithmetic addr_rhs astate)
+          |> Option.bind ~f:(function (a1, _), (a2, _) -> Arithmetic.binop bop a1 a2)
+        with
+        | None ->
+            (astate, (binop_addr, (* TODO history *) []))
+        | Some binop_a ->
+            let binop_hist = (* TODO: add event *) hist_lhs in
+            let binop_trace = Trace.Immediate {location; history= binop_hist} in
+            let astate =
+              Memory.add_attribute binop_addr (Arithmetic (binop_a, binop_trace)) astate
+            in
+            (astate, (binop_addr, binop_hist)) )
+    | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in
   eval exp0 astate

infer/tests/codetoanalyze/cpp/pulse/conditionals.cpp

@@ -50,3 +50,73 @@ void compare_deref_ok(int *x) {
     *x = 42;
   }
 }
+
+void arith_test_ok(int* x, int y, int z) {
+  free(x);
+  if (y != 0 && y != 1 && y >= 1) { // should infer y >= 2
+    if (y < 2) { // always false
+      *x = 42;
+    }
+  }
+}
+
+void add_test1_ok(int* x) {
+  free(x);
+  int y = 0;
+  if (y + 1 != 1) { // always false
+    *x = 42;
+  }
+}
+
+void add_test2_ok(int* x, int y, int z) {
+  free(x);
+  if (y >= 0) {
+    if (z >= 4 && z <= 42) {
+      if (y + z < 4 || y + z <= 3 || z + 5 > 47) { // always false
+        *x = 42;
+      }
+    }
+  }
+}
+
+void add_test3_bad(int* x, int y, int z) {
+  free(x);
+  if (y > 2 && y + z > 5) { // sometimes true
+    *x = 42;
+  }
+}
+
+void add_test4_bad_FN(int* x) {
+  free(x);
+  // the concrete bound is never reached because it requires too many iterations
+  // and we never widen
+  for (int i = 0; i < 1000; i++) {
+  }
+  *x = 42;
+}
+
+void add_test5_bad(int* x, int n) {
+  free(x);
+  // the unknown bound is treated non-deterministically, good thing here
+  for (int i = 0; i < n; i++) {
+  }
+  *x = 42;
+}
+
+void add_test6_bad(int* x, int n, int step) {
+  free(x);
+  // the unknown bound is treated non-deterministically, "bad thing" here as
+  // loop should diverge but arguably the code is wrong and should have a more
+  // explicit "false" condition (so not marking FP because we would want to
+  // report here)
+  for (int i = n - 1; i < n;) {
+  }
+  *x = 42;
+}
+
+void minus_test_ok(int* x) {
+  free(x);
+  if (-1 + 3 - 2 != 0) { // always false
+    *x = 42;
+  }
+}

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,11 +1,14 @@
 codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here]
 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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,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 `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here]
 codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_interproc_compare_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_unreachable_interproc_compare_ok,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_unreachable_interproc_compare_ok,invalid access occurs here]
+codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_bad, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test3_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test5_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/conditionals.cpp, add_test6_bad, 8, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of add_test6_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test6_bad,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,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int*>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int*>::templated_wrapper_access_ok,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,parameter `a` of deduplication::SomeTemplatedClass<int>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int>::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass<int>::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass<int>::templated_wrapper_access_ok,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,assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here]