		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-eval-impure-binop-expr

Propogate a constant through an impure c$::binop.

Signature
(const-prop-eval-impure-binop-expr binop left right env) → (mv value? env)
Arguments: binop — Guard (binopp binop).; left — Guard (exprp left).; right — Guard (c::valuep right).; env — Guard (envp env).
Returns: value? — Type (c::value-optionp value?).; env — Type (envp env).

If the lvalue cannot be resolved, the environment is nullified, as we cannot be sure what has been mutated. For instance, consider the following sequence of statements:

int a = 1;
int b = 4;
*x = 0;
int c = a + b;

Without knowing the value of x, we cannot constant fold the initializer of c. For instance, the constraints x == &a, x == &b, and x != &a && x != &b would all produce different results.

Definitions and Theorems

Function: const-prop-eval-impure-binop-expr

(defun const-prop-eval-impure-binop-expr (binop left right env)
 (declare (xargs :guard (and (binopp binop)
                             (exprp left)
                             (c::valuep right)
                             (envp env))))
 (declare (xargs :guard (not (pure-binopp binop))))
 (let ((__function__ 'const-prop-eval-impure-binop-expr))
  (declare (ignorable __function__))
  (b* ((env (env-fix env))
       (right (c::value-fix right)))
    (binop-case binop :asg
                (b* ((ident? (expr-to-ident left)))
                  (if ident? (mv right (write-env ident? right env))
                    (mv nil nil)))
                :otherwise (mv nil nil)))))

Theorem: value-optionp-of-const-prop-eval-impure-binop-expr.value?

(defthm value-optionp-of-const-prop-eval-impure-binop-expr.value?
  (b* (((mv ?value? ?env)
        (const-prop-eval-impure-binop-expr binop left right env)))
    (c::value-optionp value?))
  :rule-classes :rewrite)

Theorem: envp-of-const-prop-eval-impure-binop-expr.env

(defthm envp-of-const-prop-eval-impure-binop-expr.env
  (b* (((mv ?value? ?env)
        (const-prop-eval-impure-binop-expr binop left right env)))
    (envp env))
  :rule-classes :rewrite)