bil.tex

\documentclass[11pt]{article}
\usepackage{amsmath,amssymb}
\usepackage{supertabular}
\usepackage{geometry}
\usepackage{ifthen}
\usepackage{alltt}%hack
\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm}
\usepackage{color}

\begin{document}
\include{ott}

\title{A formal specification for BIL: BIL Instruction Language}
\maketitle

\tableofcontents
\clearpage

\section{Introduction}
\label{sec:intro}

This document describes the syntax and semantics of BAP Instruction
Language.  The language is used to represent a semantics of machine
instructions. Each machine instruction is represented by a BIL program
that captures side effect of the instruction.

\section{Syntax}
\label{sec:syntax}

\subsection{Metavariables}
\label{sec:meta}

We define a small set of metavariables that are used to denote
subscripts, numerals and string literals:

\ottmetavars

\subsection{BIL syntax}

BIL program is reperesented as a sequence of statements. Each
statement performs some side-effectful computation.

\ottgrammartabular{
\ottbil\ottinterrule
}

\ottgrammartabular{
\ottstmt\ottinterrule
}

BIL expressions are side-effect free. Expressions include a usual set
of operations on bitvectors, like arithmetic operations and converting
bitvectors of one size to bitvectors of another size (casting in BIL
parlance).  We write $[e_1/var]e_2$ for the capture-avoiding
substitution of $e_1$ for free occurances of $var$ in $e_2$

\ottgrammartabular{
\ottexp\ottinterrule
}

\ottgrammartabular{
\ottvar\ottinterrule
}

\ottgrammartabular{
\ottbop\ottinterrule
\ottaop\ottinterrule
\ottlop\ottinterrule
\ottuop\ottinterrule
\ottendian\ottinterrule
\ottcast\ottinterrule
}

The type system of BIL consists of two type families - immediate
values, indexed by a bitwidth, and storagies (aka memories), indexed
with address bitwidth and values bitwidth.

\ottgrammartabular{
\otttype\ottinterrule
}

\subsection{Bitvector syntax}
\label{sec:bitvector}

We define a type of {\em words}, which are concrete bitvectors
represented by a pair of value and size.  Many operations on words are
required by the semantics and are listed below.

Operations marked with \verb|sbv| are signed. All other operations are
unsigned (if it does matter).  Operations \verb|ext| and \verb|exts|
performs extract/extend operation. The former is unsigned (i.e., it
extends with zeros), the latter is signed. This operation extracts
bits from a bitvector starting from $\mathit{hi}$ and ending with
$\mathit{lo}$ bit (both ends included). If $\mathit{hi}$ is greater
than the bitwidth of the bitvector, then it is extended with zeros
(for \verb|ext| operation) or with a sign bit (for \verb|exts|)
operation.

\ottgrammartabular{
\ottword\ottinterrule
}

\subsection{Value syntax}
\label{sec:values}

Values are syntactic subset of expressions. They are used to represent
expressions that are not reducible.

We have three kinds of values --- immediates, represented as
bitvectors; unknown values and storages (memories in BIL parlance),
represented symbolically as a list of assignments:

\ottgrammartabular{
\ottval\ottinterrule
}

\subsection{Context syntax}
\label{sec:context}

Contexts are used in the typing judgments to specify the types of all
variables. While each variable is annotated with its type, the context
ensures that all uses of a given variable have the same type.

\ottgrammartabular{
\ottgamma\ottinterrule
}

\subsection{Formula syntax}
\label{sec:formula}

The following syntax is used to specify symbolic formulas in premises
of judgments.

We use $\Delta$ to denote set of bindings of variables to values. The
$\Delta$ context is represented as list of pairs. We write
$(var,v) \in \Delta$ to indicate that the value $v$ is the right-most
binding of $var$ in $\Delta$.  Additionally, we write
$\mathsf{dom}(\Delta)$ for $\Delta$'s {\em domain} (the set of
variables for which it contains values).

We also add a small set of operations over natural numbers, like
comparison and arithmetics. Natural numbers are mostly used to reason
about sizes of bitvectors, that's why they are often referred as
$\mathit{sz}$.

We also add syntax for equality comparison for values and variables.


\ottgrammartabular{
\ottdelta\ottinterrule
}

\ottgrammartabular{
\ottformula\ottinterrule
}

\ottgrammartabular{
\ottnat\ottinterrule
}

\subsection{Instruction syntax}
\label{sec:insn}

To reason about the whole program we introduce a syntax for
instruction. An instruction is a binary sequence of $\mathit{w_2}$
bytes, that was read by a decoder from an address $\mathit{w_1}$. The
semantics of an instruction is described by the $\mathit{bil}$ program.

