-
Notifications
You must be signed in to change notification settings - Fork 82
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
145 changed files
with
23,938 additions
and
1,429 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -9,161 +9,49 @@ additions and extensions to SMACK relatively easy. Furthermore, the open | |
| architecture of SMACK encourages prototyping custom software verifiers on top | ||
| of SMACK. | ||
|
|
||
| ## A Quick Demo | ||
|
|
||
| ## Requirements | ||
| SMACK can verify C programs, such as the following: | ||
|
|
||
| ### Dependencies | ||
| // simple.c | ||
| #include "smack.h" | ||
|
|
||
| SMACK depends on the following projects: | ||
| * [LLVM](http://www.llvm.org) (release [3.2](http://llvm.org/releases/download.html#3.2)), | ||
| [clang](http://clang.llvm.org) (release [3.2](http://llvm.org/releases/download.html#3.2)) | ||
| * [Boogie](http://boogie.codeplex.com), [Z3](http://z3.codeplex.com/) | ||
| * [Python](http://www.python.org) (version 2.7) | ||
| int incr(int x) { | ||
| return x + 1; | ||
| } | ||
|
|
||
| To configure, build, and install LLVM and clang, follow their [Getting Started | ||
| Quickly](http://llvm.org/docs/GettingStarted.html#getting-started-quickly-a-summary) | ||
| summary. You have to build and install LLVM and clang from sources since SMACK | ||
| does not build properly with their packaged versions. SMACK supports only major | ||
| LLVM releases and not the latest version found on its Subversion repository. | ||
| Therefore, instead of checking out LLVM from SVN, download its sources for the | ||
| required release as noted above. | ||
| int main(void) { | ||
| int a; | ||
|
|
||
| ### Supported Platforms | ||
| a = 1; | ||
| a = incr(a); | ||
| __SMACK_assert(a == 2); | ||
| return 0; | ||
| } | ||
|
|
||
| SMACK is known to work on the following platforms: | ||
| * Linux (Ubuntu) | ||
| * MacOS | ||
| * Cygwin | ||
| To do so, SMACK invokes [Clang](http://clang.llvm.org) to compile `simple.c` | ||
| into LLVM bitcode `simple.bc`: | ||
|
|
||
| **Note for Cygwin users:** | ||
| You should configure LLVM/clang with the --enable-shared option (which may also | ||
| require the --enable-optimized option). Then when configuring SMACK you should | ||
| use these options as well. | ||
| clang -c -Wall -emit-llvm -O0 -g -I../../include/smack simple.c -o simple.bc | ||
|
|
||
| then translates the bitcode `simple.bc` to a program in the | ||
| [Boogie](http://boogie.codeplex.com) verification language, | ||
|
|
||
| ## Getting Started Quickly (on Linux) | ||
| smackgen.py simple.bc -o simple.bpl | ||
|
|
||
| To get you started with SMACK quickly, we provide a reference installation | ||
| script that downloads and installs Z3, Boogie, LLVM/clang, and SMACK. Simply | ||
| download | ||
| [build-linux.sh](http://github.com/smackers/smack/blob/master/bin/build-linux.sh) | ||
| and execute it. | ||
| and finally verifies `simple.bpl` with the [Boogie Verifier](http://boogie.codeplex.com) | ||
|
|
||
| Note that this script is primarily provided as a reference and we do not expect | ||
| it will work out-of-the-box on all platforms and required software | ||
| combinations. You can still give it a try and modify it based on your specific | ||
| needs. | ||
| Boogie simple.bpl | ||
|
|
||
| **Known problems:** | ||
| Z3 source code cannot be cloned from codeplex using git sometimes. This is a | ||
| known | ||
| [problem](http://z3.codeplex.com/wikipage?title=Git%20HTTPS%20cloning%20errors). | ||
| In that case you can manually download Z3's sources from its codeplex site. | ||
| concluding that the original program `simple.c` is verified to be correct. | ||
| While SMACK is designed to be a *modular* verifier, for our convenience, this | ||
| whole process has also been wrapped into a single command in SMACK: | ||
|
|
||
| smack-verify.py simple.c -o simple.bpl | ||
|
|
||
| which equally reports that the program `simple.c` is verified. | ||
|
|
||
| ## Getting Started with SMACK | ||
|
|
||
| ### Installation Guide | ||
|
|
||
| 1. Checkout SMACK: | ||
|
|
||
| ``` | ||
| cd where-you-want-smack-source-to-live | ||
| git clone [email protected]:smackers/smack.git | ||
| ``` | ||
|
|
||
| 2. Configure SMACK: | ||
|
|
||
| ``` | ||
| cd where-you-want-to-build-smack | ||
| mkdir build (for building without polluting the source dir) | ||
| cd build | ||
| ../smack/configure --with-llvmsrc=<directory> --with-llvmobj=<directory> --prefix=<directory> | ||
| ``` | ||
|
|
||
| Options for configure are: | ||
| * --with-llvmsrc=<directory> : Tell SMACK where the LLVM source tree is located [required]. | ||
| * --with-llvmobj=<directory> : Tell SMACK where the LLVM object tree is located [required]. | ||
| * --prefix=<directory> : Specify full pathname of where you want SMACK installed [required]. | ||
| * --enable-optimized : Compile with optimizations enabled [default is NO]. | ||
| * --enable-assertions : Compile with assertion checks enabled [default is YES]. | ||
|
|
||
| 3. Build and install SMACK: | ||
|
|
||
| ``` | ||
| make | ||
| make install | ||
| ``` | ||
|
|
||
| If everything goes well, you should now have lib/libsmack.a and lib/smack.so | ||
| (or smack.dylib on MacOS, or smack.dll on Cygwin) in the SMACK installation | ||
| directory. | ||
|
|
||
| 4. Create an environment variable called BOOGIE containing a Boogie invocation | ||
| command for your platform. For example: | ||
|
|
||
| ``` | ||
| export BOOGIE="mono /home/john/Boogie/Binaries/Boogie.exe" | ||
| ``` | ||
|
|
||
| **Important note:** | ||
| LLVM/clang binaries (e.g., clang, llvm-link, opt) should all be in your path, | ||
| as well as your smack-install-dir/bin directory! | ||
|
|
||
|
|
||
| ### Running Regression Tests | ||
|
|
||
| To make sure SMACK has been installed properly, run its regression tests. | ||
| Go to smack/test directory and compile the regression tests by running | ||
| `make`. You should get a number of LLVM bitcode files, one per test. | ||
| Execute the regression test script with `./regtest.py`. All tests should pass. | ||
|
|
||
|
|
||
| ## SMACK Tools | ||
|
|
||
| Currently, SMACK comes with the following tools in the bin directory: | ||
| * llvm2bpl is a bare-bone translator from LLVM bitcode into Boogie. | ||
| * smack-check is tool for statically checking properties of programs written in | ||
| C/C++. For a given input program, the tool checks for violations of | ||
| user-provided assertions. | ||
|
|
||
| Type `llvm2bpl.py -h` or `smack-check.py -h` for a full list of supported | ||
| command line options. | ||
|
|
||
|
|
||
| ## The SMACK Checker User Guide | ||
|
|
||
| Next, we illustrate how to check the following simple C program using the SMACK | ||
| checker: | ||
| ``` | ||
| // simple.c | ||
| #include "smack.h" | ||
| int incr(int x) { | ||
| return x + 1; | ||
| } | ||
| int main(void) { | ||
| int a; | ||
| a = 1; | ||
| a = incr(a); | ||
| __SMACK_assert(a == 2); | ||
| return 0; | ||
| } | ||
| ``` | ||
| Note that this example can also be found in the smack/examples/simple | ||
| directory. | ||
|
|
||
| First, compile the example into an LLVM bitcode file using clang: | ||
| ``` | ||
| clang -c -Wall -emit-llvm -O0 -g -I../../headers simple.c -o simple.bc | ||
| ``` | ||
| We use the -g flag to compile with debug information enabled, which the SMACK | ||
| checker leverages to generate more informative error traces. | ||
| Then, run the SMACK checker on the generated bitcode file: | ||
| ``` | ||
| smack-check.py simple -o simple.bpl | ||
| ``` | ||
| SMACK should report no errors for this example. | ||
| ## Further Information | ||
|
|
||
| For requirements, installation, usage, and whatever else, please consult the | ||
| [SMACK Wiki on Github](https://github.com/smackers/smack/wiki). | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.