[K-Bug] checkSubstitutionCoverage error in Haskell backend
Open
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
Research direction
Start by saving the reported contents as lambda.k and simple.lambda, then run kompile --backend haskell lambda.k followed by krun simple.lambda to reproduce ErrorRewritesInstantiation. Trace the checkSubstitutionCoverage failure from the Haskell backend entry point; done means the minimized lambda-term example no longer triggers this error or its cause and expected behavior are documented.
Written by the indexing model from the issue text.
Description
What component is the issue in?
haskell-backend
Which command
- kompile
- kast
- krun
- kprove
- kprovex
- ksearch
What K Version?
v5.6.90 (Thu May 11 22:42:38 CEST 2023)
Operating System
Linux
K Definitions (If Possible)
This is minimized from a larger file that is supposed to reduce λ-terms (NB I am a beginner with K).
module LAMBDA-SYNTAX
import DOMAINS
syntax Lambda ::= Id
| Lambda Lambda
| "/\\\\" Id "." Lambda
| "(" Lambda ")" [bracket]
endmodule
module LAMBDA
imports LAMBDA-SYNTAX
syntax State ::= ListFreeVariables()
| RenameBoundVariables()
| Reduce()
| Replace()
syntax KItem ::= AppLeftFreezer(Lambda)
| AppRightFreezer(Lambda)
| AbstracFreezer(Id)
| todo(KItem)
| done(KItem)
configuration
<state> ListFreeVariables() </state>
<list-free-variables> todo($PGM) ~> .K </list-free-variables>
<all-free-variables> .Set </all-free-variables>
<bound-variables> .Set ~> .K </bound-variables>
<rename-bound-variables> todo($PGM) ~> .K </rename-bound-variables>
<bound-variable-renamings> .Map ~> .K </bound-variable-renamings>
<bound-variable-renaming-sources> .Map </bound-variable-renaming-sources>
<reduce> .K </reduce>
<replace> .K </replace>
<replace-var> .K </replace-var>
<replace-term> .K </replace-term>
rule <state> ListFreeVariables() </state>
<list-free-variables>
todo(X:Id) ~> Rest => done(X:Id) ~> Rest
</list-free-variables>
<bound-variables> _S SetItem(X) ~> _BoundRest </bound-variables>
rule <state> ListFreeVariables() </state>
<list-free-variables>
todo(X:Id) ~> Rest => done(X:Id) ~> Rest
</list-free-variables>
<all-free-variables>
S => S SetItem(X)
</all-free-variables>
<bound-variable-renaming-sources>
M => (X |-> 0) M
</bound-variable-renaming-sources>
[owise]
rule <state> ListFreeVariables() </state>
<list-free-variables>
todo(U V) ~> Rest => todo(U) ~> AppRightFreezer(V) ~> Rest
</list-free-variables>
rule <state> ListFreeVariables() </state>
<list-free-variables>
todo(/\\ X . U) ~> Rest => todo(U) ~> AbstracFreezer(X) ~> Rest
</list-free-variables>
<bound-variables>
S ~> BoundRest => S SetItem(X) ~> S ~> BoundRest
</bound-variables>
rule [debugme]: <state> ListFreeVariables() </state>
<list-free-variables>
done(U) ~> AbstracFreezer(X) ~> Rest => done(/\\ X . U) ~> Rest
</list-free-variables>
<bound-variables>
_S ~> BoundRest => BoundRest
</bound-variables>
endmodule
Steps to Reproduce
Save the above as lambda.k. Save the following as simple.lambda:
(/\\ x . x) (/\\ y . (/\\ z . (y z)))
Then run:
kompile --backend haskell lambda.k
krun simple.lambda
This gives this huge error message:
kore-exec: [334353] Error (ErrorRewritesInstantiation):
While rewriting the configuration:
\and{SortGeneratedTopCell{}}(
/* term: */
/* T Fn D Sfa Cl */
Lbl'-LT-'generatedTop'-GT-'{}(
/* T Fn D Sfa Cl */
Lbl'-LT-'state'-GT-'{}(
/* T Fn D Sfa Cl */
LblListFreeVariables'LParRParUnds'LAMBDA'Unds'State{}()
),
/* T Fn D Sfa Cl */
Lbl'-LT-'list-free-variables'-GT-'{}(
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cl */
Lbldone'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'KItem{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortKItem{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "x")
)
),
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cl */
LblAbstracFreezer'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'Id{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "x")
),
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cl */
LblAppRightFreezer'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'Lambda{}(
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "y"),
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"z"),
/* T Fn D Sfa Cl */
Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Lambda'Unds'Lambda{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"y")
),
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"z")
)
)
)
)
),
/* T Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* T Fn D Sfa Cl */
Lbl'-LT-'all-free-variables'-GT-'{}(
/* T Fn D Sfa Cl */ /* InternalSet: */ Lbl'Stop'Set{}()
),
/* T Fn D Sfa Cl */
Lbl'-LT-'bound-variables'-GT-'{}(
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortSet{}, SortKItem{}}(
/* T Fn D Sfa Cl */
/* InternalSet: */ /* concrete element: */ LblSetItem{}(
/* Inj: */ inj{SortId{}, SortKItem{}}(
\dv{SortId{}}("x")
)
)
),
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortSet{}, SortKItem{}}(
/* T Fn D Sfa Cl */
/* InternalSet: */ Lbl'Stop'Set{}()
),
/* T Fn D Sfa Cl */ dotk{}()
)
)
),
/* T Fn D Sfa Cl */
Lbl'-LT-'rename-bound-variables'-GT-'{}(
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cl */
Lbltodo'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'KItem{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortLambda{}, SortKItem{}}(
/* T Fn D Sfa Cl */
Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Lambda'Unds'Lambda{}(
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "x"),
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"x")
)
),
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "y"),
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"z"),
/* T Fn D Sfa Cl */
Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Lambda'Unds'Lambda{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"y")
),
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"z")
)
)
)
)
)
)
),
/* T Fn D Sfa Cl */ dotk{}()
)
),
/* T Fn D Sfa Cl */
Lbl'-LT-'bound-variable-renamings'-GT-'{}(
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortMap{}, SortKItem{}}(
/* T Fn D Sfa Cl */
/* InternalMap: */ Lbl'Stop'Map{}()
),
/* T Fn D Sfa Cl */ dotk{}()
)
),
/* T Fn D Sfa Cl */
Lbl'-LT-'bound-variable-renaming-sources'-GT-'{}(
/* T Fn D Sfa Cl */ /* InternalMap: */ Lbl'Stop'Map{}()
),
/* T Fn D Sfa Cl */
Lbl'-LT-'reduce'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}()),
/* T Fn D Sfa Cl */
Lbl'-LT-'replace'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}()),
/* T Fn D Sfa Cl */
Lbl'-LT-'replace-var'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}()),
/* T Fn D Sfa Cl */
Lbl'-LT-'replace-term'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}()),
/* T Fn D Sfa Cl */
Lbl'-LT-'generatedCounter'-GT-'{}(
/* T Fn D Sfa Cl */ \dv{SortInt{}}("0")
)
),
\and{SortGeneratedTopCell{}}(
/* predicate: */
/* D Sfa */ \top{SortGeneratedTopCell{}}(),
/* substitution: */
\top{SortGeneratedTopCell{}}()
))
Unable to instantiate semantic rule at /home/jean/Documents/bug-report/lambda.k:69:19-75:26
Unification did not find a solution for the variables:
RuleVar'Unds'S RuleVarBoundRest
The unification solution was:
\and{SortGeneratedTopCell{}}(
/* term: */
/* Spa */
\rewrites{SortGeneratedTopCell{}}(
/* Spa */
\and{SortGeneratedTopCell{}}(
/* D Sfa */ \top{SortGeneratedTopCell{}}(),
/* T Fn D Sfa */
Lbl'-LT-'generatedTop'-GT-'{}(
/* T Fn D Sfa Cl */
Lbl'-LT-'state'-GT-'{}(
/* T Fn D Sfa Cl */
LblListFreeVariables'LParRParUnds'LAMBDA'Unds'State{}()
),
/* T Fn D Sfa */
Lbl'-LT-'list-free-variables'-GT-'{}(
/* T Fn D Sfa */
kseq{}(
/* T Fn D Sfa */
Lbldone'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'KItem{}(
/* T Fn D Sfa */
/* Inj: */ inj{SortLambda{}, SortKItem{}}(
/* T Fn D Sfa */ RuleVarU:SortLambda{}
)
),
/* T Fn D Sfa */
kseq{}(
/* T Fn D Sfa */
LblAbstracFreezer'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'Id{}(
/* T Fn D Sfa */ RuleVarX:SortId{}
),
/* T Fn D Sfa */ RuleVarRest:SortK{}
)
)
),
/* T Fn D Sfa */
RuleVar'Unds'Gen0:SortAllFreeVariablesCell{},
/* T Fn D Sfa */
Lbl'-LT-'bound-variables'-GT-'{}(
/* T Fn D Sfa */
append{}(
/* T Fn D Sfa */ RuleVar'Unds'S:SortK{},
/* T Fn D Sfa */ RuleVarBoundRest:SortK{}
)
),
/* T Fn D Sfa */
RuleVar'Unds'Gen1:SortRenameBoundVariablesCell{},
/* T Fn D Sfa */
RuleVar'Unds'Gen2:SortBoundVariableRenamingsCell{},
/* T Fn D Sfa */
RuleVar'Unds'Gen3:SortBoundVariableRenamingSourcesCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen4:SortReduceCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen5:SortReplaceCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen6:SortReplaceVarCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen7:SortReplaceTermCell{},
/* T Fn D Sfa */
RuleVar'Unds'Gen8:SortGeneratedCounterCell{}
)
),
/* T Fn D Spa */
Lbl'-LT-'generatedTop'-GT-'{}(
/* T Fn D Sfa Cl */
Lbl'-LT-'state'-GT-'{}(
/* T Fn D Sfa Cl */
LblListFreeVariables'LParRParUnds'LAMBDA'Unds'State{}()
),
/* T Fn D Spa */
Lbl'-LT-'list-free-variables'-GT-'{}(
/* T Fn D Spa */
kseq{}(
/* T Fn D Spa */
Lbldone'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'KItem{}(
/* T Fn D Spa */
/* Inj: */ inj{SortLambda{}, SortKItem{}}(
/* T Fn D Spa */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa */ RuleVarX:SortId{},
/* T Fn D Sfa */ RuleVarU:SortLambda{}
)
)
),
/* T Fn D Sfa */ RuleVarRest:SortK{}
)
),
/* T Fn D Sfa */ RuleVar'Unds'Gen0:SortAllFreeVariablesCell{},
/* T Fn D Spa */
Lbl'-LT-'bound-variables'-GT-'{}(
/* T Fn D Sfa */ RuleVarBoundRest:SortK{}
),
/* T Fn D Sfa */
RuleVar'Unds'Gen1:SortRenameBoundVariablesCell{},
/* T Fn D Sfa */
RuleVar'Unds'Gen2:SortBoundVariableRenamingsCell{},
/* T Fn D Sfa */
RuleVar'Unds'Gen3:SortBoundVariableRenamingSourcesCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen4:SortReduceCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen5:SortReplaceCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen6:SortReplaceVarCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen7:SortReplaceTermCell{},
/* T Fn D Sfa */ RuleVar'Unds'Gen8:SortGeneratedCounterCell{}
)
),
\and{SortGeneratedTopCell{}}(
/* predicate: */
/* Sfa */
\equals{SortK{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortSet{}, SortKItem{}}(
/* T Fn D Sfa Cl */
/* InternalSet: */ /* concrete element: */ LblSetItem{}(
/* Inj: */ inj{SortId{}, SortKItem{}}(
\dv{SortId{}}("x")
)
)
),
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortSet{}, SortKItem{}}(
/* T Fn D Sfa Cl */ /* InternalSet: */ Lbl'Stop'Set{}()
),
/* T Fn D Sfa Cl */ dotk{}()
)
),
/* T Fn D Sfa */
append{}(
/* T Fn D Sfa */ RuleVar'Unds'S:SortK{},
/* T Fn D Sfa */ RuleVarBoundRest:SortK{}
)
),
/* substitution: */
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortAllFreeVariablesCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVar'Unds'Gen0:SortAllFreeVariablesCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'all-free-variables'-GT-'{}(
/* T Fn D Sfa Cl */ /* InternalSet: */ Lbl'Stop'Set{}()
)
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortRenameBoundVariablesCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */
RuleVar'Unds'Gen1:SortRenameBoundVariablesCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'rename-bound-variables'-GT-'{}(
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cl */
Lbltodo'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'KItem{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortLambda{}, SortKItem{}}(
/* T Fn D Sfa Cl */
Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Lambda'Unds'Lambda{}(
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "x"),
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"x")
)
),
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "y"),
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"z"),
/* T Fn D Sfa Cl */
Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Lambda'Unds'Lambda{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"y")
),
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */
"z")
)
)
)
)
)
)
),
/* T Fn D Sfa Cl */ dotk{}()
)
)
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortBoundVariableRenamingsCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */
RuleVar'Unds'Gen2:SortBoundVariableRenamingsCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'bound-variable-renamings'-GT-'{}(
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortMap{}, SortKItem{}}(
/* T Fn D Sfa Cl */
/* InternalMap: */ Lbl'Stop'Map{}()
),
/* T Fn D Sfa Cl */ dotk{}()
)
)
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortBoundVariableRenamingSourcesCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */
RuleVar'Unds'Gen3:SortBoundVariableRenamingSourcesCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'bound-variable-renaming-sources'-GT-'{}(
/* T Fn D Sfa Cl */ /* InternalMap: */ Lbl'Stop'Map{}()
)
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortReduceCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVar'Unds'Gen4:SortReduceCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'reduce'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}())
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortReplaceCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVar'Unds'Gen5:SortReplaceCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'replace'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}())
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortReplaceVarCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVar'Unds'Gen6:SortReplaceVarCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'replace-var'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}())
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortReplaceTermCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVar'Unds'Gen7:SortReplaceTermCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'replace-term'-GT-'{}(/* T Fn D Sfa Cl */ dotk{}())
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVar'Unds'Gen8:SortGeneratedCounterCell{},
/* T Fn D Sfa Cl */
Lbl'-LT-'generatedCounter'-GT-'{}(
/* T Fn D Sfa Cl */ \dv{SortInt{}}("0")
)
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortK{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVarRest:SortK{},
/* T Fn D Sfa Cl */
kseq{}(
/* T Fn D Sfa Cl */
LblAppRightFreezer'LParUndsRParUnds'LAMBDA'Unds'KItem'Unds'Lambda{}(
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "y"),
/* T Fn D Sfa Cl */
Lbl'SlshBashBashUndsStopUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Id'Unds'Lambda{}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "z"),
/* T Fn D Sfa Cl */
Lbl'UndsUndsUnds'LAMBDA-SYNTAX'Unds'Lambda'Unds'Lambda'Unds'Lambda{}(
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "y")
),
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */
\dv{SortId{}}(/* T Fn D Sfa Cl */ "z")
)
)
)
)
),
/* T Fn D Sfa Cl */ dotk{}()
)
),
\and{SortGeneratedTopCell{}}(
/* Spa */
\equals{SortLambda{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVarU:SortLambda{},
/* T Fn D Sfa Cli */
/* Inj: */ inj{SortId{}, SortLambda{}}(
/* T Fn D Sfa Cl */ \dv{SortId{}}(/* T Fn D Sfa Cl */ "x")
)
),
/* Spa */
\equals{SortId{}, SortGeneratedTopCell{}}(
/* T Fn D Sfa */ RuleVarX:SortId{},
/* T Fn D Sfa Cl */ \dv{SortId{}}(/* T Fn D Sfa Cl */ "x")
)
)))))))))))
))
Error! Please report this.
CallStack (from HasCallStack):
checkSubstitutionCoverage, called at src/Kore/Rewrite/RewriteStep.hs:253:13 in kore-0.60.0.0-4eN71WxNolKFApfOeZr3qd:Kore.Rewrite.RewriteStep
Created bug report: kore-exec.tar.gz
[Error] krun: kore-exec ./lambda-kompiled/haskellDefinition.bin --module LAMBDA
--pattern .krun-2023-05-14-21-00-28-tTPvT1C4Fx/tmp.in.OJdxlSuE2I --output
.krun-2023-05-14-21-00-28-tTPvT1C4Fx/result.kore
[Error] krun: Backend crashed during rewriting with exit code 1
Here is the file it created: kore-exec.tar.gz
If the LLVM backend is used, it doesn't crash, but it stops at a point where I would have thought that the rule marked debugme would apply. Not sure if I'm doing something silly.
I tried debugging with GDB but it gives errors as well. Not sure if this is related. Excerpt from GDB session:
jean@ubuntu22:~/Documents/bug-report$ kompile --enable-llvm-debug lambda.k
jean@ubuntu22:~/Documents/bug-report$ krun --debugger simple.lambda
GNU gdb (Ubuntu 12.1-0ubuntu1~22.04) 12.1
Copyright (C) 2022 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<https://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
<http://www.gnu.org/software/gdb/documentation/>.
For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ./lambda-kompiled/interpreter...
(gdb) k start
Temporary breakpoint 1 at 0x73e50
Starting program: /home/jean/Documents/bug-report/lambda-kompiled/interpreter .krun-2023-05-14-21-03-48-uFQyu6QtbK/tmp.in.WhF8QtUabr -1 .krun-2023-05-14-21-03-48-uFQyu6QtbK/result.kore
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
Temporary breakpoint 1, 0x00005555555c7e50 in main ()
0x00005555555a5f20 in k_step (subject=<generatedTop>
<state>
ListFreeVariables ( )
</state>
<list-free-variables>
todo ( ( /\\ x . x ) /\\ y . /\\ z . ( y z ) ) ~> .
</list-free-variables>
<all-free-variables>
.Set
</all-free-variables>
<bound-variables>
.Set ~> .
</bound-variables>
<rename-bound-variables>
todo ( ( /\\ x . x ) /\\ y . /\\ z . ( y z ) ) ~> .
</rename-bound-variables>
<bound-variable-renamings>
.Map ~> .
</bound-variable-renamings>
<bound-variable-renaming-sources>
.Map
</bound-variable-renaming-sources>
<reduce>
.
</reduce>
<replace>
.
</replace>
<replace-var>
.
</replace-var>
<replace-term>
.
</replace-term>
</generatedTop>) at /home/jean/Documents/bug-report/lambda.k:56
56 rule <state> ListFreeVariables() </state>
(gdb) k step
Continuing.
Temporary breakpoint -9, 0x00005555555a5f20 in k_step (subject=<generatedTop>
<state>
ListFreeVariables ( )
</state>
<list-free-variables>
todo ( /\\ x . x ) ~> AppRightFreezer ( /\\ y . /\\ z . ( y z ) ) ~> .
</list-free-variables>
<all-free-variables>
.Set
</all-free-variables>
<bound-variables>
.Set ~> .
</bound-variables>
<rename-bound-variables>
todo ( ( /\\ x . x ) /\\ y . /\\ z . ( y z ) ) ~> .
</rename-bound-variables>
<bound-variable-renamings>
.Map ~> .
</bound-variable-renamings>
<bound-variable-renaming-sources>
.Map
</bound-variable-renaming-sources>
<reduce>
.
</reduce>
<replace>
.
</replace>
<replace-var>
.
</replace-var>
<replace-term>
.
</replace-term>
</generatedTop>) at /home/jean/Documents/bug-report/lambda.k:56
56 rule <state> ListFreeVariables() </state>
(gdb) k step
Continuing.
Temporary breakpoint -10, 0x00005555555a5f20 in k_step (subject=<generatedTop>
<state>
ListFreeVariables ( )
</state>
<list-free-variables>
todo ( x ) ~> AbstracFreezer ( x ) ~> AppRightFreezer ( /\\ y . /\\ z . ( y z ) ) ~> .
</list-free-variables>
<all-free-variables>
.Set
</all-free-variables>
<bound-variables>
SetItem ( x ) ~> .Set ~> .
</bound-variables>
<rename-bound-variables>
todo ( ( /\\ x . x ) /\\ y . /\\ z . ( y z ) ) ~> .
</rename-bound-variables>
<bound-variable-renamings>
.Map ~> .
</bound-variable-renamings>
<bound-variable-renaming-sources>
.Map
</bound-variable-renaming-sources>
<reduce>
.
</reduce>
<replace>
.
</replace>
<replace-var>
.
</replace-var>
<replace-term>
.
</replace-term>
</generatedTop>) at /home/jean/Documents/bug-report/lambda.k:56
56 rule <state> ListFreeVariables() </state>
(gdb) k step
Continuing.
Temporary breakpoint -11, 0x00005555555a5f20 in k_step (subject=<generatedTop>
<state>
ListFreeVariables ( )
</state>
<list-free-variables>
done ( x ) ~> AbstracFreezer ( x ) ~> AppRightFreezer ( /\\ y . /\\ z . ( y z ) ) ~> .
</list-free-variables>
<all-free-variables>
.Set
</all-free-variables>
<bound-variables>
SetItem ( x ) ~> .Set ~> .
</bound-variables>
<rename-bound-variables>
todo ( ( /\\ x . x ) /\\ y . /\\ z . ( y z ) ) ~> .
</rename-bound-variables>
<bound-variable-renamings>
.Map ~> .
</bound-variable-renamings>
<bound-variable-renaming-sources>
.Map
</bound-variable-renaming-sources>
<reduce>
.
</reduce>
<replace>
.
</replace>
<replace-var>
.
</replace-var>
<replace-term>
.
</replace-term>
</generatedTop>) at /home/jean/Documents/bug-report/lambda.k:56
56 rule <state> ListFreeVariables() </state>
(gdb) k match LAMBDA.debugme subject
Traceback (most recent call last):
File "<string>", line 793, in invoke
gdb.error: No type named .
Python Exception <class 'gdb.error'>: No type named .
Error occurred in Python: No type named .
Expected Results
No crash.
- Dominant language
- Python
- Stars
- 591
- Forks
- 163
- PR merge metrics
- No merged PRs in 30d
Contributor guide
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.
More from runtimeverification/k
-
runtimeverification/k#4939 · 1 assignee ·
-
Concolic Explorer Open
Difficulty 5/5 Over a week Newbie friendliness 32/100
runtimeverification/k#4937 ·
-
Difficulty 5/5 Over a week Newbie friendliness 30/100
runtimeverification/k#4936 ·
-
type:epic
runtimeverification/k#4934 · 4 comments · 1 assignee ·
-
runtimeverification/k#4924 · 1 assignee ·
All issues in runtimeverification/k
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
bancolombia/sentinel#23 ·
-
test md OpenCI
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
-
integration:quickjs org:external priority:backlog topic:code-interpreter topic:middleware type:feature
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
langchain-ai/deepagents#6450 ·
-
bug client
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100