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
sym name
constructs a sort with the given name.
A symbolic sort could represent an abstract data type with no further information available, e.g., some machine status word of unknown size or representation; it may also be used to denote data with obvious representation, e.g., the Bool
sort; finally, a symbolic sort could be used as a constructor name for an indexed sort, e.g., (BitVec(width)).
See the Example in the module description for more information.
int x
a numeric sort.
While it is possible to create a standalone numeric sort, it wouldn't be possible to refine it, since only symbolic sorts re refinable.
Numeric sorts are used mostly as parameters. See the Example section of the module documentation for more information.
app s1 s2
constructs a sort of sort s1
and s2
.
An application could be seen as a tuple building operators, thus this operation defines a sort that is described by two other sorts.
Basically, the app
operator builds a heterogenous list, with elements which should be other sorts. The list could be then traversed using the Sort.hd
and Sort.tl
operators, and individual elements could be read with the value
and name
operators. Since the structure of the sort is fully encoded in this type, those operations are total.
value s
returns the number associated with the numeric sort.
name s
returns the symbol associated with a symbolic sort
hd s
the first argument of sort s
tl
the list of arguments of sort s
excluding the first one
val refine : name -> unit sort -> 'a t option
refine witness s
restores the type of the sort.
The sort type is an index type which could be lost, e.g., when the forget
function is applied or when the sort is stored and read from its textual representation.
The refine
function will re-instantiate the type index if the constructor name of the sort s
is the name
.
This function gives a mandate for the refine function to index the sort s
with any type, which will breach the sort type safety, therefore this function should be used with care and be hidden behind the abstraction barrier and have a concrete type.
See the Example section in the module documentation for the demonstration of how refine should be used.
val forget : 'a t -> unit t
forget s
forgets the type index associated with the sort s
.
This is effectively an upcasting function, that could be used when the typing information is not necessary anymore or is not representable. The type index could be later restored with the refine
function.
val same : 'a t -> 'b t -> bool
same x y
is true if x
and y
are of the same structure.
Sorts with erased type indices.
module Name : sig ... end