diff --git a/infer/src/IR/AccessPath.ml b/infer/src/IR/AccessPath.ml index 5d65faaf2..4ad8b78d8 100644 --- a/infer/src/IR/AccessPath.ml +++ b/infer/src/IR/AccessPath.ml @@ -251,7 +251,7 @@ module Abs = struct let is_exact = function Exact _ -> true | Abstracted _ -> false - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = match (lhs, rhs) with | Abstracted _, Exact _ -> false diff --git a/infer/src/IR/AccessPath.mli b/infer/src/IR/AccessPath.mli index 1ce7eb29e..833ffd515 100644 --- a/infer/src/IR/AccessPath.mli +++ b/infer/src/IR/AccessPath.mli @@ -111,7 +111,7 @@ module Abs : sig val is_exact : t -> bool (** return true if [t] is an exact representation of an access path, false if it's an abstraction *) - val ( <= ) : lhs:t -> rhs:t -> bool + val leq : lhs:t -> rhs:t -> bool (** return true if \gamma(lhs) \subseteq \gamma(rhs) *) val pp : Format.formatter -> t -> unit diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 9bc3cb33c..27b9654b4 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -23,7 +23,7 @@ exception Stop_analysis module type NoJoin = sig include PrettyPrintable.PrintableType - val ( <= ) : lhs:t -> rhs:t -> bool + val leq : lhs:t -> rhs:t -> bool end module type S = sig @@ -37,7 +37,7 @@ end module Empty : S with type t = unit = struct type t = unit - let ( <= ) ~lhs:() ~rhs:() = true + let leq ~lhs:() ~rhs:() = true let join () () = () @@ -63,7 +63,7 @@ module type WithTop = sig end module BottomLiftedUtils = struct - let ( <= ) ~le ~lhs ~rhs = + let leq ~leq ~lhs ~rhs = if phys_equal lhs rhs then true else match (lhs, rhs) with @@ -72,7 +72,7 @@ module BottomLiftedUtils = struct | _, Bottom -> false | NonBottom lhs, NonBottom rhs -> - le ~lhs ~rhs + leq ~lhs ~rhs let map ~f astate = @@ -96,7 +96,7 @@ module BottomLifted (Domain : S) = struct let is_bottom = function Bottom -> true | NonBottom _ -> false - let ( <= ) = BottomLiftedUtils.( <= ) ~le:Domain.( <= ) + let leq = BottomLiftedUtils.leq ~leq:Domain.leq let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 @@ -128,7 +128,7 @@ module BottomLifted (Domain : S) = struct end module TopLiftedUtils = struct - let ( <= ) ~le ~lhs ~rhs = + let leq ~leq ~lhs ~rhs = if phys_equal lhs rhs then true else match (lhs, rhs) with @@ -137,7 +137,7 @@ module TopLiftedUtils = struct | Top, _ -> false | NonTop lhs, NonTop rhs -> - le ~lhs ~rhs + leq ~lhs ~rhs let pp_top f = F.pp_print_string f SpecialChars.down_tack @@ -152,7 +152,7 @@ module TopLifted (Domain : S) = struct let is_top = function Top -> true | _ -> false - let ( <= ) = TopLiftedUtils.( <= ) ~le:Domain.( <= ) + let leq = TopLiftedUtils.leq ~leq:Domain.leq let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 @@ -180,10 +180,9 @@ end module Pair (Domain1 : S) (Domain2 : S) = struct type t = Domain1.t * Domain2.t - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true - else - Domain1.( <= ) ~lhs:(fst lhs) ~rhs:(fst rhs) && Domain2.( <= ) ~lhs:(snd lhs) ~rhs:(snd rhs) + else Domain1.leq ~lhs:(fst lhs) ~rhs:(fst rhs) && Domain2.leq ~lhs:(snd lhs) ~rhs:(snd rhs) let join astate1 astate2 = @@ -218,7 +217,7 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) = struct let is_top = function Top -> true | _ -> false - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = phys_equal lhs rhs || match (lhs, rhs) with @@ -271,18 +270,18 @@ module StackedUtils = struct cmp_above a1 a2 - let ( <= ) ~le_below ~le_above ~lhs ~rhs = + let leq ~leq_below ~leq_above ~lhs ~rhs = phys_equal lhs rhs || match (lhs, rhs) with | Below lhs, Below rhs -> - le_below ~lhs ~rhs + leq_below ~lhs ~rhs | Below _, Above _ -> true | Above _, Below _ -> false | Above lhs, Above rhs -> - le_above ~lhs ~rhs + leq_above ~lhs ~rhs let combine ~dir x1 x2 ~f_below ~f_above = @@ -305,7 +304,7 @@ end module Stacked (Below : S) (Above : S) = struct type t = (Below.t, Above.t) below_above - let ( <= ) = StackedUtils.( <= ) ~le_below:Below.( <= ) ~le_above:Above.( <= ) + let leq = StackedUtils.leq ~leq_below:Below.leq ~leq_above:Above.leq let join = StackedUtils.combine ~dir:`Increasing ~f_below:Below.join ~f_above:Above.join @@ -327,7 +326,7 @@ module MinReprSet (Element : PrettyPrintable.PrintableOrderedType) = struct let is_bottom = Option.is_none - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = match (lhs, rhs) with | None, _ -> true @@ -382,7 +381,7 @@ module FiniteSetOfPPSet (S : PrettyPrintable.PPSet) = struct let is_bottom = is_empty - let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else subset lhs rhs + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else subset lhs rhs let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else union astate1 astate2 @@ -405,7 +404,7 @@ module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) = struct let is_top = is_empty - let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else subset rhs lhs + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else subset rhs lhs let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else inter astate1 astate2 @@ -430,12 +429,12 @@ module MapOfPPMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct let is_bottom = is_empty (** true if all keys in [lhs] are in [rhs], and each lhs value <= corresponding rhs value *) - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else M.for_all (fun k lhs_v -> - try ValueDomain.( <= ) ~lhs:lhs_v ~rhs:(M.find k rhs) with Caml.Not_found -> false ) + try ValueDomain.leq ~lhs:lhs_v ~rhs:(M.find k rhs) with Caml.Not_found -> false ) lhs @@ -493,10 +492,10 @@ module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S let is_top = is_empty - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else - try for_all (fun k rhs_v -> ValueDomain.( <= ) ~lhs:(find k lhs) ~rhs:rhs_v) rhs + try for_all (fun k rhs_v -> ValueDomain.leq ~lhs:(find k lhs) ~rhs:rhs_v) rhs with Caml.Not_found -> false @@ -637,7 +636,7 @@ struct let pp = M.pp - let ( <= ) = M.( <= ) + let leq = M.leq let inter ~f astate1 astate2 = if phys_equal astate1 astate2 then astate1 @@ -692,7 +691,7 @@ struct let is_bottom = M.is_empty - let ( <= ) = M.( <= ) + let leq = M.leq let join = M.join @@ -720,7 +719,7 @@ end module BooleanAnd = struct type t = bool - let ( <= ) ~lhs ~rhs = lhs || not rhs + let leq ~lhs ~rhs = lhs || not rhs let join = ( && ) @@ -736,7 +735,7 @@ module BooleanOr = struct let is_bottom astate = not astate - let ( <= ) ~lhs ~rhs = (not lhs) || rhs + let leq ~lhs ~rhs = (not lhs) || rhs let join = ( || ) @@ -763,7 +762,7 @@ module CountDomain (MaxCount : MaxCount) = struct let is_bottom = Int.equal bottom - let ( <= ) ~lhs ~rhs = lhs <= rhs + let leq ~lhs ~rhs = lhs <= rhs let join astate1 astate2 = Int.min top (Int.max astate1 astate2) @@ -792,7 +791,7 @@ module DownwardIntDomain (MaxCount : MaxCount) = struct let is_bottom = Int.equal bottom - let ( <= ) ~lhs ~rhs = lhs >= rhs + let leq ~lhs ~rhs = lhs >= rhs let join astate1 astate2 = Int.min astate1 astate2 diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 2de4a5696..da4003043 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -26,7 +26,7 @@ exception Stop_analysis module type NoJoin = sig include PrettyPrintable.PrintableType - val ( <= ) : lhs:t -> rhs:t -> bool + val leq : lhs:t -> rhs:t -> bool (** the implication relation: [lhs <= rhs] means [lhs |- rhs] *) end @@ -104,9 +104,9 @@ include end module StackedUtils : sig - val ( <= ) : - le_below:(lhs:'b -> rhs:'b -> bool) - -> le_above:(lhs:'a -> rhs:'a -> bool) + val leq : + leq_below:(lhs:'b -> rhs:'b -> bool) + -> leq_above:(lhs:'a -> rhs:'a -> bool) -> lhs:('b, 'a) below_above -> rhs:('b, 'a) below_above -> bool diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index b0a7c211e..dd4a11966 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -212,10 +212,10 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s if if is_narrowing then (old_state.State.visit_count :> int) > Config.max_narrows - || Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre - else Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre + || Domain.leq ~lhs:old_state.State.pre ~rhs:new_pre + else Domain.leq ~lhs:new_pre ~rhs:old_state.State.pre then (inv_map, ReachedFixPoint) - else if is_narrowing && not (Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) then ( + else if is_narrowing && not (Domain.leq ~lhs:new_pre ~rhs:old_state.State.pre) then ( L.(debug Analysis Verbose) "Terminate narrowing because old and new states are not comparable at %a:%a@." Typ.Procname.pp (Summary.get_proc_name summary) Node.pp_id node_id ; diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 20b39f427..f0f0e5bac 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -93,7 +93,7 @@ module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveCon let rev_filter_not_over_approximated disjuncts ~not_in = List.rev_filter disjuncts ~f:(fun disjunct -> List.exists not_in ~f:(fun disj_not_in -> - TransferFunctions.Domain.( <= ) ~lhs:disjunct.astate ~rhs:disj_not_in.astate ) + TransferFunctions.Domain.leq ~lhs:disjunct.astate ~rhs:disj_not_in.astate ) |> not ) @@ -137,7 +137,7 @@ module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveCon false - let ( <= ) ~lhs ~rhs = phys_equal lhs rhs || is_trivial_subset lhs ~of_:rhs + let leq ~lhs ~rhs = phys_equal lhs rhs || is_trivial_subset lhs ~of_:rhs let widen ~prev ~next ~num_iters = let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in @@ -145,7 +145,7 @@ module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveCon else let visited_prev = set_visited true prev in let post = join_up_to_imply visited_prev next in - if ( <= ) ~lhs:post ~rhs:prev then set_visited false prev else post + if leq ~lhs:post ~rhs:prev then set_visited false prev else post let pp = Disjuncts.pp diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 6ec345279..d0f3d3ea7 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -66,7 +66,7 @@ module ArrInfo = struct Top - let ( <= ) : lhs:t -> rhs:t -> bool = + let leq : lhs:t -> rhs:t -> bool = fun ~lhs ~rhs -> if phys_equal lhs rhs then true else diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 0f208c6fb..23d600c3f 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -1167,7 +1167,7 @@ end module NonNegativeBound = struct type t = Bound.t * BoundTrace.t [@@deriving compare] - let ( <= ) ~lhs:(bound_lhs, _) ~rhs:(bound_rhs, _) = Bound.le bound_lhs bound_rhs + let leq ~lhs:(bound_lhs, _) ~rhs:(bound_rhs, _) = Bound.le bound_lhs bound_rhs let join (bound_x, trace_x) (bound_y, trace_y) = (Bound.overapprox_max bound_x bound_y, BoundTrace.join trace_x trace_y) diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index d614e971a..6c586b8e9 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -132,7 +132,7 @@ type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't module NonNegativeBound : sig type t [@@deriving compare] - val ( <= ) : lhs:t -> rhs:t -> bool + val leq : lhs:t -> rhs:t -> bool val join : t -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 7d0eac088..36a704aac 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -33,7 +33,7 @@ end) module ItvUpdatedBy = struct type t = Addition | Multiplication | Top - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = match (lhs, rhs) with | Addition, _ -> true @@ -47,7 +47,7 @@ module ItvUpdatedBy = struct true - let join x y = if ( <= ) ~lhs:x ~rhs:y then y else x + let join x y = if leq ~lhs:x ~rhs:y then y else x let widen ~prev ~next ~num_iters:_ = join prev next @@ -149,18 +149,18 @@ module Val = struct ; traces } - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else - Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv - && ItvThresholds.( <= ) ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds - && ItvUpdatedBy.( <= ) ~lhs:lhs.itv_updated_by ~rhs:rhs.itv_updated_by - && ModeledRange.( <= ) ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range - && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym - && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc - && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk - && Relation.Sym.( <= ) ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym - && Relation.Sym.( <= ) ~lhs:lhs.size_sym ~rhs:rhs.size_sym + Itv.leq ~lhs:lhs.itv ~rhs:rhs.itv + && ItvThresholds.leq ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds + && ItvUpdatedBy.leq ~lhs:lhs.itv_updated_by ~rhs:rhs.itv_updated_by + && ModeledRange.leq ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range + && Relation.Sym.leq ~lhs:lhs.sym ~rhs:rhs.sym + && PowLoc.leq ~lhs:lhs.powloc ~rhs:rhs.powloc + && ArrayBlk.leq ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk + && Relation.Sym.leq ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym + && Relation.Sym.leq ~lhs:lhs.size_sym ~rhs:rhs.size_sym let widen ~prev ~next ~num_iters = @@ -951,7 +951,7 @@ module AliasTarget = struct Some Top - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = equal lhs rhs || match (lhs, rhs) with @@ -1180,9 +1180,9 @@ end module Alias = struct type t = {map: AliasMap.t; ret: AliasRet.t} - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true - else AliasMap.( <= ) ~lhs:lhs.map ~rhs:rhs.map && AliasRet.( <= ) ~lhs:lhs.ret ~rhs:rhs.ret + else AliasMap.leq ~lhs:lhs.map ~rhs:rhs.map && AliasRet.leq ~lhs:lhs.ret ~rhs:rhs.ret let join x y = @@ -1335,14 +1335,14 @@ end module PruningExp = struct type t = Unknown | Binop of {bop: Binop.t; lhs: CoreVal.t; rhs: CoreVal.t} [@@deriving compare] - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = match (lhs, rhs) with | _, Unknown -> true | Unknown, _ -> false | Binop {bop= bop1; lhs= lhs1; rhs= rhs1}, Binop {bop= bop2; lhs= lhs2; rhs= rhs2} -> - Binop.equal bop1 bop2 && Val.( <= ) ~lhs:lhs1 ~rhs:lhs2 && Val.( <= ) ~lhs:rhs1 ~rhs:rhs2 + Binop.equal bop1 bop2 && Val.leq ~lhs:lhs1 ~rhs:lhs2 && Val.leq ~lhs:rhs1 ~rhs:rhs2 let join x y = @@ -1386,7 +1386,7 @@ module PruningExp = struct let is_empty = - let le_false v = Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:Itv.zero in + let le_false v = Itv.leq ~lhs:(Val.get_itv v) ~rhs:Itv.zero in function | Unknown -> false @@ -1420,8 +1420,8 @@ end module PrunedVal = struct type t = {v: CoreVal.t; pruning_exp: PruningExp.t} [@@deriving compare] - let ( <= ) ~lhs ~rhs = - Val.( <= ) ~lhs:lhs.v ~rhs:rhs.v && PruningExp.( <= ) ~lhs:lhs.pruning_exp ~rhs:rhs.pruning_exp + let leq ~lhs ~rhs = + Val.leq ~lhs:lhs.v ~rhs:rhs.v && PruningExp.leq ~lhs:lhs.pruning_exp ~rhs:rhs.pruning_exp let join x y = {v= Val.join x.v y.v; pruning_exp= PruningExp.join x.pruning_exp y.pruning_exp} @@ -1523,7 +1523,7 @@ module LatestPrune = struct F.fprintf fmt "LatestPrune: ret(%a) %a / %a" Ident.pp v PrunePairs.pp p1 PrunePairs.pp p2 - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else match (lhs, rhs) with @@ -1532,29 +1532,29 @@ module LatestPrune = struct | Top, _ -> false | Latest p1, Latest p2 -> - PrunePairs.( <= ) ~lhs:p1 ~rhs:p2 + PrunePairs.leq ~lhs:p1 ~rhs:p2 | TrueBranch (x1, p1), TrueBranch (x2, p2) | FalseBranch (x1, p1), FalseBranch (x2, p2) | TrueBranch (x1, p1), V (x2, p2, _) | FalseBranch (x1, p1), V (x2, _, p2) -> - Pvar.equal x1 x2 && PrunePairs.( <= ) ~lhs:p1 ~rhs:p2 + Pvar.equal x1 x2 && PrunePairs.leq ~lhs:p1 ~rhs:p2 | V (x1, ptrue1, pfalse1), V (x2, ptrue2, pfalse2) -> Pvar.equal x1 x2 - && PrunePairs.( <= ) ~lhs:ptrue1 ~rhs:ptrue2 - && PrunePairs.( <= ) ~lhs:pfalse1 ~rhs:pfalse2 + && PrunePairs.leq ~lhs:ptrue1 ~rhs:ptrue2 + && PrunePairs.leq ~lhs:pfalse1 ~rhs:pfalse2 | VRet (x1, ptrue1, pfalse1), VRet (x2, ptrue2, pfalse2) -> Ident.equal x1 x2 - && PrunePairs.( <= ) ~lhs:ptrue1 ~rhs:ptrue2 - && PrunePairs.( <= ) ~lhs:pfalse1 ~rhs:pfalse2 + && PrunePairs.leq ~lhs:ptrue1 ~rhs:ptrue2 + && PrunePairs.leq ~lhs:pfalse1 ~rhs:pfalse2 | _, _ -> false let join x y = match (x, y) with - | _, _ when ( <= ) ~lhs:x ~rhs:y -> + | _, _ when leq ~lhs:x ~rhs:y -> y - | _, _ when ( <= ) ~lhs:y ~rhs:x -> + | _, _ when leq ~lhs:y ~rhs:x -> x | Latest p1, Latest p2 -> Latest (PrunePairs.join p1 p2) @@ -1713,14 +1713,14 @@ module MemReach = struct ; oenv= GOption.GSome oenv } - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else - StackLocs.( <= ) ~lhs:lhs.stack_locs ~rhs:rhs.stack_locs - && MemPure.( <= ) ~lhs:lhs.mem_pure ~rhs:rhs.mem_pure - && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias - && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune - && Relation.( <= ) ~lhs:lhs.relation ~rhs:rhs.relation + StackLocs.leq ~lhs:lhs.stack_locs ~rhs:rhs.stack_locs + && MemPure.leq ~lhs:lhs.mem_pure ~rhs:rhs.mem_pure + && Alias.leq ~lhs:lhs.alias ~rhs:rhs.alias + && LatestPrune.leq ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune + && Relation.leq ~lhs:lhs.relation ~rhs:rhs.relation let widen ~prev ~next ~num_iters = @@ -2113,7 +2113,7 @@ module Mem = struct let is_exc_raised = function ExcRaised -> true | _ -> false - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else match (lhs, rhs) with @@ -2126,7 +2126,7 @@ module Mem = struct | _, ExcRaised -> false | NonBottom lhs, NonBottom rhs -> - MemReach.( <= ) ~lhs ~rhs + MemReach.leq ~lhs ~rhs let join x y = diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml index a59a0463c..6ead94fb0 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml @@ -126,7 +126,7 @@ module NoRelation = struct let f3_false _ _ _ = false - let ( <= ) ~lhs:() ~rhs:() = true + let leq ~lhs:() ~rhs:() = true let join = f2 @@ -980,7 +980,7 @@ module Make (Manager : Manager_S) = struct let pp fmt x = Abstract1.print fmt x - let ( <= ) ~lhs ~rhs = sync_env_lift (Abstract1.is_leq man) lhs rhs + let leq ~lhs ~rhs = sync_env_lift (Abstract1.is_leq man) lhs rhs let sat_tcons tcons x = let tcons = Constraints.remove_strict_ineq_tcons1 tcons in @@ -1213,7 +1213,7 @@ module Make (Manager : Manager_S) = struct let ge_than_lhs pack_id rhs = match PackMap.find pack_id lhs with | lhs -> - Val.( <= ) ~lhs ~rhs + Val.leq ~lhs ~rhs | exception Caml.Not_found -> Val.is_top rhs in @@ -1247,7 +1247,7 @@ module Make (Manager : Manager_S) = struct PackMap.merge widen_opt prev next - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = let _, packs_lhs, packs_rhs = sync_pack lhs rhs in le_synced_packs ~lhs:packs_lhs ~rhs:packs_rhs diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 57d880d98..7a1a99cd7 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -729,7 +729,7 @@ module Prune = struct let is_unreachable_constant : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> bool = fun integer_type_widths e m -> let v = eval integer_type_widths e m in - Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) + Itv.leq ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) && PowLoc.is_bot (Val.get_pow_loc v) && ArrayBlk.is_bot (Val.get_array_blk v) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index ae66e1109..63495a510 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -226,7 +226,7 @@ module Exec = struct let set_c_strlen1 allocsite arrinfo acc = let loc = Loc.of_allocsite allocsite in let idx = Dom.Val.of_itv ~traces (ArrayBlk.ArrInfo.offsetof arrinfo) in - if Itv.( <= ) ~lhs:Itv.zero ~rhs:src_itv then Dom.Mem.set_first_idx_of_null loc idx acc + if Itv.leq ~lhs:Itv.zero ~rhs:src_itv then Dom.Mem.set_first_idx_of_null loc idx acc else Dom.Mem.unset_first_idx_of_null loc idx acc in ArrayBlk.fold set_c_strlen1 (Dom.Val.get_array_blk tgt) mem diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml index efae6a0f8..d5a965a92 100644 --- a/infer/src/bufferoverrun/ints.ml +++ b/infer/src/bufferoverrun/ints.ml @@ -73,7 +73,7 @@ module NonNegativeInt = struct let to_int_exn = Z.to_int - let ( <= ) ~lhs ~rhs = lhs <= rhs + let leq ~lhs ~rhs = lhs <= rhs let succ = Z.succ diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli index ed348de04..14d9a0c3f 100644 --- a/infer/src/bufferoverrun/ints.mli +++ b/infer/src/bufferoverrun/ints.mli @@ -63,7 +63,7 @@ module NonNegativeInt : sig val is_one : t -> bool - val ( <= ) : lhs:t -> rhs:t -> bool + val leq : lhs:t -> rhs:t -> bool val succ : t -> t diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 6980abaa6..a6e024c5e 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -53,7 +53,7 @@ module ItvPure = struct let exists_str ~f (l, u) = Bound.exists_str ~f l || Bound.exists_str ~f u - let ( <= ) : lhs:t -> rhs:t -> bool = + let leq : lhs:t -> rhs:t -> bool = fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Bound.le l2 l1 && Bound.le u1 u2 @@ -545,9 +545,9 @@ let of_int_lit : IntLit.t -> t = fun n -> of_big_int (IntLit.to_big_int n) let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false -let le : lhs:t -> rhs:t -> bool = ( <= ) +let le : lhs:t -> rhs:t -> bool = leq -let eq : t -> t -> bool = fun x y -> ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x +let eq : t -> t -> bool = fun x y -> leq ~lhs:x ~rhs:y && leq ~lhs:y ~rhs:x let range loop_head : t -> ItvRange.t = function | Bottom -> diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 3165d4604..f6c9c8986 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -57,7 +57,7 @@ module ItvPure : sig val is_le_mone : t -> bool - val ( <= ) : lhs:t -> rhs:t -> bool + val leq : lhs:t -> rhs:t -> bool val have_similar_bounds : t -> t -> bool diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 062c3aa66..cca90a6a9 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -292,13 +292,12 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct (* assumes symbols are not comparable *) - let rec ( <= ) : lhs:t -> rhs:t -> bool = + let rec leq : lhs:t -> rhs:t -> bool = fun ~lhs ~rhs -> phys_equal lhs rhs - || NonNegativeInt.( <= ) ~lhs:lhs.const ~rhs:rhs.const - && M.le ~le_elt:( <= ) lhs.terms rhs.terms + || (NonNegativeInt.leq ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:leq lhs.terms rhs.terms) || Option.exists (int_ub lhs) ~f:(fun lhs_ub -> - NonNegativeInt.( <= ) ~lhs:lhs_ub ~rhs:(int_lb rhs) ) + NonNegativeInt.leq ~lhs:lhs_ub ~rhs:(int_lb rhs) ) let rec xcompare ~lhs ~rhs = @@ -317,7 +316,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct let p' = mask_min_max_constant p in M.update (S.mask_min_max_constant s) (function - | None -> Some p' | Some p -> if ( <= ) ~lhs:p ~rhs:p' then Some p' else Some p ) + | None -> Some p' | Some p -> if leq ~lhs:p ~rhs:p' then Some p' else Some p ) acc ) terms M.empty } @@ -499,9 +498,9 @@ module NonNegativePolynomial = struct type degree_with_term = (Degree.t * NonNegativeNonTopPolynomial.t, TopTraces.t) AbstractDomain.Types.below_above - let ( <= ) = - AbstractDomain.StackedUtils.( <= ) ~le_below:NonNegativeNonTopPolynomial.( <= ) - ~le_above:TopTraces.( <= ) + let leq = + AbstractDomain.StackedUtils.leq ~leq_below:NonNegativeNonTopPolynomial.leq + ~leq_above:TopTraces.leq let pp ~hum = diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index d0cfa9c09..3f96fa6e8 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/infer/src/bufferoverrun/polynomials.mli @@ -41,7 +41,7 @@ module NonNegativePolynomial : sig val pp_hum : Format.formatter -> t -> unit - val ( <= ) : lhs:t -> rhs:t -> bool + val leq : lhs:t -> rhs:t -> bool val top : t diff --git a/infer/src/checkers/Bindings.ml b/infer/src/checkers/Bindings.ml index 0e0c0982f..045a2bb51 100644 --- a/infer/src/checkers/Bindings.ml +++ b/infer/src/checkers/Bindings.ml @@ -100,7 +100,7 @@ let pp f {resolve; reverse} = Reverse.pp reverse -let ( <= ) ~lhs ~rhs = IdAccessPathMapDomain.( <= ) ~lhs:lhs.resolve ~rhs:rhs.resolve +let leq ~lhs ~rhs = IdAccessPathMapDomain.leq ~lhs:lhs.resolve ~rhs:rhs.resolve let join bindings1 bindings2 = if phys_equal bindings1 bindings2 then bindings1 diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index f410c5056..dc468ba6a 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -32,7 +32,7 @@ let check_invariant ap1 ap2 = function HilExp.AccessExpression.pp ap2 -let ( <= ) ~lhs ~rhs = +let leq ~lhs ~rhs = if phys_equal lhs rhs then true else IdMap.for_all diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml index 879484d0a..2808d7d69 100644 --- a/infer/src/checkers/Trace.ml +++ b/infer/src/checkers/Trace.ml @@ -162,12 +162,12 @@ module Make (Spec : Spec) = struct type t = {known: Known.t; footprint: Footprint.t; sanitizers: Sanitizers.t} - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else - Known.( <= ) ~lhs:lhs.known ~rhs:rhs.known - && Footprint.( <= ) ~lhs:lhs.footprint ~rhs:rhs.footprint - && Sanitizers.( <= ) ~lhs:lhs.sanitizers ~rhs:rhs.sanitizers + Known.leq ~lhs:lhs.known ~rhs:rhs.known + && Footprint.leq ~lhs:lhs.footprint ~rhs:rhs.footprint + && Sanitizers.leq ~lhs:lhs.sanitizers ~rhs:rhs.sanitizers let join astate1 astate2 = @@ -546,9 +546,9 @@ module Make (Spec : Spec) = struct {sources; sinks; passthroughs} - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = phys_equal lhs rhs - || Sources.( <= ) ~lhs:lhs.sources ~rhs:rhs.sources + || Sources.leq ~lhs:lhs.sources ~rhs:rhs.sources && Sinks.subset lhs.sinks rhs.sinks && Passthroughs.subset lhs.passthroughs rhs.passthroughs diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml index 6a947d6c8..dc1d658a2 100644 --- a/infer/src/checkers/accessPathDomains.ml +++ b/infer/src/checkers/accessPathDomains.ml @@ -24,9 +24,8 @@ module Set = struct APSet.filter (fun lhs -> not - (APSet.exists - (fun rhs -> (not (phys_equal lhs rhs)) && AccessPath.Abs.( <= ) ~lhs ~rhs) - aps) ) + (APSet.exists (fun rhs -> (not (phys_equal lhs rhs)) && AccessPath.Abs.leq ~lhs ~rhs) aps) + ) aps @@ -35,18 +34,17 @@ module Set = struct let of_list = APSet.of_list let mem ap aps = - APSet.mem ap aps - || APSet.exists (fun other_ap -> AccessPath.Abs.( <= ) ~lhs:ap ~rhs:other_ap) aps + APSet.mem ap aps || APSet.exists (fun other_ap -> AccessPath.Abs.leq ~lhs:ap ~rhs:other_ap) aps let mem_fuzzy ap aps = let has_overlap ap1 ap2 = - AccessPath.Abs.( <= ) ~lhs:ap1 ~rhs:ap2 || AccessPath.Abs.( <= ) ~lhs:ap2 ~rhs:ap1 + AccessPath.Abs.leq ~lhs:ap1 ~rhs:ap2 || AccessPath.Abs.leq ~lhs:ap2 ~rhs:ap1 in APSet.mem ap aps || APSet.exists (has_overlap ap) aps - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else let rhs_contains lhs_ap = mem lhs_ap rhs in diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 7788cdb7e..cd433b468 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -176,7 +176,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct let rec access_tree_lteq ((lhs_trace, lhs_tree) as lhs) ((rhs_trace, rhs_tree) as rhs) = if phys_equal lhs rhs then true else - TraceDomain.( <= ) ~lhs:lhs_trace ~rhs:rhs_trace + TraceDomain.leq ~lhs:lhs_trace ~rhs:rhs_trace && match (lhs_tree, rhs_tree) with | Subtree lhs_subtree, Subtree rhs_subtree -> @@ -193,7 +193,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct false - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else BaseMap.for_all diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 9e2a6683a..1ebbb128f 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -315,7 +315,7 @@ module ControlFlowCost = struct let f sum = let cost_of_sum = Sum.cost ~of_item sum in let new_cost = BasicCost.min_default_left t.cost cost_of_sum in - if not (BasicCost.( <= ) ~lhs:t.cost ~rhs:new_cost) then ( + if not (BasicCost.leq ~lhs:t.cost ~rhs:new_cost) then ( on_improve sum cost_of_sum new_cost ; t.cost <- new_cost ) in @@ -325,7 +325,7 @@ module ControlFlowCost = struct let improve_cost_with t cost' = let old_cost = t.cost in let new_cost = BasicCost.min_default_left old_cost cost' in - if not (BasicCost.( <= ) ~lhs:old_cost ~rhs:new_cost) then ( + if not (BasicCost.leq ~lhs:old_cost ~rhs:new_cost) then ( t.cost <- new_cost ; Some old_cost ) else None @@ -652,7 +652,7 @@ module WorstCaseCost = struct subsequent 'don't know's. Instead, we report Top cost only at the top level per function. *) let should_report_cost cost ~threshold = - (not (BasicCost.is_top cost)) && not (BasicCost.( <= ) ~lhs:cost ~rhs:threshold) + (not (BasicCost.is_top cost)) && not (BasicCost.leq ~lhs:cost ~rhs:threshold) let exec_node tenv {costs; reports} extras instr_node = diff --git a/infer/src/checkers/uninitDomain.ml b/infer/src/checkers/uninitDomain.ml index 2d6ae9f0f..52df4a24e 100644 --- a/infer/src/checkers/uninitDomain.ml +++ b/infer/src/checkers/uninitDomain.ml @@ -100,7 +100,7 @@ module Record struct type t = {maybe_uninit_vars: Domain1.t; aliased_vars: Domain2.t; prepost: Domain3.t prepost} - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = if phys_equal lhs rhs then true else let {maybe_uninit_vars= lhs_uv; aliased_vars= lhs_av; prepost= {pre= lhs_pre; post= lhs_post}} @@ -111,10 +111,10 @@ struct = rhs in - Domain1.( <= ) ~lhs:lhs_uv ~rhs:rhs_uv - && Domain2.( <= ) ~lhs:lhs_av ~rhs:rhs_av - && Domain3.( <= ) ~lhs:lhs_pre ~rhs:rhs_pre - && Domain3.( <= ) ~lhs:lhs_post ~rhs:rhs_post + Domain1.leq ~lhs:lhs_uv ~rhs:rhs_uv + && Domain2.leq ~lhs:lhs_av ~rhs:rhs_av + && Domain3.leq ~lhs:lhs_pre ~rhs:rhs_pre + && Domain3.leq ~lhs:lhs_post ~rhs:rhs_post let join astate1 astate2 = diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index f9d6f4bcf..54be60197 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -187,7 +187,7 @@ module ThreadsDomain = struct let bottom = NoThread (* NoThread < AnyThreadButSelf < Any *) - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = phys_equal lhs rhs || match (lhs, rhs) with @@ -319,7 +319,7 @@ module OwnershipAbstractValue = struct let make_owned_if formal_index = OwnedIf (IntSet.singleton formal_index) - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = phys_equal lhs rhs || match (lhs, rhs) with @@ -518,13 +518,13 @@ let is_bottom {threads; locks; accesses; ownership; attribute_map} = && AttributeMapDomain.is_empty attribute_map -let ( <= ) ~lhs ~rhs = +let leq ~lhs ~rhs = if phys_equal lhs rhs then true else - ThreadsDomain.( <= ) ~lhs:lhs.threads ~rhs:rhs.threads - && LocksDomain.( <= ) ~lhs:lhs.locks ~rhs:rhs.locks - && AccessDomain.( <= ) ~lhs:lhs.accesses ~rhs:rhs.accesses - && AttributeMapDomain.( <= ) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map + ThreadsDomain.leq ~lhs:lhs.threads ~rhs:rhs.threads + && LocksDomain.leq ~lhs:lhs.locks ~rhs:rhs.locks + && AccessDomain.leq ~lhs:lhs.accesses ~rhs:rhs.accesses + && AttributeMapDomain.leq ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map let join astate1 astate2 = diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 056bef0c5..b5870b320 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -22,7 +22,7 @@ module ThreadDomain = struct match (st1, st2) with AnyThread, _ | _, AnyThread -> AnyThread | _, _ -> UIThread - let ( <= ) ~lhs ~rhs = match (lhs, rhs) with AnyThread, UIThread -> false | _, _ -> true + let leq ~lhs ~rhs = match (lhs, rhs) with AnyThread, UIThread -> false | _, _ -> true let widen ~prev ~next ~num_iters:_ = join prev next @@ -191,7 +191,7 @@ end = struct {map; acquisitions} - let ( <= ) ~lhs ~rhs = Map.( <= ) ~lhs:lhs.map ~rhs:rhs.map + let leq ~lhs ~rhs = Map.leq ~lhs:lhs.map ~rhs:rhs.map let top = {map= Map.top; acquisitions= Acquisitions.empty} @@ -444,11 +444,11 @@ let join lhs rhs = let widen ~prev ~next ~num_iters:_ = join prev next -let ( <= ) ~lhs ~rhs = - GuardToLockMap.( <= ) ~lhs:lhs.guard_map ~rhs:rhs.guard_map - && LockState.( <= ) ~lhs:lhs.lock_state ~rhs:rhs.lock_state - && CriticalPairs.( <= ) ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs - && ThreadDomain.( <= ) ~lhs:lhs.thread ~rhs:rhs.thread +let leq ~lhs ~rhs = + GuardToLockMap.leq ~lhs:lhs.guard_map ~rhs:rhs.guard_map + && LockState.leq ~lhs:lhs.lock_state ~rhs:rhs.lock_state + && CriticalPairs.leq ~lhs:lhs.critical_pairs ~rhs:rhs.critical_pairs + && ThreadDomain.leq ~lhs:lhs.thread ~rhs:rhs.thread let add_critical_pair tenv_opt lock_state event thread ~loc acc = diff --git a/infer/src/labs/00_dummy_checker/ResourceLeakDomain.ml b/infer/src/labs/00_dummy_checker/ResourceLeakDomain.ml index d9108510f..43cad302b 100644 --- a/infer/src/labs/00_dummy_checker/ResourceLeakDomain.ml +++ b/infer/src/labs/00_dummy_checker/ResourceLeakDomain.ml @@ -10,7 +10,7 @@ module F = Format type t = unit -let ( <= ) ~lhs:_ ~rhs:_ = assert false +let leq ~lhs:_ ~rhs:_ = assert false let join _a _b = assert false diff --git a/infer/src/labs/01_integer_domain/ResourceLeakDomain.ml b/infer/src/labs/01_integer_domain/ResourceLeakDomain.ml index 675257c37..400b7f300 100644 --- a/infer/src/labs/01_integer_domain/ResourceLeakDomain.ml +++ b/infer/src/labs/01_integer_domain/ResourceLeakDomain.ml @@ -10,7 +10,7 @@ module F = Format type t = int -let ( <= ) ~lhs ~rhs = lhs <= rhs +let leq ~lhs ~rhs = lhs <= rhs let join _a _b = assert false diff --git a/infer/src/labs/02_domain_join/ResourceLeakDomain.ml b/infer/src/labs/02_domain_join/ResourceLeakDomain.ml index 98c0c3f10..3828e29da 100644 --- a/infer/src/labs/02_domain_join/ResourceLeakDomain.ml +++ b/infer/src/labs/02_domain_join/ResourceLeakDomain.ml @@ -10,7 +10,7 @@ module F = Format type t = int -let ( <= ) ~lhs ~rhs = lhs <= rhs +let leq ~lhs ~rhs = lhs <= rhs let join a b = max a b diff --git a/infer/src/labs/03_domain_top/ResourceLeakDomain.ml b/infer/src/labs/03_domain_top/ResourceLeakDomain.ml index c86c01c48..c259dc4d3 100644 --- a/infer/src/labs/03_domain_top/ResourceLeakDomain.ml +++ b/infer/src/labs/03_domain_top/ResourceLeakDomain.ml @@ -11,7 +11,7 @@ module F = Format module FiniteBounds = struct type t = int - let ( <= ) ~lhs ~rhs = lhs <= rhs + let leq ~lhs ~rhs = lhs <= rhs let join a b = max a b diff --git a/infer/src/labs/04_interprocedural/ResourceLeakDomain.ml b/infer/src/labs/04_interprocedural/ResourceLeakDomain.ml index 47047aa4b..4ebf10fe3 100644 --- a/infer/src/labs/04_interprocedural/ResourceLeakDomain.ml +++ b/infer/src/labs/04_interprocedural/ResourceLeakDomain.ml @@ -11,7 +11,7 @@ module F = Format module FiniteBounds = struct type t = int - let ( <= ) ~lhs ~rhs = lhs <= rhs + let leq ~lhs ~rhs = lhs <= rhs let join a b = max a b diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml b/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml index 5bd5bc011..f133d3cff 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeakDomain.ml @@ -11,7 +11,7 @@ module F = Format module FiniteBounds = struct type t = int - let ( <= ) ~lhs ~rhs = lhs <= rhs + let leq ~lhs ~rhs = lhs <= rhs let join a b = max a b diff --git a/infer/src/labs/ResourceLeakDomain.ml b/infer/src/labs/ResourceLeakDomain.ml index d9108510f..43cad302b 100644 --- a/infer/src/labs/ResourceLeakDomain.ml +++ b/infer/src/labs/ResourceLeakDomain.ml @@ -10,7 +10,7 @@ module F = Format type t = unit -let ( <= ) ~lhs:_ ~rhs:_ = assert false +let leq ~lhs:_ ~rhs:_ = assert false let join _a _b = assert false diff --git a/infer/src/nullsafe/NullabilitySuggest.ml b/infer/src/nullsafe/NullabilitySuggest.ml index c76c9fa9e..c1e7a3a3d 100644 --- a/infer/src/nullsafe/NullabilitySuggest.ml +++ b/infer/src/nullsafe/NullabilitySuggest.ml @@ -16,11 +16,11 @@ module UseDefChain = struct | NullDefAssign of (Location.t * AccessPath.t) [@@deriving compare] - let ( <= ) ~lhs ~rhs = compare lhs rhs <= 0 + let leq ~lhs ~rhs = compare lhs rhs <= 0 (* Keep only one chain in join/widen as we are going to report only one * trace to the user eventually. *) - let join lhs rhs = if ( <= ) ~lhs ~rhs then rhs else lhs + let join lhs rhs = if leq ~lhs ~rhs then rhs else lhs let widen ~prev ~next ~num_iters:_ = join prev next diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 182e875f0..6bd3a1a70 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -61,7 +61,7 @@ module InvertedDomain : BaseDomain = struct let pp = BaseDomain.pp (** inverted lattice *) - let ( <= ) ~lhs ~rhs = BaseDomain.( <= ) ~rhs:lhs ~lhs:rhs + let leq ~lhs ~rhs = BaseDomain.leq ~rhs:lhs ~lhs:rhs end (** biabduction-style pre/post state *) @@ -71,7 +71,7 @@ type t = let pp f {post; pre} = F.fprintf f "@[%a@;PRE=[%a]@]" Domain.pp post InvertedDomain.pp pre -let ( <= ) ~lhs ~rhs = +let leq ~lhs ~rhs = match BaseDomain.isograph_map BaseDomain.empty_mapping ~lhs:(rhs.pre :> BaseDomain.t) diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index 92ae35dd2..57dbfafaf 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -168,7 +168,7 @@ module GraphComparison = struct match isograph_map ~lhs ~rhs mapping with IsomorphicUpTo _ -> true | NotIsomorphic -> false end -let ( <= ) ~lhs ~rhs = +let leq ~lhs ~rhs = phys_equal lhs rhs || GraphComparison.is_isograph ~lhs ~rhs GraphComparison.empty_mapping diff --git a/infer/src/unit/TraceTests.ml b/infer/src/unit/TraceTests.ml index 335d961ce..46ed4a14a 100644 --- a/infer/src/unit/TraceTests.ml +++ b/infer/src/unit/TraceTests.ml @@ -82,7 +82,7 @@ module MockTrace = Trace.Make (struct else None end) -let trace_equal t1 t2 = MockTrace.( <= ) ~lhs:t1 ~rhs:t2 && MockTrace.( <= ) ~lhs:t2 ~rhs:t1 +let trace_equal t1 t2 = MockTrace.leq ~lhs:t1 ~rhs:t2 && MockTrace.leq ~lhs:t2 ~rhs:t1 let source_equal s source = MockSource.equal s source diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 5dd58881a..adcb7cd1f 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -22,7 +22,7 @@ module PathCountDomain = struct let initial = make_path_count 1 - let ( <= ) ~lhs ~rhs = + let leq ~lhs ~rhs = match (lhs, rhs) with | PathCount c1, PathCount c2 -> c1 <= c2 diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index 994bdab45..96f379638 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -117,10 +117,10 @@ let tests = assert_bool "extract" (AccessPath.equal (AccessPath.Abs.extract xF_exact) xF) ; assert_bool "is_exact" (AccessPath.Abs.is_exact x_exact) ; assert_bool "not is_exact" (not (AccessPath.Abs.is_exact x_abstract)) ; - assert_bool "(<=)1" (AccessPath.Abs.( <= ) ~lhs:x_exact ~rhs:x_abstract) ; - assert_bool "(<=)2" (AccessPath.Abs.( <= ) ~lhs:xF_exact ~rhs:x_abstract) ; - assert_bool "not (<=)1" (not (AccessPath.Abs.( <= ) ~lhs:x_abstract ~rhs:x_exact)) ; - assert_bool "not (<=)2" (not (AccessPath.Abs.( <= ) ~lhs:x_abstract ~rhs:xF_exact)) + assert_bool "(<=)1" (AccessPath.Abs.leq ~lhs:x_exact ~rhs:x_abstract) ; + assert_bool "(<=)2" (AccessPath.Abs.leq ~lhs:xF_exact ~rhs:x_abstract) ; + assert_bool "not (<=)1" (not (AccessPath.Abs.leq ~lhs:x_abstract ~rhs:x_exact)) ; + assert_bool "not (<=)2" (not (AccessPath.Abs.leq ~lhs:x_abstract ~rhs:xF_exact)) in "abstraction" >:: abstraction_test_ in @@ -151,11 +151,11 @@ let tests = (* [mem_fuzzy] should behave the same as [mem] except in this case *) assert_bool "mem_fuzzy_not_fully_contained" (AccessPathDomains.Set.mem_fuzzy yF_abstract aps3) ; - assert_bool "<= on same is true" (AccessPathDomains.Set.( <= ) ~lhs:aps1 ~rhs:aps1) ; - assert_bool "aps1 <= aps2" (AccessPathDomains.Set.( <= ) ~lhs:aps1 ~rhs:aps2) ; - assert_bool "aps2 <= aps1" (AccessPathDomains.Set.( <= ) ~lhs:aps2 ~rhs:aps1) ; - assert_bool "aps1 <= aps3" (AccessPathDomains.Set.( <= ) ~lhs:aps1 ~rhs:aps3) ; - assert_bool "not aps3 <= aps1" (not (AccessPathDomains.Set.( <= ) ~lhs:aps3 ~rhs:aps1)) ; + assert_bool "<= on same is true" (AccessPathDomains.Set.leq ~lhs:aps1 ~rhs:aps1) ; + assert_bool "aps1 <= aps2" (AccessPathDomains.Set.leq ~lhs:aps1 ~rhs:aps2) ; + assert_bool "aps2 <= aps1" (AccessPathDomains.Set.leq ~lhs:aps2 ~rhs:aps1) ; + assert_bool "aps1 <= aps3" (AccessPathDomains.Set.leq ~lhs:aps1 ~rhs:aps3) ; + assert_bool "not aps3 <= aps1" (not (AccessPathDomains.Set.leq ~lhs:aps3 ~rhs:aps1)) ; assert_eq (AccessPathDomains.Set.join aps1 aps1) "{ x*, x }" ; assert_eq (AccessPathDomains.Set.join aps1 aps2) "{ x*, x, x.f }" ; assert_eq (AccessPathDomains.Set.join aps1 aps3) "{ x*, x, x.f, y.f }" ; diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 7fd621aec..baccf3c60 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -295,25 +295,25 @@ let tests = let lteq_test = let lteq_test_ _ = (* regular tree tests *) - assert_bool "<= equal;" (Domain.( <= ) ~lhs:tree ~rhs:tree) ; - assert_bool "<= bases" (Domain.( <= ) ~lhs:x_base_tree ~rhs:x_y_base_tree) ; - assert_bool "<= regular1" (Domain.( <= ) ~lhs:x_base_tree ~rhs:xFG_tree) ; - assert_bool "<= regular2" (Domain.( <= ) ~lhs:xFG_tree ~rhs:tree) ; - assert_bool "<= regular3" (Domain.( <= ) ~lhs:y_base_tree ~rhs:tree) ; - assert_bool "<= bases negative1" (not (Domain.( <= ) ~lhs:x_y_base_tree ~rhs:x_base_tree)) ; - assert_bool "<= bases negative2" (not (Domain.( <= ) ~lhs:x_base_tree ~rhs:y_base_tree)) ; - assert_bool "<= negative1" (not (Domain.( <= ) ~lhs:xFG_tree ~rhs:y_base_tree)) ; - assert_bool "<= negative2" (not (Domain.( <= ) ~lhs:tree ~rhs:xFG_tree)) ; + assert_bool "<= equal;" (Domain.leq ~lhs:tree ~rhs:tree) ; + assert_bool "<= bases" (Domain.leq ~lhs:x_base_tree ~rhs:x_y_base_tree) ; + assert_bool "<= regular1" (Domain.leq ~lhs:x_base_tree ~rhs:xFG_tree) ; + assert_bool "<= regular2" (Domain.leq ~lhs:xFG_tree ~rhs:tree) ; + assert_bool "<= regular3" (Domain.leq ~lhs:y_base_tree ~rhs:tree) ; + assert_bool "<= bases negative1" (not (Domain.leq ~lhs:x_y_base_tree ~rhs:x_base_tree)) ; + assert_bool "<= bases negative2" (not (Domain.leq ~lhs:x_base_tree ~rhs:y_base_tree)) ; + assert_bool "<= negative1" (not (Domain.leq ~lhs:xFG_tree ~rhs:y_base_tree)) ; + assert_bool "<= negative2" (not (Domain.leq ~lhs:tree ~rhs:xFG_tree)) ; (* star tree tests *) - assert_bool "<= star lhs equal" (Domain.( <= ) ~lhs:x_star_tree ~rhs:x_star_tree) ; - assert_bool "<= star rhs1" (Domain.( <= ) ~lhs:x_base_tree ~rhs:x_star_tree) ; - assert_bool "<= star rhs2" (Domain.( <= ) ~lhs:xFG_tree ~rhs:x_star_tree) ; - assert_bool "<= star rhs3" (Domain.( <= ) ~lhs:y_base_tree ~rhs:yF_star_tree) ; - assert_bool "<= star rhs4" (Domain.( <= ) ~lhs:yF_star_tree ~rhs:tree) ; - assert_bool "<= star lhs negative1" (not (Domain.( <= ) ~lhs:x_star_tree ~rhs:x_base_tree)) ; - assert_bool "<= star lhs negative2" (not (Domain.( <= ) ~lhs:x_star_tree ~rhs:xFG_tree)) ; - assert_bool "<= star lhs negative3" (not (Domain.( <= ) ~lhs:yF_star_tree ~rhs:y_base_tree)) ; - assert_bool "<= star lhs negative4" (not (Domain.( <= ) ~lhs:tree ~rhs:yF_star_tree)) ; + assert_bool "<= star lhs equal" (Domain.leq ~lhs:x_star_tree ~rhs:x_star_tree) ; + assert_bool "<= star rhs1" (Domain.leq ~lhs:x_base_tree ~rhs:x_star_tree) ; + assert_bool "<= star rhs2" (Domain.leq ~lhs:xFG_tree ~rhs:x_star_tree) ; + assert_bool "<= star rhs3" (Domain.leq ~lhs:y_base_tree ~rhs:yF_star_tree) ; + assert_bool "<= star rhs4" (Domain.leq ~lhs:yF_star_tree ~rhs:tree) ; + assert_bool "<= star lhs negative1" (not (Domain.leq ~lhs:x_star_tree ~rhs:x_base_tree)) ; + assert_bool "<= star lhs negative2" (not (Domain.leq ~lhs:x_star_tree ~rhs:xFG_tree)) ; + assert_bool "<= star lhs negative3" (not (Domain.leq ~lhs:yF_star_tree ~rhs:y_base_tree)) ; + assert_bool "<= star lhs negative4" (not (Domain.leq ~lhs:tree ~rhs:yF_star_tree)) ; (* <= tree but not <= trace tests *) (* same as x_base_tree, but with a trace higher in the traces lattice *) let x_base_tree_higher_trace = @@ -323,14 +323,13 @@ let tests = let x_star_tree_diff_trace = Domain.BaseMap.singleton x_base (Domain.make_starred_leaf y_trace) in - assert_bool "(x, {}) <= (x, {y})" - (Domain.( <= ) ~lhs:x_base_tree ~rhs:x_base_tree_higher_trace) ; + assert_bool "(x, {}) <= (x, {y})" (Domain.leq ~lhs:x_base_tree ~rhs:x_base_tree_higher_trace) ; assert_bool "(x, {y}) not <= (x, {})" - (not (Domain.( <= ) ~lhs:x_base_tree_higher_trace ~rhs:x_base_tree)) ; + (not (Domain.leq ~lhs:x_base_tree_higher_trace ~rhs:x_base_tree)) ; assert_bool "(x*, {y})* not <= (x*, {x})" - (not (Domain.( <= ) ~lhs:x_star_tree_diff_trace ~rhs:x_star_tree)) ; + (not (Domain.leq ~lhs:x_star_tree_diff_trace ~rhs:x_star_tree)) ; assert_bool "(x*, {x})* not <= (x*, {y})" - (not (Domain.( <= ) ~lhs:x_star_tree ~rhs:x_star_tree_diff_trace)) + (not (Domain.leq ~lhs:x_star_tree ~rhs:x_star_tree_diff_trace)) in "lteq" >:: lteq_test_ in