		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-cfun-call-stmt

Generate a C block item statement that consists of a call of a void function.

Signature
(atc-gen-cfun-call-stmt called-fn arg-terms arg-types affect extobjs limit called-fn-guard gin state) → (mv erp gout)
Arguments: called-fn — Guard (symbolp called-fn).; arg-terms — Guard (pseudo-term-listp arg-terms).; arg-types — Guard (type-listp arg-types).; affect — Guard (symbol-listp affect).; extobjs — Guard (symbol-listp extobjs).; limit — Guard (pseudo-termp limit).; called-fn-guard — Guard (symbolp called-fn-guard).; gin — Guard (stmt-ginp gin).
Returns: gout — Type (stmt-goutp gout).

We also generate a theorem about exec-expr-call-or-asg applied to the call expression. The limit is 2 more than the function's limit: it takes 1 to go from exec-expr-call-or-asg to exec-expr-call, and another 1 to go from there to exec-expr-pure-list. Since the limit term for the function is over the function's formal, we need to perform a substitution of the formals with the actuals.

Definitions and Theorems

Function: atc-gen-cfun-call-stmt

(defun atc-gen-cfun-call-stmt
       (called-fn arg-terms arg-types affect
                  extobjs limit called-fn-guard gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp called-fn)
                             (pseudo-term-listp arg-terms)
                             (type-listp arg-types)
                             (symbol-listp affect)
                             (symbol-listp extobjs)
                             (pseudo-termp limit)
                             (symbolp called-fn-guard)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-cfun-call-stmt))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-stmt-gout))
    (wrld (w state))
    ((stmt-gin gin) gin)
    ((when gin.loop-flag)
     (reterr
      (msg
       "A loop body must end with ~
               a recursive call on every path, ~
               but in the function ~x0 it ends with ~
               a call of ~x1 on arguments ~x2 instead."
       gin.fn called-fn arg-terms)))
    ((unless (equal gin.affect affect))
     (reterr
      (msg
       "When generating C code for the function ~x0, ~
               a call of the non-recursive function ~x1 ~
               has been encountered that affects ~x2, ~
               which differs from the variables ~x3 ~
               being affected here."
       gin.fn called-fn affect gin.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 arg-types))
     (reterr
      (msg
       "The function ~x0 with argument 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
       arg-types arg-terms args.types)))
    (call-args
        (atc-remove-extobj-args args.exprs (formals+ called-fn wrld)
                                extobjs))
    (call-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
          (make-stmt-gout
               :items (list (block-item-stmt (stmt-expr call-expr)))
               :type (type-void)
               :term term
               :context gin.context
               :inscope gin.inscope
               :limit (cons 'binary-+
                            (cons ''5 (cons limit 'nil)))
               :events args.events
               :thm-name nil
               :thm-index args.thm-index
               :names-to-avoid 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 & new-compst)
     (atc-gen-call-result-and-endstate
          (type-void)
          gin.affect
          gin.inscope gin.compst-var uterm))
    (exec-formula
     (cons
         'equal
         (cons (cons 'exec-expr-call-or-asg
                     (cons (cons 'quote (cons call-expr 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons new-compst '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 inscope-thms)
     (atc-gen-term-type-formula
          uterm (type-void)
          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-asg-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
                   inscope-thms
                   (cons
                    'exec-fun-of-const-identifier
                    (cons
                     '(:e identp)
                     (cons
                      '(:e ident->name)
                      (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
                                 (cons
                                  'value-kind-when-uchar-arrayp
                                  (cons
                                   'value-kind-when-schar-arrayp
                                   (cons
                                    'value-kind-when-ushort-arrayp
                                    (cons
                                     'value-kind-when-sshort-arrayp
                                     (cons
                                      'value-kind-when-uint-arrayp
                                      (cons
                                       'value-kind-when-sint-arrayp
                                       (cons
                                        'value-kind-when-ulong-arrayp
                                        (cons
                                         'value-kind-when-slong-arrayp
                                         (cons
                                          'value-kind-when-ullong-arrayp
                                          (cons
                                           'value-kind-when-sllong-arrayp
                                           (append
                                            (atc-string-taginfo-alist-to-value-kind-thms
                                                 gin.prec-tags)
                                            (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
                                                      (cons
                                                       'valuep-when-uchar-arrayp
                                                       (cons
                                                        'valuep-when-schar-arrayp
                                                        (cons
                                                         'valuep-when-ushort-arrayp
                                                         (cons
                                                          'valuep-when-sshort-arrayp
                                                          (cons
                                                           'valuep-when-uint-arrayp
                                                           (cons
                                                            'valuep-when-sint-arrayp
                                                            (cons
                                                             'valuep-when-ulong-arrayp
                                                             (cons
                                                              'valuep-when-slong-arrayp
                                                              (cons
                                                               'valuep-when-ullong-arrayp
                                                               (cons
                                                                'valuep-when-sllong-arrayp
                                                                (append
                                                                 (atc-string-taginfo-alist-to-valuep-thms
                                                                  gin.prec-tags)
                                                                 (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
                                                                     
                (append
                                                                     
                 (atc-string-taginfo-alist-to-type-of-value-thms
                                                                     
                  gin.prec-tags)
                                                                     
                 '(expr-valuep-of-expr-value
                                                                     
                   expr-value->value-of-expr-value
                                                                     
                   value-fix-when-valuep
                                                                     
                   (:e
                                                                     
                    value-listp)
                                                                     
                   value-listp-of-cons
                                                                     
                   (:e
                                                                     
                    value-optionp)
                                                                     
                   (:e
                                                                     
                    expr-kind)
                                                                     
                   (:e
                                                                     
                    expr-call->fun)
                                                                     
                   (:e
                                                                     
                    expr-call->args)
                                                                     
                   not-zp-of-limit-variable
                                                                     
                   not-zp-of-limit-minus-const
                                                                     
                   compustatep-of-add-var
                                                                     
                   compustatep-of-enter-scope
                                                                     
                   compustatep-of-add-frame
                                                                     
                   mv-nth-of-cons
                                                                     
                   (:e
                                                                     
                    zp)
                                                                     
                   write-object-to-update-object
                                                                     
                   write-object-okp-of-add-var
                                                                     
                   write-object-okp-of-enter-scope
                                                                     
                   write-object-okp-of-add-frame
                                                                     
                   write-object-okp-of-update-object-same
                                                                     
                   write-object-okp-of-update-object-disjoint
                                                                     
                   write-object-okp-when-valuep-of-read-object-no-syntaxp
                                                                     
                   value-array->length-when-uchar-arrayp
                                                                     
                   value-array->length-when-schar-arrayp
                                                                     
                   value-array->length-when-ushort-arrayp
                                                                     
                   value-array->length-when-sshort-arrayp
                                                                     
                   value-array->length-when-uint-arrayp
                                                                     
                   value-array->length-when-sint-arrayp
                                                                     
                   value-array->length-when-ulong-arrayp
                                                                     
                   value-array->length-when-slong-arrayp
                                                                     
                   value-array->length-when-ullong-arrayp
                                                                     
                   value-array->length-when-sllong-arrayp
                                                                     
                   read-object-of-objdesign-static-to-objdesign-of-var
                                                                     
                   read-object-of-objdesign-static
                                                                     
                   var-autop-of-add-frame
                                                                     
                   var-autop-of-enter-scope
                                                                     
                   var-autop-of-add-var
                                                                     
                   var-autop-of-update-var
                                                                     
                   var-autop-of-update-static-var
                                                                     
                   var-autop-of-update-object
                                                                     
                   write-static-var-to-update-static-var
                                                                     
                   write-static-var-okp-of-add-var
                                                                     
                   write-static-var-okp-of-enter-scope
                                                                     
                   write-static-var-okp-of-add-frame
                                                                     
                   write-static-var-okp-when-valuep-of-read-static-var))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv call-event &)
     (evmac-generate-defthm call-thm-name
                            :formula call-formula
                            :hints call-hints
                            :enable nil))
    (stmt (stmt-expr call-expr))
    (stmt-limit (cons 'binary-+
                      (cons ''1 (cons call-limit 'nil))))
    (stmt-thm-name (pack gin.fn '-correct- thm-index))
    ((mv stmt-thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          stmt-thm-name nil names-to-avoid wrld))
    (thm-index (1+ thm-index))
    (stmt-exec-formula
     (cons
         'equal
         (cons (cons 'exec-stmt
                     (cons (cons 'quote (cons stmt 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons 'nil (cons new-compst 'nil)))
                     'nil))))
    (stmt-exec-formula
         (atc-contextualize stmt-exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var stmt-limit t wrld))
    ((mv stmt-type-formula &)
     (atc-gen-term-type-formula
          uterm (type-void)
          gin.affect gin.inscope gin.prec-tags))
    (stmt-type-formula
         (atc-contextualize stmt-type-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (stmt-formula (cons 'and
                        (cons stmt-exec-formula
                              (cons stmt-type-formula 'nil))))
    (stmt-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-stmt-when-expr
            (cons
             '(:e stmt-kind)
             (cons
              '(:e stmt-expr->get)
              (cons
                  'not-zp-of-limit-variable
                  (cons call-thm-name
                        '(compustatep-of-update-var
                              compustatep-of-update-object
                              compustatep-of-update-static-var))))))
           'nil))
         'nil)))
      'nil))
    ((mv stmt-event &)
     (evmac-generate-defthm stmt-thm-name
                            :formula stmt-formula
                            :hints stmt-hints
                            :enable nil))
    ((mv item item-limit item-events
         item-thm-name thm-index names-to-avoid)
     (atc-gen-block-item-stmt
          stmt stmt-limit
          (append args.events
                  (list guard-lemma-event
                        call-event stmt-event))
          stmt-thm-name uterm (type-void)
          nil new-compst
          (change-stmt-gin gin
                           :thm-index thm-index
                           :names-to-avoid names-to-avoid
                           :proofs (and stmt-thm-name t))
          state))
    (new-context
        (atc-context-extend
             gin.context
             (list (make-atc-premise-compustate :var gin.compst-var
                                                :term new-compst))))
    (premise (if (consp (cdr gin.affect))
                 (make-atc-premise-cvalues :vars gin.affect
                                           :term term)
               (make-atc-premise-cvalue :var (car gin.affect)
                                        :term term)))
    (new-context (atc-context-extend new-context (list premise)))
    (new-inscope-rules
     (cons
      'objdesign-of-var-of-update-object-iff
      (cons
       'read-object-of-objdesign-of-var-to-read-var
       (cons
        'read-var-of-update-object
        (cons
         'compustate-frames-number-of-add-var-not-zero
         (cons
          'compustate-frames-number-of-update-object
          (cons
           'read-var-of-add-var
           (cons
            'remove-flexible-array-member-when-absent
            (cons
             'not-flexible-array-member-p-when-ucharp
             (cons
              'not-flexible-array-member-p-when-scharp
              (cons
               'not-flexible-array-member-p-when-ushortp
               (cons
                'not-flexible-array-member-p-when-sshortp
                (cons
                 'not-flexible-array-member-p-when-uintp
                 (cons
                  'not-flexible-array-member-p-when-sintp
                  (cons
                   'not-flexible-array-member-p-when-ulongp
                   (cons
                    'not-flexible-array-member-p-when-slongp
                    (cons
                     'not-flexible-array-member-p-when-ullongp
                     (cons
                      'not-flexible-array-member-p-when-sllongp
                      (cons
                       'not-flexible-array-member-p-when-uchar-arrayp
                       (cons
                        'not-flexible-array-member-p-when-schar-arrayp
                        (cons
                         'not-flexible-array-member-p-when-ushort-arrayp
                         (cons
                          'not-flexible-array-member-p-when-sshort-arrayp
                          (cons
                           'not-flexible-array-member-p-when-uint-arrayp
                           (cons
                            'not-flexible-array-member-p-when-sint-arrayp
                            (cons
                             'not-flexible-array-member-p-when-ulong-arrayp
                             (cons
                              'not-flexible-array-member-p-when-slong-arrayp
                              (cons
                               'not-flexible-array-member-p-when-ullong-arrayp
                               (cons
                                'not-flexible-array-member-p-when-sllong-arrayp
                                (cons
                                 'not-flexible-array-member-p-when-value-pointer
                                 (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
                                            (cons
                                             'valuep-when-uchar-arrayp
                                             (cons
                                              'valuep-when-schar-arrayp
                                              (cons
                                               'valuep-when-ushort-arrayp
                                               (cons
                                                'valuep-when-sshort-arrayp
                                                (cons
                                                 'valuep-when-uint-arrayp
                                                 (cons
                                                  'valuep-when-sint-arrayp
                                                  (cons
                                                   'valuep-when-ulong-arrayp
                                                   (cons
                                                    'valuep-when-slong-arrayp
                                                    (cons
                                                     'valuep-when-ullong-arrayp
                                                     (cons
                                                      'valuep-when-sllong-arrayp
                                                      (append
                                                       (atc-string-taginfo-alist-to-valuep-thms
                                                        gin.prec-tags)
                                                       (cons
                                                        'read-object-of-update-object-same
                                                        (cons
                                                         'read-object-of-update-object-disjoint
                                                         (cons
                                                          called-fn-thm
                                                          (cons
                                                           guard-lemma-name
                                                           '(ident-fix-when-identp
                                                             identp-of-ident
                                                             equal-of-ident-and-ident
                                                             (:e
                                                              str-fix)
                                                             objdesign-of-var-of-update-static-var-iff
                                                             read-object-of-objdesign-static
                                                             read-var-to-read-static-var
                                                             read-static-var-of-update-static-var
                                                             var-autop-of-add-frame
                                                             var-autop-of-enter-scope
                                                             var-autop-of-add-var
                                                             var-autop-of-update-var
                                                             var-autop-of-update-static-var
                                                             var-autop-of-update-object
                                                             object-disjointp-commutative))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    ((mv new-inscope
         new-inscope-events names-to-avoid)
     (atc-gen-new-inscope gin.fn gin.fn-guard
                          gin.inscope new-context gin.compst-var
                          new-inscope-rules gin.prec-tags
                          thm-index names-to-avoid wrld))
    (thm-index (1+ thm-index))
    (events (append item-events new-inscope-events))
    (gout (atc-gen-block-item-list-one
               term (type-void)
               item item-limit events item-thm-name
               nil new-compst new-context new-inscope
               (change-stmt-gin gin
                                :thm-index thm-index
                                :names-to-avoid names-to-avoid
                                :proofs (and item-thm-name t))
               state)))
   (retok gout))))

Theorem: stmt-goutp-of-atc-gen-cfun-call-stmt.gout

(defthm stmt-goutp-of-atc-gen-cfun-call-stmt.gout
  (b* (((mv acl2::?erp ?gout)
        (atc-gen-cfun-call-stmt called-fn
                                arg-terms arg-types affect extobjs
                                limit called-fn-guard gin state)))
    (stmt-goutp gout))
  :rule-classes :rewrite)