|
|
|---|
|
|
|
|---|
Execute an expression.
(exec-expr e compst fenv limit) → (mv eval new-compst)
We return an optional expression value,
and a possibly updated computation state.
The optional expression value is
We support the execution of expressions whose order of evaluation is determined by [C17] or does not matter; we characterize this subset of the expressions conservatively, returning errors on expressions outside the characterization. As noted in exec-expr-pure, we are in the process of moving the code from there to here, and we will eventually eliminate exec-expr-pure; as we move the code here, we also generalize it in the sense of supporting the execution of more expressions, namely ones that are not pure but have a deterministic order of evaluation.
Variables and constants are always deterministic, so they are supported in all cases.
An array subscript expression involves two sub-expressions, whose order of evaluation is unspecified. So we require both of them to be pure, so that the order of evaluation does not matter. We execute the first one before the second one, but we could as well do the opposite, since the computations state does not change.
In a function call,
the order of evaluation of the function and arguments is not specified.
In our current abstract syntax,
the function sub-expression is always pure;
we require all the argument expressions to be pure.
Thus the order of evaluation of function and arguments does not matter.
We use exec-expr-pure-list for the arguments
(but we plan to use a new function
If the expression is a function call, its arguments must be all pure expressions; if they were not, they might modify the function-valued expression. We execute the arguments and then the function.
A member or unary expression is always deterministic, because it has a single sub-expression.
For now we do not support pre/post-increment/decrement expressions.
A cast expression is always deterministic in our current C subset, because the type name does not undergo any execution currently.
For a binary expression with a strict pure operator, we require the two sub-expressions to be pure, because the order of evaluation is not specified; we evaluate the left one before the right one, but it makes no difference because the computation state does not change.
Non-strict binary expressions must be pure for now, but we plan to relax this, since the order of evaluation is determined. We delegate their execution to exec-expr-pure for now.
If the binary expression is a (simple, not compound) assignment,
the left-hand side must be a pure lvalue expression;
if it were not pure,
it could potentially change the value of the right-hand side,
if evaluated before the right-hand side,
so it is conservatively safe to require the left-hand side to be pure.
We perform array-to-pointer conversion [C23:6.3.3.1]
on the result of evaluating the left-hand side;
this must yield an expression value with an object designator.
The right-hand side must be a pure expression (lvalue or not),
but if the left-hand side is just an identifier,
then we allow the right-hand side to be any supported expression.
The latter relaxation is justified by the fact that,
if the left-hand side is a variable,
it the object that it designates is not affected
by any side effect of the right-hand side
(see variable-resolution-preservation):
it is always the same variable,
whose value may be affected by the right-hand side,
but its value is not used for the assignment,
as it is overwritten by the assignment.
Array-to-pointer conversion [C23:6.3.3.1] is applied
to the result of evaluating the right-hand side,
which must return an expression value (not
The remaining binary expressions are compound assignments. They are not supported for now.