Compiling SMIR JSON to kore to avoid static data in config

kmir/src/kmir/__main__.py

@@ -2,6 +2,7 @@
 
 import logging
 import sys
+import tempfile
 from argparse import ArgumentParser
 from pathlib import Path
 from typing import TYPE_CHECKING
@@ -57,13 +58,14 @@ def _kmir_run(opts: RunOpts) -> None:
         # target = opts.bin if opts.bin else cargo.default_target
         smir_info = cargo.smir_for_project(clean=False)
 
-    result = kmir.run_smir(smir_info, start_symbol=opts.start_symbol, depth=opts.depth)
-    print(kmir.kore_to_pretty(result))
+    with tempfile.TemporaryDirectory() as work_dir:
+        kmir = KMIR.from_kompiled_kore(smir_info, symbolic=opts.haskell_backend, target_dir=work_dir)
+        result = kmir.run_smir(smir_info, start_symbol=opts.start_symbol, depth=opts.depth)
+        print(kmir.kore_to_pretty(result))
 
 
 def _kmir_prove_rs(opts: ProveRSOpts) -> None:
-    kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report)
-    proof = kmir.prove_rs(opts)
+    proof = KMIR.prove_rs(opts)
     print(str(proof.summary))
     if not proof.passed:
         sys.exit(1)

kmir/src/kmir/build.py

@@ -10,3 +10,4 @@
 LLVM_DEF_DIR: Final = kdist.which('mir-semantics.llvm')
 LLVM_LIB_DIR: Final = kdist.which('mir-semantics.llvm-library')
 HASKELL_DEF_DIR: Final = kdist.which('mir-semantics.haskell')
+KMIR_SOURCE_DIR: Final = kdist.which('mir-semantics.source')

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

@@ -43,21 +43,20 @@ Execution of a program begins by creating a stack frame for the `main`
 function and executing its function body. Before execution begins, the
 function map and the initial memory have to be set up.
 
-```k
+All of this is done in the client code so we omit the initialisation code which was historically placed here.
+
+```
   // #init step, assuming a singleton in the K cell
-  rule <k> #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:TypeMappings _MACHINE:MachineInfo)
+  rule <k> #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames _ITEMS:MonoItems _TYPES:TypeMappings _MACHINE:MachineInfo)
          =>
            #execFunction(#findItem(ITEMS, FUNCNAME), FUNCTIONS)
        </k>
-       <functions> _ => #mkFunctionMap(FUNCTIONS, ITEMS) </functions>
-       <start-symbol> FUNCNAME </start-symbol>
-       <types> _ => #mkTypeMap(.Map, TYPES) </types>
 ```
 
 The `Map` of types is static information used for decoding constants and allocated data into `Value`s.
 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, symbol("mkTypeMap")]
 
   rule #mkTypeMap(ACC, .TypeMappings) => ACC
@@ -83,7 +82,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, symbol("mkFunctionMap") ]
                | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ]
                | #accumItems ( Map, MonoItems )              [ function, total ]
@@ -138,7 +137,7 @@ structure from its function body and then execute the first basic
 block of the body. The function's `Ty` index in the `functions` map must
 be known to populate the `currentFunc` field.
 
-```k
+```
   // find function through its MonoItemFn.name
   syntax MonoItem ::= #findItem ( MonoItems, Symbol ) [ function ]
 
@@ -185,20 +184,9 @@ be known to populate the `currentFunc` field.
     [owise]
 
   rule #tyFromName(_, .List) => ty(-1) // HACK see #mainIsMinusOne above
-
-  syntax List ::= toKList(BasicBlocks) [function, total]
-
-  rule toKList( .BasicBlocks )                => .List
-  rule toKList(B:BasicBlock REST:BasicBlocks) => ListItem(B) toKList(REST)
-
-  syntax List ::= #reserveFor( LocalDecls ) [function, total]
-
-  rule #reserveFor(.LocalDecls) => .List
-
-  rule #reserveFor(localDecl(TY, _, MUT) REST:LocalDecls)
-      =>
-       ListItem(newLocal(TY, MUT)) #reserveFor(REST)
 ```
+#### Function Execution
+
 
 Executing a function body consists of repeated calls to `#execBlock`
 for the basic blocks that, together, constitute the function body. The
@@ -345,7 +333,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        </k>
        <currentFunc> _ => CALLER </currentFunc>
        //<currentFrame>
-         <currentBody> _ => #getBlocks(FUNCS, CALLER) </currentBody>
+         <currentBody> _ => #getBlocks(CALLER) </currentBody>
          <caller> CALLER => NEWCALLER </caller>
          <dest> DEST => NEWDEST </dest>
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
@@ -354,9 +342,6 @@ 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> FUNCS </functions>
-     requires CALLER in_keys(FUNCS)
-     [preserves-definedness] // CALLER lookup defined
 
   // no value to return, skip writing
   rule <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
@@ -365,7 +350,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
        </k>
        <currentFunc> _ => CALLER </currentFunc>
        //<currentFrame>
-         <currentBody> _ => #getBlocks(FUNCS, CALLER) </currentBody>
+         <currentBody> _ => #getBlocks(CALLER) </currentBody>
          <caller> CALLER => NEWCALLER </caller>
          <dest> _ => NEWDEST </dest>
          <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
@@ -374,15 +359,11 @@ 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> FUNCS </functions>
-     requires CALLER in_keys(FUNCS)
-     [preserves-definedness] // CALLER lookup defined
 
-  syntax List ::= #getBlocks(Map, Ty) [function]
-                | #getBlocksAux(MonoItemKind)  [function, total]
+  syntax List ::= #getBlocks( Ty )               [function, total]
+                | #getBlocksAux( MonoItemKind )  [function, total]
 
