1 files changed, 124 insertions, 0 deletions
diff --git a/lib/compiler/internal_doc/ssa_checks.md b/lib/compiler/internal_doc/ssa_checks.md
new file mode 100644
index 0000000000..f4c68e3939
--- /dev/null
+++ b/lib/compiler/internal_doc/ssa_checks.md
@@ -0,0 +1,124 @@
+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.
+
+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}.
+
+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.
+
+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.
+
+Limitations
+-----------
+
+* Unbound variables are not allowed in the key-part of map literals nor
+in annotation assertions.