		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-context-preamble

Generate a context preamble from the formals of a function.

Signature
(atc-gen-context-preamble typed-formals compst-var fenv-var prog-const) → terms
Arguments: typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; compst-var — Guard (symbolp compst-var).; fenv-var — Guard (symbolp fenv-var).; prog-const — Guard (symbolp prog-const).
Returns: terms — Type (true-listp terms).

As explained in atc-context, the logical contexts for the generated theorems includes a preamble of premises that is a list of untranslated terms. This is calculated from the typed formals of the ACL2 function that is translated to a C function.

For each formal x not representing an external object and whose C type is pointer or array, we generate a portion of the preamble saying that x-ptr is a valid pointer value of the right type, the pointer's object designator is in allocated memory (for now; this will be generalized later), and reading the object yields x. Thus, a formal that is a pointer or array is represented by two variables in the generated theorems: this is necessary because the ACL2 function takes integers and structures and arrays (not pointers), but the C function takes pointers that point to integers and structures, and pointers that point to the beginning of arrays. In the theorems, we use the name of the formal as the integer or structure or array, and we introduce a new name, with a -ptr suffix, for the pointer. Note that, because of the restriction on portable ASCII C identifiers, dashes cannot occur in names of formals, and thus something ending in -ptr cannot cause conflicts. The terms generated in the preamble constrain x-ptr to be the pointer, and include a binding hypothesis that sets x to be the integer or structure or array to which x-ptr points to. There is also a binding hypothesis for a variable x-objdes that is the object designator in x-ptr; note that it cannot conflict with other variables, for the same reason as x-ptr.

In addition, for each formal x not representing an external object and whose C type is a pointer or array, we generate a portion of the preamble saying that the designated object is disjoint from the objects designated by other formal parameters. We collect these disjointness hypotheses separately, so that we can put them all at the end of the final list of preamble terms, instead of interspersed with other preamble terms, for readability.

For each formal x not representing an external object and whose C type is not pointer or array (i.e. is integer of structure), we generate no preamble terms. This is because the ACL2 formal directly represents the C formal.

For each formal x that represents an external object, we generate a binding hypothesis saying that x equals read-object applied to the object designator for the variable in static storage. This is adequate whether the external object is an integer or an array.

Definitions and Theorems

Function: atc-gen-context-preamble-aux-aux

