From 51ad50bc69cd8be5cdeef114a8c8afe5a42bb0a9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 16 Mar 2026 20:33:16 +1100 Subject: [PATCH 1/4] Avoid LLVM kompile: Ported previous code changes to current master * Lookup functions have `no-evaluators` attributes and no defaults - LLVM backend won't be called to evaluate expressions containing them - HS backend (booster) will evaluate * No LLVM `kompile` step before executing symbolically * Only the HS definition.kore is extended with the lookup function equations --- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 11 ++--- kmir/src/kmir/kompile.py | 42 ++----------------- 2 files changed, 7 insertions(+), 46 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index 676784869..595facf64 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -141,19 +141,14 @@ These functions are global static data accessed from many places, and will be e ```k // // function store, Ty -> MonoItemFn - syntax MonoItemKind ::= lookupFunction ( Ty ) [function, total, symbol(lookupFunction)] + syntax MonoItemKind ::= lookupFunction ( Ty ) [function, total, symbol(lookupFunction), no-evaluators] // // static allocations: AllocId -> AllocData (Value or error) - syntax Evaluation ::= lookupAlloc ( AllocId ) [function, total, symbol(lookupAlloc)] + syntax Evaluation ::= lookupAlloc ( AllocId ) [function, total, symbol(lookupAlloc), no-evaluators] | InvalidAlloc ( AllocId ) // error marker // // static information about the base type interning in the MIR: Ty -> TypeInfo - syntax TypeInfo ::= lookupTy ( Ty ) [function, total, symbol(lookupTy)] - - // default rules (unused, only required for compilation of the base semantics) - rule lookupFunction(ty(TY)) => monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(TY), noBody ) [owise] - rule lookupAlloc(ID) => InvalidAlloc(ID) [owise] - rule lookupTy(_) => typeInfoFunType(" ** INVALID LOOKUP CALL **" ) [owise] + syntax TypeInfo ::= lookupTy ( Ty ) [function, total, symbol(lookupTy), no-evaluators] ``` ```k diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 85035d4bd..d9c336d13 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -287,45 +287,11 @@ def kompile_smir( all_rules = smir_rules + extra_rules if symbolic: - # Create output directories - target_llvmdt_path = target_llvm_lib_path / 'dt' - - _LOGGER.info(f'Creating directories {target_llvmdt_path} and {target_hs_path}') - target_llvmdt_path.mkdir(parents=True, exist_ok=True) + # no llvm-kompile required, HS backend will evaluate the static data lookups + # Create output directory + _LOGGER.info(f'Creating directory {target_hs_path}') target_hs_path.mkdir(parents=True, exist_ok=True) - # Process LLVM definition (only SMIR rules, not extra module rules) - # Extra module rules are configuration rewrites that LLVM backend doesn't support - _LOGGER.info('Writing LLVM definition file') - llvm_lib_dir = kdist.which(llvm_lib_target) - llvm_def_file = llvm_lib_dir / 'definition.kore' - llvm_def_output = target_llvm_lib_path / 'definition.kore' - _insert_rules_and_write(llvm_def_file, smir_rules, llvm_def_output) - - # Run llvm-kompile-matching and llvm-kompile for LLVM - # TODO use pyk to do this if possible (subprocess wrapper, maybe llvm-kompile itself?) - # TODO align compilation options to what we use in plugin.py - import subprocess - - _LOGGER.info('Running llvm-kompile-matching') - subprocess.run( - ['llvm-kompile-matching', str(llvm_def_output), 'qbaL', str(target_llvmdt_path), '1/2'], check=True - ) - _LOGGER.info('Running llvm-kompile') - subprocess.run( - [ - 'llvm-kompile', - str(llvm_def_output), - str(target_llvmdt_path), - 'c', - '-O2', - '--', - '-o', - target_llvm_lib_path / 'interpreter', - ], - check=True, - ) - # Process Haskell definition (includes both SMIR rules and extra module rules) _LOGGER.info('Writing Haskell definition file') hs_def_file = haskell_def_dir / 'definition.kore' @@ -341,7 +307,7 @@ def kompile_smir( shutil.copytree(file_path, target_hs_path / file_path.name, dirs_exist_ok=True) kompile_digest.write(target_dir) - return KompiledSymbolic(haskell_dir=target_hs_path, llvm_lib_dir=target_llvm_lib_path) + return KompiledSymbolic(haskell_dir=target_hs_path, llvm_lib_dir=kdist.which(llvm_lib_target)) else: target_llvmdt_path = target_llvm_path / 'dt' From af25ccd24de36c4b90cf2f25f26da2ccfa268da0 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sun, 26 Apr 2026 19:01:20 +1000 Subject: [PATCH 2/4] Mark stratified helper functions 'no-evaluators' to avoid LLVM backend errors --- kmir/src/kmir/kompile.py | 1 + 1 file changed, 1 insertion(+) diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index d9c336d13..b56d89511 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -381,6 +381,7 @@ def _make_stratified_rules( attrs=( App('function'), App('total'), + App('no-evaluators'), # HS backend only ), ) for i in range(strata) From c4b6dbb1280d306f847b3a28ece60d1f903d40df Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 27 Apr 2026 23:05:19 +1000 Subject: [PATCH 3/4] Annotate functions calling lookup functions as no-evaluators, transitively --- .../kmir/kdist/mir-semantics/intrinsics.md | 2 +- kmir/src/kmir/kdist/mir-semantics/kmir.md | 4 +-- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 6 ++-- .../kmir/kdist/mir-semantics/rt/decoding.md | 16 +++++----- kmir/src/kmir/kdist/mir-semantics/rt/types.md | 31 +++++++------------ 5 files changed, 26 insertions(+), 33 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index 8788d9861..c4434f6c7 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -112,7 +112,7 @@ Execution gets stuck (no matching rule) when operands have different types or un rule #withDeref(OP) => OP [owise] // Extract type from operands (locals with projections, constants, fallback to unknown) - syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total] + syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total, no-evaluators] rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS) => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) requires 0 <=Int I andBool I ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK - syntax List ::= #getBlocks( Ty ) [function, total] + syntax List ::= #getBlocks( Ty ) [function, total, no-evaluators] | #getBlocksAux( MonoItemKind ) [function, total] rule #getBlocks(TY) => #getBlocksAux(lookupFunction(TY)) @@ -324,7 +324,7 @@ where the returned result should go. requires isTy(#projectedCallTy(I, PROJS, LOCALS)) [preserves-definedness] // valid local indexing checked, projected call target must resolve to a Ty - syntax MaybeTy ::= #projectedCallTy(Int, ProjectionElems, List) [function, total] + syntax MaybeTy ::= #projectedCallTy(Int, ProjectionElems, List) [function, total, no-evaluators] rule #projectedCallTy(I, PROJS, LOCALS) => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 2cc068084..89211d3f2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1463,7 +1463,7 @@ Otherwise, compute the type projection and convert metadata accordingly. The pointer's metadata needs to be adapted to the new type. ```k - syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total] + syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total, no-evaluators] ``` Pointers to slices can be converted to pointers to single elements, _losing_ their metadata. @@ -1696,13 +1696,13 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. requires COUNT >Int 0 [preserves-definedness] - syntax Bool ::= #isStaticU8Array ( TypeInfo ) [function, total] + syntax Bool ::= #isStaticU8Array ( TypeInfo ) [function, total, no-evaluators] // ------------------------------------------------------------- rule #isStaticU8Array(typeInfoArrayType(ELEM_TY, someTyConst(_))) => lookupTy(ELEM_TY) ==K typeInfoPrimitiveType(primTypeUint(uintTyU8)) rule #isStaticU8Array(_OTHER) => false [owise] - syntax Int ::= #staticArrayLenBits ( TypeInfo ) [function, total] + syntax Int ::= #staticArrayLenBits ( TypeInfo ) [function, total, no-evaluators] // ------------------------------------------------------------- rule #staticArrayLenBits(typeInfoArrayType(_, someTyConst(tyConst(KIND, _)))) => readTyConstInt(KIND) *Int 8 diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md index 98b522012..fa040c665 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -36,7 +36,7 @@ and arrays (where layout is trivial). ### Decoding `PrimitiveType`s ```k - syntax Evaluation ::= #decodeValue ( Bytes , TypeInfo ) [function, total, symbol(decodeValue)] + syntax Evaluation ::= #decodeValue ( Bytes , TypeInfo ) [function, total, symbol(decodeValue), no-evaluators] | UnableToDecode ( Bytes , TypeInfo ) [symbol(Evaluation::UnableToDecode)] | UnableToDecodePy ( msg: String ) [symbol(Evaluation::UnableToDecodePy)] @@ -115,7 +115,7 @@ rule #msBytes(machineSize(NBITS)) => NBITS /Int 8 [owise, preserves-definedness] // Uses builtin maxInt to compute max(offset + size). The lists of types and // offsets must have the same length; if not, this function returns -1 to signal // an invalid layout for decoding. -syntax Int ::= #neededBytesForOffsets ( Tys , MachineSizes ) [function, total] +syntax Int ::= #neededBytesForOffsets ( Tys , MachineSizes ) [function, total, no-evaluators] rule #neededBytesForOffsets(.Tys, .MachineSizes) => 0 rule #neededBytesForOffsets(TY TYS, OFFSET OFFSETS) => maxInt(#msBytes(OFFSET) +Int #elemSize(lookupTy(TY)), #neededBytesForOffsets(TYS, OFFSETS)) @@ -123,7 +123,7 @@ rule #neededBytesForOffsets(TY TYS, OFFSET OFFSETS) rule #neededBytesForOffsets(_, _) => -1 [owise] // Decode each field at its byte offset and return values in declaration order. -syntax List ::= #decodeFieldsWithOffsets ( Bytes , Tys , MachineSizes ) [function, total] +syntax List ::= #decodeFieldsWithOffsets ( Bytes , Tys , MachineSizes ) [function, total, no-evaluators] rule #decodeFieldsWithOffsets(_, .Tys, _OFFSETS) => .List rule #decodeFieldsWithOffsets(_, _TYS, .MachineSizes) => .List [owise] rule #decodeFieldsWithOffsets(BYTES, TY TYS, OFFSET OFFSETS) @@ -150,7 +150,7 @@ All unimplemented cases will become thunks by way of this default rule: ```k // TODO: this function should go into the rt/types.md module - syntax Int ::= #elemSize ( TypeInfo ) [function, total] + syntax Int ::= #elemSize ( TypeInfo ) [function, total, no-evaluators] ``` Known element sizes for common types: @@ -349,7 +349,7 @@ per-variant layout offsets. // --------------------------------------------------------------------------- // #decodeEnumDirectFields: given the variant index, decode its fields // --------------------------------------------------------------------------- - syntax Evaluation ::= #decodeEnumDirectFields ( Bytes , VariantIdx , Tyss , LayoutShapes , TypeInfo ) [function, total] + syntax Evaluation ::= #decodeEnumDirectFields ( Bytes , VariantIdx , Tyss , LayoutShapes , TypeInfo ) [function, total, no-evaluators] // -------------------------------------------------------------------------------------------------------------------------- rule #decodeEnumDirectFields(BYTES, variantIdx(IDX), FIELD_TYPESS, VARIANT_LAYOUTS, _ENUM_TYPE) => Aggregate( @@ -458,13 +458,13 @@ bytes for the declared array length, the function will get stuck rather than pro results. ```k - syntax Value ::= #decodeArrayAllocation ( Bytes, TypeInfo, Int ) [function] + syntax Value ::= #decodeArrayAllocation ( Bytes, TypeInfo, Int ) [function, no-evaluators] // bytes, element type info, array length, type map (for recursion) rule #decodeArrayAllocation(BYTES, ELEMTYPEINFO, LEN) => Range(#decodeArrayElements(BYTES, ELEMTYPEINFO, LEN, .List)) - syntax List ::= #decodeArrayElements ( Bytes, TypeInfo, Int, List ) [function] + syntax List ::= #decodeArrayElements ( Bytes, TypeInfo, Int, List ) [function, no-evaluators] // bytes, elem type info, remaining length, accumulated list rule #decodeArrayElements(BYTES, _ELEMTYPEINFO, LEN, ACC) @@ -495,7 +495,7 @@ The `#decodeSliceAllocation` function computes the array length by dividing the by the element size, then uses the same element-by-element decoding approach as arrays. ```k - syntax Value ::= #decodeSliceAllocation ( Bytes, TypeInfo ) [function] + syntax Value ::= #decodeSliceAllocation ( Bytes, TypeInfo ) [function, no-evaluators] // ------------------------------------------------------------------- rule #decodeSliceAllocation(BYTES, ELEMTYPEINFO) => Range(#decodeArrayElements( diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index aaf854c13..64cef0681 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -36,7 +36,7 @@ The interface function is meant for pointer casts to compute pointee projections syntax MaybeProjectionElems ::= ProjectionElems | "NoProjectionElems" - syntax MaybeProjectionElems ::= #typeProjection ( TypeInfo , TypeInfo ) [function, total] + syntax MaybeProjectionElems ::= #typeProjection ( TypeInfo , TypeInfo ) [function, total, no-evaluators] // --------------------------------------------------------------------------------------- rule #typeProjection ( typeInfoPtrType(TY1) , typeInfoPtrType(TY2) ) => #pointeeProjection(lookupTy(TY1), lookupTy(TY2)) rule #typeProjection ( _, _ ) => NoProjectionElems [owise] @@ -82,7 +82,7 @@ and target-side rules, because a type cannot be both a struct and an array simul When the source cannot be unwrapped further, target-side unwrapping is handled by `#pointeeProjectionTarget`. ```k - syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total] + syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total, no-evaluators] ``` A short-cut rule for identical types takes preference. @@ -158,7 +158,7 @@ After one step of target unwrapping, recurse back to `#pointeeProjection` to mai the source-first strategy. ```k - syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( TypeInfo , TypeInfo ) [function, total] + syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( TypeInfo , TypeInfo ) [function, total, no-evaluators] rule #pointeeProjectionTarget(TY1, typeInfoArrayType(TY2, _)) => maybeConcatProj( @@ -217,13 +217,6 @@ To make this function total, an optional `MaybeTy` is used. requires #zeroFieldOffset(LAYOUT) rule #transparentFieldTy(_) => TyUnknown [owise] - syntax Int ::= #transparentDepth ( TypeInfo ) [function, total] - - rule #transparentDepth(typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) - => 1 +Int #transparentDepth(lookupTy(FIELD)) - requires #zeroFieldOffset(LAYOUT) - rule #transparentDepth(_) => 0 [owise] - syntax String ::= #typeName ( TypeInfo ) [function, total] // ------------------------------------------------------- rule #typeName(typeInfoUnionType(NAME, _, _, _)) => NAME @@ -257,17 +250,17 @@ To make this function total, an optional `MaybeTy` is used. rule getArrayElemTy(typeInfoArrayType(ELEM_TY, _)) => ELEM_TY rule getArrayElemTy(_) => ty(-1) [owise] - syntax TypeInfo ::= getArrayElemTypeInfo ( TypeInfo ) [function, total] + syntax TypeInfo ::= getArrayElemTypeInfo ( TypeInfo ) [function, total, no-evaluators] // -------------------------------------------------------------------- rule getArrayElemTypeInfo(typeInfoArrayType(ELEM_TY, _)) => lookupTy(ELEM_TY) rule getArrayElemTypeInfo(_) => typeInfoVoidType [owise] - syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total] + syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total, no-evaluators] // ------------------------------------------------------------- rule #lookupMaybeTy(TY:Ty) => lookupTy(TY) rule #lookupMaybeTy(TyUnknown) => typeInfoVoidType - syntax MaybeTy ::= getTyOf( MaybeTy , ProjectionElems ) [function, total] + syntax MaybeTy ::= getTyOf( MaybeTy , ProjectionElems ) [function, total, no-evaluators] // ---------------------------------------------------------------------- rule getTyOf(TyUnknown, _ ) => TyUnknown rule getTyOf(TY, .ProjectionElems ) => TY @@ -310,9 +303,9 @@ A [similar function exists in `rustc`](https://doc.rust-lang.org/nightly/nightly Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does not. ```k - syntax MetadataSize ::= #metadataSize ( Ty , ProjectionElems ) [function, total] - | #metadataSize ( MaybeTy ) [function, total] - | #metadataSizeAux ( TypeInfo ) [function, total] + syntax MetadataSize ::= #metadataSize ( Ty , ProjectionElems ) [function, total, no-evaluators] + | #metadataSize ( MaybeTy ) [function, total, no-evaluators] + | #metadataSizeAux ( TypeInfo ) [function, total, no-evaluators] // -------------------------------------------------------------------------------------- rule #metadataSize(TY, PROJS) => #metadataSize(getTyOf(TY, PROJS)) @@ -327,7 +320,7 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does ```k // reading Int-valued TyConsts from allocated bytes - syntax Int ::= readTyConstInt ( TyConstKind ) [function] + syntax Int ::= readTyConstInt ( TyConstKind ) [function, no-evaluators] // ----------------------------------------------------------- rule readTyConstInt( tyConstKindValue(TY, allocation(BYTES, _, _, _))) => Bytes2Int(BYTES, LE, Unsigned) requires isUintTy(#numTypeOf(lookupTy(TY))) @@ -362,8 +355,8 @@ The `alignOf` and `sizeOf` nullary operations return the alignment / size in byt This information is either hard-wired for primitive types (numbers, first and foremost), or read from the layout in `TypeInfo`. ```k - syntax Int ::= #sizeOf ( TypeInfo ) [function, total] - | #alignOf ( TypeInfo ) [function, total] + syntax Int ::= #sizeOf ( TypeInfo ) [function, total, no-evaluators] + | #alignOf ( TypeInfo ) [function, total, no-evaluators] // primitive int types: use bit width (both for size and alignment) rule #sizeOf(typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness] From 0c830d6802ec32e0d4b1a685d76925681a4b78d8 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 27 Apr 2026 19:36:04 +0200 Subject: [PATCH 4/4] Added missing `no-evaluators` attribute --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index a8bd595ce..c14ef496c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -379,13 +379,13 @@ where the returned result should go. rule getFunctionName(IntrinsicFunction(symbol(NAME))) => NAME // Check whether a function name matches any filter in the break-on-functions list. - syntax Bool ::= #functionNameMatchesEnv(String) [function, total] + syntax Bool ::= #functionNameMatchesEnv(String) [function, total, no-evaluators] //---------------------------------------------------------------- rule #functionNameMatchesEnv(NAME) => #functionNameMatchesEnvStr(NAME, #breakOnFunctionsString(0)) // The Int argument is unused; it exists only so the Haskell backend can // pattern-match on it and not error since zero-argument functions cannot use [owise]. - syntax String ::= #breakOnFunctionsString(Int) [function, total, symbol(breakOnFunctionsString)] + syntax String ::= #breakOnFunctionsString(Int) [function, total, symbol(breakOnFunctionsString), no-evaluators] //----------------------------------------------------------------------------------------------- rule #breakOnFunctionsString(_) => "" [owise] // This gets overridden by corresponding python function