Skip to content

Commit 6e562b7

Browse files
shadajshadaj
authored
Add initial docs site (metalift#66)
* Add initial docs site * Animate the lift text too * Rename docs -> website * Fix broken link * Improve landing page title * Speed up animation and drop text lifting for now * Add overview and start writing synthesis tutorial * Try to bring back lift animation but reduce lift height
1 parent 8b148ae commit 6e562b7

27 files changed

+22893
-0
lines changed

‎website/.gitignore

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
# Dependencies
2+
/node_modules
3+
4+
# Production
5+
/build
6+
7+
# Generated files
8+
.docusaurus
9+
.cache-loader
10+
11+
# Misc
12+
.DS_Store
13+
.env.local
14+
.env.development.local
15+
.env.test.local
16+
.env.production.local
17+
18+
npm-debug.log*
19+
yarn-debug.log*
20+
yarn-error.log*

‎website/README.md

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
# Website
2+
3+
This website is built using [Docusaurus 2](https://docusaurus.io/), a modern static website generator.
4+
5+
### Installation
6+
7+
```
8+
$ yarn
9+
```
10+
11+
### Local Development
12+
13+
```
14+
$ yarn start
15+
```
16+
17+
This command starts a local development server and opens up a browser window. Most changes are reflected live without having to restart the server.
18+
19+
### Build
20+
21+
```
22+
$ yarn build
23+
```
24+
25+
This command generates static content into the `build` directory and can be served using any static contents hosting service.
26+
27+
### Deployment
28+
29+
Using SSH:
30+
31+
```
32+
$ USE_SSH=true yarn deploy
33+
```
34+
35+
Not using SSH:
36+
37+
```
38+
$ GIT_USER=<Your GitHub username> yarn deploy
39+
```
40+
41+
If you are using GitHub pages for hosting, this command is a convenient way to build the website and push to the `gh-pages` branch.

‎website/babel.config.js

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
module.exports = {
2+
presets: [require.resolve('@docusaurus/core/lib/babel/preset')],
3+
};

‎website/blog/2019-05-28-first-blog-post.md

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
---
2+
slug: first-blog-post
3+
title: First Blog Post
4+
authors: shadaj
5+
tags: [hola, docusaurus]
6+
---
7+
8+
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Pellentesque elementum dignissim ultricies. Fusce rhoncus ipsum tempor eros aliquam consequat. Lorem ipsum dolor sit amet

‎website/blog/authors.yml

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
shadaj:
2+
name: Shadaj Laddad
3+
title: PhD Student @ UC Berkeley
4+
url: https://github.com/shadaj
5+
image_url: https://github.com/shadaj.png

‎website/docs/installation.md

+59
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
---
2+
sidebar_position: 1
3+
---
4+
5+
# Installation
6+
Let's get started by installing Metalift and it's dependencies!
7+
8+
## Get the Metalift source code
9+
First, you'll need to clone the Metalift repository (we are working on making Metalift available as a Python package in the near future):
10+
11+
```bash
12+
git clone https://github.com/metalift/metalift.git
13+
cd metalift
14+
```
15+
16+
## Install the dependencies
17+
- [Racket](https://racket-lang.org) as the underlying language for the synthesis engine
18+
- [Rosette](https://github.com/emina/rosette), the synthesis engine that Metalift uses
19+
- For maximum performance on Apple Silicon machines, you may want to replace the built-in Intel binary for Z3 with a native build
20+
- [CVC5](https://cvc5.github.io/), the theorem prover that Metalift uses to check candidate solutions
21+
- [Clang/LLVM 11](https://llvm.org), to compile input programs to LLVM IR for analysis
22+
- [CMake](https://cmake.org/), to build the custom LLVM pass
23+
24+
### Installation using Nix
25+
If you use [Nix](https://nixos.org/), you can automatically get all these dependencies using the `shell.nix` definition in the base directory of the Metalift repository.
26+
27+
```
28+
$ nix-shell
29+
$ # all dependencies are available!
30+
```
31+
32+
## Build our fork of `llvmlite`
33+
We use a modified version of `llvmlite` to parse and analyze LLVM IR. To build the fork, you'll need to start by cloning the submodule:
34+
35+
```bash
36+
git submodule update --init --recursive
37+
```
38+
39+
Then, you can build the fork:
40+
41+
```bash
42+
cd llvmlite
43+
python setup.py build
44+
cd ..
45+
```
46+
47+
## Build the custom LLVM pass
48+
Metalift makes use of a custom LLVM pass to organize the basic blocks in a way that is easier to analyze. To build the pass, we'll use CMake:
49+
50+
```bash
51+
cd llvm-pass
52+
mkdir build
53+
cd build
54+
cmake ..
55+
make
56+
cd ../..
57+
```
58+
59+
Now, we are ready to start building verified lifting systems with Metalift!

‎website/docs/overview.md

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
---
2+
sidebar_position: 0
3+
---
4+
5+
# Overview
6+
Metalift is a framework for building compilers for domain-specific languages (DSLs). If you are a developer and you want to use a new DSL for your application, you would need to rewrite your code manually, which is often tedious and error-prone. Rather than doing that, you can use Metalift to _generate a compiler_ that translates from your source language to your favorite DSL!
7+
8+
## How does it work?
9+
Metalift is a compiler generator. Unlike traditional syntax-driven compilers, which consists of rules that recognize patterns in the input code and translate them into the target language, Metalift uses [verified lifting](https://homes.cs.washington.edu/~akcheung/papers/pldi16.html) to search for possible candidate programs in the target language that the given input can be
10+
translated to. This frees you from the need to devise, check, and maintain those pesky syntax-driven rules!
11+
12+
To make the search efficient, rather than searching programs that are expressible in the concrete syntax of the target DSL, Metalift searches over the space of programs expressed in a high-level _specification language_ instead. The specification language has a functional language-like syntax (think Haskell) and represents the semantics of the target DSL. See [below](#specLang) for details.
13+
14+
The Metalift toolchain consists of three components, as shown below:
15+
![](/img/docs/overview/arch.png)
16+
17+
First, the input code is parsed into an abstract syntax tree (AST), with each node in the tree representing some part of the input program (e.g., a statement, an expression, etc). After that, Metalift extracts code fragments from the input AST that are amenable for translation to the target DSL. Note that we are not aiming to do whole program transformations here. Given the target being a _domain-specific language_, it is likely that only parts of the input application is expressible using the DSL. You probably don't want to translate the entire application anyway: consider moving computation to the GPU for instance. You probably only want to move the most computationally intensive kernels to the GPU, and leave the rest of your application to remain on the CPU.
18+
19+
Metalift currently has a parser for input programs in LLVM IR, which can be generated from languages like C/C++ and Rust.
20+
21+
Each extracted code fragment is then passed to a program synthesizer (we currently use the [Rosette](https://emina.github.io/rosette/) synthesizer) which searches over the space of programs expressed in the specification language. If a candidate program can be proven to be semantically equivalent to the input (this is currently done using the [CVC5](https://cvc5.github.io) theorem prover), it is then passed over to the code generator. Otherwise, we ask the synthesizer to find another candidate until we run out of programs or it times out.
22+
23+
Each successfully verified candidate program is then processed by the code generator, which translates the candidate program into the concrete syntax of the DSL. The resulting DSL program is then "stitched" back into the original code, with glue code generated to call the generated DSL program as needed. This is illustrated in the diagram above.

‎website/docs/tutorial/_category_.json

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
{
2+
"label": "Tutorial",
3+
"position": 2
4+
}

‎website/docs/tutorial/creating-synthesis-problem.md

+46
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
---
2+
sidebar_position: 1
3+
---
4+
5+
# Solving a Synthesis Problem
6+
Before we dive into an end-to-end verified lifting application, let's familiarize ourselves with the basic concepts in Metalift with a synthesis problem.
7+
8+
Let us synthesize a function $f(x)$ such that for all integer $x$, $f(x) \geq 0$ and $f(x) \geq x$. Formally, we want to solve the following problem: $\exists{f}. \forall x \in \mathbb{N}. f(x) \geq 0 \wedge f(x) \geq x$. The $\forall$ **universal quantifier** is so key to verification that it's in our logo!
9+
10+
## Define the Verification Conditions
11+
The first step to encoding this with Metalift is to define the conditions that we want to verify. These conditions can be specified using the __Metalift IR__, which includes a variety of common operations on types like booleans, integers, lists, and sets that Metalift knows the meaning of.
12+
13+
First, we import the IR package as well as the Metalift types we'll be using in the verification conditions:
14+
15+
```python
16+
from metalift import ir, types
17+
```
18+
19+
Then, we define the verification conditions:
20+
21+
```python
22+
x = ir.Var("x", types.Int())
23+
24+
correct = ir.And(
25+
# f(x) >= 0
26+
ir.Ge(
27+
ir.Call(
28+
'f', # function name
29+
types.Int(), # return type
30+
x # arguments
31+
),
32+
ir.IntLit(0)
33+
),
34+
# f(x) >= x
35+
ir.Ge(
36+
ir.Call('f', types.Int(), x),
37+
x
38+
)
39+
)
40+
```
41+
42+
## Create a Program Grammar
43+
TODO
44+
45+
## Synthesize!
46+
TODO

‎website/docusaurus.config.js

+139
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,139 @@
1+
// @ts-check
2+
// Note: type annotations allow type checking and IDEs autocompletion
3+
4+
const lightCodeTheme = require('prism-react-renderer/themes/github');
5+
const darkCodeTheme = require('prism-react-renderer/themes/dracula');
6+
const math = require('remark-math');
7+
const katex = require('rehype-katex');
8+
9+
/** @type {import('@docusaurus/types').Config} */
10+
const config = {
11+
title: 'Metalift',
12+
tagline: 'A program synthesis framework for verified lifting applications',
13+
url: 'https://metalift.netlify.com',
14+
baseUrl: '/',
15+
onBrokenLinks: 'throw',
16+
onBrokenMarkdownLinks: 'warn',
17+
favicon: 'img/favicon.ico',
18+
organizationName: 'metalift', // Usually your GitHub org/user name.
19+
projectName: 'docusaurus', // Usually your repo name.
20+
21+
presets: [
22+
[
23+
'classic',
24+
/** @type {import('@docusaurus/preset-classic').Options} */
25+
({
26+
docs: {
27+
sidebarPath: require.resolve('./sidebars.js'),
28+
// Please change this to your repo.
29+
editUrl: 'https://github.com/metalift/metalift/tree/llvm/docs',
30+
remarkPlugins: [math],
31+
rehypePlugins: [katex],
32+
},
33+
blog: {
34+
showReadingTime: true,
35+
// Please change this to your repo.
36+
editUrl:
37+
'https://github.com/metalift/metalift/tree/llvm/docs',
38+
},
39+
theme: {
40+
customCss: require.resolve('./src/css/custom.css'),
41+
},
42+
}),
43+
],
44+
],
45+
stylesheets: [
46+
{
47+
href: 'https://cdn.jsdelivr.net/npm/katex@0.13.24/dist/katex.min.css',
48+
type: 'text/css',
49+
integrity:
50+
'sha384-odtC+0UGzzFL/6PNoE8rX/SPcQDXBJ+uRepguP4QkPCm2LBxH3FA3y+fKSiJ+AmM',
51+
crossorigin: 'anonymous',
52+
},
53+
],
54+
55+
themeConfig:
56+
/** @type {import('@docusaurus/preset-classic').ThemeConfig} */
57+
({
58+
navbar: {
59+
title: 'Metalift',
60+
logo: {
61+
alt: 'The Metalift logo (a forall symbol with an upward pointing arrow)',
62+
src: 'img/metalift-icon.svg',
63+
},
64+
items: [
65+
{
66+
type: 'doc',
67+
docId: 'overview',
68+
position: 'left',
69+
label: 'Docs',
70+
},
71+
{to: '/blog', label: 'Blog', position: 'left'},
72+
{
73+
href: 'https://github.com/metalift/metalift',
74+
label: 'GitHub',
75+
position: 'right',
76+
},
77+
],
78+
},
79+
footer: {
80+
style: 'dark',
81+
links: [
82+
{
83+
title: 'Docs',
84+
items: [
85+
{
86+
label: 'Overview',
87+
to: '/docs/overview',
88+
},
89+
{
90+
label: 'Installation',
91+
to: '/docs/installation',
92+
},
93+
{
94+
label: 'Tutorial',
95+
to: '/docs/tutorial/creating-synthesis-problem',
96+
},
97+
],
98+
},
99+
// {
100+
// title: 'Community',
101+
// items: [
102+
// {
103+
// label: 'Stack Overflow',
104+
// href: 'https://stackoverflow.com/questions/tagged/docusaurus',
105+
// },
106+
// {
107+
// label: 'Discord',
108+
// href: 'https://discordapp.com/invite/docusaurus',
109+
// },
110+
// {
111+
// label: 'Twitter',
112+
// href: 'https://twitter.com/docusaurus',
113+
// },
114+
// ],
115+
// },
116+
{
117+
title: 'More',
118+
items: [
119+
{
120+
label: 'Blog',
121+
to: '/blog',
122+
},
123+
{
124+
label: 'GitHub',
125+
href: 'https://github.com/metalift/metalift',
126+
},
127+
],
128+
},
129+
],
130+
copyright: `Copyright © ${new Date().getFullYear()} UC Berkeley. Built with Docusaurus.`,
131+
},
132+
prism: {
133+
theme: lightCodeTheme,
134+
darkTheme: darkCodeTheme,
135+
},
136+
}),
137+
};
138+
139+
module.exports = config;

0 commit comments

Comments
 (0)