In-place testing with Scribble
A lot of projects come with their own set of tests. Tests are a useful quick check for your properties - if the properties you have in mind don't hold for the user tests, then something might be wrong with them. However in order to build an arbitrary project and run its test suite, Scribble needs to instrument the files in-place, without changing the file/directory structure, or contracts' external interfaces.
In this tutorial we will learn how to instrument a simple project in-place with scribble, and check whether its tests still pass after instrumentation. A failing test may indicate either a bug in your specifications or a bug in your actual program.
You should have the following installed:
- git
- node version 12.x
You need to first install
scribble:npm install -g eth-scribble
Next you need to clone the sample project repo:
git clone https://github.com/consensys/scribble-getting-started
And run
npm install in the directory containing the tutorial:cd scribble-getting-started/in-place-testing
npm install
This will install
truffle and ganache-cli and any remaining dependencies.In the
scribble-getting-started/in-place-testing directory of the repository you should find a simple Truffle project. Under contracts/ there are 2 contracts of interest - a base contract Managed that contains some logic for adding and removing administrators and a test contract Test that extendsManaged.Managed.sol
contract Managed {
address owner;
mapping(address=>bool) admins;
constructor() public {
owner = msg.sender;
admins[owner] = true;
}
modifier OwnerOnly {
assert(owner == msg.sender);
_;
}
modifier AdminOnly {
assert(admins[msg.sender]);
_;
}
function addAdminInternal(address addr) internal {
admins[addr] = true;
}
}
Test.sol
import "./Managed.sol";
contract Test is Managed {
function addAdmin(address newAdmin) public {
addAdminInternal(newAdmin);
}
}
One property we may want to add to
Managed.sol, is that only current administrators may call the addAdminInternal function. The contract Test violates that property - Test.addAdmin calls addAdminInternal without first checking if the caller is an admin.
As a first try we can add the following annotation in Managed.sol (extra brownie points if you see something weird already ;)):/// #if_succeeds {:msg "only owner can add admins"} admins[msg.sender];
function addAdminInternal(address addr) internal {
admins[addr] = true;
}
- 1.
#if_succeedsspecifies that the predicate should only be checked if theaddAdminInternalfunction succeeds. - 2.
{:msg "only owner can add admins"}provides a human-readable message to help remind you what this property is checking. As shorthand you can skip the{:msg }and only specify"only owner can add admins". - 3.
admins[msg.sender]is the actual property. Its a valid boolean Solidity expression. In this case we are saying that the value ofadmin[msg.sender]must be true upon successful execution ofaddAdminInternal.
This project has a test
test/tests.js in which a random user tries to add himself as an admin.contract("Test", (accounts) => {
it("can add admin", () => {
return Test.deployed().then(
async function(instance) {
await instance.addAdmin(accounts[1], {from: accounts[1]});
}
);
})
})
If we run the test suite without instrumentation this test would actually succeed. We would expect that if we instrumented the contract, and ran the test, the test would fail, showing that the contract doesn't respect the specification.
To instrument the contracts we can run:
scribble contracts/Test.sol --output-mode files
Found 1 annotations in 1 different files.
contracts/Managed.sol -> contracts/Managed.sol.instrumented
The output tells us that
scribble created a .instrumented version for Managed.sol. Indeed we should see the new under contracts:ls contracts
Managed.sol Managed.sol.instrumented Migrations.sol __scribble_ReentrancyUtils.sol Test.sol
There is a 2nd new file there as well -
__scribble_ReentrancyUtils.sol. This is a contract for internal use that scribble always emits.Now we want to swap the
.instrumented file with its original counterpart and re-run the tests. Since we don't want to loose our original files, lets first copy the originals to the side:cp contracts/Managed.sol contracts/Managed.sol.original
Then copy the instrumented file in-place of the original:
cp contracts/Managed.sol.instrumented contracts/Managed.sol
Now you should be able to run the test suite and hit the failure. To do so in another shell window you must start
ganache-cli by running:npm run testrpc
Back in the original shell you can run the tests with:
truffle test
Using network 'development'.
Compiling your contracts...
===========================
> Compiling ./contracts/Managed.sol
> Compiling ./contracts/Test.sol
> Compiling ./contracts/__scribble_ReentrancyUtils.sol
> Compilation warnings encountered:
/home/dimo/work/consensys/scribble-getting-started/in-place-testing/contracts/__scribble_ReentrancyUtils.sol:2:1: Warning: Source file does not specify required compiler version! Consider adding "pragma solidity ^0.5.16;"
contract __scribble_REENTRANCY_UTILS {
^ (Relevant source part starts here and spans across multiple lines).
> Artifacts written to /tmp/test-202066-9871-gaivy6.q7obe
> Compiled successfully using:
- solc: 0.5.16+commit.9c3226ce.Emscripten.clang
Contract: Test
✓ can add admin (77ms)
1 passing (104ms)
But wait! why did that test succeed? Shouldn't it have failed since the sender wasn't an administrator?
The key here is when the
admin[msg.sender] predicate was evaluated - it was evaluated after the function had successfully executed, at which point the sender had already added themselves to the admin map. To fix this, we want to talk about the value of admin[msg.sender] before the function started executing. We can do this using the old()operator, which specifies that scribble should compute the value of a given expression before the function is called.So lets fix this. First lets move the original annotated file back:
cp contracts/Managed.sol.original contracts/Managed.sol
Now lets change the annotation to look like this:
/// #if_succeeds {:msg "only owner can add admins"} old(admins[msg.sender]);
function addAdminInternal(address addr) internal {
admins[addr] = true;
}
Now if we repeated the whole process of instrumenting, swapping the files, and running tests we should hit an error. But that process is so laborious! There must be a better way! And there is - introducing
--armand --disarm.Copying files back and forth, keeping track of
.sol.instrumented and .sol.original files is annoying. So scribble provides you with two options that take care of this for you.If you add the
--arm option when instrumenting, then scribble will automatically create .sol.original copies of the original files, and swap the instrumented files in-place, so you can start testing immediately. So now that we have fixed our annotation, lets use --arm and --disarm.First we will instrument the contracts and swap them in-place with a single command:
scribble contracts/Test.sol --output-mode files --arm
Found 1 annotations in 1 different files.
contracts/Managed.sol -> contracts/Managed.sol.instrumented
Copying contracts/Managed.sol to contracts/Managed.sol.original
Copying contracts/Managed.sol.instrumented to contracts/Managed.sol
Note that the new output shows which files were copied where. At this point if we run the tests, we can verify that the fixed annotation fails:
truffle test
...
1) Contract: Test
can add admin:
Error: Returned error: VM Exception while processing transaction: invalid opcode
at /home/dimo/work/consensys/scribble-getting-started/in-place-testing/test/test.js:7:32
at process._tickCallback (internal/process/next_tick.js:68:7)
And afterwards we can revert the workspace back by using the
--disarm option:scribble contracts/Test.sol --disarm
Moving contracts/Managed.sol.original to contracts/Managed.sol
Removing contracts/Managed.sol.instrumented
Removing /home/dimo/work/consensys/tmp/test_pass/scribble-getting-started/in-place-testing/contracts/__scribble_ReentrancyUtils.sol
Removing /home/dimo/work/consensys/tmp/test_pass/scribble-getting-started/in-place-testing/instrumentation.scribble.json
Note that the additional
.original and .instrumented files, as well as other auxilary files emitted by scribble are all removed:ls contracts/
Managed.sol Migrations.sol Test.sol
If you want to keep the
.instrumented files for debugging purposes, add the --keep-instrumented option when disarming.When we ran the instrumented tests, we hit an assertion and the test fails. However if we had multiple properties, we wouldn't know WHICH property fails. It would be nice to get a message telling us which property failed. To do so, lets re-instrument the code with the
--no-assert option:scribble contracts/Test.sol --output-mode files --arm --no-assert
Found 1 annotations in 1 different files.
contracts/Managed.sol -> contracts/Managed.sol.instrumented
Copying contracts/Managed.sol to contracts/Managed.sol.original
Copying contracts/Managed.sol.instrumented to contracts/Managed.sol
The
--no-assert option tells scribble to not emit an explicit assert(false) on failure, and instead just emit an event. As a result, the tests may not fail anymore, but if you run them with--show-eventsyou will see all the failing properties:truffle test --show-events
Using network 'development'.
Compiling your contracts...
===========================
> Compiling ./contracts/Managed.sol
> Compiling ./contracts/Test.sol
> Compiling ./contracts/__scribble_ReentrancyUtils.sol
...
Contract: Test
✓ can add admin (72ms)
Events emitted during test:
---------------------------
Managed.AssertionFailed(
message: '0: only owner can add admins' (type: string)
)
---------------------------
1 passing (177ms)
Now we see the
AssertionFailed event. Its text contains the human-readable label from the original annotation.Last modified 1yr ago