# 4vmask

Bitmasks indicating the relevant bits of SVEX expressions.

A **4vmask** is a data structure that records which bits of an
expression we care about.

We represent 4vmasks as ordinary integers, which we treat as bit masks where
1s encode the relevant bit positions and 0s encode the irrelevant positions.
However, rather than directly using the integerp type, we treat 4vmasks
as a new, custom type, with its own recognizer, fixing function, etc. This
gives us a semantically nicer fixing behavior where the default mask is -1,
i.e., by default all bits are relevant.

4vmasks are intended to support rewriting and other applications,
e.g., composing update functions to reach a fixpoint. In these contexts,
knowing that certain bits of an svex expression are irrelevant can allow
for additional simplifications. For instance, in an expression like:

(zerox 4 (bitand <a> <b>))

we can see that only the bottom four bits of <a> and <b> matter,
because the zero extension will discard anything above four bits. By taking
advantage of this information, we may be able to simplify <a> or <b>
in ways that are would otherwise not be sound. For instance, if <a> is an
expression such as:

(concat 4 <low> <high>)

Then we can simply rewrite it to <low> and get rid of <high>
altogether. Typically we make these sorts of inferences using svex-argmasks.

### Subtopics

- Svex-argmasks
- Statically compute the care masks for a function's arguments,
starting from the care mask for the result of the function application.
- 4vmask-p
- Recognizer for 4vmasks.
- 4vmask-subsumes
`(4vmask-subsumes x y)` checks whether the 4vmask x cares
about strictly more bits than y cares about.- 4veclist-mask
- Reduce a list of constant 4vecs using individual 4vmasks; any irrelevant bits become Xes.
- 4vec-mask-to-zero
- Reduce a constant 4vec using a 4vmask; any irrelevant
bits become 0s.
- 4vec-mask
- Reduce a constant 4vec using a 4vmask; any irrelevant
bits become Xes.
- 4vmasklist-subsumes
`(4vmasklist-subsumes x y)` checks whether the masks in the list
x all subsume the corresponding masks in y, in the sense of 4vmask-subsumes.- 4vmask-union
`(4vmask-union x y)` unions the 4vmasks x and y,
creating a new mask that includes all bits that are relevant for in either
x or y.- 4vec-mask?
- 4vmask-equiv
- Equivalence up to 4vmask-fix.
- 4vmask-fix
- Fixing function for 4vmasks.
- 4vmask-alist
- An alist mapping svar-p to 4vmask-p.
- 4veclist-mask?
- 4vmasklist
- A list of 4vmask-p objects.
- 4vmask-empty
`(4vmask-empty x)` recognizes the empty 4vmask.