The TASS Intermediate Representation
The TASS Intermediate Representation is a programming language-neutral abstract representation of a program. It provides support for multiple processes,
functions, variables, pointers, message passing, etc.
It is the job of a TASS front-end module to translate from source code in a language such as MiniMP, C, C++, or Fortran to a TASS Intermediate Representation.
TASS currently includes a front-end for MiniMP, and front-ends for other languages
with support for the Message Passing Interface (MPI) is in progress.
Model
A model is an abstract representation of a program. It has a name, a set of shared variables, and a sequence of processes.
Java interface: ModelIF
Method to create: ModelFactory.newModel(String name, int numProcs)
Processes
Processes are numbered 0,1,...,n-1, where n is the number of processes. The number n is fixed when the model is created and can never change. The unique number associated to a process is known as the process's "pid."
Each process contains a number of process variables, and a number of functions. One of the functions is designated the "main" function (though that function's name does not have to be "main"). In particular, every process must contain at least one function.
Java interface: ProcessIF
Method to create: ModelFactory.newModel(String name, int numProcs)
Variables
There are four different scopes to which a variable may belong.
- SharedVariable
Shared scope includes all input and output variables, and general shared variables; these are variables that can be accessed by any process.
Java interface: SharedVariableIF
Method to create: Model.newSharedVariable(TypeIF type, String name)
- ProcessVariable
Process variables have the scope of one process; they can be accessed by any function in that process.
Java interface: ProcessVariableIF
Method to create: Model.newProcessVariable(ProcessIF process, TypeIF type, String name)
- LocalVariable
Local variables are local to a specific function in a specific process. They can only be accessed within the function body.
Java interface: LocalVariableIF
Method to create: Model.newLocalVariable(FunctionIF function, TypeIF type,
String name)
- FormalVariable
Formal variables are the formal parameters to a function. They are a special type of local variable.
Java interface: FormalVariableIF
Method to create: Model.newFormalVariable(FunctionIF function, TypeIF type,
String name, int index)
- BoundVariable
Bound variables are specific to an expression; these are variables from forall and exists statements.
Java interface: BoundVariableIF
Method to create: ModelFactory.boundVariable(String name, ModelIF model,
TypeIF type, QuantifierExpressionIF expr)
Types
- ArrayType
Java interface: ArrayTypeIF
Methods to create: ModelFactory.arrayType(TypeIF),
ModelFactory.arrayType(TypeIF, int)
- FunctionType
Java interface: FunctionTypeIF
Method to create: ModelFactory.functionType(TypeIF[] inputTypes, TypeIF outputType)
- PointerType
Java interface: PointerTypeIF
Method to create: ModelFactory.pointerType(TypeIF baseType)
- RecordType
Java interface: RecordTypeIF
Method to create: ModelFactory.newRecordType(String name, String[] fieldNames,
TypeIF[] fieldTypes)
Expressions
- AddExpression
Java interface: BinaryExpressionIF
Method to create: ModelFactory.addExpression(ExpressionIF left, ExpressionIF right)
- MultiplyExpression
Java interface: BinaryExpressionIF
Method to create: ModelFactory.multiplyExpression(ExpressionIF left,
ExpressionIF right)
- DivideExpression
Java interface: BinaryExpressionIF
Method to create: ModelFactory.divideExpression(ExpressionIF left,
ExpressionIF right)
- AddressOfExpression
Java interface: UnaryExpressionIF
Method to create: ModelFactory.addressOfExpression(LHSExpressionIF argument)
- LHSExpression
- DereferenceExpression
Java interface: DereferenceExpressionIF
Method to create: ModelFactory.dereferenceExpression(ExpressionIF argument)
- RecordNavigationExpression
Java interface: RecordNavigationIF
Method to create: ModelFactory.recordNavigationExpression(
LHSExpressionIF recordExpression, String fieldName)
- ExistsExpression
Java interface: ExistsExpressionIF
Method to create: DynamicFactory.exists(ValueIF assumption, BoundVariableIF variable,
ValueIF boundExpression, ValueIF expression)
- ForallExpression
Java interface: ForallExpressionIF
Method to create: DynamicFactory.forall(ValueIF assumption, BoundVariableIF variable,
ValueIF boundExpression, ValueIF expression)
- IfThenElseExpression
Java interface: IfThenElseExpressionIF
Method to create: ModelFactory.ifThenElseExpression(ExpressionIF condition,
ExpressionIF trueValue, ExpressionIF falseValue)
- LiteralExpression
Java interface: LiteralExpressionIF
Methods to create: ModelFactory.literalExpression(boolean), modelFactory.literalExpression(double), modelFactory.literalExpression(float), modelFactory.literalExpression(int)
- NotEmptyExpression
Java interface: NotEmptyExpressionIF
Method to create: ModelFactory.notEmptyExpression(ModelIF model,
ExpressionIF source, ExpressionIF destination, ExpressionIF tag)
- NotFullExpression
Java interface: NotFullExpressionIF
Method to create: ModelFactory.notFullExpression(ModelIF model,
ExpressionIF source, ExpressionIF destination, ExpressionIF tag)
- VariableExpression
Java interface: VariableExpressionIF
Method to create: ModelFactory.variableExpression(VariableIF variable)
Locations
The locations fall into a number of categories, for the most part corresponding to the kinds of statements that can emanate from that location. Some locations only allow one outgoing statement, while others allow several, and others none.
- AllocateLocation
Java interface: AllocateLocationIF
Method to create: Model.newAllocateLocation(FunctionIF function)
- AssertionLocation
Java interface: AssertionLocationIF
Method to create: Model.newAssertionLocation(FunctionIF function)
- AssignmentLocation
Java interface: AssignmentLocationIF
Method to create: Model.newAssignmentLocation(FunctionIF function)
- AssumeLocation
Java interface: AssumeLocationIF
Method to create: Model.newAssumeLocation(FunctionIF function)
- BranchLocation
Java interface: BranchLocationIF
Method to create: Model.newBranchLocation(FunctionIF function,
ExpressionIF condition)
- ChoiceLocation
Java interface: ChoiceLocationIF
Method to create: Model.newChoiceLocation(FunctionIF function)
- DeallocateLocation
Java interface: DeallocateLocationIF
Method to create: Model.newDeallocateLocation(FunctionIF function)
- ForLoopLocation
Java interface: ForLoopLocationIF
Method to create: Model.newForLoopLocation(FunctionIF function,
ExpressionIF condition)
- InvocationLocation
Java interface: InvocationLocationIF
Method to create: Model.newInvocationLocation(FunctionIF function)
- StandardReceiveLocation
Java interface: StandardReceiveLocationIF
Method to create: Model.newStandardReceiveLocation(
FunctionIF function)
- ReturnLocation
Java interface: ReturnLocationIF
Method to create: Model.newReturnLocation(FunctionIF function)
- SendLocation
Java interface: SendLocationIF
Method to create: Model.newSendLocation(FunctionIF function)
- TerminalLocation
Java interface: TerminalLocationIF
Method to create: Model.newTerminalLocation(FunctionIF function)
Statements
Each statement has a single source location and a single destination location.
- AllocateStatement
Used to allocate contiguous memory for an array of elements, similar to C's "malloc." You specify the type of element and the number of elements to allocate an array of that length and element type. An allocation statement returns a pointer to the first element in the array.
Java interface: AllocateStatementIF
Method to create: Model.newAllocateStatement(
AllocateLocationIF sourceLocation, LHSExpressionIF lhs,
TypeIF elementType, ExpressionIF numElements)
- AssertionStatement
Used to input a boolean condition. The condition will be checked, and an error returned if it cannot be shown to hold.
Java interface: AssertionStatementIF
Method to create: Model.newAssertionStatement(
AssertionLocationIF sourceLocation, ExpressionIF assertion)
- AssignmentStatement
Statement of the form lhs = rhs;. Note that rhs is an expression. Expressions are side-effect free. In particular, they cannot involve function calls. There is a special InvocationStatement for dealing with function calls and assigning the returned value of the function call to a variable.
Java interface: AssignmentStatementIF
Method to create: Model.newAssignmentStatement(
AssignmentLocationIF sourceLocation, LHSExpressionIF lhs,
ExpressionIF rhs)
- AssumeStatement
Used to add a boolean statement to the path condition. A statement added in this will be assumed to hold for future statements.
Java interface: AssumeStatementIF
Method to create: Model.newAssumeStatement(
AssumeLocationIF sourceLocation, ExpressionIF assumption)
- DeallocateStatement
A deallocate statement deallocates previously allocated memory, similar to C's "free."
Java interface: DeallocateStatementIF
Method to create: Model.newDeallocateStatement(
DeallocateLocationIF sourceLocation, ExpressionIF pointerExpression)
- InvocationStatement
Represents a statement of the form lhs = f(a0, a1, ...); or the form f(a0, a1, ...); In the left hand side is null.
Java interface: InvocationStatementIF
Method to create: Model.newInvocationStatement(
InvocationLocationIF sourceLocation, LHSExpressionIF lhs,
FunctionIF callee, List arguments)
- NoopStatement
A statement that does nothing.
Java interface: NoopStatementIF
Method to create: Model.newLoopFalseBranchStatement(
LoopLocationIF sourceLocation), Model.newLoopTrueBranchStatement(
LoopLocationIF sourceLocation)
- ReceiveStatement
A statement to receive a message.
Java interface: ReceiveStatementIF
Method to create: Model.newReceiveStatement(
ReceiveLocationIF sourceLocation, LHSExpressionIF buffer,
ExpressionIF source, ExpressionIF tag)
- SendStatement
A statement to send a message.
Java interface: SendStatementIF
Method to create: Model.newSendStatement(SendLocationIF sourceLocation,
LHSExpressionIF buffer, ExpressionIF dest, ExpressionIF tag)
Functions
A function specifies a number of formal parameters, or "formal variables." In addition, it specifies a number of "proper local variables." All of these (formal and proper locals) are referred to as "local variables." The local variables can only be accessed within the function body.
The function body itself is a transition system. The function contains a set of locations and a set of statements. These define a directed graph in which the locations are nodes and the statements are edges. A function has a designated "start location," and thus every function must have at least one location.
Java interface: FunctionIF
Method to create: Model.newFunction(ProcessIF process, String name,
TypeIF returnType, int numFormals)
VSL