|
|
|
|
An informal specification of BIR.
Authors: Robby, Matthew Hoosier
In this documentation, we describe the constructs available in
the Bogor modeling language. We use grammar in the Extended Backus-Naur
Form (EBNF) to describe BIR production rules and regular expression to
denote lexical definitions of terminal symbols. For simplicity, we
often use double quotes (") to denote terminal symbols. For example,
"system" denotes the terminal symbol equivalent to the regular
expression 's' 'y' 's' 't' 'e' 'm', where the single quotes (') denote
characters. We use angle brackets to denote non-terminal symbols (e.g.,
<system>). We also liberally use angle brackets to denote
terminal symbols defined using regular expressions.
In the following sections, we describe each BIR construct in
details. For each construct, we give its concrete syntax and some
well-formed-ness rules. When describing the concrete syntax grammar, we
will choose readability of the grammar over ambiguity issues. However,
in some important cases, we will explicitly present the issues and how
we resolve them. We use paragraphs with "Namespace" as the header to
describe namespaces of BIR constructs (whenever applicable).
Identifiers that belong to the same namespace must be distinct. In some
cases, a namespace can be shadowed by another namespace; we will
explicitly describe the well-formed-ness rules in those cases.
We also give the Java abstract syntax tree (AST) class for
each construct in paragraphs with "Abstract Syntax Tree" as the header.
Note
In some cases, the UML diagrams used to present these syntax tree class
hierarchy may be out-of-date. The tool used to generate these is
presently incompatible with the J2SE 5.0 language in which Bogor is
written.
Figure 1,
“Concrete Syntax for Systems�? presents the
concrete syntax for BIR models. A BIR model begins with a declaration
of the system identifier <system-id> followed by
declarations of its members:
Namespace. System has its own
namespace and it is not shared with any other constructs.
Abstract Syntax Tree.
The abstract syntax tree class for BIR system is the System
class[1].
The top level Java AST class for system member is the SystemMember
class.
Before we describe each system member, we first describe BIR identifiers,
types,
and literals,
as they are used in various places when describing the system members.
Figure 3,
“Concrete Syntax for Identifiers�? presents the
concrete syntax and lexical definitions of BIR identifiers. They are
categorized into two: (1) normal identifiers, and (2) type variable
identifiers. There are two kinds of normal identifiers: (a) basic
identifiers, and (b) Bogor identifiers. Basic identifiers are similar
to Java identifiers. That is, they cannot have sequences of characters
that are equal to BIR keywords, boolean literals, the null literal, and
the float and double special literals (see bir-keywords).
Bogor identifiers are provided for convenience when
translating from other languages because one can encode almost anything
inside the Bogor identifiers. For example, when translating a Java
program that has system as a local variable identifier, the identifier
will clash with the BIR "system" terminal symbol (i.e., the BIR system
keyword). One can resolve this issue by always encode Java identifiers
inside one of the Bogor identifiers. For example, one can use a
convention to always encode Java local variables names using the
"[|"..."|]" identifier delimiters to avoid name clashes (e.g.,
"[|system|]").
Type variable identifiers can only be used as variables for
types (see generic types).
Notice that in the lexical definitions for identifiers in Figure 3,
“Concrete Syntax for Identifiers�?, we use
parameterized terminal symbols for simplicity (e.g.
<bogor-id-char(x)>).
Notice also that we use escape characters that are usually used in
other programming languages such as Java (e.g., '\n' and the unicode
escape characters). For simplicity, we define identifiers with -id as
their suffixes to be equivalent as <id>, unless specified
otherwise.
Examples.
this_is_a_basic_id{|this is a bogor id|}(|this is a bogor id|)<|this is a bogor
id|>[|this is a bogor id|]/|this is a bogor id|\\|this is a bogor id|/+|this is a bogor id|+.|this is a bogor id|.'this_is_a_type_var_id
Abstract Syntax Tree. Identifier
does not have dedicated Java abstract syntax tree class, instead, we
use java.lang.String
objects to represent BIR identifier.
Figure 4,
“Concrete Syntax for Types�? presents the concrete
syntax for BIR types. Similar to other modern programming languages,
BIR basic types are categorized into two general categories: (1)
primitive types, and (2) non-primitive (reference) types. In addition
to basic types, BIR features generic types (used strictly for
extensions). BIR also features functional types to support the
functional programming sub-language of BIR.
Abstract Syntax Tree.
The top level Java AST class for BIR (syntactic) type is the ASTType
class.
We describe each type category in details in the following
subsections. We use an italized font to denote variables representing
BIR values.
BIR primitive types consist of boolean types, integral types,
real types, and enumeration types, as well as special primitive types
such as the thread ID type used to hold BIR thread descriptors. In
addition, BIR features facilities to introduce new first-class
primitive types.
BIR does not support automatic primitive type promotions such
as in Java. For example, suppose we have a Java code as follows:
double x, z;
int y;
...
z := x + y;
Notice that in the last line, x
is automatically promoted to the double type before the addition is
evaluated. In contrast, x
should be casted explicitly in BIR. This restriction (or lack of
feature) is done to simplify the semantics of BIR constructs such as
the binary expressions. That is, when implementing the evaluation
binary expressions, one does not need to worry about type promotions.
Instead, all type promotions are handled in the cast
expression construct.
The boolean type "boolean" represents a type whose values
represent logical truth quantities (i.e., true and false).
Compatibility. The boolean type is
incompatible with the other types.
Default Value. The default value
for the boolean type is false.
Basic Operators. The
"&&", "||", "=>", "==", and "!=") binary
operators (see binary expression)
and the "!" unary operator (see unary expression)
can be used for boolean type.
Abstract Syntax Tree. The Java AST
class for (syntactic) boolean type is the ASTBooleanType
class.
There are four kinds of integral types:
-
the integral type "int", whose values range from
-2147483648 to 2147483647, inclusive.
-
int range types "int" "(" x
"," y
")", whose values range from x
to y,
inclusive. The range limitters x
and y
are either integer literals (see literals) or integer constants
(see constants).
Note that x
must be equal or less than y.
The minimum value for x
is -2147483647, and the maximum value for y
is 2147483647. Values outside the x
and y
range cannot be assigned/casted unless the "wrap" modifier is specified.
If the "wrap" modifier is specified, then values outside x and y are
wrapped so it become in range. There is a degree of freedom of what
should be done if a value outside of the range of an unwrapped range
type is assigned/casted to that type (e.g., raising an exception).
An advantage of having tighter bounds for values is that
one can compute fewer number of bits necessary to store the values a
priori. This is a very useful feature when doing explicit-state model
checking.
Note that the range is not checked statically, instead, it
is checked at run-time. Furthermore, range types do not affect the
semantics of arithmetic operators. That is, they are treated as if they
are non-range types. Thus, only the semantics of assignment (see assignment
action) and type casting (see cast expression)
are affected.
-
the long type "long", whose values range from
-9223372036854775808 to 9223372036854775807, inclusive.
-
long range types "long" "(" x
"," y
")", is similar to the int range type except that the mininum value for
x
is -9223372036854775808 and the maximum value for y is
9223372036854775807.
Compatibility. Integral types are
compatible with each other and with real types.
Default Values.
-
The default value of the int type is 0.
-
The default value of a int range type is 0, if x
<= 0 <= y.
Otherwise, the default value is x.
-
The default value of the long type is 0.
-
The default value of a long range type is 0, if x
<= 0 <= y.
Otherwise, the default value is x.
Basic Operators. The "+", "-",
"*", "/", "%", "==", "!=", "<", ">=", ">",
">=", "shl", "shr", "ushr", "&", "|", and "^" binary
operators (see binary expression)
and the "+" and "-" unary operators (see unary expression)
can be used for integral types.
Examples.
- int range types:
int (0, 8),
int wrap (-1, 8)
- long range types:
long (0,
10000000000L), long wrap
(0, 10000000000L)
Abstract Syntax Tree.
-
The Java AST class for (syntactic) int type is the ASTIntType
class.
-
The Java AST class for (syntactic) int range type is the ASTIntRangeType
class.
-
The Java AST class for (syntactic) long type is the ASTLongType
class.
-
The Java AST class for (syntactic) long range type is the ASTLongRangeType
class.
The BIR "float" and "double" real types follow Java's float
and double types, respectively (i.e., it uses the standard specified in
the Java Language Specification). The
special Not-a-Number (NaN) literal for BIR float type is "NaNf", while
the NaN literal for BIR double type is "NaNd". Furthermore, the special
positive/negative infinities for BIR float type and BIR double type are
"pINFf"/"nINFf" and "pINFd"/"nINFd", respectively.[2]
Compatibility. Real types are
compatible with each other and with integral types.
Default Values. The default value
of both float and double type is 0.0.
Basic Operators. The "+", "-",
"*", "/", "%", "==", "!=", "<", "<=", ">", and
">=" binary operators (see binary expression)
and the "+" and "-" unary operators (see unary expression)
can be used for float or double types.
Abstract Syntax Tree. The Java AST
class for (syntactic) float and double types are ASTFloatType
and ASTDoubleType
, respectively.
An enumeration type <enum-id> is a type whose
values are defined by the user using symbols (see enumerations).
Compatibility. Enumeration types
are incompatible with each other, and they are incompatible with other
types.
Default Value. The default value
of an enumeration type is the first declared element of the type.
Basic Operators. The "==" and "!="
binary operators (see binary expression)
can be used for enumeration types.
Abstract Syntax Tree. The Java AST
class for an enumeration (syntactic) type is the IdType
class. That is, it is parameterized by the enumeration
type's identifier.
The thread ID type represents a type whose values are BIR
thread descriptors. The intuition of having a separate type for thread
descriptors in a strongly typed language is that one can track where
the thread descriptors flow (i.e., it can only flow to a variable whose
type is the thread ID type).
Compatibility. The thread ID type
is incompatible with other types.
Default Value. The default value
of the thread ID type is the first thread descriptor created.
Basic Operators. The "==" and "!="
binary operators (see binary expression)
can be used for the thread ID type.
Abstract Syntax Tree. The Java AST
class for the thread ID (syntactic) type is the ASTThreadIdType
class.
4.1.6. Primitive
Extension Types
BIR supports introductions of new primitive types as
first-class types (see type extensions).
We call these types primitive extension types. A primitive extension
type is refered using the extension that declares the type followed by
dot (.) and the identifier of the type (e.g., <ext-id>
"." <prim-ext-type-id>). If the primitive extension type
is declared as a generic type, then the
arguments to its type variables must be supplied (i.e.,
<type-args>). This process is called instantiation of the
generic type. The arguments must match the constraints on the type
variables of the generic types (e.g., type compatibility and matching
number of parameters and arguments).
Compatibility. Primitive extension
types are incompatible with each other, and they are incompatible with
other types.
Default Value. The default values
of primitive extension types are defined by the module that declares
the types.
Basic Operators. The "==" and "!="
binary operators (see binary expression)
can be used for primitive extension types.
Abstract Syntax Tree. The Java AST
class for primitive type extension (syntactic) type is the ASTExtType
class.
Basic non-primitive types are reference types. There are five
kinds of non-primitive types: (1) record types, (2) array types, (3) a
string type, (4) a lock type, and (5) non-primitive extension types.
Compatibility. Non-primitive types
are incompatible with each other, with the exceptions of record and
array types.
Default Values. The default value
of non-primitive types is null.
Basic Operators. The "==" and "!="
binary operators (see records) can be used
for non-primitive types.
A record type <record-id> represents a type
whose values are named-tuple values consisting its fields' values (see record
declaration).
Abstract Syntax Tree. The Java AST
class for a record (syntactic) type is the IdType
class. That is, it is parameterized by the record type's
identifier.
An array type <basic-type> "[" "]" represents a
type whose values are fixed-size indexed collections of values of type
<basic-type>. Each array value has an implicit field
length that store the length/size of the array. The array index ranges
from 0 to the array length - 1.
Compatibility. In general, array
types are not compatible with each other. However, there is a degree of
freedom in this matter. For example, it is convenient to relax array
types compatibility when modeling Java programs as follows: an array
type is compatible with another array type if their ranks are equal
(i.e., the number of array dimensions), and the array base (non-array)
types are compatible for record types and equal for other types.
However, this relaxation causes the static type checking of BIR to
accept programs with bad types (unsound). This problem is also present
in Java and it can be illustrated as follows:
class Foo {
public void bar(Object[] baz)
{
if (baz != null && baz.length > 0)
{
baz[0] = new Foo();
}
}
}
We can now have a bad Java code that uses the Foo class as follows:
new Foo().bar(new String[1]);
The above code passed the static type checking in Java, but,
it will fail at runtime (i.e., it raises an exception of type java.lang.ArrayStoreException).
Thus, when this relaxation is used in BIR, every assignment to an array
element should be type checked again at run-time.
Abstract Syntax Tree. The Java AST
class for an array (syntactic) type is the ASTArrayType
class.
The string type "string" represents a type whose values are
immutable sequences of characters.
Abstract Syntax Tree. The Java AST
class for the string (syntactic) type is the ASTStringType
class.
The lock type "lock" represents a type whose values are used
for synchronization purposes. Although the guarded-command language
aspect of BIR provides means for synchronization, however, when
modeling programs from feature rich programming languages such as Java
programs, one often needs higher-level abstract data types. The lock
type is specifically designed to model Java monitors. A lock value
contains several information:
-
the thread descriptor of the lock's owner (if the lock is
held),
-
how many times the owner acquired the lock (if the lock is
held),
-
a wait set that contains thread descriptors where the
corresponding threads are waiting on the lock, and
-
a notification set that contains thread descriptors where
he corresponding threads have been notified after waiting on the lock.
Abstract Syntax Tree. The Java AST
class for the string (syntactic) type is the ASTLockType
class.
4.2.5. Non-Primitive
Extension Types
A non-primitive extension type is similar to a primitive
extension type, except that it is a reference type.
Abstract Syntax Tree. The Java AST
class for non-primitive type extension (syntactic) type is the ASTExtType
class.
The alias type represents the type associated with it (see type
alias declaration).
Abstract Syntax Tree. The Java AST
class for the alias type is the IdType
class.
BIR supports generic type that is strictly used for extension
types (see extensions) and
action/expression extension type arguments (see action
and expression
extensions). The genericity of the types arises because of the use of
type variables. Generic type cannot have corresponding value until it
is instantiated. Since generic type is only used for extensions, the
values of instantiated generic type depend on the extension module that
declares the generic type.
Abstract Syntax Tree. The Java AST
class for generic (syntactic) type is the ASTExtType
class.
BIR supports pure functional expression similar to what is
available in functional programming languages such as SML. A functional
type represents a type whose values are pure functional expressions.
The "unit" symbol indicates a function does not take parameters. String
values are used to represent functional types because all functional
expressions should be declared (named) globally, thus, the string
values are enough to distinguish which functional expressions are
referred.
Default Value. There is no default
value for a functional type because functional types cannot be used for
variables.
Abstract Syntax Tree. The Java AST
class for pure functional (syntactic) type is the ASTFunType
class.
Figure 6,
“Concrete Syntax for Literals�? presents the
lexical definitions for BIR literals. The literals are syntactic
representation of BIR values. BIR does not have a dedicated type for
characters, instead, the int type is used. Note that unicode escape
characters are not shown. A unicode pre-processor is used to convert
unicode escape characters to the corresponding unicode characters.
Examples.
- boolean literals:
true,
false
- char literals:
'a',
'b', 'c'
- int literals:
1,
2, 3
- long literals:
1l,
2l, 3L
- float literals:
1.0f,
2f, 3.0F, 4F
- double literals:
1.0d,
2d, 3.0D, 4D
- string literals:
"a",
"b", "c"
Abstract Syntax Tree.
The top level Java AST class for BIR literal is Literal. The
boolean, character, int, long, float, double, string, and null literals
Java AST classes are the BooleanLiteral
class, the IntLiteral
class, the IntLiteral
class, the LongLiteral
class, the FloatLiteral
class, the DoubleLiteral
class, the StringLiteral
class, and the NullLiteral
class, respectively.
Figure 8,
“Concrete Syntax for Constant Declaration�?
presents the concrete syntax for BIR constant declaration. Constants
are useful to parameterize BIR models. A constant declaration consists
of declarations of its identifier <const-id>, its
elements, and the literals assigned to the elements. The type of
constant elements depend on the type of the literals assigned to them.
Constant elements are not variables, instead, they are simply value
bindings of the literals to the constant element identifiers. The
bindings cannot be changed at run-time. The fully qualified name of a
constant element is <const-id> "."
<const-elem-id>. A constant element can only be referred
using its fully qualified name.
Namespace. The namespace for
constants is the global namespace that is shared with enumerations,
records,
extensions,
type-aliases,
global
variables, threads and
functions, virtual tables,
and functional
expressions. Each constant has its own namespace for its
elements.
Examples.
const C {
N = 5; // int constant
M = (int wrap (0, 255)) 5; // int wrap (0, 255) constant
L1 = 5L; // long constant
L2 = 5l; // long constant
L3 = -5L; // long constant
L4 = -5l; // long constant
F1 = 1.0F; // float constant
F2 = 1.0f; // float constant
F3 = -1.0F; // float constant
F4 = -1.0f; // float constant
F5 = 1F; // float constant
F6 = 1f; // float constant
F7 = -1F; // float constant
F8 = -1f; // float constant
D1 = 1.0; // double constant
D2 = 1.0D; // double constant
D3 = 1.0d; // double constant
D4 = -1.0; // double constant
D5 = -1.0D; // double constant
D6 = -1.0d; // double constant
D7 = 1D; // double constant
D8 = 1d; // double constant
D9 = -1D; // double constant
D10 = -1d; // double constant
C = 'c'; // char constant
B1 = true; // boolean constant
B2 = false; // boolean constant
S1 = null; // string constant
S2 = "s"; // string constant
}
Abstract Syntax Tree.
The Java AST class for BIR constant is the ConstantDefinition.
The top level Java AST class for BIR constant elements is Constant
class. The Java AST class for boolean constant element, char constant
element, int constant element, long constant element, float constant
element, double constant element, and string constant element are the BooleanConstant
class, the IntConstant
class, the IntConstant
class, the LongConstant
class, the FloatConstant
class, the DoubleConstant
class, and the StringConstant
class, respectively.
7. Enumeration Declaration
Figure 10,
“Concrete Syntax for Enumeration Declaration�?
presents the concrete syntax for BIR enumeration type declarations. An
enumeration type declaration consists of declarations of its identifier
<enum-id> and its elements. The elements represents the
valid values of the enumeration type. The fully qualified name of an
enumeration element is <enum-id> "."
<enum-elem-id>. An enumeration element can only be
referred using its fully qualified name, except in virtual tables on
enumerations (see virtual table
declaration).
Namespace. The namespace for
enumerations is the global namespace that is shared with constants,
records,
extensions,
type-aliases,
global
variables, threads and
functions, virtual tables,
and functional
expressions. Each enumeration type has its own namespace for
its elements.
Examples.
enum Day {
Sunday, Monday, Tuesday, Wednesday, Thursday, Friday
}
Abstract Syntax Tree.
The Java AST class for BIR enumeration is the EnumDefinition
class. There is no dedicated Java AST class for enumeration element,
instead, the java.lang.String
class is used.
Figure 12,
“Concrete Syntax for Record Declaration�? presents
the concrete syntax for record declarations. A record r' can extend
another record r (i.e., r!= r'). The record r is called the (direct)
super record of r', and r' is called a (direct) sub-record of r. Super
record and sub-record relations are transitive relations (e.g, r is a
super record of r''s sub-records). The fields of r is implicitly
present in r', however, the implicit fields share the namespace of the
fields of r'. Furthermore, constructs that can be used for r can also
be used with r', but not necessarily the other way around. A record can
also extend multiple records.
The "top" modifier is used to indicate that the record is the
top record. That is, all other records that do not explicitly extend
another record extend the top record. In a BIR model, there can be at
most one top record. The "throwable" modifier is used to indicate the
record can be thrown as an exception. All sub-records of a throwable
record are also throwable.
In BIR, we allow a degree of freedom of how the language is
implemented. The language can be implemented in a way that is biased
toward a specific domain. For example, when modeling Java, it is
convenient to have each record contains an implicit lock. Thus, the
lock operations (see lock action)
and the lock tests (see lock test expression)
can be used directly on records. Another example, it is also convenient
to have arrays that can be treated as the top record because arrays are
objects in Java (i.e., they can be casted to the Java top object java.lang.Object). Thus, if a
top record is specified in a BIR model, then all array types "extend"
the top record in a sense that it can be casted to/from. This degree of
freedom, however, should be used carefully and it should be documented
clearly when used.
Namespace. The namespace for
records is the global namespace that is shared with constants,
enumerations,
extensions,
type-aliases,
global
variables, threads and
functions, virtual tables,
and functional
expressions. Each record type has its own namespace for its
fields. Note that fields of a record are implicitly present in its
sub-records. This means that the inherited fields will also use the
namespace of each sub-record's field namespace.
Examples.
top throwable record A { int x; }
throwable record B { int y; }
record C extends A, B { int z; }
Abstract Syntax Tree.
The Java AST class for BIR records is the RecordDefinition
class. The Java AST class for BIR record field is the TypedId
class.
Figure 14,
“Concrete Syntax for Extension Declaration�?
presents the concrete syntax for extension declaration. Extension
declaration is used to introduce new first-class constructs. An
extension declaration begins with the declaration of the extension
identifier, followed by the Java class that implements it and the
language extension definitions. There are three kind of language
extension definition for BIR: (1) type extension, (2) expression
extension, and (3) action extension. Each extension definition's fully
qualified name is prefixed with the name extension identifier
<ext-id> and dot (".") and it can only be referenced
using its fully qualified name (even when used in declaring other
language extension definitions within the same extension). We describe
each extension definition in the following subsections.
Namespace. The namespace for
extensions is the global namespace that is shared with constants,
enumerations,
records,
type-aliases,
global
variables, threads and
functions, virtual tables,
and functional
expressions. Each extension has its own namespace for its
language extension definitions.
Abstract Syntax Tree.
The Java AST class for extension declaration is the ExtensionDefinition
class.
9.1. Type
Extension Declaration
Type extension is used to introduce new data types. Following
the categories of BIR basic types, there are two kinds of type
extension: (1) primitive type extension using the "ptypedef" keyword,
and (2) non-primitive (reference) type extension using the "typedef"
keyword. Regardless of the kind, each type can be declared as a generic
type by specifying the parameters of the type using type variables.
In general, a type variable can be substituted by any basic
type when the extension (generic) type is instantiated. However, there
are special prefixes for type variable identifiers to constrain the
kind of types that they may match
-
"`integral$", constrains a type variable to only accepts
integral types,
-
"`real$", constrains a type variable to only accept real
types,
-
"`numeral$", constrains a type variable to only accepts
integral or real types,
-
"`enum$", constrains a type variable to only accept
enumeration types,
-
"`record$", constrains a type variables to only accepts
record types,
-
"`array$", constrains a type variables to only accept
array types.
Generic type is used to conveniently reduce redundant
extension declarations. For example, one can contribute a set type that
works for all BIR types. A non-generic type solution would require one
to declare the set extensions for every element type instance that is
used in a model. Instead, a generic solution allows the possibility of
the generic set to be instantiated with any basic type for its element.
However, we limit the use of generic types only for extensions because
all types in closed systems (i.e., BIR models) should be known. Thus,
all other constructs in BIR only need to work with non-generic types or
instances of generic types.
Examples.
extension MyExtension for mypackage.MyExtensionModule {
typedef type1; // non-primitive extension type
typedef type2<'a>; // parametric non-primitive extension type
typedef type3<'enum$a, 'rec$a>; // parametric non-primitive extension type
ptypedef type4; // primitive extension type
ptypedef type5<'numeral$a>; // parametric primitive extension type
ptypedef type6<'array$a, 'real$a>; // parametric primitive extension type
}
Abstract Syntax Tree. The Java AST
class for type extension is the TypeExtension
class.
9.2. Expression
Extension Declaration
Expression extension is used to introduce new BIR expressions.
Following the spirit of BIR expression, the new
expression constructs should be side-effect free, but they are allowed
to be non-deterministic. Note that an expression can create a new
object because the object creation does not change the state (until the
new object is assigned to a variable). An expression extension can also
be defined to be polymorphic by specifying type parameters using type
variables similar to generic type extension. If the expression
extension takes or returns a parametric type, then it has to be
declared to be parametric. In addition, expression extension parameters
can be defined as lazy parameters. Arguments to lazy parameters are not
evaluated, instead the argument expression ASTs are passed.
Furthermore, expression extension can take a functional
expression as its parameter.
Examples.
extension MyExtension for mypackage.MyExtensionModule {
typedef type<'a>; // parametric non-primitive extension type
// foo is parameterized by 'a and 'b, takes two parameters
// and returns an int
expdef int foo<'a, 'b>(MyExtension.type<'a>, MyExtension.type<'b>);
// bar takes zero or more int parameters and returns an int
expdef int bar(int ...);
// bar takes one or more int parameters and returns an int
expdef int baz(int, int...);
// bazz takes two lazy expressions of type boolean
expdef boolean bazz(lazy boolean, lazy boolean);
// bazzz takes: (1) a function that takes an int and
// returns boolean and (2) one or more ints
expdef int bazzz(int -> boolean, int, int ...);
}
Abstract Syntax Tree. The Java AST
class for exp extension is the ExpExtension
class.
9.3. Action
Extension Declaration
Action extension is similar to expression extension. However,
it is allowed to have side-effect, but cannot return values.
Examples.
extension MyExtension for mypackage.MyExtensionModule {
typedef type<'a>; // parametric non-primitive extension type
// foo is parameterized by 'a and 'b, takes two parameters
actiondef foo<'a, 'b>(MyExtension.type<'a>, MyExtension.type<'b>);
// bar takes zero or more int parameters
actiondef bar(MyExtension.type<int>, int ...);
// bazz takes two expressions of type boolean
actiondef bazz(lazy boolean, boolean);
// bazzz takes: (1) a function that takes an int and
// (2) one or more ints
actiondef bazzz(int -> boolean, int, int ...);
}
Abstract Syntax Tree. The Java AST
class for action extension is the ActionExtension
class.
10. Type-alias
Declaration
Figure 16,
“Concrete Syntax for Type-alias Declaration�?
presents the concrete syntax for type-alias declaration. Type-alias is
used to introduce an alias name for a type. That is, every use of the
new type name will be substituted by the actual type, and used for
conveniently introducing compact names for types. A type-alias can be
used to introduce an alias for any basic type; cycles cannot be
introduced because type-alias declarations are considered in the order
of their declarations.
Namespace. The namespace for
type-aliases is the global namespace that is shared with constants,
enumerations,
records,
extensions,
global
variables, threads and
functions, virtual tables,
and functional
expressions.
Examples.
typealias byte int wrap(0, 255);
typealias abc Triple.type<A, B, C>;
typealias abcset Set.type<abc>;
Abstract Syntax Tree.
The Java AST class for type-alias declaration is the TypeAliasDefinition
class.
11. Global Variable
Declaration
Figure 18,
“Concrete Syntax for Global Variable Declaration�?
presents the concrete syntax for global variable declarations. Global
variables are accessible by any thread, function, or functional
expression. If the global initialization is specified in a global
variable declaration, then the global variable has the value specified
by the literal in the initial state of the model. If the transient modifier is used, then
the global variable is not stored in the state vector.
Namespace. The namespace for
global variables is the global namespace that is shared with constants,
enumerations,
records,
extensions,
type-aliases,
threads and
functions, virtual tables,
and functional
expressions.
Examples.
int n1; // int global variable
int n2 := 5; // int global variable
int wrap (0, 255) m1; // int wrap (0, 255) global variable
int wrap (0, 255) m2 := (int wrap (0, 255)) 5; // int wrap (0, 255) global variable
long l1; // long global variable
long l2 := 5L; // long global variable
long l3 := 5l; // long global variable
long l4 := -5L; // long global variable
long l5 := -5l; // long global variable
float f1; // float global variable
float f2 := 1.0F; // float global variable
float f3 := 1.0f; // float global variable
float f4 := -1.0F; // float global variable
float f5 := -1.0f; // float global variable
float f6 := 1F; // float global variable
float f7 := 1f; // float global variable
float f8 := -1F; // float global variable
float f9 := -1f; // float global variable
double d1; // double global variable
double d2 := 1.0; // double global variable
double d3 := 1.0D; // double global variable
double d4 := 1.0d; // double global variable
double d5 := -1.0; // double global variable
double d6 := -1.0D; // double global variable
double d7 := -1.0d; // double global variable
double d8 := 1D; // double global variable
double d9 := 1d; // double global variable
double d10 := -1D; // double global variable
double d11 := -1d; // double global variable
int c := 'c'; // char/int global variable
boolean b1 := true; // boolean global variable
boolean b2 := false; // boolean global variable
string s1 := null; // string global variable
string s2 := "s"; // string global variable
Abstract Syntax Tree.
The Java AST class for global variable declaration is the Global
class.
12. Thread and Function
Declarations
Figure 20,
“Concrete Syntax for Thread and Function Declarations�?
presents the concrete syntax for thread and function declarations.
Threads and functions are similar, except that functions can return
values. If the "active" modifier is used, then the thread is alive in
the initial state of the system; one can optionally put the
multiplicities for an active thread to specify the number of instances
of that thread in the initial state.
There are two kinds of thread and function bodies in BIR: (1) low-level body,
and (2) high-level
body. Low-level body is unstructured (similar to Java
bytecode), while high-level body is structured (similar to Java
sourcecode). Bogor actually works on the low-level body; it first
translates high-level bodies to their low-level equivalents.
Namespace. The namespace for
threads and functions is the global namespace that is shared with constants,
enumerations,
records,
extensions,
type-aliases,
virtual
tables, and functional
expressions.
Abstract Syntax Tree.
The Java AST class for both thread and function declarations
is the FSM
class.
12.1. Parameters
and Local Variables
Namespace. Each thread and
function has its own namespace for parameters and local variables
(i.e., parameters and local variables share the same namespace), but
hiding the name in the global namespace is disallowed.
Abstract Syntax Tree. The Java AST
class for parameters is the TypedId
class. The Java AST class for local is the Local
class.
13. Low-level Thread
or Function Body
Figure 22,
“Concrete Syntax for Low-level Thread or Function Body�?
presents the concrete syntax for low-level thread or function body.
Low-level body is designed as a target for translation from other
languages and as the representation that the model checking engine
works on, and also used for the representation used by the monotonic
dataflow analysis framework in Bogor. Low-level body is often used for
pedagogical reasons when describing concurrent models since its
interleaving points are explicit, i.e., interleavings only happen
between locations.
A low-level body consists of one or more locations followed by
zero or more catch declarations. See the next section
for examples.
Locations represent the control points of threads and
functions. The first declared location in a body is called the body's
initial location. When a thread is created, its program counter is set
to the initial location. Similarly, when a function is called, the
executing thread's program counter is set to the initial location of
the functio after the thread's stack frames are stored.
Each location can be annotated with a live variable set. The
live variable set indicates which parameters or local variables whose
values should be preserved after executing the location's
transformations. That is, parameters and local variables that are not
in the live set are set to their default values once any of the
location's transformation is executed. If the live set is not
specified, then Bogor automatically calculates this set by using the
well-known dead-variable analysis (using its monotonic dataflow
analysis framework).
Namespace. Each thread or function
has a dedicated namespace for its locations.
Abstract Syntax Tree. The Java AST
class for location declaration is the Location
class. The Java AST class for live sets is the LiveSet
class.
Transformations represent transitions in BIR. There are two
kinds of transformations: (1) block transformation and (2) invoke
transformation. Regardless of the kind, a transformation can have a
guard which is a predicate over state variables. If the guard is true
in a certain state or not specified, then the transformation is called
enabled in that state. In contrast, if the guard is false, then the
transformation is called disabled. When a thread is executed, it
non-deterministically chooses one of its enabled transformation to be
executed. Evaluation of a guard should not cause an exception to be
raised, however, there is a degree of freedom in the implementation of
how it can be handled (e.g., consider the guard to be true/false, or
raising an exception).
A transformation can be annotated with the "invisible" or the
"visible" modifiers. The invisible modifier indicates that the state
after the transformation is executed is invisible from the other
thread, thus, it prevents a thread context switch in that state (unless
all the transformations of the executing thread at the next state are
all disabled or none at all). The visible modifier is the dual of the
invisible modifier. When the modifiers are not specified, the
transformation are usually considered visible, unless a reduction
algorithm such as partial order reduction can determine that the
transformation is invisible.
Abstract Syntax Tree. The top
level Java AST class for transformation declaration is the Transformation
class.
13.2.1. Block
Transformation
A block transformation consists of a sequence of actions and a
jump. The actions are executed atomically.
Abstract Syntax Tree. The Java AST
class for block transformation is the BlockTransformation
class.
13.2.2. Invoke
Transformation
An invoke transformation is used to call a function. The call
can be facilitated using a virtual table
by using the "virtual" modifier. If the function that is called has a
return type, then the returned value can be assigned to a local
variable. The return type of the function should be compatible with the
type of the local variable.
PENDING: "reflect"
Abstract Syntax Tree. The Java AST
class for invoke transformation is the InvokeTransformation
class.
A jump indicates the next control point after a transformation
is executed. There are two kinds of jumps: (1) goto jump and (2) return
jump.
Abstract Syntax Tree. The top
level Java AST class for jump declaration is the NextState
class.
A goto jump "goto" <loc-id> indicates that the
next control point is the location <loc-id> within the
same thread or function (the <loc-id> must be declared).
Abstract Syntax Tree. The Java AST
class for goto jump is the GotoNextState
class.
For a thread, a return jump indicates that the thread is
terminated after the transformation is executed. For a function, a
return jump indicates that the next control point is the next control
point of the caller. If the function has a return type, then the local
variable that contains the value to be returned should be specified.
The type of the local variable should be compatible with the return
type of the function.
Abstract Syntax Tree. The Java AST
class for return jump is the ReturnNextState
class.
A catch construct indicates the throwable record that can be
caught at the specified locations. Once caught, the throwable record is
assigned to the local variable and then the control point is
transferred according to the jump construct that is specified. When an
exception is raised, the catch declarations are consulted in the order
of their declarations. If there is no catch whose throwable record type
is equal (or the super record of the record being thrown), then the
exception is propagated up to the call chain. If the exception is not
handled at the top of the call chain (i.e., the threads), then the
exception is uncaught. Uncaught exceptions are errors in the model.
Abstract Syntax Tree. The Java AST
class for catch declaration is the Catch
class.
14. High-level
Thread or Function Body
Figure 23,
“Concrete Syntax for High-level Thread or Function Body�?
presents the concrete syntax for high-level thread or function body.
High-level body is designed for manual Bogor model construction, and it
offers high-level control structure constructs found in most imperative
programming languages such as Java. In addition, it features guarded
command and atomic constructs to naturally model concurrent programs.
A high-level body consists of a sequence of statements. These
sequence of statements are translated for their low-level equivalents
before model checking. We now describe the statement constructs
available in BIR, and we illustrate how they are translated to
low-level via examples.
Abstract Syntax Tree.
The top Java AST class for statement is the Statement
class.
Atomic statement is used to group transitions into one
indivisible block. Another thread cannot interleave the execution of
atomic statement until it (normally or exceptionally) terminates.
Examples.
- High-level example:
system AtomicExample {
int x;
int y;
active thread MAIN() {
atomic
x := x + 1;
y := y + 1;
end
}
}
- Translated code in low-level:
system AtomicExample {
throwable record A extends ANY_THROWABLE {}
int x;
int y;
active thread MAIN() {
ANY_THROWABLE atomicCatch$Local;
loc loc0: do { Atomic.beginAtomic(); } goto loc1;
loc loc1: do { x := x + 1; } goto loc2;
loc loc2: do { y := y + 1; } goto loc3;
loc loc3: do { Atomic.endAtomic(); } goto loc4;
loc loc4: do { } return;
loc atomicCatch: do { Atomic.endAtomic();
throw atomicCatch$Local;
} goto atomicCatch;
catch ANY_THROWABLE atomicCatch$Local
at loc1, loc2 goto atomicCatch;
}
extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule {
actiondef beginAtomic ();
actiondef endAtomic ();
}
throwable record ANY_THROWABLE {}
}
Abstract Syntax Tree. The Java AST
class for atomic statement is the AtomicStatement
class.
While statement in BIR is similar to while statement in most
imperative programming language, i.e., it iteratively execute its body
until its condition is no longer hold.
Examples.
- High-level example:
system WhileExample {
active thread MAIN() {
int i := 0;
while i < 10 do
i := i + 1;
end
}
}
- Translated code in low-level:
system WhileExample {
active thread MAIN() {
int i := 0;
boolean temp$0;
loc loc0: do { temp$0 := i < 10; } goto loc1;
loc loc1: when temp$0 do { } goto loc2;
when !(temp$0) do { } goto loc4;
loc loc2: do { i := i + 1; } goto loc3;
loc loc3: do { } goto loc0;
loc loc4: do { } return;
}
}
Abstract Syntax Tree. The Java AST
class for while statement is the WhileStatement
class.
If statement in BIR is also similar to if statement in most
imperative programming languages, i.e., it executes its first body
whose condition holds.
Examples.
- High-level example:
system IfExample {
int i := 0;
active[3] thread MAIN() {
atomic
if i < 1 do
i := i + 1;
elseif i < 2 do
i := i + 2;
else do
i := i + 3;
end
end
}
}
- Translated code in low-level:
system IfExample {
int i := 0;
active [3] thread MAIN() {
boolean temp$0;
boolean temp$1;
ANY_THROWABLE atomicCatch$Local;
loc loc0: do { Atomic.beginAtomic(); } goto loc1;
loc loc1: do { temp$0 := i < 1; } goto loc2;
loc loc2: when temp$0 do { } goto loc3;
when !(temp$0) do { } goto loc5;
loc loc3: do { i := i + 1; } goto loc4;
loc loc4: do { } goto loc10;
loc loc5: do { temp$1 := i < 1; } goto loc6;
loc loc6: when temp$1 do { } goto loc7;
when !(temp$1) do { } goto loc9;
loc loc7: do { i := i + 1; } goto loc8;
loc loc8: do { } goto loc10;
loc loc9: do { i := i + 3; } goto loc10;
loc loc10: do { Atomic.endAtomic(); } goto loc11;
loc loc11: do { } return;
loc atomicCatch: do {
Atomic.endAtomic();
throw atomicCatch$Local;
} goto atomicCatch;
catch ANY_THROWABLE atomicCatch$Local at loc1, loc2,
loc3, loc4, loc5, loc6, loc7, loc8, loc9 goto atomicCatch;
}
extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule {
actiondef beginAtomic ();
actiondef endAtomic ();
}
throwable record ANY_THROWABLE {}
}
Abstract Syntax Tree. The Java AST
class for if-statement is the IfStatement
class.
Choose statement non-deterministically executes its bodies
whose conditions hold. Bogor first evaluates all the conditions, and in
a full-state-space exploration mode, it introduces branches in the
state-space for each body whose condition evaluates to true. The else
body is executed only when the other conditions evaluate to false. Note
that the conditions and the first instructions of the bodies whose
conditions hold are evaluated atomically.
Examples.
- High-level example:
system ChooseExample {
int i := 0;
active[3] thread MAIN() {
atomic
choose
when <i < 1> do
i := i + 1;
when <i < 2> do
i := i + 2;
else do
i := i + 3;
end
end
}
}
- Translated code in low-level:
system ChooseExample {
int i := 0;
active [3] thread MAIN() {
boolean temp$0;
boolean temp$1;
boolean temp$2;
ANY_THROWABLE atomicCatch$Local;
loc loc0: do { Atomic.beginAtomic(); } goto loc1;
loc loc1: do invisible {
temp$0 := i < 1;
temp$1 := i < 2;
temp$2 := !((temp$0 || temp$1));
} goto loc2;
loc loc2: when temp$0 do invisible { } goto loc3;
when temp$1 do invisible { } goto loc5;
when temp$2 do invisible { } goto loc7;
loc loc3: do { i := i + 1; } goto loc4;
loc loc4: do { } goto loc9;
loc loc5: do { i := i + 2; } goto loc6;
loc loc6: do { } goto loc9;
loc loc7: do { i := i + 3; } goto loc8;
loc loc8: do { } goto loc9;
loc loc9: do { Atomic.endAtomic(); } goto loc10;
loc loc10: do { } return;
loc atomicCatch: do {
Atomic.endAtomic();
throw atomicCatch$Local;
} goto atomicCatch;
catch ANY_THROWABLE atomicCatch$Local at loc1, loc2, loc3,
loc4, loc5, loc6, loc7, loc8 goto atomicCatch;
}
extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule {
actiondef beginAtomic ();
actiondef endAtomic ();
}
throwable record ANY_THROWABLE {}
}
Abstract Syntax Tree. The Java AST
class for choose statement is the ChooseStatement
class.
Try statement is used to handle raised exceptions similar to
the try-catch statement in Java. For each of catch clauses, a throwable
record type and a local variable identifier must be supplied that
indicate the throwable type to be caught and stored to the variable.
Note that, the local variable has to be declared in the beginning of
the thread and function body. When an exception is raised in the try
body, then the catch clauses are considered in the order of its
declaration. If there is no catch clause that handles the raised
exception, then the exception is transferred to the caller function, or
if it is a thread, then it is considered an uncaught exception, i.e.,
an error in the model.
Examples.
- High-level example:
system TryExample {
throwable record NPE { }
record A { int x; }
active thread MAIN() {
A a;
NPE npe;
try
assert a.x > 0;
catch (NPE npe)
a := null;
end
}
}
- Translated code in low-level:
system TryExample {
throwable record NPE {}
record A { int x; }
active thread MAIN() {
A a;
NPE npe;
int temp$0;
loc loc0: do { temp$0 := a.x; } goto loc1;
loc loc1: do { assert temp$0 > 0; } goto loc2;
loc loc2: do { } goto loc5;
loc loc3: do { a := null; } goto loc4;
loc loc4: do { } goto loc5;
loc loc5: do { } return;
catch NPE npe at loc0, loc1, loc2 goto loc3;
}
}
Abstract Syntax Tree. The Java AST
class for try statement is the TryStatement
class.
Return statement is used to exit from function (i.e., return
to the caller) and thread (i.e., the thread dies) similar to Java. If
the function has a return type, then the return statement should have
an expression whose type is compatible with the return type.
Examples.
- High-level example:
system ReturnExample {
active thread MAIN() {
assert fact(3) == 6;
}
function fact(int x) returns int {
return x <= 1 ? 1 : x * fact(x - 1);
}
}
- Translated code in low-level:
system ReturnExample {
active thread MAIN() {
int temp$0;
loc loc0: temp$0 := invoke fact(3) goto loc1;
loc loc1: do { assert temp$0 == 6; } goto loc2;
loc loc2: do { } return;
}
function fact(int x) returns int {
boolean temp$0;
int temp$1;
int temp$2;
int temp$3;
loc loc0: do { temp$0 := x <= 1; } goto loc1;
loc loc1: when temp$0 do { } goto loc2;
when !(temp$0) do { } goto loc3;
loc loc2: do { temp$1 := 1; } goto loc6;
loc loc3: do { temp$2 := x - 1; } goto loc4;
loc loc4: temp$3 := invoke fact(temp$2) goto loc5;
loc loc5: do { temp$1 := x * temp$3; } goto loc6;
loc loc6: do { } return temp$1;
}
}
Abstract Syntax Tree. The Java AST
class for return statement is the ReturnStatement
class.
Action statement represents a BIR action at the high-level
body.
Examples.
- High-level example:
system ActionExample {
int x;
active thread MAIN() {
x := x + 1;
}
}
- Translated code in low-level:
system ActionExample {
int x;
active thread MAIN() {
int temp$0;
loc loc0: do { temp$0 := x; } goto loc1;
loc loc1: do { x := temp$0 + 1; } goto loc2;
loc loc2: do { } return;
}
}
Abstract Syntax Tree. The Java AST
class for action statement is the ActionStatement
class.
14.1.8. Atomic
Action Statement
Atomic action statement represents a BIR action that is
executed atomically similar to the atomic statement. This syntax is
introduced for convenience.
Examples.
- High-level example:
system AtomicActionExample {
int x;
active thread MAIN() {
<x := x + 1;>
}
}
- Translated code in low-level:
system AtomicActionExample {
int x;
active thread MAIN() {
ANY_THROWABLE atomicCatch$Local;
loc loc0: do { Atomic.beginAtomic(); } goto loc1;
loc loc1: do { x := x + 1; } goto loc2;
loc loc2: do { Atomic.endAtomic(); } goto loc3;
loc loc3: do { } return;
loc atomicCatch: do {
Atomic.endAtomic();
throw atomicCatch$Local;
} goto atomicCatch;
catch ANY_THROWABLE atomicCatch$Local
at loc1 goto atomicCatch;
}
extension Atomic for edu.ksu.cis.bogor.projects.bogor.ext.atomicity.AtomicModule {
actiondef beginAtomic ();
actiondef endAtomic ();
}
throwable record ANY_THROWABLE {}
}
Skip statement allows one to move to the next control point.
Examples.
- High-level example:
system SkipExample {
active thread MAIN() {
skip;
choose
do
skip;
do
skip;
end
}
}
- Translated code in low-level:
system SkipExample {
active thread MAIN() {
boolean temp$0;
boolean temp$1;
loc loc0: do invisible {
temp$0 := true;
temp$1 := true;
} goto loc1;
loc loc1: when temp$0 do invisible { } goto loc2;
when temp$1 do invisible { } goto loc3;
loc loc2: do { } goto loc4;
loc loc3: do { } goto loc4;
loc loc4: do { } return;
}
}
Abstract Syntax Tree. The Java AST
class for atomic action statement is the AtomicActionStatement
class.
15. Virtual Table
Declaration
Figure 25,
“Concrete Syntax for Virtual Table Declaration�?
presents the concrete syntax for virtual table definitions. BIR virtual
tables are used to model dynamic dispatch of methods in OOP language or
type-safe function pointers. There are two kinds of virtual tables: (1)
records-based and (2) enumeration-based.
Namespace. The namespace for
virtual tables is the global namespace that is shared with constants,
enumerations,
records,
extensions,
type-aliases,
threads and
functions, and functional
expressions.
Abstract Syntax Tree.
The Java AST class for virtual table declaration is the VirtualTableDefinition
class.
A records-based virtual table maps the records in the virtual
table to the functions that handle the call. The first parameter of a
function that is mapped to handle a record type should accept the
record type or one of its super-records. The non-first parameter types
of all functions in the virtual table should match (equivalent).
Furthermore, the records that are handled by a virtual table should be
closed under the sub-records relation. That is, if a record r is mapped
in a virtual table, then all sub-records of r should also be mapped.
An enumeration-based virtual table is similar to the
records-based, except that an enumeration type is used instead of
record types. The virtual table should map all elements (values) of the
specified enumeration type.
16. Functional Expression
Declaration
BIR features functional expression usually found in functional
programming languages such as SML. Functional expressions can be
recursive and are useful, for example, to express sophisticated heap
properties because data structures are usually recursive (or mutually
recursive). Since BIR expressions are side-effect free, thus,
functional expressions are also side-effect free. BIR currently only
support first-order functions; more advanced features may be added in
the future. Figure 27,
“Concrete Syntax for Functional Expression Declaration�?
presents the concrete syntax for functional expression declaration.
Namespace. The namespace for
functional expressions is the global namespace that is shared with constants,
enumerations,
records,
extensions,
type-aliases,
threads and
functions, and virtual tables.
Abstract Syntax Tree.
The Java AST class for functional expression declaration is
the Fun
class.
Figure 29,
“Concrete Syntax for Expressions�? presents the
concrete syntax of expressions. BIR expressions are strictly evaluated
for their values. In other words, BIR expressions are pure expressions
(i.e., side-effect free). We use paragraphs with "Type" as headers to
describe the type of the expressions. Table ?? presents the precedence
of BIR compound expression operators. Operators that are in the same
line have the same precedence. Operators listed higher than other
operators have higher precedence than the other operators. Operators
with higher precedence are evaluated before operators with lower
precedence. Unary expressions and the conditional expression are
right-associative; all other expressions are left-associative. We now
describe each expression construct in details in the following
subsections.
Non-atomic high-level expressions are translated to their
3-address code low-level equivalent.
Abstract Syntax Tree.
The top level Java AST class for expressions is the Exp class.
17.1. Literal
Expressions
A literal expression is an expression whose valuation is the
value represented by the literal.
Type. The type of a literal
expression is the same as the type of the literal.
Examples.
- Boolean literals:
true,
false
- Int literals:
1,
-1
- Double literals:
1.0,
-1.0d
- Float literals:
1.0f,
-1F
- String literals:
"a",
"b"
Abstract Syntax Tree. The Java AST
class for literal expression is the LiteralExp class.
17.2. Variable
Expression
A variable expression is an expression whose valuation is the
value being held (or bound) by the specified variable at the state (or
environment) where the expression is evaluated. Depending on where a
variable expression is used, the variable can refer to a global
variable, a local variable,
a let-local variable (see let expression),
or a functional
expression.
Type. The type of a variable
expression is the same as the type of the variable.
Examples.
Abstract Syntax Tree. The Java AST
class for variable expression is the IdExp class.
A unary expression is an expression whose valuation is
computed by applying its (unary) operator to the valuation of its
operand. There are three kinds of unary operators: (1) the logical
complement unary operator "!", (2) the plus unary operator "+", and (3)
the minus unary operator "!". The semantics of the operators are
defined similar to other programming languages such as Java.
Type. The type of a unary
expression is the same as the type of its operand.
Examples.
Abstract Syntax Tree. The Java AST
class for unary expression is the UnaryExp class. The unary operators
are defined in the UnaryOp class.
A binary expression is an expression whose valuation is
computed by applying its (binary) operator to the valuations of both of
its operands. Binary operators in BIR are:
-
the addition binary operator ("+"),
-
the substraction binary operator ("-"),
-
the multiplication binary operator ("*"),
-
the division binary operator ("/"),
-
the modulus (remainder) binary operator ("%"),
-
the equality test binary operator ("=="),
-
the inequality test binary operator ("!="),
-
the less than test binary operator ("<"),
-
the less than or equal test binary operator ("<="),
-
the greater than test binary operator (">"),
-
the greater than or equal to test binary operator
(">="),
-
the shift left binary operator ("shl"),
-
the shift right binary operator ("shr"),
-
the unsigned shift right binary operator ("ushr"),
-
the conditional-and binary operator ("&&"),
-
the conditional-or binary operator ("||"),
-
the conditional-implication binary operator ("=>"),
-
the bit-wise-and binary operator ("&"),
-
the bit-wise-or binary operator ("|"), and
-
the bit-wise-xor binary operator ("^").
For binary conditional operators, the binary expression's
second operand may not be evaluated. The semantics of the operators are
defined similar to other programming languages such as Java ("shl",
"shr", and "ushr" are "<<", ">>", and
">>>" in Java, respectively).
Type. The types of a most binary
expression's operands must be equal if they are primitive types (the
shift operators <<, >>, and
>>> are the exception: they require that the left
operand be an integral type and the right operand be an integer). The
type of a binary expression depends on its operator's type. The type of
arithmetic operators ("+", "-", "*", "/", "%"), shift operators
("<<", ">>", and
">>>"), and bit-wise operators ("&", "|",
and "^") is the same as the type of the binary expression's operands.
All other operators are of type boolean.
Examples.
Abstract Syntax Tree. The Java AST
class for binary expression is the BinaryExp class. The binary
operators are defined in the BinaryOp class.
17.5. Conditional
Expression
A conditional expression is an expression whose valuation
depends on the valuation of its first operand. If the valuation of the
first operand is true, then, the valuation of the conditional
expression is the valuation of its second operand (its third operand
will not be evaluated). Otherwise, the valuation of the conditional
expression is the valuation of its third operand (its second operand
will not be evaluated).
Type. The first operand of a
conditional expression must be of type boolean. The second and third
operands must be of equal types. The type of a conditional expression
is the same as its second and third operands.
Examples.
b? null : "s"x > 0? 5 : 3
Abstract Syntax Tree. The Java AST
class for conditional expression is the ConditionalExp class.
17.6. Parenthesis
Expression
Parenthesis expression is used to override the precedence
rules for lower precendence compound expressions. The valuation of a
parenthesis expression is the valuation of the expression inside the
parenthesis.
Type. The type of a parenthesis
expression is the same as the type of the expression inside the
parenthesis.
Examples.
Abstract Syntax Tree. The Java AST
class for parenthesis expression is the ParenExp class.
Atomic expression is used to force the evaluation of the
contained expression to be indivisible. This expression can only be
used in high-level BIR as expression in low-level is atomic by default.
Type. The type of an atomic
expression is the same as the type of the contained expression.
Examples.
Abstract Syntax Tree. The Java AST
class for parenthesis expression is the AtomicExp class.
17.8. Record,
Array, and Lock Creation Expressions
There are three kinds of creation expressions: (1) record
creation expressions, (2) array creation expressions, and (3) the lock
creation expression. The valuation of a creation expression is a fresh
instance of the specified type.
Note that creation expressions are pure expressions because
they do not change the current state until the new instances are
assigned to some program variables.
Type. The type of a creation
expression is the type of the record, the array, or the lock being
created.
Examples.
new Anew int[6]new lock
Abstract Syntax Tree. The Java AST
classes for record creation, array creation, and lock creation are the NewRecordExp class, the NewArrayExp class, and the NewLockExp class, respectively.
17.9. Field
Access Expression
Field access expression is used to access a field value of a
record value or an array value (i.e., fields from the top record, if
any). If the record/array value is null, then a null pointer exception
is raised.
Examples.
Abstract Syntax Tree. The Java AST
class for field access expression is the FieldAccessExp class.
17.10. Array
Access Expression
Array access expression is used to access an element value of
an array value. If the array value is null, then a null pointer
exception is raised.
Examples.
Abstract Syntax Tree. The Java AST
class for array access expression is the ArrayAccessExp class.
Cast expression is used to coerce a value to one of its
compatible type value.
Examples.
(int wrap (0, 255) -1(B) a
Abstract Syntax Tree. The Java AST
class for cast expression is the CastExp class.
17.12. Kind-of
Expression
Kind-of expression is used to test a value's exact type.
Examples.
Abstract Syntax Tree. The Java AST
class for kind-of expression is the KindofExp class.
17.13. Instance-of
Expression
Kind-of expression is used to test a value's type with respect
to record extension (i.e., inheritance).
Examples.
a instanceof Bb instanceof C
Abstract Syntax Tree. The Java AST
class for instance-of expression is the InstanceofExp class.
17.14. Lock
Test Expressions
Lock test expressions are used to query the state of a lock:
(1) lockAvailable is used
to test whether a thread's attempt to acquire a lock would succeed
(that is, either the thread already owns the lock or the lock is
unowned), (2) hasLock is
used to test whether the current executing thread holds a lock, and (3)
wasNotified is used to
test whether there was a notification for a lock.
Examples.
lockAvailable(l)hasLock(l)wasNotified(l)
Abstract Syntax Tree. The Java AST
class for lock test expression is the LockTestExp class. The lock test
operators are defined in the LockTestOp class.
17.15. Thread
Test Expression
Thread test expression is used to determine the status of a
thread, i.e., whether the thread is terminated. It takes a tid value as
its argument (i.e., from the start thread action).
If the tid given as the operand is uninitialized (it does not reference
any thread either running or terminated), then the thread-test
operation returns true.
Example.
Abstract Syntax Tree. The Java AST
class for thread test expression is the ThreadTestExp class.
17.16. Let
Binding Expression
Let binding expression is used to bind a value to a name
similar to a construct in a functional programming language. Note that
the expression does not change the state. Also note that the name may
hide local variables or global variables.
Example.
Abstract Syntax Tree. The Java AST
class for let expression is the LetExp class.
17.17. Application
Expression
Application expression is used to apply functional
expression in both low-level and high-level BIR. In
high-level BIR, it also used to represent function
call.
Example.
Abstract Syntax Tree. The Java AST
class for apply expression is the ApplyExp class.
17.18. Extension
Call Expression
Extension call expression is used to call an expression
extension. For a parametric expression extension, Bogor tries to infer
the arguments to the declared parametric type variables. It is limited,
however, as it cannot infer the argument of a type variable that is
only used as the return type of the expression extension.
Example.
Set.create(1, 2, 3)Set.isEmpty(myset)
Abstract Syntax Tree. The Java AST
class for extension call expression is the ExtExp class.
Figure 31,
“Concrete Syntax for Actions�? presents the
concrete syntax for BIR actions declarations. Non-atomic high-level
actions are translated to their 3-address code low-level equivalent.
Abstract Syntax Tree.
The top level Java AST class for BIR actions is the Action
class.
Assign action is used to update the value of a variable, a
record/array field, or an array element.
Examples.
x := 1;x.f := 1;x[0] := 1;
Abstract Syntax Tree. The Java AST
class for assign action is the AssignAction
class.
Assert action is used to check whether the assert's condition
(of type boolean) holds. If the condition does not hold, then it is
considered as an error in the model.
Examples.
assert f(x);assert x > 0;
Abstract Syntax Tree. The Java AST
class for assert action is the AssertAction
class.
Assume action is used to filter paths. If the assume's
condition is false, then Bogor will backtrack from exploring the
current path.
Examples.
assume f(x);assume x > 0;
Abstract Syntax Tree. The Java AST
class for assume action is the AssumeAction
class.
18.4. Lock
Operation Action
Lock operation action is used to change the state of a lock
value:
lock acquires
the given lock so it is held by the current executing thread and set
the lock count to one if the lock is free. Otherwise, if the lock has
been held by the current executing thread, then it increases its lock
count by one. If not, then a bad monitor exception is raised.unlock
releases the given lock if the lock is held by the current executing
thread; it decreases the lock's lock count by one. If the lock count is
zero after the decrement, then the lock becomes free. If the current
executing thread does not hold the lock, then a bad monitor exception
is raised.wait puts the
current executing thread in the lock wait set and stores its lock count
in the state if the lock is held by the current executing thread.
Otherwise, a bad monitor exception is raised.unwait removes
the current executing thread from the lock's notification set and makes
the thread as the owner of the lock as well as restoring the lock's
lock count from the thread's lock count stored in the state (i.e., the
thread's lock count is removed from the state). The lock must be free
before unwait is
executed, otherwise, a bad monitor exception is raised. notify
non-deterministically removes one thread from the lock's wait set, if
any, and puts it in the lock's notification set. The current executing
thread must hold the lock, otherwisem a bad monitor exception is
raised. notifyAll
removes all threads from the lock's wait set and put them in the lock's
notification set. The current executing thread must hold the lock,
otherwisem a bad monitor exception is raised.
Examples.
Abstract Syntax Tree. The Java AST
class for lock operation actions is the LockAction
class. The lock operators are defined in the LockOp class.
18.5. Throw
Exception Action
Throw exception action is used to raise a throwable record
value.
Examples.
throw r;throw new ThrowableRecord;
Abstract Syntax Tree. The Java AST
class for throw exception action is the ThrowAction
class.
18.6. Start
Thread Action
Start thread action is used to create an instance of a thread,
and returns the newly created thread descriptor value (of type tid).
Examples.
start T(5);myTID := start T();
Abstract Syntax Tree. The Java AST
class for start thread action is the ExpAction
class with the StartThreadExp class.
Exit thread action is used to terminate the current executing
thread.
Example.
Abstract Syntax Tree. The Java AST
class for exit thread action is the ExitThreadAction
class.
18.8. Extension
Call Action
Extension call action is used to call an action extension. For
a parametric action extension, Bogor tries to infer the arguments to
the declared parametric type variables.
Examples.
Set.add(myset, 5);Set.remove(myset, 5);
Abstract Syntax Tree. The Java AST
class for extension call action is the ExpAction
class with the ExtExp class.
|
|
|
|
|
