Avoid llvm-kompile when running proofs - rebooted

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 <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -252,7 +252,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        // remaining call stack (without top frame)
        <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => 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)
@@ -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
 

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

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,15 +115,15 @@ 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))
 // Any remaining pattern indicates a length mismatch between types and 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(

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]

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

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'
@@ -415,6 +381,7 @@ def _make_stratified_rules(
             attrs=(
                 App('function'),
                 App('total'),
+                App('no-evaluators'),  # HS backend only
             ),
         )
         for i in range(strata)