Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add optional pointers to values #77

Merged
merged 1 commit into from
Sep 6, 2024
Merged

Add optional pointers to values #77

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion rust-semantics/execution/block.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

```
4 changes: 2 additions & 2 deletions rust-semantics/execution/let.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
2 changes: 1 addition & 1 deletion rust-semantics/expression/casts.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion rust-semantics/expression/constants.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down
2 changes: 1 addition & 1 deletion rust-semantics/expression/literals.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 1 addition & 1 deletion rust-semantics/expression/variables.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
50 changes: 25 additions & 25 deletions rust-semantics/preprocessing/arithmetic-operations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

```
2 changes: 1 addition & 1 deletion rust-semantics/preprocessing/constants.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 11 additions & 3 deletions rust-semantics/representation.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions rust-semantics/test/execution.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading