LINKS
author Christian Urban <urbanc@in.tum.de>
Mon, 22 Oct 2018 23:37:11 +0100
changeset 582 cd7a08469b3c
parent 570 49053023bb7e
child 595 d062fb6feefd
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
     1
Compiler courses
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
     2
http://www.cse.chalmers.se/edu/year/2017/course/TDA283/lectures/
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
     3
http://www.cs.columbia.edu/~sedwards/classes/2017/4115-fall/index.html
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
     4
http://www.cs.dartmouth.edu/~mckeeman/cs48/index.html
553
a05c412b1550 updated
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
     5
http://www.cl.cam.ac.uk/teaching/1718/CompConstr/materials.html
555
85f4eeefaea5 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
     6
85f4eeefaea5 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
     7
85f4eeefaea5 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
     8
http://spivey.oriel.ox.ac.uk/corner/Welcome_to_Spivey%27s_Corner
85f4eeefaea5 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
     9
http://spivey.oriel.ox.ac.uk/corner/Compilers_(The_Farewell_Tour)
85f4eeefaea5 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    10
http://spivey.oriel.ox.ac.uk/wiki2/files/compilers/book.pdf
85f4eeefaea5 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    11
http://spivey.oriel.ox.ac.uk/corner/Programming_Languages
85f4eeefaea5 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    12
556
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    13
http://www.cs.cornell.edu/courses/cs3110/2015fa/index.php#Assignments
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    14
Magnus
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    15
http://www.cse.chalmers.se/edu/course/TDA283/
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    16
Pfenning
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    17
https://www.cs.cmu.edu/~fp/courses/15411-f14/
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    18
https://www.cs.cmu.edu/~fp/courses/15411-f13/lectures/
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    19
https://www.cs.cmu.edu/~fp/courses/15411-f14/lectures/
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    20
===============================
570
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    21
Compiler book links
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    22
https://www.reddit.com/r/ProgrammingLanguages/comments/9k2hfd/introduction_to_compilers_and_language_design/
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    23
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    24
http://www.craftinginterpreters.com
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    25
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    26
Book about SSA
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    27
http://ssabook.gforge.inria.fr/latest/book-full.pdf
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    28
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    29
http://cs.lmu.edu/~ray/notes/ir/
Christian Urban <urbanc@in.tum.de>
parents: 557
diff changeset
    30
===============================
556
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    31
Selfhosting Lisp compiler for Lua
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    32
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    33
https://github.com/sctb/lumen
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    34
============================
4b0fffaef849 updated
Christian Urban <urbanc@in.tum.de>
parents: 553
diff changeset
    35
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    36
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    37
Pictures from the Starting Forth book
546
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    38
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    39
https://www.forth.com/starting-forth/2-stack-manipulation-operators-arithmetic/
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    40
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    41
--------------------------------
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    42
Java Byte Code for SCALA
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    43
https://www.toptal.com/scala/scala-bytecode-and-the-jvm
546
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    44
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    45
------------------
546
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    46
Yeti - ML for the JVM
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    47
https://mth.github.io/yeti/
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    48
http://dot.planet.ee/yeti/intro.html
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    49
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    50
------------------
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    51
Ocaml for LLVM
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    52
https://github.com/artagnon/rhine-ml 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    53
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    54
---------------
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    55
Type inference 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    56
http://www.calebh.io/Type-Inference-by-Solving-Constraints/
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    57
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
    58
546
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    59
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    60
JVM languages
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    61
https://en.wikipedia.org/wiki/List_of_JVM_languages
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    62
https://www.codeproject.com/Articles/50377/Create-Your-Own-Programming-Language
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    63
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    64
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    65
Scheme
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    66
https://wespiser.com/writings/wyas/home.html
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    67
http://peter.michaux.ca/index#Scheme
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    68
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    69
b2db644b7442 updated
Christian Urban <urbanc@in.tum.de>
parents: 495
diff changeset
    70
476
147a5560efd7 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
assmebly (calculator RPN)
147a5560efd7 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
147a5560efd7 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
https://dere.github.io/2017-02-12/beginners-assembly-part1/
147a5560efd7 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
147a5560efd7 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
477
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    76
webassembly
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    77
https://sourceware.org/ml/binutils/2017-03/msg00044.html
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    78
https://hacks.mozilla.org/2017/02/a-cartoon-intro-to-webassembly/
495
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    79
https://webassembly.github.io/spec/
477
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    80
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    81
webassembly explorer
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    82
https://mbebenita.github.io/WasmExplorer/
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    83
495
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    84
ARM
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    85
https://azeria-labs.com/writing-arm-assembly-part-1/
477
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    86
495
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    87
JVM
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    88
https://www.toptal.com/scala/scala-bytecode-and-the-jvm
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    89
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    90
Growing a compiler
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    91
http://www.cs.dartmouth.edu/~mckeeman/cs48/mxcom/gem/html/GrowingCompiler.html
477
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    92
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    93
free books
28e872e7efb3 updated
Christian Urban <urbanc@in.tum.de>
parents: 476
diff changeset
    94
