From 001f9ea58f52663de81da2d0ea923d89df9cccb4 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Fri, 25 Oct 2024 17:30:04 +0300
Subject: [PATCH] Run constructors (#173)
---
tests/ukm-with-contract/erc_20_token.1.run | 7 ++---
ukm-semantics/main/encoding/encoder.md | 2 ++
ukm-semantics/main/encoding/syntax.md | 1 +
ukm-semantics/main/execution/dispatch.md | 19 ++++++++----
ukm-semantics/main/execution/syntax.md | 4 ++-
ukm-semantics/main/preprocessing/endpoints.md | 29 ++++++++++++-------
.../targets/execution/configuration.md | 2 +-
ukm-semantics/test/execution.md | 22 ++++++++++++--
8 files changed, 62 insertions(+), 24 deletions(-)
diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ukm-with-contract/erc_20_token.1.run
index 3aedc1c..a6cc960 100644
--- a/tests/ukm-with-contract/erc_20_token.1.run
+++ b/tests/ukm-with-contract/erc_20_token.1.run
@@ -21,13 +21,11 @@ list_mock SetAccountStorageHook ( 7089066454179379067 , 300 ) ukmNoResult();
list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9700, u256);
list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(300, u256);
-push "#init";
-hold_string_from_test_stack;
push "uint256";
hold_list_values_from_test_stack;
push 10000_u256;
hold_list_values_from_test_stack;
-encode_call_data;
+encode_constructor_data;
return_value;
@@ -36,7 +34,8 @@ mock CallData;
push_value 1010101_u160;
mock Caller;
-call_contract 12345;
+init_contract 12345;
+clear_pgm;
return_value;
check_eq ();
diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md
index a560feb..432662a 100644
--- a/ukm-semantics/main/encoding/encoder.md
+++ b/ukm-semantics/main/encoding/encoder.md
@@ -67,6 +67,8 @@ module UKM-CALLDATA-ENCODER
// then use it here and in the rules below.
rule encodeCallData(FN:String, FAT:List, FAL:List) =>
encodeFunctionSignature(FN, FAT) +Bytes encodeFunctionParams(FAL, FAT, b"")
+ rule encodeConstructorData(FAT:List, FAL:List) =>
+ encodeFunctionParams(FAL, FAT, b"")
// Function signature encoding
rule encodeFunctionSignature(FuncName:String, RL:List) =>
diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md
index 0f6af3f..469e1eb 100644
--- a/ukm-semantics/main/encoding/syntax.md
+++ b/ukm-semantics/main/encoding/syntax.md
@@ -10,6 +10,7 @@ module UKM-ENCODING-SYNTAX
// TODO: Make these functions total and returning BytesOrError
syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list
+ | encodeConstructorData (List, List) [function] // argument types, argument list
| encodeFunctionSignature (String, List) [function]
| encodeFunctionSignatureHelper (List, String) [function]
| encodeFunctionParams (List, List, Bytes) [function]
diff --git a/ukm-semantics/main/execution/dispatch.md b/ukm-semantics/main/execution/dispatch.md
index f7e5743..16dacd9 100644
--- a/ukm-semantics/main/execution/dispatch.md
+++ b/ukm-semantics/main/execution/dispatch.md
@@ -1,7 +1,9 @@
```k
module UKM-EXECUTION-DISPATCH
+ imports private BYTES-SYNTAX
imports private COMMON-K-CELL
+ imports private K-EQUAL-SYNTAX
imports private RUST-REPRESENTATION
imports private RUST-VALUE-SYNTAX
imports private RUST-EXECUTION-CONFIGURATION
@@ -9,12 +11,15 @@ module UKM-EXECUTION-DISPATCH
imports private UKM-EXECUTION-SYNTAX
imports private UKM-PREPROCESSING-CONFIGURATION
- syntax UkmInstruction ::= ukmExecute(contract:Value, gas: ValueOrError)
+ syntax UkmInstruction ::= ukmExecute(create: Bool, contract:Value, gas: ValueOrError)
rule
- ukmExecute(_AccountId:Int, Gas:Int)
- => ukmExecute(struct(ContractTrait, .Map), integerToValue(Gas, u64))
+ // TODO: For some reason, kompile rejects 'Create' as a variabler name below.
+ // Figure out why.
+ ukmExecute(Createy:Bool, Pgm:Bytes, _AccountId:Int, Gas:Int)
+ => ukmExecute(Createy, struct(ContractTrait, .Map), integerToValue(Gas, u64))
+ ~> #if Createy #then Pgm #else .K #fi
...
@@ -22,8 +27,12 @@ module UKM-EXECUTION-DISPATCH
rule
- ukmExecute(... contract: Contract:Value, gas: Gas:Value)
- => ptr(NVI) . dispatcherMethodIdentifier ( ptrValue(null, Gas), .CallParamsList )
+ ukmExecute(... create: Createy:Bool, contract: Contract:Value, gas: Gas:Value)
+ => ptr(NVI) . dispatcherMethodIdentifier
+ ( ptrValue(null, Createy)
+ , ptrValue(null, Gas)
+ , .CallParamsList
+ )
...
Values:Map => Values[NVI <- Contract]
diff --git a/ukm-semantics/main/execution/syntax.md b/ukm-semantics/main/execution/syntax.md
index 52b1158..2ee0238 100644
--- a/ukm-semantics/main/execution/syntax.md
+++ b/ukm-semantics/main/execution/syntax.md
@@ -1,9 +1,11 @@
```k
module UKM-EXECUTION-SYNTAX
+ imports BOOL-SYNTAX
+ imports BYTES-SYNTAX
imports INT-SYNTAX
- syntax UKMInstruction ::= ukmExecute(accountId: Int, gas: Int)
+ syntax UKMInstruction ::= ukmExecute(create: Bool, pgm:Bytes, accountId: Int, gas: Int)
endmodule
diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md
index 5128220..76bd220 100644
--- a/ukm-semantics/main/preprocessing/endpoints.md
+++ b/ukm-semantics/main/preprocessing/endpoints.md
@@ -117,22 +117,27 @@ module UKM-PREPROCESSING-ENDPOINTS
typePathToPathInExpression(append(TypePath, dispatcherMethodIdentifier))
- self : $selftype , gas : u64, .NormalizedFunctionParameterList
+ self : $selftype , create : bool , gas : u64 , .NormalizedFunctionParameterList
():Type
block({
.InnerAttributes
- concatNonEmptyStatements
- ( let buffer_id = :: ukm :: CallData();
- let ( buffer_id | .PatternNoTopAlts
- , signature | .PatternNoTopAlts
- , .Patterns
- ) = decodeSignature(buffer_id);
- .NonEmptyStatements
- , signatureToCall(signature, keys_list(Signatures), Signatures, buffer_id, gas)
- .NonEmptyStatements
- )
+ let buffer_id = :: ukm :: CallData();
+ if create {
+ .InnerAttributes
+ self . ukmWrap##init ( buffer_id , gas , .CallParamsList );
+ .NonEmptyStatements
+ } else {
+ .InnerAttributes
+ let ( buffer_id | .PatternNoTopAlts
+ , signature | .PatternNoTopAlts
+ , .Patterns
+ ) = decodeSignature(buffer_id);
+ signatureToCall(signature, keys_list(Signatures), Signatures, buffer_id, gas)
+ .NonEmptyStatements
+ };
+ .NonEmptyStatements
})
`emptyOuterAttributes`(.KList)
@@ -142,6 +147,7 @@ module UKM-PREPROCESSING-ENDPOINTS
syntax Identifier ::= "buffer_id" [token]
+ | "create" [token]
| "signature" [token]
| "gas" [token]
| "state_hooks" [token]
@@ -170,6 +176,7 @@ module UKM-PREPROCESSING-ENDPOINTS
| "empty" [token]
| "equals" [token]
| "ukm" [token]
+ | "ukmWrap##init" [token]
| "CallData" [token]
| "EVMC_BAD_JUMP_DESTINATION" [token]
| "EVMC_SUCCESS" [token]
diff --git a/ukm-semantics/targets/execution/configuration.md b/ukm-semantics/targets/execution/configuration.md
index fd6f427..efbae4d 100644
--- a/ukm-semantics/targets/execution/configuration.md
+++ b/ukm-semantics/targets/execution/configuration.md
@@ -13,7 +13,7 @@ module COMMON-K-CELL
configuration
ukmDecodePreprocessedCell($PGM:Bytes)
- ~> ukmExecute($ACCTCODE:Int, $GAS:Int)
+ ~> ukmExecute($CREATE:Bool, $PGM:Bytes, $ACCTCODE:Int, $GAS:Int)
endmodule
diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md
index b0f0d3b..bd03373 100644
--- a/ukm-semantics/test/execution.md
+++ b/ukm-semantics/test/execution.md
@@ -25,7 +25,10 @@ module UKM-TEST-SYNTAX
| "list_mock" UkmHook UkmHookResult
| "encode_call_data"
| "encode_call_data_to_string"
+ | "encode_constructor_data"
| "call_contract" Int
+ | "init_contract" Int
+ | "clear_pgm"
| "hold" KItem
| "output_to_arg"
| "push_status"
@@ -56,7 +59,7 @@ module UKM-TEST-EXECUTION
imports private UKM-HOOKS-UKM-SYNTAX
imports private UKM-REPRESENTATION
imports private UKM-TEST-SYNTAX
- imports RUST-SHARED-SYNTAX
+ imports private RUST-SHARED-SYNTAX
imports private BYTES
syntax Mockable ::= UkmHook
@@ -111,6 +114,17 @@ module UKM-TEST-EXECUTION
...
[owise]
+ rule encode_constructor_data
+ ~> list_values_holder ARGS , list_values_holder PTYPES , .UKMTestTypeHolderList
+ => ukmBytesNew(encodeConstructorData(PTYPES, ARGS))
+ ...
+
+
+ rule encode_constructor_data
+ => ukmBytesNew(encodeConstructorData(.List, .List))
+ ...
+ [owise]
+
rule
mock CallData => mock(CallDataHook(), V) ...
@@ -128,7 +142,11 @@ module UKM-TEST-EXECUTION
rule mock Hook:UkmHook Result:UkmHookResult => mock(Hook, Result)
rule list_mock Hook:UkmHook Result:UkmHookResult => listMock(Hook, Result)
- rule call_contract Account => ukmExecute(Account, 100)
+ rule call_contract Account => ukmExecute(false, .Bytes, Account, 100)
+
+ rule init_contract Account => ukmExecute(true, b"init", Account, 100)
+
+ rule (V:PtrValue ~> b"init" ~> clear_pgm) => V
rule