package mopsa

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

Install

Dune Dependency

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

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.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/itvUtils/ItvUtils/IntItv/index.html

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