Merge branch 'dev' into dev-formatters

pull/362/head
Josselin 5 years ago
commit d77fcfe6b6
  1. 1
      .travis.yml
  2. 16
      scripts/travis_test_kspec.sh
  3. 3
      setup.py
  4. 1
      slither/tools/kspec_coverage/__init__.py
  5. 58
      slither/tools/kspec_coverage/__main__.py
  6. 146
      slither/tools/kspec_coverage/analysis.py
  7. 14
      slither/tools/kspec_coverage/kspec_coverage.py
  8. 10
      tests/check-kspec/safeAdd/safeAdd.sol
  9. 29
      tests/check-kspec/safeAdd/spec.md
  10. 7
      tests/check-kspec/test_1.txt

@ -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

@ -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

@ -22,7 +22,8 @@ setup(
'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'
]
}
)

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

@ -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()

@ -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)

@ -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)

@ -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);
}
}

@ -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
```

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

[ ] (Missing function) SafeAdd.add_v2(uint256,uint256)

[ ] (Unresolved) SafeAdd.addv2(uint256,uint256)

Loading…
Cancel
Save