Generate hypotheses saying that the pointers designate disjoint objects.
(atc-gen-object-disjoint-hyps pointer-vars) → hyps
The ACL2 functions that represent C functions and loops take and return whole arrays and structured as inputs: thus, the possible modification to each array or structure only applies to that array or structure. In the generated C code, arrays and structures are passed as pointers instead. If two of these pointers, for different arrays or structures in ACL2, were equal, then the C code would not be correct in general, because modifying one array or structure would also modify the other one: there is, in fact, just one array or structure, which both pointers point to, but here we are talking about the two different arrays or structures in the ACL2 representation. It is thus critical that the generated correctness theorems include the assumption that all the pointers are distinct. This is the case not only for the arrays and structures that may be modified, but also for the ones that may not: otherwise, we could not rely on the latter to be unmodified, during the symbolic execution proof.
We generate these hypotheses here, by going through the pointer variables involved in the correctness theorem of the C function or loop. More precisely, we generate hypotheses saying that the object designated by the pointers are pairwise disjoint.
Function:
(defun atc-gen-object-disjoint-hyps (pointer-vars) (declare (xargs :guard (symbol-listp pointer-vars))) (let ((__function__ 'atc-gen-object-disjoint-hyps)) (declare (ignorable __function__)) (b* (((when (endp pointer-vars)) nil) (var (car pointer-vars)) (hyps (loop$ for var2 in (cdr pointer-vars) collect (cons 'object-disjointp (cons (cons 'value-pointer->designator (cons var 'nil)) (cons (cons 'value-pointer->designator (cons var2 'nil)) 'nil))))) (more-hyps (atc-gen-object-disjoint-hyps (cdr pointer-vars)))) (append hyps more-hyps))))
Theorem:
(defthm true-listp-of-atc-gen-object-disjoint-hyps (b* ((hyps (atc-gen-object-disjoint-hyps pointer-vars))) (true-listp hyps)) :rule-classes :rewrite)