From e7919d3a42af279a61c67e15882ebb97ff3d62ea Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Fri, 6 Sep 2024 18:39:25 +0300
Subject: [PATCH] Add optional pointers to values (#77)
---
rust-semantics/execution/block.md | 2 +-
rust-semantics/execution/let.md | 4 +-
rust-semantics/expression/casts.md | 2 +-
rust-semantics/expression/constants.md | 2 +-
rust-semantics/expression/literals.md | 2 +-
rust-semantics/expression/variables.md | 2 +-
.../preprocessing/arithmetic-operations.md | 50 +++++++++----------
rust-semantics/preprocessing/constants.md | 2 +-
rust-semantics/representation.md | 14 ++++--
rust-semantics/test/execution.md | 6 +--
10 files changed, 47 insertions(+), 39 deletions(-)
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/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/casts.md b/rust-semantics/expression/casts.md
index ebbd293..f6de835 100644
--- a/rust-semantics/expression/casts.md
+++ b/rust-semantics/expression/casts.md
@@ -38,7 +38,7 @@ module RUST-CASTS
// 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..ba9ff3e 100644
--- a/rust-semantics/expression/constants.md
+++ b/rust-semantics/expression/constants.md
@@ -6,7 +6,7 @@ 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
diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md
index ea8ffbd..1ea7cf4 100644
--- a/rust-semantics/expression/literals.md
+++ b/rust-semantics/expression/literals.md
@@ -16,7 +16,7 @@ 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))
syntax ValueOrError ::= parseInteger(IntegerLiteral) [function, total]
| parseInteger(String) [function, total]
diff --git a/rust-semantics/expression/variables.md b/rust-semantics/expression/variables.md
index 26fc630..8f5e77b 100644
--- a/rust-semantics/expression/variables.md
+++ b/rust-semantics/expression/variables.md
@@ -8,7 +8,7 @@ module RUST-EXPRESSION-VARIABLES
rule
- Variable:Identifier :: .PathExprSegments => V
+ Variable:Identifier :: .PathExprSegments => ptrValue(ptr(VarId), V)
...
Variable |-> VarId:Int ...
diff --git a/rust-semantics/preprocessing/arithmetic-operations.md b/rust-semantics/preprocessing/arithmetic-operations.md
index cd51556..d30793d 100644
--- a/rust-semantics/preprocessing/arithmetic-operations.md
+++ b/rust-semantics/preprocessing/arithmetic-operations.md
@@ -8,35 +8,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 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 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(_, 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 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 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(_, 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
```
diff --git a/rust-semantics/preprocessing/constants.md b/rust-semantics/preprocessing/constants.md
index 76caa73..3d8a8aa 100644
--- a/rust-semantics/preprocessing/constants.md
+++ b/rust-semantics/preprocessing/constants.md
@@ -9,7 +9,7 @@ module RUST-CONSTANTS
syntax KItem ::= setConstant(Identifier, ValueOrError)
rule
- (const Name:Identifier : T:Type = V:Value;):ConstantItem:KItem
+ (const Name:Identifier : T:Type = ptrValue(_, V:Value);):ConstantItem:KItem
=> setConstant(Name, implicitCast(V, T))
rule
diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
index 5d4976f..0272602 100644
--- a/rust-semantics/representation.md
+++ b/rust-semantics/representation.md
@@ -25,11 +25,19 @@ module RUST-VALUE-SYNTAX
| struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int)
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
diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
index 7f98469..15f4685 100644
--- a/rust-semantics/test/execution.md
+++ b/rust-semantics/test/execution.md
@@ -66,12 +66,12 @@ 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 ...
endmodule