From 2c353d3ad4f5b98641b71acb83ed56597234e814 Mon Sep 17 00:00:00 2001 From: Jack J Garzella Date: Fri, 29 Jun 2018 09:02:08 -0700 Subject: [PATCH 1/2] Add documentation for multi-langauge verification Update the README to reflect that SMACK now supports many languages Add a short tutorial on how to compile a new language into SMACK. --- README.md | 10 +++++++--- docs/language.md | 50 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 57 insertions(+), 3 deletions(-) create mode 100644 docs/language.md diff --git a/README.md b/README.md index 0367ec47d..484716d83 100644 --- a/README.md +++ b/README.md @@ -15,9 +15,12 @@ Under the hood, SMACK is a translator from the [LLVM](http://www.llvm.org) compiler's popular intermediate representation (IR) into the [Boogie](https://github.com/boogie-org/boogie) intermediate verification language (IVL). Sourcing LLVM IR exploits an increasing number of compiler front-ends, -optimizations, and analyses. Currently SMACK only supports the C language via -the [Clang](http://clang.llvm.org) compiler, though we are working on providing -support for additional languages. Targeting Boogie exploits a canonical +optimizations, and analyses. Currently SMACK robustly supports the C language +(and experimentally, C++ and Objective-C) via the [Clang](http://clang.llvm.org) compiler. +We are in the process of adding support for FORTRAN +(via [Flang](https://github.com/flang-compiler/flang)), Rust, and Swift. +In general, any AoT comipler that targets LLVM can be used with SMACK +(see the [tutorial](docs/language.md)). Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation. Currently, SMACK leverages the [Boogie](https://github.com/boogie-org/boogie) and [Corral](https://github.com/boogie-org/corral) @@ -60,6 +63,7 @@ SMACK. 1. [Demos](docs/demos.md) 1. [FAQ](docs/faq.md) 1. [Inline Boogie Code](docs/boogie-code.md) +1. [Other Languages](docs/langauge.md) 1. [Contribution Guidelines](CONTRIBUTING.md) 1. [Projects](docs/projects.md) 1. [Publications](docs/publications.md) diff --git a/docs/language.md b/docs/language.md new file mode 100644 index 000000000..8064d808b --- /dev/null +++ b/docs/language.md @@ -0,0 +1,50 @@ + +# How to use SMACK with your own programming language. + +SMACK can be used to verify any langauge that comiples to LLVM IR. Because there are so many languages, we are unable to provide out-of-the-box for the majority of LLVM languages. However, you can still verify code by manually compiling to LLVM and running SMACK on the LLVM IR. + +### Prerequisites + +- An AoT compiler that targets the same version of LLVM as SMACK. + +For compatibility, SMACK version == LLVM version - 2. So, for LLVM 3.9, you want SMACK 1.9, etc. + +- A working C interop + +### Tutorial + +Step 1: Import smack.h using C interop + +You can use the functions smack.h to call verifier operations like `__VERIFIER_assert`. + +Step 2: Compile to LLVM IR + +Compile your code to either a .ll or a .bc file (the two formats are equivalent). Most compilers provide a command-line option like `-emit-llvm` or `-output-ll`. You should also add debug symbols, which is `-g` on most compilers. Disabling optimizations may also be useful, with `-O0` or similar. + +Step 3: Find the entry point + +Inspect the code to find the `main` function or equivalent entry point. Add `--entry-points [mainfunction]` whenever you call SMACK if this is anything other than `main`. + +If you chose to compile your program into a .bc, you can use llvm-dis and llvm-as to convert between bitcode and human-readable format. + +Step 4: Run SMACK! + +Now, you can run SMACK on your .ll or .bc file. There may be small bugs if your compiler uses LLVM features that aren't used by current languages. If there are any problems, feel free to open an issue. + +### Example commands + +#### Clang + +`clang -S -g -O0 -emit-llvm program.c` + +Note: as flang implements the same compiler options as clang, we can compile FORTRAN for SMACK with + +`flang -S -g -O0 -emit-llvm program.f90` + +#### Swift + +`swiftc -g -emit-ir -import-objc-header smack.h program.swift > program.ll` + +#### D + +`ldc2 -g -O0 -output-ll program.d` From 57a2b71a86dece1c7a6d66bced4ca17da0bc8105 Mon Sep 17 00:00:00 2001 From: Jack J Garzella Date: Sat, 4 Aug 2018 10:32:42 -0700 Subject: [PATCH 2/2] Update language and line widths --- README.md | 2 +- docs/language.md | 45 +++++++++++++++++++++++++++++++++------------ 2 files changed, 34 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index 484716d83..30b771b7e 100644 --- a/README.md +++ b/README.md @@ -19,7 +19,7 @@ optimizations, and analyses. Currently SMACK robustly supports the C language (and experimentally, C++ and Objective-C) via the [Clang](http://clang.llvm.org) compiler. We are in the process of adding support for FORTRAN (via [Flang](https://github.com/flang-compiler/flang)), Rust, and Swift. -In general, any AoT comipler that targets LLVM can be used with SMACK +In general, any Ahead of Time comipler that targets LLVM can be used with SMACK (see the [tutorial](docs/language.md)). Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation. Currently, SMACK leverages the diff --git a/docs/language.md b/docs/language.md index 8064d808b..14c39dc70 100644 --- a/docs/language.md +++ b/docs/language.md @@ -1,35 +1,55 @@ -# How to use SMACK with your own programming language. +# Using SMACK with your favorite programming language. -SMACK can be used to verify any langauge that comiples to LLVM IR. Because there are so many languages, we are unable to provide out-of-the-box for the majority of LLVM languages. However, you can still verify code by manually compiling to LLVM and running SMACK on the LLVM IR. +In theory, SMACK can be used to verify any langauge that compiles to LLVM IR. +In practice, due to language-specific peculiarities, it is not always clear how +well SMACK will work on any given language. However, our experience has been +positive, especially with C-family languages. + +Currently, we have rudimentary SMACK bindings for the following languages: +C, C++, Rust, D, FORTRAN, and Objective-C. This document is for users of other +languages, or users who need more than what SMACK provides in one of the listed +examples. ### Prerequisites -- An AoT compiler that targets the same version of LLVM as SMACK. +- An Ahead of Time compiler that targets the same version of LLVM as SMACK. -For compatibility, SMACK version == LLVM version - 2. So, for LLVM 3.9, you want SMACK 1.9, etc. +For compatibility, SMACK version == LLVM version - 2. So, for LLVM 3.9, +you want SMACK 1.9, etc. -- A working C interop +- A way of importing C headers and calling C functions from your language ### Tutorial -Step 1: Import smack.h using C interop +Step 1: Import smack.h using the C-import functionality -You can use the functions smack.h to call verifier operations like `__VERIFIER_assert`. +You can use the functions smack.h to call verifier operations like +`__VERIFIER_assert`. Note that functions in smack.h follow the C style +of using integers as booleans, so it may be good to write a wrapper that +takes advantage of your language's first-class boolean type. Step 2: Compile to LLVM IR -Compile your code to either a .ll or a .bc file (the two formats are equivalent). Most compilers provide a command-line option like `-emit-llvm` or `-output-ll`. You should also add debug symbols, which is `-g` on most compilers. Disabling optimizations may also be useful, with `-O0` or similar. +Compile your code to either a .ll or a .bc file (the two formats are equivalent). +Most compilers provide a command-line option like `-emit-llvm` or `-output-ll`. +You should also add debug symbols, which is `-g` on most compilers. +Disabling optimizations may also be useful, with `-O0` or similar. Step 3: Find the entry point -Inspect the code to find the `main` function or equivalent entry point. Add `--entry-points [mainfunction]` whenever you call SMACK if this is anything other than `main`. +Inspect the code to find the `main` function or equivalent entry point. Add +`--entry-points [mainfunction]` whenever you call SMACK if this is anything +other than `main`. -If you chose to compile your program into a .bc, you can use llvm-dis and llvm-as to convert between bitcode and human-readable format. +If you chose to compile your program into a .bc, you can use llvm-dis and +llvm-as to convert between bitcode and human-readable format. Step 4: Run SMACK! -Now, you can run SMACK on your .ll or .bc file. There may be small bugs if your compiler uses LLVM features that aren't used by current languages. If there are any problems, feel free to open an issue. +Now, you can run SMACK on your .ll or .bc file. There may be small bugs if your +compiler uses LLVM features that aren't used by current languages. If there +are any problems, feel free to open an issue. ### Example commands @@ -37,7 +57,8 @@ Now, you can run SMACK on your .ll or .bc file. There may be small bugs if your `clang -S -g -O0 -emit-llvm program.c` -Note: as flang implements the same compiler options as clang, we can compile FORTRAN for SMACK with +Note: as flang implements the same compiler options as clang, we can compile +FORTRAN for SMACK with `flang -S -g -O0 -emit-llvm program.f90`