2 BEAM SSA Checks

While developing optimizations operating on the BEAM SSA it is often hard to check that various transforms have the intended effect. For example, unless a transform produces crashing code, it is hard to detect that the transform is broken. Likewise missing an optimization opportunity is also hard to detect.

To simplify the creation of tests on BEAM SSA the compiler has an internal mode in which it parses and checks assertions on the structure and content of the produced BEAM SSA code. This is a short introduction to the syntax and semantics of the SSA checker functionality.

2.1 Syntax

SSA checks are embedded in the source code as comments starting with with one of %ssa%, %%ssa% or %%%ssa%. This is a short introduction the syntax, for the full syntax please refer to the ssa_check_when_clause production in erl_parse.yrl.

SSA checks can be placed inside any Erlang function, for example:

t0() ->
%ssa% () when post_ssa_opt ->
%ssa%   ret(#{}).
  #{}.

will check that t0/0 returns the literal #{}. If we want to check that a function returns its first formal parameter, we can write:

t1(A, _B) ->
%ssa% (X, _) when post_ssa_opt ->
%ssa%   ret(X).
  A.

Note how we match the first formal parameter using X. The reason for having our own formal parameters for the SSA check, is that we don't want to introduce new identifiers at the Erlang level to support SSA-level checks. Consider if t1/2 had been defined as t1([A|As], B) we would have had to introduce a new identifier for the aggregate value [A|As].

The full syntax for a SSA check clause is:

<expected-result>? (<formals>) when <pipeline-location> -> <checks> '.'

where <expected-result> can be one of pass (the check must succeed), fail and xfail (the check must fail). Omitting <expected-result> is parsed as an implicit pass.

<formals> is a comma-separated list of variables.

<pipeline-location> specifies when in the compiler pipeline to run the checks. For now the only supported value for <pipeline-location> is post_ssa_opt which runs the checks after the ssa_opt pass.

<checks> is a comma-separated list of matches against the BEAM SSA code. For non-flow-control operations the syntax is:

<variable> = <operation> ( <arguments> ) <annotation>?

where <operation> is the #b_set.op field from the internal SSA representation. BIFs are written as bif:<atom>.

<arguments> is a comma-separated list of variables or literals.

For flow control operations and labels, the syntax is as follows:

br(<bool>, <true-label>, <false-label>)

switch(<value>, <fail-label>, [{<label>,<value>},...])

ret(<value>)

label <value>

where <value> is a literal or a variable.

A check can also include an assertion on operation annotations. The assertion is written as a map-like pattern following the argument list, for example:

t0() ->
%ssa% () when post_ssa_opt ->
%ssa% _ = call(fun return_int/0) { result_type => {t_integer,{17,17}},
%ssa%                              location => {_,32} },
%ssa% _ = call(fun return_tuple/0) {
%ssa%    result_type => {t_tuple,2,true,#{1 => {t_integer,{1,1}},
%ssa%                                     2 => {t_integer,{2,2}}}}
%ssa% }.
    X = return_int(),
    Y = return_tuple(),
    {X, Y}.

2.2 Semantics

When an SSA assertion is matched against the BEAM SSA for a function, patterns are applied sequentially. If the current pattern doesn't match, the checker tries with the next instruction. If the checker reaches the end of the SSA representation without having matched all patterns, the check is considered failed otherwise the assertion is considered successful. When a pattern is matched against an SSA operation, the values of variables already bound are considered and if the patterns matches, free variables introduced in the successfully matched pattern are bound to the values they have in the matched operation.

2.3 Compiler integration

The BEAM SSA checker is enabled by the compiler option {check_ssa,post_ssa_opt}. When enabled, a failed SSA assertion will be reported using the same mechanisms as an ordinary compilation error.

2.4 Limitations

Unbound variables are not allowed in the key-part of map literals nor in annotation assertions.