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/Bitfields/IntBitfields/index.html

Module Bitfields.IntBitfields

Bitfields - Sequences of bits that can be set, cleared, or unknown

We rely on Zarith for arithmetic operations.

Types

type t = Z.t * Z.t

cleared

type t_with_bot = t Core.Bot.with_bot

The type of possibly empty bitfields.

module I = ItvUtils.IntItv
val is_valid : t -> bool

Every bit in a bitfield must be set, cleared, or both.

Constructors

val of_z : Z.t -> Z.t -> t
val of_z_bot : Z.t -> Z.t -> t_with_bot
val cst : Z.t -> t

Constant.

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

0

val one : t

1

val mone : t

-1

val zero_one : t

0,1

val minf_inf : t

All integers. Indistiguishable from 0,+∞.

val unsigned : int -> t

Bitfields of unsigned integers with the specified bitsize.

val unsigned8 : t
val unsigned16 : t
val unsigned32 : t
val unsigned64 : t
val of_range_bot : Z.t -> Z.t -> t Core.Bot.with_bot

Bitfield enclosing the range lo,hi.

val of_bound_bot : B.t -> B.t -> t Core.Bot.with_bot

Bitfield enclosing the range lo,hi.

val of_range : Z.t -> Z.t -> t

Bitfield enclosing the range lo,hi. Fails with invalid_arg if the range is empty.

val of_bound : B.t -> B.t -> t

Bitfield enclosing the range lo,hi. Fails with invalid_arg if the range is empty.

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 intersection is non-empty.

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

A total ordering on bitfields, returning -1, 0, or 1. Can be used as compare for sets, maps, etc.

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

Total ordering on possibly empty bitfields.

val contains_zero : t -> bool

Whether the bifield contains zero.

val contains_one : t -> bool

Whether the bifield contains one.

val contains_nonzero : t -> bool

Whether the bifield contains a non-zero value.

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

Contains only non-zero elements.

val is_minf_inf : t -> bool

The bitfield represents -∞,+∞.

val is_singleton : t -> bool

Whether the bitfield contains a single element.

val is_bounded : t -> bool

Whether the bitfield contains a finite number of elements.

val lower_bound : t -> B.t

Get the lower bound (possibly MINF).

val upper_bound : t -> B.t

Get the upper bound (possibly PINF).

Printing

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

Enumeration

val size : t -> int

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

Abstract union.

val join_bot : t_with_bot -> t_with_bot -> t_with_bot
val join_list : t list -> t_with_bot
val meet : t -> t -> t_with_bot

Abstract intersection.

val meet_bot : t_with_bot -> t_with_bot -> t_with_bot
val meet_list : t list -> t_with_bot

Forward operations

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

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

val is_log_eq : t -> t -> bool
val is_log_neq : 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

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

val shift_left : t -> t -> t

Bitshift left: multiplication by a power of 2.

val shift_right : t -> t -> t

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

val shift_right_trunc : t -> t -> t

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

val bit_not : t -> t

Bitwise negation.

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_eq : t -> t -> (t * t) Core.Bot.with_bot
val filter_sgl : (Z.t -> Z.t -> bool) -> t -> t -> (t * t) Core.Bot.with_bot
val filter_neq : t -> t -> (t * t) Core.Bot.with_bot
val filter_leq : t -> t -> (t * t) Core.Bot.with_bot
val filter_geq : t -> t -> (t * t) Core.Bot.with_bot
val filter_lt : t -> t -> (t * t) Core.Bot.with_bot
val filter_gt : t -> t -> (t * t) Core.Bot.with_bot

Reduction

val of_interval : I.t -> t
val to_interval : t -> I.t
val meet_inter : t -> I.t -> (t * I.t) Core.Bot.with_bot

Intersects a bitfield with an interval, and returns the set represented both as a bitfield and as an interval. Useful to implement reductions.