Merge pull request #364 from crytic/dev-kspec

slither-check-kspec

.travis.yml

@@ -20,6 +20,7 @@ env:
   - TEST_SUITE=scripts/travis_test_slither_config.sh
   - TEST_SUITE=scripts/travis_test_simil.sh
   - TEST_SUITE=scripts/travis_test_erc.sh
+  - TEST_SUITE=scripts/travis_test_kspec.sh
 branches:
   only:
   - master

scripts/travis_test_kspec.sh

@@ -0,0 +1,16 @@
+#!/bin/bash
+
+DIR_TESTS="tests/check-kspec"
+
+slither-check-kspec "$DIR_TESTS/safeAdd/safeAdd.sol" "$DIR_TESTS/safeAdd/spec.md" --solc solc-0.5.0 > test_1.txt 2>&1
+DIFF=$(diff test_1.txt "$DIR_TESTS/test_1.txt")
+if [  "$DIFF" != "" ] 
+then
+    echo "slither-check-upgradeability 1 failed"
+    cat test_1.txt
+    echo ""
+    cat "$DIR_TESTS/test_1.txt"
+    exit -1
+fi
+
+rm test_1.txt

setup.py

@@ -22,7 +22,8 @@
             'slither-simil = slither.tools.similarity.__main__:main',
             'slither-flat = slither.tools.flattening.__main__:main',
             'slither-format = slither.tools.slither_format.__main__:main',
-            'slither-check-erc = slither.tools.erc_conformance.__main__:main'
+            'slither-check-erc = slither.tools.erc_conformance.__main__:main',
+            'slither-check-kspec = slither.tools.kspec_coverage.__main__:main'
         ]
     }
 )

slither/tools/kspec_coverage/__init__.py

@@ -0,0 +1 @@
+from .analysis import run_analysis

slither/tools/kspec_coverage/__main__.py

@@ -0,0 +1,58 @@
+import sys
+import logging
+import argparse
+from slither import Slither
+from .kspec_coverage import kspec_coverage
+from crytic_compile import cryticparser
+
+logging.basicConfig()
+logger = logging.getLogger("Slither.kspec")
+logger.setLevel(logging.INFO)
+
+ch = logging.StreamHandler()
+ch.setLevel(logging.INFO)
+formatter = logging.Formatter('%(message)s')
+logger.addHandler(ch)
+logger.handlers[0].setFormatter(formatter)
+logger.propagate = False
+
+def parse_args():
+    """
+    Parse the underlying arguments for the program.
+    :return: Returns the arguments for the program.
+    """
+    parser = argparse.ArgumentParser(description='slither-kspec-coverage',
+                                     usage='slither-kspec-coverage contract.sol kspec.md')
+
+    parser.add_argument('contract', help='The filename of the contract or truffle directory to analyze.')
+    parser.add_argument('kspec', help='The filename of the Klab spec markdown for the analyzed contract(s)')
+
+    parser.add_argument('--version', help='displays the current version', version='0.1.0',action='version')
+    parser.add_argument('--json',
+                        help='Export the results as a JSON file ("--json -" to export to stdout)',
+                        action='store',
+                        default=False
+    )
+
+    cryticparser.init(parser) 
+
+    if len(sys.argv) < 2: 
+        parser.print_help(sys.stderr) 
+        sys.exit(1)
+
+    return parser.parse_args()
+
+
+def main():
+    # ------------------------------
+    #       Usage: slither-kspec-coverage contract kspec
+    #       Example: slither-kspec-coverage contract.sol kspec.md
+    # ------------------------------
+    # Parse all arguments
+
+    args = parse_args()
+
+    kspec_coverage(args)
+
+if __name__ == '__main__':
+    main()

slither/tools/kspec_coverage/analysis.py

