Skip to content

GlobalAllocs in configuration #533

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

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from
Draft

GlobalAllocs in configuration #533

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
ec8bc28
GlobalAllocs are added to memory map
dkcumming Apr 11, 2025
e604728
Set Version: 0.3.122
rv-auditor Apr 24, 2025
0452223
Merge remote-tracking branch 'origin/master' into dc/global-allocs
dkcumming May 15, 2025
c13170b
Set Version: 0.3.163
rv-auditor May 15, 2025
e2cca64
Fixed duplicate memory typox
dkcumming May 15, 2025
a80d051
Map is now from AllocId -> GlobalAllocKind
dkcumming May 16, 2025
4348cb1
Reference now RefStack and RefAlloc
dkcumming May 16, 2025
8d14018
Decoding Constant with Prov
dkcumming May 16, 2025
05e9a3b
Added tests with GlobalAlloc / promoted
dkcumming May 16, 2025
1005aa0
Updated output of tests
dkcumming May 16, 2025
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
2 changes: 1 addition & 1 deletion kmir/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "hatchling.build"

[project]
name = "kmir"
version = "0.3.162"
version = "0.3.163"
description = ""
requires-python = "~=3.10"
dependencies = [
Expand Down
2 changes: 1 addition & 1 deletion kmir/src/kmir/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
from typing import Final

VERSION: Final = '0.3.162'
VERSION: Final = '0.3.163'
10 changes: 9 additions & 1 deletion 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 @@ -45,11 +45,12 @@ function map and the initial memory have to be set up.

```k
// #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>
<memory> _ => #mkMemoryMap(ALLOCS) </memory>
<start-symbol> FUNCNAME </start-symbol>
<types> _ => #mkTypeMap(.Map, TYPES) </types>
<adt-to-ty> _ => #mkAdtMap(.Map, TYPES) </adt-to-ty>
Expand Down Expand Up @@ -108,7 +109,14 @@ they are callee in a `Call` terminator within an `Item`).
The function _names_ and _ids_ are not relevant for calls and therefore dropped.

```k
rule #mkMemoryMap(Globals) => #accumMemory(.Map, Globals)

rule #accumMemory(Acc, .GlobalAllocs) => Acc
rule #accumMemory(Acc, globalAllocEntry(ID, ALLOC) REST) => #accumMemory(Acc (ID |-> ALLOC), REST)

syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total ]
| #mkMemoryMap ( GlobalAllocs ) [ function, total ]
| #accumMemory ( Map, GlobalAllocs ) [ function, total ]
| #accumFunctions ( Map, Map, FunctionNames ) [ function, total ]
| #accumItems ( Map, MonoItems ) [ function, total ]

Expand Down
2 changes: 1 addition & 1 deletion 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,11 +46,11 @@ module KMIR-CONFIGURATION
</currentFrame>
// remaining call stack (without top frame)
<stack> .List </stack>
// heap, Address(Int) -> ( GlobalAlloc | Data? )
<memory> .Map </memory>
// ============ static information ============
// function store, Ty -> MonoItemFn
<functions> .Map </functions>
// heap
<start-symbol> symbol($STARTSYM:String) </start-symbol>
// static information about the base type interning in the MIR
<types> .Map </types>
Expand Down
36 changes: 22 additions & 14 deletions kmir/src/kmir/kdist/mir-semantics/rt/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,10 +74,11 @@ Constant operands are simply decoded according to their type.
```k
rule <k> operandConstant(constOperand(_, _, mirConst(KIND, TY, _)))
=>
typedValue(#decodeConstant(KIND, {TYPEMAP[TY]}:>TypeInfo), TY, mutabilityNot)
typedValue(#decodeConstant(KIND, {TYPEMAP[TY]}:>TypeInfo, MEM), TY, mutabilityNot)
...
</k>
<types> TYPEMAP </types>
<memory> MEM </memory>
requires TY in_keys(TYPEMAP)
andBool isTypeInfo(TYPEMAP[TY])
[preserves-definedness] // valid Map lookup checked
Expand Down Expand Up @@ -232,7 +233,7 @@ In the simplest case, the reference refers to a local in the same stack frame (h

```k
rule <k> #readProjection(
typedValue(Reference(0, place(local(I:Int), PLACEPROJS:ProjectionElems), _), _, _),
typedValue(RefStack(0, place(local(I:Int), PLACEPROJS:ProjectionElems), _), _, _),
projectionElemDeref PROJS:ProjectionElems
)
=>
Expand All @@ -259,7 +260,7 @@ An important prerequisite of this rule is that when passing references to a call

