blob: 8d9c3d6d4b59a54a2ce4ed0b9ce817b774e715e4 (
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
|
SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail
PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
SAIL_DIR ?= $(realpath ..)
export SAIL_DIR
all: platform Riscv.thy
check: $(SAIL_SRCS) main.sail Makefile
$(SAIL_DIR)/sail $(SAIL_SRCS) main.sail
_sbuild/riscv.ml: $(SAIL_SRCS) Makefile main.sail
$(SAIL_DIR)/sail -ocaml -ocaml-nobuild -o riscv $(SAIL_SRCS)
_sbuild/platform_main.native: _sbuild/riscv.ml _tags $(PLATFORM_OCAML_SRCS) Makefile
cp _tags $(PLATFORM_OCAML_SRCS) _sbuild
cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native
platform: _sbuild/platform_main.native
rm -f $@ && ln -s $^ $@
riscv_duopod_ocaml: prelude.sail riscv_duopod.sail
$(SAIL_DIR)/sail -ocaml -o $@ $^
riscv_duopod.lem: prelude.sail riscv_duopod.sail
$(SAIL_DIR)/sail -lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^
Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem
lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
riscv_extras.lem \
riscv_duopod_types.lem \
riscv_duopod.lem
riscv_duopod: riscv_duopod_ocaml Riscv_duopod.thy
Riscv.thy: riscv.lem riscv_extras.lem
lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
riscv_extras.lem \
riscv_types.lem \
riscv.lem
sed -i 's/datatype ast/datatype (plugins only: size) ast/' Riscv_types.thy
riscv.lem: $(SAIL_SRCS) Makefile
$(SAIL_DIR)/sail -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
riscv_sequential.lem: $(SAIL_SRCS) Makefile
$(SAIL_DIR)/sail -lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS)
riscvScript.sml : riscv.lem riscv_extras.lem
lem -hol -outdir . -lib ../lib/hol -lib ../src/lem_interp -lib ../src/gen_lib \
riscv_extras.lem \
riscv_types.lem \
riscv.lem
riscvTheory.uo riscvTheory.ui: riscvScript.sml
Holmake riscvTheory.uo
# we exclude prelude.sail here, most code there should move to sail lib
LOC_FILES:=$(SAIL_SRCS) main.sail
include ../etc/loc.mk
clean:
-rm -rf riscv _sbuild
-rm -f riscv.lem riscv_types.lem
-rm -f Riscv.thy Riscv_types.thy \
Riscv_extras.thy
-rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem
-rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml
-rm -f platform_main.native platform
-Holmake cleanAll
ocamlbuild -clean
|
