runtimeverification / runtimeverification/llvm-backend
Buggy decision tree generated in case involving overloads
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 43
- Forks
- 22
- PR merge metrics
- No merged PRs in 30d
Description
I have another example of the llvm backend generating broken decision trees. It's quite remarkable that I've managed to uncover so many of these issues that have gone undetected for so long.
Here is the K definition which reproduces the error:
module TEST-COMMON
syntax ConstructorName [token]
syntax Name [token]
syntax Exp ::= Name
syntax Exp ::= Val
syntax Val ::= Name
syntax Exps ::= List{Exp,","} [klabel(exps)]
syntax Vals ::= List{Val,","} [klabel(exps)]
syntax Names ::= List{Name,","} [klabel(exps)]
syntax Exps ::= Names
syntax Exps ::= Vals
syntax Vals ::= Names
syntax Exp ::= ConstructorName "(" Exps ")" [klabel(constructor)]
syntax Val ::= ConstructorName "(" Vals ")" [klabel(constructor)]
endmodule
module TEST-SYNTAX
imports TEST-COMMON
syntax ConstructorName ::= r"[A-Za-z]+" [token]
syntax Name ::= ConstructorName [token]
endmodule
module TEST
imports TEST-COMMON
syntax Names ::= getNames(Exp) [function]
rule getNames(C:ConstructorName(E:Exp,Es:Exps)) => getNames(E)
rule getNames(N:Name) => N
rule (E::Exp => getNames(E):KItem)
endmodule
The program that reproduces the error is Pair(m,n). What happens is that the occurrence used to get the value bound to the variable E in the first rule for getNames is incorrectly bound, and thus it reads an undefined value when the value on the stack is loaded to be passed to the function that constructs the right hand side. this leads to an incorrect term representation that either segfaults or simply gets stuck. The correct output of this program ought to be m.
I'm not entirely sure exactly what is going wrong with the decision tree generation process yet. It appears to be related to the case where we make use of MakePattern nodes to construct an injection which is not actually part of the term being matched. This has something to do with the overloaded productions, in particular, it appears due to the conjunction of the overload on exps and the overload on constructor. Somehow the case when you match on a Val that contains a Names leads it to use the wrong occurrence when constructing the pattern which is passed to the leaf node. I know what the correct occurrence ought to be, but I still need to reason through exactly where the current algorithm is going wrong.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the K definition and the Pair(m,n) reproducer in the issue, then trace LLVM backend decision-tree generation around MakePattern nodes, overloaded exps and constructor productions, and the occurrence bound to E. Done means the generated tree handles this case correctly, produces m, and no longer segfaults or gets stuck.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 20/100