package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.2.tar.gz
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa

doc/mopsa.mopsa_utils/Mopsa_utils/ItvUtils/FloatItv/index.html

Module ItvUtils.FloatItv

FloatItv - Floating-point interval arithmetics with rounding.

We rely on C code to provide functions with correct rounding (rounding direction and rounding precision).

module F = Float
module II = ItvUtils.IntItv

Types

type t = {
  1. mutable lo : float;
    (*

    lower bound

    *)
  2. mutable up : float;
    (*

    upper bound

    *)
}

The type of non-empty intervals: a lower bound and an upper bound. The bounds can be -∞ and +∞. In particular, we can have -∞,-∞ and +∞,+∞ (useful to model sets of floating-point numbers). We must have lo ≤ up. The bounds shall not be NaN.

type t_with_bot = t Core.Bot.with_bot

The type of possibly empty intervals.

val is_valid : t -> bool

Constructors

val mk : float -> float -> t
val zero : t
val one : t
val two : t
val mone : t
val zero_one : t
val mone_zero : t
val mone_one : t
val mhalf_half : t
val zero_inf : t
val minf_zero : t
val minf_inf : t

Useful intervals

val of_float : float -> float -> t

Constructs a non-empty interval. We must have lo ≤ up, or an exception is raised. NaN bounds are transformed into infinities.

val of_float_bot : float -> float -> t_with_bot

Constructs a possibly empty interval (no rounding). NaN bounds are transformed into infinities.

val hull : float -> float -> t

Constructs the smallest interval containing a and b.

val cst : float -> t

Singleton interval.

Predicates

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

Set ordering. = also works to compare for equality.

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 : float -> t -> bool

Whether the interval contains a certain value.

val compare : t -> t -> int

