		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-integer-asg

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

Signature
(atc-gen-block-item-integer-asg var val-term arg-term type integer-write-fn wrapper? 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).; val-term — Guard (pseudo-termp val-term).; arg-term — Guard (pseudo-termp arg-term).; type — Guard (typep type).; integer-write-fn — Guard (symbolp integer-write-fn).; wrapper? — Guard (symbolp wrapper?).; gin — Guard (stmt-ginp gin).
Returns: item — Type (block-itemp item).; val-term* — Type (pseudo-termp val-term*), given (symbolp integer-write-fn).; 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).

This is somewhat analogous to atc-gen-block-item-var-asg.

The limit is set to 3 more than the sum of the limits for left and right expressions (the maximum would also work): 1 to go from exec-block-item to exec-stmt, 1 to go from there to exec-expr, 1 to go from there to exec-expr on the left and right sides. The left side is a unary expression with the indirection operator, so we need 1 to go to the operand expression; the latter is always a variable, so we need 1 more to execute it.

Definitions and Theorems

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

(defun atc-gen-block-item-integer-asg
       (var val-term arg-term type
            integer-write-fn wrapper? gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp var)
                             (pseudo-termp val-term)
                             (pseudo-termp arg-term)
                             (typep type)
                             (symbolp integer-write-fn)
                             (symbolp wrapper?)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-integer-asg))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (irr-block-item)
     nil nil nil nil nil (irr-atc-context)
     1 nil)
    (wrld (w state))
    ((stmt-gin gin) gin)
    ((unless (eq wrapper? nil))
     (reterr
      (msg
       "The pointed integer write term ~x0 ~
               to which ~x1 is bound ~
               has the ~x2 wrapper, which is disallowed."
       val-term var wrapper?)))
    ((unless (member-eq var gin.affect))
     (reterr
      (msg
       "The pointed integer ~x0 is being written to, ~
               but it is not among the variables ~x1 ~
               currently affected."
       var gin.affect)))
    ((erp (expr-gout ptr))
     (atc-gen-expr-pure
          var
          (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))
    ((unless (equal ptr.type (type-pointer type)))
     (reterr
      (msg
       "The variable ~x0 of type ~x1 does not have ~
               the expected type ~x2. ~
               This is indicative of ~
               unreachable code under the guards, ~
               given that the code is guard-verified."
       var ptr.type (type-pointer type))))
    ((erp (expr-gout int))
     (atc-gen-expr-pure
          arg-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 ptr.thm-index
                         :names-to-avoid ptr.names-to-avoid
                         :proofs (and ptr.thm-name t))
          state))
    ((unless (equal int.type type))
     (reterr
      (msg
       "The term ~x0 of type ~x1 does not have ~
               the expected type ~x2. ~
               This is indicative of ~
               unreachable code under the guards, ~
               given that the code is guard-verified."
       arg-term int.type type)))
    (asg (make-expr-binary :op (binop-asg)
                           :arg1 (make-expr-unary :op (unop-indir)
                                                  :arg ptr.expr)
                           :arg2 int.expr))
    (stmt (stmt-expr asg))
    (item (block-item-stmt stmt))
    ((unless (expr-purep int.expr))
     (reterr (raise "Internal error: non-pure expression ~x0."
                    int.expr)))
    (var-limit ''1)
    (left-limit (cons '+
                      (cons ''1 (cons var-limit 'nil))))
    (right-limit (cons 'quote
                       (cons (expr-pure-limit int.expr) 'nil)))
    (expr-limit
     (cons
        '+
        (cons ''1
              (cons (cons '+
                          (cons left-limit (cons right-limit 'nil)))
                    'nil))))
    (stmt-limit (cons '+
                      (cons ''1 (cons expr-limit 'nil))))
    (item-limit (cons '+
                      (cons ''1 (cons stmt-limit 'nil))))
    ((when (eq integer-write-fn 'quote))
     (reterr (raise "Internal error: integer writer is QUOTE.")))
    (integer-write-term
         (cons integer-write-fn (cons int.term 'nil)))
    (varinfo (atc-get-var var gin.inscope))
    ((unless varinfo)
     (reterr
          (raise "Internal error: no information for variable ~x0."
                 var)))
    ((when (not int.thm-name))
     (retok item integer-write-term item-limit
            (append ptr.events int.events)
            nil gin.inscope gin.context
            int.thm-index int.names-to-avoid))
    (new-compst (cons 'update-object
                      (cons (add-suffix-to-fn var "-OBJDES")
                            (cons integer-write-term
                                  (cons gin.compst-var 'nil)))))
    (new-compst (untranslate$ new-compst nil state))
    (asg-thm-name (pack gin.fn '-correct- int.thm-index))
    ((mv asg-thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          asg-thm-name
          nil int.names-to-avoid wrld))
    (thm-index (1+ int.thm-index))
    (uterm (untranslate$ int.term nil state))
    (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 uterm '(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 int.type gin.prec-tags))
    (type-formula (cons pred (cons uterm '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))))
    (type-pred (atc-type-to-recognizer type gin.prec-tags))
    (exec-expr-when-asg-thm (pack 'exec-expr-when-asg-indir-when-
                                  type-pred '-for-modular-proofs))
    (value-kind-thm (atc-type-to-value-kind-thm type gin.prec-tags))
    (valuep-when-type-pred
         (atc-type-to-valuep-thm type gin.prec-tags))
    (type-of-value-thm
         (atc-type-to-type-of-value-thm type gin.prec-tags))
    (type-pred-of-integer-write-fn
         (pack type-pred '-of- integer-write-fn))
    (asg-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            exec-expr-when-asg-thm
            (cons
             '(:e expr-kind)
             (cons
              '(:e expr-binary->op)
              (cons
               '(:e expr-binary->arg1)
               (cons
                '(:e expr-binary->arg2)
                (cons
                 '(:e binop-kind)
                 (cons
                  '(:e expr-unary->op)
                  (cons
                   '(:e expr-unary->arg)
                   (cons
                    '(:e unop-kind)
                    (cons
                     'not-zp-of-limit-variable
                     (cons
                      'not-zp-of-limit-minus-const
                      (cons
                       '(:e expr-ident->get)
                       (cons
                        'read-var-of-const-identifier
                        (cons
                         '(:e identp)
                         (cons
                          '(:e ident->name)
                          (cons
                           'read-var-to-read-object-of-objdesign-of-var
                           (cons
                            (atc-var-info->thm varinfo)
                            (cons
                             ptr.thm-name
                             (cons
                              int.thm-name
                              (cons
                               'expr-valuep-of-expr-value
                               (cons
                                'apconvert-expr-value-when-not-value-array
                                (cons
                                 value-kind-thm
                                 (cons
                                  'expr-value->value-of-expr-value
                                  (cons
                                   'value-fix-when-valuep
                                   (cons
                                    valuep-when-type-pred
                                    (cons
                                     'write-object-to-update-object
                                     (cons
                                      'write-object-okp-of-add-var
                                      (cons
                                       'write-object-okp-of-add-frame
                                       (cons
                                        'write-object-okp-when-valuep-of-read-object-no-syntaxp
                                        (cons
                                         type-of-value-thm
                                         (cons
                                          type-pred-of-integer-write-fn
                                          '(compustatep-of-update-object
                                            expr-valuep-of-expr-value
                                            expr-value->value-of-expr-value
                                            value-fix-when-valuep
                                            (:e expr-purep)
                                            (:e expr-pure-limit)
                                            max))))))))))))))))))))))))))))))))
           '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 ptr.events int.events (list asg-event))
          asg-thm-name new-compst
          (change-stmt-gin gin
                           :thm-index thm-index
                           :names-to-avoid names-to-avoid
                           :proofs t)
          state))
    (new-context
     (atc-context-extend
      gin.context
      (list
        (make-atc-premise-cvalue :var var
                                 :term integer-write-term)
        (make-atc-premise-compustate
             :var gin.compst-var
             :term
             (cons 'update-object
                   (cons (add-suffix-to-fn var "-OBJDES")
                         (cons var (cons gin.compst-var 'nil))))))))
    (type-pred-of-type-write (pack type-pred '-of-
                                   (type-kind type)
                                   '-write))
    (not-flexible-array-member-p-when-type-pred
         (pack 'not-flexible-array-member-p-when-
               type-pred))
    (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
          'read-object-of-update-object-same
          (cons
           'read-object-of-update-object-disjoint
           (cons
            'object-disjointp-commutative
            (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-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
                                     type-pred-of-type-write
                                     (cons
                                      not-flexible-array-member-p-when-type-pred
                                      '(ident-fix-when-identp
                                        identp-of-ident
                                        equal-of-ident-and-ident
                                        (:e str-fix)
                                        read-var-of-update-object
                                        compustate-frames-number-of-enter-scope-not-zero
                                        read-var-of-enter-scope
                                        read-var-of-update-object
                                        compustate-frames-number-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 integer-write-term item-limit
          events item-thm-name new-inscope
          new-context thm-index names-to-avoid))))

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

(defthm block-itemp-of-atc-gen-block-item-integer-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-integer-asg
             var val-term arg-term type
             integer-write-fn wrapper? gin state)))
    (block-itemp item))
  :rule-classes :rewrite)

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

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

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

(defthm pseudo-termp-of-atc-gen-block-item-integer-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-integer-asg
             var val-term arg-term type
             integer-write-fn wrapper? gin state)))
    (pseudo-termp limit))
  :rule-classes :rewrite)

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

(defthm
   pseudo-event-form-listp-of-atc-gen-block-item-integer-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-integer-asg
             var val-term arg-term type
             integer-write-fn wrapper? gin state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

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

(defthm symbolp-of-atc-gen-block-item-integer-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-integer-asg
             var val-term arg-term type
             integer-write-fn wrapper? gin state)))
    (symbolp thm-name))
  :rule-classes :rewrite)

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

(defthm
 atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-integer-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-integer-asg
            var val-term arg-term type
            integer-write-fn wrapper? gin state)))
   (atc-symbol-varinfo-alist-listp new-inscope))
 :rule-classes :rewrite)

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

(defthm atc-contextp-of-atc-gen-block-item-integer-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-integer-asg
             var val-term arg-term type
             integer-write-fn wrapper? gin state)))
    (atc-contextp new-context))
  :rule-classes :rewrite)

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

(defthm posp-of-atc-gen-block-item-integer-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-integer-asg
             var val-term arg-term type
             integer-write-fn wrapper? gin state)))
    (posp thm-index))
  :rule-classes :rewrite)

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

(defthm
      symbol-listp-of-atc-gen-block-item-integer-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-integer-asg
             var val-term arg-term type
             integer-write-fn wrapper? gin state)))
    (symbol-listp names-to-avoid))
  :rule-classes :rewrite)