File 3522-compiler-Document-SSA-checker.patch of Package erlang
From 8c058d16eed765b8161d2099fa3b11f640061b59 Mon Sep 17 00:00:00 2001
From: Frej Drejhammar <frej.drejhammar@gmail.com>
Date: Wed, 18 Jan 2023 10:49:41 +0100
Subject: [PATCH 12/13] compiler: Document SSA checker
Provide internal documentation for the SSA checker.
---
lib/compiler/doc/src/Makefile | 2 +-
lib/compiler/doc/src/internal.xml | 3 +-
lib/compiler/internal_doc/ssa_checks.md | 124 ++++++++++++++++++++++++
3 files changed, 127 insertions(+), 2 deletions(-)
create mode 100644 lib/compiler/internal_doc/ssa_checks.md
diff --git a/lib/compiler/doc/src/Makefile b/lib/compiler/doc/src/Makefile
index 801e1adfac..7d5abca9dd 100644
--- a/lib/compiler/doc/src/Makefile
+++ b/lib/compiler/doc/src/Makefile
@@ -36,7 +36,7 @@ EDOC_REF3_FILES = cerl.xml cerl_trees.xml cerl_clauses.xml
XML_PART_FILES = internal.xml
XML_NOTES_FILES = notes.xml
-XML_INTERNAL_FILES = beam_ssa.xml
+XML_INTERNAL_FILES = beam_ssa.xml ssa_checks.xml
XML_GEN_FILES = $(XML_INTERNAL_FILES:%=$(XMLDIR)/%)
diff --git a/lib/compiler/doc/src/internal.xml b/lib/compiler/doc/src/internal.xml
index be2cf75356..57b2231218 100644
--- a/lib/compiler/doc/src/internal.xml
+++ b/lib/compiler/doc/src/internal.xml
@@ -4,7 +4,7 @@
<internal xmlns:xi="http://www.w3.org/2001/XInclude">
<header>
<copyright>
- <year>2018</year><year>2021</year>
+ <year>2018</year><year>2023</year>
<holder>Ericsson AB. All Rights Reserved.</holder>
</copyright>
<legalnotice>
@@ -35,5 +35,6 @@
<xi:include href="cerl_trees.xml"/>
<xi:include href="cerl_clauses.xml"/>
<xi:include href="beam_ssa.xml"/>
+ <xi:include href="ssa_checks.xml"/>
</internal>
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.
--
2.35.3
