Skip to content
Draft
Changes from 2 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
20 changes: 14 additions & 6 deletions src/kontrol/foundry.py
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,7 @@
)

_LOGGER: Final = logging.getLogger(__name__)
_CONSOLE_LOG_DATETIME_FORMAT: Final = '%Y-%m-%d %H:%M:%S'

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Consider moving this to a utils.py file so we can reuse it if needed in the future.



class KontrolSemantics(KEVMSemantics):
Expand Down Expand Up @@ -158,7 +159,9 @@ def _console_log_pattern(self) -> KSequence:
def _ffi_pattern(self) -> KSequence:
return KSequence([KApply('ffi_shell', KVariable('###CMD')), KVariable('###CONTINUATION')])

def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
def _exec_rename_custom_step(
self, subst: Subst, cterm: CTerm, _c: CTermSymbolic, _node_id: int
) -> KCFGExtendResult | None:
# Extract the target var and new name from the substitution
target_var = subst['###RENAME_TARGET']
name_token = subst['###NEW_NAME']
Expand All @@ -182,7 +185,7 @@ def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic
return Step(CTerm(new_cterm.config, constraints), 1, (), ['foundry_rename'], cut=True)

def _exec_forget_custom_step(
self, subst: Subst, cterm: CTerm, cterm_symbolic: CTermSymbolic
self, subst: Subst, cterm: CTerm, cterm_symbolic: CTermSymbolic, _node_id: int
) -> KCFGExtendResult | None:
"""Remove the constraint at the top of K_CELL of a given CTerm from its path constraints,
as part of the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
Expand Down Expand Up @@ -293,28 +296,33 @@ def _filter_constraints_by_simplification(
new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True)

def _exec_console_log_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
def _exec_console_log_custom_step(
self, subst: Subst, cterm: CTerm, _c: CTermSymbolic, node_id: int
) -> KCFGExtendResult | None:
selector_token = subst['###SELECTOR']
data = subst['###DATA']
assert type(selector_token) is KToken

prefix = f' [{node_id}] [{datetime.datetime.now().strftime(_CONSOLE_LOG_DATETIME_FORMAT)}]'
try:
if type(data) is KToken:
selector = int(selector_token.token)
output = decode_log_message(data.token, selector)
if output is not None:
print(f' {output}')
print(f'{prefix} {output}')
else:
kevm = KEVM(kdist.get('kontrol.base'))
print(f' {kevm.pretty_print(data)}')
print(f'{prefix} {kevm.pretty_print(data)}')
except Exception as e:
_LOGGER.warning(f'Console log decode error: {e}')

# Update the K_CELL with the continuation
new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
return Step(CTerm(new_cterm.config, cterm.constraints), 1, (), ['console.log'], cut=True)

def _exec_ffi_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
def _exec_ffi_custom_step(
self, subst: Subst, cterm: CTerm, _c: CTermSymbolic, _node_id: int
) -> KCFGExtendResult | None:
"""Execute vm.ffi() cheatcode by running external commands and encoding their output as ABI bytes.

This function decodes the command from the ABI-encoded string array, executes it as a subprocess, and processes
Expand Down
Loading