Mining Function Specifications (for dynamic invariants)

However, not every piece of code is developed with explicit specifications in the first place; let alone does most code comes with formal pre- and post-conditions. (Just take a look at the chapters in this book.) This is a pity: As Ken Thompson famously said, "Without specifications, there are no bugs – only surprises". It is also a problem for testing, since, of course, testing needs some specification to test against. This raises the interesting question: Can we somehow retrofit existing code with "specifications" that properly describe their behavior, allowing developers to simply check them rather than having to write them from scratch? This is what we do in this chapter.

my_sqrt() does not come with any functionality that would check types or values. Hence, it is easy for callers to make mistakes when calling my_sqrt():

At least, the Python system catches these errors at runtime. The following call, however, simply lets the function enter an infinite loop:

Our goal is to avoid such errors by annotating functions with information that prevents errors like the above ones. The idea is to provide a specification of expected properties – a specification that can then be checked at runtime or statically.

\todo{Introduce the concept of contract.}

As writer of Python code, omitting explicit type declarations may save time (and allows for some fun hacks). It is not sure whether a lack of types helps in reading and understanding code for humans. For a computer trying to analyze code, the lack of explicit types is detrimental. If, say, a constraint solver, sees if x: and cannot know whether x is supposed to be a number or a string, this introduces an ambiguity. Such ambiguities may multiply over the entire analysis in a combinatorial explosion – or in the analysis yielding an overly inaccurate result.

Python 3.6 and later allows data types as annotations to function arguments (actually, to all variables) and return values. We can, for instance, state that my_sqrt() is a function that accepts a floating-point value and returns one:

By default, such annotations are ignored by the Python interpreter. Therefore, one can still call my_sqrt_typed() with a string as an argument and get the exact same result as above. However, one can make use of special typechecking modules that would check types – dynamically at runtime or statically by analyzing the code without having to execute it.

Now, invoking my_sqrt_with_checked_type_annotations() raises an exception when invoked with a type different from the one declared:

Note that this error is not caught by the "untyped" variant, where passing a boolean value happily returns $\sqrt{1}$ as result.

In Python (and other languages), the boolean values True and False can be implicitly converted to the integers 1 and 0; however, it is hard to think of a call to sqrt() where this would not be an error.

These are the contents of our newly created Python file:

Mypy is a type checker for Python programs. As it checks types statically, types induce no overhead at runtime; plus, a static check can be faster than a lengthy series of tests with runtime type checking enabled. Let us see what mypy produces on the above file:

We see that mypy complains about untyped function definitions such as my_sqrt(); most important, however, it finds that the call to my_sqrt_with_type_annotations() in the last line has the wrong type.

With mypy, we can achieve the same type safety with Python as in statically typed languages – provided that we as programmers also produce the necessary type annotations. Is there a simple way to obtain these?

The traceit() method does nothing yet; this is done in specialized subclasses. The CallTracker class implements a traceit() function that checks for function calls and returns:

trace_call() is called when a function is called; it retrieves the function name and current arguments, and saves them on a stack.

When the function returns, trace_return() is called. We now also have the return value. We log the whole call with arguments and return value (if desired) and save it in our list of calls.

simple_call_string() is a helper for logging that prints out calls in a user-friendly manner.

add_call() saves the calls in a list; each function name has its own list.

Using calls(), we can retrieve the list of calls, either for a given function, or for all functions.

Let us now put this to use. We turn on logging to track the individual calls and their return values:

After execution, we can retrieve the individual calls:

Each call is pair (argument_list, return_value), where argument_list is a list of pairs (parameter_name, value).

If the function does not return a value, return_value is None.

We can retrieve the type of the first argument to my_sqrt():

as well as the type of the return value:

Hence, we see that (so far), my_sqrt() is a function taking (among others) integers and floats and returning floats. We could declare my_sqrt() as:

This is a representation we could place in a static type checker, allowing to check whether calls to my_sqrt() actually pass a number. A dynamic type checker could run such checks at runtime. And of course, any symbolic interpretation will greatly profit from the additional annotations.

By default, Python does not do anything with such annotations. However, tools can access annotations from functions and other objects:

This is how run-time checkers access the annotations to check against.

We can get the source of a Python function using inspect.getsource(). (Note that this does not work for functions defined in other notebooks.)

To view these in a visually pleasing form, our function print_content(s, suffix) formats and highlights the string s as if it were a file with ending suffix. We can thus view (and highlight) the source as if it were a Python file:

Parsing this gives us an abstract syntax tree (AST) – a representation of the program in tree form.

What does this AST look like? The helper functions ast.dump() (textual output) and showast.show_ast() (graphical output with showast) allow us to inspect the structure of the tree. We see that the function starts as a FunctionDef with name and arguments, followed by a body, which is a list of statements of type Expr (the docstring), type Assign (assignments), While (while loop with its own body), and finally Return.

