Skip to content

Commit 098a52a

Browse files
author
Daniel Kroening
authored
Merge pull request #548 from mgudemann/miniz_support
Miniz support
2 parents 921fdfd + 6ae2c79 commit 098a52a

File tree

24 files changed

+8644
-135
lines changed

24 files changed

+8644
-135
lines changed

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

721 Bytes
Binary file not shown.

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

721 Bytes
Binary file not shown.

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

934 Bytes
Binary file not shown.
709 Bytes
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
public class jarfile3
2+
{
3+
public class A
4+
{
5+
int x=1;
6+
}
7+
public class B
8+
{
9+
int x=1;
10+
}
11+
12+
void f(int i)
13+
{
14+
A a=new A();
15+
B b=new B();
16+
assert(a.x==1);
17+
assert(b.x==1);
18+
}
19+
}
+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
C.jar
3+
--function jarfile3.f -classpath A.jar:B.jar
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL
7+
--
8+
^warning: ignoring

src/Makefile

+3-27
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
22
goto-symex langapi pointer-analysis solvers util linking xmllang \
33
assembler analyses java_bytecode path-symex musketeer \
44
json cegis goto-analyzer jsil symex goto-diff clobber \
5-
memory-models
5+
memory-models miniz
66

77
all: cbmc.dir goto-cc.dir goto-instrument.dir symex.dir goto-analyzer.dir goto-diff.dir
88

@@ -20,7 +20,7 @@ cpp.dir: ansi-c.dir linking.dir
2020

2121
languages: util.dir langapi.dir \
2222
cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \
23-
jsil.dir
23+
jsil.dir miniz.dir
2424

2525
goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
2626
goto-symex.dir linking.dir analyses.dir solvers.dir \
@@ -84,28 +84,4 @@ glucose-download:
8484
@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
8585
@rm glucose-syrup.tgz
8686

87-
zlib-download:
88-
@echo "Downloading zlib 1.2.11"
89-
@lwp-download http://zlib.net/zlib-1.2.11.tar.gz
90-
@tar xfz zlib-1.2.11.tar.gz
91-
@rm -Rf ../zlib
92-
@mv zlib-1.2.11 ../zlib
93-
@rm zlib-1.2.11.tar.gz
94-
95-
libzip-download:
96-
@echo "Downloading libzip 1.1.2"
97-
# The below wants SSL
98-
#@lwp-download http://www.nih.at/libzip/libzip-1.1.2.tar.gz
99-
@lwp-download http://http.debian.net/debian/pool/main/libz/libzip/libzip_1.1.2.orig.tar.gz
100-
@tar xfz libzip_1.1.2.orig.tar.gz
101-
@rm -Rf ../libzip
102-
@mv libzip-1.1.2 ../libzip
103-
@rm libzip_1.1.2.orig.tar.gz
104-
105-
libzip-build:
106-
@echo "Building zlib"
107-
@(cd ../zlib; ./configure; make)
108-
@echo "Building libzip"
109-
@(cd ../libzip; BASE=`pwd`; ./configure --with-zlib=$(BASE)/zlib ; make)
110-
111-
.PHONY: minisat2-download glucose-download zlib-download libzip-download libzip-build
87+
.PHONY: minisat2-download glucose-download

src/cbmc/Makefile

+2-4
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
2727
../xmllang/xmllang$(LIBEXT) \
2828
../assembler/assembler$(LIBEXT) \
2929
../solvers/solvers$(LIBEXT) \
30-
../util/util$(LIBEXT)
30+
../util/util$(LIBEXT) \
31+
../miniz/miniz$(OBJEXT)
3132

3233
INCLUDES= -I ..
3334

@@ -48,9 +49,6 @@ endif
4849
ifneq ($(wildcard ../java_bytecode/Makefile),)
4950
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
5051
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
51-
ifneq ($(wildcard $(LIBZIPINC)),)
52-
LIBS += $(LIBZIPLIB)
53-
endif
5452
endif
5553

5654
ifneq ($(wildcard ../jsil/Makefile),)

src/cegis/Makefile

+2-4
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
115115
../cbmc/show_vcc$(OBJEXT) \
116116
../cbmc/cbmc_dimacs$(OBJEXT) ../cbmc/all_properties$(OBJEXT) \
117117
../cbmc/fault_localization$(OBJEXT) \
118-
../cbmc/symex_coverage$(OBJEXT)
118+
../cbmc/symex_coverage$(OBJEXT) \
119+
../miniz/miniz$(OBJEXT)
119120

120121
INCLUDES= -I ..
121122

@@ -137,9 +138,6 @@ all: cegis$(EXEEXT)
137138
ifneq ($(wildcard ../java_bytecode/Makefile),)
138139
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
139140
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
140-
ifneq ($(wildcard $(LIBZIPINC)),)
141-
LIBS += $(LIBZIPLIB)
142-
endif
143141
endif
144142

145143
###############################################################################

src/clobber/Makefile

