Build and infrastructure fixes for FreeBSD

.githooks/pre-commit

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 # Runs scripts/cpplint.py on the modified files
 # Based on https://github.com/s0enke/git-hooks/
 #

.github/workflows/bsd.yaml

@@ -0,0 +1,193 @@
+name: Build and Test on *BSD
+on:
+  push:
+    branches: [ develop ]
+  pull_request:
+    branches: [ develop ]
+
+jobs:
+  # This job takes approximately 6 to 26 minutes
+  FreeBSD:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Prepare ccache
+        uses: actions/cache@v3
+        with:
+          path: .ccache
+          key: freebsd-13.2-gmake-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            freebsd-13.2-gmake-${{ github.ref }}
+            freebsd-13.2-gmake
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Build and Test
+        uses: vmactions/freebsd-vm@v1
+        with:
+          release: 13.2
+          usesh: true
+          run: |
+            # apparently fail-on-error isn't the default here
+            set -e -x
+            echo "Fetch dependencies"
+            pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3
+            echo "Fetch JBMC dependencies"
+            pkg install -y openjdk8 wget maven
+            echo "Zero ccache stats and limit in size"
+            export CCACHE_BASEDIR=$PWD
+            export CCACHE_DIR=$PWD/.ccache
+            ccache -z --max-size=500M
+            ccache -p
+            echo "Build with gmake"
+            # don't do JBMC as to keep the overall time in check
+            gmake -C src minisat2-download
+            gmake -C src -j2 CXX="ccache clang++"
+            # gmake -C jbmc/src setup-submodules
+            # gmake -C jbmc/src -j2 CXX="ccache clang++"
+            gmake -C unit "CXX=ccache clang++"
+            # gmake -C jbmc/unit "CXX=ccache clang++"
+            echo "Print ccache stats"
+            ccache -s
+            echo "Checking completeness of help output"
+            scripts/check_help.sh clang++
+            echo "Run unit tests"
+            gmake -C unit test
+            # gmake -C jbmc/unit test
+            echo "Running expected failure tests"
+            gmake TAGS='[!shouldfail]' -C unit test
+            # gmake TAGS='[!shouldfail]' -C jbmc/unit test
+            echo "Run regression tests"
+            gmake -C regression/cbmc test
+            # gmake -C regression test-parallel JOBS=2
+            # gmake -C regression/cbmc test-paths-lifo
+            # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
+            # # gmake -C jbmc/regression test-parallel JOBS=2
+
+  # This job takes approximately 7 to 34 minutes
+  OpenBSD:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Prepare ccache
+        uses: actions/cache@v3
+        with:
+          path: .ccache
+          key: openbsd-7.4-gmake-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            openbsd-7.4-gmake-${{ github.ref }}
+            openbsd-7.4-gmake
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Build and Test
+        uses: vmactions/openbsd-vm@v1
+        with:
+          release: 7.4
+          run: |
+            # apparently fail-on-error isn't the default here
+            set -e -x
+            echo "Fetch dependencies"
+            pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3
+            ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar
+            echo "Fetch JBMC dependencies"
+            pkg_add -v jdk%1.8 wget maven
+            echo "Zero ccache stats and limit in size"
+            export CCACHE_BASEDIR=$PWD
+            export CCACHE_DIR=$PWD/.ccache
+            ccache -z --max-size=500M
+            ccache -p
+            echo "Build with gmake"
+            # don't do JBMC so as to keep the overall time in check
+            gmake -C src minisat2-download
+            gmake -C src -j2 CXX="ccache clang++"
+            # gmake -C jbmc/src setup-submodules
+            # gmake -C jbmc/src -j2 CXX="ccache clang++"
+            gmake -C unit "CXX=ccache clang++"
+            # gmake -C jbmc/unit "CXX=ccache clang++"
+            echo "Print ccache stats"
+            ccache -s
+            echo "Checking completeness of help output"
+            scripts/check_help.sh clang++
+            echo "Run unit tests"
+            gmake -C unit test
+            # gmake -C jbmc/unit test
+            echo "Running expected failure tests"
+            gmake TAGS='[!shouldfail]' -C unit test
+            # gmake TAGS='[!shouldfail]' -C jbmc/unit test
+            echo "Run regression tests"
+            gmake -C regression/cbmc test
+            # gmake -C regression test-parallel JOBS=2
+            # gmake -C regression/cbmc test-paths-lifo
+            # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
+            # # gmake -C jbmc/regression test-parallel JOBS=2
+
+  # This job takes approximately 6 to 29 minutes
+  NetBSD:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Prepare ccache
+        uses: actions/cache@v3
+        with:
+          path: .ccache
+          key: netbsd-9.3-gmake-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            netbsd-9.3-gmake-${{ github.ref }}
+            netbsd-9.3-gmake
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Build and Test
+        uses: vmactions/netbsd-vm@v1
+        with:
+          release: 9.3
+          run: |
+            # apparently fail-on-error isn't the default here
+            set -e -x
+            echo "Fetch dependencies"
+            pkg_add -v bash gmake git python311 patch flex bison ccache parallel z3 gcc10
+            ln -s $(which python3.11) /usr/pkg/bin/python3
+            export PATH=/usr/pkg/gcc10/bin:$PATH
+            echo "Fetch JBMC dependencies"
+            pkg_add -v openjdk8 wget apache-maven
+            echo "Zero ccache stats and limit in size"
+            export CCACHE_BASEDIR=$PWD
+            export CCACHE_DIR=$PWD/.ccache
+            ccache -z --max-size=500M
+            ccache -p
+            echo "Build with gmake"
+            # don't do JBMC so as to keep the overall time in check
+            gmake -C src minisat2-download
+            gmake -C src -j2 CXX="ccache g++"
+            # gmake -C jbmc/src setup-submodules
+            # gmake -C jbmc/src -j2 CXX="ccache g++"
+            gmake -C unit "CXX=ccache g++"
+            # gmake -C jbmc/unit "CXX=ccache g++"
+            echo "Print ccache stats"
+            ccache -s
+            echo "Checking completeness of help output"
+            scripts/check_help.sh g++
+            echo "Run unit tests"
+            # TODO: unit tests are failing, requires debugging
+            gmake -C unit test || true
+            # gmake -C jbmc/unit test
+            echo "Running expected failure tests"
+            gmake TAGS='[!shouldfail]' -C unit test
+            # gmake TAGS='[!shouldfail]' -C jbmc/unit test
+            echo "Run regression tests"
+            # TODO: we need to model some more library functions
+            gmake -C regression/cbmc test || true
+            # gmake -C regression test-parallel JOBS=2
+            # gmake -C regression/cbmc test-paths-lifo
+            # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
+            # # gmake -C jbmc/regression test-parallel JOBS=2

