vericuda/Makefile at main · neelsomani/vericuda · GitHub

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
PYTHON ?= python3
RUSTC ?= rustc

MIR_DUMP_DIR ?= mir_dump
SAXPY_SRC := examples/saxpy.rs
ATOMIC_SRC := examples/atomic_flag.rs
REDUCTION_SRC := examples/reduction.rs

COQ_DIR := coq
PTX_DIR := target
SAXPY_PTX := $(PTX_DIR)/saxpy.ptx
ATOMIC_PTX := $(PTX_DIR)/atomic_flag.ptx
REDUCTION_PTX := $(PTX_DIR)/reduction.ptx

.PHONY: demo translate mir-saxpy mir-atomic mir-reduction ptx check-ptx translator-test translator-validation coq

demo: translate translator-test check-ptx translator-validation coq

translate: mir-saxpy mir-atomic mir-reduction
	@SAXPY_MIR=`ls -t $(MIR_DUMP_DIR)/saxpy.saxpy.*.PreCodegen.after.mir 2>/dev/null | head -n 1`; \
	if [ -z "$$SAXPY_MIR" ]; then \
	  echo "error: no saxpy PreCodegen MIR dump found" >&2; \
	  exit 1; \
	fi; \
	$(PYTHON) tools/mir2coq.py $$SAXPY_MIR coq/examples/saxpy_gen.v
	@ATOMIC_MIR=`ls -t $(MIR_DUMP_DIR)/atomic_flag.acquire_release.*.PreCodegen.after.mir 2>/dev/null | head -n 1`; \
	if [ -z "$$ATOMIC_MIR" ]; then \
	  echo "error: no atomic_flag PreCodegen MIR dump found" >&2; \
	  exit 1; \
	fi; \
	$(PYTHON) tools/mir2coq.py $$ATOMIC_MIR coq/examples/atomic_flag_gen.v
	@REDUCTION_MIR=`ls -t $(MIR_DUMP_DIR)/reduction.reduction.*.PreCodegen.after.mir 2>/dev/null | head -n 1`; \
	if [ -z "$$REDUCTION_MIR" ]; then \
	  echo "error: no reduction PreCodegen MIR dump found" >&2; \
	  exit 1; \
	fi; \
	$(PYTHON) tools/mir2coq.py --shared-param _1 \
	  $$REDUCTION_MIR coq/examples/reduction_gen.v

mir-saxpy:
	@mkdir -p $(MIR_DUMP_DIR)
	RUSTFLAGS="-Zunstable-options" $(RUSTC) --crate-type=lib -Z dump-mir=all $(SAXPY_SRC)

mir-atomic:
	@mkdir -p $(MIR_DUMP_DIR)
	RUSTFLAGS="-Zunstable-options" $(RUSTC) --crate-type=lib -Z dump-mir=all $(ATOMIC_SRC)

mir-reduction:
	@mkdir -p $(MIR_DUMP_DIR)
	RUSTFLAGS="-Zunstable-options" $(RUSTC) --crate-type=lib -Z dump-mir=all $(REDUCTION_SRC)

ptx:
	@mkdir -p $(PTX_DIR)
	$(RUSTC) --crate-type=lib --target nvptx64-nvidia-cuda \
		-C link-dead-code=yes -O --emit=asm $(SAXPY_SRC) -o $(SAXPY_PTX)
	$(RUSTC) --crate-type=lib --target nvptx64-nvidia-cuda \
		-C target-cpu=sm_70 -C link-dead-code=yes -O --emit=asm \
		$(ATOMIC_SRC) -o $(ATOMIC_PTX)
	$(RUSTC) --crate-type=lib --target nvptx64-nvidia-cuda \
		-C target-cpu=sm_70 -C link-dead-code=yes -O --emit=asm \
		$(REDUCTION_SRC) -o $(REDUCTION_PTX)

check-ptx: translate ptx tools/check_ptx.sh
	tools/check_ptx.sh

translator-test:
	$(PYTHON) tools/test_mir2coq.py

coq: translate
	$(MAKE) -C $(COQ_DIR) all

translator-validation: examples/atomic_bad.rs tools/mir2coq.py
	@mkdir -p $(MIR_DUMP_DIR)
	RUSTFLAGS="-Zunstable-options" $(RUSTC) --crate-type=lib -Z dump-mir=all examples/atomic_bad.rs
	@BAD_MIR=`ls -t $(MIR_DUMP_DIR)/atomic_bad.*.PreCodegen.after.mir 2>/dev/null | head -n 1`; \
	if [ -z "$$BAD_MIR" ]; then \
	  echo "error: no atomic_bad PreCodegen MIR dump found" >&2; exit 1; \
	fi; \
	if $(PYTHON) tools/mir2coq.py $$BAD_MIR coq/examples/atomic_bad_gen.v; then \
	  echo "ERROR: translator accepted an unsupported atomic ordering"; \
	  rm -f coq/examples/atomic_bad_gen.v; \
	  exit 1; \
	else \
	  echo "[ok] translator input validation rejected unsupported atomic orderings"; \
	fi
	@rm -f coq/examples/atomic_bad_gen.v