diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 80 |
1 files changed, 68 insertions, 12 deletions
@@ -22,22 +22,30 @@ TAG ?= $(tag) BRANCH ?= $(branch) ifeq ($(wildcard $(ARCH)_$(BITSIZE)),) -ARCHDIRS=$(ARCH) +ARCHDIRS?=$(ARCH) else -ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +ARCHDIRS?=$(ARCH)_$(BITSIZE) $(ARCH) endif -DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser +BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v -COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d)) +DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \ + exportclight cparser + +RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \ + cparser + +COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d)) ifeq ($(LIBRARY_FLOCQ),local) DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 +RECDIRS += flocq COQINCLUDES += -R flocq Flocq endif ifeq ($(LIBRARY_MENHIRLIB),local) DIRS += MenhirLib +RECDIRS += MenhirLib COQINCLUDES += -R MenhirLib MenhirLib endif @@ -87,9 +95,12 @@ endif # General-purpose libraries (in lib/) 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/) @@ -101,7 +112,7 @@ COMMON=Errors.v AST.v Linking.v \ # Back-end modules (in backend/, $(ARCH)/) BACKEND=\ - Cminor.v Cminortyping.v Op.v CminorSel.v \ + Cminor.v Cminortyping.v Op.v CminorSel.v OpHelpers.v OpHelpersproof.v \ SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \ SelectOpproof.v SelectDivproof.v SplitLongproof.v \ SelectLongproof.v Selectionproof.v \ @@ -109,16 +120,28 @@ BACKEND=\ RTLgen.v RTLgenspec.v RTLgenproof.v \ Tailcall.v Tailcallproof.v \ Inlining.v Inliningspec.v Inliningproof.v \ + Profiling.v Profilingproof.v \ + ProfilingExploit.v ProfilingExploitproof.v \ Renumber.v Renumberproof.v \ + Duplicate.v Duplicateproof.v Duplicatepasses.v \ RTLtyping.v \ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ + Inject.v Injectproof.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ + CSE2deps.v CSE2depsproof.v \ + CSE2.v CSE2proof.v \ + CSE3analysis.v CSE3analysisproof.v CSE3.v CSE3proof.v \ + KillUselessMoves.v KillUselessMovesproof.v \ + LICM.v LICMproof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ - Allocation.v Allocproof.v \ + ForwardMoves.v ForwardMovesproof.v \ + FirstNop.v FirstNopproof.v \ + Allnontrap.v Allnontrapproof.v \ + Allocation.v Allocationproof.v \ Tunneling.v Tunnelingproof.v \ Linear.v Lineartyping.v \ Linearize.v Linearizeproof.v \ @@ -126,7 +149,16 @@ BACKEND=\ Debugvar.v Debugvarproof.v \ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ - Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v + Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ + RTLpathSE_simplify.v \ + $(BACKENDLIB) + +SCHEDULING= \ + RTLpathLivegenproof.v RTLpathSE_simu_specs.v \ + RTLpathLivegen.v RTLpathSE_impl.v \ + RTLpathproof.v RTLpathSE_theory.v \ + RTLpathSchedulerproof.v RTLpath.v \ + RTLpathScheduler.v RTLpathWFcheck.v # C front-end modules (in cfrontend/) @@ -157,7 +189,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 @@ -172,6 +204,7 @@ all: $(MAKE) proof $(MAKE) extraction $(MAKE) ccomp + $(MAKE) ccomp.byte ifeq ($(HAS_RUNTIME_LIB),true) $(MAKE) runtime endif @@ -202,6 +235,10 @@ ccomp: .depend.extr compcert.ini driver/Version.ml FORCE ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr ccomp.byte +# DM force compilation without checking dependencies +ccomp.force: .depend.extr compcert.ini driver/Version.ml FORCE + $(MAKE) -f Makefile.extr ccomp.force + clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE @@ -227,6 +264,13 @@ else ocamlc -o tools/ndfun str.cma tools/ndfun.ml endif +tools/compiler_expand: tools/compiler_expand.ml +ifeq ($(OCAML_NATIVE_COMP),true) + ocamlopt -o $@ $+ +else + ocamlc -o $@ $+ +endif + tools/modorder: tools/modorder.ml ifeq ($(OCAML_NATIVE_COMP),true) ocamlopt -o tools/modorder str.cmxa tools/modorder.ml @@ -248,6 +292,18 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod a-w $*.v +# this trick aims to allow extraction to depend on the target processor +# (currently: export extra Coq-functions for OCaml code, depending on the target) +extraction/extraction.v: Makefile extraction/extraction.vexpand + (echo "(* WARNING: this file is generated from extraction.vexpand *)"; \ + echo "(* by the Makefile -- target \"extraction/extraction.v\" *)"; \ + cat extraction/extraction.vexpand; \ + echo "$(EXTRA_EXTRACTION)"; \ + echo ".") > extraction/extraction.v + +driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand + tools/compiler_expand driver/Compiler.vexpand $@ + compcert.ini: Makefile.config (echo "stdlib_path=$(LIBDIR)"; \ echo "prepro=$(CPREPRO)"; \ @@ -325,10 +381,10 @@ clean: rm -f $(patsubst %, %/*.vo*, $(DIRS)) rm -f $(patsubst %, %/.*.aux, $(DIRS)) rm -rf doc/html doc/*.glob - rm -f driver/Version.ml + rm -f driver/Version.ml driver/Compiler.v rm -f compcert.ini compcert.config - rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr - rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o + rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr extraction/extraction.v + rm -f tools/ndfun tools/modorder tools/compiler_expand tools/*.cm? tools/*.o rm -f $(GENERATED) .depend rm -f .lia.cache $(MAKE) -f Makefile.extr clean |