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
- Mutually recursive functions for execution.
- Exec-arrsub
- Execute the array subscripting operation on expression values.
- Exec-expr-pure
- Execute a pure expression.
- Exec-expr-asg
- Execute an assignment expression.
- Init-value-to-value
- Turn an initialization value into a value of a given type.
- Exec-memberp
- Execute a structure pointer member operation
on an expression value.
- Apconvert-expr-value
- Array-to-pointer conversion [C17:6.3.2.1/3] on expression values.
- Exec-address
- Execute & on an expression value [C17:6.5.3.2/1] [C17:6.5.3.2/3].
- Exec-member
- Execute a structure member operation on an expression value.
- Init-scope
- Initialize the variable scope for a function call.
- Exec-unary
- Execute a unary operation on an expression value.
- Exec-fun
- Execute a function on argument values.
- Exec-block-item
- Execute a block item.
- Eval-iconst
- Evaluate an integer constant.
- Exec-binary-strict-pure
- Execute a strict pure binary operation on expression values.
- Exec-expr-pure-list
- Execute a list of pure expression.
- 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-expr-call-or-pure
- Execute a function call or a pure expression.
- Exec-stmt-while
- Execute a while statement.
- Exec-stmt
- Execute a statement.
- Exec-ident
- Execute a variable.
- Eval-cast
- Evaluate a type cast on a value.
- Exec-cast
- Execute a type cast on an expression value.
- Eval-unary
- Evaluate a unary operation that does not involve pointers,
on a value, returning a value.
- Exec-const
- Execute a constant.
- Exec-initer
- Execute an initializer.
- Exec-expr-call-or-asg
- Execute a function call or assignment expression.
- Eval-const
- Evaluate a constant.
- Exec-expr-call
- Execution a function call.
