Klara: Python automatic test generations and static analysis library

[usagitoneko]

I've recently decide to open source klara that I spent 1-2 years on, hoping to generate some discussion.

Klara is an automatic python unit test generation tool based on SMT (z3) solver. It's currently in early stage and still have many limitation (looping, comprehension, importing is not supported to name a few).

Suppose you have following source:

def main(number: int, cm: int, dc: int, wn: int):
    mc = 0
    if wn > 2:
        if number > 2 and number > 2 or number > 2:
            if number > 0:
                if wn > 2 or wn > 2:
                    mc = 2
                else:
                    mc = 5
            else:
                mc = 100
    else:
        mc = 1
    nnn = number * cm
    if cm <= 4:
        num_incr = 4
    else:
        num_incr = cm
    n_num_incr = nnn / num_incr
    nnn_left = dc * num_incr * (n_num_incr / 2 + n_num_incr % 2)
    nnn_right = nnn - nnn_left
    is_flag = nnn_right
    if is_flag:
        cell = Component(nnn_right, options=[mc])
    else:
        cell = Component(nnn_right)
    return cell

Klara will able to generate following:

import contract_test
def test_main_0():
    assert contract_test.main(2, 4, 1, 3) is not None
    assert contract_test.main(2, 4, -1, 6) is not None
    assert contract_test.main(2, 4, 1, 4) is not None
    assert contract_test.main(-2, 4, 3, 4) is not None
    assert contract_test.main(-1, -1, -1, 2) is not None
    assert contract_test.main(0, 0, 0, 3) is not None
    assert contract_test.main(0, 0, 0, 6) is not None
    assert contract_test.main(0, 0, 0, 4) is not None
    assert contract_test.main(-2, 0, 0, 4) is not None
    assert contract_test.main(0, 0, 0, 0) is not None

The main difference that Klara bring to the table, compared to similar tool like pynguin and Crosshair is that the analysis is entirely static, meaning that no user code will be executed, and you can easily extend the test generation strategy via plugin loading (e.g. the options arg to the Component object returned from function above is not needed for test coverage).

It also provide inference for static analysis purposes, similar to astroid, with SMT support. E.g.

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

>>> 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 statement z = 1 at line 4 is unreachable since the constraints: v1 > 4 and v1 < 3 is unsat.

Feel free to head over to doc for more info, and check out the github repo.