Move third-party miniz library to 3p/miniz-3.0.2

.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

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 <richgel99@gmail.com>
+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.

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

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

jbmc/src/java_bytecode/mz_zip_archive.cpp

@@ -10,7 +10,7 @@ Author: Diffblue Ltd
 #include <stdexcept>
 #include <string>
 #define _LARGEFILE64_SOURCE 1
-#include <miniz/miniz.h>
+#include <miniz-3.0.2/miniz.h>
 
 // Original struct is an anonymous struct with a typedef, This is
 // required to remove internals from the header file

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)

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)

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"