Skip to content
Permalink
Browse files

Addition of hooks in makefiles for benchmarking ulib, examples/micro-…

…benchmarks and ocaml-output extract
  • Loading branch information
ctk21 committed Jun 27, 2019
1 parent 00201d8 commit 21694b917dd98418775fa799136818704490fc95
Showing with 70 additions and 0 deletions.
  1. +1 −0 .gitignore
  2. +6 −0 examples/Makefile.include
  3. +7 −0 src/Makefile.boot
  4. +3 −0 ulib/Makefile
  5. +31 −0 ulib/Makefile.verify
  6. +22 −0 ulib/gmake/fstar.mk
@@ -8,6 +8,7 @@
*.sav
*.hints.fsval
*.hints.mlval
*.bench
dump*
cache/
/VS/packages
@@ -14,8 +14,14 @@ else
MSBUILD = $(shell which msbuild || (echo '\n\n\033[0;31mWarning:\033[0m could not find "msbuild", trying (deprecated) "xbuild"\n\n'>&2; which xbuild))
endif

# we ignore the return result in benchmark runs because we can have micro-benchmarks which
# produce error asserts when executed with '--admit_smt_queries true'
%.uver: %.fst
ifdef BENCHMARK_FSTAR
-$(BENCHMARK_CMD) -o $@.bench -- $(FSTAR) --use_extracted_interfaces true $^
else
$(FSTAR) --use_extracted_interfaces true $^
endif

%.fail-uver: %.fst
(! $(FSTAR) $^ >/dev/null 2>&1) || (echo "NEGATIVE TEST FAILED ($@)!" ; false)
@@ -69,9 +69,16 @@ EXTRACT = $(addprefix --extract_module , $(EXTRACT_MODULES)) \
# And then, in a separate invocation, from each .checked.lax we
# extract an .ml file
ocaml-output/%.ml:
ifdef BENCHMARK_FSTAR
$(BENCHMARK_CMD) -o $@.bench -- \
$(FSTAR_C) $(notdir $(subst .checked.lax,,$<)) \
--codegen OCaml \
--extract_module $(basename $(notdir $(subst .checked.lax,,$<)))
else
$(FSTAR_C) $(notdir $(subst .checked.lax,,$<)) \
--codegen OCaml \
--extract_module $(basename $(notdir $(subst .checked.lax,,$<)))
endif

# --------------------------------------------------------------------
# Dependency analysis for bootstrapping
@@ -9,6 +9,9 @@ FSTAR_HOME=..
all:
+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-core

benchmark:
+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-benchmark

extra:
+$(MAKE) FSTAR_HOME=$(FSTAR_HOME) -f Makefile.verify verify-extra

@@ -34,3 +34,34 @@ LowStar.Printf.fst.checked: USE_EXTRACTED_INTERFACES=
verify-core: $(addsuffix .checked, $(filter-out $(EXTRA) ,$(FSTAR_FILES)))

verify-extra: $(addsuffix .checked, $(EXTRA))

# Benchmarking rules
#
# we want to run FStar with just the target file as that being checked
# ideally all the .checked files will exist and we will:
# - move them to the side
# - execute the benchmark
# - move the checked file back
#

# a.fst.bench will move the a.fst.checked binary and then move it back
%.fst.bench: %.fst
-mv -f $*.fst.checked $*.fst.checked.bench_bkp
ifdef BENCHMARK_FSTAR
$(BENCHMARK_CMD) -o $@ -- $(MY_FSTAR) $*.fst
else
$(MY_FSTAR) $*.fst
endif
-mv -f $*.fst.checked.bench_bkp $*.fst.checked

# a.fsti.bench will move the a.fsti.checked binary and then move it back
%.fsti.bench: %.fsti
-mv -f $*.fsti.checked $*.fsti.checked.bench_bkp
ifdef BENCHMARK_FSTAR
$(BENCHMARK_CMD) -o $@ -- $(MY_FSTAR) $*.fsti
else
$(MY_FSTAR) $*.fsti
endif
-mv -f $*.fsti.checked.bench_bkp $*.fsti.checked

verify-benchmark: $(addsuffix .bench, $(filter-out $(EXTRA) ,$(FSTAR_FILES)))
@@ -14,3 +14,25 @@ else
# FSTAR_HOME not defined, assume fstar.exe reachable from PATH
FSTAR=fstar.exe $(OTHERFLAGS) $(HINTS_ENABLED)
endif

# Benchmarking wrappers are enabled when you pass BENCHMARK_FSTAR=true, for example:
# make -C examples/micro-benchmarks BENCHMARK_FSTAR=true
# make -C ulib benchmark BENCHMARK_FSTAR=true BENCHMARK_CMD='perf stat -x,'
#
# This will utilize the BENCHMARK_CMD wrapper to collect data on the commands executed
#
# BENCHMARK_CMD can be set to a wrapper command that works when called as follows:
# $BENCHMARK_CMD -o <output-file> -- <program-to-benchmark> <arguments-to-program>
#
# For example Linux perf stat or strace:
# BENCHMARK_CMD=perf stat -x,
# BENCHMARK_CMD=strace
#
# or GNU time:
# BENCHMARK_CMD=time
#
# or the orun OCaml benchmarking program which will include GC stats and available at:
# https://github.com/ocaml-bench/sandmark/tree/master/orun
# BENCHMARK_CMD=orun
#
BENCHMARK_CMD?=time

0 comments on commit 21694b9

Please sign in to comment.
You can’t perform that action at this time.