Discriminants/variant numbers are checked too late, causing assertion violations in user-defined functor

[markusscherer]

Hi everybody!

I encountered an issue very similar to #2373.

When executing the following code (with the functors.cpp file below; both minified from actual code the bug appeared in), I can consistently trigger an assertion violation in the current master (e6cc668).

.functor id(symbol): symbol stateful
.functor decode(symbol): symbol stateful

.type T = C1 {A0 : symbol} | C2 {A0: number}

.decl A(A2: T)
.decl B()

A($C2(10000000)).
.output B

B() :-
  A($C1(X)),
  (@decode(X) = @id("Y")).

//functors.cpp
#include "souffle/SymbolTable.h"
#include "souffle/RecordTable.h"

extern "C" {

souffle::RamDomain id(souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable, souffle::RamDomain x) {
  return x;
}

souffle::RamDomain decode(souffle::SymbolTable* symbolTable, souffle::RecordTable* recordTable, souffle::RamDomain x) {
  symbolTable->decode(x);
  return x;
}

}

Error:

souffle: /build/source/src/include/souffle/datastructure/ConcurrentFlyweight.h:296: const Key& souffle::ConcurrentFlyweight<LanesPolicy, Key, Hash, KeyEqual, KeyFactory>::fetch(lane_id, index_type) const [with LanesPolicy = souffle::ConcurrentLanes; Key = std::__cxx11::basic_string<char>; Hash = std::hash<std::__cxx11::basic_string<char> >; KeyEqual = std::equal_to<std::__cxx11::basic_string<char> >; KeyFactory = souffle::details::Factory<std::__cxx11::basic_string<char> >; lane_id = long unsigned int; index_type = long unsigned int]: Assertion `Idx < SlotCount.load(std::memory_order_relaxed)' failed.
[1]    674346 IOT instruction (core dumped)  souffle min-rules.dl

The problem (as in #2373) seems to be that the discriminant is checked after the "payload" of the ADT is passed into the functor (which then does a lookup using an improperly constrained ordinal). I first found the problem by checking the C++ code, but it is better visible in the transformed RAM

// annotated output of `souffle --show=transformed-ram min-rules.dl | cat -n`
// ...SNIP...
     9	   QUERY
    10	    IF (ISEMPTY(+disconnected0) AND (NOT ISEMPTY(A)))
    11	     FOR t0 IN A
    12	      IF (NOT ISEMPTY(+disconnected0)) BREAK
    13	       UNPACK t1 ARITY 2 FROM t0.0
    14	        IF ((@decode(t1.1) = @id(STRING("Y"))) AND (t1.0 = NUMBER(0)))
                     ^^^^^^^ functor call      before check ^^^^^^^^^^^^^^^^
    15	         INSERT () INTO +disconnected0
    16	   END QUERY
// ...SNIP...

[markusscherer]

I'm not well-acquainted with the code that does the ordering of premises, but one thing I deem possible is that returning the maximum integer here, might cause an integer overflow somewhere else (maybe here?). That would cause the return value to be std::numeric_limits<int>::max() + std::numeric_limits<int>::max() which is -2.

I'm wildly conjecturing here, but it might be that ordering the premises by purely looking at one premise at a time is not even possible. Maybe something like a topological sort on a graph describing the "constrainedness" of ADT values has to come first with the current numerical sorting as a tie-breaker.

[quentin]

I confirm there is an overflow occurring in the complexity analysis. A simple fix is to set complexity to a smaller value like std::numeric_limits<int>::max() >> 6 that is still safe for expressions with less than 64 user-defined functors.

I agree with you that in a more general case, ADT branch constraints should be evaluated strictly before accessing any other part of the ADT value.