diff --git a/devel/Makefile b/devel/Makefile index 4da71e0953a1f..51481c8a3aca7 100644 --- a/devel/Makefile +++ b/devel/Makefile @@ -351,6 +351,7 @@ SUBDIR += catch2 SUBDIR += cbang SUBDIR += cbfmt + SUBDIR += cbmc SUBDIR += cbrowser SUBDIR += cc65 SUBDIR += ccache diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile new file mode 100644 index 0000000000000..c7f7b3650e633 --- /dev/null +++ b/devel/cbmc/Makefile @@ -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 diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo new file mode 100644 index 0000000000000..f3e6d1161c6aa --- /dev/null +++ b/devel/cbmc/distinfo @@ -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 diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc new file mode 100644 index 0000000000000..c15c2f12fb0a3 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc @@ -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); diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h new file mode 100644 index 0000000000000..fa26c6372b367 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h @@ -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 ++#include + union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; ++#include + + 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: diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h new file mode 100644 index 0000000000000..d8c9ddedb701e --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h @@ -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 ++#ifndef _MSC_VER + # include ++#endif + + #endif + diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h new file mode 100644 index 0000000000000..b3062972c5c91 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_Vec.h @@ -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::capacity(int min_cap) { + void vec::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 diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h new file mode 100644 index 0000000000000..8c8b9680bf6d2 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_XAlloc.h @@ -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 + #include + + 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; diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc new file mode 100644 index 0000000000000..c83101829f033 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_simp_SimpSolver.cc @@ -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& 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:; diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc new file mode 100644 index 0000000000000..84b5f289e8a5a --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.cc @@ -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]; ++ } + } + } + diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h new file mode 100644 index 0000000000000..c844c16940d9a --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_Options.h @@ -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"); diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h new file mode 100644 index 0000000000000..a0b2311038055 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_ParseUtils.h @@ -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 + #include + +-#include ++//#include + + 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(); } diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h new file mode 100644 index 0000000000000..a49382def0dc8 --- /dev/null +++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_utils_System.h @@ -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 + #endif + diff --git a/devel/cbmc/files/patch-src_common b/devel/cbmc/files/patch-src_common new file mode 100644 index 0000000000000..6944a39d7788d --- /dev/null +++ b/devel/cbmc/files/patch-src_common @@ -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) diff --git a/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp b/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp new file mode 100644 index 0000000000000..f0dd61cd99630 --- /dev/null +++ b/devel/cbmc/files/patch-src_solvers_sat_external__sat.cpp @@ -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) + { diff --git a/devel/cbmc/files/patch-src_util_optional.h b/devel/cbmc/files/patch-src_util_optional.h new file mode 100644 index 0000000000000..4507ce0ade2bd --- /dev/null +++ b/devel/cbmc/files/patch-src_util_optional.h @@ -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 + #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) diff --git a/devel/cbmc/pkg-descr b/devel/cbmc/pkg-descr new file mode 100644 index 0000000000000..2004194d7c431 --- /dev/null +++ b/devel/cbmc/pkg-descr @@ -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. diff --git a/devel/cbmc/pkg-plist b/devel/cbmc/pkg-plist new file mode 100644 index 0000000000000..2d23b585ef577 --- /dev/null +++ b/devel/cbmc/pkg-plist @@ -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