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