Separation Logic for Non-local Control Flow and Block Scope Variables

Robbert Krebbers and Freek Wiedijk

ICIS, Radboud University Nijmegen, The Netherlands

Abstract. We present an approach for handling non-local control flow (goto and return statements) in the presence of allocation and deallocation of block scope variables in imperative programming languages. We define a small step operational semantics and an axiomatic semantics (in the form of a separation logic) for a small C-like language that combines these two features, and which also supports pointers to block scope variables. Our operational semantics represents the program state through a generalization of Huet’s zipper data structure. We prove soundness of our axiomatic semantics with respect to our operational semantics. This proof has been fully formalized in Coq.

1 Introduction

There is a gap between programming language features that can be described well by a formal semantics, and those that are available in widely used programming languages. This gap needs to be bridged in order for formal methods to become mainstream. However, interaction between the more ‘dirty’ features of widely used programming languages tends to make an accurate formal semantics even more difficult. An example of such interaction is the goto statement in the presence of block scope variables in the C programming language.

C allows unrestricted gotos which (unlike break and continue) may not only jump out of blocks, but can also jump into blocks. Orthogonal to this, blocks may contain local variables, which can be “taken out of their block” by keeping a pointer to them. This makes non-local control in C (including break and continue) even more unrestricted, as leaving a block results in the memory of these variables being freed, and thus making pointers to them invalid. Consider:

   int *p = NULL;
   l: if (p) { return (*p); }
      else { int j = 10; p = &j; goto l; }

Here, when the label l is passed for the first time, the variable p is NULL. Hence, execution continues in the block containing j where p is assigned a pointer to j. However, after the goto l statement, the block containing j is left, and the memory of j is freed. After this, dereferencing p is no longer legal, making the program exhibit undefined behavior.

If a program exhibits undefined behavior, the ISO C standard [8] allows it to do literally anything. This is to avoid compilers having to insert (possibly expensive) dynamic checks to handle corner cases. In particular, in the case of non-local control flow this means that an implementation can ignore allocation issues when jumping, but a semantics cannot. Not describing certain undefined behaviors would therefore mean that some programs can be proven correct with respect to the formal semantic whereas they may crash or behave unexpectedly when compiled with an actual C compiler.

It is well known that a small step semantics is more flexible than a big step semantics for modeling more intricate programming language features. In a small step semantics, it is nonetheless intuitive to treat uses of goto as big steps, as executing them makes the program jump to a totally different place in one step. For functional languages, there has been a lot of research on modeling control (call/cc and variants thereof) in a purely small step manner (see [6] for example). This indicates that the intuition that uses of non-local control should be treated as big steps is not correct.

We show that a purely small step semantics is also better suited to handle the interaction between gotos and block scope variables in imperative programming languages. Our semantics lets the goto statement traverse in small steps through the program to search for its corresponding label. The required allocations and deallocations are calculated incrementally during this traversal.

Our choice of considering goto at all may seem surprising. Since the revolution of structured programming in the seventies, many people have considered goto as bad programming practice [4]. However, some have disagreed [9], and gotos are still widely used in practice. For example, the current Linux kernel contains about a hundred thousand uses of goto. Goto statements are particularly useful for breaking from multiple nested loops, and for systematically cleaning up resources after an error occurred. Also, gotos can be used to increase performance.

Approach. We define a small step operational semantics for a small C-like language that supports both non-local control flow and block scope variables. To obtain more confidence in this semantics, and to support reasoning about programs in this language, we define an axiomatic semantics for the same fragment, and prove its soundness with respect to the operational semantics.

Our operational semantics uses a zipper-like data structure [7] to store both the location of the substatement that is being executed and the program stack. Because we allow pointers to local variables, the stack contains references to the value of each variable instead of the value itself. Execution of the program occurs by traversal through the zipper in one of the following directions: down ↘, up ↗, jump ↷, or top ↑↑. When a goto l statement is executed, the direction is changed to ↷l, and the semantics performs a small step traversal through the zipper until the label l has been reached.

Related work. Goto statements (and other forms of non-local control) are often modeled using continuations. Appel and Blazy provide a small step continuation semantics for Cminor [2] that supports return statements. CompCert extends their approach to support goto statements in Cmedium [12]. Ellison and Rosu [5] also use continuations to model gotos in their C11 semantics, but whereas the CompCert semantics does not support block scope variables, they do. We further discuss the differences between continuations and our approach in Section 3.

Tews [18] defines a denotational semantics for a C-like language that supports goto and unstructured switch statements. His state includes variants for nonlocal control corresponding to our directions ↷and ↑↑.

The most closely related work to our axiomatic semantics is Appel and Blazy’s separation logic for Cminor in Coq [2]. Their separation logic supports return statements, but does not support gotos, nor block scope variables. Von Oheimb [15] defines an operational and axiomatic semantics for a Java-like language in Isabelle. His language supports both local variables and mutually recursive function calls. Although his work is fairly different from ours, our approach to mutual recursion is heavily inspired by his. Furthermore, Chlipala [3] gives a separation logic for a low-level language in Coq that supports gotos. His approach to automation is impressive, but he does not give an explicit operational semantics and does not consider block scope variables.

Contribution. Our contribution is threefold:

– We define a small step operational semantics using a novel zipper based data structure to handle the interaction between gotos and block scope variables in a correct way (Section 2 and 3).

– We give an axiomatic semantics that allows reasoning about programs with gotos, pointers to local variables, and mutually recursive function calls. We demonstrate it by verifying Euclid’s algorithm (Section 4).

– We prove the soundness of our axiomatic semantics (Section 5). This proof has been fully formalized in the Coq proof assistant (Section 6).

2 The language

Our memory is a finite partial function from natural numbers to values, where a value is either an unbounded integer, a pointer represented by a natural number corresponding to the index of a memory cell, or the NULL-pointer.

