Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 0 additions & 29 deletions pyk/src/pyk/kore/rpc.py
Original file line number Diff line number Diff line change
Expand Up @@ -570,8 +570,6 @@ class LogEntry(ABC):
@classmethod
def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE:
match dct['tag']:
case 'processing-time':
return LogTiming.from_dict(dct) # type: ignore
case 'rewrite':
return LogRewrite.from_dict(dct) # type: ignore
case _:
Expand All @@ -581,27 +579,6 @@ def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE:
def to_dict(self) -> dict[str, Any]: ...


@final
@dataclass(frozen=True)
class LogTiming(LogEntry):
class Component(Enum):
KORE_RPC = 'kore-rpc'
BOOSTER = 'booster'
PROXY = 'proxy'

time: float
component: Component | None

@classmethod
def from_dict(cls, dct: Mapping[str, Any]) -> LogTiming:
return LogTiming(
time=dct['time'], component=LogTiming.Component(dct['component']) if 'component' in dct else None
)

def to_dict(self) -> dict[str, Any]:
return {'tag': 'processing-time', 'time': self.time, 'component': self.component}


@final
@dataclass(frozen=True)
class LogRewrite(LogEntry):
Expand Down Expand Up @@ -1025,7 +1002,6 @@ def execute(
module_name: str | None = None,
log_successful_rewrites: bool | None = None,
log_failed_rewrites: bool | None = None,
log_timing: bool | None = None,
) -> ExecuteResult:
params = filter_none(
{
Expand All @@ -1039,7 +1015,6 @@ def execute(
'state': self._state(pattern),
'log-successful-rewrites': log_successful_rewrites,
'log-failed-rewrites': log_failed_rewrites,
'log-timing': log_timing,
}
)

Expand All @@ -1052,14 +1027,12 @@ def implies(
consequent: Pattern,
*,
module_name: str | None = None,
log_timing: bool | None = None,
) -> ImpliesResult:
params = filter_none(
{
'antecedent': self._state(antecedent),
'consequent': self._state(consequent),
'module': module_name,
'log-timing': log_timing,
}
)

Expand All @@ -1071,13 +1044,11 @@ def simplify(
pattern: Pattern,
*,
module_name: str | None = None,
log_timing: bool | None = None,
) -> tuple[Pattern, tuple[LogEntry, ...]]:
params = filter_none(
{
'state': self._state(pattern),
'module': module_name,
'log-timing': log_timing,
}
)

Expand Down
43 changes: 0 additions & 43 deletions pyk/src/tests/integration/kore/test_kore_client.py
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,6 @@
InvalidModuleError,
LogOrigin,
LogRewrite,
LogTiming,
RewriteFailure,
RewriteSuccess,
SatResult,
Expand Down Expand Up @@ -625,48 +624,6 @@ def test(
assert actual == expected[server_type]


class TestTimeLogging(KoreClientTest):
KOMPILE_DEFINITION = """
module TIMING-TEST
imports INT
configuration <k> $PGM:Int </k>
endmodule
"""
KOMPILE_MAIN_MODULE = 'TIMING-TEST'
KOMPILE_ARGS = {'syntax_module': 'TIMING-TEST'}
LLVM_ARGS = KOMPILE_ARGS

@staticmethod
def config(i: int) -> Pattern:
return generated_top((k(kseq((inj(INT, SORT_K_ITEM, int_dv(i)),))), generated_counter(int_dv(0))))

def test_execute(self, kore_client: KoreClient) -> None:
# When
response = kore_client.execute(self.config(0), log_timing=True)
logs = response.logs

# Then
assert logs
assert all(isinstance(log, LogTiming) for log in logs)

def test_implies(self, kore_client: KoreClient) -> None:
# When
response = kore_client.implies(EVar('X', INT), int_top, log_timing=True)
logs = response.logs

# Then
assert logs
assert all(isinstance(log, LogTiming) for log in logs)

def test_simplify(self, kore_client: KoreClient) -> None:
# When
_, logs = kore_client.simplify(int_top, log_timing=True)

# Then
assert logs
assert all(isinstance(log, LogTiming) for log in logs)


class TestAddModule(KoreClientTest):
KOMPILE_DEFINITION = """
module INT-CONFIG
Expand Down