|
3 | 3 | from typing import TYPE_CHECKING
|
4 | 4 |
|
5 | 5 | from pyk.kdist import kdist
|
6 |
| -from pyk.kore.parser import KoreParser |
7 |
| -from pyk.utils import run_process_2 |
| 6 | +from pyk.ktool.krun import llvm_interpret |
8 | 7 |
|
9 | 8 | from .gst_to_kore import filter_gst_keys, gst_to_kore
|
10 | 9 |
|
11 | 10 | if TYPE_CHECKING:
|
12 |
| - from subprocess import CompletedProcess |
13 | 11 | from typing import Any
|
14 | 12 |
|
15 | 13 | from pyk.kore.syntax import Pattern
|
16 | 14 |
|
17 | 15 |
|
18 | 16 | def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool, *, check: bool = True) -> Pattern:
|
19 |
| - proc_res = _interpret(gst_data, schedule, mode, chainid, usegas) |
20 |
| - |
21 |
| - if check: |
22 |
| - proc_res.check_returncode() |
23 |
| - |
24 |
| - kore = KoreParser(proc_res.stdout).pattern() |
25 |
| - return kore |
26 |
| - |
27 |
| - |
28 |
| -def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool) -> CompletedProcess: |
29 |
| - gst_data_filtered = filter_gst_keys(gst_data) |
30 |
| - interpreter = kdist.get('evm-semantics.llvm') / 'interpreter' |
31 |
| - init_kore = gst_to_kore(gst_data_filtered, schedule, mode, chainid, usegas) |
32 |
| - proc_res = run_process_2([str(interpreter), '/dev/stdin', '-1', '/dev/stdout'], input=init_kore.text, check=False) |
33 |
| - return proc_res |
| 17 | + """Interpret the given GST data using the LLVM backend.""" |
| 18 | + init_kore = gst_to_kore(filter_gst_keys(gst_data), schedule, mode, chainid, usegas) |
| 19 | + return llvm_interpret(kdist.get('evm-semantics.llvm'), init_kore, check=check) |
0 commit comments