End-to-End Verification of Stack-Space Bounds for C Programs
Zhong Shao
tifact ** Complete* Consi

cu m
e

*

ll
We

st

t
en

*

PLDI *

Ar*
AECDo Ev

Yale University
tquentin.carbonneaux, jan.hoffmann, tahina.ramananandro, zhong.shaou@yale.edu

seeu

Tahina Ramananandro* Easy toed
Rnt

Jan Hoffmann

alu

Quentin Carbonneauxat e dAbstract

1.

Verified compilers guarantee the preservation of semantic properties
and thus enable formal verification of programs at the source level.
However, important quantitative properties such as memory and time
usage still have to be verified at the machine level where interactive
proofs tend to be more tedious and automation is more challenging.
This article describes a framework that enables the formal
verification of stack-space bounds of compiled machine code at
the C level. It consists of a verified CompCert-based compiler that
preserves quantitative properties, a verified quantitative programlogic for interactive stack-bound development, and a verified stackanalyzer that automatically derives stack bounds during compilation.
The framework is based on event traces that record function calls
and returns. The source language is CompCert Clight and the target
language is x86 assembly. The compiler is implemented in the Coq
Proof Assistant and it is proved that crucial properties of event traces
are preserved during compilation. A novel quantitative Hoare logic is
developed to verify stack-space bounds at the CompCert Clight level.
The quantitative logic is implemented in Coq and proved sound withrespect to event traces generated by the small-step semantics of
CompCert Clight. Stack-space bounds can be proved at the source
level without taking into account low-level details that depend on
the implementation of the compiler. The compiler fills in these
low-level details during compilation and generates a concrete stackspace bound that applies to the produced machine code. The verified
stack analyzer is guaranteed to automatically derive bounds forcode with non-recursive functions. It generates a derivation in thequantitative logic to ensure soundness as well as interoperability
with interactively developed stack bounds.
In an experimental evaluation, the developed framework isused to obtain verified stack-space bounds for micro benchmarks
as well as real system code. The examples include the verified
operating-system kernel CertiKOS, parts of the MiBench embedded
benchmark suite, and programs from the CompCert benchmarks.
The derived bounds are close to the measured stack-space usage of
executions of the compiled programs on a Linux x86 system.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; D.3.3 [Programming Languages]: Processors—Compilers
Keywords Formal Verification, Compiler Construction, Program
Logics, Stack-Space Bounds, Quantitative Verification

