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 Lesser General Public License as        #
#  published by the Free Software Foundation, either version 2.1 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

#
# Variables from Makefile.config:
# -OCAML_NATIVE_COMP: native-code compilation is supported
# -OCAML_OPT_COMP: can we use the natively-compiled compilers
# -COMPFLAGS: compile options
# -LINK_OPT: additional linker flags for the native binary
#

# Menhir configuration.

include Makefile.menhir

#
# Variables from Makefile.menhir:
# -MENHIR_INCLUDES: additional menhir include paths
# -MENHIR_LIBS: additional menhir libraries
#

# The pre-parser's error message database is compiled as follows.

# cparser/pre_parser_messages.ml:
#	$(MAKE) -C cparser correct

# Directories containing plain Caml code

DIRS=extraction \
  lib common $(ARCH) cfrontend cparser driver $(shell find VPL/ocaml/src -type d ! -name extracted ! -name smt)

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

# Control of warnings:
# See: https://v2.ocaml.org/manual/toplevel.html
WARNINGS=-w +a-4-8-9-26-27-29-32-33-34-37-39-40-42-44-50-66-69-70
extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67

# Turn warnings into errors, but not for released tarballs
ifeq ($(wildcard .git),.git)
# WARN_ERRORS=-warn-error +a
else
WARN_ERRORS=
endif

COMPFLAGS+=-g -strict-sequence -safe-string -package zarith \
  $(INCLUDES) -I "$(MENHIR_DIR)" -I +str -I +unix -I +zarith \
  $(WARNINGS) $(WARN_ERRORS)

# Using .opt compilers if available

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

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

OCAMLLEX=ocamllex -q
MODORDER=tools/modorder .depend.extr
COPY=cp

PARSERS=lib/OpenScopParser.mly VPL/ocaml/src/lin/poly/PolyParser.mly
LEXERS=lib/Tokenize.mll \
	     lib/Readconfig.mll lib/Responsefile.mll lib/OpenScopLexer.mll VPL/ocaml/src/lin/poly/PolyLexer.mll \

LIBS=str.cmxa unix.cmxa zarith.cmxa $(MENHIR_LIBS)
LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS)))

EXECUTABLES=polcert polcert.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/Entry.cmx)

ifeq ($(OCAML_NATIVE_COMP),true)
polcert: $(CCOMP_OBJS)
	@echo "Linking $@"
	@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
else
polcert: polcert.byte
	@echo "Copying to $@"
	@$(COPY) $+ $@
endif

polcert.byte: $(CCOMP_OBJS:.cmx=.cmo)
	@echo "Linking $@"
	@$(OCAMLC) -o $@ $(LIBS_BYTE) $+

CLIGHTGEN_OBJS:=$(shell $(MODORDER) export/ExportDriver.cmx)

ifeq ($(OCAML_NATIVE_COMP),true)
clightgen: $(CLIGHTGEN_OBJS)
	@echo "Linking $@"
	@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
else
clightgen: clightgen.byte
	@echo "Copying to $@"
	@$(COPY) $+ $@
endif

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

include .depend.extr

endif

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

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

%.ml: %.mll
	$(OCAMLLEX) $<

clean:
	rm -f $(EXECUTABLES)
	rm -f $(GENERATED)
	for d in $(DIRS); do rm -f $$d/*.cm[iotx] $$d/*cmti $$d/*.o; done
# $(MAKE) -C cparser clean

# Generation of .depend.extr

depend: $(GENERATED)
	@echo "Analyzing OCaml dependencies"
	@$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.ml)) $(GENERATED) >.depend.extr || { rm -f .depend.extr; exit 2; }
	@$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli)) $(GENERATED) >>.depend.extr || { rm -f .depend.extr; exit 2; }