Skip to content

Commit 0915734

Browse files
committed
kevm-pyk/{kevm,__main__}: include srcmap information in short node output
1 parent ca235f4 commit 0915734

File tree

2 files changed

+59
-20
lines changed

2 files changed

+59
-20
lines changed

kevm-pyk/src/kevm_pyk/__main__.py

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -428,9 +428,10 @@ def exec_foundry_show(
428428
kcfgs_dir = foundry_out / 'kcfgs'
429429
srcmap_dir = foundry_out / 'srcmaps'
430430
kcfg_file = kcfgs_dir / f'{test}.json'
431-
contract = test.split('.')[0]
432-
srcmap_file = srcmap_dir / f'{contract}.json'
433-
foundry = Foundry(definition_dir, profile=profile, use_directory=use_directory, srcmap_file=srcmap_file)
431+
contract_name = test.split('.')[0]
432+
foundry = Foundry(
433+
definition_dir, profile=profile, use_directory=use_directory, srcmap_dir=srcmap_dir, contract_name=contract_name
434+
)
434435

435436
with open(kcfg_file, 'r') as kf:
436437
kcfg = KCFG.from_dict(json.loads(kf.read()))
@@ -533,8 +534,12 @@ def exec_foundry_view_kcfg(foundry_out: Path, test: str, profile: bool, **kwargs
533534
use_directory = foundry_out / 'specs'
534535
kcfgs_dir = foundry_out / 'kcfgs'
535536
kcfg_file = kcfgs_dir / f'{test}.json'
537+
srcmap_dir = foundry_out / 'srcmaps'
536538
use_directory.mkdir(parents=True, exist_ok=True)
537-
foundry = Foundry(definition_dir, profile=profile, use_directory=use_directory)
539+
contract_name = test.split('.')[0]
540+
foundry = Foundry(
541+
definition_dir, profile=profile, use_directory=use_directory, srcmap_dir=srcmap_dir, contract_name=contract_name
542+
)
538543
viewer = KCFGViewer(kcfg_file, foundry, node_printer=foundry.short_info)
539544
viewer.run()
540545

kevm-pyk/src/kevm_pyk/kevm.py

Lines changed: 50 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import sys
44
from pathlib import Path
55
from subprocess import CalledProcessError
6-
from typing import Any, Dict, Final, Iterable, List, Optional
6+
from typing import Any, Dict, Final, Iterable, List, Optional, Tuple
77

88
from pyk.cli_utils import run_process
99
from pyk.cterm import CTerm, remove_useless_constraints
@@ -17,7 +17,7 @@
1717
from pyk.prelude.ml import mlAnd, mlEqualsTrue
1818
from pyk.prelude.string import stringToken
1919

20-
from .utils import add_include_arg
20+
from .utils import add_include_arg, byte_offset_to_lines
2121

2222
_LOGGER: Final = logging.getLogger(__name__)
2323

@@ -27,7 +27,11 @@
2727

2828
class KEVM(KProve, KRun):
2929

30-
srcmap: Optional[Dict[int, str]]
30+
_srcmap_dir: Optional[Path]
31+
_contract_name: Optional[str]
32+
_contract_ids: Dict[int, str]
33+
_srcmaps: Dict[str, Dict[int, Tuple[int, int, int, str, int]]]
34+
_contract_srcs: Dict[str, List[str]]
3135

3236
def __init__(
3337
self,
@@ -37,7 +41,8 @@ def __init__(
3741
profile: bool = False,
3842
kprove_command: str = 'kprove',
3943
krun_command: str = 'krun',
40-
srcmap_file: Optional[Path] = None,
44+
srcmap_dir: Optional[Path] = None,
45+
contract_name: Optional[str] = None,
4146
) -> None:
4247
# I'm going for the simplest version here, we can change later if there is an advantage.
4348
# https://stackoverflow.com/questions/9575409/calling-parent-class-init-with-multiple-inheritance-whats-the-right-way
@@ -52,10 +57,15 @@ def __init__(
5257
)
5358
KRun.__init__(self, definition_dir, use_directory=use_directory, profile=profile, command=krun_command)
5459
KEVM._patch_symbol_table(self.symbol_table)
55-
self.srcmap = None
56-
if srcmap_file is not None and srcmap_file.exists():
57-
with open(srcmap_file, 'r') as sm:
58-
self.srcmap = {int(k): v for k, v in json.loads(sm.read()).items()}
60+
self._srcmap_dir = srcmap_dir
61+
self._contract_name = contract_name
62+
self._contract_ids = {}
63+
self._srcmaps = {}
64+
self._contract_srcs = {}
65+
if self._srcmap_dir is not None:
66+
self._contract_ids = {
67+
int(k): v for k, v in json.loads((self._srcmap_dir / 'contract_id_map.json').read_text()).items()
68+
}
5969

6070
@staticmethod
6171
def kompile(
@@ -196,12 +206,34 @@ def short_info(self, cterm: CTerm) -> List[str]:
196206
_pc = get_cell(cterm.config, 'PC_CELL')
197207
pc_str = f'pc: {self.pretty_print(_pc)}'
198208
ret_strs = [k_str, calldepth_str, statuscode_str, pc_str]
199-
if type(_pc) is KToken and self.srcmap is not None:
200-
pc = int(_pc.token)
201-
if pc in self.srcmap:
202-
ret_strs.append(f'srcmap: {self.srcmap[pc]}')
203-
else:
204-
_LOGGER.warning(f'pc not found in srcmap: {pc}')
209+
if self._srcmap_dir is not None and self._contract_name is not None and self._contract_ids is not None:
210+
if self._contract_name not in self._srcmaps:
211+
_srcmap_pre = json.loads((self._srcmap_dir / f'{self._contract_name}.json').read_text())
212+
_srcmap: Dict[int, Tuple[int, int, int, str, int]] = {}
213+
for k, v in _srcmap_pre.items():
214+
s, l, f, j, m = v
215+
assert type(s) is int
216+
assert type(l) is int
217+
assert type(f) is int
218+
assert type(j) is str
219+
assert type(m) is int
220+
_srcmap[int(k)] = (s, l, f, j, m)
221+
self._srcmaps[self._contract_name] = _srcmap
222+
_srcmap = self._srcmaps[self._contract_name]
223+
if type(_pc) is KToken:
224+
pc = int(_pc.token)
225+
if pc in _srcmap:
226+
s, l, f, j, m = _srcmap[pc]
227+
if f in self._contract_ids:
228+
contract_file = self._contract_ids[f]
229+
if contract_file not in self._contract_srcs:
230+
self._contract_srcs[contract_file] = (
231+
(self._srcmap_dir.parent.parent / contract_file).read_text().split('\n')
232+
)
233+
_, start, end = byte_offset_to_lines(self._contract_srcs[contract_file], s, l)
234+
ret_strs.append(f'src: {self._contract_ids[f]}:{start}:{end}')
235+
else:
236+
_LOGGER.warning(f'pc not found in srcmap: {pc}')
205237
return ret_strs
206238

207239
@staticmethod
@@ -467,7 +499,8 @@ def __init__(
467499
main_file: Optional[Path] = None,
468500
use_directory: Optional[Path] = None,
469501
profile: bool = False,
470-
srcmap_file: Optional[Path] = None,
502+
srcmap_dir: Optional[Path] = None,
503+
contract_name: Optional[str] = None,
471504
) -> None:
472505
# copied from KEVM class and adapted to inherit KPrint instead
473506
KEVM.__init__(
@@ -476,7 +509,8 @@ def __init__(
476509
main_file=main_file,
477510
use_directory=use_directory,
478511
profile=profile,
479-
srcmap_file=srcmap_file,
512+
srcmap_dir=srcmap_dir,
513+
contract_name=contract_name,
480514
)
481515
Foundry._patch_symbol_table(self.symbol_table)
482516

0 commit comments

Comments
 (0)