Add optional pointers to values (#77)

Pi-Squared-Inc · Sep 6, 2024 · e7919d3 · e7919d3
1 parent 2c3287d
commit e7919d3
Show file tree

Hide file tree

Showing 10 changed files with 47 additions and 39 deletions.
diff --git 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
@@ -10,15 +10,15 @@ module RUST-LET
     // Not all cases are implemented
     rule
         <k>
-            let Variable:Identifier : T:Type = V:Value ; => .K
+            let Variable:Identifier : T:Type = ptrValue(_, V:Value) ; => .K
             ...
         </k>
         <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
         <locals> Locals:Map => Locals[Variable <- NextId] </locals>
         <values> Values:Map => Values[NextId <- implicitCast(V, T)] </values>
     rule
         <k>
-            let Variable:Identifier = V:Value ; => .K
+            let Variable:Identifier = ptrValue(_, V:Value) ; => .K
             ...
         </k>
         <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>

diff --git 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
@@ -6,7 +6,7 @@ module RUST-EXPRESSION-CONSTANTS
     imports private RUST-REPRESENTATION
     imports private RUST-PREPROCESSING-CONFIGURATION
 
-    rule <k> Name:Identifier::.PathExprSegments => V ... </k>
+    rule <k> Name:Identifier::.PathExprSegments => ptrValue(null, V) ... </k>
         <constant-name> Name </constant-name>
         <constant-value> V:Value </constant-value>
 

diff --git 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
@@ -8,7 +8,7 @@ module RUST-EXPRESSION-VARIABLES
 
     rule
         <k>
-            Variable:Identifier :: .PathExprSegments => V
+            Variable:Identifier :: .PathExprSegments => ptrValue(ptr(VarId), V)
             ...
         </k>
         <locals> Variable |-> VarId:Int ... </locals>

diff --git 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
@@ -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
@@ -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
@@ -66,12 +66,12 @@ module RUST-EXECUTION-TEST
         ) => normalizedMethodCall(TraitName, MethodName, Args)
 
     rule
-        <k> (V:Value ~> return_value ; Es:ExecutionTest) => Es ... </k>
+        <k> (V:PtrValue ~> return_value ; Es:ExecutionTest) => Es ... </k>
         <test-stack> .List => ListItem(V) ... </test-stack>
 
     rule
-        <k> check_eq V:Value => .K ... </k>
-        <test-stack> ListItem(V) => .List ... </test-stack>
+        <k> check_eq ptrValue(_, V:Value) => .K ... </k>
+        <test-stack> ListItem(ptrValue(_, V)) => .List ... </test-stack>
 
 endmodule