From afcc98e7463d35e251e1bd0cfa72c2edf65081cc Mon Sep 17 00:00:00 2001 From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com> Date: Wed, 8 Nov 2023 14:56:36 +0200 Subject: [PATCH] Profile specific instructions (#30) * Profile specific instructions * More profiling instructions --- README.md | 52 +++++ kmxwasm/src/kmxwasm/property.py | 179 +++++++++++++++++- .../src/kmxwasm/property_testing/running.py | 9 +- kmxwasm/src/kmxwasm/timing.py | 6 +- 4 files changed, 232 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index dfd8188b..9da50889 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,54 @@ # mx-wasm Symbolic execution backend for the MultiversX blockchain network + +# Running + +Example: + +``` +cd kmxwasm +time poetry run python3 -m src.kmxwasm.property \ + --claim tmp2/test_change_quorum-spec-1k.json \ + --kcfg=../.property/kcfg.json +``` + +# Profiling + +Example: + +* Run a contract normally: +``` +cd kmxwasm +time poetry run python3 -m src.kmxwasm.property \ + --claim tmp2/test_change_quorum-spec-1k.json \ + --kcfg=../.property/kcfg.json +``` + +* List all configurations: +``` +cd kmxwasm +time poetry run python3 -m src.kmxwasm.property \ + --claim tmp2/test_change_quorum-spec-1k.json \ + --kcfg=../.property/kcfg.json \ + --tree +``` + +* Look at configurations and pick one (example for configuration 48): +``` +cd kmxwasm +time poetry run python3 -m src.kmxwasm.property \ + --claim tmp2/test_change_quorum-spec-1k.json \ + --kcfg=../.property/kcfg.json \ + --show-node 48 +``` + + +* Run profiling using that configuration as a base; also, pick an instruction from PROFILE_INSTRUCTIONS: +``` +cd kmxwasm +time poetry run python3 -m src.kmxwasm.property \ + --claim tmp2/test_change_quorum-spec-1k.json \ + --kcfg=../.property/kcfg.json \ + --profile 48 + --profile-instruction aIConst +``` diff --git a/kmxwasm/src/kmxwasm/property.py b/kmxwasm/src/kmxwasm/property.py index dc0fa392..fc33a42b 100644 --- a/kmxwasm/src/kmxwasm/property.py +++ b/kmxwasm/src/kmxwasm/property.py @@ -6,14 +6,14 @@ from pathlib import Path from pyk.cterm import CTerm -from pyk.kast.inner import KApply, KSequence, KVariable +from pyk.kast.inner import KApply, KInner, KSequence, KVariable from pyk.kcfg import KCFG from pyk.kcfg.show import KCFGShow from pyk.kore.rpc import KoreClientError from pyk.prelude.utils import token from .ast.mx import ( - get_first_instr, + instrs_cell_contents, replace_instrs_cell, set_all_code_cell_content, set_call_stack_cell_content, @@ -27,7 +27,7 @@ from .property_testing.wasm_krun_initializer import WasmKrunInitializer from .timing import Timer -sys.setrecursionlimit(8000) +sys.setrecursionlimit(16000) def usage_error() -> None: @@ -186,6 +186,106 @@ def run(self) -> None: raise NotImplementedError(f'Unknown run_claim result: {type(result)}') +@dataclass(frozen=True) +class InstructionProfile: + name: str + steps: int + to_run: KInner + setup_steps: int = 0 + setup: KInner = KSequence([]) + + +PROFILE_INSTRUCTIONS = [ + InstructionProfile( + name='aLocal.tee', + steps=1, + to_run=KApply('aLocal.tee', token(0)), + setup_steps=3, + setup=KSequence( + [ + KApply('aIConst', [KApply('i32'), token(1)]), + KApply( + 'init_local___WASM_Instr_Int_Val', + [token(0), KApply('<_>__WASM-DATA-COMMON_IVal_IValType_Int', [KApply('i32'), token(1)])], + ), + ] + ), + ), + InstructionProfile( + name='aIConst', + steps=2, + to_run=KApply('aIConst', [KApply('i32'), token(1)]), + ), # ITYPE:IValType . const VAL => #chop (< ITYPE > VAL) => valstack + InstructionProfile( + name='push.i32', + steps=1, + to_run=KApply('<_>__WASM-DATA-COMMON_IVal_IValType_Int', [KApply('i32'), token(2)]), + ), + InstructionProfile( + name='store', + steps=2 + 2 + 4, # TODO: Test only the "store" "{" Int Int Number Int "}" form. + to_run=KSequence( + KApply('aIConst', [KApply('i32'), token(1)]), # Index for storing + KApply('aIConst', [KApply('i32'), token(1)]), # Value to store + KApply('aStore', [KApply('i32'), KApply('storeOpStore8'), token(10)]), # Offset + ), + ), # uses two stack entries + InstructionProfile( + name='aLocal.get', + steps=1, + to_run=KApply('aLocal.get', token(0)), + setup_steps=3, + setup=KSequence( + [ + KApply('aIConst', [KApply('i32'), token(1)]), + KApply( + 'init_local___WASM_Instr_Int_Val', + [token(0), KApply('<_>__WASM-DATA-COMMON_IVal_IValType_Int', [KApply('i32'), token(1)])], + ), + ] + ), + ), + InstructionProfile( + name='aLocal.set', + steps=2 + 1, + to_run=KSequence([KApply('aIConst', [KApply('i32'), token(1)]), KApply('aLocal.set', token(0))]), + setup_steps=3, + setup=KSequence( + [ + KApply('aIConst', [KApply('i32'), token(1)]), + KApply( + 'init_local___WASM_Instr_Int_Val', + [token(0), KApply('<_>__WASM-DATA-COMMON_IVal_IValType_Int', [KApply('i32'), token(1)])], + ), + ] + ), + ), + InstructionProfile( + name='aLoad', + steps=2 + 6, + to_run=KSequence( + KApply('aIConst', [KApply('i32'), token(1)]), # Index for storing + KApply('aLoad', [KApply('i32'), KApply('loadOpLoad8_u'), token(10)]), # Offset + ), + ), # uses two stack entries + InstructionProfile( + name='aGlobal.set', + steps=2 + 1, + to_run=KSequence( + KApply('aIConst', [KApply('i32'), token(1)]), # Index for storing + KApply('aGlobal.set', [token(0)]), + ), + ), # uses two stack entries +] +# TODO: Also profile the instructions below. +# ~> i32 . add +# ~> #br ( 1 ) +# ~> label [ .ValTypes ] { .EmptyStmts } .ValStack +# ~> i32 . xor +# ~> #call ( 168 ) +# ~> return + + @dataclass(frozen=True) class Profile(Action): node_id: int @@ -193,8 +293,22 @@ class Profile(Action): depth: int kcfg_path: Path booster: bool + instruction_name: str def run(self) -> None: + steps = 1 + instruction_kitem: KInner = KApply('aNop') + setup: KInner = KSequence([]) + setup_steps = 0 + for profile in PROFILE_INSTRUCTIONS: + if profile.name == self.instruction_name: + (steps, instruction_kitem, setup_steps, setup) = ( + profile.steps, + profile.to_run, + profile.setup_steps, + profile.setup, + ) + break with kbuild_semantics( output_dir=KBUILD_DIR, config_file=KBUILD_ML_PATH, target=HASKELL, booster=self.booster ) as tools: @@ -210,11 +324,7 @@ def run(self) -> None: t = Timer('Prepare profile node') node = kcfg.get_node(self.node_id) assert node - instr = get_first_instr(node.cterm.config) - assert instr - # instr = KApply('aNop') - print(f'Instr: {instr.label.name}') - instrs = KSequence([instr] * self.depth) + instrs = KSequence([setup, KSequence([instruction_kitem] * self.depth)]) new_config = replace_instrs_cell(node.cterm.config, instrs) new_config = set_call_stack_cell_content(new_config, KVariable('CallStackVar')) new_config = set_interim_states_cell_content(new_config, KVariable('InterimStatesVar')) @@ -223,13 +333,48 @@ def run(self) -> None: kcfg.replace_node(node.id, cterm=CTerm(new_config, node.cterm.constraints)) t.measure() + existing = {node.id for node in kcfg.nodes} + + steps_needed = self.depth * steps + setup_steps result = profile_step( tools, restart_kcfg=kcfg, node_id=self.node_id, - depth=self.depth, + depth=steps_needed, + groups=self.depth, ) + if isinstance(result, Success): + new = {node.id for node in kcfg.nodes if not node.id in existing} + if len(new) != 1: + result = RunException( + kcfg=kcfg, + exception=Exception(f'Invalid number of new nodes: {len(new)}'), + last_processed_node=self.node_id, + ) + else: + new_id = list(new)[0] + new_node = kcfg.node(new_id) + maybe_instrs = instrs_cell_contents(new_node.cterm.config) + if maybe_instrs is None: + result = RunException( + kcfg=kcfg, exception=Exception('Instrs not found.'), last_processed_node=new_id + ) + elif 0 != len(maybe_instrs): + result = RunException( + kcfg=kcfg, exception=Exception('Unprocessed instrs.'), last_processed_node=new_id + ) + else: + edge = kcfg.edges(target_id=new_id)[0] + if steps_needed != edge.depth: + result = RunException( + kcfg=kcfg, + exception=Exception( + f'Did not execute the expected number of steps: {[steps_needed , edge.depth]}.' + ), + last_processed_node=new_id, + ) + if isinstance(result, Success): print('Success') return @@ -379,6 +524,13 @@ def read_flags() -> Action: required=False, help='Use the booster backend', ) + parser.add_argument( + '--profile-instruction', + dest='profile_instruction', + required=False, + default='nop', + help='Which instruction to profile.', + ) args = parser.parse_args() if args.show_node is not None: return ShowNode(args.show_node, Path(args.kcfg), booster=args.booster) @@ -392,7 +544,14 @@ def read_flags() -> Action: to_remove = [int(n_id) for n_id in args.remove_nodes.split(',')] if args.profile: - return Profile(args.profile, remove=to_remove, depth=args.step, kcfg_path=Path(args.kcfg), booster=args.booster) + return Profile( + args.profile, + remove=to_remove, + depth=args.step, + kcfg_path=Path(args.kcfg), + booster=args.booster, + instruction_name=args.profile_instruction, + ) if args.claimfile is None: usage_error() diff --git a/kmxwasm/src/kmxwasm/property_testing/running.py b/kmxwasm/src/kmxwasm/property_testing/running.py index 2a70f4d2..e1ddea26 100644 --- a/kmxwasm/src/kmxwasm/property_testing/running.py +++ b/kmxwasm/src/kmxwasm/property_testing/running.py @@ -370,7 +370,7 @@ def split_edge(tools: Tools, restart_kcfg: KCFG, start_node_id: int) -> RunClaim return RunException(kcfg, e, start_node_id) -def profile_step(tools: Tools, restart_kcfg: KCFG, node_id: int, depth: int) -> RunClaimResult: +def profile_step(tools: Tools, restart_kcfg: KCFG, node_id: int, depth: int, groups: int) -> RunClaimResult: kcfg = restart_kcfg kcfg_exploration = KCFGExploration(kcfg) @@ -397,7 +397,12 @@ def profile_step(tools: Tools, restart_kcfg: KCFG, node_id: int, depth: int) -> logs = {} timer = Timer(f'Running {depth} steps.') tools.explorer.extend(kcfg_exploration=kcfg_exploration, node=start, logs=logs, execute_depth=depth) - timer.measure() + time = timer.measure() + + print(f'Average time per group: {time / groups}') + print(f'Average time per step: {time / depth}') + + # TODO: Check that the explorer consumed all instructions and finished successfully. return Success(kcfg) except BaseException as e: diff --git a/kmxwasm/src/kmxwasm/timing.py b/kmxwasm/src/kmxwasm/timing.py index 26e45aef..0200668d 100644 --- a/kmxwasm/src/kmxwasm/timing.py +++ b/kmxwasm/src/kmxwasm/timing.py @@ -6,5 +6,7 @@ def __init__(self, message: str) -> None: self.__message = message self.__start = time.time() - def measure(self) -> None: - print(self.__message, time.time() - self.__start, 'sec.', flush=True) + def measure(self) -> float: + duration = time.time() - self.__start + print(self.__message, duration, 'sec.', flush=True) + return duration