Conversation
swissiety
enabled auto-merge
September 23, 2026 08:52
swissiety
merged commit Sep 23, 2026
268be53
into
secure-software-engineering:develop
9 checks passed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Summary
Four independent changes: one correctness fix, three memory reductions.
Forward the locality checks through
AllocValAllocValdecoratesValand forwards nearly every method to its delegate, but notisThisLocal,isReturnLocalandisParameterLocal. Those are implemented inValin terms of
this, andAllocVal.equalsrequires both sides to be anAllocValwhile a method's locals are always plain values — so all three answer
falsefor anywrapped local.
ForwardBoomerangSolver.applyCallSummarybranches on them to build its out-set, so areturned seed never produced the this/return/parameter entries and the call summary was
dropped silently. It surfaces as an assertion in
computeSuccessor, but only with-ea;without assertions it just loses flows.
Also unwraps the wrapper where a fact is lifted off a transition's start state before
being propagated on (
ForwardBoomerangSolver,IDEALSeedSolver).New tests in
SootAllocValTestfail on the unmodified code and pass with the fix.Drop the
transitionssetIt held exactly the same elements as
transitionToWeights.keySet()— every transitionadded to one was put in the other in the same call, and a fresh transition always has a
null old weight so the put always fires.
transitionToWeightsbecomes aLinkedHashMapto preserve the iteration order
getTransitions()callers relied on.~32 bytes per transition, ~1.3 GB on the workload below.
Small inline set for multimap values
SimpleSetMultimap's per-key sets are usually tiny; aLinkedHashSetcosts ~190 bytesfor a single element.
SmallOrderedSetholds 1 element in a field, 2–8 in an array, andpromotes to a
LinkedHashSetbeyond that. Representation is chosen bysizealone, neverinstanceof, and insertion order andadd()'s contract are preserved.The measured distribution behind this (88.5% singletons) came from a smaller workload and
did not hold on the large one, where most sets promote past the array limit. Benefit
there is correspondingly smaller.
Release a seed's phase-1 solver, and optionally its query solvers
IDEALSeedSolverconstructs both phase solvers up front, so phase 1's automata stayreachable for all of phase 2. Clearing them halves the in-flight live set.
clearListeners()is required, not tidying:runPhaseregisters a lambda on the sharedidealWeightFunctionsthat captures the phase's solver.Separately,
releaseSolversAfterQuery(default off) dropsqueryToSolversonce everyquery-scoped result has been materialized.
Measurements
APK tested with 166 seeds, 5 GB heap, 3 runs per config, means:
releaseSolvers()The phase-1 release accounts for all of the win.
releaseSolvers()nets out to nothingmeasurable here, and the reason is a trade rather than a no-op: it breaks a real retention
chain --
queryToSolversis an anonymous inner class capturing itsWeightedBoomerang, soa result held by
StoreIDEALResultHandlerotherwise pins that instance and all its solvers-- but to do so it must eagerly materialize the query-scoped views, which are then retained
for the life of the result. On this bounded workload the two roughly cancel. On a larger,
unbounded analysis, where solver graphs per seed are far bigger relative to those tables,
the balance should favour releasing. That is not measured here, which is why it is opt-in
and defaults to off.
Testing
Full suite green under
-DtestSetup=SootUp: boomerangPDS 352/0, idealPDS 113/0/5 skipped,matching baseline. Under
-DtestSetup=Soot,typestate.IteratorHasNextTesttest1/2/4 fail —these reproduce on unmodified
developand are unrelated to this PR.