[RFC] Implement DexVerify and LTD

[OCHyams]

EDIT Here's the full RFC walk through.

DexVerify and LTD

Background

Combined with #26, this patch allows us to use DExTer to verify any and all expected program states are encountered while debugging.

The work is all based on Linear Temporal Logic (LTL). Using LTL you can verify that a set of propositions hold over time. LTL uses a small set of base temporal operators and boolean connectives to build up complex propositions.

While not strictly true in LTL theory, consider the following to be our base set of operators:

Boolean
/\   - And
\/   - Or
!    - Not

Temporal:
U   - Until
W   - Weak
X   - Next

Andour atomic propositions as:

True
False
Some assertion about program state

LTL_work.md covers all the definitions of the operators, but I'll give a quick overview here.

Until: p U q means p must hold at least until q holds, which it must do at some point.

Weak (weak Until): p W q means p must hold until q holds, or forever if q does not hold.

Next: X p means p must hold in the next time frame.

Propositions can be combined with these operators to create new propositions:

p ::= a  |  p /\ p | p \/ p |  !p  |  Xp |  p U p | p W q

Where a is an atomic proposition as described above.

It becomes useful to define common formulae patterns as composite operators. One such example is Eventually or F for future.

F a == True U a

Taking the definition I provided earlier "True (p) must hold at least until q (a) holds, which it must do at some point". That is to say, a must Eventually hold.

LTL to LTD

The LTL operators are exposed as subcommands (referred to as LTD) to a new dexter command DexVerify.

Time is discrete, where each step represents a debugger step. Next(p) means that p must hold at the next debugger step.

Use the LTD command ExpectState to make an assertion about the program state. ExpectState behaves very similarly to the standalone DexExpectProgramState command.

To verify an assertion that some program state is eventually encountered, you'd write:

DexVerify(Eventually(ExpectState(/* Program state description  */)))

Implementation

The base operators are defined in BasicOperators.py. These are derived from an operator type (binary, unary) from OperatorTypes.py, which are all in turn derived from Proposition from Proposition.py.

Propositions and boolean connectives can only work on the program state as described by the debugger at a specific point in time. Temporal operators, however, need to look into the future.

To accomodate this a program state iterator DextStepIter is defined in DextIR.py. Operators can dereference and increment the iterator before passing it on to their operands. Any operator which must increment the iterator first copies it so that the "future looking" is limited to only its operands.

See Until.eval(...) and Next.eval(...) for concrete examples.

Using the basic operator types as a foundation with which to build all composite operators makes for some really compact defintions.

Composite operators, defined in CompositeOperators.py, inherit from Composite. They must call set_proposition to define the forumla they represent. For example, The sum of the class Eventually is as follows:

class Eventually(Composite, UnaryOperator):
    def __init__(self, *args):
        super().__init__(*args)
        self.set_proposition(Until(True, self.operand))

Remember that the definition for Eventually (F) is True U a.

This RFC defines more composite operators but hopefully you're now equipped to look at these in source.

The examples/LTD/ directory contains some simple examples which can be run through DExTer with this patch (xfail prefix denotes an expected failure).

Shortcomings

1. This patch doesn't provide any nice output for --verbose. We need to implement a nice error reporter which can concisely explain why a given model doesn't hold.

2. Exposing operators as function calls means all formulae read in prefix notation. This turns p Until q into Until(p, q). I personally read this left to right as "Until p holds, q must hold". This is incorrect. Until(p, q) means "Until q holds, p must hold". I find that swapping the operands makes it more readable, but then of course makes it confusing to people who read prefix notation naturally. I think this at least warrants a discussion.

3. Prefix notation also makes some operators read strangely. I think Both(p, q) and Either(p, q) instead of And(p, q) and Or(p, q) respectively are more natural.

4. The implementation doesn't do anything to prevent someone adding an operator with circular dependencies. Hopefully whoever implemented the new operator will have run tests with it and then seen a max stack depth exception.

[OCHyams]

At the moment the LTL_work document is around 200 lines, there are at least 100 lines of license comments, and there are around 150 lines of "example" test files. So, this PR is not actually as large as it looks.

[OCHyams]

I've noticed that my implementation of Next() is inconsistent. Say we are on the last program step and are verifying Next(p). If p is an Expect or ExpectState it will not hold because the step_iter cannot be dereferenced. However, if p is simply True, it will hold because we never have to dereference the iter to find out the result of the proposition.

An easy fix: Next() should return False if the end of the program is reached after incrementing the iterator.

[OCHyams]

Thanks @Melamoto for taking a look!

[OCHyams]

Latest commit (afbd9ff) fixes Next, simplifies Henceforth(), and corrects some typos. Note: I haven't added/updated the docstrings yet.