kast better error messages and defaults

[grosu]

There are several problems below:

D:\github\grosu\k\k-distribution\tutorial\1_k\4_imp++\lesson_7>kompile imp.k
D:\github\grosu\k\k-distribution\tutorial\1_k\4_imp++\lesson_7>krun ..\lesson_1\tests\sum-io.imp
[Error] Critical: Parser returned a non-zero exit code: 113
Stdout:
[B@51acdf2e
Stderr:
[B@6a55299e
D:\github\grosu\k\k-distribution\tutorial\1_k\4_imp++\lesson_7>kast ..\lesson_1\tests\sum-io.imp
[Error] Inner Parser: Parse error: unexpected character 'w'.
        Source(D:\github\grosu\k\k-distribution\tutorial\1_k\4_imp++\lesson_7\.\..\lesson_1\tests\sum-io.imp)
        Location(2,1,2,2)
D:\github\grosu\k\k-distribution\tutorial\1_k\4_imp++\lesson_7>kast ..\lesson_1\tests\sum-io.imp --sort Stmts
`__`(`int_;`(`_,_`(#token("n","Id"),`_,_`(#token("s","Id"),`.List{"'_,_"}`(.KList)))),`__`(`while(_)_`(#token("true","Bool"),`{_}`(`__`(`print(_);`(`_,_`(#token("\"Add numbers up to (<= 0 to quit)? \"","String"),`.List{"'_,_"}`(.KList))),`__`(`_;`(`_=_`(#token("n","Id"),`read()`(.KList))),`__`(`if(_)_else_`(`_<=_`(#token("n","Id"),#token("0","Int")),`{_}`(`__`(`halt;`(.KList),`.List{"'__"}`(.KList))),`{_}`(`__`(`_;`(`_=_`(#token("s","Id"),#token("0","Int"))),`__`(`while(_)_`(`!_`(`_<=_`(#token("n","Id"),#token("0","Int"))),`{_}`(`__`(`_;`(`_=_`(#token("s","Id"),`_+_`(#token("s","Id"),#token("n","Id")))),`__`(`_;`(`_=_`(#token("n","Id"),`_+_`(#token("n","Id"),#token("-1","Int")))),`.List{"'__"}`(.KList))))),`__`(`print(_);`(`_,_`(#token("\"Sum = \"","String"),`_,_`(#token("s","Id"),`_,_`(#token("\"\\n\"","String"),`.List{"'_,_"}`(.KList))))),`.List{"'__"}`(.KList)))))),`.List{"'__"}`(.KList)))))),`.List{"'__"}`(.KList)))

1. The krun error messages due to kast is obviously bad. Why not just reproduce the kast error message in krun, saying so? Something like this: "[Error]: parsing, see kast output below\n".

2. We should have not had the krun error first place, because we have $PGM:Stmts in the configuration, so krun should have called the parser appropriately.

3. By default, kast should attempt to parse no matter what. If one gives it a sort, then great, it knows what to look for and it will fail if it cannot parse to that given sort. But if one does not give it a sort, then it should search for a sort to which it can parse the input.

Let's do this after/if we release K4.0.

[cos]

@dwightguth, this seems related to the binary serialization change

[hksskh]

We are working on this issue, and find that the first two problems put by @grosu may have already been fixed in the current version (master branch). We pick the commit 78cc611c87ae49acdb747603026018851de3dca5 on 17 Jan to reproduce these problems.

For the first problem, it outputs in this former commit like: huangkesongdeMacBook-Pro:lesson_7 hksskh$ krun ../lesson_1/tests/sum-io.imp [Error] Critical: Parser returned a non-zero exit code: 113 Stdout:

Stderr: [Error] Inner Parser: Parse error: unexpected character 'w'. Source(/Users/hksskh/Documents/uiuc_on-campus_courses/CS427/4_credit_hour_task/k/k-distribution/tutorial/1_k/4_imp++/lesson_7/./../lesson_1/tests/sum-io.imp) Location(2,1,2,2) We can see the Stdout part is blank since there is nothing in output stream. And in error stream, it outputs the error message of parser, just like that in KAST output, so we think this error message in KRUN is already good. @grosu

2. For the second problem, we check between this commit and current version about content of sum-io.imp and imp.k. the sum-io.imp is exactly the same, and the imp.k has the difference that does not effect the error. What really makes a difference here is the function externalParse in KRun.java. Here we have "environment.put("KRUN_SORT", startSymbol.name());" For the current version, this sort value is Stmts(as shown in imp.k as $PGM:Stmts). However, in this former commit, this sort value is K. Tracing back we find function parseConfigVars in KRun.java, which call externalParse and pass the startSymbol to it. In the former commit we have a TODO here : // TODO(dwightguth): start symbols, and we simply pass Sorts.K() to the externalParse function. In the current version, the externalParse function is called in function getUserConfigVarsMap. here the sort is not simple Sorts.K() as before, but is given as: Sort sort = compiledDef.configurationVariableDefaultSorts.get("$" + name); the configurationVariableDefaultSorts is a new HashMap field in class CompiledDefinition, which is not there in the former commit. this map is initialized in the function initializeConfigurationVariableDefaultSorts in class CompiledDefinition. Therefore in current version, we can retrieve from imp.k the Stmts sort after $PGM and pass it to KRun to ensure normal execution of the KRun command in this issue.

So basically we think the first to problems put by @grosu has already be solved, what do you think? @grosu

We are currently working on problem3 to provide KastFrondEnd a possible default sort to parse the input. Thank you. @grosu @cos

[hksskh]

For the first problem, we manage to reproduce it in commit 0a16a1f51bb3b434935272e736c41e35750ec6c3 on 16 Jan. What causes this bad output is the block in function externalParse in KRun.java: if (output.exitCode != 0) { throw new ParseFailedException(new KException(KException.ExceptionType.ERROR, KException.KExceptionGroup.CRITICAL, "Parser returned a non-zero exit code: " + output.exitCode + "\nStdout:\n" + output.stdout + "\nStderr:\n" + output.stderr)); } Here those following Stdout and Stderr is the output.stdout and the output.stderr. While in current version, here we have: "\nStdout:\n" + new String(output.stdout) + "\nStderr:\n" + new String(output.stderr) So these previous output have now been passed to new String, and can then output more readable content at present. Here is how the problem 1 is fixed. @grosu

[hksskh]

The third problem put by @grosu is also fixed in current version. if the KRun command is proceeded without error, then the KAST command will also proceed normally. When running KRun, the function of parseConfigVars and externalParse will be called(both in KRun.java). And function getUserConfigVarsMap will then be called. In this function, we have an assertion: Sort sort = compiledDef.configurationVariableDefaultSorts.get("$" + name); assert sort != null: "Could not find configuration variable: $" + name; this assertion assure that there is a sort after $PGM in imp.k. Therefore, in KastFrontEnd(run function in this class is called when running KAST): CompiledDefinition def = compiledDef; org.kframework.kore.Sort sort = options.sort; if (sort == null) { if (env.get("KRUN_SORT") != null) { sort = Sort(env.get("KRUN_SORT")); } else { sort = def.programStartSymbol; } } if the KAST is not given a sort, then from this code block in KastFrontEnd in current version, the KAST will get the sort from environment variable, or from the programStartSymbol in compiledDefinition. In class CompiledDefinition, in the constructor, the programStartSymbol is initialized as: this.programStartSymbol = configurationVariableDefaultSorts.getOrDefault("$PGM", Sorts.K()); so here we can get the sort after $PGM. Therefore, KAST will have a not-null sort.

If the KRUN fails because of the assertion, that is, there is not sort after $PGM in imp.k, then we can see from above code that the programStartSymbol will return default sort of K to KAST, so KAST have a default not-null sort.

In sum, in any cases, the KAST will have the passed sort, or the sort after $PGM in definition, or the default K sort. So KAST will have a not-null sort to attempt to parse any input. We believe that the third problem has already be fixed. That is, we think all the three problems put by @grosu have been fixed in current version, so we need no modification and new pull request. Do you think this issue have been solved? Please review our explanation of problems in this issue. Thank you. @grosu @cos