The set of C0 programs that are defined by the abstract syntax in Section 6.2 contains programs that get stuck for some input. For example, the following program is a syntactically-correct C0 program. (Which means that the sequence of characters in the program text complies with the concrete syntax of C0 and therefore we can attribute a unique abstract syntax tree with this text.) However, the execution of the program, as defined by the C0 semantics directly leads to a configuration in which the program gets stuck.
The reason is that the contents of x's container is not an address but an integer. For some programs, such as the program above, we can detect and prevent their getting stuck statically. We do this by means of a static semantics. This semantics gives “meaning” to the abstract syntax of a C0 program, hence the name semantics. This meaning is however not dependent on some input but independent of any input, hence it is static. Types of variables and expressions are one example for such a static property.
From the information that variable \(\CVar x\) has type \(\CInt\text{,}\) we want to deduce that for every program execution \(\CVar x\) contains an int and never, for example, an address. Hence, \(\CIndir{\CVar x}\) will always get stuck if \(\CVar x\) has type \(\CInt\text{.}\) In the following, we will formulate type rules that characterize programs for which such errors do not occur. We will call these programs then well-typed.
Since C0 is not a statically type-safe language, there will be programs that are well-typed but nevertheless get stuck, for example:
int x;
x = x + 1
RunListing6.6.1.\(\CVar x\) is read from but not written to before.
int x;
int *p;
{ int y; p = &y; }
x = *p;
RunListing6.6.2.After the inner block has been left, the pointer \(\CVar p\) is dangling (i.e. contains an invalid address) because the container of \(\CVar y\) has been freed.
int x = 666;
x = x / 0;
RunListing6.6.3.Division by zero also is undefined behavior in C.
This means that in C0 and C there are getting-stuck situations that are not ruled out by the static semantics. Languages where well-typed programs never get stuck are called statically type-safe 13
The static semantics of C0 is defined by relations that relate the abstract syntax of C0 with a type environment. The type environment maps, based on variable declarations, identifiers to types. These relations are defined inductively for each language element of C0 which means that we can elaborate the typing relation for an expression based on the typing relations of its sub-expressions.
Before defining the typing relations for statements and expressions, we need to add types to C0. For the sake of simplicity, we only define the concrete syntax here, since we mostly use concrete syntax for better readability in our formal development.
C supports implicit type conversion which means that at some places values of some type can be automatically (without further annotations by the programmer) converted to a value of a different type. For example, a \(\CPtr\CVoid\) can be implicitly converted into a \(\CPtr\CInt\) We model this here by the relation \(\castrel\text{.}\)
which we will inductively define over the syntax of C0. It is standard to use the following notation to indicate that a triple of type environment, expression, and type is in \(\ExprS\text{:}\)
\begin{equation*}
\typeGamma et \quad:\Longleftrightarrow\quad(\Gamma,e,t)\in\mathit{ExprS}
\end{equation*}
So, \(\typeGamma et\) says that expression \(e\) has type \(t\) under type environment \(\Gamma\text{.}\)
Definition6.6.6.Static Semantics of the C0 Expression Language.
The rule [TVar] determines the type of the expression ‘occurrence of a variable’ by looking up the type of the variable in the type environment. Constants are always int. Binary arithmetic expressions also always have the type int irrespective of the operand types. Arithmetic is only allowed for integer types. Pointer arithmetic is handled by two specific rules: [TPtrArith] to add an offset to a pointer and [TPtrDiff] to subtract two pointers of the same type. The results of comparisons are of integer type (executing them yields either 0 or 1). Pointers can also be compared. However, the operands of a comparison have to be implicitly convertible to each other: We can compare a \(\CPtr\CVoid\) with a \(\CPtr\CInt\) and a \(\CChar\) with a \(\CInt\) but not a \(\CPtr\CChar\) with a \(\CPtr\CInt\text{.}\) As a special case, pointers can be compared against 0 ([TPtrCmp] and [TPtrCmpN]). Additionally, [TPtrArith], [TPtrCmp], [TCmp], and [TPtrCmpN] also need variants to handle commutativity which we omit here for the sake of brevity.
Note however that comparing two pointers or subtracting two pointers that do not point to the same object is undefined behavior and will cause the program to get stuck. These cases are not caught by our type system.
Subsection6.6.2Statements and Programs
Similar to expressions we also use a relation to indicate if a statement and a program is well-typed. Now, statements and programs do not have a type themselves that we can associate with them. The well-typedness relation for statements and programs therefore merely captures if the expressions that are contained in the statements are well-typed. Therefore, the well-typedness relation is only binary and not ternary as the one for expressions:
The rules [TWhile] and [TIf] make sure that the condition expression they contain have a scalar type (i.e. are not \(\CVoid\)). The rule [TAssign] makes sure that the right-hand side type can be converted to the left-hand side type. This rules out a program like the following:
Most notably however is the rule [TBlock] which administers the type environment: In order for a block to be well-typed, its constituent statements must be well-typed under the type environment that additionally contains the local variables declared in the block. Note that this also models variable hiding: Variables declared in inner blocks hide the declarations of outer blocks.
Subsection6.6.3Examples
Let us consider a couple of examples that put our small type system to work and compute the types of several expressions or check the well-typedness of statements.
Example6.6.8.
Let's consider the derivation of the type of an expression with the type environment \(\Gamma\defeq\{\CVar x\mapsto\CPtr\CChar,\CVar y\mapsto\CInt\}\)
Here, we can see nicely that we are not able to prove the premise \(\typeGamma{\CVar x}{\CPtr\CChar}\) with [Var] because the the type environment does not provide the type \(\CPtr\CChar\) for \(\CVar x\text{.}\)
In statically type-safe languages (like C#, Java, OCaml, etc.), the semantics ensures that in exceptional situations that cannot be covered statically because they may depend on the input of a program, a certain well-defined behavior is triggered, such as throwing an exception.
