		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-bitand

Implements svex-argmasks for BITAND.

Signature
(svmask-for-bitand mask args) → argmasks
Arguments: mask — Care mask for the full expression.
Guard (4vmask-p mask).; args — Arguments to this BITAND operator.
Guard (svexlist-p args).
Returns: argmasks — The new care masks inferred for the args.
Type (4vmasklist-p argmasks).

We are considering a (bitand x y) expression and we know that we only care about the bits mentioned in mask. We want to figure out which bits of X and Y we care about. As a starting point, since bitwise AND operates in a bit-by-bit fashion, we certainly don't care about any bits that are don't cares in our outer mask. But we can do better than that.

For any particular bit of x, if we can tell that the corresponding bit of y is zero, then we know that the resulting bit from the AND is going to be 0, so this bit of X doesn't matter. The basic idea here, then, is to improve mask for x by taking away any bits of y that we can tell are zero. Symmetrically, we can take improve mask for y by taking away any bits of x that are known to be zero.

Well, almost. What if we know that bit 4 of x is zero AND that bit 4 of y is zero. We can't just mark bit 4 as a don't care in both arguments, because we need to keep at least one zero or the other. This leads to a certain kind of asymmetry, and leaves us with some choice regarding which argument we want to mask more aggressively.

We don't currently try very hard to make any kind of sensible choice here. Instead, as a rather arbitrary default, we normally mask y more aggressively than x. However, as a special exception, if y is entirely constant under the outer mask, then we will mask x more aggressively.

Definitions and Theorems

Function: svmask-for-bitand

(defun svmask-for-bitand (mask args)
 (declare (xargs :guard (and (4vmask-p mask)
                             (svexlist-p args))))
 (let ((__function__ 'svmask-for-bitand))
  (declare (ignorable __function__))
  (b* (((svex-nths x y) args)
       (mask (4vmask-fix mask)))
    (b*
     (((s4vec xval) (svex-s4xeval x))
      ((s4vec yval) (svex-s4xeval y))
      (x-zero (sparseint-bitnor xval.upper xval.lower))
      (y-zero (sparseint-bitnor yval.upper yval.lower))
      (shared-zeros
           (sparseint-bitand x-zero (sparseint-bitand y-zero mask)))
      (xm-nonzero (sparseint-bitandc2 mask x-zero))
      (ym-nonzero (sparseint-bitandc2 mask y-zero))
      ((when (sparseint-equal 0 shared-zeros))
       (list ym-nonzero xm-nonzero))
      (y-x (sparseint-bitandc2 yval.upper yval.lower))
      (ym-x (sparseint-test-bitand mask y-x))
      ((unless ym-x)
       (list ym-nonzero
             (sparseint-bitor xm-nonzero shared-zeros))))
     (list (sparseint-bitor ym-nonzero shared-zeros)
           xm-nonzero)))))

Theorem: 4vmasklist-p-of-svmask-for-bitand

(defthm 4vmasklist-p-of-svmask-for-bitand
  (b* ((argmasks (svmask-for-bitand mask args)))
    (4vmasklist-p argmasks))
  :rule-classes :rewrite)

Theorem: svmask-for-bitand-of-4vmask-fix-mask

(defthm svmask-for-bitand-of-4vmask-fix-mask
  (equal (svmask-for-bitand (4vmask-fix mask)
                            args)
         (svmask-for-bitand mask args)))

Theorem: svmask-for-bitand-4vmask-equiv-congruence-on-mask

(defthm svmask-for-bitand-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (svmask-for-bitand mask args)
                  (svmask-for-bitand mask-equiv args)))
  :rule-classes :congruence)

Theorem: svmask-for-bitand-of-svexlist-fix-args

(defthm svmask-for-bitand-of-svexlist-fix-args
  (equal (svmask-for-bitand mask (svexlist-fix args))
         (svmask-for-bitand mask args)))

Theorem: svmask-for-bitand-svexlist-equiv-congruence-on-args

(defthm svmask-for-bitand-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svmask-for-bitand mask args)
                  (svmask-for-bitand mask args-equiv)))
  :rule-classes :congruence)

Theorem: svmask-for-bitand-correct

(defthm svmask-for-bitand-correct
 (implies
    (and (equal (4veclist-mask (svmask-for-bitand mask args)
                               (svexlist-eval args env))
                (4veclist-mask (svmask-for-bitand mask args)
                               args1))
         (syntaxp (not (equal args1
                              (cons 'svexlist-eval
                                    (cons args (cons env 'nil)))))))
    (equal (4vec-mask mask (svex-apply 'bitand args1))
           (4vec-mask mask
                      (svex-apply 'bitand
                                  (svexlist-eval args env))))))