-
Notifications
You must be signed in to change notification settings - Fork 4
/
Makefile
142 lines (121 loc) · 5.08 KB
/
Makefile
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
134
135
136
137
138
139
140
141
142
SEMANTICS_DIR = semantics
SCRIPTS_DIR = scripts
PARSER_DIR = parser
PARSER = $(PARSER_DIR)/cparser
DIST_DIR = dist
#svnversion
export C_K_BASE ?= $(K_BASE)
# this should be defined by the user
# K_MAUDE_BASE ?= .
#OUTPUT_FILTER_DIR = $(K_MAUDE_BASE)/tools/OutputFilter
#OUTPUT_FILTER ?= $(OUTPUT_FILTER_DIR)/filterOutput
#FILTER = $(SEMANTICS_DIR)/outputFilter.yml
#VPATH = programs
#FILES_TO_DIST = \
$(K_BASE)/core/java/wrapperAndServer.jar \
$(K_BASE)/core/java/jopt-simple-3.3.jar \
$(SEMANTICS_DIR)/cu-total.maude \
$(SEMANTICS_DIR)/cu-total-nd.maude \
$(wildcard $(SCRIPTS_DIR)/*.sql) \
$(SCRIPTS_DIR)/accessProfiling.pl \
$(SCRIPTS_DIR)/link.pl \
$(SCRIPTS_DIR)/wrapper.pl \
$(SCRIPTS_DIR)/compile.pl \
$(SCRIPTS_DIR)/xmlToK.pl \
$(SCRIPTS_DIR)/graphSearch.pl \
$(SCRIPTS_DIR)/programRunner.pl \
$(SCRIPTS_DIR)/analyzeProfile.pl \
$(PARSER_DIR)/cparser \
$(wildcard $(SEMANTICS_DIR)/includes/*) \
$(wildcard $(SEMANTICS_DIR)/lib/*)
FILES_TO_DIST = \
$(K_BASE)/core/java/wrapperAndServer.jar \
$(K_BASE)/core/java/jopt-simple-3.3.jar \
$(SEMANTICS_DIR)/cu-total.maude \
$(wildcard $(SCRIPTS_DIR)/*.sql) \
$(SCRIPTS_DIR)/accessProfiling.pl \
$(SCRIPTS_DIR)/link.pl \
$(SCRIPTS_DIR)/wrapper.pl \
$(SCRIPTS_DIR)/compile.pl \
$(SCRIPTS_DIR)/xmlToK.pl \
$(SCRIPTS_DIR)/graphSearch.pl \
$(SCRIPTS_DIR)/programRunner.pl \
$(SCRIPTS_DIR)/analyzeProfile.pl \
$(PARSER_DIR)/cparser \
$(wildcard $(SEMANTICS_DIR)/includes/*) \
$(wildcard $(SEMANTICS_DIR)/lib/*)
.PHONY: all clean run test force cparser maude-fragments build-all dynamic match fix semantics gcc-output benchmark dist fast-test dist-make check-input
all: WHICH_SEMANTICS="semantics"
all: dist
fast: WHICH_SEMANTICS="fast"
fast: dist
# nd: WHICH_SEMANTICS="nd"
# nd: dist
check-vars:
ifeq ($(C_K_BASE),)
@echo "ERROR: Please set K_BASE to the full path of your K installation."
@echo "Make sure you do NOT include a trailing slash\\"
@echo "One way to do this is to type 'export K_BASE=/path/to/k/framework', and then rerun 'make'"
@exit 1
endif
@if ! ocaml -version > /dev/null 2>&1; then echo "ERROR: You don't seem to have ocaml installed. You need to install this before continuing. Please see the README for more information."; false; fi
@if ! gcc -v > /dev/null 2>&1; then echo "ERROR: You don't seem to have gcc installed. You need to install this before continuing. Please see the README for more information."; false; fi
@if ! maude --version > /dev/null 2>&1; then echo "ERROR: You don't seem to have maude installed. You need to install this before continuing. Please see the README for more information."; false; fi
@perl $(SCRIPTS_DIR)/checkForModules.pl
dist: check-vars $(DIST_DIR)/dist.done
pdf: check-vars
@$(MAKE) -C $(SEMANTICS_DIR) pdf
$(K_BASE)/core/java/wrapperAndServer.jar: $(wildcard $(K_BASE)/core/java/IOServer/src/*/*.java) $(wildcard $(K_BASE)/core/java/Wrapper/src/*/*.java) $(K_BASE)/core/java/Wrapper/Manifest.txt
@$(MAKE) -C $(K_BASE)/core/java
$(DIST_DIR)/dist.done: check-vars Makefile cparser semantics $(FILES_TO_DIST)
@mkdir -p $(DIST_DIR)
@mkdir -p $(DIST_DIR)/includes
@mkdir -p $(DIST_DIR)/lib
@cp $(FILES_TO_DIST) $(DIST_DIR)
@mv $(DIST_DIR)/*.h $(DIST_DIR)/includes
@mv $(DIST_DIR)/*.c $(DIST_DIR)/lib
@mv $(DIST_DIR)/compile.pl $(DIST_DIR)/cudak
@echo "Compiling the standard library..."
@echo compiling clib
@$(DIST_DIR)/cudak -c -o $(DIST_DIR)/lib/clib.o $(DIST_DIR)/lib/clib.c
@echo compiling ctype
@$(DIST_DIR)/cudak -c -o $(DIST_DIR)/lib/ctype.o $(DIST_DIR)/lib/ctype.c
@echo compiling math
@$(DIST_DIR)/cudak -c -o $(DIST_DIR)/lib/math.o $(DIST_DIR)/lib/math.c
@echo compiling stdio
@$(DIST_DIR)/cudak -c -o $(DIST_DIR)/lib/stdio.o $(DIST_DIR)/lib/stdio.c
@echo compiling stdlib
@$(DIST_DIR)/cudak -c -o $(DIST_DIR)/lib/stdlib.o $(DIST_DIR)/lib/stdlib.c
@echo compiling string
@$(DIST_DIR)/cudak -c -o $(DIST_DIR)/lib/string.o $(DIST_DIR)/lib/string.c
@echo "Done."
@echo "Testing cudak..."
@perl $(SCRIPTS_DIR)/testInstall.pl $(DIST_DIR)/cudak $(DIST_DIR)/testProgram.c $(DIST_DIR)/testProgram.compiled
@echo "Done."
@echo "Calibrating the semantic profiler..."
# done so that an empty file gets copied by the analyzeProfile.pl wrapper
@mv maudeProfileDBfile.sqlite maudeProfileDBfile.sqlite.calibration.bak > /dev/null 2>&1 || true
@touch maudeProfileDBfile.sqlite
@perl $(SCRIPTS_DIR)/initializeProfiler.pl $(SEMANTICS_DIR)/cu-total.maude
@mv maudeProfileDBfile.sqlite $(DIST_DIR)/maudeProfileDBfile.calibration.sqlite
@mv maudeProfileDBfile.sqlite.calibration.bak maudeProfileDBfile.sqlite > /dev/null 2>&1 || true
@echo "Done."
@echo "Cleaning up..."
@rm -f $(DIST_DIR)/testProgram.c
@rm -f $(DIST_DIR)/testProgram.compiled
@echo "Done."
@touch $(DIST_DIR)/dist.done
# test: dist
# @$(MAKE) -C tests
force: ;
cparser:
@$(MAKE) -C $(PARSER_DIR)
@-strip $(PARSER)
semantics: check-vars
#@rm -f $(SEMANTICS_DIR)/cu-total-nd.maude
@$(MAKE) $(WHICH_SEMANTICS) -C $(SEMANTICS_DIR)
clean:
$(MAKE) -C $(PARSER_DIR) clean
$(MAKE) -C $(SEMANTICS_DIR) clean
rm -rf $(DIST_DIR)
rm -f ./*.tmp ./*.log ./*.cil ./*-gen.maude ./*.gen.maude ./*.pre.gen ./*.prepre.gen ./a.out ./*.kdump ./*.pre.pre