Skip to content

Commit

Permalink
More int types
Browse files Browse the repository at this point in the history
  • Loading branch information
@virgil-serbanuta
virgil-serbanuta committed Oct 1, 2024
1 parent 8692ea7 commit 696bc1e
Show file tree
Hide file tree
Showing 16 changed files with 332 additions and 53 deletions.
4 changes: 3 additions & 1 deletion mx-rust-semantics/main/expression/mx-to-rust.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,9 @@ module MX-RUST-EXPRESSION-MX-TO-RUST
rule mxToRustTyped(T:Type, mxIntValue(I:Int)) => mxRustNewValue(integerToValue(I, T))
requires
(T ==K i32 orBool T ==K u32)
(T ==K i8 orBool T ==K u8)
orBool (T ==K i16 orBool T ==K u16)
orBool (T ==K i32 orBool T ==K u32)
orBool (T ==K i64 orBool T ==K u64)
rule mxToRustTyped(str, mxStringValue(S:String)) => mxRustNewValue(S)
rule mxToRustTyped
Expand Down
10 changes: 9 additions & 1 deletion mx-rust-semantics/main/expression/strings.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,14 @@ module MX-RUST-EXPRESSION-STRINGS
rule concatString(ptrValue(_, S1:String), ptrValue(_, S2:String))
=> ptrValue(null, S1 +String S2)
rule toString(ptrValue(_, i8(Value:MInt{8})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 8 divInt 4))
rule toString(ptrValue(_, u8(Value:MInt{8})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 8 divInt 4))
rule toString(ptrValue(_, i16(Value:MInt{16})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 16 divInt 4))
rule toString(ptrValue(_, u16(Value:MInt{16})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 16 divInt 4))
rule toString(ptrValue(_, i32(Value:MInt{32})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4))
rule toString(ptrValue(_, u32(Value:MInt{32})))
Expand All @@ -20,7 +28,7 @@ module MX-RUST-EXPRESSION-STRINGS
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4))
rule toString(ptrValue(_, u128(Value:MInt{128})))
=> ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 128 divInt 4))
rule toString(ptrValue(null, Value:String)) => ptrValue(null, Value)
rule toString(ptrValue(_, Value:String)) => ptrValue(null, Value)
// TODO: convert all Value entries to string
syntax String ::= padLeftString(value:String, padding:String, count:Int) [function, total]
Expand Down
4 changes: 3 additions & 1 deletion mx-rust-semantics/main/glue.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,9 @@ module MX-RUST-GLUE
rule mxValueToRust(T:Type, mxIntValue(I:Int))
=> mxRustNewValue(integerToValue(I, T))
requires
(T ==K i32 orBool T ==K u32)
(T ==K i8 orBool T ==K u8)
orBool (T ==K i16 orBool T ==K u16)
orBool (T ==K i32 orBool T ==K u32)
orBool (T ==K i64 orBool T ==K u64)
rule ptrValue(_, V) ~> rustValueToMx => rustValueToMx(V)
Expand Down
37 changes: 31 additions & 6 deletions mx-rust-semantics/main/modules/address.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,33 +6,58 @@ module MX-RUST-MODULES-ADDRESS
imports private MX-RUST-REPRESENTATION-CONVERSIONS
imports private RUST-SHARED-SYNTAX
syntax Identifier ::= "ManagedAddress" [token]
| "mx_address_value" [token]
rule
normalizedMethodCall
( ManagedAddress
, #token("zero", "Identifier"):Identifier
, ( .PtrList)
)
=> mxRustEmptyValue(rustType(ManagedAddress))
rule
normalizedMethodCall
( ManagedAddress
, #token("is_zero", "Identifier"):Identifier
, ( ptr(SelfId) , .PtrList)
)
=> ptr(SelfId) . mx_address_value == ""
// --------------------------------------
syntax MxRustType ::= "addressType" [function, total]
rule addressType
=> rustStructType
( #token("ManagedAddress", "Identifier"):Identifier
( ManagedAddress
, ( mxRustStructField
( #token("mx_address_value", "Identifier"):Identifier
( mx_address_value
, str
)
, .MxRustStructFields
)
)
rule mxRustEmptyValue(rustType(#token("ManagedAddress", "Identifier")))
rule mxRustEmptyValue(rustType(ManagedAddress))
=> mxToRustTyped(addressType, mxListValue(mxStringValue("")))
rule mxValueToRust(#token("ManagedAddress", "Identifier"), V:MxValue)
rule mxValueToRust(ManagedAddress, V:MxValue)
=> mxToRustTyped(addressType, mxListValue(V))
rule rustValueToMx
( struct
( #token("ManagedAddress", "Identifier"):Identifier
, #token("mx_address_value", "Identifier"):Identifier |-> AddressValueId:Int
( ManagedAddress
, mx_address_value |-> AddressValueId:Int
.Map
)
)
=> ptr(AddressValueId) ~> rustValueToMx
// --------------------------------------
rule toString(ptrValue(P:Ptr, struct(ManagedAddress, _:Map)))
=> toString(P . #token("mx_address_value", "Identifier"))
endmodule
```
7 changes: 7 additions & 0 deletions mx-rust-semantics/main/preprocessing/methods.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,13 @@ module MX-RUST-PREPROCESSING-METHODS
_:NonEmptyOuterAttributes
, _:Identifier
) => IdentifierToString(Name)
rule getEndpointName
( (#[ #token("view", "Identifier") :: .SimplePathList
( Name:Identifier :: .PathExprSegments, .CallParamsList )
])
_:NonEmptyOuterAttributes
, _:Identifier
) => IdentifierToString(Name)
rule getEndpointName(_:OuterAttribute Atts:NonEmptyOuterAttributes, Default:Identifier)
=> getEndpointName(Atts, Default)
[owise]
Expand Down
56 changes: 56 additions & 0 deletions rust-semantics/expression/casts.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,27 +9,83 @@ module RUST-CASTS
// https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-implicitCast
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)))
Expand Down
28 changes: 28 additions & 0 deletions rust-semantics/expression/comparisons.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,34 @@ module RUST-INTEGER-RELATIONAL-OPERATIONS
imports private RUST-SHARED-SYNTAX
imports private RUST-REPRESENTATION
rule ptrValue(_, i8(A):Value) == ptrValue(_, i8(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, i8(A):Value) != ptrValue(_, i8(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, i8(A):Value) > ptrValue(_, i8(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(_, i8(A):Value) < ptrValue(_, i8(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(_, i8(A):Value) >= ptrValue(_, i8(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(_, i8(A):Value) <= ptrValue(_, i8(B):Value) => ptrValue(null, A <=sMInt B)
rule ptrValue(_, u8(A):Value) == ptrValue(_, u8(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, u8(A):Value) != ptrValue(_, u8(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, u8(A):Value) > ptrValue(_, u8(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(_, u8(A):Value) < ptrValue(_, u8(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(_, u8(A):Value) >= ptrValue(_, u8(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u8(A):Value) <= ptrValue(_, u8(B):Value) => ptrValue(null, A <=uMInt B)
rule ptrValue(_, i16(A):Value) == ptrValue(_, i16(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, i16(A):Value) != ptrValue(_, i16(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, i16(A):Value) > ptrValue(_, i16(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(_, i16(A):Value) < ptrValue(_, i16(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(_, i16(A):Value) >= ptrValue(_, i16(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(_, i16(A):Value) <= ptrValue(_, i16(B):Value) => ptrValue(null, A <=sMInt B)
rule ptrValue(_, u16(A):Value) == ptrValue(_, u16(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, u16(A):Value) != ptrValue(_, u16(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, u16(A):Value) > ptrValue(_, u16(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(_, u16(A):Value) < ptrValue(_, u16(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(_, u16(A):Value) >= ptrValue(_, u16(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u16(A):Value) <= ptrValue(_, u16(B):Value) => ptrValue(null, A <=uMInt B)
rule ptrValue(_, i32(A):Value) == ptrValue(_, i32(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, i32(A):Value) != ptrValue(_, i32(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, i32(A):Value) > ptrValue(_, i32(B):Value) => ptrValue(null, A >sMInt B)
Expand Down
51 changes: 49 additions & 2 deletions rust-semantics/expression/integer-operations.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,42 +6,85 @@ module RUST-INTEGER-OPERATIONS
endmodule
module RUST-INTEGER-ARITHMETIC-OPERATIONS
imports RUST-SHARED-SYNTAX
imports private K-EQUAL-SYNTAX
imports private RUST-SHARED-SYNTAX
imports private RUST-REPRESENTATION
// Operations are implemented only for the same types,
// as implicit type casting (coercion) is not available
// in Rust.
rule ptrValue(_, i8(A):Value) * ptrValue(_, i8(B):Value) => ptrValue(null, i8(A *MInt B))
rule ptrValue(_, i8(A):Value) + ptrValue(_, i8(B):Value) => ptrValue(null, i8(A +MInt B))
rule ptrValue(_, i8(A):Value) - ptrValue(_, i8(B):Value) => ptrValue(null, i8(A -MInt B))
rule ptrValue(_, i8(A):Value) / ptrValue(_, i8(B):Value) => ptrValue(null, i8(A /sMInt B))
requires B =/=K 0p8
rule ptrValue(_, i8(A):Value) % ptrValue(_, i8(B):Value) => ptrValue(null, i8(A %sMInt B))
requires B =/=K 0p8
rule ptrValue(_, u8(A):Value) * ptrValue(_, u8(B):Value) => ptrValue(null, u8(A *MInt B))
rule ptrValue(_, u8(A):Value) + ptrValue(_, u8(B):Value) => ptrValue(null, u8(A +MInt B))
rule ptrValue(_, u8(A):Value) - ptrValue(_, u8(B):Value) => ptrValue(null, u8(A -MInt B))
rule ptrValue(_, u8(A):Value) / ptrValue(_, u8(B):Value) => ptrValue(null, u8(A /sMInt B))
requires B =/=K 0p8
rule ptrValue(_, u8(A):Value) % ptrValue(_, u8(B):Value) => ptrValue(null, u8(A %sMInt B))
requires B =/=K 0p8
rule ptrValue(_, i16(A):Value) * ptrValue(_, i16(B):Value) => ptrValue(null, i16(A *MInt B))
rule ptrValue(_, i16(A):Value) + ptrValue(_, i16(B):Value) => ptrValue(null, i16(A +MInt B))
rule ptrValue(_, i16(A):Value) - ptrValue(_, i16(B):Value) => ptrValue(null, i16(A -MInt B))
rule ptrValue(_, i16(A):Value) / ptrValue(_, i16(B):Value) => ptrValue(null, i16(A /sMInt B))
requires B =/=K 0p16
rule ptrValue(_, i16(A):Value) % ptrValue(_, i16(B):Value) => ptrValue(null, i16(A %sMInt B))
requires B =/=K 0p16
rule ptrValue(_, u16(A):Value) * ptrValue(_, u16(B):Value) => ptrValue(null, u16(A *MInt B))
rule ptrValue(_, u16(A):Value) + ptrValue(_, u16(B):Value) => ptrValue(null, u16(A +MInt B))
rule ptrValue(_, u16(A):Value) - ptrValue(_, u16(B):Value) => ptrValue(null, u16(A -MInt B))
rule ptrValue(_, u16(A):Value) / ptrValue(_, u16(B):Value) => ptrValue(null, u16(A /sMInt B))
requires B =/=K 0p16
rule ptrValue(_, u16(A):Value) % ptrValue(_, u16(B):Value) => ptrValue(null, u16(A %sMInt B))
requires B =/=K 0p16
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))
requires B =/=K 0p32
rule ptrValue(_, i32(A):Value) % ptrValue(_, i32(B):Value) => ptrValue(null, i32(A %sMInt B))
requires B =/=K 0p32
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))
requires B =/=K 0p32
rule ptrValue(_, u32(A):Value) % ptrValue(_, u32(B):Value) => ptrValue(null, u32(A %uMInt B))
requires B =/=K 0p32
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))
requires B =/=K 0p64
rule ptrValue(_, i64(A):Value) % ptrValue(_, i64(B):Value) => ptrValue(null, i64(A %sMInt B))
requires B =/=K 0p64
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))
requires B =/=K 0p64
rule ptrValue(_, u64(A):Value) % ptrValue(_, u64(B):Value) => ptrValue(null, u64(A %uMInt B))
requires B =/=K 0p64
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))
requires B =/=K 0p128
rule ptrValue(_, u128(A):Value) % ptrValue(_, u128(B):Value) => ptrValue(null, u128(A %uMInt B))
requires B =/=K 0p128
endmodule
Expand All @@ -50,6 +93,10 @@ module RUST-INTEGER-RANGE-OPERATIONS
imports RUST-SHARED-SYNTAX
imports private RUST-REPRESENTATION
rule (ptrValue(_, i8 (A):Value) .. ptrValue(_, i8 (B):Value)):Expression => ptrValue(null, intRange(i8 (A), i8 (B)))
rule (ptrValue(_, u8 (A):Value) .. ptrValue(_, u8 (B):Value)):Expression => ptrValue(null, intRange(u8 (A), u8 (B)))
rule (ptrValue(_, i16(A):Value) .. ptrValue(_, i16(B):Value)):Expression => ptrValue(null, intRange(i16(A), i16(B)))
rule (ptrValue(_, u16(A):Value) .. ptrValue(_, u16(B):Value)):Expression => ptrValue(null, intRange(u16(A), u16(B)))
rule (ptrValue(_, i32(A):Value) .. ptrValue(_, i32(B):Value)):Expression => ptrValue(null, intRange(i32(A), i32(B)))
rule (ptrValue(_, u32(A):Value) .. ptrValue(_, u32(B):Value)):Expression => ptrValue(null, intRange(u32(A), u32(B)))
rule (ptrValue(_, i64(A):Value) .. ptrValue(_, i64(B):Value)):Expression => ptrValue(null, intRange(i64(A), i64(B)))
Expand Down
Loading

0 comments on commit 696bc1e

Please sign in to comment.