+2-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1515
../goto-symex/rewrite_union$(OBJEXT) \
1616
../pointer-analysis/dereference$(OBJEXT) \
1717
../goto-instrument/dump_c$(OBJEXT) \
18-
../goto-instrument/goto_program2code$(OBJEXT)
18+
../goto-instrument/goto_program2code$(OBJEXT) \
19+
../miniz/miniz$(OBJEXT)
1920

2021
INCLUDES= -I ..
2122

src/config.inc

-2
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,6 @@ BUILD_ENV = AUTO
2424
MINISAT2 = ../../minisat-2.2.1
2525
#GLUCOSE = ../../glucose-syrup
2626
#SMVSAT =
27-
LIBZIPLIB = ../../libzip/lib/.libs/libzip.a ../../zlib/libz.a
28-
LIBZIPINC = ../../libzip/lib
2927

3028
# Signing identity for MacOS Gatekeeper
3129

src/goto-analyzer/Makefile

+2-4
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1212
../langapi/langapi$(LIBEXT) \
1313
../json/json$(LIBEXT) \
1414
../assembler/assembler$(LIBEXT) \
15-
../util/util$(LIBEXT)
15+
../util/util$(LIBEXT) \
16+
../miniz/miniz$(OBJEXT)
1617

1718
INCLUDES= -I ..
1819

@@ -28,9 +29,6 @@ all: goto-analyzer$(EXEEXT)
2829
ifneq ($(wildcard ../java_bytecode/Makefile),)
2930
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
3031
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
31-
ifneq ($(wildcard $(LIBZIPINC)),)
32-
LIBS += $(LIBZIPLIB)
33-
endif
3432
endif
3533

3634
ifneq ($(wildcard ../jsil/Makefile),)

src/goto-cc/Makefile

+2-4
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ OBJ += ../big-int/big-int$(LIBEXT) \
1313
../cpp/cpp$(LIBEXT) \
1414
../xmllang/xmllang$(LIBEXT) \
1515
../assembler/assembler$(LIBEXT) \
16-
../langapi/langapi$(LIBEXT)
16+
../langapi/langapi$(LIBEXT) \
17+
../miniz/miniz$(OBJEXT)
1718

1819
INCLUDES= -I ..
1920

@@ -31,9 +32,6 @@ all: goto-cc$(EXEEXT)
3132

3233
ifneq ($(wildcard ../java_bytecode/Makefile),)
3334
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
34-
ifneq ($(wildcard $(LIBZIPINC)),)
35-
LIBS += $(LIBZIPLIB)
36-
endif
3735
endif
3836

3937
ifneq ($(wildcard ../jsil/Makefile),)

src/goto-diff/Makefile

+2-4
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1313
../langapi/langapi$(LIBEXT) \
1414
../xmllang/xmllang$(LIBEXT) \
1515
../util/util$(LIBEXT) \
16-
../solvers/solvers$(LIBEXT)
16+
../solvers/solvers$(LIBEXT) \
17+
../miniz/miniz$(OBJEXT)
1718

1819
INCLUDES= -I ..
1920

@@ -29,9 +30,6 @@ all: goto-diff$(EXEEXT)
2930
ifneq ($(wildcard ../java_bytecode/Makefile),)
3031
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
3132
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
32-
ifneq ($(wildcard $(LIBZIPINC)),)
33-
LIBS += $(LIBZIPLIB)
34-
endif
3533
endif
3634

3735
ifneq ($(wildcard ../specc/Makefile),)

src/goto-instrument/Makefile

+2-4
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
3737
../langapi/langapi$(LIBEXT) \
3838
../xmllang/xmllang$(LIBEXT) \
3939
../util/util$(LIBEXT) \
40-
../solvers/solvers$(LIBEXT)
40+
../solvers/solvers$(LIBEXT) \
41+
../miniz/miniz$(OBJEXT)
4142

4243
INCLUDES= -I ..
4344

@@ -53,9 +54,6 @@ all: goto-instrument$(EXEEXT)
5354
ifneq ($(wildcard ../java_bytecode/Makefile),)
5455
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
5556
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
56-
ifneq ($(wildcard $(LIBZIPINC)),)
57-
LIBS += $(LIBZIPLIB)
58-
endif
5957
endif
6058

6159
ifneq ($(LIB_GLPK),)

src/java_bytecode/Makefile

-5
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,6 @@ include ../common
1515

1616
CLEANFILES = java_bytecode$(LIBEXT)
1717

18-
ifneq ($(wildcard $(LIBZIPINC)),)
19-
INCLUDES += -I $(LIBZIPINC)
20-
CP_CXXFLAGS += -DHAVE_LIBZIP
21-
endif
22-
2318
all: java_bytecode$(LIBEXT)
2419

2520
###############################################################################

src/java_bytecode/jar_file.cpp

+35-57
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,12 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9+
#include <cstring>
910
#include <cassert>
1011
#include <sstream>
1112

1213
#include "jar_file.h"
1314

