Compiling with provenance fails

[gfour]

Hello, I am trying to run Doop analyses with provenance and compilation fails:

$ souffle -c -o out gen_2922395936733669313.dl --provenance=explain
souffle: ast/Program.cpp:39: void souffle::ast::Program::addRelation(souffle::Own<souffle::ast::Relation>): Assertion `existingRelation == nullptr && "Redefinition of relation!"' failed.
[1]    21088 abort (core dumped)  souffle -c -o out gen_2922395936733669313.dl --provenance=explain

The same code compiles fine without the --provenance flag. Adding --legacy (suggested in issue #1881) does not work. The code (attached) does not use custom functors.

Tested on Ubuntu 18.04 both with the released Souffle 2.0.2 .deb and with latest git repo version:

$ souffle --version
Souffle: 2.0.2-1180-gc9b0e3f36(32bit Domains)

gen_2922395936733669313.dl.zip

[b-scholz]

We will have a look!

[b-scholz]

I found the culprit - it is the "as" conversion

as(?t, ReferenceType)

[b-scholz]

The problem is that after adding the rule for type cast:

--- a/src/ast2ram/provenance/UnitTranslator.cpp
+++ b/src/ast2ram/provenance/UnitTranslator.cpp
@@ -218,6 +218,10 @@ Own<ram::Sequence> UnitTranslator::generateInfoClauses(const ast::Program* progr
             if (isA<ast::Aggregator>(arg)) {
                 return tfm::format("agg_%d", aggregateNumber++);
             }
+            if (isA<ast::TypeCast>(arg)) {
+                return tfm::format("type_cast%d", functorNumber++);
+            }

There are still issues related aggregates. Basically, our current provenance system cannot deal with aggregates at the moment. We need to add this.

[b-scholz]

The problem is in the method UnitTranslator::makeNegationSubproofSubroutine which does not support constraints and aggregates at the moment.

[gfour]

Thanks for the quick response! We are currently porting Doop's logic to Souffle 2.0 with subtyping and I might have misused the as() functor. I am also seeing differences between the released 2.0.2 version and latest git HEAD, the latter requiring "as" casts in fewer places.

[b-scholz]

It would be better to port to the latest git HEAD. Version 2.0.2 uses the old ast-to-ram translator, which we abandoned and replaced by a proper engineered one. As soon as most of the bugs on the issue list are fixed (related to magic set/inlining), we should create a new version.