blob: 6e3ef49efdf918679656bf38dc5ee391dc5e0ae8 (
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
|
THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..)
export SAIL_DIR
SAIL_LIB_DIR:=$(SAIL_DIR)/lib
MIPS_SAIL_DIR:=$(SAIL_DIR)/mips
SAIL:=$(SAIL_DIR)/sail
MIPS_PRE:=$(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail
MIPS_TLB:=$(MIPS_SAIL_DIR)/mips_tlb.sail
MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail
MIPS_SAILS:=$(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_MAIN:=$(MIPS_SAIL_DIR)/main.sail
mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
$(SAIL) -ocaml -o mips -memo_z3 $^
mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
$(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^
mips_no_tlb_types.lem: mips_no_tlb.lem
# TODO: Use monomorphisation so that we can switch to machine words
mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
$(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen -memo_z3 $^
mips_types.lem: mips.lem
M%.thy: m%.lem m%_types.lem mips_extras.lem
lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy
LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
include ../etc/loc.mk
cloc: $(LOC_FILES)
cloc --by-file --force-lang C,sail $^
clean:
rm -rf mips Mips.thy mips.lem _sbuild
|
