Add unit test setup

Author: kroening

.github/workflows/pull-request-checks.yaml

@@ -43,6 +43,8 @@ jobs:
           make -C lib/cbmc/src minisat2-download
       - name: Build with make
         run: make -C src -j4 CXX="ccache g++"
+      - name: Run unit tests
+        run: make -C unit -j4 CXX="ccache g++"
       - name: Run the ebmc tests with SAT
         run: make -C regression/ebmc test
       - name: Run the ebmc tests with Z3
@@ -101,6 +103,8 @@ jobs:
           make -C lib/cbmc/src minisat2-download
       - name: Build with make
         run: make CXX="ccache clang++" -C src -j4
+      - name: Run unit tests
+        run: make -C unit -j4 CXX="ccache clang++"
       - name: Run the ebmc tests with SAT
         run: make -C regression/ebmc test
       - name: Run the ebmc tests with Z3
@@ -203,6 +207,8 @@ jobs:
         run: make -C lib/cbmc/src minisat2-download
       - name: Build with make
         run: make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j4
+      - name: Run unit tests
+        run: make -C unit -j4 CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs"
       - name: Run the ebmc tests with SAT
         run: |
           rm regression/ebmc/neural-liveness/counter1.desc
@@ -246,6 +252,8 @@ jobs:
         run: make -C lib/cbmc/src minisat2-download
       - name: Build with make
         run: make YACC="/opt/homebrew/opt/bison/bin/bison" CXX="ccache clang++" -C src -j3
+      - name: Run unit tests
+        run: make -C unit -j3 CXX="ccache g++"
       - name: Run the ebmc tests with SAT
         run: make -C regression/ebmc test
       - name: Run the ebmc tests with Z3
@@ -279,6 +287,9 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq emscripten flex bison libxml2-utils cpanminus ccache
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 22
       - name: Prepare ccache
         uses: actions/cache@v4
         with:
@@ -299,7 +310,13 @@ jobs:
       - name: Build with make
         run: make -C src -j4 CXX="ccache emcc" HOSTCXX="ccache g++" BUILD_ENV=Unix LINKLIB="emar rc \$@ \$^" AR="emar" EXEEXT=".html"
       - name: print version number via node.js
-        run: node --no-experimental-fetch src/ebmc/ebmc.js --version
+        run: |
+          node --version
+          # node --experimental-wasm-exnref --no-experimental-fetch src/ebmc/ebmc.js --version
+      - name: Run unit tests
+        run: |
+          make -C unit -j4 unit_tests.html CXX="ccache emcc" BUILD_ENV=Unix LINKLIB="emar rc \$@ \$^" AR="emar" EXEEXT=".html"
+          # node --experimental-wasm-exnref --no-experimental-fetch unit/unit_tests.js
       - name: Print ccache stats
         run: ccache -s
 
@@ -358,5 +375,10 @@ jobs:
           # disable MSYS file-name mangling
           MSYS2_ARG_CONV_EXCL: "*"
         run: make CXX=clcache BUILD_ENV=MSVC -j4 -C src
+      - name: Run unit tests
+        env:
+          # disable MSYS file-name mangling
+          MSYS2_ARG_CONV_EXCL: "*"
+        run: make CXX=clcache BUILD_ENV=MSVC -j4 -C unit
       - name: Print ccache stats
         run: clcache -s

unit/Makefile

@@ -0,0 +1,38 @@
+.PHONY: test
+
+# Main
+SRC = unit_tests.cpp
+
+# Test source files
+SRC += temporal-logic/nnf.cpp \
+       # Empty last line
+
+INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src
+
+CPROVER_DIR = ../lib/cbmc
+
+include $(CPROVER_DIR)/src/config.inc
+include $(CPROVER_DIR)/src/common
+
+CXXFLAGS += -D'LOCAL_IREP_IDS=<hw_cbmc_irep_ids.h>'
+
+OBJ += ../src/temporal-logic/temporal-logic$(LIBEXT)
+
+cprover.dir:
+	$(MAKE) $(MAKEARGS) -C ../src
+
+CPROVER_LIBS = $(CPROVER_DIR)/src/util/util$(LIBEXT) \
+               $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+               # Empty last line
+
+OBJ += $(CPROVER_LIBS)
+
+all: test
+
+test: unit_tests$(EXEEXT)
+	./unit_tests$(EXEEXT)
+
+###############################################################################
+
+unit_tests$(EXEEXT): $(OBJ)
+	$(LINKBIN)

unit/temporal-logic/nnf.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: NNF Unit Tests
+
+Author: Daniel Kroening, Amazon, [email protected]
+
+\*******************************************************************/
+
+#include <temporal-logic/ltl.h>
+#include <temporal-logic/nnf.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO("Generating NNF")
+{
+  GIVEN("A formula not in NNF")
+  {
+    auto p = symbol_exprt{"p", bool_typet{}};
+    auto formula = not_exprt{G_exprt{p}};
+    REQUIRE(property_nnf(formula) == F_exprt{not_exprt{p}});
+  }
+}

unit/unit_tests.cpp

@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: Unit Tests Main
+
+Author: Daniel Kroening, Amazon, [email protected]
+
+\*******************************************************************/
+
+#define CATCH_CONFIG_MAIN
+#include <util/irep.h>
+
+#include <testing-utils/use_catch.h>
+
+// Debug printer for irept
+std::ostream &operator<<(std::ostream &os, const irept &value)
+{
+  os << value.pretty();
+  return os;
+}