.github/workflows/pull-request-check-clang-format.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # Stop on errors
 set -e

.github/workflows/pull-request-check-cpplint.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # Stop on errors
 set -e

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

@@ -59,7 +59,7 @@ jobs:
       - name: Print ccache stats
         run: ccache -s
       - name: Checking completeness of help output
-        run: scripts/check_help.sh
+        run: scripts/check_help.sh g++
       - name: Run unit tests
         run: |
           make -C unit test IPASIR=$PWD/riss.git/riss
@@ -247,7 +247,7 @@ jobs:
       - name: Print ccache stats
         run: ccache -s
       - name: Checking completeness of help output
-        run: scripts/check_help.sh build/bin
+        run: scripts/check_help.sh /usr/bin/g++ build/bin
       - name: Check if package building works
         run: |
           cd build

COMPILING.md

@@ -16,7 +16,7 @@ The environments below have been used successfully in the
 past, but are not actively tested:
 
 - Solaris 11
-- FreeBSD 11
+- FreeBSD 13
 
 # Building using CMake
 
@@ -246,11 +246,11 @@ Maven 3 manually.
 
 1. As root, get the necessary tools:
    ```
-   pkg install bash gmake git www/p5-libwww patch flex bison
+   pkg install bash gmake git www/p5-libwww python python3 patch flex bison cvc5 z3
    ```
    To compile JBMC, additionally install
    ```
-   pkg install openjdk8 wget maven3
+   pkg install openjdk8 wget maven
    ```
 2. As a user, get the CBMC source via
    ```

doc/doxygen-root/doxygen-markdown/markdown.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -euo pipefail
 

doc/man/cbmc.1

@@ -201,8 +201,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
 .TP
 \fB\-\-os\fR \fIos\fR
 Set analysis operating system, which defaults to the host operating system. Use
-one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
-\fBwindows\fR.
+one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
+\fBsolaris\fR, or \fBwindows\fR.
 .TP
 \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
 Set analysis architecture and operating system.

doc/man/goto-analyzer.1

@@ -460,8 +460,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
 .TP
 \fB\-\-os\fR \fIos\fR
 Set analysis operating system, which defaults to the host operating system. Use
-one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
-\fBwindows\fR.
+one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
+\fBsolaris\fR, or \fBwindows\fR.
 .TP
 \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
 Set analysis architecture and operating system.

doc/man/janalyzer.1

@@ -278,8 +278,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
 .TP
 \fB\-\-os\fR \fIos\fR
 Set analysis operating system, which defaults to the host operating system. Use
-one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
-\fBwindows\fR.
+one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
+\fBsolaris\fR, or \fBwindows\fR.
 .TP
 \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
 Set analysis architecture and operating system.

doc/man/jbmc.1

@@ -82,8 +82,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
 .TP
 \fB\-\-os\fR \fIos\fR
 Set analysis operating system, which defaults to the host operating system. Use
-one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
-\fBwindows\fR.
+one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
+\fBsolaris\fR, or \fBwindows\fR.
 .TP
 \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
 Set analysis architecture and operating system.

doc/slides/cbmc-latex-beamer/do_figures

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 FIG="cbmc-flow.fig frontend.fig"
 

integration/linux/compile_linux.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # Fail on errors
 # set -e # not for now

jbmc/regression/jbmc-json-ui/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 JBMC_PATH=$1
 shift

jbmc/regression/jbmc/deterministic_assignments_json/generate-json.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 mvn package
 java -cp target/jsonGenerator-1.0-SNAPSHOT-jar-with-dependencies.jar:. org.cprover.JsonGenerator

jbmc/regression/strings-smoke-tests/performance.py

@@ -1,4 +1,4 @@
-#!/usr/bin/python
+#!/usr/bin/env python
 
 '''
 This script collects the running times of the tests present in the current

regression/acceleration/accelerate.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 cleanup()
 {

regression/cbmc-concurrency/CMakeLists.txt

@@ -1,4 +1,4 @@
-if((NOT WIN32) AND (NOT APPLE))
+if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
 )

regression/cbmc-concurrency/Makefile

@@ -3,9 +3,9 @@ default: tests.log
 include ../../src/config.inc
 include ../../src/common
 
-ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),)
+ifeq ($(filter-out OSX MSVC FreeBSD,$(BUILD_ENV_)),)
 	# no POSIX threads on Windows
-	# for OSX we'd need sound handling of pointers in multi-threaded programs
+	# for OSX and FreeBSD we'd need sound handling of pointers in multi-threaded programs
 	no_pthread = -X pthread
 endif
 

regression/contracts-dfcc/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 

regression/contracts/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 

regression/extract_type_header/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 

regression/goto-analyzer-simplify/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 

regression/goto-harness-multi-file-project/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -x
 set -e

regression/goto-harness/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 

regression/goto-inspect/chain.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e