Closed virgil-serbanuta closed 2 years ago
ehildenb
commented
3 years ago This is unexpected, because we expect that #as pattern has the exact same sort on the LHS and RHS.
(1, a(2)) is sort List, and X is Thing, they are in the same connected component.
ehildenb
commented
3 years ago @virgil-serbanuta are you blocked on this? It seems you can fix this with parens.
virgil-serbanuta
commented
3 years ago I'm not blocked.
gtrepta
commented
2 years ago At some point during the proof parsing, the parseStringTerm method in the ParseInModule class has an ambiguous node:
amb( #KAs( `_,__TMP_MyList_Elem_MyList`(#token("1","Int"),`a(_)_TMP_Thing_Int`(#token("2","Int")))
, #SemanticCastToThing(#token("X","#KVariable"))
)
, `_,__TMP_MyList_Elem_MyList`( #token("1","Int")
, #KAs(`a(_)_TMP_Thing_Int`(#token("2","Int"))
,#SemanticCastToThing(#token("X","#KVariable"))
)
)
)The second element in the node has the intended parsing of #as, but it's resolving to the first element, which of course ends up causing the wrong expected sort.
I notice the X variable is inside of a #SemanticCastToThing. Does the type inferencer mishandle this?
gtrepta
commented
2 years ago What is the expected sort relation of _ #as X:Thing?
It looks like the problem emerges from the z3 statements generated by ExpectedSortsVisitor. It's hard for me to parse through, but it looks like it's asserting that Sort(X) <= Sort(_), which is satisfied in this case if Sort(_) == MyList. I think it makes sense if the sort relation is Sort(_) <= Sort(X), but it doesn't looks like that's anywhere in the assertions. @radumereuta Can you shed some light on the assertions made by ExpectedSortsVisitor?
The claim will parse and run correctly if it's written as claim count(1, a(2) #as X::Thing) => 2 (strict cast)
Attached is the z3 script that gets generated: z3.txt
I think FreshVarSort_4_15_4_34_#KAs represents (1, a(2)) #as X:Thing
and FreshVarSort_4_18_4_34_#KAs represents a(2) #as X:Thing
radumereuta
commented
2 years ago I think this is a duplicate of this issue: https://github.com/runtimeverification/k/issues/2219 The problem here is that the type inferencer discards one of the ambiguities when it shouldn't.
In https://github.com/runtimeverification/k/issues/2219 we avoided fixing the underlying issue by adding global priority to #let #in
gtrepta
commented
2 years ago Yes, something I forgot to mention is that it does seem to be dropping the correct term after the wrong one is satisfied. I couldn't tell if that's exactly what the type inferencer is doing though.
radumereuta
commented
2 years ago We need to tinker a bit with the soft constraints to force Z3 to generate some Bottom value for variables which are left out of the constraint. Bottom should be <=Sort than all the sorts.
Another issue is when you are invalidating the solution you just got, you force X to not be Thing and not allowing Z3 to explore the other branches.
Another solution would be to just remove them from Z3 because we don't need them. We can calculate them directly in Java faster. We just have to look at the restriction given by the parent node.
radumereuta
commented
2 years ago Dwight has some work that could improve performance for the type inferencer committed here: https://github.com/runtimeverification/k/tree/z3
To profile the time taken by the type inferencer you can use --profile-rule-parsing <file> in kompile or kprove. This also disables caching.
TermCons is the data structure similar to KApp, but it has a reference to a production instead of KLabel. Note that the items: PStack[Term] are in reverse order for performance reasons.
The job of the TypeInferencer is to infer types for variables in order to maximize the chances of the rule to match.
Here are some more written examples about problems with parsing and type inferencing frequently found in K: https://docs.google.com/document/d/14ZsLAfZqq0UJVdqHFQCo4aY0AGnzHbRFDEPEfZRPg34/edit
Notes from the meeting:
//syntax Exp ::= Exp "*" Exp
// > Exp "+" Exp
syntax KBott ::= K "=>" K
syntax K ::= Exp
syntax Exp ::= Int
syntax Int ::= KBott
syntax {Sort} Sort ::= Sort "=>" Sort
syntax Exp ::= Exp "=>" Exp
syntax Int ::= Int "=>" Int
// rule 1 + 2 * 3 => .
// rule 1 + (2 => 3)
// amb(+(1, *(2,3))
// *(+(1,2),3)))
// non-assoc 1 => 2 => 3
// (Id, Exp), (Exp, Id)
// syntax Exp ::= Exp "+" Int
// syntax Exp ::= Int "+" Exp
// rule A + B => . // type error
// syntax Exp ::= Exp "+" Exp
syntax Exps ::= Exp “,” Exps | Exp
syntax Exp ::= [A-Za-z][A-Za-z0-9]*
syntax Stmt ::= “val” Exps “;” Stmt
syntax KBott ::= “(“ K “)” | “(“ Id “,” Stmt “)”
rule val X; S => (X,S)
Here the question is: is the RHS of the rule (Id, Stmt) or (Exp, Exp)?
// Z3 query: (X:Exps and S:Stmt) and ((X:Id and S:Stmt) or (X:Exp and S:Exp))
// the sort DAG
// K at the top, KBott at the bottom, every other user sort in between
// rule X:Id => X:Stmt
// if you include KBott in the sort DAG you can use it as a marker to detect type errors
// because you will always find a solution for type inference. If the only one you find has
// a KBott in it, then you can report it as a type error.I remember @dwightguth mentioning that removing the soft constraints that the type inferencer generates could help with correctness, so I became curious and gave it a try. Doing that fixed the proof above. I expected the performance to suffer, but when I tried to measure it I instead found that the performance improved?
I kompiled KEVM with --profile-rule-parsing and summed up the column of times measured by the type inferencer. For the unmodified type inferencer, the sum was 78402, and with the modified inferencer it was 33428. The total kompile process ran in 582.01 seconds unmodified and 275.08 seconds modified.
radumereuta
commented
2 years ago To test the evm semantics I usually add these extra options for proofs in kevm script:
proof_args+=( -v --dry-run --profile-rule-parsing "timings/${run_file}.log" )I also like to add -v in the Makefile for kompile.
How to run the proofs:
radu@radu:~/work/evm-semantics$ time make test-prove -j 8 -O > evm-kprove-dry-run-j8-z3-15.txt3 2>&1This uses a lot of RAM, so you will need a beefy machine.
dwightguth
commented
2 years ago As I told Guy, there is a way to fix this issue, I believe, that doesn't require futzing with the z3 constraints.
Essentially, right now the issue is that we do not in any way try to choose optimal values for sort parameters of parametric sorts and productions, but we still try to apply a single sort for each parameters across all branches of the parse forest.
The solution is to simply not use the z3 model to compute these values. Instead, in TypeInferenceVisitor.java, when we use the TypeCheckVisitor to compute the sort of parametric productions here: https://github.com/runtimeverification/k/blob/26cdcf2d18dce2eea6953da73af77be12edcbdd6/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java#L227
Instead, we should simply use the same logic we use later on in the compilation pipeline (here: https://github.com/runtimeverification/k/blob/26cdcf2d18dce2eea6953da73af77be12edcbdd6/kernel/src/main/java/org/kframework/compile/AddSortInjections.java#L251) to compute the sort of the parametric production using the sorts of its children and the expected sort at that position. This means on each branch of the ambiguity, we may assign a different sort to the parameters of the same term, which ought to solve this issue.
One nuance is what to do if one or more of the children of the parametric production is an ambiguity node, in which case it is not trivial to compute the sort of that child of the production since it may have different sorts on different branches of the ambiguity. If this happens, the solution is to push the ambiguity up one level and then retry with the modified ast. You can see one example of pushing an ambiguity up here: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushTopAmbiguityUp.java
This code will probably have to be tweaked some, but it ought to give you a place to start.
radumereuta
commented
2 years ago Make sure to test the performance on C and KEVM.
You can profile with kompile --verbose and --profile-rule-parsing <file>
gtrepta
commented
2 years ago Here's a first attempt, it doesn't work though.
https://github.com/runtimeverification/k/commit/c1049c2c4c4070abb4d832fec867d1a4f45f1594
Trying kprove proof-temp.k throws this error:
org.kframework.utils.errorsystem.KEMException: [Error] Internal: Could not compute least upper bound for rewrite sort. Possible candidates: []
Source(/home/gtrepta/runtimeverification/k/type-inferencer/temp/proof-tmp.k)
Location(4,9,4,40)
4 | claim count(1, a(2) #as X:Thing) => 2
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~The lub function in AddSortInjections ends up with an empty set of sorts to choose from.
gtrepta
commented
2 years ago I have pushed up a branch sort-param-inference with an implementation of @dwightguth's solution above, with as much code re-use as possible. It isn't correct yet, still. The next step should be to determine if parts of the re-used code need to be reimplemented for this use case and then implement them.
gtrepta
commented
2 years ago I made some interesting progress. I think I have the issue for this card partially fixed, the type inferencer now knows to keep both branches of the ambiguity. I believe the ambiguity is supposed to be resolved later in the pipeline, but I get this error message instead, which makes it seem to me like there's a second bug that's affecting this issue:
[Error] Inner Parser: Parsing ambiguity.
1: syntax {Sort} Sort ::= Sort "#as" Sort [klabel(#KAs), symbol]
#KAs(`_,__TMP_MyList_Elem_MyList`(#token("1","Int"),`a(_)_TMP_Thing_Int`(#token("2","Int"))),#SemanticCastToThing(#token("X","#KVariable")))
2: syntax MyList ::= Elem "," MyList
`_,__TMP_MyList_Elem_MyList`(#token("1","Int"),#KAs(`a(_)_TMP_Thing_Int`(#token("2","Int")),#SemanticCastToThing(#token("X","#KVariable"))))
Source(/home/gtrepta/runtimeverification/k/type-inferencer/temp/proof-tmp.k)
Location(4,15,4,34)
4 | claim count(1, a(2) #as X:Thing) => 2
. ^~~~~~~~~~~~~~~~~~~
[Error] Compiler: Had 1 parsing errors.My work still isn't correct as it at least doesn't pass one of the regression tests. tests/regression-new/fun-llvm will throw an exception because while computing the least upper bound, it runs into an unexpected ambiguity node. I'm already lifting ambiguity nodes that are direct children of the term, but there are nested ambiguities further down the tree in this test. I think the only option will be to recursively lift all of the ambiguities, that sounds overkill though.
I've opened a PR with my work so far. Even though it's a draft I would appreciate @dwightguth or @radumereuta taking a look at it to see if it looks like it's on the right track. #2923
radumereuta
commented
2 years ago @gtrepta that's actually the expected behavior. See this other issue which was similar in nature: https://github.com/runtimeverification/k/issues/2219 Now we just have to think about how to fix the tests.
dwightguth
commented
2 years ago Duplicate of #2219
K Version
Tell us what version of K you are using.
Example:
Description
Kprove parses #as in a way incompatible with the sorts around it and, instead of printing an error, sends the broken parse to the haskell backend.
Input Files
File:
tmp.kFile:
proof-tmp.kReproduction Steps
Running the proof like this:
produces a long Haskell backend error:
Looking at the generated files, it seems that the frontend parsed the list above as
which is obviously wrong.
Expected Behavior
Either kprove should provide an error that the
#assorts do not match, or it should parse the list as1, (a(2) #as X:Thing).