blob: 22f22945021574df5a992d9bb3efd54b9d19a253 (
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
|
DIR=general
BINDIR=bin
ASMDIR=asm
TESTNAMES=$(notdir $(subst .c,,$(wildcard $(DIR)/*.c)))
CCOMP=../../ccomp
ELF=$(addprefix $(DIR)/$(BINDIR)/,$(addsuffix .bin,$(TESTNAMES)))
TOK=$(addprefix $(DIR)/$(BINDIR)/,$(addsuffix .tok,$(TESTNAMES)))
ASM=$(addprefix $(DIR)/$(ASMDIR)/,$(addsuffix .s,$(TESTNAMES)))
DEBUG:=$(if $(DEBUG),"-dall",)
.PHONY: all
all: $(ELF)
nobin: $(ASM)
##
# Assembling CompCert's assembly file
##
$(DIR)/$(BINDIR)/%.bin: $(DIR)/$(ASMDIR)/%.s
@mkdir -p $(@D)
ccomp $< -o $@
##
# Compiling the C file with CompCert
##
.SECONDARY:
$(DIR)/$(ASMDIR)/%.s: $(DIR)/%.c $(CCOMP)
@mkdir -p $(@D)
ccomp $(DEBUG) -O0 -v -S $< -o $@
##
# A token (.tok) is created if the .bin (created by CompCert) yields the same
# result as the .bin.exp (created by executing the binary compiled with gcc)
##
$(DIR)/$(BINDIR)/%.tok: $(DIR)/$(BINDIR)/%.bin $(DIR)/output/%.bin.exp
@mkdir -p $(@D)
@bash check.sh $< $@
##
# Generate .bin.exp : compile with gcc, execute, store the result in .bin.exp
##
$(DIR)/output/%.bin.exp: $(DIR)/%.c
@bash generate.sh $< $@
.PHONY: FORCE
FORCE:
.PHONY: check
check: $(TOK) sort mmult
##
# A utility displaying which of the pseudo-instructions are covered in the tests
##
.PHONY: coverage
coverage: $(ASM)
bash coverage.sh $(DIR)/$(ASMDIR)
##
# Different versions of a sorting algorithm
##
.PHONY: sort
sort: FORCE
(cd sort && make compc-check)
##
# Different versions of a matrix multiply
##
.PHONY: mmult
mmult: FORCE
(cd mmult && make compc-check)
.PHONY: clean
clean:
rm -f $(DIR)/*.alloctrace
rm -f $(DIR)/*.cm
rm -f $(DIR)/*.compcert.c
rm -f $(DIR)/*.i
rm -f $(DIR)/*.light.c
rm -f $(DIR)/*.ltl
rm -f $(DIR)/*.mach
rm -f $(DIR)/*.parsed.c
rm -f $(DIR)/*.rtl.?
rm -f $(DIR)/$(ASMDIR)/*.s
rm -f $(DIR)/$(BINDIR)/*.bin
rm -f $(DIR)/$(BINDIR)/*.tok
rm -f $(DIR)/output/*.out
rm -f $(DIR)/output/*.exp
rm -rf $(DIR)/profile/
rm -f $(ELF)
|