|
|
|---|
|
|
|
|---|
Code to generate the rules for executing strict pure binary operations.
Since there are 16 binary operations and 10 integer types, there are 1600 instances of these rules. Generating all of them in the same file takes a bit of time; for example, a machine takes about 300 seconds to process all of them, which is actually less than 0.2 seconds for each instance, which is not particularly slow, but things add up.
So we split the generation across 16 files, one per operation,
to take advantage of parallel certification.
Each file contains a make-event form that generates
(i) the rules for the operation,
(ii) a named constant with the rules of the operation, and
(iii) a named constant with the rule events.
The argument of the make-event is
a call of
Function:
(defun atc-exec-binary-rules-gen-op-ltype-rtype (op ltype rtype) (declare (xargs :guard (and (binopp op) (typep ltype) (typep rtype)))) (declare (xargs :guard (and (type-nonchar-integerp ltype) (type-nonchar-integerp rtype)))) (let ((__function__ 'atc-exec-binary-rules-gen-op-ltype-rtype)) (declare (ignorable __function__)) (b* ((lfixtype (integer-type-to-fixtype ltype)) (rfixtype (integer-type-to-fixtype rtype)) (rpred (pack rfixtype 'p)) (op-kind (binop-kind op)) (op-values (pack op-kind '-values)) (op-arithmetic-values (and (or (binop-case op :div) (binop-case op :mul) (binop-case op :rem) (binop-case op :add) (binop-case op :sub) (binop-case op :eq) (binop-case op :ne)) (pack op-kind '-arithmetic-values))) (op-real-values (and (or (binop-case op :lt) (binop-case op :gt) (binop-case op :le) (binop-case op :ge)) (pack op-kind '-real-values))) (op-integer-values (pack op-kind '-integer-values)) (op-ltype-and-value (pack op-kind '- lfixtype '-and-value)) (type (uaconvert-types ltype rtype)) (promotedp (and (member-eq op-kind '(:shl :shr)) (member-eq (type-kind ltype) '(:schar :uchar :sshort :ushort)))) (name (pack op-ltype-and-value '-when- rfixtype)) (op-ltype-rtype (pack op-kind '- lfixtype '- rfixtype)) (op-type-type (pack op-kind '- (type-kind type) '- (type-kind type))) (op-type-type-okp (pack op-type-type '-okp)) (op-ltype-rtype-okp (and (or (member-eq op-kind '(:div :rem :shl :shr)) (and (member-eq op-kind '(:add :sub :mul)) (type-signed-integerp type))) (pack op-ltype-rtype '-okp))) (op-ltype (and (member-eq op-kind '(:shl :shr)) (pack op-kind '- (type-kind ltype)))) (op-ltype-okp (and op-ltype (pack op-ltype '-okp))) (formula (cons 'implies (cons (cons 'and (cons (atc-syntaxp-hyp-for-expr-pure 'y) (cons (cons rpred '(y)) (and op-ltype-rtype-okp (cons (cons op-ltype-rtype-okp '(x y)) 'nil))))) (cons (cons 'equal (cons (cons op-ltype-and-value '(x y)) (cons (cons op-ltype-rtype '(x y)) 'nil))) 'nil)))) (enables (cons op-ltype-and-value (append (if (member-eq op-kind '(:shl :shr)) '(shl-values-to-shl-integer-values shr-values-to-shr-integer-values value-integerp-when-scharp value-integerp-when-ucharp value-integerp-when-sshortp value-integerp-when-ushortp value-integerp-when-sintp value-integerp-when-uintp value-integerp-when-slongp value-integerp-when-ulongp value-integerp-when-sllongp value-integerp-when-ullongp) (list op-values)) (append (and op-arithmetic-values (list op-arithmetic-values)) (append (and op-real-values (list op-real-values)) (cons op-integer-values (cons op-ltype-rtype (append (and op-ltype (list op-ltype)) (append (and (member-eq op-kind '(:mul :div :rem :add :sub :lt :gt :le :ge :eq :ne :bitand :bitxor :bitior)) (or (not (equal type ltype)) (not (equal type rtype))) (list op-type-type)) (append (and promotedp (list (pack op-kind '-sint))) (append (and op-ltype-rtype-okp (list op-ltype-rtype-okp)) (append (and op-ltype-okp (list op-ltype-okp)) (append (and (member-eq op-kind '(:mul :div :rem :add :sub)) op-ltype-rtype-okp (or (not (equal type ltype)) (not (equal type rtype))) (list op-type-type-okp)) (append (and promotedp (list (pack op-kind '-sint-okp))) (append (if (member-eq op-kind '(:shl :shr)) *atc-promote-value-rules* *atc-uaconvert-values-rules*) (cons 'result-integer-value (append *atc-value-integer->get-rules* (append (and (member-eq op-kind '(:shl :shr)) *atc-sint-get-rules*) (append (and (member-eq op-kind '(:shl :shr)) '(integer-type-bits-when-type-sint integer-type-bits-when-type-uint integer-type-bits-when-type-slong integer-type-bits-when-type-ulong integer-type-bits-when-type-sllong integer-type-bits-when-type-ullong type-of-value-when-sintp type-of-value-when-uintp type-of-value-when-slongp type-of-value-when-ulongp type-of-value-when-sllongp type-of-value-when-ullongp)) (cons 'apconvert-expr-value-when-not-value-array (cons 'value-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 '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 (append (and (member-eq op-kind '(:add :sub :mul :div :rem)) '(value-arithmeticp-when-uintp value-arithmeticp-when-sintp value-arithmeticp-when-ulongp value-arithmeticp-when-slongp value-arithmeticp-when-ullongp value-arithmeticp-when-sllongp)) (append (and (member-eq op-kind '(:add :sub :mul :div :rem)) '(type-of-value-when-sintp type-of-value-when-uintp type-of-value-when-slongp type-of-value-when-ulongp type-of-value-when-sllongp type-of-value-when-ullongp)) (append (and (member-eq op-kind '(:add :sub :mul :div :rem)) '((:e uint-max) (:e ulong-max) (:e ullong-max) (:e sint-min) (:e sint-max) (:e slong-min) (:e slong-max) (:e sllong-min) (:e sllong-max))) (cons 'integer-type-rangep (and (not (member-eq op-kind '(:add :sub :mul :div :rem))) '(integer-type-min integer-type-max bit-width-value-choices))))))))))))))))))))))))))))))))))))))))))) (event (cons 'defruled (cons name (cons formula (cons ':enable (cons enables (cons ':disable (cons (append (and (member-eq op-kind '(:shl :shr)) '((:e int-bits) (:e integer-type-bits) (:e integer-type-min) (:e integer-type-max))) '(equal-of-error equal-of-value-schar equal-of-value-uchar equal-of-value-sshort equal-of-value-ushort equal-of-value-sint equal-of-value-uint equal-of-value-slong equal-of-value-ulong equal-of-value-sllong equal-of-value-ullong)) 'nil))))))))) (mv name event))))
Theorem:
(defthm symbolp-of-atc-exec-binary-rules-gen-op-ltype-rtype.name (b* (((mv ?name acl2::?event) (atc-exec-binary-rules-gen-op-ltype-rtype op ltype rtype))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-atc-exec-binary-rules-gen-op-ltype-rtype.event (b* (((mv ?name acl2::?event) (atc-exec-binary-rules-gen-op-ltype-rtype op ltype rtype))) (pseudo-event-formp event)) :rule-classes :rewrite)
Function:
(defun atc-exec-binary-rules-gen-op-ltype (op ltype rtypes) (declare (xargs :guard (and (binopp op) (typep ltype) (type-listp rtypes)))) (declare (xargs :guard (and (type-nonchar-integerp ltype) (type-nonchar-integer-listp rtypes)))) (let ((__function__ 'atc-exec-binary-rules-gen-op-ltype)) (declare (ignorable __function__)) (b* (((when (endp rtypes)) (mv nil nil)) ((mv name event) (atc-exec-binary-rules-gen-op-ltype-rtype op ltype (car rtypes))) ((mv names events) (atc-exec-binary-rules-gen-op-ltype op ltype (cdr rtypes)))) (mv (cons name names) (cons event events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-binary-rules-gen-op-ltype.names (b* (((mv ?names ?events) (atc-exec-binary-rules-gen-op-ltype op ltype rtypes))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-binary-rules-gen-op-ltype.events (b* (((mv ?names ?events) (atc-exec-binary-rules-gen-op-ltype op ltype rtypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-binary-rules-gen-op (op ltypes rtypes) (declare (xargs :guard (and (binopp op) (type-listp ltypes) (type-listp rtypes)))) (declare (xargs :guard (and (type-nonchar-integer-listp ltypes) (type-nonchar-integer-listp rtypes)))) (let ((__function__ 'atc-exec-binary-rules-gen-op)) (declare (ignorable __function__)) (b* (((when (endp ltypes)) (mv nil nil)) (ltype (car ltypes)) (lfixtype (integer-type-to-fixtype ltype)) (lpred (pack lfixtype 'p)) (ltype-fix (pack lfixtype '-fix)) (op-kind (binop-kind op)) (op-values (pack op-kind '-values)) (op-ltype-and-value (pack op-kind '- lfixtype '-and-value)) (op-values-when-ltype (pack op-kind '-values-when- lfixtype)) (fun-event (cons 'defund (cons op-ltype-and-value (cons '(x y) (cons (cons op-values (cons (cons ltype-fix '(x)) '(y))) 'nil))))) (thm-event (cons 'defruled (cons op-values-when-ltype (cons (cons 'implies (cons (cons 'and (cons (atc-syntaxp-hyp-for-expr-pure 'x) (cons (cons lpred '(x)) 'nil))) (cons (cons 'equal (cons (cons op-values '(x y)) (cons (cons op-ltype-and-value '(x y)) 'nil))) 'nil))) (cons ':enable (cons (cons op-ltype-and-value 'nil) 'nil)))))) ((mv names events) (atc-exec-binary-rules-gen-op-ltype op (car ltypes) rtypes)) ((mv more-names more-events) (atc-exec-binary-rules-gen-op op (cdr ltypes) rtypes))) (mv (append (list op-values-when-ltype) names more-names) (append (list fun-event thm-event) events more-events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-binary-rules-gen-op.names (b* (((mv ?names ?events) (atc-exec-binary-rules-gen-op op ltypes rtypes))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-binary-rules-gen-op.events (b* (((mv ?names ?events) (atc-exec-binary-rules-gen-op op ltypes rtypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-binary-rules-gen (ops ltypes rtypes) (declare (xargs :guard (and (binop-listp ops) (type-listp ltypes) (type-listp rtypes)))) (declare (xargs :guard (and (type-nonchar-integer-listp ltypes) (type-nonchar-integer-listp rtypes)))) (let ((__function__ 'atc-exec-binary-rules-gen)) (declare (ignorable __function__)) (b* (((when (endp ops)) (mv nil nil)) (op (car ops)) (op-kind (binop-kind op)) (op-values (pack op-kind '-values)) (exec-binary-strict-pure-when-op (pack 'exec-binary-strict-pure-when- op-kind)) (thm-event (cons 'defruled (cons exec-binary-strict-pure-when-op (cons (cons 'implies (cons (cons 'and (cons (cons 'equal (cons 'op (cons (cons (pack 'binop- op-kind) 'nil) 'nil))) (cons '(not (equal (value-kind x) :array)) (cons '(not (equal (value-kind y) :array)) (cons (cons 'equal (cons 'val (cons (cons op-values '(x y)) 'nil))) '((valuep val))))))) '((equal (exec-binary-strict-pure op (expr-value x objdes-x) (expr-value y objdes-y)) (expr-value val nil))))) '(:enable (exec-binary-strict-pure eval-binary-strict-pure apconvert-expr-value-when-not-value-array)))))) ((mv names events) (atc-exec-binary-rules-gen-op op ltypes rtypes)) ((mv more-names more-events) (atc-exec-binary-rules-gen (cdr ops) ltypes rtypes))) (mv (append (list exec-binary-strict-pure-when-op) names more-names) (append (list thm-event) events more-events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-binary-rules-gen.names (b* (((mv ?names ?events) (atc-exec-binary-rules-gen ops ltypes rtypes))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-binary-rules-gen.events (b* (((mv ?names ?events) (atc-exec-binary-rules-gen ops ltypes rtypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-binary-rules-for-op-gen (op) (declare (xargs :guard (binopp op))) (let ((__function__ 'atc-exec-binary-rules-for-op-gen)) (declare (ignorable __function__)) (b* (((mv names events) (atc-exec-binary-rules-gen (list op) *nonchar-integer-types* *nonchar-integer-types*)) (atc-exec-op-rules (pack '*atc-exec- (binop-kind op) '-rules*)) (defconst-names (cons 'defconst (cons atc-exec-op-rules (cons (cons 'quote (cons names 'nil)) 'nil)))) (atc-exec-op-events (pack '*atc-exec- (binop-kind op) '-events*)) (defconst-events (cons 'defconst (cons atc-exec-op-events (cons (cons 'quote (cons events 'nil)) 'nil))))) (cons 'progn (append events (cons defconst-names (cons defconst-events 'nil)))))))
Theorem:
(defthm pseudo-event-formp-of-atc-exec-binary-rules-for-op-gen (b* ((event (atc-exec-binary-rules-for-op-gen op))) (pseudo-event-formp event)) :rule-classes :rewrite)