The *-spec.k files were automatically generated from spec.ini and templates in the resources directory, by running, e.g., the following commands:
$ python3 gen-spec.py module-tmpl.k spec-tmpl.k spec.ini openzeppelin-erc20-test-transfer openzeppelin-erc20-test-transfer >openzeppelin-erc20-test-transfer-spec.k
$ python3 gen-spec.py module-tmpl.k spec-tmpl.k spec.ini bectoken-test-batchtransfer bectoken-test-batchtransfer >bectoken-test-batchtransfer-spec.k
Most of the contents of spec.ini is program-independent, thus can be reused for other contracts, but there are two program-specific contents: runtime bytecode and calldata.
The spec.ini file contains the runtime bytecode for both target contracts and test contracts.
For example, in the following snippet of spec.ini, RUNTIME_CODE refers to the runtime bytecode of the test contract BecToken.test.sol, and TOKEN_CODE refers to the runtime bytecode of the target contract BecToken.sol.
[bectoken-test]
RUNTIME_CODE: "0x6060...4157..."
TOKEN_CODE: "0x6060...e657..."
...
The above runtime bytecode can be generated by running solc using its JSON interface, as follows:
$ echo '{ "language": "Solidity", "sources": { "BecToken.test.sol": { "urls": [ "BecToken.test.sol" ] } }, "settings": { "outputSelection": { "*": { "*": [ "*" ] } } } }' | \
./solc-static-linux.0.4.19 --allow-paths . --standard-json | python3 -c "import sys, json; print(json.load(sys.stdin)['contracts']['BecToken.test.sol']['test']['evm']['deployedBytecode']['object'])"
6060...4157...
$ echo '{ "language": "Solidity", "sources": { "BecToken.sol": { "urls": [ "BecToken.sol" ] } }, "settings": { "outputSelection": { "*": { "*": [ "*" ] } } } }' | \
./solc-static-linux.0.4.19 --allow-paths . --standard-json | python3 -c "import sys, json; print(json.load(sys.stdin)['contracts']['BecToken.sol']['BecToken']['evm']['deployedBytecode']['object'])"
6060...e657...
Note that the prefix 0x needs to be added in the solc output.
Currently, the spec.ini file specifies the calldata of each test function.
(Note that, however, this can be avoided by using another approach that allows test contracts to generate symbolic values on the fly.)
For example, the following is the calldata information for the test_batchTransfer() function in BecToken.test.sol.
[bectoken-test-batchtransfer]
call_data: #abiCallData("test_batchTransfer", #address(TOKEN), #address(A2), #address(A3), #uint256(VALUE))
+requires:
andBool #rangeAddress(A2)
andBool #rangeAddress(A3)
andBool #rangeUInt(256, VALUE)
//
andBool CALL_VALUE ==Int 0
This calldata information (both parameters and their type-based range predicates, as well as the callvalue condition) can be generated by using the type information of parameters which in turn can be obtained from solc as follows:
$ echo '{ "language": "Solidity", "sources": { "BecToken.test.sol": { "urls": [ "BecToken.test.sol", "BecToken.sol" ] } }, "settings": { "outputSelection": { "*": { "*": [ "*" ] } } } }' | \
./solc-static-linux.0.4.19 --allow-paths . --standard-json | python3 -c "import sys, json; print(json.load(sys.stdin)['contracts']['BecToken.test.sol']['test']['abi'])"
[{'constant': False, 'inputs': [{'name': 'token', 'type': 'address'}, {'name': 'a2', 'type': 'address'}, {'name': 'a3', 'type': 'address'}, {'name': 'value', 'type': 'uint256'}], 'name': 'test_batchTransfer', 'outputs': [], 'payable': False, 'stateMutability': 'nonpayable', 'type': 'function'}]