Atc-gen-outer-bindings-and-hyps
Generate the outer bindings,
pointer hypotheses,
pointer substitutions,
and lemma instantiation,
for a correctness theorem.
- Signature
(atc-gen-outer-bindings-and-hyps typed-formals
compst-var fn-recursivep prec-objs)
→
(mv bindings hyps subst instantiation)
- Arguments
- typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).
- compst-var — Guard (symbolp compst-var).
- fn-recursivep — Guard (booleanp fn-recursivep).
- prec-objs — Guard (atc-string-objinfo-alistp prec-objs).
- Returns
- bindings — Type (doublet-listp bindings).
- hyps — Type (true-listp hyps).
- subst — Type (symbol-symbol-alistp subst), given (atc-symbol-varinfo-alistp typed-formals).
- instantiation — Type (symbol-pseudoterm-alistp instantiation), given (and (atc-symbol-varinfo-alistp typed-formals) (symbolp compst-var)).
Both C functions and C loops have correctness theorems of the form
(b* (<bindings>) ...).
Here we generate the <bindings>,
which we designate as `outer' since they are
at the outermost level of the theorem's formula.
We also generate some of the hypotheses
used in the correctness theorems
that relate to the bindings,
explained below.
We also generate a variable substitution, explained below.
We also generate an instantiation
for lemmas used in the hints of generated theorems;
the instantiation is in alist form,
so that we can use a readily available stronger type for it.
The (outer) bindings can be determined from
the formals of the ACL2 function fn that represents
the C function or C loop.
The bindings differ between C functions and loops,
but there is also commonality,
which justifies having this one ACL2 code generation function
that handles both cases.
Consider a non-recursive fn, which represents a C function.
Its correctness theorem equates (roughly speaking)
a call of exec-fun with a call of fn.
However, while fn takes arrays and structures in the heap
as arguments,
exec-fun takes pointers to those arrays and structures
as arguments.
So we introduce variables for the pointers,
named after the formals of fn that are arrays or structures:
we add -PTR to the formals of fn,
which should not cause name conflicts because
the names of the formals must be portable C identifiers.
For each array or structure formal a of fn,
we generate a pointer variable a-ptr as explained,
along with a binding
(a (read-object (value-pointer->designator a-ptr) compst)):
this binding relates the two variables,
and lets us use the guard of fn as hypothesis in the theorem,
which uses a,
which the binding replaces with the array or structure
pointed to by a-ptr.
Along with this binding, we also generate hypotheses saying that
a-ptr is a top-level pointer of the appropriate type;
the type is determined from the type of the formal a.
Along with the binding and the hypotheses,
we also generate an alist element (a . a-ptr),
returned as part of the subst result,
that is used to generate the argument list of exec-fun,
by applying the substitution subst to the formals of fn:
this way, a gets substituted with a-ptr,
which is what we want since exec-fun takes pointers, not arrays.
The substitution is also used to calculate the final computation state,
in atc-gen-cfun-final-compustate.
The treatment of arrays that are external objects is different.
Similarly to heap arrays,
fn takes the whole external arrays as arguments.
But exec-fun takes nothing for these as arguments:
those arrays are found in the static storage of the computation state.
We still need to generate a binding that relates
the variables passed to fn that contain these arrays
to the computation state:
we do it via bindings of the form
((a (read-static-var (ident ...) compst))),
which we generate here.
We generate no hypotheses in this case:
we do not introduce a pointer variable,
so there is no need for hypotheses about it;
the pointer is generated internally during symbolic execution,
with an object designator for the variable in static storage.
We generate no pointer substitution in this case:
again, there is no pointer variable introduced here.
Finally, we generate an instantiation pair consisting of
the formal and the (read-static-var (ident ...) compst) call.
For a non-array that is an external object,
the situation is similar to the external object array case,
but we do not introduce any pointer variable.
The non-array non-structure formals of a non-recursive fn
do not cause any bindings, hypotheses, or substitutions to be generated.
They are passed to both exec-fun and fn in the theorem,
and it is the guard of fn that constrains them
in the hypotheses of the theorem.
The treatment of a recursive fn is a bit more complicated.
The correctness theorem for the loop represented by fn
equates (roughly speaking)
a call of exec-stmt with a call of fn.
However, exec-stmt is called on a computation state,
not on anything that corresponds to the formals of fn,
as is the case for a non-recursive fn as explained above.
There is still a correspondence, of course:
the formals of fn correspond to variables in the computation state.
We consider separately
the case of arrays or structures in the heap,
the case of arrays in static storage,
and the case of non-arrays and non-structures.
If a is a non-array non-structure formal of a recursive fn,
it corresponds to (read-var <a> compst),
where <a> is the identifier derived from the name of a.
Thus, in this case we generate the binding (a (read-var <a> compst)).
Since no pointers are involved, in this case we generate
no hypotheses and no substitutions;
we generate an instantiation that instantiates
the formal with (read-var <a> compst).
If a is a heap array or structure formal of a recursive fn,
we introduce an additional a-ptr variable,
similarly to the case of non-recursive fn.
We generate two bindings (a-ptr (read-var <a> compst))
and (a (read-object (value-pointer->designator a-ptr) compst)),
in that order.
The first binding serves to tie a-ptr
to the corresponding variable in the computation state,
which has the name of a, but it holds a pointer.
The second binding is analogous in purpose
to the case of a non-recursive fn explained above:
it lets us use the guard of fn, which references a,
in the hypotheses of the generated theorem
without having to make an explicit substitution,
because the bindings are in fact doing the substitution.
It should be clear why the two bindings have to be in that order;
the bindings are put into a b*,
which enforces the order.
We generate a substitution of a with a-ptr,
for use by atc-gen-loop-final-compustate
(not to calculate the arguments of exec-fun,
because no exec-fun call is involved in the theorem for loops.
The instantiation combines read-var and read-object.
If a is an array in static storage,
things are more similar to the case in which fn is not recursive.
The binding is with read-static-var, i.e. the same.
We generate a different hypothesis from all other cases:
the hypothesis is that the variable is not in automatic storage,
i.e. that it is found in static storage.
This is necessary for theorems for C loops,
because a read-var during execution cannot reach add-frame
and be turned into read-static-var as done for C functions.
This hypothesis is relieved in the correctness theorem
of the non-recursive function that calls the recursive one:
the symbolic execution for the non-recursive one
can have read-var reach add-frame
and turn that into read-static-var.
We generate no substitution, since there are no pointer variables.
We generate an instantiation that instantiates the formal
with the read-static-var call.
The reason for generating and using the described bindings in the theorems,
as opposed to making the substitutions in the theorem's formula,
is greater readability of the theorems.
Particularly in the case of loop theorems,
if a occurs a few times in the guard,
the guard with just a in those occurrences is more readable than
if all those occurrences are replaced with (read-var <a> compst).
The lemma instantiation is similar to the bindings,
but it only concerns the formals of fn, not the a-ptr variables.
The instantiation is used on the guard and termination theorems of fn,
and therefore it can only concern the formals of fn.
There is an intentional discrepancy between the fact that
an array pointer points to the whole array
while the type of the pointer is the array element type.
The reason is the approximate, but correct in our C subset,
treatment of arrays and pointers discussed in exec-arrsub.
Definitions and Theorems
Function: atc-gen-outer-bindings-and-hyps
(defun atc-gen-outer-bindings-and-hyps
(typed-formals compst-var fn-recursivep prec-objs)
(declare
(xargs :guard (and (atc-symbol-varinfo-alistp typed-formals)
(symbolp compst-var)
(booleanp fn-recursivep)
(atc-string-objinfo-alistp prec-objs))))
(let ((__function__ 'atc-gen-outer-bindings-and-hyps))
(declare (ignorable __function__))
(b*
(((when (endp typed-formals))
(mv nil nil nil nil))
((cons formal info) (car typed-formals))
(type (atc-var-info->type info))
(formal-ptr (add-suffix-to-fn formal "-PTR"))
(formal-objdes (cons 'value-pointer->designator
(cons formal-ptr 'nil)))
(formal-id (cons 'ident
(cons (cons 'quote
(cons (symbol-name formal) 'nil))
'nil)))
(pointerp (or (type-case type :pointer)
(type-case type :array)))
(extobjp (assoc-equal (symbol-name formal)
prec-objs))
(bindings
(if fn-recursivep
(if pointerp
(if extobjp
(list
(cons formal
(cons (cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))
'nil)))
(list
(cons formal-ptr
(cons (cons 'read-var
(cons formal-id (cons compst-var 'nil)))
'nil))
(cons
formal
(cons (cons 'read-object
(cons formal-objdes (cons compst-var 'nil)))
'nil))))
(if extobjp
(list
(cons formal
(cons (cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))
'nil)))
(list
(cons formal
(cons (cons 'read-var
(cons formal-id (cons compst-var 'nil)))
'nil)))))
(if pointerp
(if extobjp
(list
(cons formal
(cons (cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))
'nil)))
(list
(cons
formal
(cons (cons 'read-object
(cons formal-objdes (cons compst-var 'nil)))
'nil))))
(if extobjp
(list
(cons formal
(cons (cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))
'nil)))
nil))))
(subst (and pointerp (not extobjp)
(list (cons formal formal-ptr))))
(hyps
(and
pointerp
(if extobjp
(list
(cons 'not
(cons (cons 'var-autop
(cons formal-id (cons compst-var 'nil)))
'nil)))
(list
(cons 'valuep (cons formal-ptr 'nil))
(cons 'value-case
(cons formal-ptr '(:pointer)))
(cons 'value-pointer-validp
(cons formal-ptr 'nil))
(cons 'equal
(cons (cons 'objdesign-kind
(cons (cons 'value-pointer->designator
(cons formal-ptr 'nil))
'nil))
'(:alloc)))
(if
(type-case type :pointer)
(cons 'equal
(cons (cons 'value-pointer->reftype
(cons formal-ptr 'nil))
(cons (type-to-maker (type-pointer->to type))
'nil)))
(cons 'equal
(cons (cons 'value-pointer->reftype
(cons formal-ptr 'nil))
(cons (type-to-maker (type-array->of type))
'nil))))))))
(inst
(if fn-recursivep
(if pointerp
(if extobjp
(list (cons formal
(cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))))
(list
(cons
formal
(cons
'read-object
(cons
(cons
'value-pointer->designator
(cons (cons 'read-var
(cons formal-id (cons compst-var 'nil)))
'nil))
(cons compst-var 'nil))))))
(if extobjp
(list (cons formal
(cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))))
(list
(cons formal
(cons 'read-var
(cons formal-id (cons compst-var 'nil)))))))
(if pointerp
(if extobjp
(list (cons formal
(cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))))
(list (cons formal
(cons 'read-object
(cons formal-objdes
(cons compst-var 'nil))))))
(if extobjp
(list (cons formal
(cons 'read-static-var
(cons formal-id (cons compst-var 'nil)))))
nil))))
((mv more-bindings
more-hyps more-subst more-inst)
(atc-gen-outer-bindings-and-hyps
(cdr typed-formals)
compst-var fn-recursivep prec-objs)))
(mv (append bindings more-bindings)
(append hyps more-hyps)
(append subst more-subst)
(append inst more-inst)))))
Theorem: doublet-listp-of-atc-gen-outer-bindings-and-hyps.bindings
(defthm doublet-listp-of-atc-gen-outer-bindings-and-hyps.bindings
(b* (((mv ?bindings ?hyps
common-lisp::?subst ?instantiation)
(atc-gen-outer-bindings-and-hyps
typed-formals
compst-var fn-recursivep prec-objs)))
(doublet-listp bindings))
:rule-classes :rewrite)
Theorem: true-listp-of-atc-gen-outer-bindings-and-hyps.hyps
(defthm true-listp-of-atc-gen-outer-bindings-and-hyps.hyps
(b* (((mv ?bindings ?hyps
common-lisp::?subst ?instantiation)
(atc-gen-outer-bindings-and-hyps
typed-formals
compst-var fn-recursivep prec-objs)))
(true-listp hyps))
:rule-classes :rewrite)
Theorem: symbol-symbol-alistp-of-atc-gen-outer-bindings-and-hyps.subst
(defthm
symbol-symbol-alistp-of-atc-gen-outer-bindings-and-hyps.subst
(implies (atc-symbol-varinfo-alistp typed-formals)
(b* (((mv ?bindings ?hyps
common-lisp::?subst ?instantiation)
(atc-gen-outer-bindings-and-hyps
typed-formals
compst-var fn-recursivep prec-objs)))
(symbol-symbol-alistp subst)))
:rule-classes :rewrite)
Theorem: symbol-pseudoterm-alistp-of-atc-gen-outer-bindings-and-hyps.instantiation
(defthm
symbol-pseudoterm-alistp-of-atc-gen-outer-bindings-and-hyps.instantiation
(implies (and (atc-symbol-varinfo-alistp typed-formals)
(symbolp compst-var))
(b* (((mv ?bindings ?hyps
common-lisp::?subst ?instantiation)
(atc-gen-outer-bindings-and-hyps
typed-formals
compst-var fn-recursivep prec-objs)))
(symbol-pseudoterm-alistp instantiation)))
:rule-classes :rewrite)