Too much text for you? This graphical representation may make things simpler.

The function ast.unparse() converts such a tree back into the more familiar textual Python code representation. Comments are gone, and there may be more parentheses than before, but the result has the same semantics:

The core of TypeTransformer is the method visit_FunctionDef(), which is called for every function definition in the AST. Its argument node is the subtree of the function definition to be transformed. Our implementation accesses the individual arguments and invokes annotate_args() on them; it also sets the return type in the returns attribute of the node.

Each argument gets its own annotation, taken from the types originally passed to the class:

Does this work? Let us annotate the AST from my_sqrt() with types for the arguments and return types:

When we unparse the new AST, we see that the annotations actually are present:

Similarly, we can annotate the hello() function from above:

For composite structures, type_string() does not examine element types; hence, the type of [3] is simply list instead of, say, list[int]. For now, list will do fine.

type_string() will be used to infer the types of argument values found at runtime, as returned by CallTracker.calls():

The function annotate_types() takes such a list of calls and annotates each function listed:

For each function, we get the source and its AST and then get to the actual annotation in annotate_function_ast_with_types():

The function annotate_function_ast_with_types() invokes the TypeTransformer with the calls seen, and for each call, iterate over the arguments, determine their types, and annotate the AST with these. The universal type Any is used when we encounter type conflicts, which we will discuss below.

Here is my_sqrt() annotated with the types recorded usign the tracker, above.

Here is how to use TypeAnnotator. We first track a series of calls:

After tracking, we can immediately retrieve an annotated version of the functions tracked:

This also works for multiple and diverse functions. One could go and implement an automatic type annotator for Python files based on the types seen during execution.

A content as above could now be sent to a type checker, which would detect any type inconsistency between callers and callees. Likewise, type annotations such as the ones above greatly benefit symbolic code analysis (as in the chapter on symbolic fuzzing), as they effectively constrain the set of values that arguments and variables can take.

The following function sum3() can be called with floating-point numbers as arguments, resulting in the parameters getting a float type:

If we call sum3() with integers, though, the arguments get an int type:

And we can also call sum3() with strings, giving the arguments a str type:

If we have multiple calls, but with different types, TypeAnnotator() will assign an Any type to both arguments and return values:

A type Any makes it explicit that an object can, indeed, have any type; it will not be type-checked at runtime or statically. To some extent, this defeats the power of type checking; but it also preserves some of the type flexibility that many Python programmers enjoy. Besides Any, the typing module supports several additional ways to define ambiguous types; we will keep this in mind for a later exercise.

With these, we can now start decorating my_sqrt():

This catches arguments violating the precondition:

Likewise, we can provide a postcondition:

If we have a buggy implementation of $\sqrt{x}$, this gets caught quickly:

While checking pre- and postconditions is a great way to catch errors, specifying them can be cumbersome. Let us try to see whether we can (again) mine some of them.

When my_sqrt(x) is called as, say my_sqrt(5.0), we see that x = 5.0 holds. The above properties would then all be checked for x. Only the properties X > 0, X >= 0, and X != 0 hold for the call seen; and hence x > 0, x >= 0, and x != 0 would make potential preconditions for my_sqrt(x).

We can check for many more properties such as relations between two arguments:

Types also can be checked using properties. For any function parameter X, only one of these will hold:

We can check for arithmetic properties:

Here's relations over three values, a Python special:

Finally, we can also check for list or string properties. Again, this is just a tiny selection.

Here is a simple example:

To get all combinations, we use the Python permutations() function:

The function true_property_instantiations() takes a property and a list of tuples (var_name, value). It then produces all instantiations of the property with the given values and returns those that evaluate to True.

Here is an example. If x == -1 and y == 1, the property X < Y holds for x < y, but not for y < x:

The instantiation retrieves the short form:

Likewise, with values for x and y as above, the property X < 0 only holds for x, but not for y:

By default, an InvariantTracker uses the properties as defined above; however, one can specify alternate sets of properties.

The key method of the InvariantTracker is the invariants() method. This iterates over the calls observed and checks which properties hold. Only the intersection of properties – that is, the set of properties that hold for all calls – is preserved, and eventually returned. The special variable return_value is set to hold the return value.

Here's an example of how to use invariants(). We run the tracker on a small set of calls.

The invariants() method produces a set of properties that hold for the observed runs, together with their instantiations over function arguments.

As before, the actual instantiations are easier to read:

We see that the both x and the return value have a float type. We also see that both are always greater than zero. These are properties that may make useful pre- and postconditions, notably for symbolic analysis.

