souffle icon indicating copy to clipboard operation
souffle copied to clipboard

Insufficient checking on unground variable

Open DerZc opened this issue 2 years ago • 1 comments

Hi,

Consider the following program:

.type typeHejh = symbol
.type typeMrgs = unsigned
.type typeAiik = symbol

.decl tdfw(A:float, B:float, C:float)
.decl hhxs(A:typeHejh, B:typeAiik, C:number, D:typeAiik)
.decl vxeo(A:typeHejh, B:symbol, C:number, D:typeAiik, E:typeAiik, F:typeHejh)

hhxs("40uD340uD3", "40uD3", 4, "40uD3").
tdfw(10.712999999999999, 16.931999999999999, 10.712999999999999).

vxeo(E, C, F, D, C, D) :- tdfw(B, max(A,7.179), --A), hhxs(D, C, F, E).

.output vxeo

This program would hang. I guess it was caused by the unground variable A, but the grammar checker did not find this. If I write this rule b(A):-tdfw(B, max(A,7.179), --A), the grammar can find this error.

The souffle version is 3cd802d, I tried with some older version, also have this issue.

DerZc avatar Dec 23 '22 08:12 DerZc

The ResolveAnonymousRecordAliasesTransformer that runs before the semantics checker calls the type analysis. And the type analysis loops infinitely because A cannot be given a definite type.

quentin avatar Dec 16 '23 08:12 quentin