How Does It Work?

This is a gentle introduction to Klara’s internal

Test case generation

The majority of Klara is built on the inference system. Consider the function below:

def foo(v1: int, v2: int):
    if v1 > v2:
        return 1
    else:
        return 10

If we try to infer the return value, we’ll get:

[InferenceResult(value=1, z3_assumptions=[v1 > v2]),
 InferenceResult(value=10, z3_assumptions=[Not(v1 > v2])]

From the InferenceResult, we’ll obtain the z3 assumptions that are sets of constraints that need to be True to get the corresponding value.

We’ll then consult the Z3 to generate a model that satisfy the constraint. The process can be simplified as:

>>> import z3
>>> v1 = z3.Int("v1")
>>> v2 = z3.Int("v2")
>>> solver = z3.Solver()
>>> solver.add(v1 > v2)
>>> if solver.check() == z3.sat:
...     model = solver.model()
...     print(model)
[v1 = 1, v2 = 0]

And for the value 10.:

>>> solver.reset()
>>> solver.add(z3.Not(v1 > v2))
>>> if solver.check() == z3.sat:
...     model = solver.model()
...     print(model)
[v1 = 0, v2 = 0]

Now, we have 2 sets of arguments, [v1 = 1, v2 = 0] and [v1 = 0, v2 = 0] and we can generate 2 function call that cover all return values from the function.

Z3 solver Integration

Let’s look closer at the interaction between inference system and Z3. For code below, say we want to infer() The value of variable target, assume that we have already setup function foo’s arguments as z3 variable

def foo(v1: int):
    target = v1 + 3

If we infer() target, it will return infer_binop with v1 + 3. Since we have setup v1 as Z3 variable, infer() of v1 will return a special value that emulates Z3 variable, and when it involve with other operation (e.g. v1 + 3), it will return InferenceResult of Z3 binop v1 + 3.

In a slightly complex example below:

def foo(v1: int, v2: int):
    if v1 > v2:
        return 1 + v2 + v1
    else:
        return 10 - v1

We’ll obtain Inference result of both result and z3 assumptions in a form of z3 expression. We’ll solve for z3 assumptions as usual and obtain the model, which we’ll substitute in the result to give us a constant that can be tested in pytest. The test file will generated for input above:

import test


def test_foo_0():
    assert test.foo(0, -1) == 0
    assert test.foo(0, 0) == 10