		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-integer-read

Generate a C expression from an ACL2 term that represents an indirection of a pointer to integer.

Signature
(atc-gen-expr-integer-read fn arg-term arg-expr arg-type arg-events arg-thm type gin state) → (mv erp gout)
Arguments: fn — Guard (symbolp fn).; arg-term — Guard (pseudo-termp arg-term).; arg-expr — Guard (exprp arg-expr).; arg-type — Guard (typep arg-type).; arg-events — Guard (pseudo-event-form-listp arg-events).; arg-thm — Guard (symbolp arg-thm).; type — Guard (typep type).; gin — Guard (expr-ginp gin).
Returns: gout — Type (expr-goutp gout).

The expression and theorem for the argument are generated in the caller, and passed here.

Currently, the argument term must be an ACL2 variable. We defensively check that it is the case. The generated theorem needs not only the theorem about the argument, but also the theorem about the variable in the symbol table. The reason is that the theorem about the argument just says that the execution of the C variable yields the ACL2 -ptr variable, but here we need to show that the execution of the indirection expression yields the ACL2 variable that contains the integer, not the pointer: that assertion is in the theorem about the variable in the symbol table. An alternative proof generation approach is to extend the theorem about the argument to also say that dereferncing the pointer yields the integer variable, i.e. the same assertion in the symbol table: doing this obviated the need to use, in the theorem generated here, the theorem from the symbol table. However, that approach makes the theorem about the argument expression disuniform with other theorems about expressions; in particular, atc-gen-expr-pure-correct-thm would have to be generalized. Thus, the approach we use here seems better for now, since the only slight ``disuniformity'' is in the fact that we need to retrieve and use the theorem from the symbol table. The current approach critically depends on the argument of the indirection operator always being a variable; if in the future our ACL2 representation of C is extended so that the indirection operator can be applied to more general arguments, we may need to choose the alternative approach sketched above, which in that case would be more uniform.

Definitions and Theorems

Function: atc-gen-expr-integer-read

(defun atc-gen-expr-integer-read
       (fn arg-term arg-expr arg-type
           arg-events arg-thm type gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (pseudo-termp arg-term)
                             (exprp arg-expr)
                             (typep arg-type)
                             (pseudo-event-form-listp arg-events)
                             (symbolp arg-thm)
                             (typep type)
                             (expr-ginp gin))))
 (declare (xargs :guard (type-nonchar-integerp type)))
 (let ((__function__ 'atc-gen-expr-integer-read))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr-gout))
    ((expr-gin gin) gin)
    ((unless (equal arg-type (type-pointer type)))
     (reterr
      (msg
       "The indirection operator representation for integer type ~x0 ~
               is applied to an expression term ~x1 returning ~x2, ~
               but a ~x3 operand is expected. ~
               This is indicative of provably dead code, ~
               given that the code is guard-verified."
       type
       arg-term arg-type (type-pointer type))))
    (expr (make-expr-unary :op (unop-indir)
                           :arg arg-expr))
    (term (cons fn (cons arg-term 'nil)))
    ((when (not gin.proofs))
     (retok (make-expr-gout :expr expr
                            :type type
                            :term term
                            :events arg-events
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid)))
    ((unless (symbolp arg-term))
     (reterr
      (raise
           "Interal error: indirection applied to non-variable ~x0."
           arg-term)))
    (info (atc-get-var arg-term gin.inscope))
    ((unless info)
     (reterr
          (raise "Internal error: variable ~x0 not found in scope."
                 arg-term)))
    (var-thm (atc-var-info->thm info))
    (hints
     (b* ((type-pred (atc-type-to-recognizer type gin.prec-tags))
          (exec-indir-when-type-pred
               (pack 'exec-indir-when- type-pred))
          (type-read (pack (type-kind type) '-read))
          (type-read-when-type-pred
               (pack type-read '-when- type-pred)))
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
            (cons
             'exec-expr-pure-when-unary
             (cons
              '(:e expr-kind)
              (cons
               '(:e expr-unary->arg)
               (cons
                '(:e expr-unary->op)
                (cons
                 arg-thm
                 (cons
                  'expr-valuep-of-expr-value
                  (cons
                   exec-indir-when-type-pred
                   (cons
                    '(:e unop-kind)
                    (cons
                       var-thm
                       (cons type-read-when-type-pred 'nil))))))))))
            'nil))
          'nil)))
       'nil)))
    (objdes (add-suffix-to-fn arg-term "-OBJDES"))
    ((mv thm-event
         thm-name thm-index names-to-avoid)
     (atc-gen-expr-pure-correct-thm
          gin.fn gin.fn-guard gin.context expr
          type term term objdes gin.compst-var
          hints nil gin.prec-tags gin.thm-index
          gin.names-to-avoid state)))
   (retok
        (make-expr-gout :expr expr
                        :type type
                        :term term
                        :events (append arg-events (list thm-event))
                        :thm-name thm-name
                        :thm-index thm-index
                        :names-to-avoid names-to-avoid)))))

Theorem: expr-goutp-of-atc-gen-expr-integer-read.gout

(defthm expr-goutp-of-atc-gen-expr-integer-read.gout
  (b*
   (((mv acl2::?erp ?gout)
     (atc-gen-expr-integer-read fn arg-term arg-expr arg-type
                                arg-events arg-thm type gin state)))
   (expr-goutp gout))
  :rule-classes :rewrite)