add more tests to Holmakefiles

examples/bsl-wp-smt/Holmakefile

@@ -7,9 +7,10 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared/HolSmt \
            $(HOLBADIR)/src/shared \
+           $(HOLBADIR)/src/tools/cfg \
            $(HOLBADIR)/src/tools/wp
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) test-addrs-eq-imp-x42.exe test-cjmp.exe test-gauss-no-mem.exe
 .PHONY: all
 
 example-gauss-with-mem.exe: example-gauss-with-mem.uo
@@ -26,3 +27,12 @@ test-gauss-no-mem.exe: test-gauss-no-mem.uo
 
 wpsimp_test-gauss-no-mult.exe: wpsimp_test-gauss-no-mult.uo
 	$(HOLMOSMLC) -o $@ $<
+
+test: test-addrs-eq-imp-x42.exe test-cjmp.exe test-gauss-no-mem.exe
+	./test-addrs-eq-imp-x42.exe
+	./test-cjmp.exe
+	./test-gauss-no-mem.exe
+.PHONY: test
+
+EXTRA_CLEANS = example-gauss-with-mem.exe test-addrs-eq-imp-x42.exe \
+               test-cjmp.exe test-gauss-no-mem.exe wpsimp_test-gauss-no-mult.exe

examples/tutorial/7-composition/Holmakefile

@@ -17,5 +17,14 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/5-wp \
            $(HOLBADIR)/examples/tutorial/6-smt
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) test-composition.exe
 .PHONY: all
+
+test-composition.exe: test-composition.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-composition.exe
+	./test-composition.exe
+.PHONY: test
+
+EXTRA_CLEANS = test-composition.exe

src/shared/HolSmt/Holmakefile

@@ -1,4 +1,13 @@
 INCLUDES = 
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) selftest.exe
 .PHONY: all
+
+selftest.exe: selftest.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: selftest.exe
+	./selftest.exe
+.PHONY: test
+
+EXTRA_CLEANS = selftest.exe

src/shared/examples/Holmakefile

@@ -1,4 +1,41 @@
-INCLUDES = 
+INCLUDES = $(HOLBADIR)/src/shared \
+           $(HOLBADIR)/src/shared/HolSmt \
+           $(HOLBADIR)/src/shared/sml-simplejson \
+           $(HOLBADIR)/src/theory/bir \
+           $(HOLBADIR)/src/theory/bir-support
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) test-bir-to-word-to-z3-sat-model.exe test-bir-to-word.exe test-bsl-progs.exe test-json.exe test-smtLib.exe test-z3-sat-model.exe test-z3_wrapper.exe
 .PHONY: all
+
+test-bir-to-word-to-z3-sat-model.exe: test-bir-to-word-to-z3-sat-model.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-bir-to-word.exe: test-bir-to-word.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-bsl-progs.exe: test-bsl-progs.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-json.exe: test-json.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-smtLib.exe: test-smtLib.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-z3-sat-model.exe: test-z3-sat-model.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-z3_wrapper.exe: test-z3_wrapper.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-bir-to-word-to-z3-sat-model.exe test-bir-to-word.exe test-bsl-progs.exe test-json.exe test-smtLib.exe test-z3-sat-model.exe test-z3_wrapper.exe
+	./test-bir-to-word-to-z3-sat-model.exe
+	./test-bir-to-word.exe
+	./test-bsl-progs.exe
+	./test-json.exe
+	./test-smtLib.exe
+	./test-z3-sat-model.exe
+	./test-z3_wrapper.exe
+.PHONY: test
+
+EXTRA_CLEANS = test-bir-to-word-to-z3-sat-model.exe test-bir-to-word.exe test-bsl-progs.exe test-json.exe test-smtLib.exe test-z3-sat-model.exe test-z3_wrapper.exe

src/shared/examples/test-json.sml

@@ -1,5 +1,9 @@
 open HolKernel Parse boolLib bossLib;
 
+open wordsTheory;
+open bir_valuesTheory;
+open bir_programTheory;
+
 (*
 val _ = load "sml-simplejson/jsonparse";
 *)

src/theory/bir-support/Holmakefile

@@ -9,3 +9,5 @@ selftest.exe: selftest.uo
 test: selftest.exe
 	./selftest.exe
 .PHONY: test
+
+EXTRA_CLEANS = selftest.exe

src/theory/bir/Holmakefile

@@ -9,3 +9,5 @@ selftest.exe: selftest.uo
 test: selftest.exe
 	./selftest.exe
 .PHONY: test
+
+EXTRA_CLEANS = selftest.exe

