README.md
1<!--
2 Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3
4 SPDX-License-Identifier: CC-BY-SA-4.0
5-->
6
7The NICTA Graph Refinement Toolset
8==================================
9
10This is a set of tools which discover and check refinement proofs between
11programs with fairly arbitrary control flow graphs, including a number of
12kinds of loop relationships. The tools are written in python and make heavy
13use of SMT solvers.
14
15The design and theory of this tool are described in the paper [Translation
16Validation for a Verified OS Kernel][1] by Sewell, Myreen & Klein.
17
18 [1]: https://ssrg.nicta.com.au/publications/nictaabstracts/Sewell_MK_13.abstract.pml "Translation Validation for a Verified OS Kernel"
19
20Repository Setup
21----------------
22
23This tool can be used as it is. It is also designed to link with the
24[L4.verified][2] proof chain. The full proof chain can be fetched via a
25Google [repo][3] setup. To obtain the full environment, instead of cloning
26this repository, follow the instructions in the [manifest repository][4] here:
27
28 https://github.com/seL4/verification-manifest
29
30To set up the various tools in the verification bundle, see the section
31[Dependencies](#dependencies) below.
32
33 [2]: https://github.com/seL4/l4v "L4.verified Repository"
34 [3]: http://source.android.com/source/downloading.html#installing-repo "google repo installation"
35 [4]: https://github.com/seL4/verification-manifest "Verification Manifest Repository"
36
37Examples
38--------
39
40The [`example`](example/) and [`loop-example`](loop-example/) directories
41contain prebuilt example refinement targets. The [`example`](example/)
42directory contains a number of handwritten demonstration problems. The
43[`loop-example`](loop-example/) contains example compilation and decompilation
44of a simple example program involving a loop both the `-O1` and `-O2` arguments
45to `gcc`. Both versions should be provable, but the `-O2` version involves a
46loop unrolling that is computationally expensive to verify.
47
48The examples can be used to exercise the tool as follows:
49
50 python graph-refine.py example f g rotate_right has_value
51 python graph-refine.py loop-example/O1 all
52
53 # *much* slower
54 python graph-refine.py loop-example/O2 all
55
56The [`seL4-example`](seL4-example/) directory contains a recipe for building
57the seL4 binary verification problem. If this repository is set up via the
58[verification manifest][4] then most of the necessary components will be
59present. More information on running the full process is included in the
60[`seL4-example`](seL4-example/) directory.
61
62Dependencies
63------------
64
65The tool requires the use of an SMT solver supporting the QF\_ABV logic, which
66is not provided here. Available solvers should be listed in a `.solverlist`
67configuration file. Further documentation will be given on the command line if
68the configuration is missing or invalide. The `.solverlist` file format is also
69documented in in [`solver.py`](solver.py).
70
71To test the solver setup is working:
72
73 python solver.py test
74
75Additional dependencies are required to run the full seL4 binary verification
76problem. They are described in the [`seL4-example`](seL4-example/) directory.
77
78Usage
79-----
80
81The tool is invoked by:
82
83 python graph-refine.py <target> <instructions>
84
85A target is a directory which contains all of the functions and configuration
86associated with an input problem. Target directories must contain a target.py
87setup script. See the example directory for an example.
88
89There are various instructions available:
90
91 - all: test all functions. this will usually be the last instruction.
92 - no-loops: skip functions with loops
93 - only-loops: skip functions without loops
94 - verbose: produce a lot of diagnostic output in subsequent instructions.
95 - `function-name`: other instructions will be taken as the name of a single
96function to be tested.
97
98Overview
99--------
100
101 - [syntax.py](syntax.py): defines the syntax of the graph language and its parser. A syntax reference is included.
102 - [logic.py](logic.py): defines the top-level per-function proof obligations. Also provides various graph algorithms.
103 - [problem.py](problem.py): stores the state of one refinement problem. Keeps mutable copies of graph functions, allowing inlining.
104 - [solver.py](solver.py): controls the SMT solver. Manages an SMT problem state and some logical extensions.
105 - [rep\_graph.py](rep_graph.py): populates the solver state with a model produced from a problem.
106 - [check.py](check.py): defines the refinement proof format and the process for checking a proof.
107 - [search.py](search.py): searches for a refinement proof.
108 - [stack\_logic.py](stack_logic.py): provides additional analysis to address stack aspects of the binary calling convention.
109 - [graph-refine.py](graph-refine.py): top level.
110
111 - [trace\_refute.py](trace_refute.py): adaptation of this tool to detect
112 impossible traces. This may be useful for other static analysis, e.g. WCET
113 estimation.
114 - [debug.py](debug.py): debug helper code.
115
116 - [example](example), [loop-example](loop-example),
117 [seL4-example](seL4-example) are discussed in the [Examples](#examples)
118above.
119
120