runtimeverification / runtimeverification/llvm-backend

Buggy decision tree generated in case involving overloads

Open
#676 1 comment 0 reactions 0 assignees View on GitHub

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

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.