diff --git a/Dockerfile b/Dockerfile index 418d523..305329a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,26 +1,17 @@ ARG Z3_VERSION ARG K_COMMIT - -ARG Z3_VERSION=4.12.1 -FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3 +ARG LLVM_VERSION ARG K_COMMIT -FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_COMMIT} - -COPY --from=Z3 /usr/bin/z3 /usr/bin/z3 +FROM runtimeverificationinc/kframework-k:ubuntu-noble-${K_COMMIT} RUN apt-get update \ && apt-get upgrade --yes \ && apt-get install --yes \ curl -# cmake \ -# pandoc \ -# python3 \ -# python3-pip \ -# wabt -ARG USER_ID=1000 -ARG GROUP_ID=1000 +ARG USER_ID=1001 +ARG GROUP_ID=1001 RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user USER user:user @@ -28,8 +19,4 @@ WORKDIR /home/user RUN curl -sSL https://install.python-poetry.org | python3 - --version 1.7.1 -# RUN pip3 install --user \ -# cytoolz \ -# numpy - ENV PATH=/home/user/.local/bin:$PATH diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md index d0a9fe1..424c992 100644 --- a/rust-semantics/expression/casts.md +++ b/rust-semantics/expression/casts.md @@ -7,89 +7,35 @@ module RUST-CASTS rule implicitCast(V:Value, T:Type) => error("Unknown implicitCast.", ListItem(V) ListItem(T)) [owise] - // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-implicitCast + // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast - rule implicitCast(i8(Value), i8 ) => i8 (Value) - rule implicitCast(i8(Value), u8 ) => u8 (Value) - rule implicitCast(i8(Value), i16) => i16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i8(Value), u16) => u16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i8(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(i8(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(i8(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(i8(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) - - rule implicitCast(u8(Value), i8 ) => i8 (Value) - rule implicitCast(u8(Value), u8 ) => u8 (Value) - rule implicitCast(u8(Value), i16) => i16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u8(Value), u16) => u16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u8(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u8(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u8(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u8(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) - - rule implicitCast(i16(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(i16(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(i16(Value), i16) => i16(Value) - rule implicitCast(i16(Value), u16) => u16(Value) - rule implicitCast(i16(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(i16(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(i16(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(i16(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) - - rule implicitCast(u16(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u16(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u16(Value), i16) => i16(Value) - rule implicitCast(u16(Value), u16) => u16(Value) - rule implicitCast(u16(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u16(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u16(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u16(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) - - rule implicitCast(i32(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(i32(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(i32(Value), i16) => i16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i32(Value), u16) => u16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i32(Value), i32) => i32(Value) - rule implicitCast(i32(Value), u32) => u32(Value) - rule implicitCast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value))) - - rule implicitCast(u32(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u32(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u32(Value), i16) => i16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u32(Value), u16) => u16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u32(Value), i32) => i32(Value) - rule implicitCast(u32(Value), u32) => u32(Value) - rule implicitCast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) - - - rule implicitCast(i64(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(i64(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(i64(Value), i16) => i16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i64(Value), u16) => u16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value))) - rule implicitCast(i64(Value), i64) => i64(Value) - rule implicitCast(i64(Value), u64) => u64(Value) - - rule implicitCast(u64(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u64(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u64(Value), i16) => i16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u64(Value), u16) => u16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u64(Value), i64) => i64(Value) - rule implicitCast(u64(Value), u64) => u64(Value) - - rule implicitCast(u128(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u128(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value))) - rule implicitCast(u128(Value), i16) => i16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u128(Value), u16) => u16(Int2MInt(MInt2Signed(Value))) - rule implicitCast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value))) - rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value))) + syntax ValueOrError ::= implicitCast(Int, Type) [function, total] + rule implicitCast(Value:Int, T:Type) + => error("implicitCast(Int, Type)", ListItem(Value) ListItem(T)) + [owise] + rule implicitCast(Value:Int, i8 ) => i8 (Int2MInt(Value)) + rule implicitCast(Value:Int, u8 ) => u8 (Int2MInt(Value)) + rule implicitCast(Value:Int, i16 ) => i16 (Int2MInt(Value)) + rule implicitCast(Value:Int, u16 ) => u16 (Int2MInt(Value)) + rule implicitCast(Value:Int, i32 ) => i32 (Int2MInt(Value)) + rule implicitCast(Value:Int, u32 ) => u32 (Int2MInt(Value)) + rule implicitCast(Value:Int, i64 ) => i64 (Int2MInt(Value)) + rule implicitCast(Value:Int, u64 ) => u64 (Int2MInt(Value)) + rule implicitCast(Value:Int, u128) => u128(Int2MInt(Value)) + rule implicitCast(Value:Int, u160) => u160(Int2MInt(Value)) + rule implicitCast(Value:Int, u256) => u256(Int2MInt(Value)) + + rule implicitCast(i8 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T) + rule implicitCast(u8 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T) + rule implicitCast(i16 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T) + rule implicitCast(u16 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T) + rule implicitCast(i32 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T) + rule implicitCast(u32 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T) + rule implicitCast(i64 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T) + rule implicitCast(u64 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T) + rule implicitCast(u128(Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T) + rule implicitCast(u160(Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T) + rule implicitCast(u256(Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T) rule implicitCast(V:Bool, bool) => V rule implicitCast(S:String, str) => S diff --git a/rust-semantics/expression/comparisons.md b/rust-semantics/expression/comparisons.md index 1c75f95..b85bbda 100644 --- a/rust-semantics/expression/comparisons.md +++ b/rust-semantics/expression/comparisons.md @@ -115,6 +115,20 @@ module RUST-INTEGER-RELATIONAL-OPERATIONS rule ptrValue(_, u128(A):Value) >= ptrValue(_, u128(B):Value) => ptrValue(null, A >=uMInt B) rule ptrValue(_, u128(A):Value) <= ptrValue(_, u128(B):Value) => ptrValue(null, A <=uMInt B) + rule ptrValue(_, u160(A):Value) == ptrValue(_, u160(B):Value) => ptrValue(null, A ==MInt B) + rule ptrValue(_, u160(A):Value) != ptrValue(_, u160(B):Value) => ptrValue(null, A =/=MInt B) + rule ptrValue(_, u160(A):Value) > ptrValue(_, u160(B):Value) => ptrValue(null, A >uMInt B) + rule ptrValue(_, u160(A):Value) < ptrValue(_, u160(B):Value) => ptrValue(null, A = ptrValue(_, u160(B):Value) => ptrValue(null, A >=uMInt B) + rule ptrValue(_, u160(A):Value) <= ptrValue(_, u160(B):Value) => ptrValue(null, A <=uMInt B) + + rule ptrValue(_, u256(A):Value) == ptrValue(_, u256(B):Value) => ptrValue(null, A ==MInt B) + rule ptrValue(_, u256(A):Value) != ptrValue(_, u256(B):Value) => ptrValue(null, A =/=MInt B) + rule ptrValue(_, u256(A):Value) > ptrValue(_, u256(B):Value) => ptrValue(null, A >uMInt B) + rule ptrValue(_, u256(A):Value) < ptrValue(_, u256(B):Value) => ptrValue(null, A = ptrValue(_, u256(B):Value) => ptrValue(null, A >=uMInt B) + rule ptrValue(_, u256(A):Value) <= ptrValue(_, u256(B):Value) => ptrValue(null, A <=uMInt B) + endmodule ``` diff --git a/rust-semantics/expression/integer-operations.md b/rust-semantics/expression/integer-operations.md index 66004a8..86405d7 100644 --- a/rust-semantics/expression/integer-operations.md +++ b/rust-semantics/expression/integer-operations.md @@ -86,6 +86,22 @@ module RUST-INTEGER-ARITHMETIC-OPERATIONS rule ptrValue(_, u128(A):Value) % ptrValue(_, u128(B):Value) => ptrValue(null, u128(A %uMInt B)) requires B =/=K 0p128 + rule ptrValue(_, u160(A):Value) * ptrValue(_, u160(B):Value) => ptrValue(null, u160(A *MInt B)) + rule ptrValue(_, u160(A):Value) + ptrValue(_, u160(B):Value) => ptrValue(null, u160(A +MInt B)) + rule ptrValue(_, u160(A):Value) - ptrValue(_, u160(B):Value) => ptrValue(null, u160(A -MInt B)) + rule ptrValue(_, u160(A):Value) / ptrValue(_, u160(B):Value) => ptrValue(null, u160(A /uMInt B)) + requires B =/=K 0p160 + rule ptrValue(_, u160(A):Value) % ptrValue(_, u160(B):Value) => ptrValue(null, u160(A %uMInt B)) + requires B =/=K 0p160 + + rule ptrValue(_, u256(A):Value) * ptrValue(_, u256(B):Value) => ptrValue(null, u256(A *MInt B)) + rule ptrValue(_, u256(A):Value) + ptrValue(_, u256(B):Value) => ptrValue(null, u256(A +MInt B)) + rule ptrValue(_, u256(A):Value) - ptrValue(_, u256(B):Value) => ptrValue(null, u256(A -MInt B)) + rule ptrValue(_, u256(A):Value) / ptrValue(_, u256(B):Value) => ptrValue(null, u256(A /uMInt B)) + requires B =/=K 0p256 + rule ptrValue(_, u256(A):Value) % ptrValue(_, u256(B):Value) => ptrValue(null, u256(A %uMInt B)) + requires B =/=K 0p256 + endmodule @@ -102,6 +118,8 @@ module RUST-INTEGER-RANGE-OPERATIONS rule (ptrValue(_, i64(A):Value) .. ptrValue(_, i64(B):Value)):Expression => ptrValue(null, intRange(i64(A), i64(B))) rule (ptrValue(_, u64(A):Value) .. ptrValue(_, u64(B):Value)):Expression => ptrValue(null, intRange(u64(A), u64(B))) rule (ptrValue(_, u128(A):Value) .. ptrValue(_, u128(B):Value)):Expression => ptrValue(null, intRange(u128(A), u128(B))) + rule (ptrValue(_, u160(A):Value) .. ptrValue(_, u160(B):Value)):Expression => ptrValue(null, intRange(u160(A), u160(B))) + rule (ptrValue(_, u256(A):Value) .. ptrValue(_, u256(B):Value)):Expression => ptrValue(null, intRange(u256(A), u256(B))) endmodule diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md index fd90bca..789b4be 100644 --- a/rust-semantics/expression/literals.md +++ b/rust-semantics/expression/literals.md @@ -40,6 +40,9 @@ module RUST-EXPRESSION-INTEGER-LITERALS 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(S) => suffix(u128, 4) requires endsWith(S, "u128") + rule findSuffix(S) => suffix(u160, 4) requires endsWith(S, "u160") + rule findSuffix(S) => suffix(u256, 4) requires endsWith(S, "u256") rule findSuffix(_) => suffix(( ), 0) [owise] syntax IntegerSuffix ::= suffix(Type, Int) @@ -82,6 +85,12 @@ module RUST-EXPRESSION-INTEGER-LITERALS 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) => u128(Int2MInt(I)) + requires uminMInt(128) <=Int I andBool I <=Int umaxMInt(128) + rule integerToValue(I:Int, u160) => u160(Int2MInt(I)) + requires uminMInt(160) <=Int I andBool I <=Int umaxMInt(160) + rule integerToValue(I:Int, u256) => u256(Int2MInt(I)) + requires uminMInt(256) <=Int I andBool I <=Int umaxMInt(256) rule integerToValue(I:Int, ( )) => u128(Int2MInt(I)) rule integerToValue(I:Int, T:Type) => error("integerToValue: unimplemented", ListItem(I:Int:KItem) ListItem(T:Type:KItem)) @@ -97,6 +106,8 @@ module RUST-EXPRESSION-INTEGER-LITERALS rule valueToInteger(i64(V:MInt{64})) => MInt2Signed(V) rule valueToInteger(u64(V:MInt{64})) => MInt2Unsigned(V) rule valueToInteger(u128(V:MInt{128})) => MInt2Unsigned(V) + rule valueToInteger(u160(V:MInt{160})) => MInt2Unsigned(V) + rule valueToInteger(u256(V:MInt{256})) => MInt2Unsigned(V) syntax Bool ::= endsWith(containing:String, contained:String) [function, total] rule endsWith(Containing:String, Contained:String) diff --git a/rust-semantics/expression/loops.md b/rust-semantics/expression/loops.md index c6d68b9..766d2c0 100644 --- a/rust-semantics/expression/loops.md +++ b/rust-semantics/expression/loops.md @@ -1,6 +1,7 @@ ```k module RUST-LOOP-EXPRESSIONS + imports K-EQUAL-SYNTAX imports RUST-REPRESENTATION syntax IteratorLoopExpression ::= "for1" Pattern "limit" PtrValue BlockExpression @@ -32,32 +33,22 @@ module RUST-LOOP-EXPRESSIONS syntax LetStatement ::= incrementPatt(Identifier, Value) [function] rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i8 (Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, i8 ) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u8 (Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, u8 ) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i16(Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, i16) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u16(Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, u16) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i32(Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, i32) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u32(Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, u32) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u64(Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, u64) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i64(Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, i64) - rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => - let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u128(Int2MInt(1:Int))); - requires checkIntOfType(ComparisonValue, u128) + let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, oneOfSameType(ComparisonValue)); + requires oneOfSameType(ComparisonValue) =/=K tuple(.ValueList) + + syntax Value ::= oneOfSameType(Value) [function, total] + rule oneOfSameType(_) => tuple(.ValueList) [owise] + rule oneOfSameType(u8 (_)) => u8 (Int2MInt(1)) + rule oneOfSameType(i8 (_)) => i8 (Int2MInt(1)) + rule oneOfSameType(u16 (_)) => u16 (Int2MInt(1)) + rule oneOfSameType(i16 (_)) => i16 (Int2MInt(1)) + rule oneOfSameType(u32 (_)) => u32 (Int2MInt(1)) + rule oneOfSameType(i32 (_)) => i32 (Int2MInt(1)) + rule oneOfSameType(u64 (_)) => u64 (Int2MInt(1)) + rule oneOfSameType(i64 (_)) => i64 (Int2MInt(1)) + rule oneOfSameType(u128(_)) => u128(Int2MInt(1)) + rule oneOfSameType(u160(_)) => u160(Int2MInt(1)) + rule oneOfSameType(u256(_)) => u256(Int2MInt(1)) endmodule diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md index 6ebdcb5..ac59498 100644 --- a/rust-semantics/helpers.md +++ b/rust-semantics/helpers.md @@ -12,6 +12,9 @@ module RUST-HELPERS rule isSameType(_, _) => false [owise] rule isSameType(_:Value, & T => T) rule isSameType(_, $selftype) => true + rule isSameType(u256(_), u256) => true + rule isSameType(u160(_), u160) => true + rule isSameType(u128(_), u128) => true rule isSameType(i64(_), i64) => true rule isSameType(u64(_), u64) => true rule isSameType(i32(_), i32) => true @@ -32,6 +35,8 @@ module RUST-HELPERS rule isUnsignedInt(u32) => true rule isUnsignedInt(u64) => true rule isUnsignedInt(u128) => true + rule isUnsignedInt(u160) => true + rule isUnsignedInt(u256) => true rule isUnsignedInt(&T => T) syntax Bool ::= isSignedInt(Type) [function, total] diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index a4fe88d..cafdfc1 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -13,6 +13,8 @@ module RUST-VALUE-SYNTAX syntax MInt{32} syntax MInt{64} syntax MInt{128} + syntax MInt{160} + syntax MInt{256} syntax SemanticsError ::= error(String, KItem) @@ -25,6 +27,8 @@ module RUST-VALUE-SYNTAX | i64(MInt{64}) | u64(MInt{64}) | u128(MInt{128}) + | u160(MInt{160}) + | u256(MInt{256}) | tuple(ValueList) | struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int) | Range @@ -116,6 +120,8 @@ module RUST-REPRESENTATION | "i64" [token] | "u64" [token] | "u128" [token] + | "u160" [token] + | "u256" [token] | "bool" [token] | "str" [token] @@ -150,7 +156,9 @@ module RUST-REPRESENTATION rule checkIntOfType(i32(_), i32) => true rule checkIntOfType(u64(_), u64) => true rule checkIntOfType(i64(_), i64) => true - rule checkIntOfType(i64(_), u128) => true + rule checkIntOfType(u128(_), u128) => true + rule checkIntOfType(u160(_), u160) => true + rule checkIntOfType(u256(_), u256) => true rule checkIntOfType(_, _) => false [owise] rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u8) requires checkIntOfType(B, u8) @@ -162,6 +170,8 @@ module RUST-REPRESENTATION rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u64) requires checkIntOfType(B, u64) rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, i64) requires checkIntOfType(B, i64) rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u128) requires checkIntOfType(B, u128) + rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u160) requires checkIntOfType(B, u160) + rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u256) requires checkIntOfType(B, u256) rule checkIntOfSameType(_, _) => false [owise] syntax TypePathOrError ::= TypePath | SemanticsError diff --git a/tests/preprocessing/casts_int.rs b/tests/preprocessing/casts_int.rs index 329ea8b..de9c982 100644 --- a/tests/preprocessing/casts_int.rs +++ b/tests/preprocessing/casts_int.rs @@ -11,7 +11,10 @@ pub const I8_05: i8 = 10_i32; pub const I8_06: i8 = 10_u32; pub const I8_07: i8 = 10_i64; pub const I8_08: i8 = 10_u64; -pub const I8_09: i8 = 10; +pub const I8_09: i8 = 10_u128; +pub const I8_10: i8 = 10_u160; +pub const I8_11: i8 = 10_u256; +pub const I8_12: i8 = 10; pub const U8_01: u8 = 10_i8; pub const U8_02: u8 = 10_u8; @@ -21,7 +24,10 @@ pub const U8_05: u8 = 10_i32; pub const U8_06: u8 = 10_u32; pub const U8_07: u8 = 10_i64; pub const U8_08: u8 = 10_u64; -pub const U8_09: u8 = 10; +pub const U8_09: u8 = 10_u128; +pub const U8_10: u8 = 10_u160; +pub const U8_11: u8 = 10_u256; +pub const U8_12: u8 = 10; pub const I16_01: i16 = 10_i8; pub const I16_02: i16 = 10_u8; @@ -31,7 +37,10 @@ pub const I16_05: i16 = 10_i32; pub const I16_06: i16 = 10_u32; pub const I16_07: i16 = 10_i64; pub const I16_08: i16 = 10_u64; -pub const I16_09: i16 = 10; +pub const I16_09: i16 = 10_u128; +pub const I16_10: i16 = 10_u160; +pub const I16_11: i16 = 10_u256; +pub const I16_12: i16 = 10; pub const U16_01: u16 = 10_i8; pub const U16_02: u16 = 10_u8; @@ -41,7 +50,10 @@ pub const U16_05: u16 = 10_i32; pub const U16_06: u16 = 10_u32; pub const U16_07: u16 = 10_i64; pub const U16_08: u16 = 10_u64; -pub const U16_09: u16 = 10; +pub const U16_09: u16 = 10_u128; +pub const U16_10: u16 = 10_u160; +pub const U16_11: u16 = 10_u256; +pub const U16_12: u16 = 10; pub const I32_01: i32 = 10_i8; pub const I32_02: i32 = 10_u8; @@ -51,7 +63,10 @@ pub const I32_05: i32 = 10_i32; pub const I32_06: i32 = 10_u32; pub const I32_07: i32 = 10_i64; pub const I32_08: i32 = 10_u64; -pub const I32_09: i32 = 10; +pub const I32_09: i32 = 10_u128; +pub const I32_10: i32 = 10_u160; +pub const I32_11: i32 = 10_u256; +pub const I32_12: i32 = 10; pub const U32_01: u32 = 10_i8; pub const U32_02: u32 = 10_u8; @@ -61,7 +76,10 @@ pub const U32_05: u32 = 10_i32; pub const U32_06: u32 = 10_u32; pub const U32_07: u32 = 10_i64; pub const U32_08: u32 = 10_u64; -pub const U32_09: u32 = 10; +pub const U32_09: u32 = 10_u128; +pub const U32_10: u32 = 10_u160; +pub const U32_11: u32 = 10_u256; +pub const U32_12: u32 = 10; pub const I64_01: i64 = 10_i8; pub const I64_02: i64 = 10_u8; @@ -71,7 +89,10 @@ pub const I64_05: i64 = 10_i32; pub const I64_06: i64 = 10_u32; pub const I64_07: i64 = 10_i64; pub const I64_08: i64 = 10_u64; -pub const I64_09: i64 = 10; +pub const I64_09: i64 = 10_u128; +pub const I64_10: i64 = 10_u160; +pub const I64_11: i64 = 10_u256; +pub const I64_12: i64 = 10; pub const U64_01: u64 = 10_i8; pub const U64_02: u64 = 10_u8; @@ -81,7 +102,49 @@ pub const U64_05: u64 = 10_i32; pub const U64_06: u64 = 10_u32; pub const U64_07: u64 = 10_i64; pub const U64_08: u64 = 10_u64; -pub const U64_09: u64 = 10; +pub const U64_09: u64 = 10_u128; +pub const U64_10: u64 = 10_u160; +pub const U64_11: u64 = 10_u256; +pub const U64_12: u64 = 10; + +pub const U128_01: u128 = 10_i8; +pub const U128_02: u128 = 10_u8; +pub const U128_03: u128 = 10_i16; +pub const U128_04: u128 = 10_u16; +pub const U128_05: u128 = 10_i32; +pub const U128_06: u128 = 10_u32; +pub const U128_07: u128 = 10_i64; +pub const U128_08: u128 = 10_u64; +pub const U128_09: u128 = 10_u128; +pub const U128_10: u128 = 10_u160; +pub const U128_11: u128 = 10_u256; +pub const U128_12: u128 = 10; + +pub const U160_01: u160 = 10_i8; +pub const U160_02: u160 = 10_u8; +pub const U160_03: u160 = 10_i16; +pub const U160_04: u160 = 10_u16; +pub const U160_05: u160 = 10_i32; +pub const U160_06: u160 = 10_u32; +pub const U160_07: u160 = 10_i64; +pub const U160_08: u160 = 10_u64; +pub const U160_09: u160 = 10_u128; +pub const U160_10: u160 = 10_u160; +pub const U160_11: u160 = 10_u256; +pub const U160_12: u160 = 10; + +pub const U256_01: u256 = 10_i8; +pub const U256_02: u256 = 10_u8; +pub const U256_03: u256 = 10_i16; +pub const U256_04: u256 = 10_u16; +pub const U256_05: u256 = 10_i32; +pub const U256_06: u256 = 10_u32; +pub const U256_07: u256 = 10_i64; +pub const U256_08: u256 = 10_u64; +pub const U256_09: u256 = 10_u128; +pub const U256_10: u256 = 10_u160; +pub const U256_11: u256 = 10_u256; +pub const U256_12: u256 = 10; #[multiversx_sc::contract] pub trait Empty { diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md index ee69b79..e024361 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ukm-semantics/main/hooks/bytes.md @@ -33,6 +33,8 @@ module UKM-HOOKS-BYTES syntax Identifier ::= "bytes_hooks" [token] | "empty" [token] | "length" [token] + | "append_u256" [token] + | "append_u160" [token] | "append_u128" [token] | "append_u64" [token] | "append_u32" [token] @@ -40,6 +42,8 @@ module UKM-HOOKS-BYTES | "append_u8" [token] | "append_bool" [token] | "append_str" [token] + | "decode_u256" [token] + | "decode_u160" [token] | "decode_u128" [token] | "decode_u64" [token] | "decode_u32" [token] @@ -72,6 +76,20 @@ module UKM-HOOKS-BYTES ) => ukmBytesLength(BufferIdId) + rule + normalizedFunctionCall + ( :: bytes_hooks :: append_u256 :: .PathExprSegments + , BufferIdId:Ptr, IntId:Ptr, .PtrList + ) + => ukmBytesAppendInt(BufferIdId, IntId) + + rule + normalizedFunctionCall + ( :: bytes_hooks :: append_u160 :: .PathExprSegments + , BufferIdId:Ptr, IntId:Ptr, .PtrList + ) + => ukmBytesAppendInt(BufferIdId, IntId) + rule normalizedFunctionCall ( :: bytes_hooks :: append_u128 :: .PathExprSegments @@ -121,12 +139,26 @@ module UKM-HOOKS-BYTES ) => ukmBytesAppendStr(BufferIdId, StrId) + rule + normalizedFunctionCall + ( :: bytes_hooks :: decode_u256 :: .PathExprSegments + , BufferIdId:Ptr, .PtrList + ) + => ukmBytesDecode(BufferIdId, u256) + + rule + normalizedFunctionCall + ( :: bytes_hooks :: decode_u160 :: .PathExprSegments + , BufferIdId:Ptr, .PtrList + ) + => ukmBytesDecode(BufferIdId, u160) + rule normalizedFunctionCall ( :: bytes_hooks :: decode_u128 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u32) + => ukmBytesDecode(BufferIdId, u128) rule normalizedFunctionCall @@ -217,6 +249,10 @@ module UKM-HOOKS-BYTES => ptrValue(null, u32(Int2MInt(lengthBytes(Value)))) requires notBool uoverflowMInt(32, lengthBytes(Value)) + rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u256(Value))) + => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) + rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u160(Value))) + => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u128(Value))) => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u64(Value))) diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index 33accc4..f567980 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -151,11 +151,17 @@ module UKM-PREPROCESSING-ENDPOINTS | "append_u16" [token] | "append_u32" [token] | "append_u64" [token] + | "append_u128" [token] + | "append_u160" [token] + | "append_u256" [token] | "append_bool" [token] | "decode_u8" [token] | "decode_u16" [token] | "decode_u32" [token] | "decode_u64" [token] + | "decode_u128" [token] + | "decode_u160" [token] + | "decode_u256" [token] | "decode_str" [token] | "empty" [token] | "ukm" [token] @@ -184,6 +190,9 @@ module UKM-PREPROCESSING-ENDPOINTS rule signatureType(u16) => "Uint16" rule signatureType(u32) => "Uint32" rule signatureType(u64) => "Uint64" + rule signatureType(u128) => "Uint128" + rule signatureType(u160) => "Uint160" + rule signatureType(u256) => "Uint256" rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T)) [owise] @@ -233,6 +242,12 @@ module UKM-PREPROCESSING-ENDPOINTS => v(:: bytes_hooks :: append_u32 ( BufferId , Value , .CallParamsList )) rule appendValue(BufferId:Identifier, Value:Identifier, u64) => v(:: bytes_hooks :: append_u64 ( BufferId , Value , .CallParamsList )) + rule appendValue(BufferId:Identifier, Value:Identifier, u128) + => v(:: bytes_hooks :: append_u128 ( BufferId , Value , .CallParamsList )) + rule appendValue(BufferId:Identifier, Value:Identifier, u160) + => v(:: bytes_hooks :: append_u160 ( BufferId , Value , .CallParamsList )) + rule appendValue(BufferId:Identifier, Value:Identifier, u256) + => v(:: bytes_hooks :: append_u256 ( BufferId , Value , .CallParamsList )) rule appendValue(BufferId:Identifier, Value:Identifier, bool) => v(:: bytes_hooks :: append_bool ( BufferId , Value , .CallParamsList )) rule appendValue(BufferId:Identifier, _Value:Identifier, ()) => v(BufferId) @@ -263,6 +278,9 @@ module UKM-PREPROCESSING-ENDPOINTS rule decodeForType(u16) => v(:: bytes_hooks :: decode_u16 ( buffer_id , .CallParamsList )) rule decodeForType(u32) => v(:: bytes_hooks :: decode_u32 ( buffer_id , .CallParamsList )) rule decodeForType(u64) => v(:: bytes_hooks :: decode_u64 ( buffer_id , .CallParamsList )) + rule decodeForType(u128) => v(:: bytes_hooks :: decode_u128 ( buffer_id , .CallParamsList )) + rule decodeForType(u160) => v(:: bytes_hooks :: decode_u160 ( buffer_id , .CallParamsList )) + rule decodeForType(u256) => v(:: bytes_hooks :: decode_u256 ( buffer_id , .CallParamsList )) syntax Expression ::= callMethod(Identifier, NormalizedFunctionParameterList) [function, total] syntax Expression ::= callMethod(Identifier, CallParamsList) [function, total] diff --git a/ukm-semantics/main/preprocessing/storage.md b/ukm-semantics/main/preprocessing/storage.md index 3391c73..a6b108a 100644 --- a/ukm-semantics/main/preprocessing/storage.md +++ b/ukm-semantics/main/preprocessing/storage.md @@ -69,6 +69,9 @@ module UKM-PREPROCESSING-STORAGE | "append_u16" [token] | "append_u32" [token] | "append_u64" [token] + | "append_u128" [token] + | "append_u160" [token] + | "append_u256" [token] | "empty" [token] | "hash" [token] | "new" [token] @@ -109,6 +112,12 @@ module UKM-PREPROCESSING-STORAGE => v(:: bytes_hooks :: append_u32 ( buffer_id , Name , .CallParamsList )) rule encodeForType(Name:Identifier, u64) => v(:: bytes_hooks :: append_u64 ( buffer_id , Name , .CallParamsList )) + rule encodeForType(Name:Identifier, u128) + => v(:: bytes_hooks :: append_u128 ( buffer_id , Name , .CallParamsList )) + rule encodeForType(Name:Identifier, u160) + => v(:: bytes_hooks :: append_u160 ( buffer_id , Name , .CallParamsList )) + rule encodeForType(Name:Identifier, u256) + => v(:: bytes_hooks :: append_u256 ( buffer_id , Name , .CallParamsList )) endmodule