Up  

Module Newspeak


module Newspeak: sig .. end
Newspeak is a language designed for the purpose of static analysis. It was designed with these features in mind: Newspeak can be seen as a kind of high-level assembly language with annotations for analysis. The type of Newspeak programs, types, statements and expressions are described in this module. Additionnally, some functions to create, manipulate, export and display Newspeak programs are provided.

Types


module Nat: sig .. end
type t = file list * prog * size_t 
type prog = globals * (fid, fundec) Hashtbl.t * specs 
type globals = (string, gdecl) Hashtbl.t 
type gdecl = typ * init_t 
type fundec = ftyp * blk 
type specs = assertion list 
type assertion = spec_token list

type spec_token =
| SymbolToken of char
| IdentToken of string
| VarToken of string
| CstToken of cte

type stmtkind =
| Set of (lval * exp * scalar_t)
| Copy of (lval * lval * size_t)
| Decl of (string * typ * blk)
| ChooseAssert of (exp list * blk) list
| InfLoop of blk
| DoWith of (blk * lbl * blk)
| Goto of lbl
| Call of fn 
type stmt = stmtkind * location 
type blk = stmt list

type lval =
| Local of vid
| Global of string
| Deref of (exp * size_t)
| Shift of (lval * exp)

type exp =
| Const of cte
| Lval of (lval * scalar_t)
| AddrOf of (lval * size_t)
| AddrOfFun of (fid * ftyp)
| UnOp of (unop * exp)
| BinOp of (binop * exp * exp)

type cte =
| CInt of Nat.t
| CFloat of (float * string)
| Nil

type unop =
| Belongs of bounds
| Coerce of bounds
| Not
| BNot of bounds
| PtrToInt of ikind
| IntToPtr of ikind
| Cast of (scalar_t * scalar_t)

type binop =
| PlusI
| MinusI
| MultI
| DivI
| Mod
| PlusF of size_t
| MinusF of size_t
| MultF of size_t
| DivF of size_t
| BOr of bounds
| BAnd of bounds
| BXor of bounds
| Shiftlt
| Shiftrt
| PlusPI
| MinusPP
| Gt of scalar_t
| Eq of scalar_t

type fn =
| FunId of fid
| FunDeref of (exp * ftyp)

type typ =
| Scalar of scalar_t
| Array of (typ * length)
| Region of (field list * size_t) 
type field = offset * typ

type scalar_t =
| Int of ikind
| Float of size_t
| Ptr
| FunPtr

type init_t =
| Zero
| Init of (offset * scalar_t * exp) list 
type ftyp = typ list * typ option 
type lbl = int 
type vid = int 
type fid = string 
type file = string 
type ikind = sign_t * size_t

type sign_t =
| Signed
| Unsigned 
type size_t = int 
type offset = int 
type length = int 
type bounds = Nat.t * Nat.t 
type location = string * int * int 
val zero : exp
val one : exp
val zero_f : exp
val unknown_loc : location
val dummy_loc : string -> location
val domain_of_typ : sign_t * size_t -> bounds
val belongs : Nat.t -> bounds -> bool
val contains : bounds -> bounds -> bool
val negate : exp -> exp
val exp_of_int : int -> exp
val simplify_gotos : blk -> blk
val normalize_loops : blk -> blk
val simplify : blk -> blk
val simplify_exp : exp -> exp

Display


val string_of_loc : location -> string
Raises Invalid_argument "Newspeak.string_of_loc: unknown location" if the file name is unknown
val string_of_bounds : bounds -> string
string_of_bounds r returns the string representation of range r.
val string_of_cte : cte -> string
string_of_cte c returns the string representation of constant c.
val string_of_scalar : scalar_t -> string
val string_of_typ : typ -> string
val string_of_ftyp : ftyp -> string
val string_of_exp : exp -> string
val string_of_lval : lval -> string
val string_of_stmt : stmt -> string
val string_of_blk : blk -> string
string_of_block blk returns the string representation of block blk.
val dump : t -> unit
val dump_prog : prog -> unit
val dump_globals : globals -> unit
dump_globals glbdecls prints the global definitions glbdecls to standard output.
val dump_fundec : string -> fundec -> unit
val string_of_binop : binop -> string
class visitor : object .. end
val visit_fun : visitor -> fid -> fundec -> unit
val visit_glb : visitor -> string -> gdecl -> unit
val visit : visitor -> prog -> unit
class builder : object .. end
val build : builder -> prog -> prog
val build_gdecl : builder -> gdecl -> gdecl
val write : string -> t -> unit
val read : string -> t
read name retrieves the list of file names, program and size of pointers from a .npk file.
Raises Invalid_argument if the input file is not a valid .npk file, or its newspeak version is not the same as this file's.
name : file name of the .npk file to read
val write_hdr : Pervasives.out_channel ->
       string list * (string, gdecl) Hashtbl.t * specs *
       size_t -> unit
val write_fun : Pervasives.out_channel -> fid -> fundec -> unit
val size_of_scalar : size_t -> scalar_t -> size_t
val size_of : size_t -> typ -> size_t
val bind_var : string -> typ -> blk -> stmtkind
bind_var x t blk encloses the block blk with the declaration of variable x of type t and then binds all occurances of x as a global variable in blk.
val build_call : fid -> ftyp -> exp list -> blk
build_call f ft args builds the call to function f of type ft with arguments args.
Raises Invalid_argument "Newspeak.build_call: non scalar argument" if some argument is not of scalar type
val build_main_call : size_t -> ftyp -> string list -> blk
build_main_call ptr_sz ft params returns a block of newspeak code to call the main function with parameters params.
ptr_sz : the size of pointers
val create_cstr : string -> string -> string * gdecl

type alt_stmtkind =
| While of (exp list * blk)
| Npk of stmtkind 
type alt_blk = (alt_stmtkind * location) list 
val convert_loops : blk -> alt_blk
val max_ikind : ikind -> ikind -> ikind
val collect_fid_addrof : prog -> fid list
returns the list of all function identifiers that are stored as function pointers in the program.