Map cells with static data for LLVM kompile

kmir/src/kmir/kast.py

@@ -73,28 +73,37 @@ def make_call_config(
     smir_info: SMIRInfo,
     start_symbol: str,
     mode: CallConfigMode,
+    cell_maps: dict[str, KInner] | None = None,
 ) -> CallConfig:
     fn_data = _FunctionData.load(smir_info=smir_info, start_symbol=start_symbol)
     match mode:
         case ConcreteMode():
+            if cell_maps is None:
+                raise ValueError('cell_maps is required for ConcreteMode')
             config = _make_concrete_call_config(
                 definition=definition,
                 fn_data=fn_data,
+                cell_maps=cell_maps,
             )
             return CallConfig(config=config, constraints=())
         case SymbolicMode():
+            if cell_maps is not None:
+                raise ValueError('cell_maps must not be provided for SymbolicMode')
             config, constraints = _make_symbolic_call_config(
                 definition=definition,
                 fn_data=fn_data,
                 types=smir_info.types,
             )
             return CallConfig(config=config, constraints=tuple(constraints))
         case RandomMode(seed):
+            if cell_maps is None:
+                raise ValueError('cell_maps is required for RandomMode')
             config = _make_random_call_config(
                 definition=definition,
                 fn_data=fn_data,
                 types=smir_info.types,
                 seed=seed,
+                cell_maps=cell_maps,
             )
             return CallConfig(config=config, constraints=())
 
@@ -140,6 +149,7 @@ def _make_concrete_call_config(
     *,
     definition: KDefinition,
     fn_data: _FunctionData,
+    cell_maps: dict[str, KInner],
 ) -> KInner:
     if fn_data.args:
         raise ValueError(f'Cannot create concrete call configuration for {fn_data.symbol}: function has parameters')
@@ -149,6 +159,7 @@ def _make_concrete_call_config(
         fn_data=fn_data,
         localvars=[],
         seed=None,
+        cell_maps=cell_maps,
     )
 
 
@@ -158,13 +169,15 @@ def _make_random_call_config(
     fn_data: _FunctionData,
     types: Mapping[Ty, TypeMetadata],
     seed: int,
+    cell_maps: dict[str, KInner],
 ) -> KInner:
     localvars = _random_locals(Random(seed), fn_data.args, types)
     return _make_concrete_call_config_with_locals(
         definition=definition,
         fn_data=fn_data,
         localvars=localvars,
         seed=seed,
+        cell_maps=cell_maps,
     )
 
 
@@ -174,6 +187,7 @@ def _make_concrete_call_config_with_locals(
     fn_data: _FunctionData,
     localvars: list[KInner],
     seed: int | None,
+    cell_maps: dict[str, KInner],
 ) -> KInner:
     def init_subst() -> dict[str, KInner]:
         init_config = definition.init_config(KSort('GeneratedTopCell'))
@@ -199,6 +213,7 @@ def init_subst() -> dict[str, KInner]:
                 'K_CELL': k_cell,
                 'LOCALS_CELL': list_of(localvars),
             },
+            **cell_maps,
         }
     )
 
@@ -215,11 +230,15 @@ def _make_symbolic_call_config(
     types: Mapping[Ty, TypeMetadata],
 ) -> tuple[KInner, list[KInner]]:
     locals, constraints = _symbolic_locals(fn_data.args, types)
+    nomap = KApply('MaybeMap::noMap')
     subst = Subst(
         {
             'K_CELL': fn_data.call_terminator,
             'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
             'LOCALS_CELL': list_of(locals),
+            'FUNCTIONS_CELL': nomap,
+            'TYPES_CELL': nomap,
+            'MEMORY_CELL': nomap,
         },
     )
     empty_config = definition.empty_config(KSort('GeneratedTopCell'))

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

