Need example of a couple types of functions

Epoch Infinity
1

Hey all,

I need sample code or documentation for spec that deals with the following

  • A function that returns a Struct
  • Spec to target function modifiers (like pure, view, or custom modifiers like non-reentrant, etc)

Any help will be greatly appreciated.

2

  • Regarding your first bullet - at the moment one cannot access structs directly from CVL. A support for that is experimental at the moment and aren’t available on the stable version.
    There are 2 things that can be done, depends on what you are looking to do:

    • If you need to declare a function that returns/take struct as an arg, then you can use the function sighash instead. (keep in mind that this is a temp bypass until struct support will be tested enough and deemed as stable).
      example. This is not for a function that take/return struct, but it serves the same purpose - If you cannot write a function signature because some type is not supported you can bypass it by using the sighash.

    • if you are looking to assign and get values from a function that take/return structs then you need to harness. Basically what that means is create a solidity contract of you own that inherits from the contract you are looking to verify, and implement getters for the specific elements that you want to access, or wrappers that doesnt take any struct arg, create an instance of the struct, fill it, then send it to the parent (super) function. for example the function:

struct structure {
uint e1;
bool e2;
bytes32 e3;
...
}

function foo(struct) public returns (bool){
...
}

Will be harnessed and wrapped into:

function call_foo_without_struct_arg(uint a, bool b, bytes32 c, ...) public returns (bool){
structure str = structure({e1: a, e2: b, e3: c});
return super.foo(str);
}
  • Regarding your second bullet, im not sure what do you mean by targeting function modifiers can you explain a little more what do you mean by that?
3

Thanks, the first point is clear now.

I want to target specific solidity function modifiers. Similar to how f.selector == call(uint256).selector, can target a function call which takes a uint arg, is there a way to say f.modifier == view? If there is, can it also be extended to custom modifiers like nonreentrant or ownerOnly?

For example, a rule like this

rule ownerOnlyFunctionChangesUserBalance(address user, method f){
  require(user != owner());
  require(f.modifier == `ownerOnly`);
  uint256 balanceBefore = balanceOf(user);
  env e; calldataarg args;
  f(e, args);
  uint256 balanceAfter = balanceOf(user);
  assert(balanceBefore == balanceAfter, "Owner shouldn't be able to change user balance");
}

Being able to target function modifier would allow for spec to be cleaner and more modular. I couldn’t find if something like this already exists.

4

Oh, now i see your point.
No, at the moment there is no way to access specific modifiers as you mentioned since we never thought about it this way.
The isView option was embedded to allow filtering out methods and reduce runtime and not to filter it in and check things only on view functions.

What you suggest is interesting, and we can think about the use cases and whether it’s worth implementing.

Thanks for the suggestion!

5

modifiers are code sections that should also be verified. The best way to do such a check is to first check which functions owner-only

/*
This rule finds which functions are privileged.
A function is privileged if only one address can call it.

The rule identifies this by checking which functions can be called by two different users.

*/


rule privilegedOperation(method f, address privileged)
{
	env e1;
	calldataarg arg;
	require e1.msg.sender == privileged;

	storage initialStorage = lastStorage;
	f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation.
	bool firstSucceeded = !lastReverted;

	env e2;
	calldataarg arg2;
	require e2.msg.sender != privileged;
	f@withrevert(e2, arg2) at initialStorage; // unprivileged
	bool secondSucceeded = !lastReverted;

	assert  !(firstSucceeded && secondSucceeded), "${f.selector} can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged";
}

Then you can have a definition in the spec of all functions that are owner-only and filter according to that