Definition 2.1. A partial function from A to B is a (total) function from A to B^{opt}, where A^{opt} is the option type, defined as containing either ⊥ or x for some x ∈ A. A partial function is called finite if its domain is finite. The operation f[x := y] stores the value y at index x, and f[x := ⊥] deletes the value at index x. Disjointness, notation f_{1} ⊥ f_{2}, is defined as ∀x . f_{1} x = ⊥ ∨ f_{2} x = ⊥. Given f_{1} and f_{2} with f_{1} ⊥ f_{2}, the operation f_{1} ∪ f_{2} yields their union. Moreover, the inclusion f_{1} ⊆ f_{2} is defined as ∀x y . f_{1} x = y → f_{2} x = y.

Definition 2.2. Values are defined as:

                       v ::= int n | ptr b | NULL

Memories (typically named m) are finite partial functions from natural numbers to values. A value v is true, notation istrue v, if it is of the shape int n with n ≠ 0, or ptr b. It is false, notation isfalse v, otherwise.

Expressions are side-effect free and will be given a deterministic semantics by an evaluation function. The variables used in expressions are De Bruijn indexes, i.e. the variable x_{i} refers to the ith value on the stack. De Bruijn indexes avoid us from having to deal with shadowing due to block scope variables. Especially in the axiomatic semantics this is useful, as we do not want to lose information by a local variable shadowing an already existing one.

Definition 2.3. Expressions are defined as:

⊚ ::= == | ≤ | + | ∗ | / | %
e ::= x_{i} | v | load e | e_{1} ⊚ e_{2}

Stacks (typically named ρ) are lists of memory indexes rather than lists of values. This allows us to treat pointers to both local and allocated storage in a uniform way. Evaluation of a variable thus consists of looking up its address in the stack, and returning a pointer to that address.

Definition 2.4. Evaluation [[ e]]_{ρ,m} of an expression e in a stack ρ and memory m is defined by the following partial function:

[[ x_{i}]]_{ρ,m} := ptr a  if ρ i = a
[[ v]]_{ρ,m} := v
[[ load e]]_{ρ,m} := m a  if [[ e]]_{ρ,m} = ptr a
[[ e_{1} ⊚ e_{2} ]]_{ρ,m} := [[ e_{1} ]]_{ρ,m}⊚[[ e_{2} ]]_{ρ,m}

Lemma 2.5. If m_{1} ⊆ m_{2} and [[ e]]_{ρ,m_{1}} = v, then [[ e]]_{ρ,m_{2}} = v.

Definition 2.6. Statements are defined as:

s ::= block s | e_{l} := e_{r} | f(e⃗) | skip | goto l
| l: s | s_{1} ; s_{2} | if (e) s_{1} else s_{2} | return

The construct block s opens a new scope with one variable. Since we use De Bruijn indexes for variables, it does not contain the name of the variable. For presentation’s sake, we have omitted functions that return values (these are however included in our Coq formalization). In the semantics presented here, an additional function parameter with a pointer for the return value can be used instead. Given a statement s, the function labels s collects the labels of labeled statements in s, and the function gotos s collects the labels of gotos in s.

3 Operational semantics

We define the semantics of statements by a small step operational semantics. That means, computation is defined by the reflexive transitive closure of a reduction relation ⇾ on program states. This reduction relation traverses through the program in small steps by moving the focus on the substatement that is being executed. Uses of non-local control (goto and return) are performed in small steps rather than in big steps as well.

In order to model the concept of focusing on the substatement that is being executed, we need a data structure to capture the location in the program. For this we define program contexts as an extension of Huet’s zipper data structure [7]. Program contexts extend the zipper data structure by annotating each block scope variable with its associated memory index, and furthermore contain the full call stack of the program. Program contexts can also be seen as a generalization of continuations (as for example being used in CompCert [2,11,12]). However, there are some notable differences.

– Program contexts implicitly contain the stack, whereas a continuation semantics typically stores the stack separately.

– Program contexts also contain the part of the program that has been executed, whereas continuations only contain the part that remains to be done.

– Since the complete program is preserved, looping constructs like the while statement do not have to duplicate code (see the Coq formalization).

The fact that program contexts do not throw away the parts of the statement that have been executed is essential for our treatment of goto. Upon an invocation of a goto, the semantics traverses through the program context until the corresponding label has been found. During this traversal it passes all block scope variables that went out of scope, allowing it to perform required allocations and deallocations in a natural way. Hence, the point of this traversal is not so much to search for the label, but much more to incrementally calculate the required allocations and deallocations.

In a continuation semantics, upon the use of a goto, one typically computes, or looks up, the statement and continuation corresponding to the target label. However, it is not very natural to reconstruct the required allocations and deallocations from the current and target continuations.

Definition 3.1. Singular statement contexts are defined as:

E_{S} ::= □; s_{2} | s_{1} ; □ | if (e) □ else s_{2} | if (e) s_{1} else □ | l: □

Given a singular statement context E_{S} and a statement s, substitution of s for the hole in E_{S}, notation E_{S}[ s], is defined in the ordinary way.

A pair (E⃗_{S}, s) consisting of a list of singular statement contexts E⃗_{S} and a statement s forms a zipper for statements without block scope variables. That means, E⃗_{S} is a statement turned inside-out that represents a path from the focused substatement s to the top of the whole statement.

Definition 3.2. Singular program contexts are defined as:

E ::= E_{S} | block_{b} □ | call f e⃗ | params b⃗

Program contexts (typically named k) are lists of singular program contexts.

The previously introduced contexts will be used as follows.

– When entering a block, block s, the context block_{b} □ is appended to the head of the program context. It associates the block scope variable with its corresponding memory index b.

– Upon a function call, f(e⃗), the context call f e⃗ is appended to the head of the program context. It contains the location of the caller so that it can be restored when the called function f returns.

– When a function body is entered, the context params b⃗ is appended to the head of the program context. It contains a list of memory indexes of the function parameters.

As program contexts implicitly contain the stack, we define a function to extract it from them.

Definition 3.3. The corresponding stack getstack k of k is defined as:

getstack (E_{S} :: k) := getstack k
getstack (block_{b} □ :: k) := b :: getstack k
getstack (call f e⃗ :: k) := [ ]
getstack (params b⃗ :: k) := b⃗ ++ getstack k