@@ -0,0 +1,146 @@
+import re
+import logging
+
+from slither.core.declarations import Function
+from slither.core.variables.variable import Variable
+from slither.utils.colors import yellow, green, red
+from slither.utils import json_utils
+
+logging.basicConfig(level=logging.WARNING)
+logger = logging.getLogger('Slither.kspec')
+
+def _refactor_type(type):
+    return {
+        'uint': 'uint256',
+        'int': 'int256'
+    }.get(type, type)
+
+def _get_all_covered_kspec_functions(target):
+    # Create a set of our discovered functions which are covered
+    covered_functions = set()
+
+    BEHAVIOUR_PATTERN = re.compile('behaviour\s+(\S+)\s+of\s+(\S+)')
+    INTERFACE_PATTERN = re.compile('interface\s+([^\r\n]+)')
+
+    # Read the file contents
+    with open(target, 'r', encoding='utf8') as target_file:
+        lines = target_file.readlines()
+
+    # Loop for each line, if a line matches our behaviour regex, and the next one matches our interface regex,
+    # we add our finding
+    i = 0
+    while i < len(lines):
+        match = BEHAVIOUR_PATTERN.match(lines[i])
+        if match:
+            contract_name = match.groups()[1]
+            match = INTERFACE_PATTERN.match(lines[i + 1])
+            if match:
+                function_full_name = match.groups()[0]
+                start, end = function_full_name.index('(') + 1, function_full_name.index(')')
+                function_arguments = function_full_name[start:end].split(',')
+                function_arguments = [_refactor_type(arg.strip().split(' ')[0]) for arg in function_arguments]
+                function_full_name = function_full_name[:start] + ','.join(function_arguments) + ')'
+                covered_functions.add((contract_name, function_full_name))
+                i += 1
+        i += 1
+    return covered_functions
+
+
+def _get_slither_functions(slither):
+    # Use contract == contract_declarer to avoid dupplicate
+    all_functions_declared = [f for f in slither.functions if (f.contract == f.contract_declarer
+                                                               and f.is_implemented
+                                                               and not f.is_constructor
+                                                               and not f.is_constructor_variables)]
+    # Use list(set()) because same state variable instances can be shared accross contracts
+    # TODO: integrate state variables
+    all_functions_declared += list(set([s for s in slither.state_variables if s.visibility in ['public', 'external']]))
+    slither_functions = {(function.contract.name, function.full_name): function for function in all_functions_declared}
+
+    return slither_functions
+
+def _generate_output(kspec, message, color, generate_json):
+    info = ""
+    for function in kspec:
+        info += f"{message} {function.contract.name}.{function.full_name}\n"
+    if info:
+        logger.info(color(info))
+
+    if generate_json:
+        json_kspec_present = json_utils.generate_json_result(info)
+        for function in kspec:
+            json_utils.add_function_to_json(function, json_kspec_present)
+        return json_kspec_present
+    return None
+
+def _generate_output_unresolved(kspec, message, color, generate_json):
+    info = ""
+    for contract, function in kspec:
+        info += f"{message} {contract}.{function}\n"
+    if info:
+        logger.info(color(info))
+
+    if generate_json:
+        json_kspec_present = json_utils.generate_json_result(info, additional_fields={"signatures": kspec})
+        return json_kspec_present
+    return None
+
+
+def _run_coverage_analysis(args, slither, kspec_functions):
+    # Collect all slither functions
+    slither_functions = _get_slither_functions(slither)
+
+    # Determine which klab specs were not resolved.
+    slither_functions_set = set(slither_functions)
+    kspec_functions_resolved = kspec_functions & slither_functions_set
+    kspec_functions_unresolved = kspec_functions - kspec_functions_resolved
+
+
+    kspec_missing = []
+    kspec_present = []
+
+    for slither_func_desc in sorted(slither_functions_set):
+        slither_func = slither_functions[slither_func_desc]
+
+        if slither_func_desc in kspec_functions:
+            kspec_present.append(slither_func)
+        else:
+            kspec_missing.append(slither_func)
+
+    logger.info('## Check for functions coverage')
+    json_kspec_present = _generate_output(kspec_present, "[✓]", green, args.json)
+    json_kspec_missing_functions = _generate_output([f for f in kspec_missing if isinstance(f, Function)],
+                                                    "[ ] (Missing function)",
+                                                    red,
+                                                    args.json)
+    json_kspec_missing_variables = _generate_output([f for f in kspec_missing if isinstance(f, Variable)],
+                                                     "[ ] (Missing variable)",
+                                                     yellow,
+                                                     args.json)
+    json_kspec_unresolved = _generate_output_unresolved(kspec_functions_unresolved,
+                                                        "[ ] (Unresolved)",
+                                                        yellow,
+                                                        args.json)
+
+    # Handle unresolved kspecs
+    if args.json:
+        json_utils.output_json(args.json, None, {
+                                   "functions_present": json_kspec_present,
+                                   "functions_missing": json_kspec_missing_functions,
+                                   "variables_missing": json_kspec_missing_variables,
+                                   "functions_unresolved": json_kspec_unresolved
+                               })
+
+def run_analysis(args, slither, kspec):
+    # Get all of our kspec'd functions (tuple(contract_name, function_name)).
+    if ',' in kspec:
+        kspecs = kspec.split(',')
+        kspec_functions = set()
+        for kspec in kspecs:
+            kspec_functions |= _get_all_covered_kspec_functions(kspec)
+    else:
+        kspec_functions = _get_all_covered_kspec_functions(kspec)
+
+    # Run coverage analysis
+    _run_coverage_analysis(args, slither, kspec_functions)
+

slither/tools/kspec_coverage/kspec_coverage.py

@@ -0,0 +1,14 @@
+from slither.tools.kspec_coverage.analysis import run_analysis
+from slither import Slither
+
+def kspec_coverage(args):
+
+    contract = args.contract
+    kspec = args.kspec
+
+    slither = Slither(contract, **vars(args))
+
+    # Run the analysis on the Klab specs
+    run_analysis(args, slither, kspec)
+
+

tests/check-kspec/safeAdd/safeAdd.sol

@@ -0,0 +1,10 @@
+pragma solidity >=0.4.24;
+
+contract SafeAdd {
+    function add(uint x, uint y) public pure returns (uint z) {
+        require((z = x + y) >= x);
+    }
+    function add_v2(uint x, uint y) public pure returns (uint z) {
+        require((z = x + y) >= x);
+    }
+}

tests/check-kspec/safeAdd/spec.md

@@ -0,0 +1,29 @@
+
+```act
+behaviour add of SafeAdd
+interface add(uint256 X, uint256 Y)
+
+iff in range uint256
+
+    X + Y
+
+iff
+
+    VCallValue == 0
+
+returns X + Y
+```
+```act
+behaviour addv2 of SafeAdd
+interface addv2(uint256 X, uint256 Y)
+
+iff in range uint256
+
+    X + Y
+
+iff
+
+    VCallValue == 0
+
+returns X + Y
+```

tests/check-kspec/test_1.txt

@@ -0,0 +1,7 @@
+## Check for functions coverage
+[✓] SafeAdd.add(uint256,uint256)
+
+[ ] (Missing function) SafeAdd.add_v2(uint256,uint256)
+
+[ ] (Unresolved) SafeAdd.addv2(uint256,uint256)
+