Miniz support

regression/cbmc-java/jar-file3/jarfile3.java

@@ -0,0 +1,19 @@
+public class jarfile3
+{
+  public class A
+  {
+    int x=1;
+  }
+  public class B
+  {
+    int x=1;
+  }
+
+  void f(int i)
+  {
+    A a=new A();
+    B b=new B();
+    assert(a.x==1);
+    assert(b.x==1);
+  }
+}

regression/cbmc-java/jar-file3/test.desc

@@ -0,0 +1,8 @@
+CORE
+C.jar
+--function jarfile3.f -classpath A.jar:B.jar
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/Makefile

@@ -2,7 +2,7 @@ DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
        goto-symex langapi pointer-analysis solvers util linking xmllang \
        assembler analyses java_bytecode path-symex musketeer \
        json cegis goto-analyzer jsil symex goto-diff clobber \
-       memory-models
+       memory-models miniz
 
 all: cbmc.dir goto-cc.dir goto-instrument.dir symex.dir goto-analyzer.dir goto-diff.dir
 
@@ -20,7 +20,7 @@ cpp.dir: ansi-c.dir linking.dir
 
 languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \
-           jsil.dir
+           jsil.dir miniz.dir
 
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir \
@@ -84,28 +84,4 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz
 
-zlib-download:
-	@echo "Downloading zlib 1.2.11"
-	@lwp-download http://zlib.net/zlib-1.2.11.tar.gz
-	@tar xfz zlib-1.2.11.tar.gz
-	@rm -Rf ../zlib
-	@mv zlib-1.2.11 ../zlib
-	@rm zlib-1.2.11.tar.gz
-
-libzip-download:
-	@echo "Downloading libzip 1.1.2"
-	# The below wants SSL
-	#@lwp-download http://www.nih.at/libzip/libzip-1.1.2.tar.gz
-	@lwp-download http://http.debian.net/debian/pool/main/libz/libzip/libzip_1.1.2.orig.tar.gz
-	@tar xfz libzip_1.1.2.orig.tar.gz
-	@rm -Rf ../libzip
-	@mv libzip-1.1.2 ../libzip
-	@rm libzip_1.1.2.orig.tar.gz
-
-libzip-build:
-	@echo "Building zlib"
-	@(cd ../zlib; ./configure; make)
-	@echo "Building libzip"
-	@(cd ../libzip; BASE=`pwd`; ./configure --with-zlib=$(BASE)/zlib ; make)
-
-.PHONY: minisat2-download glucose-download zlib-download libzip-download libzip-build
+.PHONY: minisat2-download glucose-download

src/cbmc/Makefile

@@ -27,7 +27,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
-      ../util/util$(LIBEXT)
+      ../util/util$(LIBEXT) \
+      ../miniz/miniz$(OBJEXT)
 
 INCLUDES= -I ..
 
@@ -48,9 +49,6 @@ endif
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-  ifneq ($(wildcard $(LIBZIPINC)),)
-    LIBS += $(LIBZIPLIB)
-  endif
 endif
 
 ifneq ($(wildcard ../jsil/Makefile),)

src/cegis/Makefile

@@ -115,7 +115,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cbmc/show_vcc$(OBJEXT) \
       ../cbmc/cbmc_dimacs$(OBJEXT) ../cbmc/all_properties$(OBJEXT) \
       ../cbmc/fault_localization$(OBJEXT) \
-      ../cbmc/symex_coverage$(OBJEXT)
+      ../cbmc/symex_coverage$(OBJEXT) \
+      ../miniz/miniz$(OBJEXT)
 
 INCLUDES= -I ..
 
@@ -137,9 +138,6 @@ all: cegis$(EXEEXT)
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-  ifneq ($(wildcard $(LIBZIPINC)),)
-    LIBS += $(LIBZIPLIB)
-  endif
 endif
 
 ###############################################################################

src/clobber/Makefile

