[pulse] Add bo_itv to pulse attributes

Summary:
This diff adds inferbo's interval values to pulse's attributes.  The added values will be used to
filter out infeasible passes in the following diffs.

Reviewed By: jvillard

Differential Revision: D18726667

fbshipit-source-id: c1125ac6e

infer/src/bufferoverrun/bounds.ml

@@ -308,6 +308,8 @@ module Bound = struct
 
   let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
 
+  let of_pulse_value v = of_sym (SymLinear.singleton_one (Symb.Symbol.of_pulse_value v))
+
   let of_path path_of_partial make_symbol ~unsigned ?non_int partial =
     let s = make_symbol ~unsigned ?non_int (path_of_partial partial) in
     of_sym (SymLinear.singleton_one s)

infer/src/bufferoverrun/bounds.mli

@@ -23,6 +23,8 @@ module Bound : sig
 
   val of_big_int : Z.t -> t
 
+  val of_pulse_value : PulseAbstractValue.t -> t
+
   val minf : t
 
   val mone : t

infer/src/bufferoverrun/itv.ml

@@ -119,6 +119,8 @@ module ItvPure = struct
 
   let of_big_int n = of_bound (Bound.of_big_int n)
 
+  let of_pulse_value v = of_bound (Bound.of_pulse_value v)
+
   let mone = of_bound Bound.mone
 
   let zero_255 = (Bound.zero, Bound.z255)
@@ -574,6 +576,8 @@ let of_big_int : Z.t -> t = fun n -> NonBottom (ItvPure.of_big_int n)
 
 let of_int_lit : IntLit.t -> t = fun n -> of_big_int (IntLit.to_big_int n)
 
+let of_pulse_value : PulseAbstractValue.t -> t = fun v -> NonBottom (ItvPure.of_pulse_value v)
+
 let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
 
 let le : lhs:t -> rhs:t -> bool = leq

infer/src/bufferoverrun/itv.mli

@@ -145,6 +145,8 @@ val of_big_int : Z.t -> t
 
 val of_int_lit : IntLit.t -> t
 
+val of_pulse_value : PulseAbstractValue.t -> t
+
 val get_const : t -> Z.t option
 
 val is_zero : t -> bool

infer/src/bufferoverrun/symb.ml

@@ -267,6 +267,7 @@ module Symbol = struct
   (* NOTE: non_int represents the symbols that are not integer type,
      so that their ranges are not used in the cost checker. *)
   type t =
+    | PulseValue of PulseAbstractValue.t
     | OneValue of {unsigned: extra_bool; non_int: extra_bool; path: SymbolPath.t}
     | BoundEnd of
         {unsigned: extra_bool; non_int: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t}
@@ -275,13 +276,15 @@ module Symbol = struct
   let pp : F.formatter -> t -> unit =
    fun fmt s ->
     match s with
+    | PulseValue v ->
+        PulseAbstractValue.pp fmt v
     | OneValue {unsigned; non_int; path} | BoundEnd {unsigned; non_int; path} ->
         SymbolPath.pp fmt path ;
         ( if Config.developer_mode then
           match s with
           | BoundEnd {bound_end} ->
               Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end)
-          | OneValue _ ->
+          | PulseValue _ | OneValue _ ->
               () ) ;
         if Config.bo_debug > 1 then
           F.fprintf fmt "(%c%s)" (if unsigned then 'u' else 's') (if non_int then "n" else "")
@@ -289,6 +292,12 @@ module Symbol = struct
 
   let compare s1 s2 =
     match (s1, s2) with
+    | PulseValue _, (OneValue _ | BoundEnd _) ->
+        -1
+    | (OneValue _ | BoundEnd _), PulseValue _ ->
+        1
+    | PulseValue x, PulseValue y ->
+        PulseAbstractValue.compare x y
     | OneValue _, BoundEnd _ ->
         -1
     | BoundEnd _, OneValue _ ->
@@ -308,7 +317,7 @@ module Symbol = struct
 
   let paths_equal s1 s2 =
     match (s1, s2) with
-    | OneValue _, BoundEnd _ | BoundEnd _, OneValue _ ->
+    | PulseValue _, _ | _, PulseValue _ | OneValue _, BoundEnd _ | BoundEnd _, OneValue _ ->
         false
     | OneValue {path= path1}, OneValue {path= path2} | BoundEnd {path= path1}, BoundEnd {path= path2}
       ->
@@ -325,24 +334,39 @@ module Symbol = struct
    fun bound_end ~unsigned ?(non_int = false) path -> BoundEnd {unsigned; non_int; path; bound_end}
 
 