We will treat getstack as an implicit coercion and will omit it everywhere.

We define getstack (call f e⃗ :: k) as [ ] instead of getstack k, as otherwise it would be possible to refer to the local variables of the calling function.

Definition 3.4. Directions, focuses and program states are defined as:

d ::= ↘| ↗| ↷l | ↑↑
ϕ ::= (d, s) | \overline{call} f v⃗ | \overline{return}
S ::= S(k, ϕ, m)

A program state S(k, ϕ, m) consists of a program context k, the part of the program that is focused ϕ, and the memory m. Like Leroy’s semantics for Cminor [11], we consider three kinds of states: (a) execution of statements (b) calling a function (c) returning from a function. The CompCert Cmedium semantics [12] also includes a state for execution of expressions and a stuck state for undefined behavior. Since our expressions are side-effect free, we do not need an additional expression state. Furthermore, since expressions are deterministic, we can easily capture undefined behavior by letting the reduction get stuck.

Definition 3.5. The relation allocparams m_{1} b⃗ v⃗ m_{2} (non-deterministically) allocates fresh blocks b⃗ for function parameters v⃗. It is inductively defined as:

   allocparams m [ ] [ ] m

                             allocparams m_{1} b⃗ v⃗ m_{2}  m_{2} b = ⊥

allocparams m_{1} (b :: b⃗) (v :: v⃗) m_{2}[b := v]

Definition 3.6. Given a function δ assigning statements to function names, the small step reduction relation S_{1} ⇾ S_{2} is defined as:

1. For simple statements:

(a) S(k, (↘, e_{1} := e_{2}), m) ⇾ S(k, (↗, e_{1} := e_{2}), m[a := v])

for any a and v such that [[ e_{1} ]]_{k,m} = ptr a, [[ e_{2} ]]_{k,m} = v and m a ≠ ⊥.

(b) S(k, (↘, f(e⃗)), m) ⇾ S(call f e⃗ :: k, \overline{call} f v⃗, m)

for any v⃗ such that [[ e_{i}]]_{k,m} = v_{i} for each i.

(c) S(k, (↘, skip), m) ⇾ S(k, (↗, skip), m)

(d) S(k, (↘, goto l), m) ⇾ S(k, (↷l, goto l), m)

(e) S(k, (↘, return), m) ⇾ S(k, (↑↑, return), m)

2. For compound statements:

(a) S(k, (↘, block s), m) ⇾ S((block_{b} □) :: k, (↘, s), m[b := v]) for any b and v such that m b = ⊥.

(b) S(k, (↘, s_{1} ; s_{2}), m) ⇾ S((□; s_{2}) :: k, (↘, s_{1}), m)

(c) S(k, (↘, if (e) s_{1} else s_{2}), m) ⇾ S((if (e) □ else s_{2}) :: k, (↘, s_{1}), m) for any v such that [[ e]]_{k,m} = v and istrue v.

(d) S(k, (↘, if (e) s_{1} else s_{2}), m) ⇾ S((if (e) s_{1} else □) :: k, (↘, s_{2}), m) for any v such that [[ e]]_{k,m} = v and isfalse v.

(e) S(k, (↘, l: s), m) ⇾ S((l: □) :: k, (↘, s), m)

(f) S((block_{b} □) :: k, (↗, s), m) ⇾ S(k, (↗, block s), m[b := ⊥])

(g) S((□; s_{2}) :: k, (↗, s_{1}), m) ⇾ S((s_{1} ; □) :: k, (↘, s_{2}), m)

(h) S((s_{1} ; □) :: k, (↗, s_{2}), m) ⇾ S(k, (↗, s_{1} ; s_{2}), m)

(i) S((if (e) □ else s_{2}) :: k, (↗, s_{1}), m) ⇾ S(k, (↗, if (e) s_{1} else s_{2}), m)

(j) S((if (e) s_{1} else □) :: k, (↗, s_{2}), m) ⇾ S(k, (↗, if (e) s_{1} else s_{2}), m)

(k) S((l: □) :: k, (↗, s), m) ⇾ S(k, (↗, l: s), m)

3. For function calls:

(a) S(k, \overline{call} f v⃗, m_{1}) ⇾ S(params b⃗ :: k, (↘, s), m_{2})

for any s, b⃗ and m_{2} such that δ f = s and allocparams m_{1} b⃗ v⃗ m_{2}.

(b) S(params b⃗ :: k, (↗, s), m) ⇾ S(k, \overline{return}, m[b⃗ := ⊥])

(c) S(params b⃗ :: k, (↑↑, s), m) ⇾ S(k, \overline{return}, m[b⃗ := ⊥])

(d) S(call f e⃗ :: k, \overline{return}, m) ⇾ S(k, (↗, f(e⃗)), m)

4. For non-local control flow:

(a) S((block_{b} □) :: k, (↑↑, s), m) ⇾ S(k, (↑↑, block s), m[b := ⊥])

(b) S(E_{S} :: k, (↑↑, s), m) ⇾ S(k, (↑↑, E_{S}[ s]), m)

(c) S(k, (↷l, block s), m) ⇾ S((block_{b} □) :: k, (↷l, s), m[b := v]) for any b and v such that m b = ⊥, and provided that l ∈ labels s.

(d) S(k, (↷l, l: s), m) ⇾ S((l: □) :: k, (↘, s), m)

(e) S(k, (↷l, E_{S}[ s]), m) ⇾ S(E_{S} :: k, (↷l, s), m) provided that l ∈ labels s.

(f) S(block_{b} □ :: k, (↷l, s), m) ⇾ S(k, (↷l, block s), m[b := ⊥]) provided that l ∉ labels s.

(g) S(E_{S} :: k, (↷l, s), m) ⇾ S(k, (↷l, E_{S}[ s]), m) provided that l ∉ labels s.

Note that the rules 4d and 4e overlap, and that the splitting into E_{S} and s in rule 4e is non-deterministic. We let ⇾^{∗} denote the reflexive-transitive closure, and ⇾^{n} paths of ≤ n steps.

