Dynamic-semantics
A dynamic semantics of C.
We distinguish between pure (i.e. side-effect-free) expressions
and expressions that may have side effects.
We allow the latter to appear only in certain parts of statements,
and we put restrictions to ensure a predictable order of evaluation.
Pure expressions may be evaluated in any order;
we evaluate them left to right.
We formalize a big-step operational interpretive semantics.
To ensure the termination of the ACL2 mutually recursive functions
that formalize the execution of statements, function calls, etc.,
these ACL2 functions take a limit on the depth of the recursive calls,
which ends the recursion with an error when it reaches 0,
which is decremented at each recursive call,
and which is used as termination measure.
Thus, a proof of total correctness
(i.e. the code terminates and produces correct results)
involves showing the existence of sufficiently large limit values,
while a proof of partial correctness
(i.e. the code produces correct results if it terminates)
is relativized to the limit value not running out.
The limit is an artifact of the formalization;
it has no explicit counterpart in the execution state of the C code.
The current definition of this dynamic semantics
may not be completely accurate in terms of
execution of arbitrary C in the covered subset of C,
in particular in the treatment of arrays.
However, it is accurate for our current uses
(namely, supporting proof generation in ATC. This dynamic semantics is work in progress;
we plan to make it completely accurate
for all the covered subset of C.
Subtopics
- Exec-expr
- Execute an expression.
- Exec
- Mutually recursive functions for execution.
- Exec-expr-pure
- Execute a pure expression.
- Exec-arrsub
- Execute the array subscripting operation on expression values.
- Variable-resolution-preservation
- Preservation of variable resolution under execution.
- Init-value-to-value
- Turn an initialization value into a value of a given type.
- Apconvert-expr-value
- Array-to-pointer conversion [C17:6.3.2.1/3] on expression values.
- Execution-limit-monotonicity
- A monotonicity property of execution limits.
- Exec-memberp
- Execute a structure pointer member operation
on an expression value.
- Exec-stmt
- Execute a statement.
- Exec-address
- Execute & on an expression value [C17:6.5.3.2/1] [C17:6.5.3.2/3].
- Init-scope
- Initialize the variable scope for a function call.
- Exec-unary
- Execute a unary operation on an expression value.
- Exec-member
- Execute a structure member operation on an expression value.
- Exec-fun
- Execute a function on argument values.
- Exec-stmt-while
- Execute a while statement.
- Eval-iconst
- Evaluate an integer constant.
- Exec-binary-strict-pure
- Execute a strict pure binary operation on expression values.
- Variable-visibility-preservation
- Preservation of variable visibility under execution.
- Exec-expr-pure-list
- Execute a list of pure expression.
- Object-type-preservation
- Preservation of object types under execution.
- Eval-binary-strict-pure
- Evaluate a binary expression with a strict pure operator,
on two values, returning a value.
- Exec-block-item-list
- Execute a list of block items.
- Exec-indir
- Execute * on an expression value [C17:6.5.3.2/2] [C17:6.5.3.2/4].
- Exec-ident
- Execute a variable.
- Exec-block-item
- Execute a block item.
- Eval-cast
- Evaluate a type cast on a value.
- Frame-and-scope-peeling
- Functions and theorems about peeling frames and scopes.
- Exec-obj-declon
- Execute an object declaration.
- Exec-cast
- Execute a type cast on an expression value.
- Exec-const
- Execute a constant.
- Eval-unary
- Evaluate a unary operation that does not involve pointers,
on a value, returning a value.
- Exec-stmt-dowhile
- Execute a do-while statement.
- Pure-expression-execution
- Properties about the execution of pure expressions.
- Exec-initer
- Execute an initializer.
- Eval-const
- Evaluate a constant.
- Execution-without-function-calls
- Properties about execution without function calls.
