		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist-eval-gl

Equivalent of svexlist-eval intended to work well under GL symbolic execution.

Signature
(svexlist-eval-gl x env symbolic-params) → *
Arguments: x — Svex expressions to evaluate.
Guard (svexlist-p x).; env — Bindings of variables to 4vec values.
Guard (svex-env-p env).; symbolic-params — Alist giving symbolic execution parameters; see below.
Guard (alistp symbolic-params).

This function is provably equivalent to svexlist-eval, but is tailored to perform well under symbolic execution. For symbolic execution, we assume that the inputs to this function other than env are fully concrete, and that env is symbolic only in its values, not its keys or its shape.

The symbolic-params input is logically irrelevant, but allows important optimizations for symbolic execution performance, discussed further below. It is safe (but not necessarily optimal) to call this with symbolic-params equal NIL.

Behavior under Symbolic Execution

Applies rewriting to the supplied svex expressions, if :SIMPLIFY is bound to a non-nil value in the symbolic-params input -- see svexlist-rewrite-fixpoint.
If :boolmasks is bound in the symbolic-params, compares the given env with the bound value, which should be an alist. If there is a pair (name . mask) in the boolmasks alist for which the binding for name in env is not Boolean-valued on the bits set to 1 in mask, then fail out of symbolic simulation. (In AIG mode, the masked bits must be syntactically Boolean-valued -- practically speaking, this means the upper/lower parts should result from the same computation.)
If :VARS is bound in symbolic-params, it should be bound to a list of input variables of the SVTV. Unions this list with the variables bound in env to obtain the full list of variables to bind as inputs to the SVTV. Or if :ALLVARS is bound in symbolic params, all the variables in the svex expressions are used instead.
Compiles the svex list x into a4vec objects, a symbolic analogue of 4vec but with each bit an AIG -- see svexlist->a4vecs-for-varlist. This computation uses the assumptions, checked in the two steps above, that only the variables in vars are non-X, and that the masked bits in boolmasks are Boolean-valued. These assumptions can reduce the complexity of the generated AIGs. (Note everything used in this computation is concrete -- the env isn't involved.)
Creates an alist binding the AIG variables used in the above step to the appropriate symbolic bits from env.
Symbolically evaluates each of the a4vec objects from step 4 under the bindings from step 5 using GL's symbolic simulator of aig-eval. This results in GL-native symbolic 4vec objects, which is the result we want.

Optimization using the Extra Arguments

Performance of symbolic execution (and SAT solving, when in AIG mode) is related to the size of the AIGs produced by the svex to AIG transformation (step 4, above). Two ways to decrease that size are (1) to turn certain variables into constant Xes, if it is known that they're irrelevant, and (2) to assume certain bits of some variables are Boolean-valued, which means it can be represented by just one AIG variable rather than two.

Another performance consideration is that the transformation to AIGs is itself sometimes significant. Especially for theorems proved by case-splitting, it is important not to need to repeat this transformation for each case. The function that does the transformation is memoized, but it is important in this case that it always be called with the same arguments.

The vars list pertains to optimization (1): if not present in the list, a variable in the svex expressions will just be replaced with an X. Therefore, in general it's best to use exactly the set of variables bound in the environment. However, it may not be worth it to redo the AIG conversion each time the environment's bound variables changes, so we take vars separately.

The boolmasks allows optimization (2). It is best for symbolic execution performance to bind every variable in vars to -1, but this may fail if the env is not constructed in such a way that the values are obviously 2-vectors.

Definitions and Theorems

Function: svexlist-eval-gl

(defun svexlist-eval-gl (x env symbolic-params)
 (declare (xargs :guard (and (svexlist-p x)
                             (svex-env-p env)
                             (alistp symbolic-params))))
 (let ((__function__ 'svexlist-eval-gl))
  (declare (ignorable __function__))
  (b*
   ((env (make-fast-alist (svex-env-fix env)))
    (svars (svexlist-vars-for-symbolic-eval x env symbolic-params))
    (x (svexlist-x-out-unused-vars
            x svars
            (symbolic-params-x-out-cond symbolic-params)))
    (x (maybe-svexlist-rewrite-fixpoint
            x
            (cdr (assoc :simplify symbolic-params))))
    (boolmasks
     (make-fast-alist
      (hons-copy
         (ec-call (svar-boolmasks-fix
                       (cdr (assoc :boolmasks symbolic-params)))))))
    ((unless (svex-env-check-boolmasks boolmasks env))
     (b*
      ((?ign
           (cw "ERROR: some bits assumed to be Boolean were not~%"))
       (?ign (gl::gl-error 'boolcheck-failed)))
      (gl::gl-hide (svexlist-eval x env))))
    ((mv err a4vecs)
     (time$ (svexlist->a4vecs-for-varlist x svars boolmasks)
            :msg "; svex->aigs: ~st sec, ~sa bytes.~%"))
    ((when err)
     (b* ((?ign (cw "ERROR gathering AIG bits for variables: ~@0~%"
                    err))
          (?ign (gl::gl-error 'a4env-failed)))
       (gl::gl-hide (svexlist-eval x env))))
    ((mv ?err aig-env)
     (time$
         (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env)
         :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (?ign (fast-alist-free env))
    (aig-env (make-fast-alist aig-env))
    (ans (a4veclist-eval a4vecs aig-env)))
   (fast-alist-free aig-env)
   ans)))

Theorem: svexlist-eval-gl-is-svexlist-eval

(defthm svexlist-eval-gl-is-svexlist-eval
  (equal (svexlist-eval-gl x env symbolic-params)
         (svexlist-eval x env)))

Theorem: svexlist-eval-for-symbolic-redef

(defthm svexlist-eval-for-symbolic-redef
  (equal (svexlist-eval-for-symbolic x env symbolic-params)
         (svexlist-eval-gl x env symbolic-params)))

Theorem: svexlist-eval-gl-of-svexlist-fix-x

(defthm svexlist-eval-gl-of-svexlist-fix-x
  (equal (svexlist-eval-gl (svexlist-fix x)
                           env symbolic-params)
         (svexlist-eval-gl x env symbolic-params)))

Theorem: svexlist-eval-gl-svexlist-equiv-congruence-on-x

(defthm svexlist-eval-gl-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-eval-gl x env symbolic-params)
                  (svexlist-eval-gl x-equiv env symbolic-params)))
  :rule-classes :congruence)

Theorem: svexlist-eval-gl-of-svex-env-fix-env

(defthm svexlist-eval-gl-of-svex-env-fix-env
  (equal (svexlist-eval-gl x (svex-env-fix env)
                           symbolic-params)
         (svexlist-eval-gl x env symbolic-params)))

Theorem: svexlist-eval-gl-svex-env-equiv-congruence-on-env

(defthm svexlist-eval-gl-svex-env-equiv-congruence-on-env
  (implies (svex-env-equiv env env-equiv)
           (equal (svexlist-eval-gl x env symbolic-params)
                  (svexlist-eval-gl x env-equiv symbolic-params)))
  :rule-classes :congruence)