It has been shown that formal verification can greatly improve
software quality [25, 33, 35]. Consequently, formal verification isextensively studied in ongoing research and there exist sophisticatedtools that can verify important program properties automatically.
However, the most interesting program properties are undecidable
and user interaction is therefore inevitable in formal verification.
If a software system is (partly or entirely) developed in a highlevel language then the question arises on which language level
the verification should be carried out. Formal verification at thesource level has the advantage that a developer can interact with theverification tools using the code she has developed. This is beneficial
because the compiled code can substantially differ from the sourcecode and low-level code is harder to understand. Moreover, evenfully automatic tools profit from the control-flow information andthe structure that is available at higher abstraction layers. The
disadvantage of verification at the source level is that tools such ascompilers have to be part of the trusted computing base and that theverified properties are not directly guaranteed for the code that is
executed on the system.
Formally verified compilers [11, 24] such as the CompCert C
Compiler [27] guarantee that certain program properties of thesource programs are preserved during compilation. As a result,
CompCert enables source-level verification of the preserved properties of the compiled code without increasing the size of the trusted
computing base.1 In fact, this has been one of the main motivations for the development of CompCert [27]. However, important
quantitative properties such as memory and time consumption are
not modeled nor preserved by CompCert and other verified compilers [11, 24]. Such quantitative properties are nevertheless crucial in
the verification of safety-critical embedded systems. For example,
the DO-178C standard, which is used by in the avionics industry
and by regulatory authorities, requires verification activities to showthat a program in executable form complies with its requirements
on stack usage and worst-case execution time (WCET) [28].
Quantitative program requirements such as stack usage and
WCET are usually directly checked at the machine or assemblycode level “since only at this level is all necessary information available” [34]. For stack-space bounds there exist commercial abstract
interpretation–based tools—such as Absint’s StackAnalyzer [14]—that operate directly on machine code. While such tools can derive
many simple bounds automatically, they rely on user annotations in
the machine code to obtain bounds for more involved programs. The
produced bounds are usually not parametric in the input, and theanalysis is not modular and only applies to specific hardware platforms. Additionally, the used analysis tools rely on the correctnessof the user annotations and are not formally verified.
In this article, we present the first framework for deriving
formally verified end-to-end stack-space bounds for C programs.
Stack bounds are particularly interesting because stack overflow

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for components of this work owned by others than theauthor(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specific permission
and/or a fee. Request permissions from permissions@acm.org.
PLDI ’14, June 9 - 11, 2014, Edinburgh, United Kingdom.
Copyright is held by the owner/author(s). Publication rights licensed to ACM.
ACM 978-1-4503-2784-8/14/06. . . $15.00.
http://dx.doi.org/10.1145/2594291.2594301

Introduction

1 If we assume that all verification is carried out using the same trusted base.

is “one of the toughest (and unfortunately common) problems
in embedded systems” [13]. Moreover, stack-memory is the only
dynamically allocated memory in many embedded systems and thestack usage depends on the implementation of the compiler. While
we focus exclusively on stack bounds in this article, our framework
is developed with other quantitative resources in mind. Many of thedeveloped techniques can be applied to derive bounds for resources
such as heap memory or clock cycles. However, for clock-cycle
bounds there is a lot of additional work to be done that is beyond thescope of this article (e.g., developing a formal model for hardware
caches and instruction pipelines).
The main innovation of our framework is that it enables theformal verification of stack bounds for compiled x86 assembly
code at the C level. To gain the benefits of source-level verification
without the entailed disadvantages, we have to deal with three main
challenges.
1. We have to model the stack consumption of programs at the C
level and we have to formally prove that our model is consistent
with the stack consumption of the compiled code.
2. We have to design and implement a C-level verification mechanism that allows users to derive parametric stack-usage bounds
in an interactive and flexible way.
3. We have to minimize user interaction during the verification to
enable the verification of large systems.
To meet Challenge 1, we use event traces and verified compilation.
Our starting point is the CompCert C Compiler. It relies on event
traces to prove that a compiled program is a refinement of the source
program. We extend event traces with events for function calls andreturns and define a weight for event traces. The weight describes
the stack-space consumption of one program execution as a functionof a cost metric that assigns a cost to individual call and return
events. The idea is that a user or an (semi) automatic analysis tool
derives bounds on the weights of event traces that depend on thestack-frame sizes of the program functions. During compilation thecompiler produces a specific cost metric that guarantees that theweight of an event trace under this metric is an upper bound on
the stack-space usage of the compiled assembly program which
produces this trace. As a result, we derive a verified upper bound
if we instantiate the derived memory bound with the cost metricproduced by the compiler.
We implemented the extended event traces for full CompCert C
and all intermediate languages down to x86 assembly in Coq. We
extended CompCert’s soundness theorem to take into account theweights of traces. In addition to CompCert’s refinement theorem
for the original event traces, we prove that compiled programs
produce extended event traces whose weights are less than or equal
to the weights of the traces at the source level. This means that weallow reordering or deletion of call and return events as long as theweight of the trace is reduced or unchanged. To relate the weightof traces to the execution on a system with finite stack space, we
modified the CompCert x86 assembly semantics into a more realistic
x86 assembly that features a finite stack, and reimplemented theassembly generation pass of CompCert to our new x86 assembly
semantics.
To meet Challenge 2, we have developed and implemented a novel
quantitative Hoare logic for CompCert Clight in Coq. To account for
memory consumption, the assertions of the logic generalize the usual
boolean-valued assertions of Hoare logic. Instead of the classic true,
our quantitative assertions return a natural number that indicatesthe amount of memory that is needed to execute the program. The
boolean false is represented by 8 and indicates that there are no
guarantees provided for the future execution.
We proved the soundness of our quantitative Hoare logic withrespect to Clight and CompCert’s continuation-based small-stepsemantics. The soundness theorem states that Hoare triples thatare derived with our inference rules describe sound bounds on theweights of traces. The logic can be used for interactive stack-bounddevelopment or as a backend for verified static analysis tools. For
clarity, we do not prove the safety of programs and simply assume
that this is done using a different tool such as Appel’s separation
logic for Clight [3]. It would be possible to integrate our logic into
a separation logic for safety proofs. This would however diminish
the deployability of the quantitative logic as a backend for static
stack-bound analysis tools since they would be required to also
prove memory safety.
To meet Challenge 3, we implemented an automatic stack analyzer for C programs. To verify the soundness of the stack analyzer
each successful run generates a derivation in the quantitative Hoare
logic. Not only does this simplify the verification, but it also allows interoperability with stack bounds that have been interactively
developed in the logic or derived by some other static analysis. Conceptually, our stack analyzer is rather simple but we have provedthat it derives bounds for all programs without recursion and function pointers. This is already sufficient for many programs that areused in embedded systems. Using our automatic analysis we havecreated a verified C compiler that translates a program without function pointers and recursive calls to x86 assembly and automaticallyderives a stack bound for each function in the program including
mainpq.
We have successfully used our framework to verify end-to-end
memory bounds for micro benchmarks and system software. Our
main example is the CertiKOS [15] operating system kernel that iscurrently under development at Yale. Our automatic analyzer finds
stack bounds for all functions in the simplified development versionof CertiKOS that is currently verified. Other examples are takenfrom Leroy’s CompCert benchmarks and the MiBench embedded
benchmark suite [17]. To evaluate the quality of the verified stackspace bounds, we experimentally compared the automatically andmanually verified bounds with the actual stack-space consumption
during the execution of the compiled C programs. Our experiments
indicate that both the manually and automatically derived bounds
over-approximate the stack usage by exactly four bytes. More details
can be found in Section 6.
In summary, we make the following contributions.
• We introduce a methodology that uses cost metrics to link event
traces to resource consumption. This approach enables us tolink source-level code to the resource consumption of compiled
target-level code.
• We develop a novel quantitative Hoare logic to reason about
the resource consumption of programs at the source level. We
have formally verified the soundness of the logic with respect to
CompCert Clight in Coq.
• We introduce Quantitative CompCert, a modified version of
the verified CompCert C Compiler, in which parametric stackbounds are preserved during compilation. Furthermore, Quantitative CompCert creates a cost metric so that the instantiation of
the bounds with the metric forms an upper bound on the memory
consumption of the compiled code.
• We have implemented and verified an automatic stack analyzer.
• We have evaluated the practicability of our framework withexperiments using micro benchmarks and system code.
The complete Coq development and the implemented tools are well
documented and publically available on the authors’ websites. The
PLDI Artifact Evaluation Committee reproduced samples of our experiments and tested the implemented tools on additional programs.
The reviewers unanimously stated that our implementation exceeded
their expectations. A companion technical report [9] contains additional explanation, lemmas, and examples.

2.

An Illustrative Example

typedef unsigned int u32;
u32 a[ALEN];
u32 seed = SEED;In this section, we sketch the verification of stack-space bounds foran example program in our framework. Figure 1 shows a C programwith two integer parameters: ALEN and SEED.
This program will fill an array of size ALEN with an increasing
sequence of pseudo random integers and search through it. The
random numbers are created by a linear congruential generator
initialized by the SEED parameter. The search procedure used is abinary search implemented in the recursive function search.
Our goal is to derive stack bounds for the compiled x86 assembly
code of the program that are verified with respect to our accurate
x86 model in Coq. The first step is to create an abstract syntax treeof the code in Coq. This can be done automatically, for instance byusing CompCert’s parsing mechanism. The second step is to use ourquantitative Hoare logic to prove bounds on the function calls thatare performed when executing main.
To relate function calls and returns at different abstraction levels
during compilation we use call and return events. For instance, an
execution of main could produce the following trace.

u32 search(u32 elem, u32 beg, u32 end) {u32 mid = beg + (end-beg) / 2;
if (end-beg <= 1) return beg;
if (a[mid] > elem) end = mid;else beg = mid;return search(elem, beg, end);}
u32 random() {seed = (seed * 1664525) + 1013904223;
return seed;}void init() {u32 i, rnd, prev = 0;
for (i=0; i<ALEN; i++) {rnd = random();a[i] = prev + rnd % 17;
prev = a[i]; }callpmainq, callpinitq, callprandomq, retprandomq, retpinitq,
callpsearchq, callpsearchq, retpsearchq, retpsearchq, retpmainq}
int main() {u32 idx, elem;init();
elem = random() % (17 * ALEN);
idx = search(elem, 0, ALEN);
return a[idx] == elem;}

From such a trace and a metric M that maps each function name in
the program to its stack-frame size, we can obtain the stack usageof the execution that produced the trace. For the previous example
trace, we can for instance derive the following stack usage.
M pmainq ` maxtM pinitq ` M prandomq, 2 ¨ M psearchqu
In classical Hoare logic, assertions map program states to Booleans.
In our quantitative Hoare logic assertions map program states to
non-negative numbers. Intuitively, the meaning of a quantitative
Hoare triple tP u S tQu is the following. For every program state σ,
P pσq is an upper bound on the stack consumption of the statement
S started in state σ. Furthermore, Q describes the stack space thathas become available after the execution, as a function of the final
program state. This is similar to type systems and program logics
for amortized resource analysis [5, 21].
We implemented a function in Coq that automatically computes
a derivation in the quantitative logic for a program without recursive functions. Using this automatic stack analyzer, we derive for
instance the following triple for the function call initpq.
tM pinitq ` M prandomqu initpq tM pinitq ` M prandomqu
For functions making use of recursion such as search, we derive aquantitative triple interactively using Coq. For search we derivetLpend ´ begqu searchpelem, beg, endq tLpend ´ begquwhere Lp∆q “ M psearchq¨p2`log2 p∆qq . Since the mathematicallog2 function is undefined on non-positive values, we take asconvention that log2 p∆q “ `8 when ∆ ă 0 and log2 p0q “ 0.
This trick allows us to simulate a logical precondition stating thatbeg must be lower or equal to end before calling search.
For main we combine the previous results and derive the boundtM pmainq ` N u mainpq tM pmainq ` N u
where N “ maxpM pinitq ` M prandomq, LpALENqq. To be able
to derive this bound on the main function we have to require that0 ă ALEN ď 232 ´ 1, in the Coq development this is stated as asection hypothesis which will later be instantiated when ALEN ischosen by the user before compiling.
The third and final step in the derivation of the stack bounds
is to compile the program with Quantitative CompCert, our modified CompCert C Compiler. The compiler produces x86 assembly code and a concrete metric M0 . It follows from CompCert’s
correctness theorem that the compiled code is a semantic refine-Figure 1. An illustrative example for static stack-bound computation. Constant stack bounds for the non-recursive functions are derived automatically. The logarithmic bound for the function search
is derived with a hand-crafted proof in our quantitative Hoare logic.
ment of our source program. In addition, we have formally verified
that the metric M0 correctly relates the abstractly defined stackconsumption—using the event traces—to the actual stack consumption in our abstract x86 machine. Moreover, we have verified that
applying M0 to the preconditions in the triples of the quantitative
Hoare logic results in sound stack bounds on the x86 machine. The
final bounds that we obtain for our examples are for instance 32
bytes for initpq and 112 ` 40 ¨ log2 pALENq bytes for mainpq.

3.

Quantitative CompCert: Verified Stack-Aware
Compilation

In this section, we introduce our new technique for verifying quantitative compiler correctness and its implementation in Quantitative
CompCert. We focus on stack-space usage but believe that similar
techniques can be used to bound the time and heap-space requirements of programs. Our development is highly influenced by thedesign of CompCert [27], a verified compiler for the C language.
CompCert C accepts most of the ISO-C-90 language and produces
machine code for the IA32 architecture (among others). CompCert
uses 11 intermediate languages and 20 passes to compile a C AST
to x86 assembly.
The soundness proof of CompCert is based on trace-based operational semantics for the source, target, and intermediate languages.
These semantics generate traces of events during the execution ofprograms. Events include input/output and external function calls.
The soundness theorem of CompCert states that every event tracethat can be generated by the compiled program can also be generated
by the source program provided that the source program does not
go wrong. In other words, the compiled program is a refinement of
the source program with respect to the observable events.

Safety Proof

Source Program

Weight Bound

Verified Quantitative
Hoare Logics: (E ! Z) ! N

8 M . WM (s)  (M)C (s) v s

Safety Proof

C (s) vQ s

Verified Compiler
stack(C (s))  WMs (C (s))

Target Program

Event Metric

Stack-Usage BoundC (s)Ms : E ! Z

stack(C (s))  (Ms )Figure 2. Overview of our quantitative verification framework. We write WM psq “ suptWM pBq | B P JsKu for the weight of the programs under the metric M . We write stackpsq for the smallest number n so that s runs without stack overflow if executed with a stack of size n.
3.1 Quantitative Compiler Correctness
In the following, we show how to extend trace-based compilercorrectness proofs to also cover stack-space consumption. In short,
our technique works as follows.
1. We generate events for all semantic actions that are relevant for
stack-space usage, that is, function calls and returns.
2. We define a weight function for event traces that describes thestack-space consumption of program executions that producethat trace. The weight of an event trace is parameterized by aresource metric that describes the cost of each event.
3. We formally verify that for all resource metrics and for all
event traces produced by a target program, the source program
either goes wrong or produces an equivalent (see the following
definition) event trace with a greater or equal weight.
4. During compilation, we produce a cost metric that accurately
describes the memory consumption of target programs: If an
execution of a target program produces an event trace of weight nunder the produced metric then this execution can be performed
on a system with stack size n.
We now formalize and elaborate on these points.
Event Traces In CompCert, the observable events are externalfunction calls (e.g., I/O events) that are represented by function
identifiers together with a list of input values and an output value
as given by the following grammar. To track stack usage, we add
memory events for internal function calls and returns. In contrast
to I/O events, memory events do not have to be preserved duringcompilation.
Event values
I/O events

v ::“ intpnq | floatpqq
ν ::“ f p~v ÞÑ vq

Memory eventsµ ::“ callpx q | retpx q

Event traces are defined in a similar way to CompCert. We distinguish finite (inductive) traces t and possibly infinite (coinductive)
traces T . A program behavior is either a converging computation
convpt, nq producing a finite event trace t and a return code n, adiverging computation divpT q producing a finite or infinite trace
T , or a computation failptq that goes wrong and produces the finite
trace t.
Finite event traces
Coinductive event traces
Behaviorst ::“  | ν ¨ t | µ ¨ t
T ::“  | ν ¨ T | µ ¨ T
B ::“ convpt, nq | divpT q | failptq

We write E for the set of memory and I/O events, B for the set of
behaviors, and T for the set of traces.

Weights of Behaviors For a behavior B, we define the set of finite
prefix traces prefspBq of B as follows.
prefspconvpt, nqq “ tt1 | t “ t1 ¨ t2 u
prefspdivpT qq “ tt | T “ t ¨ T 1 u
prefspfailptqq “ tt1 | t “ t1 ¨ t2 u
The weight WM pBq P N Y t8u of a behavior B describes thenumber of bytes that are needed in an execution that produces B. It
is parameterized by a resource metric M : E Ñ Z that maps events
to integers (bytes). The purpose of the metric in our work is to relate
memory events to the sizes of the stack frames of functions in thetarget code. To this end, we only use stack metrics, that is, metrics
M such that for all functions f and for all external functions g
0 ď M pcallpf qq “ ´M pretpf qq and M pgp~v ÞÑ vqq “ 0 .
In the Coq implementation of our compiler, we can also deal with
nonzero stack consumption for external functions as long as thestack consumption of each call is bounded by a constant.
Before we define the weight, we first inductively define thevaluation VM ptq of a finite trace t.
VM pq “ 0andVM pα ¨ tq “ VM ptq ` M pαq

We now define the weight WM pT q of a potentially infinite trace
T and the weight WM pBq of a behavior B under the metric M as
follows:
WM pT q “ suptVM ptq | T “ t ¨ T 1 u
WM pBq “ suptVM ptq | t P prefspBqu
Quantitative Refinement For our description of quantitative refinements we leave the definition of programs abstract. A programs P P is simply an object that is associated, through a function
J¨K : P Ñ B, with a set of behaviors JsK P B. An execution of aprogram can produce different traces, either due to non-determinism
in the semantics or due to user inputs recorded in the event traces.
For a behavior B we define the pruned behavior as the behavior
B that results from deleting all memory events (callpx q or retpx q)
from B. The formal definition can be found in the TR [9].
In CompCert, compiler correctness is formalized through thenotion of refinement. A (target) program s1 is a refinement of a(source) program s, written s1 ă s, if for every behavior B 1 P Js1 K
there is B P JsK such that B “ B 1 or failptq P JsK for some trace t.2
Note that memory events are not taken into account in CompCert’sclassic definition of refinement.
2 In fact, it is enough to prove that B 1 „ B (bisimilarity of infinite traces),because JsK is closed by bisimilarity.

Quantitative Hoare Logic

x86 ASM

Automatic Stack Analyzer

Stack Merging

CompCert 1.13 w

C Source

wQ

ClightwQ

CminorwQ

wQLinear

wQ

Mach

wQ

Mach2szw

x86 ASMsz

Figure 3. Our modified stack-aware CompCert C compiler. We replace CompCert’s x86 assembly with the more realistic x86 assembly
semantics ASMsz with finite stack. Pseudo assembly instructions such as Pallocframe and Pfreeframe are not needed anymore.
To also relate the memory events in the behaviors of two
programs, we define a novel quantitative refinement. A (target)
program s1 is a quantitative refinement of a (source) program s,
written s1 ăQ s if the following holds. For every behavior B 1 P Js1 K
there exists B P JsK such that B “ B 1 and WM pB 1 q ď WM pBq
for all stack metrics M , or failptq P JsK for some trace t. In
Quantitative CompCert, our modified CompCert compiler, we provefor each compiler pass C that Cpsq ăQ s for every program s.
Verifying Stack-Space Usage Figure 2 summarizes how we verify
the stack-space usage of a program in our framework. First, we
prove a bound β : pE Ñ Zq Ñ N on the weights of the event
traces that a program can produce. This bound is parameterized byan event metric M : E Ñ Z. Second, our verified compiler—thanks
to quantitative refinement—ensures that the computed bound also
holds for the weights of the traces of the compiled program.
Third, we have to relate the computed bound to the actual stackusage of the compiled code. Therefore, our compiler computes not
only a target program Cpsq but also a metric Ms such that Cpsq
can be safely executed with a stack-memory size of suptWMs pBq |B P JCpsqKu bytes. As a result, the initially derived bound for thesource code can be instantiated with the metric Ms to obtain thewanted stack-space bound Ms pβq for the target program.
In this overview picture, we assume that the semantics of thetarget and source languages are both formulated with an unboundedstack. The final step of the soundness proof (not illustrated in
Figure 2) is to relate the trace-based semantics of the target language
to a realistic assembly semantics in which the program is executedwith a fixed stack size. To this end, we prove that an executionof Cpsq with bounded stack space suptWMs pBq | B P JCpsqKu
is a refinement of the execution of Cpsq in the semantics withunbounded stack (see explanation in Section 3.2).
3.2 Verification and Implementation
We implemented the verification framework that we outlined in
Section 3.1 for the CompCert C compiler using the proof assistantCoq. The verification consists of about 5000 lines of Coq code that
we integrated into CompCert 1.13 (which originally consists ofabout 90000 lines of Coq code) to obtain a modified version that wecall Quantitative CompCert. CompCert 1.13 is decomposed into 20
passes between 11 intermediate languages (see [9] for an overview).
We describe our modified Quantitative CompCert in this section.
The problem: stack consumption in CompCert For each intermediate language of CompCert (beyond C subsets), each function callallocates a memory region—called the stack frame—to store its
addressable local variables, and later the spilling locations and thefunction arguments to handle the calling conventions. This stack
frame is freed upon function return. However, even though eachstack frame is finite, there may well be an unbounded number ofsuch allocations, even for nested function calls. Indeed, in CompCert,
allocating a stack frame always succeeds, thus CompCert does notmodel stack overflow.
Our solution: Quantitative CompCert In Quantitative CompCert,
we overcome this issue by modifying the semantics of the target
assembly language. We preallocate a finite memory region for thewhole stack, into which all stack frames shall be merged together
during the execution instead of being individually allocated.
By contrast, we still want the source and intermediate languages
to allocate an individual stack frame per function call. First, wewant to change CompCert only if necessary so as to still support allfeatures of CompCert C. Second, it would not be very meaningful
to introduce a finite stack at a high language level since it is unclear
how to model stack sizes. The only major change we bring to thoselanguages is to introduce our call and return events into the trace.
As shown in Figure 3, this leads us to split CompCert into
two parts. In the first part, we compile CompCert C down to
the CompCert Mach low-level language (which comes just before
assembly generation) by adapting the proofs of existing passes toquantitative refinement. In the second part, we perform two passes
to merge all stack frames together. The key point of our work is that
this second part will require the Mach traces to not stack overflow,which justifies the use of quantitative refinement for the first part.
Quantitative Refinement In the first part of the compiler, from
CompCert C down to Mach, we add call and return events to thesemantics of each language, at the level of each function call andreturn (as described in Section 3.1). This change is uniform in all
languages between CompCert C to Mach: indeed, in each small-step
operational semantics, the rules responsible for internal function
call and return all have the same shape.
Then, thanks to these changes, we support all of CompCert 1.13
passes except two optional optimizations (see Section 3.3), and,with no significant changes to the proofs, we prove that they exactly
preserve traces with function call events.
Generation of Target Cost Metric The semantics of CompCert
C allocates a separate memory region for each addressable local
variable. In Mach, all those variables as well as the spilling locations,the function arguments, and the return address are stored in astack frame. Actually, the stack frame of a Mach function call iscompletely laid out, so that no additional memory is necessary whengenerating the CompCert x86 assembly code. This means that, atthe level of Mach, we already know the stack size necessary for afunction call (thanks to the fact that the original CompCert does notsupport some C features, see 3.3): for a given function, this size isconstant and does not depend on the arguments nor the input. So, we
can use the sizes of Mach stack frames as cost metric for functions
to accurately estimate stack bounds at the source level.
Generation of Assembly Code Recall that CompCert x86 assembly language is not realistic enough as it does not prevent a programfrom allocating an infinite number of stack frames. Our goal, as oneof our main applications of our quantitative refinement, is to makethe CompCert x86 assembly language more realistic by having it
model a contiguous finite stack that is preallocated at the beginningof the program. The semantics of our new CompCert x86 assemblyis parameterized by the size sz ` 4 3 of the whole stack (provided,in most cases, by the host operating system). We call this new x86
semantics ASMsz . We design it in such a way that an execution goes3 sz is the stack size actually consumed by the program starting from main,

but we have to account for the return address of the “caller” of mainwrong if the program tries to access more than sz bytes of stack. In
other words, stack overflow becomes possible in ASMsz .
Because the notion of function call is no longer relevant (there isno “control stack”), we lose the ability to extend this semantics withcall and return events. So, rather than quantitative refinement, weare actually interested in whether a CompCert C source program canrun on ASMsz without going wrong because of stack overflow. The
correctness of our Quantitative CompCert compiler is formalized by
the following theorem.
“
˘
Theorem 1. Let sz ` 4 P 4, 232 be the size of the whole target
stack. Consider a CompCert C source program S and assume thefollowing:
1. S does not go wrong in the ordinary setting of unbounded stackspace, that is, Et, failptq P JSK.
2. Quantitative CompCert produces a Mach intermediate target
code I, with the sizes of stack frames4 SF and the subsequent
cost metric M pf q “ SFpf q ` 4.
3. The stack bounds of S inferred at the source level are lower thansz under the Match cost metric M : @B P JSK, WM pBq ď sz .
4. From I, our compiler produces a target assembly code T .
Then, when run in ASMsz , T refines S in the sense of CompCert:@B 1 P JT Ksz , DB P JSK, B 1 “ B. In particular, T cannot go wrong
and thus does not stack overflow.
It is important to first prove that S cannot go wrong in unboundedstack space. Indeed, the correctness of our assembly generation
depends on the fact that the weights of Mach traces are lower thansz . If S were to have a wrong behavior failptq then I might actually
have a behavior t ¨ B whose weight could well exceed sz eventhough WM pfailptqq does not. As each pass is proved independentlyof the others, it is not possible to track the behaviors of I that could
potentially come from wrong behaviors of S.
In the original CompCert x86 assembly language, the notionof stack frame is still kept, so that this language has two pseudoinstructions Pallocframe and Pfreeframe responsible of allocating
and freeing the corresponding memory block, even though thosepseudo-instructions are then turned into real x86 assembly instructions performing pointer arithmetics with the ESP stack pointerregister. This latter transformation cannot be proved correct in
CompCert because pointer arithmetics cannot cross block boundaries in the CompCert memory model. Therefore this transformation
is done in an unverified “pretty-printing” stage, after CompCert has
generated the x86 assembly code of the source program.
Our new assembly semantics overcomes this limitation. Now,
instead of allocating different memory blocks, we preallocate one
single block of size sz ` 4 at the beginning of the program tohold the whole stack, and our assembly generation pass ensuresthat the value of ESP always points within this block. Therefore
the pseudo-instructions are no longer necessary, and the pointerarithmetics needed at function entry and exit can be performed
within our formalized ASMsz assembly language.
As an interesting side effect, accessing function arguments isnow simpler in our assembly language. Indeed, in the x86 calling
convention, a function has to look for its arguments in the stack
frame of its caller. To this purpose, the original CompCert keeps aback pointer to link each stack frame to its parent. Thanks to ourchanges, function arguments can now be provably accessed throughpointer arithmetics with no indirection, so that this back link is nolonger necessary. Because in the original CompCert, stack frames
are independent memory blocks, it was necessary for the callee tohave a pointer to the caller stack frame, called the back link, in its
4 In CompCert Mach, the syntax of a program p includes a finite map SF

such that, for any function f defined in p, the operational semantics of Machallocates a stack frame of SFpf q bytes whenever f is entered.

own stack frame. The callee could then access its arguments by
one indirection through this back link. In our new ASMsz assembly
language, stack frames are no longer independent, so that the callee
can access its arguments directly by pointer arithmetics within thewhole stack block.
3.3 Limitations
Neither the original CompCert nor Quantitative CompCert do
support variable stack-frame size: C features such as variablelength arrays or dynamic stack allocation (alloca special libraryfunctions) are not supported. Thus, the size of the stack frame of
a Mach function can be computed statically, and can be used todefine the cost metric of the program. Moreover, the subsequently
produced assembly code does not need to use push or pop, so any
change to the stack pointer is done only through pointer arithmetics.
Quantitative CompCert currently does not support the following
optional two optimization passes (that are present in the original
CompCert): tail-call recognition and function inlining. We describe
how to deal with these two optimizations in the companion TR [9]and the implementation is underway.

4.

Quantitative Hoare Logic for CompCert Clight

In this section, we describe the novel quantitative program logic
for CompCert Clight. The logic has been formalized and proved
sound using Coq. At some points, we simplify the presented logic
in comparison to the implemented version to discuss general ideas
instead of technical details.
Some particularities of the logic can be better understood withrespect to Clight and the continuation-based small-step semantics
for Clight programs that is used in CompCert.
4.1 CompCert Clight
CompCert Clight is the most abstract intermediate language usedby CompCert. Mainly, it is a subset of C in which loops can only
be exited with a break statement and expressions are free of side
effects. Using Clight instead of C simplifies the definition of ourquantitative program logic and is also in line with the design of
CompCert and the verification of CertiKOS.
Syntax We use Clight expressions in the logic. Our statements’
syntax is a subset of Clight’s to focus on the main ideas of our program logic. For simplicity, loops are infinite unless they are terminated using a break statement. We do not consider function pointers,
goto statements, continue statements, and switch statements (seeSection 4.4).
S, S1 , S2 ::“ skip | x “ E | x “ f pE ˚ q | S1 ; S2 | loop S| if pEq then S1 else S2 | break | return E
Like in C, a program consists of a list of global variable declarations, a list of function declarations, and the identifier of the mainstatement, which is the entry point of the program.
4.2 Operational Semantics
CompCert Clight’s semantics is based on small-step transitions
and continuations. Expressions—which do not have side effects—
are evaluated in a big-step fashion. We use a simplified version of
Clight’s semantics that is sufficient for our subset. It is easy to relate
evaluations in our simplified version to evaluations in the original
semantics and we have implemented a verified compiler from oursimple Clight to Clight with CompCert’s original semantics.
Values and Memory Model A value is either an integer n or amemory address `.
Val ::“ int n | adr `In the Coq development we use CompCert’s memory model. However, the main ideas of the logic can be described with a simpleΓ $ tQs u skip tQu (Q:S KIP )Γ $ tQb u break tQu (Q:B REAK )Γ $ tI s u S tIu

Γpf q“pPf , Qf q

Γ $ tλσ . Qr JEK∆σ qu return E tQu (Q:R ETURN )Γ $ tI u loop S tpI , K, I qu

P “ λpθ, H q.Pf pJEK∆
Q “ λpθ, H q.Qf pJxK∆
pθ,H q , H qpθ,H q , H q(Q:C ALL )Γ $ tP ` M pf qu x “ f pEq tpQ ` M pf q, K, KquΓ $ tP u S1 tpR, Qb , Qr qu Γ $ tRu S2 tQu(Q:S EQ )Γ $ tP u S1 ; S2 tQu

c ě 0 tP u S tQu(Q:F RAME )tP ` cu S tQ ` cu

s

b

r

(Q:L OOP )P ě P1

tP 1 u S tQ1 u Q1 ě Q(Q:C ONSEQ )tP u S tQu

Figure 4. Selected rules of the quantitative program logic.
memory model in which locations are mapped to values and labels.
H : Mem “ Loc Ñ Val Y t‚u
The label ‚ is used to indicate that a location has been freed and canno longer be used.
Evaluating Expressions Expressions are evaluated with respect
to a memory H : Mem and two environmentsθ : VID Ñ Val

and∆ : VID Ñ Loc .

The local environment θ maps local variables to values and theglobal environment ∆ maps global variables to locations. We
assume that always domp∆q X dompθq “ H.
The semantics JEK∆pθ,H q “ v of an expression E under a global
environment ∆, a local environment θ, and a memory H is definedby induction on the structure of E.
Continuations The small-step transition relation for statements isbased on continuations. Continuations handle the local control flow
within a function as well as the logical call stack.
K ::“ Kstop | Kseq S K | Kloop S K | Kcall x f θ K
A continuation K is either the empty continuation Kstop, a sequence
Kseq S K , a loop Kloop S K , or a stack frame Kcall x f θ K .
Evaluating Statements Statements are evaluated under a program
state pθ, H q P State “ pVID Ñ Val q ˆ Mem and a global
environmentpΣ, ∆q : FID Ñ prVIDs ˆ Sq ˆ pVID Ñ Locq
that maps internal functions to their definitions—a list of argument
names and the function body—and global variables to values.
The small-step evaluation rules are given in the companion
TR [9]. They define a transitionpΣ, ∆q $ pS, K, σq Ñtµ|ν|u pS 1 , K 1 , σ 1 q
where µ is a memory event, ν is an I/O event,  denotes no event,S, S 1 are statements, K, K 1 are continuations, and σ, σ 1 P State.
From the small-step transition relation we derive the following
many-step relation in which t is a finite trace. We writepΣ, ∆q $ pS1 , K1 , σ1 q Ñnt pSn`1 , Kn`1 , σn`1 q
if t “ a1 , . . . , an and there exists pSi , Ki , σi q such that for all ipΣ, ∆q $ pSi , Ki , σi q Ñai pSi`1 , Ki`1 , σi`1 q .
For a statement S and a continuation K, we define the weightunder the global environment pΣ, ∆q, the program state σ, andthe metric M as pΣ, ∆q $ Wpσ,M q pS, Kq “ suptVM ptq |1
1
1
DS 1 , K 1 , σ 1 , t, n . pΣ, ∆q $ pS, K, σq Ñnt pS , K , σ qu .
4.3 Quantitative Hoare Logic
In the following we describe a simplified version of the quantitative
Hoare logic that we use in Coq to prove bounds on the weightsof the traces of Clight programs. For a given statement S and acontinuation K, our goal is to derive a bound pΣ, ∆q $ P pσ, M q P

N such that pΣ, ∆q $ P pσ, M q ě pΣ, ∆q $ Wpσ,M q pS, Kq for
all program states σ and resource metrics M . In the remainder ofthis section we assume a fixed global environment pΣ, ∆q.
We generalize classic Hoare logic to express not only classicalboolean-valued assertions but also assertions that talk about the future stack-space usage. Instead of the usual assertions P : State Ñbool of Hoare logic we use assertions
P : State Ñ N Y t8u .
This can be understood as a refinement of boolean assertions where
false is interpreted by 8 and true is refined by N. We write
Assn for State Ñ N Y t8u, and K “ p ÞÑ 8q. In the actual
implementation, assertions have the type State Ñ N Ñ Prop. For
a given σ P State, such an assertion can be seen as a set B Ď N ofvalid bounds. We do this only to use Coq’s support for propositional
reasoning. The presentation here is easier to read.
The continuation-based semantics of Clight requires that we
distinguish pre- and postconditions in the logic to account fordifferent possible ways to exit a block of code. This approachis standard in Hoare logics and followed for instance in Appel’s
separation logic for Clight [3]. Our postconditions
Q “ pQs , Qb , Qr q : Assn ˆ Assn ˆ pVal Ñ Assnq
provide one assertion Qs for the case in which the block is exited byfall through, one assertion Qb if the block is exited by a break, anda function Qr from values to assertions in case the block is exitedby a return. The function Qr takes the return value as argument.
Since we have to deal with (possibly recursive) functions, we
also need a function context
Γ:FIDÑppVal ˆ MemqÑN Y t8uqˆppVal ˆ MemqÑNYt8uq
that maps function names to their specifications, that is, pre- andpostconditions. The precondition depends on the value that is passed
to the function by the caller and the memory. The postcondition
depends on the return value and the memory. We assume that a function has only one argument in this article. In the Coq implementation,an arbitrary number of function arguments is allowed.
In summary, a quantitative Hoare triple has the form Γ $tP u S tQu where Γ is a function context, P : Assn is a precondition, Q : Assn ˆ Assn ˆ pVal Ñ Assnq is a postcondition, andS is a statement.
Intuitively, an assertion can be seen as a potential function thatmaps a program state to a non-negative potential. The potentialof the precondition P must be sufficient to cover the cost of theexecution of the statement S and the potential Q after the executionof S (as in amortized resource analysis [19]).
Rules Figure 4 shows selected rules of the quantitative logic. We
lift the operations ` and ě pointwise to assertions P, Q : Assn. A
constant c P N Y t8u is sometimes used as the constant assertion
ÞÑ c. We fix an event metric M and a global environment pΣ, ∆q.
In the Q:S KIP rule, we do not have to account for any stackconsumption. As a result, the precondition can be any (potential)Γpf q “ pλpv, H q . 0, λpv, H q . 0q
Γpgq “ pλpv, H q . 0, λpv, H q . 0q
(Q:C ALL )(Q:C ALL )Γ $ tpmf u fpq tpmf , K, KquΓ $ tpmg u gpq tpmg , K, Kqu(Q:F RAME )(Q:F RAME )Γ $ tpmf ` Xf u fpq tpmf ` Xf , K, KquΓ $ tpmg ` Xg u gpq tpmg ` Xg , K, Kqu(E Q )(E Q )
Γ $ tmaxpmf , mg qu fpq tQu
Γ $ tmaxpmf , mg qu gpq tQu(Q:S EQ )Γ $ tmaxpmf , mg qu fpq; gpq tQu
where

M pcallpf qq “ mfM pcallpgqq “ mgQ “ pmaxpmf , mg q, K, Kq

Xθ “ maxpmf , mg q ´ mθ for θ P tf, gu

Figure 5. An example derivation of a stack-space bound in the quantitative logic.
function. After the execution, the skip part of the postcondition must
be valid on the same (unchanged) program state. So we have to
make sure that we do not end up with more potential and simply use
the precondition as the skip part of the postcondition. The break andreturn parts of the postcondition are not reachable and can therefore
be arbitrary. The rules Q:B REAK and Q:R ETURN are similar.
In the Q:S EQ rule we have to account for early exits in statements.
For instance, if S1 contains a break statement then S2 will never be
executed so we must ensure in the break part of S1 ’s postcondition
that the break part of S1 ; S2 holds. For the same reason, the return
part of S1 ’s postcondition is special.
The Q:L OOP rule uses the same principles as the Q:S EQ rule
to tweak the final postcondition. In the case of Q:L OOP, we simply
ensure that the break part of the inner statement becomes the skip
part of the overall statement. We use K as the break part of theloop S statement since its operational semantics prevent it fromterminating differently than with a skip or a return.
The Q:C ALL rule accounts for the actual stack-space usage ofprograms. It enforces that enough stack space is available to call thefunction f by adding M pf q to the pre- and postcondition. The preand postconditions are taken from the function context Γ.
There are two weakening rules in the quantitative Hoare logic.
The framing rule Q:F RAME weakens a statement by stating that if
S needs P bytes to run and leaves Q bytes free at its end, then it canvery well run with P ` c bytes and return Q ` c bytes. It is very
handy to prove tight bounds using the max function as demonstrated
in Figure 5. The consequence Q:C ONSEQ rule is directly imported
from classical Hoare logics except that instead of using the logicalimplication ñ we use the quantitative ě.
Auxiliary State The main difference between the implemented
logic and the logic described here is that the latter does not havean auxiliary state. Auxiliary state is a classic extension of Hoare
logic (see for example [30]). The auxiliary state is used to share
information between the pre- and postcondition of a triple. In a logic
without auxiliary state (or similar techniques) it is not possible torelate program states before and after a statement. For example, you
cannot specify that the function int twice () t i = i+i;udoubles the value of the variable i. With an auxiliary variable
Z it is possible specify this fact in Hoare logic using the triple
ti “ Zu twicepq ti “ 2 ¨ Zu.
One technical challenge with this auxiliary state is that sometriples, for example ti “ Zu c ti “ Zu and ti “ Z ´ 1u c ti “Z ´ 1u need to be proved equivalent by the logic to handle recursive
calls. This problem is usually solved by introducing a more complex
consequence rule, which our implemented system features. The
typical use case is when we apply the rule Q:C ALL to a recursive
call. In this case, the Hoare triple for the function call is proved byan assumption from the derivation context with a slightly different
auxiliary state. In the example derivation in Figure 6 this different
state is Z ´ 1. Adapting the derivation hypothesis to prove therecursive call is enabled in our logic by an extended consequence
rule that we proved sound in the quantitative setting.
Stack Framing Another minor difference is in the function application rule where we only present the rule for function calls with atZ “ log2 phσ ´lσ q ñ Mb ¨ Zu
bsearch(x,l,h) {if (h-l <= 1) return l;tpZą0 ^ Z “ log2 phσ ´lσ qq ñ Mb ¨ Zu
m = (h+l)/2;σtpZą0 ^ Z “ log2 phσ ´lσ q ^ mσ “ hσ `lq ñ Mb ¨ Zu
2if (a[m]>x) h=m else l=m;trZ´1 “ log2 phσ ´lσ q ñ Mb ¨ pZ´1qs ` Mb u
return bsearch(x,l,h);trMb ¨ pZ´1qs ` Mb u}tMb ¨ Zu

Figure 6. Derivation with auxiliary state for the bsearch function.

single argument and without framing of stack assertions. The latteris necessary to carry over information on the local environment fromthe precondition to the postcondition of the function call.
Soundness The soundness of our quantitative logic can be simply
expressed by the following theorem.
Theorem 2. For a fixed global environment pΣ, ∆q, a derivationin our quantitative logic for a statement S implies a bound on theweight of S, that is,¨ $ tP u S tQu ùñ @σ, M . P pσ, M q ě Wpσ,M q pS, Kstopq.
Naturally, we have to prove a stronger statement that takes postconditions and continuations into account to justify the soundnessof the rules of the logic. This is not unlike as in program logics for
low-level code [22] and Hoare-style logics for CompCert Clight [3].
Furthermore, we have to assume that we have a non-empty function
context Γ; and finally, we have to step-index the correctness statement in order to prove its soundness by induction. The details canbe found in the TR [9] and in the Coq development. Of course we
prove in Coq that the intuitive validity, as formulated in Theorem 2
is a consequence of our stronger formulation of validity.
Example Figure 5 contains an example derivation for the statement fpq; gpq in our logic. We assume that we have already verified
that the function bodies of f and g do not allocate stack space, thatis, Γpgq “ Γpf q “ pλpv, H q . 0, λpv, H q . 0q.
Our goal is to derive a quantitative Hoare triple that expresses
that maxpmf , mg q, the maximum of the stack frame sizes of f
and g, is a bound on the stack usage; and that after the execution
maxpmf , mg q stack space is available. Since the effect of break
and return statements cannot leak outside of a function body, thecorresponding postconditions can be arbitrary and we simply use K.
To derive our goal, we first have to apply the rule Q:S EQ for
sequential composition. In the derivation of the function call fpq,
we first reorder the precondition to get it in a form in which we canapply the rule Q:F RAME to eliminate the max operator. We thenhave a triple that is amenable to an application of the rule Q:C ALL
that uses the specification of the body of f in Γ.

4.4 Limitations
In our program logic described in this section, we do not consider
function pointers, goto statements, continue statements, and switch
statements, even though our Quantitative CompCert compiler still
supports all of these. It would be possible to add these features toour logic by building on the ideas of advanced program logics like
XCAP [29].

5.

Automatic Stack Analyzer

In larger C programs a manual, interactive verification with aprogram logic is too tedious and time-consuming to be practical.
Therefore we have developed an automatic stack analysis tool that
operates at the Clight level to enable the analysis of real systemcode. We view this automatic tool mainly as a proof of concept that
demonstrates the value of the logic for formal verification of static
analysis tools. In the future, we will extend our automatic analyzer
with advanced techniques like amortized resource analysis [5, 21].
This is however beyond the scope of this article.
The basic idea of our automatic stack analyzer is to computea call graph from the Clight code and to derive a stack boundfor each function in topological order. In Coq, the derivation of afunction bound is implemented by a recursive function auto boundon the abstract syntax tree (AST) of a Clight program. The function
auto bound does not only compute a stack bound but also aderivation in our quantitative program logic. This verifies thecorrectness of the generated bound and enables the compositionof stack bounds that have been derived interactively or with otherstatic analysis tools. In addition to the AST, auto bound takes acontext of known function bounds together with their derivations in
the logic as an argument.
Given our verified quantitative logic, the implementation of
auto bound is straightforward. For trivial commands like assignments or skip, auto bound simply generates the bound 0
and a derivation like t0u skip tp0, 0, 0qu. For a sequential composition S1 ; S2 we inductively apply auto bound to S1 and S2 ,and derive the bounds tBi u Si tpBis , Bib , Bir qu for i“1, 2. We
then return the precondition maxtB1 , B2 u and the postcondition
pmaxtB1s , B2s u, maxtB1b , B2b u, maxtB1s , B2s uq for the command
S1 ; S2 . The derivation of this bound is similar to the example derivation that is sketched in Figure 5. The computation of the boundfor the conditional works similar. For loops we can use the boundderived for the loop body to obtain a bound for the loop. In thederivation we just apply the rule Q:L OOP. Function calls are handled with the context of known function bounds (recursion is notallowed here) and the rule Q:C ALL.
We envision, that the quantitative logic can be a useful backend toverify more sophisticated static analyses. For our simple, automatic
stack analyzer the logic was already very convenient and enabled us
to verify the analyzer almost without additional effort.
We have combined our automatic stack analyzer with our Quantitative CompCert compiler. The result is a verified C compiler thattranslates a program without function pointers and recursive calls
to x86 assembly and automatically derives a stack bound for eachfunction in the program including mainpq. The soundness theorem
we have proved states the following. If a given program is memorysafe and the verified compiler successfully produces an assembly
program A then A refines the source program and runs safely onan x86 machine with the stack size that has been computed by theautomatic stack analysis for mainpq (see Point 3 of Theorem 1).

6.

Experimental Evaluation

To validate the practicality of our framework for stack-boundverification, we have performed an experimental evaluation withmore than 3000 lines of C code from different sources including

File Name /Line Count

Function Namemibench{net{dijkstra.cenqueuedequeuedijkstrabitcount
bitstring
BF encrypt
BF options
BF ecb encrypt
MD5Init
MD5Update
MD5Final
MD5Transform
IsPowerOfTwo
NumberOfBitsNeeded
ReverseBits
fft float
pallocpfree
mem init
pmap init
pt freept initpt init kern
pt insert
pt readpt resv
enqueuedequeue
kctxt newsched init
tdqueue init
thread init
thread spawn
main

40 bytes
40 bytes
88 bytes
16 bytes
32 bytes
40 bytes
8 bytes
80 bytes
16 bytes
168 bytes
168 bytes
128 bytes
16 bytes
24 bytes
24 bytes
160 bytes
48 bytes
40 bytes
72 bytes
176 bytes
80 bytes
152 bytes
136 bytes
80 bytes
56 bytes
120 bytes
48 bytes
48 bytes
72 bytes
232 bytes
208 bytes
192 bytes
96 bytes
56 bytes

advanceenergyoffset momentum
setup bodies
main

80 bytes
56 bytes
24 bytes
16 bytes
112 bytes(174 LOC)

mibench{auto{bitcount.c(110 LOC)

mibench{sec{blowfish.c(233 LOC)

mibench{sec{pgp{md5.c(335 LOC)

mibench{tele{fft.c(195 LOC)

certikos{vmm.c(608 LOC)

certikos{proc.c(819 LOC)

compcert{mandelbrot.c

Verified
Stack Bound(92 LOC)

compcert{nbody.c(174 LOC)

Table 1. Automatically verified stack bounds for C functions.

hand written code, programs from the CompCert test suite, programsfrom the MiBench [17] embedded software benchmark suite, andmodules from the simplified development version of the CertiKOS
operating system kernel which is currently being verified.
Tables 1 and 2 show a representative compilation of the experiments. Table 1 contains bounds that were automatically derived
with the stack analyzer. Table 2 contains 8 bounds that were interactively derived using the quantitative logic with occasional supportof the automation. The size of the analyzed example files varies
from 8 lines of code (fib.c) to 819 lines of code (proc.c). In general,
the automatic stack-bound analysis runs very efficiently and needs
less than a second for every example file on (one core of) a Linux
workstation with 32G of RAM and a x86 processor with 16 cores at
3.10Ghz.
In Table 1, the first column shows the file name of the examples
together with the number of lines, the second column contains thename of selected functions from that file, and the third column contains the verified bound. The interactively-derived bounds in Table 2
are presented as symbolic expressions parametric in the functions’Function Name
recidpqbsearchpx, lo, hiq
fibpnqqsortpa, lo, hiq
filter pospa, sz, lo, hiq
sumpa, lo, hiq
fact sqpnq
filter findpa, sz, lo, hiq

Verified Stack Bound
8a bytes
40p1 ` log2 phi ´ loqq bytes
24n bytes
48phi ´ loq bytes
48phi ´ loq bytes
32phi ´ loq bytes
40 ` 24n2 bytes
128 ` 48phi ´ loq ` 40 log2 pBLq bytes

Table 2. Manually verified stack bounds for C functions.

600

500

400

300

200

100

0

arguments. These symbolic expressions are slight simplifications of
the real pre- and postconditions of the functions that we proved in
Coq. The actual Hoare triples proved in Coq carry a logical meaning
which does, for instance, require that the qsort function be called
on a valid sub array. The file sizes of the manual verified examples
range from 8 to 52 lines of code.
Our main application of the automatic stack-analyzer is theCertiKOS operating system kernel [15]. Currently, the stack in
CertiKOS is preallocated and proving the absence of stack-overflow
is essential in the verification of the reliability of the system. Since
CertiKOS does not use recursion, we can use the automatic analysis
to derive precise stack bounds. Using our Quantitative CompCert
compiler, we were, for instance, able to compile and compute bounds
for the virtual memory management module (certikos{vmm.c) andthe process management module (certikos{proc.c). Because of
the large number of functions in CertiKOS, only a sample of theanalyzed functions is displayed in Table 1.
Testing the quantitative Hoare logic and the compiler on
CompCert test suite was a natural choice since our compiler builds
on CompCert’s architecture. This also allowed us to make surethat we did not introduce any regression with respect to the original CompCert compiler. To stress the expressivity of the logic wefocused on test programs with recursive functions. The functions
fib and qsort in Table 2 are for instance from the CompCert test
suite. Files with automatically derived bounds for non-recursivefunctions from the CompCert test suite include mandelbrot.c which
computes an approximation of the Mandelbrot set and nbody.cwhich computes an n-body simulation of a part of our solar system.
We also made sure that our technique can handle safety criticalembedded software. The MiBench [17] benchmark that we used
for this purpose is free, publicly available, and representative for
embedded software. The use of recursion in MiBench programs isrelatively rare, which makes them a great target for our automatic
stack analyzer. The analyzed examples we present in Table 1
include for instance Dijkstra’s single-source shortest-path algorithm(dijkstra.c), and the cryptographic algorithms Blowfish (blowfish.c)and MD5 (md5.c).
Finally, Table 2 contains some recursive functions that demonstrate the expressivity of our quantitative logic. The function bsearchis, for example, a recursive binary search with logarithmic recursion
depth. The function fib computes the Fibonacci sequence using an
exponential algorithm and the function qsort implements a recursive
version of the quicksort algorithm. The verification of the function
fact sq shows the modularity of the logic: We first verify a linear
bound for the factorial function and then use this bound to verify
fact sqpnq, which contains the call factpn2 q. The function filter pos
takes an array and computes a new array that contains all positiveelements of the input array. Similarly, filter find uses the binary
search bsearch to filter out all elements of an input array that arecontained in another array of size BL. The modularity of the logic
enables us to reuse the logarithmic bound that we already derived
for bsearch in the proof. The verification of some functions is stillmeasured stack consumption
40(1 + log_2(x))
0

500

1000

1500

2000

2500

3000

3500

4000

25000020000015000010000050000

0measured stack consumption
40 + 24 x^2
0

10

20

30

40

50

60

70

80

90

100

Figure 7. Experimental evaluation of the accuracy of hand-derived
stack bounds. The plots compare the derived bounds (blue lines)
for the functions bsearch (at the top) and fact sq (at the bottom)
with the measured stack usage of the execution of the respectivefunction for different inputs (red crosses). The x-axis shows either
the value of an integer argument (fact sq) or the length of an input
array (bsearch). The y-axis shows the stack usage in bytes.
underway. The bounds for the functions recid, bsearch, fib, andqsort are already completely verified.
Our experiments show that the automatic stack analyzer works
effectively for our main application, the CertiKOS OS kernel. The
reason is that we designed the quantitative logic to include exactly
the subset of Clight that is needed for CertiKOS. It turned out that
this subset is also sufficient for many examples in the CompCert
test suite and the MiBench embedded software benchmarks. If a
program is not interactively analyzable in our logic then this is due
to unsupported language constructs such as switch statements andfunction pointers. Many of these language features could easily be
supported by relatively small additions to the logic. An exception tothis are function pointers which would require more work, following
for example XCAP [29].
We have evaluated the accuracy of the verified bounds bycomparing them with the actual stack-space consumption of thecompiled C programs. Our experiments show that our framework
is expressive enough to derive very tight bounds for recursive andnon-recursive programs. All manually and automatically derived
bounds over-approximate the actual stack-space consumption by
exactly 4 bytes. Figure 7 shows the results of two representative
experiments with hand-derived bounds for recursive programs. The
bound derived in the logic is plotted together with the actual stackconsumption of C programs measured on different inputs.
Measuring the stack consumption of C programs on modern
computers is not as trivial as we originally thought. The measurement is complicated by some security mechanisms and unrestricted
manipulation of the stack pointer by the compiler. To this end, we

designed a small C program that uses the linux system call ptrace.
Using the this system call our tool forks the monitored process as achild then executes it step by step while keeping track of its stackconsumption.
The reason for the 4-byte looseness of the bounds is that stack
frames always reserve four bytes for a potential function call: The
return address needs to be pushed by a call instruction in the callee.
Obviously, the last function in the function call chain does not callany other function. So these four bytes remain unused.

7.

Related Work

We now discuss research that is related to our contributions in verified compilation, program logics, and automatic resource analysis.
Verified Compilation Soundness proofs of compilers have been
extensively studied and we focus on formally verified proofs here.
Klein and Nipkow [24] developed a verified compiler from an
object-oriented, Java-like language to JVM byte code. Chlipala [11]describes a verified compiler from the simply-typed lambda calculus
to an idealized assembly language. In contrast to our work, theaforementioned works do not model nor preserve quantitative
properties such as stack usage.
Our verified Quantitative CompCert compiler is an extension of
the CompCert C Compiler [26, 27]. Despite being formally verified,important quantitative properties such as memory and time usageof programs compiled with CompCert have still to be verified at
the assembly level [6]. Admittedly, there exists a clever annotation
mechanism [6] in CompCert that allows to transport assertions
on program states from the source level to the target machinecode. However, these assertions can only contain statements about
memory states but not bounds on the number of loop iterations andor recursion depth of functions. The novelty of our Quantitative
CompCert extension to CompCert is that it enables us to reason
about quantitative properties of event traces during compilation.
Another novelty is that we model the assembly level semantics
more realistically by using a finite stack. In particular, we do
not have to use pseudo instructions anymore. This is similar to
CompCertTSO [32]. However, we use event traces to get guarantees
on the size of the stack that is needed to ensure refinement. On theother hand, it is always possible that the compiled code runs out ofstack space in CompCertTSO.
In the context of the Hume language [18], Jost et al. [23]developed a quantitative semantics for a functional language andrelated it to memory and time consumption of the compiled codefor the Renesas M32C/85U embedded micro-controller architecture.
In contrast to our work, the relation of the compiled code withfunctional code is not formally proved.
Program Logics In the development of our quantitative Hoare
logic we have drawn inspiration from mechanically verified Hoare
logics. Nipkow’s [30] description of his implementations of Hoare
logics in Isabelle/HOL has been helpful to understand the interactionof auxiliary variables with the consequence rule. The consequence
rule we use in our Coq implementation is a quantitative version ofa consequence rule that has been attributed to Martin Hofmann by
Nipkow [30]. Appel’s separation logic for CompCert Clight [3] hasbeen a blueprint for the structure of the quantitative logic. Since we
do not deal with memory safety, our logic is much simpler and it
would be possible to integrate it with Appel’s logic. The continuationpassing style that we use in the quantitative logic is not only usedby Appel [3] but also in Hoare logics for low-level code [22, 29].
There exist quantitative logics that are integrated into separation
logic [5, 20] and they are closely related to our quantitative logic.
However, the purpose of these logics is slightly different since they
focus on the verification of bounds that depend on the shape ofheap data structures. Moreover, they are only defined for idealized

languages and do not provide any guarantees for compiled code.
Also closely related to our logic is a VDM-style logic for reasoning
about resource usage of JVM byte code by Aspinall et al. [4]. Theirlogic is more general and applies to different quantitative resources
while we focus on stack usage. However, it is unclear how realistic
the presented resource metrics are. On the other hand, our logic
applies to system code written in C, is verified with respect to
CompCert Clight, and derives bounds for x86 assembly.
Resource Analysis There exists a large body of research on
statically deriving stack bounds on low-level code [8, 10, 31] aswell as commercial tools such as the Bound-T Time and Stack
Analyser and Absint’s StackAnalyzer [14]. We are however notaware of any formally verified techniques. For high-level languages
there exists a large number of systems for statically inferring orchecking quantitative requirements such as stack usage [1, 12, 19,23]. However, they are not formally verified and do not apply tosystem code that is written in C. For C programs, there exist methods
to automatically derive loop bounds [16, 36] but the proposed
methods are not verified and it is unclear if they can be used forcomputing stack bounds.
We are only aware of two verified quantitative analysis systems.
Albert et al. [2] rely on the KeY tool to automatically verify
previously inferred loop invariants, size relations, and ranking
functions for Java Card programs. However, they do not have aformal cost semantics and do not verify actual stack bounds. Blazyet al. [7] have verified a loop bound analysis for CompCert’s RTL
intermediate language. It is however unclear how the presented
technique can be used to verify stack bounds or to formally translatebounds to a lower-level during compilation.

8.

Conclusion

Embedded software has always been a target of verified compilers.
As a result, aiding verification of quantitative properties remains amajor goal for verified compilation. In one of the earliest articles[26] on CompCert, Leroy stated:“[...] it is hopeless to prove a stack memory bound on thesource program and expect this resource certification to carryout to compiled code: stack consumption, like execution time,
is a program property that is not preserved by compilation.”
Ironically, Leroy’s groundbreaking work on CompCert has been themain inspiration in our development of a framework that enables
exactly such a resource certification of stack-consumption bounds
for compiled x86 assembly code at the C level.
We have developed Quantitative CompCert, a realistic, verified
C compiler which shows how verified compilation enables theverification of quantitative properties of compiled programs at thesource level. We have implemented and formally verified a novel
quantitative Hoare logic for CompCert Clight which is an ideal
backend for static analysis tools. This is demonstrated through theimplementation of a verified, automatic stack-analysis tool thatcomputes derivations in the quantitative logic. Finally, we haveshown through experiments that our framework can be applied toderive precise stack bounds for typical system code.
Our work opens the door for the verification of powerful static
analysis tools for quantitative properties that operate on the C
level rather than on the machine code. There are multiple future
research directions that we plan to explore on the basis of the present
development. For one thing, we want to use our quantitative Hoare
logic to verify more powerful analysis tools that can automaticallyderive stack-space bounds for recursive functions. For anotherthing, we plan to generalize the developed concepts to apply ourtechnique to other resources such as heap-memory and clock-cycle
consumption.

Acknowledgments
We thank Lennart Beringer, Francesco Logozzo, the anonymous
reviewers of PLDI’14, and the PLDI’14 Artifact Evaluation Committee for helpful comments and suggestions that improved thisarticle and the implemented tools.
This research is based on work supported in part by NSF grants
1319671 and 1065451, and DARPA grants FA8750-10-2-0254
and FA8750-12-2-0293. Any opinions, findings, and conclusions
contained in this document are those of the authors and do not reflect
the views of these agencies.

References[1] E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, and G. Puebla.
Cost Analysis of Concurrent OO Programs. In Prog. Langs. and
Systems - 9th Asian Symposium (APLAS’11), pages 238–254, 2011.
[2] E. Albert, R. Bubel, S. Genaim, R. Hähnle, and G. Román-Dı́ez.
Verified Resource Guarantees for Heap Manipulating Programs. In
Fundamental Approaches to Soft. Eng. - 15th Int. Conf. (FASE’12),
pages 130–145, 2012.
[3] A. W. Appel et al. Program Logics for Certified Compilers. Cambridge
University Press, 2013.
[4] D. Aspinall, L. Beringer, M. Hofmann, H.-W. Loidl, and
A. Momigliano. A Program Logic for Resources. Theor. Comput.
Sci., 389(3):411–445, 2007.
[5] R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th
Euro. Symp. on Prog. (ESOP’10), pages 85–103, 2010.
[6] R. Bedin França, S. Blazy, D. Favre-Felix, X. Leroy, M. Pantel, and
J. Souyris. Formally Verified Optimizing Compilation in ACG-based
Flight Control Software. In Embedded Real Time Software and Systems(ERTS 2012), 2012.
[7] S. Blazy, A. Maroneze, and D. Pichardie. Formal Verification of Loop
Bound Estimation for WCET Analysis. In Verified Software: Theories,
Tools, Experiments - 5th Int. Conf. (VSTTE’13), 2013. To appear.
[8] D. Brylow, N. Damgaard, and J. Palsberg. Static Checking of InterruptDriven Software. In 23rd Int. Conf. on Soft. Engineering (ICSE’01),
pages 47–56, 2001.
[9] Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao. Endto-End Verification of Stack-Space Bounds for C Programs. Technical
Report YALEU/DCS/TR-1487, Yale University, March 2014.
[10] W.-N. Chin, H. H. Nguyen, C. Popeea, and S. Qin. Analysing Memory
Resource Bounds for Low-Level Programs. In 7th Int Symp. on Memory
Management (ISMM’08), pages 151–160, 2008.
[11] A. Chlipala. A Certified Type-Preserving Compiler from Lambda
Calculus to Assembly Language. In 28th Conf. on Prog. Lang. Design
and Impl. (PLDI’07), pages 54–65, 2007.
[12] K. Crary and S. Weirich. Resource Bound Certification. In 27th ACM
Symp. on Principles of Prog. Langs. (POPL’00), pages 184–198, 2000.
[13] Express Logic, Inc. Helping you avoid stack overflow crashes! White
Paper, 2014. URL http://rtos.com/images/uploads/Stack_Analysis_White_paper.1_.pdf.
[14] C. Ferdinand, R. Heckmann, and B. Franzen. Static Memory andTiming Analysis of Embedded Systems Code. In 3rd Europ. Symp. on
Verification and Validation of Software Systems (VVSS’07), 2007.
[15] L. Gu, A. Vaynberg, B. Ford, Z. Shao, and D. Costanzo. CertiKOS: A
Certified Kernel for Secure Cloud Computing. In Asia Pacific Workshop
on Systems (APSys’11), 2011.
[16] S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: Precise andEfficient Static Estimation of Program Computational Complexity. In

36th ACM Symp. on Principles of Prog. Langs. (POPL’09), pages
127–139, 2009.
[17] M. R. Guthaus, J. S. Ringenberg, D. Ernst, T. M. Austin, T. Mudge,
and R. B. Brown. MiBench: A Free, Commercially Representative
Embedded Benchmark Suite. In IEEE International Workshop on
Workload Characterization (WWC’01), pages 3–14, 2001.
[18] K. Hammond and G. Michaelson. Hume: A Domain-Specific Language for Real-Time Embedded Systems. In Generative Progr. andComponent Eng., 2nd Int. Conf. (GPCE’03), pages 37–56, 2003.
[19] J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized
Resource Analysis. ACM Trans. Program. Lang. Syst., 2012.
[20] J. Hoffmann, M. Marmar, and Z. Shao. Quantitative Reasoning for
Proving Lock-Freedom. In 28th ACM/IEEE Symposium on Logic in
Computer Science (LICS’13), 2013.
[21] M. Hofmann and S. Jost. Static Prediction of Heap Space Usage forFirst-Order Functional Programs. In 30th ACM Symp. on Principles ofProg. Langs. (POPL’03), pages 185–197, 2003.
[22] J. B. Jensen, N. Benton, and A. Kennedy. High-Level Separation Logic
for Low-Level Code. In 40th ACM Symp. on Principles of Prog. Langs.
(POPL’13), pages 301–314, 2013.
[23] S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. Carbon
Credits for Resource-Bounded Computations using Amortised Analysis.
In 16th Symp. on Form. Meth. (FM’09), pages 354–369, 2009.
[24] G. Klein and T. Nipkow. A Machine-Checked Model for a Java-Like
Language, Virtual Machine, and Compiler. ACM Trans. Program. Lang.
Syst., 28(4):619–695, 2006.
[25] G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin,
D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell,
H. Tuch, and S. Winwood. seL4: Formal Verification of an OperatingSystem Kernel. Commun. ACM, 53(6):107–115, 2010.
[26] X. Leroy. Formal Certification of a Compiler Back-End, or: Programming a Compiler with a Proof Assistant. In 33rd Symposium on Principles of Prog. Langs. (POPL’06), pages 42–54, 2006.
[27] X. Leroy. Formal Verification of a Realistic Compiler. Communicationsof the ACM, 52(7):107–115, 2009.
[28] Y. Moy, E. Ledinot, H. Delseny, V. Wiels, and B. Monate. Testing or
Formal Verification: DO-178C Alternatives and Industrial Experience.
IEEE Software, 30(3):50–57, 2013. ISSN 0740-7459.
[29] Z. Ni and Z. Shao. Certified Assembly Programming with Embedded
Code Pointers. In 33th ACM Symp. on Principles of Prog. Langs.
(POPL’06), pages 320–333, 2006.
[30] T. Nipkow. Hoare Logics in Isabelle/HOL. In Proof and SystemReliability, volume 62 of NATO Science Series, pages 341–367.
Springer, 2002.
[31] J. Regehr, A. Reid, and K. Webb. Eliminating Stack Overflow by
Abstract Interpretation. ACM Trans. Embed. Comput. Syst., 4(4):751–
778, 2005.
[32] J. Sevcı́k, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell.
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM, 60(3), 2013.
[33] Z. Shao. Certified software. Commun. ACM, 53(12):56–66, 2010.
[34] R. Wilhelm et al. The Worst-Case Execution-Time Problem —Overview of Methods and Survey of Tools. ACM Trans. Embedded
Comput. Syst., 7(3), 2008.
[35] X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and Understanding
Bugs in C Compilers. In 32nd Conf. on Prog. Lang. Design and Impl.
(PLDI’11), pages 283–294, 2011.
[36] F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. Bound Analysis ofImperative Programs with the Size-change Abstraction. In 18th Int.
Static Analysis Symposium (SAS’11), 2011.