From 1c2ddaa2dfb2fc20eef90a6a81520d0f06fdec4a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 8 Nov 2024 09:58:14 -0500 Subject: [PATCH] Add unit test setup --- .github/workflows/pull-request-checks.yaml | 55 +++++++++++++++++++++- unit/Makefile | 38 +++++++++++++++ unit/temporal-logic/nnf.cpp | 21 +++++++++ unit/unit_tests.cpp | 19 ++++++++ 4 files changed, 131 insertions(+), 2 deletions(-) create mode 100644 unit/Makefile create mode 100644 unit/temporal-logic/nnf.cpp create mode 100644 unit/unit_tests.cpp diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 43e9b23ce..d4941aa58 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.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 diff --git a/unit/Makefile b/unit/Makefile new file mode 100644 index 000000000..2bf1d4c79 --- /dev/null +++ b/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=' + +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) diff --git a/unit/temporal-logic/nnf.cpp b/unit/temporal-logic/nnf.cpp new file mode 100644 index 000000000..8d11a23a2 --- /dev/null +++ b/unit/temporal-logic/nnf.cpp @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: NNF Unit Tests + +Author: Daniel Kroening, Amazon, dkr@amazon.com + +\*******************************************************************/ + +#include +#include +#include + +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}}); + } +} diff --git a/unit/unit_tests.cpp b/unit/unit_tests.cpp new file mode 100644 index 000000000..adaac0f77 --- /dev/null +++ b/unit/unit_tests.cpp @@ -0,0 +1,19 @@ +/*******************************************************************\ + +Module: Unit Tests Main + +Author: Daniel Kroening, Amazon, dkr@amazon.com + +\*******************************************************************/ + +#define CATCH_CONFIG_MAIN +#include + +#include + +// Debug printer for irept +std::ostream &operator<<(std::ostream &os, const irept &value) +{ + os << value.pretty(); + return os; +}