From c2ec55fe37f780232e68f44d9b2b320a0d7ab5ed Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 30 Apr 2020 03:11:41 -0700 Subject: [PATCH] [pulse] remove traces from interval domain Summary: The idea was to keep track of why we know certain facts but actually these traces are never read. Other arithmetic facts (BoItv and the path condition) don't have histories so remove them from concrete intervals too. Reviewed By: dulmarod Differential Revision: D21303353 fbshipit-source-id: eecf07b05 --- infer/src/pulse/Pulse.ml | 4 +- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseArithmetic.ml | 92 ++++++------------- infer/src/pulse/PulseArithmetic.mli | 33 ++----- infer/src/pulse/PulseAttribute.ml | 24 ++--- infer/src/pulse/PulseAttribute.mli | 4 +- .../src/pulse/PulseBaseAddressAttributes.mli | 2 +- infer/src/pulse/PulseInterproc.ml | 6 +- infer/src/pulse/PulseModels.ml | 46 ++++------ infer/src/pulse/PulseOperations.ml | 24 +++-- infer/src/pulse/PulseOperations.mli | 8 +- infer/src/pulse/PulseTrace.ml | 7 -- infer/src/pulse/PulseTrace.mli | 2 - 13 files changed, 90 insertions(+), 164 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index dfc5fd173..9e75138b4 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -177,8 +177,8 @@ module PulseTransferFunctions = struct Ok astate in check_error_continue summary result - | Prune (condition, loc, is_then_branch, if_kind) -> - PulseOperations.prune ~is_then_branch if_kind loc ~condition astate + | Prune (condition, loc, _is_then_branch, _if_kind) -> + PulseOperations.prune loc ~condition astate |> check_error_transform summary ~f:(fun (exec_state, cond_satisfiable) -> if cond_satisfiable then (* [condition] is true or unknown value: go into the branch *) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 3cc540023..f76ff7927 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -137,7 +137,7 @@ module AddressAttributes : sig val std_vector_reserve : AbstractValue.t -> t -> t - val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option + val get_citv : AbstractValue.t -> t -> CItv.t option val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index b2b65dc7c..91eb16fc8 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -22,21 +22,21 @@ let and_term t astate = AbductiveDomain.set_path_condition phi astate -let and_nonnegative trace v astate = +let and_nonnegative v astate = AddressAttributes.add_one v (BoItv Itv.ItvPure.nat) astate - |> AddressAttributes.add_one v (CItv (CItv.zero_inf, trace)) + |> AddressAttributes.add_one v (CItv CItv.zero_inf) |> and_term PathCondition.Term.(le zero (of_absval v)) -let and_positive trace v astate = +let and_positive v astate = AddressAttributes.add_one v (BoItv Itv.ItvPure.pos) astate - |> AddressAttributes.add_one v (CItv (CItv.ge_to IntLit.one, trace)) + |> AddressAttributes.add_one v (CItv (CItv.ge_to IntLit.one)) |> and_term PathCondition.Term.(lt zero (of_absval v)) -let and_eq_int trace v i astate = +let and_eq_int v i astate = AddressAttributes.add_one v (BoItv (Itv.ItvPure.of_int_lit i)) astate - |> AddressAttributes.add_one v (CItv (CItv.equal_to i, trace)) + |> AddressAttributes.add_one v (CItv (CItv.equal_to i)) |> and_eq_terms (PathCondition.Term.of_absval v) (PathCondition.Term.of_intlit i) @@ -44,13 +44,13 @@ let and_eq_int trace v i astate = type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t -let eval_citv_operand location binop_addr binop_hist bop op_lhs op_rhs astate = +let eval_citv_operand binop_addr bop op_lhs op_rhs astate = let citv_of_op op astate = match op with | LiteralOperand i -> Some (CItv.equal_to i) | AbstractValueOperand v -> - AddressAttributes.get_citv v astate |> Option.map ~f:fst + AddressAttributes.get_citv v astate in match Option.both (citv_of_op op_lhs astate) (citv_of_op op_rhs astate) @@ -59,8 +59,7 @@ let eval_citv_operand location binop_addr binop_hist bop op_lhs op_rhs astate = | None -> astate | Some binop_a -> - let binop_trace = Trace.Immediate {location; history= binop_hist} in - let astate = AddressAttributes.add_one binop_addr (CItv (binop_a, binop_trace)) astate in + let astate = AddressAttributes.add_one binop_addr (CItv binop_a) astate in astate @@ -91,26 +90,20 @@ let eval_path_condition_binop binop_addr binop op_lhs op_rhs astate = astate -let eval_binop location binop op_lhs op_rhs binop_hist astate = - let binop_addr = AbstractValue.mk_fresh () in - let astate = - eval_path_condition_binop binop_addr binop op_lhs op_rhs astate - |> eval_citv_operand location binop_addr binop_hist binop op_lhs op_rhs - |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs - in - (astate, (binop_addr, binop_hist)) +let eval_binop binop_addr binop op_lhs op_rhs astate = + eval_path_condition_binop binop_addr binop op_lhs op_rhs astate + |> eval_citv_operand binop_addr binop op_lhs op_rhs + |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs -let eval_unop_citv location unop_addr unop operand_addr unop_hist astate = +let eval_unop_citv unop_addr unop operand_addr astate = match - AddressAttributes.get_citv operand_addr astate - |> Option.bind ~f:(function a, _ -> CItv.unop unop a) + AddressAttributes.get_citv operand_addr astate |> Option.bind ~f:(fun a -> CItv.unop unop a) with | None -> astate | Some unop_a -> - let unop_trace = Trace.Immediate {location; history= unop_hist} in - AddressAttributes.add_one unop_addr (CItv (unop_a, unop_trace)) astate + AddressAttributes.add_one unop_addr (CItv unop_a) astate let eval_unop_bo_itv unop_addr unop operand_addr astate = @@ -128,14 +121,10 @@ let eval_path_condition_unop unop_addr unop addr astate = astate -let eval_unop location unop addr unop_hist astate = - let unop_addr = AbstractValue.mk_fresh () in - let astate = - eval_path_condition_unop unop_addr unop addr astate - |> eval_unop_citv location unop_addr unop addr unop_hist - |> eval_unop_bo_itv unop_addr unop addr - in - (astate, (unop_addr, unop_hist)) +let eval_unop unop_addr unop addr astate = + eval_path_condition_unop unop_addr unop addr astate + |> eval_unop_citv unop_addr unop addr + |> eval_unop_bo_itv unop_addr unop addr let prune_with_bop ~negated v_opt arith bop arith' astate = @@ -157,13 +146,9 @@ let prune_with_bop ~negated v_opt arith bop arith' astate = (astate, true) -let eval_operand location astate = function +let eval_operand astate = function | LiteralOperand i -> - ( None - , Some - (CItv.equal_to i, Trace.Immediate {location; history= [ValueHistory.Assignment location]}) - , Itv.ItvPure.of_int_lit i - , PathCondition.Term.of_intlit i ) + (None, Some (CItv.equal_to i), Itv.ItvPure.of_int_lit i, PathCondition.Term.of_intlit i) | AbstractValueOperand v -> ( Some v , AddressAttributes.get_citv v astate @@ -171,32 +156,21 @@ let eval_operand location astate = function , PathCondition.Term.of_absval v ) -let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate = +let record_abduced addr_opt arith_opt astate = match Option.both addr_opt arith_opt with | None -> astate | Some (addr, arith) -> - let trace = - match orig_arith_hist_opt with - | None -> - Trace.Immediate {location; history= [event]} - | Some (_, trace) -> - Trace.add_event event trace - in - let attribute = Attribute.CItv (arith, trace) in + let attribute = Attribute.CItv arith in AddressAttributes.abduce_attribute addr attribute astate |> AddressAttributes.add_one addr attribute let bind_satisfiable ~satisfiable astate ~f = if satisfiable then f astate else (astate, false) -let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op astate = - let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = - eval_operand location astate lhs_op - in - let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = - eval_operand location astate rhs_op - in +let prune_binop ~negated bop lhs_op rhs_op astate = + let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = eval_operand astate lhs_op in + let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand astate rhs_op in let astate = let path_condition = let t_positive = PathCondition.Term.of_binop bop path_cond_lhs path_cond_rhs in @@ -205,17 +179,12 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta in AbductiveDomain.set_path_condition path_condition astate in - match - CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt) - (Option.map ~f:fst arith_rhs_opt) - with + match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with | Unsatisfiable -> (astate, false) | Satisfiable (abduced_lhs, abduced_rhs) -> - let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in let astate = - record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate - |> record_abduced event location value_rhs_opt arith_rhs_opt abduced_rhs + record_abduced value_lhs_opt abduced_lhs astate |> record_abduced value_rhs_opt abduced_rhs in let satisfiable = match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with @@ -240,8 +209,7 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta (** {2 Queries} *) let is_known_zero astate v = - ( AddressAttributes.get_citv v astate - |> function Some (arith, _) -> CItv.is_equal_to_zero arith | None -> false ) + AddressAttributes.get_citv v astate |> Option.value_map ~default:false ~f:CItv.is_equal_to_zero || (let phi = astate.AbductiveDomain.path_condition in PathCondition.is_known_zero (PathCondition.Term.of_absval v) phi ) || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv v astate) diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 02f140ca3..d2c05158a 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -11,13 +11,13 @@ module AbductiveDomain = PulseAbductiveDomain (** {2 Building arithmetic constraints} *) -val and_nonnegative : Trace.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t -(** [and_nonnegative trace v astate] is [astate ∧ v≥0] *) +val and_nonnegative : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +(** [and_nonnegative v astate] is [astate ∧ v≥0] *) -val and_positive : Trace.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +val and_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t (** [and_positive v astate] is [astate ∧ v>0] *) -val and_eq_int : Trace.t -> AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t +val and_eq_int : AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t (** [and_eq_int v i astate] is [astate ∧ v=i] *) (** {2 Operations} *) @@ -25,32 +25,13 @@ val and_eq_int : Trace.t -> AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t val eval_binop : - Location.t - -> Binop.t - -> operand - -> operand - -> ValueHistory.t - -> AbductiveDomain.t - -> AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) + AbstractValue.t -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t val eval_unop : - Location.t - -> Unop.t - -> AbstractValue.t - -> ValueHistory.t - -> AbductiveDomain.t - -> AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) + AbstractValue.t -> Unop.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t val prune_binop : - is_then_branch:bool - -> Sil.if_kind - -> Location.t - -> negated:bool - -> Binop.t - -> operand - -> operand - -> AbductiveDomain.t - -> AbductiveDomain.t * bool + negated:bool -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t * bool (** {2 Queries} *) diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 501a40d41..54fa8c03d 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 | Allocated of Procname.t * Trace.t - | CItv of CItv.t * Trace.t + | CItv of CItv.t | BoItv of Itv.ItvPure.t | Closure of Procname.t | Invalid of Invalidation.t * Trace.t @@ -63,7 +63,7 @@ module Attribute = struct let std_vector_reserve_rank = Variants.to_rank StdVectorReserve - let const_rank = Variants.to_rank (CItv (CItv.equal_to IntLit.zero, dummy_trace)) + let citv_rank = Variants.to_rank (CItv (CItv.equal_to IntLit.zero)) let bo_itv_rank = Variants.to_rank (BoItv Itv.ItvPure.zero) @@ -87,8 +87,8 @@ module Attribute = struct F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv | Closure pname -> Procname.pp f pname - | CItv (phi, trace) -> - F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> CItv.pp fmt phi)) trace + | CItv phi -> + F.fprintf f "Arith %a" CItv.pp phi | Invalid (invalidation, trace) -> F.fprintf f "Invalid %a" (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation)) @@ -156,10 +156,10 @@ module Attributes = struct let get_citv attrs = - Set.find_rank attrs Attribute.const_rank + Set.find_rank attrs Attribute.citv_rank |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.CItv (a, trace)) = attr in - (a, trace) ) + let[@warning "-8"] (Attribute.CItv a) = attr in + a ) let get_bo_itv attrs = @@ -190,14 +190,16 @@ let is_suitable_for_pre = function let map_trace ~f = function | Allocated (procname, trace) -> Allocated (procname, f trace) - | CItv (arith, trace) -> - CItv (arith, f trace) | Invalid (invalidation, trace) -> Invalid (invalidation, f trace) | MustBeValid trace -> MustBeValid (f trace) | WrittenTo trace -> WrittenTo (f trace) - | (AddressOfCppTemporary _ | AddressOfStackVariable _ | BoItv _ | Closure _ | StdVectorReserve) as - attr -> + | ( AddressOfCppTemporary _ + | AddressOfStackVariable _ + | BoItv _ + | CItv _ + | Closure _ + | StdVectorReserve ) as attr -> attr diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 4a57d692c..5daa502fb 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -16,7 +16,7 @@ type t = | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t | Allocated of Procname.t * Trace.t (** the {!Procname.t} is the function causing the allocation, eg [malloc] *) - | CItv of CItv.t * Trace.t + | CItv of CItv.t | BoItv of Itv.ItvPure.t | Closure of Procname.t | Invalid of Invalidation.t * Trace.t @@ -41,7 +41,7 @@ module Attributes : sig val get_allocation : t -> (Procname.t * Trace.t) option - val get_citv : t -> (CItv.t * Trace.t) option + val get_citv : t -> CItv.t option val get_bo_itv : t -> Itv.ItvPure.t option diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 1a3a46cac..90fed44c6 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -32,7 +32,7 @@ val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location. val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option -val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option +val get_citv : AbstractValue.t -> t -> CItv.t option val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 88802d5c7..6d48cc9f3 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -238,8 +238,8 @@ let eval_sym_of_subst astate subst s bound_end = let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee = match (attr : Attribute.t) with - | CItv (arith_callee, hist) -> ( - let arith_caller_opt = AddressAttributes.get_citv addr_caller astate |> Option.map ~f:fst in + | CItv arith_callee -> ( + let arith_caller_opt = AddressAttributes.get_citv addr_caller astate in match CItv.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) with | Unsatisfiable -> raise @@ -251,7 +251,7 @@ let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee = ; arith_callee= Some arith_callee ; call_state })) | Satisfiable (Some abduce_caller, _abduce_callee) -> - Attribute.CItv (abduce_caller, hist) + Attribute.CItv abduce_caller | Satisfiable (None, _) -> attr ) | BoItv itv -> ( diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 95680c6aa..d00b0b19b 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -40,19 +40,17 @@ module Misc = struct let return_int : Int64.t -> model = - fun i64 ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun i64 ~caller_summary:_ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> let i = IntLit.of_int64 i64 in let ret_addr = AbstractValue.Constants.get_int i in - let astate = PulseArithmetic.and_eq_int (Immediate {location; history= []}) ret_addr i astate in + let astate = PulseArithmetic.and_eq_int ret_addr i astate in PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue let return_unknown_size : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun ~caller_summary:_ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in - let astate = - PulseArithmetic.and_nonnegative (Immediate {location; history= []}) ret_addr astate - in + let astate = PulseArithmetic.and_nonnegative ret_addr astate in PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue @@ -86,19 +84,17 @@ module C = struct let malloc _ : model = fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> - let hist = - [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}] - in - let immediate_hist = Trace.Immediate {location; history= hist} in let ret_addr = AbstractValue.mk_fresh () in - let ret_value = (ret_addr, hist) in + let ret_value = + (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) + in let astate = PulseOperations.write_id ret_id ret_value astate in let astate_alloc = - PulseArithmetic.and_positive immediate_hist ret_addr astate + PulseArithmetic.and_positive ret_addr astate |> PulseOperations.allocate callee_procname location ret_value in let+ astate_null = - PulseArithmetic.and_eq_int immediate_hist ret_addr IntLit.zero astate + PulseArithmetic.and_eq_int ret_addr IntLit.zero astate |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value in [ExecutionDomain.ContinueProgram astate_alloc; ExecutionDomain.ContinueProgram astate_null] @@ -107,14 +103,12 @@ module C = struct let malloc_not_null _ : model = fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in - let hist = - [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}] + let ret_value = + (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) in - let ret_value = (ret_addr, hist) in - let immediate_hist = Trace.Immediate {location; history= hist} in let astate = PulseOperations.write_id ret_id ret_value astate in PulseOperations.allocate callee_procname location ret_value astate - |> PulseArithmetic.and_positive immediate_hist ret_addr + |> PulseArithmetic.and_positive ret_addr |> PulseOperations.ok_continue @@ -173,15 +167,15 @@ module StdAtomicInteger = struct let arith_bop prepost location event ret_id bop this operand astate = - let* astate, int_addr, (old_int, old_int_hist) = load_backing_int location this astate in - let astate, (new_int, hist) = - PulseArithmetic.eval_binop location bop (AbstractValueOperand old_int) operand old_int_hist - astate + let* astate, int_addr, (old_int, hist) = load_backing_int location this astate in + let bop_addr = AbstractValue.mk_fresh () in + let astate = + PulseArithmetic.eval_binop bop_addr bop (AbstractValueOperand old_int) operand astate in let+ astate = - PulseOperations.write_deref location ~ref:int_addr ~obj:(new_int, event :: hist) astate + PulseOperations.write_deref location ~ref:int_addr ~obj:(bop_addr, event :: hist) astate in - let ret_int = match prepost with `Pre -> new_int | `Post -> old_int in + let ret_int = match prepost with `Pre -> bop_addr | `Post -> old_int in PulseOperations.write_id ret_id (ret_int, event :: hist) astate @@ -478,9 +472,7 @@ module StdVector = struct fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::vector::begin()"; location; in_call= []} in let index_zero = AbstractValue.mk_fresh () in - let astate = - PulseArithmetic.and_eq_int (Immediate {location; history= []}) index_zero IntLit.zero astate - in + let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in let* astate, ((arr_addr, _) as arr) = GenericArrayBackedCollection.eval location vector astate in diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 58d52f00b..9b340fa1e 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -135,7 +135,7 @@ let eval location exp0 astate = | Const (Cint i) -> let v = AbstractValue.Constants.get_int i in let astate = - PulseArithmetic.and_eq_int (Immediate {location; history= []}) v i astate + PulseArithmetic.and_eq_int v i astate |> AddressAttributes.invalidate (v, [ValueHistory.Assignment location]) (ConstantDereference i) location @@ -143,17 +143,16 @@ let eval location exp0 astate = Ok (astate, (v, [])) | UnOp (unop, exp, _typ) -> let+ astate, (addr, hist) = eval exp astate in - PulseArithmetic.eval_unop location unop addr hist astate + let unop_addr = AbstractValue.mk_fresh () in + (PulseArithmetic.eval_unop unop_addr unop addr astate, (unop_addr, hist)) | BinOp (bop, e_lhs, e_rhs) -> let* astate, (addr_lhs, hist_lhs) = eval e_lhs astate in - let+ ( astate - , ( addr_rhs - , (* NOTE: arbitrarily track only the history of the lhs, maybe not the brightest idea *) - _ ) ) = - eval e_rhs astate - in - PulseArithmetic.eval_binop location bop (AbstractValueOperand addr_lhs) - (AbstractValueOperand addr_rhs) hist_lhs astate + (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *) + let+ astate, (addr_rhs, _hist_rhs) = eval e_rhs astate in + let binop_addr = AbstractValue.mk_fresh () in + ( PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs) + (AbstractValueOperand addr_rhs) astate + , (binop_addr, hist_lhs) ) | Const _ | Sizeof _ | Exn _ -> Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) in @@ -169,14 +168,13 @@ let eval_to_operand location exp astate = (astate, PulseArithmetic.AbstractValueOperand value) -let prune ~is_then_branch if_kind location ~condition astate = +let prune location ~condition astate = let rec prune_aux ~negated exp astate = match (exp : Exp.t) with | BinOp (bop, exp_lhs, exp_rhs) -> let* astate, lhs_op = eval_to_operand location exp_lhs astate in let+ astate, rhs_op = eval_to_operand location exp_rhs astate in - PulseArithmetic.prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op - astate + PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate | UnOp (LNot, exp', _) -> prune_aux ~negated:(not negated) exp' astate | exp -> diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index a8383324c..26a98f5fb 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -27,13 +27,7 @@ val eval : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) Return an error state if it traverses some known invalid address or if the end destination is known to be invalid. *) -val prune : - is_then_branch:bool - -> Sil.if_kind - -> Location.t - -> condition:Exp.t - -> t - -> (t * bool) access_result +val prune : Location.t -> condition:Exp.t -> t -> (t * bool) access_result val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result (** Like [eval] but evaluates [*exp]. *) diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml index 40204c87f..1ae4fe6cd 100644 --- a/infer/src/pulse/PulseTrace.ml +++ b/infer/src/pulse/PulseTrace.ml @@ -36,13 +36,6 @@ let rec pp ~pp_immediate fmt trace = F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp ~pp_immediate) in_call -let add_event event = function - | Immediate {location; history} -> - Immediate {location; history= event :: history} - | ViaCall {f; in_call; location; history} -> - ViaCall {f; in_call; location; history= event :: history} - - let rec add_to_errlog ?(include_value_history = true) ~nesting ~pp_immediate trace errlog = match trace with | Immediate {location; history} -> diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli index 2d16c319c..5795a530b 100644 --- a/infer/src/pulse/PulseTrace.mli +++ b/infer/src/pulse/PulseTrace.mli @@ -27,8 +27,6 @@ val get_outer_location : t -> Location.t val get_start_location : t -> Location.t (** initial step in the history if not empty, or else same as {!get_outer_location} *) -val add_event : ValueHistory.event -> t -> t - val add_to_errlog : ?include_value_history:bool -> nesting:int