From 2316608b8562a5418b347aea8392246119590f38 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 9 Dec 2019 09:16:40 -0800 Subject: [PATCH] [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 | 4 ++- infer/src/bufferoverrun/itv.mli | 10 ++++++ infer/src/pulse/PulseAbductiveDomain.ml | 43 +++++++++++++++++------- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseAttribute.ml | 6 ++-- infer/src/pulse/PulseAttribute.mli | 4 +-- infer/src/pulse/PulseBaseMemory.ml | 2 +- infer/src/pulse/PulseBaseMemory.mli | 2 +- infer/src/pulse/PulseOperations.ml | 8 ++--- 9 files changed, 56 insertions(+), 25 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index a5409705d..69f3df683 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 63046423a..b7b78978c 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index af373713d..db20c9596 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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 - (!subst, Attribute.BoItv itv') + 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 - {call_state with subst} + add_call_to_attributes callee_proc_name call_loc ~addr_callee ~addr_caller history + attrs {call_state with subst} in (subst, BaseMemory.set_attrs addr_caller attrs' heap) ) (pre_post.post :> BaseDomain.t).heap (call_state.subst, heap0) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 47f7f4951..e138f40a3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/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 diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index c2c3935cf..e19197531 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/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) -> diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index f81999942..d973f9747 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/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 diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml index 1c307e233..8c38a5374 100644 --- a/infer/src/pulse/PulseBaseMemory.ml +++ b/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 diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli index 55623429a..087a45f17 100644 --- a/infer/src/pulse/PulseBaseMemory.mli +++ b/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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index b5f959cce..e2470be61 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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