ADT Bug

[b-scholz]

The refactoring of AST-To-RAM translator introduced a new bug. The following program fails to execute.

.type Expr = Number { x : number }
           | Symbol { x : symbol }
           | Add {e_1 : Expr, e_2 :Expr}

.decl S(e1:Expr, e2:Expr) eqrel

S( $Add($Number(10), $Number(20)),
   $Add($Number(10), $Number(20))).

S(right,right) :-
   S($Add(left, right), _).

.printsize S

The rule

S(right,right) :-
   S($Add(left, right), _).

fails with throwing following assertion:

souffle: ./include/souffle/RecordTable.h:124: const RamDomain* souffle::RecordTable::unpack(souffle::RamDomain, std::size_t) const: Assertion `iter != maps.end() && "Attempting to unpack record for non-existing arity"' failed.

[b-scholz]

The problem is the following RAM translation:

BEGIN_DEBUG "S(right,right) :- \n   S($Add(_, right),_).\nin file /home/scholz/souffle/src/rewrite_extended.dl [11:1-12:28]"
     QUERY
      IF (NOT (@delta_S = ∅))
       FOR t0 IN @delta_S
        UNPACK t1 FROM t0.0
         IF ((t1.0 = number(0)) AND (NOT (t1.2,t1.2) ∈ S))
          PROJECT (t1.2, t1.2) INTO @new_S
    END_DEBUG

[b-scholz]

This is a simplified version:

.type TExpr = leaf { }
           | inner {e_1 : TExpr, e_2 :TExpr}

.decl A,B(e:TExpr)
A($inner($leaf(), $leaf())).

B(right) :- 
   A($inner(_, right)).
.output B

The issue is that RAMPACK for $innner has the wrong arity. It should have three instead of two. The RAM program of the example is the following:

PROGRAM
 DECLARATION
  A(e:+:TExpr) 
  B(e:+:TExpr) 
 END DECLARATION
 SUBROUTINE stratum_0
  BEGIN_DEBUG "A($inner($leaf(), $leaf())).\nin file /Users/scholz/Projects/souffle/src/rewrite_extended.dl [5:1-5:29]"
   QUERY
    PROJECT ([number(0),[[number(1),[]],[number(1),[]]]]) INTO A
  END_DEBUG
 END SUBROUTINE
 SUBROUTINE stratum_1
  BEGIN_DEBUG "B(right) :- \n   A($inner(_, right)).\nin file /Users/scholz/Projects/souffle/src/rewrite_extended.dl [7:1-8:24]"
   QUERY
    IF (NOT (A = ∅))
     FOR t0 IN A
      UNPACK t1 FROM t0.0
       IF (t1.0 = number(0))
        PROJECT (t1.2) INTO B
  END_DEBUG
  IO B (IO="file",attributeNames="e",auxArity="0",name="B",operation="output",output-dir=".",params="{\"records\": {}, \"relation\": {\"arity\": 1, \"params\": [\"e\"]}}",types="{\"ADTs\": {\"+:TExpr\": {\"arity\": 2, \"branches\": [{\"name\": \"inner\", \"types\": [\"+:TExpr\", \"+:TExpr\"]}, {\"name\": \"leaf\", \"types\": []}], \"enum\": false}}, \"records\": {}, \"relation\": {\"arity\": 1, \"types\": [\"+:TExpr\"]}}")
  CLEAR A
 END SUBROUTINE
 BEGIN MAIN
  CALL stratum_0
  CALL stratum_1
 END MAIN
END PROGRAM

and we pack wrongly, i.e.,

    PROJECT ([number(0),[[number(1),[]],[number(1),[]]]]) INTO A

fails to pack the outer record with an arity of three and fails to unpack the record in the later query:

QUERY
    IF (NOT (A = ∅))
     FOR t0 IN A
      UNPACK t1 FROM t0.0
       IF (t1.0 = number(0))
        PROJECT (t1.2) INTO B

Note that UNPACK does not specify the arity (this is currently hidden information) and should be printed.

[b-scholz]

Ok - this is related to ADTs and encodings of ADTs as records. Packing assumes it is [tag, [payload...]] and unpacking assumes it is [tag, payload...]