WG14/N908 A formal model of sequence points and related issues Working draft Clive Feather <clive@demon.net> Last changed 2000-03-10 Introduction This paper is the latest form of my proposals for a formal model of sequence points, previously known as Annex S and appearing in FCD1 (1998) as Annex D. In this paper the proposed text for the new Annex is interspersed with discussion and with examples. The exact situation at any point is indicated as follows: [[Normative]] The text following would be normative text (or a footnote) in Annex S within the amended Standard. [[Change]] The text following describes other changes required to the Standard to retain consistency. [[Discussion]] The text following discusses and explains the proposals, and would not appear in the Standard. [[Examples]] The text following contains examples which could be included or omitted as appears desirable. [[Discussion]] The Standard puts certain restrictions on expressions based on the concept of a "sequence point". For example: 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. The problem with wording like this is that, while it appears simple enough at first glance, it actually runs into a number of problems. For example: x = y++; The value of y is accessed not only to determine the value to be stored in y, but also to determine the value to be stored in x. Or: (x += 0) + (x *= 1); Neither assignment to x alters the stored value, and so it could be argued that they do not modify it. Finally: (0, x = 1, 1) + (2, x = 3, 3); It is not clear here where the "previous" and "next" sequence points are. There are other, related, issues involved in interpreting complicated expressions which are also addressed here. Annex S would be a normative Annex that provides a full interpretation of such expressions and would override any other related text. The Annex operates by providing a formal procedure for analysing an expression to determine its status. This procedure could, in principle, be carried out by an automaton, and for any expression produces one of three results: (1) The expression is well-formed and its result and side effects are well-defined. (2) The expression is well-formed, but there are several choices in the order of evaluation of subexpressions, and so it is unspecified which of these applies; thus the result and order of side-effects is also unspecified to this extent. (3) The expression involves undefined behaviour. [[Change]] Append the following to 6.5 paragraph 2, moving the reference to footnote 70 to the end of the appended text. This rule shall be interpreted according to Annex S. [[Normative]] Annex S (normative) Formal model of sequence points and related issues -------------------------------------------------- S.1 Introduction [#1] This annex defines a formal algorithm for determining whether any given expression or set of expressions meets various requirements of the Standard such as that in 6.5: 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. An implementation is not required to follow exactly the model defined in this annex. In particular, the model assumes serial evaluation, but parallel evaluation is equally valid. However, an implementation must ensure - for all expressions that are not determined by the model to involve undefined behaviour - that expressions are evaluated in a way that will yield one of the results (including side-effects) specified by this model. S.2 Basic concepts S.2.1 Events and rules The model is defined in terms of "events" and "rules", which are concepts used only for this purpose and have no other meaning in this International Standard. Each subexpression of the expressions being analysed has associated with it one or more events. An event consists of: * a type, which is one of D, F, L, R, S, or W; * in the case of types L, R, and W only, the address of a byte and, possibly, a designation of one or more bits within that byte; * in the case of type F only, a designator for a function. Two different events may have the same type, associated address, or both and remain separate events. An event may be associated with more than one subexpression, and in each such subexpression it may be either "central" or "incidental" (this is its "status" with respect to that subexpression). Where an expression is said to "inherit" the events of a subexpression then, unless stated explicitly to the contrary, all the events associated with the subexpression are also associated with the larger expression with the same status. Events are shown in this Annex in one of the following ways: {11:R 1234} an event of type R and address 1234, referred to elsewhere as "event 11"; {12:S} an event of type S, referred to elsewhere as "event 12"; {11} another use of the same "event 11"; {x:L 567 1-3} an event of type L referring only to bits 1-3 of address 567, referred to elsewhere as "event x". A rule is a requirement that one event "comes before" another. As such, the rules generated in analysing an expression put a partial ordering on the generated events. Given two events X and Y, the notation "X < Y" means "X comes before Y". The notation "X = Y" is also used and means that any rule that applies to X also applies to Y. Rules have the normal properties of a partial ordering. Rules have global effect in the model. That is, if a rule is introduced in the analysis of one subexpression, it applies to all other subexpressions that those two events are associated with and thus to the overall expression. [*] Thus, given events X, Y, and Z: X < X never happens; if X < Y is a rule, then Y < X never happens; if X < Y and Y < Z, then X < Z. But it is possible for neither X < Y nor Y < X to be a rule. Similarly: if X = Y, then Y = X and vice versa; if X < Y and Y = Z are rules, then X < Z; if X = Y and Y < Z are rules, then X < Z; X < Y and X = Y never happen together. [[Discussion]] Events are abstractions of the processes that make up the evaluation of an expression. Each event is assumed to be atomic, and a rule is a statement that one event must occur before a different one. The event types have the following meanings: D = a dummy event, existing only to preserve order relationships F x = a call to the function designated by x L x = designates the byte or bits at x with no action being taken R x = reading the value of the byte or bits at x S = a sequence point W x = writing a value to the byte or bits at x A W event does not mean that the value has to be stored immediately at the point in the model that the event occurs, but merely that it must be stored sometime before the next sequence point. The model automatically takes this into account; if the expression is not undefined, the value will not be required again before the next sequence point. Central events are those that represent the "value" of the expression, while incidental events are others that need to be tracked in the analysis. Every function call has a sequence point immediately before it (see 6.5.2.2) and another immediately after it (either because it ends with a full expression or because 7.1.4 requires one). Thus the effects of a function call on the enclosing expression depend only on which locations are read and written, and not on the order on which those reads and writes occur. For the purposes of the rest of the model, the events making up the function call form an atomic whole. [[Examples]] If each of the variables x, y, and z occupy only one byte, then the expression "x = y + z" involves 6 events and 5 rules: {1:L x} {2} = {4} {2:L y} {3} = {5} {3:L z} {1} = {6} {4:R y} {4} < {6} {5:R z} {5} < {6} {6:W x} The events associated with each subexpression are: central incidental x {1} none y {2} none $y {4} none z {3} none $y {5} none y + z {4} {5} none x = y + z {4} {5} {6} none (The notation $y is explained below.) In future examples, unless stated otherwise, all variables occupy one byte. [[Normative]] S2.2 Optimization A particular implementation may be able to optimize an expression so that one or more subexpressions need not be evaluated (such as "0 * (a + b)"). Nonetheless the implications of this model must be followed as if the expression were evaluated fully. [[Discussion]] This rule is my particular interpretation of the Standard, and WG14 may wish to take a different view of both this and other interpretations made elsewhere. There are further implications involved; for example, the expression "x = 0 * f(x)" is well-defined according to this Annex, using the old value of x for the function argument. The model would forbid compilers to produce code corresponding to the following rewrites unless the implementer can show that they cannot affect the result: (f (0), x = 0) (x = 0, f (x)) (x = 0, f (0)) (__temp = x, x = 0, f (__temp)) the first three because the wrong value is used for the parameter, and the last one (in fact, the last three) because f might have some other access to x (for example because it is a variable with file scope). [[Normative]] S.3 Process The model requires an expression or set of expressions to be analysed in three stages: * converting each expression to a "canonical form", as described in S.3.1; * determining the associated events and rules, as described in S.3.2; * evaluating the status of the expression, as described in S.3.3. S.3.1 Canonical form Each expression is first converted to a "canonical form". First: each expression of the form is replaced by the form e->field (*(e)).field e1[e2] *((e1)+(e2)) &*e e e1 && e2 ((e1) ? (e2) : 0) e1 || e2 ((e1) ? 1 : (e2)) sizeof e } one of { 1 sizeof type } (see below) { @(e) or @(type) (each of these being done recursively). A sizeof expression is replaced by an @ exprssion if the operand has variable length array type, and by the constant 1 otherwise. Next, wherever subclause 6.3.2.1 requires an lvalue not of array type to be converted to the value stored in the designated object, the lvalue expression e is replaced by the expression $(e), and where it requires an expression of array type to be converted to a pointer to the first element of the array, or an expression of function type to be converted to a pointer to the function, it is replaced by the expression @(e) ($ and @ are notional operators introduced for the purpose of the analysis). Finally, each expression of the form "e1 ? e2 : e3" is replaced by two separate analyses: ((e1) , (e2)) where e1 is non-zero ((e1) , (e3)) where e1 is zero (this also being done recursively). If the value of e1 is unspecified, the overall result of the analysis is the worst case of the individual options (e.g. if either is undefined, so is the whole expression). [[Discussion]] Converting the expression to canonical form does three things. Firstly, certain operators that can be written in the form of other operators are done so. Strictly speaking this is not necessary - the equivalent process could be applied to the methods of subclause S.3.2, but doing it this way makes it less likely that an inconsistency might be introduced. The two notional operators $ and @ provide an explicit hook for the conversions described in 6.3.2.1. Without them it would, in effect, be necessary to repeat their definitions everywhere an lvalue might occur. The sizeof operator usually involves no evaluation, and so a sizeof expression can simply be replaced by a constant. However, if the operand has variable length array type, it is evaluated. Since the result (of evaluating the operand, not of the sizeof operator) will be an lvalue designating an array, the notional operator @ is applied to it. The ? operator (and therefore the && and || operators) requires two completely different paths of analysis depending on the value of the first expression, because either the second argument or the third is evaluated, but not both. I have considered the possibility that (a ? b : c) could be analysed as if it were (a, b, c). However, I am not convinced that this would always yield the same results. [[Normative]] S.3.2 Determining the events S.3.2.1 Primary expressions A constant, string literal, or identifier with function type has no events associated with it. A parenthesised expression has the same events associated with it that the unparenthesised version does. An identifier with object (including array and incomplete) type has one event of type L for each byte it occupies; these are all central events. If the object has register storage class it still has a notional address, even if that address cannot be determined using the & or @ operators. S.3.2.2 Type names If a type name does not have variably modified type, it has no events associated with it. If it does have variably modified type, then it inherits the events from each full expression in array declarators within the type name. S.3.2.3 Compound Literals A compound literal inherits the events of the type name and of all the expressions in the initializer. It also has one new event of type L for each byte of the resulting object. For each inherited event {i} that was a central event, for each new event {c}, there is a rule {i} < {c}. The new events are central events of the compound literal; all inherited events become incidental events. [[Examples]] Take the compound literal "(int [2]){ x, y }" and assume: * x has central event {x1} and incidental event {x2}; * y has central events {y1} and {y2} but no incidental events; * the resulting object occupies addresses 1001 and 1002. The compound literal has central events: {c1:L 1001} {c2:L 1002} and incidental events: {x1} {x2} {y1} and {y2} and there are 6 rules introduced: {x1} < {c1} {x1} < {c2} {y1} < {c1} {y1} < {c2} {y2} < {c1} {y2} < {c2} [[Discussion]] A compound literal expression is an lvalue, and therefore its important events are L events that designate the resulting object. However, this object cannot be used until it is initialized, and so rules are required to enforce this. The events of the initializer expressions become incidental to the compound literal, because once the compound literal exists the initial values don't affect its behaviour in other expressions. [[Normative]] S.3.2.4 Nominal operators and address operators The expression "$e" inherits all central events that do not have type L, and all incidental events, of the subexpression e. For each central event of type L of the subexpression (say {i:L addr}) the expression has a new central event of type R and with the same address ({c:R addr}), and there is a rule {i} = {c}. The expression "@e" or "&e" inherits all central events that do not have type L, and all incidental events, of the subexpression e. For each central event of type L of the subexpression (say {i:L addr}) the expression has a new central event of type D ({c:D}) and there is a rule {i} = {c}. The expression "*e" inherits all the events of the subexpression e. In addition, if the resulting lvalue has object (including incomplete) type then the expression has a new central event of type L for each byte of the lvalue designated. For each inherited central event {i}, for each new event {c}, there is a rule {i} < {c}. [[Discussion]] The expression "$e" represents taking the value of an lvalue. As such, each byte of the lvalue needs to be read - represented by the new R events - and the result is no longer an lvalue - represented by omitting the existing L events from the expression. Any other events associated with the expression are simply carried up without change. The expression "@e" represents the conversion of an lvalue to an address. Again, the result is not an lvalue and so the L events must be dropped. Since no action takes place, they are replaced by D (dummy placeholder) events to ensure that any other rules constraining the order of events still take place in the right order. Similarly, the expression "&e" represents the conversion of an lvalue to an address and is handled in the same way. On the other hand, the expression "*e" represents the conversion of an address to an lvalue; it is not possible to use the lvalue until after the subexpression e has been evaluated. Because the value of e is, in general, variable, it is not normally possible to determine the address of the lvalue until the program is executed. In this case the analysis will have to consider all possibilities, and the final status of the expression may be (for example) "undefined if x is 7 and well-defined otherwise". It should be noted that both & and * operators might be eliminated during the conversion to canonical form; for example, "&*x" is equivalent to "x", while "&y[z]" is equivalent to "y+z". [[Normative]] S.3.2.5 Function calls The function call operator inherits all the events of the subexpressions, both that designating the function and those providing the arguments. There is one new event {f:F function}, using the function actually called. For each central event {i} that is inherited, there is a rule {i} < {f}. The inherited events are all incidental events of the function call expression. S.3.2.6 Structures and unions In general, the events associated with an expression "e.field" are a subset of those associated with the subexpression e. All events not of type L are simply inherited. Events of type L are inherited if and only if they are for the bytes comprising the particular field of the structure or union. This rule is modified slightly in the case of bit-field members of a structure (but not of a union). The storage unit containing the member is held in one or more bytes of the structure, but in some bytes only some of the bits are used. For each such byte, any event of type L {i:L addr} for that byte is not inherited. Instead, a new event {n:L addr bits} is created, with the same status, type L, and address augmented by the bits used by that field, and there is a rule {i} = {n}. [[Examples]] Suppose that a given structure type is 8 bytes long, while field f is 3 bytes long starting at offset 4. Then, if the expression e has events {e0:L 2000} {e1:L 2001} {e2:L 2002} {e3:L 2003} {e4:L 2004} {e5:L 2005} {e6:L 2006} {e7:L 2007} designating an 8 byte structure starting at address 2000, then the expression "e.f" inherits only three of those events: {e4} {e5} and {e6}. Suppose further that field b is a bit-field occupying all of offset 1 and bits 0 to 3 of offset 2. Then the expression "e.b" inherits the event {e1} and has a new event {e2b:L 2002 0-3}, with the rule {e2} = {e2b}. [[Discussion]] A structure or union member consists of some of the bytes of the structure or union. Therefore the behaviour of an expression containing a dot operator is same as that of an expression containing the entire structure or union, except that only the relevant bytes are affected. In the case of structures, it is possible to simultaneously write to two or more members, including bit-fields. Therefore special rules are required to handle bit-fields. In the case of unions this is not possible, and so these rules are not needed. [[Normative]] S.3.2.7 Increment and decrement operators The expressions "++e", "e++", "--e", and "e--" are all handled identically. The expression inherits all central events that do not have type L, and all incidental events, of the subexpression e. For each central event of type L of the subexpression (say {i:L addr}) the expression has two new central events {r:R addr} and {w:W addr}, both with the same address, but of types R and W respectively. There are rules: {i} = {r} {r} < {w} [[Discussion]] These rules are equivalent to those for the expression e += 1. It might be a better approach to do this during the creation of the canonical form. [[Normative]] S.3.2.8 Arithmetic operators The following operators simply inherit the events of their operand(s): unary: + - ! ~ binary: + - * / % << >> < > <= >= == != & ^ | [[Discussion]] These operators do not use or create lvalues, and in the case of the binary operators they do not impose any order of evaluation on their operands. [[Normative]] S.3.2.9 Cast operators The cast operator inherits the events of its operand and of the type name. [[Discussion]] The operator does not create or use an lvalue. While the the type name has to be evaluated before the cast is completed, it does not have to be evaluated before or after the value of the operand has been determined. So there is no ordering imposed between the two. [[Normative]] S.3.2.10 Comma operator The comma operator inherits the events of its operands and has a new central event {s:S} of type S. For each event {il} inherited from the left operand there is a rule: {il} < {s} For each event {ir} inherited from the right operand there is a rule: {s} < {ir} [[Discussion]] The new event represents the sequence point. [[Normative]] S.3.2.11 Assignment operators An assignment expression inherits all the events of the two operands except for central events of the left operand that have type L. The inherited events become incidental events. For each central event of the left operand of type L (say {i:L addr}), the following happens: * for a simple assignment operator, there is a new central event of type W and the same address ({w:W addr}), plus a rule {i} < {w}; * for a compound assignment operator, there is a new central event of type W and a new incidental event of type R, both with the same address ({w:W addr} and {r:R addr}), plus rules {i} < {r} and {r} < {w}. The new type W events are the only central events of the expression. For each event {e} inherited from the right operand, for each new type W event {w} introduced in the previous paragraph, there is a rule {e} < {w}. [[Discussion]] The central events of the left operand that have type L designate the bytes that will be assigned to. Therefore we need to generate a type W event for each such byte. This analysis makes one major assumption: that an assignment cannot happen until the address to be written to and the value to be written have both been determined. The value of the assignment is the value written, and therefore the corresponding W events are the only central events of the resulting expression; any other event involved in either operand is retained, but it will not affect what happens when the result is used. The analysis for "x += y" is the same as that for "x = x + (y)", except that the events inherited from x are only done so once, not twice. [[Normative]] S.3.3 Evaluating the status Once the events and rules associated with the overall expression have been determined, the status of the expression is evaluated in the following way. (In the following, the concept of "same address" takes account of the designation of specific bits: if two events have the same address, both have bits designated, but they have no bits in common, it is as if they had different addresses.) First, all events not associated with the overall expression are changed to type D. Next, every possible ordering of the events, other than those of type D, is examined in turn. If the ordering is inconsistent with any rule (including any rule involving type D events), it is discarded. Those orderings that are consistent with all rules are called the "permitted orderings". If any permitted ordering contains an event of type W followed by an event of either type R or type W for the same address and the events are not separated by an event of either type F or type S, then the expression involves undefined behaviour. Otherwise: * If there are two or more events of type W for a given address and two permitted orderings have different ones last, the value stored in the object at that address is unspecified; it may be any of the values written by the subexpressions first generating those events. * If there is an event of type R and one of type W for a given address, and two permitted orderings arrange them different ways round, the value used by the subexpression that first generates the event of type R is unspecified; it may be either the value written by the subexpression first generating the event of type W, or it may be the previous value of the object. * The above two cases also apply if either or both of the events are replaced by (distinct) events of type F where the function designated reads or writes the appropriate object. Otherwise the expression is well-defined and always has the same value and produces the same side-effects. [[Discussion]] If there are two events of type W for the same address, the corresponding object is being written to twice by the expression. There are three cases: (1) It is possible to have the two events not separated by an event of type F or type S. In this case there is an ordering where there are two writes to the same object without a sequence point intervening, so the behaviour is undefined. (2) There is always an intervening sequence point but the two events can occur in either order. In this case it is unspecified which order they occur in, and so which one provides the last write to the object. If one of the events is the last write to the object, then the final value of the object will be unspecified. (3) There is always an intervening sequence point and the order is always the same. In this case the expression is well-defined as far as these events are concerned. If there are two events, one of type R and one of type W, for the same address, the corresponding object is both read and written. In this case: (1) If the write can be followed by the read without an intervening event of type F or type S (a sequence point) the behaviour is undefined. (2) If this cannot happen but the events can nonetheless be in either order, the actual order is unspecified. (3) Otherwise either the object is always read first, or there is always a sequence point between the write and the subsequent read, but in either case the expression is well-defined as far as these events are concerned. [[Normative]] If an event of type R applies to a volatile object, the object is being read. If there is more than one such event for the same object, the value of the expression may depend on the order they occur. If the permitted orderings allow more than one arrangement for these events, the value of the expression is unspecified. [[Discussion]] There is an obvious mapping from R events to reads of a volatile object, and if the events can occur in more than one order it implies that the corresponding reads can also do so. I understand that this area was seen as contentious in previous drafts of this document, and have tried to say as little as possible. [[Examples]] EXAMPLE 1 int x, y; x = y++; // already in canonical form The analysis proceeds as follows: associated events new rules central incidental introduced x {1:L x} none y {2:L y} none y++ {3:R y} none {2} = {3} {4:W y} {3} < {4} x = y++ {5:W x} {3} {4} {1} < {5} {3} < {5} {4} < {5} The only permitted ordering is: {3} {4} {5} The only location referred to more than once is y, and the R event occurs before the W event. So the expression is well-defined. EXAMPLE 2 int x; x = ++x; // already in canonical form The analysis proceeds as follows: associated events new rules central incidental introduced x [LHS] {1:L x} none x [RHS] {2:L x} none ++x {3:R x} none {2} = {3} {4:W x} {3} < {4} = {5:W x} {3} {4} {1} < {5} {3} < {5} {4} < {5} The only permitted ordering is: {3} {4} {5} This contains events {4} and {5}, both of which are type W events for x, without an intervening sequence point. So the expression involves undefined behaviour. EXAMPLE 3 int x; x += x * x; The canonical form is: x += $x * $x; The analysis proceeds as follows: associated events new rules central incidental introduced x [LHS] {1:L x} none x [RHS 1] {2:L x} none $x [RHS 1] {3:R x} none {2} = {3} x [RHS 2] {4:L x} none $x [RHS 2] {5:R x} none {4} = {5} $x * $x {3} {5} += {6:R x} {3} {5} {1} < {6} {7:W x} {6} < {7} {3} < {7} {5} < {7} The permitted orderings are: {3} {5} {6} {7} {3} {6} {5} {7} {5} {3} {6} {7} {5} {6} {3} {7} {6} {3} {5} {7} {6} {5} {3} {7} Since {7} is the only W event and is always last, the expression is well-defined. EXAMPLE 4 int x; extern int f(int); x = f(x++); The canonical form is: x = (@f)(x++) The analysis proceeds as follows: associated events new rules central incidental introduced x [LHS] {1:L x} none f none none @f none none x [RHS] {2:L x} none x++ {3:R x} none {2} = {3} {4:W x} {3} < {4} (@f)(x++) {5:F f} {3} {4} {3} < {5} {4} < {5} = {6:W x} {3} {4} {5} {1} < {6} {3} < {6} {4} < {6} {5} < {6} The only permitted ordering is: {3:R x} {4:W x} {5:F f} {6:W x} The two writes to x are separated by an event of type F (the sequence point in a function call). The read occurs before the first write. Therefore the expression is well-defined. Note that it is clear that x is incremented before the function call starts execution and that the final value of x will be the result of the function. 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 overwritten. If the expression is replaced by: x = 2 * f(x++); the analysis is effectively the same - multiplication by a constant adds no new events or rules. And if it is replaced by: x = 0 * f(x++); the analysis continues to remain the same; an optimizing implementation can determine that x is set to 0, but it must still make the incremented value of x available to the function. EXAMPLE 5 int x, y; (x=y) + x; The canonical form is: (x=$y)+$x The analysis proceeds as follows: associated events new rules central incidental introduced x [LHS] {1:L x} none y {2:L y} none $y {3:R y} none {2} = {3} x = $y {4:W x} {3} {1} < {4} {3} < {4} x [RHS] {5:L x} none $x {6:R x} none {5} = {6} (x=$y)+$x {4} {6} {3} The permitted orderings are: {3} {4} {6} {3} {6} {4} {6} {3} {4} Since the first of these has {4:W x} immediately before {6:R x}, the expression is undefined. EXAMPLE 6 int x, y, z; (x=y) + (x=z); The canonical form is: (x=$y)+(x=$z) The analysis proceeds as follows: associated events new rules central incidental introduced x [LHS] {1:L x} none y {2:L y} none $y {3:R y} none {2} = {3} x = $y {4:W x} {3} {1} < {4} {3} < {4} x [RHS] {5:L x} none z {6:L y} none $z {7:R y} none {6} = {7} x = $z {8:W x} {7} {5} < {8} {7} < {8} (x=y)+(x=z) {4} {8} {3} {7} The permitted orderings are: {3} {4} {7} {8} {3} {7} {4} {8} {3} {7} {8} {4} {7} {3} {4} {8} {7} {3} {8} {4} {7} {8} {3} {4} Since the second of these has {4:W x} immediately before {8:W x}, the expression is undefined. (In fact, all six involve a forbidden arrangement of events.) EXAMPLE 7 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 analysis proceeds as follows ("e" is the array element identified by x[y]): associated events new rules central incidental introduced [LHS] x {1:L x} none @x {2:D} none {1} = {2} y {3:L y} none $y {4:R y} none {3} = {4} (@x+$y) {2} {4} none *(@x+$y) {5:L e} none {2} < {5} {2} {4} {4} < {5} [RHS] x {6:L x} none @x {7:D} none {6} = {7} y {8:L y} none $y {9:R y} none {8} = {9} (@x+$y) {7} {9} none (double) none none cast {7} {9} none /= {10:R e} {2} {4} {5} < {10} {11:W e} {7} {9} {10} < {11} {7} < {11} {9} < {11} The permitted orderings are: {4} {9} {10} {11} {4} {10} {9} {11} {9} {4} {10} {11} There are no type W events for x or y; the only object written to is e. The events involving e are {10} and {11}, and they are always in that order. Therefore the expression is well-defined. EXAMPLE 8 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 analysis proceeds as follows: associated events new rules central incidental introduced x {1:L x} none y {2:L y.p} none {3:L y.q} {4:L y.r} y.q {3} none $(y.q) {5:R y.q} none {3} = {5} x = $(y.q) {6:W x} {5} {1} < {6} {5} < {6} There is only one permitted ordering: {5} {6} EXAMPLE 9 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 analysis proceeds as follows: associated events new rules central incidental introduced x [LHS] {1:L x} none $x {2:R x} none {1} = {2} *$x {2} none {2} < {3} {3:L y.p} {2} < {4} {4:L y.q} {2} < {5} {5:L y.r} (*$x).q {4} none x [RHS] {6:L x} none $x {7:R x} none {6} = {7} *$x {7} none {7} < {8} {8:L y.p} {7} < {9} {9:L y.q} {7} < {10} {10:L y.r} (*$x).r {10} none $((*$x).r) {11:W y.r} none {10} = {11} = {12:W y.q} {11} {4} < {12} {11} < {12} There is only one permitted ordering: {11} {12} EXAMPLE 10 To illustrate the rules for bit-fields: struct { int x : 10; int y : 3; } s; s.y = 4; s.x = s.y++; This is already in canonical form. The analysis proceeds as follows (assuming that s occupies two bytes called s.1 and s.2 in this description and that bits are allocated to bit-fields in numerical order): associated events new rules central incidental introduced s [LHS] {1:L s.1} none {2:L s.2} s.x {1} none {2} = {3} {3:L s.2 0-1} s [RHS] {4:L s.1} none {5:L s.2} s.y {6:L s.2 2-4} none {5} = {6} s.y++ {7:R s.2 2-4} none {6} = {7} {8:W s.2 2-4} {7} < {8} s.x = s.y {9:W s.1} {7} {8} {1} < {9} {10:W s.2 0-1} {2} < {10} {7} < {9} {8} < {9} {7} < {10} {8} < {10} The permitted orderings are: {7} {8} {9} {10} {7} {8} {10} {9} Since the three W events all identify different locations in memory (even if two of them are parts of the same storage unit) the expression is well-defined. However, if the type of s was a union instead of a structure, there would be no designation of bit-fields in the events. Events {8} and {9} would both be type W for address s.2, and the behaviour is undefined. EXAMPLE 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 example it is clear that only the latter needs to be analysed in detail, but this might not be the case in more complex expressions. Doing the analysis: associated events new rules central incidental introduced x [LHS] {1:L x} none x++ {2:R x} none {1} = {2} {3:W x} {2} < {3} x [RHS] {4:L x} none x-- {5:R x} none {4} = {5} {6:W x} {5} < {6} x++, x-- {2} {3} {5} none {2} < {7} {6} {7:S} {3} < {7} {7} < {5} {7} < {6} The only permitted ordering is: {2} {3} {7} {5} {6} The W event {3} is immediately followed by a type S event, so the expression is well-defined. It is clear that the decrement must apply to the incremented variable. EXAMPLE 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 of the previous example, and there is always a type S event between the writes on the left hand side and the reads and writes on the right hand side. EXAMPLE 13 int x[2], *y; y = x; *y = f(y++); The canonical form is: *$y = (@f)(y++) The analysis proceeds as follows: associated events new rules central incidental introduced y [LHS] {1:L y} none $y {2:R y} none {1} = {2} *$y {2} {3:L e} none {2} < {3} f none none @f none none y [RHS] {4:L y} none y++ {5:R y} none {4} = {5} {6:W y} {5} < {6} (@f)(y++) {7:F} {5} {6} {5} < {7} {6} < {7} = {8:W e} {2} {5} {6} {7} {3} < {8} {5} < {8} {6} < {8} {7} < {8} (where e is the location pointed to by y at the moment of the * operation). The permitted orderings are: {2} {5} {6} {7} {8} {5} {2} {6} {7} {8} {5} {6} {2} {7} {8} {5} {6} {7} {2} {8} The third of these involves a read of y (event {2}) immediately after a write (event {6}), and so the behaviour is undefined. [[Normative]] S.4 Application S.4.1 Expressions For each expression statement, and for each full expression in a selection, iteration, or jump statement, the expression is 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 outside a compound literal, the events of all the individual expressions are inherited together with no additional rules. [[Example]] Consider the declaration: int a [x][x++]; There are two expressions, whose canonical forms are: $x x++ The analysis of the first proceeds as follows: associated events new rules central incidental introduced x {1:L x} none $x {2:R x} none {1} = {2} and the second as follows: associated events new rules central incidental introduced x {3:L x} none x++ {4:R x} none {3} = {4} {5:W x} {4} < {5} The overall set of events is therefore {2}, {4}, and {5}, and the permitted orderings are: {2} {4} {5} {4} {2} {5} {4} {5} {2} The last one has a W event for x followed by an R event, so this declaration involves undefined behaviour. [[Normative]] S.4.2 Signals If program execution is interrupted by a signal where the handler returns to the caller, the behavior is 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.3 Floating-point environment There are four additional event types for addressing the floating-point environment: RF, WF, RV, and WV. These represent reads of and changes to the floating-point exception flags (F) and to the remainder of the floating point environment (V) respectively. Any function in <fenv.h> that reads or alters these flags generates events of the appropriate types. Wherever an event {v:WV} is generated, an incidental event {f:WF} is also generated, with the rule: {v} = {f}. If the state of the FENV_ACCESS pragma is on, then any operation that sets a floating-point exception flag causes an event {f:WF} to be created. The events associated with the subexpression based on the operator causing the flag to be set are listed, and for every event {e} other than a central event of type W, the rule {e} < {f} is added. [[Example]] In the expression: x + y * z suppose that the multiplication sets a floating-point exception flag. The expression is analysed in the following way. The canonical form is: $x + $y * $z The analysis proceeds as follows: associated events new rules central incidental introduced x {1:L x} none $x {2:R x} none {1} = {2} y {3:L y} none $y {4:R y} none {3} = {4} z {5:L z} none $z {6:R z} none {5} = {6} y * z {4} {6} none {4} < {7} {7:WF} {6} < {7} x + y * z {2} {4} {6} none [[Normative]] The principles of S.3.3 are applied to RV and WV events as though they were R and W events for a specific address, and to RF and WF events as though they were R and W events for another address. However, if a permitted ordering contains two or more WF events without an intervening event of type S or F, the expression does not involve undefined behaviour for this reason. Instead, it is unspecified which combination of flags will actually be set by the expression, so long as at least one of them is.[*] [*] 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. [[Commentary]] Nick Maclaren was kind enough to suggest semantics for floating-point in an earlier version of this document. The present semantics are my attempt to adapt his work to the present notation, and could no doubt be improved greatly.