@@ -15,7 +15,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../goto-symex/rewrite_union$(OBJEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/dump_c$(OBJEXT) \
-       ../goto-instrument/goto_program2code$(OBJEXT)
+       ../goto-instrument/goto_program2code$(OBJEXT) \
+       ../miniz/miniz$(OBJEXT)
 
 INCLUDES= -I ..
 

src/config.inc

@@ -24,8 +24,6 @@ BUILD_ENV = AUTO
 MINISAT2 = ../../minisat-2.2.1
 #GLUCOSE = ../../glucose-syrup
 #SMVSAT =
-LIBZIPLIB = ../../libzip/lib/.libs/libzip.a ../../zlib/libz.a
-LIBZIPINC = ../../libzip/lib
 
 # Signing identity for MacOS Gatekeeper
 

src/goto-analyzer/Makefile

@@ -12,7 +12,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
-      ../util/util$(LIBEXT)
+      ../util/util$(LIBEXT) \
+      ../miniz/miniz$(OBJEXT)
 
 INCLUDES= -I ..
 
@@ -28,9 +29,6 @@ all: goto-analyzer$(EXEEXT)
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-  ifneq ($(wildcard $(LIBZIPINC)),)
-    LIBS += $(LIBZIPLIB)
-  endif
 endif
 
 ifneq ($(wildcard ../jsil/Makefile),)

src/goto-cc/Makefile

@@ -13,7 +13,8 @@ OBJ += ../big-int/big-int$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
-      ../langapi/langapi$(LIBEXT)
+      ../langapi/langapi$(LIBEXT) \
+      ../miniz/miniz$(OBJEXT)
 
 INCLUDES= -I ..
 
@@ -31,9 +32,6 @@ all: goto-cc$(EXEEXT)
 
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
-  ifneq ($(wildcard $(LIBZIPINC)),)
-    LIBS += $(LIBZIPLIB)
-  endif
 endif
 
 ifneq ($(wildcard ../jsil/Makefile),)

src/goto-diff/Makefile

@@ -13,7 +13,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT)
+      ../solvers/solvers$(LIBEXT) \
+      ../miniz/miniz$(OBJEXT)
 
 INCLUDES= -I ..
 
@@ -29,9 +30,6 @@ all: goto-diff$(EXEEXT)
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-  ifneq ($(wildcard $(LIBZIPINC)),)
-    LIBS += $(LIBZIPLIB)
-  endif
 endif
 
 ifneq ($(wildcard ../specc/Makefile),)

src/goto-instrument/Makefile

@@ -37,7 +37,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../solvers/solvers$(LIBEXT)
+      ../solvers/solvers$(LIBEXT) \
+      ../miniz/miniz$(OBJEXT)
 
 INCLUDES= -I ..
 
@@ -53,9 +54,6 @@ all: goto-instrument$(EXEEXT)
 ifneq ($(wildcard ../java_bytecode/Makefile),)
   OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-  ifneq ($(wildcard $(LIBZIPINC)),)
-    LIBS += $(LIBZIPLIB)
-  endif
 endif
 
 ifneq ($(LIB_GLPK),)

src/java_bytecode/Makefile

@@ -15,11 +15,6 @@ include ../common
 
 CLEANFILES = java_bytecode$(LIBEXT)
 
-ifneq ($(wildcard $(LIBZIPINC)),)
-  INCLUDES += -I $(LIBZIPINC)
-  CP_CXXFLAGS += -DHAVE_LIBZIP
-endif
-
 all: java_bytecode$(LIBEXT)
 
 ###############################################################################

src/java_bytecode/jar_file.cpp

@@ -6,15 +6,12 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <cstring>
 #include <cassert>
 #include <sstream>
 
 #include "jar_file.h"
 
