		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-if/ifelse-stmt

Generate a C if or if-else statement from an ACL2 term.

Signature
(atc-gen-if/ifelse-stmt test-term then-term else-term test-expr then-items else-items test-type then-type else-type then-limit else-limit test-thm then-thm else-thm then-context-start else-context-start then-context-end else-context-end then-inscope else-inscope test-events then-events else-events gin state) → (mv erp gout)
Arguments: test-term — Guard (pseudo-termp test-term).; then-term — Guard (pseudo-termp then-term).; else-term — Guard (pseudo-termp else-term).; test-expr — Guard (exprp test-expr).; then-items — Guard (block-item-listp then-items).; else-items — Guard (block-item-listp else-items).; test-type — Guard (typep test-type).; then-type — Guard (typep then-type).; else-type — Guard (typep else-type).; then-limit — Guard (pseudo-termp then-limit).; else-limit — Guard (pseudo-termp else-limit).; test-thm — Guard (symbolp test-thm).; then-thm — Guard (symbolp then-thm).; else-thm — Guard (symbolp else-thm).; then-context-start — Guard (atc-contextp then-context-start).; else-context-start — Guard (atc-contextp else-context-start).; then-context-end — Guard (atc-contextp then-context-end).; else-context-end — Guard (atc-contextp else-context-end).; then-inscope — Guard (atc-symbol-varinfo-alist-listp then-inscope).; else-inscope — Guard (atc-symbol-varinfo-alist-listp else-inscope).; test-events — Guard (pseudo-event-form-listp test-events).; then-events — Guard (pseudo-event-form-listp then-events).; else-events — Guard (pseudo-event-form-listp else-events).; gin — Guard (stmt-ginp gin).
Returns: gout — Type (stmt-goutp gout).

We generate an if if the `else' branch is empty. Otherwise we generate an if-else.

We generate a theorem for each branch: each theorem is about the compound statement that consists of the block items of the branch. Recall that atc-gen-stmt recursively generates theorems for those lists of block items; these are put into compound statements that become the actual branches of the conditional, so we need to lift the theorems to those compound statements. We generate the theorem for the `else' compound statement regardless of whether it is empty or not, for uniformity. The limit for each compound statement is 1 plus the one for the block item list, because we need 1 to go from exec-stmt to the :compound case and exec-block-item-list.

We generate a theorem for the conditional statement, based on the theorems for the test and branches. We turn the ACL2 if into if*, to prevent unwanted case splits in larger terms that may contain this term (as we generate C code from those larger terms). We use proof builder commands to split on this if*. The limit for the conditional statement is one more than the sum of the ones for the branches; we could take one plus the maximum, but the sum avoids case splits. We include the compound recognizer booleanp-compound-recognizer for the same reason explained in atc-gen-expr-bool-from-type.

We lift the theorem for the conditional statement to a block item and to a singleton list of block items.

The generation of modular proofs in this code currently assumes that the if returns a single value, which is either the returned C value (if the C type is not void), or a side-effected variables (if the C type is void). This is reflected in the generated modular theorems. This will need to be generalized.

Definitions and Theorems

Function: atc-gen-if/ifelse-stmt

