diff --git a/poetry.lock b/poetry.lock index 143f0f9f4..be240c201 100644 --- a/poetry.lock +++ b/poetry.lock @@ -556,6 +556,17 @@ files = [ classify-imports = "*" flake8 = "*" +[[package]] +name = "future" +version = "1.0.0" +description = "Clean single-source support for Python 3 and 2" +optional = false +python-versions = ">=2.6, !=3.0.*, !=3.1.*, !=3.2.*" +files = [ + {file = "future-1.0.0-py3-none-any.whl", hash = "sha256:929292d34f5872e70396626ef385ec22355a1fae8ad29e1a734c3e43f9fbc216"}, + {file = "future-1.0.0.tar.gz", hash = "sha256:bd2968309307861edae1458a4f8a4f3598c03be43b97521076aebf5d94c07b05"}, +] + [[package]] name = "graphviz" version = "0.20.3" @@ -1080,6 +1091,24 @@ files = [ {file = "pycryptodome-3.20.0.tar.gz", hash = "sha256:09609209ed7de61c2b560cc5c8c4fbf892f8b15b1faf7e4cbffac97db1fffda7"}, ] +[[package]] +name = "pyevmasm" +version = "0.2.3" +description = "Ethereum Virtual Machine (EVM) assembler and disassembler" +optional = false +python-versions = ">2.7" +files = [ + {file = "pyevmasm-0.2.3-py2-none-any.whl", hash = "sha256:6dbc96f7251a5287cc2af868c96c760c2343c882afe99d01996f8133a5769355"}, + {file = "pyevmasm-0.2.3-py3-none-any.whl", hash = "sha256:57eeb2b8482a56b215402780e97c175ba11b34584d2ad0914deab146b37be540"}, + {file = "pyevmasm-0.2.3.tar.gz", hash = "sha256:1b3334e2d25bfbc4fac5e14a5d7b814999256c12dbc4c34796b9982dad73fcf6"}, +] + +[package.dependencies] +future = "*" + +[package.extras] +dev = ["coverage", "flake8", "nose"] + [[package]] name = "pyflakes" version = "3.2.0" @@ -1413,4 +1442,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "02efe427eb9e145af589b4f52107c76045cc039757787459ce61286e5baf36e5" +content-hash = "797a08803d0dccb9509b3e208e29d940c15bebd59974f3722107aa80444fdf0e" diff --git a/pyproject.toml b/pyproject.toml index 47f06714d..63fc95407 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -15,6 +15,7 @@ python = "^3.10" kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.711", subdirectory = "kevm-pyk" } eth-utils = "^4.1.1" pycryptodome = "^3.20.0" +pyevmasm = "^0.2.3" [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 5979bca6d..8eb5dd23c 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -40,6 +40,7 @@ from .hevm import Hevm from .kompile import foundry_kompile from .prove import foundry_prove +from .solc import CompilationUnit from .solc_to_k import solc_compile, solc_to_k from .utils import _LOG_FORMAT, _rv_blue, _rv_yellow, check_k_version, config_file_path, console, loglevel @@ -311,11 +312,13 @@ def exec_view_kcfg(options: ViewKcfgOptions) -> None: contract_name, _ = test_id.split('.') proof = foundry.get_apr_proof(test_id) + compilation_unit = CompilationUnit.load_build_info(options.foundry_root) + def _short_info(cterm: CTerm) -> Iterable[str]: return foundry.short_info_for_contract(contract_name, cterm) def _custom_view(elem: KCFGElem) -> Iterable[str]: - return foundry.custom_view(contract_name, elem) + return foundry.custom_view(contract_name, elem, compilation_unit) node_printer = foundry_node_printer(foundry, contract_name, proof) viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 3427cec38..84c56871a 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -37,6 +37,7 @@ from pyk.utils import ensure_dir_path, hash_str, run_process_2, single, unique from . import VERSION +from .solc import CompilationUnit from .solc_to_k import Contract, _contract_name_from_bytecode from .state_record import RecreateState, StateDiffEntry, StateDumpEntry from .utils import ( @@ -78,7 +79,6 @@ UnrefuteNodeOptions, ) - _LOGGER: Final = logging.getLogger(__name__) @@ -339,6 +339,13 @@ def srcmap_data(self, contract_name: str, pc: int) -> tuple[Path, int, int] | No _, start, end = byte_offset_to_lines(src_contract_text.split('\n'), s, l) return (src_contract_path, start, end) + def solidity_src_print(self, path: Path, start: int, end: int) -> Iterable[str]: + lines = path.read_text().split('\n') + prefix_lines = [f' {l}' for l in lines[:start]] + actual_lines = [f' | {l}' for l in lines[start:end]] + suffix_lines = [f' {l}' for l in lines[end:]] + return prefix_lines + actual_lines + suffix_lines + def solidity_src(self, contract_name: str, pc: int) -> Iterable[str]: srcmap_data = self.srcmap_data(contract_name, pc) if srcmap_data is None: @@ -346,11 +353,7 @@ def solidity_src(self, contract_name: str, pc: int) -> Iterable[str]: contract_path, start, end = srcmap_data if not (contract_path.exists() and contract_path.is_file()): return [f'No file at path for contract {contract_name}: {contract_path}'] - lines = contract_path.read_text().split('\n') - prefix_lines = [f' {l}' for l in lines[:start]] - actual_lines = [f' | {l}' for l in lines[start:end]] - suffix_lines = [f' {l}' for l in lines[end:]] - return prefix_lines + actual_lines + suffix_lines + return self.solidity_src_print(contract_path, start, end) def short_info_for_contract(self, contract_name: str, cterm: CTerm) -> list[str]: ret_strs = self.kevm.short_info(cterm) @@ -362,11 +365,21 @@ def short_info_for_contract(self, contract_name: str, cterm: CTerm) -> list[str] ret_strs.append(f'src: {str(path)}:{start}:{end}') return ret_strs - def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]: + def custom_view(self, contract_name: str, element: KCFGElem, compilation_unit: CompilationUnit) -> Iterable[str]: if type(element) is KCFG.Node: pc_cell = element.cterm.try_cell('PC_CELL') + program_cell = element.cterm.try_cell('PROGRAM_CELL') if type(pc_cell) is KToken and pc_cell.sort == INT: - return self.solidity_src(contract_name, int(pc_cell.token)) + if type(program_cell) is KToken: + try: + bytecode = ast.literal_eval(program_cell.token) + instruction = compilation_unit.get_instruction(bytecode, int(pc_cell.token)) + node = instruction.node() + start_line, _, end_line, _ = node.source_range() + return self.solidity_src_print(Path(node.source.name), start_line - 1, end_line) + except Exception: + return [f'No sourcemap data for contract at pc {contract_name}: {int(pc_cell.token)}'] + return ['NO DATA'] elif type(element) is KCFG.Edge: return list(element.rules) elif type(element) is KCFG.NDBranch: @@ -374,11 +387,22 @@ def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]: return ['NO DATA'] def build(self, no_metadata: bool) -> None: - forge_build_args = ['forge', 'build', '--build-info', '--root', str(self._root)] + ( - ['--no-metadata'] if no_metadata else [] - ) + forge_build_args = [ + 'forge', + 'build', + '--build-info', + '--extra-output', + 'storageLayout', + 'evm.bytecode.generatedSources', + 'evm.deployedBytecode.generatedSources', + '--root', + str(self._root), + ] + (['--no-metadata'] if no_metadata else []) try: - run_process_2(forge_build_args, logger=_LOGGER) + run_process_2( + forge_build_args, + logger=_LOGGER, + ) except FileNotFoundError as err: raise RuntimeError( "Error: 'forge' command not found. Please ensure that 'forge' is installed and added to your PATH." @@ -1333,24 +1357,32 @@ class FoundryNodePrinter(KEVMNodePrinter): foundry: Foundry contract_name: str omit_unstable_output: bool + compilation_unit: CompilationUnit def __init__(self, foundry: Foundry, contract_name: str, omit_unstable_output: bool = False): KEVMNodePrinter.__init__(self, foundry.kevm) self.foundry = foundry self.contract_name = contract_name self.omit_unstable_output = omit_unstable_output + self.compilation_unit = CompilationUnit.load_build_info(foundry._root) def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: ret_strs = super().print_node(kcfg, node) _pc = node.cterm.try_cell('PC_CELL') + program_cell = node.cterm.try_cell('PROGRAM_CELL') + if type(_pc) is KToken and _pc.sort == INT: - srcmap_data = self.foundry.srcmap_data(self.contract_name, int(_pc.token)) - if not self.omit_unstable_output and srcmap_data is not None: - path, start, end = srcmap_data - ret_strs.append(f'src: {str(path)}:{start}:{end}') + if type(program_cell) is KToken: + try: + bytecode = ast.literal_eval(program_cell.token) + instruction = self.compilation_unit.get_instruction(bytecode, int(_pc.token)) + ast_node = instruction.node() + start_line, _, end_line, _ = ast_node.source_range() + ret_strs.append(f'src: {str(Path(ast_node.source.name))}:{start_line}:{end_line}') + except Exception: + pass calldata_cell = node.cterm.try_cell('CALLDATA_CELL') - program_cell = node.cterm.try_cell('PROGRAM_CELL') if type(program_cell) is KToken: selector_bytes = None diff --git a/src/kontrol/solc.py b/src/kontrol/solc.py new file mode 100644 index 000000000..a13f5626b --- /dev/null +++ b/src/kontrol/solc.py @@ -0,0 +1,595 @@ +from __future__ import annotations + +import hashlib +import json +import logging +import os +from collections import deque +from functools import cache, cached_property +from typing import TYPE_CHECKING + +if TYPE_CHECKING: + from collections.abc import Iterator + from pathlib import Path + +import pyevmasm # type: ignore + +if TYPE_CHECKING: + from typing import Any + + Json = dict[str, Any] + + """ + An AstNodeSourceMapEntry is triple (s,l,f) where + s denotes the start offset in bytes + l denotes the length in bytes + f denotes the identifier of the source unit + See: https://docs.soliditylang.org/en/latest/internals/source_mappings.html + """ + AstNodeSourceMapEntry = tuple[int, int, int] + + """ + A ContractSourceMapEntry is a tuple (s,l,f,j,m) where + s denotes the start offset in bytes + l denotes the length in bytes + f denotes the identifier of the source unit + j denotes the jump type 'i', 'o', or '-' + m denotes the modifier depth + See: https://docs.soliditylang.org/en/latest/internals/source_mappings.html + """ + ContractSourceMapEntry = tuple[int, int, int, str, int] + + """ + A contract source map is a map from instruction offsets to source map entries. + See: https://docs.soliditylang.org/en/latest/internals/source_mappings.html + """ + ContractSourceMap = dict[int, ContractSourceMapEntry] + + """ + A line,column pair + """ + LineColumn = tuple[int, int] + + """ + A source range is a tuple (start_line, start_column, end_line, end_column) + """ + SourceRange = tuple[int, int, int, int] + + +_LOGGER = logging.getLogger(__name__) + + +class Instruction: + + data: pyevmasm.Instruction + compilation_unit: CompilationUnit + contract: ContractSource + source_map_entry: ContractSourceMapEntry + offset: int + + def __init__( + self, + data: pyevmasm.Instruction, + compilation_unit: CompilationUnit, + contract: ContractSource, + source_map_entry: ContractSourceMapEntry, + offset: int, + ): + self.data = data + self.compilation_unit = compilation_unit + self.contract = contract + self.source_map_entry = source_map_entry + self.offset = offset + + @property + def pc(self) -> int: + return self.data.pc + + @property + def operand_size(self) -> int: + return self.data.operand_size + + def __str__(self) -> str: + return f'{self.data}' + + def source_range(self) -> SourceRange: + try: + (s, l, f, *_) = self.source_map_entry + try: + source = self.compilation_unit.get_source_by_id(f) + except KeyError: + try: + source = self.contract.generated_sources[f] + except KeyError: + return (1, 1, 1, 1) + start_line, start_column = source.offset_to_position(s) + end_line, end_column = source.offset_to_position(s + l - 1) + return (start_line, start_column, end_line, end_column) + except Exception: + return (1, 1, 1, 1) + + def node(self) -> AstNode: + try: + s, l, f, j, m = self.source_map_entry + try: + source = self.compilation_unit.get_source_by_id(f) + except KeyError: + source = self.contract.generated_sources[f] + node = source.ast.find_by_range(s, s + l) + assert node is not None + return node + except Exception as error: + raise Exception('Node not found.') from error + + +class AstNode: + json: Json + parent: AstNode | None + source: Source + + def __init__(self, dct: Json, source: Source, parent: AstNode | None = None): + self.json = dct + self.source = source + self.parent = parent + + def __hash__(self) -> int: + result = self.json.get('id') + if isinstance(result, int): + return result + result = self.json.get('src') + if isinstance(result, str): + return hash(result) + raise TypeError('AstNode.id is not an int.') + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, AstNode): + return False + return self.json.get('src') == other.json.get('src') + + ########################################################################### + # Traveral Methods + + def _children(self) -> Iterator[AstNode]: + """Iterate all direct children.""" + values = self.json.values() + for value in values: + if AstNode.is_solidity_node_like(value): + yield AstNode(value, self.source, self) + elif isinstance(value, list): + for child in value: + if AstNode.is_solidity_node_like(child): + yield AstNode(child, self.source, self) + return + + @cache # noqa: B019 + def children(self) -> list[AstNode]: + return list(self._children()) + + @cache # noqa: B019 + def sourcemap(self) -> AstNodeSourceMapEntry: + """Return the source map associated with this node. + + The first component is the start offset in unicode points. + The second compnent is the length in unicode points. + The third compnent is the identifier of the source unit. + """ + parts = self.json['src'].split(':') + start, length, source_id = (int(part) for part in parts) + return (start, length, source_id) + + def find_by_range(self, range_start: int, range_end: int) -> AstNode | None: + """Find the inner-most AstNode surrounding the given source range""" + start, l, source_id = self.sourcemap() # noqa: E741 + end = start + l + if not (start <= range_start and range_end <= end): + return None + closest = self + queue = deque(self.children()) + while len(queue) > 0: + current = queue.popleft() + start, l, source_id = current.sourcemap() # noqa: E741 + end = start + l + if start <= range_start and range_end <= end: + queue = deque(current.children()) + closest = current + return closest + + def source_range(self) -> SourceRange: + start, l, _ = self.sourcemap() + range = self.source.offset_to_position(start) + self.source.offset_to_position(start + l - 1) + return range + + def get(self, name: str, default: Any) -> Any: + if name in self.json: + return self.json[name] + else: + return default + + ########################################################################### + # Type Checking + + @staticmethod + def is_node_like(node: Any) -> bool: + return isinstance(node, dict) and 'nodeType' in node and isinstance(node['nodeType'], str) + + @staticmethod + def is_solidity_node_like(node: Any) -> bool: + return AstNode.is_node_like(node) and not node['nodeType'].startswith('Yul') + + +class Source: + """ + Represents a source unit used during compilation. + """ + + _uuid: int + + """ + Virtual name of the source. This looks like a file path, + but it might be a generated pseudo name. + """ + _name: str + + """ + The output standard Json, i.e. output.sources.$name + """ + _json: Json + + """ + The original source text. + """ + _source_text: str + + """ + A flag indicating that this source was generated by the compiler. + """ + _generated: bool + + """ + A map of byte offsets to (line, column)-pairs. + """ + _positions: dict[int, LineColumn] + + """ + A map of (line, column)-pairs to byte offsets. + """ + _offsets: dict[LineColumn, int] + + def __init__(self, uuid: int, name: str, json: Json, source_text: str, generated: bool = False): + self._uuid = uuid + self._name = name + self._json = json + self._source_text = source_text + self._generated = generated + self._positions = {} + self._offsets = {} + self._cache_source_map() + + @property + def uuid(self) -> int: + """ + A universal unique identifier for the source unit. + Use id to get a local relative to the compilation unit. + """ + return self._uuid + + @property + def id(self) -> int: + """ + The local id of the source unit relative to the compilation unit. + Use uuid to get a univeral id. + """ + result = self._json.get('id') + if isinstance(result, int): + return result + raise TypeError('Source.json.id is not an int.') + + @property + def ast(self) -> AstNode: + dct = self._json.get('ast') + if isinstance(dct, dict): + return AstNode(dct, self) + raise TypeError('Source.json.ast is not a dict.') + + def offset_to_position(self, offset: int) -> LineColumn: + """Return the (line, column)-pair for a given byte-offset. + + lines and columns start at 1. + """ + return self._positions[offset] + + def position_to_offset(self, position: LineColumn) -> int: + """Return the byte-offset of a given (line, column)-pair + + lines and columns start at 1. + """ + return self._offsets[position] + + @property + def source_text(self) -> str: + return self._source_text + + def _cache_source_map(self) -> None: + line, column = (1, 1) + for offset in range(len(self.source_text)): + self._positions[offset] = (line, column) + self._offsets[(line, column)] = offset + char = self.source_text[offset] + if char == '\n': + line, column = (line + 1, 1) + else: + column = column + len(char.encode('utf-8')) + + @property + def offsets(self) -> dict[LineColumn, int]: + """Map from (line, column)-pairs to byte offsets.""" + return self._offsets + + @property + def name(self) -> str: + return self._name + + def is_generated(self) -> bool: + return self._generated + + +class ContractSource: + _uuid: int + _file_path: str + _contract_name: str + _json: Any + _compilation_unit: CompilationUnit + + _source_map: ContractSourceMap + _init_source_map: ContractSourceMap + _storage_layout: list[dict[str, Any]] + + def __init__( + self, id: int, file_path: str, contract_name: str, json: Any, compilation_unit: CompilationUnit + ) -> None: + self._uuid = id + self._file_path = file_path + self._contract_name = contract_name + self._json = json + self._compilation_unit = compilation_unit + self._source_map = {} + self._init_source_map = {} + self._cache_source_map() + self._cache_init_source_map() + self._storage_layout = [] + + @property + def uuid(self) -> int: + """ + A unique identifier for the contract. + """ + return self._uuid + + @cached_property + def generated_sources(self) -> dict[int, Source]: + """ + Return a map of all associated generated sources. + + The key is the local source id (not the uuid) of the source. + """ + sources: dict[int, Source] = {} + generated_sources = self._json.get('evm', {}).get('bytecode', {}).get('generatedSources', []) + generated_sources += self._json.get('evm', {}).get('deployedBytecode', {}).get('generatedSources', []) + for generated_source in generated_sources: + source_id = generated_source['id'] + source_uuid = to_uuid(f'{self.uuid}:{source_id}') + name = generated_source.get('name') + contents = generated_source.get('contents', '') + source = Source(source_uuid, name, generated_source, contents, True) + sources[source.id] = source + return sources + + @cached_property + def instructions(self) -> list[Instruction]: + def map(offset: int, instruction: pyevmasm.Instruction) -> Instruction: + source_map_entry = self._source_map.get(offset, (-1, -1, -1, '-', 0)) + return Instruction(instruction, self._compilation_unit, self, source_map_entry, offset) + + return [ + map(offset, instruction) + for offset, instruction in enumerate(pyevmasm.disassemble_all(self.get_deployed_bytecode)) + ] + + @cached_property + def init_instructions(self) -> list[Instruction]: + def map(offset: int, instruction: pyevmasm.Instruction) -> Instruction: + source_map_entry = self._init_source_map.get(offset, (-1, -1, -1, '-', 0)) + return Instruction(instruction, self._compilation_unit, self, source_map_entry, offset) + + return [ + map(offset, instruction) + for offset, instruction in enumerate(pyevmasm.disassemble_all(self.get_init_bytecode)) + ] + + @cached_property + def pc_to_instruction_offsets(self) -> dict[int, int]: + result = {} + for i, instr in enumerate(self.instructions): + pc_start = instr.pc + pc_end = instr.pc + instr.operand_size + 1 + for pc in range(pc_start, pc_end): + result[pc] = i + return result + + @cached_property + def init_pc_to_instruction_offsets(self) -> dict[int, int]: + result = {} + for i, instr in enumerate(self.init_instructions): + pc_start = instr.pc + pc_end = instr.pc + instr.operand_size + 1 + for pc in range(pc_start, pc_end): + result[pc] = i + return result + + def instruction_by_pc(self, pc: int) -> Instruction: + offset = self.pc_to_instruction_offsets[pc] + return self.instructions[offset] + + def init_instruction_by_pc(self, pc: int) -> Instruction: + offset = self.init_pc_to_instruction_offsets[pc] + return self.init_instructions[offset] + + @cached_property + def get_deployed_bytecode(self) -> bytes: + ref = self._json.get('evm') if 'evm' in self._json else self._json + raw = ref.get('deployedBytecode').get('object').removeprefix('0x') + return bytes.fromhex(raw) + + @cached_property + def get_init_bytecode(self) -> bytes: + ref = self._json.get('evm') if 'evm' in self._json else self._json + raw = ref.get('bytecode').get('object').removeprefix('0x') + return bytes.fromhex(raw) + + def _cache_source_map(self) -> None: + ref = self._json.get('evm') if 'evm' in self._json else self._json + raw = ref.get('deployedBytecode', {}).get('sourceMap', '') + instrs_srcmap = raw.split(';') + s, l, f, j, m = (0, 0, 0, '', 0) # noqa: E741 + for i, instr_srcmap in enumerate(instrs_srcmap): + fields = instr_srcmap.split(':') + s = int(fields[0]) if len(fields) > 0 and fields[0] else s + l = int(fields[1]) if len(fields) > 1 and fields[1] else l # noqa: E741 + f = int(fields[2]) if len(fields) > 2 and fields[2] else f + j = fields[3] if len(fields) > 3 and fields[3] else j + m = int(fields[4]) if len(fields) > 4 and fields[4] else m + self._source_map[i] = (s, l, f, j, m) + + def _cache_init_source_map(self) -> None: + ref = self._json.get('evm') if 'evm' in self._json else self._json + raw = ref.get('bytecode', {}).get('sourceMap', '') + instrs_srcmap = raw.split(';') + s, l, f, j, m = (0, 0, 0, '', 0) # noqa: E741 + for i, instr_srcmap in enumerate(instrs_srcmap): + fields = instr_srcmap.split(':') + s = int(fields[0]) if len(fields) > 0 and fields[0] else s + l = int(fields[1]) if len(fields) > 1 and fields[1] else l # noqa: E741 + f = int(fields[2]) if len(fields) > 2 and fields[2] else f + j = fields[3] if len(fields) > 3 and fields[3] else j + m = int(fields[4]) if len(fields) > 4 and fields[4] else m + self._init_source_map[i] = (s, l, f, j, m) + + +class CompilationUnit: + """Easy access to Solidity standard json""" + + _id: int + _sources: dict[int, Source] # Source UUID => Source + _contracts: dict[bytes, ContractSource] + + def __init__(self, id: int, sources: dict[int, Source], contracts: dict[bytes, ContractSource]): + self._id = id + self._sources = sources + self._contracts = contracts + + @property + def uuid(self) -> int: + """ + A unique identifier for the compilation unit. + """ + return self._id + + @staticmethod + def load_build_info(foundry_root: Path) -> CompilationUnit: + build_info_files = (foundry_root / 'out' / 'build-info').glob('*.json') + build_info = json.loads(max(build_info_files, key=os.path.getmtime).read_text()) + sources: dict[int, Source] = {} # Source id => Source + contracts: dict[bytes, ContractSource] = {} # CBOR metadata => contract + compilation_unit_uuid = to_uuid(build_info['id']) + compilation_unit = CompilationUnit(compilation_unit_uuid, sources, contracts) + try: + for source_name, source_json in build_info.get('output', {}).get('sources', {}).items(): + absolute_path = source_json.get('ast').get('absolutePath') + source_uuid = to_uuid(f'{compilation_unit_uuid}:{source_name}') + source_text = build_info.get('input', {}).get('sources', {}).get(source_name, {}).get('content', '') + source = Source(source_uuid, source_name, source_json, source_text) + sources[source_uuid] = source + contracts_json = build_info.get('output', {}).get('contracts', {}).get(source_name, {}) + for contract_name, contract_json in contracts_json.items(): + contract_uuid = to_uuid(f'{source_uuid}:{contract_name}') + contract = ContractSource( + contract_uuid, absolute_path, contract_name, contract_json, compilation_unit + ) + contract_bytecode = contract.get_deployed_bytecode + cbor_data = CompilationUnit.get_cbor_data(contract_bytecode) + contracts[cbor_data] = contract + + # Add all generated sources + for generated_source in contract.generated_sources.values(): + sources[generated_source.uuid] = generated_source + + except (KeyError, IndexError): + _LOGGER.error( + '.output.contracts.$contract_name.evm.deployedBytecode.generatedSources not found in build-info file.' + ) + except FileNotFoundError: + _LOGGER.error('No build-info file found in build-info directory.') + + return compilation_unit + + def get_instruction(self, contract_bytecode: bytes, pc: int) -> Instruction: + # First try to match init bytecode 1-to-1 + try: + contract_source = self.get_contract_by_initcode(contract_bytecode) + return contract_source.init_instruction_by_pc(pc) + except Exception: + pass + + # We cannot identify the contract by the full deployed bytecode. + + # The deployed bytecode on-chain can be different from the + # deployed bytecode given in the standard json. + # This can for example be the case, when a library is linked at deployment time + # or when an immutable varirable is initialized at deployment time. + # Hence, to identify the contract, we only look at the CBOR-encoded metadata + # at the end of the bytecode. This metadata should not change between deployments. + + # We don't actually need to decode it, we just need to know the length of the metadata. + cbor_data = CompilationUnit.get_cbor_data(contract_bytecode) + contract = self._contracts.get(cbor_data, None) + if contract is not None: + return contract.instruction_by_pc(pc) + + # The former method can fail to detect the contract, if the CBOR_DATA + # is not at the end of the bytecode. In this case we use this slower + # method to find the contract. Notice, that it is possible to trick + # the method into return the wrong contract by copying the CBOR_DATA + # of another contract into the malicuous contract's bytecode. + for cbor_data, contract in self._contracts.items(): + if cbor_data in contract_bytecode: + return contract.instruction_by_pc(pc) + raise Exception('Contract not found.') + + def get_contract_by_initcode(self, bytecode: bytes) -> ContractSource: + for contract in self._contracts.values(): + if contract.get_init_bytecode == bytecode: + return contract + raise Exception('Contract initialization code not found.') + + @staticmethod + def get_cbor_data(contract_bytecode: bytes) -> bytes: + # Notice, that the CBOR_DATA is not necessarily at the end of the bytecode. + # Hence this method can return incorrect data. + cbor_length = contract_bytecode[-2:] # last two bytes + cbor_length = int.from_bytes(cbor_length, byteorder='big') # type: ignore + cbor_data = contract_bytecode[-cbor_length - 2 : -2] # type: ignore + return cbor_data + + def get_source_by_id(self, source_id: int) -> Source: + for source in self._sources.values(): + if source.id == source_id: + return source + raise KeyError('Source not found.') + + +def to_uuid(s: str) -> int: + # Compute the SHA-256 hash of the input string + sha256_hash = hashlib.sha256(s.encode('utf-8')).hexdigest() + # Convert the hexadecimal hash to an integer + hash_int = int(sha256_hash, 16) % (2**31) + return hash_int diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected index df89c5b56..d7f08dfb8 100644 --- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected +++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AccountParamsTest.testDealConcrete() │ │ (898 steps) diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected index 08d0b3e0b..accc1f086 100644 --- a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected +++ b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%cse%AddConst.applyOp(uint256) ┃ ┃ (branch) @@ -14,6 +15,7 @@ ┃ │ pc: 0 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%cse%AddConst.applyOp(uint256) ┃ │ ┃ │ (446 steps) @@ -22,6 +24,7 @@ ┃ │ pc: 87 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%cse%AddConst.applyOp(uint256) ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -39,6 +42,7 @@ │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%cse%AddConst.applyOp(uint256) │ │ (371 steps) @@ -47,6 +51,7 @@ │ pc: 179 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: EVMC_REVERT + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%cse%AddConst.applyOp(uint256) │ ┊ constraint: OMITTED CONSTRAINT diff --git a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected index 2f30bcca1..512f6c543 100644 --- a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected +++ b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AddrTest.test_addr_true() │ │ (1258 steps) @@ -12,6 +13,7 @@ │ pc: 333 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AddrTest.test_addr_true() │ ┊ constraint: true diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected index b18f0d9e3..7b3499989 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%ArithmeticCallTest.setUp() │ │ (1024 steps) @@ -12,6 +13,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add(uint256,uint256) ┃ ┃ (branch) @@ -22,10 +24,11 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (73 steps) -┃ └─ 11 (leaf, terminal) +┃ └─ 13 (leaf, terminal) ┃ k: #halt ~> CONTINUATION:K ┃ pc: 2357 ┃ callDepth: 0 @@ -41,6 +44,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (486 steps) @@ -61,6 +65,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (735 steps) @@ -69,6 +74,7 @@ ┃ │ pc: 248 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:77:79 ┃ │ method: test%ArithmeticCallTest.test_double_add(uint256,uint256) ┃ │ ┃ ┊ constraint: true @@ -89,6 +95,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add(uint256,uint256) │ │ (745 steps) @@ -105,7 +112,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 - rule [BASIC-BLOCK-9-TO-11]: + rule [BASIC-BLOCK-9-TO-13]: ( #execute @@ -485,7 +492,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))) - [priority(20), label(BASIC-BLOCK-9-TO-11)] + [priority(20), label(BASIC-BLOCK-9-TO-13)] rule [BASIC-BLOCK-1-TO-7]: diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected index b0912bf92..e50b67447 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%ArithmeticCallTest.setUp() │ │ (1045 steps) @@ -12,6 +13,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add(uint256,uint256) ┃ ┃ (branch) @@ -22,10 +24,11 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (73 steps) -┃ └─ 11 (leaf, terminal) +┃ └─ 13 (leaf, terminal) ┃ k: #halt ~> CONTINUATION:K ┃ pc: 2613 ┃ callDepth: 0 @@ -41,6 +44,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (486 steps) @@ -61,10 +65,11 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (907 steps) -┃ └─ 19 (leaf, terminal) +┃ └─ 21 (leaf, terminal) ┃ k: #halt ~> CONTINUATION:K ┃ pc: 2852 ┃ callDepth: 0 @@ -82,6 +87,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (1320 steps) @@ -104,6 +110,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (1576 steps) @@ -112,6 +119,7 @@ ┃ │ pc: 248 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:77:79 ┃ │ method: test%ArithmeticCallTest.test_double_add_double_sub(uint256,uint256) ┃ │ ┃ ┊ constraint: true @@ -134,6 +142,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add(uint256,uint256) │ │ (1579 steps) @@ -150,7 +159,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT256):0 - rule [BASIC-BLOCK-9-TO-11]: + rule [BASIC-BLOCK-9-TO-13]: ( #execute @@ -530,7 +539,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))) - [priority(20), label(BASIC-BLOCK-9-TO-11)] + [priority(20), label(BASIC-BLOCK-9-TO-13)] rule [BASIC-BLOCK-1-TO-7]: @@ -1316,7 +1325,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ensures ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) + rule [BASIC-BLOCK-37-TO-21]: ( #execute @@ -1699,7 +1708,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 andBool ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int ) ))))))))))))))))))) ensures ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected index 2aef1fa31..4fc226aeb 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%ArithmeticCallTest.setUp() │ │ (1077 steps) @@ -12,6 +13,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ ┃ (branch) @@ -24,6 +26,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ │ (73 steps) @@ -32,6 +35,7 @@ ┃ pc: 1584 ┃ callDepth: 0 ┃ statusCode: EVMC_REVERT +┃ src: lib/forge-std/lib/ds-test/src/test.sol:48:48 ┃ method: test%ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256) ┃ ┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) CONTINUATION:K ┃ pc: 1584 ┃ callDepth: 0 ┃ statusCode: EVMC_REVERT +┃ src: lib/forge-std/lib/ds-test/src/test.sol:48:48 ┃ method: test%ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256) ┃ ┣━━┓ constraints: @@ -62,6 +68,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ │ (503 steps) @@ -70,6 +77,7 @@ ┃ pc: 1708 ┃ callDepth: 0 ┃ statusCode: EVMC_REVERT +┃ src: lib/forge-std/lib/ds-test/src/test.sol:54:57 ┃ method: test%ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256) ┃ ┣━━┓ constraints: @@ -82,6 +90,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ │ (503 steps) @@ -90,6 +99,7 @@ ┃ pc: 1708 ┃ callDepth: 0 ┃ statusCode: EVMC_REVERT +┃ src: lib/forge-std/lib/ds-test/src/test.sol:54:57 ┃ method: test%ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256) ┃ ┣━━┓ constraints: @@ -104,6 +114,7 @@ ┃ │ pc: 0 ┃ │ callDepth: 1 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ │ (759 steps) @@ -112,6 +123,7 @@ ┃ │ pc: 248 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:77:79 ┃ │ method: test%ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256) ┃ │ ┃ ┊ constraint: true @@ -134,6 +146,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) │ │ (762 steps) @@ -535,7 +548,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT )))))))))))))))))))) [priority(20), label(BASIC-BLOCK-9-TO-12)] - rule [BASIC-BLOCK-10-TO-13]: + rule [BASIC-BLOCK-10-TO-16]: ( #execute @@ -917,7 +930,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))) - [priority(20), label(BASIC-BLOCK-10-TO-13)] + [priority(20), label(BASIC-BLOCK-10-TO-16)] rule [BASIC-BLOCK-1-TO-7]: diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected index 6cd5b621d..7a8ac627c 100644 --- a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add(uint256,uint256) ┃ ┃ (branch) @@ -14,6 +15,7 @@ ┃ │ pc: 0 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ │ (470 steps) @@ -22,6 +24,7 @@ ┃ │ pc: 128 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add(uint256,uint256) ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -39,6 +42,7 @@ │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add(uint256,uint256) │ │ (407 steps) @@ -47,6 +51,7 @@ │ pc: 550 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: EVMC_REVERT + │ src: lib/forge-std/src/StdInvariant.sol:90:90 │ method: src%ArithmeticContract.add(uint256,uint256) │ ┊ constraint: OMITTED CONSTRAINT diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected index c8ae7e2a1..9fa9cd843 100644 --- a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ ┃ (branch) @@ -14,14 +15,16 @@ ┃ │ pc: 0 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ │ (539 steps) -┃ ├─ 7 (terminal) +┃ ├─ 9 (terminal) ┃ │ k: #halt ~> CONTINUATION:K ┃ │ pc: 295 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: EVMC_REVERT +┃ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:63 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -41,6 +44,7 @@ ┃ │ pc: 0 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ │ (552 steps) @@ -49,6 +53,7 @@ ┃ │ pc: 295 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: EVMC_REVERT +┃ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:63 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -69,6 +74,7 @@ ┃ │ pc: 0 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ │ (921 steps) @@ -77,6 +83,7 @@ ┃ │ pc: 128 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -97,6 +104,7 @@ │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) │ │ (844 steps) @@ -105,6 +113,7 @@ │ pc: 550 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: EVMC_REVERT + │ src: lib/forge-std/src/StdInvariant.sol:90:90 │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256) │ ┊ constraint: OMITTED CONSTRAINT @@ -121,7 +130,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):0 - rule [BASIC-BLOCK-17-TO-7]: + rule [BASIC-BLOCK-17-TO-9]: ( #execute => #halt ) @@ -302,7 +311,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 9 ) ) )))))))))))))))))))))))))))) - [priority(20), label(BASIC-BLOCK-17-TO-7)] + [priority(20), label(BASIC-BLOCK-17-TO-9)] rule [BASIC-BLOCK-23-TO-11]: diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected index 283cbe78a..82500f84c 100644 --- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (182 steps) @@ -12,6 +13,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.setUp() │ │ (1 step) @@ -20,6 +22,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.checkFail_assert_false() │ │ (307 steps) diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected index ae0dc65c3..3c28d7a55 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (182 steps) @@ -12,6 +13,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.setUp() │ │ (1 step) @@ -20,6 +22,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.testFail_assert_true() │ │ (200 steps) @@ -28,6 +31,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.testFail_assert_true() │ │ (1 step) @@ -36,6 +40,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.testFail_assert_true() │ │ (2 steps) @@ -44,6 +49,7 @@ pc: 328 callDepth: 0 statusCode: EVMC_SUCCESS + src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 method: test%AssertTest.testFail_assert_true() diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected index d0f1c4c14..8e19ecb0f 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (182 steps) @@ -12,6 +13,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.setUp() │ │ (1 step) @@ -20,6 +22,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.testFail_expect_revert() │ │ (417 steps) @@ -28,6 +31,7 @@ │ pc: 811 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:78:78 │ method: test%AssertTest.testFail_expect_revert() │ │ (1 step) @@ -36,6 +40,7 @@ │ pc: 811 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:78:78 │ method: test%AssertTest.testFail_expect_revert() │ │ (230 steps) @@ -44,6 +49,7 @@ │ pc: 892 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:78:78 │ method: test%AssertTest.testFail_expect_revert() │ │ (1 step) @@ -52,6 +58,7 @@ │ pc: 892 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:78:78 │ method: test%AssertTest.testFail_expect_revert() │ │ (18 steps) @@ -60,6 +67,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.call_assert_false() │ │ (1 step) @@ -68,6 +76,7 @@ │ pc: 0 │ callDepth: 1 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.call_assert_false() │ │ (319 steps) @@ -108,6 +117,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.testFail_expect_revert() │ │ (1 step) @@ -116,6 +126,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.testFail_expect_revert() │ │ (2 steps) @@ -124,6 +135,7 @@ pc: 328 callDepth: 0 statusCode: EVMC_SUCCESS + src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 method: test%AssertTest.testFail_expect_revert() diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected index cca11727d..d13b54270 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (182 steps) @@ -12,6 +13,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.setUp() │ │ (1 step) @@ -20,6 +22,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.test_assert_false() │ │ (307 steps) diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected index d96bf404a..e839585dd 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (182 steps) @@ -12,6 +13,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.setUp() │ │ (1 step) @@ -20,6 +22,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.test_assert_true() │ │ (263 steps) @@ -28,6 +31,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.test_assert_true() │ │ (1 step) @@ -36,6 +40,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.test_assert_true() │ │ (2 steps) @@ -44,6 +49,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.test_assert_true() │ ┊ constraint: true diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected index 3a39c4dc2..a9bf46b9d 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (182 steps) @@ -12,6 +13,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.setUp() │ │ (1 step) @@ -20,6 +22,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.test_failing_branch(uint256) │ │ (360 steps) @@ -28,6 +31,7 @@ │ pc: 1116 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:74:74 │ method: test%AssertTest.test_failing_branch(uint256) ┃ ┃ (branch) @@ -38,6 +42,7 @@ ┃ │ pc: 1116 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74 ┃ │ method: test%AssertTest.test_failing_branch(uint256) ┃ │ ┃ │ (39 steps) @@ -46,6 +51,7 @@ ┃ │ pc: 328 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 ┃ │ method: test%AssertTest.test_failing_branch(uint256) ┃ │ ┃ │ (1 step) @@ -54,6 +60,7 @@ ┃ │ pc: 328 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 ┃ │ method: test%AssertTest.test_failing_branch(uint256) ┃ │ ┃ │ (2 steps) @@ -62,6 +69,7 @@ ┃ │ pc: 328 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 ┃ │ method: test%AssertTest.test_failing_branch(uint256) ┃ │ ┃ ┊ constraint: true @@ -79,6 +87,7 @@ │ pc: 1116 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode + │ src: lib/forge-std/src/StdInvariant.sol:74:74 │ method: test%AssertTest.test_failing_branch(uint256) │ │ (63 steps) diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected index f065f2ab5..777598fbf 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (182 steps) @@ -12,6 +13,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.setUp() │ │ (1 step) @@ -20,6 +22,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.test_revert_branch(uint256,uint256) │ │ (366 steps) @@ -28,6 +31,7 @@ │ pc: 1590 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/lib/ds-test/src/test.sol:48:62 │ method: test%AssertTest.test_revert_branch(uint256,uint256) ┃ ┃ (branch) @@ -38,6 +42,7 @@ ┃ │ pc: 1590 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62 ┃ │ method: test%AssertTest.test_revert_branch(uint256,uint256) ┃ │ ┃ │ (72 steps) @@ -71,6 +76,7 @@ │ pc: 1590 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode + │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62 │ method: test%AssertTest.test_revert_branch(uint256,uint256) │ │ (37 steps) @@ -79,6 +85,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode + │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.test_revert_branch(uint256,uint256) │ │ (1 step) @@ -87,6 +94,7 @@ │ pc: 328 │ callDepth: 0 │ statusCode: EVMC_SUCCESS + │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 │ method: test%AssertTest.test_revert_branch(uint256,uint256) │ │ (2 steps) @@ -95,6 +103,7 @@ pc: 328 callDepth: 0 statusCode: EVMC_SUCCESS + src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 method: test%AssertTest.test_revert_branch(uint256,uint256) diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected index 571b474ec..e0cb6f154 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssumeTest.testFail_assume_false(uint256,uint256) │ │ (561 steps) @@ -28,6 +29,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%AssumeTest.testFail_assume_false(uint256,uint256) │ │ (1 step) @@ -36,6 +38,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%AssumeTest.testFail_assume_false(uint256,uint256) │ │ (2 steps) @@ -44,6 +47,7 @@ pc: 281 callDepth: 0 statusCode: EVMC_SUCCESS + src: lib/forge-std/src/StdInvariant.sol:61:63 method: test%AssumeTest.testFail_assume_false(uint256,uint256) diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected index 39dd2fc1c..28746c691 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssumeTest.testFail_assume_true(uint256,uint256) │ │ (547 steps) @@ -52,6 +53,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%AssumeTest.testFail_assume_true(uint256,uint256) │ │ (1 step) @@ -60,6 +62,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%AssumeTest.testFail_assume_true(uint256,uint256) │ │ (2 steps) @@ -68,6 +71,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%AssumeTest.testFail_assume_true(uint256,uint256) │ ┊ constraint: true diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index 12bc06a1c..e1bed70c0 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssumeTest.test_assume_false(uint256,uint256) │ │ (571 steps) @@ -52,6 +53,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%AssumeTest.test_assume_false(uint256,uint256) │ │ (1 step) @@ -60,6 +62,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%AssumeTest.test_assume_false(uint256,uint256) │ │ (2 steps) @@ -68,6 +71,7 @@ pc: 281 callDepth: 0 statusCode: EVMC_SUCCESS + src: lib/forge-std/src/StdInvariant.sol:61:63 method: test%AssumeTest.test_assume_false(uint256,uint256) diff --git a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected index b5a8c8e92..30ef0188a 100644 --- a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected +++ b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%BlockParamsTest.testWarp(uint256) │ │ (965 steps) @@ -12,6 +13,7 @@ │ pc: 281 │ callDepth: 0 │ statusCode: EVMC_SUCCESS +│ src: lib/forge-std/src/StdInvariant.sol:61:63 │ method: test%BlockParamsTest.testWarp(uint256) │ ┊ constraint: true diff --git a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected index f4306dfc4..8c13ea452 100644 --- a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%CSETest.setUp() │ │ (1550 steps) @@ -12,6 +13,7 @@ │ pc: 669 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:82:82 │ method: test%CSETest.test_add_const(uint256,uint256) ┃ ┃ (branch) @@ -22,6 +24,7 @@ ┃ │ pc: 669 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/forge-std/src/StdInvariant.sol:82:82 ┃ │ method: test%CSETest.test_add_const(uint256,uint256) ┃ │ ┃ │ (193 steps) @@ -30,6 +33,7 @@ ┃ pc: 737 ┃ callDepth: 0 ┃ statusCode: STATUSCODE:StatusCode +┃ src: lib/forge-std/src/StdInvariant.sol:78:78 ┃ method: test%CSETest.test_add_const(uint256,uint256) ┃ ┗━━┓ constraint: VV0_x_114b9705:Int CONTINUATION:K ┃ │ pc: 153 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: EVMC_REVERT +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: test%TGovernance.getEscrowTokenTotalSupply() ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -41,6 +44,7 @@ ┃ │ pc: 0 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: test%TGovernance.getEscrowTokenTotalSupply() ┃ │ ┃ │ (638 steps) @@ -49,6 +53,7 @@ ┃ │ pc: 68 ┃ │ callDepth: CALLDEPTH_CELL:Int ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/nested/SimpleNested.t.sol:7:11 ┃ │ method: test%TGovernance.getEscrowTokenTotalSupply() ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -68,6 +73,7 @@ │ pc: 0 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%TGovernance.getEscrowTokenTotalSupply() │ │ (389 steps) @@ -76,6 +82,7 @@ │ pc: 153 │ callDepth: CALLDEPTH_CELL:Int │ statusCode: EVMC_REVERT + │ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%TGovernance.getEscrowTokenTotalSupply() │ ┊ constraint: OMITTED CONSTRAINT @@ -92,7 +99,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 - rule [BASIC-BLOCK-13-TO-7]: + rule [BASIC-BLOCK-13-TO-9]: ( #execute => #halt ) @@ -331,7 +338,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < C_TGOVERNANCE_ESCROW_TOKEN_ID:Int <= 9 ) ) ))))))))))))))))))))))))))))))))))))))))))))))) - [priority(20), label(BASIC-BLOCK-13-TO-7)] + [priority(20), label(BASIC-BLOCK-13-TO-9)] rule [BASIC-BLOCK-16-TO-10]: diff --git a/src/tests/integration/test-data/show/gas-abstraction.expected b/src/tests/integration/test-data/show/gas-abstraction.expected index 9a918854c..f3c493939 100644 --- a/src/tests/integration/test-data/show/gas-abstraction.expected +++ b/src/tests/integration/test-data/show/gas-abstraction.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%GasTest.testInfiniteGas() │ │ (683 steps) diff --git a/src/tests/integration/test-data/show/merge-loop-heads.expected b/src/tests/integration/test-data/show/merge-loop-heads.expected index a92c4c7c0..0ae2a4197 100644 --- a/src/tests/integration/test-data/show/merge-loop-heads.expected +++ b/src/tests/integration/test-data/show/merge-loop-heads.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%BMCLoopsTest.test_bmc(uint256) │ │ (350 steps) @@ -12,6 +13,7 @@ │ pc: 1449 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:62:62 │ method: test%BMCLoopsTest.test_bmc(uint256) ┃ ┃ (branch) @@ -22,6 +24,7 @@ ┃ │ pc: 1449 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/forge-std/src/StdInvariant.sol:62:62 ┃ │ method: test%BMCLoopsTest.test_bmc(uint256) ┃ │ ┃ ┊ constraint: OMITTED CONSTRAINT @@ -31,6 +34,7 @@ ┃ │ pc: 1449 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/forge-std/src/StdInvariant.sol:62:62 ┃ │ method: test%BMCLoopsTest.test_bmc(uint256) ┃ │ ┃ │ (135 steps) @@ -39,6 +43,7 @@ ┃ pc: 350 ┃ callDepth: 0 ┃ statusCode: STATUSCODE:StatusCode +┃ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 ┃ method: test%BMCLoopsTest.test_bmc(uint256) ┃ ┗━━┓ constraint: 0 diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected index 6b8150ff8..a20869b04 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (493 steps) @@ -262,7 +263,7 @@ Node 10: -module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 +module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():1 rule [BASIC-BLOCK-1-TO-10]: diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected index 1354e0166..3b41871ac 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (543 steps) @@ -12,6 +13,7 @@ │ pc: 1116 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:74:74 │ method: test%AssertTest.test_failing_branch(uint256) ┃ ┃ (branch) @@ -22,6 +24,7 @@ ┃ │ pc: 1116 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74 ┃ │ method: test%AssertTest.test_failing_branch(uint256) ┃ │ ┃ │ (42 steps) @@ -30,6 +33,7 @@ ┃ │ pc: 328 ┃ │ callDepth: 0 ┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 ┃ │ method: test%AssertTest.test_failing_branch(uint256) ┃ │ ┃ ┊ constraint: true @@ -47,6 +51,7 @@ │ pc: 1116 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode + │ src: lib/forge-std/src/StdInvariant.sol:74:74 │ method: test%AssertTest.test_failing_branch(uint256) │ │ (66 steps) @@ -302,7 +307,7 @@ Node 16: -module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 +module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):1 rule [BASIC-BLOCK-1-TO-8]: diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected index 131f025b0..bccdc15e5 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%AssertTest.setUp() │ │ (549 steps) @@ -12,6 +13,7 @@ │ pc: 1590 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/lib/ds-test/src/test.sol:48:62 │ method: test%AssertTest.test_revert_branch(uint256,uint256) ┃ ┃ (branch) @@ -22,6 +24,7 @@ ┃ │ pc: 1590 ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62 ┃ │ method: test%AssertTest.test_revert_branch(uint256,uint256) ┃ │ ┃ │ (75 steps) @@ -39,6 +42,7 @@ │ pc: 1590 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode + │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62 │ method: test%AssertTest.test_revert_branch(uint256,uint256) │ │ (40 steps) @@ -47,6 +51,7 @@ pc: 328 callDepth: 0 statusCode: EVMC_SUCCESS + src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8 method: test%AssertTest.test_revert_branch(uint256,uint256) @@ -547,7 +552,7 @@ Node 15: -module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 +module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):1 rule [BASIC-BLOCK-1-TO-8]: diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected index a5a82dbea..9e2504e3f 100644 --- a/src/tests/integration/test-data/show/node-refutation.expected +++ b/src/tests/integration/test-data/show/node-refutation.expected @@ -4,6 +4,7 @@ │ pc: 0 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 │ method: test%MergeTest.test_branch_merge(uint256) │ │ (324 steps) @@ -12,6 +13,7 @@ │ pc: 525 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode +│ src: lib/forge-std/src/StdInvariant.sol:90:90 │ method: test%MergeTest.test_branch_merge(uint256) ┃ ┃ (branch) @@ -22,6 +24,7 @@ ┃ pc: 525 ┃ callDepth: 0 ┃ statusCode: STATUSCODE:StatusCode +┃ src: lib/forge-std/src/StdInvariant.sol:90:90 ┃ method: test%MergeTest.test_branch_merge(uint256) ┃ ┗━━┓ constraint: VV0_x_114b9705:Int