From b8703b5a77745fcf13d1ebe74e8009bf820a25b6 Mon Sep 17 00:00:00 2001 From: Virgil Date: Sat, 21 Sep 2024 02:52:28 +0300 Subject: [PATCH] Tuples and assignments --- rust-semantics/error.md | 14 ++++++++++ rust-semantics/expression.md | 14 +++++++--- rust-semantics/expression/assignments.md | 20 ++++++++++++++ rust-semantics/expression/expression-list.md | 23 ++++++++++++++++ rust-semantics/expression/tuple.md | 29 ++++++++++++++++++++ rust-semantics/representation.md | 7 +++++ rust-semantics/rust-common.md | 2 ++ rust-semantics/targets/preprocessing/rust.md | 10 ++++--- 8 files changed, 111 insertions(+), 8 deletions(-) create mode 100644 rust-semantics/error.md create mode 100644 rust-semantics/expression/assignments.md create mode 100644 rust-semantics/expression/expression-list.md create mode 100644 rust-semantics/expression/tuple.md diff --git a/rust-semantics/error.md b/rust-semantics/error.md new file mode 100644 index 0000000..328c617 --- /dev/null +++ b/rust-semantics/error.md @@ -0,0 +1,14 @@ +```k + +module RUST-ERROR + imports private RUST-REPRESENTATION + + rule concat(V:Value, L:ValueList) => V , L + rule concat(_:Value, E:SemanticsError) => E + rule concat(E:SemanticsError, _:ValueListOrError) => E + rule concat(E:ValueOrError, L:ValueListOrError) + => error("unexpected branch (concat(ValueOrError, ValueListOrError))", ListItem(E) ListItem(L)) + [owise] +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/expression.md b/rust-semantics/expression.md index c59585d..3fcbc89 100644 --- a/rust-semantics/expression.md +++ b/rust-semantics/expression.md @@ -1,25 +1,31 @@ ```k -requires "expression/calls.md" -requires "expression/integer-operations.md" +requires "expression/assignments.md" requires "expression/blocks.md" requires "expression/bool-operations.md" +requires "expression/calls.md" requires "expression/constants.md" requires "expression/casts.md" requires "expression/conditionals.md" +requires "expression/expression-list.md" +requires "expression/integer-operations.md" requires "expression/literals.md" requires "expression/references.md" requires "expression/struct.md" +requires "expression/tuple.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-BLOCK-EXPRESSIONS imports private RUST-CONDITIONAL-EXPRESSIONS + imports private RUST-EXPRESSION-ASSIGNMENTS + imports private RUST-EXPRESSION-CALLS + imports private RUST-EXPRESSION-CONSTANTS + imports private RUST-EXPRESSION-EXPRESSION-LIST imports private RUST-EXPRESSION-LITERALS imports private RUST-EXPRESSION-REFERENCES imports private RUST-EXPRESSION-STRUCT + imports private RUST-EXPRESSION-TUPLE imports private RUST-EXPRESSION-VARIABLES imports private RUST-INTEGER-OPERATIONS imports private RUST-BOOL-OPERATIONS diff --git a/rust-semantics/expression/assignments.md b/rust-semantics/expression/assignments.md new file mode 100644 index 0000000..5ac3200 --- /dev/null +++ b/rust-semantics/expression/assignments.md @@ -0,0 +1,20 @@ +```k + +module RUST-EXPRESSION-ASSIGNMENTS + imports private COMMON-K-CELL + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-SHARED-SYNTAX + imports private RUST-VALUE-SYNTAX + rule + + ptrValue(ptr(P:Int), _) = ptrValue(_, V:Value) + => ptrValue(null, tuple(.ValueList)) + ... + + + Values:Map => Values[P <- V] + + requires P in_keys(Values) +endmodule + +``` \ No newline at end of file diff --git a/rust-semantics/expression/expression-list.md b/rust-semantics/expression/expression-list.md new file mode 100644 index 0000000..aa59ac3 --- /dev/null +++ b/rust-semantics/expression/expression-list.md @@ -0,0 +1,23 @@ +```k + +module RUST-EXPRESSION-EXPRESSION-LIST + imports RUST-REPRESENTATION + imports RUST-VALUE-SYNTAX + + rule evaluate(L:ExpressionList) => evaluate(expressionListToValueList(L)) + + rule isValueWithPtr(.ExpressionList) => true + rule isValueWithPtr(E:Expression , T:ExpressionList) + => isValueWithPtr(E) andBool isValueWithPtr(T) + + syntax ValueListOrError ::= expressionListToValueList(ExpressionList) [function, total] + + rule expressionListToValueList(.ExpressionList) => .ValueList + rule expressionListToValueList(ptrValue(_, V:Value) , T:ExpressionList) + => concat(V , expressionListToValueList(T)) + rule expressionListToValueList(E:Expression , T:ExpressionList) + => error("Unrecognized expression (expressionListToValueList)", ListItem(E) ListItem(T)) + [owise] +endmodule + +``` diff --git a/rust-semantics/expression/tuple.md b/rust-semantics/expression/tuple.md new file mode 100644 index 0000000..8195137 --- /dev/null +++ b/rust-semantics/expression/tuple.md @@ -0,0 +1,29 @@ +```k + +module RUST-EXPRESSION-TUPLE + imports RUST-REPRESENTATION + imports RUST-VALUE-SYNTAX + + rule ():Expression => ptrValue(null, tuple(.ValueList)) + rule (E:Expression , ):TupleExpression + => tupleExpression(E , .TupleElementsNoEndComma) + rule (E:Expression , T:TupleElementsNoEndComma):TupleExpression + => tupleExpression(E , T) + rule (E:Expression , T:TupleElementsNoEndComma,):TupleExpression + => tupleExpression(E , T) + + syntax Instruction ::= tupleExpression(TupleElementsNoEndComma) + + rule (.K => evaluate(tupleElementsToExpressionList(Es))) + ~> tupleExpression(Es:TupleElementsNoEndComma) + rule (evaluate(L:ValueList) ~> tupleExpression(_:TupleElementsNoEndComma)) + => ptrValue(null, tuple(L)) + + syntax ExpressionList ::= tupleElementsToExpressionList(TupleElementsNoEndComma) [function, total] + + rule tupleElementsToExpressionList(.TupleElementsNoEndComma) => .ExpressionList + rule tupleElementsToExpressionList(E:Expression , Es:TupleElementsNoEndComma) + => E , tupleElementsToExpressionList(Es) +endmodule + +``` diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index e4f9f6b..58d8181 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -29,6 +29,9 @@ module RUST-VALUE-SYNTAX syntax ValueList ::= List{Value, ","} syntax ValueOrError ::= Value | SemanticsError + syntax ValueListOrError ::= ValueList | SemanticsError + syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError) [function, total] + syntax Ptr ::= "null" | ptr(Int) syntax PtrValue ::= ptrValue(Ptr, Value) syntax PtrValueOrError ::= PtrValue | SemanticsError @@ -101,6 +104,10 @@ module RUST-REPRESENTATION syntax CallParamsList ::= reverse(CallParamsList, CallParamsList) [function, total] + syntax ExpressionList ::= ".ExpressionList" + | Expression "," ExpressionList [seqstrict, result(ValueWithPtr)] + syntax InstructionList ::= evaluate(ExpressionList) [strict(1), result(ValueWithPtr)] + | evaluate(ValueListOrError) endmodule ``` diff --git a/rust-semantics/rust-common.md b/rust-semantics/rust-common.md index ecacecc..3b1908d 100644 --- a/rust-semantics/rust-common.md +++ b/rust-semantics/rust-common.md @@ -1,5 +1,6 @@ ```k requires "config.md" +requires "error.md" requires "execution.md" requires "expression.md" requires "helpers.md" @@ -8,6 +9,7 @@ requires "representation.md" requires "rust-common-syntax.md" module RUST-COMMON + imports RUST-ERROR imports RUST-EXECUTION imports RUST-EXPRESSION imports RUST-HELPERS diff --git a/rust-semantics/targets/preprocessing/rust.md b/rust-semantics/targets/preprocessing/rust.md index d17c2f9..2599f38 100644 --- a/rust-semantics/targets/preprocessing/rust.md +++ b/rust-semantics/targets/preprocessing/rust.md @@ -1,20 +1,22 @@ ```k requires "configuration.md" -requires "../../preprocessing.md" -requires "../../representation.md" +requires "../../error.md" +requires "../../expression/bool-operations.md" requires "../../expression/casts.md" requires "../../expression/constants.md" +requires "../../expression/integer-operations.md" requires "../../expression/literals.md" +requires "../../preprocessing.md" +requires "../../representation.md" requires "../../rust-common-syntax.md" -requires "../../expression/integer-operations.md" -requires "../../expression/bool-operations.md" module RUST-SYNTAX imports RUST-COMMON-SYNTAX endmodule module RUST + imports private RUST-ERROR imports private RUST-EXPRESSION-LITERALS imports private RUST-INTEGER-OPERATIONS imports private RUST-BOOL-OPERATIONS