~mwshinn/+junk/verify

#!/usr/bin/python

import sys

import math

import random

import itertools

import inspect

import functools

from exceptions import *

_FUN_PROPS = "__verify__"

def TypeFactory(v):

    """Ensure `v` is a valid Type.

    This function is used to convert user-specified types into

    internal types for the verification engine.  It allows Type

    subclasses, Type subclass instances, Python type, and user-defined

    classes to be passed.  Returns an instance of the type of `v`.

    Users should never access this function directly.

    """

    if issubclass(type(v), Type):

        return v

    elif issubclass(v, Type):

        return v()

    elif issubclass(type(v), type):

        return Generic(v)

    else:

        raise InvalidTypeError("Invalid type %s" % v)

class Type():

    def test(self, v):

        pass

class Generic(Type):

    def __init__(self, typ):

        super().__init__()

        assert isinstance(typ, type)

        self.type = typ

    def test(self, v):

        assert isinstance(v, self.type)

    def generate(self):

        if hasattr(self.type, "_generate") and callable(self.type._generate):

            return self.type._generate()

        else:

            raise NoGeneratorError

class Nothing(Type):

    def test(self, v):

        assert v is None

    def generate(self):

        return [None]

class Numeric(Type):

    def test(self, v):

        super().test(v)

        assert isinstance(v, (int, float)), "Invalid numeric"

    def generate(self):

        # Check infinity, nan, 0, +/- numbers, a float, a small/big number

        return [math.inf, -math.inf, math.nan, 0, 1, -1, 3.141, 1e-10, 1e10]

class Number(Numeric):

    def test(self, v):

        super().test(v)

        assert isinstance(v, (int, float)), "Invalid number"

        assert not math.isnan(v), "Number cannot be nan"

        assert not math.isinf(v), "Number must be finite"

    def generate(self):

        return [0, 1, -1, 3.141, 1e-10, 1e10]

class Integer(Number):

    def test(self, v):

        super().test(v)

        assert v // 1 == v, "Invalid integer"

    def generate(self):

        return [-100, -1, 0, 1, 100]

class Natural0(Integer):

    def test(self, v):

        super().test(v)

        assert v >= 0, "Must be greater than or equal to 0"

    def generate(self):

        return [0, 1, 10, 100]

class Natural1(Natural0):

    def test(self, v):

        super().test(v)

        assert v > 0, "Must be greater than 0"

    def generate(self):

        return [1, 2, 10, 100]

class Range(Number):

    def __init__(self, low, high):

        super().__init__()

        assert isinstance(low, (float, int)) and isinstance(high, (float, int)), "Invalid bounds"

        assert low < high, "Low %s must be strictly greater than high %s" % (low, high)

        self.low = low if low is not None else -math.inf

        self.high = high if low is not None else math.inf

    def test(self, v):

        super().test(v)

        assert self.low <= v <= self.high, "Value %f must be greater than %f and less than %f" % (v, self.low, self.high)

    def _generate_quantiles(self):

        EPSILON = 1e-5

        if not (math.isinf(self.low) or math.isinf(self.high)):

            l = self.low

            h = self.high

            return [(l+h)*EPSILON, (l+h)*.5, (l+h)*.25, (l+h)*.75, (l+h)*(1-EPSILON)]

        elif math.isinf(self.low):

            return [self.high-EPSILON]

        elif math.isinf(self.high):

            return [self.low-EPSILON]

        raise AssertionError("Invalid Range bounds")

    def generate(self):

        return [self.low, self.high] + self._generate_quantiles()

class RangeClosedOpen(Range):

    def test(self, v):

        super().test(v)

        assert v != self.high, "Value must be strictly greater than %f" % self.high

    def generate(self):

        return [self.low] + self._generate_quantiles()

class RangeOpenClosed(Range):

    def test(self, v):

        super().test(v)

        assert v != self.low, "Value must be strictly less than %f" % self.low

    def generate(self):

        return [self.high] + self._generate_quantiles()

class RangeOpen(RangeClosedOpen, RangeOpenClosed):

    def test(self, v):

        super().test(v)

    def generate(self):

        return self._generate_quantiles()

class Set(Type):

    def __init__(self, els):

        super().__init__()

        assert hasattr(els, "__contains__") and callable(els.__contains__)

        self.els = els

    def test(self, v):

        super().test(v)

        assert v in self.els, "Value %v in set" % v

    def generate(self):

        return [e for e in self.els]

