Rules for executing assignment expressions to integers by pointer.
Theorem:
(defthm exec-expr-asg-indir-when-scharp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-schar)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (scharp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-scharp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-schar)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (scharp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (schar-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ucharp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uchar)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ucharp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ucharp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uchar)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ucharp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (uchar-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-sshortp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sshort)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sshortp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-sshortp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sshort)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sshortp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sshort-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ushortp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ushort)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ushortp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ushortp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ushort)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ushortp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ushort-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-sintp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sint)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sintp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-sintp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sint)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sintp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sint-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-uintp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uint)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (uintp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-uintp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uint)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (uintp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (uint-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-slongp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-slong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (slongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-slongp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-slong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (slongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (slong-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ulongp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ulong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ulongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ulongp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ulong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ulongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ulong-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-sllongp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sllong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sllongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-sllongp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sllong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sllongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sllong-write val) compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ullongp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ullong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ullongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) val compst))))
Theorem:
(defthm exec-expr-asg-indir-when-ullongp-for-modular-proofs (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :unary) (equal (unop-kind (expr-unary->op left)) :indir) (equal arg (expr-unary->arg left)) (equal (expr-kind arg) :ident) (equal var (expr-ident->get arg)) (not (zp limit)) (equal ptr (read-var var compst)) (valuep ptr) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ullong)) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ullongp val) (valuep (read-object (value-pointer->designator ptr) compst))) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ullong-write val) compst))))