From 753b247c45fac5e28b67a506045ca3863deab30a Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Wed, 21 Aug 2024 20:53:41 +0300 Subject: [PATCH] Preprocess constants --- Makefile | 1 - rust-semantics/expression.md | 9 ++ rust-semantics/expression/casts.md | 41 ++++++++ rust-semantics/expression/literals.md | 97 +++++++++++++++++++ rust-semantics/preprocessing.md | 3 +- rust-semantics/preprocessing/configuration.md | 4 +- rust-semantics/preprocessing/constants.md | 27 ++++++ rust-semantics/preprocessing/crate.md | 37 +++---- .../preprocessing/initialization.md | 6 +- rust-semantics/preprocessing/syntax.md | 2 - rust-semantics/representation.md | 12 +++ rust-semantics/rust.md | 2 + rust-semantics/syntax.md | 44 ++++++++- tests/execution/casts-int.rs | 39 ++++++++ tests/execution/constants.rs | 19 ++++ 15 files changed, 303 insertions(+), 40 deletions(-) create mode 100644 rust-semantics/expression.md create mode 100644 rust-semantics/expression/casts.md create mode 100644 rust-semantics/expression/literals.md create mode 100644 rust-semantics/preprocessing/constants.md create mode 100644 tests/execution/casts-int.rs create mode 100644 tests/execution/constants.rs diff --git a/Makefile b/Makefile index d5f00d3..f713aa8 100644 --- a/Makefile +++ b/Makefile @@ -26,7 +26,6 @@ test: syntax-test indexing-test syntax-test: $(SYNTAX_OUTPUTS) indexing-test: $(INDEXING_OUTPUTS) - echo $(INDEXING_OUTPUTS) $(RUST_TIMESTAMP): $(SEMANTICS_FILES) $$(which kompile) rust-semantics/rust.md -o $(RUST_KOMPILED) diff --git a/rust-semantics/expression.md b/rust-semantics/expression.md new file mode 100644 index 0000000..fb6a5a6 --- /dev/null +++ b/rust-semantics/expression.md @@ -0,0 +1,9 @@ +```k +requires "expression/casts.md" +requires "expression/literals.md" + +module RUST-EXPRESSION + imports private RUST-CASTS + imports private RUST-EXPRESSION-LITERALS +endmodule +``` diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md new file mode 100644 index 0000000..5c09b8e --- /dev/null +++ b/rust-semantics/expression/casts.md @@ -0,0 +1,41 @@ +```k + +module RUST-CASTS + imports private RUST-REPRESENTATION + + syntax ValueOrError ::= cast(Value, Type) [function, total] + + rule cast(V:Value, T:Type) => error("Unknown cast.", ListItem(V) ListItem(T)) + [owise] + + // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast + + rule cast(i32(Value), i32) => i32(Value) + rule cast(i32(Value), u32) => u32(Value) + rule cast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value))) + rule cast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value))) + + rule cast(u32(Value), i32) => i32(Value) + rule cast(u32(Value), u32) => u32(Value) + rule cast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) + rule cast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) + + + rule cast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value))) + rule cast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value))) + rule cast(i64(Value), i64) => i64(Value) + rule cast(i64(Value), u64) => u64(Value) + + rule cast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) + rule cast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) + rule cast(u64(Value), i64) => i64(Value) + rule cast(u64(Value), u64) => u64(Value) + + rule cast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) + rule cast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) + rule cast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) + rule cast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) + +endmodule + +``` diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md new file mode 100644 index 0000000..ea8ffbd --- /dev/null +++ b/rust-semantics/expression/literals.md @@ -0,0 +1,97 @@ +```k +module RUST-EXPRESSION-LITERALS + imports private RUST-EXPRESSION-INTEGER-LITERALS +endmodule + +module RUST-EXPRESSION-INTEGER-LITERALS + imports BOOL + imports INT + imports K-EQUAL-SYNTAX + imports STRING + imports private RUST-REPRESENTATION + imports RUST-SHARED-SYNTAX + + // https://doc.rust-lang.org/stable/reference/expressions/literal-expr.html#integer-literal-expressions + // https://doc.rust-lang.org/stable/reference/tokens.html#number-literals + + syntax String ::= IntegerLiteralToString(IntegerLiteral) [function, total, hook(STRING.token2string)] + + rule I:IntegerLiteral => parseInteger(I) + + syntax ValueOrError ::= parseInteger(IntegerLiteral) [function, total] + | parseInteger(String) [function, total] + rule parseInteger(I:IntegerLiteral) => parseInteger(IntegerLiteralToString(I)) + rule parseInteger(I:String) => parseIntegerNormalized(replaceAll(I, "_", "")) + + syntax ValueOrError ::= parseIntegerNormalized(String) [function, total] + rule parseIntegerNormalized(I:String) => error("Literal not handled", I) + requires startsWith(I, "0b") orBool startsWith(I, "0x") orBool startsWith(I, "0o") + rule parseIntegerNormalized(I:String) => parseIntegerDecimalSplit(I, findSuffix(I)) [owise] + + syntax IntegerSuffix ::= findSuffix(String) [function, total] + rule findSuffix(S) => suffix(i32, 3) requires endsWith(S, "i32") + rule findSuffix(S) => suffix(u32, 3) requires endsWith(S, "u32") + rule findSuffix(S) => suffix(i64, 3) requires endsWith(S, "i64") + rule findSuffix(S) => suffix(u64, 3) requires endsWith(S, "u64") + rule findSuffix(_) => suffix(( ), 0) [owise] + + syntax IntegerSuffix ::= suffix(Type, Int) + syntax ValueOrError ::= parseIntegerDecimalSplit(String, IntegerSuffix) [function, total] + rule parseIntegerDecimalSplit(I:String, suffix(T:Type, Length)) + => parseIntegerDecimal(substrString(I, 0, lengthString(I) -Int Length), T) + requires Length <=Int lengthString(I) + rule parseIntegerDecimalSplit(S:String, IS:IntegerSuffix) + => error("parseIntegerDecimalSplit", ListItem(S) ListItem(IS)) + [owise] + + syntax ValueOrError ::= parseIntegerDecimal(String, Type) [function, total] + rule parseIntegerDecimal(I:String, T:Type) => integerToValue(String2Int(I), T) + requires isDecimal(I) andBool lengthString(I) >Int 0 + rule parseIntegerDecimal(S:String, T:Type) + => error("parseIntegerDecimal: Unrecognized integer", ListItem(S) ListItem(T)) + + syntax Bool ::= isDecimalDigit(String) [function, total] + rule isDecimalDigit(S) => "0" <=String S andBool S <=String "9" + + syntax Bool ::= isDecimal(String) [function, total] + rule isDecimal("") => true + rule isDecimal(S:String) => isDecimalDigit(substrString(S, 0:Int, 1:Int)) andBool isDecimal(substrString(S, 1, lengthString(S))) + [owise] + + + syntax ValueOrError ::= integerToValue(Int, Type) [function, total] + rule integerToValue(I:Int, i32) => i32(Int2MInt(I)) + requires sminMInt(32) <=Int I andBool I <=Int smaxMInt(32) + rule integerToValue(I:Int, u32) => u32(Int2MInt(I)) + requires uminMInt(32) <=Int I andBool I <=Int umaxMInt(32) + rule integerToValue(I:Int, i64) => i64(Int2MInt(I)) + requires sminMInt(64) <=Int I andBool I <=Int smaxMInt(64) + rule integerToValue(I:Int, u64) => u64(Int2MInt(I)) + requires uminMInt(64) <=Int I andBool I <=Int umaxMInt(64) + rule integerToValue(I:Int, ( )) => u128(Int2MInt(I)) + rule integerToValue(I:Int, T:Type) + => error("integerToValue: unimplemented", ListItem(I:Int:KItem) ListItem(T:Type:KItem)) + [owise] + + syntax Bool ::= endsWith(containing:String, contained:String) [function, total] + rule endsWith(Containing:String, Contained:String) + => substrString + ( Containing + , lengthString(Containing) -Int lengthString(Contained) + , lengthString(Containing) + ) ==K Contained + requires lengthString(Contained) <=Int lengthString(Containing) + rule endsWith(_, _) => false [owise] + + syntax Bool ::= startsWith(containing:String, contained:String) [function, total] + rule startsWith(Containing:String, Contained:String) + => substrString + ( Containing + , 0 + , lengthString(Contained) + ) ==K Contained + requires lengthString(Contained) <=Int lengthString(Containing) + rule startsWith(_, _) => false [owise] + +endmodule +``` diff --git a/rust-semantics/preprocessing.md b/rust-semantics/preprocessing.md index 030bf02..879f4a7 100644 --- a/rust-semantics/preprocessing.md +++ b/rust-semantics/preprocessing.md @@ -1,5 +1,6 @@ ```k +requires "preprocessing/constants.md" requires "preprocessing/crate.md" requires "preprocessing/configuration.md" requires "preprocessing/helpers.md" @@ -9,11 +10,11 @@ requires "preprocessing/trait.md" requires "preprocessing/trait-methods.md" module RUST-PREPROCESSING + imports private RUST-CONSTANTS imports private CRATE imports private INITIALIZATION imports private TRAIT imports private TRAIT-METHODS endmodule - ``` diff --git a/rust-semantics/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md index c2f5162..585745f 100644 --- a/rust-semantics/preprocessing/configuration.md +++ b/rust-semantics/preprocessing/configuration.md @@ -10,7 +10,7 @@ module RUST-PREPROCESSING-CONFIGURATION - my_identifier + .Identifier tuple(.ValueList) @@ -19,7 +19,7 @@ module RUST-PREPROCESSING-CONFIGURATION my_identifier:TypePath - my_identifier + .Identifier .NormalizedFunctionParameterList ():Type empty:FunctionBodyRepresentation diff --git a/rust-semantics/preprocessing/constants.md b/rust-semantics/preprocessing/constants.md new file mode 100644 index 0000000..43fbcd7 --- /dev/null +++ b/rust-semantics/preprocessing/constants.md @@ -0,0 +1,27 @@ +```k +module RUST-CONSTANTS + imports private RUST-CASTS + imports private RUST-REPRESENTATION + imports private RUST-RUNNING-CONFIGURATION + imports private RUST-SHARED-SYNTAX + + syntax KItem ::= setConstant(Identifier, ValueOrError) + + rule + (const Name:Identifier : T:Type = V:Value;):ConstantItem:KItem + => setConstant(Name, cast(V, T)) + + rule + + setConstant(Name, V:Value) => .K + ... + + + .Bag => + Name + V + + ... + +endmodule +``` \ No newline at end of file diff --git a/rust-semantics/preprocessing/crate.md b/rust-semantics/preprocessing/crate.md index 7acd05d..a305429 100644 --- a/rust-semantics/preprocessing/crate.md +++ b/rust-semantics/preprocessing/crate.md @@ -8,16 +8,14 @@ module CRATE imports private RUST-REPRESENTATION imports private RUST-RUNNING-CONFIGURATION - syntax MaybeIdentifier ::= ".Identifier" | Identifier - syntax Initializer ::= crateParser(crate: Crate, constants: Map, traitName: MaybeIdentifier, traitFunctions: Map) + syntax Initializer ::= crateParser(crate: Crate, traitName: MaybeIdentifier, traitFunctions: Map) - rule crateParser(C:Crate) => crateParser(... crate : C, constants : .Map, traitName : .Identifier, traitFunctions : .Map) + rule crateParser(C:Crate) => crateParser(... crate : C, traitName : .Identifier, traitFunctions : .Map) rule crateParser ( ... crate: (_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate => (.InnerAttributes Is):Crate - , constants : _Constants:Map , traitName : _Name:MaybeIdentifier , traitFunctions: _TraitFunctions:Map ) @@ -27,7 +25,6 @@ module CRATE ( ... crate: (_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate => (.InnerAttributes (ItemAtts T):Item Is):Crate - , constants : _Constants:Map , traitName : .Identifier , traitFunctions: .Map ) @@ -38,38 +35,26 @@ module CRATE ( ... crate: (_Atts:InnerAttributes (_ItemAtts:OuterAttributes _T:Trait):Item Is:Items):Crate => (.InnerAttributes Is):Crate - , constants : _Constants:Map , traitName : .Identifier => Name , traitFunctions: .Map => Functions ) - // rule (.K => CI:ConstantItem:KItem) - // ~> crateParser - // ( ... crate: - // (Atts:InnerAttributes (_ItemAtts:OuterAttributes CI:ConstantItem):Item Is:Items):Crate - // => (Atts Is):Crate - // , constants : _Constants:Map - // , traitName : _Name:MaybeIdentifier - // , traitFunctions: _TraitFunctions:Map - // ) - // rule ((const Name:Identifier : _T:Type = V:Value;):ConstantItem:KItem => .K) - // ~> crateParser - // ( ... crate : _C:Crate - // , constants : Constants:Map => Constants[Name:Identifier:KItem <- V:Value:KItem] - // , traitName : _Name:MaybeIdentifier - // , traitFunctions: _TraitFunctions:Map - // ) + rule (.K => CI:ConstantItem:KItem) + ~> crateParser + ( ... crate: + (Atts:InnerAttributes (_ItemAtts:OuterAttributes _:MaybeVisibility CI:ConstantItem):Item Is:Items):Crate + => (Atts Is):Crate + , traitName : _Name:MaybeIdentifier + , traitFunctions: _TraitFunctions:Map + ) rule crateParser ( ... crate: (_Atts:InnerAttributes .Items):Crate - , constants : Constants:Map , traitName : Name:Identifier , traitFunctions: Functions:Map ) - => constantInitializer - ( ... constantNames: keys_list(Constants), constants: Constants ) - ~> traitInitializer(Name) + => traitInitializer(Name) ~> traitMethodInitializer ( ... traitName: Name , functionNames:keys_list(Functions), functions: Functions diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md index c455036..e35e93d 100644 --- a/rust-semantics/preprocessing/initialization.md +++ b/rust-semantics/preprocessing/initialization.md @@ -5,14 +5,12 @@ module INITIALIZATION imports private RUST-PREPROCESSING-PRIVATE-HELPERS imports private RUST-PREPROCESSING-PRIVATE-SYNTAX - rule constantInitializer(... constantNames : .List) => .K - rule (.K => addMethod(TraitName, F, A)) ~> traitMethodInitializer ( ... traitName : TraitName:TypePath - , functionNames: (ListItem(Name:Identifier) => .List) _Names:List + , functionNames: (ListItem(Name:Identifier:KItem) => .List) _Names:List , functions: _Functions:Map - ((Name |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map) + ((Name:Identifier:KItem |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map) ) rule traitMethodInitializer(... functionNames: .List) => .K diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md index 768bd1a..1b5867f 100644 --- a/rust-semantics/preprocessing/syntax.md +++ b/rust-semantics/preprocessing/syntax.md @@ -14,8 +14,6 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX syntax Initializer ::= traitParser(Trait) | traitMethodsParser(AssociatedItems, functions: Map, traitName:Identifier) - | constantInitializer - ( constantNames: List, constants: Map ) | traitInitializer ( traitName: TypePath ) diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index 6e87048..578d193 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -2,6 +2,7 @@ module RUST-REPRESENTATION imports INT + imports LIST // for filling the second argument of `error`. imports MINT imports RUST-SHARED-SYNTAX @@ -9,6 +10,7 @@ module RUST-REPRESENTATION syntax MInt{16} syntax MInt{32} syntax MInt{64} + syntax MInt{128} syntax SemanticsError ::= error(String, KItem) @@ -24,12 +26,22 @@ module RUST-REPRESENTATION | u32(MInt{32}) | i64(MInt{64}) | u64(MInt{64}) + | u128(MInt{128}) | tuple(ValueList) syntax ValueList ::= List{Value, ","} syntax Expression ::= Value + syntax KResult ::= Value + + syntax ValueOrError ::= Value | SemanticsError syntax Type ::= "$selftype" + syntax Identifier ::= "i32" [token] + | "u32" [token] + | "i64" [token] + | "u64" [token] + syntax MaybeIdentifier ::= ".Identifier" | Identifier + endmodule ``` \ No newline at end of file diff --git a/rust-semantics/rust.md b/rust-semantics/rust.md index 4b12db2..f429be9 100644 --- a/rust-semantics/rust.md +++ b/rust-semantics/rust.md @@ -1,11 +1,13 @@ ```k requires "config.md" +requires "expression.md" requires "preprocessing.md" requires "representation.md" requires "syntax.md" module RUST imports RUST-CONFIGURATION + imports RUST-EXPRESSION imports RUST-PREPROCESSING imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX diff --git a/rust-semantics/syntax.md b/rust-semantics/syntax.md index 1470240..5bb4946 100644 --- a/rust-semantics/syntax.md +++ b/rust-semantics/syntax.md @@ -201,9 +201,9 @@ https://doc.rust-lang.org/reference/items/extern-crates.html ```k - syntax ConstantItem ::= "const" IdentifierOrUnderscore ":" Type MaybeEqualsExpression ";" + syntax ConstantItem ::= "const" IdentifierOrUnderscore ":" Type "=" Expression ";" [strict(3)] + | "const" IdentifierOrUnderscore ":" Type ";" syntax IdentifierOrUnderscore ::= Identifier | Underscore - syntax MaybeEqualsExpression ::= "" | "=" Expression ``` @@ -941,8 +941,44 @@ https://doc.rust-lang.org/reference/items/extern-crates.html ```k - syntax TypePath ::= TypePathSegments | "::" TypePathSegments - syntax TypePathSegments ::= NeList{TypePathSegment, "::"} + syntax TypePath ::= TypePathSegments + | "::" TypePathSegments + // There is a K bug somewhere which causes an identifier to be either directly + // injected in Type (Identifier -> PathIdentSegment -> TypePathSegment -> + // TypePathSegments -> TypePath -> TypeNoBounds -> Type) or to be included + // through a constructor (concatTypePathSegments(Identifier, .TypePathSegments)). + // This is really annoying because it does not generate compilation errors, + // but causes rules to not apply properly. + // + // As an example, this means that you can't simply write + // + // rule cast(u64(Value), u64) => u64(Value) + // + // because that rule will compile just fine, but it will never apply at + // runtime because it uses an injection (why??? there is no injection + // available!), while the parser will produce actual TypePathSegments lists + // (the K rule will also produce lists from `u64` sometimes, I'm not yet sure + // when). Instead, you need to write + // + // rule cast(u64(Value), u64 :: .TypePathSegments) => u64(Value) + // + // which will work, but you have to figure out all cases where this may happen + // without any help from the compiler. + // + // FWIW, one way of producing a list in K instead of an injection is to do + // something like: + // + // syntax KItem ::= tmp(TypePathSegments) + // rule stuff => tmp(u64) + // + // I'm not sure why one does not get an injection here (but it switches back + // to injections when replacing TypePathSegments by Type). This behaviour is + // inconsistent, and it's a bug to use injections here. + // + // I just wanted to say that I think it's better to not use NeList here. + // + // syntax TypePathSegments ::= NeList{TypePathSegment, "::"} + syntax TypePathSegments ::= TypePathSegment | TypePathSegment "::" TypePathSegments syntax TypePathSegment ::= PathIdentSegment | PathIdentSegment TypePathSegmentSuffix syntax TypePathSegmentSuffix ::= TypePathSegmentSuffixSuffix | "::" TypePathSegmentSuffixSuffix // TODO: Not implemented properly diff --git a/tests/execution/casts-int.rs b/tests/execution/casts-int.rs new file mode 100644 index 0000000..b4ac518 --- /dev/null +++ b/tests/execution/casts-int.rs @@ -0,0 +1,39 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +pub const I32_01: i32 = 10_i32; +pub const I32_02: i32 = 10_u32; +pub const I32_03: i32 = 10_i64; +pub const I32_04: i32 = 10_u64; +pub const I32_05: i32 = 10; + +pub const U32_01: u32 = 10_i32; +pub const U32_02: u32 = 10_u32; +pub const U32_03: u32 = 10_i64; +pub const U32_04: u32 = 10_u64; +pub const U32_05: u32 = 10; + +pub const I64_01: i64 = 10_i32; +pub const I64_02: i64 = 10_u32; +pub const I64_03: i64 = 10_i64; +pub const I64_04: i64 = 10_u64; +pub const I64_05: i64 = 10; + +pub const U64_01: u64 = 10_i32; +pub const U64_02: u64 = 10_u32; +pub const U64_03: u64 = 10_i64; +pub const U64_04: u64 = 10_u64; +pub const U64_05: u64 = 10; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + +} diff --git a/tests/execution/constants.rs b/tests/execution/constants.rs new file mode 100644 index 0000000..6e2f715 --- /dev/null +++ b/tests/execution/constants.rs @@ -0,0 +1,19 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +pub const UNSIGNED_CONSTANT: u64 = 10_u64; +pub const SIGNED_CONSTANT: u32 = 10; +pub const LARGE_CONSTANT: u64 = 100_000_u64; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + +}