A Formal Model of Checked C (Extended Version)
A Formal Model of Checked C

Liyi Li, Yiyun Liu^†, Deena Postol, Leonidas
Lampropoulos, David Van Horn, and Michael Hicks

University of Maryland ^†University of Pennsylvania

We present a formal model of Checked C, a dialect of C
that aims to enforce spatial memory safety. Our model pays particular
attention to the semantics of dynamically sized, potentially null-terminated

We formalize this model in Coq, and prove that any spatial memory
safety errors can be blamed on portions of the program
labeled unchecked; this is a Checked C feature that supports
incremental porting and backward compatibility.

While our model's operational semantics uses annotated
(“fat”) pointers to enforce spatial
safety, we show that such annotations can be safely erased.
Using PLT Redex we formalize an executable
version of our model and a compilation procedure to an untyped C-like
language, as well as use randomized testing to
validate that generated code faithfully simulates the original.

Finally, we develop a custom random generator
for well-typed and almost-well-typed terms in our Redex model, and
use it to search for
inconsistencies between our model and the Clang Checked C
implementation. We find these steps to be a useful way to co-develop a language
(Checked C is still in development) and a core model of it.

This is an extended version of a paper that
appears at the 2022 Computer Security Foundations Symposium.

§ INTRODUCTION

The C programming language remains extremely popular despite the
emergence of new, modern languages. Unfortunately, C programs lack
spatial memory safety, which makes them susceptible to a host
of devastating vulnerabilities, including buffer overflows and
out-of-bounds reads/writes. Despite their long history, buffer
overflows and other spatial safety violations are among the most
prevalent and dangerous vulnerabilities on the Internet today [Zeng et al., 2013].

Several industrial and research efforts—including CCured [Necula et al., 2005],
Softbound [Nagarakatte et al., 2009], and ASAN [Serebryany et al., 2012]—have
explored means to compile C programs
to automatically enforce spatial safety. These
approaches all impose performance overheads deemed too high for
deployment use. Recently, Elliott et al., 2018 introduced , an
open-source extension to C with new types and
annotations whose use can ensure a program’s spatial safety.
Importantly, supports development that is
incremental and compositional. Code regions (e.g.,
functions or whole files) designated as checked enforce
spatial safety in a manner preserved by composition with
other checked regions. But not all regions must be checked: Checked
C's annotated checked pointers are binary-compatible with legacy pointers, and
may coexist in the same code, which permits a deliberate (and
semi-automated) refactoring process. Parts of the FreeBSD kernel have
been successfully ported to  [Duan et al., 2020], and overall, performance
overhead seems low enough for practical deployment.

While promises to enforce spatial safety, we might wonder
whether its design and implementation deliver on this promise, or even
what “spatial safety” means when a program contains both checked and
unchecked code. In prior work, Ruef et al., 2019 developed a core
formalization of and with it proved a soundness theorem for
checked code: any stuck (i.e., ill-defined)
state reached by a well-typed program amounts to a spatial safety
violation; such a state can always be attributed to, i.e.,
blamed on, the execution of code that is not in a checked
region. While their work is a good start,
it fails to model important aspects of 's functionality,
particularly those involving pointers to arrays. In this paper, we
cover this gap, making three main contributions.

Dynamically bounded and null-terminated arrays

Our first contribution is a core formalism called , which extends
Ruef et al., 2019 with several new features, most notably
dynamically bounded arrays (Section <ref>).

Dynamically bounded arrays are those whose size is
known only at run time, as designated by in-scope variables using
dependent types. A pointer's accessible memory is bounded both above
and below, to admit arbitrary pointer arithmetic.

also models
null-terminated arrays, a kind of dynamically bounded array
whose upper bound
defines the array's minimum length—additional space is available
up to a null terminator. For example, the type
nt_array_ptr<char> p:count(n) says that
p has length at least n (excluding the
null terminator), but further capacity is present if
|p[n]| is not null. (and ) supports flow-sensitive
bounds widening: statements of the form |if (*p) | $s$,
where p's type is nt_array_ptr<T> count(0),
typecheck statement $s$ under the assumption that p has
type nt_array_ptr<T> count(1),
i.e., one more than it was,
since the character at the current-known length is
non-null. Similarly, the call |n = strlen(p)| will widen
|p|'s bounds to |n|. Subtyping permits treating
null-terminated arrays as normal arrays of the same size (which
does not include, and thereby protects, the null
See Sec. <ref> for a careful comparison of
Ruef et al., 2019 and .

We prove, in Coq, a blame theorem for .  As far as we are aware,
ours is the first formalized type system and proof of soundness for
pointers to null-terminated arrays with expandable bounds.

Sound compilation of checked pointers Our second
contribution is a formalization of bounds-check insertion for array
accesses (Section <ref>). Our operational semantics
annotates each pointer with metadata that describes its bounds, and
the assignment and dereference rules have premises to confirm the
access is in bounds. An obvious compilation scheme (taken by
Cyclone [Jim et al., 2002, Grossman et al., 2002], CCured [Necula et al., 2005], and
earlier works) would be to translate annotated pointers to multi-word
objects: one word for the pointer, and 1-2 words to describe its lower
and upper bounds. Inserted checks reference these bounds. While
convenient, such “fat” pointers are expensive, and break backward
binary compatibility with legacy pointers.

To show that pointer annotations can be safely
erased, and thus fat pointers are not needed, we formalize a
translation of to , which is an
untyped version of that drops metadata annotations, and
lacks bounds/null checks in the semantics rules. Instead,
the compilation process inserts null/bounds checks explicitly, leveraging
compile-time type information. While we do not definitively prove
it, we provide strong evidence that compilation is correct. We use PLT
Redex [Felleisen et al., 2009] to mechanize (a generalization of) ,
, and compilation between the two, and we use randomized testing
to validate that the compiled program simulates the
original. In addition to demonstrating the technical point that metadata
annotations in the formalism do not necessitate fat pointers,
compilation also sheds light on the actual Checked C compilation

As far as we are aware, is the first formalism to cleanly
separate bounds-checking compilation from the core semantics; prior
work [Zhou et al., 2006, Condit et al., 2007] merged the two, conflating
meaning with mechanism. In carrying out the
formalization, we discovered that our compilation approach for
null-terminated array pointers is more expressive than that proposed
in the Checked C specification [Tarditi, 2021]
(Section <ref>); we would not have discovered this
improvement had we not separated checks from semantics.

Model-based randomized testing Our third and final
contribution is a strategy and implementation of model-based
randomized testing (Section <ref>).  To check the
correctness of our formal model, we compare the behavior between the
existing Clang implementation and our own model. This is
done by a conversion tool that converts expressions from into
actual code that can be compiled by the Clang compiler. We build a random generator of programs largely based on the
typing rules of and make sure that, both statically and
dynamically, and Clang Checked C are consistent after
conversion.  This helped rapidly prototype the model and uncovered
several issues in the Checked C compiler.

models' relationship to

Summary Visualization The
relationship among our contributions is visualized in
Fig. <ref>. With the Coq model of we prove
soundness (and with it, blame) of the type system
and semantics. With the Redex model, we use randomized testing to
validate both type soundness and compilation correctness, where the
latter shows how compilation need not output fat pointers despite
the use of pointer annotations in the model. The Redex model is also the basis of randomized testing of the correctness of
the compiler implementation, both its type checker and the
semantics of its emitted code, at least for the subset of the
language in the Redex model. The Redex model's syntax
is slightly richer than the Coq version: conditional guards and
function arguments may be arbitrary expressions, where the Coq
version limits them to constants and variables, making handling of
dependent types a bit simpler. We find a useful synergy between the
Coq and Redex models for carrying out a language development. The
richer, executable Redex model is useful for quickly modeling and
testing new features, both formally and against a real
implementation. Once solidified, new features can be added to the
Coq model (perhaps somewhat simplified) for final proofs of

We begin with a review of (Section <ref>),
present our main contributions
(Sections <ref>–<ref>), and conclude with a
discussion of
related and future work (Sections <ref>,
<ref>). All code and proof artifacts (both for Coq and
Redex) can be found at <https://github.com/plum-umd/checkedc>.

§ OVERVIEW

This section describes Checked C, which extends C with new pointer
types and annotations that ensure spatial safety. Development of
Checked C was initiated by Microsoft Research in 2015 but starting in
late 2021 was forked and is now actively managed by the Secure Software
Development Project (SSDP). Details can be found in a prior
overview [Elliott et al., 2018] or the full specification [Tarditi, 2021].
Checked C is implemented as an extension of Clang/LLVM and the SSDP
fork is freely available at <https://github.com/secure-sw-dev>.

[xleftmargin=4 mm]
nt_array_ptr<const char>
parse_utf16_hex(nt_array_ptr<const char> s,
ptr<uint> result)
int x1, x2, x3, x4;
if (s[0] != 0)  x1 = hex_char_to_int(s[0]);
if (s[1] != 0)  x2 = hex_char_to_int(s[1]);
if (s[2] != 0)  x3 = hex_char_to_int(s[2]);
if (s[3] != 0)  x4 = hex_char_to_int(s[3]);
if (x1 != -1        x2 != -1        x3 != -1        x4 != -1)
*result = (uint)((x1<<12)|(x2<<8)|(x3<<4)|x4);
return s+4;
...// several  braces

return 0;

void parse(nt_array_ptr<const char> s,
array_ptr<uint> p : count(n),
int n)
array_ptr<uint> q : bounds(p,p+n) = p;
while (s        q < p+n)
array_ptr<uint> r : count(1) =
s = parse_utf16_hex(s,r);

Parsing a String of UTF16 Hex Characters in

§.§ Checked Pointer Types

introduces three varieties of checked pointer:

* ptr<$T$> types a pointer that is either null or
points to a single object of type $T$.

* array_ptr<$T$> types a pointer that is either null
or points to an array of $T$ objects. The array width is defined
by a bounds expression, discussed below.

* nt_array_ptr<$T$> is like
array_ptr<$T$> except that the bounds expression
defines the minimum array width—additional objects may
be available past the upper bound, up to a null terminator.

A bounds expression used with the latter two pointer types has three

* count($e$) where $e$ defines the array's
length. Thus, if pointer $p$ has bounds count(n) then the
accessible memory is in the range $[p,p+$n$]$. Bounds
expression $e$ must be side-effect free and may only refer to
variables whose addresses are not taken, or adjacent struct

* byte_count($e$) is like count, but
expresses arithmetic using bytes, no objects; i.e.,
count($e$) used for array_ptr<$T$> is
equivalent to byte_count($e\times\texttt{sizeof}(T)$)

* bounds($e_l$,$e_h$) where $e_l$ and $e_h$ are
pointers that bound the accessible region $[e_l,e_h)$ (the
expressions are similarly restricted). Bounds
count($e$) is shorthand for
bounds($p, p + e$). This most general form of bounds
expression is useful for supporting pointer arithmetic.

Dropping the bounds expression on an nt_array_ptr is equivalent
to the bounds being count(0).

The compiler will instrument loads and stores of checked
pointers to confirm the pointer is non-null, and the access is within
the specified bounds. For pointers $p$ of type
nt_array_ptr<$T$>, such a check could spuriously fail if
the index is past $p$'s specified upper bound, but before the null
terminator. To address this problem, Checked C supports bounds
If $p$'s bounds expression is bounds$(e_l$,$e_h)$ a program may read from (but not
write to) $e_h$; when the compiler notices that a non-null character
is read at the upper bound, it will extend that bound to $e_h+1$.

