Compiling SMIR JSON to kore to avoid static data in config (#745)

Pervasive changes to the semantics and python client code to replace the
lookup tables in the config (`memory`, `functions`, `types`) by lookup
functions whose equations are generated from the `SMIRInfo` i.e., from
the SMIR JSON , for each program.

Previously we had `Map`-sorted config cells `functions`, `types` and
`memory`, which are now _functions_ instead. The function equations have
to be added and then compiled with the LLVM backend for it to work, but
the configuration is much smaller and does not have any static data any
more.

Author: jberthold

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
 ```