[K-Bug] The LLVM backend ignores rule priorities
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 4/5
- Tiempo estimado
- 3-5 días
- Aptitud para principiantes
- 35/100
- Tipo de issue
- Error
- Claridad
- Bastante claro
- Estado de actividad
- Estancado
- Stack tecnológico
- linux
- Área
- compilers
Línea de trabajo
Start with the minimal definition in a.k and input in a.in, then run kompile followed by krun to reproduce the LLVM backend result. Compare the priority and requires cases described in the issue; done means both produce b rather than c and neither enters an infinite loop.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
What component is the issue in?
llvm-backend
Which command
- kompile
- kast
- krun
- kprove
- kprovex
- ksearch
What K Version?
v7.1.164-0-g459fdd7b84
Operating System
Linux
K Definitions (If Possible)
a.k:
module A
imports K-EQUAL-SYNTAX
syntax Stuff ::= "a" | "b" | "c"
rule A:Stuff => b requires A ==K a [priority(10)]
rule a => c
endmodule
Steps to Reproduce
use this a.in file:
a
Then, kompile a.k && krun a.in produces
<k>
c ~> .K
</k>
This is wrong, it should have produced b instead of c.
A few more notes:
Commenting out rule a => c produces b as a result. Removing the requires clause from rule A:Stuff => b requires A ==K a makes the backend enter an infinite loop. Replacing the same rule with rule a => b, while keeping the priority produces the expected result.
Expected Results
The command above should have produced this (both in the main case described above and in the infinite loop one):
<k>
b ~> .K
</k>
- Lenguaje dominante
- Python
- Estrellas
- 600
- Forks
- 164
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
- Sin Dockerfile ni archivo de Docker Compose
- Sin plantilla de pull request
- Leer la guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de runtimeverification/k
-
Dificultad 4/5 3-5 días Aptitud para principiantes 43/100
runtimeverification/k#4942 ·
-
bug
Dificultad 3/5 Medio día Aptitud para principiantes 75/100
runtimeverification/k#4941 ·
-
Introduce composable symbolic execution interface in pyxQuizá libre de nuevo @Stevengre la tomó hace 128 días y no hay ningún pull request abierto. Abierto
runtimeverification/k#4939 · 1 asignado ·
-
Concolic ExplorerAbierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 32/100
runtimeverification/k#4937 ·
-
Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100
runtimeverification/k#4936 ·
Todos los issues de runtimeverification/k
Issues similares
-
infrastructure
Dificultad 2/5 1-3 horas Aptitud para principiantes 76/100
NatLabRockies/H2Integrate#977 ·
Los mantenedores suelen responder en 1 día
-
bug
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
topoteretes/cognee#6470 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 62/100
-
area:docs priority:p2 type:docs wave:9
Dificultad 1/5 Menos de una hora Aptitud para principiantes 84/100
jejjohnson/radtrax#293 ·
Los mantenedores suelen responder en 1 día
-
bug core plugins
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
bunkerity/bunkerweb#4121 · 1 comentario ·
Los mantenedores suelen responder en 1 día