|
|
|---|
|
|
|
|---|
Code to generate the rules for executing assignments to integers by pointer.
Function:
(defun atc-exec-expr-when-asg-indir-rules-gen (type) (declare (xargs :guard (typep type))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'atc-exec-expr-when-asg-indir-rules-gen)) (declare (ignorable __function__)) (b* ((fixtype (integer-type-to-fixtype type)) (pred (pack fixtype 'p)) (constructor (pack 'type- fixtype)) (type-of-value-when-pred (pack 'type-of-value-when- pred)) (not-pred-of-value-pointer (pack 'not- pred '-of-value-pointer)) (value-kind-when-pred (pack 'value-kind-when- pred)) (writer (pack fixtype '-write)) (name (pack 'exec-expr-when-asg-indir-when- pred)) (name-mod-proofs (pack name '-for-modular-proofs)) (formula (cons 'implies (cons (cons 'and (cons '(syntaxp (quotep expr)) (cons '(equal (expr-kind expr) :binary) (cons '(equal (binop-kind (expr-binary->op expr)) :asg) (cons '(equal left (expr-binary->arg1 expr)) (cons '(equal right (expr-binary->arg2 expr)) (cons '(equal (expr-kind left) :unary) (cons '(equal (unop-kind (expr-unary->op left)) :indir) (cons '(equal arg (expr-unary->arg left)) (cons '(equal (expr-kind arg) :ident) (cons '(equal var (expr-ident->get arg)) (cons '(expr-purep right) (cons '(integerp limit) (cons '(>= limit (1+ (max 2 (expr-pure-limit right)))) (cons '(equal ptr (read-var var compst)) (cons '(valuep ptr) (cons '(value-case ptr :pointer) (cons '(value-pointer-validp ptr) (cons (cons 'equal (cons '(value-pointer->reftype ptr) (cons (cons constructor 'nil) 'nil))) (cons '(equal eval (exec-expr-pure right compst)) (cons '(expr-valuep eval) (cons '(equal eval1 (apconvert-expr-value eval)) (cons '(expr-valuep eval1) (cons '(equal val (expr-value->value eval1)) (cons (cons pred '(val)) '((equal oldval (read-object (value-pointer->designator ptr) compst)) (valuep oldval) (not (equal (value-kind oldval) :array)) (equal compst1 (write-object (value-pointer->designator ptr) val compst)) (compustatep compst1))))))))))))))))))))))))))) '((equal (exec-expr expr compst fenv limit) (mv (expr-value val nil) compst1)))))) (formula-mod-proofs (cons 'implies (cons (cons 'and (cons '(syntaxp (quotep expr)) (cons '(equal (expr-kind expr) :binary) (cons '(equal (binop-kind (expr-binary->op expr)) :asg) (cons '(equal left (expr-binary->arg1 expr)) (cons '(equal right (expr-binary->arg2 expr)) (cons '(equal (expr-kind left) :unary) (cons '(equal (unop-kind (expr-unary->op left)) :indir) (cons '(equal arg (expr-unary->arg left)) (cons '(equal (expr-kind arg) :ident) (cons '(equal var (expr-ident->get arg)) (cons '(expr-purep right) (cons '(integerp limit) (cons '(>= limit (1+ (max 2 (expr-pure-limit right)))) (cons '(equal ptr (read-var var compst)) (cons '(valuep ptr) (cons '(value-case ptr :pointer) (cons '(value-pointer-validp ptr) (cons (cons 'equal (cons '(value-pointer->reftype ptr) (cons (cons constructor 'nil) 'nil))) (cons '(equal eval (exec-expr-pure right compst)) (cons '(expr-valuep eval) (cons '(equal eval1 (apconvert-expr-value eval)) (cons '(expr-valuep eval1) (cons '(equal val (expr-value->value eval1)) (cons (cons pred '(val)) (cons '(equal oldval (read-object (value-pointer->designator ptr) compst)) (cons '(valuep oldval) (cons '(not (equal (value-kind oldval) :array)) (cons (cons 'equal (cons 'compst1 (cons (cons 'write-object (cons '(value-pointer->designator ptr) (cons (cons writer '(val)) '(compst)))) 'nil))) '((compustatep compst1))))))))))))))))))))))))))))))) '((equal (exec-expr expr compst fenv limit) (mv (expr-value val nil) compst1)))))) (events (cons (cons 'defruled (cons name (cons formula (cons ':expand (cons '((exec-expr expr compst fenv limit) (exec-expr (expr-binary->arg1 expr) compst fenv (1- limit))) (cons ':enable (cons (cons 'exec-expr-to-exec-expr-pure-when-expr-pure-limit (cons 'max (cons 'nfix (cons 'exec-expr (cons 'exec-unary (cons 'exec-indir (cons 'exec-ident (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'value-kind-when-scharp (cons 'read-object-of-objdesign-of-var-to-read-var (cons type-of-value-when-pred (cons not-pred-of-value-pointer (cons value-kind-when-pred '(expr-purep binop-purep)))))))))))))) (cons ':disable (cons '(equal-of-error equal-of-expr-value) (cons ':prep-lemmas (cons (cons (cons 'defrule (cons 'lemma (cons (cons 'implies (cons (cons 'and (cons '(expr-valuep (apconvert-expr-value eval)) (cons (cons pred '((expr-value->value (apconvert-expr-value eval)))) 'nil))) (cons (cons pred '((expr-value->value eval))) 'nil))) '(:enable apconvert-expr-value)))) 'nil) 'nil))))))))))) (cons (cons 'defruled (cons name-mod-proofs (cons formula-mod-proofs (cons ':use (cons name (cons ':enable (cons writer 'nil))))))) 'nil)))) (mv name events))))
Theorem:
(defthm symbolp-of-atc-exec-expr-when-asg-indir-rules-gen.name (b* (((mv ?name ?events) (atc-exec-expr-when-asg-indir-rules-gen type))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-expr-when-asg-indir-rules-gen.events (b* (((mv ?name ?events) (atc-exec-expr-when-asg-indir-rules-gen type))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-expr-when-asg-indir-rules-gen-loop (types) (declare (xargs :guard (type-listp types))) (declare (xargs :guard (type-nonchar-integer-listp types))) (let ((__function__ 'atc-exec-expr-when-asg-indir-rules-gen-loop)) (declare (ignorable __function__)) (b* (((when (endp types)) (mv nil nil)) ((mv name events) (atc-exec-expr-when-asg-indir-rules-gen (car types))) ((mv more-names more-events) (atc-exec-expr-when-asg-indir-rules-gen-loop (cdr types)))) (mv (cons name more-names) (append events more-events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-expr-when-asg-indir-rules-gen-loop.names (b* (((mv ?names ?events) (atc-exec-expr-when-asg-indir-rules-gen-loop types))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-expr-when-asg-indir-rules-gen-loop.events (b* (((mv ?names ?events) (atc-exec-expr-when-asg-indir-rules-gen-loop types))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-expr-when-asg-indir-rules-gen-all nil (declare (xargs :guard t)) (let ((__function__ 'atc-exec-expr-when-asg-indir-rules-gen-all)) (declare (ignorable __function__)) (b* (((mv names events) (atc-exec-expr-when-asg-indir-rules-gen-loop *nonchar-integer-types*))) (cons 'progn (cons (cons 'defsection (cons 'atc-exec-expr-when-asg-indir-rules (cons ':short (cons '"Rules for executing assignment expressions to integers by pointer." (append events (cons (cons 'defval (cons '*atc-exec-expr-when-asg-indir-rules* (cons (cons 'quote (cons (append names '((:e expr-kind) (:e binop-kind) (:e expr-binary->op) (:e expr-binary->arg1) (:e expr-binary->arg2) (:e unop-kind) (:e expr-unary->op) (:e expr-unary->arg) (:e expr-ident->get))) 'nil)) 'nil))) 'nil)))))) 'nil)))))
Theorem:
(defthm pseudo-event-formp-of-atc-exec-expr-when-asg-indir-rules-gen-all (b* ((event (atc-exec-expr-when-asg-indir-rules-gen-all))) (pseudo-event-formp event)) :rule-classes :rewrite)