[AI] rename Domain.( <= ) to Domain.leq

Summary: The way `<=` is used in `AbstractDomain` prevents infix use and forces bracketing it everywhere.  Replace with simple `leq`.

Reviewed By: jvillard

Differential Revision: D18201854

fbshipit-source-id: 8175224e4
master
Nikos Gorogiannis 5 years ago committed by Facebook Github Bot
parent 50b60bc049
commit e9b0ca9ce4

@ -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

@ -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

@ -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

@ -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

@ -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 ;

@ -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

@ -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

@ -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)

@ -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

@ -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 =

@ -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

@ -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)

@ -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

@ -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

@ -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

@ -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 ->

@ -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

@ -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 =

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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 =

@ -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 =

@ -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 =

@ -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 =

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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 "@[<v>%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)

@ -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

@ -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

@ -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

@ -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 }" ;

@ -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

Loading…
Cancel
Save