		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-expr-when-asg-arrsub-rules-generation

Code to generate the rules for executing assignments to array subscripting expressions.

We generate a rule for the large symbolic execution, and also a rule for the modular proofs. The former will be eventually eliminated, once modular proofs cover all the ATC constructs.

Definitions and Theorems

Function: atc-exec-expr-when-asg-arrsub-rules-gen

(defun atc-exec-expr-when-asg-arrsub-rules-gen (atype)
 (declare (xargs :guard (typep atype)))
 (declare (xargs :guard (type-nonchar-integerp atype)))
 (let ((__function__ 'atc-exec-expr-when-asg-arrsub-rules-gen))
  (declare (ignorable __function__))
  (b*
   ((afixtype (integer-type-to-fixtype atype))
    (apred (pack afixtype '-arrayp))
    (epred (pack afixtype 'p))
    (atype-array-index-okp (pack afixtype '-array-index-okp))
    (atype-array-write (pack afixtype '-array-write))
    (value-array->elemtype-when-apred
         (pack 'value-array->elemtype-when-
               apred))
    (value-array-read-when-apred
         (pack 'value-array-read-when- apred))
    (value-array-write-when-apred
         (pack 'value-array-write-when- apred))
    (name (pack 'exec-expr-when-asg-arrsub-when-
                apred))
    (formula
     (cons
      'implies
      (cons
       (cons
        'and
        (cons
         '(equal (expr-kind expr) :binary)
         (cons
          '(equal (binop-kind (expr-binary->op expr))
                  :asg)
          (cons
           '(equal left (expr-binary->arg1 expr))
           (cons
            '(equal right (expr-binary->arg2 expr))
            (cons
             '(equal (expr-kind left) :arrsub)
             (cons
              '(equal arr (expr-arrsub->arr left))
              (cons
               '(equal sub (expr-arrsub->sub left))
               (cons
                '(equal (expr-kind arr) :ident)
                (cons
                 '(equal var (expr-ident->get arr))
                 (cons
                  '(expr-purep right)
                  (cons
                   '(integerp limit)
                   (cons
                    '(>= limit
                         (1+ (max (1+ (expr-pure-limit sub))
                                  (expr-pure-limit right))))
                    (cons
                     '(expr-purep sub)
                     (cons
                      '(equal arr-val (read-var var compst))
                      (cons
                       '(valuep arr-val)
                       (cons
                        '(equal
                          eptr
                          (apconvert-expr-value
                           (expr-value
                            arr-val (objdesign-of-var var compst))))
                        (cons
                         '(expr-valuep eptr)
                         (cons
                          '(equal ptr (expr-value->value eptr))
                          (cons
                           '(value-case ptr :pointer)
                           (cons
                            '(value-pointer-validp ptr)
                            (cons
                             (cons
                              'equal
                              (cons
                                 '(value-pointer->reftype ptr)
                                 (cons (type-to-maker atype) 'nil)))
                             (cons
                              '(equal
                                array
                                (read-object
                                     (value-pointer->designator ptr)
                                     compst))
                              (cons
                               (cons apred '(array))
                               (cons
                                '(equal eindex
                                        (exec-expr-pure sub compst))
                                (cons
                                 '(expr-valuep eindex)
                                 (cons
                                  '(equal
                                      eindex1
                                      (apconvert-expr-value eindex))
                                  (cons
                                   '(expr-valuep eindex1)
                                   (cons
                                    '(equal
                                        index
                                        (expr-value->value eindex1))
                                    (cons
                                     '(cintegerp index)
                                     (cons
                                      (cons atype-array-index-okp
                                            '(array index))
                                      (cons
                                       '(equal eval
                                               (exec-expr-pure
                                                    right compst))
                                       (cons
                                        '(expr-valuep eval)
                                        (cons
                                         '(equal eval1
                                                 (apconvert-expr-value
                                                      eval))
                                         (cons
                                          '(expr-valuep eval1)
                                          (cons
                                           '(equal val
                                                   (expr-value->value
                                                        eval1))
                                           (cons
                                            (cons epred '(val))
                                            (cons
                                             (cons
                                              'equal
                                              (cons
                                               'compst1
                                               (cons
                                                (cons
                                                 'write-object
                                                 (cons
                                                  '(value-pointer->designator
                                                        ptr)
                                                  (cons
                                                   (cons
                                                    atype-array-write
                                                    '(array
                                                         index val))
                                                   '(compst))))
                                                'nil)))
                                             '((compustatep
                                                compst1))))))))))))))))))))))))))))))))))))))))
       '((equal (exec-expr expr compst fenv limit)
                (mv (expr-value val nil) compst1))))))
    (event
     (cons
      'defruled
      (cons
       name
       (cons
        formula
        (cons
         ':expand
         (cons
          '((exec-expr expr compst fenv limit)
            (exec-expr (expr-binary->arg1 expr)
                       compst fenv (1- limit)))
          (cons
           ':enable
           (cons
            (cons
             'exec-expr-to-exec-expr-pure-when-expr-pure-limit
             (cons
              'max
              (cons
               'nfix
               (cons
                'exec-expr
                (cons
                 'exec-ident
                 (cons
                  'exec-arrsub
                  (cons
                   'apconvert-expr-value-when-not-value-array-alt
                   (cons
                    'value-kind-not-array-when-cintegerp
                    (cons
                     'read-object-of-objdesign-of-var-to-read-var
                     (cons
                      value-array->elemtype-when-apred
                      (cons
                       'value-integer->get-when-cintegerp
                       (cons
                        atype-array-index-okp
                        (cons
                         'integer-range-p
                         (cons
                          value-array-read-when-apred
                          (cons
                           value-array-write-when-apred
                           '(write-object
                              expr-purep binop-purep))))))))))))))))
            (cons
             ':disable
             (cons
              '(equal-of-error equal-of-expr-value
                               equal-of-objdesign-element
                               cons-equal acl2::subsetp-member)
              (cons
               ':prep-lemmas
               (cons
                (cons
                 (cons
                  'defrule
                  (cons
                   'lemma
                   (cons
                    (cons
                     'implies
                     (cons
                      (cons
                       'and
                       (cons
                        '(expr-valuep (apconvert-expr-value eval))
                        (cons
                         (cons epred
                               '((expr-value->value
                                      (apconvert-expr-value eval))))
                         'nil)))
                      (cons (cons epred '((expr-value->value eval)))
                            'nil)))
                    '(:enable apconvert-expr-value))))
                 'nil)
                'nil))))))))))))
    (name-mod-prf (pack name '-for-modular-proofs))
    (formula-mod-prf
     (cons
      'implies
      (cons
       (cons
        'and
        (cons
         '(equal (expr-kind expr) :binary)
         (cons
          '(equal (binop-kind (expr-binary->op expr))
                  :asg)
          (cons
           '(equal left (expr-binary->arg1 expr))
           (cons
            '(equal right (expr-binary->arg2 expr))
            (cons
             '(equal (expr-kind left) :arrsub)
             (cons
              '(equal arr (expr-arrsub->arr left))
              (cons
               '(equal sub (expr-arrsub->sub left))
               (cons
                '(equal (expr-kind arr) :ident)
                (cons
                 '(expr-purep right)
                 (cons
                  '(integerp limit)
                  (cons
                   '(>= limit
                        (1+ (max (1+ (expr-pure-limit sub))
                                 (expr-pure-limit right))))
                   (cons
                    '(expr-purep sub)
                    (cons
                     '(equal arr-eval (exec-expr-pure arr compst))
                     (cons
                      '(expr-valuep arr-eval)
                      (cons
                       '(equal ptr-eval
                               (apconvert-expr-value arr-eval))
                       (cons
                        '(expr-valuep ptr-eval)
                        (cons
                         '(equal ptr (expr-value->value ptr-eval))
                         (cons
                          '(value-case ptr :pointer)
                          (cons
                           '(value-pointer-validp ptr)
                           (cons
                            (cons
                             'equal
                             (cons
                                 '(value-pointer->reftype ptr)
                                 (cons (type-to-maker atype) 'nil)))
                            (cons
                             '(equal
                                array
                                (read-object
                                     (value-pointer->designator ptr)
                                     compst))
                             (cons
                              (cons apred '(array))
                              (cons
                               '(equal sub-eval
                                       (exec-expr-pure sub compst))
                               (cons
                                '(expr-valuep sub-eval)
                                (cons
                                 '(equal
                                    index-eval
                                    (apconvert-expr-value sub-eval))
                                 (cons
                                  '(expr-valuep index-eval)
                                  (cons
                                   '(equal
                                     index
                                     (expr-value->value index-eval))
                                   (cons
                                    '(cintegerp index)
                                    (cons
                                     (cons atype-array-index-okp
                                           '(array index))
                                     (cons
                                      '(equal right-eval
                                              (exec-expr-pure
                                                   right compst))
                                      (cons
                                       '(expr-valuep right-eval)
                                       (cons
                                        '(equal eval
                                                (apconvert-expr-value
                                                     right-eval))
                                        (cons
                                         '(expr-valuep eval)
                                         (cons
                                          '(equal val
                                                  (expr-value->value
                                                       eval))
                                          (cons
                                           (cons epred '(val))
                                           (cons
                                            (cons
                                             'equal
                                             (cons
                                              'compst1
                                              (cons
                                               (cons
                                                'write-object
                                                (cons
                                                 '(value-pointer->designator
                                                       ptr)
                                                 (cons
                                                  (cons
                                                   atype-array-write
                                                   '(array
                                                         index val))
                                                  '(compst))))
                                               'nil)))
                                            '((compustatep
                                               compst1)))))))))))))))))))))))))))))))))))))))
       '((equal (exec-expr expr compst fenv limit)
                (mv (expr-value val nil) compst1))))))
    (event-mod-prf
     (cons
      'defruled
      (cons
       name-mod-prf
       (cons
        formula-mod-prf
        (cons
         ':enable
         (cons (cons name
                     '(read-var-to-read-object-of-objdesign-of-var
                           valuep-of-read-object-of-objdesign-of-var
                           exec-expr-pure-when-ident-no-syntaxp
                           exec-ident))
               'nil)))))))
   (mv name (list event event-mod-prf)))))

Theorem: symbolp-of-atc-exec-expr-when-asg-arrsub-rules-gen.name

(defthm symbolp-of-atc-exec-expr-when-asg-arrsub-rules-gen.name
  (b* (((mv ?name ?events)
        (atc-exec-expr-when-asg-arrsub-rules-gen atype)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-exec-expr-when-asg-arrsub-rules-gen.events

(defthm
 pseudo-event-form-listp-of-atc-exec-expr-when-asg-arrsub-rules-gen.events
 (b* (((mv ?name ?events)
       (atc-exec-expr-when-asg-arrsub-rules-gen atype)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Function: atc-exec-expr-when-asg-arrsub-rules-gen-loop

(defun atc-exec-expr-when-asg-arrsub-rules-gen-loop (atypes)
 (declare (xargs :guard (type-listp atypes)))
 (declare (xargs :guard (type-nonchar-integer-listp atypes)))
 (let ((__function__ 'atc-exec-expr-when-asg-arrsub-rules-gen-loop))
   (declare (ignorable __function__))
   (b*
     (((when (endp atypes)) (mv nil nil))
      ((mv name events)
       (atc-exec-expr-when-asg-arrsub-rules-gen (car atypes)))
      ((mv more-names more-events)
       (atc-exec-expr-when-asg-arrsub-rules-gen-loop (cdr atypes))))
     (mv (cons name more-names)
         (append events more-events)))))

Theorem: symbol-listp-of-atc-exec-expr-when-asg-arrsub-rules-gen-loop.names

(defthm
 symbol-listp-of-atc-exec-expr-when-asg-arrsub-rules-gen-loop.names
 (b* (((mv ?names ?events)
       (atc-exec-expr-when-asg-arrsub-rules-gen-loop atypes)))
   (symbol-listp names))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-exec-expr-when-asg-arrsub-rules-gen-loop.events

(defthm
 pseudo-event-form-listp-of-atc-exec-expr-when-asg-arrsub-rules-gen-loop.events
 (b* (((mv ?names ?events)
       (atc-exec-expr-when-asg-arrsub-rules-gen-loop atypes)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Function: atc-exec-expr-when-asg-arrsub-rules-gen-all

(defun atc-exec-expr-when-asg-arrsub-rules-gen-all nil
 (declare (xargs :guard t))
 (let ((__function__ 'atc-exec-expr-when-asg-arrsub-rules-gen-all))
  (declare (ignorable __function__))
  (b* (((mv names events)
        (atc-exec-expr-when-asg-arrsub-rules-gen-loop
             *nonchar-integer-types*)))
   (cons
    'progn
    (cons
     (cons
      'defsection
      (cons
       'atc-exec-expr-when-asg-arrsub-rules
       (cons
        ':short
        (cons
         '"Rules for executing assignment expressions to
                   array subscript expressions."
         (append
          events
          (cons
           (cons
            'defval
            (cons '*atc-exec-expr-when-asg-arrsub-rules*
                  (cons (cons 'quote
                              (cons (append names
                                            '((:e expr-kind)
                                              (:e expr-arrsub->arr)
                                              (:e expr-arrsub->sub)
                                              (:e expr-binary->op)
                                              (:e expr-binary->arg1)
                                              (:e expr-binary->arg2)
                                              (:e expr-ident->get)
                                              (:e binop-kind)))
                                    'nil))
                        'nil)))
           'nil))))))
     'nil)))))

Theorem: pseudo-event-formp-of-atc-exec-expr-when-asg-arrsub-rules-gen-all

(defthm
  pseudo-event-formp-of-atc-exec-expr-when-asg-arrsub-rules-gen-all
  (b* ((event (atc-exec-expr-when-asg-arrsub-rules-gen-all)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)