add previously packaged files

.gitignore

@@ -0,0 +1,7 @@
+*.vo
+*.glob
+*.v.d
+*.aux
+Makefile.coq
+Makefile.coq.conf
+.coqdeps.d

Makefile

@@ -0,0 +1,42 @@
+IMPACTEDML = extraction/impacted/ocaml/impacted.ml extraction/impacted/ocaml/impacted.mli
+IMPACTEDRBTML = extraction/impacted-rbt/ocaml/impacted_rbt.ml extraction/impacted-rbt/ocaml/impacted_rbt.mli
+
+all: default
+
+default: Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+quick: Makefile.coq
+	$(MAKE) -f Makefile.coq quick
+
+install: Makefile.coq
+	$(MAKE) -f Makefile.coq install
+
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq cleanall
+	rm -f Makefile.coq Makefile.coq.conf
+	$(MAKE) -C extraction/impacted clean
+	$(MAKE) -C extraction/impacted-rbt clean
+
+impacted:
+	+$(MAKE) -C extraction/impacted filtering.native filteringinv.native topfiltering.native
+
+impacted-rbt:
+	+$(MAKE) -C extraction/impacted-rbt filtering.native filteringinv.native topfiltering.native
+
+Makefile.coq: _CoqProject
+	coq_makefile -f _CoqProject -o Makefile.coq \
+	  -extra '$(IMPACTEDML)' \
+	    'extraction/impacted/coq/extract_impacted.v core/finn.vo' \
+	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) extraction/impacted/coq/extract_impacted.v' \
+	  -extra '$(IMPACTEDRBTML)' \
+	    'extraction/impacted-rbt/coq/extract_impacted_rbt.v core/finn_set.vo' \
+	    '$$(COQC) $$(COQDEBUG) $$(COQFLAGS) extraction/impacted-rbt/coq/extract_impacted_rbt.v'
+
+$(IMPACTEDML) $(IMPACTEDRBTML): Makefile.coq
+	$(MAKE) -f Makefile.coq $@
+
+.PHONY: all default quick clean impacted $(IMPACTEDML) $(IMPACTEDRBTML)
+
+.NOTPARALLEL: $(IMPACTEDML)
+.NOTPARALLEL: $(IMPACTEDRBTML)

README.md

@@ -0,0 +1,87 @@
+Change Impact Analysis in Coq and OCaml
+=======================================
+
+A basic requirement is to install [OPAM](http://opam.ocaml.org/doc/Install.html).
+
+Then create an OPAM switch for OCaml 4.06.1:
+```
+opam update
+opam switch 4.06.1
+eval `opam config env`
+```
+
+Building the Coq development
+----------------------------
+
+First install the requirements:
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam pin add coq 8.8.1
+opam pin add coq-mathcomp-ssreflect 1.7.0
+opam install coq-mathcomp-fingroup
+```
+
+Then run:
+```
+make
+```
+This will build the whole project and check all the proofs.
+
+Building the Chip tool
+----------------------
+
+First install the Coq requirements as above. Then install the OCaml requirements:
+```
+opam install ocamlbuild yojson extlib
+```
+
+To build regular Chip, run
+```
+make impacted
+```
+To then try the tool, go to `extraction/impacted` and run:
+```
+./filtering.native test/new.json test/old.json
+```
+
+To build Chip with red-black trees, run:
+```
+make impacted-rbt
+```
+and look in `extraction/impacted-rbt`.
+
+Coq files
+---------
+
+Adapted and extended from work by [Cohen and Thery](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
+
+Adapted from work by [Nanevski et al.](https://github.com/imdea-software/fcsl-pcm):
+
+- `core/ordtype.v`: ordered type definition for the Mathematical Components library
+
+Core definitions and lemmas:
+
+- `core/closure.v`: basic definition of transitive closures of sets
+- `core/run.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/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
+
+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/run_seq.v`: sequence-based change impact analysis definitions, optimized topological sorting using impact analysis
+- `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

_CoqProject

@@ -0,0 +1,29 @@
+-Q core chip
+-Q extraction/impacted/coq chip
+-Q extraction/impacted-rbt/coq chip
+-arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
+core/extra.v
+core/connect.v
+core/acyclic.v
+core/closure.v
+core/closure_example.v
+core/tarjan.v
+core/kosaraju.v
+core/kosaraju_acyclic.v
+core/tarjan_acyclic.v
+core/change.v
+core/run.v
+core/string.v
+core/finn.v
+core/finn_set.v
+core/run_seq.v
+core/topos.v
+core/ordtype.v
+core/dfs_set.v
+core/close_dfs.v
+core/hierarchical.v
+core/hierarchical_correct.v
+core/hierarchical_sub.v
+core/hierarchical_sub_correct.v
+extraction/impacted/coq/extract_impacted.v
+extraction/impacted-rbt/coq/extract_impacted_rbt.v