		Search-engine friendly clone of the ACL2 documentation.

Svex-argmasks

Svmask-for-signx

Implements svex-argmasks for SIGNX.

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

We are considering a (signx n x) expression and we know that we only care about the bits mentioned in mask. We need to figure out which bits of n and x we care about.

For n. If we care about ANY bit of (signx n x), then we care about all of n. But if we don't care about any bit of (signx n x), then n is completely irrelevant.

For x. The result of (signx n x) is just the low n bits of x, with the nth bit being sign extended to infinity.

If we statically determine that n is negative, then we don't care about x at all because 4vec-sign-ext will just return all Xes no matter what it is.

If we statically determine that n is positive, then:

the bits below n only matter if they are marked as care bits in the outer mask;
bit n will only matter when bit n or any greater bit, is marked as a care bit in the outer mask.

If we can't statically determine n, we may still be able to do something based on the outer mask. For instance, if mask is #b1000, then we know that we don't care about any bits above bit 4. However, we might depend on any of the bits below 4, because we might be sign extending any one of them.

BOZO for now we don't exploit this and simply say that we depend on all of x. In the future, it would be good to integrate something like mask-for-generic-signx here.

Definitions and Theorems

Function: svmask-for-signx

(defun svmask-for-signx (mask args)
  (declare (xargs :guard (and (4vmask-p mask)
                              (svexlist-p args))))
  (let ((__function__ 'svmask-for-signx))
    (declare (ignorable __function__))
    (b* (((svex-nths n x) args)
         (mask (4vmask-fix mask)))
      (b* (((when (sparseint-equal mask 0))
            (list 0 0))
           (nval (svex-s4xeval n))
           ((unless (s4vec-2vec-p nval))
            (list -1 (mask-for-generic-signx mask)))
           (nv (s4vec->upper nval))
           ((when (sparseint-< nv 0)) (list -1 0))
           (xmask (mask-for-fixed-signx mask (sparseint-val nv))))
        (list -1 xmask)))))

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

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

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

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

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

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

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

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

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

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

Theorem: svmask-for-signx-correct

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

Subtopics

Mask-for-generic-signx
Mask-for-fixed-signx