mirror of
https://git.FreeBSD.org/ports.git
synced 2024-10-18 19:49:40 +00:00
devel/cbmc: add new port
Bounded Model Checker for C and C++ programs https://github.com/diffblue/cbmc Sponsored by: Netflix
This commit is contained in:
parent
e2ea116d3d
commit
7f087b720e
@ -351,6 +351,7 @@
|
||||
SUBDIR += catch2
|
||||
SUBDIR += cbang
|
||||
SUBDIR += cbfmt
|
||||
SUBDIR += cbmc
|
||||
SUBDIR += cbrowser
|
||||
SUBDIR += cc65
|
||||
SUBDIR += ccache
|
||||
|
46
devel/cbmc/Makefile
Normal file
46
devel/cbmc/Makefile
Normal 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
devel/cbmc/distinfo
Normal file
5
devel/cbmc/distinfo
Normal 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
devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc
Normal file
20
devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc
Normal 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);
|
@ -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
devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
Normal file
12
devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
Normal 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
devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h
Normal file
16
devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h
Normal 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
devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h
Normal file
19
devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h
Normal 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;
|
@ -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:;
|
@ -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
devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h
Normal file
30
devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h
Normal 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");
|
@ -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
devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h
Normal file
11
devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h
Normal 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
devel/cbmc/files/patch-src_common
Normal file
11
devel/cbmc/files/patch-src_common
Normal 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
devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp
Normal file
13
devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp
Normal 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
devel/cbmc/files/patch-src_util_optional.h
Normal file
29
devel/cbmc/files/patch-src_util_optional.h
Normal 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
devel/cbmc/pkg-descr
Normal file
7
devel/cbmc/pkg-descr
Normal 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.
|
23
devel/cbmc/pkg-plist
Normal file
23
devel/cbmc/pkg-plist
Normal file
@ -0,0 +1,23 @@
|
||||
bin/cbmc
|
||||
bin/crangler
|
||||
bin/goto-analyzer
|
||||
bin/goto-cc
|
||||
bin/goto-diff
|
||||
bin/goto-instrument
|
||||
bin/goto-inspect
|
||||
bin/goto-harness
|
||||
bin/goto-synthesizer
|
||||
bin/symtab2gb
|
||||
bin/ls_parse.py
|
||||
bin/goto-gcc
|
||||
bin/goto-ld
|
||||
share/man/man1/cbmc.1.gz
|
||||
share/man/man1/crangler.1.gz
|
||||
share/man/man1/goto-analyzer.1.gz
|
||||
share/man/man1/goto-cc.1.gz
|
||||
share/man/man1/goto-diff.1.gz
|
||||
share/man/man1/goto-harness.1.gz
|
||||
share/man/man1/goto-inspect.1.gz
|
||||
share/man/man1/goto-instrument.1.gz
|
||||
share/man/man1/goto-synthesizer.1.gz
|
||||
share/man/man1/symtab2gb.1.gz
|
Loading…
Reference in New Issue
Block a user