```k
rule <k> #readProjection(
typedValue(Reference(FRAME, place(LOCAL:Local, PLACEPROJS), _), _, _),
typedValue(RefStack(FRAME, place(LOCAL:Local, PLACEPROJS), _), _, _),
projectionElemDeref PROJS
)
=>
Expand Down Expand Up @@ -290,8 +291,8 @@ An important prerequisite of this rule is that when passing references to a call
| #decrementRef ( TypedLocal ) [function, total]
| #adjustRef (TypedLocal, Int ) [function, total]

rule #adjustRef(typedValue(Reference(HEIGHT, PLACE, REFMUT), TY, MUT), OFFSET)
=> typedValue(Reference(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT)
rule #adjustRef(typedValue(RefStack(HEIGHT, PLACE, REFMUT), TY, MUT), OFFSET)
=> typedValue(RefStack(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT)
rule #adjustRef(TL, _) => TL [owise]

rule #incrementRef(TL) => #adjustRef(TL, 1)
Expand Down Expand Up @@ -523,7 +524,7 @@ The solution is to use rewrite operations in a downward pass through the project

rule <k> #projectedUpdate(
_DEST,
typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _MUT), _, _),
typedValue(RefStack(OFFSET, place(LOCAL, PLACEPROJ), _MUT), _, _),
projectionElemDeref PROJS,
UPDATE,
_CTXTS,
Expand All @@ -548,7 +549,7 @@ The solution is to use rewrite operations in a downward pass through the project

rule <k> #projectedUpdate(
_DEST,
typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _MUT), _, _),
typedValue(RefStack(OFFSET, place(local(I), PLACEPROJ), _MUT), _, _),
projectionElemDeref PROJS,
UPDATE,
_CTXTS,
Expand Down Expand Up @@ -799,7 +800,7 @@ The `BorrowKind` indicates mutability of the value through the reference, but al
```k
rule <k> rvalueRef(_REGION, KIND, PLACE)
=>
typedValue(Reference(0, PLACE, #mutabilityOf(KIND)), TyUnknown, #mutabilityOf(KIND))
typedValue(RefStack(0, PLACE, #mutabilityOf(KIND)), TyUnknown, #mutabilityOf(KIND))
...
</k>

Expand Down Expand Up @@ -851,19 +852,19 @@ bit width, signedness, and possibly truncating or 2s-complementing the value.
The `Value` sort above operates at a higher level than the bytes representation found in the MIR syntax for constant values. The bytes have to be interpreted according to the given `TypeInfo` to produce the higher-level value. This is currently only defined for `PrimitiveType`s (primitive types in MIR).

```k
syntax Value ::= #decodeConstant ( ConstantKind, TypeInfo ) [function]
syntax Value ::= #decodeConstant ( ConstantKind, TypeInfo, Map ) [function]

//////////////////////////////////////////////////////////////////////////////////////
// decoding the correct amount of bytes depending on base type size

// Boolean: should be one byte with value one or zero
rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool)) => BoolVal(false)
rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool), _MEM) => BoolVal(false)
requires 0 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1
rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool)) => BoolVal(true)
rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool), _MEM) => BoolVal(true)
requires 1 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1

// Integer: handled in separate module for numeric operations
rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), TYPEINFO)
rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), TYPEINFO, _MEM)
=>
#decodeInteger(BYTES, #intTypeOf(TYPEINFO))
requires #isIntType(TYPEINFO)
Expand All @@ -872,16 +873,23 @@ The `Value` sort above operates at a higher level than the bytes representation

////////////////////////////////////////////////////////////////////////////////////////////////
// FIXME Char type
// rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeChar))
// rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _), _MEM), typeInfoPrimitiveType(primTypeChar))
// =>
// Str(...)
/////////////////////////////////////////////////////////////////////////////////////////////////

rule #decodeConstant(constantKindAllocated(allocation(_BYTES, provenanceMap(
provenanceMapEntry(_SIZE, allocId(ID:Int)) .ProvenanceMapEntries
), _ALIGN, _MUT)), typeInfoRefType(_TY), MEMORY)
=>
RefAlloc(ID)
requires ID in_keys(MEMORY)
[preserves-definedness] // AllocId in Memory is checked, TY in Types checked previously

/////////////////////////////////////////////////////////////////////////////////////////////////
// TODO Float decoding: not supported natively in K

rule #decodeConstant(_, _) => Any [owise]
rule #decodeConstant(_, _, _) => Any [owise]
```

## Primitive operations on numeric data
Expand Down
5 changes: 4 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/rt/value.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,14 +30,17 @@ High-level values can be
// heterogenous value list for tuples and structs (standard, tuple, or anonymous)
| Float( Float, Int )
// value, bit-width for f16-f128
| Reference( Int , Place , Mutability )
| Reference
// stack depth (initially 0), place, borrow kind
| Range( List )
// homogenous values for array/slice
// | Ptr( Address, MaybeValue )
// address, metadata for ref/ptr
| "Any"
// arbitrary value for transmute/invalid ptr lookup

syntax Reference ::= RefStack( Int , Place , Mutability )
| RefAlloc( Int )
```

## Local variables
Expand Down
3 changes: 2 additions & 1 deletion kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,8 @@
.List
</stack>
<memory>
.Map
2 |-> Memory ( allocation (... bytes: b"unsafe precondition(s) violated: u8::unchecked_add cannot overflow" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
3 |-> Memory ( allocation (... bytes: b"unsafe precondition(s) violated: i8::unchecked_sub cannot overflow" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
</memory>
<functions>
ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
Expand Down
2 changes: 1 addition & 1 deletion kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@
.List
</stack>
<memory>
.Map
1 |-> Memory ( allocation (... bytes: b"assertion failed: b == c" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
</memory>
<functions>
ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
Expand Down
Loading