Improving lookup for specification pre-loading at startup

main.py

@@ -26,6 +26,7 @@
     copy_file_to_folder,
     copy_folder_to_folder,
     ensure_lines_at_beginning,
+    get_vresult_index,
     run_with_timeout,
 )
 from verification import (
@@ -314,9 +315,13 @@ def _verify_program(
 
     if skip_statuses:
         functions_for_workstack: list[CFunction] = []
+        cached_vresults = get_vresult_index(VERIFIER_CACHE)
         existing_specs: dict[CFunction, FunctionSpecification] = {}
+
         for function in functions:
-            if cached_vresult := _get_cached_vresult_with_status(function, skip_statuses):
+            if cached_vresult := _get_cached_vresult_with_status(
+                function, skip_statuses, cached_vresults
+            ):
                 spec = cached_vresult.get_spec()
                 function.set_specifications(spec)
                 existing_specs[function] = spec
@@ -503,7 +508,9 @@ def _set_next_step(
 
 
 def _get_cached_vresult_with_status(
-    function: CFunction, statuses: set[VerificationStatus]
+    function: CFunction,
+    statuses: set[VerificationStatus],
+    cached_vresults: dict[CFunction, list[VerificationResult]],
 ) -> VerificationResult | None:
     """Return a cached VerificationResult for a function whose status is in `statuses`.
 
@@ -517,6 +524,8 @@ def _get_cached_vresult_with_status(
     Args:
         function (CFunction): The function whose cached specification is requested.
         statuses (set[VerificationStatus]): The set of statuses to match against.
+        cached_vresults (dict[CFunction, list[VerificationResult]]): The dictionary of cached
+            VerificationResults per function.
 
     Returns:
         VerificationResult | None: The cached verification result for function if one with a
@@ -528,18 +537,14 @@ def _get_cached_vresult_with_status(
         VerificationStatus.ASSUMED,
     ]
     highest_priority_vresult: VerificationResult | None = None
-    if VERIFIER_CACHE is not None:
-        for vinput in VERIFIER_CACHE.iterkeys():
-            # This is very inefficient, but still faster than adding all the functions to workstacks
-            # and reading from the cache repeatedly.
-            vresult = VERIFIER_CACHE[vinput]
-            if vresult.status not in statuses or function != vresult.get_function():
-                continue
-            if highest_priority_vresult is None or (
-                vresult_priority.index(vresult.status)
-                < vresult_priority.index(highest_priority_vresult.status)
-            ):
-                highest_priority_vresult = vresult
+    for vresult in cached_vresults.get(function, []):
+        if vresult.status not in statuses:
+            continue
+        if highest_priority_vresult is None or (
+            vresult_priority.index(vresult.status)
+            < vresult_priority.index(highest_priority_vresult.status)
+        ):
+            highest_priority_vresult = vresult
     return highest_priority_vresult
 
 

util/__init__.py

@@ -12,6 +12,7 @@
 from .backtracking_util import parse_backtracking_info
 from .execution.execution_util import run_with_timeout
 from .tree_sitter_util import get_identifier_nodes_from_call_expressions, get_function_identifiers
+from .cache_util import get_vresult_index
 
 __all__ = [
     "SpecificationGenerationNextStep",
@@ -37,4 +38,5 @@
     "run_with_timeout",
     "get_identifier_nodes_from_call_expressions",
     "get_function_identifiers",
+    "get_vresult_index",
 ]

util/cache_util.py

@@ -0,0 +1,35 @@
+"""Utility functions for working with the verification result cache."""
+
+from __future__ import annotations
+
+from collections import defaultdict
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from diskcache import Cache
+
+    from verification import VerificationResult
+
+    from .c_function import CFunction
+
+
+def get_vresult_index(
+    vresult_cache: Cache | None,
+) -> dict[CFunction, list[VerificationResult]]:
+    """Return a dictionary of CFunction to VerificationResult(s) constructed from the given cache.
+
+    Args:
+        vresult_cache (Cache | None): The cache from which to construct the dictionary of CFunction
+            to VerificationResult(s).
+
+    Returns:
+        dict[CFunction, list[VerificationResult]]: The dictionary of CFunction to
+            VerificationResult(s). Default value for keys is an empty list.
+    """
+    function_to_vresults: dict[CFunction, list[VerificationResult]] = defaultdict(list)
+    if vresult_cache is None:
+        return function_to_vresults
+    for vinput in vresult_cache.iterkeys():
+        if vresult := vresult_cache.get(vinput):
+            function_to_vresults[vresult.get_function()].append(vresult)
+    return function_to_vresults