		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-uaconvert-values-rules-generation

Code to generate the rules for uaconvert-values.

Definitions and Theorems

Function: atc-uaconvert-values-rules-gen

(defun atc-uaconvert-values-rules-gen (ltype rtype)
 (declare (xargs :guard (and (typep ltype) (typep rtype))))
 (declare (xargs :guard (and (type-nonchar-integerp ltype)
                             (type-nonchar-integerp rtype))))
 (let ((__function__ 'atc-uaconvert-values-rules-gen))
  (declare (ignorable __function__))
  (b*
   ((lfixtype (integer-type-to-fixtype ltype))
    (rfixtype (integer-type-to-fixtype rtype))
    (lpred (pack lfixtype 'p))
    (rpred (pack rfixtype 'p))
    (type (uaconvert-types ltype rtype))
    (fixtype (integer-type-to-fixtype type))
    (lterm (if (equal type ltype)
               'x
             (cons (pack fixtype '-from- lfixtype)
                   '(x))))
    (rterm (if (equal type rtype)
               'y
             (cons (pack fixtype '-from- rfixtype)
                   '(y))))
    (name (pack 'uaconvert-values-when-
                lpred '-and-
                rpred))
    (event
     (cons
      'defruled
      (cons
       name
       (cons
        (cons
         'implies
         (cons
          (cons 'and
                (cons (cons lpred '(x))
                      (cons (cons rpred '(y)) 'nil)))
          (cons
             (cons 'equal
                   (cons '(uaconvert-values x y)
                         (cons (cons 'mv
                                     (cons lterm (cons rterm 'nil)))
                               'nil)))
             'nil)))
        (cons
         ':enable
         (cons
          (cons
           'uaconvert-values
           (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-sintp
                (cons
                 'type-of-value-when-uintp
                 (cons
                  'type-of-value-when-slongp
                  (cons
                   'type-of-value-when-ulongp
                   (cons
                    'type-of-value-when-sllongp
                    (cons
                     'type-of-value-when-ullongp
                     (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
                            'bit-width-value-choices
                            *atc-convert-integer-value-rules*))))))))))))))))))
          'nil)))))))
   (mv name event))))

Theorem: symbolp-of-atc-uaconvert-values-rules-gen.name

(defthm symbolp-of-atc-uaconvert-values-rules-gen.name
  (b* (((mv ?name acl2::?event)
        (atc-uaconvert-values-rules-gen ltype rtype)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-atc-uaconvert-values-rules-gen.event

(defthm pseudo-event-formp-of-atc-uaconvert-values-rules-gen.event
  (b* (((mv ?name acl2::?event)
        (atc-uaconvert-values-rules-gen ltype rtype)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Function: atc-uaconvert-values-rules-gen-loop-rtypes

(defun atc-uaconvert-values-rules-gen-loop-rtypes (ltype rtypes)
  (declare (xargs :guard (and (typep ltype)
                              (type-listp rtypes))))
  (declare (xargs :guard (and (type-nonchar-integerp ltype)
                              (type-nonchar-integer-listp rtypes))))
  (let ((__function__ 'atc-uaconvert-values-rules-gen-loop-rtypes))
    (declare (ignorable __function__))
    (b* (((when (endp rtypes)) (mv nil nil))
         ((mv name event)
          (atc-uaconvert-values-rules-gen ltype (car rtypes)))
         ((mv names events)
          (atc-uaconvert-values-rules-gen-loop-rtypes
               ltype (cdr rtypes))))
      (mv (cons name names)
          (cons event events)))))

Theorem: symbol-listp-of-atc-uaconvert-values-rules-gen-loop-rtypes.names

(defthm
   symbol-listp-of-atc-uaconvert-values-rules-gen-loop-rtypes.names
  (b* (((mv ?names ?events)
        (atc-uaconvert-values-rules-gen-loop-rtypes ltype rtypes)))
    (symbol-listp names))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-uaconvert-values-rules-gen-loop-rtypes.events

(defthm
 pseudo-event-form-listp-of-atc-uaconvert-values-rules-gen-loop-rtypes.events
 (b* (((mv ?names ?events)
       (atc-uaconvert-values-rules-gen-loop-rtypes ltype rtypes)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Function: atc-uaconvert-values-rules-gen-loop-ltypes

(defun atc-uaconvert-values-rules-gen-loop-ltypes (ltypes rtypes)
  (declare (xargs :guard (and (type-listp ltypes)
                              (type-listp rtypes))))
  (declare (xargs :guard (and (type-nonchar-integer-listp ltypes)
                              (type-nonchar-integer-listp rtypes))))
  (let ((__function__ 'atc-uaconvert-values-rules-gen-loop-ltypes))
    (declare (ignorable __function__))
    (b* (((when (endp ltypes)) (mv nil nil))
         ((mv names events)
          (atc-uaconvert-values-rules-gen-loop-rtypes (car ltypes)
                                                      rtypes))
         ((mv names1 events1)
          (atc-uaconvert-values-rules-gen-loop-ltypes (cdr ltypes)
                                                      rtypes)))
      (mv (append names names1)
          (append events events1)))))

Theorem: symbol-listp-of-atc-uaconvert-values-rules-gen-loop-ltypes.names

(defthm
   symbol-listp-of-atc-uaconvert-values-rules-gen-loop-ltypes.names
  (b* (((mv ?names ?events)
        (atc-uaconvert-values-rules-gen-loop-ltypes ltypes rtypes)))
    (symbol-listp names))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-uaconvert-values-rules-gen-loop-ltypes.events

(defthm
 pseudo-event-form-listp-of-atc-uaconvert-values-rules-gen-loop-ltypes.events
 (b* (((mv ?names ?events)
       (atc-uaconvert-values-rules-gen-loop-ltypes ltypes rtypes)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Function: atc-uaconvert-values-rules-gen-all

(defun atc-uaconvert-values-rules-gen-all nil
 (declare (xargs :guard t))
 (let ((__function__ 'atc-uaconvert-values-rules-gen-all))
  (declare (ignorable __function__))
  (b* (((mv names events)
        (atc-uaconvert-values-rules-gen-loop-ltypes
             *nonchar-integer-types*
             *nonchar-integer-types*)))
   (cons
    'progn
    (cons
     (cons
      'defsection
      (cons
       'atc-uaconvert-values-rules
       (cons
        ':short
        (cons
         '"Rules about @(tsee uaconvert-values)
                   on values of given types."
         (cons
          ':long
          (cons
           '(xdoc::topstring
             (xdoc::p
              "These are not used during the symbolic execution;
              they are used to prove rules
              used during the symbolic execution."))
           (append
             events
             (cons (cons 'defval
                         (cons '*atc-uaconvert-values-rules*
                               (cons (cons 'quote (cons names 'nil))
                                     'nil)))
                   'nil))))))))
     'nil)))))

Theorem: pseudo-event-formp-of-atc-uaconvert-values-rules-gen-all

(defthm pseudo-event-formp-of-atc-uaconvert-values-rules-gen-all
  (b* ((event (atc-uaconvert-values-rules-gen-all)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)