\documentclass{article}

\usepackage{url}

\usepackage{listings}

\usepackage{tabularx}

\usepackage{longtable}

\usepackage{titling}

\newcommand{\subtitle}[1]{%

\posttitle{%

\par\end{center}

\begin{center}\large#1\end{center}

\vskip0.5em}%

}

\begin{document}

\author{Jeremy Morse}

\title{A manual on some internals of ESBMC}

\subtitle{Caveat lector}

\maketitle

\tableofcontents

\section{Introduction and caveats}

This ``manual'' is supposed to be an introduction to how the ESBMC model

checkers internals are arranged and operate. It is not supposed to be a

comprehensive piece of documentation on the exact behavior of particular

functions or facilities; nor will it ever, ever be up to date. Exact

documentation on a specific function or method should be written in

doxygen in headers. The generated API reference is published online at

\url{https://esbmc.github.io/docs/api}; see the development guide at

\url{https://esbmc.github.io/docs/development/api-reference} for how to build

it locally.

When referencing portions of code from within this manual, I'll probably

end up referring to class names and methods within them. Source files and

line numbers are liable to change, whereas the code layout of the project

is the least likely to suffer significant churn. The location of such a

class or method should be obvious from the context, or discoverable with

grep. Numerous references will also be made to the \textit{Internal

representation}, or \textit{irep} of something. This refers to how some piece

of data is structured or stored; see the 'Misc' section for details.

A huge amount of the code base is derived from the CBMC project. CBMC is

open source (BSD 4-clause, ish), and available over SVN at

\url{http://www.cprover.org/svn/cbmc}. A large number of design decisions

are down to the development of CBMC; changes to ESBMC that cause

significant divergence from CBMC's design should be carefully thought

about, seeing how it's more mature than ESBMC. Likewise, code being

pulled in from CBMC should be examined to see whether it'll actually fit

into what ESBMC is doing nowadays.

All additional gunge, queries, complaints, to \url{jeremy.morse@gmail.com}

\section{Source tree structure}

In an order vaguely related to how ESBMC's execution order occurs, the

following describes the contents of directories in the source tree.

FIXME: This is ugly, make it a table.

\begin{description}

\item[docs] Directory for not-in-code documentation.

\item[papers] Self explanatory.

\item[scripts] Various scripts and auxiliary files related to building ESBMC

and dealing with things that aren't source files. Makefile

scripts and release/binary manipulating scripts.

\item[esbmc] Top-level model checking control code. Process entry point,

option handling, general direction and invocation of the rest

of the code base.

\item[langapi] Abstractions for handling input source files. Links a variety

of global functions up to input-language-appropriate routines.

Probably not massively necessary and could be ditched.

\item[ansi-c] Parser for ANSI-C software. Contains all code required to lex,

parse, store as an AST, typecheck, and link, an input file.

\item[ansi-c/cpp] C preprocessor - an import of the Portable C Compilers

preprocessor, adapted to do what ESBMC needs.

\item[ansi-c/headers] C langauge headers to override system headers.

\item[ansi-c/library] C language implementations of various code libraries

that we seek to model.

\item[cpp] Parser for C++ language. Code for all compilation steps of C++.

\item[cpp/library] Implementation / models of various C++ template libraries.

\item[big-int] Arbitrary length integer library. Used internally to avoid any

kind of problems modelling large machine integers using small

machine integers.

\item[goto-programs] Routines for general operations on GOTO instructions, as

well as all the code for converting a parsed AST into

GOTO instructions.

\item[pointer-analysis] Code for interpreting the execution of GOTO instructions

and the analysis of their effect upon pointer tracking.

Basically, a static analysis of pointer assignment and

reachability. Also, contains code for resolving pointer

indirection in dereferences.

\item[goto-symex] Symbolic execution of GOTO instructions into an SSA program.

\item[solvers] Encoding of SSA program into SMT solver logic, and solving of

the produced SMT formula.

\item[util] Miscellaneous functions, classes, and whatever to glue everything

else together.

\item[regression] Regression tests for various facets of ESBMC.

\end{description}

\section{Command line options}

What follows is a short description of each command-line option to ESBMC that

exists. All are prefixed with \url{--} when given. Some information is also

available by running \url{esbmc --help}.

\begin{longtable}{| p{.20\textwidth} | p{.80\textwidth} |}

\hline

Option & Description\\

\hline

inlining & Enables inlining of functions -- function calls are replaced with the

bodies of the called function. It's unclear when these occur.\\

\hline

program-only & Symbolically execute the program until we have an SSA program,

print the SSA program textually, then exit.\\

\hline

program-too & Like program-only, but don't exit, instead continue

verification.\\

\hline

function & Specify function to begin execution at. If a function takes arguments,

horrible undefined behavior occurs.\\

\hline

preprocess & Run the input source files through preprocessing, write the output

to stdout, then exit. Useful for debugging.\\

\hline

no-simplify & Disable simplification of expressions; effectively neuters

constant propagation so that no fact is statically determined to be true or

false, and we end up always exploring to the top of the unwind bound.\\

\hline

unwind & Takes an integer parameter. Specifies the general unwind bound to apply

to all loops in the program.\\

\hline

unwindset & Takes string parameter, a comma separate list of loopidnum:bound

pairs. Allows exact specification of a loop bound for a particular loop, see

the show-loops option.\\

\hline

z3-bv & Use Z3 solver in bitvector mode.\\

\hline

z3-ir & Use Z3 solver in integer mode.\\

\hline

boolector-bv & Use Boolector solver.\\

\hline

outfile & Output file to write an SMT formula to.\\

\hline

no-pointer-check & Disable all assertions related to pointers.\\

\hline

depth & Takes parameter n. Limit the maximum depth of the program to the

execution of n instructions.\\

\hline

no-div-by-zero-check & Disable divide-by-zero assertion checks.\\

\hline

no-unwinding-assertions & Disable unwinding assertions.\\

\hline

partial-loops & Disable unwinding assumptions.\\

\hline

memory-leak-check & Enable checking for memory leaks.\\

\hline

overflow-check & Enable integer overflow assertions.\\

\hline

no-assertions & Disable the checking of any assertion encoded in the program

with an \url{assert} function call.\\

\hline

minisat & Use the minisat sat solver.\\

\hline

16 & Model a 16 bit machine. Unlikely to work as this hasn't received any

maintenence, ever.\\

\hline

32 & Model a 32 bit machine. The default.\\

\hline

64 & Model a 64 bit machine. Will probably have hiccups involving pointer

widths.\\

\hline

little-endian & Model integers as being little endian. The default.\\

\hline

big-endian & Model integers as being big endian.\\

\hline

show-goto-functions & Print out all the functions and instructions in all the

input code.\\

\hline

show-value-sets & Print out the same data as show-goto-functions, but also

add the contents of the pointer tracking set (according to the static analysis)

at each instruction.\\

\hline

show-loops & Print out a list of loops, where they are in the source files,

and what loop ID number they have.\\

\hline

show-symbol-table & Print out a list of symbols and some simplified

information about them.\\

\hline

show-claims & Print a list of all assertions in the program.\\

\hline

claim & Takes integer argument identifying what assertion to check in the

program, from the list in show-claims. Disables all other assertions. Specify

the claim option multiple times to check multiple claims.\\

\hline

atomicity-check & During multithreaded exploration, verify that expressions

are executed atomically. Rewrites assignments to check that the variables on the

rhs are not modified between before the assignment and afterwards.\\

\hline

error-label & Check for reachability of a particular C label in the program.\\

\hline

version & Print the version of ESBMC.\\

\hline

lock-order-check & make assertions about correct operation of pthread

mutexes.\\

\hline

deadlock-check & Encode assertions checking that the program under test does not

deadlock.\\

\hline

string-abstraction & Enable an approximation of string operations. All string

operations only consider the lenght of data, rather than its contents.\\

\hline

no-slice & Disable slicing step.\\

\hline

qf\_aufbv & Print the SMT formula for the program to the file given in the

outfile option, in QF\_AUFBV logic.\\

\hline

qf\_auflira & Print the SMT formula for the program to the file given in the

outfile option, in QF\_AUFLIRA logic.\\

\hline

context-bound & Takes one integer parameter. Specifies the number of thread

context switches allowed during exploration. Defaults to infinite.\\

\hline

time-slice & How many time slice to permit during round-robin scheduling.\\

\hline

k-step & How many k-unrolls to make during k-induction.\\

\hline

no-por & Disable partial order reduction in multithreaded checking.\\

\hline

data-races-check & Check to see whether any concurrent reads/writes to a

variable are possible. Rewrites assignments to encode an assertion that fails

if an interleaving is found where either two threads can write to the same

variable at the ~same time, or can write while the other reads.\\

\hline

DFS & Perform depth first search scheduling of multithreaded code. The

default.\\

\hline

schedule & Perform a ``schedule'' scheduling of multithreaded code, encoding

all interleavings into one SSA program.\\

\hline

all-runs & Explore all interleavings in the program, even after a counterexample

is found.\\

\hline

timeout & Start a SIGALRM to time out and kill ESBMC in the future. See --help

for more details.\\

\hline

memlimit & Encode a resource limit to kill ESBMC if it uses too much memory.

See --help.\\

\hline

state-hashing & Enable state hashing. Attempts to hash program state in

multithreaded exploration and reduce duplicate states.\\

\hline

symex-trace & Print GOTO instructions as they are executed. Useful for

debugging.\\

\hline

round-robin & Enable round robin thread scheduling.\\

\hline

k-induction & Enable k-induction.\\

\hline

break-at & Takes integer parameter. Executes an x86 trap instruction when the

specified GOTO instruction is executed. This is the equivalent of putting a

breakpoint on it.\\

\hline

memstats & Cat /proc/self/status at the end of execution, to give details on

how many bytes of memory were used, and so forth.\\

\hline

dump-z3-assigns & Print all assignments to SMT symbols if a counterexample

is found.\\

\hline

symex-ssa-trace & Print SSA instructions as they are encoded. For debugging.\\

\hline

\end{longtable}

\section{Building}

A number of things are required for ESBMC to build. The first of these is a

C++ compiler and the associated headers and libraries. This is fundementally

an operating system dependant operation, but it tends to be well documented

on the internet of how to get started. Linux machines tend to have both gcc

and clang available, cygwin on Windows has gcc, the supported environment for

Macs is clang, I believe.

Once you have a C++ compiler, you require some libraries to build into it.

Currently the primary solver for ESBMC is Z3, for which Microsoft ship

precompiled binaries for Windows, Mac and Linux. Other solvers such as Minisat

and Boolector are available, but you might end up building those yourself.

After downloading some solving libraries, create a `SAT' directory anywhere

(say, \~/sat) and extract the libraries into it. Within that directory,

subdirectories should be named after the solver they contain --- the z3 dir

should contain a copy of Z3, for example. Within each solver directory, the

usual project layout is expected, i.e. directories named bin, lib, include,

and so forth.

Once you've installed solvers into these directories, add the environmental

variable \texttt{SATDIR64} or \texttt{SATDIR32} to your environment, pointing

at the SAT directory where the solvers are installed. (Chose 32 or 64 according

to what flavour of library you installed).

Finally, if you're planning on compiling the irep2 stuff right now, you need

to also install the \texttt{boost} libraries. These are package managed on

linux, in cygwin on windows, in macports on mac.

You're now ready to build: check out ESBMC over git:

\begin{quote}

\texttt{git clone git@github.com:jmorse/esbmc.git}

\end{quote}

For which you'll have to have a github account that can access ESBMC, and an

ssh key that can access your github account. See the github documentation for

more details.

Then, navigate into the ESBMC directory, and type make. Compilation

commands and errors will scroll by; if everything goes to plan, you'll end up

with a binary called 'esbmc' in the 'esbmc' directory of ESBMC. Rejoice.

If you only installed Z3 into the SAT directory, you'll run into errors

complaining that the other solvers don't exist. Open the file

\texttt{config.inc} in the top level directory of the ESBMC project, and

comment out the lines ``USE\_SOLVER\_\$\{x\}'', where \$\{x\} is the name of

a solver you haven't installed.

\section{Top level procedures}

Entry to the process starts (more or less) in the \url{doit} method of the

\url{cbmc_parseoptionst} object. Various command line options are checked

for validity, before the \url{get_goto_program} method invokes the

frontend parsers to compile input source code into an AST. The AST for the

entire environment (all source files and libraries) is stored in a

\url{contextt} object, containing a list of symbols and their AST value.

The contents of the \url{contextt} object is passed to the

\url{goto_convert} function, which produces a set of

\url{goto_functiont}s corresponding to each function in the source language.

Each function contains little more than a \url{goto_programt}, which

actually contain a list of instructions and some annotations.

With the set of GOTO functions, the \url{process_goto_program} method

applies the string abstraction transformation, the pointer analysis,

installs various pointer validity checks, and anything else that transforms

the source program into different instructions (such as LTL property monitors

or data race checking).

With these fixed-up goto functions, a \url{bmct} object is created and the

\url{run} method invoked on the functions. These functions are fed into a

\url{reachability_treet} object, the primary interface to symbolic

execution. Within the \url{bmct::run} method, the symbolic execution engine

is asked to run through instructions creating an SSA program; potentially

several times if there are multiple threads involved. A result itself is a

\url{goto_symext::symex_resultt} containing the SSA program container and

a count of how many assertions remain to be verified in the program.

The SSA program is then optionally sliced; see the 'Misc' section for details.

A solver object is then created, a subclass of \url{bmct::solver_base}

abstraction which solver to use. The SSA program is then fed to the solver,

which encodes it to SMT or whatever appropritate encoding it uses. It's then

asked to solve the equation, returning:

\begin{description}

\item[UNSATISFIABLE] The formula isn't satisfiable.

\item[SATISFIABLE] The formula is satisfiable.

\item[SMTLIB] A special case for printing the formula to a SMTLIB file.

\item[ERROR] Some error occured during solving.

\end{description}

Finally, if the formula is satisfiable, an error trace is created and printed.

Further details in the 'Misc' section.

\section{Source file parsing}

Code parsing is one of the untouched pastures of CBMC code, mostly. The ANSI-C

frontend is almost entirely like the original, while the C++ frontend has been

significantly developed by Manaus. The author is really familar with neither.

I'll talk about the ANSI-C frontend, then how the C++ frontend relates to it.

There are some significant conceptual steps involved. Firstly consider

the input and the output. Coming in is a C source file that must be preprocessed

and parsed - two fairly straightforward (although not easy) tasks. The top

levels of ESBMC then receive an AST representing the types and code structure

of the source file, which is more complex. The irep / structure of this data

is entirely undocumented and closely coupled between the parsers and the

\url{goto-programs} dir that converts it to GOTO instructions. However the

contents of this AST tends to be fairly high level language constructs,

for example \url{for} and \url{switch} statements. Refer to the method

\url{goto_convertt:convert} for an idea of what kind of constructs these

are. The majority of the source file parsing code deals with converting between

the parse tree and the AST.

The preprocessing stage is contained in the \url{c_preprocess} function.

In CBMC this used to offload preprocessing to the host preprocessor, however

our requirements have become more complicated since then. We now do

preprocessing using the preprocessor from the Portable C Compiler project

(which is BSD licensed). Unfortunately it wasn't designed with memory management

in mind, so ESBMC picks an output file, forks, calls the preprocessor to pump

outupt to the selected file, then exits the child process.

The complicated requirements from the preprocessor is that we generally want

code under test to have access to all headers on the host system, however we

also want to shoehorn our own types and functions in there --- for example the

glibc headers for assert have some obnoxious defines involved. Additionally

given how much lee-way standards give to libraries to define the format of

opaque data structures, we may need to define our own data structures to

avoid having to special case code for different operating systems. For example,

\url{pthread_t}'s, \url{pthread_mutex_lock}'s and so forth differ

between operating systems, and we currently rely on on using Linux' pthread.h

header. The current fix for this is to intercept \url{\#include} statements

and read in an ESBMC specific header file from \url{ansi-c/headers} rather

than the system headers.

We parse C in the normal way; a flex tokenizer is defined, and a yacc grammar

defined which translate the input C into a parse tree. This needs no special

description. A class (\url{ansi_c_convertt}) takes the parse tree and

makes a simple translation to the format of the AST. The bulk of the work then

lies in the \textit{typechecking} phase. Here, the nasty parts of C that are

context-dependant\footnote{i.e., all of them} are fixed up. Factors such as

integer promotion, operation signedness, and actual correctness are

considered, and various casts or extensions are inserted. The output is stored

as a set of symbols with associated AST values in a \url{contextt} object.

After parsing and compilation is linking. In the past CBMC has just

tacked all libraries available onto the end of a source file being compiled,

and that's all. Nowdays the libraries are pre-compiled into a binary

representation of GOTO instructions, and linked in after typechecking of C

code, by copying in any symbol referred to from the compiled source files

that are in the compiled library files.

Finally there's the initialization of C global and static lifetime variables.

Seeing how the GOTO language is only made up of assignments, ish, their

initialization must be made by assignments too. So, an initial 'main' GOTO

function is synthesized from the \url{c_main} and

\url{static_lifetime_init} functions. For each global variable an

assignment is emitted assigning the initial value to the global variable.

\section{GOTO programs}

This section covers both the GOTO program record itself, and the GOTO

instructions that make it up. Before launching into a description of these

records, it is important to understand that CBMC synthesizes the

\url{goto_programt} class from the \url{goto_program_templatet}

template. This can lead to the most confusing and obscure error messages

if you do not realise that you're manipulating a template. From a design

point of view, the reason for this appears to be so that the types of

the GOTO program body could be parameterised; a decision that is almost

entirely without merit.

The \url{goto_programt} class is more or less just a container for a

list of GOTO instructions (of class \url{goto_programt::instructiont}).

It stores \textbf{no} additional information. Instead, all of its methods

perform operations on the contained instructions. Most of these relate

to the creation, insertion, and deletion of instructions, recalculating

their contents to be consistent after such a modification, and a few

special cases such as determining the successor instructions from a

particular instruction,

The actual GOTO instruction class itself's primary piece of data comes in

two flavours -- the \url{code} member or the \url{guard} member.

These store the internal representation of what the body of the instruction

\textit{is}. Exactly what the instruction means depends on the \url{type}

field, described thus:

\begin{description}

\item[GOTO] Jump from the current instruction to the instruction in the

\url{targets} field. If \url{guard} is not true, then the jump is

conditional, depending on the evaluation of \url{guard}. If \url{guard}

is true the jump to the target occurs; if not, execution continues to the next

instruction.

\item[ASSUME] Encode an assumption, stored in the \url{guard} field, to the

solver.

\item[ASSERT] Encode an assertion, stored in the \url{guard} field, to the

solver.

\item[OTHER] Catch-all instruction for storing special cases, enumerated below.

Identified by what kind of irep is stored in the \url{code} field.

\begin{description}

\item[cpp\_delete] Also \url{cpp_delete[]}. Represents a deallocation of

some memory allocated by C++'s \url{new} or \url{new[]} operators.

\item[printf]\footnote{Yes, really} Represents a printf operation, for later

printing in a counterexample.

\item[decl] Represent declaration of a variable. Normally the declaration of

a variable is uninteresting as we only care about when it is initialized.

However in a loop where a variable is declared inside the loop block, it

transitions from being initialized to uninitialized when the loop iteration

finishes. Hence the importance of knowing where it is declared.

\item[nondet] Represent a nondeterministic value, from a \url{nondet_*}

function call.

\item[asm] Inline assembly statement. Mercifully ignored.

\item[typeid] Fetch a C++ type ID record, I belive.

\end{description}

\item[SKIP] An ignored instruction.

\item[LOCATION] Previously caused a ``location'' SSA step to be recorded for

future tracking of the code path of the counterexample. Now redundant.

\item[END\_FUNCTION] End instruction of a function. Not the same as a return,

which can occur anywhere, but actually the final instruction in the list of

instructions.

\item[ATOMIC\_BEGIN] Self explanatory.

\item[ATOMIC\_END] Self explanatory.

\item[RETURN] Record a return statement, identifying the expression to return.

Stored in a ``return'' irep in the \url{code} field.

\item[ASSIGN] Self explanatory. An ``assign'' irep is stored in the

\url{code} field, identifying the left and right hand sides.

\item[DECL] Unused. Probably used to be, or was intended to be, the decl

irep from the OTHER instruction.

\item[DEAD] Unused. Comments say ``marks the end-of-live of a local variable''.

\item[FUNCTION\_CALL] A function call record; stores a function call irep in

the \url{code} field, which in turn records the left hand side of the call,

the arguments, and the target.

\item[THROW] Throw record; not familiar with this, but it'll result in some

kind of an assignment to a record of what's been thrown, and a jump to somewhere

else.

\item[THROW\_DECL] Record the start of a catch block for a particular type

of variable.

\item[THROW\_DECL] Record the end of a catch block for a particular type

of variable.

\end{description}

All behaviors of GOTO programs are described by lists of these instructions.

Additional annotations are stored with each instruction, for example the

\url{function} and \url{location} fields identify where in the source

files the instruction came from. The \url{targets} list contains a list

of where the instruction can jump to (which should only ever contain zero or

one target instructions).

\url{loop_number} identifies a unique loop number for backwards

GOTO instructions. \url{target_number} is a numeric ID that labels

the instruction within a function. This don't actually do anything, but

is printed in the textual representation of GOTO instructions to indicate

the targets of GOTOs. There's also a set of local variable names, and

a globally unique instruction ID in \url{location_number}.

That's the substance of instructions; more information on the interpretation

of them lies in the symbolic execution section.

\section{Pointer analysis}

The essence of the pointer analysis is a tracking of what pointer variables

exist in the GOTO code, and what they might point at. This occurs more than once

during each run of ESBMC. A static analysis of the instructions first attempts

to establish a set of all (lexical) variables that a particular (lexical)

variable in a function may point at. Then during symbolic execution, a similar

tracking maintains a set of (``runtime'') variables that an actual pointer

\textit{does} point at.

The static analysis is initiated from the GOTO program processing code in the

\url{cbmc_parseoptionst} object. The high level analysis logic actually

lies in the \url{goto-programs} directory with the

\url{static_analysist} and \url{abstract_domain_baset}

classes. Code in these classes call abstract methods to perform transformations

between states as appropriate, over all GOTO instructions, to find a fixedpoint

where all values of the abstract domain have been discovered for all states.

The \url{value_set_analysist} and \url{value_set_domaint} classes

subclass the above two classes respectively to provide concrete

methods\footnote{I'm probably using all the wrong terminology here} for

tracking states of what pointer variables might point at. Most of the logic

itself lies in the latter class, storing both the actually tracking data

and forwarding transformation method calls to the appropriate objects.

A \url{value_set_domaint} contains only a \url{value_sett} object.

That itself contains the pointer tracking map, which is, unsuprisingly,

string based. The core type is the \url{value_sett::valuest} map,

where a string identifying a variable name maps to a

\url{value_sett::entryt}, which stores a set of variables that may be

pointed at and the offset into them.

The string key of each of these entries is important -- When interpreting

an assignment of a pointer value to a variable, we take the original variable

name being worked on and then interpret the left hand side, appending strings

to indicate /what/ part of the variable is being assigned to. To illustrate,

consider an assignment to the \url{bees} field of the following struct:

\begin{lstlisting}

struct face {

void *bees[4];

};

int main() {

struct face knees;

knees.bees[0] = NULL;

return 0;

}

\end{lstlisting}

Here, the fully qualified name of the variable we are assigning to is

\url{main::main::knees}, which becomes the starting point for the string

key in the value tracking map. We then interpret the left hand side of the

assignment, observe that we access the \url{bees} field, and so append the

text \url{.bees} to the key we are calculating. The next part of the left

hand side is the access to an element of the \url{bees} array, so we

append the text \url{[]} to the key we calculate. The final key is then

\url{main::main::knees.bees[]}. Observe that this approach allows every

variable in the program to have a unique key in the tracking map, except for

elements in an array --- we instead track what \textit{all} elements of the

array may point at, thus forming an overapproximation. The reasons for this

should be obvious.

The \url{value_sett::entryt} class is responsible for tracking the target

variables that a pointer may point at. It stores a map between certain variable

names and \url{value_sett::objectt}s. The presence of a variable name key

in the map indicates that the variable may be pointed at. The

\url{value_sett::objectt} object records whether the offset into the

variable that is pointed at is nondeterministic or constant; and if fixed,

then what the offset is. (NB: the actual implementation of this stores

\url{symbol} ireps as the map keys. To optimize this, it uses a (global)

pooling technique to assign each irep an ID number; see the

\url{value_sett::object_numbering} object. The ID number is then used

as the key into the \url{value_sett::entryt} map).

The \url{value_sett} class also provides operations required in the course

of the static analysis, most importantly the ability to interpret an instruction

to record and update the tracking described above. The class can also merge

value set records into each other. This follows the obvious merging procedure;

however when the two tracking sets being merged have a pointer variable

that points at different offsets into the same data object, the merged

tracking set records a nondeterministic offset into that data object. This

forms an overapproximation of the offset into an object that a pointer points

at.

No attempt is made to track what I'll term \textit{funky} pointer assignments.

For example, if code deconstructs a pointer variable into bytes, then

reconstructs these bytes into a pointer value, we are unable to track

what the resulting pointer value points at. How to address this in the future

is an open question. The byte array memory models of other tools neatly

side-step this issue.

The static analysis process eventually reaches a fixedpoint state where we

have established all possible variables that may be pointed at byte pointer

variables. The contents of this analysis is then handed to an object of

class \url{goto_program_dereference}. This proceeds to enumerate all

GOTO instructions and attempts to perform all dereferences in the instruction.

Pointer safety assertions are then generated (see the section on dereferencing)

and inserted as ASSERT instructions prior to the dereferencing instruction.

The pointer analysis executed during symbolic execution uses the same records

and functions as the static analysis. While the static analysis attempts to find

all the variables a pointer might point at across all code paths, the symex

tracking instead tracks the set of all variables a pointer may point at in the

course of the current code path. The variables it tracks are also ``L1 renamed''

(see the section on Symbolic Execution).

It is speculated that the static analysis can be removed, and assertions

encoded on-the-fly when dereferences occur during symbolic execution. While

this might be a valid optimization, the TACAS13 performance figures indicate

that execution time is dominated by symex, rather than the pointer

analysis\footnote{660 seconds ``GOTO processing'' compared to 20,000 seconds

``BMC time''}.

\section{Symbolic execution}

This portion of ESBMC is likely the most important in terms of theory,

complexity, and performance. The overall task is to take an input set of

GOTO functions, and interpret their instructions through an execution path

that is bounded according to the rules of BMC. Along the way, a \textit{Single

Static Assignment} (SSA) program is created recording the operations that

occured during the trace, for later checking. We must also make decisions

regarding the exploration of thread interleavings if multiple threads are

involved. To cover this section, we'll first look at the substance of the

SSA program, the concept of variable ``renaming'', the classes that make up

the symex process, how specific instructions are interpreted in single

threaded code including certain special case library functions,

and finally how all this relates to multi-threaded code.

\subsection{SSA programs}

The output from a single symex run through a program is contained in a

\url{symex_target_equationt} object. This primarily stores a list of

\url{symex_target_equationt::SSA_stept} objects, each of which represents

a single operation in program, sometimes referred to as a \textit{trace}.

The idea of SSA \textit{variables} will be discussed in the ``Variable

Renaming'' section. A SSA step comes in four flavours:

\begin{description}

\item[ASSIGNMENT] An assignment to a variable, with a symbol on the left hand

side, and an expression irep on the right hand side.

\item[ASSERT] Represent an assertion that an expression evaluates to true.

\item[ASSUME] Represent an assumption that an expression evaluates to true.

\item[OUTPUT] Record an output from the trace. This is essentially a wrapper

around a printf operation, that causes variables to be printed in the

course of printing a counterexample. I recommend not asking.

\end{description}

Numerous expression fields in a step object record the details of the above

operations, and are generally uninteresting for this discussion. The only

other data of note is that each step stores a \url{source} object, recording

where in the GOTO program the SSA step was generated.

\subsection{Variable renaming}

FIXME: this section is likely worded in a cack handed manner, requires

verification.

In the course of this manual there are numerous references to ``variables'',

without futher elaboration. The different aspects of variables that might be

referred to are below:

\begin{itemize}

\item The lexical variable, i.e. the variable name itself in a particular

context, not specific to a particular value or function activation.

\item The storage of a variable. The portion of memory reserved for storing

the value of a variable, either a global variable or memory allocated on the

stack if an automatically allocated variable in a function block.

\item The contents of a variable. Simply the value assigned to the variable

at a particular point in a program.

\end{itemize}

We name these different aspects \textit{level 0}, \textit{level 1}, and

\textit{level 2} respectively, often shortened to L0, L1, or L2. The reason

for this naming will become obvious shortly. An example is in order to fully

understand this. Consider the following function, and how it relates to the

pointer analysis:

\lstset{numbers=left}

\begin{lstlisting}

int anint;

void somefunc(int **beans) {

int *bears = *beans;

bears = &anint;

}

int main1(void) {

int wololololo = 0;

somefunc(&wololololo);

}

int main2(void) {

int ponies = 0;

somefunc(&ponies);

}

\end{lstlisting}

Here, if we consider the variable \url{beans} as an L0 variable, what it

points at is the set of all pointer targets it could potentially point at over

\textit{all} execution traces that are available in the program, including

all pointers that may be fed into \url{somefunc} at any point in the

program. This set includes the \url{wololololo} and \url{ponies}

variables. However if we consider \url{beans} as an L1 variable, what it

points at is whatever it may point at across the lifetime of its storage. Thus,

this depends on the path taken through the program -- the pointer may point

at \url{wololololo} or \url{anint} if \url{somefunc} is called from

\url{main1}, or alternately it may point at \url{ponies} or \url{anint}

if called from \url{main2}. However it may never potentially point at all

three. Finally, L2 variables are the actual value of the variable at a

particular point in the program, in our example the L2 \url{beans} pointer

may only ever point at a single value, which varies with both the path through

the program and the actual instruction location.

(These differences are important during the pointer analysis -- the static

analysis tracks pointers as L0 variables, the symex pointer tracking considers

L1 variables).

The reason for describing these variable kinds in terms of ``level''s, is

that we can consider a higher ``level'' of variable as representing a set of

lower level variables. Consider: if we call the \url{somefunc} function

in the above example three times, then the L0 \url{beans} variable exists

only once (as the function only exists once, so the lexical variable exists

once). However, three L1 instances of the L1 \url{beans} variable exist,

because the function was called three times and storage allocated for the

variable three times. In the same way, repeated assignment to a variable

in a function causes only one L1 name to exist (as only one piece of storage

is required), however multiple L2 variables exist as the variable has

multiple values during the execution of the function.

This then leads to the concept of ``renaming'', which is where we take a high

level variable and reference a lower level variable, appropriate to the context.

The two forms this can take are the transitions L0 to L1, and L1 to L2. In the

former case, we are taking a lexical variable and referring to the actual

storage of that variable. If the variable is global or of a static lifetime,

no additional data is added to the record, as the variable is always the

same piece of storage across the whole program execution. If the variable is

allocated local to a function call, then the L0 variable is annotated with

a unique \textit{activation record} number that identifies which invocation

of the function we are dealing with, and a thread number. The actual values

of these numbers are derived from the context of the renaming -- a thread number

is always available, and the activation record number of the function is always

available (as it's illegal to refer to a local variable outside of its

scope\footnote{Indirect pointer references are special, see later}).

When renaming an L1 variable to an L2 variable (effectively finding the value

currently stored by that L1 variable) we annotate the L1 variable with

a context switch ID number (see later sections) and an \textit{SSA assignment

number}. The assignment number is a monotonically increasing counter giving each

assignment to an L1 variable a unique identifier. So, if we assign to a

variable four times in a function, four L2 variables are created with

assignment numbers from one to four. This preserves the SSA constraint that we

only ever assign to a variable once. When renaming an L1 variable to L2 for the

purpose of using its value rather than making an assignment, we take the

assignment number to be the greatest assignment number for that L1 variable,

thus giving us the most recently assigned value of that L1 variable.

The final complexity to this situation, is that there is never a particular

object in ESBMC that represents any of these variables. Instead, variables

are identified by \textit{name}, stored in a symbol irep. Unsuprisingly, this

name is a string\footnote{Changes in the irep2 branch}. Multiple symbol irep

objects can contain the name of the same variable; creating a new variable

at any leve is as simple as creating a new name. An interesting side-effect

of this is that, following the procedure for renaming an L1 variable to L2,

if the L1 variable has never been assigned to then the greatest assignment

number is zero, and so references to unassigned variables read from assignment

number zero. (And because when we reach the solver level there is nothing

constraining the zeroth assignment of that variable, it's a free variable).

The format of this string is as follows:

\begin{quote}

full\_variable\_name@actv\_record!thread\_no\&cswitch\_no\#assign\_no

\end{quote}

Where \url{actv_record}, \url{thread_no}, \url{cswitch_no}, and

\url{assign_no} are replaced with the appropriate numbers. L0 names only

feature the variable name at the start; L1 names follow the above format

up until the ampersand; and L2 names use the full format. These names will

frequently crop up throughout almost all of ESBMC.

\subsection{Class overview}

The top level class for symex is \url{reachability_treet}. This contains,

at some level, all the state involved in the interpretation of GOTO

instructions. It also has the high level entry-to-symex methods like

\url{reachability_treet::get_next_formula}. Almost all the actual

logic in the class is related to the exploration of multithreaded interleavings,

everything symex related exists in lower level classes. The main piece of

data stored is a set of \url{execution_statet}'s, each of which stores

the full state of the program at a particular point in time.

The next two classes of interest are the \url{goto_symext} and its

subclass, \url{execution_statet}. The former contains all the logic

for GOTO interpretation and anything else only related to single threaded

execution, plus stores a few parameters for symex exploration. The latter

overrides a number of methods and injects logic for discovering when

multithreading operations must occur. The logic in this class only relates

to operations on the program state rather than interleaving exploration.

It stores a set of thread state objects, of class

\url{goto_symex_statet}, while some specialized information is broken out

into \url{execution_statet} for easy accessibility (such as what threads

are still running, atomic blocks, startup parameters). Global program state

is also stored here as a \url{value_sett} object to track pointer value

sets, and a \url{renaming::level2t} storing data on the latest assignments

to variables.

Within the \url{goto_symex_statet} class are all thread specific pieces

of data --- things like the program counter (in

\url{symex_targett::sourcet}) or the call stack (in

\url{goto_symex_statet::framet}). Significantly more state is stored

tracking the nondeterministic exploration of the program.

\url{goto_symex_statet::goto_statet} objects contain the whole program

state resulting from a short deterministic path, which are then merged together

where control paths merge\footnote{i.e., SSA phi functions} to form the

nondeterministic program trace. Various objects of \url{guardt} class

record the guard of a particular path being taken. Also stored is the count

of how many times a loop has been unwound in the current context, for the

purpose of loop bounding.

A \url{goto_symex_statet::framet} stores information related to a

particular stack frame / function activation. Mundane facts like the function

name, call site location, return value variable and the names of local variables

live here. More exciting items such as the set of executions to be merged in

the future, and the actvation record number for renaming, live here too.

There are also some hacks related to function pointer interpretation.

\subsection{Instruction interpretation}

The execution of instructions begins in the constructor for

\url{execution_statet} where the first thread is created and its program

counter set to the entry of the \url{main} function. From that point

onwards, the \url{goto_symext::symex_step} method is repeatedly called

to take the next instruction, interpret it, and move forwards. Some

instructions are handled in \url{execution_statet::symex_step},

which overrides its superclass and interprets multithreading specific

instructions. What follows is a narative of the (not quite) high level

operations performed during the interpretation of these instructions. Assume

that pointer dereferences are already handled as described in the section

on dereferencing --- actions specific to dereferencing will be mentioned

explicitly.

\subsubsection{Assign}

The substance of an assignment is a left hand side and right hand side. The

outcome we need is an SSA assignment, where we calculate a value with a type

n the right hand side, and then create a new left hand side variable that this

right hand side can be bound to. Clearly the assignment of a constant rhs to

a variable on the lhs is the simplest example of this. The operation becomes

more complex when the left hand side is an array index, a struct field,

a cast, or a nondeterminstic symbol due to pointer dereferencing. These

assignments must be rewritten into a simple variable assignment.

Performing this rewriting for an array index, we take the array variable

on the left hand side, and create a WITH operation that updates the desired

element with the right hand side. The assignment is rewritten to become an

assignment of this new value to the array variable. A similar operation

occurs for struct and union member assignments. For a nondeterministic

assignment we encode multiple deterministic assignments, one for each left

hand side, guarded by the appropriate guard. For assignment to a

\url{byte_extract} irep, we replace the right hand side with a

\url{byte_update} irep of the base data object on the left hand side.

The logic for all these operations begins in the

\url{goto_symext::symex_assign_rec} method and methods called from there.

Once we have an assignment in this form it is suitable for being an SSA

assignment. However all the variables are L0 variables, and need to be

renamed to refer to the appropriate piece of data or value. In the course

of the \url{goto_symext::symex_assign_symbol} method we call

\url{goto_symex_statet::rename} which identifies each variable on the

right hand side, renames to L1 (storage variables), and then to L2 (actual

values). The identifying numbers for these operations are pulled from the

top level \url{goto_symex_statet::framet} object of the most recently

called function, and the global L2 state tracking. One notable exception here

is that any operand to an \url{address_of} operation will only be renamed

to L1 --- we do not take the address of a particular variable value, but

instead the storage of the variable.

Once renamed, execution passes to \url{goto_symex_statet::assignment},

which performs accounting for the assignment on the L2 level. Specifically,

it bumps the SSA assignment number for the variable assigned to, so that future

uses of it will have the updated / recently assigned value. Additionally

we inspect the contents of the right hand side, and if it is a

sufficiently\textsuperscript{\texttrademark} constant value it is cached

in the program L2 state tracking, for constant propagation. Future rename

operations on that variable will have the variable replaced with its constant

value, rather than the variable itself. This method also passes the

assignment to be interpreted by the pointer analysis, which updates what the

left hand side may possibly point at.

Finally the \url{symex_target_equationt::assignment} method is called

to encode an SSA assignment, the program counter is incremented to point at the

next instruction, and we are done.

\subsubsection{Assert and assume}

ASSERT and ASSUME instructions are no-where near complex. Their substance

is the \url{guard} field of the GOTO instruction, which records the condition

that we are asserting or assuming. This expression is renamed as above to refer

to the appropriate L2 or L1 variables, and is passed to the expression

simplifier in case we can determine the truth of the operation statically.

The time and particularly memory benefits of determining this early are

significant.

The relevant methods are \url{goto_symext::claim} for ASSERT and

\url{goto_symext::assume} for ASSUME. These perform the above operations,

and then call \url{symex_target_equationt::assertion} and

\url{symex_target_equationt::assumption} respectively.

\subsubsection{Goto}

GOTO is likely the most complex of all the GOTO instructions, due to the sheer

amount of juggling of state that results. The substance of these is again

the \url{guard} field of the instruction, and a target instruction where the

GOTO is jumping to. There are two other factors that significant decisions

are made on --- firstly whether the GOTO is \textit{backwards} to an earlier

instruction in the program, and whether the guard of the instruction is (when

simplified) a constant true or false, or nondeterministic.

Consider the naive execution of some GOTO instructions. We start by executing

the first instruction in the program, moving on to the next, and repeating until

we reach the last instruction in the program. We can also handle loops by,

whenever we execute a GOTO that jumps backwards, following that jump and

executing from an earlier instruction in the program. This basic approach to

interpretation is what is employed by ESBMC, with all control flows more

complicated than the above encoded by making portions of the execution trace

nondeterministically executed.

The best way to describe this is through an example: below is a sample piece

of C, and an approximation of the corresponding GOTO code that it translates to.

\begin{lstlisting}

if (somebool) {

a = b;

} else {

a = c;

}

return a;

\end{lstlisting}

\begin{lstlisting}

IF somebool GOTO 1

ASSIGN a = b

GOTO 2

1: ASSIGN a = c

2: RETURN a

\end{lstlisting}

In the GOTO code for this program, there are two significant control flow

operations. The first instruction (line 1) is a GOTO instruction with a

guard\footnote{Even though it's a GOTO instruction, the textual representation

always begins with IF on account of it being a conditional GOTO.}, then the

RETURN instruction on line 6, with label ``2''.

As alluded to in previous subsections, we encode complicated and

nondeterministic executions of the program as small deterministic executions,

and then merge them together later. The storage for such an execution is a

\url{goto_symex_statet::goto_statet} object, which contains a copy of

the L2 variable assignment data, pointer tracking set, and a guard for whether

this path is executed. Taking our example, at the first GOTO instruction (line

1) we duplicate the current symex state into a \url{goto_statet}, with a

guard evaluating to true when the GOTO's guard is true. This object is then

placed in the stack frame's \url{framet} object, in the

\url{goto_state_map} field, as a piece of program state to be considered

in the future, at the target of the jump (line 4).

Proceding from that GOTO instruction, the guard of the currently executing

piece of code is adjusted to be true when the current instruction is reachable,

i.e. when the guard for the GOTO on line one is false.

We encode the assignment to \url{a} as normal. We then reach the next

GOTO on line 3, which is an unconditional jump to label 2. At this point we