Atc-ensure-formals-not-lost
Ensure that no affected formals are lost.
- Signature
(atc-ensure-formals-not-lost bind-affect
fn-affect fn-typed-formals fn wrld)
→
erp- Arguments
- bind-affect — Guard (symbol-listp bind-affect).
- fn-affect — Guard (symbol-listp fn-affect).
- fn-typed-formals — Guard (atc-symbol-varinfo-alistp fn-typed-formals).
- fn — Guard (symbolp fn).
- wrld — Guard (plist-worldp wrld).
If the body of a non-recursive function fn
includes an mv-lets or a let
that affects a formal of fn of pointer or array type,
or a formal of integer type that represents an external object,
that formal must be among the variables affected by fn.
If the body of a recursive function fn
includes an mv-lets or a let
that affects a formal of fn of any type,
that formal must be among the variables affected by fn.
In other words, no modification of formals must be ``lost''.
The case of formals of pointer or array types is clear,
because it means that objects in the heap are affected.
The case of formals of integer type that represent external objects
is also clear, as that object is globally accessible.
The case of formals of non-pointer non-array types
applies to recursive functions
because they represent loops,
which may affect local variables in the function where they appear.
This ACL2 function ensures that no formals are lost in the sense above.
The parameter bind-affect consists of
the variable affected by the mv-let or let.
The parameter fn-affect consists of
the variables purported to be affected by fn.
We go through the elements of bind-affect
and check each one against the formals of fn,
taking into account the information about the formals
and whether fn is recursive.
Definitions and Theorems
Function: atc-ensure-formals-not-lost
(defun atc-ensure-formals-not-lost
(bind-affect fn-affect fn-typed-formals fn wrld)
(declare
(xargs :guard (and (symbol-listp bind-affect)
(symbol-listp fn-affect)
(atc-symbol-varinfo-alistp fn-typed-formals)
(symbolp fn)
(plist-worldp wrld))))
(let ((__function__ 'atc-ensure-formals-not-lost))
(declare (ignorable __function__))
(b*
(((reterr))
((when (endp bind-affect)) (retok))
(var (car bind-affect))
(info (cdr (assoc-eq var fn-typed-formals)))
((when (and info
(or (irecursivep+ fn wrld)
(type-case (atc-var-info->type info)
:pointer)
(type-case (atc-var-info->type info)
:array)
(atc-var-info->externalp info))
(not (member-eq var fn-affect))))
(reterr
(msg
"When generating C code for the function ~x0, ~
the formal parameter ~x1 is being affected ~
in an MV-LET or LET term, ~
but it is not being returned by ~x0."
fn var))))
(atc-ensure-formals-not-lost
(cdr bind-affect)
fn-affect fn-typed-formals fn wrld))))
