diff --git a/rust-semantics/config.md b/rust-semantics/config.md index 155771d..2f7f00f 100644 --- a/rust-semantics/config.md +++ b/rust-semantics/config.md @@ -6,8 +6,8 @@ module RUST-CONFIGURATION configuration - + endmodule diff --git a/rust-semantics/execution/block.md b/rust-semantics/execution/block.md index c478852..ff00ed0 100644 --- a/rust-semantics/execution/block.md +++ b/rust-semantics/execution/block.md @@ -16,7 +16,7 @@ module RUST-BLOCK // Blocks are always value expressions and evaluate the last operand in // value expression context. - rule V:Value ~> popLocalState => popLocalState ~> V + rule V:PtrValue ~> popLocalState => popLocalState ~> V endmodule ``` diff --git a/rust-semantics/execution/calls.md b/rust-semantics/execution/calls.md index e005cbf..5362fe6 100644 --- a/rust-semantics/execution/calls.md +++ b/rust-semantics/execution/calls.md @@ -41,19 +41,29 @@ module RUST-CALLS _ => .Map + rule setArgs + ( (CP:Ptr, CPs:NormalizedCallParams) + , (P:NormalizedFunctionParameter, Ps:NormalizedFunctionParameterList) + ) + => setArg(CP, P) ~> setArgs(CPs, Ps) + + rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K + + syntax Instruction ::= setArg(Ptr, NormalizedFunctionParameter) + rule - setArgs( - (ValueId:Int , Ids:NormalizedCallParams) => Ids, - ((Name:Identifier : T:Type) , Ps:NormalizedFunctionParameterList) => Ps - ) + setArg + ( ptr(ValueId:Int) + , Name:ValueName : T:Type + ) + => .K ... Locals:Map => Locals[Name <- ValueId] ValueId |-> Value ... - requires notBool Name in_keys(Locals) andBool isSameType(Value, T) - - rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K + requires notBool Name in_keys(Locals) + andBool isSameType(Value, T) endmodule diff --git a/rust-semantics/execution/let.md b/rust-semantics/execution/let.md index a1b7bd8..872e46b 100644 --- a/rust-semantics/execution/let.md +++ b/rust-semantics/execution/let.md @@ -10,7 +10,7 @@ module RUST-LET // Not all cases are implemented rule - let Variable:Identifier : T:Type = V:Value ; => .K + let Variable:Identifier : T:Type = ptrValue(_, V:Value) ; => .K ... NextId:Int => NextId +Int 1 @@ -18,7 +18,7 @@ module RUST-LET Values:Map => Values[NextId <- implicitCast(V, T)] rule - let Variable:Identifier = V:Value ; => .K + let Variable:Identifier = ptrValue(_, V:Value) ; => .K ... NextId:Int => NextId +Int 1 diff --git a/rust-semantics/expression.md b/rust-semantics/expression.md index 976e856..2993e93 100644 --- a/rust-semantics/expression.md +++ b/rust-semantics/expression.md @@ -1,15 +1,21 @@ ```k +requires "expression/calls.md" requires "expression/integer-operations.md" requires "expression/constants.md" requires "expression/casts.md" requires "expression/literals.md" +requires "expression/references.md" +requires "expression/tools.md" requires "expression/variables.md" module RUST-EXPRESSION imports private RUST-CASTS + imports private RUST-EXPRESSION-CALLS + imports private RUST-EXPRESSION-CONSTANTS imports private RUST-EXPRESSION-LITERALS + imports private RUST-EXPRESSION-REFERENCES + imports private RUST-EXPRESSION-TOOLS imports private RUST-EXPRESSION-VARIABLES - imports private RUST-EXPRESSION-CONSTANTS imports private RUST-INTEGER-OPERATIONS endmodule ``` diff --git a/rust-semantics/expression/calls.md b/rust-semantics/expression/calls.md new file mode 100644 index 0000000..32abd98 --- /dev/null +++ b/rust-semantics/expression/calls.md @@ -0,0 +1,97 @@ +```k + +module RUST-EXPRESSION-CALLS + imports private COMMON-K-CELL + imports private RUST-SHARED-SYNTAX + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-EXPRESSION-TOOLS + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + + syntax Instruction ::= methodCall + ( traitName: TypePath + , method: Identifier + , params: CallParamsList + , reversedNormalizedParams: NormalizedCallParams + ) + + syntax NormalizedCallParams ::= reverse(NormalizedCallParams, NormalizedCallParams) [function, total] + rule reverse(.NormalizedCallParams, R:NormalizedCallParams) => R + rule reverse((P, Ps:NormalizedCallParams), R:NormalizedCallParams) => reverse(Ps, (P, R)) + + rule SelfName:Expression . MethodName:Identifier ( ) + => methodCall(... self: SelfName, method: MethodName, params: .CallParamsList) + rule SelfName:Expression . MethodName:Identifier ( Args:CallParamsList ) + => methodCall(... self: SelfName, method: MethodName, params: Args) + rule SelfName:Expression . MethodName:Identifier ( Args:CallParamsList, ) + => methodCall(... self: SelfName, method: MethodName, params: Args) + + rule + + methodCall + (... self: ptrValue(ptr(A) #as P, _) + , method: MethodName:Identifier + , params: Args:CallParamsList + ) + => methodCall + (... traitName: TraitName + , method: MethodName + , params: Args + , reversedNormalizedParams: P, .NormalizedCallParams + ) + ... + + A |-> struct(TraitName:TypePath, _) ... + requires isValueWithPtr(Args) + + rule methodCall + (... traitName: _TraitName:TypePath + , method: _MethodName:Identifier + , params: (ptrValue(ptr(_) #as P:Ptr, _:Value) , Cps:CallParamsList) => Cps + , reversedNormalizedParams: Args:NormalizedCallParams + => P, Args + ) + rule + + methodCall + (... traitName: _TraitName:TypePath + , method: _MethodName:Identifier + , params: (ptrValue(null, V:Value) , Cps:CallParamsList) => Cps + , reversedNormalizedParams: Args:NormalizedCallParams + => ptr(NextId), Args + ) + ... + + NextId:Int => NextId +Int 1 + Values:Map => Values[NextId <- V] + rule + methodCall + (... traitName: TraitName:TypePath + , method: MethodName:Identifier + , params: .CallParamsList + , reversedNormalizedParams: Args:NormalizedCallParams + ) + => normalizedMethodCall + ( TraitName + , MethodName + , reverse(Args, .NormalizedCallParams) + ) + + // Apparently contexts need the type of the HOLE to be K, and I'm not sure + // how to transform CallParamsList in some sort of K combination in a + // reasonable way. We're using heat/cool rules instead. + rule (.K => HOLE) ~> HOLE:Expression , _:CallParamsList + [heat, result(ValueWithPtr)] + rule (HOLE:Expression ~> (_:Expression , L:CallParamsList):CallParamsList) + => HOLE , L + [cool, result(ValueWithPtr)] + rule (.K => HOLE) ~> V:Expression , HOLE:CallParamsList + requires isValueWithPtr(V) + [heat, result(ValueWithPtr)] + rule (HOLE:CallParamsList ~> V:Expression , _:CallParamsList) + => V , HOLE + requires isValueWithPtr(V) + [cool, result(ValueWithPtr)] +endmodule + +``` diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md index 5ffd642..c7988eb 100644 --- a/rust-semantics/expression/casts.md +++ b/rust-semantics/expression/casts.md @@ -38,9 +38,11 @@ module RUST-CASTS rule implicitCast(V:Bool, bool) => V + rule implicitCast(struct(T, _) #as V, T) => V + // Rewrites - rule V:Value ~> implicitCastTo(T:Type) => implicitCast(V, T) + rule ptrValue(P:Ptr, V:Value) ~> implicitCastTo(T:Type) => wrapPtrValueOrError(P, implicitCast(V, T)) // We don't need a value for the unit type rule implicitCastTo(( )) => .K diff --git a/rust-semantics/expression/constants.md b/rust-semantics/expression/constants.md index cb66638..11a3187 100644 --- a/rust-semantics/expression/constants.md +++ b/rust-semantics/expression/constants.md @@ -6,9 +6,14 @@ module RUST-EXPRESSION-CONSTANTS imports private RUST-REPRESENTATION imports private RUST-PREPROCESSING-CONFIGURATION - rule Name:Identifier::.PathExprSegments => V ... + rule Name:Identifier::.PathExprSegments => ptrValue(null, V) ... Name V:Value + requires notBool isLocalVariable(Name) + rule [[isConstant(Name:Identifier) => true]] + Name + requires notBool isLocalVariable(Name) + rule isConstant(_Name:ValueName) => false [owise] endmodule ``` \ No newline at end of file diff --git a/rust-semantics/expression/integer-operations.md b/rust-semantics/expression/integer-operations.md index f220129..d2174f2 100644 --- a/rust-semantics/expression/integer-operations.md +++ b/rust-semantics/expression/integer-operations.md @@ -13,36 +13,35 @@ module RUST-INTEGER-ARITHMETIC-OPERATIONS // as implicit type casting (coercion) is not available // in Rust. - rule i32(A):Value * i32(B):Value => i32(A *MInt B) - rule i32(A):Value + i32(B):Value => i32(A +MInt B) - rule i32(A):Value - i32(B):Value => i32(A -MInt B) - rule i32(A):Value / i32(B):Value => i32(A /sMInt B) - rule i32(A):Value % i32(B):Value => i32(A %sMInt B) + rule ptrValue(_, i32(A):Value) * ptrValue(_, i32(B):Value) => ptrValue(null, i32(A *MInt B)) + rule ptrValue(_, i32(A):Value) + ptrValue(_, i32(B):Value) => ptrValue(null, i32(A +MInt B)) + rule ptrValue(_, i32(A):Value) - ptrValue(_, i32(B):Value) => ptrValue(null, i32(A -MInt B)) + rule ptrValue(_, i32(A):Value) / ptrValue(_, i32(B):Value) => ptrValue(null, i32(A /sMInt B)) + rule ptrValue(_, i32(A):Value) % ptrValue(_, i32(B):Value) => ptrValue(null, i32(A %sMInt B)) - rule u32(A):Value * u32(B):Value => u32(A *MInt B) - rule u32(A):Value + u32(B):Value => u32(A +MInt B) - rule u32(A):Value - u32(B):Value => u32(A -MInt B) - rule u32(A):Value / u32(B):Value => u32(A /uMInt B) - rule u32(A):Value % u32(B):Value => u32(A %uMInt B) - - rule i64(A):Value * i64(B):Value => i64(A *MInt B) - rule i64(A):Value + i64(B):Value => i64(A +MInt B) - rule i64(A):Value - i64(B):Value => i64(A -MInt B) - rule i64(A):Value / i64(B):Value => i64(A /sMInt B) - rule i64(A):Value % i64(B):Value => i64(A %sMInt B) + rule ptrValue(_, u32(A):Value) * ptrValue(_, u32(B):Value) => ptrValue(null, u32(A *MInt B)) + rule ptrValue(_, u32(A):Value) + ptrValue(_, u32(B):Value) => ptrValue(null, u32(A +MInt B)) + rule ptrValue(_, u32(A):Value) - ptrValue(_, u32(B):Value) => ptrValue(null, u32(A -MInt B)) + rule ptrValue(_, u32(A):Value) / ptrValue(_, u32(B):Value) => ptrValue(null, u32(A /uMInt B)) + rule ptrValue(_, u32(A):Value) % ptrValue(_, u32(B):Value) => ptrValue(null, u32(A %uMInt B)) + + rule ptrValue(_, i64(A):Value) * ptrValue(_, i64(B):Value) => ptrValue(null, i64(A *MInt B)) + rule ptrValue(_, i64(A):Value) + ptrValue(_, i64(B):Value) => ptrValue(null, i64(A +MInt B)) + rule ptrValue(_, i64(A):Value) - ptrValue(_, i64(B):Value) => ptrValue(null, i64(A -MInt B)) + rule ptrValue(_, i64(A):Value) / ptrValue(_, i64(B):Value) => ptrValue(null, i64(A /sMInt B)) + rule ptrValue(_, i64(A):Value) % ptrValue(_, i64(B):Value) => ptrValue(null, i64(A %sMInt B)) - rule u64(A):Value * u64(B):Value => u64(A *MInt B) - rule u64(A):Value + u64(B):Value => u64(A +MInt B) - rule u64(A):Value - u64(B):Value => u64(A -MInt B) - rule u64(A):Value / u64(B):Value => u64(A /uMInt B) - rule u64(A):Value % u64(B):Value => u64(A %uMInt B) - - rule u128(A):Value * u128(B):Value => u128(A *MInt B) - rule u128(A):Value + u128(B):Value => u128(A +MInt B) - rule u128(A):Value - u128(B):Value => u128(A -MInt B) - rule u128(A):Value / u128(B):Value => u128(A /uMInt B) - rule u128(A):Value % u128(B):Value => u128(A %uMInt B) - + rule ptrValue(_, u64(A):Value) * ptrValue(_, u64(B):Value) => ptrValue(null, u64(A *MInt B)) + rule ptrValue(_, u64(A):Value) + ptrValue(_, u64(B):Value) => ptrValue(null, u64(A +MInt B)) + rule ptrValue(_, u64(A):Value) - ptrValue(_, u64(B):Value) => ptrValue(null, u64(A -MInt B)) + rule ptrValue(_, u64(A):Value) / ptrValue(_, u64(B):Value) => ptrValue(null, u64(A /uMInt B)) + rule ptrValue(_, u64(A):Value) % ptrValue(_, u64(B):Value) => ptrValue(null, u64(A %uMInt B)) + + rule ptrValue(_, u128(A):Value) * ptrValue(_, u128(B):Value) => ptrValue(null, u128(A *MInt B)) + rule ptrValue(_, u128(A):Value) + ptrValue(_, u128(B):Value) => ptrValue(null, u128(A +MInt B)) + rule ptrValue(_, u128(A):Value) - ptrValue(_, u128(B):Value) => ptrValue(null, u128(A -MInt B)) + rule ptrValue(_, u128(A):Value) / ptrValue(_, u128(B):Value) => ptrValue(null, u128(A /uMInt B)) + rule ptrValue(_, u128(A):Value) % ptrValue(_, u128(B):Value) => ptrValue(null, u128(A %uMInt B)) endmodule @@ -51,40 +50,40 @@ module RUST-INTEGER-RELATIONAL-OPERATIONS imports RUST-SHARED-SYNTAX imports private RUST-REPRESENTATION - rule i32(A):Value == i32(B):Value => A ==MInt B - rule i32(A):Value != i32(B):Value => A =/=MInt B - rule i32(A):Value > i32(B):Value => A >sMInt B - rule i32(A):Value < i32(B):Value => A = i32(B):Value => A >=sMInt B - rule i32(A):Value <= i32(B):Value => A <=sMInt B - - rule u32(A):Value == u32(B):Value => A ==MInt B - rule u32(A):Value != u32(B):Value => A =/=MInt B - rule u32(A):Value > u32(B):Value => A >uMInt B - rule u32(A):Value < u32(B):Value => A = u32(B):Value => A >=uMInt B - rule u32(A):Value <= u32(B):Value => A <=uMInt B - - rule i64(A):Value == i64(B):Value => A ==MInt B - rule i64(A):Value != i64(B):Value => A =/=MInt B - rule i64(A):Value > i64(B):Value => A >sMInt B - rule i64(A):Value < i64(B):Value => A = i64(B):Value => A >=sMInt B - rule i64(A):Value <= i64(B):Value => A <=sMInt B - - rule u64(A):Value == u64(B):Value => A ==MInt B - rule u64(A):Value != u64(B):Value => A =/=MInt B - rule u64(A):Value > u64(B):Value => A >uMInt B - rule u64(A):Value < u64(B):Value => A = u64(B):Value => A >=uMInt B - rule u64(A):Value <= u64(B):Value => A <=uMInt B - - rule u128(A):Value == u128(B):Value => A ==MInt B - rule u128(A):Value != u128(B):Value => A =/=MInt B - rule u128(A):Value > u128(B):Value => A >uMInt B - rule u128(A):Value < u128(B):Value => A = u128(B):Value => A >=uMInt B - rule u128(A):Value <= u128(B):Value => A <=uMInt B + rule ptrValue(null, i32(A):Value) == ptrValue(null, i32(B):Value) => ptrValue(null, A ==MInt B) + rule ptrValue(null, i32(A):Value) != ptrValue(null, i32(B):Value) => ptrValue(null, A =/=MInt B) + rule ptrValue(null, i32(A):Value) > ptrValue(null, i32(B):Value) => ptrValue(null, A >sMInt B) + rule ptrValue(null, i32(A):Value) < ptrValue(null, i32(B):Value) => ptrValue(null, A = ptrValue(null, i32(B):Value) => ptrValue(null, A >=sMInt B) + rule ptrValue(null, i32(A):Value) <= ptrValue(null, i32(B):Value) => ptrValue(null, A <=sMInt B) + + rule ptrValue(null, u32(A):Value) == ptrValue(null, u32(B):Value) => ptrValue(null, A ==MInt B) + rule ptrValue(null, u32(A):Value) != ptrValue(null, u32(B):Value) => ptrValue(null, A =/=MInt B) + rule ptrValue(null, u32(A):Value) > ptrValue(null, u32(B):Value) => ptrValue(null, A >uMInt B) + rule ptrValue(null, u32(A):Value) < ptrValue(null, u32(B):Value) => ptrValue(null, A = ptrValue(null, u32(B):Value) => ptrValue(null, A >=uMInt B) + rule ptrValue(null, u32(A):Value) <= ptrValue(null, u32(B):Value) => ptrValue(null, A <=uMInt B) + + rule ptrValue(null, i64(A):Value) == ptrValue(null, i64(B):Value) => ptrValue(null, A ==MInt B) + rule ptrValue(null, i64(A):Value) != ptrValue(null, i64(B):Value) => ptrValue(null, A =/=MInt B) + rule ptrValue(null, i64(A):Value) > ptrValue(null, i64(B):Value) => ptrValue(null, A >sMInt B) + rule ptrValue(null, i64(A):Value) < ptrValue(null, i64(B):Value) => ptrValue(null, A = ptrValue(null, i64(B):Value) => ptrValue(null, A >=sMInt B) + rule ptrValue(null, i64(A):Value) <= ptrValue(null, i64(B):Value) => ptrValue(null, A <=sMInt B) + + rule ptrValue(null, u64(A):Value) == ptrValue(null, u64(B):Value) => ptrValue(null, A ==MInt B) + rule ptrValue(null, u64(A):Value) != ptrValue(null, u64(B):Value) => ptrValue(null, A =/=MInt B) + rule ptrValue(null, u64(A):Value) > ptrValue(null, u64(B):Value) => ptrValue(null, A >uMInt B) + rule ptrValue(null, u64(A):Value) < ptrValue(null, u64(B):Value) => ptrValue(null, A = ptrValue(null, u64(B):Value) => ptrValue(null, A >=uMInt B) + rule ptrValue(null, u64(A):Value) <= ptrValue(null, u64(B):Value) => ptrValue(null, A <=uMInt B) + + rule ptrValue(null, u128(A):Value) == ptrValue(null, u128(B):Value) => ptrValue(null, A ==MInt B) + rule ptrValue(null, u128(A):Value) != ptrValue(null, u128(B):Value) => ptrValue(null, A =/=MInt B) + rule ptrValue(null, u128(A):Value) > ptrValue(null, u128(B):Value) => ptrValue(null, A >uMInt B) + rule ptrValue(null, u128(A):Value) < ptrValue(null, u128(B):Value) => ptrValue(null, A = ptrValue(null, u128(B):Value) => ptrValue(null, A >=uMInt B) + rule ptrValue(null, u128(A):Value) <= ptrValue(null, u128(B):Value) => ptrValue(null, A <=uMInt B) endmodule diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md index ea8ffbd..dd7eac5 100644 --- a/rust-semantics/expression/literals.md +++ b/rust-semantics/expression/literals.md @@ -16,7 +16,8 @@ module RUST-EXPRESSION-INTEGER-LITERALS syntax String ::= IntegerLiteralToString(IntegerLiteral) [function, total, hook(STRING.token2string)] - rule I:IntegerLiteral => parseInteger(I) + rule I:IntegerLiteral => wrapPtrValueOrError(null, parseInteger(I)) + rule B:Bool:LiteralExpression => wrapPtrValueOrError(null, B:Bool:Value) syntax ValueOrError ::= parseInteger(IntegerLiteral) [function, total] | parseInteger(String) [function, total] diff --git a/rust-semantics/expression/references.md b/rust-semantics/expression/references.md new file mode 100644 index 0000000..71e5057 --- /dev/null +++ b/rust-semantics/expression/references.md @@ -0,0 +1,11 @@ +```k + +module RUST-EXPRESSION-REFERENCES + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + + rule & E:Expression => E + +endmodule + +``` diff --git a/rust-semantics/expression/tools.md b/rust-semantics/expression/tools.md new file mode 100644 index 0000000..c81fdfe --- /dev/null +++ b/rust-semantics/expression/tools.md @@ -0,0 +1,15 @@ +```k + +module RUST-EXPRESSION-TOOLS + imports private BOOL + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + imports private RUST-VALUE-SYNTAX + + rule isValueWithPtr(_) => false [owise] + rule isValueWithPtr(_:PtrValue) => true + rule isValueWithPtr(.CallParamsList) => true + rule isValueWithPtr(P:Expression , Ps:CallParamsList) => isValueWithPtr(P) andBool isValueWithPtr(Ps) +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/expression/variables.md b/rust-semantics/expression/variables.md index 26fc630..52cab4d 100644 --- a/rust-semantics/expression/variables.md +++ b/rust-semantics/expression/variables.md @@ -1,18 +1,33 @@ ```k module RUST-EXPRESSION-VARIABLES - imports COMMON-K-CELL - imports RUST-EXECUTION-CONFIGURATION - imports RUST-VALUE-SYNTAX - imports RUST-SHARED-SYNTAX + imports private COMMON-K-CELL + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + imports private RUST-VALUE-SYNTAX rule - Variable:Identifier :: .PathExprSegments => V + Variable:Identifier :: .PathExprSegments => ptrValue(ptr(VarId), V) ... Variable |-> VarId:Int ... VarId |-> V:Value ... + + rule + + self :: .PathExprSegments => ptrValue(ptr(VarId), V) + ... + + self:PathIdentSegment |-> VarId:Int ... + VarId |-> V:Value ... + + rule [[isLocalVariable(Name:ValueName) => true]] + Locals + requires Name in_keys(Locals) + rule isLocalVariable(_) => false [owise] + endmodule ``` \ No newline at end of file diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md index 5abff5f..06e54c7 100644 --- a/rust-semantics/helpers.md +++ b/rust-semantics/helpers.md @@ -10,6 +10,7 @@ module RUST-HELPERS syntax Bool ::= isSameType(Value, Type) [function, total] rule isSameType(_, _) => false [owise] + rule isSameType(_:Value, & T => T) rule isSameType(_, $selftype) => true rule isSameType(i64(_), i64) => true rule isSameType(u64(_), u64) => true diff --git a/rust-semantics/preprocessing/constants.md b/rust-semantics/preprocessing/constants.md index ad5e993..3d8a8aa 100644 --- a/rust-semantics/preprocessing/constants.md +++ b/rust-semantics/preprocessing/constants.md @@ -9,8 +9,8 @@ module RUST-CONSTANTS syntax KItem ::= setConstant(Identifier, ValueOrError) rule - (const Name:Identifier : T:Type = V:Value;):ConstantItem:KItem - => setConstant(Name, implicitCast(V, T)) + (const Name:Identifier : T:Type = ptrValue(_, V:Value);):ConstantItem:KItem + => setConstant(Name, implicitCast(V, T)) rule diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md index 3b7fdc9..e848d55 100644 --- a/rust-semantics/preprocessing/syntax.md +++ b/rust-semantics/preprocessing/syntax.md @@ -28,8 +28,6 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX OuterAttributes ) - // TODO: Move to a more generic place - syntax Identifier ::= "self" [token] endmodule ``` diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index 8dedb5c..e3f2506 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -26,11 +26,19 @@ module RUST-VALUE-SYNTAX | Bool syntax ValueList ::= List{Value, ","} - syntax Expression ::= Value - syntax KResult ::= Value - syntax ValueOrError ::= Value | SemanticsError + syntax Ptr ::= "null" | ptr(Int) + syntax PtrValue ::= ptrValue(Ptr, Value) + syntax PtrValueOrError ::= PtrValue | SemanticsError + + syntax Expression ::= PtrValue + syntax KResult ::= PtrValue + + syntax PtrValueOrError ::= wrapPtrValueOrError(Ptr, ValueOrError) [function, total] + rule wrapPtrValueOrError(P:Ptr, V:Value) => ptrValue(P, V) + rule wrapPtrValueOrError(_:Ptr, E:SemanticsError) => E + syntax Bool ::= mayBeDefaultTypedInt(Value) [function, total] rule mayBeDefaultTypedInt(_V) => false [owise] rule mayBeDefaultTypedInt(u128(_)) => true @@ -43,13 +51,21 @@ module RUST-REPRESENTATION syntax FunctionBodyRepresentation ::= block(BlockExpression) | "empty" - syntax NormalizedFunctionParameter ::= Identifier ":" Type + | storageAccessor(StringLiteral) + syntax ValueName ::= Identifier | SelfSort + syntax NormalizedFunctionParameter ::= ValueName ":" Type syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","} - syntax NormalizedCallParams ::=List{Int, ","} + syntax NormalizedCallParams ::=List{Ptr, ","} syntax Instruction ::= normalizedMethodCall(TypePath, Identifier, NormalizedCallParams) | implicitCastTo(Type) + | methodCall + ( self: Expression + , method:Identifier + , params: CallParamsList + ) + [seqstrict(1, 3), result(ValueWithPtr)] syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError @@ -63,6 +79,12 @@ module RUST-REPRESENTATION syntax MaybeIdentifier ::= ".Identifier" | Identifier + syntax ExpressionOrCallParams ::= Expression | CallParams + + syntax Bool ::= isConstant(ValueName) [function, total] + syntax Bool ::= isLocalVariable(ValueName) [function, total] + syntax Bool ::= isValueWithPtr(K) [function, total, symbol(isValueWithPtr)] + endmodule ``` diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md index 2cf8122..bad7899 100644 --- a/rust-semantics/rust-common-syntax.md +++ b/rust-semantics/rust-common-syntax.md @@ -82,7 +82,7 @@ module RUST-SHARED-SYNTAX syntax Visibility ::= "pub" | "pub" "(" "crate" ")" - | "pub" "(" "self" ")" + | "pub" "(" SelfSort ")" | "pub" "(" "super" ")" | "pub" "(" "in" SimplePath ")" @@ -92,7 +92,7 @@ module RUST-SHARED-SYNTAX syntax SimplePath ::= SimplePathList | "::" SimplePathList syntax SimplePathList ::= NeList{SimplePathSegment, "::"} - syntax SimplePathSegment ::= Identifier | "super" | "self" | "crate" | "$crate" + syntax SimplePathSegment ::= Identifier | "super" | SelfSort | "crate" | "$crate" ``` https://doc.rust-lang.org/reference/items/modules.html @@ -154,11 +154,11 @@ https://doc.rust-lang.org/reference/items/extern-crates.html syntax SelfParam ::= OuterAttributes ShorthandOrTypedSelf syntax ShorthandOrTypedSelf ::= ShorthandSelf | TypedSelf - syntax ShorthandSelf ::= MaybeReferenceOrReferenceLifetime MaybeMutable "self" + syntax ShorthandSelf ::= MaybeReferenceOrReferenceLifetime MaybeMutable SelfSort syntax MaybeReferenceOrReferenceLifetime ::= "" | ReferenceOrReferenceLifetime syntax ReferenceOrReferenceLifetime ::= "&" | "&" Lifetime syntax MaybeMutable ::= "" | "mut" - syntax TypedSelf ::= MaybeMutable "self" ":" Type + syntax TypedSelf ::= MaybeMutable SelfSort ":" Type syntax FunctionParam ::= OuterAttributes FunctionParamDetail // TODO: Missing cases syntax FunctionParamDetail ::= FunctionParamPattern @@ -322,7 +322,6 @@ https://doc.rust-lang.org/reference/items/extern-crates.html | AsyncBlockExpression | ContinueExpression | BreakExpression - | ReturnExpression | UnderscoreExpression | CallExpression @@ -335,7 +334,9 @@ https://doc.rust-lang.org/reference/items/extern-crates.html // to make it easy to disambiguate based on priority syntax Expression ::= PathExpression - > MethodCallExpression + // https://doc.rust-lang.org/reference/expressions/method-call-expr.html + > Expression "." PathExprSegment "(" ")" + | Expression "." PathExprSegment "(" CallParams ")" > Expression "." Identifier // FieldExpression @@ -399,6 +400,11 @@ https://doc.rust-lang.org/reference/items/extern-crates.html | Expression "<<=" Expression | Expression ">>=" Expression + // https://doc.rust-lang.org/reference/expressions/return-expr.html + > "return" + | "return" Expression + + syntax ExpressionWithBlock ::= BlockExpression | UnsafeBlockExpression | LoopExpression @@ -423,7 +429,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html syntax PathInExpression ::= PathExprSegments | "::" PathExprSegments syntax PathExprSegments ::= NeList{PathExprSegment, "::"} syntax PathExprSegment ::= PathIdentSegment | PathIdentSegment "::" GenericArgs - syntax PathIdentSegment ::= Identifier | "super" | "self" | "Self" | "crate" | "$crate" + syntax PathIdentSegment ::= Identifier | "super" | SelfSort | "Self" | "crate" | "$crate" syntax GenericArgs ::= "<" ">" | "<" GenericArgList MaybeComma ">" syntax GenericArgList ::= NeList{GenericArg, ","} // TODO: Not implemented properly @@ -527,16 +533,6 @@ https://doc.rust-lang.org/reference/items/extern-crates.html syntax CallParams ::= CallParamsList | CallParamsList "," syntax CallParamsList ::= NeList{Expression, ","} -``` - - https://doc.rust-lang.org/reference/expressions/method-call-expr.html - -```k - - // TODO: Not implemented properly to avoid ambiguities - syntax MethodCallExpression ::= PathExpression "." PathExprSegment "(" MaybeCallParams ")" - | MethodCallExpression "." PathExprSegment "(" MaybeCallParams ")" - ``` https://doc.rust-lang.org/reference/expressions/closure-expr.html @@ -569,15 +565,6 @@ https://doc.rust-lang.org/reference/items/extern-crates.html syntax BreakExpression ::= "TODO: not needed yet, not implementing" -``` - - https://doc.rust-lang.org/reference/expressions/return-expr.html - -```k - - syntax ReturnExpression ::= "return" MaybeExpression - syntax MaybeExpression ::= "" | Expression - ``` https://doc.rust-lang.org/reference/expressions/underscore-expr.html @@ -1067,6 +1054,8 @@ https://doc.rust-lang.org/reference/items/extern-crates.html // TODO: Not implemented properly syntax TypeParam ::= Identifier + syntax SelfSort ::= "self" + syntax Underscore [token] syntax Identifier [token] endmodule diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md index 7f98469..ee6f3e8 100644 --- a/rust-semantics/test/execution.md +++ b/rust-semantics/test/execution.md @@ -10,6 +10,7 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX | "call" TypePath "." Identifier | "return_value" | "check_eq" Expression [strict] + | "push" Expression [strict] endmodule module RUST-EXECUTION-TEST @@ -27,7 +28,7 @@ module RUST-EXECUTION-TEST rule new P:TypePath => .K ... - .List => ListItem(NVI) ... + .List => ListItem(ptr(NVI)) ... P VALUES:Map => VALUES[NVI <- struct(P, .Map)] NVI:Int => NVI +Int 1 @@ -66,12 +67,18 @@ module RUST-EXECUTION-TEST ) => normalizedMethodCall(TraitName, MethodName, Args) rule - (V:Value ~> return_value ; Es:ExecutionTest) => Es ... + (V:PtrValue ~> return_value ; Es:ExecutionTest) => Es ... .List => ListItem(V) ... rule - check_eq V:Value => .K ... - ListItem(V) => .List ... + check_eq ptrValue(_, V:Value) => .K ... + ListItem(ptrValue(_, V)) => .List ... + + rule + push ptrValue(_, V:Value) => .K ... + .List => ListItem(ptr(NVI)) ... + VALUES:Map => VALUES[NVI <- V] + NVI:Int => NVI +Int 1 endmodule diff --git a/tests/execution/function-call.1.run b/tests/execution/function-call.1.run new file mode 100644 index 0000000..cb55780 --- /dev/null +++ b/tests/execution/function-call.1.run @@ -0,0 +1,2 @@ +new FunctionCalls; +call FunctionCalls.call_empty diff --git a/tests/execution/function-call.2.run b/tests/execution/function-call.2.run new file mode 100644 index 0000000..5b7dae9 --- /dev/null +++ b/tests/execution/function-call.2.run @@ -0,0 +1,4 @@ +new FunctionCalls; +call FunctionCalls.call_one; +return_value; +check_eq 1_u64 diff --git a/tests/execution/function-call.3.run b/tests/execution/function-call.3.run new file mode 100644 index 0000000..4f4b8fe --- /dev/null +++ b/tests/execution/function-call.3.run @@ -0,0 +1,4 @@ +new FunctionCalls; +call FunctionCalls.call_sum; +return_value; +check_eq 3_u64 diff --git a/tests/execution/function-call.4.run b/tests/execution/function-call.4.run new file mode 100644 index 0000000..dbc41b4 --- /dev/null +++ b/tests/execution/function-call.4.run @@ -0,0 +1,4 @@ +new FunctionCalls; +call FunctionCalls.call_ref; +return_value; +check_eq 3_u64 diff --git a/tests/execution/function-call.5.run b/tests/execution/function-call.5.run new file mode 100644 index 0000000..a2778f2 --- /dev/null +++ b/tests/execution/function-call.5.run @@ -0,0 +1,4 @@ +new FunctionCalls; +call FunctionCalls.call_chained; +return_value; +check_eq 1_u64 diff --git a/tests/execution/function-call.7.run b/tests/execution/function-call.7.run new file mode 100644 index 0000000..942835a --- /dev/null +++ b/tests/execution/function-call.7.run @@ -0,0 +1,6 @@ +new FunctionCalls; +push 1_u64; +push 3_u64; +call FunctionCalls.call_arguments; +return_value; +check_eq 4_u64 diff --git a/tests/execution/function-call.rs b/tests/execution/function-call.rs new file mode 100644 index 0000000..ec3db18 --- /dev/null +++ b/tests/execution/function-call.rs @@ -0,0 +1,46 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait FunctionCalls { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + + fn call_empty(&self) { + self.empty() + } + fn empty(&self) {} + + fn call_one(&self) -> u64 { + self.one() + } + fn one(&self) -> u64 { 1u64 } + + fn call_sum(&self) -> u64 { + self.sum(1u64, 2u64) + } + fn sum(&self, first: u64, second: u64) -> u64 { first + second } + + fn call_ref(&self) -> u64 { + self.sum_ref(&1u64, &2u64) + } + fn sum_ref(&self, first: &u64, second: &u64) -> u64 { first + second } + + fn call_chained(&self) -> u64 { + self.get_self().one() + } + fn get_self(&self) -> FunctionCalls { self } + + fn call_arguments(&self, x: u64, y: &u64) -> u64 { + self.sum_arguments(x, y) + } + fn sum_arguments(&self, x: u64, y: &u64) -> u64 { + x + y + } +}