Clog: Declarative Program Analysis for C

Clog is a Datalog language extension that enables analysis of C programs inside Datalog.

FunctionWithGoto($func, g, l) :-
                    <: $type $func(..) { .. } :>,
                    @$func g <: goto $label1; :>,
                    @$func l <: $label2 : $substmt :>,
                    $label1 == $label2.

BackwardGoto(g, l) :-
                       g <: goto $label1; :>,
                       l <: $label2 : $substmt :>,
                       $label1 == $label2,
                       c_src_line_start(g) > c_src_line_start(l).

LabeledReturn(l) :-
                 l <: $label : return $v;  :>.

LabeledReturn(l) :-
                 l <: $label : return ; :>.


WarnBackwardGoto(file, line) :- BackwardGoto(g, _), file = io_relative_path(c_src_file(g)), line = c_src_line_start(g).

WarnMoreThanOneLabel(file, line) :- FunctionWithGoto(f, _, l1),
                                    FunctionWithGoto(f, _, l2),
                                    l1 != l2,
                                    line = c_src_line_start(l1),
                                    line >= c_src_line_start(l2),
                                    file = io_relative_path(c_src_file(f)).

WarnLabeledReturn(file, line) :- LabeledReturn(l), file = io_relative_path(c_src_file(l)), line = c_src_line_start(l).

