		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-cast-rules-generation

Code to generate the rules for executing cast operations.

The hints expand exec-cast, convert-integer-value, value-integer, and value-integer->get, which produces something like (value-<dst> (value-<src>->get ...)), where <src> is the source type and <dst> is the destination type, with an intervening mod when the destination type is unsigned. We use the bridge rules to turn those constructor and destructors into the shallowly embedded ones (i.e. (<dst> (integer-from-<src> ...)), which are the ones used in the definitions of the shallowly embedded conversion functions, which we also open (unless source and destination types are equal), along with the okp predicates if applicable. We also need open u...-from-integer-mod to expose the mod in the shallowly embedded conversions to unsigned type, thus matching the mod in convert-integer-value. We open the <dst>-integerp functions to show that the ACL2 integer is in range, i.e. that convert-integer-value does not return an error; for this, we also need (locally included) rules about mod, to show that it is never negative as required for an unsigned range.

Definitions and Theorems

Function: atc-exec-cast-rules-gen

(defun atc-exec-cast-rules-gen (dtype stype)
 (declare (xargs :guard (and (typep dtype) (typep stype))))
 (declare (xargs :guard (and (type-nonchar-integerp dtype)
                             (type-nonchar-integerp stype))))
 (let ((__function__ 'atc-exec-cast-rules-gen))
  (declare (ignorable __function__))
  (b*
   ((dfixtype (integer-type-to-fixtype dtype))
    (sfixtype (integer-type-to-fixtype stype))
    (spred (pack sfixtype 'p))
    (name (pack 'exec-cast-of-
                dfixtype '-when-
                spred))
    (dtyname (type-to-tyname dtype))
    (dtype-from-stype (pack dfixtype '-from- sfixtype))
    (dtype-from-stype-okp (pack dtype-from-stype '-okp))
    (guardp
     (and
       (not (equal dtype stype))
       (or (type-case dtype :schar)
           (and (type-case dtype :sshort)
                (not (member-eq (type-kind stype)
                                '(:schar))))
           (and (type-case dtype :sint)
                (not (member-eq (type-kind stype)
                                '(:schar :sshort))))
           (and (type-case dtype :slong)
                (not (member-eq (type-kind stype)
                                '(:schar :sshort :sint))))
           (and (type-case dtype :sllong)
                (not (member-eq (type-kind stype)
                                '(:schar :sshort :sint :slong)))))))
    (hyps
       (cons 'and
             (cons (atc-syntaxp-hyp-for-expr-pure 'x)
                   (cons (cons spred '(x))
                         (and guardp
                              (cons (cons dtype-from-stype-okp '(x))
                                    'nil))))))
    (rhs (if (equal dtype stype)
             'x
           (cons dtype-from-stype '(x))))
    (formula
     (cons
      'implies
      (cons
       hyps
       (cons
           (cons 'equal
                 (cons (cons 'exec-cast
                             (cons (cons 'quote (cons dtyname 'nil))
                                   '((expr-value x objdes))))
                       (cons (cons 'expr-value (cons rhs '(nil)))
                             'nil)))
           'nil))))
    (hints
     (cons
      ':enable
      (cons
       (cons
        'exec-cast
        (cons
         'eval-cast
         (cons
          'convert-integer-value
          (cons
           'value-integer
           (append
            *atc-value-integer->get-rules*
            (cons
             'integer-type-rangep
             (cons
              'integer-type-min
              (cons
               'integer-type-max
               (cons
                'value-schar-to-schar-from-integer
                (cons
                 'value-uchar-to-uchar-from-integer
                 (cons
                  'value-sshort-to-sshort-from-integer
                  (cons
                   'value-ushort-to-ushort-from-integer
                   (cons
                    'value-sint-to-sint-from-integer
                    (cons
                     'value-uint-to-uint-from-integer
                     (cons
                      'value-slong-to-slong-from-integer
                      (cons
                       'value-ulong-to-ulong-from-integer
                       (cons
                        'value-sllong-to-sllong-from-integer
                        (cons
                         'value-ullong-to-ullong-from-integer
                         (cons
                          'uchar-from-integer-mod
                          (cons
                           'ushort-from-integer-mod
                           (cons
                            'uint-from-integer-mod
                            (cons
                             'ulong-from-integer-mod
                             (cons
                              'ullong-from-integer-mod
                              (cons
                               'schar-integerp-alt-def
                               (cons
                                'uchar-integerp-alt-def
                                (cons
                                 'sshort-integerp-alt-def
                                 (cons
                                  'ushort-integerp-alt-def
                                  (cons
                                   'sint-integerp-alt-def
                                   (cons
                                    'uint-integerp-alt-def
                                    (cons
                                     'slong-integerp-alt-def
                                     (cons
                                      'ulong-integerp-alt-def
                                      (cons
                                       'sllong-integerp-alt-def
                                       (cons
                                        'ullong-integerp-alt-def
                                        (append
                                         (and
                                           (not (equal dtype stype))
                                           (list dtype-from-stype))
                                         (append
                                          (and
                                           guardp
                                           (list
                                              dtype-from-stype-okp))
                                          '(apconvert-expr-value-when-not-value-array
                                            value-kind-when-ucharp
                                            value-kind-when-scharp
                                            value-kind-when-ushortp
                                            value-kind-when-sshortp
                                            value-kind-when-uintp
                                            value-kind-when-sintp
                                            value-kind-when-ulongp
                                            value-kind-when-slongp
                                            value-kind-when-ullongp
                                            value-kind-when-sllongp
                                            ifix
                                            not-errorp-when-expr-valuep
                                            not-errorp-when-valuep
                                            valuep-when-ucharp
                                            valuep-when-scharp
                                            valuep-when-ushortp
                                            valuep-when-sshortp
                                            valuep-when-uintp
                                            valuep-when-sintp
                                            valuep-when-ulongp
                                            valuep-when-slongp
                                            valuep-when-ullongp
                                            valuep-when-sllongp
                                            value-integerp
                                            value-unsigned-integerp
                                            value-signed-integerp))))))))))))))))))))))))))))))))))))
       '(:disable ((:e tau-system)
                   (:e integer-type-max)
                   (:e integer-type-min))))))
    (event (cons 'defruled
                 (cons name (cons formula hints)))))
   (mv name event))))

Theorem: symbolp-of-atc-exec-cast-rules-gen.name

(defthm symbolp-of-atc-exec-cast-rules-gen.name
  (b* (((mv ?name acl2::?event)
        (atc-exec-cast-rules-gen dtype stype)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-atc-exec-cast-rules-gen.event

(defthm pseudo-event-formp-of-atc-exec-cast-rules-gen.event
  (b* (((mv ?name acl2::?event)
        (atc-exec-cast-rules-gen dtype stype)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Function: atc-exec-cast-rules-gen-loop-stypes

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

Theorem: symbol-listp-of-atc-exec-cast-rules-gen-loop-stypes.names

(defthm symbol-listp-of-atc-exec-cast-rules-gen-loop-stypes.names
  (b* (((mv ?names ?events)
        (atc-exec-cast-rules-gen-loop-stypes dtype stypes)))
    (symbol-listp names))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-exec-cast-rules-gen-loop-stypes.events

(defthm
 pseudo-event-form-listp-of-atc-exec-cast-rules-gen-loop-stypes.events
 (b* (((mv ?names ?events)
       (atc-exec-cast-rules-gen-loop-stypes dtype stypes)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Function: atc-exec-cast-rules-gen-loop-dtypes

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

Theorem: symbol-listp-of-atc-exec-cast-rules-gen-loop-dtypes.names

(defthm symbol-listp-of-atc-exec-cast-rules-gen-loop-dtypes.names
  (b* (((mv ?names ?events)
        (atc-exec-cast-rules-gen-loop-dtypes dtypes stypes)))
    (symbol-listp names))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-exec-cast-rules-gen-loop-dtypes.events

(defthm
 pseudo-event-form-listp-of-atc-exec-cast-rules-gen-loop-dtypes.events
 (b* (((mv ?names ?events)
       (atc-exec-cast-rules-gen-loop-dtypes dtypes stypes)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Function: atc-exec-cast-rules-gen-all

(defun atc-exec-cast-rules-gen-all nil
 (declare (xargs :guard t))
 (let ((__function__ 'atc-exec-cast-rules-gen-all))
  (declare (ignorable __function__))
  (b*
   (((mv names events)
     (atc-exec-cast-rules-gen-loop-dtypes *nonchar-integer-types*
                                          *nonchar-integer-types*)))
   (cons
    'progn
    (cons
     (cons
      'defsection
      (cons
       'atc-exec-cast-rules
       (cons
        ':short
        (cons
         '"Rules for executing casts."
         (append
             events
             (cons (cons 'defval
                         (cons '*atc-exec-cast-rules*
                               (cons (cons 'quote (cons names 'nil))
                                     'nil)))
                   'nil))))))
     'nil)))))

Theorem: pseudo-event-formp-of-atc-exec-cast-rules-gen-all

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