This repository supports the quantification of STG constraints. It consists of a library for manipulating constraints generated by the STG instrumentation component STG-I, tools for simplifying constraints, translators for target quantification tools, and tools for aggregating quantification results.
STG constraints are defined by a grammar written in ANTLR4. A constraint consists of a dictionary which defines set of symbol definitions (a name, type, and initial value) and a boolean expression written in terms of symbols, constants, and the operators defined by the grammar.
Operators in STG constraints are designed to reflect those that are implemented in LLVM instructions and comparisons. Only the operators that are applied to values computed in terms of program inputs are supported. For example, pointer manipulating instructions such as GEP are not supported since they operate on addresses to which values are stored and not the values themselves. More generally, operators manipulating l-values are not be supported.
The constraint [ S0:i32 = 7 ] (slt S0 (i32 10)) expresses that a signed 32-bit Integer symbol, S0, is less than 10. Additional constraint examples are in the test sub-directories. By convention we use an .stg suffix for files with the textual encoding of an STG constraint.
The library is implemented in C++ using an ANTLR4 generated lexer, parser, and parse-tree visitor.
This project uses cmake to manage the build process. The CMakeLists.txt file configures the ANTLR4 and Cpp build process, e.g., source files, targets, libraries, etc. The file requires 3.13 of cmake.
We follow the cmake build model for the ANTLR4 Cpp target. The cmake directory stores ANTLR4 related cmake files.
You will need to adjust the path to the jar file that ANTLR4 uses (antlr-4.8-complete.jar) which is hardcoded in CMakeLists.txt. Note that if the normal install of antlr4 doesn't provide you with this file, then you can download it from the ANTLR4 download site and place it wherever you like, e.g., $HOME/lib, and then point to it from CMakeLists.txt.
We use the llvm command line parsing library. To install it on linux run the following:
apt-get install libllvm-10-ocaml-dev libllvm10 llvm-10 llvm-10-dev llvm-10-doc llvm-10-examples llvm-10-runtime
as super user.
You need to create a build directory at the top-level of this project, i.e., .../STG-Q/build, within which you will build the project. To get started you should create that, empty, build directory if it doesn't exist. All of the generated runtime files for ANTLR4 will be built the first time and stored in the build directory; this may take some time.
To build the libraries and executable:
mkdir buildcd buildcmake ..makemake install
NB: You may see warnings related to ignored type attribute ATN that are due to some type gymnastics in the current implementation of the ANTLR4 CPP Visitor implementation.
This will produce two executables:
build/stgpp: takes the name of a.stgfile, parses it, and pretty print its contents to stdout.build/stg2qc: takes the name of an.stgfile, parses it, and prints the constraint in a form that can be accepted by theqCoralcounter.
stgpp supports pretty printing, type checking, and constant folding by default. The latter features can be disabled with command line options:
OVERVIEW: stgpp - STG constraint pretty printer with type checking and constant folding
USAGE: stgpp [options] <stg source file>
OPTIONS:
Generic Options:
--help - Display available options (--help-hidden for more)
--help-list - Display list of available options (--help-list-hidden for more)
--version - Display the version of this program
stgpp Options:
Options for controlling STG constraint pretty printing.
--no-constant-folding - disable constant folding
--no-type-checking - disable type checking
--verbose - verbose mode
The include directory stores the header files needed by translators and other constraint manipulating tools. The library source has the source code for the library components including the grammar file, ConstraintGrammar.g4. Generating a parser from this file produces a number of ANTLR4 generated files. These are not under configuration management and are stored in the build directory once generated.
Constraint.{h,cpp} define the core data structure. The core type is
Constraint::Constraint which stored the dictionary information and
an constraint expression. Constraint expressions are instances of
subtypes of Constraint::Expr, the base class, and generally are
constituted by a tree of such expressions. To reduce duplication
of symbols, Constraint::Symbol, in expressions their definitions
are interned. Arbitrary expressions could be interned since they
are side-effect free, but this has not been implemented.
ConstraintBuilder.{h,cpp} implements a subtype of an ANTLR4 parse-tree
visitor. It traverses the parse-tree and constructs an instance of
Constraint::DictExpr.
Once built a Constraint::Constraint structure can be processed by
subtyping ConstraintVisitor, defined in ConstraintVisitor.h.
ConstraintPrinter.{h,cpp} is one such visitor that pretty prints
a constraint. QCoralPrinter.{h.cpp} for the qcoral target
is another example of a constraint visitor.
There are several scripts that are useful for simplifying sets of constraints.
src/tools/stgred.sh accepts the name of a directory and prints the names of redundant .stg files. It does this by performing some preprocessing, e.g., dropping the dictionary, and then diffing the constraints; implemented in src/tools/stgdiff.sh.
These tools should be installed in a directory and the shell variable STGINSTALL should be set to that directory's path. This is how these STG scripting tools reference one another.
Tests for the library itself are run using the script run.sh in test/lib.
Tests for the STG tools are run using the script run.sh in test/tools.
These test provide a non-trivial degree of coverage, but they are incomplete.
Each target is expected to provide its own run.sh script to test its translator and associated tools.
We know that there will not be a direct one-to-one mapping from STG constraint operators and types into the input languages of all targets.
There are several strategies that we can use to address this:
- throw an
Unsupportedassertion (this is the minimal behavior) - rewrite an operator into an equivalent expression
- rewrite an operator into an underapproximating expression
- rewrite an operator into an overapproximating expression
For the last two cases, translators should record a series of log messages, e.g., in comments embedded into the translated constraint, documenting the approximations. Downstream tools might consume these to provide information about the fidelity of any computed results from the translated expressions.
- RealPaver
- Download RealPaver: http://pagesperso.lina.univ-nantes.fr/~granvilliers-l/realpaver/src/realpaver-0.4.tar.gz
- Run "tar -xzvf realpaver-0.4.tar.gz"
- Inside the extracted directory: Run "./configure; make"
- Java 1.7+
- Ant (we use 1.9)
-
Download qCORAL: https://s3-us-west-2.amazonaws.com/qcoral/qcoral-fse-replication.tar.xz
-
Uncompress the file
-
Set the location of the RealPaver executable in "scripts/variables" (Eg. => ....../realpaver-0.4/bin/realpaver)
-
After this, if you can have a constraint file (.qcoral file), you can run the following command to generate the probability distribution.
./run_qcoral --mcIterativeImprovement --mcProportionalBoxSampleAllocation
--mcSeed 123456 --mcMaxSamples 500000 --mcInitialPartitionBudget 50000
--mcTargetVariance 1E-20 --mcSamplesPerIncrement 10000
your_file.qcoral
To know more about the command line arguments: http://qcoral.s3-website-us-west-2.amazonaws.com/QCoralOptions.html
To know more about qCORAL: http://qcoral.s3-website-us-west-2.amazonaws.com/index.html