Add unit test setup

.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,20 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq emscripten flex bison libxml2-utils cpanminus ccache
+      - name: Install node.js 23
+        uses: actions/setup-node@v4
+        with:
+          node-version: 23
+      - name: Install emscripten
+        run: |
+          # The emscripten package in Ubuntu is too far behind.
+          git clone https://github.com/emscripten-core/emsdk.git
+          cd emsdk
+          git checkout 3.1.31
+          ./emsdk install latest
+          ./emsdk activate latest
+          source ./emsdk_env.sh
+          emcc --version
       - name: Prepare ccache
         uses: actions/cache@v4
         with:
@@ -297,9 +319,33 @@ jobs:
       - name: Get minisat
         run: make -C lib/cbmc/src minisat2-download
       - 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"
+        run: |
+          source emsdk/emsdk_env.sh
+          make -C src -j4 \
+               BUILD_ENV=Unix \
+               CXX="ccache emcc -fwasm-exceptions" \
+               LINKFLAGS="-sEXPORTED_RUNTIME_METHODS=callMain" \
+               LINKLIB="emar rc \$@ \$^" \
+               AR="emar" \
+               EXEEXT=".html" \
+               HOSTCXX="ccache g++" \
+               HOSTLINKFLAGS=""
       - name: print version number via node.js
-        run: node --no-experimental-fetch src/ebmc/ebmc.js --version
+        run:  node --experimental-wasm-exnref src/ebmc/ebmc.js --version
+      - name: Compile unit tests
+        run: |
+          source emsdk/emsdk_env.sh
+          make -C unit unit_tests.html -j4 \
+               BUILD_ENV=Unix \
+               CXX="ccache emcc -fwasm-exceptions" \
+               LINKFLAGS="-sEXPORTED_RUNTIME_METHODS=callMain" \
+               LINKLIB="emar rc \$@ \$^" \
+               AR="emar" \
+               EXEEXT=".html" \
+               HOSTCXX="ccache g++" \
+               HOSTLINKFLAGS=""
+      - name: Run unit tests
+        run:  node --experimental-wasm-exnref unit/unit_tests.js
       - name: Print ccache stats
         run: ccache -s
 
@@ -358,5 +404,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, dkr@amazon.com
+
+\*******************************************************************/
+
+#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, dkr@amazon.com
+
+\*******************************************************************/
+
+#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;
+}