`kprove` crashes on claims without <k> tag or with repeated <k> tags

Open
#3,995 6 comments 1 reaction 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
3/5
Estimated time
1-2 days
Newbie friendliness
45/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Stale
Tech stack
python
Domain
compilers

Research direction

Reproduce both failures with spec-no-k-tag.k and spec-repeated-k-tag.k, using the empty test.k definition and the documented kompile and kprove commands. Compare the generated KORE from --dry-run with the frontend failure, then verify that claims without or with repeated tags no longer produce null sorts or a NoSuchElement exception.

Written by the indexing model from the issue text.

Description

With K version 6.2.24 (and probably others after 6.0.181), the command kprove may crash in one of two different ways when trying to process claims that used to work in earlier versions.

claim without <k> tags around the claim

spec-no-k-tag.k

module SPEC-NO-K-TAG
  imports TEST

  claim (_X => ?_) ~> .K
endmodule

The command kprove spec-no-k-tag.k crashes when calling the backend kore-exec because the generated kore contains null where a Sort should be.

$ kprove spec-no-k-tag.k 
kore-exec: [37802] Error (ErrorVerify):
    Error:
      module 'SPEC-NO-K-TAG':
      claim declaration:
      \implies (/tmp/.kprove-2024-02-16-13-48-35-222-904ec37e-072a-4a20-b563-6c83b247e774/spec.kore 10:20):
      (/tmp/.kprove-2024-02-16-13-48-35-222-904ec37e-072a-4a20-b563-6c83b247e774/spec.kore 10:20):
        Sort variable null not declared.
Using `kprove spec-no-k-tag.k --dry-run`, one can inspect the intermediate kore from the claim.
$ kprove spec-no-k-tag.k --dry-run
kore-exec /home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/./test-kompiled/definition.kore --module TEST --prove /tmp/.kprove-2024-02-16-13-49-18-274-e7b62ba3-2327-4065-b73c-b4ee7d623b42/spec.kore --spec-module SPEC-NO-K-TAG --output /tmp/.kprove-2024-02-16-13-49-18-274-e7b62ba3-2327-4065-b73c-b4ee7d623b42/result.kore

$ cat /tmp/.kprove-2024-02-16-13-49-18-274-e7b62ba3-2327-4065-b73c-b4ee7d623b42/spec.kore
[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)")]
module SPEC-NO-K-TAG

// imports
import TEST []


// claims
// claim _X=>?_Gen0 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(3761007019618ccc9ec3f08d7970ea9fd82125e826fed962533b93a9bf5565cc), org.kframework.attributes.Location(Location(4,9,4,25)), org.kframework.attributes.Source(Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
  claim{} \implies{null} (
      \and{null} (
      \top{null}(), Var'Unds'X:SortK{}), weakAlwaysFinally{null} (
       \exists{null} (Var'QuesUnds'Gen0:SortK{}, 
      \and{null} (
      Var'QuesUnds'Gen0:SortK{}, \top{null}()))))
  [UNIQUE'Unds'ID{}("3761007019618ccc9ec3f08d7970ea9fd82125e826fed962533b93a9bf5565cc"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(4,9,4,25)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]

endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1,1,5,10)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/jost/work/RV/code/haskell-backend/scratch/k-bug-null-sort/spec-no-k-tag.k)")]

Claim using the tags <k> twice

spec-repeated-k-tag.k

module SPEC-REPEATED-K-TAG
  imports TEST

  claim <k> _X </k> => <k> ?_ </k>
endmodule

The command kprove spec-repeated-k-tag.k fails in the frontend with a NoSuchElement exception.

[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/runtimeverification/k/issues
(NoSuchElementException: None.get)

The definition file for both is an empty test.k

module TEST
endmodule

$ kompile --backend haskell test.k
Dominant language
Python
Stars
591
Forks
163
No merged PRs in 30d

Contributor guide

Open the contributing guide

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.

More from runtimeverification/k

All issues in runtimeverification/k

Similar issues

More Python issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.