Technical Report Number 2 (#248)

The overall output of my work in 2017.

papers/dynamic_checks/.gitignore

@@ -0,0 +1,29 @@
+# Ignore LaTeX (and Latexmk) files
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+*.dvi
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+*.fdb_latexmk
+*.synctex
+*.synctex(busy)
+*.synctex.gz
+*.synctex.gz(busy)
+*.pdfsync
+**/auto/*
+.R*
+*.ent
+tr02.pdf

papers/dynamic_checks/Makefile

@@ -0,0 +1,32 @@
+# This Makefile uses latexmk as far as possible
+# because it understands LaTeX files better than
+# a hand-coded makefile. latexmk should be in any
+# modern Tex Live distribution.
+# Info: http://mg.readthedocs.io/latexmk.html
+
+.PHONY: tr02.pdf all clean cleanall pres
+
+all : tr02.pdf
+
+pres : $(addprefix scripts/,modifications_pres.pdf overheads_pres.pdf)
+
+clean :
+	latexmk -c
+
+cleanall :
+	latexmk -C
+	$(MAKE) -C scripts clean
+
+GEN_TEX_SCRIPTS=$(addprefix scripts/,bm_results_tab.tex bm_results_macros.tex)
+GEN_GRAPHS=$(addprefix scripts/,modifications.pdf overheads.pdf)
+GEN_RESULTS=$(GEN_TEX_SCRIPTS) $(GEN_GRAPHS)
+
+tr02.pdf : $(GEN_RESULTS)
+	latexmk -pdf -use-make tr02.tex
+
+scripts/%.pdf : scripts
+	$(MAKE) -C scripts $(@F)
+scripts/%.tex : scripts
+	$(MAKE) -C scripts $(@F)
+
+

papers/dynamic_checks/README.md

@@ -0,0 +1,9 @@
+# Putting the Checks into Checked C
+## Checked C Technical Report Number 2
+
+This document is current as of October 2017, and omits a description of null-terminated pointers.
+
+### Building
+
+To build this document fully, you'll need to install [R](https://www.r-project.org) and put `Rscript` on your path, as well as LaTeX.
+

papers/dynamic_checks/abstract.tex

@@ -0,0 +1,24 @@
+Checked C is an extension to C that aims to provide a route for
+programmers to upgrade their existing C programs to a safer language
+without losing the low-level control they enjoy. Checked C currently
+only addresses unsafe code with spatial memory violations such as
+buffer overruns and out-of-bounds memory accesses. \\[1em]
+
+Checked C addresses these memory safety problems by adding new pointer
+and array types to C, and a method for annotating pointers with
+expressions denoting the bounds of the objects they reference in
+memory. To ensure memory safety, the Checked C compiler uses a mixture
+of static and dynamic checks over these additions to the C language. \\[1em]
+
+This Technical Report concerns these Dynamic Checks, and the
+algorithms and infrastructure required to support them, including: the
+soundness property Checked C is aiming to preserve, propagation rules
+for bounds information, and the code generation algorithm for the
+checks themselves. This report includes an evaluation of these dynamic
+bounds checks, their overhead, and their interaction with a
+state-of-the-art optimizer. 
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "tr02"
+%%% End:

papers/dynamic_checks/c_syntax.tex

@@ -0,0 +1,77 @@
+\chapter{C Syntax}
+\label{app:c-syntax}
+
+This appendix contains a definition of the relevant parts of C Syntax
+for this report. This is based on the C11 Specification, but written
+with mathematical symbols rather than ASCII text.
+
+\begin{align*}
+  \text{LValue Expressions} \\*
+  e_l \gis {} & x  \tag*{Variables} \\
+  \gor {} & \deref e_v \tag*{Dereference} \\
+  \gor {} & e_v[e_v] \tag*{Index} \\
+  \gor {} & e_l \member m \tag*{Struct Member Access} \\
+  \gor {} & e_v \arrow m \tag*{Pointer Member Access} \\[1em]
+%
+\text{Value Expressions} \\*
+  e_v \gis {} & \addrof e_l \tag*{Address-of} \\
+  \gor {} & e_l \assign e_v \tag*{Assignment} \\
+  \gor {} & e_l \compassign e_v \tag*{Compound Assignment} \\
+  \gor {} & e_l \inc \mathrel{\mid} \inc e_l \tag*{Increment} \\
+  \gor {} & e_l \dec \mathrel{\mid} \dec e_l \tag*{Decrement} \\
+  \gor {} & e_v \member m \tag*{Struct Member Access} \\
+  \gor {} & e_v , e_v \tag*{Comma Expression} \\
+  \gor {} & e_v \binop e_v \tag*{Binary Operation} \\
+  \gor {} & e_v \mathrel{R} e_v \tag*{Binary Relational Operation} \\
+  \gor {} & \unop e_v \tag*{Unary Operation} \\
+  \gor {} & e_v(\overline{e_v}) \tag*{Function Call} \\
+  \gor {} & (t)e_v \tag*{Cast} \\
+  \gor {} & e_v \mathrel{?} e_v : e_v \tag*{Conditional Operator} \\
+  \gor {} & l \tag*{Literal Value} \\
+  \gor {} & e_l \tag*{Lvalue \& Array Conversion} \displaybreak\\[1em]
+  % 
+  \text{Binary Operators} \\*
+  \binop \gis {} & + \tag*{Addition} \\
+  \gor {} & - \tag*{Subtraction} \\
+  \gor {} & * \tag*{Multiplication} \\
+  \gor {} & / \tag*{Division} \\
+  \gor {} & \% \tag*{Modulus} \\
+  \gor {} & \& \tag*{Bitwise AND} \\
+  \gor {} & \mid \tag*{Bitwise OR} \\
+  \gor {} & \wedge \tag*{Bitwise XOR} \\
+  \gor {} & \gg \tag*{Bitwise Shift Right} \\
+  \gor {} & \ll \tag*{Bitwise Shift Left} \\[1em]  
+  % 
+  \text{Relational Operators} \\*
+  R \gis {} & \&\& \tag*{Logical AND} \\
+  \gor {} & \mid\mid \tag*{Logical OR} \\
+  \gor {} & \mathord{==} \tag*{Equality} \\
+  \gor {} & \mathord{!=} \tag*{Negated Equality} \\
+  \gor {} & \mathord{>} \mathrel{\mid}
+             \mathord{\ge} \mathrel{\mid}
+             \mathord{<} \mathrel{\mid}
+             \mathord{\le} \tag*{Comparison} \\[1em]
+  % 
+  \text{Unary Operators} \\*
+  \unop \gis {} & + \tag*{Unary Plus} \\
+  \gor {} & - \tag*{Numerical Negation} \\
+  \gor {} & \sim \tag*{Bitwise Negation} \\
+  \gor {} & ! \tag*{Logical Negation} \\[1em]
+  %
+  \text{Literals} \\*
+  l \gis {} & \mathtt{NULL} \tag*{Null Pointer Literal} \\
+  \gor {} & \mathrm{integers} \tag*{Integer Literals} \\
+  \gor {} & \mathrm{floats} \tag*{Float Literals} \\
+  \gor {} & \{ l , \dots \} \tag*{Array \& Struct Literals} \\[1em]
+  %
+  \text{Types} \\*
+  t \gis {} & \dots \\[1em]
+  %
+  \text{Struct Members} \\*
+  m \gis {} & \dots \\
+\end{align*}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "tr02"
+%%% End: