souffle-lang / souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
http://souffle-lang.github.io/
Universal Permissive License v1.0
927 stars 208 forks source link

Refactoring of RAM #541

Closed b-scholz closed 5 years ago

b-scholz commented 6 years ago

The RAM intermediate representation needs to be refactored. We should aim to apply the same design patterns as in AST, i.e., prototype pattern and subscriber mechanism for analyses, and transformers. In addition, the intermediate representation should be separated from the operations on it (e.g., levelling). We should have a transformer pipeline similar to the AST, i.e., RAM should mimic a similar design like the AST of Souffle.

b-scholz commented 6 years ago

This is our battle-plan for the refactoring so that we can perform correctness checks after each step:

(1) IndexMap should become a RamAnalysis (done)

(2) Differentiate between a RamScan with Index and without Index as proper RAM Classes

(3) Write a transformer that translates RamScan without Index to RamScan with Index, and remove detection of Indexed/Non-indexed searches from AstTranslator.

(4) Remove Levelling (getDepth() / getLevel()) from RAM (addCondition etc.) and perform Levelling as a RamTransformer

(5) Have a list of RamRelation Declarations defining properties of RamRelation and actual use of relations in RamStatements are referring to RamRelations by own RamRelationRef object (done)

(6) Tidy up some quirks in Ram IR / make interfaces uniform / check naming conventions

(7) Rewrite AstTranslator (partially done)

brofranks commented 5 years ago

This is a list of some remaining items that need to be done:

mmcgr commented 5 years ago

What is needed for "Fix RAM print output"? I don't see a problem, other than RamCreate has a TODO to add type info - which would clash with 'Remove RamCreate operation'.

mmcgr commented 5 years ago

Ram print methods have some formatting and style issues that hinder readability. debug output for a more complicated program will demonstrate the issue.

b-scholz commented 5 years ago

Let's remove the RAM semantic checker.
The only reason why we would like to have it is to check the correctness of the translation / transformers. Let's leave this as future work.

Also, the SMT solver / constraint simplifier would only be useful if there were use cases that could profit from the simplifications. This is not clear to me at the moment.

I am inclined to fix as many issues as possible related to RAM representation.

Let's defer some remaining issues to a new issue. This issue becomes convoluted!

b-scholz commented 5 years ago

We need more RAM Representation fixes...

mmcgr commented 5 years ago