diff --git a/deps/k_release b/deps/k_release index 65a488eaa..2d5fc4fe6 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.300 +7.1.301 diff --git a/flake.lock b/flake.lock index 91c96f4ed..d375b030a 100644 --- a/flake.lock +++ b/flake.lock @@ -136,16 +136,16 @@ "uv2nix": "uv2nix" }, "locked": { - "lastModified": 1760983440, - "narHash": "sha256-SYrGoV4PuOWux7d4nYhluWD515+9sh0DjAMcEDbREVM=", + "lastModified": 1761816560, + "narHash": "sha256-W+HQS0dexhL1iBQ7eAmZS3r6hv5Ui0VmZhgAqehx0yE=", "owner": "runtimeverification", "repo": "k", - "rev": "3f0bf132df94785670cb324fbb759e85ff5ad0b6", + "rev": "137f9560cf035365a957770d41882cb6c75c3982", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.300", + "ref": "v7.1.301", "repo": "k", "type": "github" } @@ -213,11 +213,11 @@ }, "nixpkgs-unstable_2": { "locked": { - "lastModified": 1760878510, - "narHash": "sha256-K5Osef2qexezUfs0alLvZ7nQFTGS9DL2oTVsIXsqLgs=", + "lastModified": 1761672384, + "narHash": "sha256-o9KF3DJL7g7iYMZq9SWgfS1BFlNbsm6xplRjVlOCkXI=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "5e2a59a5b1a82f89f2c7e598302a9cacebb72a67", + "rev": "08dacfca559e1d7da38f3cf05f1f45ee9bfd213c", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 62f1004ef..1afa2277b 100644 --- a/flake.nix +++ b/flake.nix @@ -12,7 +12,7 @@ inputs.flake-utils.follows = "flake-utils"; }; - k-framework.url = "github:runtimeverification/k/v7.1.300"; + k-framework.url = "github:runtimeverification/k/v7.1.301"; k-framework = { inputs.flake-utils.follows = "flake-utils"; inputs.nixpkgs.follows = "nixpkgs"; diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 2616bb766..465678bb5 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -8,7 +8,7 @@ version = "0.3.181" description = "" requires-python = ">=3.10" dependencies = [ - "kframework==v7.1.300", + "kframework==v7.1.301", "rust-demangler==1.0", ] diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index ce0e0463c..bcc3adbae 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -24,6 +24,7 @@ ProveRSOpts, PruneOpts, RunOpts, + SectionEdgeOpts, ShowOpts, ViewOpts, ) @@ -141,6 +142,38 @@ def _kmir_prune(opts: PruneOpts) -> None: proof.write_proof_data() +def _kmir_section_edge(opts: SectionEdgeOpts) -> None: + # Proof dir is checked to be some in arg parsing for instructive errors + assert opts.proof_dir is not None + + if not APRProof.proof_data_exists(opts.id, opts.proof_dir): + raise ValueError(f'Proof id {opts.id} not found in proof dir {opts.proof_dir}') + + target_path = opts.proof_dir / opts.id + + _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {opts.id}') + apr_proof = APRProof.read_proof_data(opts.proof_dir, opts.id) + + smir_info = SMIRInfo.from_file(target_path / 'smir.json') + + kmir = KMIR.from_kompiled_kore(smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=target_path) + + source_id, target_id = opts.edge + _LOGGER.info(f'Attempting to add {opts.sections} sections from node {source_id} to node {target_id}') + + with kmir.kcfg_explore(apr_proof.id) as kcfg_explore: + node_ids = kcfg_explore.section_edge( + apr_proof.kcfg, + source_id=int(source_id), + target_id=int(target_id), + logs=apr_proof.logs, + sections=opts.sections, + ) + _LOGGER.info(f'Added nodes on edge {(source_id, target_id)}: {node_ids}') + + apr_proof.write_proof_data() + + def _kmir_info(opts: InfoOpts) -> None: smir_info = SMIRInfo.from_file(opts.smir_file) @@ -171,6 +204,8 @@ def kmir(args: Sequence[str]) -> None: _kmir_show(opts) case PruneOpts(): _kmir_prune(opts) + case SectionEdgeOpts(): + _kmir_section_edge(opts) case ProveRSOpts(): _kmir_prove_rs(opts) case LinkOpts(): @@ -210,6 +245,84 @@ def _arg_parser() -> ArgumentParser: '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take' ) prove_args.add_argument('--reload', action='store_true', help='Force restarting proof') + prove_args.add_argument( + '--break-on-calls', dest='break_on_calls', action='store_true', help='Break on all function and intrinsic calls' + ) + prove_args.add_argument( + '--break-on-function-calls', + dest='break_on_function_calls', + action='store_true', + help='Break on function calls (not intrinsics)', + ) + prove_args.add_argument( + '--break-on-intrinsic-calls', + dest='break_on_intrinsic_calls', + action='store_true', + help='Break on intrinsic calls (not other functions)', + ) + prove_args.add_argument( + '--break-on-thunk', dest='break_on_thunk', action='store_true', help='Break on thunk evaluation' + ) + prove_args.add_argument( + '--break-every-statement', + dest='break_every_statement', + action='store_true', + help='Break on every MIR Statement execution', + ) + prove_args.add_argument( + '--break-on-terminator-goto', + dest='break_on_terminator_goto', + action='store_true', + help='Break on Goto terminator', + ) + prove_args.add_argument( + '--break-on-terminator-switch-int', + dest='break_on_terminator_switch_int', + action='store_true', + help='Break on SwitchInt terminator', + ) + prove_args.add_argument( + '--break-on-terminator-return', + dest='break_on_terminator_return', + action='store_true', + help='Break on Return terminator', + ) + prove_args.add_argument( + '--break-on-terminator-call', + dest='break_on_terminator_call', + action='store_true', + help='Break on Call terminator', + ) + prove_args.add_argument( + '--break-on-terminator-assert', + dest='break_on_terminator_assert', + action='store_true', + help='Break on Assert terminator', + ) + prove_args.add_argument( + '--break-on-terminator-drop', + dest='break_on_terminator_drop', + action='store_true', + help='Break on Drop terminator', + ) + prove_args.add_argument( + '--break-on-terminator-unreachable', + dest='break_on_terminator_unreachable', + action='store_true', + help='Break on Unreachable terminator', + ) + prove_args.add_argument( + '--break-every-terminator', + dest='break_every_terminator', + action='store_true', + help='Break on every MIR terminator execution', + ) + prove_args.add_argument( + '--break-every-step', + dest='break_every_step', + action='store_true', + help='Break on every MIR step (statements and terminators)', + ) proof_args = ArgumentParser(add_help=False) proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view') @@ -287,6 +400,16 @@ def _arg_parser() -> ArgumentParser: ) prune_parser.add_argument('node_id', metavar='NODE', type=int, help='The node to prune') + section_edge_parser = command_parser.add_parser( + 'section-edge', help='Break an edge into sections', parents=[kcli_args.logging_args, proof_args] + ) + section_edge_parser.add_argument( + 'edge', type=lambda s: tuple(s.split(',')), help='Edge to section in CFG (format: `source,target`)' + ) + section_edge_parser.add_argument( + '--sections', type=int, default=2, help='Number of sections to make from edge (>= 2, default: 2)' + ) + prove_rs_parser = command_parser.add_parser( 'prove-rs', help='Prove a rust program', parents=[kcli_args.logging_args, prove_args] ) @@ -354,6 +477,11 @@ def _parse_args(ns: Namespace) -> KMirOpts: case 'prune': proof_dir = Path(ns.proof_dir) return PruneOpts(proof_dir, ns.id, ns.node_id) + case 'section-edge': + if ns.proof_dir is None: + raise ValueError('Must pass --proof-dir to section-edge command') + proof_dir = Path(ns.proof_dir) + return SectionEdgeOpts(proof_dir, ns.id, ns.edge, ns.sections) case 'prove-rs': return ProveRSOpts( rs_file=Path(ns.rs_file), @@ -365,6 +493,20 @@ def _parse_args(ns: Namespace) -> KMirOpts: save_smir=ns.save_smir, smir=ns.smir, start_symbol=ns.start_symbol, + break_on_calls=ns.break_on_calls, + break_on_function_calls=ns.break_on_function_calls, + break_on_intrinsic_calls=ns.break_on_intrinsic_calls, + break_on_thunk=ns.break_on_thunk, + break_every_statement=ns.break_every_statement, + break_on_terminator_goto=ns.break_on_terminator_goto, + break_on_terminator_switch_int=ns.break_on_terminator_switch_int, + break_on_terminator_return=ns.break_on_terminator_return, + break_on_terminator_call=ns.break_on_terminator_call, + break_on_terminator_assert=ns.break_on_terminator_assert, + break_on_terminator_drop=ns.break_on_terminator_drop, + break_on_terminator_unreachable=ns.break_on_terminator_unreachable, + break_every_terminator=ns.break_every_terminator, + break_every_step=ns.break_every_step, ) case 'link': return LinkOpts( diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 144b8f3fa..ed6b128f0 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -2,12 +2,13 @@ import logging from itertools import count +from random import Random from typing import TYPE_CHECKING, NamedTuple -from pyk.kast.inner import KApply, KSort, KVariable, Subst, build_cons +from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst, build_cons from pyk.kast.manip import free_vars, split_config_from from pyk.kast.prelude.collections import list_empty, list_of -from pyk.kast.prelude.kint import eqInt, leInt +from pyk.kast.prelude.kint import eqInt, intToken, leInt from pyk.kast.prelude.ml import mlEqualsTrue from pyk.kast.prelude.utils import token @@ -29,7 +30,6 @@ if TYPE_CHECKING: from collections.abc import Iterable, Iterator, Mapping, Sequence - from random import Random from typing import Any, Final from pyk.kast import KInner @@ -56,7 +56,7 @@ class SymbolicMode(NamedTuple): ... class RandomMode(NamedTuple): - random: Random + seed: int CallConfigMode = ConcreteMode | SymbolicMode | RandomMode @@ -89,12 +89,12 @@ def make_call_config( types=smir_info.types, ) return CallConfig(config=config, constraints=tuple(constraints)) - case RandomMode(random): + case RandomMode(seed): config = _make_random_call_config( definition=definition, fn_data=fn_data, types=smir_info.types, - random=random, + seed=seed, ) return CallConfig(config=config, constraints=()) @@ -148,6 +148,7 @@ def _make_concrete_call_config( definition=definition, fn_data=fn_data, localvars=[], + seed=None, ) @@ -156,13 +157,14 @@ def _make_random_call_config( definition: KDefinition, fn_data: _FunctionData, types: Mapping[Ty, TypeMetadata], - random: Random, + seed: int, ) -> KInner: - localvars = _random_locals(random, fn_data.args, types) + localvars = _random_locals(Random(seed), fn_data.args, types) return _make_concrete_call_config_with_locals( definition=definition, fn_data=fn_data, localvars=localvars, + seed=seed, ) @@ -171,23 +173,35 @@ def _make_concrete_call_config_with_locals( definition: KDefinition, fn_data: _FunctionData, localvars: list[KInner], + seed: int | None, ) -> KInner: def init_subst() -> dict[str, KInner]: init_config = definition.init_config(KSort('GeneratedTopCell')) _, res = split_config_from(init_config) return res - # The configuration is the default initial configuration, with the K cell updated with the call terminator + # The configuration is the default initial configuration, + # with the K cell updated with the call terminator (and with an srandInt call, if seed is set) # TODO: see if this can be expressed in more simple terms + + k_cell = fn_data.call_terminator + if seed is not None: + # Seed the pseudorandom generator. This is necessary for cheatcode use in concrete execution. + k_cell = KSequence( + KApply('srandInt(_)_INT-COMMON_K_Int', intToken(seed)), + k_cell, + ) + subst = Subst( { **init_subst(), **{ - 'K_CELL': fn_data.call_terminator, + 'K_CELL': k_cell, 'LOCALS_CELL': list_of(localvars), }, } ) + empty_config = definition.empty_config(KSort('GeneratedTopCell')) config = subst(empty_config) assert not free_vars(config), f'Config by construction should not have any free variables: {config}' diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 67243238e..776b51bff 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -96,7 +96,7 @@ will effectively be no-ops at this level). ```k // all memory accesses relegated to another module (to be added) - rule #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN)) + rule [execStmt]: #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN)) => #setLocalValue(PLACE, RVAL) ... @@ -139,7 +139,7 @@ function call, pushing a new stack frame and returning to a different block after the call returns. ```k - rule #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT + rule [termGoto]: #execTerminator(terminator(terminatorKindGoto(I), _SPAN)) ~> _CONT => #execBlockIdx(I) @@ -154,7 +154,7 @@ will be `129`. ```k syntax KItem ::= #selectBlock ( SwitchTargets , Evaluation ) [strict(2)] - rule #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT + rule [termSwitchInt]: #execTerminator(terminator(terminatorKindSwitchInt(DISCR, TARGETS), _SPAN)) ~> _CONT => #selectBlock(TARGETS, DISCR) @@ -188,7 +188,7 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped. ```k - rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ + rule [termReturnSome]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #setLocalValue(DEST, #decrementRef(VAL)) ~> #execBlockIdx(TARGET) @@ -205,7 +205,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK // no value to return, skip writing - rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ + rule [termReturnNone]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #execBlockIdx(TARGET) @@ -279,14 +279,14 @@ where the returned result should go. ```k // Intrinsic function call - execute directly without state switching - rule #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _ + rule [termCallIntrinsic]: #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _ => #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET) requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC))) // Regular function call - full state switching and stack setup - rule #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _ + rule [termCallFunction]: #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _ => #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS) @@ -324,7 +324,7 @@ An operand may be a `Reference` (the only way a function could access another fu syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands) // reserve space for local variables and copy/move arguments from old locals into their place - rule #setUpCalleeData( + rule [setupCalleeData]: #setUpCalleeData( monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))), ARGS ) @@ -403,7 +403,7 @@ Otherwise the provided message is passed to a `panic!` call, ending the program ```k syntax MIRError ::= AssertError ( AssertMessage ) - rule #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT + rule [termAssert]: #execTerminator(terminator(assert(COND, EXPECTED, MSG, TARGET, _UNWIND), _SPAN)) ~> _CONT => #expect(COND, EXPECTED, MSG) ~> #execBlockIdx(TARGET) @@ -430,7 +430,7 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error. ```k - rule #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN)) + rule [termDrop]: #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN)) => #execBlockIdx(TARGET) ... @@ -438,7 +438,7 @@ Drops are elaborated to Noops but still define the continuing control flow. Unre syntax MIRError ::= "ReachedUnreachable" - rule #execTerminator(terminator(terminatorKindUnreachable, _SPAN)) + rule [termUnreachable]: #execTerminator(terminator(terminatorKindUnreachable, _SPAN)) => ReachedUnreachable ... diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index cd744b4a2..e3304290b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -102,7 +102,7 @@ It is also useful to capture unimplemented semantic constructs so that we can ha ```k syntax Value ::= thunk ( Evaluation ) - rule EV:Evaluation => thunk(EV) ... requires notBool isValue(EV) andBool notBool isTypedValue(EV) [owise] + rule [thunk]: EV:Evaluation => thunk(EV) ... requires notBool isValue(EV) andBool notBool isTypedValue(EV) [owise] ``` ### Errors Related to Accessing Local Variables diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 6fedcb209..53265f6c6 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -28,7 +28,6 @@ if TYPE_CHECKING: from collections.abc import Iterator - from random import Random from typing import Final from pyk.cterm.show import CTermShow @@ -54,6 +53,65 @@ def __init__( KParse.__init__(self, definition_dir) self.llvm_library_dir = llvm_library_dir + @staticmethod + def cut_point_rules( + break_on_calls: bool, + break_on_function_calls: bool, + break_on_intrinsic_calls: bool, + break_on_thunk: bool, + break_every_statement: bool, + break_on_terminator_goto: bool, + break_on_terminator_switch_int: bool, + break_on_terminator_return: bool, + break_on_terminator_call: bool, + break_on_terminator_assert: bool, + break_on_terminator_drop: bool, + break_on_terminator_unreachable: bool, + break_every_terminator: bool, + break_every_step: bool, + ) -> list[str]: + cut_point_rules = [] + if break_on_thunk: + cut_point_rules.append('RT-DATA.thunk') + if break_every_statement or break_every_step: + cut_point_rules.append('KMIR-CONTROL-FLOW.execStmt') + if break_on_terminator_goto or break_every_terminator or break_every_step: + cut_point_rules.append('KMIR-CONTROL-FLOW.termGoto') + if break_on_terminator_switch_int or break_every_terminator or break_every_step: + cut_point_rules.append('KMIR-CONTROL-FLOW.termSwitchInt') + if break_on_terminator_return or break_every_terminator or break_every_step: + cut_point_rules.extend( + [ + 'KMIR-CONTROL-FLOW.termReturnSome', + 'KMIR-CONTROL-FLOW.termReturnNone', + 'KMIR-CONTROL-FLOW.endprogram-return', + 'KMIR-CONTROL-FLOW.endprogram-no-return', + ] + ) + if ( + break_on_intrinsic_calls + or break_on_calls + or break_on_terminator_call + or break_every_terminator + or break_every_step + ): + cut_point_rules.append('KMIR-CONTROL-FLOW.termCallIntrinsic') + if ( + break_on_function_calls + or break_on_calls + or break_on_terminator_call + or break_every_terminator + or break_every_step + ): + cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunction') + if break_on_terminator_assert or break_every_terminator or break_every_step: + cut_point_rules.append('KMIR-CONTROL-FLOW.termAssert') + if break_on_terminator_drop or break_every_terminator or break_every_step: + cut_point_rules.append('KMIR-CONTROL-FLOW.termDrop') + if break_on_terminator_unreachable or break_every_terminator or break_every_step: + cut_point_rules.append('KMIR-CONTROL-FLOW.termUnreachable') + return cut_point_rules + @staticmethod def from_kompiled_kore( smir_info: SMIRInfo, target_dir: Path, bug_report: Path | None = None, symbolic: bool = True @@ -93,10 +151,10 @@ def run_smir( *, start_symbol: str = 'main', depth: int | None = None, - random: Random | None = None, + seed: int | None = None, ) -> Pattern: smir_info = smir_info.reduce_to(start_symbol) - mode = RandomMode(random) if random else ConcreteMode() + mode = RandomMode(seed) if seed else ConcreteMode() init_config, _ = make_call_config( self.definition, smir_info=smir_info, @@ -185,8 +243,25 @@ def prove_rs(opts: ProveRSOpts) -> APRProof: if apr_proof.passed: return apr_proof + cut_point_rules = KMIR.cut_point_rules( + break_on_calls=opts.break_on_calls, + break_on_function_calls=opts.break_on_function_calls, + break_on_intrinsic_calls=opts.break_on_intrinsic_calls, + break_on_thunk=opts.break_on_thunk, + break_every_statement=opts.break_every_statement, + break_on_terminator_goto=opts.break_on_terminator_goto, + break_on_terminator_switch_int=opts.break_on_terminator_switch_int, + break_on_terminator_return=opts.break_on_terminator_return, + break_on_terminator_call=opts.break_on_terminator_call, + break_on_terminator_assert=opts.break_on_terminator_assert, + break_on_terminator_drop=opts.break_on_terminator_drop, + break_on_terminator_unreachable=opts.break_on_terminator_unreachable, + break_every_terminator=opts.break_every_terminator, + break_every_step=opts.break_every_step, + ) + with kmir.kcfg_explore(label) as kcfg_explore: - prover = APRProver(kcfg_explore, execute_depth=opts.max_depth) + prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules) prover.advance_proof(apr_proof, max_iterations=opts.max_iterations) return apr_proof diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 52aab8ec9..cda622524 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -41,6 +41,20 @@ class ProveOpts(KMirOpts): max_depth: int | None max_iterations: int | None reload: bool + break_on_calls: bool + break_on_function_calls: bool + break_on_intrinsic_calls: bool + break_on_thunk: bool + break_every_statement: bool + break_on_terminator_goto: bool + break_on_terminator_switch_int: bool + break_on_terminator_return: bool + break_on_terminator_call: bool + break_on_terminator_assert: bool + break_on_terminator_drop: bool + break_on_terminator_unreachable: bool + break_every_terminator: bool + break_every_step: bool def __init__( self, @@ -49,12 +63,40 @@ def __init__( max_depth: int | None = None, max_iterations: int | None = None, reload: bool = False, + break_on_calls: bool = False, + break_on_function_calls: bool = False, + break_on_intrinsic_calls: bool = False, + break_on_thunk: bool = False, + break_every_statement: bool = False, + break_on_terminator_goto: bool = False, + break_on_terminator_switch_int: bool = False, + break_on_terminator_return: bool = False, + break_on_terminator_call: bool = False, + break_on_terminator_assert: bool = False, + break_on_terminator_drop: bool = False, + break_on_terminator_unreachable: bool = False, + break_every_terminator: bool = False, + break_every_step: bool = False, ) -> None: self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None self.bug_report = bug_report self.max_depth = max_depth self.max_iterations = max_iterations self.reload = reload + self.break_on_calls = break_on_calls + self.break_on_function_calls = break_on_function_calls + self.break_on_intrinsic_calls = break_on_intrinsic_calls + self.break_on_thunk = break_on_thunk + self.break_every_statement = break_every_statement + self.break_on_terminator_goto = break_on_terminator_goto + self.break_on_terminator_switch_int = break_on_terminator_switch_int + self.break_on_terminator_return = break_on_terminator_return + self.break_on_terminator_call = break_on_terminator_call + self.break_on_terminator_assert = break_on_terminator_assert + self.break_on_terminator_drop = break_on_terminator_drop + self.break_on_terminator_unreachable = break_on_terminator_unreachable + self.break_every_terminator = break_every_terminator + self.break_every_step = break_every_step @dataclass @@ -75,6 +117,20 @@ def __init__( save_smir: bool = False, smir: bool = False, start_symbol: str = 'main', + break_on_calls: bool = False, + break_on_function_calls: bool = False, + break_on_intrinsic_calls: bool = False, + break_on_thunk: bool = False, + break_every_statement: bool = False, + break_on_terminator_goto: bool = False, + break_on_terminator_switch_int: bool = False, + break_on_terminator_return: bool = False, + break_on_terminator_call: bool = False, + break_on_terminator_assert: bool = False, + break_on_terminator_drop: bool = False, + break_on_terminator_unreachable: bool = False, + break_every_terminator: bool = False, + break_every_step: bool = False, ) -> None: self.rs_file = rs_file self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None @@ -85,6 +141,20 @@ def __init__( self.save_smir = save_smir self.smir = smir self.start_symbol = start_symbol + self.break_on_calls = break_on_calls + self.break_on_function_calls = break_on_function_calls + self.break_on_intrinsic_calls = break_on_intrinsic_calls + self.break_on_thunk = break_on_thunk + self.break_every_statement = break_every_statement + self.break_on_terminator_goto = break_on_terminator_goto + self.break_on_terminator_switch_int = break_on_terminator_switch_int + self.break_on_terminator_return = break_on_terminator_return + self.break_on_terminator_call = break_on_terminator_call + self.break_on_terminator_assert = break_on_terminator_assert + self.break_on_terminator_drop = break_on_terminator_drop + self.break_on_terminator_unreachable = break_on_terminator_unreachable + self.break_every_terminator = break_every_terminator + self.break_every_step = break_every_step @dataclass @@ -187,6 +257,26 @@ def __init__(self, smir_file: Path, types: str | None = None) -> None: self.types = tuple(int(t.strip()) for t in types.split(',')) if types is not None else None +@dataclass +class SectionEdgeOpts(ProofOpts): + edge: tuple[str, str] + sections: int + + def __init__( + self, + proof_dir: Path | str, + id: str, + edge: tuple[str, str], + sections: int = 2, + bug_report: Path | None = None, + ) -> None: + self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None + self.id = id + self.edge = edge + self.sections = sections + self.bug_report = bug_report + + @dataclass class LinkOpts(KMirOpts): smir_files: list[Path] diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected index 14527a5bb..7e6b4e60a 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 0 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected index 7a6a29a6d..8d4f34f7d 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 1 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected index e34f6216e..6bbd4c726 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 2 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected index 5f53a5c0b..a46aea65e 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 3 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected index f3ae4154d..77d20383f 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 4 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected index 07b2192ed..b2eeca22a 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 5 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected index 69d9614c2..175fabdab 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 6 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected index 727ba3e1e..d186da3b3 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 7 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected index 4a696675e..5a1813338 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-8.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 8 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected index 6b31064b2..edca97d9f 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/init-9.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 9 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected index 6beeccb47..821e11dd2 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-0.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 0 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected index 115e9be29..49c6c69f5 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-1.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 1 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected index b47d6d6ab..d28072381 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-2.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 2 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected index a0ec80885..27c8bd0af 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-3.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 3 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected index 386bf94c3..56e7fffcf 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-4.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 4 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected index d4e24d40e..23a47f9da 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-5.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 5 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected index c09ff1224..5d3b0ff0c 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-6.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 6 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected index 184516b2e..6d7802d4e 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-7.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 7 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected index cbaf7ff63..c2dccad40 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-8.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 8 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected index 908e2de92..cf31f963d 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/init-9.expected @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K + srandInt ( 9 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -4 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/test_run_smir_random.py b/kmir/src/tests/integration/test_run_smir_random.py index ae0241dc1..7fcb220ca 100644 --- a/kmir/src/tests/integration/test_run_smir_random.py +++ b/kmir/src/tests/integration/test_run_smir_random.py @@ -2,7 +2,6 @@ from dataclasses import dataclass from functools import cached_property -from random import Random from typing import TYPE_CHECKING import pytest @@ -31,11 +30,6 @@ def seed(request: FixtureRequest) -> int: return request.param -@pytest.fixture -def random(seed: int) -> Random: - return Random(seed) - - @pytest.fixture( scope='module', params=[project_dir.name for project_dir in TEST_ROOT_DIR.iterdir()], @@ -98,7 +92,7 @@ def handle(project_name: str, seed: int) -> _TestDataHandle: def test_run_smir_random( kmir: KMIR, smir_info: SMIRInfo, - random: Random, + seed: int, handle: _TestDataHandle, update_expected_output: bool, ) -> None: @@ -107,7 +101,7 @@ def test_run_smir_random( kmir.definition, smir_info=smir_info, start_symbol='test', - mode=RandomMode(random), + mode=RandomMode(seed), ) init_kore = kmir.kast_to_kore(init_kast, sort=GENERATED_TOP_CELL) actual_init = kore_print( diff --git a/kmir/uv.lock b/kmir/uv.lock index d929cafa6..3268c1d77 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -365,7 +365,7 @@ name = "exceptiongroup" version = "1.3.0" source = { registry = "https://pypi.org/simple" } dependencies = [ - { name = "typing-extensions", marker = "python_full_version < '3.11'" }, + { name = "typing-extensions", marker = "python_full_version < '3.13'" }, ] sdist = { url = "https://files.pythonhosted.org/packages/0b/9f/a65090624ecf468cdca03533906e7c69ed7588582240cfe7cc9e770b50eb/exceptiongroup-1.3.0.tar.gz", hash = "sha256:b241f5885f560bc56a59ee63ca4c6a8bfa46ae4ad651af316d4e81817bb9fd88", size = 29749, upload-time = "2025-05-10T17:42:51.123Z" } wheels = [ @@ -475,16 +475,16 @@ wheels = [ [[package]] name = "hypothesis" -version = "6.142.2" +version = "6.142.4" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "attrs" }, { name = "exceptiongroup", marker = "python_full_version < '3.11'" }, { name = "sortedcontainers" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/47/83/8f76d7c965beb4d3a65d188232c32db97b0799b0e893227d520d5d2a0144/hypothesis-6.142.2.tar.gz", hash = "sha256:c4204a2ce327e45fbaf83a2b58142a285135698dc1d08e368ae9901f06b49e64", size = 465987, upload-time = "2025-10-20T16:08:20.225Z" } +sdist = { url = "https://files.pythonhosted.org/packages/47/0b/76a062d1d6cd68342b460c2f5627e1ad1102a3dd781acd5c096c75aca0d6/hypothesis-6.142.4.tar.gz", hash = "sha256:b3e71a84708994aa910ea47f1483ad892a7c390839959d689b2a2b07ebfd160e", size = 466047, upload-time = "2025-10-25T16:19:03.838Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/9b/8f/194d63f715c7b0ace35b4f2a83b756d5bc703299b706c401b7ec593054fc/hypothesis-6.142.2-py3-none-any.whl", hash = "sha256:cc6c6e66c06aff695dd255501a767b528e00d84ce3572160425a9ba5e4a47845", size = 533375, upload-time = "2025-10-20T16:08:16.903Z" }, + { url = "https://files.pythonhosted.org/packages/3e/9f/8010f93e175ecd996f54df9019ee8c58025fc21ed47658b0a58dd25ebe8b/hypothesis-6.142.4-py3-none-any.whl", hash = "sha256:25eecc73fadecd8b491aed822204cfe4be9c98ff5c1e8e038d181136ffc54b5b", size = 533467, upload-time = "2025-10-25T16:19:00.443Z" }, ] [[package]] @@ -528,7 +528,7 @@ wheels = [ [[package]] name = "kframework" -version = "7.1.300" +version = "7.1.301" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "coloredlogs" }, @@ -545,9 +545,9 @@ dependencies = [ { name = "tomli" }, { name = "xdg-base-dirs" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/0b/25/ff0d0d1fc03840579c4458dc375bd40ca6710604a3853cb7ee795c5f0757/kframework-7.1.300.tar.gz", hash = "sha256:2c2cd0e8a9821709ac0244fc364a70dd9f8f34728ed1956269dd15110d59ff94", size = 243019, upload-time = "2025-10-20T19:45:30.037Z" } +sdist = { url = "https://files.pythonhosted.org/packages/32/81/d2c8bed054adff8ce33a73e1d13f965d97a48d56c55e01612bde2c587826/kframework-7.1.301.tar.gz", hash = "sha256:2dae3e1863ea7f0107d1aacdd42174beaec8af0ac794eda34b328c3de9835aa8", size = 243112, upload-time = "2025-10-30T10:11:05.711Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/50/b4/a661ec61d0da64b290bd821e67fe425a02ca25bd2edee05b10bc8710b69c/kframework-7.1.300-py3-none-any.whl", hash = "sha256:31fd872fadad1c0b9a855017911b0b9a643280ea07bb4078f49c400ad7db7163", size = 294221, upload-time = "2025-10-20T19:45:28.309Z" }, + { url = "https://files.pythonhosted.org/packages/68/f3/820a38f833b573e1900f6d6fa15a289f6b15a7eeac406bdfa36c5e82bc25/kframework-7.1.301-py3-none-any.whl", hash = "sha256:480714ad945afa93c3b6d3d27e42591833b2de03aa67b48098533d190781de6e", size = 294306, upload-time = "2025-10-30T10:11:04.052Z" }, ] [[package]] @@ -580,7 +580,7 @@ dev = [ [package.metadata] requires-dist = [ - { name = "kframework", specifier = "==7.1.300" }, + { name = "kframework", specifier = "==7.1.301" }, { name = "rust-demangler", specifier = "==1.0" }, ] @@ -631,9 +631,6 @@ wheels = [ linkify = [ { name = "linkify-it-py" }, ] -plugins = [ - { name = "mdit-py-plugins" }, -] [[package]] name = "markupsafe" @@ -1176,18 +1173,19 @@ wheels = [ [[package]] name = "textual" -version = "6.3.0" +version = "6.4.0" source = { registry = "https://pypi.org/simple" } dependencies = [ - { name = "markdown-it-py", extra = ["linkify", "plugins"] }, + { name = "markdown-it-py", extra = ["linkify"] }, + { name = "mdit-py-plugins" }, { name = "platformdirs" }, { name = "pygments" }, { name = "rich" }, { name = "typing-extensions" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/ff/51/51a0863339c4c3fa204f43044e52dfd688a7ee2ba2c987e021acc9583a42/textual-6.3.0.tar.gz", hash = "sha256:a89c557fa740611551dcf4f93643f33853eca488183ef5882200dde8e94315e8", size = 1573232, upload-time = "2025-10-11T11:17:01.888Z" } +sdist = { url = "https://files.pythonhosted.org/packages/23/6c/565521dc6dd00fa857845483ae0c070575fda1f9a56d92d732554fecfea4/textual-6.4.0.tar.gz", hash = "sha256:f40df9165a001c10249698d532f2f5a71708b70f0e4ef3fce081a9dd93ffeaaa", size = 1573599, upload-time = "2025-10-22T17:29:51.357Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/ff/2a/bca677b0b05ee77b4105f73db0d8ef231a9f1db154d69388abd5c73f9dcc/textual-6.3.0-py3-none-any.whl", hash = "sha256:ec908b4b008662e7670af4a3e7c773847066b0950b1c50126c72fa939b514c97", size = 711457, upload-time = "2025-10-11T11:16:59.754Z" }, + { url = "https://files.pythonhosted.org/packages/37/20/6eed0e55bdd2576475e9cea49cc71c47f8e56ab54f04cbe04b2fb56440de/textual-6.4.0-py3-none-any.whl", hash = "sha256:b346dbb8e12f17cefb33ddfdf7f19bdc9e66c29daf82fc981a8db6b7d985e115", size = 711663, upload-time = "2025-10-22T17:29:49.346Z" }, ] [[package]]