Execution of a statement S(k, (d, s), m) is performed by traversing through the program context k and statement s in direction d. The direction down ↘ (respectively up ↗) is used to traverse downwards (respectively upwards) to the next substatement to be executed. Consider the example from the introduction (with the return expression omitted).

   int *p = NULL;
   l: if (p) { return; }
      else { int j = 10; p = &j; goto l; }

Figure 1 below displays some states corresponding to execution of this program starting at p = &j in downwards direction.

Execution of a function call S(k, (↘, f(e⃗)), m) consists of two reductions. The reduction to S(call f e⃗ :: k, \overline{call} f v⃗, m) evaluates the function parameters e⃗ to values v⃗, and stores the location of the calling function on the program context. The subsequent reduction to S(params b⃗ :: call f e⃗ :: k, (↘, s), m′) looks up the called function’s body s, allocates storage for the parameters v⃗, and then performs a transition to execute the called function’s body.

We consider two directions for non-local control flow: jump ↷l and top ↑↑. After a goto l the direction ↷l is used to traverse to the substatement labeled l. Although this search is non-deterministic, there are some side conditions on it so as to ensure it not going back and forth between the same locations. This is required as it otherwise may impose non-terminating behavior on terminating programs. The non-determinism could be removed entirely by adding additional side conditions. However we omitted doing so in order to ease formalization.

The direction ↑↑ is used to traverse to the top of the statement after a return. When it reaches the top, there will be two reductions to leave the called function. The first reduction, from S(params b⃗ :: call f e⃗ :: k, (↑↑, s), m) to S(call f e⃗ :: k, \overline{return}, m[b⃗ := ⊥]), deallocates the function parameters, and the second, to S(k, (↗, f(e⃗)), m), reinstates the calling function.

k_{1} = □; goto l
:: x_{0} := int 10 ; □

      :: block_{bj} □
      :: if (load x_{0}) return
        else □

:: l: □
:: x_{0} := NULL ; □

      :: block_{bp} □

ϕ_{1} = (↘, x_{1} := x_{0})
m_{1} = {b_{p} ↦ NULL, b_{j} ↦ 10}
S_{1} = S(k_{1}, ϕ_{1}, m_{1})

k_{2} = □; goto l
:: x_{0} := int 10 ; □

                                     :: block_{bj} □
                                     :: if (load x_{0}) return
                                      else □

:: l: □
:: x_{0} := NULL ; □

                                     :: block_{bp} □

ϕ_{2} = (↗, x_{1} := x_{0})
m_{2} = {b_{p} ↦ ptr b_{j}, b_{j} ↦ 10}
S_{2} = S(k_{2}, ϕ_{2}, m_{2})

k_{3} = x_{1} := x_{0} ; □
:: x_{0} := int 10 ; □

                                                                     :: block_{bj} □
                                                                     :: if (load x_{0}) return
                                                                       else □

:: l: □
:: x_{0} := NULL ; □

                                                                     :: block_{bp} □

ϕ_{3} = (↘, goto l)
m_{3} = {b_{p} ↦ ptr b_{j}, b_{j} ↦ 10}
S_{3} = S(k_{3}, ϕ_{3}, m_{3})

Fig. 1. An example reduction path S_{1} ⇾ S_{2} ⇾ S_{3}.

When we relate our operational and axiomatic semantics in Section 5, we will have to restrict the traversal through the program to remain below a certain context.

Definition 3.7. The k-restricted reduction S_{1} ⇾_{k} S_{2} is defined as S_{1} ⇾ S_{2} provided that k is a suffix of the program context of S_{2}. We let ⇾_{k}^{∗} denote the reflexive-transitive closure, and ⇾_{k}^{n} paths of ≤ n steps.

Lemma 3.8. If S(k, (d, s), m) ⇾_{k}^{∗} S(k, (d′, s′), m′), then s = s′.

The previous lemma shows that the small step semantics indeed behaves as traversing through a zipper. Its proof is not entirely trivial due to the presence of function calls, as these add the statement of the called function to the state.

4 Axiomatic semantics

Judgments of Hoare logic are triples {P } s {Q}, where s is a statement, and P and Q are assertions called the pre- and postcondition. The intuitive reading of such a triple is: if P holds for the state before executing s, and execution of s terminates, then Q holds afterwards. To deal with non-local control flow and function calls, our judgments become sextuples Δ; J; R ⊢ {P } s {Q}, where:

– Δ is a finite function from function names to their pre- and postconditions. This environment is used to cope with (mutually) recursive functions.

– J is a function that gives the jumping condition for each goto. When executing a goto l, the assertion J l has to hold.

– R is the assertion that has to hold when executing a return.

The assertions P, Q, J and R correspond to the four directions ↘, ↗, ↷and ↑↑in which traversal through a statement can be performed. We therefore often treat the sextuple as a triple Δ; P̄ ⊢ s, where P̄ is a function from directions to assertions such that P̄ ↘= P, P̄ ↗= Q, P̄ (↷l) = J l and P̄ ↑↑= R.

We use a shallow embedding for the representation of assertions. This treatment is similar to that of Appel and Blazy [2] and Von Oheimb [15].

Definition 4.1. Assertions are predicates over the the stack and the memory. We define the following connectives on assertions.

\begin{matrix}P → Q := & λρ m . P ρ m → Q ρ m \\ P ∧ Q := & λρ m . P ρ m ∧ Q ρ m \\ P ∨ Q := & λρ m . P ρ m ∨ Q ρ m \\ ¬P := & λρ m . ¬P ρ m \\ ∀x . P x := & λρ m . ∀x . P x ρ m \\ ∃x . P x := & λρ m . ∃x . P x ρ m \end{matrix} P := λρ m . P

e ⇓ v := λρ m . [[ e]]_{ρ,m} = v
e ⇓ – := ∃v . e ⇓ v
e ⇓ ⊤ := ∃v . istrue v ∧ e ⇓ v
e ⇓ ⊥ := ∃v . isfalse v ∧ e ⇓ v
P [a := v] := λρ m . P ρ m[a := v]