https://github.com/vhf/free-programming-books/blob/master/free-programming-books.md
495
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    95
https://john.cs.olemiss.edu/~hcc/csci658/notes/Free_Prog_Lang_Textbooks.html
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    96
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    97
MIPS
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    98
http://courses.missouristate.edu/kenvollmar/mars/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
    99
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   100
PEG
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   101
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   102
https://github.com/taocpp/PEGTL
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   103
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   104
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   105
Parser
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   106
https://www.reddit.com/r/programming/comments/615hoz/how_to_write_a_recursive_descent_parser/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   107
https://www.reddit.com/r/ProgrammingLanguages/comments/60gmgc/writing_a_recursive_descent_expression_parser/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   108
http://www.craftinginterpreters.com/parsing-expressions.html
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   109
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   110
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   111
small languages
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   112
https://github.com/Michael2109/cobalt
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   113
http://www.red-lang.org/p/about.html
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   114
http://craftinginterpreters.com/contents.html
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   115
https://michaelhaywoodblog.wordpress.com
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   116
https://ruslanspivak.com/lsbasi-part1/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   117
http://selfie.cs.uni-salzburg.at
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   118
https://academy.realm.io/posts/tryswift-samuel-giddins-building-tiny-compiler-swift-ios/
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   119
https://legacy.gitbook.com/book/luxlang/the-lux-programming-language/details
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   120
https://github.com/rhysd/gocaml
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   121
https://github.com/aalhour/awesome-compilers#educational-and-toy-projects
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   122
https://rsms.me/hue-intro
495
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   123
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   124
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   125
automata
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   126
https://www7.in.tum.de/um/courses/auto/ws1314/script/autonotes.pdf
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   127
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   128
Reges helpers
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   129
https://regex101.com
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   130
http://www.regular-expressions.info/tutorial.html
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   131
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   132
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   133
Regex performance benchmark
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   134
https://rust-leipzig.github.io/regex/2017/03/28/comparison-of-regex-engines/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   135
https://github.com/k-takata/Onigmo
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   136
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   137
Sulzmann
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   138
https://github.com/pippijn/dreml/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   139
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   140
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   141
Scala parser
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   142
http://enear.github.io/2016/03/31/parser-combinators/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   143
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   144
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   145
ANTLR megatutorial
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   146
https://tomassetti.me/antlr-mega-tutorial/
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   147
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   148
From regex to LLVM
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   149
https://www.youtube.com/watch?v=Ukqb6nMjFyk
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   150
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   151
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   152
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   153
acd4567735ce updated
Christian Urban <urbanc@in.tum.de>
parents: 477
diff changeset
   154
Static code analysis
550
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   155
https://medium.com/@Coder_HarryLee/videos-about-static-code-analysis-7654b40f9a3b
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   156
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   157
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   158
Brainfuck compiler
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   159
https://github.com/PurpleMyst/bf_compiler
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   160
https://www.reddit.com/r/programming/comments/8371tk/a_brainfuck_to_llvm_ir_compiler_written_in_python/
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   161
http://www.wilfred.me.uk/blog/2015/02/21/my-first-llvm-compiler/
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   162
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   163
===============================
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   164
A simple recursive regular expression matcher written in Scala.
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   165
https://github.com/marconilanna/RegexMatcher
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   166
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   167
===============================
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   168
A neat little tool to build presentations using the Scala REPL
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   169
https://github.com/marconilanna/REPLesent
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   170
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   171
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   172
======================
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   173
Minimal Static Single Assignment Form
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   174
Max Wagner and Denis Lohner
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   175
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   176
This formalization is an extension to "Verified Construction of Static Single 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   177
Assignment Form". In their work, the authors have shown that Braun et al.'s 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   178
static single assignment (SSA) construction algorithm produces minimal SSA form 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   179
for input programs with a reducible control flow graph (CFG). However Braun et 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   180
al. also proposed an extension to their algorithm that they claim produces 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   181
minimal SSA form even for irreducible CFGs.
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   182
In this formalization we support that claim by giving a mechanized proof.
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   183
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   184
As the extension of Braun et al.'s algorithm aims for removing so-called 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   185
redundant strongly connected components of phi functions, we show that this 
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   186
suffices to guarantee minimality according to Cytron et al..
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   187
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   188
https://www.isa-afp.org/entries/Minimal_SSA.shtml
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   189
a62357075346 updated
Christian Urban <urbanc@in.tum.de>
parents: 546
diff changeset
   190
553
a05c412b1550 updated
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   191
=========================
a05c412b1550 updated
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   192
How Clang compiles a function
a05c412b1550 updated
Christian Urban <urbanc@in.tum.de>
parents: 550
diff changeset
   193
https://blog.regehr.org/archives/1605