Skip to content

Commit

Permalink
Sort ambiguities generated by GLR Bison parsers (#4261)
Browse files Browse the repository at this point in the history
The order in which the different stanzas in K's Bison parsers are
generated depends on the iteration order of a Java set, which is not
well defined and may be different across platforms. Normally, this isn't
a problem as the location of a grammar action in the file doesn't affect
whether it gets run or not for a particular input string.

However, one situation in which this can present an issue is when
merging ambiguities. The ordering of the two nodes present under an
ambiguity _can_ be changed if the ordering of stanzas in the file
changes.

This manifested with #4171
causing build failures in the C semantics, and in the subsequent LLVM
backend update PR #4257.

The solution is to sort the two nodes that make up an ambiguity when the
merge function is called; this PR implements a simple ordering function
over parse tree nodes and updates related tests to respect the new
consistent ordering of ambiguity nodes.
  • Loading branch information
Baltoli authored Apr 17, 2024
1 parent e52dabb commit ab7fafb
Show file tree
Hide file tree
Showing 2 changed files with 52 additions and 5 deletions.
47 changes: 47 additions & 0 deletions k-distribution/include/kframework/cparser/main.c
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,46 @@ bool equalsNode(node *x0, node *x1) {
}
}

// Define an ordering on nodes as follows:
// - Any string node is < any constructor node
// - String nodes are compared via strcmp
// - Constructor nodes are:
// - First compared by symbol via strcmp
// - If their symbols are identical, they are compared recursively:
// - First by their number of children
// - Then lexicographically over their children
//
// Returns true if x0 < x1
bool ltNode(node *x0, node *x1) {
if (x0->str && x1->str) {
return strcmp(x0->symbol, x1->symbol) < 1;
}

if (x0->str && !x1->str) {
return true;
}

if (!x0->str && x1->str) {
return false;
}

if (!equalsSymbol(x0, x1)) {
return strcmp(x0->symbol, x1->symbol) < 1;
}

if (x0->nchildren != x1->nchildren) {
return x0->nchildren < x1->nchildren;
}

for (size_t i = 0; i < x0->nchildren; i++) {
if (!equalsNode(x0->children[i], x1->children[i])) {
return ltNode(x0->children[i], x1->children[i]);
}
}

return false;
}

char *injSymbol(char *lesser, char *greater) {
char *prefix = "inj{";
char *infix = ", ";
Expand All @@ -152,6 +192,13 @@ YYSTYPE mergeAmb(YYSTYPE x0, YYSTYPE x1) {
if (equalsNode(x0.nterm, x1.nterm)) {
return x0;
}

if(ltNode(x1.nterm, x0.nterm)) {
YYSTYPE tmp = x0;
x0 = x1;
x1 = tmp;
}

node *n = malloc(sizeof(node) + sizeof(node *) * 2);
node *x0n = x0.nterm;
node *x1n = x1.nterm;
Expand Down
10 changes: 5 additions & 5 deletions k-distribution/tests/regression-new/parse-c/test.ref
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@ amb ( .DeclSpecifiers typedef int AA ; , .DeclSpecifiers typedef int .InitD
.BlockItems
amb ( .DeclSpecifiers T .InitDecls , ( x ) ; , T ( x ) ; )
amb ( .DeclSpecifiers S .InitDecls , ( x ) ; , S ( x ) ; )
amb ( T * y ; , .DeclSpecifiers T .InitDecls , * y ; )
amb ( .DeclSpecifiers T .InitDecls , * y ; , T * y ; )
.DeclSpecifiers int .InitDecls , U , z ;
amb ( U * z ; , .DeclSpecifiers U .InitDecls , * z ; )
func ( amb ( T * x , ( .SpecifierQuals T ) * x ) ) ;
func ( amb ( U * z , ( .SpecifierQuals U ) * z ) ) ;
amb ( .DeclSpecifiers U .InitDecls , * z ; , U * z ; )
func ( amb ( ( .SpecifierQuals T ) * x , T * x ) ) ;
func ( amb ( ( .SpecifierQuals U ) * z , U * z ) ) ;
amb ( .DeclSpecifiers int AA ; , .DeclSpecifiers int .InitDecls , AA ; )
.DeclSpecifiers int .InitDecls , BB = AA * 2 ;
amb ( .DeclSpecifiers typedef int CC ; , .DeclSpecifiers typedef int .InitDecls , CC ; )
Expand All @@ -27,5 +27,5 @@ amb ( .DeclSpecifiers typedef int AA ; , .DeclSpecifiers typedef int .InitD
amb ( .DeclSpecifiers typedef char C ; , .DeclSpecifiers typedef char .InitDecls , C ; )
.DeclSpecifiers void baz ( ) {
.BlockItems
.DeclSpecifiers int .InitDecls , aa = amb ( sizeof C , sizeof ( .SpecifierQuals C ) ) , C , bb = amb ( sizeof C , sizeof ( .SpecifierQuals C ) ) ;
.DeclSpecifiers int .InitDecls , aa = amb ( sizeof ( .SpecifierQuals C ) , sizeof C ) , C , bb = amb ( sizeof ( .SpecifierQuals C ) , sizeof C ) ;
}

0 comments on commit ab7fafb

Please sign in to comment.