package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ItvUtils.IntItvSource

IntItv - Intervals for arbitrary precision integers.

We rely on Zarith for arithmetic operations, and IntBounds to represent unbounded intervals.

Sourcemodule B = IntBound

Types

Sourcetype t = B.t * B.t

upper bound

The type of possibly empty intervals.

Sourceval is_valid : t -> bool

Constructors

Sourceval of_bound : B.t -> B.t -> t
Sourceval of_z : Z.t -> Z.t -> t
Sourceval of_int : int -> int -> t
Sourceval of_int64 : int64 -> int64 -> t

Constructs a non-empty interval.

Sourceval of_float : float -> float -> t

Constructs a non-empty interval.

Sourceval of_range : Z.t -> Z.t -> t
Sourceval of_bound_bot : B.t -> B.t -> t_with_bot
Sourceval of_range_bot : Z.t -> Z.t -> t_with_bot
Sourceval of_int_bot : int -> int -> t_with_bot
Sourceval of_int64_bot : int64 -> int64 -> t_with_bot

Constructs a possibly empty interval.

Sourceval of_float_bot : float -> float -> t_with_bot

Constructs a possibly empty interval.

Sourceval hull : B.t -> B.t -> t

Constructs the smallest interval containing a and b.

Sourceval cst : Z.t -> t

Singleton interval.

Sourceval cst_int : int -> t
Sourceval cst_int64 : int64 -> t
Sourceval zero : t

0,0

Sourceval one : t

1,1

Sourceval mone : t

-1,-1

Sourceval zero_one : t

0,1

Sourceval mone_zero : t

-1,0

Sourceval mone_one : t

-1,1

Sourceval zero_inf : t

0,+∞

Sourceval minf_zero : t

-∞,0

Sourceval minf_inf : t

-∞,+∞

Sourceval unsigned : int -> t
Sourceval unsigned8 : t
Sourceval unsigned16 : t
Sourceval unsigned32 : t
Sourceval unsigned64 : t

Intervals of unsigned integers with the specified bitsize.

Sourceval signed : int -> t
Sourceval signed8 : t
Sourceval signed16 : t
Sourceval signed32 : t
Sourceval signed64 : t

Intervals of two compement's integers with the specified bitsize.

Predicates

Sourceval equal : t -> t -> bool

Equality. = also works

Sourceval equal_bot : t_with_bot -> t_with_bot -> bool
Sourceval included : t -> t -> bool

Set ordering.

Sourceval included_bot : t_with_bot -> t_with_bot -> bool
Sourceval intersect : t -> t -> bool

Whether the intervals have an non-empty intersection.

Sourceval intersect_bot : t_with_bot -> t_with_bot -> bool
Sourceval contains : Z.t -> t -> bool

Whether the interval contains a (finite) value.

Sourceval compare : t -> t -> int

A total ordering (lexical ordering) returning -1, 0, or 1. Can be used as compare for sets, maps, etc.

Total ordering on possibly empty intervals.

Sourceval contains_zero : t -> bool

a,b contains 0.

Sourceval contains_one : t -> bool

a,b contains 1.

Sourceval contains_nonzero : t -> bool

a,b contains a non-zero value.

Sourceval is_zero : t -> bool
Sourceval is_one : t -> bool
Sourceval is_positive : t -> bool
Sourceval is_negative : t -> bool
Sourceval is_positive_strict : t -> bool
Sourceval is_negative_strict : t -> bool
Sourceval is_nonzero : t -> bool

Interval sign.

Sourceval is_singleton : t -> bool

a,b contains a single element.

Sourceval is_bounded : t -> bool

a,b has finite bounds.

Sourceval is_minf_inf : t -> bool

a,b represents -∞,+∞.

Sourceval is_in_range : t -> Z.t -> Z.t -> bool

Whether the interval is included in the range lo,up.

Printing

Sourceval to_string : t -> string
Sourceval print : Stdlib.out_channel -> t -> unit
Sourceval fprint : Stdlib.Format.formatter -> t -> unit
Sourceval bprint : Stdlib.Buffer.t -> t -> unit
Sourceval to_string_bot : t Utils_core.Bot.with_bot -> string
Sourceval print_bot : Stdlib.out_channel -> t Utils_core.Bot.with_bot -> unit
Sourceval fprint_bot : Stdlib.Format.formatter -> t Utils_core.Bot.with_bot -> unit
Sourceval bprint_bot : Stdlib.Buffer.t -> t Utils_core.Bot.with_bot -> unit

Enumeration

Sourceval size : t -> Z.t

Number of elements. Raises an invalid argument if it is unbounded.

Sourceval to_list : t -> Z.t list

List of elements, in increasing order. Raises an invalid argument if it is unbounded.

Set operations

Sourceval join : t -> t -> t

Join of non-empty intervals.

Join of possibly empty intervals.

Sourceval join_list : t list -> t_with_bot

Join of a list of (non-empty) intervals.

Sourceval meet : t -> t -> t_with_bot

Intersection of non-emtpty intervals (possibly empty)

Intersection of possibly empty intervals.

Sourceval meet_list : t list -> t_with_bot

Meet of a list of (non-empty) intervals.

Sourceval widen : t -> t -> t

Basic widening: put unstable bounds to infinity.

Sourceval widen_bot : t_with_bot -> t_with_bot -> t_with_bot
Sourceval positive : t -> t_with_bot
Sourceval negative : t -> t_with_bot

Positive and negative part.

Sourceval meet_zero : t -> t_with_bot

Intersects with

.

Sourceval meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.

Forward operations

Given one or two interval argument(s), return the interval result.

Sourceval neg : t -> t

Negation.

Sourceval abs : t -> t

Absolute value.

