blob: fb71396d985789654700605709085fa55312ad49 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
.PHONY: all sail test clean doc lib power test_power test_idempotence
all: sail lib doc
full: sail lib power doc test
sail:
ocamlbuild sail.native sail_lib.cma sail_lib.cmxa
sail.native: sail
sail.byte:
ocamlbuild -cflag -g sail.byte
interpreter:
ocamlbuild lem_interp/extract.cmxa
ocamlbuild lem_interp/extract.cma
test: sail interpreter
ocamlbuild test/run_tests.native
./run_tests.native
THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
BITBUCKET_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..)
LEM = $(BITBUCKET_ROOT)/lem/lem
LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
ELFDIR= $(BITBUCKET_ROOT)/linksem
MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/mips
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:=$(MIPS_SAILS_PRE) $(BITBUCKET_ROOT)/sail/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:=$(MIPS_NOTLB_SAILS_PRE) $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude.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_prelude.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)
_build/mips_extras.lem: ../mips/mips_extras.lem
mkdir -p _build
cp $< $@
_build/run_with_elf.ml: lem_interp/run_with_elf.ml
mkdir -p _build
cp $< $@
_build/run_with_elf_cheri.ml: lem_interp/run_with_elf_cheri.ml
mkdir -p _build
cp $< $@
_build/mips.lem: $(MIPS_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
../sail.native -lem_ast -o mips $(MIPS_SAILS)
_build/mips_embed_types.lem: $(MIPS_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS)
_build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
mkdir -p _build
cd _build ; \
../sail.native -lem_ast -o mips_notlb $(MIPS_NOTLB_SAILS)
_build/cheri.lem: $(CHERI_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
../sail.native -lem_ast -o cheri $(CHERI_SAILS)
_build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
../sail.native -lem_ast -o cheri_notlb $(CHERI_NOTLB_SAILS)
_build/cheri_embed_types.lem: $(CHERI_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS)
_build/Cheri_embed_sequential.thy: _build/cheri_embed_types.lem
cd _build ;\
lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem ../../mips/mips_extras_embed_sequential.lem cheri_embed_sequential.lem
_build/mips_all.sail: $(MIPS_SAILS)
cat $(MIPS_SAILS) > $@
_build/cheri_all.sail: $(CHERI_SAILS)
cat $(CHERI_SAILS) > $@
_build/%_trimmed.sail: _build/%_all.sail
grep -v -e '^\s*$$' $< > $@
count: _build/cheri_trimmed.sail _build/mips_trimmed.sail
wc -l $^
%.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 -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(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_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(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
mips_notlb: _build/mips_notlb.ml _build/mips_embed_types.lem _build/mips_extras.ml
true
mips: elf run_mips.native
cheri: elf run_cheri.native
clean:
-ocamlbuild -clean
-rm -rf _build *.native
-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
|
