-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add an execution target; execute an empty method
- Loading branch information
Virgil Serbanuta
authored and
Virgil Serbanuta
committed
Aug 23, 2024
1 parent
d66be36
commit b132b8a
Showing
20 changed files
with
347 additions
and
9 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
#! /bin/bash | ||
|
||
kast \ | ||
--output kore \ | ||
--definition .build/rust-execution-kompiled \ | ||
--module RUST-SYNTAX \ | ||
--sort ExecutionTest \ | ||
$1 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
```k | ||
requires "execution/configuration.md" | ||
requires "execution/block.md" | ||
requires "execution/calls.md" | ||
requires "execution/stack.md" | ||
module RUST-EXECUTION | ||
imports RUST-BLOCK | ||
imports RUST-CALLS | ||
imports RUST-STACK | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
```k | ||
module RUST-BLOCK | ||
imports RUST-SHARED-SYNTAX | ||
imports RUST-STACK | ||
// https://doc.rust-lang.org/stable/reference/expressions/block-expr.html | ||
// https://doc.rust-lang.org/stable/reference/names/scopes.html | ||
rule {.InnerAttributes}:BlockExpression => .K | ||
// Pushin and popping the local state (without cleaing) should help with | ||
// variable shadowing | ||
rule {.InnerAttributes S:Statements}:BlockExpression | ||
=> pushLocalState ~> S ~> popLocalState | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,56 @@ | ||
```k | ||
module RUST-CALLS | ||
imports BOOL | ||
imports RUST-STACK | ||
imports RUST-HELPERS | ||
imports RUST-REPRESENTATION | ||
imports RUST-RUNNING-CONFIGURATION | ||
// https://doc.rust-lang.org/stable/reference/expressions/method-call-expr.html | ||
syntax Instruction ::= "clearLocalState" | ||
| setArgs(NormalizedCallParams, NormalizedFunctionParameterList) | ||
rule | ||
<k> | ||
normalizedMethodCall( | ||
TraitName:TypePath, | ||
MethodName:Identifier, | ||
Args:NormalizedCallParams | ||
) => pushLocalState | ||
~> clearLocalState | ||
~> setArgs(Args, Params) | ||
~> FunctionBody | ||
~> popLocalState | ||
... | ||
</k> | ||
<trait-path> TraitName </trait-path> | ||
<method-name> MethodName </method-name> | ||
<method-params> Params:NormalizedFunctionParameterList </method-params> | ||
<method-implementation> block(FunctionBody) </method-implementation> | ||
rule | ||
<k> | ||
clearLocalState => .K | ||
... | ||
</k> | ||
<locals> _ => .Map </locals> | ||
rule | ||
<k> | ||
setArgs( | ||
(ValueId:Int , Ids:NormalizedCallParams) => Ids, | ||
((Name:Identifier : T:Type) , Ps:NormalizedFunctionParameterList) => Ps | ||
) | ||
... | ||
</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 | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
```k | ||
module RUST-EXECUTION-CONFIGURATION | ||
imports INT | ||
imports LIST | ||
imports MAP | ||
configuration | ||
<execution> | ||
<values> .Map </values> // Map from ValueId:Int |-> Value | ||
<locals> .Map </locals> // Map from Identifier |-> ValueId:Int | ||
<stack> .List </stack> // list of locals map. | ||
<next-value-id> 0 </next-value-id> | ||
</execution> | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
```k | ||
module RUST-STACK | ||
imports LIST | ||
imports RUST-RUNNING-CONFIGURATION | ||
syntax Instruction ::= "pushLocalState" | ||
| "popLocalState" | ||
rule | ||
<k> | ||
pushLocalState => .K | ||
... | ||
</k> | ||
<locals> Locals </locals> | ||
<stack> .List => ListItem(Locals) ... </stack> | ||
rule | ||
<k> | ||
popLocalState => .K | ||
... | ||
</k> | ||
<locals> _ => Locals </locals> | ||
<stack> ListItem(Locals) => .List ... </stack> | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
```k | ||
module RUST-HELPERS | ||
imports BOOL | ||
imports private RUST-REPRESENTATION | ||
syntax Int ::= paramsLength(NormalizedFunctionParameterList) [function, total] | ||
rule paramsLength(.NormalizedFunctionParameterList) => 0 | ||
rule paramsLength(_P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList) | ||
=> 1 +Int paramsLength(Ps) | ||
syntax Bool ::= isSameType(Value, Type) [function, total] | ||
rule isSameType(_, _) => false [owise] | ||
rule isSameType(_, $selftype) => true | ||
rule isSameType(i64(_), i64) => true | ||
rule isSameType(u64(_), u64) => true | ||
rule isSameType(i32(_), i32) => true | ||
rule isSameType(u32(_), u32) => true | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,17 +1,19 @@ | ||
```k | ||
requires "config.md" | ||
requires "execution.md" | ||
requires "expression.md" | ||
requires "helpers.md" | ||
requires "preprocessing.md" | ||
requires "representation.md" | ||
requires "rust-common-syntax.md" | ||
module RUST-COMMON | ||
imports RUST-RUNNING-CONFIGURATION | ||
imports RUST-EXECUTION | ||
imports RUST-EXPRESSION | ||
imports RUST-HELPERS | ||
imports RUST-PREPROCESSING | ||
imports RUST-REPRESENTATION | ||
imports RUST-RUNNING-CONFIGURATION | ||
imports RUST-SHARED-SYNTAX | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
```k | ||
module RUST-RUNNING-CONFIGURATION | ||
imports private RUST-PREPROCESSING-SYNTAX | ||
imports private RUST-EXECUTION-TEST-PARSING-SYNTAX | ||
imports RUST-CONFIGURATION | ||
imports RUST-EXECUTION-TEST-CONFIGURATION | ||
configuration | ||
<rust-mx> | ||
<k> crateParser($PGM:Crate) ~> $TEST:ExecutionTest </k> | ||
<rust/> | ||
<rust-test/> | ||
</rust-mx> | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
```k | ||
requires "configuration.md" | ||
requires "../../rust-common.md" | ||
requires "../../rust-common-syntax.md" | ||
requires "../../test.md" | ||
module RUST-SYNTAX | ||
imports RUST-COMMON-SYNTAX | ||
imports RUST-EXECUTION-TEST-PARSING-SYNTAX | ||
endmodule | ||
module RUST | ||
imports RUST-COMMON | ||
imports RUST-EXECUTION-TEST | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,11 +1,14 @@ | ||
```k | ||
module RUST-RUNNING-CONFIGURATION | ||
imports private RUST-PREPROCESSING-SYNTAX | ||
imports RUST-CONFIGURATION | ||
configuration | ||
<rust-mx> | ||
<k> crateParser($PGM:Crate) </k> | ||
<rust/> | ||
</rust-mx> | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
```k | ||
requires "test/configuration.md" | ||
requires "test/execution.md" | ||
module RUST-TEST | ||
imports RUST-EXECUTION-TEST | ||
endmodule | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
```k | ||
module RUST-EXECUTION-TEST-CONFIGURATION | ||
imports LIST | ||
configuration | ||
<rust-test> | ||
<test-stack> .List </test-stack> | ||
</rust-test> | ||
endmodule | ||
``` |
Oops, something went wrong.