[pulsebo] Bottom intervals cannot appear in an abstract state

Summary:
Refine the type of inferbo intervals attributes to "pure" (non-bottom)
ones. This is because were we to get a Bottom value from inferbo we
should stop the abstract execution instead of recording it in the state.

Reviewed By: ezgicicek

Differential Revision: D18811165

fbshipit-source-id: fff8664b7

infer/src/bufferoverrun/itv.ml

@@ -123,6 +123,8 @@ module ItvPure = struct
 
   let of_big_int n = of_bound (Bound.of_big_int n)
 
+  let of_int_lit n = of_big_int (IntLit.to_big_int n)
+
   let of_pulse_value v = of_bound (Bound.of_pulse_value v)
 
   let mone = of_bound Bound.mone
@@ -582,7 +584,7 @@ let of_int : int -> t = fun n -> NonBottom (ItvPure.of_int n)
 
 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_int_lit : IntLit.t -> t = fun n -> NonBottom (ItvPure.of_int_lit n)
 
 let of_pulse_value : PulseAbstractValue.t -> t = fun v -> NonBottom (ItvPure.of_pulse_value v)
 

infer/src/bufferoverrun/itv.mli

@@ -100,6 +100,16 @@ module ItvPure : sig
   val mult : t -> t -> t
 
   val exists_str : f:(string -> bool) -> t -> bool
+
+  val of_int_lit : IntLit.t -> t
+
+  val of_pulse_value : PulseAbstractValue.t -> t
+
+  val get_bound : t -> Symb.BoundEnd.t -> Bound.t
+
+  val arith_binop : Binop.t -> t -> t -> t option
+
+  val arith_unop : Unop.t -> t -> t option
 end
 
 include module type of AbstractDomain.BottomLifted (ItvPure)

infer/src/pulse/PulseAbductiveDomain.ml

@@ -360,6 +360,10 @@ module PrePost = struct
         ; arith_callee: Arithmetic.t option }
         (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller
             state *)
+    | ArithmeticBo of
+        {addr_caller: AbstractValue.t; addr_callee: AbstractValue.t; arith_callee: Itv.ItvPure.t}
+        (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller
+            state *)
 
   let pp_cannot_apply_pre fmt = function
     | Aliasing {addr_caller; addr_callee; addr_callee'} ->
@@ -370,6 +374,10 @@ module PrePost = struct
           AbstractValue.pp addr_caller (Pp.option Arithmetic.pp) arith_caller AbstractValue.pp
           addr_callee (Pp.option Arithmetic.pp) arith_callee AbstractValue.pp addr_caller
           AbstractValue.pp addr_callee
+    | ArithmeticBo {addr_caller; addr_callee; arith_callee} ->
+        F.fprintf fmt
+          "callee addr %a%a is incompatible with caller addr %a's arithmetic constraints"
+          AbstractValue.pp addr_callee Itv.ItvPure.pp arith_callee AbstractValue.pp addr_caller
 
 
   exception CannotApplyPre of cannot_apply_pre
@@ -532,23 +540,29 @@ module PrePost = struct
           ~addr_pre ~addr_hist_caller call_state )
 
 
