package mopsa

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

IntItv - Intervals for arbitrary precision integers.

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

module B = IntBound

Types

type t = B.t * B.t

upper bound

type t_with_bot = t Utils_core.Bot.with_bot

The type of possibly empty intervals.

val is_valid : t -> bool

Constructors

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

Constructs a non-empty interval.

val of_float : float -> float -> t

Constructs a non-empty interval.

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

Constructs a possibly empty interval.

val of_float_bot : float -> float -> t_with_bot

Constructs a possibly empty interval.

val hull : B.t -> B.t -> t

Constructs the smallest interval containing a and b.

val cst : Z.t -> t

Singleton interval.

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

0,0

val one : t

1,1

val mone : t

-1,-1

val zero_one : t

0,1

val mone_zero : t

-1,0

val mone_one : t

-1,1

val zero_inf : t

0,+∞

val minf_zero : t

-∞,0

val minf_inf : t

-∞,+∞

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

Intervals of unsigned integers with the specified bitsize.

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

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

Predicates

val equal : t -> t -> bool

Equality. = also works

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

Set ordering.

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

Whether the intervals have an non-empty intersection.

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

Whether the interval contains a (finite) value.

val 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.

val contains_zero : t -> bool

a,b contains 0.

val contains_one : t -> bool

a,b contains 1.

val contains_nonzero : t -> bool

a,b contains a non-zero value.

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

Interval sign.

val is_singleton : t -> bool

a,b contains a single element.

val is_bounded : t -> bool

a,b has finite bounds.

val is_minf_inf : t -> bool

a,b represents -∞,+∞.

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

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

Printing

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

Enumeration

val size : t -> Z.t

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

val to_list : t -> Z.t list

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

Set operations

val join : t -> t -> t

Join of non-empty intervals.

val join_bot : t_with_bot -> t_with_bot -> t_with_bot

Join of possibly empty intervals.

val join_list : t list -> t_with_bot

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

val meet : t -> t -> t_with_bot

Intersection of non-emtpty intervals (possibly empty)

val meet_bot : t_with_bot -> t_with_bot -> t_with_bot

Intersection of possibly empty intervals.

val meet_list : t list -> t_with_bot

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

val widen : t -> t -> t

Basic widening: put unstable bounds to infinity.

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

Positive and negative part.

val meet_zero : t -> t_with_bot

Intersects with

.

val meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.

Forward operations

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

val neg : t -> t

Negation.

val abs : t -> t

Absolute value.

val succ : t -> t

Add 1.

val pred : t -> t

Subtract 1.

val add : t -> t -> t

Addition.

val sub : t -> t -> t

Subtraction.

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

Multiplication.

val div_unmerged : t -> t -> t list

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

val ediv_unmerged : t -> t -> t list

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

val div : t -> t -> t_with_bot

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

val ediv : t -> t -> t_with_bot

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

val rem : t -> t -> t_with_bot

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

val erem : t -> t -> t_with_bot

Euclidian remainder. rounding towards -oo

val pow : t -> t -> t

Power.

val 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.

val to_bool : bool -> bool -> t
val log_cast : t -> t

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

val 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.

val log_and : t -> t -> t

Logical and.

val log_or : t -> t -> t

Logical or.

val log_xor : t -> t -> t

Logical exclusive or.

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

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

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

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

Bit operations

val shift_left : t -> t -> t_with_bot

Bitshift left: multiplication by a power of 2.

val shift_right : t -> t -> t_with_bot

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

val shift_right_trunc : t -> t -> t_with_bot

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

val bit_not : t -> t

Bitwise negation: ~x = -x-1

Internal functions

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

Interval functions, based on the previous ones

val bit_or : t -> t -> t

Bitwise or.

val bit_and : t -> t -> t

Bitwise and.

val bit_xor : t -> t -> t

Bitwise exclusive or.

Filters

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

val filter_leq : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_geq : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_lt : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_gt : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_eq : t -> t -> (t * t) Utils_core.Bot.with_bot
val 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.

val bwd_default_unary : t -> t -> t_with_bot

Fallback for backward unary operators

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

Fallback for backward binary operators

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

Backward join: both arguments are intersected with the result.

val bwd_shift_left : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_shift_right : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_shift_right_trunc : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_bit_or : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_bit_and : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_bit_xor : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_convex_join : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val 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
val bwd_log_eq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_log_neq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_log_lt : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_log_gt : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_log_leq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_log_geq : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_wrap : t -> (Z.t * Z.t) -> t -> t_with_bot
val pos_mod : IntBound.t -> IntBound.t -> IntBound.t
val bwd_rem : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_erem : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_pow : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct