ISLearn

ISLearn is a system for learning ISLa constraints from a set of patterns. Patterns are instantiated according to sample inputs (that can also automatically be generated based on a given program property), filtered, and combined to a disjunctive normal form (conjunctions of disjunctions of literals, where literals are possibly negated, instantiated patterns). ISLearn output the result ranked by estimates for specificity and recall of the results: Top-ranked invariants were found to be best suitable for distinguishing positive (with respect to a program property) and negative inputs.

Example

Consider a grammar of a simple assignment programming language (e.g., "x := 1 ; y := x"):

import string

LANG_GRAMMAR = {
    "<start>":
        ["<stmt>"],
    "<stmt>":
        ["<assgn>", "<assgn> ; <stmt>"],
    "<assgn>":
        ["<var> := <rhs>"],
    "<rhs>":
        ["<var>", "<digit>"],
    "<var>": list(string.ascii_lowercase),
    "<digit>": list(string.digits)
}

For learning input invariants, we need a property of the inputs satisfying that invariant. If the goal is to learn properties about (non-context-free) syntactical correctness of a programming language, this is a function returning True if, and only if, a statement is executed without raising a specific class of errors. For our language described by LANG_GRAMMAR, we define an eval_lang function that raises an error if an identifier is not defined; validate_lang turns this into a property.

from typing import Dict
from islearn.parse_tree_utils import dfs, get_subtree, tree_to_string

from isla.language import DerivationTree
from isla.parser import EarleyParser
from isla.type_defs import ParseTree

def eval_lang(inp: str) -> Dict[str, int]:
    def assgnlhs(assgn: ParseTree):
        return tree_to_string(get_subtree(assgn, (0,)))

    def assgnrhs(assgn: ParseTree):
        return tree_to_string(get_subtree(assgn, (2,)))

    valueMap: Dict[str, int] = {}
    tree = list(EarleyParser(LANG_GRAMMAR).parse(inp))[0]

    def evalAssignments(tree):
        node, children = tree
        if node == "<assgn>":
            lhs = assgnlhs(tree)
            rhs = assgnrhs(tree)
            if rhs.isdigit():
                valueMap[lhs] = int(rhs)
            else:
                valueMap[lhs] = valueMap[rhs]

    dfs(tree, evalAssignments)

    return valueMap

def validate_lang(inp: DerivationTree) -> bool:
    try:
        eval_lang(str(inp))
        return True
    except Exception:
        return False

ISLearn can learn this property based on the "Def-Use (reST Strict)" pattern from the catalog (the standard catalog is in src/islearn/patterns.toml). You call the learner as follows:

from islearn.learner import InvariantLearner
from isla.language import ISLaUnparser, Formula
from typing import Dict, Tuple

result: Dict[Formula, Tuple[float, float]] = InvariantLearner(
    LANG_GRAMMAR,
    prop=validate_lang,
    activated_patterns={
        "Def-Use (reST Strict)",  # Optional; leads to quicker results
    },
).learn_invariants()

print("\n".join(map(
    lambda p: f"{p[1]}: " + ISLaUnparser(p[0]).unparse(),
    {f: p for f, p in result.items() if p[0] > .0}.items())))

The expected result is

(1.0, 1.0): forall <rhs> use_ctx="{<var> use}" in start:
  exists <assgn> def_ctx="{<var> def} := <rhs>" in start:
    (before(def_ctx, use_ctx) and
    (= use def))

That invariant has full specificity (first value in the tuple) and recall (second value), since it holds exactly for all valid inputs.

Resources / Important Files

• You find the pattern catalog in src/islearn/patterns.toml.
• The evaluation scripts are in the directory evaluations/.
• The most important files of our implementation are src/islearn/learner.py, containing the learning incl. candidate generation, filtering, etc., and and src/islearn/language.py, which defines the abstract ISLa langauge for the patterns catalog.

Configuration Parameters

ISLearn (the class InvariantLearner) has a number of optional configuration parameters that can be passed to the constructor; many of them can be used to reduce or expand the search space, and thus either lead to more / longer invariants or to quicker results.

Install, Build, Test

ISLearn depends on Python 3.10 and the Python header files. To compile all of ISLearns's dependencies, you need gcc, g++ make, and cmake. To check out the current ISLearn version, git will be needed. Furthermore, python3.10-venv is required to run ISLearn in a virtual environment.

On Alpine Linux, all dependencies can be installed using

apk add python3.10 python3.10-dev python3.10-venv gcc g++ make cmake git 

Install

To install ISLearn, a simple pip install islearn suffices. We recommend installing ISLearn inside a virtual environment (virtualenv):

python3.10 -m venv venv
source venv/bin/activate
pip install --upgrade pip
pip install islearn

Build

ISLearn is built locally as follows:

git clone https://github.com/rindPHI/islearn.git
cd islearn/

python3.10 -m venv venv
source venv/bin/activate

pip install --upgrade pip
pip install --upgrade build
python3 -m build

Then, you will find the built wheel (*.whl) in the dist/ directory.

Testing & Development

For running the ISLearn tests, you additionally need clang, racket, and graphviz. On Alpine Linux, you can install those by

apk update
apk upgrade
apk add clang racket graphviz

Then, you can run the ISLearn tests as follows:

git clone https://github.com/rindPHI/islearn.git
cd islearn/

python3.10 -m venv venv
source venv/bin/activate
pip install --upgrade pip

# Run tests
pip install -e .[test]
python3 -m pytest -n 16 tests