Skip to content

Commit

Permalink
Bug: Correctly typing and initialising prior_loops_cache (#4654)
Browse files Browse the repository at this point in the history
If an APR proof on disk contains a `loops_cache`, it cannot be executed
further because of a typing error in the style of:
```
...
File "/nix/store/6bi78qgqbnqryswaly3m4rggsqkrj72w-python3.10-kframework-7.1.145/lib/python3.10/site-packages/pyk/proof/reachability.py", line 793, in step_proof                                                                                    
    prior_loops = step.prior_loops_cache[node.id] + (node.id,)                                                                                                                                                                                        
TypeError: can only concatenate list (not "tuple") to list     
```
when initialising `prior_loops_cache` from disk. 

This PR corrects this bug by enforcing the correct types.
  • Loading branch information
PetarMax authored Oct 3, 2024
1 parent 990e82a commit 64b0260
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions pyk/src/pyk/proof/reachability.py
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,7 @@ def __init__(
admitted: bool = False,
_exec_time: float = 0,
error_info: Exception | None = None,
prior_loops_cache: dict[int, tuple[int, ...]] | None = None,
prior_loops_cache: dict[int, Iterable[int]] | None = None,
):
Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted)
KCFGExploration.__init__(self, kcfg, terminal)
Expand All @@ -148,7 +148,9 @@ def __init__(
self.logs = logs
self.circularity = circularity
self.node_refutations = {}
self.prior_loops_cache = prior_loops_cache if prior_loops_cache is not None else {}
self.prior_loops_cache = (
{int(k): tuple(v) for k, v in prior_loops_cache.items()} if prior_loops_cache is not None else {}
)
self.kcfg._kcfg_store = KCFGStore(self.proof_subdir / 'kcfg') if self.proof_subdir else None
self._exec_time = _exec_time
self.error_info = error_info
Expand Down

0 comments on commit 64b0260

Please sign in to comment.