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