Thesis Makefile

Makefile

# config
N = 10
S = 4321
T = 20

PROBLEM_SELECTOR   = control
BENCHMARK_SELECTOR = unsat/big

# constants
CSV_HEADER = "problem,elapsed,start,end,command"
NUM_CORES  = 6
PREFIX     = $(PROBLEM_SELECTOR)-S$(S)-N$(N)-T$(T)-
EMPTY      =
SPACE      = $(EMPTY) $(EMPTY)
COMMA      = ,

# compilers and flags
CXX    = g++-4.9
CC     = gcc-4.9
MFLAGS = -j$(NUM_CORES)

# colors
RED    = "\033[31m"
GREEN  = "\033[32m"
TEAL   = "\033[36m"
BOLD   = "\033[1m"
NORMAL = "\033[22m"
CLEAR  = "\033[m"

# directories
INSTALL_DIR    = installed
SOLVERS_DIR    = $(INSTALL_DIR)/solvers
BENCH_DIR      = $(INSTALL_DIR)/benchmarks
BIN_DIR        = bin
FUZZED_DIR     = fuzzers
EXPERIMENT_DIR = experiment
PROBLEM_DIR    = $(EXPERIMENT_DIR)/problems
DATA_DIR       = $(EXPERIMENT_DIR)/data
GRAPH_DIR      = $(EXPERIMENT_DIR)/graphs

PROBLEM_SELECTORS = repeat permute reverse unprintable control

ifeq ($(filter $(PROBLEM_SELECTOR),$(PROBLEM_SELECTORS)),)
$(error \
PROBLEM_SELECTOR ($(PROBLEM_SELECTOR)) must be set to a valid value \
(i.e. one of [$(subst $(SPACE),$(COMMA)$(SPACE),$(PROBLEM_SELECTORS)])))
endif

SELECTED_PROBLEM_DIR = $(PROBLEM_DIR)/$(PROBLEM_SELECTOR)

# solvers
S3_CODE        = $(SOLVERS_DIR)/s3
CVC4_CODE      = $(SOLVERS_DIR)/cvc4
Z3STR2_CODE    = $(SOLVERS_DIR)/z3str2
Z3STR2_Z3_CODE = $(Z3STR2_CODE)/z3
Z3STR3_CODE    = $(SOLVERS_DIR)/z3str3

S3_SOLVER     = /Users/dblotsky/bin/s3
CVC4_SOLVER   = /usr/local/bin/cvc4
Z3STR2_SOLVER = /Users/dblotsky/bin/Z3-str.py
Z3STR3_SOLVER = /Users/dblotsky/bin/z3str3

S3_RESULTS     = $(DATA_DIR)/$(PREFIX)s3.csv
CVC4_RESULTS   = $(DATA_DIR)/$(PREFIX)cvc4.csv
Z3STR2_RESULTS = $(DATA_DIR)/$(PREFIX)z3str2.csv
Z3STR3_RESULTS = $(DATA_DIR)/$(PREFIX)z3str3.csv

# benchmarks
SMT20_BENCH_DIR    = $(BENCH_DIR)/kaluza-smt20
SMT25_BENCH_DIR    = $(BENCH_DIR)/kaluza-smt25
BASE_BENCH_DIR     = $(SMT25_BENCH_DIR)
SELECTED_BENCH_DIR = $(BASE_BENCH_DIR)/$(BENCHMARK_SELECTOR)

# tools
SAMPLE = $(BIN_DIR)/sample.py
TIME   = $(BIN_DIR)/timesolver.py
FUZZER = $(FUZZED_DIR)/fuzzer

# files
SOLVERS =
# SOLVERS += $(S3_SOLVER)
SOLVERS += $(CVC4_SOLVER)
SOLVERS += $(Z3STR2_SOLVER)
SOLVERS += $(Z3STR3_SOLVER)

ALL_RESULTS =
# ALL_RESULTS += $(S3_RESULTS)
ALL_RESULTS += $(CVC4_RESULTS)
ALL_RESULTS += $(Z3STR2_RESULTS)
ALL_RESULTS += $(Z3STR3_RESULTS)