-  let subst_attributes attrs_callee {astate; subst} =
+  let subst_attributes ~addr_callee ~addr_caller attrs_callee {astate; subst} =
     let eval_sym_of_subst subst s bound_end =
       let v = Symb.Symbol.get_pulse_value_exn s in
       match PulseAbstractValue.Map.find_opt v !subst with
       | Some (v', _) ->
-          Itv.get_bound (Memory.get_bo_itv v' astate) bound_end
+          Itv.ItvPure.get_bound (Memory.get_bo_itv v' astate) bound_end
       | None ->
           let v' = PulseAbstractValue.mk_fresh () in
           subst := PulseAbstractValue.Map.add v (v', []) !subst ;
-          AbstractDomain.Types.NonBottom (Bounds.Bound.of_pulse_value v')
+          Bounds.Bound.of_pulse_value v'
     in
     let subst_attribute subst attr =
       match (attr : Attribute.t) with
-      | BoItv itv ->
+      | BoItv itv -> (
           let subst = ref subst in
-          let itv' = Itv.subst itv (eval_sym_of_subst subst) in
+          match
+            Itv.ItvPure.subst itv (fun symb bound ->
+                AbstractDomain.Types.NonBottom (eval_sym_of_subst subst symb bound) )
+          with
+          | NonBottom itv' ->
               (!subst, Attribute.BoItv itv')
+          | Bottom ->
+              raise (CannotApplyPre (ArithmeticBo {addr_callee; addr_caller; arith_callee= itv})) )
       | AddressOfCppTemporary _
       | AddressOfStackVariable _
       | Arithmetic _
@@ -602,7 +616,10 @@ module PrePost = struct
 
   let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state =
     let one_address_sat addr_pre callee_attrs addr_hist_caller call_state =
-      let subst, attrs_pre = subst_attributes callee_attrs call_state in
+      let subst, attrs_pre =
+        subst_attributes ~addr_callee:addr_pre ~addr_caller:(fst addr_hist_caller) callee_attrs
+          call_state
+      in
       solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre
         ~addr_hist_caller {call_state with subst}
     in
@@ -673,7 +690,8 @@ module PrePost = struct
             old_post_edges edges_pre )
 
 
-  let add_call_to_attributes proc_name call_location caller_history attrs call_state =
+  let add_call_to_attributes proc_name call_location ~addr_callee ~addr_caller caller_history attrs
+      call_state =
     let add_call_to_attribute attr =
       match (attr : Attribute.t) with
       | Invalid (invalidation, trace) ->
@@ -691,7 +709,7 @@ module PrePost = struct
       | WrittenTo _ ->
           attr
     in
-    let call_state, attrs = subst_attributes attrs call_state in
+    let call_state, attrs = subst_attributes ~addr_callee ~addr_caller attrs call_state in
     (call_state, Attributes.map attrs ~f:(fun attr -> add_call_to_attribute attr))
 
 
@@ -703,7 +721,8 @@ module PrePost = struct
     let heap = (call_state.astate.post :> base_domain).heap in
     let subst, heap =
       let subst, attrs_post_caller =
-        add_call_to_attributes callee_proc_name call_loc hist_caller attrs_post call_state
+        add_call_to_attributes ~addr_callee ~addr_caller callee_proc_name call_loc hist_caller
+          attrs_post call_state
       in
       (subst, BaseMemory.set_attrs addr_caller attrs_post_caller heap)
     in
@@ -873,8 +892,8 @@ module PrePost = struct
                 (* callee address has no meaning for the caller *) (subst, heap)
             | Some (addr_caller, history) ->
                 let subst, attrs' =
-                  add_call_to_attributes callee_proc_name call_loc history attrs
+                  add_call_to_attributes callee_proc_name call_loc ~addr_callee ~addr_caller history
-                    {call_state with subst}
+                    attrs {call_state with subst}
                 in
                 (subst, BaseMemory.set_attrs addr_caller attrs' heap) )
         (pre_post.post :> BaseDomain.t).heap (call_state.subst, heap0)

infer/src/pulse/PulseAbductiveDomain.mli

@@ -82,7 +82,7 @@ module Memory : sig
 
   val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
 
-  val get_bo_itv : AbstractValue.t -> t -> Itv.t
+  val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
 end
 
 val is_local : Var.t -> t -> bool

infer/src/pulse/PulseAttribute.ml

@@ -29,7 +29,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
+    | BoItv of Itv.ItvPure.t
     | Closure of Typ.Procname.t
     | Invalid of Invalidation.t * Trace.t
     | MustBeValid of Trace.t
@@ -64,7 +64,7 @@ module Attribute = struct
 
   let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero, dummy_trace))
 
-  let bo_itv_rank = Variants.to_rank (BoItv Itv.zero)
+  let bo_itv_rank = Variants.to_rank (BoItv Itv.ItvPure.zero)
 
   let pp f attribute =
     let pp_string_if_debug string fmt =
@@ -76,7 +76,7 @@ module Attribute = struct
     | 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
+        F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv
     | Closure pname ->
         Typ.Procname.pp f pname
     | Arithmetic (phi, trace) ->

infer/src/pulse/PulseAttribute.mli

@@ -15,7 +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
+  | BoItv of Itv.ItvPure.t
   | Closure of Typ.Procname.t
   | Invalid of Invalidation.t * Trace.t
   | MustBeValid of Trace.t
@@ -34,7 +34,7 @@ module Attributes : sig
 
   val get_arithmetic : t -> (Arithmetic.t * Trace.t) option
 
-  val get_bo_itv : t -> Itv.t option
+  val get_bo_itv : t -> Itv.ItvPure.t option
 
   val get_invalid : t -> (Invalidation.t * Trace.t) option
 

infer/src/pulse/PulseBaseMemory.ml

@@ -93,7 +93,7 @@ let get_arithmetic = get_attribute Attributes.get_arithmetic
 let get_bo_itv v memory =
   match get_attribute Attributes.get_bo_itv v memory with
   | None ->
-      Itv.of_pulse_value v
+      Itv.ItvPure.of_pulse_value v
   | Some itv ->
       itv
 

infer/src/pulse/PulseBaseMemory.mli

@@ -62,7 +62,7 @@ val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
 val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
 
-val get_bo_itv : AbstractValue.t -> t -> Itv.t
+val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
 
 val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
 

infer/src/pulse/PulseOperations.ml

@@ -122,11 +122,11 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs astate =
   let bo_itv_of_op op astate =
     match op with
     | LiteralOperand i ->
-        Itv.of_int_lit i
+        Itv.ItvPure.of_int_lit i
     | AbstractValueOperand v ->
         Memory.get_bo_itv v astate
   in
-  match Itv.arith_binop bop (bo_itv_of_op op_lhs astate) (bo_itv_of_op op_rhs astate) with
+  match Itv.ItvPure.arith_binop bop (bo_itv_of_op op_lhs astate) (bo_itv_of_op op_rhs astate) with
   | None ->
       astate
   | Some itv ->
@@ -155,7 +155,7 @@ let eval_unop_arith location unop_addr unop operand_addr unop_hist astate =
 
 
 let eval_unop_bo_itv unop_addr unop operand_addr astate =
-  match Itv.arith_unop unop (Memory.get_bo_itv operand_addr astate) with
+  match Itv.ItvPure.arith_unop unop (Memory.get_bo_itv operand_addr astate) with
   | None ->
       astate
   | Some itv ->
@@ -212,7 +212,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.add_attribute addr (BoItv (Itv.ItvPure.of_int_lit i))
           |> Memory.invalidate
                (addr, [ValueHistory.Assignment location])
                (ConstantDereference i) location