########################################################################## # Sail # # # # Copyright (c) 2013-2017 # # Kathyrn Gray # # Shaked Flur # # Stephen Kell # # Gabriel Kerneis # # Robert Norton-Wright # # Christopher Pulte # # Peter Sewell # # Alasdair Armstrong # # Brian Campbell # # Thomas Bauereiss # # Anthony Fox # # Jon French # # Dominic Mulligan # # Stephen Kell # # Mark Wassell # # # # All rights reserved. # # # # This software was developed by the University of Cambridge Computer # # Laboratory as part of the Rigorous Engineering of Mainstream Systems # # (REMS) project, funded by EPSRC grant EP/K008528/1. # # # # Redistribution and use in source and binary forms, with or without # # modification, are permitted provided that the following conditions # # are met: # # 1. Redistributions of source code must retain the above copyright # # notice, this list of conditions and the following disclaimer. # # 2. Redistributions in binary form must reproduce the above copyright # # notice, this list of conditions and the following disclaimer in # # the documentation and/or other materials provided with the # # distribution. # # # # THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' # # AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED # # TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A # # PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR # # CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, # # SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT # # LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF # # USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND # # ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, # # OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT # # OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF # # SUCH DAMAGE. # ########################################################################## THIS_MAKEFILE := $(lastword $(MAKEFILE_LIST)) # NOTE: it matters that this path is *not* canonicalised (realpath'd). # If we realpath it, the ocaml deps files will include realpaths, and # make won't know they're the same CMX files that we're building. So # will not correctly merge dependency subgraphs, and we will not build # stuff in the right order. # In general, the lesson is that the whole system needs to use the same # path, whether absolute or relative, to name a given file. # Sometimes that's difficult. Rules which cd to another directory break # if we're using absolute paths. I have used $(realpath $(srcdir)) in # those cases. This is not ideal. We shouldn't cd unless we really have to. srcdir := $(dir $(THIS_MAKEFILE)) $(warning srcdir is $(srcdir)) BITSTRING ?= $(srcdir)/contrib/bitstring BATTERIES ?= $(srcdir)/contrib/batteries-included/_build/src UINT ?= $(srcdir)/contrib/ocaml-uint/_build/lib export CAML_LD_LIBRARY_PATH := $(BITSTRING) $(CAML_LD_LIBRARY_PATH) LEM ?= ~/bitbucket/lem/lem LEMLIB ?= ~/bitbucket/lem/ocaml-lib/_build/ OCAMLFLAGS += -I $(LEMLIB) # FIXME .PHONY: all sail test clean doc lib power test_power test_idempotence contrib install_elf all: sail lib doc full: all power test test sail: sail.native sail_lib.cma sail_lib.cmxa interpreter: _build/lem_interp/extract.cmxa _build/lem_interp/extract.cma sail.native sail_lib.cma sail_lib.cmxa: ocamlbuild sail.native sail_lib.cma sail_lib.cmxa _build/lem_interp/extract.cmxa: ocamlbuild lem_interp/extract.cmxa _build/lem_interp/extract.cma: ocamlbuild lem_interp/extract.cma test: sail interpreter ocamlbuild test/run_tests.native ./run_tests.native contrib: cd contrib && ./checkout.sh install_elf: cp -p ../../system-v-abi/src/*.lem elf_model/ cp -p ../../system-v-abi/src/*.ml elf_model/ %.ml: %.lem $(LEM) -outdir $$(dirname "$<") -ocaml -only_changed_output "$<" # HACK: special case for bitstring_local elf_model/bitstring_local.ml: elf_model/bitstring.lem $(LEM) -outdir $$(dirname "$<") -ocaml -only_changed_output "$<" ELF_LEM_SRC := $(addprefix elf_model/,missing_pervasives.lem show.lem endianness.lem bitstring.lem elf_types.lem elf_interpreted_segment.lem elf_header.lem elf_file1.lem elf_program_header_table.lem elf_executable_file2.lem elf_section_header_table.lem elf_executable_file3.lem string_table.lem elf_executable_file4.lem elf_executable_file5.lem sail_interface.lem main.lem) vpath _build/%.lem . vpath _build/%.cmx . CAMLP4FLAGS += -nolib CAMLP4FLAGS += -I $(srcdir)/contrib/$(BITSTRING) CAMLP4FLAGS += -parser o -parser op -printer p CAMLP4FLAGS += unix.cma CAMLP4FLAGS += bitstring.cma CAMLP4FLAGS += bitstring_persistent.cma CAMLP4FLAGS += pa_bitstring.cmo # HACK: rewrite for bitstring_local ELF_ML_LEM := $(filter-out elf_model/bitstring.ml,$(patsubst %.lem,%.ml,$(ELF_LEM_SRC))) elf_model/bitstring_local.ml ELF_ML_SRC := $(addprefix elf_model/,error.ml ml_bindings.ml) ELF_ML := $(ELF_ML_SRC) $(ELF_ML_LEM) ELF_ML_DEPS := $(patsubst %.ml,%.d,$(ELF_ML)) ELF_CMX := $(patsubst %.ml,%.cmx,$(ELF_ML)) $(ELF_CMX): OCAMLFLAGS += \ -I $(BITSTRING) -pp 'env CAML_LD_LIBRARY_PATH=$(BITSTRING) camlp4o $(CAMLP4FLAGS)' \ -I $(BATTERIES) \ -I $(UINT) \ -I $(srcdir)/elf_model $(ELF_ML_DEPS): OCAMLFLAGS += \ -I $(BITSTRING) -pp 'env CAML_LD_LIBRARY_PATH=$(BITSTRING) camlp4o $(CAMLP4FLAGS)' \ -I $(BATTERIES) \ -I $(UINT) \ -I $(srcdir)/elf_model $(ELF_ML_DEPS): %.d: %.ml ocamldep -native $(OCAMLFLAGS) "$<" > "$@" || (rm -f "$@"; false) ifneq ($(MAKECMDGOALS),clean) include $(ELF_ML_DEPS) endif elf_extract.cmxa: OCAMLFLAGS += \ -I $(BITSTRING) -package bitstring,bitstring.syntax -syntax bitstring \ -I $(BATTERIES) -package batteries \ -I $(UINT) -package bitstring \ -pp 'camlp4 $(CAMLP4FLAGS)' \ -I $(LEMLIB)/../ocaml-lib/_build LEM_CMX := $(addprefix $(LEMLIB)/../ocaml-lib/,nat_num.cmx lem.cmx lem_function.cmx lem_list.cmx) %.cmx: %.ml echo CAML_LD_LIBRARY_PATH is $$CAML_LD_LIBRARY_PATH ocamlopt $(OCAMLFLAGS) -c "$<" elf_model/elf_extract.cmxa: $(ELF_CMX) ocamlopt $(OCAMLFLAGS) -a -o "$@" $+ elf: $(ELF_CMX) $(LEM_CMX) elf_model/elf_extract.cmxa _build/test/power.lem: sail.native test/power.sail mkdir -p _build/test cp -p test/* _build/test/ cd _build/test && \ ../../sail.native -lem_ast power.sail pprint/src/_build/PPrintLib.cmxa: $(MAKE) -C $(srcdir)/pprint/src _build/test/run_power.native: OCAMLFLAGS += \ -I $(LEMLIB) \ -I $(srcdir)/_build/lem_interp/ \ -I $(srcdir)/elf_model/ \ -I $(UINT) _build/test/run_power.native: OCAMLLIBS += \ $(LEMLIB)/extract.cmxa _build/test/power.ml: _build/test/power.lem cd _build/test && $(LEM) -ocaml -only_changed_output -lib $(realpath $(srcdir))/lem_interp/ power.lem touch "$@" # HACK HACK HACK! why didn't lem update the timestamp? _build/test/run_power.native: pprint/src/_build/PPrintLib.cmxa _build/lem_interp/extract.cmxa elf_model/elf_extract.cmxa _build/test/power.ml test/run_power.ml cd _build/test && \ ocamlopt $(OCAMLFLAGS) $(OCAMLLIBS) -I $(realpath $(srcdir))/_build/lem_interp $(addprefix $(realpath $(srcdir))/,$+) -o run_power.native power: run_power.native run_power.native: _build/test/run_power.native ln -fs _build/test/run_power.native run_power.native test_power: power ./run_power.native --file ../../../rsem/idl/power/binary/main.bin test_power_interactive: power ./run_power.native --interactive --file ../../../rsem/idl/power/binary/main.bin test_power_interactive_srcs: ebig ~/rsem/idl/power/generated/power.sail ../../../rsem/idl/power/binary/hello.c ../../../rsem/idl/power/binary/hello.s # or test/power.sail for cut-down one test_idempotence: sail @cd test; for file in *.sail; do \ ./idempotence.sh $$file; echo ;\ done clean: #-ocamlbuild -clean -rm -rf _build *.native -rm -rf $(srcdir)/elf_model/*.o $(srcdir)/elf_model/*.cmx $(srcdir)/elf_model/*.cmi $(ELF_ML_LEM) $(ELF_ML_DEPS) -rm -rf html-doc -rm -rf tex-doc -rm -rf lem lib -rm -rf sail.docdir doc: ocamlbuild sail.docdir/index.html lib: ocamlbuild pretty_print.cmxa pretty_print.cma