We treat as an implicit coercion, for example, we write True instead of True . Also, we often lift the above connectives to functions to assertions, for example, we write P ∧ Q instead of λv . P v ∧ Q v.

Definition 4.2. An assertion P is stack independent if P ρ_{1} m → P ρ_{2} m for each memory m and stacks ρ_{1} and ρ_{2}, and similarly is memory independent if P ρ m_{1} → P ρ m_{2} for each stack ρ and memories m_{1} and m_{2}.

Next, we define the assertions of separation logic [14]. The assertion emp asserts that the memory is empty. The separating conjunction P ∗ Q asserts that the memory can be split into two disjoint parts such that P holds in the one part, and Q in the other. Finally, e_{1} ↦ e_{2} asserts that the memory consists of exactly one cell at address e_{1} with contents e_{2}, and e_{1} ↪ e_{2} asserts that the memory contains at least a cell at address e_{1} with contents e_{2}.

Definition 4.3. The connectives of separation logic are defined as follows.

emp := λρ m . m = ∅
P ∗ Q := λρ m . ∃m_{1} m_{2} . m = m_{1} ∪ m_{2} ∧ m_{1} ⊥ m_{2} ∧ P ρ m_{1} ∧ Q ρ m_{2}
e_{1} ↦ e_{2} := λρ m . ∃b v . [[ e_{1} ]]_{ρ,m} = ptr b ∧ [[ e_{2} ]]_{ρ,m} = v ∧ m = {(b, v)}
e_{1} ↦ – := ∃e_{2} . e_{1} ↦ e_{2}
e_{1} ↪ e_{2} := λρ m . ∃b v . [[ e_{1} ]]_{ρ,m} = ptr b ∧ [[ e_{2} ]]_{ρ,m} = v ∧ m b = v
e_{1} ↪ – := ∃e_{2} . e_{1} ↪ e_{2}

To deal with block scope variables we need to lift an assertion such that the De Bruijn indexes of its variables are increased. We define the lifting P ↑ of an assertion P semantically, and prove that it indeed behaves as expected.

Definition 4.4. The assertion P ↑ is defined as λρ m . P (tail ρ) m.

Lemma 4.5. We have (e ⇓ v) ↑ = (e↑) ⇓ v and (e_{1} ↦ e_{2}) ↑ = (e_{1} ↑) ↦ (e_{2} ↑), where the operation e↑ replaces each variable x_{i} in e by x_{i+1}. Furthermore, ( ) ↑ distributes over the connectives →, ∧, ∨, ¬, ∀, ∃, and ∗.

In order to relate the pre- and postcondition of a function, we allow universal quantification over arbitrary logical variables y⃗. The specification of a function with parameters v⃗ consists therefore of a precondition P y⃗ v⃗ and postcondition Q y⃗ v⃗. These should be stack independent because local variables will have a different meaning at the calling function than in the called function’s body. We will write such a specification as ∀y⃗ ∀v⃗ . {P y⃗ v⃗} {Q y⃗ v⃗}.

Definition 4.6. Given a function δ assigning statements to function names, the rules of the axiomatic semantics are defined as:

\begin{matrix}Δ; J; R ⊢ \{P \} s \{Q\} \\ Δ; A ∗ J; A ∗ R ⊢ \{A ∗ P \} s \{A ∗ Q\} \end{matrix} {∀x.(Δ; J; R ⊢ \{P x\} s \{Q\}) \atop Δ; J; R ⊢ \{∃x . P x\} s \{Q\}} (frame & exists)
{P′ → P Δ; J; R ⊢ \{P \} s \{Q\} Q → Q′ \atop Δ; J′; R′ ⊢ \{P′\} s \{Q′\}}  (weaken)

(∀l ∈ labels s . J′l → Jl) (∀l ∉ labels s . Jl → J′l) R → R′ Δ; J; R ⊢ {P } skip {P }  Δ; J; R ⊢ {R} return {Q}  (skip & return)

Δ; J; R ⊢ {∃a v . e_{1} ⇓ a ∧ e_{2} ⇓ v ∧ ptr a ↪ – ∧ P [a := v]} e_{1} := e_{2} {P } (assign)
\begin{matrix}Δ; J; R ⊢ \{J l\} s \{Q\} \\ Δ; J; R ⊢ \{J l\} l: s \{Q\} \end{matrix}  Δ; J; R ⊢ \{J l\} goto l \{Q\}  (label & goto)

{Δ; x_{0} ↦ – ∗ J ↑; x_{0} ↦ – ∗ R ↑ ⊢ \{x_{0} ↦ – ∗ P ↑\} s \{x_{0} ↦ – ∗ Q ↑\} \atop Δ; J; R ⊢ \{P \} block s \{Q\}}  (block)

\begin{matrix}Δ; J; R ⊢ \{P \} s_{1} \{P′\} & Δ; J; R ⊢ \{P′\} s_{2} \{Q\} \\ Δ; J; R ⊢ \{P \} s_{1} ; s_{2} \{Q\} \end{matrix}  (comp)

\begin{matrix}Δ; J; R ⊢ \{e ⇓ ⊤ ∧ P \} s_{1} \{Q\} & Δ; J; R ⊢ \{e ⇓ ⊥ ∧ P \} s_{2} \{Q\} \\ Δ; J; R ⊢ \{e ⇓ – ∧ P \} if (e) s_{1} else s_{2} \{Q\} \end{matrix}  (cond)
Δ f = {P } {Q} e⃗ ⇓ v⃗ ∧ P y⃗ v⃗ → A A memory independent

Δ; J; R ⊢ {e⃗ ⇓ v⃗ ∧ P y⃗ v⃗} f(e⃗) {A ∧ Q y⃗ v⃗} (call)

