From 1ccfabef3f159fbc22c8015c39f21982551408a3 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 1 May 2025 11:10:11 +1000 Subject: [PATCH 1/4] Remove error rules for reading and writing locals (should not occur in valid MIR) --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 136 +++++-------------- 1 file changed, 32 insertions(+), 104 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a4fd43085..08edc3cad 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -43,17 +43,10 @@ Other uses of heating and cooling are to _read_ local variables as operands. Thi ### 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 ) -``` +It is an error to read a `Moved` local or an uninitialised `NewLocal`. +Also, locals are accessed via their index in list `` in a stack frame, which may be out of bounds +(but the compiler should guarantee that all local indexes are valid). +Types (`Ty`, an opaque number assigned by the Stable MIR extraction) are not checked, the local's type is used. ### Reading Operands (Local Variables and Constants) @@ -96,28 +89,7 @@ local value cannot be read, though, and the value should be initialised. andBool isTypedValue(LOCALS[I]) [preserves-definedness] // valid list indexing checked - rule operandCopy(place(local(I) #as LOCAL, _)) - => - LocalMoved(LOCAL) - ... - - LOCALS - requires 0 <=Int I - andBool I operandCopy(place(local(I), _)) - => - LocalUninitialised(local(I)) - ... - - LOCALS - requires I operandMove(place(local(I) #as LOCAL, _)) - => - LocalMoved(LOCAL) - ... - - LOCALS - requires 0 <=Int I - andBool I operandMove(place(local(I), _)) - => - LocalUninitialised(local(I)) - ... - - LOCALS - requires 0 <=Int I - andBool I #setLocalValue( place(local(I) #as LOCAL, _), _) => InvalidLocal(LOCAL) ... - LOCALS - requires size(LOCALS) <=Int I orBool I #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems), typedValue(_, TY, _) #as VAL) - => - TypeMismatch(LOCAL, tyOfLocal({LOCALS[I]}:>TypedLocal), VAL) - ... - - LOCALS - requires 0 <=Int I - andBool I TypedLocal) =/=K TY - [preserves-definedness] // list index checked before lookup + // error cases (not checked, just matched below to prevent them) - // setting a local which was Moved is an error - rule #setLocalValue( place(local(I), .ProjectionElems), _) - => - LocalMoved(local(I)) - ... - - LOCALS - requires 0 <=Int I - andBool I #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems), _) - => - LocalNotMutable(LOCAL) - ... - - LOCALS - requires I TypedLocal) ==K mutabilityNot // if all is well, write the value // mutable local - rule #setLocalValue(place(local(I), .ProjectionElems), typedValue(VAL:Value, TY, _ )) + rule #setLocalValue(place(local(I), .ProjectionElems), typedValue(VAL:Value, _, _ )) => .K ... @@ -448,22 +364,34 @@ The `#setLocalValue` operation writes a `TypedLocal` value to a given `Place` wi andBool I TypedLocal) ==K mutabilityMut - andBool (tyOfLocal({LOCALS[I]}:>TypedLocal) ==K TY orBool TY ==K TyUnknown) // matching or unknown type [preserves-definedness] // valid list indexing checked - // special case for non-mutable uninitialised values: mutable once - rule #setLocalValue(place(local(I), .ProjectionElems), typedValue(VAL:Value, TY, _ )) + // non-mutable uninitialised values are mutable once + rule #setLocalValue(place(local(I), .ProjectionElems), typedValue(VAL:Value, _, _ )) => .K ... - - LOCALS => LOCALS[I <- typedValue(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutabilityOf({LOCALS[I]}:>TypedLocal))] + + LOCALS => LOCALS[I <- typedValue(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutabilityOf({LOCALS[I]}:>TypedLocal))] requires 0 <=Int I andBool I TypedLocal) ==K TY orBool TY ==K TyUnknown) // matching or unknown type + [preserves-definedness] // valid list indexing checked + + // reusing a local which was Moved is allowed + rule #setLocalValue(place(local(I), .ProjectionElems), typedValue(VAL:Value, _, _ )) + => + .K + ... + + + LOCALS => LOCALS[I <- typedValue(VAL, tyOfLocal({LOCALS[I]}:>TypedLocal), mutabilityOf({LOCALS[I]}:>TypedLocal))] + + requires 0 <=Int I + andBool I rvalueLen(PLACE) => #lengthU64(operandCopy(PLACE)) ... rule #lengthU64(typedValue(Range(LIST), _, _)) - => + => typedValue(Integer(size(LIST), 64, false), TyUnknown, mutabilityNot) // returns usize ... @@ -724,7 +652,7 @@ Likewise built into the language are aggregates (tuples and `struct`s) and varia Besides their list of arguments, `enum`s also carry a `VariantIdx` indicating which variant was used. For tuples and `struct`s, this index is always 0. Tuples, `struct`s, and `enum`s are built as `Aggregate` values with a list of argument values. -For `enums`, the `VariantIdx` is set, and for `struct`s and `enum`s, the type ID (`Ty`) is retrieved from a special mapping of `AdtDef` to `Ty`. +For `enums`, the `VariantIdx` is set, and for `struct`s and `enum`s, the type ID (`Ty`) is retrieved from a special mapping of `AdtDef` to `Ty`. ```k rule rvalueAggregate(KIND, ARGS) => #readOperands(ARGS) ~> #mkAggregate(KIND) ... @@ -852,7 +780,7 @@ rewriting `typedLocal(...) ~> #cast(...) ~> REST` to `typedLocal(...) ~> REST`. ``` -### Integer Type Casts +### Integer Type Casts Casts between signed and unsigned integral numbers of different width exist, with a truncating semantics. These casts can only operate on the `Integer` variant of the `Value` type, adjusting @@ -919,7 +847,7 @@ The `Value` sort above operates at a higher level than the bytes representation // Integer: handled in separate module for numeric operations rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), TYPEINFO) - => + => #decodeInteger(BYTES, #intTypeOf(TYPEINFO)) requires #isIntType(TYPEINFO) andBool lengthBytes(BYTES) ==K #bitWidth(#intTypeOf(TYPEINFO)) /Int 8 From d551ef010969f1f3d454359ab3e5981dd7361b4d Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 1 May 2025 01:17:16 +0000 Subject: [PATCH 2/4] Set Version: 0.3.135 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 7de9bb80b..c6d79ec31 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.134" +version = "0.3.135" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 217b0a44a..06c348435 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.134' +VERSION: Final = '0.3.135' diff --git a/kmir/uv.lock b/kmir/uv.lock index 9d71d30aa..ef0258283 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.134" +version = "0.3.135" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index d6f2cdd3f..4212f2702 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.134 +0.3.135 From 776f91515bd8f5b00d97603ced0557bf0a2f8db0 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 1 May 2025 11:37:00 +1000 Subject: [PATCH 3/4] remove error rules for arithmetic (except overflow and divByZero --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 61 ++++---------------- 1 file changed, 12 insertions(+), 49 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 08edc3cad..55cc76bc4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -900,29 +900,15 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` ```k syntax MIRError ::= 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 - | OpNotimplemented ( BinOp, TypedValue, TypedValue) - // errors below are program errors - | "DivisionByZero" + // (dynamic) program errors causing undefined behaviour + syntax OperationError ::= "DivisionByZero" | "Overflow_U_B" - // catch Moved or uninitialised operands - rule #compute(OP, ARG1, ARG2, _FLAG) => OperandError(OP, ARG1, ARG2) - requires notBool (isTypedValue(ARG1) andBool isTypedValue(ARG2)) + // errors caused by invalid MIR code get stuck - rule #applyUnOp(OP, ARG) => OperandError(OP, ARG) - requires notBool isTypedValue(ARG) + // Moved or uninitialised operands - // catch-all rule to make `#compute` total - rule #compute(OP, ARG1, ARG2, _FLAG) => OpNotimplemented(OP, ARG1, ARG2) - requires isTypedValue(ARG1) - andBool isTypedValue(ARG2) - [owise] + // specific errors for the particular operation types (argument or type mismatches) ``` #### Arithmetic @@ -968,6 +954,10 @@ The arithmetic operations require operands of the same numeric type. requires Y =/=Int 0 // operation undefined otherwise + // error cases for isArithmetic(BOP): + // * arguments must have the same type (TY match) + // * arguments must be Numbers + // Checked operations return a pair of the truncated value and an overflow flag // signed numbers: must check for wrap-around (operation specific) rule #compute( @@ -1095,22 +1085,6 @@ The arithmetic operations require operands of the same numeric type. requires DIVISOR ==Int -1 andBool DIVIDEND ==Int 0 -Int (1 < - OperandMismatch(BOP, ARG1, ARG2) - requires isArithmetic(BOP) - [owise] - - // different argument types - rule #compute(BOP, typedValue(_, TY1, _), typedValue(_, TY2, _), _) - => - TypeMismatch(BOP, TY1, TY2) - requires TY1 =/=K TY2 - andBool isArithmetic(BOP) - [owise] ``` #### Comparison operations @@ -1146,9 +1120,9 @@ 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, typedValue(_, TY, _), typedValue(_, TY2, _), _) => TypeMismatch(OP, TY, TY2) - requires isComparison(OP) - andBool TY =/=K TY2 + // error cases for isComparison and binOpCmp: + // * arguments must have the same type + // * arguments must be numbers or Bool rule #compute(OP, typedValue(Integer(VAL1, WIDTH, SIGN), TY, _), typedValue(Integer(VAL2, WIDTH, SIGN), TY, _), _) => @@ -1161,12 +1135,6 @@ All operations except `binOpCmp` return a `BoolVal`. The argument types must be typedValue(BoolVal(cmpOpBool(OP, VAL1, VAL2)), TyUnknown, mutabilityNot) requires isComparison(OP) [preserves-definedness] // OP known to be a comparison - - rule #compute(OP, typedValue(ARG1, TY, _), typedValue(ARG2, TY, _), _) - => - OperandMismatch(OP, ARG1, ARG2) - requires isComparison(OP) - [owise] ``` The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `std::cmp::Ordering as i8`), indicating `LE`, `EQ`, or `GT`. @@ -1228,11 +1196,6 @@ The `unOpNot` operation works on boolean and integral values, with the usual sem ``` -```k - rule #applyUnOp(OP, typedValue(VAL, _, _)) => OperandMismatch(OP, VAL) ... - [owise] -``` - #### Bit-oriented operations `binOpBitXor` From e519bf9d22c89a5c817920dc8d2229e59b944871 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 30 Apr 2025 21:56:59 -0400 Subject: [PATCH 4/4] Adding loop test cases --- .../integration/data/prove-rs/loop-fail.rs | 17 +++++++++++++++++ .../src/tests/integration/data/prove-rs/loop.rs | 17 +++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/loop-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/loop.rs diff --git a/kmir/src/tests/integration/data/prove-rs/loop-fail.rs b/kmir/src/tests/integration/data/prove-rs/loop-fail.rs new file mode 100644 index 000000000..c1def9c46 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/loop-fail.rs @@ -0,0 +1,17 @@ +fn property_test() { + let mut x = 0; + let y = 10; + let mut s = 0; + + while x < y { + x += 1; + s += x; + } + + assert!(s == 56); + +} + +fn main() { + property_test(); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/loop.rs b/kmir/src/tests/integration/data/prove-rs/loop.rs new file mode 100644 index 000000000..5f80c15ee --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/loop.rs @@ -0,0 +1,17 @@ +fn property_test() { + let mut x = 0; + let y = 10; + let mut s = 0; + + while x < y { + x += 1; + s += x; + } + + assert!(s == 55); + +} + +fn main() { + property_test(); +} \ No newline at end of file