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/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index dcf29818e..8732836fa 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -308,23 +308,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 @@ -420,13 +409,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)) ~> _ => - #decrementRef(LOCAL0) ~> #setLocalValue(DEST) ~> #execBlockIdx(TARGET) ~> .K + #if isLocalValue(LOCAL0) #then #setLocalValue(DEST, #decrementRef({LOCAL0}:>LocalValue)) #else .K #fi + ~> #execBlockIdx(TARGET) + ~> .K _ => CALLER // @@ -441,8 +433,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] @@ -564,35 +555,40 @@ 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]}:>LocalValue)) ... ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List requires 0 <=Int I andBool I #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems))) => - #incrementRef({CALLERLOCALS[I]}:>TypedLocal) ~> #setLocalValue(place(local(IDX), .ProjectionElems)) + #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>LocalValue)) ... ListItem(StackFrame(_, _, _, _, CALLERLOCALS => CALLERLOCALS[I <- Moved])) _:List requires 0 <=Int I andBool I true requires N N -Int 1 true - rule hasValue(Moved) => false - rule hasValue(noValue(_, _)) => false - - rule isNoValue(typedLocal(_, _, _)) => false - rule isNoValue(Moved) => false - rule isNoValue(noValue(_, _)) => true - 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. @@ -78,7 +74,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 ``` @@ -136,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))) @@ -146,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))) @@ -157,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))) @@ -187,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))) @@ -198,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 #readOperand(operandCopy(place(local(I), PROJECTIONS))) => - #readProjection({LOCALS[I]}:>TypedLocal, PROJECTIONS) + #readProjection({LOCALS[I]}:>TypedLocal, PROJECTIONS) // FIXME should operate on LocalValue ... LOCALS requires PROJECTIONS =/=K .ProjectionElems andBool 0 <=Int I andBool I TypedLocal) + andBool isLocalValue(LOCALS[I]) [preserves-definedness] // valid list indexing checked ``` @@ -239,14 +230,23 @@ 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 + | Projected + | TypedLocal + | EvalResult + + syntax KResult ::= EvalResult + + syntax EvalResult ::= LocalValue // 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,16 +260,19 @@ 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))) ... LOCALS - requires LOCALS[I] ==K Moved + requires I typedLocal(_, _, _) ~> #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems)) + rule #setLocalValue( place(local(I) #as LOCAL, .ProjectionElems), typedLocal(_, _, _)) => #LocalError(LocalNotMutable(LOCAL)) ... @@ -277,20 +280,13 @@ 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 noValue(_, _) ~> #setLocalValue( _) => .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) ... + andBool isLocalValue(LOCALS[I]) + andBool mutability({LOCALS[I]}:>TypedLocal) ==K mutabilityNot + [preserves-definedness] // valid list indexing checked // 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 ... @@ -298,24 +294,22 @@ 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 - rule typedLocal(VAL:Value, TY, _ ) ~> #setLocalValue(place(local(I), .ProjectionElems)) + rule #setLocalValue(place(local(I), .ProjectionElems), typedLocal(VAL:Value, TY, _ )) => .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 ``` @@ -343,8 +337,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) ... @@ -435,15 +432,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 ``` @@ -731,10 +720,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 ... ``` @@ -782,7 +772,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( @@ -801,20 +792,21 @@ An important prerequisite of this rule is that when passing references to a call syntax TypedLocal ::= #localFromFrame ( StackFrame, Local, Int ) [function] - rule #localFromFrame(StackFrame(... locals: LOCALS), local(I:Int), OFFSET) => #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) 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) ``` @@ -831,7 +823,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 +851,7 @@ The solution is to use rewrite operations in a downward pass through the project andBool I #projectedUpdate( _DEST, @@ -915,20 +907,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 ... @@ -948,6 +940,7 @@ The solution is to use rewrite operations in a downward pass through the project requires 0 VAL ~> #setLocalValue(place(local(I), PROJ)) + rule #setLocalValue(place(local(I), PROJ), VAL) => #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false) ... @@ -1028,8 +1021,9 @@ For binary operations generally, both arguments have to be read from the provide ```k syntax KItem ::= #suspend ( BinOp, Operand, Bool) - | #ready ( BinOp, TypedLocal, Bool ) - | #compute ( BinOp, TypedLocal, TypedLocal, Bool ) [function, total] + | #ready ( BinOp, Value, Ty, Bool ) + + syntax EvalResult ::= #compute ( BinOp, Value, Ty, Value, Ty, Bool ) [function, total] rule rvalueBinaryOp(BINOP, OP1, OP2) => @@ -1043,15 +1037,15 @@ For binary operations generally, both arguments have to be read from the provide ... - rule ARG1:TypedLocal ~> #suspend(BINOP, OP2, CHECKFLAG) + rule typedLocal(VAL1, TY1, _) ~> #suspend(BINOP, OP2, CHECKFLAG) => - #readOperand(OP2) ~> #ready(BINOP, ARG1, CHECKFLAG) + #readOperand(OP2) ~> #ready(BINOP, VAL1, TY1, CHECKFLAG) ... - rule ARG2:TypedLocal ~> #ready(BINOP, ARG1,CHECKFLAG) + rule typedLocal(VAL2, TY2, _) ~> #ready(BINOP, VAL1, TY1, CHECKFLAG) => - #compute(BINOP, ARG1, ARG2, CHECKFLAG) + #compute(BINOP, VAL1, TY1, VAL2, TY2, CHECKFLAG) ... ``` @@ -1059,7 +1053,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 EvalResult ::= #applyUnOp ( UnOp ) rule rvalueUnaryOp(UNOP, OP1) => @@ -1071,7 +1065,9 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` #### Potential errors ```k - syntax KItem ::= #OperationError( OperationError ) + syntax MIRError ::= #OperationError( OperationError ) + + syntax EvalResult ::= OperationError syntax OperationError ::= TypeMismatch ( BinOp, Ty, Ty ) | OperandMismatch ( BinOp, Value, Value ) @@ -1079,19 +1075,13 @@ There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata` | 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, _TY1, ARG2, _TY2, _FLAG) => Unimplemented(OP, ARG1, ARG2) [owise] ``` @@ -1138,30 +1128,23 @@ 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), TY, Integer(ARG2, WIDTH, SIGNEDNESS), TY, 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, _), _) + rule #compute(BOP, _, TY1, _, TY2, _) => - #OperationError(OperandMismatch(BOP, ARG1, ARG2)) + TypeMismatch(BOP, TY1, TY2) requires isArithmetic(BOP) - [owise] + andBool TY1 =/=K TY2 - // different argument types - rule #compute(BOP, typedLocal(_, TY1, _), typedLocal(_, TY2, _), _) + rule #compute(BOP, ARG1, _, ARG2, _, _) => - #OperationError(TypeMismatch(BOP, TY1, TY2)) - requires TY1 =/=K TY2 - andBool isArithmetic(BOP) + OperandMismatch(BOP, ARG1, ARG2) + requires isArithmetic(BOP) [owise] // helper function to truncate int values @@ -1190,8 +1173,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 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) => @@ -1261,32 +1244,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), TY, Integer(VAL2, WIDTH, SIGN), TY, _) => 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), TY, BoolVal(VAL2), TY, _) => 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, _, 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] ``` 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), TY, Integer(VAL2, WIDTH, SIGN), TY, _) => 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), TY, BoolVal(VAL2), TY, _) => typedLocal(Integer(cmpBool(VAL1, VAL2), 8, true), TyUnknown, mutabilityNot) - ``` #### Unary operations on Boolean and integral values 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', 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