A total ordering of intervals (lexical ordering) returning -1, 0, or 1. Can be used as compare for sets, maps, etc. (The hypothesis that bounds cannot be NaN is important to make the order total.

val compare_bot : t Core.Bot.with_bot -> t Core.Bot.with_bot -> int

Total ordering on possibly empty intervals.

val is_zero : 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 contains_positive : t -> bool
val contains_negative : t -> bool
val contains_positive_strict : t -> bool
val contains_negative_strict : t -> bool
val contains_zero : t -> bool
val contains_nonzero : t -> bool

Whether the interval contains an element of the specified sign.

val is_singleton : t -> bool

Whether the interval contains a single element.

val is_bounded : t -> bool

Whether the interval has finite bounds.

val is_in_range : t -> float -> float -> bool

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

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 true if the test may succeed, false if it cannot.

Printing

type print_format = F.print_format
val dfl_fmt : F.print_format
val hex_fmt : F.print_format
val to_string : print_format -> t -> string
val print : print_format -> out_channel -> t -> unit
val fprint : print_format -> Format.formatter -> t -> unit
val bprint : print_format -> Buffer.t -> t -> unit
val to_string_bot : print_format -> t Core.Bot.with_bot -> string
val print_bot : print_format -> out_channel -> t Core.Bot.with_bot -> unit
val fprint_bot : print_format -> Format.formatter -> t Core.Bot.with_bot -> unit
val bprint_bot : print_format -> Buffer.t -> t Core.Bot.with_bot -> unit

Operations without rounding

val neg : t -> t

Negation.

val abs : t -> t

Absolute value.

val fmod : t -> t -> t_with_bot

Remainder (fmod).

val to_z : t -> Z.t * Z.t

Conversion to integer (using truncation).

val to_int_itv : t -> II.t Core.Bot.with_bot
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 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 widen : t -> t -> t

Basic widening: put unstable bounds to infinity.

val widen_bot : t_with_bot -> t_with_bot -> t_with_bot
val bwd_default_unary : t -> t -> t_with_bot

Fallback for backward unary operators

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

Fallback for backward binary operators

val bwd_neg : t -> t -> t_with_bot

Backward negation.

val bwd_abs : t -> t -> t_with_bot

Backward absolute value.

val bwd_fmod : t -> t -> t -> (t * t) Core.Bot.with_bot

Backward remainder (fmod).

Rounding-dependent functions

Interval operations support six rounding modes. The first four correspond to rounding both bounds in the same direction: to nearest, upwards, downards, or to zero. To this, we add outer rounding (lower bound downwards and upper bound upwards) and inner rounding (lower bound upwards and upper bound downwards).

Rounding can be performed for single-precision or double-precision.

Outer interval arithmetic can model soundly real arithmetic. In this case, infinities model unbounded intervals.

Directed roundings and outer arithmetics can model soundly float arithmetic. In this case, infinite bounds signal the precence of infinite float values. Directed roundings can produce -∞,-∞ or +∞,+∞ (denoting a set of floats reduced to an infinite float).

Inner rounding can return empty intervals. Divisions and square roots can return empty intervals for any rounding mode.

We do not track NaN. NaN bounds, as in -∞,-∞ + +∞,+∞, are transformed into infinities.

val add_dbl_itv_near : t -> t -> t -> unit
val add_dbl_itv_up : t -> t -> t -> unit
val add_dbl_itv_down : t -> t -> t -> unit
val add_dbl_itv_zero : t -> t -> t -> unit
val add_dbl_itv_outer : t -> t -> t -> unit
val add_dbl_itv_inner : t -> t -> t -> unit
val add_sgl_itv_near : t -> t -> t -> unit
val add_sgl_itv_up : t -> t -> t -> unit
val add_sgl_itv_down : t -> t -> t -> unit
val add_sgl_itv_zero : t -> t -> t -> unit
val add_sgl_itv_outer : t -> t -> t -> unit
val add_sgl_itv_inner : t -> t -> t -> unit
val sub_dbl_itv_near : t -> t -> t -> unit
val sub_dbl_itv_up : t -> t -> t -> unit
val sub_dbl_itv_down : t -> t -> t -> unit
val sub_dbl_itv_zero : t -> t -> t -> unit
val sub_dbl_itv_outer : t -> t -> t -> unit
val sub_dbl_itv_inner : t -> t -> t -> unit
val sub_sgl_itv_near : t -> t -> t -> unit
val sub_sgl_itv_up : t -> t -> t -> unit
val sub_sgl_itv_down : t -> t -> t -> unit
val sub_sgl_itv_zero : t -> t -> t -> unit
val sub_sgl_itv_outer : t -> t -> t -> unit
val sub_sgl_itv_inner : t -> t -> t -> unit
val mul_dbl_itv_near : t -> t -> t -> unit
val mul_dbl_itv_up : t -> t -> t -> unit
val mul_dbl_itv_down : t -> t -> t -> unit
val mul_dbl_itv_zero : t -> t -> t -> unit
val mul_dbl_itv_outer : t -> t -> t -> unit
val mul_dbl_itv_inner : t -> t -> t -> unit
val mul_sgl_itv_near : t -> t -> t -> unit
val mul_sgl_itv_up : t -> t -> t -> unit
val mul_sgl_itv_down : t -> t -> t -> unit
val mul_sgl_itv_zero : t -> t -> t -> unit
val mul_sgl_itv_outer : t -> t -> t -> unit
val mul_sgl_itv_inner : t -> t -> t -> unit
val divpos_dbl_itv_near : t -> t -> t -> unit
val divpos_dbl_itv_up : t -> t -> t -> unit
val divpos_dbl_itv_down : t -> t -> t -> unit
val divpos_dbl_itv_zero : t -> t -> t -> unit
val divpos_dbl_itv_outer : t -> t -> t -> unit
val divpos_dbl_itv_inner : t -> t -> t -> unit
val divpos_sgl_itv_near : t -> t -> t -> unit
val divpos_sgl_itv_up : t -> t -> t -> unit
val divpos_sgl_itv_down : t -> t -> t -> unit
val divpos_sgl_itv_zero : t -> t -> t -> unit
val divpos_sgl_itv_outer : t -> t -> t -> unit
val divpos_sgl_itv_inner : t -> t -> t -> unit
val mkop : unit -> t
val wrap_op1 : ('a -> t -> 'b) -> 'a -> t
val wrap_op2 : ('a -> 'b -> t -> 'c) -> 'a -> 'b -> t
val wrap_op1_bot : ('a -> t -> 'b) -> 'a -> t Core.Bot.with_bot
val wrap_op2_bot : ('a -> 'b -> t -> 'c) -> 'a -> 'b -> t Core.Bot.with_bot
val wrap_sqrt : (float -> float) -> (float -> float) -> t -> t Core.Bot.with_bot
val wrap_div_unmerged : ('a -> t -> 'b) -> 'a -> t -> 'b list
val wrap_div_unmerged_bot : ('a -> t -> 'b Core.Bot.with_bot) -> 'a -> t -> 'b list
val wrap_div : ('a -> t -> t) -> 'a -> t -> t_with_bot
val wrap_div_bot : ('a -> t -> t Core.Bot.with_bot) -> 'a -> t -> t_with_bot
module Double : sig ... end

Intervals with rounding to double.

module Single : sig ... end

Intervals with rounding to float.

Operations with rounding mode as argument

type prec = [
  1. | `SINGLE
    (*

    32-bit single precision

    *)
  2. | `DOUBLE
    (*

    64-bit double precision

    *)
  3. | `REAL
    (*

    real arithmetic (outward double rounding is used)

    *)
]

Precision.

type round = [
  1. | `NEAR
    (*

    To nearest

    *)
  2. | `UP
    (*

    Upwards

    *)
  3. | `DOWN
    (*

    Downwards

    *)
  4. | `ZERO
    (*

    Towards 0

    *)
  5. | `ANY
    (*

    Any rounding mode

    *)
]

Rounding direction. This is ignored for real arithmetic.

val add : prec -> round -> t -> t -> t

Addition.

val sub : prec -> round -> t -> t -> t

Subtraction.

val mul : prec -> round -> t -> t -> t

Multiplication.

val div : prec -> round -> t -> t -> t_with_bot

Division.

val div_unmerged : prec -> round -> t -> t -> t list

Division. Returns a list of intervals to remain precise.

val square : prec -> round -> t -> t

Square.

val sqrt : prec -> round -> t -> t_with_bot

Square root.

val round_int : prec -> round -> t -> t

Round to integer.

val unround_int : prec -> round -> t -> t

Backward round to integer.

val round : prec -> round -> t -> t

Round to float.

val unround : prec -> round -> t -> t

Backward round to float.

val of_int : prec -> round -> int -> int -> t

Conversion from integer range.

val of_int64 : prec -> round -> int64 -> int64 -> t

Conversion from int64 range.

val of_z : prec -> round -> Z.t -> Z.t -> t

Conversion from integer range.

val filter_leq : prec -> t -> t -> (t * t) Core.Bot.with_bot

<= filtering.

val filter_geq : prec -> t -> t -> (t * t) Core.Bot.with_bot

>= filtering.

val filter_lt : prec -> t -> t -> (t * t) Core.Bot.with_bot

< filtering.

val filter_gt : prec -> t -> t -> (t * t) Core.Bot.with_bot

> filtering.

val filter_eq : prec -> t -> t -> (t * t) Core.Bot.with_bot

== filtering.

val filter_neq : prec -> t -> t -> (t * t) Core.Bot.with_bot

!= filtering.

val meet_nonzero : prec -> t -> t Core.Bot.with_bot
val bwd_add : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward addition.

val bwd_sub : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward subtraction.

val bwd_mul : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward multiplication.

val bwd_div : prec -> round -> t -> t -> t -> (t * t) Core.Bot.with_bot

Backward division.

val bwd_round_int : prec -> round -> t -> t -> t_with_bot

Backward rounding to integer.

val bwd_round : prec -> round -> t -> t -> t_with_bot

Backward rounding to float.

val bwd_square : prec -> round -> t -> t -> t_with_bot

Backward square.

val bwd_sqrt : prec -> round -> t -> t -> t_with_bot

Backward square root.

val bwd_of_z : prec -> round -> Z.t -> Z.t -> t -> (Z.t * Z.t) Core.Bot.with_bot

Backward conversion from int.

val bwd_to_z : prec -> Z.t -> Z.t -> t -> t_with_bot

Backward conversion to integer.