class String(Type):

    def test(self, v):

        super().test(v)

        assert isinstance(v, str), "Non-string passed"

    def generate(self):

        return ["", "a"*1000, "{100}", " ", "abc123", "two words", "\\", "%s", "1", "баклажан"]

class List(Type):

    def __init__(self, t):

        super().__init__()

        self.type = TypeFactory(t)

    def test(self, v):

        super().test(v)

        assert isinstance(v, list), "Non-list passed"

        for e in v:

            self.type.test(e)

    def generate(self):

        return [[], self.type.generate(), [self.type.generate()[0]]*1000]

class Dict(Type):

    def __init__(self, k, v):

        self.valtype = TypeFactory(v)

        self.keytype = TypeFactory(k)

    def test(self, v):

        super().test(v)

        assert isinstance(v, dict), "Non-dict passed"

        for e in v.keys():

            self.keytype.test(e)

        for e in v.values():

            self.valtype.test(e)

    def generate(self):

        return [{}, dict(zip(self.keytype.generate(), self.valtype.generate()))]

class And(Type):

    def __init__(self, *types):

        self.types = [TypeFactory(a) for a in types]

    def test(self, v):

        for t in self.types:

            t.test(v)

    def generate(self):

        all_generated = [e for t in self.types for e in t.generate()]

        valid_generated = []

        for g in all_generated:

            try:

                for t in self.types:

                    t.test(g)

            except AssertionError:

                continue

            else:

                valid_generated.append(g)

        return valid_generated

class Or(Type):

    def __init__(self, *types):

        self.types = [TypeFactory(a) for a in types]

    def test(self, v):

        passed = False

        for t in self.types:

            try:

                t.test(v)

                passed = True

            except AssertionError:

                continue

        if passed == False:

            raise AssertionError("Neither type in Or holds")

    def generate(self):

        return [e for t in self.types for e in t.generate()]

def has_fun_prop(f, k):

    """Test whether function `f` has property `k`.

    We define properties as annotations added to a function throughout

    the process of defining a function for verification, e.g. the

    argument types.  If `f` is an unannotated function, this returns

    False.  If `f` has the property named `k`, it returns True.

    Otherwise, it returns False.

    Users should never access this function directly.

    """

    if not hasattr(f, _FUN_PROPS):

        return False

    if not isinstance(getattr(f, _FUN_PROPS), dict):

        return False

    if k not in getattr(f, _FUN_PROPS).keys():

        return False

    return True

def get_fun_prop(f, k):

    """Get the value of property `k` from function `f`.

    We define properties as annotations added to a function throughout

    the process of defining a function for verification, e.g. the

    argument types.  If `f` does not have a property named `k`, this

    throws an error.  If `f` has the property named `k`, it returns

    the value of it.

    Users should never access this function directly.

    """

    if not has_fun_prop(f, k):

        raise InternalError("Function %s has no property %s" % (str(f), k))

    return getattr(f, _FUN_PROPS)[k]

def set_fun_prop(f, k, v):

    """Set the value of property `k` to be `v` in function `f`.

    We define properties as annotations added to a function throughout

    the process of defining a function for verification, e.g. the

    argument types.  This sets function `f`'s property named `k` to be

    value `v`.

    Users should never access this function directly.

    """

    if not hasattr(f, _FUN_PROPS):

        setattr(f, _FUN_PROPS, {})

    if not isinstance(getattr(f, _FUN_PROPS), dict):

        raise InternalError("Invalid function properties dictionary for %s" % str(f))

    getattr(f, _FUN_PROPS)[k] = v

