Svex-argmasks
Statically compute the care masks for a function's arguments,
starting from the care mask for the result of the function application.
- Signature
(svex-argmasks mask fn args) → argmasks
- Arguments
- mask — Outer care mask, i.e., the care mask for the whole expression
fn(args).
Guard (4vmask-p mask).
- fn — The function being applied.
Guard (fnsym-p fn).
- args — The arguments that fn is being applied to, whose care masks we
want to determine.
Guard (svexlist-p args).
- Returns
- argmasks — Care masks to use for the arguments.
Type (and (4vmasklist-p argmasks) (equal (len argmasks) (len args))).
This function understands the SVEX functions and which bits
of their arguments are sure to influence which bits of their outputs. For
example, if we are given a function like:
(bitsel 4 <bigexpr>)
and if the initial, outer 4vmask for the whole expression is -1,
i.e., we care about all of the bits of the result, then we will produce two new
masks, one for each of the function's arguments:
- For 4, we will just care about all the bits, i.e., our mask will be
-1. This expression is already a constant anyway so there isn't much hope
of simplifying it further and it poses no problems in computations such as
reaching a compositional fixpoint.
- For <bigexpr>, since we are selecting bit 4, we obviously only care
about the fourth bit. Accordingly, the resulting care mask will be
#b1000. Knowing that we only care about the fourth bit of <bigexpr>
may allow us to make important simplifications to it, and may also allow us to
generate better (more restrictive) care masks for its subexpressions.
In this way, care mask information can flow downward, starting from the
outside of the expression and into the arguments.
Definitions and Theorems
Function: svex-argmasks
(defun svex-argmasks (mask fn args)
(declare (xargs :guard (and (4vmask-p mask)
(fnsym-p fn)
(svexlist-p args))))
(let ((__function__ 'svex-argmasks))
(declare (ignorable __function__))
(if (4vmask-empty mask)
(replicate (len args) 0)
(4vmasklist-len-fix
(len args)
(svex-argmasks-cases (mbe :logic (fnsym-fix fn)
:exec fn))))))
Theorem: return-type-of-svex-argmasks
(defthm return-type-of-svex-argmasks
(b* ((argmasks (svex-argmasks mask fn args)))
(and (4vmasklist-p argmasks)
(equal (len argmasks) (len args))))
:rule-classes :rewrite)
Theorem: svex-argmasks-correct
(defthm svex-argmasks-correct
(implies
(and (equal (4veclist-mask (svex-argmasks mask fn args)
(svexlist-eval args env))
(4veclist-mask (svex-argmasks mask fn args)
args1))
(syntaxp (not (equal args1
(cons 'svexlist-eval
(cons args (cons env 'nil)))))))
(equal (4vec-mask mask (svex-apply fn args1))
(4vec-mask mask
(svex-apply fn (svexlist-eval args env))))))
Theorem: svex-argmasks-correct2
(defthm svex-argmasks-correct2
(implies
(and (equal (4veclist-mask (svex-argmasks mask fn args)
args1)
(4veclist-mask (svex-argmasks mask fn args)
(svexlist-eval args env)))
(syntaxp (not (equal args1
(cons 'svexlist-eval
(cons args (cons env 'nil)))))))
(equal (4vec-mask mask (svex-apply fn args1))
(4vec-mask mask
(svex-apply fn (svexlist-eval args env))))))
Theorem: svex-argmasks-of-4vmask-fix-mask
(defthm svex-argmasks-of-4vmask-fix-mask
(equal (svex-argmasks (4vmask-fix mask)
fn args)
(svex-argmasks mask fn args)))
Theorem: svex-argmasks-4vmask-equiv-congruence-on-mask
(defthm svex-argmasks-4vmask-equiv-congruence-on-mask
(implies (4vmask-equiv mask mask-equiv)
(equal (svex-argmasks mask fn args)
(svex-argmasks mask-equiv fn args)))
:rule-classes :congruence)
Theorem: svex-argmasks-of-fnsym-fix-fn
(defthm svex-argmasks-of-fnsym-fix-fn
(equal (svex-argmasks mask (fnsym-fix fn) args)
(svex-argmasks mask fn args)))
Theorem: svex-argmasks-fnsym-equiv-congruence-on-fn
(defthm svex-argmasks-fnsym-equiv-congruence-on-fn
(implies (fnsym-equiv fn fn-equiv)
(equal (svex-argmasks mask fn args)
(svex-argmasks mask fn-equiv args)))
:rule-classes :congruence)
Theorem: svex-argmasks-of-svexlist-fix-args
(defthm svex-argmasks-of-svexlist-fix-args
(equal (svex-argmasks mask fn (svexlist-fix args))
(svex-argmasks mask fn args)))
Theorem: svex-argmasks-svexlist-equiv-congruence-on-args
(defthm svex-argmasks-svexlist-equiv-congruence-on-args
(implies (svexlist-equiv args args-equiv)
(equal (svex-argmasks mask fn args)
(svex-argmasks mask fn args-equiv)))
:rule-classes :congruence)
Theorem: svex-argmasks-of-none
(defthm svex-argmasks-of-none
(implies (4vmask-empty mask)
(equal (svex-argmasks mask fn args)
(replicate (len args) 0))))
Theorem: 4veclist-mask-idempotent
(defthm 4veclist-mask-idempotent
(equal (4veclist-mask masks (4veclist-mask masks x))
(4veclist-mask masks x)))
Theorem: svex-argmasks-remove-mask
(defthm svex-argmasks-remove-mask
(equal
(4vec-mask mask
(svex-apply fn
(4veclist-mask (svex-argmasks mask fn args)
(svexlist-eval args env))))
(4vec-mask mask
(svex-apply fn (svexlist-eval args env)))))
Subtopics
- Svmask-for-bitand
- Implements svex-argmasks for BITAND.
- Svmask-for-signx
- Implements svex-argmasks for SIGNX.
- Svmask-for-bitxor
- Implements svex-argmasks for BITXOR.
- Svmask-for-concat
- Implements svex-argmasks for CONCAT.
- Svmask-for-bit?!
- Implements svex-argmasks for BIT?!.
- Svmask-for-bit?
- Implements svex-argmasks for BIT?.
- Svmask-for-?!
- Implements svex-argmasks for ?!.
- Svmask-for-?
- Implements svex-argmasks for ?.
- Svmask-for-?*
- Implements svex-argmasks for ?*.
- Svmask-for-==??
- Implements svex-argmasks for ==??.
- Svmask-for-rsh
- Implements svex-argmasks for RSH.
- Svmask-for-bitsel
- Implements svex-argmasks for BITSEL.
- Svmask-for-+
- Implements svex-argmasks for +.
- Svmask-for-override
- Implements svex-argmasks for OVERRIDE.
- Svmask-for-uand
- Implements svex-argmasks for UAND.
- Svmask-for-zerox
- Implements svex-argmasks for ZEROX.
- Svmask-for-safer-==?
- Implements svex-argmasks for SAFER-==?.
- Svmask-for-bitor
- Implements svex-argmasks for BITOR.
- Svmask-for-partinst
- Implements svex-argmasks for PARTINST.
- 4vmasklist-len-fix
- Svmask-for-==?
- Implements svex-argmasks for ==?.
- Svmask-for-xdet
- Implements svex-argmasks for XDET.
- Svmask-for-unfloat
- Implements svex-argmasks for UNFLOAT.
- 4vmask-all-or-none
- Care mask for an argument that matters fully, unless we don't care
about any bits at all.
- Svmask-for-partsel
- Implements svex-argmasks for PARTSEL.
- Svmask-for-offp
- Implements svex-argmasks for OFFP.
- Svmask-for-bitnot
- Implements svex-argmasks for BITNOT.
- Svmask-for-===*
- Implements svex-argmasks for ===*.
- Svmask-for-===
- Implements svex-argmasks for ===.
- Svmask-for-res
- Implements svex-argmasks for RES.
- Svmask-for-onp
- Implements svex-argmasks for ONP.
- Svmask-for-blkrev
- Implements svex-argmasks for BLKREV.
- Svmask-for-resor
- Implements svex-argmasks for RESOR.
- Svmask-for-resand
- Implements svex-argmasks for RESAND.
- Svmask-for-pow
- Implements svex-argmasks for POW.
- Svmask-for-onehot0
- Implements svex-argmasks for ONEHOT0.
- Svmask-for-onehot
- Implements svex-argmasks for ONEHOT.
- Svmask-for-lsh
- Implements svex-argmasks for LSH.
- Svmask-for-id
- Implements svex-argmasks for ID.
- Svmask-for-countones
- Implements svex-argmasks for COUNTONES.
- Svmask-for-clog2
- Implements svex-argmasks for CLOG2.
- Svmask-for-/
- Implements svex-argmasks for /.
- Svmask-for-==
- Implements svex-argmasks for ==.
- Svmask-for-<
- Implements svex-argmasks for <.
- Svmask-for-*
- Implements svex-argmasks for *.
- Svmask-for-%
- Implements svex-argmasks for %.
- Svmask-for-uxor
- Implements svex-argmasks for UXOR.
- Svmask-for-uor
- Implements svex-argmasks for UOR.
- Svmask-for-u-
- Implements svex-argmasks for U-.
- Svmask-for-b-
- Implements svex-argmasks for B-.
- Unrev-block-index
- Svmask-for-unknown-function
- Sparseint-unrev-blocks
