diff --git a/main.py b/main.py index 18b6f44..d37e464 100755 --- a/main.py +++ b/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 diff --git a/util/__init__.py b/util/__init__.py index 6ad43d0..b93475e 100644 --- a/util/__init__.py +++ b/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", ] diff --git a/util/cache_util.py b/util/cache_util.py new file mode 100644 index 0000000..2e8e8e1 --- /dev/null +++ b/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