Reorganized the development, modularizing away machine-dependent parts.

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 40 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index 58d494c..c2ffceb 100644
--- a/Makefile
+++ b/Makefile
@@ -15,20 +15,31 @@ include Makefile.config
 COQC=coqc $(INCLUDES)
 COQDEP=coqdep $(INCLUDES)
 COQDOC=coqdoc
+OCAMLBUILD=ocamlbuild
+OCB_OPTIONS=\
+  -no-hygiene \
+  -I extraction $(INCLUDES) \
+  -cflags -I,`pwd`/cil/obj/$(ARCHOS) \
+  -lflags -I,`pwd`/cil/obj/$(ARCHOS) \
+  -libs unix,str,cil
 
-INCLUDES=-I lib -I common -I backend -I cfrontend
+DIRS=lib common $(ARCH)/$(VARIANT) $(ARCH) backend cfrontend driver
 
-# Files in lib/
+VPATH=$(DIRS)
+GPATH=$(DIRS)
+INCLUDES=$(patsubst %,-I %, $(DIRS))
+
+# General-purpose libraries (in lib/)
 
 LIB=Coqlib.v Maps.v Lattice.v Ordered.v \
   Iteration.v Integers.v Floats.v Parmov.v
 
-# Files in common/
+# Parts common to the front-ends and the back-end (in common/)
 
 COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \
-  Smallstep.v Switch.v Main.v Complements.v
+  Smallstep.v Switch.v
 
-# Files in backend/
+# Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT))
 
 BACKEND=\
   Cminor.v Op.v CminorSel.v \
@@ -39,7 +50,7 @@ BACKEND=\
   Kildall.v \
   Constprop.v Constpropproof.v \
   CSE.v CSEproof.v \
-  Locations.v Conventions.v LTL.v LTLtyping.v \
+  Machregs.v Locations.v Conventions.v LTL.v LTLtyping.v \
   InterfGraph.v Coloring.v Coloringproof.v \
   Allocation.v Allocproof.v Alloctyping.v \
   Tunneling.v Tunnelingproof.v Tunnelingtyping.v \
@@ -48,29 +59,34 @@ BACKEND=\
   Linear.v Lineartyping.v \
   Parallelmove.v Reload.v Reloadproof.v Reloadtyping.v \
   Mach.v Machabstr.v Machtyping.v \
-  Bounds.v Stacking.v Stackingproof.v Stackingtyping.v \
+  Bounds.v Stacklayout.v Stacking.v Stackingproof.v Stackingtyping.v \
   Machconcr.v Machabstr2concr.v \
-  PPC.v PPCgen.v PPCgenretaddr.v PPCgenproof1.v PPCgenproof.v
+  Asm.v Asmgen.v Asmgenretaddr.v Asmgenproof1.v Asmgenproof.v
 
-# Files in cfrontend/
+# C front-end modules (in cfrontend/)
 
 CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \
   Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v \
   Csharpminor.v Cminorgen.v Cminorgenproof.v
 
-# All source files
+# Putting everything together (in driver/)
+
+DRIVER=Compiler.v Complements.v
 
-FILES=$(LIB:%=lib/%) $(COMMON:%=common/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%)
+# All source files
 
-FLATFILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND)
+FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER)
 
 proof: $(FILES:.v=.vo)
 
+exec:
+	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native && mv Driver.native ccomp
+
 all:
 	$(MAKE) proof
 	$(MAKE) -C cil
-	$(MAKE) -C extraction extraction
-	$(MAKE) -C extraction depend
+	$(MAKE) -C extraction
+	$(MAKE) exec
 	$(MAKE) -C extraction
 	$(MAKE) -C runtime
 
@@ -78,8 +94,8 @@ documentation: doc/removeproofs
 	@ln -f $(FILES) doc/
 	@mkdir -p doc/html
 	cd doc; $(COQDOC) --html -d html \
-          $(FLATFILES:%.v=--glob-from %.glob) $(FLATFILES)
-	@cd doc; rm -f $(FLATFILES)
+          $(FILES:%.v=--glob-from %.glob) $(FILES)
+	@cd doc; rm -f $(FILES)
 	cp doc/coqdoc.css doc/html/coqdoc.css
 	doc/removeproofs doc/html/*.html
 
@@ -100,14 +116,19 @@ latexdoc:
 	@$(COQC) -dump-glob doc/$(*F).glob $*.v
 
 depend:
-	$(COQDEP) $(FILES) > .depend
+	$(COQDEP) $(patsubst %, %/*.v, $(DIRS)) \
+        | sed -e 's|$(ARCH)/$(VARIANT)/|$$(ARCH)/$$(VARIANT)/|g' \
+              -e 's|$(ARCH)/|$$(ARCH)/|g' \
+        > .depend
 
 install:
-	$(MAKE) -C extraction install
+	install -d $(BINDIR)
+	install ../ccomp $(BINDIR)
 	$(MAKE) -C runtime install
 
 clean:
-	rm -f */*.vo *~ */*~
+	rm -f $(patsubst %, %/*.vo, $(DIRS))
+	rm -rf _build
 	rm -rf doc/html doc/*.glob
 	rm -f doc/removeproofs.ml doc/removeproofs
 	$(MAKE) -C extraction clean