Symbolic Execution Slowdown with Summary Rules
@Stevengre ya está trabajando en esto.
Desde el 8/8/2025.
Evaluación
Este issue todavía no se ha evaluado.
Descripción
Issue:
The current implementation of summary rules does not consistently improve the performance of symbolic execution.
Description:
Based on the analysis in the evaluation report, it is evident that summary rules provide a definitive performance boost for concrete execution. However, their impact on symbolic execution is inconsistent and can sometimes lead to slower performance.
Potential Cause:
The root of the problem may lie in how the backend processes rules during symbolic execution. When the booster or the old backend encounters a high-priority rule (i.e., one with a lower priority number), it attempts to determine if this rule subsumes all possible cases of the current state. If it cannot definitively prove this, it is then forced to also evaluate all lower-priority rules. This process can introduce significant overhead and slow down execution.
It is possible that the existing summary rules are not general enough for the backend to easily recognize their broad applicability, thus triggering this time-consuming fallback mechanism.
Next Steps:
To address this issue, we need to:
- Investigate the specific cases where symbolic execution is slower.
- Identify which of these cases are triggering the old backend.
- Pinpoint the specific rule or component within the backend that is causing the slowdown.
This investigation will help us understand the precise conditions under which summary rules fail to improve performance and guide the development of a more effective solution.
- Lenguaje dominante
- KCL
- Estrellas
- 592
- Forks
- 156
- Merge medio
- 2 h 19 min
- PR fusionados (30 d)
- 1
Preparar el entorno
Aún no hemos revisado los archivos de configuración de este proyecto. Empieza por su README y consulta nuestra guía para la primera contribución para los pasos generales.
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/evm-semantics
-
Dificultad 1/5 Menos de una hora Aptitud para principiantes 78/100
runtimeverification/evm-semantics#1190 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 45/100
runtimeverification/evm-semantics#2879 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
runtimeverification/evm-semantics#2869 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
runtimeverification/evm-semantics#2832 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 30/100
runtimeverification/evm-semantics#2824 ·