-
Notifications
You must be signed in to change notification settings - Fork 0
/
paper.tex
8777 lines (8420 loc) · 415 KB
/
paper.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
%% Commands for TeXCount
%TC:macro \cite [option:text,text]
%TC:macro \citep [option:text,text]
%TC:macro \citet [option:text,text]
%TC:envir table 0 1
%TC:envir table* 0 1
%TC:envir tabular [ignore] word
%TC:envir displaymath 0 word
%TC:envir math 0 word
%TC:envir comment 0 0
\documentclass[acmsmall,screen,review]{acmart}
\usepackage{syntax}
\renewcommand{\syntleft}{\normalfont\itshape}
\renewcommand{\syntright}{\normalfont\itshape}
\usepackage{prftree}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{caption}
\usepackage{subcaption}
\usepackage{fancyvrb}
\usepackage{enumitem}
\usepackage{string-diagrams}
\usepackage{cancel}
\usepackage{thmtools}
\usetikzlibrary{calc}
\definecolor{codegreen}{rgb}{0,0.6,0}
\definecolor{codegray}{rgb}{0.5,0.5,0.5}
\definecolor{codepurple}{rgb}{0.58,0,0.82}
\definecolor{backcolour}{rgb}{0.95,0.95,0.92}
\lstdefinestyle{mystyle}{
% backgroundcolor=\color{backcolour},
commentstyle=\color{codegreen},
keywordstyle=\color{magenta},
numberstyle=\tiny\color{codegray},
stringstyle=\color{codepurple},
basicstyle=\ttfamily\footnotesize,
breakatwhitespace=false,
breaklines=true,
captionpos=b,
keepspaces=true,
numbers=left,
numbersep=5pt,
showspaces=false,
showstringspaces=false,
showtabs=false,
tabsize=2
}
\lstset{style=mystyle}
\newcounter{todos}
\newcommand{\TODO}[1]{{
\stepcounter{todos}
\begin{center}\large{\textcolor{red}{\textbf{TODO \arabic{todos}:} #1}}\end{center}
}}
\newcommand{\todo}[1]{\stepcounter{todos} \textcolor{red}{\textbf{TODO \arabic{todos}}: #1}}
% Math fonts
\newcommand{\mc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\mb}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}
% Math
\newcommand{\nats}{\mathbb{N}}
% Syntax atoms
\newcommand{\lbl}[1]{{`#1}}
\newcommand{\lto}{:}
\newcommand{\linl}[1]{\iota_l\;{#1}}
\newcommand{\linr}[1]{\iota_r\;{#1}}
\newcommand{\labort}[1]{\ms{abort}\;{#1}}
% Syntax
\newcommand{\letexpr}[3]{\ensuremath{\ms{let}\;#1 = #2;\;#3}}
\newcommand{\caseexpr}[5]{\ms{case}\;#1\;\{\linl{#2} \lto #3, \linr{#4} \lto #5\}}
\newcommand{\letstmt}[3]{\ensuremath{\ms{let}\;#1 = #2; #3}}
\newcommand{\brb}[2]{\ms{br}\;#1\;#2}
\newcommand{\ite}[3]{\ms{if}\;#1\;\{#2\}\;\ms{else}\;\{#3\}}
\newcommand{\casestmt}[5]{\ms{case}\;#1\;\{\linl{#2} \lto #3, \linr{#4} \lto #5\}}
\newcommand{\where}[2]{#1\;\ms{where}\;#2}
\newcommand{\wbranch}[3]{#1(#2) \lto \{#3\}}
\newcommand{\cfgsubst}[1]{\ms{cfgs}\;\{#1\}}
\newcommand{\wseq}[2]{{#1} \mathbin{{;}{;}} {#2}}
\newcommand{\rupg}[1]{{#1}^\upharpoonright}
\newcommand{\lupg}[1]{{#1}^\upharpoonleft}
% Judgements
\newcommand{\cwk}[2]{#1 \mapsto #2}
\newcommand{\lwk}[2]{#1 \rightsquigarrow #2}
\newcommand{\thyp}[3]{#1 : {#2}^{#3}}
\newcommand{\bhyp}[2]{#1 : #2}
\newcommand{\lhyp}[2]{#1(#2)}
\newcommand{\rle}[1]{{\scriptsize\textsf{#1}}}
\newcommand{\hasty}[4]{#1 \vdash_{#2} #3: {#4}}
\newcommand{\haslb}[3]{#1 \vdash #2 \rhd #3}
\newcommand{\ahasty}[4]{#1 \vdash_{#2}^{\ms{anf}} #3 : {#4}}
\newcommand{\thaslb}[3]{#1 \vdash^{\ms{t}}_{\ms{ssa}} #2 \rhd #3}
\newcommand{\ahaslb}[3]{#1 \vdash^{\ms{anf}} #2 \rhd #3}
\newcommand{\bhaslb}[3]{#1 \vdash^{\ms{b}}_{\ms{ssa}} #2 \rhd #3}
% \newcommand{\chaslb}[3]{#1 \vdash^{\ms{c}}_{\ms{ssa}} #2 \rhd #3}
\newcommand{\shaslb}[3]{#1 \vdash^{\ms{s}} #2 \rhd #3}
\newcommand{\isop}[4]{#1 \in \mc{I}_{#4}(#2, #3)}
\newcommand{\issubst}[3]{#1: #2 \mapsto #3}
\newcommand{\lbsubst}[4]{#1 \vdash #2: #3 \rightsquigarrow #4}
\newcommand{\teqv}{\approx}
\newcommand{\tmeq}[5]{#1 \vdash_{#2} #3 \teqv #4 : {#5}}
\newcommand{\lbeq}[4]{#1 \vdash #2 \teqv #3 \rhd {#4}}
\newcommand{\tmseq}[4]{\issubst{#1 \teqv #2}{#3}{#4}}
\newcommand{\lbseq}[5]{\lbsubst{#1 \teqv #2}{#3}{#4}{#5}}
\newcommand{\brle}[1]{{\textsf{#1}}}
\newcommand{\toanf}[1]{\ms{ANF}(#1)}
\newcommand{\letanf}[3]{\ms{ANF}_{\ms{let}}(#1, #2, #3)}
\newcommand{\tossa}[1]{\ms{SSA}(#1)}
\newcommand{\ssawhere}[2]{\ms{SSA}_{\ms{a}}(#1, #2)}
\newcommand{\toentry}[1]{\ms{entry}(#1)}
\newcommand{\todom}[1]{\ms{children}(#1)}
\newcommand{\tocfg}[1]{\ms{cfg}(#1)}
\newcommand{\adddom}[2]{\ms{bb}(#1, #2)}
\newcommand{\toreg}[1]{\ms{reg}(#1)}
\newcommand{\todnf}[1]{\ms{dom}(#1)}
\newcommand{\towhile}[2]{\ms{WH}_{#1}(#2)}
\newcommand{\topwhile}[2]{\ms{PW}_{#1}(#2)}
% Denotational semantics
\newcommand{\dnt}[1]{\llbracket{#1}\rrbracket}
\newcommand{\ednt}[1]{\left\llbracket{#1}\right\rrbracket}
\newcommand{\tmor}[1]{{!}_{#1}}
\newcommand{\dmor}[1]{{\Delta}_{#1}}
\newcommand{\entrymor}[3]{\ms{esem}_{#1, #3}(#2)}
\newcommand{\loopmor}[3]{\ms{lsem}_{#1, #3}(#2)}
\newcommand{\substpure}[1]{#1\;\ms{pure}}
% Comonadic lore
\newcommand{\lmor}[1]{\ms{let}(#1)}
\newcommand{\envcom}[2]{{#1}_{#2 \otimes \cdot}}
\newcommand{\rlmor}[1]{\ms{rlet}(#1)}
\newcommand{\rcase}[1]{\ms{rcase}(#1)}
\newcommand{\rfix}[1]{\ms{rfix}(#1)}
\newcommand{\rseq}[3]{#2 \gg_{#1} #3}
\newcommand{\envpil}[1]{\pi_{{#1}l}}
\newcommand{\envpir}[1]{\pi_{{#1}r}}
\newcommand{\toenv}[2]{\ms{env}_{#1}(#2)}
\newcommand{\envcop}[3]{[#2, #3]_{#1}}
\newcommand{\envinr}[1]{\iota^{#1}_{r}}
\newcommand{\envinl}[1]{\iota^{#1}_{l}}
\newcommand{\envtn}[3]{{#2} \otimes_{#1} {#3}}
% Composition
\newcommand{\invar}{\square}
\newcommand{\outlb}{\blacksquare}
\newcommand{\pckd}[1]{\langle #1 \rangle}
% Weak memory
\newcommand{\bufloc}[1]{\overline{#1}}
% Branding
\newcommand{\isotopessa}{\(\lambda_{\ms{SSA}}\)}
% Formalization pointers
\newcommand{\formalizedas}[1]{Formalized as \texttt{#1}}
%% Rights management information. This information is sent to you
%% when you complete the rights form. These commands have SAMPLE
%% values in them; it is your responsibility as an author to replace
%% the commands and values with those provided to you when you
%% complete the rights form.
\setcopyright{acmcopyright}
\copyrightyear{2024}
\acmYear{2024}
\acmDOI{XXXXXXX.XXXXXXX}
%%
%% These commands are for a JOURNAL article.
% \acmJournal{JACM}
% \acmVolume{37}
% \acmNumber{4}
% \acmArticle{111}
% \acmMonth{8}
%%
%% Submission ID.
%% Use this when submitting an article to a sponsored event. You'll
%% receive a unique submission ID from the organizers
%% of the event, and this ID should be used as the parameter to this command.
%%\acmSubmissionID{123-A56-BU3}
\begin{document}
\title{The Denotational Semantics of SSA}
\author{Jad Ghalayini}
\email{[email protected]}
\orcid{0000-0002-6905-1303}
\author{Neel Krishnaswami}
\email{[email protected]}
\orcid{0000-0003-2838-5865}
\begin{abstract}
Static single assignment form, or SSA, has been the dominant
compiler intermediate representation for decades. In this paper, we
give a type theory for a variant of SSA, including its equational
theory, which are strong enough to validate a variety of control and
data flow transformations. We also give a categorical semantics for
SSA, and show that the type theory is sound and complete with
respect to the categorical axiomatization. We demonstrate the
utility of our model by exhibiting a variety of concrete models
satisfying our axioms, including in particular a model of TSO weak
memory. The correctness of the syntactic metatheory, as well as the
completeness proof has been mechanized in the Lean proof assistant.
\end{abstract}
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003752.10010124.10010131.10010133</concept_id>
<concept_desc>Theory of computation~Denotational semantics</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10010124.10010131.10010137</concept_id>
<concept_desc>Theory of computation~Categorical semantics</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10011740</concept_id>
<concept_desc>Theory of computation~Type theory</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Theory of computation~Denotational semantics}
\ccsdesc[500]{Theory of computation~Categorical semantics}
\ccsdesc[500]{Theory of computation~Type theory}
%%
%% Keywords. The author(s) should pick words that accurately describe
%% the work being presented. Separate the keywords with commas.
\keywords{SSA, Categorical Semantics, Elgot Structure, Effectful Category}
% \received{20 February 2007}
% \received[revised]{12 March 2009}
% \received[accepted]{5 June 2009}
\maketitle
\emph{This paper is dedicated to the memory of Alan Jeffrey, who
taught us about both premonoidal categories and the semantics of weak memory, and
who never shied away from either theory or implementation.}
\section{Introduction}
Static single assignment form, or SSA form, has been the dominant compiler intermediate
representation since its introduction by \citet{alpern-ssa-original-88} and \citet{rosen-gvn-1988}
in the late 1980s. Most major compilers -- GCC, Clang, MLIR, Cranelift -- use this representation,
because it makes many optimizations much easier to do than traditional 3-address code IRs.
The key idea behind SSA is to adapt an idea from functional programming: namely, every variable is
defined only once. This means that substitution is unconditionally valid, without first requiring a
dataflow analysis to compute where definitions reach. Unlike in functional programming, though,
scoping of definitions in SSA is traditionally not lexical. Instead, scoping is determined by
\emph{dominance}: every variable occurrence must be dominated by a single assignment in the control
flow graph.
The semantics of SSA has traditionally been handled quite informally, because conceptually, it is a
simple first-order imperative programming language. As a result, whether a rewrite is sound or not
is usually obvious, without having to do a complex correctness argument.
Unfortunately, computers are no longer as simple as they were in the late 1980s. Modern computers
are typically multicore, and feature many levels of caching, and as a result the semantics of memory
is no longer correctly modelled as a big array of bytes. Finding good semantics for modern weak
memory systems remains an ongoing challenge.
As a result, it is not correct to justify compiler optimizations in terms of a simple imperative
model, and it is an open question which equations should hold of an SSA program. This is a
particularly fraught question, because it is also unclear which equations weak memory models should
satisfy.
What we would like to know is which equations any SSA representation should satisfy. This would let
us establish a contract between compiler writers and hardware designers. The compiler writers could
rely upon the equational theory of SSA when justifying optimizations, without needing to know all
the details of the memory model at all times. Conversely, memory models could be validated by
seeing if they satisfy the equations of SSA, without needing to study every possible compiler
optimization.
Concretely, our contributions are as follows:
\begin{itemize}
\item First, we give a type-theoretic presentation of SSA, with both typing rules (in
Section~\ref{sec:typing}) and an equational theory (in Section~\ref{sec:equations}) for
well-typed terms. We also prove the correctness of suitable substitution properties for this
calculus.
\item Next, in Section~\ref{sec:densem}, we give a categorical semantics for this type theory, in
terms of distributive Elgot categories. We show that any denotational model with this categorical
structure is also a model of SSA. This shows that all of the equations we give are sound with
respect to the categorical structure.
\item We also show, in Section~\ref{ssec:completeness}, that syntax quotiented by the equational
theory yields the initial distributive Elgot category. This establishes that our set of syntactic
equations is complete, and that there are no equations which the denotational semantics validates,
but which cannot be proved syntactically.
\item We proceed in Section~\ref{sec:concrete} to show that this denotational axiomatization is
useful in practice, by giving a variety of concrete models, including a model of TSO weak memory
based on~\citet{sparky} in Section~\ref{ssec:tso}. This demonstrates that it is possible to give
realistic weak memory models which do not disturb the structure of SSA in fundamental ways.
\item Finally, we have substantially mechanized our proofs using the Lean 4 proof assistant. We have
mechanized proofs of substitution for our type theory, as well as proofs that the syntax forms the
initial model, and that the SPARC TSO semantics forms a valid model of SSA. The denotational
semantics and its proof of the soundness of substitution are done on paper.
\end{itemize}
\section{Static Single Assignment Form}
In this section, we describe SSA form and the isomorphism between the standard $\phi$-node-based
presentation and the more functional \emph{basic blocks with arguments} format. We then discuss
standard dominance-based scoping and how it can be recast as lexical scoping to make it more
amenable to standard type-theoretic treatment. We further generalize this format to allow branching
to arbitrary code rather than only labels, obtaining \emph{A-normal form}
(ANF)~\cite{flanagan-93-anf}, analogously to the transformation described by
\citet{chakravarty-functional-ssa-2003}. Finally, to allow for substitution, we relax our syntax to
permit arbitrary expression nesting and \ms{let}-expressions, resulting in \emph{type-theoretic
SSA}, or \isotopessa{}, which will be the focus of the rest of this paper. A straightforward
argument shows that these extensions add no expressive power; we give a more formal version of this
argument, as well as algorithms to interconvert between \isotopessa{}, standard SSA, and ANF, in
Section~\ref{ssec:ssa-normal}.
As a running example, consider the simple imperative program to compute $10!$ given in
Figure~\ref{fig:fact-program}. Operating directly on an imperative language can be challenging,
since having a uniform representation of code friendly to mechanized optimization and analysis is
often in tension with features designed to improve readability and programmer productivity, such as
syntactic sugar. Early work on compiler intermediate representations, notably by Frances
Allen~\cite{allen-70-cfa}, introduced \emph{three-address code}, also known as \emph{register
transfer language (RTL)}, to normalize programs into a form more suitable for analysis and
optimization. We can normalize our code into 3-address code, as in Figure~\ref{fig:fact-3addr}, by:
\begin{itemize}
\item Converting structured control flow (e.g., \ms{while}) into unstructured jumps between basic
blocks labelled \ms{start}, \ms{loop}, and \ms{body}.
\item Replacing subexpressions like $i + 1$ in $a * (i + 1)$ with \ms{let}-bindings so that every
expression in our program is atomic.
\end{itemize}
\begin{figure}
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{let\;mut}\;i = 1; \\
& \ms{let\;mut}\;a = 1; \\
& \ms{while}\;i_0 < n\;\{ \\
& \quad a = a * (i + 1) \\
& \quad i = i + 1; \\
& \} \\
& \ms{ret}\;a \\
\end{align*}
\caption{As an imperative program}
\label{fig:fact-imp}
\end{subfigure}%
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
\ms{start}:\quad & \ms{let}\;n = 10; \\
& \ms{let\;mut}\;i = 1; \\
& \ms{let\;mut}\;a = 1; \\
& \ms{br}\;\ms{loop} \\
\ms{loop}: \quad & \ms{if}\;i < n\;
\{\;\ms{br}\;\ms{body}\;\}\;
\ms{else}\;\{\;\ms{ret}\;a\;\} \\
\ms{body}: \quad & \ms{let}\;t = i + 1; \\
& a = a * t; \\
& i = i + 1; \\
& \ms{br}\;\ms{loop}
\end{align*}
\caption{As 3-address code}
\label{fig:fact-3addr}
\end{subfigure}
\caption{
A simple, slightly suboptimal program to compute $10!$ via multiplication in a loop, represented
as typical imperative code and in 3-address code.
}
\Description{}
\label{fig:fact-program}
\end{figure}
While functional languages typically rely on \emph{lexical scoping}, where the scope of a variable
is determined by its position within the code's nested structure, 3-address code uses a different
scoping mechanism based on \emph{dominance}. In particular, a variable $x$ is considered to be in
scope at a specific point $P$ if and only if all execution paths from the program's entry point to
$P$ pass through a definition $D$ for $x$. In this case, we say that the definition $D$
\emph{strictly dominates} $P$. The relation on basic blocks ``$A$ strictly dominates $B$"
intersected with ``$A$ is a \emph{direct predecessor} of $B$" forms a tree called the
\emph{dominance tree} of the CFG -- this can be computed in nearly linear time
\cite{cytron-ssa-intro-91}.
Despite this normalization, many optimizations remain difficult to express in this format because a
variable's value may be set by multiple definitions throughout the program's execution. To improve
our ability to reason about programs, we introduce the \emph{static single assignment} restriction,
originally proposed by \citet{alpern-ssa-original-88}, which states that every variable must be
defined at exactly one point in the program. We can intuitively represent this as every variable
being given by an immutable \ms{let}-binding. In particular, given a variable $x$, which we can now
associate to its unique definition $D_x$, $x$ is in scope at a point $P$ if and only if $D_x$
strictly dominates $P$.
One might attempt to convert programs to SSA form by numbering each definition of a variable,
effectively changing references to $x$ to references to $x_t$, i.e. ``$x$ at time $t$.'' For
example, we could rewrite
\begin{multline}
\letexpr{x}{3y + 5}{\letexpr{x}{3x + 2}{\letexpr{x}{3x + 1}{\ms{ret}\;x}}}
\\ \teqv \letexpr{x_0}{3y + 5}{\letexpr{x_1}{3x_0 + 2}{\letexpr{x_2}{3x_1 + 1}{\ms{ret}\;x_2}}}
\end{multline}
This transformation enables algebraic reasoning about expressions involving each $x_t$. However,
since we can only define a variable once in SSA form, expressing programs with loops and branches
becomes challenging. For example, na\"ively trying to lower the program in
Figure~\ref{fig:fact-3addr} into SSA form would not work, since the $i$ definition $i = i + 1$ can
refer to \emph{either} the previous value of $i$ from the last iteration of the loop \emph{or} the
original value $i = 1$. The classical solution is to introduce \emph{$\phi$-nodes}, which select a
value based on the predecessor block from which control arrived. We give the lowering of our program
into SSA with $\phi$-nodes in Figure~\ref{fig:fact-ssa}.
\citet{cytron-ssa-intro-91} introduced the first efficient algorithm to lower a program in 3-address
code to valid SSA while introducing a minimum number of $\phi$-nodes, making SSA practical for
widespread use as an intermediate representation. Unfortunately, $\phi$-nodes do not have an obvious
operational semantics. Additionally, they require us to adopt more complex scoping rules than simple
dominance-based scoping. For example, in basic block \ms{loop} in Figure~\ref{fig:fact-ssa}, $i_0$
evaluates to 1 if we came from \ms{start} and to $i_1$ if we came from \ms{body}. Similarly, $a_0$
evaluates to either 1 or $a_1$ based on the predecessor block. This does not obey dominance-based
scoping, since $i_0$ and $i_1$ are defined \emph{after} the $\phi$-nodes $i_0$, $a_0$ that reference
them, which seems counterintuitive -- after all, variables are typically used after they are
defined. In fact, since the value of a $\phi$-node is determined by which basic block is our
immediate predecessor, we instead need to use the rule that expressions in $\phi$-node branches with
source $S$ can use any variable $y$ defined at the \emph{end} of $S$. Note that this is a strict
superset of the variables visible for a normal instruction $x$, which can only use variables $y$
which \emph{dominate} $x$ -- i.e., such that \emph{every} path from the entry block to the
definition of $x$ goes through $y$, rather than only those paths which also go through $S$.
\begin{figure}
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
\ms{start}:\quad & \ms{let}\;n = 10; \\
& \ms{let\;mut}\;i = 1; \\
& \ms{let\;mut}\;a = 1; \\
& \ms{br}\;\ms{loop} \\
\ms{loop}: \quad & \ms{if}\;i < n\;
\{\;\ms{br}\;\ms{body}\;\}\;
\ms{else}\;\{\;\ms{ret}\;a\;\} \\
\ms{body}: \quad & \ms{let}\;t = i + 1; \\
& a = a * t; \\
& i = i + 1; \\
& \ms{br}\;\ms{loop}
\end{align*}
\caption{3-address code}
\end{subfigure}%
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
\ms{start}:\quad & \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop} \\
\ms{loop}: \quad & \ms{let}\;i_0 = \phi(\ms{start}: 1, \ms{body}: i_1) \\
& \ms{let}\;a_0 = \phi(\ms{start}: 1, \ms{body}: a_1) \\
& \ms{if}\;i_0 < n\;
\{\;\ms{br}\;\ms{body}\;\}\;
\ms{else}\;\{\;\ms{ret}\;a_0\;\} \\
\ms{body}: \quad & \ms{let}\;t = i_0 + 1 \\
& \ms{let}\;a_1 = a_0 * t \\
& \ms{let}\;i_1 = i_0 + 1 \\
& \ms{br}\;\ms{loop}
\end{align*}
\caption{Converted to SSA form}
\label{fig:fact-ssa}
\end{subfigure}
\caption{
Conversion of three address code for the program in Figure~\ref{fig:fact-program} to SSA
form, requring the insertion of $\phi$-nodes for $i$ and $a$ due to control-flow dependent
updates. Note how SSA-form can be viewed as ``three address code in which all
\ms{let}-bindings are immutable.''
}
\Description{}
\end{figure}
While this rule can be quite confusing, and in particular makes it non-obvious how to assign an
operational semantics to $\phi$-nodes, the fact that the scoping for $\phi$-node branches is based
on the source block, rather than the block in which the $\phi$-node itself appears, hints at a
possible solution. By \emph{moving} the expression in each branch to the \emph{call-site}, we can
transition to an isomorphic syntax called basic blocks with arguments (BBA), as illustrated in
Figure \ref{fig:fact-bba}. In this approach, each $\phi$-node -- since it lacks side effects and has
scoping rules independent of its position in the basic block, depending only on the source of each
branch -- can be moved to the top of the block. This reorganization allows us to treat each
$\phi$-node as equivalent to an argument for the basic block, with the corresponding values passed
at the jump site. Converting a program from BBA format back to standard SSA form with $\phi$-nodes
is straightforward: introduce a $\phi$-node for each argument of a basic block, and for each branch
corresponding to the $\phi$-node, add an argument to the jump instruction from the appropriate
source block.
This allows us to use standard dominance-based scoping without any special cases for $\phi$-nodes.
When considering basic blocks, this means that a variable is visible within the block $D$ where it
is defined, starting from the point of its definition. It continues to be visible in all subsequent
blocks $P$ that are strictly dominated by $D$ in the control-flow graph (CFG). For example, in
Figure~\ref{fig:fact-bba}:
\begin{itemize}
\item \ms{start} strictly dominates \ms{loop} and \ms{body}; thus, the variable $n$ defined in
\ms{start} is visible in \ms{loop} and \ms{body}.
\item \ms{loop} strictly dominates \ms{body}; therefore, the parameters $i_0$, $a_0$ to \ms{loop}
are visible in \ms{body} without the need to pass them as parameters.
\item \ms{body} does \emph{not} strictly dominate \ms{loop}, since there is a path from \ms{start}
to \ms{loop} that does not pass through \ms{body}.
\end{itemize}
\begin{figure}
\begin{subfigure}[t]{.5\textwidth}
\centering
\begin{align*}
\ms{start}:\quad & \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop} \\
\ms{loop}: \quad & \begingroup \color{red}
\ms{let}\;i_0 = \phi(\ms{start}: 1, \ms{body}: i_1)
\endgroup \\
& \begingroup \color{blue}
\ms{let}\;a_0 = \phi(\ms{start}: 1, \ms{body}: a_1)
\endgroup \\
& \ms{if}\;i_0 < n\;\{\;\ms{br}\;\ms{body}\;\} \\
& \ms{else}\;\{\;\ms{ret}\;a_0\;\} \\
\ms{body}: \quad & \ms{let}\;t = i_0 + 1 \\
& \ms{let}\;a_1 = a_0 * t \\
& \ms{let}\;i_1 = i_0 + 1 \\
& \ms{br}\;\ms{loop}
\end{align*}
\caption{With $\phi$-nodes}
\label{fig:fact-phi}
\end{subfigure}%
\begin{subfigure}[t]{.5\textwidth}
\centering
\begin{align*}
\ms{start}:\quad & \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(\textcolor{red}{1}, \textcolor{blue}{1}) \\
\ms{loop}(\textcolor{red}{i_0}, \textcolor{blue}{a_0}): \quad
& \ms{if}\;i_0 < n\; \{\;\ms{br}\;\ms{body}\;\} \\
& \ms{else}\;\{\;\ms{ret}\;a_0\;\} \\
\ms{body}: \quad & \ms{let}\;t = i_0 + 1 \\
& \ms{let}\;a_1 = a_0 * t \\
& \ms{let}\;i_1 = i_0 + 1 \\
& \ms{br}\;\ms{loop}(\textcolor{red}{i_1}, \textcolor{blue}{a_1})
\\ \\
\end{align*}
\caption{Basic-blocks with arguments}
\label{fig:fact-bba}
\end{subfigure}
\caption{
The program in Figure \ref{fig:fact-program} written in standard SSA (using $\phi$ nodes),
like in LLVM \cite{llvm}, and in basic-blocks with arguments SSA, like in MLIR \cite{mlir} and
Cranelift \cite{cranelift}. The arguments $i_0, a_0$ corresponding to the $\phi$-nodes $i_0,
a_0$ are colored in \textcolor{red}{red} and \textcolor{blue}{blue}, respectively.
}
\Description{}
\end{figure}
An important insight provided by the BBA format, as discussed by \citet{appel-ssa} and
\citet{kelsey-95-cps}, is that a program in SSA form can in this way be interpreted as a collection
of tail-recursive functions, where each basic block and branch correspond to a function and tail
call, respectively. This interpretation offers a natural framework for defining the semantics of SSA
and reasoning about optimizations. However, there is a subtle difference between the scoping rules
in this format and the actual scoping used in traditional SSA, which requires careful consideration.
By topologically sorting the basic blocks in the CFG according to this partial order and inserting
brackets based on the dominance tree, we can convert dominance-based scoping to lexical scoping. In
this arrangement, a variable is in lexical scope if and only if it is in scope under dominance-based
scoping, as shown in Figure~\ref{fig:dominance-to-lexical}. This transformation is straightforward,
and standard SSA can be recovered by removing the inserted \ms{where}-blocks.
\begin{figure}
\centering
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
\ms{start}:\quad & \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
\ms{loop}(i_0, a_0): \quad & \ms{if}\;i_0 < n\; \{\;\ms{br}\;\ms{body}\;\} \\
& \ms{else}\;\{\;\ms{ret}\;a_0\;\} \\
\ms{body}: \quad & \ms{let}\;t = i_0 + 1 \\
& \ms{let}\;a_1 = a_0 * t \\
& \ms{let}\;i_1 = i_0 + 1 \\
& \ms{br}\;\ms{loop}(i_1, a_1) \\ \\ \\ \\
\end{align*}
\caption{Dominance-based scoping}
\end{subfigure}%
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{ \\
& \quad \ms{if}\;i_0 < n\;\{\;\ms{br}\;\ms{body}\;\} \\
& \quad \ms{else}\;\{\;\ms{ret}\;a_0\;\} \\
& \quad \ms{where}\;\ms{body}: \{\\
& \qquad \ms{let}\;t = i_0 + 1 \\
& \qquad \ms{let}\;a_1 = a_0 * t \\
& \qquad \ms{let}\;i_1 = i_0 + 1 \\
& \qquad \ms{br}\;\ms{loop}(i_1, a_1) \\
& \quad \} \\
& \}
\end{align*}
\caption{Lexical scoping}
\end{subfigure}
\caption{Conversion of an SSA program from dominance-based scoping to explicit lexical scoping}
\Description{}
\label{fig:dominance-to-lexical}
\end{figure}
Lexical scoping allows us to apply many of the techniques developed in theoretical computer science
and functional programming for reasoning about and developing optimizations and analysis passes --
in particular, the result of our conversion to lexical scoping looks a lot like the correspondence
between SSA and CPS described in \citet{kelsey-95-cps}. We can use this correspondence to guide us
in developing an \textit{equational theory} for SSA programs, with the goal of enabling
compositional reasoning about program transformations such as:
\begin{itemize}
\item \textit{Control-flow rewrites}, such as jump-threading or fusing two identical branches of
an \ms{if}-statement
\item \textit{Algebraic rewrites}, such as simplifying arithmetic expressions
\item Combinations of the two, such as rewriting $\ms{if}\;x > 0\;\ms{then}\;1 - x\;\ms{else}\;1 +
x$ to $1 + \ms{abs}(x)$.
\end{itemize}
We can work towards making these easier to express by generalizing our syntax to allow the branches
of if-statements to contain arbitrary code, rather than just unconditional branches, as in
Figure~\ref{fig:bba-to-anf}. This clearly adds no additional expressive power, since:
\begin{itemize}
\item This syntax clearly generalizes the previous syntax, so no conversion into it is necessary
\item To revert back to the less general syntax, one must simply introduce new anonymous basic
blocks for each branch of the if-statement, likeso:
\begin{equation}
\ms{if}\;e\;\{s\}\;\ms{else}\;\{t\}
\to (\ms{if}\;e\;\{\ms{br}\;\ell_\top\}\;\ms{else}\;\{\ms{br}\;\ell_\bot\})\;
\ms{where}\;\ell_\top: \{s\},\;\ell_\bot: \{t\}
\end{equation}
\end{itemize}
What we end up with is something which looks a lot like \textit{administrative normal form} (ANF),
with our transformation analogous to that described in \citet{chakravarty-functional-ssa-2003}. The
key difference is that, in our format (which is strictly first order), we require an explicit
\ms{ret} instruction (rather than adopting an expression-oriented language), and write
``$\ms{let\;rec}\;f(x) = e; t$" as ``$\where{t}{\wbranch{f}{x}{e}}$."
\begin{figure}
\centering
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{ \\
& \quad \ms{if}\;i_0 < n\;\{\;\ms{br}\;\ms{body}\;\} \\
& \quad \ms{else}\;\{\;\ms{ret}\;a_0\;\} \\
& \quad \ms{where}\;\ms{body}: \{\\
& \qquad \ms{let}\;t = i_0 + 1 \\
& \qquad \ms{let}\;a_1 = a_0 * t \\
& \qquad \ms{let}\;i_1 = i_0 + 1 \\
& \qquad \ms{br}\;\ms{loop}(i_1, a_1) \\
& \quad \} \\
& \}
\end{align*}
\end{subfigure}%
\begin{subfigure}[t]{.5\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{\\
& \quad \ms{if}\;i_0 < n\;\{ \\
& \qquad \ms{let}\;t = i_0 + 1 \\
& \qquad \ms{let}\;a_1 = a_0 * t \\
& \qquad \ms{let}\;i_1 = i_0 + 1 \\
& \qquad \ms{br}\;\ms{loop}(i_1, a_1) \\
& \quad \}\;\ms{else}\;\{ \\
& \qquad \ms{ret}\;a_0 \\
& \quad \} \\
& \}
\end{align*}
\end{subfigure}
\caption{Allowing if-statements to jump to arbitrary instructions, rather than a terminator}
\Description{}
\label{fig:bba-to-anf}
\end{figure}
ANF, however, lacks a good substitution property, since substituting a value for a variable can take
you out of ANF, making it difficult to express optimizations like $(i + 1) - 1 \to i$ as rewrite
rules. To fix this, we can simply relax the restriction that expressions in a program must be
atomic. This can again trivially be seen to add no excessive power, since we can always introduce
temporary variables via \ms{let}-bindings to make any expression atomic. For full generality, we
will also allow \ms{let}-bindings and \ms{if}-statements \textit{inside} expressions, which again
can be eliminated in the obvious manner, such as by taking
\begin{align*}
\ms{let}\;x = (\ms{if}\;e\;\{a\}\;\ms{else}\;\{b\}); t &
\to \ms{if}\;e\;\{\ms{let}\;x = a; t\}\;\ms{else}\;\{\ms{let}\;x = b; t\} \\
& \to \ms{if}\;e\;\{\ms{br}\;\ell(x)\}\;\ms{else}\;\{\ms{br}\;\ell(x)\}\;
\ms{where}\;\ell(x): \{t\}
\end{align*}
\begin{figure}
\centering
\begin{subfigure}[t]{.31\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{\\
& \quad \ms{if}\;i_0 < n\;\{ \\
& \qquad \ms{let}\;t = i_0 + 1 \\
& \qquad \ms{let}\;a_1 = a_0 * t \\
& \qquad \ms{let}\;i_1 = i_0 + 1 \\
& \qquad \ms{br}\;\ms{loop}(i_1, a_1) \\
& \quad \}\;\ms{else}\;\{ \\
& \qquad \ms{ret}\;a_0 \\
& \quad \} \\
& \}
\end{align*}
\caption{Program in ANF}
\label{fig:fact-anf}
\end{subfigure}%
\begin{subfigure}[t]{.35\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{\\
& \quad \ms{if}\;i_0 < n\;\{ \\
& \qquad \ms{br}\;\ms{loop}(i_0 + 1, a_0 * (i_0 + 1)) \\
& \quad \}\;\ms{else}\;\{ \\
& \qquad \ms{ret}\;a_0 \\
& \quad \} \\
& \} \\ \\ \\
\end{align*}
\caption{
Programs \ref{fig:fact-anf} and \ref{fig:fact-subst} after substitution;
since the result is the same, both programs must be equivalent.
}
\label{fig:fact-subst}
\end{subfigure}\hspace{1em}%
\begin{subfigure}[t]{.31\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{\\
& \quad \ms{if}\;i_0 < n\;\{ \\
& \qquad \ms{let}\;i_1 = i_0 + 1 \\
& \qquad \ms{let}\;a_1 = a_0 * i_1 \\
& \qquad \ms{br}\;\ms{loop}(i_1, a_1) \\
& \quad \}\;\ms{else}\;\{ \\
& \qquad \ms{ret}\;a_0 \\
& \quad \} \\
& \} \\
\end{align*}
\caption{Optimized ANF program}
\label{fig:fact-opt}
\end{subfigure}
\caption{
Adding support for expressions, allowing us to perform substitutions of (pure) expressions.
Optimizations such as common subexpression elimination can be built using substitution as a
building block.
}
\Description{}
\label{fig:fact-cse}
\end{figure}
This gives us our final \isotopessa{} calculus, which we will call \emph{type-theoretic SSA}. In
this language, we can safely perform \textit{substitutions}, like in Figure~\ref{fig:fact-cse}.
These can then be used to build up optimizations such as \textit{common-subexpression elimination}.
More generally, substitution lets us do \textit{algebra}. For example, since we know that:
\begin{align*}
(i_0 + 1, a_0 * (i_0 + 1)) &= (\ms{let}\;(x, y) = (i_0, a_0)\;\ms{in}\;(x + 1, y * (x + 1))) \\
(1, 1) &= (\ms{let}\;(x, y) = (0, 1)\;\ms{in}\;(x + 1, y * (x + 1)))
\end{align*}
we can rewrite the program in Figure~\ref{fig:fact-subst-2} to that in Figure~\ref{fig:fact-dinat}.
We can then apply general rewrite rules such as \textit{dinaturality} to rewrite
Figure~\ref{fig:fact-dinat} to Figure~\ref{fig:fact-zero}. This allows us to build up justifications
for complex optimizations, such as rewriting \ref{fig:fact-zero} to \ref{fig:fact-opt}, in terms of
simple rewriting steps. In particular, we can do \textit{complex}, \textit{error-prone} loop and
control-flow graph optimizations by breaking them down into closed set of simple algebraic steps,
with each step rigorously justified via our denotational semantics
\begin{figure}
\begin{minipage}{.5\textwidth}
\begin{subfigure}{\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}(1, 1) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{\\
& \quad \ms{if}\;i_0 < n\;\{ \\
& \qquad \ms{br}\;\ms{loop}(i_0 + 1, a_0 * (i_0 + 1)) \\
& \quad \}\;\ms{else}\;\{ \\
& \qquad \ms{ret}\;a_0 \\
& \quad \} \\
& \}
\end{align*}
\caption{Substituted program from Figure \ref{fig:fact-subst}}
\label{fig:fact-subst-2}
\end{subfigure}
\begin{subfigure}{\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}\;(0, 1) \\
& \ms{where}\;\ms{loop}(x, y): \{\\
& \quad \ms{let}\;(i_0, a_0) = (x + 1, y * (x + 1)); \\
& \quad \ms{if}\;i_0 < n\;\{ \\
& \qquad \ms{br}\;\ms{loop}(i_0, a_0) \\
& \quad \}\;\ms{else}\;\{ \\
& \qquad \ms{ret}\;a_0 \\
& \quad \} \\
& \}
\end{align*}
\caption{Equivalent to Figure \ref{fig:fact-zero} by \textit{dinaturality}}
\label{fig:fact-dinat}
\end{subfigure}
\end{minipage}%
\begin{subfigure}[c]{.5\textwidth}
\begin{align*}
& \ms{let}\;n = 10; \\
& \ms{br}\;\ms{loop}( \\
& \quad \ms{let}\;(x, y) = (0, 1); \\
& \quad(x + 1, y * (x + 1)) \\
& ) \\
& \ms{where}\;\ms{loop}(i_0, a_0): \{\\
& \quad \ms{if}\;i_0 < n\;\{ \\
& \qquad \ms{br}\;\ms{loop}( \\
& \qquad \quad \ms{let}\;(x, y) = (i_0, a_0); \\
& \qquad \quad (x + 1, y * (x + 1)) \\
& \qquad ) \\
& \quad \}\;\ms{else}\;\{ \\
& \qquad \ms{ret}\;a_0 \\
& \quad \} \\
& \}
\end{align*}
\caption{Equivalent to Figure \ref{fig:fact-subst-2} by substitution}
\label{fig:fact-zero}
\end{subfigure}
\caption{
Decomposing multi-block rewrites (from \ref{fig:fact-zero} to
\ref{fig:fact-subst-2}, and therefore to the more optimal program
\ref{fig:fact-opt}) into simple algebraic steps. By verifying each step, we can
verify complex optimizations through decomposition.
}
\Description{}
\label{fig:fact-dinat-rewrites}
\end{figure}
\section{Type Theory}
\label{sec:typing}
We now give a formal account of \isotopessa{}, starting with the types. Our types are first order,
and consists of binary sums $A + B$, products $A \otimes B$, the unit type $\mathbf{1}$, and the
empty type $\mb{0}$, all parameterised over a set of base types $X \in \mc{T}$. We write our set of
types as $\ms{Ty}(X)$. We also parameterise over:
\begin{itemize}
\item A set of effects $\epsilon \in \mc{E}$, forming a join-semilattice with bottom element $\bot
\in \mc{E}$
\item For each pair $A, B \in \ms{Ty}(X)$ and effect $\epsilon \in \mc{E}$, a
set of \textit{primitive instructions} $f \in \mc{I}_\epsilon(A, B)$, where
$\epsilon \leq \epsilon' \implies \mc{I}_\epsilon(A, B) \subseteq
\mc{I}_{\epsilon'}(A, B)$.
We write $\mc{I}(A, B) = \bigcup_\epsilon\mc{I}_\epsilon(A, B)$,
$\mc{I}_\epsilon = \bigcup_{A, B}\mc{I}_\epsilon(A, B)$, and $\mc{I} =
\bigcup_\epsilon\mc{I}_\epsilon$.
\end{itemize}
We'll call a tuple $Sg = (\mc{E}, \mc{T}, \mc{I})$ of types and instructions over these types an
\emph{\isotopessa{}-signature}.
A (variable )\textit{context} $\Gamma$ is a list of \textit{typing hypotheses}
$\thyp{x}{A}{\epsilon}$, where $x$ is a variable name, $A$ is the type of that variable, and
$\epsilon$ is the effect of using that variable (used when filling holes with effectful
expressions). If $\epsilon = \bot$, we often omit it, writing $\bhyp{x}{A}$. Similarly, we define a
\textit{label-context} to be a list of \textit{labels} $\lhyp{\ell}{A}$, where $A$ is the parameter
type that must be passed on a jump to the label $\ell$.
\begin{figure}[H]
\begin{center}
\begin{grammar}
<\(A, B, C\)> ::=
\(X\)
\;|\; \(A \otimes B\)
\;|\; \(\mathbf{1}\)
\;|\; \(A + B\)
\;|\; \(\mathbf{0}\)
<\(a, b, c, e\)> ::= \(x\)
\;|\; \(f\;a\)
\;|\; \(\letexpr{x}{a}{e}\)
\alt \(()\)
\;|\; \((a, b)\)
\;|\; \(\letexpr{(x, y)}{a}{e}\)
\alt \(\linl{a}\)
\;|\; \(\linr{a}\)
\;|\; \(\labort{a}\)
\;|\; \(\caseexpr{e}{x}{s}{y}{t}\)
<\(s, t\)> ::= \(\brb{\ell}{a}\)
\alt \(\letstmt{x}{a}{t}\)
\;|\; \(\letstmt{(x, y)}{a}{t}\)
\;|\; \(\casestmt{e}{x}{s}{y}{t}\)
\alt \(\where{t}{(\wbranch{\ell_i}{x_i}{t_i},)_i}\)
<\(\Gamma\)> ::= \(\cdot\) \;|\; \(\Gamma, \thyp{x}{A}{\epsilon}\)
<\(\ms{L}\)> ::= \(\cdot\) \;|\; \(\ms{L}, \lhyp{\ell}{A}\)
\end{grammar}
\end{center}
\caption{Grammar for \isotopessa{}, parametrized over an \isotopessa{} signature}
\Description{}
\label{fig:ssa-grammar}
\end{figure}
As shown in Figure~\ref{fig:ssa-grammar}, \isotopessa{} terms are divided into two syntactic
categories, each of with associated with a judgement:
\begin{itemize}
\item \emph{Expressions} $a, b, c, e$ typed with the judgement $\hasty{\Gamma}{\epsilon}{a}{A}$,
which says that under the typing context $\Gamma$, the expression $a$ has type $A$ and effect
$\epsilon$. We say a term is \emph{pure} if it has effect $\bot$; note that whether an expression
is pure or not depends both on the expression itself and on the purity of the variables used in
the expression; this is to allow reasoning about impure substitutions.
\item \emph{Regions} $r, s, t$, which recursively define a lexically-scoped SSA program with a
single entry and (potentially) multiple exits. This is typed with the judgement
$\haslb{\Gamma}{r}{\ms{L}}$, which states that given that $\Gamma$ is live at the unique entry
point, $r$ will either loop forever or branch to one of the exit labels in $\ell(A) \in \ms{L}$
with an argument of type $A$.
\end{itemize}
The typing rules for expressions are given in Figure~\ref{fig:ssa-expr-rules}. In particular,
expressions may be built up from the following fairly standard primitives:
\begin{itemize}
\item A variable $x$ in the context $\Gamma$, as typed by \brle{var}. We write $(A, \epsilon) \leq
(B, \epsilon') \iff A = B \and \epsilon \leq \epsilon'$.
\item An \emph{primitive instruction} $f \in \mc{I}_\epsilon(A, B)$ applied to an expression
$\hasty{\Gamma}{\epsilon}{a}{A}$, typed by \brle{op}
\item Unary and binary \emph{let-bindings}, typed by \brle{let$_1$} and \brle{let$_2$}
respectively
\item A \emph{pair} of expressions $\hasty{\Gamma}{\epsilon}{a}{A}$,
$\hasty{\Gamma}{\epsilon}{b}{B}$, typed by \brle{pair}. Operationally, we interpret this as
executing $a$, and then $b$, and returning the pair of their values.
\item An empty tuple $()$, which types in any context by \brle{unit}
\item Injections, typed by \brle{inl} and \brle{inr}
\item Pattern matching on sum types, typed by \brle{case}. Operationally, we interpret this as
executing $e$, and then, if $e$ is a left injection $\iota_l\;x$, executing $a$ with its value
($x$), otherwise executing $b$.
\item An operator $\ms{abort}\;e$ allowing us to abort execution if given a value of the empty type. Since the empty type is a 0-ary sum type, $\ms{abort}$ can be seen as a $\ms{case}$ with no branches. Since the empty type is uninhabited, execution can never reach an $\ms{abort}$. This can be viewed as a typesafe version of the \texttt{unreachable} instruction in LLVM IR.
\end{itemize}
Traditional presentations of SSA use a boolean type instead of sum types. Naturally, booleans can be encoded with sum types as $\mb{1} + \mb{1}$. If-then-else is then a $\ms{case}$ which ignores the unit payloads, so that
$\ite{e_1}{e_2}{e_3} := \caseexpr{e_1}{()}{e_2}{()}{e_3}$.
\begin{figure}
\begin{gather*}
\boxed{\hasty{\Gamma}{\epsilon}{a}{A}} \\
\prftree[r]{\rle{var}}{\Gamma\;x \leq (A, \epsilon)}{\hasty{\Gamma}{\epsilon}{x}{A}} \qquad
\prftree[r]{\rle{op}}{\isop{f}{A}{B}{\epsilon}}{\hasty{\Gamma}{\epsilon}{a}{A}}
{\hasty{\Gamma}{\epsilon}{f\;a}{B}} \qquad
\prftree[r]{\rle{let$_1$}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\hasty{\Gamma, \bhyp{x}{A}}{\epsilon}{b}{B}}
{\hasty{\Gamma}{\epsilon}{\letexpr{x}{a}{b}}{B}} \\
\prftree[r]{\rle{unit}}{\hasty{\Gamma}{\epsilon}{()}{\mb{1}}} \qquad
\prftree[r]{\rle{pair}}{\hasty{\Gamma}{\epsilon}{a}{A}}{\hasty{\Gamma}{\epsilon}{b}{B}}
{\hasty{\Gamma}{\epsilon}{(a, b)}{A \otimes B}} \\
\prftree[r]{\rle{let$_2$}}
{\hasty{\Gamma}{\epsilon}{e}{A \otimes B}}
{\hasty{\Gamma, \bhyp{x}{A}, \bhyp{y}{B}}{\epsilon}{c}{C}}
{\hasty{\Gamma}{\epsilon}{\letexpr{(x, y)}{e}{c}}{C}} \\
\prftree[r]{\rle{inl}}{\hasty{\Gamma}{\epsilon}{a}{A}}
{\hasty{\Gamma}{\epsilon}{\linl{a}}{A + B}} \qquad
\prftree[r]{\rle{inr}}{\hasty{\Gamma}{\epsilon}{b}{B}}
{\hasty{\Gamma}{\epsilon}{\linr{b}}{A + B}} \qquad
\prftree[r]{\rle{abort}}{\hasty{\Gamma}{\epsilon}{a}{\mb{0}}}
{\hasty{\Gamma}{\epsilon}{\labort{a}}{A}} \\
\prftree[r]{\rle{case}}
{\hasty{\Gamma}{\epsilon}{e}{A + B}}
{\hasty{\Gamma, \bhyp{x}{A}}{\epsilon}{a}{C}}
{\hasty{\Gamma, \bhyp{y}{A}}{\epsilon}{b}{C}}
{\hasty{\Gamma}{\epsilon}{\caseexpr{e}{x}{a}{y}{b}}{C}}
\end{gather*}
\caption{Rules for typing \isotopessa{} expressions}
\Description{}
\label{fig:ssa-expr-rules}
\end{figure}
We now move on to \emph{regions}, which can be built up as follows:
\begin{itemize}
\item A branch to a label $\ell$ with pure argument $a$, typed with \brle{br}.
\item Unary and binary \emph{let-bindings}, typed by \brle{let$_1$} and \brle{let$_2$}
respectively