A difficult-to-reproduce segmentation fault.
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 5/5
- Tiempo estimado
- Más de una semana
- Aptitud para principiantes
- 15/100
- Tipo de issue
- Error
- Claridad
- Necesita aclaración
- Estado de actividad
- Estancado
- Área
- compilers
Línea de trabajo
Start by reducing the reported configuration to a minimal reproducible example, using the shown program and comparing kompile with krun --depth 0. Investigate the suspected automatic cell-filling path; done means reproducing the segmentation fault reliably and confirming that the reduced case no longer crashes after the fix.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
The image shows an error we encountered during the development of our project. This error may also occur when running krun --depth 0. We suspect it is caused by an anomaly in the automatic filling of cells.
Initially, we provided a program similar to the one below:
module TEST-SYNTAX
imports INT-SYNTAX
syntax Top ::= List{Inst, ";"}
syntax Inst ::= "spawn" Int
endmodule
module TEST
imports TEST-SYNTAX
imports INT
configuration
<pgm> $PGM:Top </pgm>
<ks>
<k-thread multiplicity="*" type="Map">
<kid> 0 </kid>
<k> 0 </k>
</k-thread>
</ks>
rule
<pgm> spawn X ; T:Top => T </pgm>
(.Bag =>
<k-thread>
<kid> !_:Int </kid>
<k> X </k>
</k-thread>
)
rule
<k> X => X +Int Y </k>
<k-thread>
<k> Y => Y -Int Y </k>
...
</k-thread>
requires Y >Int 0
endmodule
After placing <k> into the </k-thread>, the bug disappears. However, this program itself can be correctly compiled using kompile and executed with krun. Therefore, we have not yet identified the minimal reproducible example. Additionally, due to the complexity of our project and the lack of backups for the error, we are currently unsure how to reproduce the issue.
- Lenguaje dominante
- Python
- Estrellas
- 591
- Forks
- 163
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
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
-
Introduce composable symbolic execution interface in pyxQuizá libre de nuevo @Stevengre la tomó hace 99 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 ·
-
Accelerating all-path reachability proofs with one-path reachability proofsQuizá libre de nuevo @Stevengre la tomó hace 104 días y no hay ningún pull request abierto. Abiertotype:epic
runtimeverification/k#4934 · 4 comentarios · 1 asignado ·
-
Support progressive depth halving as a generic policy in `Prover.advance_proof`Quizá libre de nuevo @Stevengre la tomó hace 124 días y no hay ningún pull request abierto. Abierto
runtimeverification/k#4924 · 1 asignado ·
Todos los issues de runtimeverification/k
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 85/100
kornia/kornia#5263 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
Metadata correction for W16-5400Abiertoapproved correction metadata
Dificultad 1/5 Menos de una hora Aptitud para principiantes 88/100
acl-org/acl-anthology#10133 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
BasedHardware/omi#20084 ·
Los mantenedores suelen responder en 1 día
-
bug needs-acceptance wg/evaluation-quality
Dificultad 2/5 1-3 horas Aptitud para principiantes 76/100
vllm-project/semantic-router#4424 ·
Los mantenedores suelen responder en 1 día