RAW_PROBLEMS = $(shell find $(SELECTED_BENCH_DIR) -name *.smt2 | $(SAMPLE) $(N) $(S))

GENERATED_PROBLEMS = \
	$(foreach s,$(PROBLEM_SELECTORS),\
		$(subst .smt2,.smt20,\
			$(subst $(BASE_BENCH_DIR),$(PROBLEM_DIR)/$(s),$(RAW_PROBLEMS))) \
		$(subst .smt2,.smt25,\
			$(subst $(BASE_BENCH_DIR),$(PROBLEM_DIR)/$(s),$(RAW_PROBLEMS))))

ALL_TESTS = \
	$(subst .smt2,.test,\
		$(subst $(BASE_BENCH_DIR),$(SELECTED_PROBLEM_DIR),$(RAW_PROBLEMS)))

debug:
	python -c 'print "$(GENERATED_PROBLEMS)"'

# functions
define getproblem
	@echo $(1) "->" $(2)
	@mkdir -p $(dir $(subst $(3),$(4),$(1)))
	@$(5)
endef

define escape_slash
$(subst /,\/,$(1))
endef

# targets
all default help usage:
	@echo "Usage: don't use."

time:
	@echo "This will run for at most" `python3 -c "print($(T) * $(N))"` "seconds"

bench_smt20: $(SMT20_BENCH_DIR)
bench_smt25: $(SMT25_BENCH_DIR)

bench benchmarks: bench_smt20 bench_smt25

get_s3: $(S3_CODE)
get_cvc4: $(CVC4_CODE)
get_z3str2: $(Z3STR2_CODE)
get_z3str3: $(Z3STR3_CODE)

get code: get_s3 get_cvc4 get_z3str2 get_z3str3

install_s3: $(S3_SOLVER)
install_cvc4: $(CVC4_SOLVER)
install_z3str2: $(Z3STR2_SOLVER)
install_z3str3: $(Z3STR3_SOLVER)

# install: install_s3
install: install_cvc4 install_z3str2 install_z3str3

smoke run check: install
	@echo $(GREEN)running s3$(CLEAR)
	# $(S3_SOLVER)
	@echo $(GREEN)running cvc4$(CLEAR)
	$(CVC4_SOLVER) --version
	@echo $(GREEN)running z3str2$(CLEAR)
	$(Z3STR2_SOLVER)
	@echo $(GREEN)running z3str3$(CLEAR)
	$(Z3STR3_SOLVER) -version

problems: $(GENERATED_PROBLEMS)
test: $(ALL_TESTS)
results: $(ALL_RESULTS)

graphs:
	./bin/csv2cactus.py $(ALL_RESULTS) > \
	$(GRAPH_DIR)/$(PREFIX)cactus.svg
	./bin/csv2compare.py $(Z3STR3_RESULTS) $(CVC4_RESULTS) > \
	$(GRAPH_DIR)/$(PREFIX)z3str3-vs-cvc4.svg
	./bin/csv2compare.py $(Z3STR3_RESULTS) $(Z3STR2_RESULTS) > \
	$(GRAPH_DIR)/$(PREFIX)z3str3-vs-z3str2.svg

$(foreach s,$(PROBLEM_SELECTORS),$(PROBLEM_DIR)/$(s) ): | $(PROBLEM_DIR)

# getting benchmarks
$(INSTALL_DIR) $(BENCH_DIR) $(SOLVERS_DIR) $(PROBLEM_DIR) $(EXPERIMENT_DIR):
	mkdir -p $@

$(SMT20_BENCH_DIR): | $(BENCH_DIR)
	tar -C $(BENCH_DIR) -xvzf resources/benchmarks/kaluza.Z3str.tar.bz2
	mv $(BENCH_DIR)/kaluza.Z3str $@

$(SMT25_BENCH_DIR): | $(BENCH_DIR)
	tar -C $(BENCH_DIR) -xvzf resources/benchmarks/kaluza.smtlib25.zip
	mv $(BENCH_DIR)/kaluza.SMTLIB25 $@

