Skip to content

Commit

Permalink
devel/cbmc: add new port
Browse files Browse the repository at this point in the history 
Bounded Model Checker for C and C++ programs
https://github.com/diffblue/cbmc

Sponsored by:	Netflix
  • Loading branch information
@ocochard
ocochard committed Feb 1, 2024
1 parent e2ea116 commit 7f087b7
Show file tree
Hide file tree
Showing 18 changed files with 387 additions and 0 deletions.
1 change: 1 addition & 0 deletions devel/Makefile
View file
Expand Up @@ -351,6 +351,7 @@
SUBDIR += catch2
SUBDIR += cbang
SUBDIR += cbfmt
SUBDIR += cbmc
SUBDIR += cbrowser
SUBDIR += cc65
SUBDIR += ccache
Expand Down
46 changes: 46 additions & 0 deletions devel/cbmc/Makefile
View file
@@ -0,0 +1,46 @@
PORTNAME= cbmc
PORTVERSION= 5.95.1
DISTVERSIONPREFIX= cbmc-
CATEGORIES= devel
MASTER_SITES= DEBIAN/pool/main/m/minisat2:minisat
DISTFILES= minisat2_2.2.1.orig.tar.gz:minisat

MAINTAINER= olivier@FreeBSD.org
COMMENT= Bounded Model Checker for C and C++ programs
WWW= https://github.com/diffblue/cbmc

LICENSE= BSD4CLAUSE
LICENSE_FILE= ${WRKSRC}/LICENSE

BUILD_DEPENDS= ${LOCALBASE}/bin/flex:textproc/flex
RUN_DEPENDS= ${LOCALBASE}/bin/cvc5:math/cvc5 \
${LOCALBASE}/bin/z3:math/z3

USES= gmake bison python shebangfix

USE_GITHUB= yes
GH_ACCOUNT= diffblue
SHEBANG_FILES= ${WRKSRC}/scripts/ls_parse.py
WRKSRC_minisat= ${WRKDIR}/minisat2-2.2.1

