Rules for executing constants.
To symbolically execute a constant,
which in our current C subset may only be an integer constant,
we use rules corresponding to the possible integer types of the constant.
The rules are openers for exec-const,
under suitable conditions.
The argument of exec-const is a quoted constant
during symbolic execution,
because it is taken from the ASTs being executed;
thus, we enable the executable counterparts
of the fixtype functions that operate on constants
and of the
Theorem:
(defthm exec-const-to-sint (implies (and (syntaxp (quotep const)) (const-case const :int) (equal iconst (const-int->get const)) (not (iconst->unsignedp iconst)) (iconst-length-case (iconst->length iconst) :none) (equal value (iconst->value iconst)) (sint-integerp value)) (equal (exec-const const) (expr-value (sint-from-integer value) nil))))
Theorem:
(defthm exec-const-to-slong (implies (and (syntaxp (quotep const)) (const-case const :int) (equal iconst (const-int->get const)) (not (iconst->unsignedp iconst)) (equal value (iconst->value iconst)) (slong-integerp value) (equal length (iconst->length iconst)) (equal base (iconst->base iconst)) (or (and (iconst-length-case length :none) (not (sint-integerp value)) (or (iconst-base-case base :dec) (not (uint-integerp value)))) (iconst-length-case length :long))) (equal (exec-const const) (expr-value (slong-from-integer value) nil))))
Theorem:
(defthm exec-const-to-sllong (implies (and (syntaxp (quotep const)) (const-case const :int) (equal iconst (const-int->get const)) (not (iconst->unsignedp iconst)) (equal value (iconst->value iconst)) (sllong-integerp value) (equal length (iconst->length iconst)) (equal base (iconst->base iconst)) (or (and (iconst-length-case length :none) (not (slong-integerp value)) (or (iconst-base-case base :dec) (not (ulong-integerp value)))) (and (iconst-length-case length :long) (not (slong-integerp value)) (or (iconst-base-case base :dec) (not (ulong-integerp value)))) (iconst-length-case length :llong))) (equal (exec-const const) (expr-value (sllong-from-integer value) nil))))
Theorem:
(defthm exec-const-to-uint (implies (and (syntaxp (quotep const)) (const-case const :int) (equal iconst (const-int->get const)) (iconst-length-case (iconst->length iconst) :none) (equal value (iconst->value iconst)) (uint-integerp value) (or (iconst->unsignedp iconst) (and (not (iconst-base-case (iconst->base iconst) :dec)) (not (sint-integerp value))))) (equal (exec-const const) (expr-value (uint-from-integer value) nil))))
Theorem:
(defthm exec-const-to-ulong (implies (and (syntaxp (quotep const)) (const-case const :int) (equal iconst (const-int->get const)) (equal value (iconst->value iconst)) (ulong-integerp value) (equal length (iconst->length iconst)) (equal base (iconst->base iconst)) (or (and (iconst->unsignedp iconst) (or (and (iconst-length-case length :none) (not (uint-integerp value))) (iconst-length-case length :long))) (and (not (iconst-base-case base :dec)) (not (slong-integerp value)) (or (and (iconst-length-case length :none) (not (uint-integerp value))) (iconst-length-case length :long))))) (equal (exec-const const) (expr-value (ulong-from-integer value) nil))))
Theorem:
(defthm exec-const-to-ullong (implies (and (syntaxp (quotep const)) (const-case const :int) (equal iconst (const-int->get const)) (equal value (iconst->value iconst)) (ullong-integerp value) (equal length (iconst->length iconst)) (equal base (iconst->base iconst)) (or (and (iconst->unsignedp iconst) (or (iconst-length-case length :llong) (not (ulong-integerp value)))) (and (not (iconst-base-case base :dec)) (not (sllong-integerp value)) (or (iconst-length-case length :llong) (not (ulong-integerp value)))))) (equal (exec-const const) (expr-value (ullong-from-integer value) nil))))