SC22/WG14 N822 1998-05-03 Annex S (normative) Formal model of Sequence Points S.1 Introduction Subclause 6.3 reads in part: Between the previous and next sequence point an object shall have its stored value modified at most once by the evaluation of an expression. Furthermore, the prior value shall be accessed only to determine the value to be stored. This annex defines a formal algorithm for determining whether any given expression or set of expressions obeys this requirement, and therefore whether or not it involves unspecified or undefined behaviour. An implementation is not required to follow the model defined in this annex. In particular the model assumes serial evaluation, but parallel evaluation is equally valid. However, an implementation shall ensure - for all expressions that are not determined to be undefined in this model - that expressions are evaluated in a way that will yield one of the results specified by this model, and that each volatile object is accessed exactly the number of times determined by the model. S.2 Basic concepts This model operates in terms of "events". An expression or set of expressions give rise to a number of events and some constraints on their order of occurence. All possible arrangements that meet those constraints are then examined. If any of these arrangements involves undefined or unspecified behavior then so does the expression or set of expressions. S.2.1 Events An event is one of: - reading the value of a byte - writing a value to a byte - designation of a byte in an object - a function call - a sequence point. A "write" event does not mean that the value is stored immediately, but that it will be stored before the next sequence point. The model automatically takes this into account. S.2.2 Function calls Where an expression involves a function call, that call is "atomic" for the purposes of this model. There must be a sequence point immediately before (see 6.3.2.2) and after each function call (either because it ends in a full expression, or because it is required by 7.1.8), and so it can be seen that the effects of the call - for the purposes of the surrounding expression - can be determined purely by the read and write events involved in it, ignoring their ordering. These events cannot be interspersed with events from outside the call. Therefore this model treats a function call as being a sequence point. S.2.3 Short circuits and optimisation The && || and ?: operators are "short circuiting" - the way in which an expression containing them is evaluated depends on the operands. The model described in this annex handles this. Other expressions can sometimes be optimised, for example because the result of an operator can be determined from only some of the operands; the most obvious case is multiplication by constant zero. Not only does this model require the other operand be evaluated in this case, but all the implications of this model must continue to hold even where an optimising implementation could store values in objects earlier than the model would allow. [*] [*] Of course, provided the relevant side-effects take place as if the model were followed, any optimisation that yields a valid result (as specified in S.1) is permitted. S.2.4 Notation Events are written as follows: R(a) read the byte at address a; W(a) write the byte at address a; L(a) an lvalue designating the byte at address a; F(e) the call to the function designated by e; S a sequence point; D a dummy event with no effect. If it is necessary to distinguish separate events of the same kind, this is done by placing a number or name in braces after the event (such as "R(a,n){5}" or "S{pre}"). In addition the following notation is used: X < Y for each event P in those indicated by X, and each event Q in those indicated by Y, P must occur before Q; R(a,n) R(a), R(a+1), ... R(a+n-1) W(a,n) W(a), W(a+1), ... W(a+n-1) L(a,n) L(a), L(a+1), ... L(a+n-1) E(e) the events and constraints of expression e; V(e) the events and constraints of expression e, but with each L(a) event replaced by a (different) dummy event D; Z(e) the size (in bytes) of an object with the same type as the expression e (or 1 if e has function type). S.3 Operation of the model The model is operated in the following stages: (1) transforming each expression (2) identifying events and constraints (3) analysis of all possible orders of events Where more than one expression is involved, each is processed through the first two stages separately, and then combined as given in S.4 before the last stage. S.3.1 Transformation The first stage of analysis of an expression is to transform it to a canonical form. Then: each expression of the form is replaced by the form e->field (*(e)).field e1 [e2] *((e1)+(e2)) &*e e e1 && e2 where e1 is zero (e1) where e1 is nonzero ((e1) , (e2)) e1 || e2 where e1 is zero ((e1) , (e2)) where e1 is nonzero (e1) e1 ? e2 : e3 where e1 is zero ((e1) , (e3)) where e1 is nonzero ((e1) , (e2)) Note that the && || and ?: operators require multiple analyses to be made; the expression involves undefined behavior in those situations where the corresponding case does; if the value of e1 is unspecified, the expression involves undefined behavior if either alternative does. Finally, wherever subclause 6.3 requires an lvalue not of array type to be converted to the value stored in the designated object, replace the lvalue expression e by the expression $e and where it requires an lvalue of array type to be converted to a pointer to the first element of the array, or an lvalue of function type to be converted to a pointer to the function, replace it by the expression @e (where $ and @ are notional operators introduced by the model). S.3.2 Event identification Each sub-expression gives rise to a set of events and constraints on events as follows. A constant or string literal does not give rise to any events. A parenthesised expression gives rise to the same events and constraints that the unparenthesised version would. An identifier x gives rise to L(a,Z(x)), where a is the address of x. This includes the case where x has an array type. However, an identifier with function type does not give rise to any events. A compound literal (type){e1,e2,...} gives rise to L(a,Z(type)) plus the constraints E(e1) < L(a,Z(type)), E(e2) < L(a,Z(type)), etc, where a is the address of the object generated by the compound literal. A type name with variably modified type and containing the expressions e1, e2, etc. (in array declarators) gives rise to all the events and constraints from V(e1), V(e2), etc. (with no contraints between these). All other expressions give rise to events and constraints as follows: Expression Events and constraints --------------------------------------- $e E(e), but replacing each L(a) by R(a) @e V(e) e0(e1,e2,...) E(e0), E(e1), E(e2), etc. plus new F(e0), E(e0) < F(e0), E(e1) < F(e0), E(e2) < F(e0), etc. e.field E(e), but if this contains L(a,Z(e)) for some address a then that is replaced by L(a+b,Z(e.field)), where b is the offset of the field in the structure or union type ++e --e ) E(e), but replacing each L(a) by the pair [R(a), W(a)], e++ e-- ) with the constraint R(a) < W(a) for each such pair &e V(e) *e E(e) plus new L(a,Z(*e)), where a is the address pointed to, and the constraint E(e) < L(a,Z(*e)) sizeof e ) V(e) or V(type) if e or type has variably modified type sizeof(type) ) otherwise none +e -e !e ~e E(e) (type)e V(e), E(type) e1<op>e2 E(e1), E(e2) e1,e2 E(e1), E(e2), plus new S E(e1) < S, S < E(e2) e1=e2 E(e1) but replacing each L(a) by W(a), E(e2), E(e2) < W(a) for each W(a) created by the replacement e1<op=>e2 E(e1) but replacing each L(a) by the pair [R(a), W(a)], E(e2), and for each W(a) created by the replacement the constraints [E(e2), R(a)] < W(a) where the R(a) is the corresponding event created by the replacement <op> is any of * / % + - << >> < > <= >= == != & ^ | <op=> is any of *= /= %= += -= <<= >>= &= ^= |= S.3.3 Event analysis When all events and constraints in the expression have been determined, every possible arrangement of the remaining events[*] that obeys the constraints is considered. [*] There will be no L(a) events remaining, since they represent lvalues and these will have been made the operand of some operator, possibly a $ operator. If an arrangement contains W(a) followed by either R(a) or W(a) (for the same address a) without an intervening S or F event, the expression involves undefined behavior. Otherwise, if two different arrangements would have different effects then it is unspecified which results. [*] [*] This will occur if one arrangement contains W(a){1} followed by either R(a){2} or W(a){3} and the other arrangement contains either R(a){2} or W(a){3} followed by W(a){1} (in each case possibly with other events intervening). If an R(a) event applies to a volatile object, this is an access to the object. If there is more than one R(a) event for the same volatile object, the model shows which possible orderings can apply to the accesses for each purpose; if the value of the expression depends on the order of these accesses and the model permits more than one order, which order is used is unspecified. S.4 Application For each expression statement, and for each full expression in a selection, iteration, or jump statement, the expression shall be considered separately in its normal place in the sequence of execution. For each array declarator involving a variably modified type, and for each initializer list, the events of all the individual expressions shall be considered together with no constraints applying between events from two different full expressions. S.4.1 Signals If program execution is interrupted by a signal where the handler returns to the caller, the behavior shall be as if an F event for the signal handler were inserted at an unspecified place in the sequence of events forming the full expression or array declarator being evaluated at the time of the signal. S.4.2 Floating-point Environment For the purposes of this model, the floating-point exception flags constitute a single object and the remainder of the floating-point environment another single object. Any W event to the latter implies a W event to the former with the same constraints and with no constraint between the two. If the state of the FENV_ACCESS pragma is on, then any operation that sets a floating-point exception flag shall imply a W event for the floating-point exception flags ("WX") with the following constraints: Operations Constraints ---------------------------- $e ) WX shall occur after every event associated with +e -e !e ~e ) the sub-expression e1<op>e2 ) ++e --e ) WX shall have the same constraints as the W events e++ e-- ) generated in the analysis of the sub-expression, but e1=e2 ) may occur before any or all of those W events. e1<op=>e2 ) Notwithstanding S.3.3, if an arrangement contains more than one W event for the floating-point exception flags without an intervening S or F event, the behaviour shall not be undefined but it is unspecified which of the flags associated with the W events will be set (though at least one of those flags shall be set). [*] [*] If it were undefined to write twice to the flags between sequence points, it would not be practical to use the facilities of the <fenv.h> header in complicated expressions. S.5 Examples In these examples the type int and all pointer types have a size of 1, double has a size of 3, and addresses are in the range 1000 to 1999. In each case it is the final line that is being analysed. (1) int x, y, z; x = y + z; The canonical form is: x = $y + $z The events and constraints identified by each sub-expression are: x: L(1000){1} y: L(1234){2} z: L(1666){3} $y: R(1234){4} $z: R(1666){5} +: {4}, {5} =: W(1000){6}, {4}, {5}, [{4}, {5}] < {6} Since each address only appears in one R or W event, there is no undefined behavior. (2) int z, y; x = y++; // already in canonical form The events and constraints identified by each sub-expression are: x: L(1000){1} y: L(1234){2} y++: R(1234){3}, W(1234){4}, {3} < {4} =: W(1000){5}, {3}, {4}, {3} < {4}, [{3}, {4}] < {5} There is only one possible ordering: R(1234) : W(1234) : W(1000) Again each address only appears in one event, so there is no undefined behavior. (3) int x; x = ++x; // already in canonical form The events and constraints identified by each sub-expression are: x: L(1000){1} [the "x" that is the left operand of =] x: L(1000){2} [the "x" that is the operand of ++] ++x: R(1000){3}, W(1000){4}, {3} < {4} =: W(1000){5}, {3}, {4}, {3} < {4}, [{3}, {4}] < {5} Even though there is still only one possible ordering, this time the same address appears in two separate W events without an intervening sequence point, and so the behavior is undefined. (4) int x; x += x * x; The canonical form is: x += $x * $x; The events and constraints identified by each sub-expression are: x: L(1000){1} [the "x" that is the left operand of =] x: L(1000){2} [the "x" that is the left operand of *] x: L(1000){3} [the "x" that is the right operand of *] $x: R(1000){4} [derived from {2}] $x: R(1000){5} [derived from {3}] *: {4}, {5} +=: R(1000){6}, W(1000){7}, {4}, {5}, [{4}, {5}, {6}] < {7} The address 1000 appears in all four of the remaining events, and this time there are six permitted orderings but none of the 6 involve undefined behavior, and so the expression is valid. If x had volatile- qualified type it would be unspecified which of the three reads would be used for each of the three operands of the (implied) x + x * x. (5) int x; extern int f(int); x = f(x++); The canonical form is: x = (@f)(x++) The events and constraints identified by each sub-expression are: x: L(1000){1} [the "x" that is the left operand of =] x: L(1000){2} [the "x" that is operand of ++] x++: R(1000){3}, W(1000){4}, {3} < {4} f: none @f: none call: {3}, {4}, F(f){5}, {3} < {4}, [{3}, {4}] < {5} =: W(1000){6}, {3}, {4}, {5}, {3} < {4}, [{3}, {4}] < {5}, [{3}, {4}, {5}] < {6} The four events have one possible ordering: R(1000) : W(1000) : F(f) : W(1000) It is therefore clear that x is incremented before the function call starts execution, that the result of the function is stored in x, and that the expression is valid. If the function has some other form of access to x, it will see the incremented value, and any value it stores in x will be lost. If the expression is replaced by: x = 2 * f(x++); the analysis is effectively the same - the multiplication by a constant adds no new events. And if it is replaced by: x = 0 * f(x++); the analysis continues to remain the same; an optimising implemenation can determine that x is set to 0, but it must still make the incremented value of x available to the function. (6) int x, y; (x=y) + x; The canonical form is: (x=$y)+$x The events and constraints identified by each sub-expression are: x: L(1000){1} [the "x" that is the left operand of =] y: L(1234){2} x: L(1000){3} [the "x" that is the right operand of +] $y: R(1234){4} =: W(1000){5}, {4}, {4} < {5} $x: R(1000){6} +: {4}, {5}, {6}, {4} < {5} There are three possible orderings: {4} : {5} : {6} R(1234) : W(1000) : R(1000) {4} : {6} : {5} R(1234) : R(1000) : W(1000) {6} : {4} : {5} R(1000) : R(1234) : W(1000) The first of the three involves reading address 1000 after writing it - without an intervening sequence point - and so the expression is undefined. (7) int x, y, z; (x=y) + (x=z); The canonical form is: (x=$y)+(x=$z) The events and constraints identified by each sub-expression are: x: L(1000){1} [the "x" that is set to "y"] y: L(1234){2} x: L(1000){3} [the "x" that is set to "z"] z: L(1666){4} $y: R(1234){5} x=$y: W(1000){6}, {5}, {5} < {6} $z: R(1666){7} x=$z: W(1000){8}, {7}, {7} < {8} +: {5}, {6}, {7}, {8} There are six possible orderings, but all involve both {6} and {8} not separated by a sequence point, and so the expression is undefined. (8) To demonstrate the rules for arrays: double x [5]; int y = 3; x[y] /= (double) &x[y]; The canonical form is: *(@x+$y) /= (double)(@x+$y); The events and constraints identified by each sub-expression are: x: L(1000,15){1} [the "x" to the left of the =] y: L(1666){2} [the "y" to the left of the =] x: L(1000,15){3} [the "x" to the right of the =] y: L(1666){4} [the "y" to the right of the =] @x: D{5} [derived from {1}] $y: R(1666){6} [derived from {2}] +: {5}, {6} x[y]: {5}, {6}, L(1009,3){7}, [{5}, {6}] < {7} @x: D{8} [derived from {3}] $y: R(1666){9} [derived from {4}] +: {8}, {9} double: none cast: {8}, {9} /=: {5}, {6}, R(1009,3){10}, W(1009,3){11}, {5} < {10}, {5} < {11}, {6} < {10}, {6} < {11}, {8}, {9}, [{8}, {9}, {10}] < {11} The only purpose of D events is to preserve ordering in cases like [{22} < D, D < {23}] and so {5} and {8} can be ignored. This leaves the events: R(1666){6}, R(1666){9}, R(1009,3){10}, W(1009,3){11} and the constraints: {6} < {10}, {6} < {11}, {9} < {11}, {10} < {11} This permits three orderings: R(1666){6} : R(1009,3) : R(1666){9} : W(1009,3) R(1666){6} : R(1666){9} : R(1009,3) : W(1009,3) R(1666){9} : R(1666){6} : R(1009,3) : W(1009,3) None of these involve undefined behavior. (9) To demonstrate the rules for structures: int x; struct s { double p; int q; double r; } y; x = y.q; The canonical form is: x = $(y.q) The events and constraints identified by each sub-expression are: x: L(1000){1} y: L(1230,7){2} y.q: L(1233,1){3} $(y.q): R(1233){4} =: L(1233,1){5}, {4}, {4} < {5} (10) struct s { double p; int q; int r; } *x, y; x = &y; x->q = x->r; The canonical form is: (*$x).q = $((*$x).r) The events and constraints identified by each sub-expression are: x: L(1000){1} [part of the left operand of the =] x: L(1000){2} [part of the right operand of the =] $x: R(1000){3} [derived from {1}] *$x: {3}, L(1220,5){4}, {3} < {4} x->q: {3}, L(1223,1){5}, {3} < {5} $x: R(1000){6} [derived from {2}] *$x: {6}, L(1220,5){7}, {6} < {7} x->r: {6}, L(1224,1){8}, {6} < {8} $(x->r): {6}, R(1224,1){9}, {6} < {9} =: {3}, W(1223,1){10}, {3} < {10}, {6}, {9}, {6} < {9}, [{6}, {9}] < {10} These constraints allow three orderings: {3} : {6} : {9} : {10} {6} : {3} : {9} : {10} {6} : {9} : {3} : {10} and it is clear that all of these are valid. (11) int x; x++ && x--; This expression has two canonical forms, depending on whether x is or is not initially zero: x++ // x is initially 0 x++ , x-- // x is not initially 0 In this case it is clear that only the latter needs to be evaluated but this might not be the case in more complex expression. Doing so, the events and constraints identified by each sub-expression are: x: L(1000){1} [the "x" in x++] x: L(1000){2} [the "x" in x--] x++: R(1000){3}, W(1000){4}, {3} < {4} x--: R(1000){5}, W(1000){6}, {5} < {6} ,: {3}, {4}, {3} < {4}, {5}, {6}, {5} < {6}, S{7}, [{3}, {4}] < {7}, {7} < [{5}, {6}] There is only one possible ordering, and this has two W events to the same address, but these are separated by an S event and so the expression is valid. It is clear that the decrement must apply to the incremented variable. (12) int x, y; x++ * y++ ? x-- : y--; Again there are two canonical forms: x++ * y++ , x-- // x and y both initially nonzero x++ * y++ , y-- // either x or y initially zero In each case the analysis follows the lines above. The first case yields: R(1000){1}, W(1000){2}, R(1234){3}, W(1234){4}, S{5}, W(1000){6}, {1} < {2}, {1} < {5}, {2} < {5}, {3} < {4}, {3} < {5}, {4} < {5}, {5} < {6} There are six possible orderings, but all place a sequence point between the first and second writes to x. (13) int x[2], *y; y = x; *y = f(y++); The canonical form is: *$y = (@f)(y++) The events and constraints identified by each sub-expression are: y: L(1234){1} [the "y" on the left of the =] y: L(1234){2} [the "y" that is the operand of y++] y++: R(1234){3}, W(1234){4}, {3} < {4} f: none @f: none call: {3}, {4}, {3} < {4}, F(f){5}, [{3}, {4}] < {5} $y: R(1234){6} [derived from {1}] *$y: {6}, L(X){7}, {6} < {7} =: {6}, W(X){8}, {6} < {8}, {3}, {4}, {5}, {3} < {4}, [{3}, {4}] < {5}, [{3}, {5}] < {8} where X is the location pointed to by y at the point of the * operator. One possible ordering is: R(1234){3} : W(1234){4} : R(1234){6} : F(f){5} : W(X){8} and therefore the expression involves undefined behavior. (14) int x[2], y; y = 0; x[y] = f(y++); The canonical form is: *(@x+$y) = (@f)(y++) The events and constraints identified by each sub-expression are: x: L(1000,2){1} y: L(1234){2} [the "y" on the left of the =] y: L(1234){3} [the "y" that is the operand of y++] @x: D{4} $y: R(1234){5} [derived from {1}] +: {4}, {5} x[y]: {4}, {5}, L(X){6}, [{4}, {5}] < {6} where X is 1000 plus the value determined at {5} y++: R(1234){7}, W(1234){8}, {7} < {8} f: none @f: none call: {7}, {8}, {7} < {8}, F(f){9}, [{7}, {8}] < {9} =: {4}, {5}, W(X){10}, [{4}, {5}] < {10}, {7}, {8}, {9}, {7} < {8}, {8} < {9}, {7} < {9}, [{7}, {8}, {9}] < {10} One possible ordering is: D{4} : R(1234){7} : W(1234){8} : R(1234){5} : F(f){9} : W(X){10} and therefore the expression involves undefined behavior. (15) int x = 5; int a [x][x++]; There are two expressions to be considered, and their canonical forms are: $x x++ The first generates the event: R(1000){1} and the second the events and constraints: R(1000){2}, W(1000){3}, {2} < {3} There are no constraints between {1} and the other two events, and so they can occur in any of three orders. One of these arrangements puts W(1000) before R(1000) and so the declaration as a whole involves undefined behavior.