OUTPUT('WarnBackwardGoto, "WarnBackwardGoto.csv", "csv").
OUTPUT('WarnMoreThanOneLabel, "WarnMoreThanOneLabel.csv", "csv").
OUTPUT('WarnLabeledReturn, "WarnLabeledReturn.csv", "csv").

Building

Clog depends on modified versions of JastAdd and JastAddParser. These dependencies are packaged as submodules, so run git submodule update --init --recursive to fetch them.

Ensure that the souffle executable is available in your $PATH.

For the hybrid and incremental evaluation modes, a version a modified version of Souffle is needed. This version exposes an extended JNI interface and uses a different format for SQLite input and output.

Building Soufflé (optional)

Soufflé can be used for some execution modes, though by default Clog does not use it.

To build, you will need the following:

• a complete build system for C, including the GNU autotools
• mcpp
• swig

Clone the repository

git clone https://github.com/creichen/souffle.git -b javadl

When building, make sure to enable 64-bit domains and SWIG (needed only for the hybrid mode):

cd souffle
./bootstrap
./configure --enable-swig --enable-64bit-domain
make

Environment variables (relative to clog project root):

• PATH must contain ./souffle/src/, unless you install souffle globally (sudo make install)

C support (required for Clog)

For analyzing C, Clog uses the Clang front-end for pattern matching. We have built a Clang library to interface with Clog. Run the following commands to fetch and build a modified version of the LLVM repository:

Install the following dependencies:

• swig4.0

git clone git@github.com:alexdura/llvm-project.git -b clog

To build the library, run the following commands:

mkdir llvm-project/build-release
cd llvm-project/build-release
cmake -G Ninja -DCMAKE_BUILD_TYPE=Release -DLLVM_ENABLE_PROJECTS="clang;clang-tools-extra"  -DBUILD_SHARED_LIBS=ON  -DLLVM_APPEND_VC_REV=OFF   ../llvm
ninja

Environment variables (relative to clog project root):

• PATH must contain ./llvm-project/build-release/bin/
• LD_LIBRARY_PATH must contain ./llvm-project/build-release/lib/

Docker image (if you want to run in Podman or Docker)

We provide a Docker image which contains Clog and evaluation scripts, packaged together with all the required dependencies.

cd docker
./build.sh

then run the image using:

docker run -it clog23:cc24

Clog itself

Java versions that should work:

• Java 11

./gradlew clean jar
./gradlew test

Troubleshooting

If any Clog tests fail, try the following tests to narrow down the problem. You can run an individual test (e.g., lang.CEvaluationTest) as follows:

./gradlew test --info --tests lang.CEvaluationTest

• Cannot find symbol: var: Make sure to use Java 11
• Could not create an instance of type org.gradle.initialization.DefaultSettings_Decorated: Make sure to use Java 11
• lang.CEvaluationTest fails with UnsatisfiedLinkError: See UnsatisfiedLinkError below
• clang.ASTImporterTest fails with IOException: Cannot run program "clang": See “Missing clang” below
• lang.EvaluationTest fails with IOException: Cannot run program "souffle": See “Missing Soufflé” below (not needed to run Clog with internal evaluation)

Troubleshooting: UnsatisfiedLinkError

./gradlew test --info --tests lang.CEvaluationTest

If you get the error java.lang.UnsatisfiedLinkError: no clangClogSWIG in ..., make sure that libclangClogSWIG.so is in your LD_LIBRARY_PATH. If you followed the “C support” steps above and are using bash, you might e.g. run:

export LD_LIBRARY_PATH=${LD_LIBRARY_PATH}:`pwd`/llvm-project/build-release/lib/

Troubleshooting: Missing Soufflé

./gradlew test --info --tests lang.EvaluationTest

If you get the error java.io.IOException: Cannot run program "souffle": error=2, No such file or directory, then the souffle binary is not in your PATH. Make sure it is visible there (i.e., you should be able to run souffle on the shell and see a help message). If you followed the “Building soufflé” steps above and are using bash, you might e.g. run:

export PATH=${PATH}:`pwd`/souffle/src

Troubleshooting: Missing Clang

./gradlew test --info --tests clang.ASTImporterTest

If you get the error java.io.IOException: Cannot run program "clang": error=2, No such file or directory, then the clang binary is not in your PATH. Make sure it is visible there (i.e., you should be able to run clang --help on the shell and see a help message). If you followed the “C support” steps above and are using bash, you might e.g. run:

export PATH=${PATH}:`pwd`/llvm-project/build-release/bin/

Running

Clog supports multiple running modes, which represent a trade-off between speed and external dependencies.

Internal evaluation

Uses the internal semi-naive evaluator and it is reasonably fast when the number of tuples is small (< 1 million).

java -jar compiler.jar --eval metadl program.mdl -F fact_dir -D output_dir

Internal parallel evaluation

Depending on the shape of the strata dependency is graph, the parallel evaluator may speed things up.

java -jar compiler.jar --eval metadl-par program.mdl -F fact_dir -D output_dir

Language description

Datalog

Datalog is a declarative query language, with roots in logic programming. Relations between tables are expressed as Horn clauses. Clog extends Datalog with syntactic patterns and associates side-effects to the following predicates EDB and OUTPUT. The order of evaluation is as follows:

1. All predicates the EDB predicate depends upon are evaluated. For all tuples ('P, "file") in the the EDB relation, the file is read as a CSV and its tuples are added to the relation P.
2. Fixpoint evaluation.
3. For all values ('P) in the OUTPUT relation, the contents of relation P are written out to a file P.csv.

Additional Supported features:

• Stratified negation !P(x1,...,xn)
• Filtering expr1 < expr2, expr1 > expr2
• Object creation v = expr binds a variable to the result of an expression
• Arithmetic expressions ( +, -, *, /) and string concatenation (cat)
• Monomorphic type inference

Metalanguage description

Syntactic patterns

Patterns are a mechanism to match rules and bind metavariables to terms, expressions and predicate symbols.

Bounded patterns

The root node of a pattern can be accessed by using a bounded pattern $p <:$x + $y:>.

Gaps

Datalog ... and C or Java ..

Gaps express missing elements inside a list.

Metavariables

Datalog: $x, $p or Java: `c, `i

Variables used inside analyze blocks to connect patterns with other literals in the rule

• Terms: p($x, $y)
• Predicates: $p(x, y)
• Arithmetic expressions: $x + $y
• Index metavariables p(..., $i:$v, ...)

License

This repository is covered by a BSD 2-clause license, see LICENSE.

Debugging

The following commands are useful when debugging Clog:

• Pretty print the desugared program in Clog format java -jar compiler.jar --pretty-print metadl program.mdl
• Pretty print the desugared program in Souffle format java -jar compiler.jar --pretty-print metadl program.mdl
• Enable internal debug printouts by setting METADL_LOG=debug|time|info in the environment.

Dependencies

SEP

SEP is an Earley parser implementation. We use it to parse the patterns.

JastAdd

JastAdd is a meta-compilation system that supports Reference Attribute Grammars (RAGs). It uses the parser generated from Beaver. In addition it takes an abstract grammar description file as input. The abstract grammar description is used to generate the classes that represent the pattern AST.