		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-expr

Generate a C expression from an ACL2 term that must be an expression term.

Signature
(atc-gen-expr term gin state) → (mv erp expr type term* result new-compst limit events thm-name new-inscope new-context thm-index names-to-avoid)
Arguments: term — Guard (pseudo-termp term).; gin — Guard (stmt-ginp gin).
Returns: expr — Type (exprp expr).; type — Type (typep type).; term* — Type (pseudo-termp term*), given (pseudo-termp term).; result — An untranslated term.; new-compst — An untranslated term.; limit — Type (pseudo-termp limit).; events — Type (pseudo-event-form-listp events).; thm-name — Type (symbolp thm-name).; new-inscope — Type (atc-symbol-varinfo-alist-listp new-inscope).; new-context — Type (atc-contextp new-context).; thm-index — Type (posp thm-index).; names-to-avoid — Type (symbol-listp names-to-avoid).

At the same time, we check that the term is an expression term, as described in the user documentation.

It may seem surprising that this function is under atc-statement-generation instead of atc-expression-generation, but it needs to come after stmt-gin because it takes that as an input. Indeed, this ACL2 function is used for top-level or near-top-level expressions within statements, and so it is not unreasonable that this function is ``close'' to the statement generation functions. Note that functions to generate assignment expressions are also under atc-statement-generation, since they are top-level expressions (in C terminology, they are full expressions [C17:6.8/4]).

We also return the C type of the expression, the transformed term, the term for the C result of the expression, the term for the C computation state after the execution of the expression, a limit that suffices for exec-expr-call-or-pure to execute the expression completely, and then the usual outputs.

If the term is a call of a function that precedes fn in the list of target functions among t1, ..., tp, we translate it to a C function call on the translated arguments. The type of the expression is the result type of the function, which is looked up in the function alist passed as input: we ensure that this type is not void. A sufficient limit for exec-fun to execute the called function is retrieved from the called function's information; we add 2 to it, to take into account the decrementing of the limit to go from exec-expr-call-or-pure to exec-expr-call and from there to exec-fun. If the called function affects no objects, the result term is essentially the untranslation of the input term, and new-compst is the same as the computation state variable; if the called function affects objects, the result term is mv-nth of 0 applied to the call, and new-compst updates the computation state variable with the mv-nths of 1, 2, etc. applied to the call.

Otherwise, we attempt to translate the term as a pure expression term. The type is the one returned by that translation. As limit we return 1, which suffices for exec-expr-call-or-pure to not stop right away due to the limit being 0. In this case, result is essentially the untranslated input term, and new-compst is the computation state variable unchanged.

Definitions and Theorems

Function: atc-gen-expr

