Merge pull request #166 from kth-step/holmake+test

add some selftests to Holmakefile with test action
kth-step · Mar 5, 2024 · 396b261 · 396b261
2 parents 2fb51ce + 6eab9c9
commit 396b261
Show file tree

Hide file tree

Showing 5 changed files with 39 additions and 3 deletions.
diff --git a/src/theory/bir-support/Holmakefile b/src/theory/bir-support/Holmakefile
@@ -1,4 +1,11 @@
 INCLUDES = $(HOLBADIR)/src/theory/bir
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) selftest.exe
 .PHONY: all
+
+selftest.exe: selftest.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: selftest.exe
+	./selftest.exe
+.PHONY: test
diff --git a/src/theory/bir/Holmakefile b/src/theory/bir/Holmakefile
@@ -1,4 +1,11 @@
 INCLUDES = $(HOLBADIR)/src/aux
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) selftest.exe
 .PHONY: all
+
+selftest.exe: selftest.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: selftest.exe
+	./selftest.exe
+.PHONY: test
diff --git a/src/tools/lifter/Holmakefile b/src/tools/lifter/Holmakefile
@@ -12,5 +12,16 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/tools/lifter
 
-all: $(DEFAULT_TARGETS)
+all: $(DEFAULT_TARGETS) selftest_arm.exe selftest_riscv.exe
 .PHONY: all
+
+selftest_arm.exe: selftest_arm.uo
+	$(HOLMOSMLC) -o $@ $<
+
+selftest_riscv.exe: selftest_riscv.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: selftest_arm.exe selftest_riscv.exe
+	./selftest_arm.exe
+	./selftest_riscv.exe
+.PHONY: test
diff --git a/src/tools/lifter/selftest_arm.sml b/src/tools/lifter/selftest_arm.sml
@@ -1,5 +1,12 @@
 open HolKernel Parse;
 open testutils;
+
+(* FIXME: needed to avoid quse errors *)
+open m0_stepLib;
+
+open bir_update_blockTheory;
+open bir_inst_liftingTheory;
+
 open bir_inst_liftingLib;
 open bir_inst_liftingLibTypes;
 open bir_inst_liftingHelpersLib;

diff --git a/src/tools/lifter/selftest_riscv.sml b/src/tools/lifter/selftest_riscv.sml
@@ -1,5 +1,9 @@
 open HolKernel Parse
 open testutils
+
+(* FIXME: needed to avoid quse errors *)
+open m0_stepLib;
+
 open bir_inst_liftingLib;
 open PPBackEnd
 open riscv_assemblerLib;