Atj-mark-term
Mark the variables in a term as `new' or `old'.
- Signature
(atj-mark-term term vars-in-scope vars-used-after vars-to-mark-new)
→
(mv marked-term new-vars-in-scope)
- Arguments
- term — Guard (pseudo-termp term).
- vars-in-scope — Guard (symbol-listp vars-in-scope).
- vars-used-after — Guard (symbol-listp vars-used-after).
- vars-to-mark-new — Guard (symbol-listp vars-to-mark-new).
- Returns
- marked-term — Type (pseudo-termp marked-term).
- new-vars-in-scope — Type (symbol-listp new-vars-in-scope).
Marking a variable as `new' is always ``safe'',
because it is always safe to introduce a new Java local variable.
On the other hand, marking a variable as `old' requires care,
to prevent a Java local variable to be erroneously reused.
To understand this marking algorithm,
one has to keep in mind how ACL2 terms are translated to Java:
see atj-gen-shallow-term and companions.
This is a delicate algorithm:
a proof of correctness would be very beneficial.
Two conditions are necessary for reusing a variable:
(i) the variable must be in scope (i.e. exist and be accessible); and
(ii) the previous value of the variable must not be used afterwards.
The parameters vars-in-scope and vars-used-after
support the checking of these conditions.
The parameter vars-in-scope consists of the variables in scope
at the point where the term under consideration occurs.
At the top level (see atj-mark-formals+body),
it is intialized with the (unmarked) formal parameters
of the ACL2 function whose formal parameters and body are being marked:
indeed, the formal parameters of a function are in scope for the body.
As we descend into subterms, when we encounter a lambda expression,
we extend vars-in-scope with its (unmarked) formal parameters;
only the ones that are marked as `new' actually extend the scope,
while the ones marked as `old' were already in vars-in-scope.
The generated Java code evaluates functions' actual arguments
left-to-right:
thus, local variables introduced (for lambda expressions in) an argument
are generally (see exception shortly) in scope for successive arguments.
Therefore, vars-in-scope is threaded through the marking functions
(i.e. passed as argument and returned, possibly updated, as result).
When processing a lambda expression applied to arguments,
vars-in-scope is threaded first through the arguments,
and then through the body (which is evaluated after the arguments),
after augmenting it with the formal parameters.
The exception mentioned above is for if,
which is turned into a Java if
whose branches are Java blocks:
Java variables declared inside these blocks
have a more limited scope (namely, the respective block),
and therefore should not be added to the vars-in-scope
that is passed to mark terms after the if.
The variables introduced in the test of the if
are declared outside the branches' blocks,
and so they are threaded through.
The vars-in-scope resulting from marking the test of the if
is passed to mark both branches,
but their returned vars-in-scope is ignored.
The code for if is a bit more complicated
because of the special treatment of (if a a b) terms,
which are treated as (or a b):
the Java code generated for this case is a little different
(see atj-gen-shallow-or-call),
but the treatment of vars-in-scope
is essentially the same as just explained
(there is no `then' branch to mark, because it is the same as the test,
which has already been marked).
The parameter vars-used-after consists of the variables
whose current values are used ``after'' the term under consideration.
At the top level (see atj-mark-formals+body),
this is initialized with nil,
because no variables are used after evaluating the body of the function.
As we descend into subterms,
vars-used-after is extended as needed,
based on the ``neighboring'' subterms
that will be evaluated (in the generated Java code)
after the subterm under consideration.
In particular, when marking an actual argument of a function call,
vars-used-after is extended with all the free variables
of the actual arguments of the same function call
that occur after the one being marked;
recall that arguments are evaluated left-to-right
in the generated Java code.
The function atj-mark-terms,
which is used to mark the actual arguments of a function call,
augments vars-used-after with the free variables
in the cdr of the current list of arguments;
this is somewhat inefficient,
as the same free variables are collected repeatedly
as the argument terms are processed,
but terms are not expected to be too large in the near future;
this may be eventually optimized when needed.
Furthermore, as we traverse the arguments of a function call,
we augment the used variables with the ones that will occur
in the Java expressions generated for the preceding arguments;
see atj-vars-in-jexpr.
Calls of if are treated a little differently,
because the arguments are not evaluated left-to-right
in the generated Java code:
when marking the test, we augment vars-used-after
with all the free variables in the branches;
when marking either branch, we use the same vars-used-after
that was passed for the if,
because the two branches are independent.
The or form of if is treated slightly differently as usual,
but the essence is the same.
Unlike vars-in-scope, var-used-after is not threaded through;
it is simply passed down, and augmented as needed.
The body of a lambda expression is evaluated after its actual arguments:
thus, when marking the actual arguments of a lambda expression
we must augment vars-used-after
with the free variables of the lambda expression,
i.e. the free variables in the body minus the formal parameters.
As we mark the formal parameters of a lambda expression,
we need to mark in the same way
all the references to these variables in the body of the lambda expression.
For this purpose, we pass around a mapping, vars-to-mark-new,
from (unmarked) variables to markings:
this could be an alist from symbols to booleans,
but we isomorphically use lists (treated as sets) of symbols instead,
which are the variable marked as `new',
while the variables not in the list are marked as `old'.
When the term to be marked is a variable,
we look it up in this list, and mark it accordingly.
When the term to be marked is a quoted constant,
it is obviously left unchanged.
When the term to be marked is a function call,
we first treat the if (and or) case separately.
We mark the test, and after that the two branches.
The handling of vars-in-scope and vars-used-after for this case
has been explained above.
For all other function calls, which are strict,
we first mark the actual arguments,
treating vars-in-scope and vars-used-after
as explained above.
For calls of named functions, we are done at this point:
we put the named function in front of the marked arguments and return.
For calls of lambda expression,
we use the auxiliary function atj-mark-lambda-formals
to decide which formal parameters should be marked as `new' or `old'.
We mark the parameter as `old' (indicating that the variable can be reused)
iff the following three conditions hold.
The first condition is that the variable must be in scope;
note that variables have already been annotated with types at this point,
and so by testing variable names we also test their types,
which is needed for Java
(i.e. we could not reuse a Java variable of type Acl2Symbol
to store a value of type Acl2String).
The second condition is that the variable is not used
after the lambda call term, i.e. it is not in vars-used-after:
otherwise, we would overwrite something that was supposed to be used later,
with incorrect results in general.
The third condition is that the variable is not free
in any of the actual arguments that correspond to
the formal parameters of the lambda expression
that come just after the one being marked:
this is because, in the generated Java code,
the lambda variables are assigned one after the other,
and therefore we should not overwrite a variable
that may be needed afterwards.
For instance, consider a swap (let ((x y) (y x)) ...):
x cannot be reused
(even if it is in scope and not used after the let)
because it must be assigned to y after y is assigned to x
(Java does not support parallel assignment);
on the other hand, y could be reused,
if it is in scope and not used after the let,
because at the time of assigning to y
its (previous) value has already been assigned to x.
When analyzing the arguments of a call of a lambda expression,
we need to extend vars-used-after with
the free variables in the lambda expression
(i.e. the free variables in the body minus the formal arguments).
This is because the body of the lambda expression
is evaluated after the arguments of the call.
We store the extended list into vars-used-after-args.
But when we process the body of the lambda expression after that,
we go back to using vars-used-after,
which excludes the variables used in the lambda expression,
and only includes the variables used
after the call of the lambda expression.
Theorem: return-type-of-atj-mark-term.marked-term
(defthm return-type-of-atj-mark-term.marked-term
(b* (((mv ?marked-term ?new-vars-in-scope)
(atj-mark-term term vars-in-scope
vars-used-after vars-to-mark-new)))
(pseudo-termp marked-term))
:rule-classes :rewrite)
Theorem: return-type-of-atj-mark-term.new-vars-in-scope
(defthm return-type-of-atj-mark-term.new-vars-in-scope
(b* (((mv ?marked-term ?new-vars-in-scope)
(atj-mark-term term vars-in-scope
vars-used-after vars-to-mark-new)))
(symbol-listp new-vars-in-scope))
:rule-classes :rewrite)
Theorem: return-type-of-atj-mark-terms.marked-terms
(defthm return-type-of-atj-mark-terms.marked-terms
(b* (((mv ?marked-terms ?new-vars-in-scope)
(atj-mark-terms terms vars-in-scope vars-used-after
vars-used-in-jexprs vars-to-mark-new)))
(and (pseudo-term-listp marked-terms)
(equal (len marked-terms) (len terms))))
:rule-classes :rewrite)
Theorem: return-type-of-atj-mark-terms.new-vars-in-scope
(defthm return-type-of-atj-mark-terms.new-vars-in-scope
(b* (((mv ?marked-terms ?new-vars-in-scope)
(atj-mark-terms terms vars-in-scope vars-used-after
vars-used-in-jexprs vars-to-mark-new)))
(symbol-listp new-vars-in-scope))
:rule-classes :rewrite)
Subtopics
- Atj-mark-terms
