		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-var-asg

Generate a C block item statement that consists of an assignment to a variable.

Signature
(atc-gen-block-item-var-asg var var-info? val-term gin state) → (mv erp item val-term* limit events thm-name new-inscope new-context thm-index names-to-avoid)
Arguments: var — Guard (symbolp var).; var-info? — Guard (atc-var-info-optionp var-info?).; val-term — Guard (pseudo-termp val-term).; gin — Guard (stmt-ginp gin).
Returns: item — Type (block-itemp item).; val-term* — Type (pseudo-termp val-term*), given (pseudo-termp val-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).

The limit is set to 3 more than the limit for the right expression. We need 1 to go from exec-block-item to exec-stmt, 1 to go from there to exec-expr on the assignment, 1 to go from there to exec-expr to the left and right side. The left side is a variable so it just needs 1, so the limit for the right side, which is always at least 1, covers it.

Definitions and Theorems

Function: atc-gen-block-item-var-asg

(defun atc-gen-block-item-var-asg (var var-info? val-term gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp var)
                             (atc-var-info-optionp var-info?)
                             (pseudo-termp val-term)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-var-asg))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (irr-block-item)
     nil nil nil nil nil (irr-atc-context)
     1 nil)
    ((stmt-gin gin) gin)
    (wrld (w state))
    ((unless var-info?)
     (reterr
          (raise "Internal error: no information for variable ~x0."
                 var)))
    (var-info var-info?)
    (prev-type (atc-var-info->type var-info))
    ((erp rhs.expr rhs.type rhs.term rhs.result
          & rhs.limit rhs.events rhs.thm-name
          & & rhs.thm-index rhs.names-to-avoid)
     (atc-gen-expr val-term
                   (change-stmt-gin gin :affect nil)
                   state))
    ((unless (equal prev-type rhs.type))
     (reterr
      (msg
       "The type ~x0 of the term ~x1 ~
               assigned to the LET variable ~x2 ~
               of the function ~x3 ~
               differs from the type ~x4 ~
               of a variable with the same symbol in scope."
       rhs.type
       val-term var gin.fn prev-type)))
    ((when (type-case rhs.type :array))
     (reterr
      (msg
       "The term ~x0 to which the variable ~x1 is bound ~
               must not have a C array type, ~
               but it has type ~x2 instead."
       val-term var rhs.type)))
    ((when (type-case rhs.type :pointer))
     (reterr
      (msg
       "The term ~x0 to which the variable ~x1 is bound ~
               must not have a C pointer type, ~
               but it has type ~x2 instead."
       val-term var rhs.type)))
    (asg
        (make-expr-binary
             :op (binop-asg)
             :arg1 (expr-ident (make-ident :name (symbol-name var)))
             :arg2 rhs.expr))
    (stmt (stmt-expr asg))
    (item (block-item-stmt stmt))
    (expr-limit (cons '+
                      (cons ''1 (cons rhs.limit 'nil))))
    (stmt-limit (cons '+
                      (cons ''1 (cons expr-limit 'nil))))
    (item-limit (cons '+
                      (cons ''1 (cons stmt-limit 'nil))))
    ((when (not rhs.thm-name))
     (retok item rhs.term item-limit
            rhs.events nil gin.inscope gin.context
            rhs.thm-index rhs.names-to-avoid))
    (new-compst
      (if
        (atc-var-info->externalp var-info)
        (cons 'update-static-var
              (cons (cons 'ident
                          (cons (cons 'quote
                                      (cons (symbol-name var) 'nil))
                                'nil))
                    (cons rhs.term (cons gin.compst-var 'nil))))
        (cons 'update-var
              (cons (cons 'ident
                          (cons (cons 'quote
                                      (cons (symbol-name var) 'nil))
                                'nil))
                    (cons rhs.term (cons gin.compst-var 'nil))))))
    (new-compst (untranslate$ new-compst nil state))
    (asg-thm-name (pack gin.fn '-correct- rhs.thm-index))
    ((mv asg-thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          asg-thm-name
          nil rhs.names-to-avoid wrld))
    (thm-index (1+ rhs.thm-index))
    (exec-formula
     (cons
         'equal
         (cons (cons 'exec-expr
                     (cons (cons 'quote (cons asg 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons (cons 'expr-value
                                       (cons rhs.result '(nil)))
                                 (cons new-compst 'nil)))
                     'nil))))
    (exec-formula
         (atc-contextualize exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var expr-limit t wrld))
    (pred (atc-type-to-recognizer rhs.type gin.prec-tags))
    (type-formula (cons pred (cons rhs.result 'nil)))
    (type-formula
         (atc-contextualize type-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (asg-formula
         (cons 'and
               (cons exec-formula (cons type-formula 'nil))))
    (valuep-when-type
         (atc-type-to-valuep-thm rhs.type gin.prec-tags))
    (value-kind-when-type-pred
         (atc-type-to-value-kind-thm rhs.type gin.prec-tags))
    (type-of-value-when-type
         (atc-type-to-type-of-value-thm rhs.type gin.prec-tags))
    (asg-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-expr-when-asg-ident-via-object
            (cons
             '(:e expr-kind)
             (cons
              '(:e expr-binary->op)
              (cons
               '(:e expr-binary->arg1)
               (cons
                '(:e expr-binary->arg2)
                (cons
                 '(:e binop-kind)
                 (cons
                  'not-zp-of-limit-variable
                  (cons
                   'not-zp-of-limit-minus-const
                   (cons
                    rhs.thm-name
                    (cons
                     'mv-nth-of-cons
                     (cons
                      '(:e zp)
                      (cons
                       valuep-when-type
                       (cons
                        'objdesign-of-var-of-const-identifier
                        (cons
                         '(:e identp)
                         (cons
                          '(:e ident->name)
                          (cons
                           '(:e expr-ident->get)
                           (cons
                            (atc-var-info->thm var-info)
                            (cons
                             'write-object-of-objdesign-of-var-to-write-var
                             (cons
                              'write-var-to-update-var
                              (cons
                               'compustate-frames-number-of-add-var-not-zero
                               (cons
                                'compustate-frames-number-of-enter-scope-not-zero
                                (cons
                                 'compustate-frames-number-of-add-frame-not-zero
                                 (cons
                                  'compustate-frames-number-of-update-var
                                  (cons
                                   'write-var-okp-of-add-var
                                   (cons
                                    'write-var-okp-of-enter-scope
                                    (cons
                                     'write-var-okp-of-update-var
                                     (cons
                                      'ident-fix-when-identp
                                      (cons
                                       'identp-of-ident
                                       (cons
                                        'equal-of-ident-and-ident
                                        (cons
                                         '(:e str-fix)
                                         (cons
                                          type-of-value-when-type
                                          (cons
                                           'write-var-to-write-static-var
                                           (cons
                                            'var-autop-of-add-frame
                                            (cons
                                             'var-autop-of-enter-scope
                                             (cons
                                              'var-autop-of-add-var
                                              (cons
                                               'var-autop-of-update-var
                                               (cons
                                                'var-autop-of-update-static-var
                                                (cons
                                                 'var-autop-of-update-object
                                                 (cons
                                                  'write-static-var-to-update-static-var
                                                  (cons
                                                   'write-static-var-okp-of-add-var
                                                   (cons
                                                    'write-static-var-okp-of-enter-scope
                                                    (cons
                                                     'write-static-var-okp-of-add-frame
                                                     (cons
                                                      'write-static-var-okp-when-valuep-of-read-static-var
                                                      (cons
                                                       'read-object-of-objdesign-static
                                                       (cons
                                                        'compustatep-of-update-var
                                                        (cons
                                                         'compustatep-of-update-static-var
                                                         (cons
                                                          'expr-valuep-of-expr-value
                                                          (cons
                                                           'expr-value->value-of-expr-value
                                                           (cons
                                                            'value-fix-when-valuep
                                                            (cons
                                                             value-kind-when-type-pred
                                                             '(apconvert-expr-value-when-not-value-array)))))))))))))))))))))))))))))))))))))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv asg-event &)
     (evmac-generate-defthm asg-thm-name
                            :formula asg-formula
                            :hints asg-hints
                            :enable nil))
    ((mv item item-limit item-events
         item-thm-name thm-index names-to-avoid)
     (atc-gen-block-item-asg
          asg expr-limit
          (append rhs.events (list asg-event))
          asg-thm-name new-compst
          (change-stmt-gin gin
                           :thm-index thm-index
                           :names-to-avoid names-to-avoid
                           :proofs (and asg-thm-name t))
          state))
    (new-context
     (atc-context-extend
      gin.context
      (list
       (make-atc-premise-cvalue :var var
                                :term rhs.term)
       (make-atc-premise-compustate
          :var gin.compst-var :term
          (if (atc-var-info->externalp var-info)
              (cons 'update-static-var
                    (cons (cons 'ident
                                (cons (symbol-name var) 'nil))
                          (cons var (cons gin.compst-var 'nil))))
            (cons 'update-var
                  (cons (cons 'ident
                              (cons (symbol-name var) 'nil))
                        (cons var (cons gin.compst-var 'nil)))))))))
    (notflexarrmem-thms
         (atc-type-to-notflexarrmem-thms rhs.type gin.prec-tags))
    (new-inscope-rules
     (cons
      rhs.thm-name
      (cons
       'remove-flexible-array-member-when-absent
       (append
        notflexarrmem-thms
        (cons
         'value-fix-when-valuep
         (cons
          valuep-when-type
          '(objdesign-of-var-of-update-var-iff
            read-object-of-objdesign-of-var-of-update-var
            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-of-var-of-update-static-var-different
            read-object-of-objdesign-of-var-of-update-static-var-same
            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)))))))
    ((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)))
   (retok item rhs.term item-limit
          events item-thm-name new-inscope
          new-context thm-index names-to-avoid))))

Theorem: block-itemp-of-atc-gen-block-item-var-asg.item

(defthm block-itemp-of-atc-gen-block-item-var-asg.item
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (block-itemp item))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-block-item-var-asg.val-term*

(defthm pseudo-termp-of-atc-gen-block-item-var-asg.val-term*
 (implies
  (pseudo-termp val-term)
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (pseudo-termp val-term*)))
 :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-block-item-var-asg.limit

(defthm pseudo-termp-of-atc-gen-block-item-var-asg.limit
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (pseudo-termp limit))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-block-item-var-asg.events

(defthm pseudo-event-form-listp-of-atc-gen-block-item-var-asg.events
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-block-item-var-asg.thm-name

(defthm symbolp-of-atc-gen-block-item-var-asg.thm-name
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (symbolp thm-name))
  :rule-classes :rewrite)

Theorem: atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-var-asg.new-inscope

(defthm
 atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-var-asg.new-inscope
 (b*
  (((mv acl2::?erp ?item ?val-term*
        ?limit ?events ?thm-name ?new-inscope
        ?new-context ?thm-index ?names-to-avoid)
    (atc-gen-block-item-var-asg var var-info? val-term gin state)))
  (atc-symbol-varinfo-alist-listp new-inscope))
 :rule-classes :rewrite)

Theorem: atc-contextp-of-atc-gen-block-item-var-asg.new-context

(defthm atc-contextp-of-atc-gen-block-item-var-asg.new-context
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (atc-contextp new-context))
  :rule-classes :rewrite)

Theorem: posp-of-atc-gen-block-item-var-asg.thm-index

(defthm posp-of-atc-gen-block-item-var-asg.thm-index
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (posp thm-index))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-block-item-var-asg.names-to-avoid

(defthm symbol-listp-of-atc-gen-block-item-var-asg.names-to-avoid
  (b*
   (((mv acl2::?erp ?item ?val-term*
         ?limit ?events ?thm-name ?new-inscope
         ?new-context ?thm-index ?names-to-avoid)
     (atc-gen-block-item-var-asg var var-info? val-term gin state)))
   (symbol-listp names-to-avoid))
  :rule-classes :rewrite)