From ef8bccd8960c3bac540733ca5737efc441fec20e Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 21 Mar 2025 15:46:10 +1100 Subject: [PATCH 01/12] add definedness annotation and declare buildUpdate total --- 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 4f10c9cfa..a94f5853b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -831,7 +831,7 @@ The solution is to use rewrite operations in a downward pass through the project syntax KItem ::= #projectedUpdate ( WriteTo , TypedLocal, ProjectionElems, TypedLocal, Contexts , Bool ) - syntax TypedLocal ::= #buildUpdate ( TypedLocal, Contexts ) [function] + syntax TypedLocal ::= #buildUpdate ( TypedLocal, Contexts ) [function, total] // retains information about the value that was deconstructed by a projection syntax Context ::= CtxField( Ty, List, Int ) @@ -859,7 +859,7 @@ The solution is to use rewrite operations in a downward pass through the project andBool I #projectedUpdate( _DEST, From 3c64932c34f77e5f4d63bdfb78e6dc978a02daef Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 21 Mar 2025 17:11:49 +1100 Subject: [PATCH 02/12] use heating/cooling rules for setLocalValue --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 30 ++++++++--------- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 33 +++++++++++-------- ...nt.23.state => main-a-b-with-int.21.state} | 0 ...uples.84.state => structs-tuples.90.state} | 0 .../src/tests/integration/test_integration.py | 8 ++--- 5 files changed, 36 insertions(+), 35 deletions(-) rename kmir/src/tests/integration/data/exec-smir/call-with-args/{main-a-b-with-int.23.state => main-a-b-with-int.21.state} (100%) rename kmir/src/tests/integration/data/exec-smir/structs-tuples/{structs-tuples.84.state => structs-tuples.90.state} (100%) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 1ea57c0a5..b908c4884 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -307,23 +307,12 @@ these are irrelevant at the MIR level that this semantics is modeling will effectively be no-ops at this level). ```k - - // all memory accesses relegated to another module (to be added) rule #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN)) => - RVAL ~> #assign(PLACE) + #setLocalValue(PLACE, RVAL) // RVAL evaluation is implemented in rt/data.md ... - // RVAL evaluation is implemented in rt/data.md - - syntax KItem ::= #assign ( Place ) - - rule VAL:TypedLocal ~> #assign(PLACE) ~> CONT - => - VAL ~> #setLocalValue(PLACE) ~> CONT - - rule #execStmt(statement(statementKindSetDiscriminant(_PLACE, _VARIDX), _SPAN)) => .K // FIXME! write variant index to PLACE @@ -425,7 +414,7 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l ```k rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => - #decrementRef(LOCAL0) ~> #setLocalValue(DEST) ~> #execBlockIdx(TARGET) ~> .K + #setLocalValue(DEST, #decrementRef(LOCAL0)) ~> #execBlockIdx(TARGET) ~> .K _ => CALLER // @@ -563,15 +552,22 @@ An operand may be a `Reference` (the only way a function could access another fu #setArgFromStack(IDX, OP) ~> #setArgsFromStack(IDX +Int 1, MORE) ~> CONT - rule #setArgFromStack(IDX, operandConstant(_) #as CONSTOPERAND) + rule #setArgFromStack(IDX, operandConstant(constOperand(_, _, mirConst(KIND, TY, _)))) => - #readOperand(CONSTOPERAND) ~> #setLocalValue(place(local(IDX), .ProjectionElems)) + #setLocalValue( + place(local(IDX), .ProjectionElems), + typedLocal(#decodeConstant(KIND, {TYPEMAP[TY]}:>RigidTy), TY, mutabilityNot) + ) ... + TYPEMAP + requires TY in_keys(TYPEMAP) + andBool isRigidTy(TYPEMAP[TY]) + [preserves-definedness] // valid Map lookup checked rule #setArgFromStack(IDX, operandCopy(place(local(I), .ProjectionElems))) => - #incrementRef({CALLERLOCALS[I]}:>TypedLocal) ~> #setLocalValue(place(local(IDX), .ProjectionElems)) + #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>TypedLocal)) ... ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List @@ -583,7 +579,7 @@ An operand may be a `Reference` (the only way a function could access another fu rule #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems))) => - #incrementRef({CALLERLOCALS[I]}:>TypedLocal) ~> #setLocalValue(place(local(IDX), .ProjectionElems)) + #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>TypedLocal)) ... ListItem(StackFrame(_, _, _, _, CALLERLOCALS => CALLERLOCALS[I <- Moved])) _:List diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a94f5853b..0c82a9fbe 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -239,14 +239,19 @@ Related code currently resides in the value-implementing module. The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the K sequence 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. ```k - syntax KItem ::= #setLocalValue( Place ) + syntax KItem ::= #setLocalValue( Place , Evaluation) [strict(2)] + + syntax Evaluation ::= Rvalue + | TypedLocal + + syntax KResult ::= TypedLocal // error cases first - rule _:TypedLocal ~> #setLocalValue( place(local(I) #as LOCAL, _)) => #LocalError(InvalidLocal(LOCAL)) ... + rule #setLocalValue( place(local(I) #as LOCAL, _), _) => #LocalError(InvalidLocal(LOCAL)) ... LOCALS requires size(LOCALS) <=Int I orBool I typedLocal(_, TY, _) #as VAL ~> #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems)) + rule #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems), typedLocal(_, TY, _) #as VAL) => #LocalError(TypeMismatch(LOCAL, tyOfLocal({LOCALS[I]}:>TypedLocal), VAL)) ... @@ -260,7 +265,7 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the [preserves-definedness] // list index checked before lookup // setting a local to Moved is an error - rule _:TypedLocal ~> #setLocalValue( place(local(I), _)) + rule #setLocalValue( place(local(I), _), _) => #LocalError(LocalMoved(local(I))) ... @@ -269,7 +274,7 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the requires LOCALS[I] ==K Moved // setting a non-mutable local that is initialised is an error - rule typedLocal(_, _, _) ~> #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems)) + rule #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems), typedLocal(_, _, _)) => #LocalError(LocalNotMutable(LOCAL)) ... @@ -282,15 +287,15 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the andBool notBool isNoValue({LOCALS[I]}:>TypedLocal) // noValue(_, mutabilityNot) is mutable once // writing no value is a no-op - rule noValue(_, _) ~> #setLocalValue( _) => .K ... + rule #setLocalValue( _, noValue(_, _)) => .K ... // FIXME some zero-sized values are not initialised. Otherwise we could use a special value `ZeroSized` here // writing a moved value is an error - rule Moved ~> #setLocalValue( _) => #LocalError(ValueMoved) ... + rule #setLocalValue( _, Moved) => #LocalError(ValueMoved) ... // if all is well, write the value // - rule typedLocal(VAL:Value, TY, _ ) ~> #setLocalValue(place(local(I), .ProjectionElems)) + rule #setLocalValue(place(local(I), .ProjectionElems), typedLocal(VAL:Value, TY, _ ) ) => .K ... @@ -304,7 +309,7 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the [preserves-definedness] // valid list indexing checked // special case for non-mutable uninitialised values: mutable once - rule typedLocal(VAL:Value, TY, _ ) ~> #setLocalValue(place(local(I), .ProjectionElems)) + rule #setLocalValue(place(local(I), .ProjectionElems), typedLocal(VAL:Value, TY, _ )) => .K ... @@ -915,20 +920,20 @@ The solution is to use rewrite operations in a downward pass through the project rule #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false) => - #buildUpdate(NEW, CONTEXTS) ~> #setLocalValue(place(local(I), .ProjectionElems)) + #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) ... rule #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, true) => - #buildUpdate(NEW, CONTEXTS) ~> #forceSetLocal(local(I)) + #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) ... - syntax KItem ::= #forceSetLocal ( Local ) + syntax KItem ::= #forceSetLocal ( Local , TypedLocal ) // #forceSetLocal sets the given value unconditionally (to write Moved values) - rule VALUE:TypedLocal ~> #forceSetLocal(local(I)) + rule #forceSetLocal(local(I), VALUE) => .K ... @@ -971,7 +976,7 @@ We could first read the original value using `#readProjection` and compare the t ```k - rule VAL ~> #setLocalValue(place(local(I), PROJ)) + rule #setLocalValue(place(local(I), PROJ), VAL) => #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false) ... diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.23.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.21.state similarity index 100% rename from kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.23.state rename to kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.21.state diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.84.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.90.state similarity index 100% rename from kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.84.state rename to kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.90.state diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index fcdd5f910..bf5880d82 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -225,8 +225,8 @@ def test_schema_kapply_parse( ( 'call-with-args', EXEC_DATA_DIR / 'call-with-args' / 'main-a-b-with-int.smir.json', - EXEC_DATA_DIR / 'call-with-args' / 'main-a-b-with-int.23.state', - 23, + EXEC_DATA_DIR / 'call-with-args' / 'main-a-b-with-int.21.state', + 21, ), ( 'assign-cast', @@ -237,8 +237,8 @@ def test_schema_kapply_parse( ( 'structs-tuples', EXEC_DATA_DIR / 'structs-tuples' / 'structs-tuples.smir.json', - EXEC_DATA_DIR / 'structs-tuples' / 'structs-tuples.84.state', - 84, + EXEC_DATA_DIR / 'structs-tuples' / 'structs-tuples.90.state', + 90, ), ( 'struct-field-update', From e0d20cf08cbf72bc36c255cd8fb0c8c69bf6ab4e Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 21 Mar 2025 19:03:08 +1100 Subject: [PATCH 03/12] introduce separate sorts for MIRError and Projection --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 26 +++++++++++--------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 0c82a9fbe..8faa3aa6b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -20,6 +20,8 @@ module RT-DATA-SYNTAX syntax Value syntax Value ::= #decodeConstant ( ConstantKind, RigidTy ) [function] + + syntax MIRError ``` ### Local variables @@ -44,6 +46,7 @@ with their type information (to enable type-checking assignments). Also, the // accessors syntax Bool ::= hasValue ( TypedLocal ) [function, total] | isNoValue ( TypedLocal ) [function, total] + rule hasValue(typedLocal(_, _, _)) => true rule hasValue(Moved) => false rule hasValue(noValue(_, _)) => false @@ -52,7 +55,12 @@ with their type information (to enable type-checking assignments). Also, the rule isNoValue(Moved) => false rule isNoValue(noValue(_, _)) => true + syntax Value ::= valueOf ( TypedLocal ) [function] // partial, requires hasValue(T) + + rule valueOf(typedLocal(V, _, _)) => V + syntax MaybeTy ::= tyOfLocal ( TypedLocal ) [function, total] + rule tyOfLocal(typedLocal(_, TY, _)) => TY rule tyOfLocal(Moved) => TyUnknown rule tyOfLocal(noValue(TY, _)) => TY @@ -78,7 +86,7 @@ Every access is modelled as a _function_ whose result needs to be checked by the | "ValueMoved" | Unsupported ( String ) // draft code - syntax KItem ::= #LocalError ( LocalAccessError ) + syntax MIRError ::= #LocalError ( LocalAccessError ) endmodule ``` @@ -212,7 +220,7 @@ further access. Apart from that, the same caveats apply as for operands that are 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). ```k - syntax KItem ::= #readProjection ( TypedLocal , ProjectionElems ) + syntax Projected ::= #readProjection ( TypedLocal , ProjectionElems ) rule #readOperand(operandCopy(place(local(I), PROJECTIONS))) => @@ -242,6 +250,7 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the syntax KItem ::= #setLocalValue( Place , Evaluation) [strict(2)] syntax Evaluation ::= Rvalue + | Projected | TypedLocal syntax KResult ::= TypedLocal @@ -348,8 +357,11 @@ The `RValue` sort in MIR represents various operations that produce a value whic | 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. +Type casts between a number of different types exist in MIR. ```k + syntax KItem ::= #cast( CastKind, Ty ) // TODO make this an Evaluation subsort + rule rvalueUse(OPERAND) => #readOperand(OPERAND) ... rule rvalueCast(CASTKIND, OPERAND, TY) => #readOperand(OPERAND) ~> #cast(CASTKIND, TY) ... @@ -440,15 +452,7 @@ A `CopyForDeref` `RValue` has the semantics of a simple `Use(operandCopy(...))`, // AddressOf: not implemented yet ``` -## Type casts - -Type casts between a number of different types exist in MIR. We implement a type -cast from a `TypedLocal` to another when it is followed by a `#cast` item, -rewriting `typedLocal(...) ~> #cast(...) ~> REST` to `typedLocal(...) ~> REST`. - ```k - syntax KItem ::= #cast( CastKind, Ty ) - endmodule ``` @@ -1076,7 +1080,7 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` #### Potential errors ```k - syntax KItem ::= #OperationError( OperationError ) + syntax MIRError ::= #OperationError( OperationError ) syntax OperationError ::= TypeMismatch ( BinOp, Ty, Ty ) | OperandMismatch ( BinOp, Value, Value ) From e4d9d7e75187da41896014ca24373f3f554333a5 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 21 Mar 2025 19:33:14 +1100 Subject: [PATCH 04/12] WIP using Value type for computing binops --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 101 +++++++------------ 1 file changed, 38 insertions(+), 63 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 8faa3aa6b..32afc8c43 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -740,10 +740,11 @@ The implementation of projections (a list `ProjectionElems`) accesses the struct #### Reading data from places with projections -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 `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. This is a subsort of `Evaluation` and will ultimately produce a `TypedValue`. +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. ```k - // syntax KItem ::= #readProjection ( TypedLocal , ProjectionElems ) + // syntax Projected ::= #readProjection ( TypedLocal , ProjectionElems ) rule #readProjection(TL, .ProjectionElems) => TL ... ``` @@ -791,7 +792,8 @@ In the simplest case, the reference refers to a local in the same stack frame (h ``` 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. +An important prerequisite of this rule is that when passing references to a callee as arguments, the stack height must be adjusted +(NB this is done automatically in the `#localFromFrame` function using its 3rd argument). ```k rule #readProjection( @@ -824,6 +826,7 @@ An important prerequisite of this rule is that when passing references to a call => typedLocal(Reference(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT) rule #adjustRef(TL, _) => TL [owise] + // for the common case of passing references as function arguments and return values rule #incrementRef(TL) => #adjustRef(TL, 1) rule #decrementRef(TL) => #adjustRef(TL, -1) ``` @@ -957,6 +960,7 @@ The solution is to use rewrite operations in a downward pass through the project requires 0 rvalueBinaryOp(BINOP, OP1, OP2) => @@ -1052,15 +1057,15 @@ For binary operations generally, both arguments have to be read from the provide ... - rule ARG1:TypedLocal ~> #suspend(BINOP, OP2, CHECKFLAG) + rule typedLocal(VAL1, _, _) ~> #suspend(BINOP, OP2, CHECKFLAG) => - #readOperand(OP2) ~> #ready(BINOP, ARG1, CHECKFLAG) + #readOperand(OP2) ~> #ready(BINOP, VAL1, CHECKFLAG) ... - rule ARG2:TypedLocal ~> #ready(BINOP, ARG1,CHECKFLAG) + rule typedLocal(VAL2, _, _) ~> #ready(BINOP, VAL1, CHECKFLAG) => - #compute(BINOP, ARG1, ARG2, CHECKFLAG) + #compute(BINOP, VAL1, VAL2, CHECKFLAG) ... ``` @@ -1068,7 +1073,7 @@ For binary operations generally, both arguments have to be read from the provide There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata`) used in `RValue:UnaryOp`. These operations only read a single operand and do not need a `#suspend` helper. ```k - syntax KItem ::= #applyUnOp ( UnOp ) + syntax Evaluation ::= #applyUnOp ( UnOp ) rule rvalueUnaryOp(UNOP, OP1) => @@ -1082,25 +1087,21 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` ```k syntax MIRError ::= #OperationError( OperationError ) + syntax Evaluation ::= OperationError + syntax OperationError ::= TypeMismatch ( BinOp, Ty, Ty ) | OperandMismatch ( BinOp, Value, Value ) | OperandError( BinOp, TypedLocal, TypedLocal) | OperandMismatch ( UnOp, Value ) | OperandError( UnOp, TypedLocal) // errors above are compiler bugs or invalid MIR - | Unimplemented ( BinOp, TypedLocal, TypedLocal) + | Unimplemented ( BinOp, Value, Value) // errors below are program errors | "DivisionByZero" | "Overflow_U_B" // better than getting stuck - // catch pathological cases where ARG1 or ARG2, or both, are Moved or NoValue. - rule #compute(OP, ARG1, ARG2, _FLAG) => #OperationError(OperandError(OP, ARG1, ARG2)) - requires notBool (hasValue(ARG1) andBool hasValue(ARG2)) - // catch-all rule to make `#compute` total - rule #compute(OP, ARG1, ARG2, _FLAG) - => - #OperationError(Unimplemented(OP, ARG1, ARG2)) + rule #compute(OP, ARG1, ARG2, _FLAG) => Unimplemented(OP, ARG1, ARG2) [owise] ``` @@ -1147,32 +1148,19 @@ The arithmetic operations require operands of the same numeric type. requires Y =/=Int 0 // operation undefined otherwise - rule #compute( - BOP, - typedLocal(Integer(ARG1, WIDTH, SIGNEDNESS), TY, _), - typedLocal(Integer(ARG2, WIDTH, SIGNEDNESS), TY, _), - CHK) - => - #arithmeticInt(BOP, ARG1, ARG2, WIDTH, SIGNEDNESS, TY, CHK) + rule #compute(BOP, Integer(ARG1, WIDTH, SIGNEDNESS), Integer(ARG2, WIDTH, SIGNEDNESS), CHK) + => + #arithmeticInt(BOP, ARG1, ARG2, WIDTH, SIGNEDNESS, TY, CHK) requires isArithmetic(BOP) [preserves-definedness] - // error cases: - // non-scalar arguments - rule #compute(BOP, typedLocal(ARG1, TY, _), typedLocal(ARG2, TY, _), _) + // error case: non-numeric arguments + rule #compute(BOP, ARG1, ARG2, _) => - #OperationError(OperandMismatch(BOP, ARG1, ARG2)) + OperandMismatch(BOP, ARG1, ARG2) requires isArithmetic(BOP) [owise] - // different argument types - rule #compute(BOP, typedLocal(_, TY1, _), typedLocal(_, TY2, _), _) - => - #OperationError(TypeMismatch(BOP, TY1, TY2)) - requires TY1 =/=K TY2 - andBool isArithmetic(BOP) - [owise] - // helper function to truncate int values syntax Int ::= truncate(Int, Int, Signedness) [function, total] // ------------------------------------------------------------- @@ -1199,8 +1187,8 @@ The arithmetic operations require operands of the same numeric type. [preserves-definedness] // perform arithmetic operations on integral types of given width - syntax KItem ::= #arithmeticInt ( BinOp, Int , Int, Int, Bool, Ty, Bool ) [function] - // arg1 arg2 width signedness result overflowcheck + syntax Evaluation ::= #arithmeticInt ( BinOp, Int , Int, Int, Bool, Ty, Bool ) [function] + // arg1 arg2 width signedness result overflowcheck // signed numbers: must check for wrap-around (operation specific) rule #arithmeticInt(BOP, ARG1, ARG2, WIDTH, true, TY, true) => @@ -1270,32 +1258,24 @@ The arithmetic operations require operands of the same numeric type. andBool truncate(onInt(BOP, ARG1, ARG2), WIDTH, Unsigned) ==Int onInt(BOP, ARG1, ARG2) [preserves-definedness] - rule #arithmeticInt(BOP, _, _, _, _, _, false) => #OperationError(Overflow_U_B) + rule #arithmeticInt(BOP, _, _, _, _, _, false) => Overflow_U_B requires isArithmetic(BOP) [owise] // These are additional high priority rules to detect/report divbyzero and div/rem overflow/underflow // (the latter can only happen for signed Ints with dividend minInt and divisor -1 - rule #arithmeticInt(binOpDiv, _, DIVISOR, _, _, _, _) - => - #OperationError(DivisionByZero) + rule #arithmeticInt(binOpDiv, _, DIVISOR, _, _, _, _) => DivisionByZero requires DIVISOR ==Int 0 [priority(40)] - rule #arithmeticInt(binOpRem, _, DIVISOR, _, _, _, _) - => - #OperationError(DivisionByZero) + rule #arithmeticInt(binOpRem, _, DIVISOR, _, _, _, _) => DivisionByZero requires DIVISOR ==Int 0 [priority(40)] - rule #arithmeticInt(binOpDiv, DIVIDEND, DIVISOR, WIDTH, true, _, _) - => - #OperationError(Overflow_U_B) + rule #arithmeticInt(binOpDiv, DIVIDEND, DIVISOR, WIDTH, true, _, _) => Overflow_U_B requires DIVISOR ==Int -1 andBool DIVIDEND ==Int 0 -Int (1 < - #OperationError(Overflow_U_B) + rule #arithmeticInt(binOpRem, DIVIDEND, DIVISOR, WIDTH, true, _, _) => Overflow_U_B requires DIVISOR ==Int -1 andBool DIVIDEND ==Int 0 -Int (1 < cmpOpBool(binOpLe, Y, X) rule cmpOpBool(binOpGt, X, Y) => cmpOpBool(binOpLt, Y, X) - rule #compute(OP, typedLocal(_, TY, _), typedLocal(_, TY2, _), _) => #OperationError(TypeMismatch(OP, TY, TY2)) - requires isComparison(OP) - andBool TY =/=K TY2 - - rule #compute(OP, typedLocal(Integer(VAL1, WIDTH, SIGN), TY, _), typedLocal(Integer(VAL2, WIDTH, SIGN), TY, _), _) + rule #compute(OP, Integer(VAL1, WIDTH, SIGN), Integer(VAL2, WIDTH, SIGN), _) => typedLocal(BoolVal(cmpOpInt(OP, VAL1, VAL2)), TyUnknown, mutabilityNot) requires isComparison(OP) - rule #compute(OP, typedLocal(BoolVal(VAL1), TY, _), typedLocal(BoolVal(VAL2), TY, _), _) + rule #compute(OP, BoolVal(VAL1), BoolVal(VAL2), _) => typedLocal(BoolVal(cmpOpBool(OP, VAL1, VAL2)), TyUnknown, mutabilityNot) requires isComparison(OP) - rule #compute(OP, typedLocal(ARG1, TY, _), typedLocal(ARG2, TY, _), _) - => - #OperationError(OperandMismatch(OP, ARG1, ARG2)) + rule #compute(OP, ARG1, ARG2, _) => OperandMismatch(OP, ARG1, ARG2) [owise] ``` The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `std::cmp::Ordering as i8`), indicating `LE`, `EQ`, or `GT`. ```k + // FIXME this should be a custom `Ordering` type instead (must be hard-wired) syntax Int ::= cmpInt ( Int , Int ) [function , total] | cmpBool ( Bool, Bool ) [function , total] rule cmpInt(VAL1, VAL2) => -1 requires VAL1 0 requires X ==Bool Y rule cmpBool(X, Y) => 1 requires X andBool notBool Y - rule #compute(binOpCmp, typedLocal(Integer(VAL1, WIDTH, SIGN), TY, _), typedLocal(Integer(VAL2, WIDTH, SIGN), TY, _), _) + rule #compute(binOpCmp, Integer(VAL1, WIDTH, SIGN), Integer(VAL2, WIDTH, SIGN), _) => typedLocal(Integer(cmpInt(VAL1, VAL2), 8, true), TyUnknown, mutabilityNot) - rule #compute(binOpCmp, typedLocal(BoolVal(VAL1), TY, _), typedLocal(BoolVal(VAL2), TY, _), _) + rule #compute(binOpCmp, BoolVal(VAL1), BoolVal(VAL2), _) => typedLocal(Integer(cmpBool(VAL1, VAL2), 8, true), TyUnknown, mutabilityNot) From 63032e8b1550f070d2a8c1ffe7cf040bd0586570 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 21 Mar 2025 20:12:13 +1100 Subject: [PATCH 05/12] fix rules, pass type information to #compute --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 41 ++++++++++++-------- 1 file changed, 25 insertions(+), 16 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 32afc8c43..991306b2c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1041,9 +1041,9 @@ For binary operations generally, both arguments have to be read from the provide ```k syntax KItem ::= #suspend ( BinOp, Operand, Bool) - | #ready ( BinOp, Value, Bool ) + | #ready ( BinOp, Value, Ty, Bool ) - syntax Evaluation ::= #compute ( BinOp, Value, Value, Bool ) [function, total] + syntax Evaluation ::= #compute ( BinOp, Value, Ty, Value, Ty, Bool ) [function, total] rule rvalueBinaryOp(BINOP, OP1, OP2) => @@ -1057,15 +1057,15 @@ For binary operations generally, both arguments have to be read from the provide ... - rule typedLocal(VAL1, _, _) ~> #suspend(BINOP, OP2, CHECKFLAG) + rule typedLocal(VAL1, TY1, _) ~> #suspend(BINOP, OP2, CHECKFLAG) => - #readOperand(OP2) ~> #ready(BINOP, VAL1, CHECKFLAG) + #readOperand(OP2) ~> #ready(BINOP, VAL1, TY1, CHECKFLAG) ... - rule typedLocal(VAL2, _, _) ~> #ready(BINOP, VAL1, CHECKFLAG) + rule typedLocal(VAL2, TY2, _) ~> #ready(BINOP, VAL1, TY1, CHECKFLAG) => - #compute(BINOP, VAL1, VAL2, CHECKFLAG) + #compute(BINOP, VAL1, TY1, VAL2, TY2, CHECKFLAG) ... ``` @@ -1101,7 +1101,7 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` | "Overflow_U_B" // better than getting stuck // catch-all rule to make `#compute` total - rule #compute(OP, ARG1, ARG2, _FLAG) => Unimplemented(OP, ARG1, ARG2) + rule #compute(OP, ARG1, _TY1, ARG2, _TY2, _FLAG) => Unimplemented(OP, ARG1, ARG2) [owise] ``` @@ -1148,14 +1148,20 @@ The arithmetic operations require operands of the same numeric type. requires Y =/=Int 0 // operation undefined otherwise - rule #compute(BOP, Integer(ARG1, WIDTH, SIGNEDNESS), Integer(ARG2, WIDTH, SIGNEDNESS), CHK) + rule #compute(BOP, Integer(ARG1, WIDTH, SIGNEDNESS), TY, Integer(ARG2, WIDTH, SIGNEDNESS), TY, CHK) => #arithmeticInt(BOP, ARG1, ARG2, WIDTH, SIGNEDNESS, TY, CHK) requires isArithmetic(BOP) [preserves-definedness] - // error case: non-numeric arguments - rule #compute(BOP, ARG1, ARG2, _) + // error cases: + rule #compute(BOP, _, TY1, _, TY2, _) + => + TypeMismatch(BOP, TY1, TY2) + requires isArithmetic(BOP) + andBool TY1 =/=K TY2 + + rule #compute(BOP, ARG1, _, ARG2, _, _) => OperandMismatch(BOP, ARG1, ARG2) requires isArithmetic(BOP) @@ -1314,17 +1320,21 @@ All operations except `binOpCmp` return a `BoolVal`. The argument types must be rule cmpOpBool(binOpGe, X, Y) => cmpOpBool(binOpLe, Y, X) rule cmpOpBool(binOpGt, X, Y) => cmpOpBool(binOpLt, Y, X) - rule #compute(OP, Integer(VAL1, WIDTH, SIGN), Integer(VAL2, WIDTH, SIGN), _) + rule #compute(OP, Integer(VAL1, WIDTH, SIGN), TY, Integer(VAL2, WIDTH, SIGN), TY, _) => typedLocal(BoolVal(cmpOpInt(OP, VAL1, VAL2)), TyUnknown, mutabilityNot) requires isComparison(OP) - rule #compute(OP, BoolVal(VAL1), BoolVal(VAL2), _) + rule #compute(OP, BoolVal(VAL1), TY, BoolVal(VAL2), TY, _) => typedLocal(BoolVal(cmpOpBool(OP, VAL1, VAL2)), TyUnknown, mutabilityNot) requires isComparison(OP) - rule #compute(OP, ARG1, ARG2, _) => OperandMismatch(OP, ARG1, ARG2) + rule #compute(OP, _, TY1, _, TY2, _) => TypeMismatch(OP, TY1, TY2) + requires (isComparison(OP) orBool OP ==K binOpCmp) + andBool TY1 =/=K TY2 + + rule #compute(OP, ARG1, _, ARG2, _, _) => OperandMismatch(OP, ARG1, ARG2) [owise] ``` @@ -1342,14 +1352,13 @@ The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `st rule cmpBool(X, Y) => 0 requires X ==Bool Y rule cmpBool(X, Y) => 1 requires X andBool notBool Y - rule #compute(binOpCmp, Integer(VAL1, WIDTH, SIGN), Integer(VAL2, WIDTH, SIGN), _) + rule #compute(binOpCmp, Integer(VAL1, WIDTH, SIGN), TY, Integer(VAL2, WIDTH, SIGN), TY, _) => typedLocal(Integer(cmpInt(VAL1, VAL2), 8, true), TyUnknown, mutabilityNot) - rule #compute(binOpCmp, BoolVal(VAL1), BoolVal(VAL2), _) + rule #compute(binOpCmp, BoolVal(VAL1), TY, BoolVal(VAL2), TY, _) => typedLocal(Integer(cmpBool(VAL1, VAL2), 8, true), TyUnknown, mutabilityNot) - ``` #### Unary operations on Boolean and integral values From 73f2f26827a594622604bf5fd3cc4f294f91b619 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 21 Mar 2025 09:19:31 +0000 Subject: [PATCH 06/12] Set Version: 0.3.100 --- 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 a29f2a860..a954c6075 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.99" +version = "0.3.100" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 2f6fb6b06..8d2bd08cc 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.99' +VERSION: Final = '0.3.100' diff --git a/package/version b/package/version index 85ea6eaf6..72280e8da 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.99 +0.3.100 From 39d177483cc490963bbaa134d77ca945d557a44b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 24 Mar 2025 11:21:26 +1100 Subject: [PATCH 07/12] Use separate result type (only TypedLocal and Errors) --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 991306b2c..d0df52468 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -251,9 +251,11 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the syntax Evaluation ::= Rvalue | Projected - | TypedLocal + | EvalResult - syntax KResult ::= TypedLocal + syntax KResult ::= EvalResult + + syntax EvalResult ::= TypedLocal // error cases first rule #setLocalValue( place(local(I) #as LOCAL, _), _) => #LocalError(InvalidLocal(LOCAL)) ... @@ -1043,7 +1045,7 @@ For binary operations generally, both arguments have to be read from the provide syntax KItem ::= #suspend ( BinOp, Operand, Bool) | #ready ( BinOp, Value, Ty, Bool ) - syntax Evaluation ::= #compute ( BinOp, Value, Ty, Value, Ty, Bool ) [function, total] + syntax EvalResult ::= #compute ( BinOp, Value, Ty, Value, Ty, Bool ) [function, total] rule rvalueBinaryOp(BINOP, OP1, OP2) => @@ -1073,7 +1075,7 @@ For binary operations generally, both arguments have to be read from the provide There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata`) used in `RValue:UnaryOp`. These operations only read a single operand and do not need a `#suspend` helper. ```k - syntax Evaluation ::= #applyUnOp ( UnOp ) + syntax EvalResult ::= #applyUnOp ( UnOp ) rule rvalueUnaryOp(UNOP, OP1) => @@ -1087,7 +1089,7 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` ```k syntax MIRError ::= #OperationError( OperationError ) - syntax Evaluation ::= OperationError + syntax EvalResult ::= OperationError syntax OperationError ::= TypeMismatch ( BinOp, Ty, Ty ) | OperandMismatch ( BinOp, Value, Value ) @@ -1193,7 +1195,7 @@ The arithmetic operations require operands of the same numeric type. [preserves-definedness] // perform arithmetic operations on integral types of given width - syntax Evaluation ::= #arithmeticInt ( BinOp, Int , Int, Int, Bool, Ty, Bool ) [function] + syntax EvalResult ::= #arithmeticInt ( BinOp, Int , Int, Int, Bool, Ty, Bool ) [function] // arg1 arg2 width signedness result overflowcheck // signed numbers: must check for wrap-around (operation specific) rule #arithmeticInt(BOP, ARG1, ARG2, WIDTH, true, TY, true) From 7b40bcde16c0948c6c901edd70b6559d01da8905 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 24 Mar 2025 12:22:27 +1100 Subject: [PATCH 08/12] distinguish moved and uninitialised locals by sort --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 8 +- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 98 ++++++++------------ 2 files changed, 43 insertions(+), 63 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index b908c4884..bc2aee94f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -408,13 +408,16 @@ value is the value in local `_0`, and will go to the _destination_ in the `LOCALS` of the caller's stack frame. Execution continues with the context of the enclosing stack frame, at the _target_. +If the returned value is not initialised ( `NewValue`), the write is skipped. If the returned value is a `Reference`, its stack height must be decremented because a stack frame is popped. NB that a stack height of `0` cannot occur here, because the compiler prevents local variable references from escaping. ```k rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => - #setLocalValue(DEST, #decrementRef(LOCAL0)) ~> #execBlockIdx(TARGET) ~> .K + #if isLocalValue(LOCAL0) #then #setLocalValue(DEST, #decrementRef(LOCAL0)) #else .K #fi + ~> #execBlockIdx(TARGET) + ~> .K _ => CALLER // @@ -429,8 +432,7 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK FUNCS requires CALLER in_keys(FUNCS) - // andBool DEST #within(LOCALS) - [preserves-definedness] // CALLER lookup defined, DEST within locals TODO + [preserves-definedness] // CALLER lookup defined, DEST within locals checked by write syntax List ::= #getBlocks(Map, Ty) [function] | #getBlocksAux(MonoItemKind) [function, total] diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index d0df52468..5c44217b0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -34,9 +34,13 @@ with their type information (to enable type-checking assignments). Also, the // local storage of the stack frame // syntax TypedLocals ::= List {TypedLocal, ","} but then we lose size, update, indexing - syntax TypedLocal ::= typedLocal ( Value, MaybeTy, Mutability ) // regular value - | "Moved" // inaccessible - | noValue ( Ty, Mutability ) // not initialised + syntax TypedLocal ::= MovedLocal | NewLocal | LocalValue + + syntax LocalValue ::= typedLocal ( Value, MaybeTy, Mutability ) // regular value + + syntax MovedLocal ::= "Moved" // inaccessible local + + syntax NewLocal ::= noValue ( Ty, Mutability) // not initialised // 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. @@ -44,33 +48,17 @@ with their type information (to enable type-checking assignments). Also, the | "TyUnknown" // accessors - syntax Bool ::= hasValue ( TypedLocal ) [function, total] - | isNoValue ( TypedLocal ) [function, total] - - rule hasValue(typedLocal(_, _, _)) => true - rule hasValue(Moved) => false - rule hasValue(noValue(_, _)) => false - - rule isNoValue(typedLocal(_, _, _)) => false - rule isNoValue(Moved) => false - rule isNoValue(noValue(_, _)) => true - - syntax Value ::= valueOf ( TypedLocal ) [function] // partial, requires hasValue(T) - - rule valueOf(typedLocal(V, _, _)) => V - syntax MaybeTy ::= tyOfLocal ( TypedLocal ) [function, total] - + // ------------------------------------------------------- rule tyOfLocal(typedLocal(_, TY, _)) => TY rule tyOfLocal(Moved) => TyUnknown rule tyOfLocal(noValue(TY, _)) => TY - syntax Bool ::= isMutable ( TypedLocal ) [function, total] - rule isMutable(typedLocal(_, _, mutabilityMut)) => true - rule isMutable(typedLocal(_, _, mutabilityNot)) => false - rule isMutable(Moved) => false - rule isMutable(noValue(_, mutabilityMut)) => true - rule isMutable(noValue(_, mutabilityNot)) => false + syntax Mutability ::= mutability ( TypedLocal ) [function, total] + // ------------------------------------------------------- + rule mutability(typedLocal(_, _, MUT)) => MUT + rule mutability(Moved) => mutabilityNot + rule mutability(noValue(_, MUT)) => MUT ``` Access to a `TypedLocal` (whether reading or writing( may fail for a number of reasons. @@ -144,8 +132,7 @@ local value cannot be read, though, and the value should be initialised. LOCALS requires 0 <=Int I andBool I TypedLocal) + andBool isLocalValue(LOCALS[I]) [preserves-definedness] // valid list indexing checked rule #readOperand(operandCopy(place(local(I) #as LOCAL, .ProjectionElems))) @@ -154,9 +141,9 @@ local value cannot be read, though, and the value should be initialised. ... LOCALS - requires LOCALS[I] ==K Moved - andBool 0 <=Int I + requires 0 <=Int I andBool I #readOperand(operandCopy(place(local(I), .ProjectionElems))) @@ -165,10 +152,9 @@ local value cannot be read, though, and the value should be initialised. ... LOCALS - requires isNoValue({LOCALS[I]}:>TypedLocal) + requires 0 <=Int I andBool I LOCALS => LOCALS[I <- Moved] - requires hasValue({LOCALS[I]}:>TypedLocal) - andBool 0 <=Int I + requires 0 <=Int I andBool I #readOperand(operandMove(place(local(I) #as LOCAL, .ProjectionElems))) @@ -195,9 +180,9 @@ further access. Apart from that, the same caveats apply as for operands that are ... LOCALS - requires LOCALS[I] ==K Moved - andBool 0 <=Int I + requires 0 <=Int I andBool I #readOperand(operandMove(place(local(I), .ProjectionElems))) @@ -206,10 +191,9 @@ further access. Apart from that, the same caveats apply as for operands that are ... LOCALS - requires isNoValue({LOCALS[I]}:>TypedLocal) - andBool 0 <=Int I + requires 0 <=Int I andBool I TypedLocal) + andBool isLocalValue(LOCALS[I]) [preserves-definedness] // valid list indexing checked ``` @@ -251,11 +234,12 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the syntax Evaluation ::= Rvalue | Projected + | TypedLocal | EvalResult syntax KResult ::= EvalResult - syntax EvalResult ::= TypedLocal + syntax EvalResult ::= LocalValue // error cases first rule #setLocalValue( place(local(I) #as LOCAL, _), _) => #LocalError(InvalidLocal(LOCAL)) ... @@ -282,7 +266,10 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the ... LOCALS - requires LOCALS[I] ==K Moved + requires I #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems), typedLocal(_, _, _)) @@ -293,16 +280,9 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the LOCALS requires I TypedLocal) // not mutable - andBool notBool isNoValue({LOCALS[I]}:>TypedLocal) // noValue(_, mutabilityNot) is mutable once - - // writing no value is a no-op - rule #setLocalValue( _, noValue(_, _)) => .K ... - // FIXME some zero-sized values are not initialised. Otherwise we could use a special value `ZeroSized` here - - // writing a moved value is an error - rule #setLocalValue( _, Moved) => #LocalError(ValueMoved) ... + andBool isLocalValue(LOCALS[I]) + andBool mutability({LOCALS[I]}:>TypedLocal) ==K mutabilityNot + [preserves-definedness] // valid list indexing checked // if all is well, write the value // @@ -314,9 +294,9 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the LOCALS => LOCALS[I <- typedLocal(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutabilityMut)] requires 0 <=Int I andBool I TypedLocal) ==K TY orBool TY ==K TyUnknown) // matching or unknown type - andBool isMutable({LOCALS[I]}:>TypedLocal) // mutable + andBool mutability({LOCALS[I]}:>TypedLocal) ==K mutabilityMut [preserves-definedness] // valid list indexing checked // special case for non-mutable uninitialised values: mutable once @@ -325,13 +305,11 @@ The `#setLocalValue` operation writes a `TypedLocal` value preceeding it in the .K ... - LOCALS => LOCALS[I <- typedLocal(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutabilityNot)] + LOCALS => LOCALS[I <- typedLocal(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutability({LOCALS[I]}:>TypedLocal))] requires 0 <=Int I andBool I TypedLocal) ==K TY orBool TY ==K TyUnknown) // matching or unknown type - andBool notBool isMutable({LOCALS[I]}:>TypedLocal) // not mutable but - andBool isNoValue({LOCALS[I]}:>TypedLocal) // not initialised yet [preserves-definedness] // valid list indexing checked ``` From 4e30d491b630c23402d881f28c515966835c7c84 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 24 Mar 2025 05:39:09 +0000 Subject: [PATCH 09/12] Set Version: 0.3.103 --- 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 ac5ce6b16..7e487ea32 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.102" +version = "0.3.103" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index d86960dcd..cfdb78e48 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.102' +VERSION: Final = '0.3.103' diff --git a/package/version b/package/version index 27d5f4a6e..b73ea9581 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.102 +0.3.103 From 5c00aaab9b177efc82fd2e162866ddde1b41e1da Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 24 Mar 2025 20:08:09 +1100 Subject: [PATCH 10/12] specialise #adjustRef to LocalValue sort --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 12 +++++------- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 10 +++++----- 2 files changed, 10 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 154451e33..8732836fa 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -416,7 +416,7 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l ```k rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => - #if isLocalValue(LOCAL0) #then #setLocalValue(DEST, #decrementRef(LOCAL0)) #else .K #fi + #if isLocalValue(LOCAL0) #then #setLocalValue(DEST, #decrementRef({LOCAL0}:>LocalValue)) #else .K #fi ~> #execBlockIdx(TARGET) ~> .K @@ -570,27 +570,25 @@ An operand may be a `Reference` (the only way a function could access another fu rule #setArgFromStack(IDX, operandCopy(place(local(I), .ProjectionElems))) => - #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>TypedLocal)) + #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>LocalValue)) ... ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List requires 0 <=Int I andBool I #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems))) => - #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>TypedLocal)) + #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>LocalValue)) ... ListItem(StackFrame(_, _, _, _, CALLERLOCALS => CALLERLOCALS[I <- Moved])) _:List requires 0 <=Int I andBool I #adjustRef({LOCALS[I]}:>TypedLocal, OFFSET) + rule #localFromFrame(StackFrame(... locals: LOCALS), local(I:Int), OFFSET) => #adjustRef({LOCALS[I]}:>LocalValue, OFFSET) requires 0 <=Int I andBool I typedLocal(Reference(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT) From aecadb418685e5bf30cd24ff947c74d550575300 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 24 Mar 2025 20:08:44 +1100 Subject: [PATCH 11/12] fix list length lemmas to apply more broadly --- kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 95b98e85d..00fce0f07 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -26,11 +26,11 @@ The lists used in the semantics are cons-lists, so only rules with a head elemen ```k rule N true requires N N -Int 1 Date: Mon, 24 Mar 2025 22:15:54 +1100 Subject: [PATCH 12/12] note about incomplete conversion --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index abb87321c..ac6c35414 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -208,7 +208,7 @@ Projections operate on the data stored in the `TypedLocal` and are therefore spe rule #readOperand(operandCopy(place(local(I), PROJECTIONS))) => - #readProjection({LOCALS[I]}:>TypedLocal, PROJECTIONS) + #readProjection({LOCALS[I]}:>TypedLocal, PROJECTIONS) // FIXME should operate on LocalValue ... LOCALS