From 8b39122cc806a9c3da6f92275829b89dd741813d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 12 Jul 2026 09:08:54 -0700 Subject: [PATCH] Move third-party miniz library to 3p/miniz-3.0.2 Moves the vendored miniz sources from jbmc/src/miniz/ to 3p/miniz-3.0.2/, and adds 3p/copyright.miniz-3.0.2 (Debian copyright-format 1.0) documenting provenance (upstream commit 0c30a001bc3c70, Expat license) and the local modifications. The build glue remains in jbmc/src/miniz/. Also removes the stale src/miniz/module_dependencies.txt, left behind when miniz moved to jbmc/src. Co-Authored-By: Claude Fable 5 --- .clang-format-ignore | 3 +- 3p/copyright.miniz-3.0.2 | 47 ++++++++++++++++++++ {jbmc/src/miniz => 3p/miniz-3.0.2}/miniz.cpp | 0 {jbmc/src/miniz => 3p/miniz-3.0.2}/miniz.h | 0 AGENTS.md | 3 +- jbmc/src/java_bytecode/Makefile | 2 +- jbmc/src/java_bytecode/mz_zip_archive.cpp | 2 +- jbmc/src/miniz/CMakeLists.txt | 11 ++++- jbmc/src/miniz/Makefile | 3 ++ scripts/run_diff.sh | 2 +- src/miniz/module_dependencies.txt | 2 - 11 files changed, 65 insertions(+), 10 deletions(-) create mode 100644 3p/copyright.miniz-3.0.2 rename {jbmc/src/miniz => 3p/miniz-3.0.2}/miniz.cpp (100%) rename {jbmc/src/miniz => 3p/miniz-3.0.2}/miniz.h (100%) delete mode 100644 src/miniz/module_dependencies.txt diff --git a/.clang-format-ignore b/.clang-format-ignore index c2404ee65ce..c6ef417ee3f 100644 --- a/.clang-format-ignore +++ b/.clang-format-ignore @@ -1,4 +1,3 @@ -jbmc/src/miniz/miniz.cpp -jbmc/src/miniz/miniz.h +3p/ src/cprover/wcwidth.c unit/catch/catch.hpp diff --git a/3p/copyright.miniz-3.0.2 b/3p/copyright.miniz-3.0.2 new file mode 100644 index 00000000000..6ed38a5019a --- /dev/null +++ b/3p/copyright.miniz-3.0.2 @@ -0,0 +1,47 @@ +Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Upstream-Name: miniz +Upstream-Contact: Rich Geldreich +Source: https://github.com/richgel999/miniz +Comment: miniz is a lossless, high performance data compression library that + implements the zlib (RFC 1950) and Deflate (RFC 1951) compressed data format + specification standards, with ZIP archive reading support. The vendored copy + consists of the amalgamated files miniz.h and miniz.cpp (upstream: miniz.c), + and is used by jbmc/src/java_bytecode/ to read .jar files. + . + The in-tree files are based on upstream commit + 0c30a001bc3c70770a8742ff00899e662f040c75 (release 3.0.2 plus all upstream + changes up to and including the fix for CVE-2018-12913), with the + following local modifications: + * miniz.c has been renamed to miniz.cpp and is compiled as C++; + * the configuration macros MINIZ_NO_TIME, MINIZ_NO_DEFLATE_APIS, + MINIZ_NO_ARCHIVE_WRITING_APIS, MINIZ_NO_ZLIB_APIS and + MINIZ_NO_ZLIB_COMPATIBLE_NAMES are enabled in miniz.h; + * compiler warnings (conversion and unhandled-enum warnings, in + particular with Visual Studio) have been silenced; + * functions that are only used when archive writing is enabled have + been removed. + +Files: miniz-3.0.2/* +Copyright: 2013-2014, RAD Game Tools and Valve Software + 2010-2014, Rich Geldreich and Tenacious Software LLC + 2016, Martin Raiber +License: Expat + +License: Expat + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to + deal in the Software without restriction, including without limitation the + rights to use, copy, modify, merge, publish, distribute, sublicense, and/or + sell copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + . + The above copyright notice and this permission notice shall be included in + all copies or substantial portions of the Software. + . + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING + FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS + IN THE SOFTWARE. diff --git a/jbmc/src/miniz/miniz.cpp b/3p/miniz-3.0.2/miniz.cpp similarity index 100% rename from jbmc/src/miniz/miniz.cpp rename to 3p/miniz-3.0.2/miniz.cpp diff --git a/jbmc/src/miniz/miniz.h b/3p/miniz-3.0.2/miniz.h similarity index 100% rename from jbmc/src/miniz/miniz.h rename to 3p/miniz-3.0.2/miniz.h diff --git a/AGENTS.md b/AGENTS.md index de9550ec739..0b31d54fac9 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -47,6 +47,7 @@ formal verification of C and C++ programs. ``` cbmc/ +├── 3p/ # Third-party libraries ├── src/ # Main source code ├── jbmc/ # Java Bounded Model Checker ├── regression/ # Regression test suites @@ -170,7 +171,7 @@ Parallel structure to main CBMC for Java: - Abstract interpretation for Java - **`jdiff/`** - Diff tool for Java programs - Comparison of Java GOTO programs - - **`miniz/`** - ZIP compression library + - **`miniz/`** - ZIP compression library (sources in `3p/miniz-3.0.2/`) - Used for reading JAR files and compressed class files - **`jbmc/regression/`** - Java regression tests - **`jbmc/unit/`** - Java unit tests diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index 3dd396bf345..938d88827c6 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -57,7 +57,7 @@ SRC = assignments_from_json.cpp \ simple_method_stubbing.cpp \ # Empty last line -INCLUDES= -I .. -I ../$(CPROVER_DIR)/src +INCLUDES= -I .. -I ../$(CPROVER_DIR)/src -I ../$(CPROVER_DIR)/3p include ../config.inc include ../$(CPROVER_DIR)/src/config.inc diff --git a/jbmc/src/java_bytecode/mz_zip_archive.cpp b/jbmc/src/java_bytecode/mz_zip_archive.cpp index dfa70f9659b..1e89397fbff 100644 --- a/jbmc/src/java_bytecode/mz_zip_archive.cpp +++ b/jbmc/src/java_bytecode/mz_zip_archive.cpp @@ -10,7 +10,7 @@ Author: Diffblue Ltd #include #include #define _LARGEFILE64_SOURCE 1 -#include +#include // Original struct is an anonymous struct with a typedef, This is // required to remove internals from the header file diff --git a/jbmc/src/miniz/CMakeLists.txt b/jbmc/src/miniz/CMakeLists.txt index ac8d013b4a4..762ffe41ac2 100644 --- a/jbmc/src/miniz/CMakeLists.txt +++ b/jbmc/src/miniz/CMakeLists.txt @@ -1,6 +1,13 @@ -file(GLOB_RECURSE sources "*.cpp" "*.h") -add_library(miniz ${sources}) +add_library(miniz + ${CBMC_SOURCE_DIR}/3p/miniz-3.0.2/miniz.cpp + ${CBMC_SOURCE_DIR}/3p/miniz-3.0.2/miniz.h +) generic_includes(miniz) +target_include_directories(miniz + PUBLIC + ${CBMC_SOURCE_DIR}/3p +) + target_link_libraries(miniz) diff --git a/jbmc/src/miniz/Makefile b/jbmc/src/miniz/Makefile index d7c937a7dd1..b55b83ff8a2 100644 --- a/jbmc/src/miniz/Makefile +++ b/jbmc/src/miniz/Makefile @@ -7,6 +7,9 @@ include ../config.inc include ../$(CPROVER_DIR)/src/config.inc include ../$(CPROVER_DIR)/src/common +# the miniz sources are in the third-party directory 3p/ +vpath miniz.cpp ../$(CPROVER_DIR)/3p/miniz-3.0.2 + CLEANFILES = miniz$(OBJEXT) all: miniz$(OBJEXT) diff --git a/scripts/run_diff.sh b/scripts/run_diff.sh index 3f41b836994..00cbf0f30ba 100755 --- a/scripts/run_diff.sh +++ b/scripts/run_diff.sh @@ -37,7 +37,7 @@ then echo "Ensure cpplint.py is inside the $script_folder directory then run again" exit 1 else - cmd='${script_folder}/cpplint.py --exclude=jbmc/src/miniz/* --filter=-whitespace/operators,-readability/identifier_spacing $file 2>&1 >/dev/null' + cmd='${script_folder}/cpplint.py --exclude=3p/* --filter=-whitespace/operators,-readability/identifier_spacing $file 2>&1 >/dev/null' fi else echo "Mode $mode not recognized" diff --git a/src/miniz/module_dependencies.txt b/src/miniz/module_dependencies.txt deleted file mode 100644 index d415f87922b..00000000000 --- a/src/miniz/module_dependencies.txt +++ /dev/null @@ -1,2 +0,0 @@ -miniz -sys # system