@@ -89,10 +89,11 @@ Execution gets stuck (no matching rule) when operands have different types or un
 ```k
   // Raw eq: dereference operands, extract types, and delegate to typed comparison
   rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE, _SPAN)
-        => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS),
-                                  #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS))
+        => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(TYPESMAP, #withDeref(ARG1), LOCALS),
+                                  #withDeref(ARG2), #extractOperandType(TYPESMAP, #withDeref(ARG2), LOCALS))
        ... </k>
        <locals> LOCALS </locals>
+       <types> TYPESMAP </types>
 
   // Compare values only if types are identical
   syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)]
@@ -112,17 +113,35 @@ 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, no-evaluators]
-  rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS)
-       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+```
+
+```{.k .concrete}
+  syntax MaybeTy ::= #extractOperandType(MaybeMap, Operand, List) [function, total]
+  rule #extractOperandType(TYPESMAP, operandCopy(place(local(I), PROJS)), LOCALS)
+       => getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+    requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness]
+  rule #extractOperandType(TYPESMAP, operandMove(place(local(I), PROJS)), LOCALS)
+       => getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
     requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
     [preserves-definedness]
-  rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS)
-       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+```
+
+```{.k .symbolic}
+  syntax MaybeTy ::= #extractOperandType(MaybeMap, Operand, List) [function, total, no-evaluators]
+  rule #extractOperandType(_, operandCopy(place(local(I), PROJS)), LOCALS)
+       => getTyOf(noMap, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
     requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
     [preserves-definedness]
-  rule #extractOperandType(operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => TY
-  rule #extractOperandType(_, _) => TyUnknown [owise]
+  rule #extractOperandType(_, operandMove(place(local(I), PROJS)), LOCALS)
+       => getTyOf(noMap, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+    requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness]
+```
+
+```k
+  rule #extractOperandType(_, operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => TY
+  rule #extractOperandType(_, _, _) => TyUnknown [owise]
 ```
 
 #### Volatile Store (`std::intrinsics::volatile_store`, `std::ptr::write_volatile`)

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

@@ -105,8 +105,9 @@ will effectively be no-ops at this level).
          ...
        </k>
        <locals> LOCALS </locals>
+       <types> TYPESMAP </types>
        requires 0 <=Int I andBool I <Int size(LOCALS)
-        andBool notBool #isUnionType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
+        andBool notBool #isUnionType(lookupTy(TYPESMAP, tyOfLocal(getLocal(LOCALS, I))))
        [preserves-definedness]
 
   rule [execStmt.union]: <k> #execStmt(statement(statementKindAssign(place(local(I), _PROJ) #as PLACE, RVAL), _SPAN))
@@ -115,8 +116,9 @@ will effectively be no-ops at this level).
          ...
        </k>
        <locals> LOCALS </locals>
+       <types> TYPESMAP </types>
        requires 0 <=Int I andBool I <Int size(LOCALS)
-        andBool #isUnionType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
+        andBool #isUnionType(lookupTy(TYPESMAP, tyOfLocal(getLocal(LOCALS, I))))
        [preserves-definedness]
 
   // RVAL evaluation is implemented in rt/data.md
@@ -225,7 +227,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        </k>
        <currentFunc> _ => CALLER </currentFunc>
        //<currentFrame>
-         <currentBody> _ => #getBlocks(CALLER) </currentBody>
+         <currentBody> _ => #getBlocks(FUNCSMAP, CALLER) </currentBody>
          <caller> CALLER => NEWCALLER </caller>
          <dest> DEST => NEWDEST </dest>
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
@@ -234,6 +236,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        //</currentFrame>
        // remaining call stack (without top frame)
        <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
+       <functions> FUNCSMAP </functions>
 
   // no value to return, skip writing
   rule [termReturnNone]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
@@ -242,7 +245,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        </k>
        <currentFunc> _ => CALLER </currentFunc>
        //<currentFrame>
-         <currentBody> _ => #getBlocks(CALLER) </currentBody>
+         <currentBody> _ => #getBlocks(FUNCSMAP, CALLER) </currentBody>
          <caller> CALLER => NEWCALLER </caller>
          <dest> _ => NEWDEST </dest>
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
@@ -251,11 +254,22 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        //</currentFrame>
        // remaining call stack (without top frame)
        <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
+       <functions> FUNCSMAP </functions>
 
-  syntax List ::= #getBlocks( Ty )               [function, total, no-evaluators]
-                | #getBlocksAux( MonoItemKind )  [function, total]
+```
+
+```{.k .concrete}
+  syntax List ::= #getBlocks( MaybeMap, Ty )  [function, total]
+  rule #getBlocks(FUNCSMAP, TY) => #getBlocksAux(lookupFunction(FUNCSMAP, TY))
+```
+
+```{.k .symbolic}
+  syntax List ::= #getBlocks( MaybeMap, Ty )  [function, total, no-evaluators]
+  rule #getBlocks(_, TY) => #getBlocksAux(lookupFunctionKore(TY))
+```
 
-  rule #getBlocks(TY) => #getBlocksAux(lookupFunction(TY))
+```k
+  syntax List ::= #getBlocksAux( MonoItemKind )  [function, total]
 
   // returns blocks from the body
   rule #getBlocksAux(monoItemFn(_, _, noBody)) => .List
@@ -312,27 +326,44 @@ where the returned result should go.
   syntax KItem ::= #checkFunctionFilter(MonoItemKind)
 
   rule <k> #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), SPAN))
