Symbolic Execution Slowdown with Summary Rules

[Stevengre]

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.