Skip to content

Update from master: smaller configuration with static data compiled to kore #749

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

Update from master: smaller configuration with static data compiled to kore #749

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions kmir/src/kmir/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import logging
import sys
import tempfile
from argparse import ArgumentParser
from pathlib import Path
from typing import TYPE_CHECKING
Expand Down Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions kmir/src/kmir/build.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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')
97 changes: 41 additions & 56 deletions kmir/src/kmir/kdist/mir-semantics/kmir.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 ]
Expand Down Expand Up @@ -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 ]

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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>
Expand All @@ -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)) ~> _
Expand All @@ -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>
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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>
Expand All @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)]
Expand All @@ -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
Expand Down Expand Up @@ -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
22 changes: 14 additions & 8 deletions kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
Loading
Loading