\begin{matrix}∀f P′ Q′ . Δ′f = (∀z⃗ ∀w⃗ . \{P z⃗ w⃗\} \{Q z⃗ w⃗\}) → ∀y⃗ v⃗ . \\ (Δ′ ∪ Δ; λl.False; Π_{∗}[x_{i} ↦ –] ∗ Q′y⃗ v⃗ ⊢ \{Π_{∗}[x_{i} ↦ v_{i}] ∗ P′y⃗ v⃗\} δ f \{Π_{∗}[x_{i} ↦ –] ∗ Q′y⃗ v⃗\}) \end{matrix}

\begin{matrix}Δ′ ∪ Δ; J; R ⊢ \{P \} s \{Q\} & dom Δ′ ⊆ dom δ \\ Δ; J; R ⊢ \{P \} s \{Q\} \end{matrix}  (add funs)

The traditional frame rule of separation logic [14] includes the side-condition vars s ∩ vars A = ∅ on the free variables in the statement s and assertion A. However, as our local variables are just (immutable) references into the memory, we do not need this side-condition. Also, the (frame) and (block) rule are uniform in all assertions, allowing us to write:

\begin{matrix}Δ; P̄ ⊢ s \\ Δ; A ∗ P̄ ⊢ s \end{matrix}  \begin{matrix}Δ; P̄ ⊢ block s \\ Δ; x_{0} ↦ – ∗ P̄ ↑ ⊢ s \end{matrix}

Since the return and goto statements leave the normal control flow, the postconditions of the (goto) and (return) rules are arbitrary.

Our rules for function calls are similar to those by Von Oheimb [15]. The (call) rule is to call a function that is already in Δ. It is important to notice that its postcondition is not e⃗ ⇓ v⃗ ∧ Q y⃗ v⃗, as after calling f evaluation of e⃗ may be different after all. However, in case e⃗ contains no load expressions, we have that e⃗ ⇓ v⃗ is memory independent, and we can simply take A to be e⃗ ⇓ v⃗.

The (add funs) rule can be used to add an arbitrary family Δ′ of specifications of (possibly mutually recursive) functions to Δ. For each function f in Δ′ with precondition P′ and postcondition Q′, it has to be verified that the function body δ f is correct for all instantiations of the logical variables y⃗ and input values v⃗. The precondition Π_{∗}[x_{i} ↦ v_{i}] ∗ P′y⃗ v⃗, where Π_{∗}[x_{i} ↦ v_{i}] denotes the assertion x_{i} ↦ v_{i} ∗ … x_{n} ↦ v_{n}, states that the function parameters x⃗ are allocated with values v⃗ for which the precondition P′ of the function holds. The post- and returning condition Π_{∗}[x_{i} ↦ –] ∗ Q′y⃗ v⃗ ensure that the parameters have not been deallocated while executing the function body and that the postcondition P′ of the function holds on a return. The jumping condition λl.False ensures that all gotos jump to a label that occurs in the function body.

Euclid’s algorithm in C:

void swap(int *p, int *q) {
  int z = *p; *p = *q; *q = z;

}

int gcd(int y, int z) {
  l: if (z) {
    y = y % z; swap(&y, &z); goto l;

  }

  return y;

}

Verification of the body of swap:

{x_{0} ↦ p ∗ x_{1} ↦ q ∗ p ↦ y ∗ q ↦ z}

  block (

{x_{0} ↦ – ∗ x_{1} ↦ p ∗ x_{2} ↦ q ∗ p ↦ y ∗ q ↦ z}

x_{0} := load (load x_{1}) ; {x_{0} ↦ y ∗ x_{1} ↦ p ∗ x_{2} ↦ q ∗ p ↦ y ∗ q ↦ z}

    load x_{1} := load (load x_{2}) ;

{x_{0} ↦ y ∗ x_{1} ↦ p ∗ x_{2} ↦ q ∗ p ↦ z ∗ q ↦ z}

    load x_{2} := load x_{0}

{x_{0} ↦ y ∗ x_{1} ↦ p ∗ x_{2} ↦ q ∗ p ↦ z ∗ q ↦ y}

) {x_{0} ↦ p ∗ x_{1} ↦ q ∗ p ↦ z ∗ q ↦ y}

Verification of the body of gcd:

{x_{0} ↦ int y ∗ x_{1} ↦ int z}

l : {J l}

                                                 if (load x_{1}) (

{load x_{1} ⇓ ⊤ ∧ J l}

{x_{0} ↦ int y′ ∗ x_{1} ↦ int z′ ∧ z′ ≠ 0 ∧ gcd y z = gcd y′ z′} x_{0} := load x_{0} % load x_{1} ; {x_{0} ↦ int (y′ % z′) ∗ x_{1} ↦ int z′ ∗ (z′ ≠ 0 ∧ gcd y z = gcd y′ z′ ∧ emp)}

swap(x_{0}, x_{1}) ; {x_{0} ↦ int z′ ∗ x_{1} ↦ int (y′ % z′) ∗ (z′ ≠ 0 ∧ gcd y z = gcd y′ z′ ∧ emp)} {J l}

                                                   goto l

{x_{0} ↦ int (gcd y z) ∗ x_{1} ↦ int 0}

                                                 ) else

{load x_{1} ⇓ ⊥ ∧ J l}

{x_{0} ↦ int y′ ∗ x_{1} ↦ int 0 ∧ gcd y z = gcd y′ 0}

                                                   skip

{x_{0} ↦ int (gcd y z) ∗ x_{1} ↦ int 0}

Fig. 2. Verification of Euclid’s algorithm.

As an example we verify Euclid’s algorithm for computing the greatest common divisor. We first verify the swap function, which takes two pointers p and q and swaps their contents. Its specification is as follows:

∀y z ∀p q . {p ↦ y ∗ q ↦ z} {p ↦ z ∗ q ↦ y}

Here, universal quantification over the logical variables y and z is used to relate the contents of the pointers p and q in the pre- and postcondition. In order to add this function to the context Δ of verified functions using the (add funs) rule, we have to prove that the body satisfies the above specification. An outline of this proof (with implicit uses of weakening) is displayed in Figure 2.

