We are currently working on support for LLVM 8. Luckily, moving to LLVM 8 does not seem to break too many things in PhASAR. We fixed all breaking changes in the
llvm-8.0.0 branch on Github (https://github.com/secure-software-engineering/phasar/tree/llvm-8.0.0). One of the changes made to LLVM 8 worth mentioning is the removal of the terminator instruction class
llvm::TerminatorInst. Instead of using
llvm::isa, one has to use
bool llvm::Instruction::isTerminator() const in order to check for terminator instructions. After being able to successfully compile and link PhASAR against LLVM 8, we are now checking the semantically correctness of the analysis framework in combination with LLVM 8. The
llvm-8.0.0 branch will be promptly merged into
development after having assessed the semantically correctness.
Due to the many friendly emails that we received, it came to our attention that people do not only wish to use PhASAR as a standalone static analysis tool for general purpose and security data-flow analysis, but also wish to build performance optimizations based on PhASAR’s inter-procedural static analysis results.
For this reason, we are currently building a full-LTO pass that wraps PhASAR’s functionalities into an ordinary LLVM pass. Thus, we allow a tighter coupling between LLVM and PhASAR; other LLVM optimization passes will be able to directly access PhASAR inter-procedural static analysis information that may allow more aggressive performance optimizations.
In order to be able to perform code transformations based on static analysis, the analysis must be sound. For other applications—including security analysis—soundy analyses might be sufficient (A soundy analysis uses sensible under-approximations to cope with certain language features such as C’s setjmp()/longjmp() that would otherwise degrade precision.). Hence, we will add a new option to PhASAR that allows to control the level of soundness.
The latest version of PhASAR v1218 is now available. Please check https://github.com/secure-software-engineering/phasar/wiki/PhASAR’s-Releases for details. Among other features, we added infrastructure for backward control-flow graphs. These graphs can be used in order to solve backward data-flow problems.
Today, we will release a minor update (1018) that includes various bug fixes, improved code quality, as well as some minor changes in the API (mostly renaming).
In addition, we will switch to a monthly release plan to avoid expensive, breaking changes and to keep our users up-to-date.
Next week we will release a major update that includes various bug fixes, faster compiles, heavy performance optimizations and novel features. To take just one small example, we were able to reduce the overall runtime of a complete analysis run on clang from several hours to several minutes.
The slides and the analysis code of our taint analysis toy-example, that we presented at our tutorial, are now available at phasar.org/download.
We have prepared the material for our tutorial given @PLDI 2018. If you participate in the tutorial, we kindly ask you to install Phasar on your machine before the tutorial, so we can get right into working with it from the start in order to maximize your learning experience. As many C++ projects Phasar does have a considerable compile time and we would like you to be productive from the very beginning and not to wait for the compiler to be done. Also some of our provided pre-packaged options for the tutorial are quite large, so we would like you to download and install your preferred option ahead of time.
There are three options to work with Phasar during the tutorial:
1. Using a VirtualBox VM
2. Using a Docker container
3. With a cloned copy of the source code
Please have a detailed look at phasar.org/tutorial and phasar.org/download.
We are looking forward to an interesting tutorial with you.
We will present the Phasar framework at the PLDI 2018 conference held in Philadelphia, Pennsylvania, United States.
We have implemented Phasar, a novel static-analysis framework on top of LLVM. Phasar provides various solvers that allow the solving of arbitrary monotone data-flow problems (distributive or not) in a fully automated manner. A user just has to provide the specific description of the problem to solve.
Phasar’s solver supports a context and flow-sensitive analysis, which is notoriously hard to scale.
Also, the C and C++ programming languages make it especially hard to statically analyze. This is due to their deliberately unsafe type system, function pointers and in case of C++ virtual dispatch and other powerful language constructs.
We will explain how Phasar uses summaries, tabulation and a compositional analysis approach to nevertheless scale to actual applications with millions of lines of code.
We will give an introduction to the framework, explain its relationship to LLVM, its architecture, and give hands-on examples of how to implement useful example analyses with Phasar. For the examples we will focus on security applications.
Before the tutorial, we will release Phasar as a well documented open-source project on Github.