Corresponding commit version of Datalog engines for each bug:
| # | Datalog Engine | commit version | bug report link | bug status |
|---|---|---|---|---|
| bug1 | Souffle | 3cd802d |
souffle-lang/souffle#2311 | confirmed |
| bug2 | Souffle | 3cd802d |
souffle-lang/souffle#2375 | unconfirmed |
| bug3 | Souffle | 29c5921 |
souffle-lang/souffle#2322 | confirmed |
| bug4 | Souffle | 29c5921 |
souffle-lang/souffle#2323 | unconfirmed |
| bug5 | Souffle | 29c5921 |
souffle-lang/souffle#2327 | unconfirmed |
| bug6 | Souffle | 29c5921 |
souffle-lang/souffle#2337 | unconfirmed |
| bug7 | Souffle | 29c5921 |
souffle-lang/souffle#2343 | unconfirmed |
| bug8 | Souffle | 3cd802d |
souffle-lang/souffle#2385 | unconfirmed |
| bug9 | Souffle | 29c5921 |
souffle-lang/souffle#2382 | unconfirmed |
| bug10 | μZ | cbc5b1f |
Z3Prover/z3#6446 | fixed |
| bug11 | μZ | cbc5b1f |
Z3Prover/z3#6447 | confirmed |
| bug12 | CozoDB | release version 0.7.0 | cozodb/cozo#101 | fixed |
| bug13 | CozoDB | release version 0.7.0 | cozodb/cozo#122 | confirmed |
The Dockerfile in the root directory of deopt will contains all source code of Souffle, Z3 (μZ), and DDlog. Build the docker image first.
For bugs of Souffle (bug1 - bug9), enter the root directory of Souffle (/tmp/souffle in docker) and check out to the corresponding commit version, compile Souffle with command shown in here, or follow the command shown in Dockerfile.
For bugs of μZ (bug10 and bug11), enter the root dictory of Z3 (/tmp/z3 in docker) and checkout to the corresponding commit version, compile z3 with command shown in here, or follow the command shown in Dockerfile.
For bugs of CozoDB, I use the python driver to run the program, which can be found at pycozo.
For bug1-6, 9-11, in each directory of these bugs, there is a bug-inducing test case named bug.dl, and corresponding reference programs prefn.dl and optimized programs poptn.dl, n indicates the iteration of test case generation. You can directly execute these files with souffle -D- file_name.dl for Souffle bugs (-D- means to print the output to the command line.) or z3 file_name.dl for μZ bugs. All of these bugs don't need additional execution options.
For bug7 and bug8, there is only bug.dl in their directory, as these two bugs were triggered by different execution options. Bug7 only occurred in synthesizer mode, which need -c in execution options. The execution will produce different result when remove -c option. Bug8 needs -t none --disable-transformers=ExpandEqrelsTransformer, and can produce different result when remove -t none.
We also provide the supplementary_material.pdf file in main directory to record the result of each step for reproduction.
| # | Datalog Engine | commit version | bug report link | bug status |
|---|---|---|---|---|
| bug1 | Souffle | 3cd802d |
souffle-lang/souffle#2318 | unconfirmed |
| bug2 | Souffle | 3cd802d |
souffle-lang/souffle#2320 | confirmed |
| bug3 | Souffle | 3cd802d |
souffle-lang/souffle#2321 | confirmed |
| bug4 | Souffle | 3cd802d |
souffle-lang/souffle#2324 | confirmed |
| bug5 | Souffle | 3cd802d |
souffle-lang/souffle#2326 | confirmed |
| bug6 | Souffle | 29c5921 |
souffle-lang/souffle#2338 | unconfirmed |
| bug7 | Souffle | 29c5921 |
souffle-lang/souffle#2339 | unconfirmed |
| bug8 | Souffle | 29c5921 |
souffle-lang/souffle#2340 | confirmed |
| bug9 | Souffle | 29c5921 |
souffle-lang/souffle#2346 | fixed |
| bug10 | Souffle | 1fc233d |
souffle-lang/souffle#2351 | fixed |
| bug11 | Souffle | 15b114a |
souffle-lang/souffle#2355 | confirmed |
| bug12 | Souffle | b8b1d69 |
souffle-lang/souffle#2369 | unconfirmed |
| bug13 | Souffle | 3cd802d |
souffle-lang/souffle#2379 | confirmed |
| bug14 | Souffle | 0ad4109 |
souffle-lang/souffle#2426 | confirmed |
| bug15 | CozoDB | release version 0.7.0 | cozodb/cozo#97 | fixed |
| bug16 | CozoDB | release version 0.7.0 | cozodb/cozo#99 | fixed |
| bug17 | CozoDB | release version 0.7.0 | cozodb/cozo#113 | confirmed |