@ -10,11 +10,14 @@ CLANG_ARGS?=-O0
SLEDGE_DBG = $( CURDIR) /../_build/debug/cli/sledge_cli.exe
SLEDGE_DBG = $( CURDIR) /../_build/debug/cli/sledge_cli.exe
SLEDGE_OPT = $( CURDIR) /../_build/release/cli/sledge_cli.exe
SLEDGE_OPT = $( CURDIR) /../_build/release/cli/sledge_cli.exe
# additional arguments to pass to sledge
# additional arguments to pass to sledge translate, disassemble, analyze, and smt
SLEDGE_ARGS ?= -bound 5
SLEDGE_T_ARGS ?=
SLEDGE_D_ARGS ?=
SLEDGE_A_ARGS ?= -bound 5
SLEDGE_S_ARGS ?=
# limits for each test run
# limits for each test run
TIMEOUT ?= 100
TIMEOUT ?= 3 00
MEMOUT ?= 4096
MEMOUT ?= 4096
sledge_dbg = ./wrap.sh $( TIMEOUT) $( MEMOUT) $( SLEDGE_DBG)
sledge_dbg = ./wrap.sh $( TIMEOUT) $( MEMOUT) $( SLEDGE_DBG)
@ -34,25 +37,25 @@ export LANG := C
default : test
default : test
# compile c to llvm bitcode
# compile c to llvm bitcode
%.bc : %.c
%.bc : %.c $( CURDIR ) /../model /llair_intrinsics .h
@ ( cd $( @D) && clang -g -c -emit-llvm -include $( CURDIR) /../model/llair_intrinsics.h -Wno-main-return-type $( CLANG_ARGS) -o $( @F) $( <F) )
( cd $( @D) && clang -g -c -emit-llvm -include $( CURDIR) /../model/llair_intrinsics.h -Wno-main-return-type $( CLANG_ARGS) -o $( @F) $( <F) )
# compile c++ to llvm bitcode
# compile c++ to llvm bitcode
%.bc : %.cpp
%.bc : %.cpp
@ ( cd $( @D) && clang++ -g -c -emit-llvm $( CLANG_ARGS) -o $( @F) $( <F) )
( cd $( @D) && clang++ -g -c -emit-llvm $( CLANG_ARGS) -o $( @F) $( <F) )
# disassemble bitcode to llvm assembly
# disassemble bitcode to llvm assembly
%.ll : %.bc
%.ll : %.bc
@ ( cd $( @D) && llvm-dis -show-annotations -o $( @F) $( <F) )
( cd $( @D) && llvm-dis -show-annotations -o $( @F) $( <F) )
%.bllair : %.bc
%.bllair : %.bc
$( SLEDGE_DBG) llvm translate $< -output $@
$( SLEDGE_DBG) llvm translate $< -output $@
%.llair : %.bc
%.llair : %.bc
$( SLEDGE_DBG) llvm disassemble -no-models -no-internalize $< -llair-output $@
$( SLEDGE_DBG) llvm disassemble $< -llair-output $@
%.llair : %.ll
%.llair : %.ll
$( SLEDGE_DBG) llvm disassemble -no-models -no-internalize $< -llair-output $@
$( SLEDGE_DBG) llvm disassemble $< -llair-output $@
# code to test sledge translate
# code to test sledge translate
TranslateCs := $( shell find -L { ,local/} translate -name '*.c' 2>/dev/null)
TranslateCs := $( shell find -L { ,local/} translate -name '*.c' 2>/dev/null)
@ -85,21 +88,20 @@ compile: $(GeneratedBCs)
# run sledge llvm translate tests
# run sledge llvm translate tests
.PHONY : translate
.PHONY : translate
translate : compile
translate : compile
-@ parallel --bar $( sledge_dbg) llvm disassemble -no-models -no-internalize $( SLEDGE_ARGS) ::: $( TranslateTests)
-parallel --bar $( sledge_dbg) llvm disassemble $( SLEDGE_D _ARGS) ::: $( TranslateTests)
.PHONY : translate .sexp
.PHONY : translate .sexp
translate.sexp :
translate.sexp :
@find -L { ,local/,extra/} translate -not -path 'baseline/*' -name '*.sexp' 2>/dev/null \
find -L { ,local/,extra/} translate -not -path 'baseline/*' -name '*.sexp' 2>/dev/null | xargs cat > translate.sexp
| xargs cat > translate.sexp
baseline/translate.sexp : translate .sexp
baseline/translate.sexp : translate .sexp
@ cp translate.sexp $@
cp translate.sexp $@
translate.html : translate .sexp
translate.html : translate .sexp
@ $( sledge_report) html -baseline baseline/translate.sexp translate.sexp -output $@
$( sledge_report) html -baseline baseline/translate.sexp translate.sexp -output $@
translate-status : translate .sexp
translate-status : translate .sexp
@ $( sledge_report) status -baseline baseline/translate.sexp translate.sexp | column -ts$$ '\t'
$( sledge_report) status -baseline baseline/translate.sexp translate.sexp | column -ts$$ '\t'
#
#
# analyze (backend) tests
# analyze (backend) tests
@ -108,35 +110,34 @@ translate-status: translate.sexp
# run analyze tests
# run analyze tests
.PHONY : analyze
.PHONY : analyze
analyze : compile
analyze : compile
-@ parallel --bar $( sledge_dbg) llvm analyze -trace Report+Control $( SLEDGE_ARGS) ::: $( AnalyzeTests)
-parallel --bar $( sledge_dbg) llvm analyze -trace Report+Control $( SLEDGE_A _ARGS) ::: $( AnalyzeTests)
parallel_sledge_opt = parallel --shuf --bar $( sledge_opt) llvm analyze -append-report $( SLEDGE_ARGS) :::
parallel_sledge_opt = parallel --use-cores-instead-of-threads -- shuf --bar $( sledge_opt) llvm analyze -append-report $( SLEDGE_A _ARGS) :::
analyze-perf1 : compile
analyze-perf1 : compile
@$( parallel_sledge_opt) $( AnalyzeTests)
- @$( parallel_sledge_opt) $( AnalyzeTests)
analyze-perf3 : compile
analyze-perf3 : compile
@$( parallel_sledge_opt) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests)
- @$( parallel_sledge_opt) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests)
analyze-perf5 : compile
analyze-perf5 : compile
@$( parallel_sledge_opt) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests)
- @$( parallel_sledge_opt) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests)
analyze-perf7 : compile
analyze-perf7 : compile
@$( parallel_sledge_opt) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests)
- @$( parallel_sledge_opt) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests) $( AnalyzeTests)
.PHONY : analyze .sexp
.PHONY : analyze .sexp
analyze.sexp :
analyze.sexp :
@find -L { ,local/,extra/} analyze -not -path 'baseline/*' -name '*.sexp' 2>/dev/null \
find -L { ,local/,extra/} analyze -not -path 'baseline/*' -name '*.sexp' 2>/dev/null | xargs cat > analyze.sexp
| xargs cat > analyze.sexp
baseline/analyze.sexp : analyze .sexp
baseline/analyze.sexp : analyze .sexp
@ cp analyze.sexp $@
cp analyze.sexp $@
analyze.html : analyze .sexp
analyze.html : analyze .sexp
@ $( sledge_report) html -baseline baseline/analyze.sexp analyze.sexp -output $@
$( sledge_report) html $( SLEDGE_R_ARGS) -baseline baseline/analyze.sexp analyze.sexp -output $@
analyze-status : analyze .sexp
analyze-status : analyze .sexp
@ $( sledge_report) status -baseline baseline/analyze.sexp analyze.sexp | column -ts$$ '\t'
$( sledge_report) status -baseline baseline/analyze.sexp analyze.sexp | column -ts$$ '\t'
#
#
# smt tests
# smt tests
@ -147,9 +148,9 @@ SmtTests:=$(shell find smt -name '*.smt2' 2>/dev/null)
# run sledge smt tests
# run sledge smt tests
.PHONY : smt
.PHONY : smt
smt :
smt :
-@ parallel --bar $( sledge_dbg) smt $( SLEDGE_ARGS) ::: $( SmtTests)
-parallel --bar $( sledge_dbg) smt $( SLEDGE_S _ARGS) ::: $( SmtTests)
parallel_sledge_opt_smt = parallel --shuf --bar $( sledge_opt) smt -append-report $( SLEDGE_ARGS) :::
parallel_sledge_opt_smt = parallel --shuf --bar $( sledge_opt) smt -append-report $( SLEDGE_S_ ARGS) :::
smt-perf1 :
smt-perf1 :
@$( parallel_sledge_opt_smt) $( SmtTests)
@$( parallel_sledge_opt_smt) $( SmtTests)
@ -165,17 +166,16 @@ smt-perf7:
.PHONY : smt .sexp
.PHONY : smt .sexp
smt.sexp :
smt.sexp :
@find -L { ,local/,extra/} smt -not -path 'baseline/*' -name '*.sexp' 2>/dev/null \
find -L { ,local/,extra/} smt -not -path 'baseline/*' -name '*.sexp' 2>/dev/null | xargs cat > smt.sexp
| xargs cat > smt.sexp
baseline/smt.sexp : smt .sexp
baseline/smt.sexp : smt .sexp
@ cp smt.sexp $@
cp smt.sexp $@
smt.html : smt .sexp
smt.html : smt .sexp
@ $( sledge_report) html -baseline baseline/smt.sexp smt.sexp -output $@
$( sledge_report) html -baseline baseline/smt.sexp smt.sexp -output $@
smt-status : smt .sexp
smt-status : smt .sexp
@ $( sledge_report) status -baseline baseline/smt.sexp smt.sexp | column -ts$$ '\t'
$( sledge_report) status -baseline baseline/smt.sexp smt.sexp | column -ts$$ '\t'
#
#
# llvm tests
# llvm tests
@ -184,22 +184,20 @@ smt-status: smt.sexp
# run sledge llvm translate tests
# run sledge llvm translate tests
.PHONY : llvm
.PHONY : llvm
llvm :
llvm :
-@find -L llvm -name '*.ll' -or -name '*.bc' 2>/dev/null \
-find -L llvm -name '*.ll' -or -name '*.bc' 2>/dev/null | parallel --bar $( sledge_dbg) llvm translate -no-models -no-internalize $( SLEDGE_T_ARGS)
| parallel --bar $( sledge_dbg) llvm translate -no-models -no-internalize $( SLEDGE_ARGS)
.PHONY : llvm .sexp
.PHONY : llvm .sexp
llvm.sexp :
llvm.sexp :
@find -L { ,local/,extra/} llvm -not -path 'baseline/*' -name '*.sexp' 2>/dev/null \
find -L { ,local/,extra/} llvm -not -path 'baseline/*' -name '*.sexp' 2>/dev/null | xargs cat > llvm.sexp
| xargs cat > llvm.sexp
baseline/llvm.sexp : llvm .sexp
baseline/llvm.sexp : llvm .sexp
@ cp llvm.sexp $@
cp llvm.sexp $@
llvm.html : llvm .sexp
llvm.html : llvm .sexp
@ $( sledge_report) html -baseline baseline/llvm.sexp llvm.sexp -output $@
$( sledge_report) html -baseline baseline/llvm.sexp llvm.sexp -output $@
llvm-status : llvm .sexp
llvm-status : llvm .sexp
@ $( sledge_report) status -baseline baseline/llvm.sexp llvm.sexp | column -ts$$ '\t'
$( sledge_report) status -baseline baseline/llvm.sexp llvm.sexp | column -ts$$ '\t'
#
#
# test workflow
# test workflow
@ -207,27 +205,27 @@ llvm-status: llvm.sexp
# report warnings
# report warnings
warnings :
warnings :
@ find -L * -name '*.out' | xargs grep -h "Warning:" | sort
find -L * -name '*.out' | xargs grep -h "Warning:" | sort
test-translate :
test-translate :
-@find -L { ,local/,extra/} translate -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' -or -name '*.llair' -delete 2>/dev/null
-rm $( TranslateTests:= .sexp) $( TranslateTests:= .out) $( TranslateTests:= .err) $( TranslateTests:= .bllair) $( TranslateTests:= .llair) 2>/dev/null
-@ $( MAKE) --no-print-directory translate
-$( MAKE) --no-print-directory translate
@ $( MAKE) --no-print-directory translate-status
$( MAKE) --no-print-directory translate-status
test-analyze :
test-analyze :
-@find -L { ,local/,extra/} analyze -name "*.sexp" -or -name "*.out" -or -name '*.err' -delete 2>/dev/null
-rm $( AnalyzeTests:= .sexp) $( AnalyzeTests:= .out) $( AnalyzeTests:= .err) 2>/dev/null
-@ $( MAKE) --no-print-directory analyze
-$( MAKE) --no-print-directory analyze
@ $( MAKE) --no-print-directory analyze-status
$( MAKE) --no-print-directory analyze-status
test-smt :
test-smt :
-@find -L { ,local/,extra/} smt -name "*.sexp" -or -name "*.out" -or -name '*.err' -delete 2>/dev/null
-rm $( SmtTests:= .sexp) $( SmtTests:= .out) $( SmtTests:= .err) 2>/dev/null
-@ $( MAKE) --no-print-directory smt
-$( MAKE) --no-print-directory smt
@ $( MAKE) --no-print-directory smt-status
$( MAKE) --no-print-directory smt-status
test-llvm :
test-llvm :
-@ find -L { ,local/,extra/} llvm -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' -delete 2>/dev/null
-find -L { ,local/,extra/} llvm \( -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' \) -delete 2>/dev/null
-@ $( MAKE) --no-print-directory llvm
-$( MAKE) --no-print-directory llvm
@ $( MAKE) --no-print-directory llvm-status
$( MAKE) --no-print-directory llvm-status
# run tests and check against expected results
# run tests and check against expected results
test : test -translate translate .html test -analyze analyze .html test -llvm llvm .html
test : test -translate translate .html test -analyze analyze .html test -llvm llvm .html
@ -237,24 +235,23 @@ promote: baseline/translate.sexp baseline/analyze.sexp baseline/smt.sexp baselin
# copy the current out and err files to the baseline dir
# copy the current out and err files to the baseline dir
promote-out :
promote-out :
@ find -L * -not -path 'baseline/*' \( -name '*.out' -or -name '*.err' \) | xargs gcp --parents -t baseline
find -L * -not -path 'baseline/*' \( -name '*.out' -or -name '*.err' \) | xargs gcp --parents -t baseline
# diff the current out files against the ones in the baseline dir
# diff the current out files against the ones in the baseline dir
diff-out :
diff-out :
@ $( diff) -mask-uniques -include '.*\.out' baseline -alt-next current .
$( diff) -mask-uniques -include '.*\.out' baseline -alt-next current .
# diff the current err files against the ones in the baseline dir
# diff the current err files against the ones in the baseline dir
diff-err :
diff-err :
@ $( diff) -mask-uniques -include '.*\.err' baseline -alt-next current .
$( diff) -mask-uniques -include '.*\.err' baseline -alt-next current .
# remove generated bitcode files
# remove generated bitcode files
cleanbc :
cleanbc :
@ rm -f $( GeneratedBCs)
rm -f $( GeneratedBCs)
# remove result files
# remove result files
cleanout :
cleanout :
@find -L * -not -path 'baseline/*' -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' -or -name '*.llair' \
find -L * \( -not -path 'baseline/*' -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' -or -name '*.llair' \) -delete
| xargs rm -f
clean : cleanbc cleanout
clean : cleanbc cleanout