Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package bap-core-theory
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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 8Type 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 u32type +'a t = 'a sortsym 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.
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.
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 pp : Core_kernel.Caml.Format.formatter -> 'a t -> unitprints the sort.
module Top : sig ... endSort without a type index.
module Name : sig ... endThe name registry.