To verify the body of the gcd function, we use a jumping environment J that assigns ∃y′z′ . x_{0} ↦ int y′ ∗ x_{1} ↦ int z′ ∧ gcd y z = gcd y′ z′ to the label l. For the function call to swap, we use the (frame) rule with the framing condition z′ ≠ 0 ∧ gcd y z = gcd y′ z′ ∧ emp as displayed in Figure 2. We refer to the Coq formalization for the full details of these proofs.

5 Soundness of the axiomatic semantics

We define Δ; J; R ⊨ {P } s {Q} for Hoare sextuples in terms of our operational semantics. Proving soundness of the axiomatic semantics then consists of showing that Δ; J; R ⊢ {P } s {Q} implies that Δ; J; R ⊨ {P } s {Q}.

We want Δ; J; R ⊨ {P } s {Q} to ensure partial program correctness. Intuitively, that means: if P k m and S(k, (s, ↘), m) ⇾^{∗} S(k, (s, ↗), m′), then Q k m′. However, due to the additional features, this is too simple.

1. We also have to account for reductions starting in ↑↑or ↷direction. Hence, we take the four assertions J, R, P and Q together as one function P̄ and write Δ; J; R ⊨ {P } s {Q} as Δ; P̄ ⊨ s. The intuitive meaning of Δ; P̄ ⊨ s is: if P̄ d k m and S(k, (s, d), m) ⇾^{∗} S(k, (s, d′), m′), then P̄ d′ k m′.

2. We have to enforce the reduction S(k, (s, d), m) ⇾^{∗} S(k, (s, d′), m′) to remain below k as it could otherwise take too many items off the context.

3. Our language has various kinds of undefined behavior (e.g. invalid pointer dereferences). We therefore also want Δ; P̄ ⊨ s to guarantee that s does not exhibit such undefined behaviors. Hence, Δ; P̄ ⊨ s should at least guarantee that if P̄ d k m and S(k, (s, d), m) ⇾_{k}^{∗} S, then S is either:

– reducible (no undefined behavior has occurred); or:

– of the shape S(k, (s, d′), m′) with P̄ d′ k m′ (execution is finished).

4. The program should satisfy a form of memory safety so as the make the frame rule derivable. Hence, if before execution the memory can be extended with a disjoint part, that part should not be modified during the execution.

5. We take a step indexed approach in order to relate the assertions of functions in Δ to the statement s.

Together this leads to the following definitions:

Definition 5.1. Given a predicate P̄ over stacks, focuses and memories, specifying valid ending states, the relation P̄ ⊨_{n} Ŝ(k, ϕ, m ∪ □) is defined as: for each reduction S(k, ϕ, m ∪ m_{f}) ⇾_{k}^{n} S(k′, ϕ′, m′), we have that m′ is of the shape m′ = m′′ ∪ m_{f} for some memory m′′, and either:

1. there is a state S such that S(k′, ϕ′, m′) ⇾_{k} S; or:

2. k′ = k and P̄ k′ ϕ′ m′′.

Definition 5.2. Validity of the environment Δ, notation ⊨_{n} Δ is defined as: if Δ f = (∀y⃗ . ∀v⃗ . \{P y⃗ v⃗\} \{Q y⃗ v⃗\}) and P y⃗ v⃗ k m, then Q′ ⊨_{n} Ŝ(k, \overline{call} f v⃗, m ∪ □), where Q′ := λρ ϕ m′ . (ϕ = \overline{return}) ∧ Q y⃗ v⃗ ρ m′.

Definition 5.3. Validity of a statement s, notation Δ; P̄ ⊨ s is defined as: if ⊨_{n} Δ, down d s, and P̄ d k m, then Q′ ⊨_{n} Ŝ(k, (d, s), m ∪ □), where

Q′ := λρ ϕ m′ . ∃d′ s′ . ϕ = (d′, s′) ∧ ¬down d′ s′ ∧ P̄ d′ ρ m′

The predicate down holds if down ↘s′ or down (↷l) s′ with l ∈ labels s′.

Proposition 5.4 (Soundness). Δ; P̄ ⊢ s implies Δ; P̄ ⊨ s.

This proposition is proven by induction on the derivation of Δ; P̄ ⊢ s. Thus, for each rule of the axiomatic semantics, we have to show that it holds in the model. The rules for the skip, return, assignment, goto and function calls are proven by chasing all possible reduction paths. In the case of the assignment statement, we need weakening of expression evaluation (Lemma 2.5).

All structural rules are proven by induction on the length of the reduction. These proofs involve chasing all possible reduction paths. We refer to the Coq formalization for the proofs of these rules.

6 Formalization in Coq

All proofs in this paper have been fully formalized using the Coq proof assistant. Formalization has been of great help in order to develop and debug the semantics. We used Coq’s notation mechanism combined with unicode symbols and type classes for overloading to let the Coq development correspond as well as possible to the definitions in this paper.

There are some small differences between the Coq development and this paper. Firstly, we omitted while statements and functions with return values here, whereas they are included in the Coq development. Secondly, in this paper, we presented the axiomatic semantics as an inference system, and then showed that it has a model. Since we did not consider completeness, in Coq we directly proved all rules to be derivable with respect to the model.

We used type classes to provide abstract interfaces for commonly used structures like finite sets and finite functions, so we were able to prove theory and implement automation in an abstract way. Our approach is greatly inspired by the unbundled approach of Spitters and van der Weegen [17]. However, whereas their work heavily relies on setoids (types equipped with an equivalence relation), we tried to avoid that, and used Leibniz equality wherever possible. In particular, our interface for finite functions requires extensionality with respect to Leibniz equality. That means m_{1} = m_{2} ↔ ∀x . m_{1} x = m_{2} x.

Intensional type theories like Coq do not satisfy extensionality. However, finite functions indexed by a countable type can still be implemented in a way that extensionality holds. For the memory we used finite functions indexed by binary natural numbers implemented as radix-2 search trees. This implementation is based on the implementation in CompCert [12]. But whereas CompCert’s implementation does not satisfy canonicity, and thus allows different trees for the same finite function, we have equipped our trees with a proof of canonicity. This way, equality on these finite functions as trees becomes extensional.

