diff options
| -rw-r--r-- | Makefile | 17 | ||||
| -rw-r--r-- | Makefile.extr | 2 | ||||
| -rwxr-xr-x | configure | 1 | ||||
| -rw-r--r-- | scheduling/InstructionScheduler.ml (renamed from kvx/InstructionScheduler.ml) | 0 | ||||
| -rw-r--r-- | scheduling/InstructionScheduler.mli (renamed from kvx/InstructionScheduler.mli) | 0 | ||||
| -rw-r--r-- | scheduling/PrepassSchedulingOracle.ml (renamed from kvx/lib/PrepassSchedulingOracle.ml) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpath.v (renamed from kvx/lib/RTLpath.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathLivegen.v (renamed from kvx/lib/RTLpathLivegen.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathLivegenaux.ml (renamed from kvx/lib/RTLpathLivegenaux.ml) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathLivegenproof.v (renamed from kvx/lib/RTLpathLivegenproof.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_impl.v (renamed from kvx/lib/RTLpathSE_impl.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_impl_junk.v (renamed from kvx/lib/RTLpathSE_impl_junk.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_theory.v (renamed from kvx/lib/RTLpathSE_theory.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathScheduler.v (renamed from kvx/lib/RTLpathScheduler.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathScheduleraux.ml (renamed from kvx/lib/RTLpathScheduleraux.ml) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathSchedulerproof.v (renamed from kvx/lib/RTLpathSchedulerproof.v) | 0 | ||||
| -rw-r--r-- | scheduling/RTLpathproof.v (renamed from kvx/lib/RTLpathproof.v) | 0 |
17 files changed, 15 insertions, 5 deletions
@@ -23,11 +23,11 @@ endif BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v -DIRS=lib lib/Impure common $(ARCHDIRS) backend cfrontend driver \ +DIRS=lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \ flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ exportclight MenhirLib cparser -RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ +RECDIRS=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \ MenhirLib cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) $(subst /,.,compcert.$(d))) @@ -60,7 +60,9 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ HashedSet.v \ Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ - Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v + Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v \ + ImpConfig.v ImpExtern.v ImpIO.v ImpMonads.v \ + ImpCore.v ImpHCons.v ImpLoops.v ImpPrelude.v # Parts common to the front-ends and the back-end (in common/) @@ -111,6 +113,13 @@ BACKEND=\ Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ $(BACKENDLIB) +SCHEDULING= \ + RTLpathLivegenproof.v RTLpathSE_impl_junk.v \ + RTLpathLivegen.v RTLpathSE_impl.v \ + RTLpathproof.v RTLpathSE_theory.v \ + RTLpathSchedulerproof.v RTLpath.v \ + RTLpathScheduler.v + # C front-end modules (in cfrontend/) CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ @@ -136,7 +145,7 @@ DRIVER=Compopts.v Compiler.v Complements.v # All source files -FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ +FILES=$(VLIB) $(COMMON) $(BACKEND) $(SCHEDULING) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ $(MENHIRLIB) $(PARSER) # Generated source files diff --git a/Makefile.extr b/Makefile.extr index 5e328a4c..1a894a16 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -42,7 +42,7 @@ cparser/pre_parser_messages.ml: # Directories containing plain Caml code DIRS=extraction \ - lib common $(ARCH) backend cfrontend cparser driver \ + lib common $(ARCH) scheduling backend cfrontend cparser driver \ exportclight debug kvx/unittest lib/Impure/ocaml \ kvx/lib @@ -689,6 +689,7 @@ echo "-R lib compcert.lib \ -R common compcert.common \ -R ${arch} compcert.${arch} \ -R backend compcert.backend \ +-R scheduling compcert.scheduling \ -R cfrontend compcert.cfrontend \ -R driver compcert.driver \ -R flocq compcert.flocq \ diff --git a/kvx/InstructionScheduler.ml b/scheduling/InstructionScheduler.ml index eab0b21a..eab0b21a 100644 --- a/kvx/InstructionScheduler.ml +++ b/scheduling/InstructionScheduler.ml diff --git a/kvx/InstructionScheduler.mli b/scheduling/InstructionScheduler.mli index 85e2a5c6..85e2a5c6 100644 --- a/kvx/InstructionScheduler.mli +++ b/scheduling/InstructionScheduler.mli diff --git a/kvx/lib/PrepassSchedulingOracle.ml b/scheduling/PrepassSchedulingOracle.ml index 78961310..78961310 100644 --- a/kvx/lib/PrepassSchedulingOracle.ml +++ b/scheduling/PrepassSchedulingOracle.ml diff --git a/kvx/lib/RTLpath.v b/scheduling/RTLpath.v index 82991a4d..82991a4d 100644 --- a/kvx/lib/RTLpath.v +++ b/scheduling/RTLpath.v diff --git a/kvx/lib/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v index 1f0ebe3c..1f0ebe3c 100644 --- a/kvx/lib/RTLpathLivegen.v +++ b/scheduling/RTLpathLivegen.v diff --git a/kvx/lib/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml index dd971db8..dd971db8 100644 --- a/kvx/lib/RTLpathLivegenaux.ml +++ b/scheduling/RTLpathLivegenaux.ml diff --git a/kvx/lib/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v index 0ba5ed44..0ba5ed44 100644 --- a/kvx/lib/RTLpathLivegenproof.v +++ b/scheduling/RTLpathLivegenproof.v diff --git a/kvx/lib/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index afc9785e..afc9785e 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/scheduling/RTLpathSE_impl_junk.v index 1b4efad7..1b4efad7 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/scheduling/RTLpathSE_impl_junk.v diff --git a/kvx/lib/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v index 5002b7c5..5002b7c5 100644 --- a/kvx/lib/RTLpathSE_theory.v +++ b/scheduling/RTLpathSE_theory.v diff --git a/kvx/lib/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index b70c1685..b70c1685 100644 --- a/kvx/lib/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v diff --git a/kvx/lib/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index 88f777a5..88f777a5 100644 --- a/kvx/lib/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml diff --git a/kvx/lib/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v index 5c32847e..5c32847e 100644 --- a/kvx/lib/RTLpathSchedulerproof.v +++ b/scheduling/RTLpathSchedulerproof.v diff --git a/kvx/lib/RTLpathproof.v b/scheduling/RTLpathproof.v index 20eded97..20eded97 100644 --- a/kvx/lib/RTLpathproof.v +++ b/scheduling/RTLpathproof.v |