Rules for exec-expr-pure.
For
We include the executable counterpart of member-equal, needed to discharge the hypothesis of the rule for strict pure binary expressions.
We include executable counterparts of accessor functions for expressions, used to check the kind of expression and to retrieve its constituents.
Besides the rules for the large symbolic execution, whose names we put into the constant defined at the end, we also prove rules used in the new modular proofs. The latter rules avoid if in the right side, to avoid unwanted case splits; furthermore, they wrap the if tests into test* to prevent unwanted rewrites (see atc-contextualize).
We also include the function
We also include the function
Function:
(defun exec-arrsub-of-member (str mem sub compst) (declare (xargs :guard (and (expr-valuep str) (identp mem) (expr-valuep sub) (compustatep compst)))) (let ((__function__ 'exec-arrsub-of-member)) (declare (ignorable __function__)) (b* ((str (apconvert-expr-value str)) ((when (errorp str)) str) (val-str (expr-value->value str)) ((unless (value-case val-str :struct)) (error (list :mistype-member :required :struct :supplied (type-of-value val-str)))) (val-mem (value-struct-read mem val-str)) ((when (errorp val-mem)) val-mem) (objdes-str (expr-value->object str)) (objdes-mem (and objdes-str (make-objdesign-member :super objdes-str :name mem))) (eval-mem (apconvert-expr-value (expr-value val-mem objdes-mem))) ((when (errorp eval-mem)) eval-mem) (val-mem (expr-value->value eval-mem)) ((unless (value-case val-mem :pointer)) (error (list :mistype-arrsub :required :pointer :supplied (type-of-value val-mem)))) ((unless (value-pointer-validp val-mem)) (error (list :invalid-pointer val-mem))) (objdes-mem (value-pointer->designator val-mem)) (reftype (value-pointer->reftype val-mem)) (array (read-object objdes-mem compst)) ((when (errorp array)) (error (list :array-not-found val-mem (compustate-fix compst)))) ((unless (value-case array :array)) (error (list :not-array val-mem (compustate-fix compst)))) ((unless (equal reftype (value-array->elemtype array))) (error (list :mistype-array-read :pointer reftype :array (value-array->elemtype array)))) (sub (apconvert-expr-value sub)) ((when (errorp sub)) sub) (sub (expr-value->value sub)) ((unless (value-integerp sub)) (error (list :mistype-array :index :required :integer :supplied (type-of-value sub)))) (index (value-integer->get sub)) ((when (< index 0)) (error (list :negative-array-index :array array :index sub))) (val (value-array-read index array)) ((when (errorp val)) val) (elem-objdes (make-objdesign-element :super objdes-mem :index index))) (make-expr-value :value val :object elem-objdes))))
Theorem:
(defthm expr-value-resultp-of-exec-arrsub-of-member (b* ((eval (exec-arrsub-of-member str mem sub compst))) (expr-value-resultp eval)) :rule-classes :rewrite)
Theorem:
(defthm exec-arrsub-of-member-of-expr-value-fix-str (equal (exec-arrsub-of-member (expr-value-fix str) mem sub compst) (exec-arrsub-of-member str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-member-expr-value-equiv-congruence-on-str (implies (expr-value-equiv str str-equiv) (equal (exec-arrsub-of-member str mem sub compst) (exec-arrsub-of-member str-equiv mem sub compst))) :rule-classes :congruence)
Theorem:
(defthm exec-arrsub-of-member-of-ident-fix-mem (equal (exec-arrsub-of-member str (ident-fix mem) sub compst) (exec-arrsub-of-member str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-member-ident-equiv-congruence-on-mem (implies (ident-equiv mem mem-equiv) (equal (exec-arrsub-of-member str mem sub compst) (exec-arrsub-of-member str mem-equiv sub compst))) :rule-classes :congruence)
Theorem:
(defthm exec-arrsub-of-member-of-expr-value-fix-sub (equal (exec-arrsub-of-member str mem (expr-value-fix sub) compst) (exec-arrsub-of-member str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-member-expr-value-equiv-congruence-on-sub (implies (expr-value-equiv sub sub-equiv) (equal (exec-arrsub-of-member str mem sub compst) (exec-arrsub-of-member str mem sub-equiv compst))) :rule-classes :congruence)
Theorem:
(defthm exec-arrsub-of-member-of-compustate-fix-compst (equal (exec-arrsub-of-member str mem sub (compustate-fix compst)) (exec-arrsub-of-member str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-member-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (exec-arrsub-of-member str mem sub compst) (exec-arrsub-of-member str mem sub compst-equiv))) :rule-classes :congruence)
Function:
(defun exec-arrsub-of-memberp (str mem sub compst) (declare (xargs :guard (and (expr-valuep str) (identp mem) (expr-valuep sub) (compustatep compst)))) (let ((__function__ 'exec-arrsub-of-memberp)) (declare (ignorable __function__)) (b* ((str (apconvert-expr-value str)) ((when (errorp str)) str) (str (expr-value->value str)) ((unless (value-case str :pointer)) (error (list :mistype-memberp :required :pointer :supplied (type-of-value str)))) ((unless (value-pointer-validp str)) (error (list :invalid-pointer str))) (objdes (value-pointer->designator str)) (reftype (value-pointer->reftype str)) (struct (read-object objdes compst)) ((when (errorp struct)) (error (list :struct-not-found str (compustate-fix compst)))) ((unless (value-case struct :struct)) (error (list :not-struct str (compustate-fix compst)))) ((unless (equal reftype (type-struct (value-struct->tag struct)))) (error (list :mistype-struct-read :pointer reftype :array (type-struct (value-struct->tag struct))))) (val-mem (value-struct-read mem struct)) ((when (errorp val-mem)) val-mem) (objdes-mem (make-objdesign-member :super objdes :name mem)) (eval-mem (apconvert-expr-value (expr-value val-mem objdes-mem))) ((when (errorp eval-mem)) eval-mem) (val-mem (expr-value->value eval-mem)) ((unless (value-case val-mem :pointer)) (error (list :mistype-arrsub :required :pointer :supplied (type-of-value val-mem)))) ((unless (value-pointer-validp val-mem)) (error (list :invalid-pointer val-mem))) (objdes-mem (value-pointer->designator val-mem)) (reftype (value-pointer->reftype val-mem)) (array (read-object objdes-mem compst)) ((when (errorp array)) (error (list :array-not-found val-mem (compustate-fix compst)))) ((unless (value-case array :array)) (error (list :not-array val-mem (compustate-fix compst)))) ((unless (equal reftype (value-array->elemtype array))) (error (list :mistype-array-read :pointer reftype :array (value-array->elemtype array)))) (sub (apconvert-expr-value sub)) ((when (errorp sub)) sub) (sub (expr-value->value sub)) ((unless (value-integerp sub)) (error (list :mistype-array :index :required :integer :supplied (type-of-value sub)))) (index (value-integer->get sub)) ((when (< index 0)) (error (list :negative-array-index :array array :index sub))) (val (value-array-read index array)) ((when (errorp val)) val) (elem-objdes (make-objdesign-element :super objdes-mem :index index))) (make-expr-value :value val :object elem-objdes))))
Theorem:
(defthm expr-value-resultp-of-exec-arrsub-of-memberp (b* ((eval (exec-arrsub-of-memberp str mem sub compst))) (expr-value-resultp eval)) :rule-classes :rewrite)
Theorem:
(defthm exec-arrsub-of-memberp-of-expr-value-fix-str (equal (exec-arrsub-of-memberp (expr-value-fix str) mem sub compst) (exec-arrsub-of-memberp str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-memberp-expr-value-equiv-congruence-on-str (implies (expr-value-equiv str str-equiv) (equal (exec-arrsub-of-memberp str mem sub compst) (exec-arrsub-of-memberp str-equiv mem sub compst))) :rule-classes :congruence)
Theorem:
(defthm exec-arrsub-of-memberp-of-ident-fix-mem (equal (exec-arrsub-of-memberp str (ident-fix mem) sub compst) (exec-arrsub-of-memberp str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-memberp-ident-equiv-congruence-on-mem (implies (ident-equiv mem mem-equiv) (equal (exec-arrsub-of-memberp str mem sub compst) (exec-arrsub-of-memberp str mem-equiv sub compst))) :rule-classes :congruence)
Theorem:
(defthm exec-arrsub-of-memberp-of-expr-value-fix-sub (equal (exec-arrsub-of-memberp str mem (expr-value-fix sub) compst) (exec-arrsub-of-memberp str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-memberp-expr-value-equiv-congruence-on-sub (implies (expr-value-equiv sub sub-equiv) (equal (exec-arrsub-of-memberp str mem sub compst) (exec-arrsub-of-memberp str mem sub-equiv compst))) :rule-classes :congruence)
Theorem:
(defthm exec-arrsub-of-memberp-of-compustate-fix-compst (equal (exec-arrsub-of-memberp str mem sub (compustate-fix compst)) (exec-arrsub-of-memberp str mem sub compst)))
Theorem:
(defthm exec-arrsub-of-memberp-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (exec-arrsub-of-memberp str mem sub compst) (exec-arrsub-of-memberp str mem sub compst-equiv))) :rule-classes :congruence)
Theorem:
(defthm exec-expr-pure-when-ident (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :ident)) (equal (exec-expr-pure e compst) (exec-ident (expr-ident->get e) compst))))
Theorem:
(defthm exec-expr-pure-when-ident-no-syntaxp (implies (equal (expr-kind e) :ident) (equal (exec-expr-pure e compst) (exec-ident (expr-ident->get e) compst))))
Theorem:
(defthm exec-expr-pure-when-const (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :const)) (equal (exec-expr-pure e compst) (exec-const (expr-const->get e)))))
Theorem:
(defthm exec-expr-pure-when-arrsub (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :arrsub) (equal arr (expr-arrsub->arr e)) (not (expr-case arr :member)) (not (expr-case arr :memberp)) (equal evalarr (exec-expr-pure arr compst)) (expr-valuep evalarr) (equal evalsub (exec-expr-pure (expr-arrsub->sub e) compst)) (expr-valuep evalsub)) (equal (exec-expr-pure e compst) (exec-arrsub evalarr evalsub compst))))
Theorem:
(defthm exec-expr-pure-when-member (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :member) (equal eval (exec-expr-pure (expr-member->target e) compst)) (expr-valuep eval)) (equal (exec-expr-pure e compst) (exec-member eval (expr-member->name e)))))
Theorem:
(defthm exec-expr-pure-when-member-no-syntaxp (implies (and (equal (expr-kind e) :member) (equal eval (exec-expr-pure (expr-member->target e) compst)) (expr-valuep eval)) (equal (exec-expr-pure e compst) (exec-member eval (expr-member->name e)))))
Theorem:
(defthm exec-expr-pure-when-memberp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :memberp) (equal eval (exec-expr-pure (expr-memberp->target e) compst)) (expr-valuep eval)) (equal (exec-expr-pure e compst) (exec-memberp eval (expr-memberp->name e) compst))))
Theorem:
(defthm exec-expr-pure-when-memberp-no-syntaxp (implies (and (equal (expr-kind e) :memberp) (equal eval (exec-expr-pure (expr-memberp->target e) compst)) (expr-valuep eval)) (equal (exec-expr-pure e compst) (exec-memberp eval (expr-memberp->name e) compst))))
Theorem:
(defthm exec-expr-pure-when-arrsub-of-member (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :arrsub) (equal arr (expr-arrsub->arr e)) (expr-case arr :member) (equal evalstr (exec-expr-pure (expr-member->target arr) compst)) (expr-valuep evalstr) (equal evalsub (exec-expr-pure (expr-arrsub->sub e) compst)) (expr-valuep evalsub)) (equal (exec-expr-pure e compst) (exec-arrsub-of-member evalstr (expr-member->name arr) evalsub compst))))
Theorem:
(defthm exec-expr-pure-when-arrsub-of-member-no-syntaxp (implies (and (equal (expr-kind e) :arrsub) (equal arr (expr-arrsub->arr e)) (expr-case arr :member) (equal evalstr (exec-expr-pure (expr-member->target arr) compst)) (expr-valuep evalstr) (equal evalsub (exec-expr-pure (expr-arrsub->sub e) compst)) (expr-valuep evalsub)) (equal (exec-expr-pure e compst) (exec-arrsub-of-member evalstr (expr-member->name arr) evalsub compst))))
Theorem:
(defthm exec-expr-pure-when-arrsub-of-memberp (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :arrsub) (equal arr (expr-arrsub->arr e)) (expr-case arr :memberp) (equal evalstr (exec-expr-pure (expr-memberp->target arr) compst)) (expr-valuep evalstr) (equal evalsub (exec-expr-pure (expr-arrsub->sub e) compst)) (expr-valuep evalsub)) (equal (exec-expr-pure e compst) (exec-arrsub-of-memberp evalstr (expr-memberp->name arr) evalsub compst))))
Theorem:
(defthm exec-expr-pure-when-arrsub-of-memberp-no-syntaxp (implies (and (equal (expr-kind e) :arrsub) (equal arr (expr-arrsub->arr e)) (expr-case arr :memberp) (equal evalstr (exec-expr-pure (expr-memberp->target arr) compst)) (expr-valuep evalstr) (equal evalsub (exec-expr-pure (expr-arrsub->sub e) compst)) (expr-valuep evalsub)) (equal (exec-expr-pure e compst) (exec-arrsub-of-memberp evalstr (expr-memberp->name arr) evalsub compst))))
Theorem:
(defthm exec-expr-pure-when-unary (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :unary) (equal eval (exec-expr-pure (expr-unary->arg e) compst)) (expr-valuep eval)) (equal (exec-expr-pure e compst) (exec-unary (expr-unary->op e) eval compst))))
Theorem:
(defthm exec-expr-pure-when-cast (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :cast) (equal eval (exec-expr-pure (expr-cast->arg e) compst)) (expr-valuep eval)) (equal (exec-expr-pure e compst) (exec-cast (expr-cast->type e) eval))))
Theorem:
(defthm exec-expr-pure-when-strict-pure-binary (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal op (expr-binary->op e)) (member-equal (binop-kind op) '(:mul :div :rem :add :sub :shl :shr :lt :gt :le :ge :eq :ne :bitand :bitxor :bitior)) (equal eval1 (exec-expr-pure (expr-binary->arg1 e) compst)) (equal eval2 (exec-expr-pure (expr-binary->arg2 e) compst)) (expr-valuep eval1) (expr-valuep eval2)) (equal (exec-expr-pure e compst) (exec-binary-strict-pure op eval1 eval2))))
Function:
(defun sint-from-boolean-with-error (test) (if (errorp test) test (if test (expr-value (sint-from-integer 1) nil) (expr-value (sint-from-integer 0) nil))))
Theorem:
(defthm exec-expr-pure-when-binary-logand (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal op (expr-binary->op e)) (equal (binop-kind op) :logand) (equal arg1 (exec-expr-pure (expr-binary->arg1 e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test1 (test-value (expr-value->value carg1))) (booleanp test1)) (equal (exec-expr-pure e compst) (if test1 (sint-from-boolean-with-error (b* ((arg2 (exec-expr-pure (expr-binary->arg2 e) compst)) ((when (errorp arg2)) arg2) (arg2 (apconvert-expr-value arg2)) ((when (errorp arg2)) arg2)) (test-value (expr-value->value arg2)))) (expr-value (sint-from-integer 0) nil)))))
Theorem:
(defthm exec-expr-pure-when-binary-logand-and-true (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal op (expr-binary->op e)) (equal (binop-kind op) :logand) (equal arg1 (exec-expr-pure (expr-binary->arg1 e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test1 (test-value (expr-value->value carg1))) (booleanp test1) (test* test1) (equal arg2 (exec-expr-pure (expr-binary->arg2 e) compst)) (expr-valuep arg2) (equal carg2 (apconvert-expr-value arg2)) (expr-valuep carg2) (equal test2 (test-value (expr-value->value carg2))) (booleanp test2)) (equal (exec-expr-pure e compst) (expr-value (sint-from-boolean test2) nil))))
Theorem:
(defthm exec-expr-pure-when-binary-logand-and-false (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal op (expr-binary->op e)) (equal (binop-kind op) :logand) (equal arg1 (exec-expr-pure (expr-binary->arg1 e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test1 (test-value (expr-value->value carg1))) (booleanp test1) (test* (not test1))) (equal (exec-expr-pure e compst) (expr-value (sint-from-integer 0) nil))))
Theorem:
(defthm exec-expr-pure-when-binary-logor (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal op (expr-binary->op e)) (equal (binop-kind op) :logor) (equal arg1 (exec-expr-pure (expr-binary->arg1 e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test1 (test-value (expr-value->value carg1))) (booleanp test1)) (equal (exec-expr-pure e compst) (if test1 (expr-value (sint-from-integer 1) nil) (sint-from-boolean-with-error (b* ((arg2 (exec-expr-pure (expr-binary->arg2 e) compst)) ((when (errorp arg2)) arg2) (arg2 (apconvert-expr-value arg2)) ((when (errorp arg2)) arg2)) (test-value (expr-value->value arg2))))))))
Theorem:
(defthm exec-expr-pure-when-binary-logor-and-true (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal op (expr-binary->op e)) (equal (binop-kind op) :logor) (equal arg1 (exec-expr-pure (expr-binary->arg1 e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test1 (test-value (expr-value->value carg1))) (booleanp test1) (test* test1)) (equal (exec-expr-pure e compst) (expr-value (sint-from-integer 1) nil))))
Theorem:
(defthm exec-expr-pure-when-binary-logor-and-false (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :binary) (equal op (expr-binary->op e)) (equal (binop-kind op) :logor) (equal arg1 (exec-expr-pure (expr-binary->arg1 e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test1 (test-value (expr-value->value carg1))) (booleanp test1) (test* (not test1)) (equal arg2 (exec-expr-pure (expr-binary->arg2 e) compst)) (expr-valuep arg2) (equal carg2 (apconvert-expr-value arg2)) (expr-valuep carg2) (equal test2 (test-value (expr-value->value carg2))) (booleanp test2)) (equal (exec-expr-pure e compst) (expr-value (sint-from-boolean test2) nil))))
Theorem:
(defthm sint-from-boolean-with-error-when-booleanp (implies (and (syntaxp (or (atom test) (not (member-eq (car test) '(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))))) (booleanp test)) (equal (sint-from-boolean-with-error test) (if test (expr-value (sint-from-integer 1) nil) (expr-value (sint-from-integer 0) nil)))))
Theorem:
(defthm sint-from-boolean-with-error-when-booleanp-and-true (implies (and (syntaxp (or (atom test) (not (member-eq (car test) '(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))))) (booleanp test) (test* test)) (equal (sint-from-boolean-with-error test) (expr-value (sint-from-integer 1) nil))))
Theorem:
(defthm sint-from-boolean-with-error-when-booleanp-and-false (implies (and (syntaxp (or (atom test) (not (member-eq (car test) '(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))))) (booleanp test) (test* (not test))) (equal (sint-from-boolean-with-error test) (expr-value (sint-from-integer 0) nil))))
Function:
(defun exec-expr-pure-apconvert-no-object (e compst) (b* ((eval (exec-expr-pure e compst)) ((when (errorp eval)) eval) (eval1 (apconvert-expr-value eval)) ((when (errorp eval1)) eval1)) (expr-value (expr-value->value eval1) nil)))
Theorem:
(defthm exec-expr-pure-apconvert-no-object-open (implies (and (equal eval (exec-expr-pure e compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1)) (equal (exec-expr-pure-apconvert-no-object e compst) (expr-value (expr-value->value eval1) nil))))
Theorem:
(defthm exec-expr-pure-when-cond (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :cond) (equal arg1 (exec-expr-pure (expr-cond->test e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test (test-value (expr-value->value carg1))) (booleanp test)) (equal (exec-expr-pure e compst) (if test (exec-expr-pure-apconvert-no-object (expr-cond->then e) compst) (exec-expr-pure-apconvert-no-object (expr-cond->else e) compst)))))
Theorem:
(defthm exec-expr-pure-when-cond-and-true (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :cond) (equal arg1 (exec-expr-pure (expr-cond->test e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test (test-value (expr-value->value carg1))) (booleanp test) (test* test) (equal eval (exec-expr-pure (expr-cond->then e) compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1)) (equal (exec-expr-pure e compst) (expr-value (expr-value->value eval1) nil))))
Theorem:
(defthm exec-expr-pure-when-cond-and-false (implies (and (syntaxp (quotep e)) (equal (expr-kind e) :cond) (equal arg1 (exec-expr-pure (expr-cond->test e) compst)) (expr-valuep arg1) (equal carg1 (apconvert-expr-value arg1)) (expr-valuep carg1) (equal test (test-value (expr-value->value carg1))) (booleanp test) (test* (not test)) (equal eval (exec-expr-pure (expr-cond->else e) compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1)) (equal (exec-expr-pure e compst) (expr-value (expr-value->value eval1) nil))))