Module Bidir.Intrinsics

An implementation of a selection of intrinsics useful for the assembly conversion.

Definitions

Direction type

type dir = [
  1. | `Forwards
  2. | `Backwards
]
val equal_dir : dir -> dir -> Ppx_deriving_runtime.bool
val dir_reverse : [< `Backwards | `Forwards ] -> [> `Backwards | `Forwards ]
val reorder_one_stmt : dir:dir -> 'a Types.bidir -> 'a Types.bidir

Reorders the topmost level of the given statement. Does not recurse into sub-statements.

Intrinsic type

type intrinsic =
  1. | BitsToUint of int
    (*

    Types.value.VBits -> Types.value.VInt. Interprets its argument as an unsigned integer. Intrinsic parameter is BV size.

    *)
  2. | BitsToSint of int
    (*

    Types.value.VBits -> Types.value.VInt. Interprets its argument as a signed integer. Intrinsic parameter is BV size.

    *)
  3. | IntToDecimal
    (*

    Types.value.VInt -> Types.value.VStr. Converts the given (signed) integer to a string.

    *)
  4. | Concat of int option list
    (*

    Types.value.VTup of Types.value.VStr -> Types.value.VStr. Concatenates the given tuple of strings into a single string. Intrinsic parameters are the length of each component of the tuple. At most one length can be None, indicating that component expands to the rest of the string.

    *)
  5. | NotIn of Types.value list
    (*

    Any -> Any. Asserts that the given value is not contained in the intrinsic's list of literals. If successful, this acts as the identity function. Otherwise, throws.

    *)
  6. | InInterval of int * int
    (*

    Types.value.VInt -> Types.value.VInt. Asserts that the given integer is within the interval (inclusive of bounds).

    *)
  7. | Multiply of int
    (*

    Types.value.VInt -> Types.value.VInt. Multiplies by the given factor. Inverting this succeeds only when the input is a multiple of the factor.

    *)
  8. | Add of int
    (*

    Types.value.VInt -> Types.value.VInt. Adds the given constant.

    *)
  9. | Inv of intrinsic
    (*

    Performs the inverse of the given intrinsic, i.e., swaps its forwards and backwards directions.

    *)

Useful intrinsics, though keep in mind that the Bidir type is generic in the allowed intrinsics.

val equal_intrinsic : intrinsic -> intrinsic -> Ppx_deriving_runtime.bool
val show_intrinsic : intrinsic -> Ppx_deriving_runtime.string
val intrinsic_to_yojson : intrinsic -> Yojson.Safe.t
val _ : Yojson.Safe.t -> intrinsic Ppx_deriving_yojson_runtime.error_or
val pp_dummy_intrinsic : Stdlib.Format.formatter -> 'a -> unit

Implementation of intrinsics

type ('i, 'a) intrinsic_impl = 'i -> dir:dir -> 'a -> 'a

An implementation of an intrinsic, parametrised by the intrinsic type and the value type. Accepts an argument of which direction to operate in.

val make_intrinsic : ((Types.value -> Types.value) * (Types.value -> Types.value)) -> dir:dir -> Types.value -> Types.value

Constructs an intrinsic_impl function from the given forwards and backwards functions. When executing the intrinsic, this helper function ensures that the given functions are inverses.

val require : ?f:(string -> unit) -> bool -> string -> unit

Types.value conversion functions

Destructing values

val vbits_of_val : Types.value -> string
val vint_of_val : Types.value -> int
val vstr_of_val : Types.value -> string
val vtup_of_val : (Types.value -> 'a) list -> Types.value -> 'a list

Constructing values

val val_of_vbits : string -> Types.value
val val_of_vint : int -> Types.value
val val_of_vstr : string -> Types.value
val val_of_vtup : ('a -> Types.value) list -> 'a list -> Types.value

Helpers for implementation

These implement both directions of a number of intrinsics, operating on built-in Ocaml types.

val uint_of_bits : 'a -> string -> int
val bits_of_uint : int -> CCInt.t -> string
val sint_of_bits : int -> string -> int
val bits_of_sint : int -> CCInt.t -> string
val notin : 'a list -> 'a -> 'a
val ininterval : lo:CCInt.t -> hi:CCInt.t -> CCInt.t -> CCInt.t
val concat_forwards : int option list -> string list -> string
val concat_helper : int option CCList.t -> string -> string list * int * int option CCList.t
val concat_backwards : int option CCList.t -> string -> string list

Isomorphisms

Really weak isomorphisms which are just a pair of forwards and back functions. These are weak because they are really only isomorphic on the image of the forwards function. Even then, they can throw and do other terrible things.

type ('a, 'b) iso = ('a -> 'b) * ('b -> 'a)
val (%%>) : (('a -> 'b) * ('c -> 'd)) -> (('b -> 'e) * ('f -> 'c)) -> ('a -> 'e) * ('f -> 'd)
val isorev : ('a * 'b) -> 'b * 'a
val val_iso_bits : (Types.value -> string) * (string -> Types.value)
val val_iso_int : (Types.value -> int) * (int -> Types.value)
val val_iso_str : (Types.value -> string) * (string -> Types.value)
val val_iso_tup : ((Types.value -> 'a) * ('b -> Types.value)) list -> (Types.value -> 'a list) * ('b list -> Types.value)
val bits_iso_uint : int -> (string -> int) * (CCInt.t -> string)
val bits_iso_sint : int -> (string -> int) * (CCInt.t -> string)
val int_iso_string : (CCInt.t -> string) * (string -> CCInt.t)
val concat_strings_iso : int option CCList.t -> (string list -> string) * (string -> string list)
val either_iso : (('a -> 'b) * ('b -> 'a)) -> (('a -> 'c) * ('c -> 'a)) -> ('a, ('b, 'c) Either.t) iso
val both_iso : (('a -> 'b) * ('c -> 'd)) -> (('a, 'a) Either.t -> ('b, 'b) Either.t) * (('c, 'c) Either.t -> ('d, 'd) Either.t)
val invol_iso : 'a -> 'a * 'a
val multiply_iso : int -> (int -> int) * (int -> int)
val add_iso : int -> (int -> int) * (int -> int)

Final implementation

val run_intrinsics : intrinsic -> dir:dir -> Types.value -> Types.value

An intrinsic_impl executing the intrinsics specified in intrinsic.