(defun atc-gen-if/ifelse-stmt
       (test-term then-term else-term
                  test-expr then-items else-items
                  test-type then-type else-type then-limit
                  else-limit test-thm then-thm else-thm
                  then-context-start else-context-start
                  then-context-end else-context-end
                  then-inscope else-inscope test-events
                  then-events else-events gin state)
 (declare (xargs :stobjs (state)))
 (declare
    (xargs :guard (and (pseudo-termp test-term)
                       (pseudo-termp then-term)
                       (pseudo-termp else-term)
                       (exprp test-expr)
                       (block-item-listp then-items)
                       (block-item-listp else-items)
                       (typep test-type)
                       (typep then-type)
                       (typep else-type)
                       (pseudo-termp then-limit)
                       (pseudo-termp else-limit)
                       (symbolp test-thm)
                       (symbolp then-thm)
                       (symbolp else-thm)
                       (atc-contextp then-context-start)
                       (atc-contextp else-context-start)
                       (atc-contextp then-context-end)
                       (atc-contextp else-context-end)
                       (atc-symbol-varinfo-alist-listp then-inscope)
                       (atc-symbol-varinfo-alist-listp else-inscope)
                       (pseudo-event-form-listp test-events)
                       (pseudo-event-form-listp then-events)
                       (pseudo-event-form-listp else-events)
                       (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-if/ifelse-stmt))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-stmt-gout))
    ((stmt-gin gin) gin)
    (wrld (w state))
    ((unless (equal then-type else-type))
     (reterr
      (msg
       "When generating C code for the function ~x0, ~
               two branches ~x1 and ~x2 of a conditional term ~
               have different types ~x3 and ~x4; ~
               use conversion operations, if needed, ~
               to make the branches of the same type."
       gin.fn then-term
       else-term then-type else-type)))
    (type then-type)
    (voidp (type-case type :void))
    (then-stmt (make-stmt-compound :items then-items))
    (else-stmt (make-stmt-compound :items else-items))
    (stmt (if (consp else-items)
              (make-stmt-ifelse :test test-expr
                                :then then-stmt
                                :else else-stmt)
            (make-stmt-if :test test-expr
                          :then then-stmt)))
    (term (cons 'if*
                (cons test-term
                      (cons then-term (cons else-term 'nil)))))
    ((when (not gin.proofs))
     (retok
      (make-stmt-gout
       :items (list (block-item-stmt stmt))
       :type type
       :term term
       :context gin.context
       :inscope gin.inscope
       :limit
       (pseudo-term-fncall
           'binary-+
           (list (pseudo-term-quote 5)
                 (pseudo-term-fncall 'binary-+
                                     (list then-limit else-limit))))
       :events (append test-events then-events else-events)
       :thm-name nil
       :thm-index gin.thm-index
       :names-to-avoid gin.names-to-avoid)))
    (thm-index gin.thm-index)
    (names-to-avoid gin.names-to-avoid)
    (then-stmt-thm (pack gin.fn '-correct- thm-index))
    (thm-index (1+ thm-index))
    ((mv then-stmt-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          then-stmt-thm nil names-to-avoid wrld))
    (else-stmt-thm (pack gin.fn '-correct- thm-index))
    (thm-index (1+ thm-index))
    ((mv else-stmt-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          else-stmt-thm nil names-to-avoid wrld))
    (valuep-when-type-pred
         (and (not voidp)
              (atc-type-to-valuep-thm type gin.prec-tags)))
    (then-stmt-limit (cons 'binary-+
                           (cons ''1 (cons then-limit 'nil))))
    (else-stmt-limit (cons 'binary-+
                           (cons ''1 (cons else-limit 'nil))))
    (then-uterm (untranslate$ then-term nil state))
    (else-uterm (untranslate$ else-term nil state))
    ((mv then-result then-stmt-type-formula &)
     (atc-gen-uterm-result-and-type-formula
          then-uterm type
          gin.affect gin.inscope gin.prec-tags))
    ((mv else-result else-stmt-type-formula &)
     (atc-gen-uterm-result-and-type-formula
          else-uterm type
          gin.affect gin.inscope gin.prec-tags))
    (then-context-end
         (atc-context-extend
              then-context-end
              (list (make-atc-premise-compustate
                         :var gin.compst-var
                         :term (cons 'exit-scope
                                     (cons gin.compst-var 'nil))))))
    (else-context-end
         (atc-context-extend
              else-context-end
              (list (make-atc-premise-compustate
                         :var gin.compst-var
                         :term (cons 'exit-scope
                                     (cons gin.compst-var 'nil))))))
    (then-new-compst (atc-contextualize-compustate
                          gin.compst-var
                          then-context-start then-context-end))
    (else-new-compst (atc-contextualize-compustate
                          gin.compst-var
                          else-context-start else-context-end))
    (then-stmt-exec-formula
     (cons
         'equal
         (cons (cons 'exec-stmt
                     (cons (cons 'quote (cons then-stmt 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons then-result
                                 (cons then-new-compst 'nil)))
                     'nil))))
    (then-stmt-exec-formula
         (atc-contextualize then-stmt-exec-formula
                            then-context-start
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var then-stmt-limit t wrld))
    (else-stmt-exec-formula
     (cons
         'equal
         (cons (cons 'exec-stmt
                     (cons (cons 'quote (cons else-stmt 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons else-result
                                 (cons else-new-compst 'nil)))
                     'nil))))
    (else-stmt-exec-formula
         (atc-contextualize else-stmt-exec-formula
                            else-context-start
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var else-stmt-limit t wrld))
    (then-stmt-type-formula
         (atc-contextualize then-stmt-type-formula
                            then-context-start gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (else-stmt-type-formula
         (atc-contextualize else-stmt-type-formula
                            else-context-start gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (then-stmt-formula
         (cons 'and
               (cons then-stmt-exec-formula
                     (cons then-stmt-type-formula 'nil))))
    (else-stmt-formula
         (cons 'and
               (cons else-stmt-exec-formula
                     (cons else-stmt-type-formula 'nil))))
    (then-stmt-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-stmt-when-compound
            (cons
             '(:e stmt-kind)
             (cons
              'not-zp-of-limit-variable
              (cons
               '(:e stmt-compound->items)
               (cons
                then-thm
                (cons
                 'mv-nth-of-cons
                 (cons
                  '(:e zp)
                  (cons
                   '(:e value-optionp)
                   (cons
                    'value-optionp-when-valuep
                    (append
                     (and (not voidp)
                          (list valuep-when-type-pred))
                     '(exit-scope-of-enter-scope
                       exit-scope-of-add-var
                       compustate-frames-number-of-add-frame-not-zero
                       compustate-frames-number-of-enter-scope-not-zero
                       compustate-frames-number-of-add-var-not-zero
                       compustatep-of-add-frame
                       compustatep-of-add-var
                       compustatep-of-enter-scope
                       uchar-array-length-of-uchar-array-write
                       schar-array-length-of-schar-array-write
                       ushort-array-length-of-ushort-array-write
                       sshort-array-length-of-sshort-array-write
                       uint-array-length-of-uint-array-write
                       sint-array-length-of-sint-array-write
                       ulong-array-length-of-ulong-array-write
                       slong-array-length-of-slong-array-write
                       ullong-array-length-of-ullong-array-write
                       sllong-array-length-of-sllong-array-write)))))))))))
           'nil))
         'nil)))
      'nil))
    (else-stmt-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-stmt-when-compound
            (cons
             '(:e stmt-kind)
             (cons
              'not-zp-of-limit-variable
              (cons
               '(:e stmt-compound->items)
               (cons
                else-thm
                (cons
                 'mv-nth-of-cons
                 (cons
                  '(:e zp)
                  (cons
                   '(:e value-optionp)
                   (cons
                    'value-optionp-when-valuep
                    (append
                     (and (not voidp)
                          (list valuep-when-type-pred))
                     '(exit-scope-of-enter-scope
                       exit-scope-of-add-var
                       compustate-frames-number-of-add-frame-not-zero
                       compustate-frames-number-of-enter-scope-not-zero
                       compustate-frames-number-of-add-var-not-zero
                       compustatep-of-add-frame
                       compustatep-of-add-var
                       compustatep-of-enter-scope
                       uchar-array-length-of-uchar-array-write
                       schar-array-length-of-schar-array-write
                       ushort-array-length-of-ushort-array-write
                       sshort-array-length-of-sshort-array-write
                       uint-array-length-of-uint-array-write
                       sint-array-length-of-sint-array-write
                       ulong-array-length-of-ulong-array-write
                       slong-array-length-of-slong-array-write
                       ullong-array-length-of-ullong-array-write
                       sllong-array-length-of-sllong-array-write)))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv then-stmt-event &)
     (evmac-generate-defthm then-stmt-thm
                            :formula then-stmt-formula
                            :hints then-stmt-hints
                            :enable nil))
    ((mv else-stmt-event &)
     (evmac-generate-defthm else-stmt-thm
                            :formula else-stmt-formula
                            :hints else-stmt-hints
                            :enable nil))
    (if-stmt-thm (pack gin.fn '-correct- thm-index))
    (thm-index (1+ thm-index))
    ((mv if-stmt-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          if-stmt-thm nil names-to-avoid wrld))
    (if-stmt-limit
         (cons 'binary-+
               (cons ''1
                     (cons (cons 'binary-+
                                 (cons then-stmt-limit
                                       (cons else-stmt-limit 'nil)))
                           'nil))))
    (uterm (untranslate$ term nil state))
    ((mv if-result
         if-stmt-type-formula if-stmt-type-thms)
     (atc-gen-uterm-result-and-type-formula
          uterm type
          gin.affect gin.inscope gin.prec-tags))
    (test-uterm (untranslate$ test-term nil state))
    (new-compst (cons 'if*
                      (cons test-uterm
                            (cons then-new-compst
                                  (cons else-new-compst 'nil)))))
    (if-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 if-result (cons new-compst 'nil)))
                     'nil))))
    (if-stmt-exec-formula
         (atc-contextualize if-stmt-exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var if-stmt-limit t wrld))
    (if-stmt-type-formula
         (atc-contextualize if-stmt-type-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (if-stmt-formula (cons 'and
                           (cons if-stmt-exec-formula
                                 (cons if-stmt-type-formula 'nil))))
    (test-type-pred
         (atc-type-to-recognizer test-type gin.prec-tags))
    (valuep-when-test-type-pred (pack 'valuep-when- test-type-pred))
    (value-kind-when-test-type-pred
         (pack 'value-kind-when- test-type-pred))
    (if-stmt-hints
     (if
      (consp else-items)
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
            (cons
             'exec-stmt-when-ifelse-and-true
             (cons
              'exec-stmt-when-ifelse-and-false
              (cons
               '(:e stmt-kind)
               (cons
                'not-zp-of-limit-variable
                (cons
                 '(:e stmt-ifelse->test)
                 (cons
                  test-thm
                  (append
                   (and (not voidp)
                        (list valuep-when-type-pred))
                   (cons
                    '(:e stmt-ifelse->then)
                    (cons
                     then-stmt-thm
                     (cons
                      '(:e stmt-ifelse->else)
                      (cons
                       else-stmt-thm
                       (cons
                        valuep-when-test-type-pred
                        (cons
                         'booleanp-compound-recognizer
                         (cons
                          'expr-valuep-of-expr-value
                          (cons
                           'expr-value->value-of-expr-value
                           (cons
                            'value-fix-when-valuep
                            (cons
                             valuep-when-test-type-pred
                             (cons
                              'apconvert-expr-value-when-not-value-array
                              (cons
                               value-kind-when-test-type-pred
                               '(uchar-array-length-of-uchar-array-write
                                 schar-array-length-of-schar-array-write
                                 ushort-array-length-of-ushort-array-write
                                 sshort-array-length-of-sshort-array-write
                                 uint-array-length-of-uint-array-write
                                 sint-array-length-of-sint-array-write
                                 ulong-array-length-of-ulong-array-write
                                 slong-array-length-of-slong-array-write
                                 ullong-array-length-of-ullong-array-write
                                 sllong-array-length-of-sllong-array-write
                                 mv-nth-of-cons
                                 (:e zp)))))))))))))))))))))
            'nil))
          'nil)))
       'nil)
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons
           'quote
           (cons
            (cons
             'exec-stmt-when-if-and-true
             (cons
              'exec-stmt-when-if-and-false
              (cons
               '(:e stmt-kind)
               (cons
                'not-zp-of-limit-variable
                (cons
                 '(:e stmt-if->test)
                 (cons
                  test-thm
                  (append
                   (and (not voidp)
                        (list valuep-when-type-pred))
                   (cons
                    '(:e stmt-if->then)
                    (cons
                     then-stmt-thm
                     (cons
                      valuep-when-test-type-pred
                      (cons
                       'booleanp-compound-recognizer
                       (cons
                        'expr-valuep-of-expr-value
                        (cons
                         'expr-value->value-of-expr-value
                         (cons
                          'value-fix-when-valuep
                          (cons
                           valuep-when-test-type-pred
                           (cons
                            'apconvert-expr-value-when-not-value-array
                            (cons
                             value-kind-when-test-type-pred
                             (cons
                              'compustatep-of-add-var
                              (cons
                               'compustate-frames-number-of-add-var-not-zero
                               (cons
                                'exit-scope-of-enter-scope
                                (append
                                 if-stmt-type-thms
                                 '(uchar-array-length-of-uchar-array-write
                                   schar-array-length-of-schar-array-write
                                   ushort-array-length-of-ushort-array-write
                                   sshort-array-length-of-sshort-array-write
                                   uint-array-length-of-uint-array-write
                                   sint-array-length-of-sint-array-write
                                   ulong-array-length-of-ulong-array-write
                                   slong-array-length-of-slong-array-write
                                   ullong-array-length-of-ullong-array-write
                                   sllong-array-length-of-sllong-array-write
                                   mv-nth-of-cons
                                   (:e zp)))))))))))))))))))))))
            'nil))
          'nil)))
       'nil)))
    (if-stmt-instructions
     (cons
      (cons 'casesplit
            (cons (atc-contextualize test-term gin.context
                                     nil nil nil nil nil nil wrld)
                  'nil))
      (cons
       (cons
        'claim
        (cons (atc-contextualize (cons 'test* (cons test-term 'nil))
                                 gin.context
                                 nil nil nil nil nil nil wrld)
              '(:hints (("Goal" :in-theory '(test*))))))
       (cons
        '(drop 1)
        (cons
         (cons
          'claim
          (cons
           (atc-contextualize
            (cons
             'equal
             (cons
                (cons 'if*
                      (cons test-term
                            (cons then-term (cons else-term 'nil))))
                (cons then-term 'nil)))
            gin.context
            nil nil nil nil nil nil wrld)
           '(:hints
               (("Goal" :in-theory '(acl2::if*-when-true test*))))))
         (cons
          (cons
           'claim
           (cons
            (atc-contextualize
                (cons 'equal
                      (cons new-compst (cons then-new-compst 'nil)))
                gin.context
                nil nil gin.compst-var nil nil nil wrld)
            '(:hints
               (("Goal" :in-theory '(acl2::if*-when-true test*))))))
          (cons
           (cons 'prove
                 (cons ':hints
                       (cons if-stmt-hints 'nil)))
           (cons
            (cons
             'claim
             (cons
                  (atc-contextualize
                       (cons 'test*
                             (cons (cons 'not (cons test-term 'nil))
                                   'nil))
                       gin.context
                       nil nil nil nil nil nil wrld)
                  '(:hints (("Goal" :in-theory '(test*))))))
            (cons
             '(drop 1)
             (cons
              (cons
               'claim
               (cons
                (atc-contextualize
                 (cons
                  'equal
                  (cons
                   (cons
                      'if*
                      (cons test-term
                            (cons then-term (cons else-term 'nil))))
                   (cons else-term 'nil)))
                 gin.context
                 nil nil nil nil nil nil wrld)
                '(:hints
                  (("Goal"
                       :in-theory '(acl2::if*-when-false test*))))))
              (cons
               (cons
                'claim
                (cons
                 (atc-contextualize
                  (cons
                      'equal
                      (cons new-compst (cons else-new-compst 'nil)))
                  gin.context
                  nil nil gin.compst-var nil nil nil wrld)
                 '(:hints
                   (("Goal"
                       :in-theory '(acl2::if*-when-false test*))))))
               (cons (cons 'prove
                           (cons ':hints
                                 (cons if-stmt-hints 'nil)))
                     'nil))))))))))))
    ((mv if-stmt-event &)
     (evmac-generate-defthm if-stmt-thm
                            :formula if-stmt-formula
                            :instructions if-stmt-instructions
                            :enable nil))
    ((mv item item-limit item-events
         item-thm-name thm-index names-to-avoid)
     (atc-gen-block-item-stmt
          stmt if-stmt-limit
          (append test-events then-events else-events
                  (list then-stmt-event
                        else-stmt-event if-stmt-event))
          if-stmt-thm
          (untranslate$ term nil state)
          type if-result new-compst
          (change-stmt-gin gin
                           :thm-index thm-index
                           :names-to-avoid names-to-avoid
                           :proofs (and if-stmt-thm t))
          state))
    (new-context
        (atc-context-extend
             gin.context
             (list (make-atc-premise-compustate :var gin.compst-var
                                                :term new-compst))))
    (new-context
     (if (consp gin.affect)
         (if (consp (cdr gin.affect))
             (atc-context-extend
                  new-context
                  (list (make-atc-premise-cvalues :vars gin.affect
                                                  :term uterm)))
           (atc-context-extend
                new-context
                (list (make-atc-premise-cvalue :var (car gin.affect)
                                               :term uterm))))
       new-context))
    ((mv new-inscope new-inscope-events
         thm-index names-to-avoid)
     (if voidp (atc-gen-if/ifelse-inscope
                    gin.fn
                    gin.fn-guard gin.inscope then-inscope
                    else-inscope gin.context new-context
                    (untranslate$ test-term nil state)
                    (untranslate$ then-term nil state)
                    (untranslate$ else-term nil state)
                    gin.compst-var
                    new-compst then-new-compst
                    else-new-compst gin.prec-tags
                    thm-index names-to-avoid wrld)
       (mv nil nil thm-index names-to-avoid))))
   (retok (atc-gen-block-item-list-one
               term type item item-limit
               (append item-events new-inscope-events)
               item-thm-name if-result new-compst
               new-context (and voidp new-inscope)
               (change-stmt-gin gin
                                :thm-index thm-index
                                :names-to-avoid names-to-avoid
                                :proofs (and item-thm-name t))
               state)))))

Theorem: stmt-goutp-of-atc-gen-if/ifelse-stmt.gout

(defthm stmt-goutp-of-atc-gen-if/ifelse-stmt.gout
 (b*
  (((mv acl2::?erp ?gout)
    (atc-gen-if/ifelse-stmt test-term then-term else-term
                            test-expr then-items else-items
                            test-type then-type else-type then-limit
                            else-limit test-thm then-thm else-thm
                            then-context-start else-context-start
                            then-context-end else-context-end
                            then-inscope else-inscope test-events
                            then-events else-events gin state)))
  (stmt-goutp gout))
 :rule-classes :rewrite)