Refactoring: Move heap handling to separate HeapSupporter and merge lots of resource-type specific code into general code

[marcoeilers]

Refactoring with two major goals:

• In current Silicon, lots of code directly interacts with the heap. As a result, there are code pieces all over the place that case split, for example, on whether a resource is quantified or not, which clutters the code. This PR moves all direct interaction with heap chunks to a new HeapSupporter. The Producer, Evaluator, Consumer etc. perform all the work they currently do and then hand it off to the HeapSupporter the moment any interaction with heap chunks is needed. As a result, quantified resource case splits now happen only in said HeapSupporter. Therefore it will be much simpler to change the heap representation (e.g. to SE-TR/Silicarbon) in the future without having to add new cases all over the place.
• Silicon currently has lots of code duplication. For example, both Producer and Consumer have three separate cases for handling QPs for fields, predicates, and wands, even though the code in those cases is largely the same. Another example is the translation of resource triggers, for which there is currently a function for field triggers, one for predicate triggers, and one for wand triggers, which largely do the same thing. Additionally, there is lots of code all over the place that, for example, checks whether a resource is quantified, or extracts arguments from a resource access, or computes the parameters of a resource. This PR creates utility methods for such common functionality, and merges a lot of code that is currently specific to a resource type into more general code that works with any resource type.

In the process, this PR also fixes a small issue with trigger translation where predicate and field triggers were treated differently for no good reason.

[Copilot]

Pull Request Overview

Refactors all direct heap interactions into a new HeapSupporter, centralizing heap initialization and chunk operations, and generalizes resource-specific handling into unified helper calls.

• Adds a heapSupporter instance to the Verifier trait and replaces Heap() with heapSupporter.getEmptyHeap(...)
• Introduces state utility methods (isUsedAsTrigger, isQuantifiedResource, getFormalArgVars, getFormalArgDecls) in State.scala
• Replaces resource-specific code in Producer, Consumer, PredicateSupporter, MagicWandSupporter, HavocSupporter, and Executor with generic heapSupporter calls

Reviewed Changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/main/scala/verifier/Verifier.scala	Added heapSupporter field and defaultHeapSupporter import
src/main/scala/supporters/functions/FunctionVerificationUnit.scala	Replaced Heap() with heapSupporter.getEmptyHeap
src/main/scala/supporters/PredicateVerificationUnit.scala	Ditto for predicate setup
src/main/scala/supporters/MethodSupporter.scala	Ditto for method verification unit
src/main/scala/supporters/CfgSupporter.scala	Ditto for CFG unit
src/main/scala/state/State.scala	Added trigger and quantified-resource utilities
src/main/scala/rules/QuantifiedChunkSupport.scala	Switched trigger checks to new isUsedAsTrigger
src/main/scala/rules/Producer.scala	Unified access predicate handling via heapSupporter
src/main/scala/rules/PredicateSupporter.scala	Delegated single/quantified produce to heapSupporter
src/main/scala/rules/MagicWandSupporter.scala	Updated heap initializations and chunk logic use heapSupporter
src/main/scala/rules/HavocSupporter.scala	Replaced raw heap updates with havocResource
src/main/scala/rules/Executor.scala	Replaced direct Heap() and chunk code with heapSupporter
src/main/scala/rules/Consumer.scala	Unified consume logic via heapSupporter
silver	Updated submodule commit

Comments suppressed due to low confidence (4)

src/main/scala/state/State.scala:121

• Hardcoding "r" in getFormalArgDecls may drift out of sync with the ?r term identifier. Consider using ?r.id.name for the LocalVarDecl name to ensure consistency between the AST variable and the internal term.

case _: ast.Field => Seq(ast.LocalVarDecl("r", ast.Ref)())

src/main/scala/rules/MagicWandSupporter.scala:368

• [nitpick] Calls to getEmptyHeap are scattered (e.g. lines 242, 368, and 412). Consider computing it once and reusing the emptyHeap variable in each block to avoid repeated invocations.

val emptyHeap = v.heapSupporter.getEmptyHeap(sLhs.program)

src/main/scala/rules/HavocSupporter.scala:46

• With the new havocResource path, add unit tests covering both quantified and non-quantified resource havoc scenarios to ensure the refactored behavior matches the previous implementation.

evals(s0, havoc.exp.args(s0.program), _ => pve, v0)((s1, tRcvrs, _, v1) => {

src/main/scala/rules/MagicWandSupporter.scala:304

• [nitpick] The parameter name s shadows the state variables used throughout this method, which can be confusing. Rename it (e.g. initialState) to avoid shadowing and improve readability.

def createWandChunkAndRecordResults(s: State,