Extensional equality on finite functions is particularly useful for dealing with assertions, which are defined as predicates on the stack and memory (Definition 4.1). Due to extensionality, we did not have to equip assertions with a proof of well-definedness with respect to extensional equality on memories.

Although the semantics described in this paper is not extremely big, it is still quite cumbersome to be treated without automation in a proof assistant. In particular, the operational semantics is defined as an inductive type consisting of 32 constructors. To this end, we have automated many steps of the proofs. For example, we implemented the tactic do_cstep to automatically perform reduction steps and to solve the required side-conditions, and the tactic inv_cstep to perform case analyzes on reductions and to automatically discharge impossible cases. Ongoing experiments show that this approach is successful, as the semantics can be extended easily without having to redo many proofs.

   Our Coq code, available at http://robbertkrebbers.nl/research/ch2o/,

is about 3500 lines of code including comments and white space. Apart from that, the library on general purpose theory (finite sets, finite functions, lists, etc.) is about 7000 lines, and the gcd example is about 250 lines.

7 Conclusions and further research

The further reaching goal of this work is to develop an operational semantics for a large part of the C11 programming language [8] as part of the Formalin project [10]. In order to get there, support for non-local control flow is a necessary step. The operational semantics in this paper extends easily to most other forms of non-local control in C: the break and continue statement, and non-structured switch statements (e.g. Duff’s device). To support these, we just have to add an additional direction and its corresponding reduction rules.

In this paper we have also defined an axiomatic semantics. The purpose of this axiomatic semantics is twofold. Firstly, it gives us more confidence in the correctness and usability of our operational semantics. Secondly, in order to reason about actual C programs, non-local control flow and pointers to block scope variables have to be supported by the axiomatic semantics.

Unfortunately, the current version of our axiomatic semantics is a bit cumbersome to be used for actual program verification. The foremost reason is that our way of handling local variables introduces some overhead. In traditional separation logic [14], there is a strict separation between local variables and allocated storage: the values of local variables are stored directly on the stack, whereas the memory is only used for allocated storage. To that end, the separating conjunction does not deal with local variables, and many assertions can be written down in a shorter way. For example, even though we do not use pointers to the local variables of the swap function (Figure 2), we still have to deal with two levels of indirection.

It seems not too hard to make allocation of local variables in the memory optional, so that it can be used only for variables that actually have pointers to them. Ordinary variables then correspond nicely to those with the register keyword in C. Alternatively, the work of Parkinson et al. [16] on variables as resources may be useful.

Another requirement to conveniently use an axiomatic semantics for program verification is strong automation. Specific to the Coq proof assistant there has been work on this by for example Appel [1] and Chlipala [3]. As our main purpose is to develop an operational semantics for a large part of C11, we consider automation a problem for future work.

In order to get closer to a semantics for C11 we are currently investigating the following additional features of the C11 standard.

– Expressions with side effects and sequence points.

– The C type system including structs, unions, arrays and integer types.

– The non-aliasing restrictions (effective types in particular).

We intend to support these features in both our operational and axiomatic semantics. Ongoing work shows that our current operational semantics can easily be extended with non-deterministic expressions using a similar approach as Norrish [13] and Leroy [12]. As non-determinism in expressions is closely related to concurrency, we use separation logic for a Hoare logic for expressions.

In this paper we have not considered completeness of the axiomatic semantics as it is not essential for program verification. Also, our future extension for nondeterministic expressions with side-effects will likely be incomplete.

Another direction for future research is to relate our semantics to the Comp-Cert semantics [12] (by eliminating block scope variables). That way we can link it to actual non-local jumps in assembly.

Acknowledgments. We thank Erik Poll for bringing up the idea of an axiomatic semantics for gotos, and thank Herman Geuvers and the anonymous referees for providing several helpful suggestions. This work is financed by the Netherlands Organisation for Scientific Research (NWO).

References

1. A. W. Appel. Tactics for Separation Logic, 2006. Available at http://www.cs.

princeton.edu/^{∼}appel/papers/septacs.pdf.

2. A. W. Appel and S. Blazy. Separation Logic for Small-Step Cminor. In TPHOLs, volume 4732 of LNCS, pages 5–21, 2007.

3. A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, pages 234–245. ACM, 2011.

4. E. W. Dijkstra. Go To statement considered harmful. Communications of the ACM, 11(3):147–148, 1968. letter to the Editor.

5. C. Ellison and G. Rosu. An executable formal semantics of C with applications. In POPL, pages 533–544, 2012.

6. M. Felleisen and R. Hieb. The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science, 103(2):235–271, 1992.

7. G. P. Huet. The Zipper. Journal of Functional Programming, 7(5):549–554, 1997.

8. International Organization for Standardization. ISO/IEC 9899-2011: Programming languages – C. ISO Working Group 14, 2012.

9. D. Knuth. Structured programming with go to statements. In Classics in software engineering, pages 257–321. Yourdon Press, 1979.

10. R. Krebbers and F. Wiedijk. A Formalization of the C99 Standard in HOL, Isabelle and Coq. In CICM, volume 6824 of LNAI, pages 297–299, 2011.

11. X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009.

12. X. Leroy. The CompCert verified compiler, software and commented proof. Avail-

able at http://compcert.inria.fr/, 2012.

13. M. Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998.

14. P. W. O’Hearn, J. C. Reynolds, and H. Yang. Local Reasoning about Programs that Alter Data Structures. In CSL, volume 2142 of LNCS, pages 1–19, 2001.

15. D. v. Oheimb. Hoare Logic for Mutual Recursion and Local Variables. In FSTTCS, volume 1738 of LNCS, pages 168–180, 1999.

16. M. J. Parkinson, R. Bornat, and C. Calcagno. Variables as Resource in Hoare Logics. In LICS, pages 137–146, 2006.

17. B. Spitters and E. van der Weegen. Type classes for mathematics in type theory. Mathematical Structures in Computer Science, 21(4):795–825, 2011.

18. H. Tews. Verifying Duff’s device: A simple compositional denotational semantics for Goto and computed jumps, 2004.