[RFC] Implement DexVerify and LTD

LTL_work.md

@@ -0,0 +1,213 @@
+# DexVerify
+## Contents
+1. Introduction
+2. Motivation
+3. Theory
+4. Quick reference
+
+## 1. Introduction
+A DexVerify command takes the form `DexVerify(p: Proposition)`. It will verify
+that the proposition `p` is true. The most basic proposition, an atomic
+proposition, expresses the expected state of the program at a given point in
+time, or `True` or `False`.
+
+For example, if you wanted to verify that at a given point in time the variable
+`a` is equal to `5`, you may write (1):
+```
+DexVerify(Expect('a', '5'))
+```
+
+In this example, it just so happens that the "given point in time" is the first
+step that the debugger takes (2). This is not a very useful verification
+because we could be stepping through pre-main startup code.
+
+If you want to check that eventually a local variable `a` is `5` you'd write:
+```
+DexVerify(Eventually(Expect('a', '5')))
+```
+
+`Eventually` is a temporal operator. **Temporal** operators work over **time**.
+Intuitively, `Eventually(p)` means that `p` must become true at some point
+during program execution.
+
+`Eventually(p)` is defined as `Until(True, p)`. It's easy to explain how this
+works if we take a look at `Until(p, q)`. `Until`, `Weak` and `Next`
+(see the Quick Reference section) are used to define all other temporal
+operators. All operators are exposed as functions so the formulae read in
+Polish, or 'prefix', notation.
+
+`Until(p, q)` means that `q` must hold in the future, and **until** then `p`
+must hold.
+
+Looking at `Eventually(p)` again then; `Until(True, p)` can be translated to
+"`p` must hold in the future, and until then, `True` must hold". `True` *is*
+always `True` so you could instead just say "`p` must hold in the future".
+
+Temporal operators are very useful but are not a catch-all solution. What if
+you want to say eventually `a == 5` and eventually `b == 1`? It's pretty much
+as easy as writing that. This is where boolean connectives come in:
+```
+DexVerify(And(Eventually(Expect('a', '5')), Eventually(Expect('b', '1'))))
+```
+
+This formula doesn't impose any ordering on the `Expect` propositions.
+If you want to say that `b == 1` at some point in the future **after**
+`a == 5` you'd write:
+```
+DexVerify(After(Expect('b', '1'), Expect('a', '5')))
+```
+
+For more examples have a look in dexter/examples/LTD. Please be aware that the
+prefix "xfail_" indicates that running that test should result in a failure.
+
+## 2. Motivation
+
+[TODO] Write this section
+
+
+## 3. Theory
+The DexVerify command formulae are based on Linear Temporal Logic (LTL).
+The standard definition of LTL is as follows (modified from
+[this](https://www.win.tue.nl/~jschmalt/teaching/2IX20/reader_software_specification_ch_9.pdf)
+source):
+
+```
+p ::= a  |  p /\ p  |  !p  |  Xp |  p U p
+```
+
+Where:
+* `a` is an atomic proposition
+* `p` represents a valid LTL formula
+* `X` denotes the ”next” operator
+* `U` denotes the ”until” operator
+* `!` denotes negation
+* `/\` denotes logical "and"
+
+
+Usual boolean connectives can be derived:
+```
+!(p /\ q) == p \/ q   // (disjunciton)
+!p \/ q == p --> q    // (implication)
+```
+
+From the syntax, we define the following:
+```
+p \/ !p == True
+!True == False
+```
+
+Further temporal operators can be derived:
+```
+F p == true U p  // p will hold at some point in the Future.
+```
+There are others, e.g. Weak(W) and Release(R) and more.
+
+[This](http://www.lsv.fr/~gastin/ltl2ba/index.php) website is a fantastic
+resource for viewing your LTL formula as a Büchi automaton.
+
+Operator precedence doesn't matter for our case because all operators
+are exposed as functions, but for infix LTL:
+1. Unary operators
+2. Binary temporal
+3. Binary boolean
+
+
+## 4. Quick reference
+### Atomic propositions
+#### Boolean
+```
+True
+False
+```
+Not strictly "atomic propositions" in terms of LTL theory.
+
+#### Expect
+```
+Expect(p, q)
+```
+Debugger C++ expression `p` must evaluate to value `q`.
+
+### Boolean functions
+
+#### And
+
+#### Or
+
+#### Not
+
+### Temporal functions
+
+#### Until
+```
+Until(p, q)
+```
+`q` must eventually hold and until then `p` must hold.<br/>
+LTL definition: `U` &#8801; Until &#8801; `q` holds at some time `i >= 0` and
+`p` holds for all `0 <= k < i`.
+
+#### Weak
+```
+Weak(p, q)
+```
+`p` must hold so long as `q` does not.<br/>
+LTL definition: `W` &#8801; Weak &#8801; Weak until &#8801; `q` holds at some
+time `i >= 0` or never holds `i = inf` and `p` holds for all `0 <= k < i`.
+
+#### Next
+```
+Next(p)
+```
+`p` must hold at the next time step.<br/>
+LTL definition: `X` &#8801; Next &#8801; `p` holds at next step.
+
+#### Eventually
+```
+Eventually(p)
+```
+`p` must eventually hold.<br/>
+LTL definition: `F` &#8801; Finally &#8801; Eventually &#8801; Future &#8801;
+`True U p`
+
+#### Release
+```
+Release(p, q)
+```
+`p` must eventually hold and up to and including that time `q` must hold.
+NOTE: Operand order and keyword *including*.<br/>
+LTL definition: `R` &#8801; Release &#8801; `q W (q /\ p)`
+
+#### Henceforth
+```
+Henceforth(p)
+```
+`p` must hold from now onwards.<br/>
+LTL definition: `G` &#8801; Globally &#8801; `False R p`
+
+#### After
+```
+After(p, q)
+```
+`p` holds at some point after `q`. Both must hold at some point but not
+simultaneously.<br/>
+LTL definition: `A` &#8801; After &#8801; `q /\ X(F(p))`
+
+#### Ordered
+```
+Ordered(p, q, r...)
+```
+The propositions may hold at any time so long as each proposition holds before
+the next (left to right) and they do all hold at some point.
+LTL definition: `O` &#8801; Ordered &#8801; `r... A (q A p)`
+
+---
+### Examples
+[TODO] Add examples after coming up with some syntactic sugar for the common
+patterns.
+
+
+### [TODO] / notes
+1. The Expect syntax will not look anything like this.
+2. Makes sense for the first step to be stepping into main -- discuss with team.
+3. It seems like all DexVerify() commands start wth Eventually. It might make
+sense to bake this in? E.g.
+DexVerify(p) == Eventually(And(Expect({frames: {main}}), p))

dex/command/CommandBase.py

@@ -35,3 +35,9 @@ def __init__(self):
     @abc.abstractmethod
     def eval(self):
         pass
+
+    def get_subcommands() -> dict:
+        """Returns a dictionary of subcommands in the form {name: command} or
+        None if no subcommands are required.
+        """
+        return None

dex/command/ParseCommand.py

@@ -32,6 +32,11 @@
 
 from dex.command.CommandBase import CommandBase
 from dex.utils.Exceptions import CommandParseError
+from dex.command.commands.LTD import (
+    And, Or, Not, Until, Expect, Eventually, Henceforth, Weak, Release,
+    ExpectState, Next, After
+)
+from dex.dextIR import CommandIR
 
 
 def _get_valid_commands():
@@ -60,30 +65,46 @@ def _get_valid_commands():
                 for c in inspect.getmembers(module, inspect.isclass)
                 if c[1] != CommandBase and issubclass(c[1], CommandBase)
             })
+
         _get_valid_commands.cached = commands
         return commands
 
 
-def get_command_object(commandIR):
-    """Externally visible version of _safe_eval.  Only returns the Command
-    object itself.
+def _get_command_name(command_raw: str) -> str:
+    """Return command name by splitting up DExTer command contained in
+       command_raw on the first opening paranthesis and further stripping
+       any potential leading or trailing whitespace.
     """
-    valid_commands = _get_valid_commands()
+    return command_raw.split('(', 1)[0].rstrip()
+
+
+def _merge_subcommands(command_name: str, valid_commands: dict) -> dict:
+    """Return a dict which merges valid_commands and subcommands for
+    command_name.
+    """
+    subcommands = valid_commands[command_name].get_subcommands()
+    if subcommands:
+        return { **valid_commands, **subcommands }
+    return valid_commands
+
+
+def _eval_command(command_raw: str, valid_commands: dict) -> CommandBase:
+    command_name = _get_command_name(command_raw)
+    valid_commands = _merge_subcommands(command_name, valid_commands)
     # pylint: disable=eval-used
-    command = eval(commandIR.raw_text, valid_commands)
+    command = eval(command_raw, valid_commands)
     # pylint: enable=eval-used
-    command.path = commandIR.loc.path
-    command.lineno = commandIR.loc.lineno
     return command
 
 
-def _get_command_name(command_raw):
-    """Return command name by splitting up DExTer command contained in
-       command_raw on the first opening paranthesis and further stripping
-       any potential leading or trailing whitespace.
+def get_command_object(commandIR: CommandIR):
+    """Externally visible version of _safe_eval.  Only returns the Command
+    object itself.
     """
-    command_name = command_raw.split('(', 1)[0].rstrip()
-    return command_name
+    command = _eval_command(commandIR.raw_text, _get_valid_commands())
+    command.path = commandIR.loc.path
+    command.lineno = commandIR.loc.lineno
+    return command
 
 
 def _find_all_commands_in_file(path, file_lines, valid_commands):
@@ -106,9 +127,7 @@ def _find_all_commands_in_file(path, file_lines, valid_commands):
 
         to_eval = line[column:].rstrip()
         try:
-            # pylint: disable=eval-used
-            command = eval(to_eval, valid_commands)
-            # pylint: enable=eval-used
+            command = _eval_command(to_eval, valid_commands)
             command_name = _get_command_name(to_eval)
             command.path = path
             command.lineno = lineno

dex/command/commands/DexVerify.py

@@ -0,0 +1,76 @@
+# DExTer : Debugging Experience Tester
+# ~~~~~~   ~         ~~         ~   ~~
+#
+# Copyright (c) 2018 by SN Systems Ltd., Sony Interactive Entertainment Inc.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in
+# all copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+# THE SOFTWARE.
+from dex.command.CommandBase import CommandBase
+from dex.command.commands.LTD.internal.Proposition import Boolean
+from dex.dextIR import DextIR, DextStepIter
+from dex.command.commands.LTD import (
+    Or, And, Not, Next, Weak, After, Until, Expect, Release, Eventually,
+    Henceforth, ExpectState, Ordered
+)
+
+
+class DexVerify(CommandBase):
+    """Define an LTD model which expresses expected debugging behaviour.
+
+    DexVerify(proposition)
+
+    See Commands.md for more info.
+    """
+
+    def __init__(self, *args):
+        if len(args) != 1:
+            raise TypeError('Expected exactly one arg')
+
+        self.model = args[0]
+        if isinstance(self.model, bool):
+            self.model = Boolean(self.model)
+
+    def eval(self, program: DextIR) -> bool:
+        # [TODO] return (bool, list) where list is a set of nested lists of
+        # string which describte the verification trace
+        trace_iter = DextStepIter(program)
+        return self.model.eval(trace_iter)
+
+    def get_subcommands():
+        # LTD operators which are exposed to test writers through DexVerify.
+        return {
+            'Or': Or,
+            'And': And,
+            'Not': Not,
+            'Next': Next,
+            'Weak': Weak,
+            'After': After,
+            'Until': Until,
+            'Expect': Expect,
+            'Ordered': Ordered,
+            'Release': Release,
+            'Eventually': Eventually,
+            'Henceforth': Henceforth,
+            'ExpectState': ExpectState,
+        }
+
+    def __str__(self):
+        return "DexVerify({})".format(self.model)
+
+    def __repr__(self):
+        return self.__str__()