def _wrap(func):

    def _decorated(*args, **kwargs):

        # @accepts decorator

        if has_fun_prop(func, "argtypes") and has_fun_prop(func, "kwargtypes"):

            argtypes = get_fun_prop(func, "argtypes")

            kwargtypes = get_fun_prop(func, "kwargtypes")

            if argtypes:

                if len(argtypes) != len(args):

                    raise ArgumentTypeError("Invalid argument specification to @accepts")

                for i,t in enumerate(argtypes):

                    try:

                        t.test(args[i])

                    except AssertionError as e:

                        raise ArgumentTypeError("Invalid argument type %s" % args[i])

            if kwargtypes:

                if all(k in kwargs.keys() for k in kwargtypes.keys()):

                    raise ArgumentTypeError("Invalid keyword argument specification to @accepts")

                for k,t in kwargtypes.items():

                    try:

                        t.test(kwargs[k])

                    except AssertionError as e:

                        raise ArgumentTypeError("Invalid argument type for %s: %s" % (k, kwargs[k]))

        # @requires decorator

        if has_fun_prop(func, "requires"):

            argspec = inspect.getargspec(func)

            # Function named arguments

            #full_locals = locals().copy()

            #full_locals.update({k : v for k,v in zip(argspec.args, args)})

            full_locals = {k : v for k,v in zip(argspec.args, args)}

            # Unnamed positional arguments

            if argspec.varargs is not None:

                positional_args = {argspec.varargs: args[len(argspec.args):]}

                full_locals.update(positional_args)

            # TODO kw arguments

            for requirement in get_fun_prop(func, "requires"):

                if not eval(requirement, globals(), full_locals):

                    raise EntryConditionsError("Function requirement '%s' failed" % requirement)

        # The actual function

        returnvalue = func(*args, **kwargs)

        # @returns decorator

        if has_fun_prop(func, "returntype"):

            try:

                get_fun_prop(func, "returntype").test(returnvalue)

            except AssertionError as e:

                raise ReturnTypeError("Invalid return type of %s" % returnvalue )

        # @ensures decorator

        if has_fun_prop(func, "ensures"):

            argspec = inspect.getargspec(func)

            # Function named arguments

            limited_locals = {k : v for k,v in zip(argspec.args, args)}

            # Return value

            limited_locals['__RETURN__'] = returnvalue

            # Unnamed positional arguments

            if argspec.varargs is not None:

                positional_args = {argspec.varargs: args[len(argspec.args):]}

                limited_locals.update(positional_args)

            if any("`" in ens for ens in get_fun_prop(func, "ensures")) : # Cache if we refer to previous executions

                if has_fun_prop(func, "exec_cache"):

                   exec_cache = get_fun_prop(func, "exec_cache")

                else:

                   exec_cache = []

                exec_cache.append(limited_locals.copy())

                set_fun_prop(func, "exec_cache", exec_cache) #TODO is this line necessary?

            # TODO kw arguments

            for ensurement in get_fun_prop(func, "ensures"):

                e = ensurement.replace("return", "__RETURN__")

                if "<-->" in e:

                    e_parts = e.split("<-->")

                    assert len(e_parts) == 2, "Only one implies per statement"

                    e = "((%s) if (%s) else True) and ((%s) if (%s) else True)" % (e_parts[1], e_parts[0], e_parts[0], e_parts[1])

                if "-->" in e: # TODO won't throw error if --> and <--> are in e

                    e_parts = e.split("-->")

                    assert len(e_parts) == 2, "Only one implies per statement"

                    e = "(%s) if (%s) else True" % (e_parts[1], e_parts[0])

                if "`" in e:

                    bt = "__BACKTICK__"

                    exec_cache = get_fun_prop(func, "exec_cache")

                    for cache_item in exec_cache:

                        limited_locals.update({k+bt : v for k,v in cache_item.items()})

                        e = e.replace("`", bt)

                        if not eval(e, globals(), limited_locals):

                            raise ExitConditionsError("Ensures statement '%s' failed" % ensurement)

                elif not eval(e, globals(), limited_locals):

                    raise ExitConditionsError("Ensures statement '%s' failed" % ensurement)

        return returnvalue

    if has_fun_prop(func, "active"):

        return func

    else:

        set_fun_prop(func, "active", True)

        assign = functools.WRAPPER_ASSIGNMENTS + (_FUN_PROPS,)

        wrapped = functools.wraps(func, assigned=assign)(_decorated)

        if "__ALL_FUNCTIONS" in globals().keys():

            global __ALL_FUNCTIONS

            __ALL_FUNCTIONS.append(wrapped)

        return wrapped

def accepts(*argtypes, **kwargtypes):

    argtypes = [TypeFactory(a) for a in argtypes]

    kwargtypes = {k : TypeFactory(a) for k,a in kwargtypes.items()}

    def _decorator(func):

        # @accepts decorator

        if argtypes is not None:

            if has_fun_prop(func, "argtypes"):

                raise ValueError("Cannot set argument types twice")

            set_fun_prop(func, "argtypes", argtypes)

        if kwargtypes is not None:

            if has_fun_prop(func, "kwargtypes"):

                raise ValueError("Cannot set set keyword argument types twice")

            set_fun_prop(func, "kwargtypes", kwargtypes)

        return _wrap(func)

    return _decorator

def returns(returntype):

    returntype = TypeFactory(returntype)

    def _decorator(func):

        # @returns decorator

        if has_fun_prop(func, "returntype"):

            raise ValueError("Cannot set return type twice")

        set_fun_prop(func, "returntype", returntype)

        return _wrap(func)

    return _decorator