-  rule #getBlocks(FUNCS, ID) => #getBlocksAux({FUNCS[ID]}:>MonoItemKind)
-    requires ID in_keys(FUNCS)
+  rule #getBlocks(TY) => #getBlocksAux(lookupFunction(TY))
 
   // returns blocks from the body
   rule #getBlocksAux(monoItemFn(_, _, noBody)) => .List
@@ -391,6 +372,11 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f
   rule #getBlocksAux(monoItemStatic(_, _, _)) => .List // should not occur in calls
   rule #getBlocksAux(monoItemGlobalAsm(_)) => .List // not supported
   rule #getBlocksAux(IntrinsicFunction(_)) => .List // intrinsics have no body
+
+  syntax List ::= toKList(BasicBlocks) [function, total]
+  // ---------------------------------------------------
+  rule toKList( .BasicBlocks )                => .List
+  rule toKList(B:BasicBlock REST:BasicBlocks) => ListItem(B) toKList(REST)
 ```
 
 When a `terminatorKindReturn` is executed but the optional target is empty
@@ -434,18 +420,14 @@ where the returned result should go.
   // Intrinsic function call - execute directly without state switching
   rule <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _
          =>
-           #execIntrinsic({FUNCTIONS[#tyOfCall(FUNC)]}:>MonoItemKind, ARGS, DEST) ~> #continueAt(TARGET)
+           #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET)
        </k>
-       <functions> FUNCTIONS </functions>
-    requires #tyOfCall(FUNC) in_keys(FUNCTIONS)
-     andBool isMonoItemKind(FUNCTIONS[#tyOfCall(FUNC)])
-     andBool isIntrinsicFunction({FUNCTIONS[#tyOfCall(FUNC)]}:>MonoItemKind)
-    [preserves-definedness] // callee lookup defined
+    requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
 
   // Regular function call - full state switching and stack setup
   rule <k> #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _
          =>
-           #setUpCalleeData({FUNCTIONS[#tyOfCall(FUNC)]}:>MonoItemKind, ARGS)
+           #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
        </k>
        <currentFunc> CALLER => #tyOfCall(FUNC) </currentFunc>
        <currentFrame>
@@ -457,11 +439,7 @@ where the returned result should go.
          <locals> LOCALS </locals>
        </currentFrame>
        <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
-       <functions> FUNCTIONS </functions>
-    requires #tyOfCall(FUNC) in_keys(FUNCTIONS)
-     andBool isMonoItemKind(FUNCTIONS[#tyOfCall(FUNC)])
-     andBool notBool isIntrinsicFunction({FUNCTIONS[#tyOfCall(FUNC)]}:>MonoItemKind)
-    [preserves-definedness] // callee lookup defined
+    requires notBool isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC)))
 
   syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function]
   rule isIntrinsicFunction(IntrinsicFunction(_)) => true
@@ -506,6 +484,14 @@ An operand may be a `Reference` (the only way a function could access another fu
        </currentFrame>
   // TODO: Haven't handled "noBody" case
 
+  syntax List ::= #reserveFor( LocalDecls ) [function, total]
+
+  rule #reserveFor(.LocalDecls) => .List
+
+  rule #reserveFor(localDecl(TY, _, MUT) REST:LocalDecls)
+      =>
+       ListItem(newLocal(TY, MUT)) #reserveFor(REST)
+
 
   syntax KItem ::= #setArgsFromStack ( Int, Operands)
                  | #setArgFromStack ( Int, Operand)
@@ -631,11 +617,10 @@ 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)
-        => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS, TYPEMAP),
-                                  #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS, TYPEMAP))
+        => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS),
+                                  #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS))
        ... </k>
        <locals> LOCALS </locals>
-       <types> TYPEMAP </types>
 
   // Compare values only if types are identical
   syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)]
@@ -655,17 +640,17 @@ 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, Map) [function, total]
-  rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS, TYPEMAP)
-       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP)
+  syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total]
+  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])
     [preserves-definedness]
-  rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS, TYPEMAP)
-       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP)
+  rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS)
+       => getTyOf(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(operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => TY
+  rule #extractOperandType(_, _) => TyUnknown [owise]
 ```
 
 ### Stopping on Program Errors
@@ -694,6 +679,6 @@ The top-level module `KMIR` includes both the control flow constructs (and trans
 module KMIR
   imports KMIR-CONTROL-FLOW
   imports KMIR-LEMMAS
-  imports KMIR-SYMBOLIC-LOCALS
+//  imports KMIR-SYMBOLIC-LOCALS
 
 endmodule

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

@@ -46,15 +46,21 @@ module KMIR-CONFIGURATION
                   </currentFrame>
                   // remaining call stack (without top frame)
                   <stack> .List </stack>
-                  // static and dynamic allocations: AllocId -> Value
-                  <memory> .Map </memory>
-                  // ============ static information ============
-                  // function store, Ty -> MonoItemFn
-                  <functions> .Map </functions>
-                  <start-symbol> symbol($STARTSYM:String) </start-symbol>
-                  // static information about the base type interning in the MIR
-                  <types> .Map </types>
                 </kmir>
+```
+
+Additional fields of the configuration contain _static_ information.
+
+* The function store mapping `Ty` to `MonoItemFn` (and `IntrinsicFn`). This is essentially the entire program.
+* The allocation store, mapping `AllocId` to `Value` (or error markers if undecoded)
+* The type metadata map, associating `Ty` with a `TypeInfo` (which may contain more `Ty`s)
+* The mapping from `AdtDef` ID to `Ty`
 
+For better performance, this information is reified to K functions,
+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.
+
+```k
 endmodule
 ```