Rules for executing unary operations that do not involve pointers.
Theorem:
(defthm plus-value-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (scharp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-schar x) nil))))
Theorem:
(defthm plus-value-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (ucharp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-uchar x) nil))))
Theorem:
(defthm plus-value-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (sshortp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-sshort x) nil))))
Theorem:
(defthm plus-value-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (ushortp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-ushort x) nil))))
Theorem:
(defthm plus-value-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (sintp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-sint x) nil))))
Theorem:
(defthm plus-value-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (uintp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-uint x) nil))))
Theorem:
(defthm plus-value-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (slongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-slong x) nil))))
Theorem:
(defthm plus-value-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (ulongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-ulong x) nil))))
Theorem:
(defthm plus-value-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (sllongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-sllong x) nil))))
Theorem:
(defthm plus-value-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-plus)) (ullongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (plus-ullong x) nil))))
Theorem:
(defthm minus-value-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (scharp x) (minus-schar-okp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-schar x) nil))))
Theorem:
(defthm minus-value-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (ucharp x) (minus-uchar-okp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-uchar x) nil))))
Theorem:
(defthm minus-value-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (sshortp x) (minus-sshort-okp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-sshort x) nil))))
Theorem:
(defthm minus-value-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (ushortp x) (minus-ushort-okp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-ushort x) nil))))
Theorem:
(defthm minus-value-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (sintp x) (minus-sint-okp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-sint x) nil))))
Theorem:
(defthm minus-value-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (uintp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-uint x) nil))))
Theorem:
(defthm minus-value-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (slongp x) (minus-slong-okp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-slong x) nil))))
Theorem:
(defthm minus-value-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (ulongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-ulong x) nil))))
Theorem:
(defthm minus-value-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (sllongp x) (minus-sllong-okp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-sllong x) nil))))
Theorem:
(defthm minus-value-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-minus)) (ullongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (minus-ullong x) nil))))
Theorem:
(defthm bitnot-value-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (scharp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-schar x) nil))))
Theorem:
(defthm bitnot-value-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (ucharp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-uchar x) nil))))
Theorem:
(defthm bitnot-value-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (sshortp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-sshort x) nil))))
Theorem:
(defthm bitnot-value-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (ushortp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-ushort x) nil))))
Theorem:
(defthm bitnot-value-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (sintp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-sint x) nil))))
Theorem:
(defthm bitnot-value-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (uintp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-uint x) nil))))
Theorem:
(defthm bitnot-value-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (slongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-slong x) nil))))
Theorem:
(defthm bitnot-value-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (ulongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-ulong x) nil))))
Theorem:
(defthm bitnot-value-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (sllongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-sllong x) nil))))
Theorem:
(defthm bitnot-value-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-bitnot)) (ullongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (bitnot-ullong x) nil))))
Theorem:
(defthm lognot-value-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (scharp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-schar x) nil))))
Theorem:
(defthm lognot-value-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (ucharp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-uchar x) nil))))
Theorem:
(defthm lognot-value-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (sshortp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-sshort x) nil))))
Theorem:
(defthm lognot-value-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (ushortp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-ushort x) nil))))
Theorem:
(defthm lognot-value-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (sintp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-sint x) nil))))
Theorem:
(defthm lognot-value-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (uintp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-uint x) nil))))
Theorem:
(defthm lognot-value-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (slongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-slong x) nil))))
Theorem:
(defthm lognot-value-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (ulongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-ulong x) nil))))
Theorem:
(defthm lognot-value-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (sllongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-sllong x) nil))))
Theorem:
(defthm lognot-value-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (equal op (unop-lognot)) (ullongp x)) (equal (exec-unary op (expr-value x objdes) compst) (expr-value (lognot-ullong x) nil))))