Some changes to a program should not change its result. Adding zero, multiplying by one, or negating a boolean twice should all give you back the original. If the compiler gets a different answer after one of these no-op changes, it has a bug.
Some program transformations should not change the result. Adding zero to a number, multiplying by one, or negating a boolean twice should all produce the original value. If the compiler produces a different result after one of these transforms, something is wrong.
Metamorphic testing applies these semantics-preserving transforms to generated programs and checks that all execution paths still agree on the same result.
The process has four steps:
1. Generate program P
2. Execute P on all paths --> result R
3. Apply a semantics-preserving transform --> P'
4. Execute P' on all paths --> result R'
5. Verify: R == R'
If the original program P already has a mismatch (the paths disagree), VAST saves it as a regular differential testing failure and skips the metamorphic check. Metamorphic testing only applies to programs where all paths agree first.
If P passes but P' produces a different result, that is an equivalence failure: the transform should have been invisible to the compiler, but it was not.
VAST implements seven semantics-preserving transforms:
| Transform | What it does | Invariant |
|---|---|---|
| Add zero | Rewrites x to x + 0 or 0 + x | Adding zero does not change the value |
| Multiply one | Rewrites x to x * 1 or 1 * x | Multiplying by one does not change the value |
| Double negation | Rewrites b to not(not(b)) | Negating a boolean twice returns the original |
| Introduce temp | Extracts an expression into a local variable | Naming a value does not change it |
| Concat empty | Rewrites s to s + "" | Concatenating an empty string does not change the string |
| Empty list length | Rewrites [].length to 0 | An empty list always has length zero |
| Singleton list length | Rewrites [x].length to 1 | A single-element list always has length one |
Each transform targets specific expression types. Add-zero and multiply-one apply to integer expressions. Double-negation applies to boolean expressions. Concat-empty applies to string expressions. The list transforms apply to list literals.
Metamorphic testing catches a different class of bugs than plain differential testing. Differential testing finds cases where the compiler produces wrong output for a program. Metamorphic testing finds cases where the compiler treats equivalent programs differently.
Consider an optimizer that folds x + 0 into x. If the folding is correct, the result should not change. But if the optimizer incorrectly handles 0 + x (commutative case), the add-zero transform will expose it: the original program returns one value, and the transformed version returns another.
| Scenario | What happens | Bug type |
|---|---|---|
Optimizer folds x + 0 correctly but mishandles 0 + x | Transform changes result | Optimizer commutativity bug |
Constant folder evaluates not(not(b)) differently | Transform changes result | Optimizer double-negation bug |
| Introducing a temp variable changes scoping | Transform changes result | Codegen variable scoping bug |
| String concatenation with empty string produces different result | Transform changes result | String handling edge case |
A generated program returns 42:
def __vast_compute() -> Int {
let x = 40
let y = 2
return x + y
}
The add-zero transform rewrites x + y to (x + y) + 0:
def __vast_compute() -> Int {
let x = 40
let y = 2
return (x + y) + 0
}
Both programs should return 42. If the transformed version returns something else, the compiler mishandled the addition of zero.
Metamorphic testing is available via the --metamorphic flag:
vary vast --metamorphic --count 100 --seed 42
VAST generates programs, runs the standard multi-path comparison, then applies each applicable transform and verifies the result stays the same.
In CI deep mode, metamorphic testing runs automatically as part of the nightly verification.
Metamorphic testing complements differential testing and mutation testing:
| Technique | What it checks |
|---|---|
| Differential testing | All paths agree on one program |
| Metamorphic testing | All paths agree on equivalent programs |
| Mutation testing | All paths disagree on non-equivalent programs |