slither-prop:

- Add support of return false/revert call in truffle test
- Improve errors reporting

slither/tools/properties/__main__.py

@@ -62,16 +62,16 @@ def parse_args():
                         nargs=0,
                         default=False)
 
-    parser.add_argument('--owner-address',
+    parser.add_argument('--address-owner',
                         help=f'Owner address. Default {OWNER_ADDRESS}',
                         default=None)
 
-    parser.add_argument('--user-address',
+    parser.add_argument('--address-user',
                         help=f'Owner address. Default {USER_ADDRESS}',
                         default=None)
 
-    parser.add_argument('--attacker-address',
-                        help=f'Owner address. Default {ATTACKER_ADDRESS}',
+    parser.add_argument('--address-attacker',
+                        help=f'Attacker address. Default {ATTACKER_ADDRESS}',
                         default=None)
 
     # Add default arguments from crytic-compile
@@ -95,7 +95,7 @@ def main():
         logger.error(f'{args.contract} not found')
         return
 
-    addresses = Addresses()
+    addresses = Addresses(args.address_owner, args.address_user, args.address_attacker)
 
     generate_erc20(contract, args.scenario, addresses)
 

slither/tools/properties/platforms/echidna.py

@@ -16,5 +16,5 @@ def generate_echidna_config(output_dir: Path, addresses: Addresses) -> str:
     content += f'sender: ["{addresses.user}", "{addresses.attacker}"]\n'
     content += 'coverage: true\n'
     filename = 'echidna_config.yaml'
-    write_file(output_dir, filename, content, allow_overwrite=False)
+    write_file(output_dir, filename, content)
     return filename

slither/tools/properties/platforms/truffle.py

@@ -24,6 +24,46 @@ def _extract_caller(p: PropertyCaller):
     return ['user']
 
 
+def _helpers():
+    """
+    Generate two functions:
+    - catchRevertThrowReturnFalse: check if the call revert/throw or return false
+    - catchRevertThrow: check if the call revert/throw
+    :return:
+    """
+    return '''
+    async function catchRevertThrowReturnFalse(promise) {
+    try {
+        const ret = await promise;
+        assert.equal(balance.valueOf(), false, "Expected revert/throw/or return false");
+    } catch (error) {
+        // Not considered: 'out of gas', 'invalid JUMP'
+        if (!error.message.includes("revert")){
+            if (!error.message.includes("invalid opcode")){
+                assert(false, "Expected revert/throw/or return false");
+            }
+        }
+        return;
+    }
+};
+
+async function catchRevertThrow(promise) {
+    try {
+        await promise;
+    } catch (error) {
+        // Not considered: 'out of gas', 'invalid JUMP'
+        if (!error.message.includes("revert")){
+            if (!error.message.includes("invalid opcode")){
+                assert(false, "Expected revert/throw/or return false");
+            }
+        }
+        return;
+    }
+    assert(false, "Expected revert/throw/or return false");
+};
+'''
+
+
 def generate_unit_test(test_contract: str, filename: str,
                        unit_tests: List[Property], output_dir: Path,
                        addresses: Addresses, assert_message: str = ''):
@@ -38,24 +78,39 @@ def generate_unit_test(test_contract: str, filename: str,
     :return:
     """
     content = f'{test_contract} = artifacts.require("{test_contract}");\n\n'
+
+    content += _helpers()
+
     content += f'contract("{test_contract}", accounts => {{\n'
 
     content += f'\tlet owner = "{addresses.owner}";\n'
     content += f'\tlet user = "{addresses.user}";\n'
     content += f'\tlet attacker = "{addresses.attacker}";\n'
     for unit_test in unit_tests:
-        if unit_test.return_type != PropertyReturn.SUCCESS:
-            continue
         content += f'\tit("{unit_test.description}", async () => {{\n'
         content += f'\t\tlet instance = await {test_contract}.deployed();\n'
+        callers = _extract_caller(unit_test.caller)
         if unit_test.return_type == PropertyReturn.SUCCESS:
-            callers = _extract_caller(unit_test.caller)
             for caller in callers:
                 content += f'\t\tlet test_{caller} = await instance.{unit_test.name[:-2]}.call({{from: {caller}}});\n'
                 if assert_message:
                     content += f'\t\tassert.equal(test_{caller}, true, "{assert_message}");\n'
                 else:
                     content += f'\t\tassert.equal(test_{caller}, true);\n'
+        elif unit_test.return_type == PropertyReturn.FAIL:
+            for caller in callers:
+                content += f'\t\tlet test_{caller} = await instance.{unit_test.name[:-2]}.call({{from: {caller}}});\n'
+                if assert_message:
+                    content += f'\t\tassert.equal(test_{caller}, false, "{assert_message}");\n'
+                else:
+                    content += f'\t\tassert.equal(test_{caller}, false);\n'
+        elif unit_test.return_type == PropertyReturn.FAIL_OR_THROW:
+            for caller in callers:
+                content += f'\t\tawait catchRevertThrowReturnFalse(instance.{unit_test.name[:-2]}.call({{from: {caller}}}));\n'
+        elif unit_test.return_type == PropertyReturn.THROW:
+            callers = _extract_caller(unit_test.caller)
+            for caller in callers:
+                content += f'\t\tawait catchRevertThrow(instance.{unit_test.name[:-2]}.call({{from: {caller}}}));\n'
         content += '\t});\n'
 
     content += '});\n'

slither/tools/properties/properties/erc20.py

@@ -56,8 +56,9 @@ def generate_erc20(contract: Contract, type_property: str, addresses: Addresses)
         return
 
     # Check if the contract is an ERC20 contract and if the functions have the correct visibility
-    if not _check_compatibility(contract):
-        # Error reported by _check_compatibility
+    errors = _check_compatibility(contract)
+    if errors:
+        logger.error(red(errors))
         return
 
     properties = ERC20_PROPERTIES.get(type_property, None)
@@ -133,29 +134,29 @@ def _platform_to_output_dir(platform: AbstractPlatform) -> Path:
 
 
 def _check_compatibility(contract):
+    errors = ''
     if not contract.is_erc20():
-        logger.error(red(f'{contract} is not ERC20 compliant. Consider checking the contract with slither-check-erc'))
-        return False
+        errors = f'{contract} is not ERC20 compliant. Consider checking the contract with slither-check-erc'
+        return errors
 
     transfer = contract.get_function_from_signature('transfer(address,uint256)')
 
     if transfer.visibility != 'public':
-        logger.error(red(f'slither-prop requires {transfer.canonical_name} to be public. Please change the visibility'))
-        return False
+        errors = f'slither-prop requires {transfer.canonical_name} to be public. Please change the visibility'
 
     transfer_from = contract.get_function_from_signature('transferFrom(address,address,uint256)')
     if transfer_from.visibility != 'public':
-        txt = f'slither-prop requires {transfer_from.canonical_name} to be public. Please change the visibility'
-        logger.error(red(txt))
-        return False
+        if errors :
+            errors += '\n'
+        errors += f'slither-prop requires {transfer_from.canonical_name} to be public. Please change the visibility'
 
     approve = contract.get_function_from_signature('approve(address,uint256)')
     if approve.visibility != 'public':
-        txt = f'slither-prop requires {approve.canonical_name} to be public. Please change the visibility'
-        logger.error(red(txt))
-        return False
+        if errors :
+            errors += '\n'
+        errors = f'slither-prop requires {approve.canonical_name} to be public. Please change the visibility'
 
-    return True
+    return errors
 
 
 def _get_properties(contract, properties: List[Property]) -> Tuple[str, List[Property]]:

slither/tools/properties/properties/ercs/erc20/properties/transfer.py

@@ -48,7 +48,7 @@ ERC20_Transferable = [
              caller=PropertyCaller.ANY),
 
     Property(name='crytic_revert_transfer_to_zero_ERC20PropertiesTransferable()',
-             description='No one should be able to send tokens to the address 0x0.',
+             description='No one should be able to send tokens to the address 0x0 (transfer).',
              content='''
 \t\tif (this.balanceOf(msg.sender) == 0){
 \t\t\trevert();
@@ -61,7 +61,7 @@ ERC20_Transferable = [
              caller=PropertyCaller.ALL),
 
     Property(name='crytic_revert_transferFrom_to_zero_ERC20PropertiesTransferable()',
-             description='No one should be able to send tokens to the address 0x0.',
+             description='No one should be able to send tokens to the address 0x0 (transferFrom).',
              content='''
 \t\tuint balance = this.balanceOf(msg.sender);
 \t\treturn transferFrom(msg.sender, address(0x0), this.balanceOf(msg.sender));''',
@@ -140,7 +140,7 @@ ERC20_Transferable = [
 \t\tif (balance == (2 ** 256 - 1))
 \t\t\treturn true;
 \t\tbool transfer_other = transfer(crytic_user, balance+1);
-\t\treturn true;''',
+\t\treturn transfer_other;''',
              type=PropertyType.HIGH_SEVERITY,
              return_type=PropertyReturn.FAIL_OR_THROW,
              is_unit_test=True,

slither/tools/properties/solidity/generate_properties.py

@@ -12,8 +12,8 @@ logger = logging.getLogger("Slither")
 def generate_solidity_properties(contract: Contract, type_property: str, solidity_properties: str,
                                  output_dir: Path) -> Path:
 
-    solidity_import = f'import "{output_dir}/interfaces.sol";\n'
-    solidity_import += f'import "{contract.source_mapping["filename_relative"]}";'
+    solidity_import = f'import "./interfaces.sol";\n'
+    solidity_import += f'import "../{contract.source_mapping["filename_short"]}";'
 
     test_contract_name = f'Properties{contract.name}{type_property}'
 
@@ -35,7 +35,7 @@ def generate_test_contract(contract: Contract,
     properties_name = f'Properties{contract.name}{type_property}'
 
     content = ''
-    content += f'import "{Path(output_dir, property_file)}";\n'
+    content += f'import "./{property_file}";\n'
     content += f"contract {test_contract_name} is {properties_name} {{\n"
     content += '\tconstructor() public{\n'
     content += '\t\t// Existing addresses:\n'