post-patch:
@${REINPLACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO = ${PORTNAME}-${PORTVERSION}|' \
${WRKSRC}/src/util/Makefile
post-extract:
@${MV} ${WRKSRC_minisat} ${WRKSRC}/minisat-2.2.1

do-build:
@${MKDIR} ${STAGEDIR}
cd ${WRKSRC} && ${GMAKE} -C src -j${MAKE_JOBS_NUMBER}

do-install:
. for x in cbmc crangler goto-analyzer goto-cc goto-diff goto-instrument \
goto-inspect goto-harness goto-synthesizer symtab2gb
${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${x} ${STAGEDIR}${PREFIX}/bin/
${INSTALL_MAN} ${WRKSRC}/doc/man/${x}.1 ${STAGEDIR}${PREFIX}/share/man/man1/
. endfor
${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc
${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld
${INSTALL_SCRIPT} ${WRKSRC}/scripts/ls_parse.py ${STAGEDIR}${PREFIX}/bin/

.include <bsd.port.mk>
5 changes: 5 additions & 0 deletions devel/cbmc/distinfo
View file
@@ -0,0 +1,5 @@
TIMESTAMP = 1706723199
SHA256 (minisat2_2.2.1.orig.tar.gz) = e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40
SIZE (minisat2_2.2.1.orig.tar.gz) = 44229
SHA256 (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b3783
SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) = 9073428
20 changes: 20 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc
View file
@@ -0,0 +1,20 @@
--- minisat-2.2.1/minisat/core/Solver.cc.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/core/Solver.cc
@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+ if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
polarity[x] = sign(trail[c]);
insertVarOrder(x); }
qhead = trail_lim[level];
@@ -666,7 +666,7 @@ lbool Solver::search(int nof_conflicts)

}else{
// NO CONFLICT
- if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
// Reached bound on number of conflicts:
progress_estimate = progressEstimate();
cancelUntil(0);
59 changes: 59 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h
View file
@@ -0,0 +1,59 @@
--- minisat-2.2.1/minisat/core/SolverTypes.h.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/core/SolverTypes.h
@@ -47,7 +47,7 @@ struct Lit {
int x;

// Use this as a constructor:
- friend Lit mkLit(Var var, bool sign = false);
+ //friend Lit mkLit(Var var, bool sign = false);

bool operator == (Lit p) const { return x == p.x; }
bool operator != (Lit p) const { return x != p.x; }
@@ -55,7 +55,7 @@ struct Lit {
};


-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
+inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
inline bool sign (Lit p) { return p.x & 1; }
@@ -127,7 +127,10 @@ class Clause {
unsigned has_extra : 1;
unsigned reloced : 1;
unsigned size : 27; } header;
+#include <util/pragma_push.def>
+#include <util/pragma_wzero_length_array.def>
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
+#include <util/pragma_pop.def>

friend class ClauseAllocator;

@@ -142,11 +145,12 @@ class Clause {
for (int i = 0; i < ps.size(); i++)
data[i].lit = ps[i];

- if (header.has_extra)
+ if (header.has_extra) {
if (header.learnt)
data[header.size].act = 0;
else
calcAbstraction();
+ }
}

// NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
@@ -157,11 +161,12 @@ class Clause {
for (int i = 0; i < from.size(); i++)
data[i].lit = from[i];

- if (header.has_extra)
+ if (header.has_extra) {
if (header.learnt)
data[header.size].act = from.data[header.size].act;
else
data[header.size].abs = from.data[header.size].abs;
+ }
}

public:
12 changes: 12 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
View file
@@ -0,0 +1,12 @@
--- minisat-2.2.1/minisat/mtl/IntTypes.h.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/mtl/IntTypes.h
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
#else

# include <stdint.h>
+#ifndef _MSC_VER
# include <inttypes.h>
+#endif

#endif

16 changes: 16 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h
View file
@@ -0,0 +1,16 @@
--- minisat-2.2.1/minisat/mtl/Vec.h.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/mtl/Vec.h
@@ -96,9 +96,11 @@ void vec<T>::capacity(int min_cap) {
void vec<T>::capacity(int min_cap) {
if (cap >= min_cap) return;
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
- if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
+ if (add > INT_MAX - cap)
throw OutOfMemoryException();
- }
+
+ data = (T*)xrealloc(data, (cap += add) * sizeof(T));
+}


template<class T>
19 changes: 19 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h
View file
@@ -0,0 +1,19 @@
--- minisat-2.2.1/minisat/mtl/XAlloc.h.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/mtl/XAlloc.h
@@ -21,7 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
#ifndef Minisat_XAlloc_h
#define Minisat_XAlloc_h

-#include <errno.h>
#include <stdlib.h>

namespace Minisat {
@@ -33,7 +32,7 @@ static inline void* xrealloc(void *ptr, size_t size)
static inline void* xrealloc(void *ptr, size_t size)
{
void* mem = realloc(ptr, size);
- if (mem == NULL && errno == ENOMEM){
+ if (mem == NULL){
throw OutOfMemoryException();
}else
return mem;
37 changes: 37 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc
View file
@@ -0,0 +1,37 @@
--- minisat-2.2.1/minisat/simp/SimpSolver.cc.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/simp/SimpSolver.cc
@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_s
return result;
}

-
-
bool SimpSolver::addClause_(vec<Lit>& ps)
{
#ifndef NDEBUG
@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause
if (var(qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(ps[j]) == var(qs[i]))
+ {
if (ps[j] == ~qs[i])
return false;
else
goto next;
+ }
out_clause.push(qs[i]);
}
next:;
@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause
if (var(__qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(__ps[j]) == var(__qs[i]))
+ {
if (__ps[j] == ~__qs[i])
return false;
else
goto next;
+ }
size++;
}
next:;
15 changes: 15 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc
View file
@@ -0,0 +1,15 @@
--- minisat-2.2.1/minisat/utils/Options.cc.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/utils/Options.cc
@@ -43,10 +43,12 @@ void Minisat::parseOptions(int& argc, char** argv, boo
}

if (!parsed_ok)
+ {
if (strict && match(argv[i], "-"))
fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
else
argv[j++] = argv[i];
+ }
}
}

30 changes: 30 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h
View file
@@ -0,0 +1,30 @@
--- minisat-2.2.1/minisat/utils/Options.h.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/utils/Options.h
@@ -60,7 +60,7 @@ class Option
struct OptionLt {
bool operator()(const Option* x, const Option* y) {
int test1 = strcmp(x->category, y->category);
- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
}
};

@@ -282,15 +282,15 @@ class Int64Option : public Option
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
- fprintf(stderr, "%4"PRIi64, range.begin);
+ fprintf(stderr, "%4" PRIi64, range.begin);

fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
- fprintf(stderr, "%4"PRIi64, range.end);
+ fprintf(stderr, "%4" PRIi64, range.end);

- fprintf(stderr, "] (default: %"PRIi64")\n", value);
+ fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");
33 changes: 33 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h
View file
@@ -0,0 +1,33 @@
--- minisat-2.2.1/minisat/utils/ParseUtils.h.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/utils/ParseUtils.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
#include <stdlib.h>
#include <stdio.h>

-#include <zlib.h>
+//#include <zlib.h>

namespace Minisat {

@@ -35,7 +35,7 @@ class StreamBuffer {


class StreamBuffer {
- gzFile in;
+ //gzFile in;
unsigned char buf[buffer_size];
int pos;
int size;
@@ -43,10 +43,10 @@ class StreamBuffer {
void assureLookahead() {
if (pos >= size) {
pos = 0;
- size = gzread(in, buf, sizeof(buf)); } }
+ /*size = gzread(in, buf, sizeof(buf));*/ } }

public:
- explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
+ //explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }

int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
void operator ++ () { pos++; assureLookahead(); }
11 changes: 11 additions & 0 deletions devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h
View file
@@ -0,0 +1,11 @@
--- minisat-2.2.1/minisat/utils/System.h.orig 2011-02-21 13:31:17 UTC
+++ minisat-2.2.1/minisat/utils/System.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT
#ifndef Minisat_System_h
#define Minisat_System_h

-#if defined(__linux__)
+#if defined(__linux__) && defined(__GLIBC__)
#include <fpu_control.h>
#endif

11 changes: 11 additions & 0 deletions devel/cbmc/files/patch-src_common
View file
@@ -0,0 +1,11 @@
--- src/common.orig 2024-02-01 00:44:35 UTC
+++ src/common
@@ -64,7 +64,7 @@ else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
YFLAGS ?= -v
else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
CP_CXXFLAGS +=
- LINKLIB = ar rcT $@ $^
+ LINKLIB = llvm-ar rcT $@ $^
LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
LINKNATIVE = $(HOSTCXX) $(HOSTLINKFLAGS) -o $@ $^
ifeq ($(origin CC),default)
13 changes: 13 additions & 0 deletions devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp
View file
@@ -0,0 +1,13 @@
--- src/solvers/sat/external_sat.cpp.orig 2023-10-30 12:11:18 UTC
+++ src/solvers/sat/external_sat.cpp
@@ -119,8 +119,8 @@ external_satt::resultt external_satt::parse_result(std
{
try
{
- signed long long as_long = std::stol(assignment_string);
- size_t index = std::labs(as_long);
+ signed long long as_long = std::stoll(assignment_string);
+ size_t index = std::llabs(as_long);

if(index >= number_of_variables)
{
29 changes: 29 additions & 0 deletions devel/cbmc/files/patch-src_util_optional.h
View file
@@ -0,0 +1,29 @@
--- src/util/optional.h.orig 2023-10-30 12:11:18 UTC
+++ src/util/optional.h
@@ -11,20 +11,20 @@ Author: Diffblue Ltd.
#define CPROVER_UTIL_OPTIONAL_H

#if defined __clang__
- #pragma clang diagnostic push ignore "-Wall"
- #pragma clang diagnostic push ignore "-Wpedantic"
+ #pragma clang diagnostic push
+ #pragma clang diagnostic ignored "-Wall"
+ #pragma clang diagnostic ignored "-Wpedantic"
#elif defined __GNUC__
- #pragma GCC diagnostic push ignore "-Wall"
- #pragma GCC diagnostic push ignore "-Wpedantic"
+ #pragma GCC diagnostic push
+ #pragma GCC diagnostic ignored "-Wall"
+ #pragma GCC diagnostic ignored "-Wpedantic"
#elif defined _MSC_VER
#pragma warning(push)
#endif
#include <nonstd/optional.hpp>
#if defined __clang__
#pragma clang diagnostic pop
- #pragma clang diagnostic pop
#elif defined __GNUC__
- #pragma GCC diagnostic pop
#pragma GCC diagnostic pop
#elif defined _MSC_VER
#pragma warning(pop)
7 changes: 7 additions & 0 deletions devel/cbmc/pkg-descr
View file
@@ -0,0 +1,7 @@
CBMC is a Bounded Model Checker for C and C++ programs.
It supports C89, C99, most of C11 and most compiler extensions provided by gcc
and Visual Studio. It allows verifying array bounds (buffer overflows), pointer
safety, exceptions and user-specified assertions. Furthermore, it can check C
and C++ for consistency with other languages, such as Verilog.
The verification is performed by unwinding the loops in the program and passing
the resulting equation to a decision procedure.

0 comments on commit 7f087b7

Please sign in to comment.