diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index bf71df0eb..d43c4bc8e 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmir" -version = "0.3.121" +version = "0.3.122" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 171936af8..1345b2f7a 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.121' +VERSION: Final = '0.3.122' diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 63beaa787..cc6642088 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -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 #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:TypeMappings) + rule #init(_NAME:Symbol ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:TypeMappings) => #execFunction(#findItem(ITEMS, FUNCNAME), FUNCTIONS) _ => #mkFunctionMap(FUNCTIONS, ITEMS) + _ => #mkMemoryMap(ALLOCS) FUNCNAME _ => #mkTypeMap(.Map, TYPES) _ => #mkAdtMap(.Map, TYPES) @@ -108,7 +109,16 @@ 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 Address ::= "Address" "(" Int ")" + + rule #mkMemoryMap(Globals) => #accumMemory(.Map, Address(1), Globals) + + rule #accumMemory(Acc, _, .GlobalAllocs) => Acc + rule #accumMemory(Acc, Address(INDEX), Global REST) => #accumMemory(Acc (Address(INDEX) |-> Global), Address(INDEX +Int 1), REST) + syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total ] + | #mkMemoryMap ( GlobalAllocs ) [ function, total ] + | #accumMemory ( Map, Address, GlobalAllocs ) [ function, total ] | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ] | #accumItems ( Map, MonoItems ) [ function, total ] diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md index 80d39e906..5e9b05ad4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md @@ -48,9 +48,8 @@ module KMIR-CONFIGURATION .List // function store, Ty -> MonoItemFn .Map - // heap - .Map // FIXME unclear how to model - // FIXME where do we put the "GlobalAllocs"? in the heap, presumably? + // heap, Address(Int) -> ( GlobalAlloc | Data? ) + .Map symbol($STARTSYM:String) // static information about the base type interning in the MIR .Map diff --git a/package/version b/package/version index b96616520..165ea630e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.121 +0.3.122