diff options
Diffstat (limited to 'src/Makefile')
| -rw-r--r-- | src/Makefile | 56 |
1 files changed, 36 insertions, 20 deletions
diff --git a/src/Makefile b/src/Makefile index deb30108..abf03c4f 100644 --- a/src/Makefile +++ b/src/Makefile @@ -48,7 +48,7 @@ # SUCH DAMAGE. # ########################################################################## -.PHONY: all sail test clean doc lib power test_power test_idempotence +.PHONY: all sail sail.native sail.byte test clean doc lib power test_power test_idempotence # set to -p on command line to enable gprof profiling OCAML_OPTS?= @@ -57,15 +57,21 @@ all: sail lib doc full: sail lib power doc test -sail: - ocamlbuild sail.native sail_lib.cma sail_lib.cmxa +ast.ml: ../language/l2.ott + ott -sort false -generate_aux_rules true -o ast.ml -picky_multiple_parses true ../language/l2.ott + +lem_interp/interp_ast.lem: ../language/l2.ott + ott -sort false -generate_aux_rules true -o lem_interp/interp_ast.lem -picky_multiple_parses true ../language/l2.ott + +sail: ast.ml + ocamlbuild sail.native sail.native: sail -sail.byte: +sail.byte: ocamlbuild -cflag -g sail.byte -interpreter: +interpreter: lem_interp/interp_ast.lem ocamlbuild lem_interp/extract.cmxa ocamlbuild lem_interp/extract.cma @@ -74,32 +80,34 @@ test: sail interpreter ./run_tests.native THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) +SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..) BITBUCKET_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..) LEM = $(BITBUCKET_ROOT)/lem/lem LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib ELFDIR= $(BITBUCKET_ROOT)/linksem ZARITH_DIR=$(LEMLIBOCAML)/dependencies/zarith -ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa +ZARITH_LIB=$(ZARITH_DIR)/zarith.cma +# ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa -SAIL_DIR:=$(BITBUCKET_ROOT)/sail -MIPS_SAIL_DIR:=$(SAIL_DIR)/mips +SAIL_LIB_DIR:=$(SAIL_DIR)/lib +MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc -MIPS_SAILS_PRE:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +MIPS_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail MIPS_SAILS:=$(MIPS_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail -MIPS_NOTLB_SAILS_PRE:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +MIPS_NOTLB_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail CHERI_SAIL_DIR:=$(SAIL_DIR)/cheri -CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_NOTLB_SAILS:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_SAILS:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI128_SAILS:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail elf: make -C $(ELFDIR) @@ -132,10 +140,14 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native cd _build ;\ ../sail.native -lem_ast -o mips $(MIPS_SAILS) -_build/mips_embed_types.lem: $(MIPS_SAILS) ./sail.native +_build/mips_embed_types.lem: $(MIPS_NOTLB_SAILS) ./sail.native mkdir -p _build cd _build ;\ - ../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS) + ../sail.native -lem_lib "Mips_extras_embed" -lem -lem_mwords -o mips $(MIPS_NOTLB_SAILS) + +_build/Mips_embed.thy: _build/mips_embed_types.lem + cd _build ;\ + lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed.lem mips_embed_types.lem mips_embed.lem _build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native mkdir -p _build @@ -177,14 +189,14 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native cd _build ;\ ../sail.native -lem_ast -o cheri_notlb $(CHERI_NOTLB_SAILS) -_build/cheri_embed_types.lem: $(CHERI_SAILS) ./sail.native +_build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native mkdir -p _build cd _build ;\ - ../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS) + ../sail.native -lem_lib "Mips_extras_embed" -lem -lem_sequential -lem_mwords -o cheri $(CHERI_SAILS) -_build/Cheri_embed_sequential.thy: _build/cheri_embed_types.lem +_build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem cd _build ;\ - lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem ../../mips/mips_extras_embed_sequential.lem cheri_embed_types.lem cheri_embed_sequential.lem + lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem _build/mips_all.sail: $(MIPS_SAILS) cat $(MIPS_SAILS) > $@ @@ -201,8 +213,11 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail %.ml: %.lem $(LEM) -only_changed_output -ocaml -lib lem_interp/ $< +#run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter +# env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native + run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native + env OCAMLRUNPARAM=l=100M ocamlfind ocamlc $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cma $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cma $(ELFDIR)/src/linksem.cma _build/pprint/src/PPrintLib.cma _build/lem_interp/extract.cma _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native @@ -241,6 +256,7 @@ clean: -rm -rf tex-doc -rm -rf lem lib -rm -rf sail.docdir + -rm -f ast.ml doc: ocamlbuild sail.docdir/index.html |