Add --always-allocate
Flag to Reduce Branching
#58
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
During symbolic execution,
allocObject
introduces branching forScVal
s that have both small and host object representations (e.g., small/bigI64s
, symbols). The prover must explore both representations, leading to exponential branching (2^N branches for N arguments), which significantly impacts performance for tests with multiple such arguments.This PR adds the
--always-allocate
flag to thekomet prove
command. When enabled, the flag forces all eligibleScVal
s to be allocated as host objects, eliminating the branching caused by symbolic ambiguity.--always-allocate
flag sets a configuration cell (<alwaysAllocate>
) that modifies the behavior ofallocObject
.ScVal
types with both small and host object representations are affected (e.g., small/bigI64s
, symbols). Types likevoid
,error
, andbool
, which are always small, remain unaffected.This feature is optional, ensuring the default behavior remains unchanged unless explicitly enabled.