		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-conv

Generate a C expression from an ACL2 term that represents an integer conversion.

Signature
(atc-gen-expr-conv fn arg-term arg-expr arg-type arg-events arg-thm in-type out-type tyname 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).; in-type — Guard (typep in-type).; out-type — Guard (typep out-type).; tyname — Guard (tynamep tyname).; 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.

For now we do not generate the theorem; we will add suppor for that later.

Definitions and Theorems

Function: atc-gen-expr-conv

(defun atc-gen-expr-conv (fn arg-term
                             arg-expr arg-type arg-events arg-thm
                             in-type out-type tyname 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 in-type)
                             (typep out-type)
                             (tynamep tyname)
                             (expr-ginp gin))))
 (let ((__function__ 'atc-gen-expr-conv))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-expr-gout))
    (wrld (w state))
    ((expr-gin gin) gin)
    ((unless (equal arg-type in-type))
     (reterr
      (msg
       "The conversion from ~x0 to ~x1 is applied ~
               to an expression term ~x2 returning ~x3, ~
               which is not the expected type ~x0. ~
               This is indicative of provably dead code, ~
               given that the code is guard-verified."
       in-type out-type arg-term arg-type)))
    (expr (make-expr-cast :type tyname
                          :arg arg-expr))
    (term (cons fn (cons arg-term 'nil)))
    ((when (not gin.proofs))
     (retok (make-expr-gout :expr expr
                            :type out-type
                            :term term
                            :events arg-events
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid)))
    (fn-okp
     (and
         (or (type-case out-type :schar)
             (and (type-case out-type :sshort)
                  (not (member-eq (type-kind in-type)
                                  '(:schar))))
             (and (type-case out-type :sint)
                  (not (member-eq (type-kind in-type)
                                  '(:schar :sshort))))
             (and (type-case out-type :slong)
                  (not (member-eq (type-kind in-type)
                                  '(:schar :sshort :sint))))
             (and (type-case out-type :sllong)
                  (not (member-eq (type-kind in-type)
                                  '(:schar :sshort :sint :slong)))))
         (pack fn '-okp)))
    ((mv okp-lemma-event?
         okp-lemma-name thm-index names-to-avoid)
     (if fn-okp
      (b*
       ((okp-lemma-name (pack gin.fn '-expr-
                              gin.thm-index '-okp-lemma))
        ((mv okp-lemma-name names-to-avoid)
         (fresh-logical-name-with-$s-suffix
              okp-lemma-name
              nil gin.names-to-avoid wrld))
        (arg-uterm (untranslate$ arg-term nil state))
        (okp-lemma-formula (cons fn-okp (cons arg-uterm 'nil)))
        (okp-lemma-formula
             (atc-contextualize okp-lemma-formula gin.context gin.fn
                                gin.fn-guard nil nil nil nil wrld))
        (okp-lemma-hints
         (cons
          (cons
           '"Goal"
           (cons
            ':in-theory
            (cons
             (cons
                'quote
                (cons (cons gin.fn-guard '(if* test* declar assign))
                      'nil))
             (cons ':use
                   (cons (cons ':guard-theorem
                               (cons gin.fn 'nil))
                         'nil)))))
          'nil))
        ((mv okp-lemma-event &)
         (evmac-generate-defthm okp-lemma-name
                                :formula okp-lemma-formula
                                :hints okp-lemma-hints
                                :enable nil)))
       (mv (list okp-lemma-event)
           okp-lemma-name (1+ gin.thm-index)
           names-to-avoid))
      (mv nil
          nil gin.thm-index gin.names-to-avoid)))
    (hints
     (b*
       ((arg-type-pred
             (atc-type-to-recognizer arg-type gin.prec-tags))
        (valuep-when-arg-type-pred
             (pack 'valuep-when- arg-type-pred))
        (exec-cast-of-out-type-when-arg-type-pred
             (pack 'exec-cast-of-
                   (type-kind out-type)
                   '-when-
                   arg-type-pred))
        (type-pred (atc-type-to-recognizer out-type gin.prec-tags))
        (type-pred-of-fn (pack type-pred '-of- fn))
        (valuep-when-type-pred (pack 'valuep-when- type-pred)))
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
            (cons
             'exec-expr-pure-when-cast
             (cons
              '(:e expr-kind)
              (cons
               '(:e expr-cast->type)
               (cons
                '(:e expr-cast->arg)
                (cons
                 arg-thm
                 (cons
                  valuep-when-arg-type-pred
                  (cons
                   exec-cast-of-out-type-when-arg-type-pred
                   (cons
                    type-pred-of-fn
                    (append
                     (and fn-okp (list okp-lemma-name))
                     (cons
                      'expr-valuep-of-expr-value
                      (cons
                       'expr-value->value-of-expr-value
                       (cons
                        'value-fix-when-valuep
                        (cons
                             valuep-when-type-pred 'nil)))))))))))))
            'nil))
          'nil)))
       'nil)))
    ((mv thm-event
         thm-name thm-index names-to-avoid)
     (atc-gen-expr-pure-correct-thm
          gin.fn gin.fn-guard gin.context
          expr out-type term term acl2::*nil*
          gin.compst-var hints nil gin.prec-tags
          thm-index names-to-avoid state)))
   (retok (make-expr-gout
               :expr expr
               :type out-type
               :term term
               :events (append arg-events
                               okp-lemma-event? (list thm-event))
               :thm-name thm-name
               :thm-index thm-index
               :names-to-avoid names-to-avoid)))))

Theorem: expr-goutp-of-atc-gen-expr-conv.gout

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