-#ifdef HAVE_LIBZIP
-#include <zip.h>
-#endif
-
 /*******************************************************************\
 
 Function: jar_filet::open
@@ -29,33 +26,32 @@ Function: jar_filet::open
 
 void jar_filet::open(const std::string &filename)
 {
-  #ifdef HAVE_LIBZIP
-  if(zip!=nullptr)
-    // NOLINTNEXTLINE(readability/identifiers)
-    zip_close(static_cast<struct zip *>(zip));
-
-  int zip_error;
-  zip=zip_open(filename.c_str(), 0, &zip_error);
+  if(!mz_ok)
+  {
+    memset(&zip, 0, sizeof(zip));
+    mz_bool mz_open=mz_zip_reader_init_file(&zip, filename.c_str(), 0);
+    mz_ok=mz_open==MZ_TRUE;
+  }
 
-  if(zip!=nullptr)
+  if(mz_ok)
   {
     std::size_t number_of_files=
-      // NOLINTNEXTLINE(readability/identifiers)
-      zip_get_num_entries(static_cast<struct zip *>(zip), 0);
+      mz_zip_reader_get_num_files(&zip);
 
     index.reserve(number_of_files);
 
     for(std::size_t i=0; i<number_of_files; i++)
     {
-      std::string file_name=
-        // NOLINTNEXTLINE(readability/identifiers)
-        zip_get_name(static_cast<struct zip *>(zip), i, 0);
+      mz_uint filename_length=mz_zip_reader_get_filename(&zip, i, nullptr, 0);
+      char *filename_char=new char[filename_length+1];
+      mz_uint filename_len=
+        mz_zip_reader_get_filename(&zip, i, filename_char, filename_length);
+      assert(filename_length==filename_len);
+      std::string file_name(filename_char);
+      delete[] filename_char;
       index.push_back(file_name);
     }
   }
-  #else
-  zip=nullptr;
-  #endif
 }
 
 /*******************************************************************\
@@ -72,11 +68,11 @@ Function: jar_filet::~jar_filet
 
 jar_filet::~jar_filet()
 {
-  #ifdef HAVE_LIBZIP
-  if(zip!=nullptr)
-    // NOLINTNEXTLINE(readability/identifiers)
-    zip_close(static_cast<struct zip *>(zip));
-  #endif
+  if(mz_ok)
+  {
+    mz_zip_reader_end(&zip);
+    mz_ok=false;
+  }
 }
 
 /*******************************************************************\
@@ -91,47 +87,29 @@ Function: jar_filet::get_entry
 
 \*******************************************************************/
 
-#define ZIP_READ_SIZE 10000
-
 std::string jar_filet::get_entry(std::size_t i)
 {
-  if(zip==nullptr)
+  if(!mz_ok)
     return std::string("");
 
   assert(i<index.size());
 
   std::string dest;
 
-  #ifdef HAVE_LIBZIP
-  void *zip_e=zip; // zip is both a type and a non-type
-  // NOLINTNEXTLINE(readability/identifiers)
-  struct zip *zip_p=static_cast<struct zip*>(zip_e);
-
-  // NOLINTNEXTLINE(readability/identifiers)
-  struct zip_file *zip_file=zip_fopen_index(zip_p, i, 0);
-
-  if(zip_file==NULL)
-  {
-    zip_close(zip_p);
-    zip=nullptr;
-    return std::string(""); // error
-  }
-
+  mz_zip_archive_file_stat file_stat;
+  memset(&file_stat, 0, sizeof(file_stat));
+  mz_bool stat_ok=mz_zip_reader_file_stat(&zip, i, &file_stat);
+  if(stat_ok!=MZ_TRUE)
+    return std::string();
   std::vector<char> buffer;
-  buffer.resize(ZIP_READ_SIZE);
-
-  while(true)
-  {
-    int bytes_read=
-      zip_fread(zip_file, buffer.data(), ZIP_READ_SIZE);
-    assert(bytes_read<=ZIP_READ_SIZE);
-    if(bytes_read<=0)
-      break;
-    dest.insert(dest.end(), buffer.begin(), buffer.begin()+bytes_read);
-  }
-
-  zip_fclose(zip_file);
-  #endif
+  size_t bufsize=file_stat.m_uncomp_size;
+  buffer.resize(bufsize);
+  mz_bool read_ok=
+    mz_zip_reader_extract_to_mem(&zip, i, buffer.data(), bufsize, 0);
+  if(read_ok!=MZ_TRUE)
+    return std::string();
+
+  dest.insert(dest.end(), buffer.begin(), buffer.end());
 
   return dest;
 }