Symbolic Execution Slowdown with Summary Rules
@Stevengre がすでに取り組んでいます。
2025年8月8日 から。
評価
この issue はまだ評価されていません。
説明
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.
- 主要言語
- KCL
- スター
- 592
- フォーク
- 156
- 平均マージ
- 2時間 19分
- マージ済み PR（30日）
- 1
環境構築
このプロジェクトの環境構築ファイルはまだ確認していません。まず README を読み、一般的な手順ははじめてのコントリビューションガイドを参照してください。
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
runtimeverification/evm-semantics のほかの issue
-
難易度 1/5 1時間未満 初心者へのやさしさ 78/100
runtimeverification/evm-semantics#1190 ·
-
難易度 4/5 3〜5日 初心者へのやさしさ 45/100
runtimeverification/evm-semantics#2879 ·
-
難易度 4/5 3〜5日 初心者へのやさしさ 35/100
runtimeverification/evm-semantics#2869 ·
-
難易度 4/5 3〜5日 初心者へのやさしさ 35/100
runtimeverification/evm-semantics#2832 ·
-
難易度 4/5 3〜5日 初心者へのやさしさ 30/100
runtimeverification/evm-semantics#2824 ·