+  let of_pulse_value v = PulseValue v
+
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 
-  let is_unsigned : t -> bool = function OneValue {unsigned} | BoundEnd {unsigned} -> unsigned
+  let is_unsigned : t -> bool = function
+    | PulseValue _ ->
+        false
+    | OneValue {unsigned} | BoundEnd {unsigned} ->
+        unsigned
+
+
+  let is_non_int : t -> bool = function
+    | PulseValue _ ->
+        false
+    | OneValue {non_int} | BoundEnd {non_int} ->
+        non_int
 
-  let is_non_int : t -> bool = function OneValue {non_int} | BoundEnd {non_int} -> non_int
 
   let is_global : t -> bool = function
+    | PulseValue _ ->
+        false
     | OneValue {path} | BoundEnd {path} ->
         SymbolPath.is_global path
 
 
-  let path = function OneValue {path} | BoundEnd {path} -> path
+  (* This should be called on non-pulse bound as of now. *)
+  let path = function PulseValue _ -> assert false | OneValue {path} | BoundEnd {path} -> path
 
   (* NOTE: This may not be satisfied in the cost checker for simplifying its results. *)
   let check_bound_end s be =
     if Config.bo_debug >= 3 then
       match s with
-      | OneValue _ ->
+      | PulseValue _ | OneValue _ ->
           ()
       | BoundEnd {bound_end} ->
           if not (BoundEnd.equal be bound_end) then
@@ -351,7 +375,11 @@ module Symbol = struct
               (BoundEnd.to_string be)
 
 
-  let exists_str ~f = function OneValue {path} | BoundEnd {path} -> SymbolPath.exists_str ~f path
+  let exists_str ~f = function
+    | PulseValue _ ->
+        false
+    | OneValue {path} | BoundEnd {path} ->
+        SymbolPath.exists_str ~f path
 end
 
 module SymbolSet = struct

infer/src/bufferoverrun/symb.mli

@@ -118,6 +118,8 @@ module Symbol : sig
 
   val make_boundend : BoundEnd.t -> make_t
 
+  val of_pulse_value : PulseAbstractValue.t -> t
+
   val exists_str : f:(string -> bool) -> t -> bool
 end
 

infer/src/pulse/PulseAbductiveDomain.ml

@@ -634,6 +634,7 @@ module PrePost = struct
         Attribute.Arithmetic (arith, add_call_to_trace proc_name call_location caller_history trace)
     | AddressOfCppTemporary (_, _)
     | AddressOfStackVariable (_, _, _)
+    | BoItv _
     | Closure _
     | MustBeValid _
     | StdVectorReserve

infer/src/pulse/PulseAttribute.ml

@@ -30,6 +30,7 @@ module Attribute = struct
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
     | Arithmetic of Arithmetic.t * Trace.t
+    | BoItv of Itv.t
     | Closure of Typ.Procname.t
     | Invalid of Invalidation.t * Trace.t
     | MustBeValid of Trace.t
@@ -73,6 +74,8 @@ module Attribute = struct
         F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history
     | AddressOfStackVariable (var, location, history) ->
         F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location
+    | BoItv bo_itv ->
+        F.fprintf f "BoItv (%a)" Itv.pp bo_itv
     | Closure pname ->
         Typ.Procname.pp f pname
     | Arithmetic (phi, trace) ->

infer/src/pulse/PulseAttribute.mli

@@ -15,6 +15,7 @@ type t =
   | AddressOfCppTemporary of Var.t * ValueHistory.t
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
   | Arithmetic of Arithmetic.t * Trace.t
+  | BoItv of Itv.t
   | Closure of Typ.Procname.t
   | Invalid of Invalidation.t * Trace.t
   | MustBeValid of Trace.t

infer/src/pulse/PulseOperations.ml

@@ -137,6 +137,7 @@ let eval location exp0 astate =
           Memory.add_attribute addr
             (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []}))
             astate
+          |> Memory.add_attribute addr (BoItv (Itv.of_int_lit i))
           |> Memory.invalidate
                (addr, [ValueHistory.Assignment location])
                (ConstantDereference i) location

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

@@ -59,6 +59,7 @@ codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad,
 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

@@ -69,3 +69,12 @@ void FP_infeasible_tricky_ok(int* x) {
     *x = 42;
   }
 }
+
+int minus(int x, int y) { return x - y; }
+
+void function_call_infeasible_error_path_ok_FP(int* x) {
+  free(x);
+  if (minus(0, 0) < 0) {
+    *x = 42;
+  }
+}