runtimeverification / runtimeverification/haskell-backend

Invalid variable names created by internalized rules

Open
#3,777 3 comments 0 reactions 2 assignees View on GitHub

@nwatson22 is already working on this.

Since Mar 26, 2024.

bug runtimeverification/hs-backend-booster
Dominant language
Haskell
Stars
224
Forks
43
PR merge metrics
No merged PRs in 30d

Description

I stumbled across a case where a Rule# prefix is seemingly being appended to the beginning of a variable name for the generatedCounter cell possibly caused by using a claim as a lemma (the last request/response in this bug report). Is this a genuine bug? See https://github.com/runtimeverification/pyk/pull/959

<generatedCounter> in the response looks like this:

                  {
                     "tag":"App",
                     "name":"Lbl'-LT-'generatedCounter'-GT-'",
                     "sorts":[
                        
                     ],
                     "args":[
                        {
                           "tag":"EVar",
                           "name":"Rule#Var'QuesUnds'GENERATEDCOUNTER'Unds'CELL'Unds'6de8d71b",
                           "sort":{
                              "tag":"SortApp",
                              "name":"SortInt",
                              "args":[
                                 
                              ]
                           }
                        }
                     ]
                  }

Executing with the legacy backend yields the same variable name Var'QuesUnds'GENERATEDCOUNTER'Unds'CELL'Unds'6de8d71b without the Rule# prefix.

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.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.