diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 85 |
1 files changed, 71 insertions, 14 deletions
@@ -23,22 +23,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 export cparser +BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v -COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d)) +DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \ + export 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 @@ -98,9 +106,13 @@ 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 \ + OptionMonad.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/) @@ -112,7 +124,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 \ @@ -120,24 +132,44 @@ 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 \ - Tunneling.v Tunnelingproof.v \ + ForwardMoves.v ForwardMovesproof.v \ + FirstNop.v FirstNopproof.v \ + Allnontrap.v Allnontrapproof.v \ + Allocation.v Allocationproof.v \ + LTLTunneling.v LTLTunnelingproof.v \ + RTLTunneling.v RTLTunnelingproof.v \ Linear.v Lineartyping.v \ Linearize.v Linearizeproof.v \ CleanupLabels.v CleanupLabelsproof.v \ 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 \ + BTL_SEsimplify.v \ + $(BACKENDLIB) + +SCHEDULING= \ + BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ + BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v\ + BTL_SEtheory.v BTL_SEsimuref.v BTL_SEimpl.v # C front-end modules (in cfrontend/) @@ -176,7 +208,7 @@ endif # All source files -FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ +FILES=$(VLIB) $(COMMON) $(BACKEND) $(SCHEDULING) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ $(MENHIRLIB) $(PARSER) $(EXPORTLIB) # Generated source files @@ -191,6 +223,7 @@ all: $(MAKE) proof $(MAKE) extraction $(MAKE) ccomp + $(MAKE) ccomp.byte ifeq ($(HAS_RUNTIME_LIB),true) $(MAKE) runtime endif @@ -221,6 +254,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 driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen clightgen.byte: .depend.extr compcert.ini driver/Version.ml FORCE @@ -246,6 +283,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 @@ -267,6 +311,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)"; \ @@ -277,6 +333,7 @@ compcert.ini: Makefile.config echo "linker_options=$(CLINKER_OPTIONS)";\ echo "arch=$(ARCH)"; \ echo "model=$(MODEL)"; \ + echo "os=$(OS)"; \ echo "abi=$(ABI)"; \ echo "endianness=$(ENDIANNESS)"; \ echo "system=$(SYSTEM)"; \ @@ -344,10 +401,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 @@ -362,7 +419,7 @@ check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." check-proof: $(FILES) - $(COQCHK) compcert.driver.Complements + $(COQCHK) -o compcert.driver.Complements print-includes: @echo $(COQINCLUDES) |