Sourceval succ : t -> t

Add 1.

Sourceval pred : t -> t

Subtract 1.

Sourceval add : t -> t -> t

Addition.

Sourceval sub : t -> t -> t

Subtraction.

Sourceval minmax4 : ('a -> 'b -> B.t) -> ('a * 'a) -> ('b * 'b) -> B.t * B.t
Sourceval mul : t -> t -> t

Multiplication.

Sourceval div_unmerged : t -> t -> t list

Division (with truncation). Returns a list of 0, 1, or 2 intervals to remain precise.

Sourceval ediv_unmerged : t -> t -> t list

Euclidian division (towards -oo). Returns a list of 0, 1, or 2 intervals to remain precise.

Sourceval div : t -> t -> t_with_bot

Division (with truncation). Returns a single (possibly empty) overapproximating interval.

Sourceval ediv : t -> t -> t_with_bot

Division (euclidian, towards -oo) Returns a single (possibly empty) overapproximating interval.

Sourceval rem : t -> t -> t_with_bot

Remainder. Uses the C semantics for remainder (%).

Sourceval erem : t -> t -> t_with_bot

Euclidian remainder. rounding towards -oo

Sourceval pow : t -> t -> t

Power.

Sourceval wrap : t -> Z.t -> Z.t -> t

Put back the interval inside lo,up by modular arithmetics. Useful to model the effect of arithmetic or conversion overflow.

Sourceval to_bool : bool -> bool -> t
Sourceval log_cast : t -> t

Conversion from integer to boolean in 0,1: maps 0 to 0 (false) and non-zero to 1 (true).

Sourceval log_not : t -> t

Logical negation. Logical operation use the C semantics: they accept 0 and non-0 respectively as false and true, but they always return 0 and 1 respectively for false and true.

Sourceval log_and : t -> t -> t

Logical and.

Sourceval log_or : t -> t -> t

Logical or.

Sourceval log_xor : t -> t -> t

Logical exclusive or.

Sourceval log_eq : t -> t -> t
Sourceval log_leq : t -> t -> t
Sourceval log_geq : t -> t -> t
Sourceval log_lt : t -> t -> t
Sourceval log_gt : t -> t -> t
Sourceval log_neq : t -> t -> t

C comparison tests. Returns an interval included in 0,1 (a boolean)

Sourceval is_log_eq : t -> t -> bool
Sourceval is_log_leq : t -> t -> bool
Sourceval is_log_geq : t -> t -> bool
Sourceval is_log_lt : t -> t -> bool
Sourceval is_log_gt : t -> t -> bool
Sourceval is_log_neq : t -> t -> bool

C comparison tests. Returns a boolean if the test may succeed

Bit operations

Sourceval shift_left : t -> t -> t_with_bot

Bitshift left: multiplication by a power of 2.

Sourceval shift_right : t -> t -> t_with_bot

Bitshift right: division by a power of 2 rounding towards -∞.

Sourceval shift_right_trunc : t -> t -> t_with_bot

Unsigned bitshift right: division by a power of 2 with truncation.

Sourceval bit_not : t -> t

Bitwise negation: ~x = -x-1

Internal functions

Sourceval min_or : Z.t -> Z.t -> Z.t -> Z.t -> Z.t
Sourceval max_or : Z.t -> Z.t -> Z.t -> Z.t -> Z.t
Sourceval bounds_or : Z.t -> Z.t -> Z.t -> Z.t -> Z.t * Z.t
Sourceval bounds_and : Z.t -> Z.t -> Z.t -> Z.t -> Z.t * Z.t
Sourceval min_xor : Z.t -> Z.t -> Z.t -> Z.t -> Z.t
Sourceval max_xor : Z.t -> Z.t -> Z.t -> Z.t -> Z.t
Sourceval bounds_xor : Z.t -> Z.t -> Z.t -> Z.t -> Z.t * Z.t

Interval functions, based on the previous ones

Sourceval bit_or : t -> t -> t

Bitwise or.

Sourceval bit_and : t -> t -> t

Bitwise and.

Sourceval bit_xor : t -> t -> t

Bitwise exclusive or.

Filters

Given two interval aruments, return the arguments assuming that the predicate holds.

Sourceval filter_leq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_geq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_lt : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_gt : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_eq : t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval filter_neq : t -> t -> (t * t) Utils_core.Bot.with_bot

Backward operations

Given one or two interval argument(s) and a result interval, return the argument(s) assuming the result in the operation is in the given result.

Sourceval bwd_default_unary : t -> t -> t_with_bot

Fallback for backward unary operators

Sourceval bwd_default_binary : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Fallback for backward binary operators

Sourceval bwd_neg : t -> t -> t_with_bot
Sourceval bwd_abs : t -> t -> t_with_bot
Sourceval bwd_succ : t -> t -> t_with_bot
Sourceval bwd_pred : t -> t -> t_with_bot
Sourceval bwd_add : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_sub : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_mul : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_div : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_ediv : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_bit_not : t -> t -> t_with_bot
Sourceval bwd_join : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward join: both arguments are intersected with the result.

Sourceval bwd_shift_left : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_shift_right : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_shift_right_trunc : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_bit_or : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_bit_and : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_bit_xor : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_convex_join : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_log_gen : (t -> t -> (t * t) Utils_core.Bot.with_bot) -> (t -> t -> (t * t) Utils_core.Bot.with_bot) -> t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_log_eq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_log_neq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_log_lt : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_log_gt : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_log_leq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_log_geq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_wrap : t -> (Z.t * Z.t) -> t -> t_with_bot
Sourceval bwd_rem : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_erem : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
Sourceval bwd_pow : t -> t -> t -> (t * t) Utils_core.Bot.with_bot