14-
#ifdef HAVE_LIBZIP
15-
#include <zip.h>
16-
#endif
17-
1815
/*******************************************************************\
1916
2017
Function: jar_filet::open
@@ -29,33 +26,32 @@ Function: jar_filet::open
2926

3027
void jar_filet::open(const std::string &filename)
3128
{
32-
#ifdef HAVE_LIBZIP
33-
if(zip!=nullptr)
34-
// NOLINTNEXTLINE(readability/identifiers)
35-
zip_close(static_cast<struct zip *>(zip));
36-
37-
int zip_error;
38-
zip=zip_open(filename.c_str(), 0, &zip_error);
29+
if(!mz_ok)
30+
{
31+
memset(&zip, 0, sizeof(zip));
32+
mz_bool mz_open=mz_zip_reader_init_file(&zip, filename.c_str(), 0);
33+
mz_ok=mz_open==MZ_TRUE;
34+
}
3935

40-
if(zip!=nullptr)
36+
if(mz_ok)
4137
{
4238
std::size_t number_of_files=
43-
// NOLINTNEXTLINE(readability/identifiers)
44-
zip_get_num_entries(static_cast<struct zip *>(zip), 0);
39+
mz_zip_reader_get_num_files(&zip);
4540

4641
index.reserve(number_of_files);
4742

4843
for(std::size_t i=0; i<number_of_files; i++)
4944
{
50-
std::string file_name=
51-
// NOLINTNEXTLINE(readability/identifiers)
52-
zip_get_name(static_cast<struct zip *>(zip), i, 0);
45+
mz_uint filename_length=mz_zip_reader_get_filename(&zip, i, nullptr, 0);
46+
char *filename_char=new char[filename_length+1];
47+
mz_uint filename_len=
48+
mz_zip_reader_get_filename(&zip, i, filename_char, filename_length);
49+
assert(filename_length==filename_len);
50+
std::string file_name(filename_char);
51+
delete[] filename_char;
5352
index.push_back(file_name);
5453
}
5554
}
56-
#else
57-
zip=nullptr;
58-
#endif
5955
}
6056

6157
/*******************************************************************\
@@ -72,11 +68,11 @@ Function: jar_filet::~jar_filet
7268

7369
jar_filet::~jar_filet()
7470
{
75-
#ifdef HAVE_LIBZIP
76-
if(zip!=nullptr)
77-
// NOLINTNEXTLINE(readability/identifiers)
78-
zip_close(static_cast<struct zip *>(zip));
79-
#endif
71+
if(mz_ok)
72+
{
73+
mz_zip_reader_end(&zip);
74+
mz_ok=false;
75+
}
8076
}
8177

8278
/*******************************************************************\
@@ -91,47 +87,29 @@ Function: jar_filet::get_entry
9187
9288
\*******************************************************************/
9389

94-
#define ZIP_READ_SIZE 10000
95-
9690
std::string jar_filet::get_entry(std::size_t i)
9791
{
98-
if(zip==nullptr)
92+
if(!mz_ok)
9993
return std::string("");
10094

10195
assert(i<index.size());
10296

10397
std::string dest;
10498

105-
#ifdef HAVE_LIBZIP
106-
void *zip_e=zip; // zip is both a type and a non-type
107-
// NOLINTNEXTLINE(readability/identifiers)
108-
struct zip *zip_p=static_cast<struct zip*>(zip_e);
109-
110-
// NOLINTNEXTLINE(readability/identifiers)
111-
struct zip_file *zip_file=zip_fopen_index(zip_p, i, 0);
112-
113-
if(zip_file==NULL)
114-
{
115-
zip_close(zip_p);
116-
zip=nullptr;
117-
return std::string(""); // error
118-
}
119-
99+
mz_zip_archive_file_stat file_stat;
100+
memset(&file_stat, 0, sizeof(file_stat));
101+
mz_bool stat_ok=mz_zip_reader_file_stat(&zip, i, &file_stat);
102+
if(stat_ok!=MZ_TRUE)
103+
return std::string();
120104
std::vector<char> buffer;
121-
buffer.resize(ZIP_READ_SIZE);
122-
123-
while(true)
124-
{
125-
int bytes_read=
126-
zip_fread(zip_file, buffer.data(), ZIP_READ_SIZE);
127-
assert(bytes_read<=ZIP_READ_SIZE);
128-
if(bytes_read<=0)
129-
break;
130-
dest.insert(dest.end(), buffer.begin(), buffer.begin()+bytes_read);
131-
}
132-
133-
zip_fclose(zip_file);
134-
#endif
105+
size_t bufsize=file_stat.m_uncomp_size;
106+
buffer.resize(bufsize);
107+
mz_bool read_ok=
108+
mz_zip_reader_extract_to_mem(&zip, i, buffer.data(), bufsize, 0);
109+
if(read_ok!=MZ_TRUE)
110+
return std::string();
111+
112+
dest.insert(dest.end(), buffer.begin(), buffer.end());
135113

136114
return dest;
137115
}

0 commit comments

Comments
 (0)