Inference

Inference provides a way to statically interpret python code, and it’s in the core of automatic test case generation.

Every ast node has corresponding infer() method, that returns a generator for potentially multiple values. Just a simple example to illustrate:

if x:
    s = 1
else:
    s = 2
d = 3 if y else 4
z = s + d

The variable s can take the value of 1 or 2, and vice versa for variable d. The binary operation between s and d will produce 4 values, which is product of both operands. To find that out in klara, we can utilize the infer() call on the node, assuming that source variable contain the program above.:

>>> import klara
>>> tree = klara.parse(source)
>>> expr = tree.body[-1].value
>>> print(expr)
s + d
>>> result = list(expr.infer())
>>> print(result)
[4, 5, 5, 6]

In some cases Klara can’t infer some node due to limited understanding or value is undefined in python, it will yield klara.Uninferable() node and no exception will be thrown. For following example, there is one path where its value is undefined, Klara will still able to infer all other possible values.:

if x > 1:
    s = undefined
elif x < 1:
    s = "str"
else:
    s = 2
z = s + 3

Running the example above, Klara will produce:

[Uninferable, 5]

By design, Klara tried to eliminate false-positive value that is, the control path corresponding to the value is invalid. One example is:

v1 = "a" if cond1() else "b"
z = v1 + v1 + v1

Each v1 has 2 possible values. But since the binary operation v1 + v1 refer to the same variable, ultimately it only produce 2 values, which is ['aaa', bbb'].

Since Klara has z3-solver support in the inference system, it can also be used to check path feasibility for more accuracy. For example:

def foo(v1: int):
    if v1 > 4:
        if v1 < 3:
            z = 1
        else:
            z = 2
    else:
        z = 3
    s = z

The statement z = 1 at line 4 is unreachable since the constraints: v1 > 4 and v1 < 3 is unsat. To do it in Klara, we need a way to tell Klara that the argument v1 should be converted to z3 int variable for symbolic interpretation. We can use MANAGER.initialize_z3_var_from_func(func) to register all arguments that are annotated in the func to be z3 symbols.:

>>> import klara
>>> tree = klara.parse(source)
>>> with klara.MANAGER.initialize_z3_var_from_func(tree.body[0]):
...     print(list(tree.body[0].body[-1].value.infer()))
[2, 3]

The value 1 is not printed since the constraints is unsat.

Note

if it’s inferring without registering the argument as z3 symbol, no constraint checking will take place, the variable s will inferred as [1, 2, 3]

Inference Result

All infer() returned result will wrapped in a class called Klara.inference.InferenceResult, that provide some helpful attributes.

• InferenceResult.status is a boolean. True if value is successfully inferred, false if otherwise.

• InferenceResult.result is the inferred value. This is also a Klara.BaseNode, since you can yield value other than const.

• InferenceResult.z3_assumptions is a set containing the constraints related to this value.

• InferenceResult.type is the type of the value. It’s also can be used as type inference (e.g. inferring function argument).

Supported features

This section will give reader a view on what sort of features that Klara support. Checking the test case (test/test_core/test_inference.py) here is also a good idea to understand features implemented.

Container/data structure

Basic features on python data structure (list, set, tuple, dict) is implemented, without dynamic modification support.