From d8dddd055c47c4b9b7e12cf79d02d82fd27ad89c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 11:00:28 +1100 Subject: [PATCH 01/12] Move basic runtime types and configuration into separate files * new module `RT-VALUE-SYNTAX` in `rt/value.md` - `Value` from `RT-DATA-HIGH-SYNTAX` - `TypedLocal` and its subsorts as well as helper functions * moved `KMIR-CONFIGURATION` into `rt/configuration.md` * an empty `rt/integer.md` file (not used yet) --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 73 ++------ .../kdist/mir-semantics/lemmas/kmir-lemmas.md | 4 +- .../kdist/mir-semantics/rt/configuration.md | 60 +++++++ kmir/src/kmir/kdist/mir-semantics/rt/data.md | 159 +++--------------- .../kmir/kdist/mir-semantics/rt/integer.md | 33 ++++ kmir/src/kmir/kdist/mir-semantics/rt/value.md | 96 +++++++++++ 6 files changed, 222 insertions(+), 203 deletions(-) create mode 100644 kmir/src/kmir/kdist/mir-semantics/rt/configuration.md create mode 100644 kmir/src/kmir/kdist/mir-semantics/rt/integer.md create mode 100644 kmir/src/kmir/kdist/mir-semantics/rt/value.md diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index d7886dac8..6809d9c38 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -3,6 +3,7 @@ ```k requires "kmir-ast.md" requires "rt/data.md" +requires "rt/configuration.md" requires "lemmas/kmir-lemmas.md" ``` @@ -25,79 +26,25 @@ endmodule ### Execution Configuration -The execution (dynamic) semantics of MIR in K is defined based on the -configuration of the running program. - -Essential parts of the configuration: -* the `k` cell to control the execution -* a `stack` of `StackFrame`s describing function calls and their data -* `currentFrame`, an unpacked version of the top of `stack` -* the `functions` map to look up function bodies when they are called -* the `memory` cell which abstracts allocated heap data - -The entire program's return value (`retVal`) is held in a separate cell. - -Besides the `caller` (to return to) and `dest` and `target` to specify where the return value should be written, a `StackFrame` includes information about the `locals` of the currently-executing function/item. Each function's code will only access local values (or heap data referenced by them). Local variables carry type information (see `RT-DATA`). - -```k -module KMIR-CONFIGURATION - imports KMIR-SYNTAX - imports INT-SYNTAX - imports BOOL-SYNTAX - imports RT-DATA-HIGH-SYNTAX - - syntax RetVal ::= return( Value ) - | "noReturn" - - syntax StackFrame ::= StackFrame(caller:Ty, // index of caller function - dest:Place, // place to store return value - target:MaybeBasicBlockIdx, // basic block to return to - UnwindAction, // action to perform on panic - locals:List) // return val, args, local variables - - configuration - #init($PGM:Pgm) - noReturn - ty(-1) // to retrieve caller - // unpacking the top frame to avoid frequent stack read/write operations - - .List - ty(-1) - place(local(-1), .ProjectionElems) - noBasicBlockIdx - unwindActionUnreachable - .List - - // remaining call stack (without top frame) - .List - // function store, Ty -> MonoItemFn - .Map - // heap - .Map // FIXME unclear how to model - // FIXME where do we put the "GlobalAllocs"? in the heap, presumably? - symbol($STARTSYM:String) - // static information about the base type interning in the MIR - .Map - - -endmodule -``` +The _configuration_ that this MIR semantics operates on carries the entire state of the running program, including local variables of the current function item, the whole call stack, as well as all code items that may potentially be executed. +See [`rt/configuration.md`](./rt/configuration.md) for a detailed description of the configuration. ### Execution Control Flow ```k module KMIR-CONTROL-FLOW - imports KMIR-SYNTAX - imports KMIR-CONFIGURATION - imports MONO - imports RT-DATA-HIGH - imports TYPES - imports BOOL imports LIST imports MAP imports K-EQUAL + + imports KMIR-SYNTAX + imports MONO + imports TYPES + + imports KMIR-CONFIGURATION + imports RT-DATA ``` Execution of a program begins by creating a stack frame for the `main` diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md index ffe5e10ac..fa01bd627 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -12,11 +12,11 @@ requires "../rt/data.md" requires "../kmir.md" module KMIR-LEMMAS - imports RT-DATA-HIGH - imports LIST imports INT-SYMBOLIC imports BOOL + + imports RT-DATA ``` ## Simplifications for lists to avoid spurious branching on error cases in control flow diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md new file mode 100644 index 000000000..2e1c1583c --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md @@ -0,0 +1,60 @@ +# KMIR Configuration + +This is the configuration of a running program in the MIR semantics. + +Essential parts of the configuration: +* the `k` cell to control the execution +* a `stack` of `StackFrame`s describing function calls and their data +* `currentFrame`, an unpacked version of the top of `stack` +* the `functions` map to look up function bodies when they are called +* the `memory` cell which abstracts allocated heap data + +The entire program's return value (`retVal`) is held in a separate cell. + +Besides the `caller` (to return to) and `dest` and `target` to specify where the return value should be written, a `StackFrame` includes information about the `locals` of the currently-executing function/item. Each function's code will only access local values (or heap data referenced by them). Local variables carry type information (see `RT-DATA`). + +```k +requires "./value.md" + +module KMIR-CONFIGURATION + imports KMIR-SYNTAX + imports INT-SYNTAX + imports BOOL-SYNTAX + imports RT-VALUE-SYNTAX + + syntax RetVal ::= return( Value ) + | "noReturn" + + syntax StackFrame ::= StackFrame(caller:Ty, // index of caller function + dest:Place, // place to store return value + target:MaybeBasicBlockIdx, // basic block to return to + UnwindAction, // action to perform on panic + locals:List) // return val, args, local variables + + configuration + #init($PGM:Pgm) + noReturn + ty(-1) // to retrieve caller + // unpacking the top frame to avoid frequent stack read/write operations + + .List + ty(-1) + place(local(-1), .ProjectionElems) + noBasicBlockIdx + unwindActionUnreachable + .List + + // remaining call stack (without top frame) + .List + // function store, Ty -> MonoItemFn + .Map + // heap + .Map // FIXME unclear how to model + // FIXME where do we put the "GlobalAllocs"? in the heap, presumably? + symbol($STARTSYM:String) + // static information about the base type interning in the MIR + .Map + + +endmodule +``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index abffce4a2..a7e69e82c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -6,76 +6,7 @@ This module addresses all aspects of handling "values" i.e., data, at runtime du ```k requires "../ty.md" requires "../body.md" - -module RT-DATA-SYNTAX - imports INT-SYNTAX - imports FLOAT-SYNTAX - imports LIST - imports MAP - imports BOOL-SYNTAX - - imports TYPES - imports BODY - - syntax Value - - syntax Value ::= #decodeConstant ( ConstantKind, RigidTy ) [function] - - syntax MIRError -``` - -### Local variables - -A list `locals` of local variables of a stack frame is stored as values together -with their type information (to enable type-checking assignments). Also, the -`Mutability` is remembered to prevent mutation of immutable values. - -The local variables may be actual values (`typedValue`), uninitialised (`NewLocal`) or `Moved`. - -```k - // local storage of the stack frame - syntax TypedLocal ::= TypedValue | MovedLocal | NewLocal - - syntax TypedValue ::= typedValue ( Value , MaybeTy , Mutability ) - - syntax MovedLocal ::= "Moved" - - syntax NewLocal ::= newLocal ( Ty , Mutability ) - - // the type of aggregates cannot be determined from the data provided when they - // occur as `RValue`, therefore we have to make the `Ty` field optional here. - syntax MaybeTy ::= Ty - | "TyUnknown" - - // accessors - syntax MaybeTy ::= tyOfLocal ( TypedLocal ) [function, total] - // ---------------------------------------------------------- - rule tyOfLocal(typedValue(_, TY, _)) => TY - rule tyOfLocal(Moved) => TyUnknown - rule tyOfLocal(newLocal(TY, _)) => TY - - syntax Mutability ::= mutabilityOf ( TypedLocal ) [function, total] - // ---------------------------------------------------------------- - rule mutabilityOf(typedValue(_, _, MUT)) => MUT - rule mutabilityOf(Moved) => mutabilityNot - rule mutabilityOf(newLocal(_, MUT)) => MUT -``` - -Access to a `TypedLocal` (whether reading or writing) may fail for a number of reasons. -It is an error to use a `Moved` local in any way, or to read an uninitialised `NewLocal`. -Also, locals are accessed via their index in list `` in a stack frame, which may be out of bounds. -Types are also checked, using the `Ty` (an opaque number assigned by the Stable MIR extraction). - -```k - syntax LocalAccessError ::= InvalidLocal ( Local ) - | TypeMismatch( Local, MaybeTy, TypedValue ) - | LocalMoved( Local ) - | LocalNotMutable ( Local ) - | LocalUninitialised( Local ) - - syntax MIRError ::= LocalAccessError - -endmodule +requires "./value.md" ``` ## Operations on local variables @@ -89,7 +20,10 @@ module RT-DATA imports MAP imports K-EQUAL - imports RT-DATA-SYNTAX + imports BODY + imports TYPES + + imports RT-VALUE-SYNTAX imports KMIR-CONFIGURATION ``` @@ -105,6 +39,21 @@ Other uses of heating and cooling are to _read_ local variables as operands. Thi syntax KResult ::= TypedLocal ``` +### Errors Related to Accessing Local Variables + +Access to a `TypedLocal` (whether reading or writing) may fail for a number of reasons. +It is an error to use a `Moved` local in any way, or to read an uninitialised `NewLocal`. +Also, locals are accessed via their index in list `` in a stack frame, which may be out of bounds. +Types are also checked, using the `Ty` (an opaque number assigned by the Stable MIR extraction). + +```k + syntax LocalAccessError ::= InvalidLocal ( Local ) + | TypeMismatch( Local, MaybeTy, TypedValue ) + | LocalMoved( Local ) + | LocalNotMutable ( Local ) + | LocalUninitialised( Local ) +``` + ### Reading operands (local variables and constants) ```k @@ -452,75 +401,9 @@ rewriting `typedLocal(...) ~> #cast(...) ~> REST` to `typedLocal(...) ~> REST`. | UnexpectedCastArgument ( TypedLocal, CastKind ) | CastNotimplemented ( CastKind ) -endmodule -``` - -## Low level representation - -```k -module RT-DATA-LOW-SYNTAX - imports RT-DATA-SYNTAX ``` + -Values in MIR are allocated arrays of `Bytes` that are interpreted according to their intended type, encoded as a `Ty` (type ID consistent across the program), and representing a `RigidTy` (other `TyKind` variants are not values that we need to operate on). - -```k - syntax Value ::= value ( Bytes , RigidTy ) - | Aggregate( List ) // retaining field structure of struct or tuple types - | Reference( Int , Place , Mutability ) // stack depth (initially 0), place, borrow kind -``` - -```k -endmodule - -module RT-DATA-LOW - imports RT-DATA-LOW-SYNTAX - imports RT-DATA - - // for low-level representations, decoding bytes is trivial - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), RIGIDTY) - => value(BYTES, RIGIDTY) - -endmodule -``` - -## High level representation - -Values in MIR can also be represented at a certain abstraction level, interpreting the given `Bytes` of a constant according to the desired type. This allows for implementing operations on values using the higher-level type and improves readability of the program data in the K configuration. - -High-level values can be -- a range of built-in types (signed and unsigned integer numbers, floats, `str` and `bool`) -- built-in product type constructs (`struct`s, `enum`s, and tuples, with heterogenous component types) -- references to a place in the current or an enclosing stack frame -- arrays and slices (with homogenous element types) - -```k -module RT-DATA-HIGH-SYNTAX - imports RT-DATA-SYNTAX - - syntax Value ::= Integer( Int, Int, Bool ) - // value, bit-width, signedness for un/signed int - | BoolVal( Bool ) - // boolean - | Aggregate( List ) - // heterogenous value list for tuples and structs (standard, tuple, or anonymous) - | Float( Float, Int ) - // value, bit-width for f16-f128 - | Reference( Int , Place , Mutability ) - // stack depth (initially 0), place, borrow kind - // | Ptr( Address, MaybeValue ) // FIXME why maybe? why value? - // address, metadata for ref/ptr - // | Range( List ) - // homogenous values for array/slice - | "Any" - // arbitrary value for transmute/invalid ptr lookup - -endmodule - -module RT-DATA-HIGH - imports RT-DATA-HIGH-SYNTAX - imports RT-DATA -``` ### Decoding constants from their bytes representation to values diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/integer.md b/kmir/src/kmir/kdist/mir-semantics/rt/integer.md new file mode 100644 index 000000000..d69f78456 --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/rt/integer.md @@ -0,0 +1,33 @@ +# Integer Implementation + +The code in this file implements functionality for `Integer` values in `mir-semantics`. + +```k +requires "./value.md" + +module RT-INTEGER + imports RT-VALUE-SYNTAX // syntax only +``` + +## Helpers and Constants for Integer Operations + +```k +// use macros for bitWidth, max/min values, bit masking, and range +``` + +## Decoding Integer values from `Bytes` for `OperandConstant` + +```k +// decode rules for int, as its own function +// what about errors? Can there be any? +``` + +## Type Casts Between Different Integer Types + +```k +// all castIntToInt rules, maybe under its own rewrite symbol +``` + +```k +endmodule +``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md new file mode 100644 index 000000000..afe363f72 --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -0,0 +1,96 @@ +# Value and Local Variable Sorts in MIR-Semantics + +This is the base module for all data in KMIR at runtime. It defines how values and local variables (holding those) are represented. + +```k +requires "../ty.md" +requires "../body.md" + +module RT-VALUE-SYNTAX + imports TYPES + imports BODY +``` + +## Values in MIR + +Values in MIR are represented at a certain abstraction level, interpreting the given `Bytes` of a constant according to the desired type. This allows for implementing operations on values using the higher-level type and improves readability of the program data in the K configuration. + +High-level values can be +- a range of built-in types (signed and unsigned integer numbers, floats, `str` and `bool`) +- built-in product type constructs (`struct`s, `enum`s, and tuples, with heterogenous component types) +- references to a place in the current or an enclosing stack frame +- arrays and slices (with homogenous element types) + +```k + syntax Value ::= Integer( Int, Int, Bool ) + // value, bit-width, signedness for un/signed int + | BoolVal( Bool ) + // boolean + | Aggregate( List ) + // heterogenous value list for tuples and structs (standard, tuple, or anonymous) + | Float( Float, Int ) + // value, bit-width for f16-f128 + | Reference( Int , Place , Mutability ) + // stack depth (initially 0), place, borrow kind + // | Ptr( Address, MaybeValue ) // FIXME why maybe? why value? + // address, metadata for ref/ptr + // | Range( List ) + // homogenous values for array/slice + | "Any" + // arbitrary value for transmute/invalid ptr lookup +``` + +## Local variables + +A list `locals` of local variables of a stack frame is stored as values together +with their type information (to enable type-checking assignments). Also, the +`Mutability` is remembered to prevent mutation of immutable values. + +The local variables may be actual values (`typedValue`), uninitialised (`NewLocal`) or `Moved`. + +```k + // local storage of the stack frame + syntax TypedLocal ::= TypedValue | MovedLocal | NewLocal + + syntax TypedValue ::= typedValue ( Value , MaybeTy , Mutability ) + + syntax MovedLocal ::= "Moved" + + syntax NewLocal ::= newLocal ( Ty , Mutability ) + + // the type of aggregates cannot be determined from the data provided when they + // occur as `RValue`, therefore we have to make the `Ty` field optional here. + syntax MaybeTy ::= Ty + | "TyUnknown" + + // accessors + syntax MaybeTy ::= tyOfLocal ( TypedLocal ) [function, total] + // ---------------------------------------------------------- + rule tyOfLocal(typedValue(_, TY, _)) => TY + rule tyOfLocal(Moved) => TyUnknown + rule tyOfLocal(newLocal(TY, _)) => TY + + syntax Mutability ::= mutabilityOf ( TypedLocal ) [function, total] + // ---------------------------------------------------------------- + rule mutabilityOf(typedValue(_, _, MUT)) => MUT + rule mutabilityOf(Moved) => mutabilityNot + rule mutabilityOf(newLocal(_, MUT)) => MUT +``` + +## Functions Operating on Values in General + +```k + syntax Value ::= #decodeConstant ( ConstantKind, RigidTy ) [function] +``` +TODO this declaration should move to the call site (dispatches into special functions for different kinds of values) + +## A generic MIR Error sort + +```k + syntax MIRError + +``` + +```k +endmodule +``` From 7f2811d48a0348cca6890073047f9de74d2e34cb Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 11:26:36 +1100 Subject: [PATCH 02/12] move contents from former RT-DATA-HIGH to RT-DATA for consistent grouping --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 896 +++++++++--------- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 7 - 2 files changed, 443 insertions(+), 460 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a7e69e82c..e12945d8c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -54,7 +54,7 @@ Types are also checked, using the `Ty` (an opaque number assigned by the Stable | LocalUninitialised( Local ) ``` -### Reading operands (local variables and constants) +### Reading Operands (Local Variables and Constants) ```k syntax Evaluation ::= Operand @@ -157,15 +157,13 @@ further access. Apart from that, the same caveats apply as for operands that are [preserves-definedness] // valid list indexing checked ``` -### Reading places with projections +#### Reading places with projections Reading an `Operand` above is only implemented for reading a `Local`, without any projecting modifications. Projections operate on the data stored in the `TypedLocal` and are therefore specific to the `Value` implementation. The following function provides an abstraction for reading with projections, its equations are co-located with the `Value` implementation(s). A projection can only be applied to an initialised value, so this operation requires `TypedValue`. ```k - syntax KItem ::= #readProjection ( TypedValue , ProjectionElems ) - rule operandCopy(place(local(I), PROJECTIONS)) => #readProjection({LOCALS[I]}:>TypedValue, PROJECTIONS) @@ -177,15 +175,140 @@ A projection can only be applied to an initialised value, so this operation requ andBool I #readProjection(VAL, .ProjectionElems) => VAL ... +``` + +A `Field` access projection operates on `struct`s and tuples, which are represented as `Aggregate` values. The field is numbered from zero (in source order), and the field type is provided (not checked here). + +```k + rule #readProjection( + typedValue(Aggregate(ARGS), _, _), + projectionElemField(fieldIdx(I), _TY) PROJS + ) + => + #readProjection({ARGS[I]}:>TypedValue, PROJS) + ... + + requires 0 <=Int I + andBool I #readProjection( + typedValue(Reference(0, place(local(I:Int), PLACEPROJS:ProjectionElems), _), _, _), + projectionElemDeref PROJS:ProjectionElems + ) + => + #readProjection({LOCALS[I]}:>TypedValue, appendP(PLACEPROJS, PROJS)) + ... + + LOCALS + requires 0 TAIL + rule appendP(X:ProjectionElem REST:ProjectionElems, TAIL) => X appendP(REST, TAIL) + +``` + +For references to enclosing stack frames, the local must be retrieved from the respective stack frame. +An important prerequisite of this rule is that when passing references to a callee as arguments, the stack height must be adjusted. + +```k + rule #readProjection( + typedValue(Reference(FRAME, place(LOCAL:Local, PLACEPROJS), _), _, _), + projectionElemDeref PROJS + ) + => + #readProjection( + {#localFromFrame({STACK[FRAME -Int 1]}:>StackFrame, LOCAL, FRAME)}:>TypedValue, + appendP(PLACEPROJS, PROJS) + ) + ... + + STACK + requires 0 StackFrame, LOCAL, FRAME)) + [preserves-definedness] // valid list indexing checked + + // TODO case of MovedLocal and NewLocal + + syntax TypedLocal ::= #localFromFrame ( StackFrame, Local, Int ) [function] + + rule #localFromFrame(StackFrame(... locals: LOCALS), local(I:Int), OFFSET) => #adjustRef({LOCALS[I]}:>TypedLocal, OFFSET) + requires 0 <=Int I + andBool I typedValue(Reference(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT) + rule #adjustRef(TL, _) => TL [owise] + + rule #incrementRef(TL) => #adjustRef(TL, 1) + rule #decrementRef(TL) => #adjustRef(TL, -1) ``` -When an operand is `Moved` by the read, the original has to be invalidated. In case of a projected value, this is a write operation nested in the data that is being read. -In contrast to regular write operations, the value does not have to be _mutable_ in order to get moved, -so we need to copy the respective code for writing, or make it generic. +#### _Moving_ Operands Under Projections + +When an operand is `Moved` by the read, the original has to be invalidated. In case of a projected value, this is a write operation nested in the data that is being read. The `#projectedUpdate` function for writing projected values is used (defined below). +In contrast to regular write operations, the value does not have to be _mutable_ in order for `Moved` to be written. The `#projectedUpdate` operation therefore carries a `force` flag to override the mutability check. + + +```k + rule operandMove(place(local(I) #as LOCAL, PROJECTIONS)) + => // read first, then write moved marker (use type from before) + #readProjection({LOCALS[I]}:>TypedValue, PROJECTIONS) ~> + #markMoved({LOCALS[I]}:>TypedLocal, LOCAL, PROJECTIONS) + ... + + LOCALS + requires PROJECTIONS =/=K .ProjectionElems + andBool 0 <=Int I + andBool I VAL:TypedLocal ~> #markMoved(OLDLOCAL, local(I), PROJECTIONS) ~> CONT + => + #projectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, Moved, .Contexts, true) + ~> VAL + ~> CONT + + [preserves-definedness] // projections already used when reading +``` -Related code currently resides in the value-implementing module. -### Setting local variables (including error cases) +### Setting Local Variables The `#setLocalValue` operation writes a `TypedLocal` value to a given `Place` within the `List` of local variables currently on top of the stack. This may fail because a local may not be accessible, moved away, or not mutable. @@ -267,89 +390,256 @@ The `#setLocalValue` operation writes a `TypedLocal` value to a given `Place` wi [preserves-definedness] // valid list indexing checked ``` -## Evaluation of RValues +### Writing Data to Places With Projections -The `Rvalue` sort in MIR represents various operations that produce a value which can be assigned to a `Place`. - -| RValue | Arguments | Action | -|----------------|-------------------------------------------------|--------------------------------------| -| Use | Operand | use (i.e., copy) operand unmodified | -| Cast | CastKind, Operand, Ty | different kinds of type casts | -| Aggregate | Box, IndexVec | `struct`, tuple, or array | -| Repeat | Operand, Const | create array [Operand;Const] | -| Len | Place | array or slice size | -| Ref | Region, BorrowKind, Place | create reference to place | -| ThreadLocalRef | DefId | thread-local reference (?) | -| AddressOf | Mutability, Place | creates pointer to place | -|----------------|-------------------------------------------------|--------------------------------------| -| BinaryOp | BinOp, Box<(Operand, Operand)> | different fixed operations | -| NullaryOp | NullOp, Ty | on ints, bool, floats | -| UnaryOp | UnOp, Operand | (see below) | -|----------------|-------------------------------------------------|--------------------------------------| -| Discriminant | Place | discriminant (of sums types) (?) | -| ShallowInitBox | Operand, Ty | | -| CopyForDeref | Place | use (copy) contents of `Place` | - -The most basic ones are simply accessing an operand, either directly or by way of a type cast. - -```k - syntax Evaluation ::= Rvalue - - rule rvalueUse(OPERAND) => OPERAND ... - - rule rvalueCast(CASTKIND, OPERAND, TY) => #cast(OPERAND, CASTKIND, TY) ... -``` - -A number of unary and binary operations exist, (which are dependent on the operand types). +Write operations to places that include (a chain of) projections are handled by a special rewrite symbol `#projectedUpdate`. ```k -// BinaryOp, UnaryOp. NullaryOp: dependent on value representation. See below -``` + syntax KItem ::= #projectedUpdate ( WriteTo , TypedLocal, ProjectionElems, TypedLocal, Contexts , Bool ) -Other `RValue`s exist in order to construct or operate on arrays and slices, which are built into the language. + rule #setLocalValue(place(local(I), PROJ), VAL) + => + #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false) + ... + + LOCALS + requires 0 <=Int I + andBool I rvalueAggregate(KIND, ARGS) => #readOperands(ARGS) ~> #mkAggregate(KIND) ... + // stores the target of the write operation, which may change when references are dereferenced. + syntax WriteTo ::= toLocal ( Int ) + | toStack ( Int , Local ) - // #mkAggregate produces an aggregate TypedLocal value of given kind from a preceeding list of values - syntax KItem ::= #mkAggregate ( AggregateKind ) + // retains information about the value that was deconstructed by a projection + syntax Context ::= CtxField( Ty, List, Int ) + // | array context will be added here - rule ARGS:List ~> #mkAggregate(_) - => - typedValue(Aggregate(ARGS), TyUnknown, mutabilityNot) - // NB ty not determined ^^^^^^^^^ - ... - + syntax Contexts ::= List{Context, ""} + syntax TypedLocal ::= #buildUpdate ( TypedLocal, Contexts ) [function] - // #readOperands accumulates a list of `TypedLocal` values from operands - syntax KItem ::= #readOperands ( Operands ) - | #readOperandsAux( List , Operands ) - | #readOn( List, Operands ) + rule #buildUpdate(VAL, .Contexts) => VAL + [preserves-definedness] - rule #readOperands(ARGS) => #readOperandsAux(.List, ARGS) ... + rule #buildUpdate(VAL, CtxField(TY, ARGS, I) CTXS) + => #buildUpdate(typedValue(Aggregate(ARGS[I <- VAL]), TY, mutabilityMut), CTXS) + [preserves-definedness] // valid list indexing checked upon context construction - rule #readOperandsAux(ACC, .Operands ) => ACC ... + rule #projectedUpdate( + DEST, + typedValue(Aggregate(ARGS), TY, MUT), + projectionElemField(fieldIdx(I), _) PROJS, + UPDATE, + CTXTS, + FORCE + ) => + #projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, ARGS, I) CTXTS, FORCE) + ... + + requires 0 <=Int I + andBool I #readOperandsAux(ACC, OP:Operand REST) - => - OP ~> #readOn(ACC, REST) + rule #projectedUpdate( + _DEST, + typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _), + projectionElemDeref PROJS, + UPDATE, + _CTXTS, + FORCE + ) + => + #projectedUpdate( + toStack(OFFSET, LOCAL), + #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), + appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest + UPDATE, + .Contexts, // previous contexts obsolete + FORCE + ) ... - + + STACK + requires 0 VAL:TypedValue ~> #readOn(ACC, REST) - => - #readOperandsAux(ACC ListItem(VAL), REST) - ... - + rule #projectedUpdate( + _DEST, + typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), MUT), _, _), + projectionElemDeref PROJS, + UPDATE, + _CTXTS, + FORCE + ) + => + #projectedUpdate( + toLocal(I), + {LOCALS[I]}:>TypedLocal, + appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest + UPDATE, + .Contexts, // previous contexts obsolete + FORCE + ) + ... + + LOCALS + requires OFFSET ==Int 0 + andBool 0 <=Int I + andBool I #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false) + => + #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) + ... + + [preserves-definedness] // valid conmtext ensured upon context construction + + rule #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, true) + => + #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) + ... + + [preserves-definedness] // valid conmtext ensured upon context construction + + syntax KItem ::= #forceSetLocal ( Local , TypedLocal ) + + // #forceSetLocal sets the given value unconditionally (to write Moved values) + rule #forceSetLocal(local(I), VALUE) + => + .K + ... + + LOCALS => LOCALS[I <- VALUE] + requires 0 <=Int I + andBool I #projectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, _) => .K ... + STACK + => + STACK[(FRAME -Int 1) <- + #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS)) + ] + + requires 0 StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- Moved]) + requires 0 <=Int I + andBool I StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutabilityMut)]) + requires 0 <=Int I + andBool I , IndexVec | `struct`, tuple, or array | +| Repeat | Operand, Const | create array [Operand;Const] | +| Len | Place | array or slice size | +| Ref | Region, BorrowKind, Place | create reference to place | +| ThreadLocalRef | DefId | thread-local reference (?) | +| AddressOf | Mutability, Place | creates pointer to place | +|----------------|-------------------------------------------------|--------------------------------------| +| BinaryOp | BinOp, Box<(Operand, Operand)> | different fixed operations | +| NullaryOp | NullOp, Ty | on ints, bool, floats | +| UnaryOp | UnOp, Operand | (see below) | +|----------------|-------------------------------------------------|--------------------------------------| +| Discriminant | Place | discriminant (of sums types) (?) | +| ShallowInitBox | Operand, Ty | | +| CopyForDeref | Place | use (copy) contents of `Place` | + +The most basic ones are simply accessing an operand, either directly or by way of a type cast. + +```k + syntax Evaluation ::= Rvalue + + rule rvalueUse(OPERAND) => OPERAND ... + + rule rvalueCast(CASTKIND, OPERAND, TY) => #cast(OPERAND, CASTKIND, TY) ... +``` + +A number of unary and binary operations exist, (which are dependent on the operand types). + +```k +// BinaryOp, UnaryOp. NullaryOp: dependent on value representation. See below +``` + +Other `RValue`s exist in order to construct or operate on arrays and slices, which are built into the language. + +```k +// Repeat, Len: not implemented yet +``` + +Likewise built into the language are aggregates (tuples and `struct`s) and variants (`enum`s). + +Tuples and structs are built as `Aggregate` values with a list of argument values. + +```k + rule rvalueAggregate(KIND, ARGS) => #readOperands(ARGS) ~> #mkAggregate(KIND) ... + + // #mkAggregate produces an aggregate TypedLocal value of given kind from a preceeding list of values + syntax KItem ::= #mkAggregate ( AggregateKind ) + + rule ARGS:List ~> #mkAggregate(_) + => + typedValue(Aggregate(ARGS), TyUnknown, mutabilityNot) + // NB ty not determined ^^^^^^^^^ + ... + + + + // #readOperands accumulates a list of `TypedLocal` values from operands + syntax KItem ::= #readOperands ( Operands ) + | #readOperandsAux( List , Operands ) + | #readOn( List, Operands ) + + rule #readOperands(ARGS) => #readOperandsAux(.List, ARGS) ... + + rule #readOperandsAux(ACC, .Operands ) => ACC ... + + rule #readOperandsAux(ACC, OP:Operand REST) + => + OP ~> #readOn(ACC, REST) + ... + + + rule VAL:TypedValue ~> #readOn(ACC, REST) + => + #readOperandsAux(ACC ListItem(VAL), REST) + ... + // Discriminant, ShallowIntBox: not implemented yet ``` @@ -402,93 +692,8 @@ rewriting `typedLocal(...) ~> #cast(...) ~> REST` to `typedLocal(...) ~> REST`. | CastNotimplemented ( CastKind ) ``` - - - -### Decoding constants from their bytes representation to values - -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 `RigidTy` to produce the higher-level value. - -```k - ////////////////////////////////////////////////////////////////////////////////////// - // 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, _, _, _)), rigidTyBool) => BoolVal(false) - requires 0 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyBool) => BoolVal(true) - requires 1 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1 - - //////////////////////////////////////////////////////////////////////////////////////////////// - // FIXME Char and str types - // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyChar) - // => - // Str(...) - // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyStr) - // => - // Str(...) - ///////////////////////////////////////////////////////////////////////////////////////////////// - // UInt decoding - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU8)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 8, false) - requires lengthBytes(BYTES) ==Int 1 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU16)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 16, false) - requires lengthBytes(BYTES) ==Int 2 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU32)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 32, false) - requires lengthBytes(BYTES) ==Int 4 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU64)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 64, false) - requires lengthBytes(BYTES) ==Int 8 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU128)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 128, false) - requires lengthBytes(BYTES) ==Int 16 - // Usize for 64bit platforms - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyUsize)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 64, false) - requires lengthBytes(BYTES) ==Int 8 - ///////////////////////////////////////////////////////////////////////////////////////////////// - // Int decoding - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI8)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 8, true) - requires lengthBytes(BYTES) ==Int 1 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI16)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 16, true) - requires lengthBytes(BYTES) ==Int 2 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI32)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 32, true) - requires lengthBytes(BYTES) ==Int 4 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI64)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 64, true) - requires lengthBytes(BYTES) ==Int 8 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI128)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 128, true) - requires lengthBytes(BYTES) ==Int 16 - // Isize for 64bit platforms - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyIsize)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 64, true) - requires lengthBytes(BYTES) ==Int 8 - - ///////////////////////////////////////////////////////////////////////////////////////////////// - // TODO Float decoding: not supported natively in K - - rule #decodeConstant(_, _) => Any [owise] -``` -### Type casts +### Integer Type Casts Casts between signed and unsigned integral numbers of different width exist, with a truncating semantics **TODO: reference**. @@ -593,6 +798,8 @@ Error cases for `castKindIntToInt` [owise] ``` +### Other type casts + Other type casts are not implemented yet. ```k @@ -601,310 +808,93 @@ Other type casts are not implemented yet. [owise] ``` -### Projections on `TypedLocal` values - -The implementation of projections (a list `ProjectionElems`) accesses the structure of a stored value and therefore depends on the value representation. Function `#readProjection ( TypedValue , Projectionelems) -> TypedLocal` is therefore implemented in the more specific module that provides a `Value` implementation. -#### Reading data from places with projections +## Decoding constants from their bytes representation to values -The `ProjectionElems` list contains a sequence of projections which is applied (left-to-right) to the value in a `TypedLocal` to obtain a derived value or component thereof. The `TypedLocal` argument is there for the purpose of recursion over the projections. We don't expect the operation to apply to an empty projection `.ProjectionElems`, the base case exists for the recursion. +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 `RigidTy` to produce the higher-level value. ```k - // syntax KItem ::= #readProjection ( TypedValue , ProjectionElems ) - rule #readProjection(VAL, .ProjectionElems) => VAL ... -``` + syntax Value ::= #decodeConstant ( ConstantKind, RigidTy ) [function] -A `Field` access projection operates on `struct`s and tuples, which are represented as `Aggregate` values. The field is numbered from zero (in source order), and the field type is provided (not checked here). + ////////////////////////////////////////////////////////////////////////////////////// + // decoding the correct amount of bytes depending on base type size -```k - rule #readProjection( - typedValue(Aggregate(ARGS), _, _), - projectionElemField(fieldIdx(I), _TY) PROJS - ) - => - #readProjection({ARGS[I]}:>TypedValue, PROJS) - ... - - requires 0 <=Int I - andBool I #readProjection( - typedValue(Reference(0, place(local(I:Int), PLACEPROJS:ProjectionElems), _), _, _), - projectionElemDeref PROJS:ProjectionElems - ) - => - #readProjection({LOCALS[I]}:>TypedValue, appendP(PLACEPROJS, PROJS)) - ... - - LOCALS - requires 0 TAIL - rule appendP(X:ProjectionElem REST:ProjectionElems, TAIL) => X appendP(REST, TAIL) - -``` - -For references to enclosing stack frames, the local must be retrieved from the respective stack frame. -An important prerequisite of this rule is that when passing references to a callee as arguments, the stack height must be adjusted. - -```k - rule #readProjection( - typedValue(Reference(FRAME, place(LOCAL:Local, PLACEPROJS), _), _, _), - projectionElemDeref PROJS - ) - => - #readProjection( - {#localFromFrame({STACK[FRAME -Int 1]}:>StackFrame, LOCAL, FRAME)}:>TypedValue, - appendP(PLACEPROJS, PROJS) - ) - ... - - STACK - requires 0 StackFrame, LOCAL, FRAME)) - [preserves-definedness] // valid list indexing checked - - // TODO case of MovedLocal and NewLocal - - syntax TypedLocal ::= #localFromFrame ( StackFrame, Local, Int ) [function] - - rule #localFromFrame(StackFrame(... locals: LOCALS), local(I:Int), OFFSET) => #adjustRef({LOCALS[I]}:>TypedLocal, OFFSET) - requires 0 <=Int I - andBool I typedValue(Reference(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT) - rule #adjustRef(TL, _) => TL [owise] - - rule #incrementRef(TL) => #adjustRef(TL, 1) - rule #decrementRef(TL) => #adjustRef(TL, -1) -``` - -### Writing data to places with projections - -A `Deref` projection in the projections list changes the target of the write operation, while `Field` updates change the value that is being written (updating just one field of it, recursively). `Index`ing operations may have to read an index from another local, which is another rewrite. Therefore a simple update _function_ cannot cater for all projections, neither can a rewrite (the context of the recursion would need to be held explicitly). - -The solution is to use rewrite operations in a downward pass through the projections, and build the resulting updated value in an upward pass with information collected in the downward one. - -```k - syntax WriteTo ::= toLocal ( Int ) - | toStack ( Int , Local ) - - syntax KItem ::= #projectedUpdate ( WriteTo , TypedLocal, ProjectionElems, TypedLocal, Contexts , Bool ) - - syntax TypedLocal ::= #buildUpdate ( TypedLocal, Contexts ) [function] - - // retains information about the value that was deconstructed by a projection - syntax Context ::= CtxField( Ty, List, Int ) - // | array context will be added here - - syntax Contexts ::= List{Context, ""} - - rule #buildUpdate(VAL, .Contexts) => VAL - [preserves-definedness] - - rule #buildUpdate(VAL, CtxField(TY, ARGS, I) CTXS) - => #buildUpdate(typedValue(Aggregate(ARGS[I <- VAL]), TY, mutabilityMut), CTXS) - [preserves-definedness] // valid list indexing checked upon context construction - - rule #projectedUpdate( - DEST, - typedValue(Aggregate(ARGS), TY, MUT), - projectionElemField(fieldIdx(I), _) PROJS, - UPDATE, - CTXTS, - FORCE - ) => - #projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, ARGS, I) CTXTS, FORCE) - ... - - requires 0 <=Int I - andBool I #projectedUpdate( - _DEST, - typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _), - projectionElemDeref PROJS, - UPDATE, - _CTXTS, - FORCE - ) - => - #projectedUpdate( - toStack(OFFSET, LOCAL), - #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), - appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest - UPDATE, - .Contexts, // previous contexts obsolete - FORCE - ) - ... - - STACK - requires 0 #projectedUpdate( - _DEST, - typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), MUT), _, _), - projectionElemDeref PROJS, - UPDATE, - _CTXTS, - FORCE - ) - => - #projectedUpdate( - toLocal(I), - {LOCALS[I]}:>TypedLocal, - appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest - UPDATE, - .Contexts, // previous contexts obsolete - FORCE - ) - ... - - LOCALS - requires OFFSET ==Int 0 - andBool 0 <=Int I - andBool I #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false) - => - #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) - ... - - [preserves-definedness] // valid conmtext ensured upon context construction - - rule #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, true) - => - #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) - ... - - [preserves-definedness] // valid conmtext ensured upon context construction - - syntax KItem ::= #forceSetLocal ( Local , TypedLocal ) - - // #forceSetLocal sets the given value unconditionally (to write Moved values) - rule #forceSetLocal(local(I), VALUE) - => - .K - ... - - LOCALS => LOCALS[I <- VALUE] - requires 0 <=Int I - andBool I #projectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, _) => .K ... - STACK - => - STACK[(FRAME -Int 1) <- - #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS)) - ] - - requires 0 StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- Moved]) - requires 0 <=Int I - andBool I StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutabilityMut)]) - requires 0 <=Int I - andBool I #setLocalValue(place(local(I), PROJ), VAL) - => - #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false) - ... - - LOCALS - requires 0 <=Int I - andBool I operandMove(place(local(I) #as LOCAL, PROJECTIONS)) - => // read first, then write moved marker (use type from before) - #readProjection({LOCALS[I]}:>TypedValue, PROJECTIONS) ~> - #markMoved({LOCALS[I]}:>TypedLocal, LOCAL, PROJECTIONS) - ... - - LOCALS - requires PROJECTIONS =/=K .ProjectionElems - andBool 0 <=Int I - andBool I BoolVal(false) + requires 0 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyBool) => BoolVal(true) + requires 1 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1 - // TODO case of MovedLocal and NewLocal + //////////////////////////////////////////////////////////////////////////////////////////////// + // FIXME Char and str types + // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyChar) + // => + // Str(...) + // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyStr) + // => + // Str(...) + ///////////////////////////////////////////////////////////////////////////////////////////////// + // UInt decoding + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU8)) + => + Integer(Bytes2Int(BYTES, LE, Unsigned), 8, false) + requires lengthBytes(BYTES) ==Int 1 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU16)) + => + Integer(Bytes2Int(BYTES, LE, Unsigned), 16, false) + requires lengthBytes(BYTES) ==Int 2 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU32)) + => + Integer(Bytes2Int(BYTES, LE, Unsigned), 32, false) + requires lengthBytes(BYTES) ==Int 4 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU64)) + => + Integer(Bytes2Int(BYTES, LE, Unsigned), 64, false) + requires lengthBytes(BYTES) ==Int 8 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU128)) + => + Integer(Bytes2Int(BYTES, LE, Unsigned), 128, false) + requires lengthBytes(BYTES) ==Int 16 + // Usize for 64bit platforms + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyUsize)) + => + Integer(Bytes2Int(BYTES, LE, Unsigned), 64, false) + requires lengthBytes(BYTES) ==Int 8 + ///////////////////////////////////////////////////////////////////////////////////////////////// + // Int decoding + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI8)) + => + Integer(Bytes2Int(BYTES, LE, Signed), 8, true) + requires lengthBytes(BYTES) ==Int 1 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI16)) + => + Integer(Bytes2Int(BYTES, LE, Signed), 16, true) + requires lengthBytes(BYTES) ==Int 2 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI32)) + => + Integer(Bytes2Int(BYTES, LE, Signed), 32, true) + requires lengthBytes(BYTES) ==Int 4 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI64)) + => + Integer(Bytes2Int(BYTES, LE, Signed), 64, true) + requires lengthBytes(BYTES) ==Int 8 + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI128)) + => + Integer(Bytes2Int(BYTES, LE, Signed), 128, true) + requires lengthBytes(BYTES) ==Int 16 + // Isize for 64bit platforms + rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyIsize)) + => + Integer(Bytes2Int(BYTES, LE, Signed), 64, true) + requires lengthBytes(BYTES) ==Int 8 - syntax KItem ::= #markMoved ( TypedLocal, Local, ProjectionElems ) + ///////////////////////////////////////////////////////////////////////////////////////////////// + // TODO Float decoding: not supported natively in K - rule VAL:TypedLocal ~> #markMoved(OLDLOCAL, local(I), PROJECTIONS) ~> CONT - => - #projectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, Moved, .Contexts, true) - ~> VAL - ~> CONT - - [preserves-definedness] // projections already used when reading + rule #decodeConstant(_, _) => Any [owise] ``` -### Primitive operations on numeric data +## Primitive operations on numeric data The `RValue:BinaryOp` performs built-in binary operations on two operands. As [described in the `stable_mir` crate](https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/enum.Rvalue.html#variant.BinaryOp), its semantics depends on the operations and the types of operands (including variable return types). Certain operation-dependent types apply to the arguments and determine the result type. Likewise, `RValue:UnaryOp` only operates on certain operand types, notably `bool` and numeric types for arithmetic and bitwise negation. @@ -932,7 +922,7 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` rule rvalueUnaryOp(UNOP, OP1) => #applyUnOp(UNOP, OP1) ... ``` -#### Potential errors +### Potential errors ```k syntax MIRError ::= OperationError diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index afe363f72..bf6862b67 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -77,13 +77,6 @@ The local variables may be actual values (`typedValue`), uninitialised (`NewLoca rule mutabilityOf(newLocal(_, MUT)) => MUT ``` -## Functions Operating on Values in General - -```k - syntax Value ::= #decodeConstant ( ConstantKind, RigidTy ) [function] -``` -TODO this declaration should move to the call site (dispatches into special functions for different kinds of values) - ## A generic MIR Error sort ```k From 7b7eac82f6ef6018473bfd18ce66423f54997393 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 12:50:24 +1100 Subject: [PATCH 03/12] populate numbers.md (ex integer.md) with int decoding code and helpers --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 139 ++---------------- .../kmir/kdist/mir-semantics/rt/integer.md | 33 ----- .../kmir/kdist/mir-semantics/rt/numbers.md | 134 +++++++++++++++++ 3 files changed, 150 insertions(+), 156 deletions(-) delete mode 100644 kmir/src/kmir/kdist/mir-semantics/rt/integer.md create mode 100644 kmir/src/kmir/kdist/mir-semantics/rt/numbers.md diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index e12945d8c..d54ab4757 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -7,11 +7,8 @@ This module addresses all aspects of handling "values" i.e., data, at runtime du requires "../ty.md" requires "../body.md" requires "./value.md" -``` - -## Operations on local variables +requires "./numbers.md" -```k module RT-DATA imports INT imports FLOAT @@ -24,9 +21,12 @@ module RT-DATA imports TYPES imports RT-VALUE-SYNTAX + imports RT-NUMBERS imports KMIR-CONFIGURATION ``` +## Operations on local variables + ### Evaluating Items to `TypedValue` or `TypedLocal` Some built-in operations (`RValue` or type casts) use constructs that will evaluate to a value of sort `TypedValue`. @@ -711,39 +711,9 @@ bit width, signedness, and possibly truncating or 2s-complementing the value. requires #isIntType({TYPEMAP[TY]}:>RigidTy) [preserves-definedness] // ensures #numTypeOf is defined - // helpers - syntax NumTy ::= IntTy | UintTy | FloatTy - - syntax Int ::= #bitWidth( NumTy ) [function, total] - // ------------------------------ - rule #bitWidth(intTyIsize) => 64 // on 64-bit systems - rule #bitWidth(intTyI8 ) => 8 - rule #bitWidth(intTyI16 ) => 16 - rule #bitWidth(intTyI32 ) => 32 - rule #bitWidth(intTyI64 ) => 64 - rule #bitWidth(intTyI128 ) => 128 - rule #bitWidth(uintTyUsize) => 64 // on 64-bit systems - rule #bitWidth(uintTyU8 ) => 8 - rule #bitWidth(uintTyU16 ) => 16 - rule #bitWidth(uintTyU32 ) => 32 - rule #bitWidth(uintTyU64 ) => 64 - rule #bitWidth(uintTyU128 ) => 128 - rule #bitWidth(floatTyF16 ) => 16 - rule #bitWidth(floatTyF32 ) => 32 - rule #bitWidth(floatTyF64 ) => 64 - rule #bitWidth(floatTyF128) => 128 - - syntax NumTy ::= #numTypeOf( RigidTy ) [function] - // ---------------------------------------------- - rule #numTypeOf(rigidTyInt(INTTY)) => INTTY - rule #numTypeOf(rigidTyUint(UINTTY)) => UINTTY - rule #numTypeOf(rigidTyFloat(FLOATTY)) => FLOATTY - - syntax Bool ::= #isIntType ( RigidTy ) [function, total] - // ----------------------------------------------------- - rule #isIntType(rigidTyInt(_)) => true - rule #isIntType(rigidTyUint(_)) => true - rule #isIntType(_) => false [owise] + +//snip + syntax Value ::= #intAsType( Int, Int, NumTy ) [function] // ------------------------------------------------------ @@ -825,6 +795,14 @@ The `Value` sort above operates at a higher level than the bytes representation rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyBool) => 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, _, _, _)), RIGIDTY) + => + #decodeInteger(BYTES, #intTypeOf(RIGIDTY)) + requires isIntTy(RIGIDTY) + andBool lengthBytes(BYTES) ==K #bitWidth({RIGIDTY}:>InTy) /Int 8 + [preserves-definedness] + //////////////////////////////////////////////////////////////////////////////////////////////// // FIXME Char and str types // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyChar) @@ -834,59 +812,7 @@ The `Value` sort above operates at a higher level than the bytes representation // => // Str(...) ///////////////////////////////////////////////////////////////////////////////////////////////// - // UInt decoding - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU8)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 8, false) - requires lengthBytes(BYTES) ==Int 1 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU16)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 16, false) - requires lengthBytes(BYTES) ==Int 2 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU32)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 32, false) - requires lengthBytes(BYTES) ==Int 4 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU64)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 64, false) - requires lengthBytes(BYTES) ==Int 8 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyU128)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 128, false) - requires lengthBytes(BYTES) ==Int 16 - // Usize for 64bit platforms - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyUint(uintTyUsize)) - => - Integer(Bytes2Int(BYTES, LE, Unsigned), 64, false) - requires lengthBytes(BYTES) ==Int 8 - ///////////////////////////////////////////////////////////////////////////////////////////////// - // Int decoding - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI8)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 8, true) - requires lengthBytes(BYTES) ==Int 1 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI16)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 16, true) - requires lengthBytes(BYTES) ==Int 2 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI32)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 32, true) - requires lengthBytes(BYTES) ==Int 4 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI64)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 64, true) - requires lengthBytes(BYTES) ==Int 8 - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyI128)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 128, true) - requires lengthBytes(BYTES) ==Int 16 - // Isize for 64bit platforms - rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyInt(intTyIsize)) - => - Integer(Bytes2Int(BYTES, LE, Signed), 64, true) - requires lengthBytes(BYTES) ==Int 8 + ///////////////////////////////////////////////////////////////////////////////////////////////// // TODO Float decoding: not supported natively in K @@ -1136,39 +1062,6 @@ The arithmetic operations require operands of the same numeric type. requires TY1 =/=K TY2 andBool isArithmetic(BOP) [owise] - - - // helper function to truncate int values - syntax Int ::= truncate(Int, Int, Signedness) [function, total] - // ------------------------------------------------------------- - // unsigned values can be truncated using a simple bitmask - // NB if VAL is negative (underflow), the truncation will yield a positive number - rule truncate(VAL, WIDTH, Unsigned) - => // mask with relevant bits - VAL &Int ((1 < VAL // shortcut when there is nothing to do - requires 0 // if truncated value small enough and positive, all is done - (VAL &Int ((1 < // subtract a bias when the truncation result too large - (VAL &Int ((1 <=Int (1 < INTTY + rule #numTypeOf(rigidTyUint(UINTTY)) => UINTTY + rule #numTypeOf(rigidTyFloat(FLOATTY)) => FLOATTY + + syntax InTy ::= #intTypeOf( RigidTy ) [function] + // ---------------------------------------------- + rule #intTypeOf(rigidTyInt(INTTY)) => INTTY + rule #intTypeOf(rigidTyUint(UINTTY)) => UINTTY + + syntax Bool ::= #isIntType ( RigidTy ) [function, total] + // ----------------------------------------------------- + rule #isIntType(rigidTyInt(_)) => true + rule #isIntType(rigidTyUint(_)) => true + rule #isIntType(_) => false [owise] +``` + +Constants used for overflow-checking and truncation are defined here as macros. +The `#bitWidth` is defined as a function so it can be called dynamically. + +```k + syntax Int ::= #bitWidth( NumTy ) [function] + // ------------------------------ + rule #bitWidth(intTyIsize) => 64 // on 64-bit systems + rule #bitWidth(intTyI8 ) => 8 + rule #bitWidth(intTyI16 ) => 16 + rule #bitWidth(intTyI32 ) => 32 + rule #bitWidth(intTyI64 ) => 64 + rule #bitWidth(intTyI128 ) => 128 + rule #bitWidth(uintTyUsize) => 64 // on 64-bit systems + rule #bitWidth(uintTyU8 ) => 8 + rule #bitWidth(uintTyU16 ) => 16 + rule #bitWidth(uintTyU32 ) => 32 + rule #bitWidth(uintTyU64 ) => 64 + rule #bitWidth(uintTyU128 ) => 128 + rule #bitWidth(floatTyF16 ) => 16 + rule #bitWidth(floatTyF32 ) => 32 + rule #bitWidth(floatTyF64 ) => 64 + rule #bitWidth(floatTyF128) => 128 + + syntax Int ::= #maxIntValue( InTy ) [macro] + | #minIntValue( InTy ) [macro] + // --------------------------------------------------- + rule #maxIntValue( INT:IntTy ) => (1 < (1 < 0 -Int (1 < 0 + + +// use macros for bitWidth, max/min values, bit masking, and range +``` + +This truncation function is instrumental in the implementation of Integer arithmetic and overflow checking. + +```k + // helper function to truncate int values + syntax Int ::= truncate(Int, Int, Signedness) [function, total] + // ------------------------------------------------------------- + // unsigned values can be truncated using a simple bitmask + // NB if VAL is negative (underflow), the truncation will yield a positive number + rule truncate(VAL, WIDTH, Unsigned) + => // mask with relevant bits + VAL &Int ((1 < VAL // shortcut when there is nothing to do + requires 0 // if truncated value small enough and positive, all is done + (VAL &Int ((1 < // subtract a bias when the truncation result too large + (VAL &Int ((1 <=Int (1 < Integer(Bytes2Int(BYTES, LE, Signed), #bitWidth(INTTY), true) + requires lengthBytes(BYTES) ==Int #bitWidth(INTTY) /Int 8 + [preserves-definedness] + rule #decodeInteger(BYTES, UINTTY:UintTy) => Integer(Bytes2Int(BYTES, LE, Unsigned), #bitWidth(UINTTY), false) + requires lengthBytes(BYTES) ==Int #bitWidth(UINTTY) /Int 8 + [preserves-definedness] +``` + +## Type Casts Between Different Integer Types + +```k +// all castIntToInt rules, maybe under its own rewrite symbol +``` + +```k +endmodule +``` \ No newline at end of file From 0e2a6d06036ce886ea359e718c85c37037ec82af Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 13:02:46 +1100 Subject: [PATCH 04/12] fix decodeConstant call (function name and sort issue) --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index d54ab4757..834c9e4f8 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -799,8 +799,8 @@ The `Value` sort above operates at a higher level than the bytes representation rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), RIGIDTY) => #decodeInteger(BYTES, #intTypeOf(RIGIDTY)) - requires isIntTy(RIGIDTY) - andBool lengthBytes(BYTES) ==K #bitWidth({RIGIDTY}:>InTy) /Int 8 + requires #isIntType(RIGIDTY) + andBool lengthBytes(BYTES) ==K #bitWidth(#intTypeOf(RIGIDTY)) /Int 8 [preserves-definedness] //////////////////////////////////////////////////////////////////////////////////////////////// From 48bd81a16aa5594d1d770ade3c8ea31c828d6894 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 15:09:28 +1100 Subject: [PATCH 05/12] move integer cast helper function to numbers.md --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 41 +------------------ .../kmir/kdist/mir-semantics/rt/numbers.md | 38 ++++++++++++++++- 2 files changed, 37 insertions(+), 42 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 834c9e4f8..521cd756a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -696,8 +696,7 @@ rewriting `typedLocal(...) ~> #cast(...) ~> REST` to `typedLocal(...) ~> REST`. ### Integer Type Casts Casts between signed and unsigned integral numbers of different width exist, with a -truncating semantics **TODO: reference**. -These casts can only operate on the `Integer` variant of the `Value` type, adjusting +truncating semantics. These casts can only operate on the `Integer` variant of the `Value` type, adjusting bit width, signedness, and possibly truncating or 2s-complementing the value. ```k @@ -710,44 +709,6 @@ bit width, signedness, and possibly truncating or 2s-complementing the value. TYPEMAP requires #isIntType({TYPEMAP[TY]}:>RigidTy) [preserves-definedness] // ensures #numTypeOf is defined - - -//snip - - - syntax Value ::= #intAsType( Int, Int, NumTy ) [function] - // ------------------------------------------------------ - // converting to signed int types: - // narrowing or converting unsigned->signed: use truncation for signed numbers - rule #intAsType(VAL, WIDTH, INTTYPE:IntTy) - => - Integer( - truncate(VAL, #bitWidth(INTTYPE), Signed), - #bitWidth(INTTYPE), - true - ) - requires #bitWidth(INTTYPE) <=Int WIDTH - [preserves-definedness] // positive shift, divisor non-zero - - // widening: nothing to do: VAL does not change (enough bits to represent, no sign change possible) - rule #intAsType(VAL, WIDTH, INTTYPE:IntTy) - => - Integer(VAL, #bitWidth(INTTYPE), true) - requires WIDTH - Integer( - (VAL %Int (1 <signed: use truncation for signed numbers + rule #intAsType(VAL, WIDTH, INTTYPE:IntTy) + => + Integer( + truncate(VAL, #bitWidth(INTTYPE), Signed), + #bitWidth(INTTYPE), + true + ) + requires #bitWidth(INTTYPE) <=Int WIDTH + [preserves-definedness] // positive shift, divisor non-zero + + // widening: nothing to do: VAL does not change (enough bits to represent, no sign change possible) + rule #intAsType(VAL, WIDTH, INTTYPE:IntTy) + => + Integer(VAL, #bitWidth(INTTYPE), true) + requires WIDTH + Integer( + (VAL %Int (1 < Date: Fri, 28 Mar 2025 15:44:36 +1100 Subject: [PATCH 06/12] remove unused max/minIntValue, make truncate actually total --- kmir/src/kmir/kdist/mir-semantics/rt/numbers.md | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md index 81c31fef5..cb27051dd 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md @@ -62,18 +62,6 @@ The `#bitWidth` is defined as a function so it can be called dynamically. rule #bitWidth(floatTyF32 ) => 32 rule #bitWidth(floatTyF64 ) => 64 rule #bitWidth(floatTyF128) => 128 - - syntax Int ::= #maxIntValue( InTy ) [macro] - | #minIntValue( InTy ) [macro] - // --------------------------------------------------- - rule #maxIntValue( INT:IntTy ) => (1 < (1 < 0 -Int (1 < 0 - - -// use macros for bitWidth, max/min values, bit masking, and range ``` This truncation function is instrumental in the implementation of Integer arithmetic and overflow checking. @@ -82,6 +70,8 @@ This truncation function is instrumental in the implementation of Integer arithm // helper function to truncate int values syntax Int ::= truncate(Int, Int, Signedness) [function, total] // ------------------------------------------------------------- + rule truncate(_, WIDTH, _) => 0 + requires WIDTH <=Int 0 // unsigned values can be truncated using a simple bitmask // NB if VAL is negative (underflow), the truncation will yield a positive number rule truncate(VAL, WIDTH, Unsigned) From c5145f03bc6a61168349688f3777974b7b00506c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 15:45:47 +1100 Subject: [PATCH 07/12] remove unused utils.k file --- kmir/src/kmir/kdist/mir-semantics/utils.k | 56 ----------------------- 1 file changed, 56 deletions(-) delete mode 100644 kmir/src/kmir/kdist/mir-semantics/utils.k diff --git a/kmir/src/kmir/kdist/mir-semantics/utils.k b/kmir/src/kmir/kdist/mir-semantics/utils.k deleted file mode 100644 index 177e46513..000000000 --- a/kmir/src/kmir/kdist/mir-semantics/utils.k +++ /dev/null @@ -1,56 +0,0 @@ -module UTILS-SYNTAX - imports INT-SYNTAX - imports BOOL-SYNTAX - - syntax Int ::= "#width_max" "(" Int "," Bool ")" [function] // params: width, signed. Calculates maximum number for the width. - syntax Int ::= "#width_min" "(" Int "," Bool ")" [function] // params: width, signed. Calculates minimum number for the width. - syntax Int ::= "#chop" "(" Int "," Int "," Bool ")" [function] // params: number, width, signed. Wraps a number into it's bound. -endmodule - -module UTILS - imports UTILS-SYNTAX - imports INT - imports BOOL - - // Unsigned - rule #width_max(8, false) => 255 // 2^8 - 1 - rule #width_max(16, false) => 65535 // 2^16 - 1 - rule #width_max(32, false) => 4294967295 // 2^32 - 1 - rule #width_max(64, false) => 18446744073709551615 // 2^64 - 1 - rule #width_max(128, false) => 340282366920938463463374607431768211455 // 2^128 - 1 - - // Signed with two's complement - rule #width_max(8, true) => 127 // 2^(8-1) - 1 - rule #width_max(16, true) => 32767 // 2^(16-1) - 1 - rule #width_max(32, true) => 2147483647 // 2^(32-1) - 1 - rule #width_max(64, true) => 9223372036854775807 // 2^(64-1) - 1 - rule #width_max(128, true) => 170141183460469231731687303715884105727 // 2^(128-1) - 1 - - // Unsigned (Can be collapsed when width is enum) - rule #width_min(8, false) => 0 - rule #width_min(16, false) => 0 - rule #width_min(32, false) => 0 - rule #width_min(64, false) => 0 - rule #width_min(128, false) => 0 - - // Signed with two's complement - rule #width_min(8, true) => -128 // -2^(8-1) - rule #width_min(16, true) => -32768 // -2^(16-1) - rule #width_min(32, true) => -2147483648 // -2^(32-1) - rule #width_min(64, true) => -9223372036854775808 // -2^(64-1) - rule #width_min(128, true) => -170141183460469231731687303715884105728 // -2^(128-1) - - // Unsigned - rule #chop(NUM, WIDTH, false) => NUM %Int (#width_max(WIDTH, false) +Int 1) requires 0 <=Int NUM - - // Signed - rule #chop(NUM, WIDTH, true) => // chopped number stays positive if in range - NUM &Int #width_max(WIDTH, false) - requires - NUM &Int #width_max(WIDTH, false) // chopped number wraps around if too large for signed WIDTH - (NUM &Int #width_max(WIDTH, false)) -Int (#width_max(WIDTH, false) +Int 1) - requires - NUM &Int #width_max(WIDTH, false) >=Int #width_max(WIDTH, true) -endmodule \ No newline at end of file From 83e64d49aaff849a7692cf867816ee46c7d9e624 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 16:16:43 +1100 Subject: [PATCH 08/12] add some definedness annotations for casting --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 521cd756a..cbb729abe 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -720,10 +720,12 @@ Error cases for `castKindIntToInt` rule #cast(_, castKindIntToInt, TY) => UnknownCastTarget(TY, TYPEMAP) ... TYPEMAP requires notBool isRigidTy(TYPEMAP[TY]) + [preserves-definedness] rule #cast(_, castKindIntToInt, TY) => UnexpectedCastTarget(castKindIntToInt, {TYPEMAP[TY]}:>RigidTy) ... TYPEMAP requires notBool (#isIntType({TYPEMAP[TY]}:>RigidTy)) + [preserves-definedness] rule #cast(NONINT, castKindIntToInt, _TY) => UnexpectedCastArgument(NONINT, castKindIntToInt) ... [owise] From 14f16ed71b1394a80fe63637d5a0dc0be69c22e7 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 28 Mar 2025 05:36:13 +0000 Subject: [PATCH 09/12] Set Version: 0.3.110 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index dcc4cafaf..de595a283 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.108" +version = "0.3.110" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index f47ac201c..c0a87a92d 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.108' +VERSION: Final = '0.3.110' diff --git a/package/version b/package/version index c2f74cb52..14e8e2472 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.108 +0.3.110 From fd141305a0cfac045d90bdae55941166ed9f287e Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 28 Mar 2025 16:38:35 +1100 Subject: [PATCH 10/12] remove KMIR-SYNTAX module (replace by KMIR-AST) --- kmir/src/kmir/kdist/mir-semantics/kmir-ast.md | 3 +++ kmir/src/kmir/kdist/mir-semantics/kmir.md | 11 +---------- kmir/src/kmir/kdist/mir-semantics/rt/configuration.md | 2 +- kmir/src/kmir/kdist/plugin.py | 2 +- 4 files changed, 6 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md b/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md index b30fca5e7..8d1de5b6c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md @@ -16,6 +16,7 @@ module KMIR-AST imports TARGET imports TYPES + syntax Pgm ::= Symbol GlobalAllocs FunctionNames MonoItems BaseTypes [symbol(pgm), group(mir---name--allocs--functions--items--types)] @@ -32,5 +33,7 @@ module KMIR-AST syntax BaseTypes ::= List{BaseType, ""} [group(mir-list), symbol(BaseTypes::append), terminator-symbol(BaseTypes::empty)] + syntax KItem ::= #init( Pgm ) + endmodule ``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 6809d9c38..4bd18784b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -13,15 +13,6 @@ The MIR syntax is largely defined in [KMIR-AST](./kmir-ast.md) and its submodules. The execution is initialised based on a loaded `Pgm` read from a json format of stable-MIR, and the name of the function to execute. -```k -module KMIR-SYNTAX - imports KMIR-AST - - syntax KItem ::= #init( Pgm ) - -endmodule -``` - ## (Dynamic) Semantics ### Execution Configuration @@ -39,7 +30,7 @@ module KMIR-CONTROL-FLOW imports MAP imports K-EQUAL - imports KMIR-SYNTAX + imports KMIR-AST imports MONO imports TYPES diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md index 2e1c1583c..13e669065 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md @@ -17,7 +17,7 @@ Besides the `caller` (to return to) and `dest` and `target` to specify where the requires "./value.md" module KMIR-CONFIGURATION - imports KMIR-SYNTAX + imports KMIR-AST imports INT-SYNTAX imports BOOL-SYNTAX imports RT-VALUE-SYNTAX diff --git a/kmir/src/kmir/kdist/plugin.py b/kmir/src/kmir/kdist/plugin.py index c2d2f6f43..b131e040f 100644 --- a/kmir/src/kmir/kdist/plugin.py +++ b/kmir/src/kmir/kdist/plugin.py @@ -44,7 +44,7 @@ def _default_args(src_dir: Path) -> dict[str, Any]: 'include_dirs': [src_dir], 'md_selector': 'k', 'warnings_to_errors': True, - 'syntax_module': 'KMIR-SYNTAX', + 'syntax_module': 'KMIR-AST', } From 4b2380f739ec5527834a8b2262e4197e08659a39 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 28 Mar 2025 05:41:11 +0000 Subject: [PATCH 11/12] Set Version: 0.3.110 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 323f90b1a..de595a283 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.109" +version = "0.3.110" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 0e5933cd0..c0a87a92d 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.109' +VERSION: Final = '0.3.110' diff --git a/package/version b/package/version index 7b32a6e29..14e8e2472 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.109 +0.3.110 From 60e69d04e3e6adcdb424e6e4474b63a221ec4c43 Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 30 Mar 2025 23:03:53 +0000 Subject: [PATCH 12/12] Set Version: 0.3.111 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index de595a283..e8c90498b 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.110" +version = "0.3.111" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index c0a87a92d..91f6ba837 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.110' +VERSION: Final = '0.3.111' diff --git a/package/version b/package/version index 14e8e2472..766a4566d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.110 +0.3.111