c432c98f7f
C only partially defines the order of evaluation of expressions. It also allows expressions to have nested assignments and control flow. This specification change revamps the description of checking of bounds declarations to account for these language features properly. The specification before handled undefined order of evaluation well, but did not handle sequential control-flow (the comma operator) or conditional control-flow (conditional expressions and logical Boolean operators) well. We specify checking using mutually-recursive functions that take C expressions and additional information about program state, and produce new information about program state after the expressions are evaluated. The information that is tracked includes contexts that map variables to bounds expressions, sets of sets of equivalent expressions, and pending variables (variables that have unordered assignments with respect to the current expression being checked). The functions may also produce an error if the meaning of the expression is undefined according to the C specification because of unordered assignments or uses of variables that are unordered with respect to assignments. This change also adds a concept of temporaries introduced/required by checking so that we can more easily describe bounds that use the value produced by an expression, as well as bounds of expressions with nested side-effects. It removes current_expr_value. This change describes some things that are already being done in the Checked C clang implementation (the use of temporaries and sets of sets of equivalent expressions). It also provides a design that can be used to check expressions with control flow. This design will replace the current implementation effort to use the clang CFG for checking expressions with control flow. There were two problems with the approach that used the clang CFG. First, it was difficult to explain at the source program level what was happening. Second, the clang CFG overspecifies the order of evaluation of expressions. The checking would not have signaled an error when the meaning of the expression was actually undefined. The clang CFG expression evaluation order isn't guaranteed to be used by the actual machine code. The order of evaluation could differ. This could potentially allow subtle order-of-evaluation issues to compromise the integrity of bounds. The new design projects against these kinds of issues. |
||
|---|---|---|
| .. | ||
| grammars | ||
| scripts | ||
| tables | ||
| .gitignore | ||
| Makefile | ||
| README.md | ||
| abstract.tex | ||
| c_syntax.tex | ||
| checked_c.sty | ||
| checkedc.bib | ||
| checks.tex | ||
| conclusion.tex | ||
| evaluation.tex | ||
| example.tex | ||
| hyperendnotes.sty | ||
| introduction.tex | ||
| listing-label.sty | ||
| overview.tex | ||
| propagation.tex | ||
| propagation_rules.tex | ||
| related_work.tex | ||
| tr02.tex | ||
README.md
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 and put Rscript on your path, as well as LaTeX.