(defun atc-gen-context-preamble-aux-aux
       (this-var-ptr typed-formals-rest)
 (declare
  (xargs
       :guard (and (symbolp this-var-ptr)
                   (atc-symbol-varinfo-alistp typed-formals-rest))))
 (let ((__function__ 'atc-gen-context-preamble-aux-aux))
  (declare (ignorable __function__))
  (b* (((when (endp typed-formals-rest)) nil)
       ((cons other-var other-info)
        (car typed-formals-rest)))
   (if
    (and (member-equal (type-kind (atc-var-info->type other-info))
                       '(:pointer :array))
         (not (atc-var-info->externalp other-info)))
    (cons
     (cons
         'object-disjointp
         (cons (cons 'value-pointer->designator
                     (cons this-var-ptr 'nil))
               (cons (cons 'value-pointer->designator
                           (cons (add-suffix-to-fn other-var "-PTR")
                                 'nil))
                     'nil)))
     (atc-gen-context-preamble-aux-aux
          this-var-ptr (cdr typed-formals-rest)))
    (atc-gen-context-preamble-aux-aux this-var-ptr
                                      (cdr typed-formals-rest))))))

Theorem: true-listp-of-atc-gen-context-preamble-aux-aux

(defthm true-listp-of-atc-gen-context-preamble-aux-aux
  (b* ((terms (atc-gen-context-preamble-aux-aux
                   this-var-ptr typed-formals-rest)))
    (true-listp terms))
  :rule-classes :rewrite)

Function: atc-gen-context-preamble-aux

(defun atc-gen-context-preamble-aux (typed-formals compst-var)
 (declare
      (xargs :guard (and (atc-symbol-varinfo-alistp typed-formals)
                         (symbolp compst-var))))
 (let ((__function__ 'atc-gen-context-preamble-aux))
  (declare (ignorable __function__))
  (b*
   (((when (endp typed-formals))
     (mv nil nil))
    ((cons var info) (car typed-formals))
    (type (atc-var-info->type info))
    (externalp (atc-var-info->externalp info))
    ((mv terms-about-this-formal
         terms-about-this-and-other-formals)
     (if externalp
      (mv
       (cons
        (cons
         'equal
         (cons
          var
          (cons
           (cons
              'read-object
              (cons (cons 'objdesign-static
                          (cons (cons 'ident
                                      (cons (symbol-name var) 'nil))
                                'nil))
                    (cons compst-var 'nil)))
           'nil)))
        'nil)
       nil)
      (if
       (member-eq (type-kind type)
                  '(:pointer :array))
       (b*
        ((var-ptr (add-suffix-to-fn var "-PTR"))
         (var-objdes (add-suffix-to-fn var "-OBJDES"))
         (reftype (if (type-case type :pointer)
                      (type-pointer->to type)
                    (type-array->of type)))
         (terms-about-this-formal
          (cons
           (cons 'valuep (cons var-ptr 'nil))
           (cons
            (cons 'equal
                  (cons (cons 'value-kind (cons var-ptr 'nil))
                        '(:pointer)))
            (cons
             (cons 'value-pointer-validp
                   (cons var-ptr 'nil))
             (cons
              (cons 'equal
                    (cons var-objdes
                          (cons (cons 'value-pointer->designator
                                      (cons var-ptr 'nil))
                                'nil)))
              (cons
               (cons 'equal
                     (cons (cons 'objdesign-kind
                                 (cons var-objdes 'nil))
                           '(:alloc)))
               (cons
                (cons 'equal
                      (cons (cons 'value-pointer->reftype
                                  (cons var-ptr 'nil))
                            (cons (type-to-maker reftype) 'nil)))
                (cons
                 (cons
                  'equal
                  (cons
                   var
                   (cons
                     (cons 'read-object
                           (cons var-objdes (cons compst-var 'nil)))
                     'nil)))
                 'nil))))))))
         (terms-about-this-and-other-formals
              (atc-gen-context-preamble-aux-aux
                   var-ptr (cdr typed-formals))))
        (mv terms-about-this-formal
            terms-about-this-and-other-formals))
       (mv nil nil))))
    ((mv more-terms-about-single-formals
         more-terms-about-formal-pairs)
     (atc-gen-context-preamble-aux (cdr typed-formals)
                                   compst-var)))
   (mv (append terms-about-this-formal
               more-terms-about-single-formals)
       (append terms-about-this-and-other-formals
               more-terms-about-formal-pairs)))))

Theorem: true-listp-of-atc-gen-context-preamble-aux.terms-about-single-formals

(defthm
 true-listp-of-atc-gen-context-preamble-aux.terms-about-single-formals
 (b* (((mv ?terms-about-single-formals
           ?terms-about-formal-pairs)
       (atc-gen-context-preamble-aux typed-formals compst-var)))
   (true-listp terms-about-single-formals))
 :rule-classes :rewrite)

Theorem: true-listp-of-atc-gen-context-preamble-aux.terms-about-formal-pairs

(defthm
 true-listp-of-atc-gen-context-preamble-aux.terms-about-formal-pairs
 (b* (((mv ?terms-about-single-formals
           ?terms-about-formal-pairs)
       (atc-gen-context-preamble-aux typed-formals compst-var)))
   (true-listp terms-about-formal-pairs))
 :rule-classes :rewrite)

Function: atc-gen-context-preamble

(defun atc-gen-context-preamble
       (typed-formals compst-var fenv-var prog-const)
 (declare
      (xargs :guard (and (atc-symbol-varinfo-alistp typed-formals)
                         (symbolp compst-var)
                         (symbolp fenv-var)
                         (symbolp prog-const))))
 (let ((__function__ 'atc-gen-context-preamble))
  (declare (ignorable __function__))
  (b* (((mv terms-about-single-formals
            terms-about-formal-pairs)
        (atc-gen-context-preamble-aux typed-formals compst-var)))
   (append
    (list
         (cons 'equal
               (cons fenv-var
                     (cons (cons 'init-fun-env
                                 (cons (cons 'preprocess
                                             (cons prog-const 'nil))
                                       'nil))
                           'nil))))
    terms-about-single-formals
    terms-about-formal-pairs))))

Theorem: true-listp-of-atc-gen-context-preamble

(defthm true-listp-of-atc-gen-context-preamble
  (b*
   ((terms
         (atc-gen-context-preamble typed-formals
                                   compst-var fenv-var prog-const)))
   (true-listp terms))
  :rule-classes :rewrite)