karmaresearch / vlog

Apache License 2.0
55 stars 9 forks source link

Sporadic segmentation faults in ChaseMgmt::getNewOrExistingIDs #86

Closed mmarx closed 3 years ago

mmarx commented 3 years ago

On 09b32fa6ed316a74515872aa8706e041d7859dd2 and later, the rulewerk unit tests VLogReasonerWriteInferencesTest sometimes cause a segmentation fault in ChaseMgmt::getNewOrExistingIDs.

[DEBUG] #
[DEBUG] # A fatal error has been detected by the Java Runtime Environment:
[DEBUG] #
[DEBUG] #  SIGSEGV (0xb) at pc=0x00007fc3b8f834cc, pid=515286, tid=0x00007fc3d9be8640
[DEBUG] #
[DEBUG] # JRE version: OpenJDK Runtime Environment (8.0_272-b10) (build 1.8.0_272-b10)
[DEBUG] # Java VM: OpenJDK 64-Bit Server VM (25.272-b10 mixed mode linux-amd64 compressed oops)
[DEBUG] # Problematic frame:
[DEBUG] # C  [libvlog-core.so+0x14f4cc]  ChaseMgmt::
[DEBUG] getNewOrExistingIDs(unsigned int, unsigned int, std::
[DEBUG] vector<std::
[DEBUG] shared_ptr<Column>, std::
[DEBUG] allocator<std::
[DEBUG] shared_ptr<Column> > >&, unsigned long)+0xd2
[DEBUG] #
[DEBUG] # Core dump written. Default location: /home/mmarx/proj/java/rulewerk/rulewerk-vlog/core or core.515286

Usually, running the tests a few times in a loop is sufficient to trigger the bug:

for i in {01..10}; do mvn test -Dtest=VLogReasonerWriteInferencesTest -DfailIfNoTests=false; done

Sometimes, the bug also triggers in the Github CI action. I have not been able to trigger the bug on c1f2d88f56959d4fcd8945c3bb3561c52278d1d6.

The ruleset used by the test looks like this:

<http://example.org/s>(<http://example.org/c>) .
LocatedIn(Egypt, Africa) .
address(TSH, <Pragerstraße13>, <01069>, dresden) .
city(dresden) .
country(germany) .
university(tudresden, germany) .
location(dresden, germany) .

LocatedIn(?X, ?Y) :- location(?X, ?Y) .
address(?X, !Y, !Z, !Q), LocatedIn(!Q, ?F) :- university(?X, ?F) .

I suspect that the repeated existential in the different head atoms might be the problem.

marco-calautti commented 3 years ago

The actual problem is that there is a frontier variable (F) in the second atom in the head. The bug is triggered by my pull request, where I tried to fix another issue, but I am wrongly assuming the rule is single head, so when I try to access the variable at position 5 (globally in the head), which is F, I do that on the first head atom, which does not have such a position. The fix should be easy: simply pick the variable from the right atom.

mmarx commented 3 years ago

Thanks for looking into this, I can confirm that with #87 in place, I can no longer trigger the bug.

CerielJacobs commented 3 years ago

Thanks Marco!