-        => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
+        => #execTerminatorCall(Ty, lookupFunction(FUNCSMAP, Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
+       <functions> FUNCSMAP </functions>
 
   rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), PROJS)), ARGS, DEST, TARGET, UNWIND), SPAN))
-        => #execTerminatorCall({#projectedCallTy(I, PROJS, LOCALS)}:>Ty, lookupFunction({#projectedCallTy(I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
+        => #execTerminatorCall({#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty, lookupFunction(FUNCSMAP, {#projectedCallTy(TYPESMAP, I, PROJS, LOCALS)}:>Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
       <locals> LOCALS </locals>
-    requires isTy(#projectedCallTy(I, PROJS, LOCALS))
+      <functions> FUNCSMAP </functions>
+      <types> TYPESMAP </types>
+    requires isTy(#projectedCallTy(TYPESMAP, 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, no-evaluators]
+```{.k .concrete}
+  syntax MaybeTy ::= #projectedCallTy(MaybeMap, Int, ProjectionElems, List) [function, total]
 
-  rule #projectedCallTy(I, PROJS, LOCALS)
-    => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+  rule #projectedCallTy(TYPESMAP, I, PROJS, LOCALS)
+    => getTyOf(TYPESMAP, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
     requires 0 <=Int I andBool I <Int size(LOCALS)
      andBool isTypedLocal(LOCALS[I])
     [preserves-definedness]
+```
 
-  rule #projectedCallTy(_, _, _) => TyUnknown [owise]
+```{.k .symbolic}
+  syntax MaybeTy ::= #projectedCallTy(MaybeMap, Int, ProjectionElems, List) [function, total, no-evaluators]
+
+  rule #projectedCallTy(_, I, PROJS, LOCALS)
+    => getTyOf(noMap, tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness]
+```
+
+```k
+  rule #projectedCallTy(_, _, _, _) => TyUnknown [owise]
 
   // Intrinsic function call - execute directly without state switching
   rule [termCallIntrinsic]:
@@ -537,14 +568,15 @@ Therefore a heuristics is used here:
           </stack>
          ...
        </currentFrame>
+       <types> TYPESMAP </types>
     requires 0 <=Int CLOSURE andBool CLOSURE <Int size(LOCALS)
      andBool 0 <=Int TUPLE andBool TUPLE <Int size(LOCALS)
      andBool isTypedValue(LOCALS[TUPLE])
-     andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
+     andBool isTupleType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
      andBool isTypedLocal(LOCALS[CLOSURE])
      andBool (
-               typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))
-               orBool isFunType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
+               typeInfoVoidType ==K lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))
+               orBool isFunType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
              )
     [priority(40), preserves-definedness]
 
@@ -570,17 +602,18 @@ Therefore a heuristics is used here:
           </stack>
          ...
        </currentFrame>
+       <types> TYPESMAP </types>
     requires 0 <=Int CLOSURE andBool CLOSURE <Int size(LOCALS)
      andBool 0 <=Int TUPLE andBool TUPLE <Int size(LOCALS)
      andBool isTypedValue(LOCALS[TUPLE])
-     andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
+     andBool isTupleType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
      andBool isTypedLocal(LOCALS[CLOSURE])
                // or the closure ref type pointee is missing from the type table
-     andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
-     andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))))
+     andBool isRefType(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
+     andBool isTy(pointeeTy(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))))
      andBool (
-               lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
-               orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty))
+               lookupTy(TYPESMAP, {pointeeTy(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
+               orBool isFunType(lookupTy(TYPESMAP, {pointeeTy(lookupTy(TYPESMAP, tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty))
              )
     [priority(45), preserves-definedness]
 

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

@@ -45,6 +45,10 @@ module KMIR-CONFIGURATION
                   </currentFrame>
                   // remaining call stack (without top frame)
                   <stack> .List </stack>
+                  // static data lookup tables (populated in concrete execution, noMap in symbolic execution)
+                  <functions> noMap </functions>
+                  <types> noMap </types>
+                  <memory> noMap </memory>
                 </kmir>
 ```
 
@@ -60,6 +64,10 @@ rather than carrying static `Map` structures with the configuration.
 
 The functions are defined in the `RT-VALUE` module for now but should have their own module.
 
+The configuration also contains cells for these lookup tables (`functions`, `types`, `memory`)
+holding `MaybeMap` values. In concrete execution they are populated with `someMap(M)` for efficient
+LLVM execution; in symbolic execution they are `noMap` and lookups use the generated functions instead.
+
 ```k
 endmodule
 ```