Code to generate the rules for executing unary operations that do not involve pointers.
Function:
(defun atc-exec-unary-nonpointer-rules-gen (op type) (declare (xargs :guard (and (unopp op) (typep type)))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'atc-exec-unary-nonpointer-rules-gen)) (declare (ignorable __function__)) (b* ((fixtype (integer-type-to-fixtype type)) (pred (pack fixtype 'p)) (op-kind (unop-kind op)) (op-value (pack op-kind '-value)) (op-scalar-value (and (unop-case op :lognot) (pack op-kind '-scalar-value))) (op-arithmetic-value (and (or (unop-case op :plus) (unop-case op :minus)) (pack op-kind '-arithmetic-value))) (op-integer-value (pack op-kind '-integer-value)) (name (pack op-value '-when- pred)) (op-type (pack op-kind '- fixtype)) (op-type-okp (and (unop-case op :minus) (member-eq (type-kind type) '(:schar :sshort :sint :slong :sllong :uchar :ushort)) (pack op-type '-okp))) (promotedp (and (member-eq op-kind '(:plus :minus :bitnot)) (member-eq (type-kind type) '(:schar :uchar :sshort :ushort)))) (hyps (cons 'and (cons (atc-syntaxp-hyp-for-expr-pure 'x) (cons (cons 'equal (cons 'op (cons (cons (pack 'unop- op-kind) 'nil) 'nil))) (cons (cons pred '(x)) (and op-type-okp (cons (cons op-type-okp '(x)) 'nil))))))) (formula (cons 'implies (cons hyps (cons (cons 'equal (cons '(exec-unary op (expr-value x objdes) compst) (cons (cons 'expr-value (cons (cons op-type '(x)) '(nil))) 'nil))) 'nil)))) (enables (cons 'exec-unary (cons 'eval-unary (cons op-value (append (and op-scalar-value (list op-scalar-value)) (append (and op-arithmetic-value (list op-arithmetic-value)) (cons op-integer-value (cons op-type (append (and promotedp (list (pack op-kind '-sint))) (append (and op-type-okp (list op-type-okp)) (append (and op-type-okp promotedp (list (pack op-kind '-sint-okp))) (append *atc-promote-value-rules* (cons 'result-integer-value (append *atc-value-integer->get-rules* (cons 'value-integer (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 '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 '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 (cons 'uint-from-integer-mod (cons 'ulong-from-integer-mod (cons 'ullong-from-integer-mod (cons 'value-unsigned-integerp-alt-def (cons 'integer-type-rangep (cons 'integer-type-min (cons 'integer-type-max (cons 'bit-width-value-choices (cons 'apconvert-expr-value-when-not-value-array (cons 'value-kind-when-ucharp (cons 'value-kind-when-scharp (cons 'value-kind-when-ushortp (cons 'value-kind-when-sshortp (cons 'value-kind-when-uintp (cons 'value-kind-when-sintp (cons 'value-kind-when-ulongp (cons 'value-kind-when-slongp (cons 'value-kind-when-ullongp (cons 'value-kind-when-sllongp (append (and (unop-case op :bitnot) '((:e sint-min) (:e sint-max) (:e slong-min) (:e slong-max) (:e sllong-min) (:e sllong-max))) (append (and (unop-case op :lognot) '(sint-from-boolean value-schar->get-to-integer-from-schar value-uchar->get-to-integer-from-uchar value-sshort->get-to-integer-from-sshort value-ushort->get-to-integer-from-ushort)) '(identity ifix fix mod lognot))))))))))))))))))))))))))))))))))))))))))))))))))))))) (event (cons 'defruled (cons name (cons formula (cons ':enable (cons enables '(:disable ((:e integer-type-min) (:e integer-type-max)))))))))) (mv name event))))
Theorem:
(defthm symbolp-of-atc-exec-unary-nonpointer-rules-gen.name (b* (((mv ?name acl2::?event) (atc-exec-unary-nonpointer-rules-gen op type))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-atc-exec-unary-nonpointer-rules-gen.event (b* (((mv ?name acl2::?event) (atc-exec-unary-nonpointer-rules-gen op type))) (pseudo-event-formp event)) :rule-classes :rewrite)
Function:
(defun atc-exec-unary-nonpointer-rules-gen-loop-types (op types) (declare (xargs :guard (and (unopp op) (type-listp types)))) (declare (xargs :guard (type-nonchar-integer-listp types))) (let ((__function__ 'atc-exec-unary-nonpointer-rules-gen-loop-types)) (declare (ignorable __function__)) (b* (((when (endp types)) (mv nil nil)) ((mv name event) (atc-exec-unary-nonpointer-rules-gen op (car types))) ((mv names events) (atc-exec-unary-nonpointer-rules-gen-loop-types op (cdr types)))) (mv (cons name names) (cons event events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-unary-nonpointer-rules-gen-loop-types.names (b* (((mv ?names ?events) (atc-exec-unary-nonpointer-rules-gen-loop-types op types))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-unary-nonpointer-rules-gen-loop-types.events (b* (((mv ?names ?events) (atc-exec-unary-nonpointer-rules-gen-loop-types op types))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-unary-nonpointer-rules-gen-loop-ops (ops types) (declare (xargs :guard (and (unop-listp ops) (type-listp types)))) (declare (xargs :guard (type-nonchar-integer-listp types))) (let ((__function__ 'atc-exec-unary-nonpointer-rules-gen-loop-ops)) (declare (ignorable __function__)) (b* (((when (endp ops)) (mv nil nil)) ((mv names events) (atc-exec-unary-nonpointer-rules-gen-loop-types (car ops) types)) ((mv more-names more-events) (atc-exec-unary-nonpointer-rules-gen-loop-ops (cdr ops) types))) (mv (append names more-names) (append events more-events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-unary-nonpointer-rules-gen-loop-ops.names (b* (((mv ?names ?events) (atc-exec-unary-nonpointer-rules-gen-loop-ops ops types))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-unary-nonpointer-rules-gen-loop-ops.events (b* (((mv ?names ?events) (atc-exec-unary-nonpointer-rules-gen-loop-ops ops types))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-unary-nonpointer-rules-gen-all nil (declare (xargs :guard t)) (let ((__function__ 'atc-exec-unary-nonpointer-rules-gen-all)) (declare (ignorable __function__)) (b* ((ops (list (unop-plus) (unop-minus) (unop-bitnot) (unop-lognot))) ((mv names events) (atc-exec-unary-nonpointer-rules-gen-loop-ops ops *nonchar-integer-types*))) (cons 'progn (cons (cons 'defsection (cons 'atc-exec-unary-nonpointer-rules (cons ':short (cons '"Rules for executing unary operations that do not involve pointers." (append events (cons (cons 'defval (cons '*atc-exec-unary-nonpointer-rules* (cons (cons 'quote (cons (append names '((:e unop-plus) (:e unop-minus) (:e unop-bitnot) (:e unop-lognot))) 'nil)) 'nil))) 'nil)))))) 'nil)))))
Theorem:
(defthm pseudo-event-formp-of-atc-exec-unary-nonpointer-rules-gen-all (b* ((event (atc-exec-unary-nonpointer-rules-gen-all))) (pseudo-event-formp event)) :rule-classes :rewrite)