NameDateSize

..25-Jul-20198

.gitignoreH A D25-Jul-20196

__init__.pyH A D25-Jul-20190

c_rodata.pyH A D25-Jul-20191,021

check.pyH A D25-Jul-201930.7 KiB

debug.pyH A D25-Jul-201925 KiB

example/H25-Jul-20194

graph-refine.pyH A D25-Jul-201910.6 KiB

graph-to-graph/H25-Jul-201926

inst_logic.pyH A D25-Jul-20196.2 KiB

LICENSE_BSD2.txtH A D25-Jul-20191.4 KiB

logic.pyH A D25-Jul-201948.5 KiB

loop-example/H25-Jul-20199

loop_bounds.pyH A D25-Jul-201931.3 KiB

objdump.pyH A D25-Jul-20194 KiB

problem.pyH A D25-Jul-201922.8 KiB

pseudo_compile.pyH A D25-Jul-201914.3 KiB

README.mdH A D25-Jul-20194.9 KiB

rep_graph.pyH A D25-Jul-201935.8 KiB

run_testsH A D25-Jul-2019844

scripts/H25-Jul-20194

search.pyH A D25-Jul-201957.5 KiB

seL4-example/H25-Jul-201910

solver.pyH A D25-Jul-201967.9 KiB

stack_logic.pyH A D25-Jul-201939.9 KiB

stats.pyH A D25-Jul-20196.8 KiB

syntax.pyH A D25-Jul-201946.5 KiB

target_objects.pyH A D25-Jul-20192.6 KiB

trace_refute.pyH A D25-Jul-201919.4 KiB

README.md

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