[pulsebo] use inferbo in prunes

Summary:
Finally use information from the inferbo intervals in pulse's domain to
make decisions about whether conditionals are feasible or not.

Reviewed By: skcho

Differential Revision: D18811193

fbshipit-source-id: d80a28657

infer/src/bufferoverrun/itv.mli

@@ -110,6 +110,8 @@ module ItvPure : sig
   val arith_binop : Binop.t -> t -> t -> t
 
   val arith_unop : Unop.t -> t -> t option
+
+  val to_boolean : t -> Boolean.t
 end
 
 include module type of AbstractDomain.BottomLifted (ItvPure)

infer/src/pulse/PulseOperations.ml

@@ -243,15 +243,17 @@ let eval_arith location exp astate =
         , None
         , Some
             ( Arithmetic.equal_to i
-            , Trace.Immediate {location; history= [ValueHistory.Assignment location]} ) )
+            , Trace.Immediate {location; history= [ValueHistory.Assignment location]} )
+        , Itv.ItvPure.of_int_lit i )
   | exp -> (
       eval location exp astate
       >>| fun (astate, (addr, _)) ->
+      let bo_itv = Memory.get_bo_itv addr astate in
       match Memory.get_arithmetic addr astate with
       | Some a ->
-          (astate, Some addr, Some a)
+          (astate, Some addr, Some a, bo_itv)
       | None ->
-          (astate, Some addr, None) )
+          (astate, Some addr, None, bo_itv) )
 
 
 let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate =
@@ -275,9 +277,9 @@ let prune ~is_then_branch if_kind location ~condition astate =
     match (exp : Exp.t) with
     | BinOp (bop, e1, e2) -> (
         eval_arith location e1 astate
-        >>= fun (astate, addr1, eval1) ->
+        >>= fun (astate, addr1, eval1, evalbo1) ->
         eval_arith location e2 astate
-        >>| fun (astate, addr2, eval2) ->
+        >>| fun (astate, addr2, eval2, evalbo2) ->
         match
           Arithmetic.abduce_binop_is_true ~negated bop (Option.map ~f:fst eval1)
             (Option.map ~f:fst eval2)
@@ -290,7 +292,18 @@ let prune ~is_then_branch if_kind location ~condition astate =
               record_abduced event location addr1 eval1 abduced1 astate
               |> record_abduced event location addr2 eval2 abduced2
             in
-            (astate, true) )
+            let satisfiable =
+              match Itv.ItvPure.arith_binop bop evalbo1 evalbo2 |> Itv.ItvPure.to_boolean with
+              | False ->
+                  negated
+              | True ->
+                  not negated
+              | Top ->
+                  true
+              | Bottom ->
+                  false
+            in
+            (astate, satisfiable) )
     | UnOp (LNot, exp', _) ->
         prune_aux ~negated:(not negated) exp' astate
     | exp ->

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

@@ -103,12 +103,10 @@ void add_test5_bad(int* x, int n) {
   *x = 42;
 }
 
-void add_test6_bad(int* x, int n, int step) {
+void add_test6_bad_FNish(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)
+  // the loop should diverge but arguably the code is wrong and should
+  // have a more explicit "false" condition (hence "FN-ish")
   for (int i = n - 1; i < n;) {
   }
   *x = 42;

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

@@ -8,7 +8,6 @@ codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFT
 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]
@@ -67,10 +66,8 @@ 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,parameter `x` of double_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of double_free_simple_bad,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,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,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 `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return 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,parameter `x` of FP_infeasible_tricky_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,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,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,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,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
-codetoanalyze/cpp/pulse/values.cpp, function_call_infeasible_error_path_ok_FP, 3, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of function_call_infeasible_error_path_ok_FP,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of function_call_infeasible_error_path_ok_FP,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,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return 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,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return 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,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/values.cpp

@@ -58,10 +58,9 @@ void free_if_deref_bad(int* x) {
   *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) {
+// that was supposed to be a FP due to tricky arithmetic but inferbo is too
+// smart!
+void infeasible_tricky_ok(int* x) {
   free_if(x, x == x);
   int y = 42;
   if (2 * y != y << 1) {
@@ -72,7 +71,7 @@ void FP_infeasible_tricky_ok(int* x) {
 
 int minus(int x, int y) { return x - y; }
 
-void function_call_infeasible_error_path_ok_FP(int* x) {
+void function_call_infeasible_error_path_ok(int* x) {
   free(x);
   if (minus(0, 0) < 0) {
     *x = 42;