Makefile.extr

#######################################################################
#                                                                     #
#              The Compcert verified compiler                         #
#                                                                     #
#          Xavier Leroy, INRIA Paris-Rocquencourt                     #
#                                                                     #
#  Copyright Institut National de Recherche en Informatique et en     #
#  Automatique.  All rights reserved.  This file is distributed       #
#  under the terms of the GNU General Public License as published by  #
#  the Free Software Foundation, either version 2 of the License, or  #
#  (at your option) any later version.  This file is also distributed #
#  under the terms of the INRIA Non-Commercial License Agreement.     #
#                                                                     #
#######################################################################

# Second-stage Makefile, after Coq extraction

include Makefile.config

# Directories containing plain Caml code (no preprocessing)

DIRS=extraction \
  lib common $(ARCH) backend cfrontend cparser driver \
  exportclight

# Directories containing Caml code that must be preprocessed by Camlp4

ifeq ($(CCHECKLINK),true)
DIRS_P4=checklink
else
DIRS_P4=
endif

ALLDIRS=$(DIRS) $(DIRS_P4)

INCLUDES=$(patsubst %,-I %, $(ALLDIRS))

# Control of warnings:
# warning 3 = deprecated feature.  Turned off for OCaml 4.02 (bytes vs strings)
# warning 20 = unused function argument.  There are some in extracted code

WARNINGS=-w -3
extraction/%.cmx: WARNINGS +=-w -20
extraction/%.cmo: WARNINGS +=-w -20

COMPFLAGS=-g $(INCLUDES) $(WARNINGS)

# Using the bitstring library and syntax extension (for checklink)

BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o

# Using .opt compilers if available

ifeq ($(OCAML_OPT_COMP),true)
DOTOPT=.opt
else
DOTOPT=
endif

# Compilers used for non-preprocessed code

OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS)
OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS)
OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES)

# Compilers used for Camlp4-preprocessed code.  Note that we cannot
# use the .opt compilers (because ocamlfind doesn't support them).

OCAMLC_P4=ocamlfind ocamlc $(COMPFLAGS) $(BITSTRING)
OCAMLOPT_P4=ocamlfind ocamlopt $(COMPFLAGS) $(BITSTRING)
OCAMLDEP_P4=ocamlfind ocamldep $(INCLUDES) $(BITSTRING)

MENHIR=menhir --explain
OCAMLLEX=ocamllex -q
MODORDER=tools/modorder .depend.extr

PARSERS=backend/CMparser.mly cparser/pre_parser.mly
LEXERS=backend/CMlexer.mll cparser/Lexer.mll \
       lib/Tokenize.mll lib/Readconfig.mll

LIBS=str.cmxa unix.cmxa
CHECKLINK_LIBS=str.cmxa

EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml)

# Beginning of part that assumes .depend.extr already exists

ifeq ($(wildcard .depend.extr),.depend.extr)

CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)

ccomp: $(CCOMP_OBJS)
	@echo "Linking $@"
	@$(OCAMLOPT) -o $@ $(LIBS) $+

ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
	@echo "Linking $@"
	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+

ifeq ($(CCHECKLINK),true)

CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx)

cchecklink: $(CCHECKLINK_OBJS)
	@echo "Linking $@"
	@$(OCAMLOPT_P4) -linkpkg -o $@ $(CHECKLINK_LIBS) $+

cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo)
	@echo "Linking $@"
	@$(OCAMLC_P4) -linkpkg -o $@ $(CHECKLINK_LIBS:.cmxa=.cma) $+

endif

CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx)

clightgen: $(CLIGHTGEN_OBJS)
	@echo "Linking $@"
	@$(OCAMLOPT) -o $@ $(LIBS) $+

clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
	@echo "Linking $@"
	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+

include .depend.extr

endif

# End of part that assumes .depend.extr already exists

checklink/%.cmi: checklink/%.mli
	@echo "OCAMLC   $<"
	@$(OCAMLC_P4) -c $<
checklink/%.cmo: checklink/%.ml
	@echo "OCAMLC   $<"
	@$(OCAMLC_P4) -c $<
checklink/%.cmx: checklink/%.ml
	@echo "OCAMLOPT $<"
	@$(OCAMLOPT_P4) -c $<

%.cmi: %.mli
	@echo "OCAMLC   $<"
	@$(OCAMLC) -c $<
%.cmo: %.ml
	@echo "OCAMLC   $<"
	@$(OCAMLC) -c $<
%.cmx: %.ml
	@echo "OCAMLOPT $<"
	@$(OCAMLOPT) -c $<

%.ml %.mli: %.mly
	$(MENHIR) $<
%.ml: %.mll
	$(OCAMLLEX) $<

clean:
	rm -f $(EXECUTABLES)
	rm -f $(GENERATED)
	for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done

# Generation of .depend.extr

depend: $(GENERATED)
	@echo "Analyzing OCaml dependencies"
	@$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli $(d)/*.ml)) >.depend.extr
	@$(OCAMLDEP) $(GENERATED) >> .depend.extr
ifneq ($(strip $(DIRS_P4)),)
	@$(OCAMLDEP_P4) $(foreach d,$(DIRS_P4),$(wildcard $(d)/*.mli $(d)/*.ml)) >>.depend.extr
endif