# getting solvers
$(S3_CODE): | $(SOLVERS_DIR)
	unzip resources/solvers/s3/S3-source-060115.zip -d $(SOLVERS_DIR)
	mv $(SOLVERS_DIR)/S3 $@

$(CVC4_CODE): | $(SOLVERS_DIR)
	tar -C $(SOLVERS_DIR) -xvzf resources/solvers/cvc4-1.4.1-prerelease-2016-01-03.tar.gz
	mv $(SOLVERS_DIR)/cvc4-1.4.1-prerelease $@

$(Z3STR2_CODE): | $(SOLVERS_DIR)
	git clone https://github.com/z3str/Z3-str.git $@
	cd $@ && git checkout ec39964ad534d7cd604f27fc88da0221306e3dbf

$(Z3STR3_CODE): | $(SOLVERS_DIR)
	git clone https://github.com/mtrberzi/z3 $@
	cd $@ && git checkout develop

# s3 install
$(S3_SOLVER): | $(S3_CODE)
	touch $@

# cvc4 install
$(CVC4_SOLVER): | $(CVC4_CODE)
	touch $@

# z3str2 install
$(Z3STR2_SOLVER): $(Z3STR2_CODE)/Z3-str.py
	ln -s -f $(PWD)/$^ $@

$(Z3STR2_CODE)/Z3-str.py: $(Z3STR2_CODE)/str
	sed -i '' -e \
		's/^solver = ""$$/solver = "$(call escape_slash,$(PWD)/$<)"/' $@
	chmod +x $@

$(Z3STR2_CODE)/str: $(Z3STR2_Z3_CODE)/bin/external/z3
	sed -i '' -e 's/^Z3_path = $$/Z3_path = "z3"/' $(Z3STR2_CODE)/Makefile
	sed -i '' -e 's/^	CXX = g++-5$$/	CXX = $(CXX)/' $(Z3STR2_CODE)/Makefile
	cd $(Z3STR2_CODE) && $(MAKE) $(MFLAGS)

$(Z3STR2_Z3_CODE)/bin/external/z3: $(Z3STR2_Z3_CODE)/z3.patch

ifndef PATCHED
	@echo $(RED)"======="$(CLEAR)
	@echo $(RED)"if this fails because the patch is applied, run with PATCHED=1"$(CLEAR)
	@echo $(RED)"======="$(CLEAR)
	cd $(Z3STR2_Z3_CODE) && patch -Np0 < z3.patch
else
	-cd $(Z3STR2_Z3_CODE) && patch -Np0 < z3.patch
endif

	cd $(Z3STR2_Z3_CODE) && autoconf
	cd $(Z3STR2_Z3_CODE) && CXX=$(CXX) CC=$(CC) ./configure
	cd $(Z3STR2_Z3_CODE) && CXX=$(CXX) CC=$(CC) $(MAKE) $(MFLAGS)
	cd $(Z3STR2_Z3_CODE) && $(MAKE) $(MFLAGS) a

$(Z3STR2_Z3_CODE)/z3.patch: $(Z3STR2_Z3_CODE).patch
	dos2unix < $< > $@

$(Z3STR2_Z3_CODE).patch: | $(Z3STR2_Z3_CODE)

$(Z3STR2_Z3_CODE): | $(Z3STR2_CODE)
	git clone https://github.com/Z3Prover/z3.git $@
	cd $@ && git checkout 9823ee3b44815285fa028e9f1e5f300789ac9874

# z3str3 install
$(Z3STR3_SOLVER): $(SOLVERS_DIR)/z3str3/build/z3
	ln -s -f $(PWD)/$^ $@

$(SOLVERS_DIR)/z3str3/build/z3: | $(Z3STR3_CODE)
	cd $(Z3STR3_CODE) && python scripts/mk_make.py
	cd $(Z3STR3_CODE)/build && $(MAKE) $(MFLAGS)

# results
$(ALL_RESULTS): $(TIME) Makefile

$(S3_RESULTS): RUN_TESTS = $(addsuffix -s3,$(ALL_TESTS))
$(CVC4_RESULTS): RUN_TESTS = $(addsuffix -cvc4,$(ALL_TESTS))
$(Z3STR2_RESULTS): RUN_TESTS = $(addsuffix -z3str2,$(ALL_TESTS))
$(Z3STR3_RESULTS): RUN_TESTS = $(addsuffix -z3str3,$(ALL_TESTS))

