New config simple exp function

[shangweilin]

Please help to review this branch.
The current version include the following semantics based on the new configuration:

1. Basic types (boolean and integers)
2. Basic expressions and statements (not including loops)
3. External and internal function calls
4. Basic testing engine

[dwightguth]

I will have more comments later, but this is my brief look at the configuration.

[ehildenb]

I agree with @dwightguth on pretty much all his points about the configuration. I think if you add some commits which make those changes and fix any resulting breakages in the rest of the semantics that would be good. I can take a closer look at the rules then.

[ehildenb]

By the way, we put type="Map" on some cells which are multiplicity="*" because it make K internally treat that cell as a Map sort instead of a List sort. This means we use the first cell (important) as the key to the Map, so that cell must occur in any rule which mentions any of the cells inside Contract. This results in a significant performance increase for the concrete execution engine.

[dfilaretti]

I agree with the other reviewers, let's sort these initial things out before moving to more in-depth review of the rules. I left a couple of comments in the meanwhile.

One other thing I'd recommend is this time to start actually using the compiler tests. Rather than using hand-written tests (like the various t1.so etc.), I think it makes sense to just pick the compiler tests and add those instead; most of them will fail right now because most features are not implemented, but that's OK, as the goal is to gradually add features and fix things so that all tests will eventually pass.

Even at the current state for example, I guess it's possible to find some simple test (from the compiler's tests) that only involves function call and arithmetic.

[shangweilin]

I have revised the configuration accordingly as much as I can. Please proceed to review the semantics rules. Thanks.

[dfilaretti]

Please see my additional comments.

[JIAOJIAO1991]

The error comes from #createStateVars(N,SV) in New-Contract-Instance. To be specific, the error comes from Allocate-State-Variables. Since a bag of the cell "account" is created in New-Contract-Instance, the subcells "context" and "Storage" need to be rewritten in #createStateVars to store state variables. new A() and new B() seem to work because they do not have any state variables to store. In other words, whenever we need to rewrite the subcells in "account" which is created in New-Contract-Instance, the error appears. It seems that rewriting of cell contents is not allowed when Map is used instead of Bag. Is it appropriate to use Map instead of Bag when rewiring of cell contents is necessary? Or how to avoid this problem when Map is used?

[shangweilin]

I have fixed the bug of mapping incomplete keys of Map. Please continue reviewing the other rules.

[tomtomjhj]

It would be nice to have a style guideline e.g. not using tabs.

[dfilaretti]

I was looking once again at the compiler tests (https://github.com/ethereum/solidity/blob/develop/test/libsolidity/SolidityEndToEndTest.cpp) and noticed how a simple search for function_ shows many possible test cases that you could actually start using (rather than having to write your own).

Like this for example:

BOOST_AUTO_TEST_CASE(same_function_in_construction_and_runtime)
{
	char const* sourceCode = R"(
		contract C {
			uint public initial;
			constructor() public {
				initial = double(2);
			}
			function double(uint _arg) public returns (uint _ret) {
				_ret = _arg * 2;
			}
			function runtime(uint _arg) public returns (uint) {
				return double(_arg);
			}
		}
	)";

	compileAndRun(sourceCode, 0, "C");
	ABI_CHECK(callContractFunction("runtime(uint256)", encodeArgs(u256(3))), encodeArgs(u256(6)));
	ABI_CHECK(callContractFunction("initial()"), encodeArgs(u256(4)));
}

or this:

BOOST_AUTO_TEST_CASE(pass_function_types_internally)
{
	char const* sourceCode = R"(
		contract C {
			function f(uint x) public returns (uint) {
				return eval(g, x);
			}
			function eval(function(uint) internal returns (uint) x, uint a) internal returns (uint) {
				return x(a);
			}
			function g(uint x) public returns (uint) { return x + 1; }
		}
	)";

	compileAndRun(sourceCode, 0, "C");
	ABI_CHECK(callContractFunction("f(uint256)", 7), encodeArgs(u256(8)));
}

I know many of those are not supposed to pass (either because they make use of features you do not support yet, or because there are issues with the current definition), but that's exactly the point of those tests: they give us a goal and a way to figure out when we are "done".

[tomtomjhj]

@dfilaretti tests that only use ABI_CHECK could be automated with K by defining those (simple) CPP functions in K. But definitely testContractAgainstCpp... stuff will be nontrivial.

[dfilaretti]

well my comment was only meant to suggest some possible tests to look at, even if we don't have a way to automate it yet. Even if done manually, it can still give us something to play with for the time being. But I agree, in the long term we need to automate, as it's impractical to rewrite them all manually (and keep them up to date as the language evolves).

[shangweilin]

I have added the desugaring rules for internal function calls. That is, for internal function calls, we can use exact Solidity syntax now, instead of functionCall.

[ehildenb]

This is the only place where #undef_Int and #undef_Id are used. I would recommend instead creating a value .Account or #undef_Account like so:

syntax AccountId ::= Int | "#undef_Account"

You declare #undef_Int for example here:

syntax Int ::= "#undef_Int"

which means you're adding junk to the Int sort, which will make reasoning using unification and Z3 very difficult when it comes time to do the proofs. Almost always better to use a super-sort (like the AccountId super-sort above) and add the extra constants there.

[shangweilin]

Fixed accordingly.

[ehildenb]

@shangweilin is it ever the case that it's useful to have an #account with only one of the entries undefined? Eg: #account(#undef_Int, x) or #account(3, #undef_Id)? If not (and I can't see any uses in the semantics of these cases), then instead of adding sorts AccountId and AccountInt as you have, I would just add an extra constant #undef_Account to sort Account.

syntax Account ::= #account(Int, Id) | "#undef_Account"

If the semantics ever could produce examples like above, then it would make sense, but otherwise would be better to avoid adding super-sorts of builtin sorts (like Int and Id) if possible.

Note that this pattern of adding an extra constant to a sort (like #undef_Account) is like the Maybe type in Haskell, or the Optional in Java/Scala.

[shangweilin]

Hi, @dfilaretti and @ehildenb. We have addressed all the comments except for the <numOfAccounts> because we don't know the syntax of apply size (is it a function or an attribute?) on <activeAccounts>, which is a set. Please advise, thanks. All the changes have been pushed into GitHub now.

[shangweilin]

Hi, @dfilaretti, @ehildenb, @tomtomjhj, and @dwightguth, I managed to figure out the usage of size in the C semantics. I think we have fixed all the issues that you raised. Please hep to review the code again, thanks.

out of date

[shangweilin]

Hi, @ehildenb, @dfilaretti, @tomtomjhj, and @dwightguth, I have fixed the final three issues. Please help to review again, thanks.

[ehildenb]

@shangweilin there is still a lot to be improved, but I'll submit a follow-up PR which fixes the formatting issues and some other things. Feel free to merge ASAP.