Module Value.Sort

Value Sorts.

A concrete and extensible representation of a value sort. The sort usually holds the static information about the value representation, like the width of a bitvector, the representation format of a floating-point number, and so on.

This module is mostly needed when a new sort is defined. The Core Theory provides a predefined collection of sorts, here is the list:

• Bitv - bitvectors, e.g., BitVec(i)
• Mem - memories, e.g., Mem(BitVec(i), BitVec(j)
• Float - floating-points, e.g., Float(IEEE754(2, 8, 23), BitVec(32);
• Rmode - rounding mode, e.g., Rmode.

This module defines a simple DSL for specifying sorts, the DSL grammar is made only from three rules:

           sort = sym | int | sort(sort)

The DSL is embedded into the host language with an infix operator @-> for application, e.g., OCaml grammar for sorts is:

v sort = sym exp | int exp | sort "@->" sort exp = ?a valid OCaml expression? v

Both symbols and numbers are indexed with a type index, which serves as a witness of the sort value, e.g.,

type int8
let int8 : int8 num sort = Sort.int 8

Type indices enable explicit reflection of the target language type system in the host type system, while still keeping the typing rules under designer's control.

As a working example, let's develop a sort for binary fixed-point numbers. We need to encode the type of the underlying bitvector as well as the scaling factor. Suppose, we chose to encode the scaling factor by an integer position of the point, e.g., 8 means scaling factor 2^8, i.e., a point fixed on 8th bit from the left.

The syntax of our sort will be Fixpoint(<num>,BitVec(<num>)), but we will keep it private to enable further extensions. The structure of the sort is explicitly captured in its type, in our case, it will be 'p num -> 's Bitv.t -> fixpoint sym, but since we want to keep it is hidden by our type ('p,'s) t. The same as with the built-in Bitv and Mem sorts.

We declare a fixpoint constructor and keep it private, to ensure that only we can construct (and refine) fixpoint sorts. Since the sort type is abstract, we also need to provide functions that access arguments of our sort.

Finally, we need to provide the refine function, that will cast an untyped sort to its type representation, essentially proving that the sort is a valid fixpoint sort.

module Fixpoint : sig
  type ('p, 's) t
  val define : int -> 's Bitv.t sort -> ('p,'s) t sort
  val refine : unit sort -> ('p,'s) t sort option
  val bits : ('p,'s) t sort -> 's Bitv.t sort
  val logscale : ('p,'s) t sort -> int
end = struct
  type fixpoint

  type ('m,'s) t =
    'm Value.Sort.num ->
    's Bitv.t ->
    fixpoint Value.Sort.sym

  let fixpoint = Value.Sort.Name.declare "FixPoint"

  let define p s = Value.Sort.(int p @-> s @-> sym fixpoint)
  let refine s = Value.Sort.refine fixpoint s
  let bits s = Value.Sort.(hd (tl s))
  let logscale s = Value.Sort.(hd s)
end

(* Example of usage: *)


type ('m,'s) fixpoint = Fixpoint.t Value.sort

type u32              (* type index for 32 bit ints *)
type p8               (* type index for points at 8th bit *)

(* a sort of 32-bit bitvectors, usually provided by the CPU model *)
let u32 : u32 Bitv.t Value.sort = Bitv.define 32

(* a sort of 8.32 fixed-point numbers. *)
let fp8_32 : (p8,u32) fixpoint = Fixpoint.define 8 u32