This module implements basic data structures for the MiniC language, the intermediate language CmdType, and the Abacus assembler language. Moreover, there are some basic functions to work with these basic data types like those for type checking MiniC programs, and determining the variables that are read and written by instructions.
Type  Description 
Abacus is a typical RISC architecture; the following data type specifies however only the scalar part of the instructions, while there are also vector instructions. See also Abacus reference card. For addition, subtraction, multiplication, division there are four variants:


AbcParams holds the parameters of a computer system with an Abacus processor, which are the following:


The following are instructions of the virtual intermediate machine (cmd language) with variables y,x1,x2,y1,y2:


This is the general exception raised by MiniC functions if something went wrong. 

These are righthandside expressions of the MiniC language, i.e., expressions that may occur on the righthand side of an assignment.




This type defines the four basic instruction classes, i.e., ALU operations, MEMory operations, BRanCh operations and JuMPs. 

LhsExpr are viewed as addresses with an offset; the address is thereby the base variable, and the offset is computed as an expression that depends on the access expressions of arrays and tuples. Note that types [m][n]alpha are parsed to Carr(m,Carr(n,alpha)) and that expressions a[i][j] are parsed to LhsArrAcc(LhsArrAcc(a,i),j). The following are lefthandside expressions of the MiniC language, i.e., expressions that may occur on the lefthand side of an assignment.


MiniC functions are defined by their name, their arguments and return type, and of course by their body statement. The body statement should always terminate with a return expression. MiniC functions can call other functions, but not themselves (also not via other functions). This restriction ensures statically bounded memory for function calls. 

MiniC programs consist of a set of threads which are pairs of the name of the thread and its statement, functions that can be called by these threads, and the declaration of the globally shared variables that are used for the threads to communicate with each other. Further information about the syntax can be found in the reference card MiniC reference card. 

Ops1 declares an enumeration type of the unary operators of the MiniC language (this makes is flexible to add operators). Available operators are:


Ops2 declares an enumeration type of the binary operators of the MiniC language (this makes is flexible to add operators). Available operators are:


These are the statements of the MiniC language (further information about the syntax can be found in the reference card MiniC reference card.)


TypeC declares the available data types of variables in MiniC. There are atomic types Cbool, Cnat and Cint, and composite types Carr and Cfun:







Function or value  Description 

check the consistency of the given parameters, i.e.,


LhsExpr are viewed as addresses with an offset (see comment on LhsExpr). GetBaseOfLhs lhs computes thereby the address, which is the target variable in the LhsExpr.


determines the InstructionClass of a given instruction


converts a LhsExpr e to a Expr (it never fails).


MayReadByCmd cmd determines the set of variables the cmd may read. Remark: CmdAccessArr(y,x1,x2), i.e. y=x1[x2], is mapped to a load instruction where x1 is the start address of the array which is a constant value determined by the memory mapping of the program. Note further that y := (c?x1:x0) may read c,x1, and x0, but only c is read for sure.

LhsExpr are viewed as addresses with an offset (see comment on LhsExpr). MkOffsetExpr computes thereby the offset from the base variable of lhs to the memory address of lhs. Since this offset depends on the variables occurring in lhs, it is computed symbolically, i.e., as an expression. To this end, one has to make use of the types of variables, and thus a declaration must be given, but also a variable renaming is applied before computing the result. Example: a[i][j].1 of type [m][n](bool * nat) has the following offset: i*SizeOfType([n](bool * nat)) + j*SizeOfType((bool * nat)) + 1



MustReadByCmd cmd determines the set of variables the cmd must read. Remark: CmdAccessArr(y,x1,x2), i.e. y=x1[x2], is mapped to a load instruction where x1 is the start address of the array which is a constant value determined by the memory mapping of the program. Note further that y := (c?x1:x0) may read c,x1, and x0, but only c is read for sure.


For any Abacus instruction instr, function ReadWritesOfInstr computes a triple (r,w,o) where


writes a comment s to output stream ostr and raises then exception ExceptionMiniC with message s.


converts rhs expression e to a LhsExpr, if possible, otherwise fails.


SizeOfType ty computes the size of a type ty in terms of machine words. The result is None in case that an array type has an unspecified dimension, otherwise it is Some(s) where s is the number of machine words required to store type ty.


SuccOfCmd (i,cmd) determines the set of indices of potential successor commands of command cmd which is found at line i. It is a conservative "may" estimation, since in case of CmdIfGoto both paths are taken.

Full Usage:
TypeCheckFunction decl mf
Parameters:
Map<string, TypeC>
mf : MiniCFunction
Returns: MiniCFunction

For simplicity, the parser will resolve all overloaded operators like the arithmetic operators to Cnat type. This function takes care of given declarations and will then determine typecorrect operators for the MiniC function mf.


For simplicity, the parser will resolve all overloaded operators like the arithmetic operators to Cnat type. This function will determine typecorrect operators for the MiniC program p.

For simplicity, the parser will resolve all overloaded operators like the arithmetic operators to Cnat type. This function takes care of given declarations and will then determine typecorrect operators for the rhs expression. The result is a pair (ty,e') where e' is the expression with corrected types and ty is its type. 

For simplicity, the parser will resolve all overloaded operators like the arithmetic operators to Cnat type. This function takes care of given declarations and will then determine typecorrect operators for the lhs expression. The result is a pair (ty,lhs') where lhs' is the LhsExpr with corrected types and ty is its type. 

For simplicity, the parser will resolve all overloaded operators like the arithmetic operators to Cnat type. This function takes care of given declarations and will then determine typecorrect operators for the statement. The result is a pair (ty,stmt) where stmt is the given statement with corrected types, and ty is the optional return type of that statement, which is usually None (meaning void) or otherwise the type of a return expression (for type checking function bodies). 


VarsOfCmd cmd determines the set of variables ocurring in cmd.


compute the set of variables that occur in an expression


compute the set of variables that occur in a lhsexpression


compute the set of variables that occur in a statement


WrittenByCmd cmd determines the set of variables written by cmd. Remark: CmdAssignArr(y,x1,x2), i.e. y[x1]=x2, is mapped to a store instruction which does not modify any of the variables (y is the start address of the array which is not modified).


compute the global and local variable declarations of MiniC program p and checks for shaddowing


compute the local variable declarations of MiniC statement st

Full Usage:
isVarname s
Parameters:
string
Returns: bool