def requires(condition):

    def _decorator(func):

        # @requires decorator

        if has_fun_prop(func, "requires"):

            if not isinstance(get_fun_prop(func, "requires"), list):

                raise InternalError("Invalid requires structure")

            base_requires = get_fun_prop(func, "requires")

        else:

            base_requires = []

        set_fun_prop(func, "requires", [condition]+base_requires)

        return _wrap(func)

    return _decorator

def ensures(condition):

    def _decorator(func):

    # @ensures decorator

        if has_fun_prop(func, "ensures"):

            if not isinstance(get_fun_prop(func, "ensures"), list):

                raise InternalError("Invalid ensures strucutre")

            base_ensures = get_fun_prop(func, "ensures")

        else:

            base_ensures = []

        set_fun_prop(func, "ensures", [condition]+base_ensures)

        return _wrap(func)

    return _decorator

def test_function(func):

    """Perform a unit test of a single function.

    Create a series of test cases by finding the type of each of the

    function arguments, and creating all possible combinations of test

    cases for each type using the type's generate() function.  Then,

    test the function with each input.  This is roughly equivalent to

    just running the function with each input, because the exceptions

    should be caught at runtime.

    Assuming runtime checking is enabled (as it should be), running

    this on a function only tests it for inputs it is likely to

    encounter in the future.

    """

    # Ensure the user has specified argument types using the @accepts

    # decorator.

    assert has_fun_prop(func, "argtypes"), "No argument annotations"

    # Generate all combinations of arguments as test cases.  Some

    # argument types cannot be generated automatically.  If we

    # encounter one of these, unit testing won't work.

    try:

        testcases = itertools.product(*[e.generate() for e in get_fun_prop(func, "argtypes")])

    except NoGeneratorError:

        testcases = []

    if not testcases:

        print("Warning: %s could not be tested" % func.__name__)

        return

    # If entry conditions are met, simply running the function will be

    # enough of a test, since all values are checked at runtime.  So

    # execute the function once for each combination of arguments.

    for tc in testcases:

        try:

            func(*tc)

        except EntryConditionsError:

            continue

# If called as "python3 -m verify script_file_name.py", then unit test

# script_file_name.py.  By this, we mean call the function

# test_function on each function which has annotations.  Note that we

# must execute the entire file script_file_name.py in order to do

# this, so any time-intensive code should be in a __name__ ==

# "__main__" guard, which will not be executed.

#

# We know if a function has annotations because all annotations are

# passed through the _decorator function (so that we can ensure we

# only use at most one more stack frame no matter how many function

# annotations we have).  The _decorator function will look for the

# global variable __ALL_FUNCTIONS to be defined within the verify

# module.  If it is defined, it will add one copy of each decorated

# function to the list.  Then, we can perform the unit test by

# iterating through each of these.  This has the advantage of allowing

# nested functions and object methods to be discovered for

# verification.

if __name__ == "__main__":

    # Pass exactly one argement: the python file to check

    if len(sys.argv) != 2: # len == 2 because the path to the module is arg 1.

        exit("Invalid argument, please pass a python file")

    # Add the __ALL_FUNCTIONS to the global scope of the verify module

    # and then run the script.  Save the global variables from script

    # execution so that we can find the __ALL_FUNCTIONS variable once

    # the script has finished executing.

    globs = {} # Global variables from script execution

    prefix = "import verify as __verifymod\n__verifymod.__ALL_FUNCTIONS = []\n"

    exec(prefix+open(sys.argv[1], "r").read(), globs)

    all_functions = globs["__verifymod"].__ALL_FUNCTIONS

    # Test each function from the script.

    for f in all_functions:

        assert hasattr(f, _FUN_PROPS), "Internal error"

        # Some function executions might take a while, so we print to

        # the screen when we begin testing a function, and then erase

        # it after we finish testing the function.  This is like a

        # make-shift progress bar.

        start_text = "    Testing %s..." % f.__name__

        print(start_text, end="", flush=True)

        test_function(f)

        import time

        time.sleep(1)

        # Extra spaces after "Tested %s" compensate for the fact that

        # the string to signal the start of testing function f is

        # longer than the string to signal function f has been tested,

        # so this avoids leaving extra characters on the terminal.

        print("\b"*len(start_text)+"    Tested %s    " % f.__name__, flush=True)

    print("Tested %i functions in %s." % (len(all_functions), sys.argv[1]))