§.§ Example

Fig. <ref> gives an example program.[Ported from the Parson JSON
parser, <https://github.com/kgabis/parson>]
The function parse_utf16_hex on lines 1-15 takes a
null-terminated pointer s as its argument, from which it attempts to read four
characters. These are interpreted as hex digits and converted to an
uint returned via parameter result. At first,
s has no specific bounds annotation, which we can interpret as
count(0); this means that s[0] may be read on line
5. The true branch of the conditional (which extends all the way to
the brace on line 13) is thus type-checked with s given a
widened bound of count(1). Likewise, the conditionals on
lines 6-8 each widen it one further; the widened pointer
(s+4) is returned on success.

The parse function on lines 16-26 repeatedly invokes
parse_utf16_hex with its parameter s, and fills out
array p whose declared length is the parameter n. Writes
happen via pointer q, which is updated using pointer
arithmetic. We specify its bounds as
bounds(p,p+n) to support this: even as q changes, variables p and n (and therefore also q's bounds) do not. Converting from an
array_ptr<uint> to a ptr<uint>, done for the call on
line 23, requires proving the array has size at least 1. While this is true
because of the loop condition q < p+n, which is q's
upper bound,  the compiler is not smart enough to figure this
out. To convince it, we manually insert a dynamic cast via
dyn_bounds_cast, which is trusted at compile-time but confirmed
with a dynamic check at run-time.

While bounds checks are conceptually inserted on every array
load and store, many of these are eliminated by LLVM. For example,
all of the pointer accesses to s on lines 5-8 are proved safe
at compile-time, so no bounds checks are inserted for
them. Elliott et al., 2018
reported average run-time overheads of 8.6% on a pointer-intensive
benchmark suite (49.3% in one case); Duan et al., 2020 measured
no overhead at all on a port of FreeBSD's UDP and IP stacks to .

§.§ Other features

has other features not modeled in this paper. Two in regular
use are interop types, which ascribe checked pointer types to
unported legacy code, notably in libraries; and generic types
on both functions and structs, for type-safe polymorphism. More
details about these can be found in the language specification.

§.§ Spatial Safety and Backward Compatibility

is backward compatible with legacy C in the sense that all
legacy code will type-check and compile. However, only code that
appears in checked regions, which we call checked code,
is spatially safe. Checked regions can be designated at the level of
files, functions, or individual code blocks, the first with a
#pragma and the latter two using the checked
keyword.[You can also designate unchecked regions
within checked ones.]  Within checked regions, both
legacy pointers and certain unsafe idioms (e.g., variadic function
calls) are disallowed. The code in Fig. <ref>
satisfies these conditions, and will type-check in a checked region.

How should we think about code that contains both checked and legacy
components? Ruef et al., 2019 proved, for a simple
formalization of , that checked code cannot be blamed:
Any spatial safety violation is caused by the execution of unchecked
code. In this paper we extend that result to a richer formalization of

§ RANDOM TESTING VIA THE IMPLEMENTATION

In addition to using the Redex model to establish simulation of
compilation (Section <ref>), we also used it to gain confidence
that our model matches the Clang implementation.
Disagreement on outcomes signals a bug in either the model or the
compiler itself. Doing so allowed us to quickly iterate on the
design of the model while adding new features, and revealed
several bugs in the Clang implementation.

Generating Well Typed Terms For this random generation, we follow
the approach of Pałka et al., 2011 to generate well-typed terms by viewing the typing rules as generation rules.

Suppose we have a context $\Gamma$, a mode
$m$ and a type $\tau$, and we are
trying to generate a well-typed expression. We can do that by
reversing the process of type checking, selecting a typing rule and
building up an expression in a way that satisfies the rule's premises.

Recall the typing rule for dereferencing an
array pointer, which we depict below as
G-DefArr[Generator rules G-* correspond one to one
with the type rules T-* in Sec. <ref>.], color-coded to represent inputs and outputs of the
generation process:
[This input-output marking is commonly called a mode in
the literature, but we eschew this term to avoid
confusion with our pointer mode annotation.]

Γ;Θ ⊢_m e : τm'

m ≤m'

Γ;Θ ⊢_m e : τ

If we selected G-DefArr for generating an expression, the
generated expression has to have the form $\textcolor{blue}{*e}$,
for some $\textcolor{blue}{e}$, to be generated according
to the rule's premises.

To satisfy the premise
\vdash_{\textcolor{red}{m}} \textcolor{blue}{e} :
\tptr{\tallarraybc{\textcolor{cyan}{\bvar}}{\textcolor{red}{\tau}}}{\textcolor{cyan}{m'}}$,
we essentially need to make a recursive call to the generator, with
appropriately adjusted inputs.

However, the type in this judgment is not fixed yet—it contains
three unknown variables: $\textcolor{cyan}{m'}$,
$\textcolor{cyan}{\bvar}$, and $\textcolor{cyan}{\kappa}$—that need
to be generated before making the call.

Looking at the second premise informs that generation:
if the input mode $\textcolor{red}{m}$ is $\umode$, then $\textcolor{cyan}{m'}$
needs to be $\umode$ as well; if not, it is unconstrained,
just like $\textcolor{cyan}{\bvar}$ and $\textcolor{cyan}{\kappa}$, and therefore all three are free to be generated at random.

Thus, the recursive call to generate $\textcolor{blue}{e}$ can now
be made, and the G-DefArr rule returns $\textcolor{blue}{*e}$
as its output.

Using such generator rules, we can create a generator for random
well-typed terms of a given type in a straightforward manner: find all
rules whose conclusion matches the given type and then randomly choose
a candidate rule to perform the generation. To ensure that this
process terminates, we follow the standard practice of using “fuel” to
bound the depth of the generated terms; once the fuel is exhausted,
only rules without recursive premises are
selected [Lampropoulos and Pierce, 2018]. Similar methods were used for
generating top level functions and struct definitions.

While using just the typing-turned-generation rules is in theory
enough to generate all well-typed terms, it's more effective in
practice to try and exercise interesting patterns.  As
in Pałka et al., 2011 this can be viewed as a way of adding admissible
but redundant typing rules, with the sole purpose of
using them for generation. For example, below is one such rule,
G-ASTR, which creates an initialized null-terminated string that
is statically cast into an array with bounds $(0,0)$.

i ∈ℕ^*     n_0,…,n_i-1  ∈ℤ     (x)

Γ ⊢_m
e' :

e = xe'n_0,…n_i-1;x

Γ ⊢_m 00ce : 00c

Given some positive number $\textcolor{cyan}{i}$, numbers
$\textcolor{cyan}{n_0, \ldots, n_{i-1}}$, and a fresh variable
$\textcolor{cyan}{x}$ (which are arbitrarily generated), we can
recursively generate a pointer $\textcolor{blue}{e'}$ with bounds
$(0,\textcolor{cyan}{i})$, and initialize it with the generated $n_j$
using $\textcolor{cyan}{x}$ to temporarily store the pointer.

This rule is particularly useful when combined with G-IfNT
since there is a much higher chance of obtaining a non-zero value when
evaluating $\estar{p}$ in the guard of $\eiftext$, skewing the
distribution towards programs that enter the $\ethentext$ branch.
Relying solely on the type-based rules, entering the $\ethentext$
branch requires that G-AssignArr was chosen before G-IfNT,
and that assignment would have to appear before $\eiftext$, which
means additional G-Let rules would need to be chosen: this
combination would therefore be essentially impossible to generate in

Adding admissible generation rules like G-Astr in this
manner, as described in Pałka et al., 2011, is a manual process. It is
guided by gathering statistics on the generated data and focusing on
language constructs that appear underrepresented in the posterior
distribution. For example, we arrived at the G-Astr rule by
recognizing that the pure type-based generation was not generating
non-trivial null-terminated strings, and then analyzing the sequence
of random choices that could lead to their generation.

Generating Ill-typed Terms

We can use generated well-typed terms to test our simulation theorem
(Section <ref>) and test that and Clang agree on what is type-correct. But it is also useful to generate
ill-typed terms to test that and Clang also agree on
what is not.  However, while it is easy to generate arbitrary
ill-typed terms, they would be very unlikely to trigger any
inconsistencies; those are far more likely to exist on the boundary
between well- and ill-typedness. Therefore, we also manually added
variations of existing generation rules modified to be slightly more
permissive, e.g., by relaxing a single premise, thus allowing terms
that are “a little” ill-typed to be generated. Unlike coming up with
admissible generation rules like G-Astr (which is quite
challenging to automate), systematically and automatically relaxing
premises of existing rules seems feasible, and worthwhile future work.

Random Testing for Language Design

We used our Redex model and random generator to successfully guide the
design of our formal model, and indeed the Clang Checked C
implementation itself, which is being actively developed. To that end, we implemented a
conversion tool that converts into a subset of the language and ensured that model and implementation exhibit the same
behavior (accept and reject the same programs and yield the same return

This approach constitutes an interesting twist to traditional
model-based checking approaches.  Usually, one checks that the
implementation and model agree on all inputs of the
implementation, with the goal of covering as many behaviors as
possible. This is the case, for example, in Guha et al., 2010, where
they use real test suites to demonstrate the faithfullness of their
core calculus to Javascript. Our approach and goal in this work is
essentially the opposite: as the Clang Checked C implementation does
not fully implement the Checked C spec, there is little hope of
covering all terms that are generated by Clang Checked C. Instead,
we're looking for inconsistencies, which could be caused by
bugs either in the Clang Checked C compiler or our own model.

One inconsistency we found comes from the following:

[xleftmargin=4 mm]
array_ptr<char> fun(void) : count(3)
array_ptr<char> x : count(3);
x = calloc(3, sizeof(char));
return x+3;

int main(void)
*(fun()) = 0;
return 0;

In this code, the function fun is supposed to return a
checked array pointer of size 3. Internally, it allocates such an
array, but instead of returning the pointer x to that array, it
increments that pointer by 3. Then, the main function just
calls fun, and tries to assign 0 to its result. Our model
correctly rules out this program, while the Clang Checked C
implementation happily accepted this out-of-bounds
assignment. Interestingly, it correctly rejected programs where the
array had size 1 or 2. This inconsistency has been fixed in the latest
version of the compiler.

We also found the opposite kind of inconsistency—programs that
the Clang Checked C implementation rejects contrary to the spec.
For instance:
[After minimization, this turned out to be a known issue:

[xleftmargin=4 mm]
array_ptr<int> f(void) : count(5)
array_ptr<int> x : count(5) =
calloc<int>(5, sizeof(int));
return x;

array_ptr<int> g(void ) : count(5)
array_ptr<int> x : count(5) =
calloc<int>(5, sizeof(int));
return x+3;

int main(void)
return *(0 ? g() : f() + 3);

In this piece of code both f and g functions compute a
pointer to the same index in an array of size 5 (as f calls
g). The main function then creates a ternary expression
whose branches call f and g, but the Clang Checked C
implementation rejects this program, as its static analysis is not
sophisticated enough to detect that both branches have the same type.

§ RELATED WORK

Our work is most closely related to prior formalizations of C(-like)
languages that aim to enforce memory safety, but it also touches on
C-language formalization in general.

Formalizing C and Low-level code

A number of prior works have looked at formalizing the semantics of C,
including CompCert [Blazy and Leroy, 2009, Leroy et al., 2012],
Ellison and Rosu, 2012, Kang et al., 2015,
and Memarian et al., 2016, Memarian et al., 2019. These works also model
pointers as logically coupled with either the bounds of the blocks
they point to, or provenance information from which bounds can be
derived. None of these is directly concerned with enforcing
spatial safety, and that is reflected in the design. For example,
memory itself is not be represented as a flat address space, as in our
model or real machines, so memory corruption due to spatial safety
violations, which Checked C's type system aims to prevent, may not be
expressible. That said, these formalizations consider much more of the
C language than does , since they are interested in the entire
language's behavior.

Spatially Safe C Formalizations

Several prior works formalize C-language transformations or C-language
dialects aiming to ensure spatial safety.

Hathhorn et al., 2015 extends the formalization
of Ellison and Rosu, 2012 to produce a semantics that detects
violations of spatial safety (and other forms of undefinedness). It
uses a CompCert-style memory model, but “fattens” logical pointer
representations to facilitate adding side conditions similar to 's.
Its concern is bug finding, not compiling programs to
use this semantics.

CCured [Necula et al., 2005] and Softbound [Nagarakatte et al., 2009] implement
spatially safe semantics for normal C via program transformation. Like
, both systems' operational semantics annotate pointers with
their bounds. CCured's equivalent of array pointers are compiled to be
“fat,” while SoftBound compiles bounds metadata to a separate
hashtable, thus retaining binary compatibility at higher checking
cost. Checked C uses static type information to enable bounds checks
without need of pointer-attached metadata, as we show in
Section <ref>. Neither CCured nor Softbound models
null-terminated array pointers, whereas our semantics ensures that
such pointers respect the zero-termination invariant, leveraging
bounds widening to enhance expressiveness.

Cyclone [Jim et al., 2002, Grossman et al., 2002] is a C dialect that aims to
ensure memory safety; its pointer types are similar to
CCured. Cyclone's formalization [Grossman et al., 2002] focuses on the
use of regions to ensure temporal safety; it does not formalize
arrays or threats to spatial safety. Deputy [Zhou et al., 2006, Condit et al., 2007]
is another safe-C dialect that aims to avoid fat pointers; it was an
initial inspiration for Checked C's design [Elliott et al., 2018], though
it provides no specific modeling for null-terminated array
pointers. Deputy's formalization [Condit et al., 2007] defines its
semantics directly in terms of compilation, similar in style to what
we present in Section <ref>. Doing so tightly couples
typing, compilation, and semantics, which are treated independently in
. Separating semantics from compilation isolates meaning
from mechanism, easing understandability. Indeed, it was this
separation that led us to notice the
limitation with Checked C's handling of bounds widening.

The most closely related work is the
formalization of done by Ruef et al., 2019. They
present the type system and semantics of a core model of ,
mechanized in Coq, and were the first to prove a blame theorem.  's
Coq-based development (Section <ref>) substantially extends
theirs to include conditionals, dynamically bounded array
pointers with dependent types, null-terminated array pointers,
dependently typed functions, and subtyping. They postulate that pointer metadata can
be erased in a real implementation, but do not show it. Our compiler, formalized and
validated in PLT Redex via randomized testing, demonstrates that such
metadata can be erased; we found that erasure was non-obvious once
null-terminated pointers and bounds widening were considered.

§ CONCLUSION AND FUTURE WORK

This paper presented , a formalization of an extended core of
the Checked C language which aims to provide spatial memory
safety. models dynamically sized and
null-terminated arrays with dependently typed bounds that can
additionally be widened at runtime. We prove, in Coq, the key safety
property of Checked C for our formalization, blame: if a mix of
checked and unchecked code gives rise to a spatial memory safety
violation, then this violation originated in an unchecked part of the
code. We also show how programs written in (whose
semantics leverage fat pointers) can be compiled to (which does
not) while preserving their behavior. We developed a version of written in PLT Redex, and used a custom term generator in conjunction with Redex's
randomized testing framework to give confidence that compilation is
correct. We also used this framework to cross-check against the compiler, finding multiple inconsistencies
in the process.

As future work, we wish to extend to model more of Checked
C, with our Redex-based testing framework guiding the process. The
most interesting Checked C feature not yet modeled is interop
types (itypes), which are used to simplify interactions with
unchecked code via function calls. A function whose
parameters are itypes can be passed checked or unchecked pointers
depending on whether the caller is in a checked region. This feature
allows for a more modular C-to-Checked C porting process, but complicates reasoning
about blame. A more ambitious next step would be to extend an existing
formally verified framework for C, such as CompCert [Leroy, 2009] or VeLLVM
[Zhao et al., 2012], with Checked C features, towards
producing a verified-correct Checked C compiler. We believe that
's Coq and Redex models lay the foundation for such a step, but
substantial engineering work remains.

We thank the anonymous reviewers for their helpful, constructive
comments. This work was supported in part by a gift from Microsoft.

[Blazy and Leroy, 2009]
Sandrine Blazy and Xavier Leroy.
Mechanized Semantics for the Clight Subset of the C Language.
Journal of Automated Reasoning, 430 (3):0
263–288, 2009.
ISSN 1573-0670.
URL <http://dx.doi.org/10.1007/s10817-009-9148-3>.

[Condit et al., 2007]
Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C.
Dependent Types for Low-Level Programming.
In Proceedings of European Symposium on Programming (ESOP
'07), 2007.

[Duan et al., 2020]
Junhan Duan, Yudi Yang, Jie Zhou, and John Criswell.
Refactoring the FreeBSD Kernel with Checked C.
In IEEE Cybersecurity Development Conference (SecDev),
September 2020.

[Elliott et al., 2018]
Archibald Samuel Elliott, Andrew Ruef, Michael Hicks, and David Tarditi.
Checked C: Making C Safe by Extension.
In 2018 IEEE Cybersecurity Development (SecDev), pages 53–60,

[Ellison and Rosu, 2012]
Chucky Ellison and Grigore Rosu.
An Executable Formal Semantics of C with Applications.
In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, POPL '12, pages 533–544, New York,
NY, USA, 2012. ACM.
ISBN 978-1-4503-1083-3.
URL <http://doi.acm.org/10.1145/2103656.2103719>.

[Felleisen et al., 2009]
Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt.
Semantics Engineering with PLT Redex.
The MIT Press, 1st edition, 2009.
ISBN 0262062755.

[Grossman et al., 2002]
Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and
James Cheney.
Region-based Memory Management in Cyclone.
In PLDI, 2002.

[Guha et al., 2010]
Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi.
The Essence of Javascript.
In Proceedings of the 24th European Conference on
Object-Oriented Programming, ECOOP'10, page 126–150, Berlin, Heidelberg,
2010. Springer-Verlag.
ISBN 3642141064.

[Hathhorn et al., 2015]
Chris Hathhorn, Chucky Ellison, and Grigore Roşu.
Defining the Undefinedness of C.
SIGPLAN Not., 500 (6):0 336–345, June 2015.
ISSN 0362-1340.
URL <https://doi.org/10.1145/2813885.2737979>.

[Jim et al., 2002]
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, , and
Yanling Wang.
Cyclone: A Safe Dialect of C.
In USENIX Annual Technical Conference, pages 275–288,
Monterey, CA, 2002. USENIX.

[Kang et al., 2015]
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic,
and Viktor Vafeiadis.
A Formal C Memory Model Supporting Integer-pointer Casts.
SIGPLAN Not., 500 (6):0 326–335, June 2015.
ISSN 0362-1340.
URL <http://doi.acm.org/10.1145/2813885.2738005>.

[Lampropoulos and Pierce, 2018]
Leonidas Lampropoulos and Benjamin C. Pierce.
QuickChick: Property-Based Testing in Coq.
Software Foundations series, volume 4. Electronic textbook, August
Version 1.0. <http://www.cis.upenn.edu/ bcpierce/sf>.

[Leroy, 2009]
Xavier Leroy.
Formal verification of a realistic compiler.
Communications of the ACM, 520 (7):0 107–115,
July 2009.
ISSN 0001-0782.
URL <http://doi.acm.org/10.1145/1538788.1538814>.

[Leroy et al., 2012]
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart.
The CompCert Memory Model, Version 2.
Research Report RR-7987, INRIA, June 2012.
URL <https://hal.inria.fr/hal-00703441>.

[Memarian et al., 2016]
Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David
Chisnall, Robert N. M. Watson, and Peter Sewell.
Into the Depths of C: Elaborating the de Facto Standards.
SIGPLAN Not., 510 (6):0 1–15, June 2016.
ISSN 0362-1340.
URL <https://doi.org/10.1145/2980983.2908081>.

[Memarian et al., 2019]
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander
Richardson, Robert N. M. Watson, and Peter Sewell.
Exploring C Semantics and Pointer Provenance.
Proc. ACM Program. Lang., 30 (POPL):0
67:1–67:32, January 2019.
ISSN 2475-1421.
URL <http://doi.acm.org/10.1145/3290380>.

[Merigoux et al., 2021]
Denis Merigoux, Nicolas Chataing, and Jonathan Protzenko.
Catala: A Programming Language for the Law.
arXiv preprint arXiv:2103.03198, 2021.

[Nagarakatte et al., 2009]
Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic.
SoftBound: Highly Compatible and Complete Spatial Memory Safety for
In Proceedings of the 30th ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI '09, page 245–258,
New York, NY, USA, 2009. Association for Computing Machinery.
ISBN 9781605583921.
URL <https://doi.org/10.1145/1542476.1542504>.

[Necula et al., 2005]
George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley
CCured: Type-Safe Retrofitting of Legacy Software.
ACM Transactions on Programming Languages and Systems
(TOPLAS), 270 (3), 2005.

[Pałka et al., 2011]
Michał H. Pałka, Koen Claessen, Alejandro Russo, and John Hughes.
Testing an Optimising Compiler by Generating Random Lambda Terms.
In Proceedings of the 6th International Workshop on Automation
of Software Test, AST '11, pages 91–97, New York, NY, USA, 2011. ACM.
ISBN 978-1-4503-0592-1.
URL <http://doi.acm.org/10.1145/1982595.1982615>.

[Peña, 2017]
Ricardo Peña.
An Introduction to Liquid Haskell.
Electronic Proceedings in Theoretical Computer Science,
237:0 68–80, Jan 2017.
ISSN 2075-2180.
URL <http://dx.doi.org/10.4204/EPTCS.237.5>.

[Ruef et al., 2019]
Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, and Michael
Achieving Safety Incrementally with Checked C.
In Flemming Nielson and David Sands, editors, Principles of
Security and Trust, pages 76–98, Cham, 2019. Springer International
ISBN 978-3-030-17138-4.

[Serebryany et al., 2012]
Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitry Vyukov.
AddressSanitizer: A Fast Address Sanity Checker.
In Proceedings of the 2012 USENIX Conference on Annual
Technical Conference, 2012.

[Tarditi, 2021]
David Tarditi.
Extending C with Bounds Safety and Improved Type Safety, 2021.
URL <https://github.com/secure-sw-dev/checkedc/>.

[Vazou et al., 2014]
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon
Refinement Types for Haskell.
SIGPLAN Not., 490 (9):0 269–282, August
ISSN 0362-1340.
URL <https://doi.org/10.1145/2692915.2628161>.

[Zeng et al., 2013]
Bin Zeng, Gang Tan, and Úlfar Erlingsson.
Strato: A Retargetable Framework for Low-level Inlined-reference
In Proceedings of the 22Nd USENIX Conference on Security,

[Zhao et al., 2012]
Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic.
Formalizing the LLVM Intermediate Representation for Verified
Program Transformations.
SIGPLAN Not., 470 (1):0 427–440, January
ISSN 0362-1340.
URL <http://doi.acm.org/10.1145/2103621.2103709>.

[Zhou et al., 2006]
Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew
Harren, George Necula, and Eric Brewer.
SafeDrive: Safe and recoverable extensions using language-based
In 7th Symposium on Operating System Design and Implementation
(OSDI'06), Seattle, Washington, 2006. USENIX Association.

§ APPENDIX

§.§ Differences with the Coq and Redex Models

The Coq and Redex models of may be found at <https://github.com/plum-umd/checkedc>.
The Coq model's syntax is slightly different from that in
Fig. <ref>. In particular, the arguments in a function call
are restricted to variables and constants, according to
a separate well-formedness condition. A function call f(e) can
always be written in let x = e in f(x) to cope.

In addition,
conditionals have two syntactic forms: EIf is a normal
conditional, and EIfDef is one whose boolean guard is of the
form x. By syntactically distinguishing these two
cases, the Coq model does not need the [prefer] rule for
if (*x)$...$ forms as in
Fig. <ref>. The Redex model does prioritize such
forms but not the same way as in the figure. It uses a variation of
the S-Var rule: The
modified rule is equipped with a precondition that is false whenever
S-IfNTT is applicable.

The Coq model uses a runtime stack $\varphi$ as described at the start
of Sec. <ref>.
The Redex model introduces let bindings during evaluation to
simulate a runtime stack. For example, consider the expression
$e \equiv \elet{x}{(\evalue{5}{\tint})}{\ebinop{x}{x}}$. Expression $e$ first steps to
$\elet{x}{(\evalue{5}{\tint})}{\ebinop{(\evalue{5}{\tint})}{x}}$, which in
turns steps to
$\elet{x}{(\evalue{5}{\tint})}{\ebinop{(\evalue{5}{\tint})}{(\evalue{5}{\tint})}}$. Since
the rhs of $x$ is a value, the let binding in $e$ effectively
functions as a stack that maps from $x$ to $\evalue{5}{\tint}$. The
let form remains in the expression and lazily replaces the variables
in its body. The let form can be removed from the expression only if its
body is evaluated to a value, e.g.,
steps to
$\evalue{10}{\tint}$. The rule for popping let bindings in this manner
corresponds to the S-Ret rule in Fig. <ref>.
Leveraging let bindings adds complexity to the semantics but
simplifies typing/consistency and term generation during randomized testing.

§.§ Typing Rules for Literal Pointers

The typing of integer literals, which can also be pointers to the
heap, was presented in Sec. <ref> in Fig. <ref>. Here
we describe these rules further.

The variable type rule
($\textsc{T-Var}$) simply checks if a given variable has the defined
type in $\Gamma$; the constant rule ($\textsc{T-Const}$) is slightly
more involved.  First, it ensures that the type annotation $\tau$ does
not contain any free variables. More importantly, it ensures that the
literal itself is well typed using an auxilliary typing relation
$\heap;\sigma \vdash n : \tau$.

If the literal's type is an integer, an unchecked pointer, or a null
pointer, it is well typed, as shown by the top three rules in
Fig. <ref>. However, if it is a checked pointer
$\tptr{\omega}{\cmode}$, we need to ensure that what it points to in
the heap is of the appropriate pointed-to type ($\omega$), and also
recursively ensure that any literal pointers reachable this way are
also well-typed. This is captured by the bottom rule in the figure,
which states that for every location $n+i$ in the pointers' range

$[n, n+\size(\omega))$, where $\size$ yields the size of its argument,
then the value at the location $\heap(n+i)$ is also well-typed.
However, as heap snapshots can contain cyclic structures (which
would lead to infinite typing deriviations), we use a scope $\sigma$
to assume that the original pointer is well-typed when checking the
types of what it points to. The middle rule then accesses the scope
to tie the knot and keep the derivation finite, just like in
Ruef et al., 2019.

§.§ Other Semantic Rules

Fig. <ref> shows the remaining semantic rules for
$\lang$. We explain a selected few rules in this subsection.

[S-Var] (φ,,x)⟶(φ,,φ(x))

0 ∈[n_l,n_h)
(φ,,nn_ln_hτ) ⟶(φ,,n_aτ)

[S-DefArrayBound]0 ∉[n_l,n_h)
(φ,,nn_ln_hτc) ⟶(φ,,)

[S-DefNTArrayBound]0 ∉[n_l,n_h]
(φ,,nn_ln_hτ) ⟶(φ,,)

(φ,,nτn_1τ_1) ⟶(φ,[n ↦n_1τ],n_1τ)

(φ,,0ωn_1τ_1) ⟶(φ,,)

[S-AssignArrBound]0 ∉[n_l,n_h)
(φ,,nn_ln_hτn_1τ_1) ⟶(φ,,)

(φ,,ω) ⟶(φ,',nω_a)

(n_l ≠0 ∨n_h ≤0)
(φ,,ω) ⟶(φ,',)

[S-IfT]n ≠0
(φ,,nτe_1e_2) ⟶(φ,,e_1)

(φ,,0τe_1e_2) ⟶(φ,,e_2)

(φ,,nτ ⟶(φ,,nτ)

0 ∈[n_l,n_h]

n_a ≤n_h

(n+n_a) = 0

(∀i. n ≤i < n+n_a ⇒(∃n_i t_i. (n+i) = n_iτ_i ∧n_i ≠0))
(φ,,nn_ln_hτm) ⟶(φ,,n_a)

0 ∉[n_l,n_h]

(φ,,nn_ln_hτc) ⟶(φ,,)

(φ,,0n_ln_hτc) ⟶(φ,,)

[S-Add]n = n_1 + n_2
(φ,,n_1 n_2) ⟶(φ,, n)

[S-AddArr]n = n_1 + n_2
n_l' = n_l - n_2
n_h' = n_h - n_2
(φ,,n_1n_ln_hτm n_2) ⟶(φ,, nn_l'n_h'τm)

n    [S-AddArrNull]
(φ,,0n_ln_hτc n_2) ⟶(φ,, )

Remaining Semantics Rules (extends Fig. <ref>)

Rule S-Var loads the value for $x$ in stack $\varphi$.
Rule S-DefArray dereferences an array pointer, which is similar to the Rule S-DefNTArray in Fig. <ref> (dealing with null-terminated array pointers).
The only difference is that the range of $0$ is at $[n_l,n_h)$ not $[n_l,n_h]$, meaning that one cannot dereference the upper-bound position in an array.
Rules DefArrayBound and DefNTArrayBound describe an error case for a dereference operation.
If we are dereferencing an array/NT-array pointer and the mode is $\cmode$, $0$ must be in the range from $n_l$ to $n_h$ (meaning that the dereference is in-bound); if not, the system results in a $\ebounds$ error. Obviously, the dereference of an array/NT-array pointer also experiences a $\enull$ state transition if $n\le 0$.

Rules S-Malloc and S-MallocBound describe the $\emalloctext$ semantics. Given a valid type $\omega_a$ that contains no free variables, $\mathtt{alloc}$ function returns an address pointing at the first position of an allocated space whose size is equal to the size of $\omega_a$, and a new heap snapshot $\heap'$ that marks the allocated space for the new allocation. The $\emalloctext$ is transitioned to the address $n$ with the type ${\tptr{\omega_a}{\cmode}}$ and new updated heap. It is possible for $\emalloctext$ to transition to a $\ebounds$ error if the $\omega_a$ is an array/NT-array type $\tallarray{n_l}{n_h}{\tau}$, and either $n_l \neq 0$ or $n_h \le 0$. This can happen when the bound variable is evaluated to a bound constant that is not desired.

§.§ Subtyping for dependent types

The subtyping relation given in Fig. <ref> involves
dependent bounds, i.e., bounds that may refer to variables. To decide
premises $b \leq b'$, we need a decision procedure that accounts for
the possible values of these variables. This process considers
$\Theta$, tracked by the typing judgment, and $\varphi$, the current
stack snapshot (when performing subtyping as part of the type
preservation proof).

* $n \le m$ if $n$ is less than or equal to $m$.

* $x+n \le x + m$ if $n$ is less than or equal to $m$.

* All other cases result in $\efalse$.

To capture bound variables in dependent types, the subtyping
relation ($\sqsubseteq$) is parameterized by a restricted stack
snapshot $\varphi|_{\rho}$ and the predicate map $\Theta$, where
$\varphi$ is a stack and $\rho$ is a set of
variables. $\varphi|_{\rho}$ means to restrict the domain of $\varphi$
to the variable set $\rho$. Clearly, we have the relation:
$\varphi|_{\rho} \subseteq \varphi$. $\sqsubseteq$
being parameterized by $\varphi|_{\rho}$ refers to that when we
compare two bounds $b \le b'$, we actually do
$\varphi|_{\rho}(b) \le \varphi|_{\rho}(b')$ by interpreting the
variables in $b$ and $b'$ with possible values in $\varphi|_{\rho}$.
Let's define a subset relation $\preceq$ for two restricted stack
snapshot $\varphi|_{\rho}$ and $\varphi'|_{\rho}$:

[Subset of Stack Snapshots]
Given two $\varphi|_{\rho}$ and $\varphi'|_{\rho}$,
$\varphi|_{\rho} \preceq \varphi'|_{\rho}$, iff for $x\in\rho$ and
$(x,y) \in \varphi|_{\rho} \Rightarrow (x,y) \in \varphi'|_{\rho}$.

For every two restricted stack snapshots $\varphi|_{\rho}$ and
$\varphi'|_{\rho}$, such that
$\varphi|_{\rho} \preceq \varphi'|_{\rho}$, we have the following
theorem in (proved in Coq):

Given two types $\tau$ and $\tau'$, two restricted stack snapshots
$\varphi|_{\rho}$ and $\varphi'|_{\rho}$, if
$\varphi|_{\rho}\preceq \varphi'|_{\rho}$, and
$\tau \sqsubseteq \tau'$ under the parameterization of
$\varphi|_{\rho}$, then $\tau \sqsubseteq \tau'$ under the
parameterization of $\varphi'|_{\rho}$.

Clearly, for every $\varphi|_{\rho}$, we have
$\emptyset \preceq \varphi|_{\rho}$. The type checking stage is a
compile-time process, so $\varphi|_{\rho}$
is $\emptyset$ at the type checking stage. Stack snapshots are needed
for proving type preserving, as variables in bounds expressions are
evaluated away.

Γ;Θ⊢_m e : τm'

m ≤m'
Γ;Θ⊢_m e : τ

Γ; Θ⊢_m ω : ω

Γ; Θ⊢_m e_1 :

Γ; Θ⊢_m e_2 :
Γ; Θ⊢_m (e_1 e_2) :

Γ; Θ⊢_m e_1 : τm'

Γ; Θ⊢_m e_2 :

m ≤m'
Γ; Θ⊢_m (e_1e_2) : τ

Γ; Θ⊢_m e_1 : τm'

Γ; Θ⊢_m e_2 : τ'

m ≤m'
Γ; Θ⊢_m e_1e_2 : τ

Γ; Θ⊢_m e_1 : τm'

Γ; Θ⊢_m e_2 :

Γ; Θ⊢_m e_3 : τ'

m ≤m'
Γ; ⊢_m (e_1 e_2)e_3 : τ

Remaining Type Rules (extends Fig. <ref>)

As mentioned in the main text, $\sqsubseteq$ is also parameterized by
$\Theta$, which provides the range of allowed values for a bound
variable; thus, more $\sqsubseteq$ relation is provable. For example,
in Fig. <ref>, the strlen operation in line 4
turns the type of dst to be $\tntarrayptr{0}{x}{\tint}{\cmode}$
and extends the upper bound to x. In the strlen type
rule, it also inserts a predicate x$\ge 0$ in $\Theta$; thus,
the cast operation in line 16 is valid because
$\tntarrayptr{0}{x}{\tint}{\cmode} \sqsubseteq
\tntarrayptr{0}{0}{\tint}{\cmode}$ is provable when we know
x$\ge 0$.

Note that if $\varphi$ and $\Theta$ are $\emptyset$, we do only the
syntactic $\le$ comparison; otherwise, we apply $\varphi$ to both
sides of $\sqsubseteq$, and then determine the $\le$ comparasion based
on a Boolean predicate decision procedure on top of $\Theta$. This
process allows us to type check both an input expression and the
intermediate expression after evaluating an expression.

§.§ Other Type Rules

Here we show the type rules for other operations in Fig. <ref>.
Rule T-Def is for dereferencing a non-array pointer.
The statement $m \leq m'$ ensures that no unchecked pointers are used in checked regions.
Rule T-Mac deals with
$\emalloctext$ operations. There is a well-formedness check to require
that the possible bound variables in $\omega$ must be in the domain of
$\Gamma$ (see Fig. <ref>). This is similar to the well-formedness assumption of the type environment (Definition <ref>) Rule T-Add deals with binary operations whose sub-terms are integer expressions, while rule T-Ind serves the case for pointer arithmetic. For simplicity, in the formalization, we do not allow arbitrary pointer arithmetic. The only pointer arithmetic operations allowed are the forms shown in rules T-Ind and T-IndAssign in Fig. <ref>. Rule T-Assign assigns a value to a non-array pointer location. The predicate $\tau'\sqsubseteq \tau$ requires that the value being assigned is a subtype of the pointer type.
The T-IndAssign rule is an extended assignment operation for handling assignments for array/NT-array pointers with pointer arithmetic. Rule T-Unchecked type checks unchecked blocks.

§.§ Struct Pointers

has struct types and struct pointers. Fig. <ref> contains the syntax of struct types as well as new subtyping relations built on the struct values.
For a struct typed value, has a special operation for it, which is $\eamper{e}{f}$. This operation indexes the $f$-th position struct $T$ item, if the expression $e$ is evaluated to a struct pointer $\tptr{\tstruct{T}}{m}$. Rule T-Struct in Fig. <ref> describes its typing behavior.
Rules S-StructChecked and S-StructUnChecked describe the semantic behaviors of $\eamper{e}{f}$ on a given struct checked/unchecked pointers, while rule S-StructNull describes a checked struct null-pointer case.
In our Coq/Redex formalization, we include the struct values and the operation $\eamper{e}{f}$. We omit it in the main text due to the paper length limitation.

\text{  Struct Syntax: }\\[0.5em]
\begin{array}{ll}
\mathtt{Type} & \tstruct{T}
\\[0.2em]
\text{Structdefs} & D \; \in \; T \rightharpoonup fs \\[0.2em]
\text{Fields} & fs \; ::= \; \tau~\mathtt{f} \mid \tau~\mathtt{f}; fs
\end{array}\\[2em]
\text{  Struct Subtype: }\\[0.5em]
\begin{array}{l}
D(T) = fs \wedge fs(0) = \tnat \Rightarrow  \tptr{\tstruct{T}}{m} \sqsubseteq \tptr{\tnat}{m}\\[0.5em]
D(T) = fs \wedge fs(0) = \tnat \wedge 0 \le b_l \wedge b_h \le 1 \\[0.2em]
\qquad\qquad \Rightarrow
\tptr{\tstruct{T}}{m} \sqsubseteq \tarrayptr{b_l}{b_h}{\tnat}{m}
\end{array}
\\[3em]
\text{  Struct Type Rule: }\\[0.5em]
\end{array}

Γ; Θ⊢_m e :  Tm

D(T) = fs
Γ; Θ⊢_m ef : τ_fm

\text{Struct Semantics: }
\end{array}

n > 0
D(T) = fs
(φ,,nTf) ⟶(φ,,n_aτ_a)

n = 0
(φ,,nTf) ⟶(φ,,)

D(T) = fs
(φ,,nTf) ⟶(φ,,n_aτ_a)

Struct Definitions

Γ⊢x + n

T ∈D

Well-formedness for Types and Bounds

Γ[x ↦τ] ⊢τ

Γ[x ↦τ]; Θ⊢_ e : τ
Γ⊢τ (x:τ) e

Γ[x ↦τ] ⊢x:τ
Γ⊢x:τ, x:τ

Well-formedness for functions

Γ⊢τ 𝚏

Γ⊢τ 𝚏; fs

Well-formedness for structs

Γ[x ↦τ]; ∅⊢e ≫ė : τ
Γ⊢τ (x:τ) e ≫(x) ė

Compilation Rules for Functions

§.§ The Compilation Rules

Fig. <ref> and Fig. <ref> shows
the syntax for $\elang$, the target language for compilation. We syntactically
restrict the expressions to be in A-normal form to simplify the
presentation of the compilation rules. In the Redex model, we
occasionally break this constraint to speed up the performance of
random testing by removing unnecessary let bindings.
To allow explicit runtime
checks, we include $\ebounds$ and $\enull$ as part of $\elang$
expressions which, once evaluated, result in an corresponding error state. $\eassignstack{x}{\dot a}$ is a new syntactic form that
modifies the stack variable $x$ with the result of $\dot a$. It is
essential for bounds widening. $\leq$ and $-$ are introduced
to operate on bounds and decide whether we need to halt with a bounds error
or widen a null-terminated string.

\[\begin{array}{llcl}
\text{Atoms}       & \dot a & ::= & n \mid x \\

\text{C-Expressions} & \dot c & ::= & \dot a \mid \estrlen{\dot a}  \mid \emalloc {\dot  a}  \mid \ecall{f} {\overline{\dot a}}  \\
& & \mid &  \mid  \dot a \circ \dot a \mid \estar{\dot a} \\
& & \mid & \eassign{\dot a}{\dot a} \mid \eassignstack{x}{\dot a}  \mid \eif{\dot a}{\dot e}{\dot e} \\
& & \mid & \ebounds \mid \enull \\
\text{Expressions}  & \dot e & ::= & \dot c \mid \elet{x}{\dot c}{\dot e}\\
\text{Binops} & \circ & ::= & + \mid - \mid \leq  \\
\text{Closure} & \dot C & ::= & \hole \mid \elet{x}{\dot a}{\dot C} \\
& & \mid & \eif{\dot a}{\dot e}{\dot C} \mid \eif{\dot a}{\dot    C}{\dot e} \\
\text{Bounds Map} & \rho & \in & \texttt{Var} \rightharpoonup \texttt{Var} \times \texttt{Var}
\end{array}
\]

\[\begin{array}{lll}
\dot \mu & ::= & n \mid \bot \\
\dot c & ::= & \ldots  \mid \eret{x}{\dot \mu}{\dot e} \\
\dot H & \in & \mathbb{Z} \rightharpoonup \mathbb{Z} \\
\dot r & ::= & \dot e \mid \enull \mid \ebounds \\
\dot E & ::= & \hole \mid  \elet{x}{\dot E}{\dot e}  \mid \eret{x}{i}{\dot E} \\
& \mid & \eif{\dot E}{\dot e}{\dot e} \mid \estrlen{\dot E} \\
& \mid & \emalloc{\dot E} \mid \ecall{f}{\overline{\dot
E}} \mid \dot E \circ \dot a \mid n \circ \dot E \\
& \mid & \estar{\dot E} \mid \eassign{\dot E}{\dot a}
\mid \eassign{n}{\dot E} \mid
\eassignstack{x}{\dot E} \\
\overline{\dot E } & ::= & \dot E \mid n,\overline{\dot E} \mid
\overline{\dot E}, \dot a

\end{array} \]

Semantic Defs

$\elang$ does not include any annotations. We remove structs from
$\elang$ because we can always statically convert expressions of the form
$\eamper{n:\tau}{f}$ into $n + n_f$, where $n_f$ is the statically
determined offset of $f$ within the struct. We ellide the semantics of
$\elang$ because it is self-evident and mirrors the semantics
$\lang$. The difference is that in $\elang$, only $\ebounds$ and
$\enull$ can step into an error state. All failed dereferences and
assignments would result in a stuck state and therefore we rely on the
compiler to explicitly insert checks for checked pointers.

Fig. <ref> and Fig. <ref>
shows the rules for the compilation judgment for expressions,

\[\Gamma;\rho \vdash e \gg \dot C, \dot a\]

The judgment is presented differently from the one in
Sec. <ref>, which was simplified for presentation purposes. First,
we remove $\Theta$ and $m$ because these
parameters are only used for checking and have no
impact on compilation. Second, the judgment includes two
outputs, a closure $\dot C$ and an atom expression $\dot a$, instead of
a single $\elang$ expression $\dot e$. $\dot C$ can be intuitively understood as a
partially constructed program or context. Whereas $\dot E$ is used for
evaluation, $\dot C$
is used purely as a device for compilation. As an example,
when compiling $(1 : \tint) \plus (2 : \tint)$,
we would first create a fresh variable $x$, and then produce two outputs:

\[    \dot C = \elet{x}{1 \plus 2}{\hole}\]

\[    \dot a = x\]

To obtain the compiled expression $\dot e$, we plug $\dot a$ into
$\dot C$ using the usual notation $\dot C[\dot a]$. We can also use $\dot C$ to represent runtime checks, which
usually take the form $\elet{x}{\dot c}{\hole}$, where $\dot c$
contains the check whose evaluation must not trigger $\ebounds$ or $\enull$ for the program to
continue (see Fig. <ref> for the metafunctions that create
those checks).

This unconventional output format enables us to separate the
evaluation of the term and the computation that relies on the term's
evaluated result. Since effects and reduction (except for variables) happen only
within closures, we can precisely control the order in which effects
and evaluation happen by composing the contexts in a specific order.
Given two closures $\dot C_1$
and $\dot C_2$, we write $\dot C_1[\dot C_2]$ to denote the meta
operation of plugging $\dot C_2$ into $\dot C_1$. We also use
$\dot C_{a;b;c}$ as a shorthand for $\dot C_a[\dot C_b[\dot C_c]]$. In
the C-Ind rule,
we first evaluate the expressions that correspond to $e_1$ and $e_2$
through $\dot C_1$ and $\dot C_2$, and then perform a null check and
an addition through $\dot C_n$ and $\dot C_3$. Finally, we dereference
the result through $\dot C_4$ before returning the pair $\dot C_4,\dot
x_4$, propagating the flexibility to the compilation rule that recursively
calls C-Ind.

Fig. <ref> shows the metafunctions that create
closures representing dynamic checks. These functions first examine
whether the pointer is a checked. If the pointer is unchecked, an empty closure $\hole$
will be returned, because there is no need to perform a check. For bounds
checking, there is a special case for NT-array pointers, where the
bounds are retrived from the shadow variables (found by
looking up $\rho$) on the stack  rather than
using the bounds specified in the type annotation. This is how we
achieve the same precise runtime behavior as $\lang$ in our compiled expressions.

Fig. <ref> shows the metafunctions related to
bounds widening. $\vdash_{extend}$ takes $\rho$,
a checked NT-array pointer variable $x$, and its bounds $(b_l,b_h)$ as inputs, and returns an
extended $\rho'$ that maps $x$ to two fresh variables $x_l$, $x_h$,
together with a closure $\dot C$ that initializes $x_l$ and $x_h$ to
$b_l$ and $b_h$ respectively. This function is used in the
C-Let rule to extend $\rho$ before compiling the body of the
$\elettext$ binding. The updated $\rho'$ can be used for generating
precise bounds checks, and for inserting expressions that can potentially
widen the upper bounds, as seen in the $\vdash_{widenstr}$
metafunction used in the C-Str compilation rule.

x_l, x_h =

ρ' = ρ[x ↦(x_l, x_h)]

Ċ = x_lb_lx_hb_h
ρxb_lb_hτcĊ, ρ'

x_l,x_h = ρ(x)

x_w =

Ċ = x_wx_h0x_h1

e ∉dom(ρ)

x_l,x_h = ρ(e)

x_a =

Ċ = x_aȧ ≤x_h0x_hȧ

Metafunctions for Widening

x =

Ċ = xȧ0

x_l,x_h = ρ(e)

x_cl,x_ch =

Ċ_cl = x_clx_l ≤ȧ0

Ċ_ch = x_chȧ ≤x_h0

e ∉dom(ρ)

x_l, x_h, x_cl,x_ch =

Ċ_l = x_lb_l

Ċ_h = x_hb_h

Ċ_cl = x_clx_l ≤ȧ0

Ċ_ch = x_chȧ ≤x_h0

e ∉dom(ρ)

x_l, x_h, x_cl,x_ch =

Ċ_l = x_lb_l

Ċ_h = x_hb_h

Ċ_cl = x_clx_l ≤ȧ0

Ċ_ch = x_chx_h ≤ȧ0

x_l,x_h = ρ(e)

x_cl,x_ch =

Ċ_cl = x_clx_l ≤ȧ0

Ċ_ch = x_chȧ ≤x_h0

e ∉dom(ρ)

x_l, x_h, x_cl,x_ch =

Ċ_l = x_lb_l

Ċ_h = x_hb_h

Ċ_cl = x_clx_l ≤ȧ0

Ċ_ch = x_chx_h ≤ȧ0

e ∉dom(ρ)

x_l,x_l',x_h,x_h' =

Ċ_1 = x_lb_lx_hb_h

Ċ_2 = x_l'b_l'x_h'b_h'

Ċ_3 = x_l' ≤x_l

Ċ_4 = x_h ≤x_h'

x_l',x_h' =ρ(e)

x_l,x_h =

Ċ_1 = x_lb_lx_hb_h

Ċ_2 = x_l' ≤x_l

Ċ_3 = x_h ≤x_h'

Metafunctions for Dynamic Checks

Γ;ρ⊢nτ ≫, n : τ

x : τ∈Γ
Γ;ρ⊢x ≫, x : τ

Γ;ρ⊢e ≫Ċ , ȧ : τ'
Γ;ρ⊢τe ≫Ċ, ȧ  : τ

Γ;ρ⊢e ≫Ċ_1, ȧ : 'τm

≫Ċ_1;b, ȧ : τm

Γ; ρ⊢e ≫Ċ_1, ȧ_1 :  τ_am

x_2 =

Ċ_2 = x_2ȧ_1

Γ;ρ⊢e ≫Ċ_1;n;b;2;w, x_2 :

Γ(y) = b_lb_hτ_a
x ∉(τ)

Γ; ρ⊢y ≫Ċ_1, ȧ_1 :

Ċ_2 = xȧ_1

Γ[x↦,y↦[b_lxτ_a]];ρ⊢e_3 ≫Ċ_3, ȧ_3 : τ

Γ;ρ⊢xye ≫Ċ_1;2;3,ȧ_3 : τ

[C-If ]
Γ; ρ⊢e ≫Ċ_1, ȧ_1 : τ

Γ; ρ⊢e_1 ≫Ċ_2, ȧ_2 : τ_2

Γ; ρ⊢e_3 ≫Ċ_3, ȧ_3 : τ_3

x_4 =

Ċ_4 = x_4ȧ_1Ċ_2[ȧ_2]Ċ_3[ȧ_3]

Γ; ρ⊢e_1e_2e_3 ≫Ċ_1;4, x_4 : τ_2 ⊔τ_3

Γ; ρ⊢x : (b_l,b_h)τc

b_h = 0 ⇒Γ' = Γ[x ↦(b_l,1)τc]

b_h ≠0 ⇒Γ' = Γ

Γ; ρ⊢x ≫Ċ_1, ȧ_1 : τ_1

Γ'; ρ⊢e_2 ≫Ċ_2, ȧ_2 : τ_2

Γ;ρ⊢e_3 ≫Ċ_3, ȧ_3 : τ_3

x_4 =

Ċ_4 = x_4ȧ_1Ċ_2;w[ȧ_2]Ċ_3[ȧ_3]
Γ;ρ⊢xe_1e_2 ≫Ċ_1;4, x_4 : τ_1 ⊔τ_2

(x∈(τ') ⇒e_1 ∈Bound)

Γ;ρ⊢e_1 ≫Ċ_1, ȧ_1 : τ_1

Ċ_3 = xȧ_1

Γ[x↦τ];ρ' ⊢e_4 ≫Ċ_4, ȧ_4  : τ_4
Γ;ρ' ⊢xe_1e_4 ≫Ċ_1;2;3;4,ȧ_4 : τ_4[τ_1 = ⇒x ↦e_1]

Γ;ρ⊢e ≫Ċ_1, ȧ_1 : τ

x_2 =

Ċ_2 = x_2xμ̇Ċ_1[ȧ_1]
Γ;ρ⊢xμe ≫Ċ_2, x_2 : τ

Ξ(f) = τ (x:τ) e

(∀e_i∈e  τ_i∈τ .  Γ; ρ⊢e_i ≫Ċ_i, ȧ_i  :
τ_i' ∧τ_i' ⊑τ_i[e / x]

x_f =

Ċ_f = x_ff(a)
Γ; ρ⊢f(e) ≫Ċ[Ċ_f] , x_f  : τ[e / x]

Γ;ρ⊢e_1 ≫Ċ_1, ȧ_1 : τm

x_2 =

Ċ_2 = x_2ȧ_1

Γ;ρ⊢e_1 ≫Ċ_1;n;2, x_2 : τ

Γ;ρ⊢e_1 ≫Ċ_1, ȧ_1 : b_lb_hτm

x_2 =

Ċ_2 = x_2ȧ_1
Γ;ρ⊢e_1 ≫Ċ_1;n;b;2,x_2 : τ

Ċ_1, ȧ_1 = ω

x_2 =

Ċ_2 = x_2ȧ_1
Γ; ρ⊢ω ≫Ċ_1;2, x_2 : ω

Γ; ρ⊢e_1 ≫Ċ_1, ȧ_1 :

Γ; ρ⊢e_2 ≫Ċ_2, ȧ_2 :

x_3 =

Ċ_3 = x_3ȧ_1 ȧ_2
Γ; ρ⊢Ċ_3, x_3 :

Γ; ρ⊢e_1 ≫Ċ_1, ȧ_1 : τm

Γ; ρ⊢e_2 ≫Ċ_2, ȧ_2 :

x_3, x_4 =

Ċ_3 = x_3ȧ_1 ȧ_2

Ċ_4 = x_4x_3

Γ; ρ⊢(e_1e_2) ≫Ċ_1;2;n;3;b;4 , x_4: τ

Γ; ρ⊢e_1 ≫Ċ_1, ȧ_1 : τm'

Γ; ρ⊢e_2 ≫Ċ_2, ȧ_2 : τ'

x_3 =

Ċ_3 = x_3ȧ_1ȧ_2

Γ; ρ⊢e_1e_2 ≫Ċ_1;2;n;3, x_3 : τ

Γ; ρ⊢e_1 ≫Ċ_1, ȧ_1 : τm'

Γ; ρ⊢e_2 ≫Ċ_2, ȧ_2 : τ'

x_3 =

Ċ_3 = x_3ȧ_1ȧ_2

Γ; ρ⊢e_1e_2 ≫Ċ_1;2;n;b;3,x_3 : τ

Γ; ρ⊢e_1 ≫Ċ_1, ȧ_1 : τm

Γ; ρ⊢e_2 ≫Ċ_2, ȧ_2 :

Γ; ρ⊢e_3 ≫Ċ_3, ȧ_3 : τ'

x_4, x_5 =

Ċ_4 = x_4ȧ_1 ȧ_2

Ċ_5 = x_5x_4x_3
Γ; ρ⊢(e_1 e_2)e_3 ≫Ċ_1;2;n;3;4;b;5 : τ

Γ; ρ⊢e_1 ≫Ċ_1, ȧ_1  :  Tm

D(T) = τ_0 f_0…; τ_j f; ...

x_2 =

Ċ_2 = x_2ȧ_1 j̇
Γ; ρ⊢e_1f ≫Ċ_2, x_2  : τ_fm

Γ;ρ⊢e ≫Ċ, ȧ : τ
Γ;ρ⊢e ≫Ċ, ȧ : τ

Compilation (Continued)