src/tools/lifter/Holmakefile

@@ -25,3 +25,5 @@ test: selftest_arm.exe selftest_riscv.exe
 	./selftest_arm.exe
 	./selftest_riscv.exe
 .PHONY: test
+
+EXTRA_CLEANS = selftest_arm.exe selftest_riscv.exe

src/tools/scamv/Holmakefile

@@ -1,7 +1,21 @@
 INCLUDES = $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/shared \
-           $(HOLBADIR)/src/theory/tools/lifter
+           $(HOLBADIR)/src/theory/tools/lifter \
+           $(HOLBADIR)/src/tools/scamv/persistence
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) test-bir_utilLib.exe test-scamv_enumLib.exe
 .PHONY: all
+
+test-bir_utilLib.exe: test-bir_utilLib.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-scamv_enumLib.exe: test-scamv_enumLib.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-bir_utilLib.exe test-scamv_enumLib.exe
+	./test-bir_utilLib.exe
+	./test-scamv_enumLib.exe
+.PHONY: test
+
+EXTRA_CLEANS = test-bir_utilLib.exe test-scamv_enumLib.exe

src/tools/scamv/bir_utilLib.sml

@@ -4,7 +4,8 @@ struct
 local
   open HolKernel Parse;
   open bslSyntax;
-  open bir_exp_to_wordsLib stringSyntax wordsSyntax 
+  open bir_exp_to_wordsLib stringSyntax wordsSyntax;
+  open experimentsLib;
 
   (* error handling *)
   val libname  = "bir_utilLib"

src/tools/scamv/obsmodel/Holmakefile

@@ -1,5 +1,15 @@
 INCLUDES = $(HOLBADIR)/src/theory/bir \
-           $(HOLBADIR)/src/shared
+           $(HOLBADIR)/src/shared \
+           $(HOLBADIR)/src/tools/cfg
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) test-bir_obs_model.exe
 .PHONY: all
+
+test-bir_obs_model.exe: test-bir_obs_model.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-bir_obs_model.exe
+	./test-bir_obs_model.exe
+.PHONY: test
+
+EXTRA_CLEANS = test-bir_obs_model.exe

src/tools/scamv/obsmodel/bir_obs_modelLib.sml

@@ -10,6 +10,7 @@ open HolKernel boolLib liteLib simpLib Parse bossLib;
 
 local
     open bir_obs_modelTheory;
+    open bir_block_collectionLib;
 in
 
 

src/tools/scamv/obsmodel/test-bir_obs_model.sml

@@ -1,4 +1,8 @@
 open HolKernel Parse boolLib bossLib;
+
+(* FIXME: needed to avoid quse errors *)
+open m0_stepLib;
+
 open bslSyntax;
 
 open bir_obs_modelLib;

src/tools/scamv/symbexec/Holmakefile

@@ -1,6 +1,7 @@
 INCLUDES = $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
-           $(HOLBADIR)/src/shared
+           $(HOLBADIR)/src/shared \
+           $(HOLBADIR)/src/tools/exec
 
 all: $(DEFAULT_TARGETS)
 .PHONY: all

src/tools/scamv/symbexec/examples/Holmakefile

@@ -1,5 +1,14 @@
 INCLUDES = $(HOLBADIR)/src/tools/scamv/symbexec \
            $(HOLBADIR)/src/tools/scamv/symbexec/examples/minimal
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) test-minimal.exe
 .PHONY: all
+
+test-minimal.exe: test-minimal.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-minimal.exe
+	./test-minimal.exe
+.PHONY: test
+
+EXTRA_CLEANS = test-minimal.exe

src/tools/wp/bir_wpLib.sml

@@ -4,6 +4,10 @@ struct
 (* these dependencies probably need cleanup *)
 (* ================================================ *)
 open HolKernel boolLib liteLib simpLib Parse bossLib;
+
+(* FIXME: needed to avoid quse errors *)
+open m0_stepLib;
+
 open bir_inst_liftingTheory
 open bir_lifting_machinesTheory
 open bir_lifting_machinesLib bir_lifting_machinesLib_instances;

src/tools/wp/examples/Holmakefile

@@ -1,4 +1,17 @@
 INCLUDES = $(HOLBADIR)/src/tools/wp
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) test-toy.exe test-wp.exe
 .PHONY: all
+
+test-toy.exe: test-toy.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test-wp.exe: test-wp.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-toy.exe test-wp.exe
+	./test-toy.exe
+	./test-wp.exe
+.PHONY: test
+
+EXTRA_CLEANS = test-toy.exe test-wp.exe