However, there's also an invariant which does not universally hold, namely return_value <= x, as the following example shows:

Clearly, 0.1 > 0.01 holds. This is a case of us not learning from sufficiently diverse inputs. As soon as we have a call including x = 0.1, though, the invariant return_value <= x is eliminated:

We will discuss later how to ensure sufficient diversity in inputs. (Hint: This involves test generation.)

Let us try out our invariant tracker on sum3(). We see that all types are well-defined; the properties that all arguments are non-zero, however, is specific to the calls observed.

If we invoke sum3() with strings instead, we get different invariants. Notably, we obtain the postcondition that the return value starts with the value of a – a universal postcondition if strings are used.

If we invoke sum3() with both strings and numbers (and zeros, too), there are no properties left that would hold across all calls. That's the price of flexibility.

We start with a helper method. params() returns a comma-separated list of parameter names as observed during calls.

Now for the actual annotation. preconditions() returns the preconditions from the mined invariants (i.e., those properties that do not depend on the return value) as a string with annotations:

postconditions() does the same for postconditions:

With these, we can take a function and add both pre- and postconditions as annotations:

Here comes function_with_invariants() in all its glory:

Quite a lot of invariants, is it? Further below (and in the exercises), we will discuss on how to focus on the most relevant properties.

Almost all these properties (except for the very first) are relevant. Of course, the reason the invariants are so neat is that the return value is equal to len(L) is that X == len(Y) is part of the list of properties to be checked.

The next example is a very simple function:

The invariants all capture the relationship between a, b, and the return value as return_value == a + b in all its variations.

If we have a function without return value, the return value is None, and we can only mine preconditions. (Well, we get a "postcondition" that the return value is non-zero, which holds for None).

The "annotated" version checks against invalid arguments – or more precisely, against arguments with properties that have not been observed yet:

This is in contrast to the original version, which just hangs on negative values:

If we make changes to the function definition such that the properties of the return value change, such regressions are caught as violations of the postconditions. Let us illustrate this by simply inverting the result, and return $-2$ as square root of 4.

Technically speaking, $-2$ is a square root of 4, since $(-2)^2 = 4$ holds. Yet, such a change may be unexpected by callers of my_sqrt(), and hence, this would be caught with the first call:

We see how pre- and postconditions, as well as types, can serve as oracles during testing. In particular, once we have mined them for a set of functions, we can check them again and again with test generators – especially after code changes. The more checks we have, and the more specific they are, the more likely it is we can detect unwanted effects of changes.

The mined precondition a == b, for instance, only holds for the single call observed; the same holds for the mined postcondition return_value == a * b. Yet, sum2() can obviously be successfully called with other values that do not satisfy these conditions.

To get out of this trap, we have to learn from more and more diverse runs. If we have a few more calls of sum2(), we see how the set of invariants quickly gets smaller:

But where to we get such diverse runs from? This is the job of generating software tests. A simple grammar for calls of sum2() will easily resolve the problem.

But then, writing tests (or a test driver) just to derive a set of pre- and postconditions may possibly be too much effort – in particular, since tests can easily be derived from given pre- and postconditions in the first place. Hence, it would be wiser to first specify invariants and then let test generators or program provers do the job.

Also, an API grammar, such as above, will have to be set up such that it actually respects preconditions – in our case, we invoke sqrt() with positive numbers only, already assuming its precondition. In some way, one thus needs a specification (a model, a grammar) to mine another specification – a chicken-and-egg problem.

However, there is one way out of this problem: If one can automatically generate tests at the system level, then one has an infinite source of executions to learn invariants from. In each of these executions, all functions would be called with values that satisfy the (implicit) precondition, allowing us to mine invariants for these functions. This holds, because at the system level, invalid inputs must be rejected by the system in the first place. The meaningful precondition at the system level, ensuring that only valid inputs get through, thus gets broken down into a multitude of meaningful preconditions (and subsequent postconditions) at the function level.

The big requirement for this, though, is that one needs good test generators at the system level. In the next part, we will discuss how to automatically generate tests for a variety of domains, from configuration to graphical user interfaces.

The interaction between test generators and invariant detection is already discussed in [Ernst et al, 2001] (incidentally also using grammars). The Eclat tool [Pacheco et al, 2005] is a model example of tight interaction between a unit-level test generator and DAIKON-style invariant mining, where the mined invariants are used to produce oracles and to systematically guide the test generator towards fault-revealing inputs.

Mining specifications is not restricted to pre- and postconditions. The paper "Mining Specifications" [Ammons et al, 2002] is another classic in the field, learning state protocols from executions. Grammar mining, as described in our chapter with the same name can also be seen as a specification mining approach, this time learning specifications of input formats.

The following implementation adds an optional doc keyword argument which is printed if the invariant is violated: