		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-unary

Execute a unary operation on an expression value.

Signature
(exec-unary op arg compst) → eval
Arguments: op — Guard (unopp op).; arg — Guard (expr-valuep arg).; compst — Guard (compustatep compst).
Returns: eval — Type (expr-value-resultp eval).

This ACL2 function wraps eval-unary to take and return expression values, and covers the remaining two unary operators & and *. Note that the only unary operator that needs an expression value (as opposed to just a value) is &, and that only unary operator that returns an expression value (as opposed to just a value) is *. The other four unary operators only operate on values, as factored in eval-unary.

Before calling eval-unary, we perform array-to-pointer conversion [C17:5.3.2.1/3]. The functions handle & and * perform that conversion as needed (specifically, & does not, while * does).

Definitions and Theorems

Function: exec-unary

(defun exec-unary (op arg compst)
  (declare (xargs :guard (and (unopp op)
                              (expr-valuep arg)
                              (compustatep compst))))
  (case (unop-kind op)
    (:address (exec-address arg))
    (:indir (exec-indir arg compst))
    (t (b* ((arg (apconvert-expr-value arg))
            ((when (errorp arg)) arg)
            (val (eval-unary op (expr-value->value arg)))
            ((when (errorp val)) val))
         (make-expr-value :value val
                          :object nil)))))

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

(defthm expr-value-resultp-of-exec-unary
  (b* ((eval (exec-unary op arg compst)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: exec-unary-of-unop-fix-op

(defthm exec-unary-of-unop-fix-op
  (equal (exec-unary (unop-fix op) arg compst)
         (exec-unary op arg compst)))

Theorem: exec-unary-unop-equiv-congruence-on-op

(defthm exec-unary-unop-equiv-congruence-on-op
  (implies (unop-equiv op op-equiv)
           (equal (exec-unary op arg compst)
                  (exec-unary op-equiv arg compst)))
  :rule-classes :congruence)

Theorem: exec-unary-of-expr-value-fix-arg

(defthm exec-unary-of-expr-value-fix-arg
  (equal (exec-unary op (expr-value-fix arg)
                     compst)
         (exec-unary op arg compst)))

Theorem: exec-unary-expr-value-equiv-congruence-on-arg

(defthm exec-unary-expr-value-equiv-congruence-on-arg
  (implies (expr-value-equiv arg arg-equiv)
           (equal (exec-unary op arg compst)
                  (exec-unary op arg-equiv compst)))
  :rule-classes :congruence)

Theorem: exec-unary-of-compustate-fix-compst

(defthm exec-unary-of-compustate-fix-compst
  (equal (exec-unary op arg (compustate-fix compst))
         (exec-unary op arg compst)))

Theorem: exec-unary-compustate-equiv-congruence-on-compst

(defthm exec-unary-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-unary op arg compst)
                  (exec-unary op arg compst-equiv)))
  :rule-classes :congruence)