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

Index a trivial program #2

Merged
merged 1 commit into from
Aug 19, 2024
Merged

Index a trivial program #2

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
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
.build
tmp
35 changes: 28 additions & 7 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,46 @@ SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -name '*')
RUST_KOMPILED ::= .build/rust-kompiled
RUST_TIMESTAMP ::= $(RUST_KOMPILED)/timestamp
SYNTAX_INPUT_DIR ::= tests/syntax
SYNTAX_OUTPUTS_DIR ::= .build/syntax-output
SYNTAX_OUTPUT_DIR ::= .build/syntax-output
EXECUTION_INPUT_DIR ::= tests/execution
EXECUTION_OUTPUT_DIR ::= .build/execution-output

SYNTAX_INPUTS ::= $(wildcard $(SYNTAX_INPUT_DIR)/*.rs)
SYNTAX_OUTPUTS ::= $(patsubst $(SYNTAX_INPUT_DIR)/%.rs,$(SYNTAX_OUTPUTS_DIR)/%.rs-parsed,$(SYNTAX_INPUTS))
SYNTAX_OUTPUTS ::= $(patsubst $(SYNTAX_INPUT_DIR)/%.rs,$(SYNTAX_OUTPUT_DIR)/%.rs-parsed,$(SYNTAX_INPUTS))

.PHONY: clean build test syntax-test
EXECUTION_INPUTS ::= $(wildcard $(EXECUTION_INPUT_DIR)/*.rs)
EXECUTION_OUTPUTS ::= $(patsubst $(EXECUTION_INPUT_DIR)/%.rs,$(EXECUTION_OUTPUT_DIR)/%.rs.executed.kore,$(EXECUTION_INPUTS))
INDEXING_OUTPUTS ::= $(patsubst %.rs.executed.kore,%.rs.indexed.kore,$(EXECUTION_OUTPUTS))
EXECUTION_STATUSES ::= $(patsubst %.rs.executed.kore,%.rs.status,$(EXECUTION_OUTPUTS))

.PHONY: clean build test syntax-test indexing-test

clean:
rm -r .build

build: $(RUST_TIMESTAMP)

test: syntax-test
test: syntax-test indexing-test

syntax-test: $(SYNTAX_OUTPUTS)

indexing-test: $(INDEXING_OUTPUTS)
echo $(INDEXING_OUTPUTS)

$(RUST_TIMESTAMP): $(SEMANTICS_FILES)
$$(which kompile) rust-semantics/rust.md -o $(RUST_KOMPILED)

$(SYNTAX_OUTPUTS_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_TIMESTAMP)
mkdir -p $(SYNTAX_OUTPUTS_DIR)
kast --definition $(RUST_KOMPILED) $< --sort Crate > $@ || (rm $@ && false)
$(SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_TIMESTAMP)
mkdir -p $(SYNTAX_OUTPUT_DIR)
kast --definition $(RUST_KOMPILED) $< --sort Crate > [email protected] && mv -f [email protected] $@

$(EXECUTION_OUTPUT_DIR)/%.rs.indexed.kore: $(EXECUTION_INPUT_DIR)/%.rs $(RUST_TIMESTAMP)
mkdir -p $(EXECUTION_OUTPUT_DIR)
krun \
$< \
--definition $(RUST_KOMPILED) \
--output kore \
--output-file [email protected]
cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
mv -f [email protected] $@

24 changes: 24 additions & 0 deletions rust-semantics/config.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
```k

module RUST-CONFIGURATION
imports RUST-INDEXING-CONFIGURATION

configuration
<rust>
<crate/>
</rust>

endmodule

module RUST-RUNNING-CONFIGURATION
imports private RUST-INDEXING-SYNTAX
imports RUST-CONFIGURATION

configuration
<rust-mx>
<k> crateParser($PGM:Crate) </k>
<rust/>
</rust-mx>
endmodule

```
19 changes: 19 additions & 0 deletions rust-semantics/indexing.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
```k

requires "indexing/crate.md"
requires "indexing/configuration.md"
requires "indexing/helpers.md"
requires "indexing/initialization.md"
requires "indexing/syntax.md"
requires "indexing/trait.md"
requires "indexing/trait-methods.md"

module RUST-INDEXING
imports private CRATE
imports private INITIALIZATION
imports private TRAIT
imports private TRAIT-METHODS
endmodule


```
32 changes: 32 additions & 0 deletions rust-semantics/indexing/configuration.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
```k

module RUST-INDEXING-CONFIGURATION
imports private RUST-REPRESENTATION
imports private RUST-SHARED-SYNTAX

syntax Identifier ::= "my_identifier" [token]

configuration
<crate>
<constants>
<constant multiplicity="*" type="Map">
<constant-name> my_identifier </constant-name>
<constant-value> tuple(.ValueList) </constant-value>
</constant>
</constants>
<trait>
<trait-name> my_identifier </trait-name>
<methods>
<method multiplicity="*" type="Map">
<method-name> my_identifier </method-name>
<method-params> .NormalizedFunctionParameterList </method-params>
<method-return-type> ():Type </method-return-type>
<method-implementation> empty:FunctionBodyRepresentation </method-implementation>
</method>
</methods>
</trait>
</crate>
endmodule


```
77 changes: 77 additions & 0 deletions rust-semantics/indexing/crate.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
```k

module CRATE
imports private LIST
imports private MAP
imports private RUST-INDEXING-PRIVATE-SYNTAX
imports private RUST-INDEXING-SYNTAX
imports private RUST-REPRESENTATION
imports private RUST-RUNNING-CONFIGURATION

syntax MaybeIdentifier ::= ".Identifier" | Identifier
syntax Initializer ::= crateParser(crate: Crate, constants: Map, traitName: MaybeIdentifier, traitFunctions: Map)

rule crateParser(C:Crate) => crateParser(... crate : C, constants : .Map, traitName : .Identifier, traitFunctions : .Map)

rule crateParser
( ... crate:
(_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate
=> (.InnerAttributes Is):Crate
, constants : _Constants:Map
, traitName : _Name:MaybeIdentifier
, traitFunctions: _TraitFunctions:Map
)
rule
(.K => traitParser(T))
~> crateParser
( ... crate:
(_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate
=> (.InnerAttributes (ItemAtts T):Item Is):Crate
, constants : _Constants:Map
, traitName : .Identifier
, traitFunctions: .Map
)
rule ( traitMethodsParser(.AssociatedItems, Functions:Map, Name:Identifier)
=> .K
)
~> crateParser
( ... crate:
(_Atts:InnerAttributes (_ItemAtts:OuterAttributes _T:Trait):Item Is:Items):Crate
=> (.InnerAttributes Is):Crate
, constants : _Constants:Map
, traitName : .Identifier => Name
, traitFunctions: .Map => Functions
)

// rule (.K => CI:ConstantItem:KItem)
// ~> crateParser
// ( ... crate:
// (Atts:InnerAttributes (_ItemAtts:OuterAttributes CI:ConstantItem):Item Is:Items):Crate
// => (Atts Is):Crate
// , constants : _Constants:Map
// , traitName : _Name:MaybeIdentifier
// , traitFunctions: _TraitFunctions:Map
// )
// rule ((const Name:Identifier : _T:Type = V:Value;):ConstantItem:KItem => .K)
// ~> crateParser
// ( ... crate : _C:Crate
// , constants : Constants:Map => Constants[Name:Identifier:KItem <- V:Value:KItem]
// , traitName : _Name:MaybeIdentifier
// , traitFunctions: _TraitFunctions:Map
// )

rule
crateParser
( ... crate: (_Atts:InnerAttributes .Items):Crate
, constants : Constants:Map
, traitName : Name:Identifier
, traitFunctions: Functions:Map
)
=> crateInitializer
( ... constantNames: keys_list(Constants), constants: Constants
, traitName: Name
, functionNames:keys_list(Functions), functions: Functions
)
endmodule

```
35 changes: 35 additions & 0 deletions rust-semantics/indexing/helpers.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
```k

module RUST-INDEXING-PRIVATE-HELPERS
imports private RUST-REPRESENTATION
imports RUST-SHARED-SYNTAX

syntax Identifier ::= getFunctionName(Function) [function, total]
rule getFunctionName(_Q:FunctionQualifiers F:FunctionWithoutQualifiers)
=> getFunctionName(F)
rule getFunctionName(F:FunctionWithWhere _B:BlockExpression)
=> getFunctionName(F ;)
rule getFunctionName(F:FunctionWithReturnType _W:WhereClause ;)
=> getFunctionName(F ;)
rule getFunctionName(F:FunctionWithParams _R:FunctionReturnType ;)
=> getFunctionName(F ;)
rule getFunctionName(fn Name:Identifier _P:GenericParams ( ) ;)
=> Name
rule getFunctionName(fn Name:Identifier ( ) ;)
=> Name
rule getFunctionName(fn Name:Identifier _P:GenericParams ( _Params:FunctionParameters ) ;)
=> Name
rule getFunctionName(fn Name:Identifier ( _Params:FunctionParameters ) ;)
=> Name

syntax NormalizedFunctionParameterList ::= reverse(NormalizedFunctionParameterList) [function, total]
// See https://github.com/runtimeverification/k/issues/4587
// for the "Non exhaustive match detected" warning
| #reverse(NormalizedFunctionParameterList, NormalizedFunctionParameterList) [function, total]
rule reverse(L:NormalizedFunctionParameterList) => #reverse(L, .NormalizedFunctionParameterList)
rule #reverse(.NormalizedFunctionParameterList, R) => R
rule #reverse((P:NormalizedFunctionParameter , L:NormalizedFunctionParameterList), R)
=> #reverse(L, (P , R))
endmodule

```
119 changes: 119 additions & 0 deletions rust-semantics/indexing/initialization.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,119 @@
```k

module INITIALIZATION
imports private RUST-RUNNING-CONFIGURATION
imports private RUST-INDEXING-PRIVATE-HELPERS
imports private RUST-INDEXING-PRIVATE-SYNTAX

// rule
// <k> crateInitializer
// ( ... constantNames:(ListItem(Name:Identifier) => .List) _Cts:List
// , constants: _Constants (Name |-> V:Value => .Map)
// )
// ...
// </k>
// <crate>
// <constants>
// .Bag =>
// <constant>
// <constant-name> Name:Identifier </constant-name>
// <constant-value> V:Value </constant-value>
// </constant>
// </constants>
// ...
// </crate>

rule (.K => addMethod(F, A))
~> crateInitializer
( ... constantNames: .List
, functionNames: (ListItem(Name:Identifier) => .List) _Names:List
, functions: _Functions:Map
((Name |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map)
)
rule
<k> crateInitializer
( ... constantNames : .List
, functionNames : .List
, traitName : Name:Identifier
) => .K
...
</k>
<crate>
...
<trait>
...
<trait-name> _Name => Name:Identifier </trait-name>
</trait>
</crate>

// rule addMethod(_Q:FunctionQualifiers F:FunctionWithoutQualifiers, A:OuterAttributes)
// => addMethod(F:FunctionWithoutQualifiers, A)
rule addMethod((F:FunctionWithWhere B:BlockExpressionOrSemicolon):FunctionWithoutQualifiers, A:OuterAttributes)
=> addMethod1(F, B, A)

// rule addMethod1(F:FunctionWithReturnType _W:WhereClause, B:BlockExpressionOrSemicolon, A:OuterAttributes)
// => addMethod1(F, B, A)
// rule addMethod1(F:FunctionWithParams -> RT:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
// => addMethod2(F, RT, B, A)
rule addMethod1(F:FunctionWithParams, B:BlockExpressionOrSemicolon, A:OuterAttributes)
=> addMethod2(F, (), B, A)

// rule addMethod2(fn Name ( ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
// => addMethod4(Name, .NormalizedFunctionParameterList, T, B, A)
rule addMethod2(fn Name (_:SelfParam), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
=> addMethod4(Name, (self : $selftype), T, B, A)
// rule addMethod2(fn Name (_:SelfParam , ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
// => addMethod4(Name, (self : $selftype), T, B, A)
// rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
// => addMethod3(Name, (self : $selftype), P, T, B, A)
// rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList ,), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes)
// => addMethod3(Name, (self : $selftype) , P, T, B, A)

// rule addMethod3(
// _MethodName:Identifier,
// ReversedNormalizedParams:NormalizedFunctionParameterList
// => (ParamName : ParamType , ReversedNormalizedParams),
// (ParamName:Identifier : ParamType:Type , Params:FunctionParameterList)
// => Params,
// _MethodReturnType:Type, _B:BlockExpressionOrSemicolon, _A:OuterAttributes
// )
// rule addMethod3(
// MethodName:Identifier,
// ReversedNormalizedParams:NormalizedFunctionParameterList,
// .FunctionParameterList,
// MethodReturnType:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes
// )
// => addMethod4(
// MethodName,
// reverse(ReversedNormalizedParams),
// MethodReturnType, B, A
// )

rule
<k> addMethod4(
Name:Identifier, P:NormalizedFunctionParameterList,
R:Type, B:BlockExpression,
_A:OuterAttributes
) => .K
...
</k>
<crate>
...
<trait>
...
<methods>
.Bag =>
<method>
<method-name> Name:Identifier </method-name>
<method-params> P </method-params>
<method-return-type> R </method-return-type>
<method-implementation> block(B) </method-implementation>
</method>
...
</methods>
</trait>
</crate>

endmodule

```
Loading
Loading