From 580a7073c80ba9c3cc05a252eb9fb85564cf15ea Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 2 May 2025 13:37:52 -0500 Subject: [PATCH 01/31] Generate symbolic Integer/Bool values --- kmir/src/kmir/kast.py | 28 +++++++++++++++++++ kmir/src/kmir/kdist/mir-semantics/rt/value.md | 4 +-- 2 files changed, 30 insertions(+), 2 deletions(-) create mode 100644 kmir/src/kmir/kast.py diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py new file mode 100644 index 000000000..346801150 --- /dev/null +++ b/kmir/src/kmir/kast.py @@ -0,0 +1,28 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from pyk.kast.inner import KApply, KVariable +from pyk.kast.prelude.kint import leInt +from pyk.kast.prelude.utils import token + +if TYPE_CHECKING: + from collections.abc import Iterable + + from pyk.kast.inner import KInner + + +def int_var(varname: str, num_bytes: int, signed: bool) -> tuple[KInner, Iterable[KInner]]: + var = KVariable(varname, 'Int') + bit_width = num_bytes * 8 + var_max = ((1 << (bit_width - 1)) if signed else (1 << bit_width)) - 1 + var_min = -(1 << (bit_width - 1)) if signed else 0 + constraints = (leInt(var, token(var_max)), leInt(token(var_min), var)) + term = KApply('Value::Integer', (var, token(bit_width), token(signed))) + return term, constraints + + +def bool_var(varname: str) -> tuple[KInner, Iterable[KInner]]: + var = KVariable(varname, 'Bool') + term = KApply('Value::Bool', (var,)) + return term, () diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index c50e6eac2..3e3d3eb27 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -22,9 +22,9 @@ High-level values can be - arrays and slices (with homogenous element types) ```k - syntax Value ::= Integer( Int, Int, Bool ) + syntax Value ::= Integer( Int, Int, Bool ) [symbol(Value::Integer)] // value, bit-width, signedness for un/signed int - | BoolVal( Bool ) + | BoolVal( Bool ) [symbol(Value::Bool)] // boolean | Aggregate( VariantIdx , List ) // heterogenous value list for tuples and structs (standard, tuple, or anonymous) From 4051dd20f324b5eb2897ad82b62ea4d6d24e9202 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 8 May 2025 03:41:26 +1000 Subject: [PATCH 02/31] Add symbols for all Value constructors --- kmir/src/kmir/kast.py | 2 +- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 346801150..2462183e8 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -24,5 +24,5 @@ def int_var(varname: str, num_bytes: int, signed: bool) -> tuple[KInner, Iterabl def bool_var(varname: str) -> tuple[KInner, Iterable[KInner]]: var = KVariable(varname, 'Bool') - term = KApply('Value::Bool', (var,)) + term = KApply('Value::BoolVal', (var,)) return term, () diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index 3e3d3eb27..b85b933f4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -22,17 +22,17 @@ High-level values can be - arrays and slices (with homogenous element types) ```k - syntax Value ::= Integer( Int, Int, Bool ) [symbol(Value::Integer)] + syntax Value ::= Integer( Int, Int, Bool ) [symbol(Value::Integer)] // value, bit-width, signedness for un/signed int - | BoolVal( Bool ) [symbol(Value::Bool)] + | BoolVal( Bool ) [symbol(Value::BoolVal)] // boolean - | Aggregate( VariantIdx , List ) + | Aggregate( VariantIdx , List ) [symbol(Value::Aggregate)] // heterogenous value list for tuples and structs (standard, tuple, or anonymous) - | Float( Float, Int ) + | Float( Float, Int ) [symbol(Value::Float)] // value, bit-width for f16-f128 - | Reference( Int , Place , Mutability ) + | Reference( Int , Place , Mutability ) [symbol(Value::Reference)] // stack depth (initially 0), place, borrow kind - | Range( List ) + | Range( List ) [symbol(Value::Range)] // homogenous values for array/slice // | Ptr( Address, MaybeValue ) // address, metadata for ref/ptr From 2e2dddd70607e26c57f2befe21409843b29b6229 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 8 May 2025 04:09:39 +1000 Subject: [PATCH 03/31] New lookup tables in SMIRInfo --- kmir/src/kmir/smir.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 704587bf2..9c60e9ff1 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -61,6 +61,28 @@ def function_arguments(self) -> dict[str, dict]: def function_symbols(self) -> dict[int, dict]: return {ty: sym for ty, sym, *_ in self._smir['functions'] if type(ty) is int} + @cached_property + def function_symbols_reverse(self) -> dict[str, int]: + return {sym['NormalSym']: ty for ty, sym in self.function_symbols.items() if 'NormalSym' in sym} + + @cached_property + def function_tys(self) -> dict[str, int]: + fun_syms = self.function_symbols_reverse + + res = {'main': -1} + for item in self._smir['items']: + if not SMIRInfo._is_func(item): + continue + + mono_item_fn = item['mono_item_kind']['MonoItemFn'] + name = mono_item_fn['name'] + sym = item['symbol_name'] + if not sym in fun_syms: + continue + + res[name] = fun_syms[sym] + return res + @staticmethod def _is_func(item: dict[str, dict]) -> bool: return 'MonoItemFn' in item['mono_item_kind'] From d0197eaf3d964dfe2b50a35cc351c673ce4a9a75 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 8 May 2025 04:14:10 +1000 Subject: [PATCH 04/31] make_call_config (without arguments) --- kmir/src/kmir/kast.py | 55 +++++++++++++++++++++++ kmir/src/kmir/kdist/mir-semantics/kmir.md | 6 +-- kmir/src/kmir/kmir.py | 45 +++++++++++++++++++ 3 files changed, 103 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 2462183e8..fb2c2b4b7 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -26,3 +26,58 @@ def bool_var(varname: str) -> tuple[KInner, Iterable[KInner]]: var = KVariable(varname, 'Bool') term = KApply('Value::BoolVal', (var,)) return term, () + + +def mk_call_terminator(target: int, _arg_count: int) -> KInner: + return KApply( + '#execTerminator(_)_KMIR-CONTROL-FLOW_KItem_Terminator', + ( + KApply( + 'terminator(_,_)_BODY_Terminator_TerminatorKind_Span', + ( + KApply( + 'TerminatorKind::Call', + ( + KApply( + 'Operand::Constant', + ( + KApply( + 'constOperand(_,_,_)_BODY_ConstOperand_Span_MaybeUserTypeAnnotationIndex_MirConst', + ( + KApply('span', token(0)), + KApply( + 'noUserTypeAnnotationIndex_BODY_MaybeUserTypeAnnotationIndex', + (), + ), + KApply( + 'mirConst(_,_,_)_TYPES_MirConst_ConstantKind_Ty_MirConstId', + ( + KApply('ConstantKind::ZeroSized', ()), + KApply( + 'ty', + (token(target),), + ), + KApply('mirConstId(_)_TYPES_MirConstId_Int', (token(0),)), + ), + ), + ), + ), + ), + ), + KApply('Operands::empty', ()), + KApply( + 'place(_,_)_BODY_Place_Local_ProjectionElems', + ( + KApply('local(_)_BODY_Local_Int', (token(0),)), + KApply('ProjectionElems::empty', ()), + ), + ), + KApply('noBasicBlockIdx_BODY_MaybeBasicBlockIdx', ()), + KApply('UnwindAction::Continue', ()), + ), + ), + KApply('span', token(0)), + ), + ), + ), + ) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index ee9ebc09a..471e325d0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -59,7 +59,7 @@ The `Map` of types is static information used for decoding constants and allocat It maps `Ty` IDs to `TypeInfo` that can be supplied to decoding and casting functions as well as operations involving `Aggregate` values (related to `struct`s and `enum`s). ```k - syntax Map ::= #mkTypeMap ( Map, TypeMappings ) [function, total] + syntax Map ::= #mkTypeMap ( Map, TypeMappings ) [function, total, symbol("mkTypeMap")] rule #mkTypeMap(ACC, .TypeMappings) => ACC @@ -80,7 +80,7 @@ It maps `Ty` IDs to `TypeInfo` that can be supplied to decoding and casting func Another type-related `Map` is required to associate an `AdtDef` ID with its corresponding `Ty` ID for `struct`s and `enum`s when creating or using `Aggregate` values. ```k - syntax Map ::= #mkAdtMap ( Map , TypeMappings ) [function, total] + syntax Map ::= #mkAdtMap ( Map , TypeMappings ) [function, total, symbol("mkAdtMap")] // -------------------------------------------------------------- rule #mkAdtMap(ACC, .TypeMappings) => ACC @@ -108,7 +108,7 @@ they are callee in a `Call` terminator within an `Item`). The function _names_ and _ids_ are not relevant for calls and therefore dropped. ```k - syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total ] + syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total, symbol("mkFunctionMap") ] | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ] | #accumItems ( Map, MonoItems ) [ function, total ] diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index b3a210a7f..88688bf80 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -8,6 +8,7 @@ from pyk.cterm import CTerm, cterm_symbolic from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, Subst from pyk.kast.manip import split_config_from +from pyk.kast.prelude.collections import list_empty, map_empty from pyk.kast.prelude.string import stringToken from pyk.kcfg import KCFG from pyk.kcfg.explore import KCFGExplore @@ -19,6 +20,7 @@ from pyk.proof.show import APRProofNodePrinter from .cargo import cargo_get_smir_json +from .kast import mk_call_terminator from .kparse import KParse from .parse.parser import Parser @@ -73,6 +75,49 @@ def make_init_config( init_config = subst.apply(self.definition.init_config(KSort(sort))) return init_config + def make_call_config( + self, + parsed_smir: KApply, + smir_info: SMIRInfo, + start_symbol: str = 'main', + ) -> KInner: + + if not start_symbol in smir_info.function_tys: + raise KeyError(f'{start_symbol} not found in program') + + _sym, _allocs, functions, items, types = parsed_smir.args + + subst = { + 'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], 0), + 'STARTSYMBOL_CELL': KApply('symbol(_)_LIB_Symbol_String', (stringToken(start_symbol),)), + 'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack + 'FUNCTIONS_CELL': KApply( + 'mkFunctionMap', + ( + functions, + items, + ), + ), + 'TYPES_CELL': KApply( + 'mkTypeMap', + ( + map_empty(), + types, + ), + ), + 'ADTTOTY_CELL': KApply( + 'mkAdtMap', + ( + map_empty(), + types, + ), + ), + } + + config = self.definition.empty_config(KSort('GeneratedTopCell')) + + return Subst(subst).apply(config) + def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', depth: int | None = None) -> Pattern: init_config = self.make_init_config(parsed_smir, start_symbol) init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell')) From b653445c28147ab147abf3b1d0969cfa0119b0e8 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 2 May 2025 16:41:27 +1000 Subject: [PATCH 05/31] Allow constructing SMIRInfo from parsed json dict Previous constructor becomes a utility `from_file` --- kmir/src/kmir/__main__.py | 4 ++-- kmir/src/kmir/smir.py | 8 ++++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 6abf198b2..265c14571 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -110,7 +110,7 @@ def _kmir_view(opts: ViewOpts) -> None: proof = APRProof.read_proof_data(opts.proof_dir, opts.id) smir_info = None if opts.smir_info is not None: - smir_info = SMIRInfo(opts.smir_info) + smir_info = SMIRInfo.from_file(opts.smir_info) node_printer = KMIRAPRNodePrinter(kmir, proof, smir_info=smir_info, full_printer=False) viewer = APRProofViewer(proof, kmir, node_printer=node_printer) viewer.run() @@ -121,7 +121,7 @@ def _kmir_show(opts: ShowOpts) -> None: proof = APRProof.read_proof_data(opts.proof_dir, opts.id) smir_info = None if opts.smir_info is not None: - smir_info = SMIRInfo(opts.smir_info) + smir_info = SMIRInfo.from_file(opts.smir_info) node_printer = KMIRAPRNodePrinter(kmir, proof, smir_info=smir_info, full_printer=opts.full_printer) shower = APRProofShow(kmir, node_printer=node_printer) lines = shower.show(proof) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 9c60e9ff1..7108a1b7c 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -17,8 +17,12 @@ class SMIRInfo: _smir: dict - def __init__(self, smir_json_file: Path) -> None: - self._smir = json.loads(smir_json_file.read_text()) + def __init__(self, smir_json: dict) -> None: + self._smir = smir_json + + @staticmethod + def from_file(smir_json_file: Path) -> SMIRInfo: + return SMIRInfo(json.loads(smir_json_file.read_text())) @cached_property def types(self) -> dict[Ty, Any]: From 9e44a4cd3c5918b8af91e9ff31efde988bf20636 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 2 May 2025 16:41:59 +1000 Subject: [PATCH 06/31] REVERT ME: run with call-config when using haskell backend. BREAKS TESTS --- kmir/src/kmir/__main__.py | 10 +++++++++- kmir/src/kmir/kmir.py | 9 +++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 265c14571..99b829361 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -7,6 +7,7 @@ from typing import TYPE_CHECKING from pyk.cli.args import KCLIArgs +from pyk.kast.inner import KApply from pyk.kast.outer import KFlatModule, KImport from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofShow @@ -47,7 +48,14 @@ def _kmir_run(opts: RunOpts) -> None: sys.exit(1) kmir_kast, _ = parse_result - result = kmir.run_parsed(kmir_kast, opts.start_symbol, opts.depth) + if opts.haskell_backend: + smir_json = SMIRInfo.from_file(smir_file) + assert type(kmir_kast) is KApply + + result = kmir.run_call(kmir_kast, smir_json, opts.start_symbol, opts.depth) + else: + result = kmir.run_parsed(kmir_kast, opts.start_symbol, opts.depth) + print(kmir.kore_to_pretty(result)) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 88688bf80..f55b42b1d 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -125,6 +125,15 @@ def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', d return result + def run_call( + self, parsed_smir: KApply, smir_json: SMIRInfo, start_symbol: str = 'main', depth: int | None = None + ) -> Pattern: + init_config = self.make_call_config(parsed_smir, smir_json, start_symbol) + init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell')) + result = self.run_pattern(init_kore, depth=depth) + + return result + def apr_proof_from_kast( self, id: str, From c67ad8c1ab8dc7ce7dbafa1652d7aa86636a88c4 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 8 May 2025 05:11:38 +1000 Subject: [PATCH 07/31] WIP code to produce the call arguments (not fully working) --- kmir/src/kmir/kast.py | 31 ++++++++++++++++++++--- kmir/src/kmir/kdist/mir-semantics/body.md | 12 ++++----- 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index fb2c2b4b7..ad7612093 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -1,5 +1,6 @@ from __future__ import annotations +from functools import reduce from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KVariable @@ -28,7 +29,29 @@ def bool_var(varname: str) -> tuple[KInner, Iterable[KInner]]: return term, () -def mk_call_terminator(target: int, _arg_count: int) -> KInner: +def mk_call_terminator(target: int, arg_count: int) -> KInner: + operands = [ + KApply( + 'Operand::Copy', + KApply( + 'place', + (KApply('local', (token(i + 1),))), + ), + ) + for i in range(arg_count) + ] + args = reduce( + lambda x, y: KApply( + 'Operands::append', + ( + x, + y, + ), + ), + operands, + KApply('Operands::empty', ()), + ) + return KApply( '#execTerminator(_)_KMIR-CONTROL-FLOW_KItem_Terminator', ( @@ -64,11 +87,11 @@ def mk_call_terminator(target: int, _arg_count: int) -> KInner: ), ), ), - KApply('Operands::empty', ()), + args, KApply( - 'place(_,_)_BODY_Place_Local_ProjectionElems', + 'place', ( - KApply('local(_)_BODY_Local_Int', (token(0),)), + KApply('local', (token(0),)), KApply('ProjectionElems::empty', ()), ), ), diff --git a/kmir/src/kmir/kdist/mir-semantics/body.md b/kmir/src/kmir/kdist/mir-semantics/body.md index 9d4259339..0603e8523 100644 --- a/kmir/src/kmir/kdist/mir-semantics/body.md +++ b/kmir/src/kmir/kdist/mir-semantics/body.md @@ -46,9 +46,9 @@ syntax MaybeOperand ::= someOperand(Operand) [group(mir-option)] syntax Operands ::= List {Operand, ""} [group(mir-list), symbol(Operands::append), terminator-symbol(Operands::empty)] -syntax Local ::= local(Int) [group(mir-int)] -syntax MaybeLocal ::= someLocal(Local) [group(mir-option)] - | "noLocal" [group(mir-option)] +syntax Local ::= local(Int) [group(mir-int) , symbol(local)] +syntax MaybeLocal ::= someLocal(Local) [group(mir-option), symbol(someLocal)] + | "noLocal" [group(mir-option), symbol(noLocal)] syntax ProjectionElem ::= "projectionElemDeref" [group(mir-enum), symbol(ProjectionElem::Deref)] | projectionElemField(FieldIdx, Ty) [group(mir-enum), symbol(ProjectionElem::Field)] @@ -60,9 +60,9 @@ syntax ProjectionElem ::= "projectionElemDeref" | projectionElemSubtype(Ty) [group(mir-enum), symbol(ProjectionElem::Subtype)] syntax ProjectionElems ::= List {ProjectionElem, ""} [group(mir-list), symbol(ProjectionElems::append), terminator-symbol(ProjectionElems::empty)] -syntax Place ::= place(local: Local, projection: ProjectionElems) [group(mir---local--projection)] -syntax MaybePlace ::= somePlace(Place) [group(mir-option)] - | "noPlace" [group(mir-option)] +syntax Place ::= place(local: Local, projection: ProjectionElems) [group(mir---local--projection), symbol(place)] +syntax MaybePlace ::= somePlace(Place) [group(mir-option), symbol(somePlace)] + | "noPlace" [group(mir-option), symbol(noPlace)] syntax Branch ::= branch(MIRInt, BasicBlockIdx) [group(mir)] syntax Branches ::= List {Branch, ""} [group(mir-list), symbol(Branches::append), terminator-symbol(Branches::empty)] From 8f0e3028c26b7103166c1fb8e97d5b41fb10604e Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 12 May 2025 14:38:31 +1000 Subject: [PATCH 08/31] small tweaks to adapt to new master. Arg.less functions working --- kmir/src/kmir/kast.py | 23 ++++------------------- kmir/src/kmir/kmir.py | 2 +- 2 files changed, 5 insertions(+), 20 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index ad7612093..2ecf05fbb 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -33,21 +33,12 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner: operands = [ KApply( 'Operand::Copy', - KApply( - 'place', - (KApply('local', (token(i + 1),))), - ), + (KApply('place', (KApply('local', (token(i + 1),)), KApply('ProjectionElems::empty', ()))),), ) for i in range(arg_count) ] args = reduce( - lambda x, y: KApply( - 'Operands::append', - ( - x, - y, - ), - ), + lambda x, y: KApply('Operands::append', (x, y)), operands, KApply('Operands::empty', ()), ) @@ -68,18 +59,12 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner: 'constOperand(_,_,_)_BODY_ConstOperand_Span_MaybeUserTypeAnnotationIndex_MirConst', ( KApply('span', token(0)), - KApply( - 'noUserTypeAnnotationIndex_BODY_MaybeUserTypeAnnotationIndex', - (), - ), + KApply('noUserTypeAnnotationIndex_BODY_MaybeUserTypeAnnotationIndex', ()), KApply( 'mirConst(_,_,_)_TYPES_MirConst_ConstantKind_Ty_MirConstId', ( KApply('ConstantKind::ZeroSized', ()), - KApply( - 'ty', - (token(target),), - ), + KApply('ty', (token(target),)), KApply('mirConstId(_)_TYPES_MirConstId_Int', (token(0),)), ), ), diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index f55b42b1d..4f3c644ee 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -85,7 +85,7 @@ def make_call_config( if not start_symbol in smir_info.function_tys: raise KeyError(f'{start_symbol} not found in program') - _sym, _allocs, functions, items, types = parsed_smir.args + _sym, _allocs, functions, items, types, _ = parsed_smir.args subst = { 'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], 0), From 6525f62230dd4f5a1bcd47aa28d1b2a9a26f2158 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 12 May 2025 21:40:18 +1000 Subject: [PATCH 09/31] WIP creating symbolic arguments in python for call_config --- kmir/src/kmir/kast.py | 64 +++++++++++++++++-- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 4 +- kmir/src/kmir/kmir.py | 11 +++- kmir/src/kmir/smir.py | 2 +- 4 files changed, 69 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 2ecf05fbb..3d49108a8 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -1,6 +1,5 @@ from __future__ import annotations -from functools import reduce from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KVariable @@ -12,6 +11,8 @@ from pyk.kast.inner import KInner + from .smir import SMIRInfo + def int_var(varname: str, num_bytes: int, signed: bool) -> tuple[KInner, Iterable[KInner]]: var = KVariable(varname, 'Int') @@ -37,11 +38,17 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner: ) for i in range(arg_count) ] - args = reduce( - lambda x, y: KApply('Operands::append', (x, y)), - operands, - KApply('Operands::empty', ()), - ) + + # args = foldr(Operands::append, Operands::empty, operands) + args = KApply('Operands::empty', ()) + for op in reversed(operands): + args = KApply( + 'Operands::append', + ( + op, + args, + ), + ) return KApply( '#execTerminator(_)_KMIR-CONTROL-FLOW_KItem_Terminator', @@ -89,3 +96,48 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner: ), ), ) + + +def symbolic_locals(smir_info: SMIRInfo, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]: + locals, constraints = ArgGenerator(smir_info).run(local_types) + local0 = KApply('newLocal', (KApply('ty', (token(0),)), KApply('Mutability::Not', ()))) + return ([local0] + locals, constraints) + + +class ArgGenerator: + smir_info: SMIRInfo + locals: list[KInner] + pointees: list[KInner] + constraints: list[KInner] + counter: int + ref_offset: int + + if TYPE_CHECKING: + from .smir import Ty + + def __init__(self, smir_info: SMIRInfo) -> None: + self.smir_info = smir_info + self.locals = [] + self.pointees = [] + self.constraints = [] + self.counter = 1 + self.ref_offset = 0 + + def run(self, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]: + self.ref_offset = len(local_types) + 1 + for ty in [t['ty'] for t in local_types]: + self._add_local(ty) + return (self.locals + self.pointees, self.constraints) + + def _add_local(self, ty: Ty) -> None: + match self.smir_info.types.get(ty): + case _: + new = KApply( + 'typedValue', (self._fresh_var('ARG'), KApply('ty', (token(ty),)), KApply('Mutability::Not', ())) + ) + self.locals.append(new) + + def _fresh_var(self, prefix: str) -> KInner: + name = prefix + str(self.counter) + self.counter += 1 + return KVariable(name) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index b85b933f4..646e7dc17 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -52,11 +52,11 @@ The local variables may be actual values (`typedValue`), uninitialised (`NewLoca // local storage of the stack frame syntax TypedLocal ::= TypedValue | MovedLocal | NewLocal - syntax TypedValue ::= typedValue ( Value , MaybeTy , Mutability ) + syntax TypedValue ::= typedValue ( Value , MaybeTy , Mutability ) [symbol(typedValue)] syntax MovedLocal ::= "Moved" - syntax NewLocal ::= newLocal ( Ty , Mutability ) + syntax NewLocal ::= newLocal ( Ty , Mutability ) [symbol(newLocal)] // the type of aggregates cannot be determined from the data provided when they // occur as `RValue`, therefore we have to make the `Ty` field optional here. diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 4f3c644ee..43b5414e7 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -8,7 +8,7 @@ from pyk.cterm import CTerm, cterm_symbolic from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, Subst from pyk.kast.manip import split_config_from -from pyk.kast.prelude.collections import list_empty, map_empty +from pyk.kast.prelude.collections import list_empty, list_of, map_empty from pyk.kast.prelude.string import stringToken from pyk.kcfg import KCFG from pyk.kcfg.explore import KCFGExplore @@ -20,7 +20,7 @@ from pyk.proof.show import APRProofNodePrinter from .cargo import cargo_get_smir_json -from .kast import mk_call_terminator +from .kast import mk_call_terminator, symbolic_locals from .kparse import KParse from .parse.parser import Parser @@ -87,10 +87,15 @@ def make_call_config( _sym, _allocs, functions, items, types, _ = parsed_smir.args + args_info = smir_info.function_arguments[start_symbol] + + locals, constraints = symbolic_locals(smir_info, args_info) + subst = { - 'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], 0), + 'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)), 'STARTSYMBOL_CELL': KApply('symbol(_)_LIB_Symbol_String', (stringToken(start_symbol),)), 'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack + 'LOCALS_CELL': list_of(locals), 'FUNCTIONS_CELL': KApply( 'mkFunctionMap', ( diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 7108a1b7c..ae1bbbf8a 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -48,7 +48,7 @@ def items(self) -> dict[str, dict]: return {_item['symbol_name']: _item for _item in self._smir['items']} @cached_property - def function_arguments(self) -> dict[str, dict]: + def function_arguments(self) -> dict[str, list[dict]]: res = {} for item in self._smir['items']: if not SMIRInfo._is_func(item): From 31d8feaf6ef18109e82d5045280c7bead9283b20 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 2 May 2025 14:47:29 -0500 Subject: [PATCH 10/31] Converting type information from SMIR to kast --- kmir/src/kmir/smir.py | 79 +++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 77 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index ae1bbbf8a..8bd18ec4f 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -1,13 +1,20 @@ from __future__ import annotations import json +from dataclasses import dataclass +from enum import Enum from functools import cached_property from typing import TYPE_CHECKING, NewType +from kmir.kast import bool_var, int_var + if TYPE_CHECKING: + from collections.abc import Iterable from pathlib import Path from typing import Any + from pyk.kast.inner import KInner + Ty = NewType('Ty', int) AdtDef = NewType('AdtDef', int) @@ -91,5 +98,73 @@ def function_tys(self) -> dict[str, int]: def _is_func(item: dict[str, dict]) -> bool: return 'MonoItemFn' in item['mono_item_kind'] - # TODO (does this go here?) - # def ty_as_kast(self, ty: Ty) -> KInner + def var_from_ty(self, ty: Ty, varname: str) -> tuple[KInner, Iterable[KInner]]: + typeinfo = self.types[ty] + type_metadata = _metadata_from_json(typeinfo) + match type_metadata: + case Int(info): + width = info.value + return int_var(varname, width, True) + case Uint(info): + width = info.value + return int_var(varname, width, False) + case Bool(): + return bool_var(varname) + case _: + return NotImplemented + + +class IntTy(Enum): + I8 = 1 + I16 = 2 + I32 = 4 + I64 = 8 + Isize = 8 + + +class UintTy(Enum): + U8 = 1 + U16 = 2 + U32 = 4 + U64 = 8 + Usize = 8 + + +@dataclass +class TypeMetadata: ... + + +@dataclass +class RigidTy(TypeMetadata): ... + + +@dataclass +class Bool(RigidTy): ... + + +@dataclass +class Int(RigidTy): + info: IntTy + + +@dataclass +class Uint(RigidTy): + info: UintTy + + +def _rigidty_from_json(typeinfo: str | dict) -> RigidTy: + if typeinfo == 'Bool': + return Bool() + + assert isinstance(typeinfo, dict) + if 'UInt' in typeinfo: + return Uint(UintTy.__members__[typeinfo['UInt']]) + if 'Int' in typeinfo: + return Int(IntTy.__members__[typeinfo['Int']]) + return NotImplemented + + +def _metadata_from_json(typeinfo: dict) -> TypeMetadata: + if 'PrimitiveType' in typeinfo: + return _rigidty_from_json(typeinfo['PrimitiveType']) + return NotImplemented From e87794d1c75b56e98a5b7305f9857506fc6e3577 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 14:51:58 +1000 Subject: [PATCH 11/31] WIP type metadata in python --- kmir/src/kmir/smir.py | 128 +++++++++++++++++++++++++++++++++--------- 1 file changed, 102 insertions(+), 26 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 8bd18ec4f..09dc3f2c6 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -6,15 +6,10 @@ from functools import cached_property from typing import TYPE_CHECKING, NewType -from kmir.kast import bool_var, int_var - if TYPE_CHECKING: - from collections.abc import Iterable from pathlib import Path from typing import Any - from pyk.kast.inner import KInner - Ty = NewType('Ty', int) AdtDef = NewType('AdtDef', int) @@ -98,21 +93,6 @@ def function_tys(self) -> dict[str, int]: def _is_func(item: dict[str, dict]) -> bool: return 'MonoItemFn' in item['mono_item_kind'] - def var_from_ty(self, ty: Ty, varname: str) -> tuple[KInner, Iterable[KInner]]: - typeinfo = self.types[ty] - type_metadata = _metadata_from_json(typeinfo) - match type_metadata: - case Int(info): - width = info.value - return int_var(varname, width, True) - case Uint(info): - width = info.value - return int_var(varname, width, False) - case Bool(): - return bool_var(varname) - case _: - return NotImplemented - class IntTy(Enum): I8 = 1 @@ -130,41 +110,137 @@ class UintTy(Enum): Usize = 8 +class FloatTy(Enum): + F16 = 2 + F32 = 4 + F64 = 8 + F128 = 16 + + @dataclass class TypeMetadata: ... @dataclass -class RigidTy(TypeMetadata): ... +class PrimitiveType(TypeMetadata): ... + + +@dataclass +class Bool(PrimitiveType): ... + + +@dataclass +class Char(PrimitiveType): ... @dataclass -class Bool(RigidTy): ... +class Str(PrimitiveType): ... @dataclass -class Int(RigidTy): +class Float(PrimitiveType): + info: FloatTy + + +@dataclass +class Int(PrimitiveType): info: IntTy @dataclass -class Uint(RigidTy): +class Uint(PrimitiveType): info: UintTy -def _rigidty_from_json(typeinfo: str | dict) -> RigidTy: +def _primty_from_json(typeinfo: str | dict) -> PrimitiveType: if typeinfo == 'Bool': return Bool() + elif typeinfo == 'Char': + return Char() + elif typeinfo == 'Str': + return Str() assert isinstance(typeinfo, dict) if 'UInt' in typeinfo: return Uint(UintTy.__members__[typeinfo['UInt']]) if 'Int' in typeinfo: return Int(IntTy.__members__[typeinfo['Int']]) + if 'Float' in typeinfo: + return Float(FloatTy.__members__[typeinfo['Float']]) return NotImplemented +@dataclass +class EnumT(TypeMetadata): + name: str + adt_def: int + discriminants: dict + + +@dataclass +class StructT(TypeMetadata): + name: str + adt_def: int + + +@dataclass +class UnionT(TypeMetadata): + name: str + adt_def: int + + +@dataclass +class ArrayT(TypeMetadata): + element_type: Ty # TypeMetadata + length: int | None + + +@dataclass +class PtrT(TypeMetadata): + pointee_type: Ty # TypeMetadata + + +@dataclass +class RefT(TypeMetadata): + pointee_type: Ty # TypeMetadata + + +@dataclass +class TupleT(TypeMetadata): + components: list[Ty] # TypeMetadata] + + +@dataclass +class FunT(TypeMetadata): + type_str: str + + def _metadata_from_json(typeinfo: dict) -> TypeMetadata: if 'PrimitiveType' in typeinfo: - return _rigidty_from_json(typeinfo['PrimitiveType']) + return _primty_from_json(typeinfo['PrimitiveType']) + elif 'EnumType' in typeinfo: + info = typeinfo['EnumType'] + discriminants = dict(info['discriminants']) + return EnumT(name=info['name'], adt_def=info['adt_def'], discriminants=discriminants) + elif 'StructType' in typeinfo: + return StructT(typeinfo['StructType']['name'], typeinfo['StructType']['adt_def']) + elif 'UnionType' in typeinfo: + return UnionT(typeinfo['UnionType']['name'], typeinfo['UnionType']['adt_def']) + + # TODO recursively produce metadata. Migrate into SMIRInfo class for that + elif 'ArrayType' in typeinfo: + info = typeinfo['ArrayType'] + assert isinstance(info, list) + # TODO decode array length from TyConst bytes + length = None # if info[1] is None else decode(info[1]['kind']['Value'][1]['bytes']) + return ArrayT(info[0], length) + elif 'PtrType' in typeinfo: + return PtrT(typeinfo['PtrType']) + elif 'RefType' in typeinfo: + return RefT(typeinfo['RefType']) + elif 'TupleType' in typeinfo: + return TupleT(typeinfo['TupleType']['types']) + elif 'FunType' in typeinfo: + return FunT(typeinfo['FunType']) + return NotImplemented From 8d4f156aa938548f7e0a81b10d87c3483ae25eb2 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 16:46:43 +1000 Subject: [PATCH 12/31] more WIP type metadata in python --- kmir/src/kmir/kast.py | 20 +++++++++++++------- kmir/src/kmir/smir.py | 35 ++++++++++++++--------------------- 2 files changed, 27 insertions(+), 28 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 3d49108a8..eb504ecc9 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -6,6 +6,8 @@ from pyk.kast.prelude.kint import leInt from pyk.kast.prelude.utils import token +from .smir import Int, Uint + if TYPE_CHECKING: from collections.abc import Iterable @@ -14,8 +16,7 @@ from .smir import SMIRInfo -def int_var(varname: str, num_bytes: int, signed: bool) -> tuple[KInner, Iterable[KInner]]: - var = KVariable(varname, 'Int') +def int_var(var: KVariable, num_bytes: int, signed: bool) -> tuple[KInner, Iterable[KInner]]: bit_width = num_bytes * 8 var_max = ((1 << (bit_width - 1)) if signed else (1 << bit_width)) - 1 var_min = -(1 << (bit_width - 1)) if signed else 0 @@ -131,13 +132,18 @@ def run(self, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]: def _add_local(self, ty: Ty) -> None: match self.smir_info.types.get(ty): + case Int(info): + value, constraints = int_var(self._fresh_var('ARG_INT'), info.value, True) + case Uint(info): + value, constraints = int_var(self._fresh_var('ARG_UINT'), info.value, False) case _: - new = KApply( - 'typedValue', (self._fresh_var('ARG'), KApply('ty', (token(ty),)), KApply('Mutability::Not', ())) - ) - self.locals.append(new) + value = self._fresh_var('ARG') + constraints = [] + + self.locals.append(KApply('typedValue', (value, KApply('ty', (token(ty),)), KApply('Mutability::Not', ())))) + self.constraints += constraints - def _fresh_var(self, prefix: str) -> KInner: + def _fresh_var(self, prefix: str) -> KVariable: name = prefix + str(self.counter) self.counter += 1 return KVariable(name) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 09dc3f2c6..af2066c14 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -8,13 +8,10 @@ if TYPE_CHECKING: from pathlib import Path - from typing import Any Ty = NewType('Ty', int) AdtDef = NewType('AdtDef', int) -# TODO: Named tuples w/ `from_dict` and helpers to create K terms - class SMIRInfo: _smir: dict @@ -27,22 +24,20 @@ def from_file(smir_json_file: Path) -> SMIRInfo: return SMIRInfo(json.loads(smir_json_file.read_text())) @cached_property - def types(self) -> dict[Ty, Any]: - res = {} - for id, type in self._smir['types']: - res[Ty(id)] = type - return res + def types(self) -> dict[Ty, TypeMetadata]: + return {Ty(id): metadata_from_json(type) for id, type in self._smir['types']} @cached_property def adt_defs(self) -> dict[AdtDef, Ty]: res = {} for ty, typeinfo in self.types.items(): - if 'StructType' in typeinfo: - adt_def = typeinfo['StructType']['adt_def'] - res[AdtDef(adt_def)] = ty - if 'EnumType' in typeinfo: - adt_def = typeinfo['EnumType']['adt_def'] - res[AdtDef(adt_def)] = ty + match typeinfo: + case StructT(adt_def=adt_def): + res[AdtDef(adt_def)] = ty + case EnumT(adt_def=adt_def): + res[AdtDef(adt_def)] = ty + case UnionT(adt_def=adt_def): + res[AdtDef(adt_def)] = ty return res @cached_property @@ -191,23 +186,23 @@ class UnionT(TypeMetadata): @dataclass class ArrayT(TypeMetadata): - element_type: Ty # TypeMetadata + element_type: Ty length: int | None @dataclass class PtrT(TypeMetadata): - pointee_type: Ty # TypeMetadata + pointee_type: Ty @dataclass class RefT(TypeMetadata): - pointee_type: Ty # TypeMetadata + pointee_type: Ty @dataclass class TupleT(TypeMetadata): - components: list[Ty] # TypeMetadata] + components: list[Ty] @dataclass @@ -215,7 +210,7 @@ class FunT(TypeMetadata): type_str: str -def _metadata_from_json(typeinfo: dict) -> TypeMetadata: +def metadata_from_json(typeinfo: dict) -> TypeMetadata: if 'PrimitiveType' in typeinfo: return _primty_from_json(typeinfo['PrimitiveType']) elif 'EnumType' in typeinfo: @@ -226,8 +221,6 @@ def _metadata_from_json(typeinfo: dict) -> TypeMetadata: return StructT(typeinfo['StructType']['name'], typeinfo['StructType']['adt_def']) elif 'UnionType' in typeinfo: return UnionT(typeinfo['UnionType']['name'], typeinfo['UnionType']['adt_def']) - - # TODO recursively produce metadata. Migrate into SMIRInfo class for that elif 'ArrayType' in typeinfo: info = typeinfo['ArrayType'] assert isinstance(info, list) From 55b3174e701eadaa58e156ca41d058e704b947aa Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 19:23:36 +1000 Subject: [PATCH 13/31] typo --- kmir/src/kmir/smir.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index af2066c14..24e87ddb1 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -156,8 +156,8 @@ def _primty_from_json(typeinfo: str | dict) -> PrimitiveType: return Str() assert isinstance(typeinfo, dict) - if 'UInt' in typeinfo: - return Uint(UintTy.__members__[typeinfo['UInt']]) + if 'Uint' in typeinfo: + return Uint(UintTy.__members__[typeinfo['Uint']]) if 'Int' in typeinfo: return Int(IntTy.__members__[typeinfo['Int']]) if 'Float' in typeinfo: From 236133ab74107b22ea78bdc1ac51018d20d1edd9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 20:59:34 +1000 Subject: [PATCH 14/31] use generated call config in prove-rs and gen-spec. Successful proof tests passing --- kmir/src/kmir/__main__.py | 6 +++++- kmir/src/kmir/kmir.py | 33 +++++++++++++++++++-------------- 2 files changed, 24 insertions(+), 15 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 99b829361..7bc1d682e 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -77,7 +77,11 @@ def _kmir_gen_spec(opts: GenSpecOpts) -> None: kmir_kast, _ = parse_result apr_proof = kmir.apr_proof_from_kast( - str(opts.input_file.stem.replace('_', '-')), kmir_kast, start_symbol=opts.start_symbol, sort='KmirCell' + str(opts.input_file.stem.replace('_', '-')), + kmir_kast, + SMIRInfo.from_file(opts.input_file), + start_symbol=opts.start_symbol, + sort='KmirCell', ) claim = apr_proof.as_claim() diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 43b5414e7..de292b59a 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -6,8 +6,8 @@ from pyk.cli.utils import bug_report_arg from pyk.cterm import CTerm, cterm_symbolic -from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, Subst -from pyk.kast.manip import split_config_from +from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, KVariable, Subst +from pyk.kast.manip import abstract_term_safely, split_config_from from pyk.kast.prelude.collections import list_empty, list_of, map_empty from pyk.kast.prelude.string import stringToken from pyk.kcfg import KCFG @@ -23,6 +23,7 @@ from .kast import mk_call_terminator, symbolic_locals from .kparse import KParse from .parse.parser import Parser +from .smir import SMIRInfo if TYPE_CHECKING: from collections.abc import Iterator @@ -33,7 +34,6 @@ from pyk.utils import BugReport from .options import ProveRSOpts - from .smir import SMIRInfo _LOGGER: Final = logging.getLogger(__name__) @@ -80,7 +80,8 @@ def make_call_config( parsed_smir: KApply, smir_info: SMIRInfo, start_symbol: str = 'main', - ) -> KInner: + sort: str = 'GeneratedTopCell' + ) -> tuple[KInner, list[KInner]]: if not start_symbol in smir_info.function_tys: raise KeyError(f'{start_symbol} not found in program') @@ -119,9 +120,9 @@ def make_call_config( ), } - config = self.definition.empty_config(KSort('GeneratedTopCell')) + config = self.definition.empty_config(KSort(sort)) - return Subst(subst).apply(config) + return (Subst(subst).apply(config), constraints) def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', depth: int | None = None) -> Pattern: init_config = self.make_init_config(parsed_smir, start_symbol) @@ -133,7 +134,7 @@ def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', d def run_call( self, parsed_smir: KApply, smir_json: SMIRInfo, start_symbol: str = 'main', depth: int | None = None ) -> Pattern: - init_config = self.make_call_config(parsed_smir, smir_json, start_symbol) + init_config, _ = self.make_call_config(parsed_smir, smir_json, start_symbol) init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell')) result = self.run_pattern(init_kore, depth=depth) @@ -143,17 +144,21 @@ def apr_proof_from_kast( self, id: str, kmir_kast: KInner, + smir_info: SMIRInfo, start_symbol: str = 'main', sort: str = 'GeneratedTopCell', proof_dir: Path | None = None, ) -> APRProof: - config = self.make_init_config(kmir_kast, start_symbol, sort=sort) - config_with_cell_vars, _ = split_config_from(config) + assert type(kmir_kast) is KApply + lhs_config, constraints = self.make_call_config(kmir_kast, smir_info, sort=sort) + lhs = CTerm(lhs_config, constraints) - lhs = CTerm(config) - - rhs_subst = Subst({'K_CELL': KMIR.Symbols.END_PROGRAM}) - rhs = CTerm(rhs_subst(config_with_cell_vars)) + var_config, var_subst = split_config_from(lhs_config) + _rhs_subst: dict[str, KInner] = { + v_name: abstract_term_safely(KVariable('_'), base_name=v_name) for v_name in var_subst + } + _rhs_subst['K_CELL'] = KSequence([KMIR.Symbols.END_PROGRAM]) + rhs = CTerm(Subst(_rhs_subst)(var_config)) kcfg = KCFG() init_node = kcfg.create_node(lhs) target_node = kcfg.create_node(rhs) @@ -176,7 +181,7 @@ def prove_rs(self, opts: ProveRSOpts) -> APRProof: kmir_kast, _ = parse_result assert isinstance(kmir_kast, KInner) apr_proof = self.apr_proof_from_kast( - label, kmir_kast, start_symbol=opts.start_symbol, proof_dir=opts.proof_dir + label, kmir_kast, SMIRInfo(smir_json), start_symbol=opts.start_symbol, proof_dir=opts.proof_dir ) if apr_proof.passed: return apr_proof From 26f92d7ada9783d34a56c421ffa8cdc225d27bb8 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 21:02:02 +1000 Subject: [PATCH 15/31] format --- kmir/src/kmir/kmir.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index de292b59a..c6c793b69 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -76,11 +76,7 @@ def make_init_config( return init_config def make_call_config( - self, - parsed_smir: KApply, - smir_info: SMIRInfo, - start_symbol: str = 'main', - sort: str = 'GeneratedTopCell' + self, parsed_smir: KApply, smir_info: SMIRInfo, start_symbol: str = 'main', sort: str = 'GeneratedTopCell' ) -> tuple[KInner, list[KInner]]: if not start_symbol in smir_info.function_tys: From 5bac823dbb0cd1bce5f7348a3a6180d766f702a8 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 21:04:54 +1000 Subject: [PATCH 16/31] Revert "REVERT ME: run with call-config when using haskell backend. BREAKS TESTS" This reverts commit 9e44a4cd3c5918b8af91e9ff31efde988bf20636. Left the `run_call` function in place as it may be useful at some point. --- kmir/src/kmir/__main__.py | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 7bc1d682e..9ba731824 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -7,7 +7,6 @@ from typing import TYPE_CHECKING from pyk.cli.args import KCLIArgs -from pyk.kast.inner import KApply from pyk.kast.outer import KFlatModule, KImport from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofShow @@ -48,14 +47,7 @@ def _kmir_run(opts: RunOpts) -> None: sys.exit(1) kmir_kast, _ = parse_result - if opts.haskell_backend: - smir_json = SMIRInfo.from_file(smir_file) - assert type(kmir_kast) is KApply - - result = kmir.run_call(kmir_kast, smir_json, opts.start_symbol, opts.depth) - else: - result = kmir.run_parsed(kmir_kast, opts.start_symbol, opts.depth) - + result = kmir.run_parsed(kmir_kast, opts.start_symbol, opts.depth) print(kmir.kore_to_pretty(result)) From 91ec123bc1980b4993166c9d731f1f7793585c17 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 21:26:48 +1000 Subject: [PATCH 17/31] adjust prove-show test expectations, use new local symbol --- .../data/prove-rs/show/assert_eq_exp-fail.expected | 9 ++++----- .../integration/data/prove-rs/show/bitwise-fail.expected | 9 ++++----- .../data/prove-rs/show/interior-mut-fail.expected | 9 ++++----- .../data/prove-rs/show/interior-mut2-fail.expected | 9 ++++----- .../data/prove-rs/show/interior-mut3-fail.expected | 9 ++++----- .../data/prove-rs/show/local-raw-fail.expected | 9 ++++----- kmir/src/tests/integration/test_integration.py | 6 +++--- 7 files changed, 27 insertions(+), 33 deletions(-) diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected index 7ecce8811..a7fc7dd0b 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected @@ -1,10 +1,9 @@ ┌─ 1 (root, init) -│ #init ( symbol ( "assert_eq_exp_fail" ) globalAllocEntry ( 0 , Memory ( allocati -│ function: main -│ span: 93 +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 │ -│ (88 steps) +│ (89 steps) └─ 3 (stuck, leaf) #readProjection ( typedValue ( Any , ty ( 25 ) , mutabilityNot ) , projectionEle function: main @@ -12,6 +11,6 @@ ┌─ 2 (root, leaf, target, terminal) -│ #EndProgram +│ #EndProgram ~> .K diff --git a/kmir/src/tests/integration/data/prove-rs/show/bitwise-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/bitwise-fail.expected index 8c1504b1f..d2a9ce886 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/bitwise-fail.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/bitwise-fail.expected @@ -1,16 +1,15 @@ ┌─ 1 (root, init) -│ #init ( symbol ( "bitwise_fail" ) globalAllocEntry ( 5 , Memory ( allocation ( . -│ function: main -│ span: 68 +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 │ -│ (30 steps) +│ (31 steps) └─ 3 (stuck, leaf) #compute ( binOpBitAnd , typedValue ( Integer ( 3 , 32 , true ) , ty ( 16 ) , mu span: 50 ┌─ 2 (root, leaf, target, terminal) -│ #EndProgram +│ #EndProgram ~> .K diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected index 9f8318b70..225c8181f 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.expected @@ -1,16 +1,15 @@ ┌─ 1 (root, init) -│ #init ( symbol ( "interior_mut_fail" ) globalAllocEntry ( 2 , Memory ( allocatio -│ function: main -│ span: 288 +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 │ -│ (138 steps) +│ (139 steps) └─ 3 (stuck, leaf) rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p span: 88 ┌─ 2 (root, leaf, target, terminal) -│ #EndProgram +│ #EndProgram ~> .K diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected index ef75df1fd..fd57ee0e5 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.expected @@ -1,16 +1,15 @@ ┌─ 1 (root, init) -│ #init ( symbol ( "interior_mut2_fail" ) globalAllocEntry ( 1 , Memory ( allocati -│ function: main -│ span: 120 +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 │ -│ (129 steps) +│ (130 steps) └─ 3 (stuck, leaf) rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p span: 50 ┌─ 2 (root, leaf, target, terminal) -│ #EndProgram +│ #EndProgram ~> .K diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected index 7cdfd662c..96a166788 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected @@ -1,16 +1,15 @@ ┌─ 1 (root, init) -│ #init ( symbol ( "interior_mut3_fail" ) globalAllocEntry ( 1 , Memory ( allocati -│ function: main -│ span: 67 +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 │ -│ (48 steps) +│ (49 steps) └─ 3 (stuck, leaf) rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p span: 52 ┌─ 2 (root, leaf, target, terminal) -│ #EndProgram +│ #EndProgram ~> .K diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.expected index 944e1fbfa..a90bc0629 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.expected @@ -1,10 +1,9 @@ ┌─ 1 (root, init) -│ #init ( symbol ( "local_raw_fail" ) .GlobalAllocs ListItem ( functionName ( ty ( -│ function: main -│ span: 51 +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 │ -│ (19 steps) +│ (20 steps) └─ 3 (stuck, leaf) rvalueAddressOf ( mutabilityMut , place ( ... local: local ( 3 ) , projection: p function: main @@ -12,6 +11,6 @@ ┌─ 2 (root, leaf, target, terminal) -│ #EndProgram +│ #EndProgram ~> .K diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d1bc8142e..7d01b9043 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -112,10 +112,10 @@ def test_schema_parse(test_dir: Path, kmir: KMIR) -> None: ] LOCAL_DECL_TESTS = [ - (2, KApply('local(_)_BODY_Local_Int', (KToken('2', KSort('Int')))), KSort('Local')), + (2, KApply('local', (KToken('2', KSort('Int')))), KSort('Local')), ( {'StorageLive': 2}, - KApply('StatementKind::StorageLive', (KApply('local(_)_BODY_Local_Int', (KToken('2', KSort('Int')))))), + KApply('StatementKind::StorageLive', (KApply('local', (KToken('2', KSort('Int')))))), KSort('StatementKind'), ), ('Not', KApply('Mutability::Not', ()), KSort('Mutability')), @@ -216,7 +216,7 @@ def test_schema_parse(test_dir: Path, kmir: KMIR) -> None: KApply( 'statement(_,_)_BODY_Statement_StatementKind_Span', ( - KApply('StatementKind::StorageLive', (KApply('local(_)_BODY_Local_Int', (KToken('42', KSort('Int')))))), + KApply('StatementKind::StorageLive', (KApply('local', (KToken('42', KSort('Int')))))), KApply('span', (KToken('1', KSort('Int')))), ), ), From 57b5013e4cb61aaa0410d3c04ba864f81198c513 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 13 May 2025 22:20:14 +1000 Subject: [PATCH 18/31] add more cases for structured symbolic locals generation --- kmir/src/kmir/kast.py | 83 +++++++++++++++++++++---- kmir/src/kmir/kdist/mir-semantics/ty.md | 2 +- 2 files changed, 73 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index eb504ecc9..06a301de4 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -3,10 +3,11 @@ from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KVariable +from pyk.kast.prelude.collections import list_of from pyk.kast.prelude.kint import leInt from pyk.kast.prelude.utils import token -from .smir import Int, Uint +from .smir import ArrayT, Bool, EnumT, Int, RefT, StructT, TupleT, Uint, UnionT if TYPE_CHECKING: from collections.abc import Iterable @@ -25,8 +26,7 @@ def int_var(var: KVariable, num_bytes: int, signed: bool) -> tuple[KInner, Itera return term, constraints -def bool_var(varname: str) -> tuple[KInner, Iterable[KInner]]: - var = KVariable(varname, 'Bool') +def bool_var(var: KVariable) -> tuple[KInner, Iterable[KInner]]: term = KApply('Value::BoolVal', (var,)) return term, () @@ -131,14 +131,7 @@ def run(self, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]: return (self.locals + self.pointees, self.constraints) def _add_local(self, ty: Ty) -> None: - match self.smir_info.types.get(ty): - case Int(info): - value, constraints = int_var(self._fresh_var('ARG_INT'), info.value, True) - case Uint(info): - value, constraints = int_var(self._fresh_var('ARG_UINT'), info.value, False) - case _: - value = self._fresh_var('ARG') - constraints = [] + value, constraints = self._symbolic_typed_value(ty) self.locals.append(KApply('typedValue', (value, KApply('ty', (token(ty),)), KApply('Mutability::Not', ())))) self.constraints += constraints @@ -147,3 +140,71 @@ def _fresh_var(self, prefix: str) -> KVariable: name = prefix + str(self.counter) self.counter += 1 return KVariable(name) + + def _symbolic_typed_value(self, ty: Ty) -> tuple[KInner, Iterable[KInner]]: + match self.smir_info.types.get(ty): + case Int(info): + return int_var(self._fresh_var('ARG_INT'), info.value, True) + + case Uint(info): + return int_var(self._fresh_var('ARG_UINT'), info.value, False) + + case Bool(): + return bool_var(self._fresh_var('ARG_UINT')) + + case EnumT(): + variantVar = self._fresh_var('ARG_VARIDX') + args = self._fresh_var('ENUM_ARGS') + return KApply('Value::Aggregate', (KApply('variantIdx', (variantVar,)), args)), [] + + case StructT(): + args = self._fresh_var('STRUCT_ARGS') + return KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)), [] + + case UnionT(): + args = self._fresh_var('ARG_UNION') + return KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), args)), [] + + case ArrayT(_, None): + elems = self._fresh_var('ARG_ARRAY') + return KApply('Value::Range', (elems,)), [] + + case ArrayT(element_type, size) if size is not None: + elem_vars: list[KInner] = [] + elem_constraints: list[KInner] = [] + for _ in range(size): + new_var, new_constraints = self._symbolic_typed_value(element_type) + elem_vars.append(new_var) + elem_constraints += new_constraints + return KApply('Value::Range', (list_of(elem_vars),)), elem_constraints + + case TupleT(components): + elem_vars = [] + elem_constraints = [] + for _ty in components: + new_var, new_constraints = self._symbolic_typed_value(_ty) + elem_vars.append(new_var) + elem_constraints += new_constraints + return ( + KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), list_of(elem_vars))), + elem_constraints, + ) + + case RefT(pointee_ty): + pointee_var, pointee_constraints = self._symbolic_typed_value(pointee_ty) + ref = self.ref_offset + self.ref_offset += 1 + self.pointees.append(pointee_var) + return ( + KApply( + 'Value::Reference', + ( + token(0), + KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))), + KApply('Mutability::Not', ()), + ), + ), + pointee_constraints, + ) + case _: + return self._fresh_var('ARG'), [] diff --git a/kmir/src/kmir/kdist/mir-semantics/ty.md b/kmir/src/kmir/kdist/mir-semantics/ty.md index 691bd13bf..76ed5237b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/ty.md +++ b/kmir/src/kmir/kdist/mir-semantics/ty.md @@ -71,7 +71,7 @@ syntax ParamDef ::= paramDef(Int) [group(mir-int)] // impo syntax RegionDef ::= regionDef(Int) [group(mir-int)] // imported from crate syntax TraitDef ::= traitDef(Int) [group(mir-int)] // imported from crate -syntax VariantIdx ::= variantIdx(Int) [group(mir-int)] +syntax VariantIdx ::= variantIdx(Int) [group(mir-int), symbol(variantIdx)] syntax DynKind ::= "dynKindDyn" [group(mir-enum), symbol(DynKind::Dyn)] | "dynKindDynStar" [group(mir-enum), symbol(DynKind::DynStar)] From c627164468b7fdd01097e7fb53d86db0ee12d5ea Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 13 May 2025 12:28:09 +0000 Subject: [PATCH 19/31] Set Version: 0.3.161 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 2a4dc0720..61f7443b5 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.160" +version = "0.3.161" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 9b333fa8a..2b9674c0a 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.160' +VERSION: Final = '0.3.161' diff --git a/kmir/uv.lock b/kmir/uv.lock index 94a602785..3b0b6bc0b 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.160" +version = "0.3.161" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index 22b94d281..a8b928366 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.160 +0.3.161 From 43a169ebb096294611d625d704f965a5dd183bfc Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 13 May 2025 15:01:58 -0500 Subject: [PATCH 20/31] Fixes for prove-rs and gen-spec --- kmir/src/kmir/kast.py | 3 ++- kmir/src/kmir/kmir.py | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 06a301de4..a3d771970 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -5,6 +5,7 @@ from pyk.kast.inner import KApply, KVariable from pyk.kast.prelude.collections import list_of from pyk.kast.prelude.kint import leInt +from pyk.kast.prelude.ml import mlEqualsTrue from pyk.kast.prelude.utils import token from .smir import ArrayT, Bool, EnumT, Int, RefT, StructT, TupleT, Uint, UnionT @@ -21,7 +22,7 @@ def int_var(var: KVariable, num_bytes: int, signed: bool) -> tuple[KInner, Itera bit_width = num_bytes * 8 var_max = ((1 << (bit_width - 1)) if signed else (1 << bit_width)) - 1 var_min = -(1 << (bit_width - 1)) if signed else 0 - constraints = (leInt(var, token(var_max)), leInt(token(var_min), var)) + constraints = (mlEqualsTrue(leInt(var, token(var_max))), mlEqualsTrue(leInt(token(var_min), var))) term = KApply('Value::Integer', (var, token(bit_width), token(signed))) return term, constraints diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index c6c793b69..bb1fd14c7 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -146,7 +146,7 @@ def apr_proof_from_kast( proof_dir: Path | None = None, ) -> APRProof: assert type(kmir_kast) is KApply - lhs_config, constraints = self.make_call_config(kmir_kast, smir_info, sort=sort) + lhs_config, constraints = self.make_call_config(kmir_kast, smir_info, start_symbol=start_symbol, sort=sort) lhs = CTerm(lhs_config, constraints) var_config, var_subst = split_config_from(lhs_config) From f9ee26ebd5b63cfc4d7479c3048597bc6b5e09fb Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 13 May 2025 15:21:34 -0500 Subject: [PATCH 21/31] Fix missing integer widths --- kmir/src/kmir/smir.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 24e87ddb1..3d18195c6 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -94,6 +94,7 @@ class IntTy(Enum): I16 = 2 I32 = 4 I64 = 8 + I128 = 16 Isize = 8 @@ -102,6 +103,7 @@ class UintTy(Enum): U16 = 2 U32 = 4 U64 = 8 + U128 = 16 Usize = 8 From 40b4424c360a5d6e60ed71b16cf26a6ce45b1aad Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 14 May 2025 10:49:14 +1000 Subject: [PATCH 22/31] use build_cons helper for operands list --- kmir/src/kmir/kast.py | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index a3d771970..a138127f1 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -2,7 +2,7 @@ from typing import TYPE_CHECKING -from pyk.kast.inner import KApply, KVariable +from pyk.kast.inner import KApply, KVariable, build_cons from pyk.kast.prelude.collections import list_of from pyk.kast.prelude.kint import leInt from pyk.kast.prelude.ml import mlEqualsTrue @@ -41,16 +41,7 @@ def mk_call_terminator(target: int, arg_count: int) -> KInner: for i in range(arg_count) ] - # args = foldr(Operands::append, Operands::empty, operands) - args = KApply('Operands::empty', ()) - for op in reversed(operands): - args = KApply( - 'Operands::append', - ( - op, - args, - ), - ) + args = build_cons(KApply('Operands::empty', ()), 'Operands::append', operands) return KApply( '#execTerminator(_)_KMIR-CONTROL-FLOW_KItem_Terminator', From a76a317587b9b8596c30da742c7cadee57e3af91 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 14 May 2025 12:22:35 +1000 Subject: [PATCH 23/31] decode array length if provided --- kmir/src/kmir/smir.py | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 3d18195c6..c04595859 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -3,7 +3,7 @@ import json from dataclasses import dataclass from enum import Enum -from functools import cached_property +from functools import cached_property, reduce from typing import TYPE_CHECKING, NewType if TYPE_CHECKING: @@ -226,8 +226,7 @@ def metadata_from_json(typeinfo: dict) -> TypeMetadata: elif 'ArrayType' in typeinfo: info = typeinfo['ArrayType'] assert isinstance(info, list) - # TODO decode array length from TyConst bytes - length = None # if info[1] is None else decode(info[1]['kind']['Value'][1]['bytes']) + length = None if info[1] is None else _decode(info[1]['kind']['Value'][1]['bytes']) return ArrayT(info[0], length) elif 'PtrType' in typeinfo: return PtrT(typeinfo['PtrType']) @@ -239,3 +238,9 @@ def metadata_from_json(typeinfo: dict) -> TypeMetadata: return FunT(typeinfo['FunType']) return NotImplemented + + +def _decode(bytes: list[int]) -> int: + # assume little-endian: reverse the bytes + bytes.reverse() + return reduce(lambda x, y: x * 256 + y, bytes) From 15ae5646fd89cd1425243feecd77c164aa558195 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 14 May 2025 14:44:18 +1000 Subject: [PATCH 24/31] create typedValues in recursion, consider mutability of the local --- kmir/src/kmir/kast.py | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index a138127f1..6081ba641 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -97,6 +97,13 @@ def symbolic_locals(smir_info: SMIRInfo, local_types: list[dict]) -> tuple[list[ return ([local0] + locals, constraints) +def _typed_value(value: KInner, ty: int, mutable: bool) -> KInner: + return KApply( + 'typedValue', + (value, KApply('ty', (token(ty),)), KApply('Mutability::Mut' if mutable else 'Mutability::Not', ())), + ) + + class ArgGenerator: smir_info: SMIRInfo locals: list[KInner] @@ -118,14 +125,14 @@ def __init__(self, smir_info: SMIRInfo) -> None: def run(self, local_types: list[dict]) -> tuple[list[KInner], list[KInner]]: self.ref_offset = len(local_types) + 1 - for ty in [t['ty'] for t in local_types]: - self._add_local(ty) + for ty, mut in [(t['ty'], t['mutability']) for t in local_types]: + self._add_local(ty, mut == 'Mut') return (self.locals + self.pointees, self.constraints) - def _add_local(self, ty: Ty) -> None: - value, constraints = self._symbolic_typed_value(ty) + def _add_local(self, ty: Ty, mutable: bool) -> None: + value, constraints = self._symbolic_value(ty, mutable) - self.locals.append(KApply('typedValue', (value, KApply('ty', (token(ty),)), KApply('Mutability::Not', ())))) + self.locals.append(_typed_value(value, ty, mutable)) self.constraints += constraints def _fresh_var(self, prefix: str) -> KVariable: @@ -133,7 +140,7 @@ def _fresh_var(self, prefix: str) -> KVariable: self.counter += 1 return KVariable(name) - def _symbolic_typed_value(self, ty: Ty) -> tuple[KInner, Iterable[KInner]]: + def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInner]]: match self.smir_info.types.get(ty): case Int(info): return int_var(self._fresh_var('ARG_INT'), info.value, True) @@ -165,8 +172,8 @@ def _symbolic_typed_value(self, ty: Ty) -> tuple[KInner, Iterable[KInner]]: elem_vars: list[KInner] = [] elem_constraints: list[KInner] = [] for _ in range(size): - new_var, new_constraints = self._symbolic_typed_value(element_type) - elem_vars.append(new_var) + new_var, new_constraints = self._symbolic_value(element_type, mutable) + elem_vars.append(_typed_value(new_var, element_type, mutable)) elem_constraints += new_constraints return KApply('Value::Range', (list_of(elem_vars),)), elem_constraints @@ -174,8 +181,8 @@ def _symbolic_typed_value(self, ty: Ty) -> tuple[KInner, Iterable[KInner]]: elem_vars = [] elem_constraints = [] for _ty in components: - new_var, new_constraints = self._symbolic_typed_value(_ty) - elem_vars.append(new_var) + new_var, new_constraints = self._symbolic_value(_ty, mutable) + elem_vars.append(_typed_value(new_var, _ty, mutable)) elem_constraints += new_constraints return ( KApply('Value::Aggregate', (KApply('variantIdx', (token(0),)), list_of(elem_vars))), @@ -183,17 +190,17 @@ def _symbolic_typed_value(self, ty: Ty) -> tuple[KInner, Iterable[KInner]]: ) case RefT(pointee_ty): - pointee_var, pointee_constraints = self._symbolic_typed_value(pointee_ty) + pointee_var, pointee_constraints = self._symbolic_value(pointee_ty, mutable) ref = self.ref_offset self.ref_offset += 1 - self.pointees.append(pointee_var) + self.pointees.append(_typed_value(pointee_var, pointee_ty, mutable)) return ( KApply( 'Value::Reference', ( token(0), KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))), - KApply('Mutability::Not', ()), + KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()), ), ), pointee_constraints, From 0939c353524282119c1ac4a73f89deeb794dc941 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 14 May 2025 05:19:09 +0000 Subject: [PATCH 25/31] Set Version: 0.3.162 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 61f7443b5..cec89ae92 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.161" +version = "0.3.162" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 2b9674c0a..679240233 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.161' +VERSION: Final = '0.3.162' diff --git a/kmir/uv.lock b/kmir/uv.lock index 3b0b6bc0b..719708d08 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.161" +version = "0.3.162" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index a8b928366..e41771856 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.161 +0.3.162 From cb3b22a00ac8ee23c41a6ba9c99f74c27f1b3566 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 14 May 2025 16:13:00 +1000 Subject: [PATCH 26/31] add test for symbolic argument generation --- .../prove-rs/show/symbolic-args-fail.expected | 39 +++++++++++++++ .../data/prove-rs/symbolic-args-fail.rs | 49 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 25 +++++----- 3 files changed, 102 insertions(+), 11 deletions(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected new file mode 100644 index 000000000..ec6c1bcd2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected @@ -0,0 +1,39 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (45 steps) +├─ 3 (split) +│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ ARG_UINT3:Bool +┃ │ +┃ ├─ 4 +┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) +┃ │ +┃ │ (65 steps) +┃ └─ 6 (stuck, leaf) +┃ #applyUnOp ( unOpPtrMetadata , typedValue ( Reference ( 0 , place ( ... local: l +┃ span: 59 +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ notBool ARG_UINT3:Bool + │ + ├─ 5 + │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) + │ + │ (16 steps) + └─ 7 (stuck, leaf) + #applyUnOp ( unOpPtrMetadata , typedValue ( Reference ( 0 , place ( ... local: l + span: 59 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs b/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs new file mode 100644 index 000000000..ffece24de --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs @@ -0,0 +1,49 @@ +// @kmir prove-rs: eats_all_args + +#[allow(dead_code)] +struct MyStruct<'a>{ field: &'a MyEnum} + +#[allow(dead_code)] +enum MyEnum { + My1, + My2(i8), +} + +#[allow(dead_code)] +#[allow(unused)] +fn eats_all_args<'a>( + x1: i32, + x2: &mut u16, + x3: bool, + mut x4: MyStruct<'a>, + x5: MyEnum, + x6: &mut [u8], + x7: &[i8; 3], + x8: &mut [MyStruct<'a>; 2] +) -> () { + *x2 = x1 as u16; + if x3 { + x8[0] = x4; + } + match x5 { + _ => { + if x6.len() > 0 + { x6[0] = x7[0] as u8; } + } + } +} + +// we need a `main` function that calls eats_all_args +fn main() { + let e1 = MyEnum::My1; + let e2 = MyEnum::My2(0); + let e3 = MyEnum::My1; + let e4 = MyEnum::My2(0); + let mut x2 = 0; + let my1 = MyStruct{field: &e1}; + let my2 = MyStruct{field: &e2}; + let my3 = MyStruct{field: &e3}; + let mut a1 = [1, 2, 3]; + let a2 = [1, 2, 3]; + eats_all_args(1, &mut x2, true, my1, e4, &mut a1, &a2, &mut [my2, my3]); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 734694b12..47f4bd442 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -435,6 +435,7 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None: 'interior-mut3-fail', 'assert_eq_exp-fail', 'bitwise-fail', + 'symbolic-args-fail', ] @@ -449,8 +450,20 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No prove_rs_opts = ProveRSOpts(rs_file) + # read start symbol(s) from the first line (default: [main] otherwise) + start_sym_prefix = '// @kmir prove-rs:' + with open(rs_file) as f: + headline = f.readline().strip('\n') + if headline.startswith(start_sym_prefix): + start_symbols = headline.removeprefix(start_sym_prefix).split() + else: + start_symbols = ['main'] + if should_show: - # always run `main` when kmir show is tested + # only run a single start symbol when kmir show is tested + assert len(start_symbols) == 1 + prove_rs_opts.start_symbol = start_symbols[0] + apr_proof = kmir.prove_rs(prove_rs_opts) if not should_fail: @@ -464,16 +477,6 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No show_res, PROVING_DIR / f'show/{rs_file.stem}.expected', update=update_expected_output ) else: - # read start symbol(s) from the first line (default: [main] otherwise) - start_sym_prefix = '// @kmir prove-rs:' - with open(rs_file) as f: - headline = f.readline().strip('\n') - - if headline.startswith(start_sym_prefix): - start_symbols = headline.removeprefix(start_sym_prefix).split() - else: - start_symbols = ['main'] - for start_symbol in start_symbols: prove_rs_opts.start_symbol = start_symbol apr_proof = kmir.prove_rs(prove_rs_opts) From cfb59d7760179092cd341182b8d342d4eee38572 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 14 May 2025 16:21:21 +1000 Subject: [PATCH 27/31] generate constraint about the enum variant index --- kmir/src/kmir/kast.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 6081ba641..3fb19c5bc 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -151,10 +151,16 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne case Bool(): return bool_var(self._fresh_var('ARG_UINT')) - case EnumT(): + case EnumT(_, _, discriminants): variantVar = self._fresh_var('ARG_VARIDX') + # constraints for variant index being in range + max_variant = max(discriminants.keys()) + idx_range = [ + mlEqualsTrue(leInt(token(0), variantVar)), + mlEqualsTrue(leInt(variantVar, token(max_variant))), + ] args = self._fresh_var('ENUM_ARGS') - return KApply('Value::Aggregate', (KApply('variantIdx', (variantVar,)), args)), [] + return KApply('Value::Aggregate', (KApply('variantIdx', (variantVar,)), args)), idx_range case StructT(): args = self._fresh_var('STRUCT_ARGS') From 29bc5f031601d394386267d23acc4992be774248 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 14 May 2025 06:31:06 +0000 Subject: [PATCH 28/31] Set Version: 0.3.162 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index d71b0983d..d338eeff7 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.161" +version = "0.3.162" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 2b9674c0a..679240233 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.161' +VERSION: Final = '0.3.162' diff --git a/kmir/uv.lock b/kmir/uv.lock index d4fb8d1bf..16c6ad2dc 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -491,7 +491,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.161" +version = "0.3.162" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index a8b928366..e41771856 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.161 +0.3.162 From c09bcd4bae37444e442b37270d59aa6f4a582e5d Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 14 May 2025 16:33:50 +1000 Subject: [PATCH 29/31] name variable prefix correctly for BOOL --- kmir/src/kmir/kast.py | 2 +- .../data/prove-rs/show/symbolic-args-fail.expected | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 3fb19c5bc..2b3bdc77e 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -149,7 +149,7 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne return int_var(self._fresh_var('ARG_UINT'), info.value, False) case Bool(): - return bool_var(self._fresh_var('ARG_UINT')) + return bool_var(self._fresh_var('ARG_BOOL')) case EnumT(_, _, discriminants): variantVar = self._fresh_var('ARG_VARIDX') diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected index ec6c1bcd2..1610e0e51 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected @@ -10,7 +10,7 @@ ┃ (branch) ┣━━┓ subst: .Subst ┃ ┃ constraint: -┃ ┃ ARG_UINT3:Bool +┃ ┃ ARG_BOOL3:Bool ┃ │ ┃ ├─ 4 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) @@ -22,7 +22,7 @@ ┃ ┗━━┓ subst: .Subst ┃ constraint: - ┃ notBool ARG_UINT3:Bool + ┃ notBool ARG_BOOL3:Bool │ ├─ 5 │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) From fb7d374280d947e45c365a60fcc1ccc5933501db Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 15 May 2025 09:47:19 +1000 Subject: [PATCH 30/31] reformatted substitution --- kmir/src/kmir/kmir.py | 24 +++--------------------- 1 file changed, 3 insertions(+), 21 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index bb1fd14c7..71cee38a0 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -93,27 +93,9 @@ def make_call_config( 'STARTSYMBOL_CELL': KApply('symbol(_)_LIB_Symbol_String', (stringToken(start_symbol),)), 'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack 'LOCALS_CELL': list_of(locals), - 'FUNCTIONS_CELL': KApply( - 'mkFunctionMap', - ( - functions, - items, - ), - ), - 'TYPES_CELL': KApply( - 'mkTypeMap', - ( - map_empty(), - types, - ), - ), - 'ADTTOTY_CELL': KApply( - 'mkAdtMap', - ( - map_empty(), - types, - ), - ), + 'FUNCTIONS_CELL': KApply('mkFunctionMap', (functions, items)), + 'TYPES_CELL': KApply('mkTypeMap', (map_empty(), types)), + 'ADTTOTY_CELL': KApply('mkAdtMap', (map_empty(), types)), } config = self.definition.empty_config(KSort(sort)) From 28e996328326c3db1595fd2307b8bc0d2b99480f Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 16 May 2025 01:19:17 +0000 Subject: [PATCH 31/31] Set Version: 0.3.164 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 6601457ea..2ad0cb394 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.163" +version = "0.3.164" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 6fff8bfbd..854795654 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.163' +VERSION: Final = '0.3.164' diff --git a/kmir/uv.lock b/kmir/uv.lock index 159fc09c6..69273ed48 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -491,7 +491,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.163" +version = "0.3.164" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index ee7ed8106..9fdf92793 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.163 +0.3.164