(defun atc-gen-expr (term gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-expr))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (irr-expr)
     (irr-type)
     nil nil
     nil nil nil nil nil (irr-atc-context)
     1 nil)
    ((stmt-gin gin) gin)
    (wrld (w state))
    ((erp okp
          called-fn arg-terms in-types out-type
          affect extobjs limit called-fn-guard)
     (atc-check-cfun-call term
                          gin.var-term-alist gin.prec-fns wrld))
    ((when okp)
     (b*
      (((when (type-case out-type :void))
        (reterr
         (msg
          "A call ~x0 of the function ~x1, which returns void, ~
                     is being used where ~
                     an expression term returning a a non-void C type ~
                     is expected."
          term called-fn)))
       ((unless (equal affect gin.affect))
        (reterr
         (msg
          "The call ~x0 affects ~x1, ~
                     but it should affect ~x2 instead."
          term gin.affect affect)))
       ((erp (exprs-gout args))
        (atc-gen-expr-pure-list
             arg-terms
             (make-exprs-gin :context gin.context
                             :inscope gin.inscope
                             :prec-tags gin.prec-tags
                             :fn gin.fn
                             :fn-guard gin.fn-guard
                             :compst-var gin.compst-var
                             :thm-index gin.thm-index
                             :names-to-avoid gin.names-to-avoid
                             :proofs gin.proofs)
             state))
       ((unless (equal args.types in-types))
        (reterr
         (msg
          "The function ~x0 with input types ~x1 ~
                     is applied to expression terms ~x2 returning ~x3. ~
                     This is indicative of provably dead code, ~
                     given that the code is guard-verified."
          called-fn
          in-types arg-terms args.types)))
       (call-args
        (atc-remove-extobj-args args.exprs (formals+ called-fn wrld)
                                extobjs))
       (expr (make-expr-call
                  :fun (make-ident :name (symbol-name called-fn))
                  :args call-args))
       ((when (eq called-fn 'quote))
        (reterr
             (raise "Internal error: called function is QUOTE.")))
       (term (cons called-fn args.terms))
       (uterm (untranslate$ term nil state))
       (fninfo (cdr (assoc-eq called-fn gin.prec-fns)))
       ((unless fninfo)
        (reterr (raise "Internal error: function ~x0 has no info."
                       called-fn)))
       (called-fn-thm (atc-fn-info->correct-mod-thm fninfo))
       ((when (or (not gin.proofs)
                  (not called-fn-thm)))
        (retok expr out-type term nil nil
               (cons 'binary-+
                     (cons ''2 (cons limit 'nil)))
               args.events nil gin.inscope gin.context
               args.thm-index args.names-to-avoid))
       (guard-lemma-name (pack gin.fn '-call-
                               args.thm-index '-guard-lemma))
       ((mv guard-lemma-name names-to-avoid)
        (fresh-logical-name-with-$s-suffix
             guard-lemma-name
             nil args.names-to-avoid wrld))
       (thm-index (1+ args.thm-index))
       (guard-lemma-formula (cons called-fn-guard args.terms))
       (guard-lemma-formula
           (atc-contextualize guard-lemma-formula gin.context gin.fn
                              gin.fn-guard nil nil nil nil wrld))
       (guard-lemma-hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
              (cons 'quote
                    (cons (cons gin.fn-guard
                                (cons called-fn-guard '(if* test*)))
                          'nil))
              (cons ':use
                    (cons (cons ':guard-theorem
                                (cons gin.fn 'nil))
                          'nil)))))
         'nil))
       ((mv guard-lemma-event &)
        (evmac-generate-defthm guard-lemma-name
                               :formula guard-lemma-formula
                               :hints guard-lemma-hints
                               :enable nil))
       (call-thm-name (pack gin.fn '-correct- thm-index))
       ((mv call-thm-name names-to-avoid)
        (fresh-logical-name-with-$s-suffix
             call-thm-name nil names-to-avoid wrld))
       (thm-index (1+ thm-index))
       (called-formals (formals+ called-fn wrld))
       ((unless (equal (len called-formals)
                       (len args.terms)))
        (reterr
         (raise
              "Internal error: ~x0 has formals ~x1 but actuals ~x2."
              called-fn called-formals args.terms)))
       (call-limit (cons 'binary-+
                         (cons ''2 (cons limit 'nil))))
       ((mv result new-compst)
        (atc-gen-call-result-and-endstate
             out-type gin.affect
             gin.inscope gin.compst-var uterm))
       (exec-formula
        (cons
         'equal
         (cons (cons 'exec-expr-call-or-pure
                     (cons (cons 'quote (cons expr 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons result (cons new-compst 'nil)))
                     'nil))))
       (exec-formula
            (atc-contextualize exec-formula gin.context
                               gin.fn gin.fn-guard gin.compst-var
                               gin.limit-var call-limit t wrld))
       ((mv type-formula &)
        (atc-gen-term-type-formula
             uterm out-type
             gin.affect gin.inscope gin.prec-tags))
       (type-formula
            (atc-contextualize type-formula gin.context gin.fn
                               gin.fn-guard nil nil nil nil wrld))
       (call-formula
            (cons 'and
                  (cons exec-formula (cons type-formula 'nil))))
       (call-hints
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               'exec-expr-call-or-pure-when-call
               (cons
                'exec-expr-call-open
                (cons
                 'exec-expr-pure-list-of-nil
                 (cons
                  'exec-expr-pure-list-when-consp
                  (append
                   args.thm-names
                   (cons
                    called-fn-thm
                    (cons
                     guard-lemma-name
                     (append
                      (atc-symbol-varinfo-alist-list-to-thms
                           gin.inscope)
                      (cons
                       'exec-fun-of-const-identifier
                       (cons
                        '(:e identp)
                        (cons
                         '(:e ident->name)
                         (cons
                          '(:e expr-kind)
                          (cons
                           '(:e expr-call->fun)
                           (cons
                            '(:e expr-call->args)
                            (cons
                             'not-zp-of-limit-variable
                             (cons
                              'not-zp-of-limit-minus-const
                              (cons
                               'expr-valuep-of-expr-value
                               (cons
                                'expr-value->value-of-expr-value
                                (cons
                                 'value-listp-of-cons
                                 (cons
                                  '(:e value-listp)
                                  (cons
                                   'apconvert-expr-value-when-not-value-array
                                   (cons
                                    'value-kind-when-ucharp
                                    (cons
                                     'value-kind-when-scharp
                                     (cons
                                      'value-kind-when-ushortp
                                      (cons
                                       'value-kind-when-sshortp
                                       (cons
                                        'value-kind-when-uintp
                                        (cons
                                         'value-kind-when-sintp
                                         (cons
                                          'value-kind-when-ulongp
                                          (cons
                                           'value-kind-when-slongp
                                           (cons
                                            'value-kind-when-ullongp
                                            (cons
                                             'value-kind-when-sllongp
                                             (append
                                              (atc-string-taginfo-alist-to-value-kind-thms
                                                   gin.prec-tags)
                                              (cons
                                               'value-fix-when-valuep
                                               (cons
                                                'valuep-when-ucharp
                                                (cons
                                                 'valuep-when-scharp
                                                 (cons
                                                  'valuep-when-ushortp
                                                  (cons
                                                   'valuep-when-sshortp
                                                   (cons
                                                    'valuep-when-uintp
                                                    (cons
                                                     'valuep-when-sintp
                                                     (cons
                                                      'valuep-when-ulongp
                                                      (cons
                                                       'valuep-when-slongp
                                                       (cons
                                                        'valuep-when-ullongp
                                                        (cons
                                                         'valuep-when-sllongp
                                                         (append
                                                          (atc-string-taginfo-alist-to-valuep-thms
                                                           gin.prec-tags)
                                                          (cons
                                                           'compustatep-of-add-var
                                                           (cons
                                                            'compustatep-of-enter-scope
                                                            (cons
                                                             'compustatep-of-add-frame
                                                             (cons
                                                              'write-object-to-update-object
                                                              (cons
                                                               'write-object-okp-when-valuep-of-read-object-no-syntaxp
                                                               (cons
                                                                'write-object-okp-of-update-object-same
                                                                (cons
                                                                 'write-object-okp-of-update-object-disjoint
                                                                 (cons
                                                                  'object-disjointp-commutative
                                                                  (cons
                                                                   'type-of-value-when-ucharp
                                                                   (cons
                                                                    'type-of-value-when-scharp
                                                                    (cons
                                                                     'type-of-value-when-ushortp
                                                                     (cons
                                                                     
 'type-of-value-when-sshortp
                                                                     
 (cons
                                                                     
  'type-of-value-when-uintp
                                                                     
  (cons
                                                                     
   'type-of-value-when-sintp
                                                                     
   (cons
                                                                     
    'type-of-value-when-ulongp
                                                                     
    (cons
                                                                     
     'type-of-value-when-slongp
                                                                     
     (cons
                                                                     
      'type-of-value-when-ullongp
                                                                     
      (cons
                                                                     
       'type-of-value-when-sllongp
                                                                     
       (cons
                                                                     
        'type-of-value-when-uchar-arrayp
                                                                     
        (cons
                                                                     
         'type-of-value-when-schar-arrayp
                                                                     
         (cons
                                                                     
          'type-of-value-when-ushort-arrayp
                                                                     
          (cons
                                                                     
           'type-of-value-when-sshort-arrayp
                                                                     
           (cons
                                                                     
            'type-of-value-when-uint-arrayp
                                                                     
            (cons
                                                                     
             'type-of-value-when-sint-arrayp
                                                                     
             (cons
                                                                     
              'type-of-value-when-ulong-arrayp
                                                                     
              (cons
                                                                     
               'type-of-value-when-slong-arrayp
                                                                     
               (cons
                                                                     
                'type-of-value-when-ullong-arrayp
                                                                     
                (cons
                                                                     
                 'type-of-value-when-sllong-arrayp
                                                                     
                 (atc-string-taginfo-alist-to-type-of-value-thms
                                                                     
                  gin.prec-tags)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
              'nil))
            'nil)))
         'nil))
       ((mv call-event &)
        (evmac-generate-defthm call-thm-name
                               :formula call-formula
                               :hints call-hints
                               :enable nil)))
      (retok expr out-type term result new-compst
             (cons 'binary-+
                   (cons ''2 (cons limit 'nil)))
             (append args.events
                     (list guard-lemma-event call-event))
             nil gin.inscope
             gin.context thm-index names-to-avoid)))
    ((erp (expr-gout pure))
     (atc-gen-expr-pure
          term
          (make-expr-gin :context gin.context
                         :inscope gin.inscope
                         :prec-tags gin.prec-tags
                         :fn gin.fn
                         :fn-guard gin.fn-guard
                         :compst-var gin.compst-var
                         :thm-index gin.thm-index
                         :names-to-avoid gin.names-to-avoid
                         :proofs gin.proofs)
          state))
    (bound ''1)
    ((when (not gin.proofs))
     (retok pure.expr pure.type pure.term
            (untranslate$ pure.term nil state)
            gin.compst-var bound
            pure.events nil gin.inscope gin.context
            pure.thm-index pure.names-to-avoid))
    (thm-name (pack gin.fn '-correct- pure.thm-index))
    ((mv thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          thm-name nil pure.names-to-avoid wrld))
    (type-pred (atc-type-to-recognizer pure.type gin.prec-tags))
    (valuep-when-type-pred
         (atc-type-to-valuep-thm pure.type gin.prec-tags))
    (value-kind-when-type-pred
         (atc-type-to-value-kind-thm pure.type gin.prec-tags))
    (uterm* (untranslate$ pure.term nil state))
    (formula1
     (cons
         'equal
         (cons (cons 'exec-expr-call-or-pure
                     (cons (cons 'quote (cons pure.expr 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons uterm* (cons gin.compst-var 'nil)))
                     'nil))))
    (formula2 (cons type-pred (cons uterm* 'nil)))
    (formula1
         (atc-contextualize formula1 gin.context gin.fn gin.fn-guard
                            gin.compst-var gin.limit-var ''1
                            t wrld))
    (formula2 (atc-contextualize formula2 gin.context gin.fn
                                 gin.fn-guard nil nil nil nil wrld))
    (formula (cons 'and
                   (cons formula1 (cons formula2 'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'compustatep-of-add-frame
            (cons
             'compustatep-of-add-var
             (cons
              'compustatep-of-enter-scope
              (cons
               'compustatep-of-update-var
               (cons
                'compustatep-of-update-object
                (cons
                 'compustatep-of-exit-scope
                 (cons
                  'compustatep-of-if*-when-both-compustatep
                  (cons
                   'exec-expr-call-or-pure-when-pure
                   (cons
                    '(:e expr-kind)
                    (cons
                     'not-zp-of-limit-variable
                     (cons
                      pure.thm-name
                      (cons
                       'expr-valuep-of-expr-value
                       (cons
                        'expr-value->value-of-expr-value
                        (cons
                         'value-fix-when-valuep
                         (cons
                          valuep-when-type-pred
                          (cons
                           'apconvert-expr-value-when-not-value-array
                           (cons value-kind-when-type-pred
                                 'nil)))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv event &)
     (evmac-generate-defthm thm-name
                            :formula formula
                            :hints hints
                            :enable nil)))
   (retok pure.expr pure.type pure.term
          (untranslate$ pure.term nil state)
          gin.compst-var
          bound (append pure.events (list event))
          thm-name gin.inscope
          gin.context (1+ pure.thm-index)
          names-to-avoid))))

Theorem: exprp-of-atc-gen-expr.expr

(defthm exprp-of-atc-gen-expr.expr
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: typep-of-atc-gen-expr.type

(defthm typep-of-atc-gen-expr.type
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (typep type))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-expr.term*

(defthm pseudo-termp-of-atc-gen-expr.term*
  (implies (pseudo-termp term)
           (b* (((mv acl2::?erp
                     ?expr ?type ?term* ?result ?new-compst
                     ?limit ?events ?thm-name ?new-inscope
                     ?new-context ?thm-index ?names-to-avoid)
                 (atc-gen-expr term gin state)))
             (pseudo-termp term*)))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-expr.limit

(defthm pseudo-termp-of-atc-gen-expr.limit
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (pseudo-termp limit))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-expr.events

(defthm pseudo-event-form-listp-of-atc-gen-expr.events
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-expr.thm-name

(defthm symbolp-of-atc-gen-expr.thm-name
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (symbolp thm-name))
  :rule-classes :rewrite)

Theorem: atc-symbol-varinfo-alist-listp-of-atc-gen-expr.new-inscope

(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-expr.new-inscope
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (atc-symbol-varinfo-alist-listp new-inscope))
  :rule-classes :rewrite)

Theorem: atc-contextp-of-atc-gen-expr.new-context

(defthm atc-contextp-of-atc-gen-expr.new-context
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (atc-contextp new-context))
  :rule-classes :rewrite)

Theorem: posp-of-atc-gen-expr.thm-index

(defthm posp-of-atc-gen-expr.thm-index
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (posp thm-index))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-expr.names-to-avoid

(defthm symbol-listp-of-atc-gen-expr.names-to-avoid
  (b* (((mv acl2::?erp
            ?expr ?type ?term* ?result ?new-compst
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-expr term gin state)))
    (symbol-listp names-to-avoid))
  :rule-classes :rewrite)