Symbolic Execution Slowdown with Summary Rules
@Stevengre ci sta già lavorando.
Dal 8/8/2025.
Valutazione
Questa issue non è ancora stata valutata.
Descrizione
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.
- Lingua principale
- KCL
- Stelle
- 592
- Fork
- 156
- Merge medio
- 2h 19m
- PR unite (30g)
- 1
Preparare l'ambiente
Non abbiamo ancora controllato i file di configurazione di questo progetto. Parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/evm-semantics
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 78/100
runtimeverification/evm-semantics#1190 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100
runtimeverification/evm-semantics#2879 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2869 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2832 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 30/100
runtimeverification/evm-semantics#2824 ·