package mopsa

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

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 Utils_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 Utils_core.Bot.with_bot

Bitfield enclosing the range lo,hi.

val of_bound_bot : B.t -> B.t -> t Utils_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.

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 : 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 -> 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) Utils_core.Bot.with_bot
val filter_sgl : (Z.t -> Z.t -> bool) -> t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_neq : t -> t -> (t * t) Utils_core.Bot.with_bot
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

Reduction

val of_interval : I.t -> t
val to_interval : t -> I.t
val meet_inter : t -> I.t -> (t * I.t) Utils_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.

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