Skip to content

Commit

Permalink
Merging with main and adjustments to the integer relational operations
Browse files Browse the repository at this point in the history
  • Loading branch information
@ACassimiro
ACassimiro committed Sep 7, 2024
2 parents def647f + 6ce711a commit 1e9fc51
Show file tree
Hide file tree
Showing 26 changed files with 369 additions and 121 deletions.
2 changes: 1 addition & 1 deletion rust-semantics/config.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ module RUST-CONFIGURATION
configuration
<rust>
<preprocessed/>
<execution/>
<preprocessed/>
</rust>
endmodule
Expand Down
2 changes: 1 addition & 1 deletion rust-semantics/execution/block.md
View file
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
```
24 changes: 17 additions & 7 deletions rust-semantics/execution/calls.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,19 +41,29 @@ module RUST-CALLS
</k>
<locals> _ => .Map </locals>
rule setArgs
( (CP:Ptr, CPs:NormalizedCallParams)
, (P:NormalizedFunctionParameter, Ps:NormalizedFunctionParameterList)
)
=> setArg(CP, P) ~> setArgs(CPs, Ps)
rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K
syntax Instruction ::= setArg(Ptr, NormalizedFunctionParameter)
rule
<k>
setArgs(
(ValueId:Int , Ids:NormalizedCallParams) => Ids,
((Name:Identifier : T:Type) , Ps:NormalizedFunctionParameterList) => Ps
)
setArg
( ptr(ValueId:Int)
, Name:ValueName : T:Type
)
=> .K
...
</k>
<locals> Locals:Map => Locals[Name <- ValueId] </locals>
<values> ValueId |-> Value ... </values>
requires notBool Name in_keys(Locals) andBool isSameType(Value, T)
rule setArgs(.NormalizedCallParams, .NormalizedFunctionParameterList) => .K
requires notBool Name in_keys(Locals)
andBool isSameType(Value, T)
endmodule
Expand Down
4 changes: 2 additions & 2 deletions rust-semantics/execution/let.md
View file
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
8 changes: 7 additions & 1 deletion rust-semantics/expression.md
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,21 @@
```k
requires "expression/calls.md"
requires "expression/integer-operations.md"
requires "expression/constants.md"
requires "expression/casts.md"
requires "expression/literals.md"
requires "expression/references.md"
requires "expression/tools.md"
requires "expression/variables.md"
module RUST-EXPRESSION
imports private RUST-CASTS
imports private RUST-EXPRESSION-CALLS
imports private RUST-EXPRESSION-CONSTANTS
imports private RUST-EXPRESSION-LITERALS
imports private RUST-EXPRESSION-REFERENCES
imports private RUST-EXPRESSION-TOOLS
imports private RUST-EXPRESSION-VARIABLES
imports private RUST-EXPRESSION-CONSTANTS
imports private RUST-INTEGER-OPERATIONS
endmodule
```
97 changes: 97 additions & 0 deletions rust-semantics/expression/calls.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
```k
module RUST-EXPRESSION-CALLS
imports private COMMON-K-CELL
imports private RUST-SHARED-SYNTAX
imports private RUST-EXECUTION-CONFIGURATION
imports private RUST-EXPRESSION-TOOLS
imports private RUST-REPRESENTATION
imports private RUST-SHARED-SYNTAX
syntax Instruction ::= methodCall
( traitName: TypePath
, method: Identifier
, params: CallParamsList
, reversedNormalizedParams: NormalizedCallParams
)
syntax NormalizedCallParams ::= reverse(NormalizedCallParams, NormalizedCallParams) [function, total]
rule reverse(.NormalizedCallParams, R:NormalizedCallParams) => R
rule reverse((P, Ps:NormalizedCallParams), R:NormalizedCallParams) => reverse(Ps, (P, R))
rule SelfName:Expression . MethodName:Identifier ( )
=> methodCall(... self: SelfName, method: MethodName, params: .CallParamsList)
rule SelfName:Expression . MethodName:Identifier ( Args:CallParamsList )
=> methodCall(... self: SelfName, method: MethodName, params: Args)
rule SelfName:Expression . MethodName:Identifier ( Args:CallParamsList, )
=> methodCall(... self: SelfName, method: MethodName, params: Args)
rule
<k>
methodCall
(... self: ptrValue(ptr(A) #as P, _)
, method: MethodName:Identifier
, params: Args:CallParamsList
)
=> methodCall
(... traitName: TraitName
, method: MethodName
, params: Args
, reversedNormalizedParams: P, .NormalizedCallParams
)
...
</k>
<values> A |-> struct(TraitName:TypePath, _) ... </values>
requires isValueWithPtr(Args)
rule methodCall
(... traitName: _TraitName:TypePath
, method: _MethodName:Identifier
, params: (ptrValue(ptr(_) #as P:Ptr, _:Value) , Cps:CallParamsList) => Cps
, reversedNormalizedParams: Args:NormalizedCallParams
=> P, Args
)
rule
<k>
methodCall
(... traitName: _TraitName:TypePath
, method: _MethodName:Identifier
, params: (ptrValue(null, V:Value) , Cps:CallParamsList) => Cps
, reversedNormalizedParams: Args:NormalizedCallParams
=> ptr(NextId), Args
)
...
</k>
<next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
<values> Values:Map => Values[NextId <- V] </values>
rule
methodCall
(... traitName: TraitName:TypePath
, method: MethodName:Identifier
, params: .CallParamsList
, reversedNormalizedParams: Args:NormalizedCallParams
)
=> normalizedMethodCall
( TraitName
, MethodName
, reverse(Args, .NormalizedCallParams)
)
// Apparently contexts need the type of the HOLE to be K, and I'm not sure
// how to transform CallParamsList in some sort of K combination in a
// reasonable way. We're using heat/cool rules instead.
rule (.K => HOLE) ~> HOLE:Expression , _:CallParamsList
[heat, result(ValueWithPtr)]
rule (HOLE:Expression ~> (_:Expression , L:CallParamsList):CallParamsList)
=> HOLE , L
[cool, result(ValueWithPtr)]
rule (.K => HOLE) ~> V:Expression , HOLE:CallParamsList
requires isValueWithPtr(V)
[heat, result(ValueWithPtr)]
rule (HOLE:CallParamsList ~> V:Expression , _:CallParamsList)
=> V , HOLE
requires isValueWithPtr(V)
[cool, result(ValueWithPtr)]
endmodule
```
4 changes: 3 additions & 1 deletion rust-semantics/expression/casts.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,11 @@ module RUST-CASTS
rule implicitCast(V:Bool, bool) => V
rule implicitCast(struct(T, _) #as V, T) => V
// 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
7 changes: 6 additions & 1 deletion rust-semantics/expression/constants.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,14 @@ 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>
requires notBool isLocalVariable(Name)
rule [[isConstant(Name:Identifier) => true]]
<constant-name> Name </constant-name>
requires notBool isLocalVariable(Name)
rule isConstant(_Name:ValueName) => false [owise]
endmodule
```
123 changes: 61 additions & 62 deletions rust-semantics/expression/integer-operations.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,36 +13,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 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(_, 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 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 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(_, 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 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
Expand All @@ -51,40 +50,40 @@ module RUST-INTEGER-RELATIONAL-OPERATIONS
imports RUST-SHARED-SYNTAX
imports private RUST-REPRESENTATION
rule i32(A):Value == i32(B):Value => A ==MInt B
rule i32(A):Value != i32(B):Value => A =/=MInt B
rule i32(A):Value > i32(B):Value => A >sMInt B
rule i32(A):Value < i32(B):Value => A <sMInt B
rule i32(A):Value >= i32(B):Value => A >=sMInt B
rule i32(A):Value <= i32(B):Value => A <=sMInt B
rule u32(A):Value == u32(B):Value => A ==MInt B
rule u32(A):Value != u32(B):Value => A =/=MInt B
rule u32(A):Value > u32(B):Value => A >uMInt B
rule u32(A):Value < u32(B):Value => A <uMInt B
rule u32(A):Value >= u32(B):Value => A >=uMInt B
rule u32(A):Value <= u32(B):Value => A <=uMInt B
rule i64(A):Value == i64(B):Value => A ==MInt B
rule i64(A):Value != i64(B):Value => A =/=MInt B
rule i64(A):Value > i64(B):Value => A >sMInt B
rule i64(A):Value < i64(B):Value => A <sMInt B
rule i64(A):Value >= i64(B):Value => A >=sMInt B
rule i64(A):Value <= i64(B):Value => A <=sMInt B
rule u64(A):Value == u64(B):Value => A ==MInt B
rule u64(A):Value != u64(B):Value => A =/=MInt B
rule u64(A):Value > u64(B):Value => A >uMInt B
rule u64(A):Value < u64(B):Value => A <uMInt B
rule u64(A):Value >= u64(B):Value => A >=uMInt B
rule u64(A):Value <= u64(B):Value => A <=uMInt B
rule u128(A):Value == u128(B):Value => A ==MInt B
rule u128(A):Value != u128(B):Value => A =/=MInt B
rule u128(A):Value > u128(B):Value => A >uMInt B
rule u128(A):Value < u128(B):Value => A <uMInt B
rule u128(A):Value >= u128(B):Value => A >=uMInt B
rule u128(A):Value <= u128(B):Value => A <=uMInt B
rule ptrValue(null, i32(A):Value) == ptrValue(null, i32(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, i32(A):Value) != ptrValue(null, i32(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, i32(A):Value) > ptrValue(null, i32(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(null, i32(A):Value) < ptrValue(null, i32(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(null, i32(A):Value) >= ptrValue(null, i32(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(null, i32(A):Value) <= ptrValue(null, i32(B):Value) => ptrValue(null, A <=sMInt B)
rule ptrValue(null, u32(A):Value) == ptrValue(null, u32(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, u32(A):Value) != ptrValue(null, u32(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, u32(A):Value) > ptrValue(null, u32(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(null, u32(A):Value) < ptrValue(null, u32(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(null, u32(A):Value) >= ptrValue(null, u32(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(null, u32(A):Value) <= ptrValue(null, u32(B):Value) => ptrValue(null, A <=uMInt B)
rule ptrValue(null, i64(A):Value) == ptrValue(null, i64(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, i64(A):Value) != ptrValue(null, i64(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, i64(A):Value) > ptrValue(null, i64(B):Value) => ptrValue(null, A >sMInt B)
rule ptrValue(null, i64(A):Value) < ptrValue(null, i64(B):Value) => ptrValue(null, A <sMInt B)
rule ptrValue(null, i64(A):Value) >= ptrValue(null, i64(B):Value) => ptrValue(null, A >=sMInt B)
rule ptrValue(null, i64(A):Value) <= ptrValue(null, i64(B):Value) => ptrValue(null, A <=sMInt B)
rule ptrValue(null, u64(A):Value) == ptrValue(null, u64(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, u64(A):Value) != ptrValue(null, u64(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, u64(A):Value) > ptrValue(null, u64(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(null, u64(A):Value) < ptrValue(null, u64(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(null, u64(A):Value) >= ptrValue(null, u64(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(null, u64(A):Value) <= ptrValue(null, u64(B):Value) => ptrValue(null, A <=uMInt B)
rule ptrValue(null, u128(A):Value) == ptrValue(null, u128(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(null, u128(A):Value) != ptrValue(null, u128(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(null, u128(A):Value) > ptrValue(null, u128(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(null, u128(A):Value) < ptrValue(null, u128(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(null, u128(A):Value) >= ptrValue(null, u128(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(null, u128(A):Value) <= ptrValue(null, u128(B):Value) => ptrValue(null, A <=uMInt B)
endmodule
Expand Down
3 changes: 2 additions & 1 deletion rust-semantics/expression/literals.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,8 @@ 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))
rule B:Bool:LiteralExpression => wrapPtrValueOrError(null, B:Bool:Value)
syntax ValueOrError ::= parseInteger(IntegerLiteral) [function, total]
| parseInteger(String) [function, total]
Expand Down
11 changes: 11 additions & 0 deletions rust-semantics/expression/references.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
```k
module RUST-EXPRESSION-REFERENCES
imports private RUST-REPRESENTATION
imports private RUST-SHARED-SYNTAX
rule & E:Expression => E
endmodule
```
Loading

0 comments on commit 1e9fc51

Please sign in to comment.