# patterns
%.csv: | $(EXPERIMENT_DIR)
	@if [ -z "$(RUN_TESTS)" ]; then echo no tests; exit 1; fi
	echo $(CSV_HEADER) > $@
	$(MAKE) $(RUN_TESTS) TEST_COMMAND=$(COMMAND) CSV_FILE=$@

%.test-s3: %.smt25 $(S3_SOLVER)
	-$(TIME) $(T) "$(S3_SOLVER) -f $<" $(subst .smt25,,$<) >> $(CSV_FILE)

%.test-cvc4: %.smt25 $(CVC4_SOLVER)
	-$(TIME) $(T) "$(CVC4_SOLVER) --lang smt < $<" $(subst .smt25,,$<) >> $(CSV_FILE)

%.test-z3str2: %.smt20 $(Z3STR2_SOLVER)
	-$(TIME) $(T) "$(Z3STR2_SOLVER) -f $<" $(subst .smt20,,$<) >> $(CSV_FILE)

%.test-z3str3: %.smt25 $(Z3STR3_SOLVER)
	-$(TIME) $(T) "$(Z3STR3_SOLVER) $<" $(subst .smt25,,$<) >> $(CSV_FILE)

%.run: %.smt25 %.smt20 $(TIME)
	-$(S3_SOLVER) -f $*.smt25
	-$(CVC4_SOLVER) --lang smt < $*.smt25
	-$(Z3STR2_SOLVER) -f $*.smt20
	-$(Z3STR3_SOLVER) -T:10 $*.smt25

$(RAW_PROBLEMS): $(SMT25_BENCH_DIR) $(SMT20_BENCH_DIR)

$(PROBLEM_DIR)/repeat/%.smt20: $(SMT20_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT20_BENCH_DIR),$(PROBLEM_DIR)/repeat,\
	cp $< $@)

$(PROBLEM_DIR)/repeat/%.smt25: $(SMT25_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT25_BENCH_DIR),$(PROBLEM_DIR)/repeat,\
	cp $< $@)

$(PROBLEM_DIR)/permute/%.smt20: $(SMT20_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT20_BENCH_DIR),$(PROBLEM_DIR)/permute,\
	cp $< $@)

$(PROBLEM_DIR)/permute/%.smt25: $(SMT25_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT25_BENCH_DIR),$(PROBLEM_DIR)/permute,\
	cp $< $@)

$(PROBLEM_DIR)/reverse/%.smt20: $(SMT20_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT20_BENCH_DIR),$(PROBLEM_DIR)/reverse,\
	cp $< $@)

$(PROBLEM_DIR)/reverse/%.smt25: $(SMT25_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT25_BENCH_DIR),$(PROBLEM_DIR)/reverse,\
	cp $< $@)

$(PROBLEM_DIR)/unprintable/%.smt20: $(SMT20_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT20_BENCH_DIR),$(PROBLEM_DIR)/unprintable,\
	$(FUZZER) < $< > $@)

$(PROBLEM_DIR)/unprintable/%.smt25: $(SMT25_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT25_BENCH_DIR),$(PROBLEM_DIR)/unprintable,\
	$(FUZZER) < $< > $@)

$(PROBLEM_DIR)/control/%.smt20: $(SMT20_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT20_BENCH_DIR),$(PROBLEM_DIR)/control,\
	cp $< $@)

$(PROBLEM_DIR)/control/%.smt25: $(SMT25_BENCH_DIR)/%.smt2
	$(call getproblem,$<,$@,$(SMT25_BENCH_DIR),$(PROBLEM_DIR)/control,\
	cp $< $@)

clean:
	$(RM) -r $(PROBLEM_DIR)

nuke_bench:
	$(RM) -r $(BENCH_DIR)

nuke_solvers:
	$(RM) $(SOLVERS)
	$(RM) -r $(SOLVERS_DIR)

nuke: nuke_bench nuke_solvers

.PRECIOUS: $(GENERATED_PROBLEMS)