Sign Up
Log In
Log In
or
Sign Up
Places
All Projects
Status Monitor
Collapse sidebar
home:Ledest:erlang:25
erlang
2522-compiler-Document-SSA-checker.patch
Overview
Repositories
Revisions
Requests
Users
Attributes
Meta
File 2522-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
Locations
Projects
Search
Status Monitor
Help
OpenBuildService.org
Documentation
API Documentation
Code of Conduct
Contact
Support
@OBShq
Terms
openSUSE Build Service is sponsored by
The Open Build Service is an
openSUSE project
.
Sign Up
Log In
Places
Places
All Projects
Status Monitor
