diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index d3446d458..6c90e7659 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -215,9 +215,7 @@ module AddressAttributes = struct BaseAddressAttributes.get_closure_proc_name addr (astate.post :> base_domain).attrs - let get_arithmetic addr astate = - BaseAddressAttributes.get_arithmetic addr (astate.post :> base_domain).attrs - + let get_citv addr astate = BaseAddressAttributes.get_citv addr (astate.post :> base_domain).attrs let get_bo_itv addr astate = BaseAddressAttributes.get_bo_itv addr (astate.post :> base_domain).attrs @@ -451,11 +449,11 @@ module PrePost = struct addresses [callee_addr] and [callee_addr'] that are distinct in the pre are aliased to a single address [caller_addr] in the caller's current state. Typically raised when calling [foo(z,z)] where the spec for [foo(x,y)] says that [x] and [y] are disjoint. *) - | Arithmetic of + | CItv of { addr_caller: AbstractValue.t ; addr_callee: AbstractValue.t - ; arith_caller: Arithmetic.t option - ; arith_callee: Arithmetic.t option + ; arith_caller: CItv.t option + ; arith_callee: CItv.t option ; call_state: call_state } (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller state *) @@ -475,11 +473,11 @@ module PrePost = struct "address %a in caller already bound to %a, not %a@\nnote: current call state was %a" AbstractValue.pp addr_caller AbstractValue.pp addr_callee' AbstractValue.pp addr_callee pp_call_state call_state - | Arithmetic {addr_caller; addr_callee; arith_caller; arith_callee; call_state} -> + | CItv {addr_caller; addr_callee; arith_caller; arith_callee; call_state} -> F.fprintf fmt "caller addr %a%a but callee addr %a%a; %a=%a is unsatisfiable@\n\ - note: current call state was %a" AbstractValue.pp addr_caller (Pp.option Arithmetic.pp) - arith_caller AbstractValue.pp addr_callee (Pp.option Arithmetic.pp) arith_callee + note: current call state was %a" AbstractValue.pp addr_caller (Pp.option CItv.pp) + arith_caller AbstractValue.pp addr_callee (Pp.option CItv.pp) arith_callee AbstractValue.pp addr_caller pp_call_state call_state AbstractValue.pp addr_callee | ArithmeticBo {addr_caller; addr_callee; arith_callee; call_state} -> F.fprintf fmt @@ -633,24 +631,20 @@ module PrePost = struct let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee = match (attr : Attribute.t) with - | Arithmetic (arith_callee, hist) -> ( - let arith_caller_opt = - AddressAttributes.get_arithmetic addr_caller astate |> Option.map ~f:fst - in - match - Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) - with + | CItv (arith_callee, hist) -> ( + let arith_caller_opt = AddressAttributes.get_citv addr_caller astate |> Option.map ~f:fst in + match CItv.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) with | Unsatisfiable -> raise (Contradiction - (Arithmetic + (CItv { addr_caller ; addr_callee ; arith_caller= arith_caller_opt ; arith_callee= Some arith_callee ; call_state })) | Satisfiable (Some abduce_caller, _abduce_callee) -> - Attribute.Arithmetic (abduce_caller, hist) + Attribute.CItv (abduce_caller, hist) | Satisfiable (None, _) -> attr ) | BoItv itv -> ( @@ -683,9 +677,8 @@ module PrePost = struct | Invalid (invalidation, trace) -> Attribute.Invalid (invalidation, add_call_to_trace proc_name call_location caller_history trace) - | Arithmetic (arith, trace) -> - Attribute.Arithmetic - (arith, add_call_to_trace proc_name call_location caller_history trace) + | CItv (arith, trace) -> + Attribute.CItv (arith, add_call_to_trace proc_name call_location caller_history trace) | Allocated trace -> Attribute.Allocated (add_call_to_trace proc_name call_location caller_history trace) | AddressOfCppTemporary _ diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 0f985d8f5..037261f60 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -84,7 +84,7 @@ module AddressAttributes : sig val std_vector_reserve : AbstractValue.t -> t -> t - val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option + val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index adf8415de..a77ff4fba 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -6,7 +6,7 @@ *) open! IStd module F = Format -module Arithmetic = PulseArithmetic +module CItv = PulseCItv module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory @@ -29,7 +29,7 @@ module Attribute = struct | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t | Allocated of Trace.t - | Arithmetic of Arithmetic.t * Trace.t + | CItv of CItv.t * Trace.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 (Arithmetic (Arithmetic.equal_to IntLit.zero, dummy_trace)) + let const_rank = Variants.to_rank (CItv (CItv.equal_to IntLit.zero, dummy_trace)) let bo_itv_rank = Variants.to_rank (BoItv Itv.ItvPure.zero) @@ -82,8 +82,8 @@ module Attribute = struct F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv | Closure pname -> Procname.pp f pname - | Arithmetic (phi, trace) -> - F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> Arithmetic.pp fmt phi)) trace + | CItv (phi, trace) -> + F.fprintf f "Arith %a" (Trace.pp ~pp_immediate:(fun fmt -> CItv.pp fmt phi)) trace | Invalid (invalidation, trace) -> F.fprintf f "Invalid %a" (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation)) @@ -143,10 +143,10 @@ module Attributes = struct || Option.is_some (Set.find_rank attrs Attribute.invalid_rank) - let get_arithmetic attrs = + let get_citv attrs = Set.find_rank attrs Attribute.const_rank |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.Arithmetic (a, trace)) = attr in + let[@warning "-8"] (Attribute.CItv (a, trace)) = attr in (a, trace) ) @@ -163,7 +163,7 @@ end include Attribute let is_suitable_for_pre = function - | Arithmetic _ | BoItv _ | MustBeValid _ -> + | CItv _ | BoItv _ | MustBeValid _ -> true | AddressOfCppTemporary _ | AddressOfStackVariable _ diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 6a56ad007..ab061475b 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -6,7 +6,7 @@ *) open! IStd module F = Format -module Arithmetic = PulseArithmetic +module CItv = PulseCItv module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory @@ -15,7 +15,7 @@ type t = | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t | Allocated of Trace.t - | Arithmetic of Arithmetic.t * Trace.t + | CItv of CItv.t * Trace.t | BoItv of Itv.ItvPure.t | Closure of Procname.t | Invalid of Invalidation.t * Trace.t @@ -35,7 +35,7 @@ module Attributes : sig val get_closure_proc_name : t -> Procname.t option - val get_arithmetic : t -> (Arithmetic.t * Trace.t) option + val get_citv : t -> (CItv.t * Trace.t) option val get_bo_itv : t -> Itv.ItvPure.t option diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 67fb3b83e..8f50e4aae 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -71,7 +71,7 @@ let get_attribute getter address attrs = let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name -let get_arithmetic = get_attribute Attributes.get_arithmetic +let get_citv = get_attribute Attributes.get_citv let get_bo_itv v memory = match get_attribute Attributes.get_bo_itv v memory with diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index a510ac6ed..28ff6ef32 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -30,7 +30,7 @@ val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location. val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option -val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option +val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index 451e74df6..845059973 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -9,10 +9,10 @@ open! IStd (** Basic Pulse modules that are safe to use in any module *) module AbstractValue = PulseAbstractValue -module Arithmetic = PulseArithmetic module Attribute = PulseAttribute module Attributes = PulseAttribute.Attributes module CallEvent = PulseCallEvent +module CItv = PulseCItv module Diagnostic = PulseDiagnostic module Invalidation = PulseInvalidation module Trace = PulseTrace diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseCItv.ml similarity index 90% rename from infer/src/pulse/PulseArithmetic.ml rename to infer/src/pulse/PulseCItv.ml index 7e562e111..d43568fba 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseCItv.ml @@ -5,8 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -[@@@ocamlformat "parse-docstrings = false"] - open! IStd module F = Format module L = Logging @@ -112,8 +110,8 @@ end module Unsafe : sig type t = private - | Between of Bound.t * Bound.t (** we write [b1,b2] for these *) - | Outside of IntLit.t * IntLit.t (** we write i1][i2 for these *) + | Between of Bound.t * Bound.t (** we write \[b1,b2\] for these *) + | Outside of IntLit.t * IntLit.t (** we write i1\]\[i2 for these *) [@@deriving compare] val between : Bound.t -> Bound.t -> t @@ -177,7 +175,7 @@ let has_empty_intersection a1 a2 = | Between (lower1, upper1), Between (lower2, upper2) -> Bound.lt upper1 lower2 || Bound.lt upper2 lower1 | Between (lower1, upper1), Outside (l2, u2) | Outside (l2, u2), Between (lower1, upper1) -> - (* is [l1, u1] inside [l2, u2]? *) + (* is \[l1, u1\] inside \[l2, u2\]? *) Bound.le (Int l2) lower1 && Bound.ge (Int u2) upper1 @@ -235,22 +233,22 @@ let rec abduce_eq (a1 : t) (a2 : t) = | Outside (l1, u1), Outside (l2, u2) -> (* ∃x. (xu1) ∧ (xu2) ∧ li<=ui*) (* all the possible cases: - x: --------[ ]--------- - y: -----[ ]-------- + x: --------\[ \]--------- + y: -----\[ \]-------- - x: ---[ ]------ - y: -----[ ]-------- + x: ---\[ \]------ + y: -----\[ \]-------- - x: ---[ ]---------- - y: -----[ ]-------- + x: ---\[ \]---------- + y: -----\[ \]-------- - x: ---------[ ]---- - y: -----[ ]-------- + x: ---------\[ \]---- + y: -----\[ \]-------- - -> SAT, can tighten both to min(l1,l2)][max(u1,u2) + -> SAT, can tighten both to min(l1,l2)\]\[max(u1,u2) - x: ---------------[ ]-- - y: -----[ ]-------- + x: ---------------\[ \]-- + y: -----\[ \]-------- or symmetrically x<->y => cannot express the 3 intervals that would be needed so return SAT (TODO: we might want to keep only one of these, which would be a kind of recency model of disequalities: remember the last known disequality) @@ -267,24 +265,24 @@ let rec abduce_eq (a1 : t) (a2 : t) = (* ∃x. l1≤x≤u1 ∧ (xu2) *) (* all the possible cases: - x: [-------] - y: --[ ]--- + x: \[-------\] + y: --\[ \]--- - case 1 above: SAT, cannot say more unless a1 is [-∞,+∞] (then we can abduce that a1 is + case 1 above: SAT, cannot say more unless a1 is \[-∞,+∞\] (then we can abduce that a1 is the same as a2) - x: [--] - y: ------[ ]-- + x: \[--\] + y: ------\[ \]-- case 2 above: UNSAT - x: [---] - y: ------[ ]-- + x: \[---\] + y: ------\[ \]-- case 3 above: SAT: x = x\cap y for both - x: [----] - y: ------[ ]-- + x: \[----\] + y: ------\[ \]-- case 4 above: SAT: x\cap y for both *) @@ -360,11 +358,11 @@ let abduce_le (a1 : t) (a2 : t) = (* two cases: 1. l1 (* similarly, two cases: 1. u1≥u2: can refine to x≤min(l1+1, u2) - x: -----[ ]--------------------- - y: ..-] - or y: ...-----] + x: -----\[ \]--------------------- + y: ..-\] + or y: ...-----\] 2. u1l2 *) diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseCItv.mli similarity index 97% rename from infer/src/pulse/PulseArithmetic.mli rename to infer/src/pulse/PulseCItv.mli index b53d2e34a..92fbbd863 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseCItv.mli @@ -7,6 +7,8 @@ open! IStd module F = Format +(** Concrete interval domain (CItv) *) + type t [@@deriving compare] val equal_to : IntLit.t -> t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 7e904bc50..dbcc755ae 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -43,7 +43,7 @@ module Misc = struct let i = IntLit.of_int64 i64 in AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit i)) astate |> AddressAttributes.add_one ret_addr - (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []})) + (CItv (CItv.equal_to i, Immediate {location; history= []})) in Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] @@ -54,7 +54,7 @@ module Misc = struct let astate = AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.nat) astate |> AddressAttributes.add_one ret_addr - (Arithmetic (Arithmetic.zero_inf, Immediate {location; history= []})) + (CItv (CItv.zero_inf, Immediate {location; history= []})) in Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] @@ -78,8 +78,8 @@ module C = struct (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we currently know about the value. This is purely to avoid contributing to path explosion. *) let is_known_zero = - ( AddressAttributes.get_arithmetic (fst deleted_access) astate - |> function Some (arith, _) -> Arithmetic.is_equal_to_zero arith | None -> false ) + ( AddressAttributes.get_citv (fst deleted_access) astate + |> function Some (arith, _) -> CItv.is_equal_to_zero arith | None -> false ) || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv (fst deleted_access) astate) in if is_known_zero then (* freeing 0 is a no-op *) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 5bfeace1f..2c043eeef 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -105,21 +105,19 @@ let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate = let arith_of_op op astate = match op with | LiteralOperand i -> - Some (Arithmetic.equal_to i) + Some (CItv.equal_to i) | AbstractValueOperand v -> - AddressAttributes.get_arithmetic v astate |> Option.map ~f:fst + AddressAttributes.get_citv v astate |> Option.map ~f:fst in match Option.both (arith_of_op op_lhs astate) (arith_of_op op_rhs astate) - |> Option.bind ~f:(fun (addr_lhs, addr_rhs) -> Arithmetic.binop bop addr_lhs addr_rhs) + |> Option.bind ~f:(fun (addr_lhs, addr_rhs) -> CItv.binop bop addr_lhs addr_rhs) with | None -> astate | Some binop_a -> let binop_trace = Trace.Immediate {location; history= binop_hist} in - let astate = - AddressAttributes.add_one binop_addr (Arithmetic (binop_a, binop_trace)) astate - in + let astate = AddressAttributes.add_one binop_addr (CItv (binop_a, binop_trace)) astate in astate @@ -148,14 +146,14 @@ let eval_binop location binop op_lhs op_rhs binop_hist astate = let eval_unop_arith location unop_addr unop operand_addr unop_hist astate = match - AddressAttributes.get_arithmetic operand_addr astate - |> Option.bind ~f:(function a, _ -> Arithmetic.unop unop a) + AddressAttributes.get_citv operand_addr astate + |> Option.bind ~f:(function 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 (Arithmetic (unop_a, unop_trace)) astate + AddressAttributes.add_one unop_addr (CItv (unop_a, unop_trace)) astate let eval_unop_bo_itv unop_addr unop operand_addr astate = @@ -210,7 +208,7 @@ let eval location exp0 astate = let addr = AbstractValue.mk_fresh () in let astate = AddressAttributes.add_one addr - (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []})) + (CItv (CItv.equal_to i, Immediate {location; history= []})) astate |> AddressAttributes.add_one addr (BoItv (Itv.ItvPure.of_int_lit i)) |> AddressAttributes.invalidate @@ -244,14 +242,14 @@ let eval_arith location exp astate = ( astate , None , Some - ( Arithmetic.equal_to i + ( CItv.equal_to i , Trace.Immediate {location; history= [ValueHistory.Assignment location]} ) , Itv.ItvPure.of_int_lit i ) | exp -> let+ astate, (value, _) = eval location exp astate in ( astate , Some value - , AddressAttributes.get_arithmetic value astate + , AddressAttributes.get_citv value astate , AddressAttributes.get_bo_itv value astate ) @@ -267,7 +265,7 @@ let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate | Some (_, trace) -> Trace.add_event event trace in - let attribute = Attribute.Arithmetic (arith, trace) in + let attribute = Attribute.CItv (arith, trace) in AddressAttributes.abduce_attribute addr attribute astate |> AddressAttributes.add_one addr attribute @@ -302,7 +300,7 @@ let prune ~is_then_branch if_kind location ~condition astate = eval_arith location exp_rhs astate in match - Arithmetic.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt) + CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt) (Option.map ~f:fst arith_rhs_opt) with | Unsatisfiable ->