		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-expr-pure

Execute a pure expression.

Signature
(exec-expr-pure e compst) → eval
Arguments: e — Guard (exprp e).; compst — Guard (compustatep compst).
Returns: eval — Type (expr-value-resultp eval).

We return an error if we encounter a non-pure expression. While function calls do not necessarily have side effects, establishing that requires looking at the function. Thus, for simplicity, we regard function calls to be non-pure, i.e. we return an error if we encounter them here.

We also reject pre/post-increment/decrement expressions, which are obviously non-pure.

When executing a ternary expression, we drop any object designators from the second or third expression's execution, because ternary expressions are not lvalues [C:6.5.15/4, footnote 113].

Recall that our C abstract syntax does not cover all the possible C expressions yet. Thus, we may extend this ACL2 function with support for more kinds of pure expressions in the future.

If no error occurs, none of the expressions has side effects. Thus, the order in which the subexpressions are evaluated does not matter: we just proceed left to right.

Definitions and Theorems

Function: exec-expr-pure

(defun exec-expr-pure (e compst)
 (declare (xargs :guard (and (exprp e) (compustatep compst))))
 (let ((__function__ 'exec-expr-pure))
  (declare (ignorable __function__))
  (b* ((e (expr-fix e)))
   (expr-case
     e :ident (exec-ident e.get compst)
     :const (exec-const e.get)
     :arrsub
     (b* ((arr (exec-expr-pure e.arr compst))
          ((when (errorp arr)) arr)
          (sub (exec-expr-pure e.sub compst))
          ((when (errorp sub)) sub))
       (exec-arrsub arr sub compst))
     :call (error (list :non-pure-expr e))
     :member
     (b* ((str (exec-expr-pure e.target compst))
          ((when (errorp str)) str))
       (exec-member str e.name))
     :memberp
     (b* ((str (exec-expr-pure e.target compst))
          ((when (errorp str)) str))
       (exec-memberp str e.name compst))
     :postinc (error (list :non-pure-expr e))
     :postdec (error (list :non-pure-expr e))
     :preinc (error (list :non-pure-expr e))
     :predec (error (list :non-pure-expr e))
     :unary
     (b* ((arg (exec-expr-pure e.arg compst))
          ((when (errorp arg)) arg))
       (exec-unary e.op arg compst))
     :cast
     (b* ((arg (exec-expr-pure e.arg compst))
          ((when (errorp arg)) arg))
       (exec-cast e.type arg))
     :binary
     (b* (((unless (binop-purep e.op))
           (error (list :non-pure-expr e))))
       (case (binop-kind e.op)
         (:logand (b* ((arg1 (exec-expr-pure e.arg1 compst))
                       ((when (errorp arg1)) arg1)
                       (arg1 (apconvert-expr-value arg1))
                       ((when (errorp arg1)) arg1)
                       (test1 (test-value (expr-value->value arg1)))
                       ((when (errorp test1)) test1)
                       ((when (not test1))
                        (make-expr-value :value (value-sint 0)
                                         :object nil))
                       (arg2 (exec-expr-pure e.arg2 compst))
                       ((when (errorp arg2)) arg2)
                       (arg2 (apconvert-expr-value arg2))
                       ((when (errorp arg2)) arg2)
                       (test2 (test-value (expr-value->value arg2)))
                       ((when (errorp test2)) test2))
                    (if test2 (make-expr-value :value (value-sint 1)
                                               :object nil)
                      (make-expr-value :value (value-sint 0)
                                       :object nil))))
         (:logor (b* ((arg1 (exec-expr-pure e.arg1 compst))
                      ((when (errorp arg1)) arg1)
                      (arg1 (apconvert-expr-value arg1))
                      ((when (errorp arg1)) arg1)
                      (test1 (test-value (expr-value->value arg1)))
                      ((when (errorp test1)) test1)
                      ((when test1)
                       (make-expr-value :value (value-sint 1)
                                        :object nil))
                      (arg2 (exec-expr-pure e.arg2 compst))
                      ((when (errorp arg2)) arg2)
                      (arg2 (apconvert-expr-value arg2))
                      ((when (errorp arg2)) arg2)
                      (test2 (test-value (expr-value->value arg2)))
                      ((when (errorp test2)) test2))
                   (if test2 (make-expr-value :value (value-sint 1)
                                              :object nil)
                     (make-expr-value :value (value-sint 0)
                                      :object nil))))
         (t (b* ((arg1 (exec-expr-pure e.arg1 compst))
                 ((when (errorp arg1)) arg1)
                 (arg2 (exec-expr-pure e.arg2 compst))
                 ((when (errorp arg2)) arg2))
              (exec-binary-strict-pure e.op arg1 arg2)))))
     :cond
     (b* ((test (exec-expr-pure e.test compst))
          ((when (errorp test)) test)
          (test (apconvert-expr-value test))
          ((when (errorp test)) test)
          (test (test-value (expr-value->value test)))
          ((when (errorp test)) test))
       (if test (b* ((eval (exec-expr-pure e.then compst))
                     ((when (errorp eval)) eval)
                     (eval (apconvert-expr-value eval))
                     ((when (errorp eval)) eval))
                  (change-expr-value eval :object nil))
         (b* ((eval (exec-expr-pure e.else compst))
              ((when (errorp eval)) eval)
              (eval (apconvert-expr-value eval))
              ((when (errorp eval)) eval))
           (change-expr-value eval
                              :object nil))))))))

Theorem: expr-value-resultp-of-exec-expr-pure

(defthm expr-value-resultp-of-exec-expr-pure
  (b* ((eval (exec-expr-pure e compst)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: expr-value-resultp-of-exec-expr-pure-forward

(defthm expr-value-resultp-of-exec-expr-pure-forward
  (b* ((common-lisp::?eval (exec-expr-pure e compst)))
    (expr-value-resultp eval))
  :rule-classes
  ((:forward-chaining :trigger-terms ((exec-expr-pure e compst)))))

Theorem: exec-expr-pure-of-expr-fix-e

(defthm exec-expr-pure-of-expr-fix-e
  (equal (exec-expr-pure (expr-fix e) compst)
         (exec-expr-pure e compst)))

Theorem: exec-expr-pure-expr-equiv-congruence-on-e

(defthm exec-expr-pure-expr-equiv-congruence-on-e
  (implies (expr-equiv e e-equiv)
           (equal (exec-expr-pure e compst)
                  (exec-expr-pure e-equiv compst)))
  :rule-classes :congruence)

Theorem: exec-expr-pure-of-compustate-fix-compst

(defthm exec-expr-pure-of-compustate-fix-compst
  (equal (exec-expr-pure e (compustate-fix compst))
         (exec-expr-pure e compst)))

Theorem: exec-expr-pure-compustate-equiv-congruence-on-compst

(defthm exec-expr-pure-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-expr-pure e compst)
                  (exec-expr-pure e compst-equiv)))
  :rule-classes :congruence)