Code to generate the rules for uaconvert-values.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)