/
meta.yml
180 lines (146 loc) · 6.53 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
---
fullname: Chip
shortname: chip
opam_name: coq-chip
organization: palmskog
community: false
action: true
dune: false
coqdoc: false
synopsis: Coq formalization of change impact analysis
description: |-
Coq specification and executable functions
for change impact analysis, as used in build systems
and tools for regression test selection.
publications:
- pub_url: http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf
pub_title: Practical Machine-Checked Formalization of Change Impact Analysis
pub_doi: 10.1007/978-3-030-45237-7_9
authors:
- name: Cyril Cohen
- name: Aleksandar Nanevski
- name: Karl Palmskog
- name: Laurent Théry
maintainers:
- name: Karl Palmskog
nickname: palmskog
opam-file-maintainer: palmskog@gmail.com
opam-file-version: dev
license:
fullname: MIT license
identifier: MIT
supported_coq_versions:
text: 8.13 or later
opam: '{>= "8.13"}'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "1.12.0"}'
description: |-
[MathComp ssreflect 1.12 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
description: |-
[MathComp fingroup](https://math-comp.github.io)
tested_coq_opam_versions:
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.14'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.13'
repo: 'mathcomp/mathcomp-dev'
- version: '1.12.0-coq-8.14'
repo: 'mathcomp/mathcomp'
- version: '1.12.0-coq-8.13'
repo: 'mathcomp/mathcomp'
namespace: chip
keywords:
- name: change impact analysis
- name: graph theory
categories:
- name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
build: |-
## Building the Coq formalization
Make sure the Coq requirements are installed, then run:
``` shell
git clone https://github.com/palmskog/chip.git
cd chip
make # or make -j <number-of-cores-on-your-machine>
```
## Building and running the executable tools
The executable tools have the following additional OCaml requirements:
- [OCaml 4.05.0 or later](https://ocaml.org)
- [Ocamlbuild](https://github.com/ocaml/ocamlbuild)
- [yojson](https://github.com/ocaml-community/yojson)
- [extlib](https://github.com/ygrek/ocaml-extlib)
After installing the Coq requirements, install the OCaml requirements:
```
opam install ocamlbuild yojson extlib
```
To build the regular tool, run:
```
make impacted
```
To try plain change impact analysis, go to `extraction/impacted` and run:
```
./filtering.native test/new.json test/old.json
```
To try hierarchical change impact analysis, run:
```
./hierarchical.native test/new-hierarchical.json test/old-hierarchical.json
```
To try topological sorting, run:
```
./topfiltering.native test/new-topsort.json test/old-topsort.json
```
To build the optimized tool:
```
make impacted-rbt
```
and look in `extraction/impacted-rbt`. The programs and command-line
options are the same as above.
documentation: |-
## Files
Coq files adapted and extended from work by [Cohen and Théry](https://github.com/CohenCyril/tarjan):
- `core/extra.v`: auxiliary sequence lemmas
- `core/connect.v`: auxiliary connect and topological sort definitions and lemmas
- `core/kosaraju.v`: implementation and correctness proof of Kosaraju's strongly connected components algorithm
- `core/tarjan.v`: implementation and correctness proof of Tarjan's strongly connected components algorithm
Coq file adapted from work by [Nanevski](https://github.com/imdea-software/fcsl-pcm):
- `core/ordtype.v`: ordered type definition for the Mathematical Components library
Coq core definitions and lemmas:
- `core/closure.v`: basic definition of transitive closures of sets
- `core/check.v`: set-based definitions of dependency graphs, impactedness, and freshness
- `core/change.v`: correctness argument for basic change impact analysis definitions
- `core/hierarchical.v`: overapproximation strategy for change impact analysis in hierarchical systems
- `core/hierarchical_correct.v`: correctness proofs for overapproximation strategy
- `core/hierarchical_sub.v`: compositional strategy for change impact analysis in hierarchical systems
- `core/hierarchical_sub_correct.v`: correctness proofs for compositional strategy
- `core/hierarchical_sub_pt.v`: improved hierarchical compositional strategy using partition of new vertices
- `core/hierarchical_sub_pt_correct.v`: correctness proofs for improved compositional strategy
- `core/acyclic.v`: definition of and basic lemmas for acyclicity, parameterized acyclicity checker
- `core/kosaraju_acyclic.v`: acyclicity checking based on Kosaraju's algorithm
- `core/tarjan_acyclic.v`: acyclicity checking based on Tarjan's algorithm
- `core/topos.v`: definitions and lemmas on topological sorting of acyclic graphs
Coq implementation-related definitions and lemmas:
- `core/close_dfs.v`: refined sequence-based transitive closure computation
- `core/dfs_set.v`: refined transitive closure computation using MSet functor (to enable red-black trees)
- `core/check_seq.v`: sequence-based change impact analysis definitions, optimized topological sorting using impact analysis
- `core/check_seq_hierarchical.v`: sequence-based hierarchical change impact analysis definitions
- `core/finn.v`: regular instantiation of sequence-based definitions for the ordinal finite type
- `core/finn_set.v`: red-black tree instantiation of sequence-based definitions for the ordinal finite type
Key OCaml files for regular tool:
- `extraction/impacted/ocaml/change_impact.mli`: interface to extracted code
- `extraction/impacted/ocaml/change_impact.ml`: mapping to extracted functions
- `extraction/impacted/ocaml/filtering.ml`: program for plain change impact analysis
- `extraction/impacted/ocaml/topfiltering.ml`: program for topological sorting
- `extraction/impacted/ocaml/hierarchical.ml`: program for two-level hierarchical change impact analysis
- `extraction/impacted/ocaml/util.ml`: utility functions
Key OCaml files for optimized tool:
- `extraction/impacted-rbt/ocaml/change_impact.mli`: interface to extracted code
- `extraction/impacted-rbt/ocaml/change_impact.ml`: mapping to extracted functions
- `extraction/impacted-rbt/ocaml/filtering.ml`: program for plain change impact analysis
- `extraction/impacted-rbt/ocaml/topfiltering.ml`: program for topological sorting
- `extraction/impacted-rbt/ocaml/hierarchical.ml`: program for two-level hierarchical change impact analysis
- `extraction/impacted-rbt/ocaml/util.ml`: utility functions
---