\ottgrammartabular{
\ottinsn\ottinterrule
}

\clearpage

\section{Typing}
\label{sec:typing}

This section defines typing rules for BIL programs.  We define four
judgements: $[[G |- bil is ok]]$ for programs, $[[G |- s is ok]]$ for
statements, $[[G |- e :: t]]$ for expressions, and $[[G is ok]]$ for
contexts.

BIL statement-level variables represent global state, and are
implicitly declared at their first use.  While variables carry their
type with them, it is still necessary to track them in a context
during type checking.  This is required to rule out programs like:
\begin{verbatim}
if (foo) then {x:imm<1> = 0} else {x:imm<32> = 42};
bar
\end{verbatim}
Such a program would leave the type associated with {\tt x} unclear in
{\tt bar}.  This is ruled out because the typing rules are set up such
that $[[G |- bil is ok]]$ implies $[[G is ok]]$, which requires that
each variable has a single type.

\ottdefnstypingXXstmt

\ottdefnstypingXXexp

\ottdefnstypingXXtype

\ottdefnstypingXXgamma

\clearpage


\section{Operational semantics}

\subsection{Model of a program}

Program is coinductively defined as an infinite stream of program
states, produced by a step rule. Each state is represented with a
triplet $(\Delta, w, var)$, where $\Delta$ is a mapping from variables
to values, $w$ is a program counter, and $var$ is a variable
denoting currently active memory.

The \verb|step| rule defines how a machine instruction is
evaluated. We use ``magic'' rule \verb|decode| that fetches
instructions from the memory and decodes them to a BIL program.

The BIL code is evaluated using reduction rules of statements (see
section \ref{sec:sema:stmt}). Then the program counter is updated with
the $w_3$, that initially points to a byte following current instruction.

\ottdefnsprogram

\section{Semantics of statements}
\label{sec:sema:stmt}

The reduction rule defines transformation of a state for each
statement. The state of the reduction rule consists of a pair
$(\Delta,w)$, where $\Delta$ is a mapping from variables to values and
$w$ is an address of a next instruction.

Two statements affect the state: \verb|Move| statement introduces new
$var \leftarrow v$ binding in $\Delta$, and \verb|Jmp| affects
program counter.

The \verb|if| and \verb|while| instructions introduce local control
flow.

There is no special semantics associated with \verb|special| and
\verb|cpuexn| statements.

\ottdefnsreduceXXstmt


\section {Semantics of expressions}
\label{sec:sema:exp}

This section describes a small step operational semantics for
expressions. A symbolic formula $\Delta \vdash e \rightarrow e' $
defines a step of transformation from expression $e$ to an expression
$e'$ under given context $\Delta$.

A well formed (well typed) expression evaluates to a value expression,
that is syntactic subset of expression grammar (see
section \ref{sec:values}).

A value can be either an immediate, represented by a bitvector, a
unknown value, or a memory storage.

A memory storage is represented symbolically as a sequence of
storages to the originally undefined memory. Each storage
operation of size greater than 8 bits is desugared into a sequence of
8 bit storages in a big endian order.

A load operation will first reduce all sub expressions of a memory
object to values and then recursively destruct the object until one of
the following conditions is met:


\begin{description}
\item[load-byte:] if the memory object is a storage of a \verb|value|
  to an immediate (known) address that we're trying to load then the
  load expression is reduced to \verb|value|.
\item[load-un-memory:] if the memory object is an \verb|unknown| value,
  then the load expression evaluates to \verb|unknown|.
\item[load-un-addr:] if the memory object is a storage to
  \verb|unknown| value address then load expression evaluates to
  \verb|unknown|.
\end{description}

This section also defines $\Delta \vdash e_1 \leadsto^{*} e_2$.  This relation
is the reflexive, transitive closure of $\leadsto$.  It is useful to describe
reductions that may take many steps.  For example, in the evaluation rules for
statements, it is often necessary to evaluate an expression completely to a
value.  The $\leadsto^{*}$ relation is used to allow reductions that take an
indeterminate number of individual $\leadsto$ steps.  Such a derivation can be
built with repeated use of the $\ottdrulename{reduce}$ rule.

Some evaluation rules depend on the type of a value. Since there are two canonical
forms for each type, we avoid duplicating each rule by defining the following metafunction:

\medskip

\ottfundefncomputeXXtype

\ottdefnsreduceXXexp

\ottdefnshelpers

\ottdefnsmultistepXXexp



\end{document}