Skip to content

Commit 1e18b03

Browse files
authored
Merge pull request diffblue#295 from diffblue/smowton/feature/boost-filesystem
Switch from custom file / path routines to Boost-filesystem
2 parents c28c135 + 48d0e8e commit 1e18b03

35 files changed

+295
-538
lines changed

CMakeLists.txt

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -52,17 +52,28 @@ set(enable_cbmc_tests off CACHE BOOL "Whether CBMC tests should be enabled (the
5252
################################################################################
5353
# BOOST
5454

55-
set(boost_include_package_URL "http://storage.googleapis.com/diffblue-mirror/boost/boost_1.63_headers.tar.bz2?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1542631994&Signature=X2GwPSm1dR8IPGP0D5JoyDmOnL%2Br4F7AI7NUA7SbmOAowMC0JS7Q5A6%2BkQziUzQa88zpddr5gSRbDOLqdoGzwLrYgPNtURS5dJ7l1q6xfJWSS%2FYf8be%2FSbdfLVN8qcXKCsfDe05Hqf%2Bz2cksqjQ1H6L0syj43rftbW4%2F7tp355%2BkinCeE466ulJeyru3CK%2F3RGX2Ul6ZQV6lNxkit1m6QM5BRtLbUQ1GOW0GCK9fWH2fry2n7kRVBCM3oz8fX62kLdKYlaXCf%2BvvXs9hOOmcQurL%2Fa4DCJYoClX%2BpznqXVmjUY%2FI3pD4HlRKbCeiPnoC6de2i1uxFNSVTBpG3w%2BtfA%3D%3D" )
55+
set(boost_include_package_URL https://storage.googleapis.com/diffblue-mirror/boost/boost-1.63-headers-and-filesystem.tar.bz2?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1545214533&Signature=cuZPWyGIjl9vh8yOpXJWgzi3Z1vWHzT5fpvaXEKp%2FuaPYOLHm0ByWZAuFc1sPHfA0OfNIKm0ScQhlonEnBZD6CnfSes3vnPG3SB4LVqPzpbfOp2MTjfOKXGQBT%2Bzdi6xVr84rKGsar98%2Bo9lXflST%2FSwBX8%2BcnnSZEfz4H2WVMHiLKqVoIgjFl4vqck3eiI4NN2S3FRaVfDWPkH%2Fm1q87yfMEE3CyY8LgjMAt65iUXMGhp3Z9mPI%2BjYDty9fPNiHT25KZkqIk73qxBrKVoc1HAH%2F2DPgGNFE4YGFhl0AaaZ9arGz4oYggNL93xcAsnaCikM7xq2D1GTs8fCPRZbIyA%3D%3D )
5656

5757
include("${CMAKE_CURRENT_SOURCE_DIR}/cbmc/cmake/DownloadProject.cmake")
5858

5959
download_project(PROJ boost-include
6060
URL ${boost_include_package_URL}
6161
DOWNLOAD_NAME boost_1.63_headers.tar.bz2
62-
SOURCE_DIR ${CMAKE_BINARY_DIR}/boost-include-src/boost
62+
SOURCE_DIR ${CMAKE_BINARY_DIR}/boost-include-src
6363
)
6464

65-
set(boost_include_include_dir ${boost-include_SOURCE_DIR}/..)
65+
execute_process(COMMAND ${boost-include_SOURCE_DIR}/bootstrap.sh --with-libraries=filesystem,system
66+
WORKING_DIRECTORY ${boost-include_SOURCE_DIR}
67+
)
68+
69+
execute_process(COMMAND ${boost-include_SOURCE_DIR}/b2
70+
WORKING_DIRECTORY ${boost-include_SOURCE_DIR}
71+
)
72+
73+
set(boost_include_include_dir ${boost-include_SOURCE_DIR})
74+
set(boost_lib_dir ${boost-include_SOURCE_DIR}/stage/lib)
75+
link_directories(${boost_lib_dir})
76+
add_definitions(-DBOOST_SYSTEM_NO_DEPRECATED=1)
6677

6778
################################################################################
6879

cbmc/src/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ macro(generic_includes name)
6161
${CBMC_SOURCE_DIR}
6262
${CMAKE_CURRENT_BINARY_DIR}
6363
${CMAKE_CURRENT_SOURCE_DIR}
64+
${boost_include_include_dir}
6465
)
6566
endmacro(generic_includes)
6667

cbmc/src/cbmc/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,9 @@ target_link_libraries(cbmc-lib
2424
solvers
2525
util
2626
xml
27+
28+
boost_filesystem
29+
boost_system
2730
)
2831

2932
add_if_library(cbmc-lib bv_refinement)

cbmc/src/goto-analyzer/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,9 @@ target_link_libraries(goto-analyzer-lib
1919
json
2020
assembler
2121
util
22+
23+
boost_filesystem
24+
boost_system
2225
)
2326

2427
add_if_library(goto-analyzer-lib java_bytecode)

cbmc/src/goto-instrument/CMakeLists.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ add_library(goto-instrument-lib ${sources})
1010

1111
generic_includes(goto-instrument-lib)
1212

13+
14+
1315
target_link_libraries(goto-instrument-lib
1416
ansi-c
1517
cpp
@@ -25,6 +27,9 @@ target_link_libraries(goto-instrument-lib
2527
util
2628
json
2729
solvers
30+
31+
boost_filesystem
32+
boost_system
2833
)
2934

3035
add_if_library(goto-instrument-lib java_bytecode)

cbmc/src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
1515
#include <iostream>
1616
#include <memory>
1717

18+
#include <boost/filesystem.hpp>
19+
1820
#include <util/config.h>
1921
#include <util/string2int.h>
2022
#include <util/unicode.h>
@@ -136,15 +138,15 @@ int goto_instrument_parse_optionst::doit()
136138
// Here we only early-check for requirements and we handle the option later.
137139
const std::string out_json_file_pathname=
138140
cmdline.get_value("save-code-statistics");
139-
if(fileutl_is_directory(out_json_file_pathname))
141+
if(boost::filesystem::is_directory(out_json_file_pathname))
140142
{
141143
error() << "The path-name '" << out_json_file_pathname
142144
<< "'passed to the option '--save-code-statistics' "
143145
"represents an existing directory."
144146
<< eom;
145147
return 12;
146148
}
147-
if(fileutl_parse_extension_in_pathname(out_json_file_pathname)!=".json")
149+
if(boost::filesystem::path(out_json_file_pathname).extension() != ".json")
148150
{
149151
error() << "The file of the path-name '" << out_json_file_pathname
150152
<< "'passed to the option '--save-code-statistics' does "
@@ -790,11 +792,11 @@ int goto_instrument_parse_optionst::doit()
790792
stats.extend(goto_model);
791793
const std::string out_json_file_pathname=
792794
cmdline.get_value("save-code-statistics");
793-
INVARIANT(!fileutl_is_directory(out_json_file_pathname),
795+
INVARIANT(!boost::filesystem::is_directory(out_json_file_pathname),
794796
"The early check passed so the JSON file indeed should not be "
795797
" a directory.");
796798
INVARIANT(
797-
fileutl_parse_extension_in_pathname(out_json_file_pathname)==".json",
799+
boost::filesystem::path(out_json_file_pathname).extension() == ".json",
798800
"The early check passed so the JSON file indeed should have "
799801
"'.json' extension.");
800802
std::ofstream ofile(out_json_file_pathname);

cbmc/src/jbmc/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,9 @@ target_link_libraries(jbmc-lib
2525
solvers
2626
util
2727
xml
28+
29+
boost_filesystem
30+
boost_system
2831
)
2932

3033
add_if_library(jbmc-lib bv_refinement)

cbmc/src/util/file_util.cpp

Lines changed: 0 additions & 220 deletions
Original file line numberDiff line numberDiff line change
@@ -156,226 +156,6 @@ std::string concat_dir_file(
156156
#endif
157157
}
158158

159-
static std::string::size_type fileutl_parse_last_dir_pos(
160-
std::string const &file_pathname)
161-
{
162-
auto found = file_pathname.find_last_of("/\\");
163-
if(found == std::string::npos)
164-
return 0;
165-
else
166-
return found + 1;
167-
}
168-
169-
bool fileutl_file_exists(std::string const &pathname)
170-
{
171-
std::ifstream f{pathname, std::ios::binary};
172-
return f.good();
173-
}
174-
175-
bool fileutl_is_directory(std::string const &pathname)
176-
{
177-
if(!fileutl_file_exists(pathname))
178-
return false;
179-
# if defined(WIN32)
180-
return PathIsDirectory(pathname.c_str());
181-
# elif defined(__linux__) || defined(__APPLE__)
182-
struct stat buf;
183-
stat(pathname.c_str(), &buf);
184-
return S_ISDIR(buf.st_mode);
185-
# else
186-
# error "Unsuported platform."
187-
# endif
188-
}
189-
190-
uint64_t fileutl_file_size(std::string const &file_pathname)
191-
{
192-
std::ifstream f{file_pathname, std::ios::binary};
193-
std::streampos const begin = f.tellg();
194-
f.seekg(0ULL, std::ios::end);
195-
std::streampos const end = f.tellg();
196-
return end - begin;
197-
}
198-
199-
std::string fileutl_parse_name_in_pathname(std::string const &file_pathname)
200-
{
201-
return file_pathname.substr(fileutl_parse_last_dir_pos(file_pathname));
202-
}
203-
204-
std::string fileutl_parse_extension_in_pathname(const std::string &pathname)
205-
{
206-
const std::size_t idx=pathname.find_last_of('.');
207-
# if defined(WIN32)
208-
const std::size_t fwd_slash_idx=pathname.find_last_of('/');
209-
const std::size_t bwd_slash_idx=pathname.find_last_of('\\');
210-
const std::size_t slash_idx=
211-
fwd_slash_idx==std::string::npos ? bwd_slash_idx :
212-
bwd_slash_idx==std::string::npos ? fwd_slash_idx :
213-
std::max(fwd_slash_idx, bwd_slash_idx);
214-
# elif defined(__linux__) || defined(__APPLE__)
215-
const std::size_t slash_idx=pathname.find_last_of('/');
216-
# else
217-
# error "Unsuported platform."
218-
# endif
219-
return
220-
idx==std::string::npos || (slash_idx!=std::string::npos && idx<slash_idx) ?
221-
std::string() : pathname.substr(idx);
222-
}
223-
224-
std::string fileutl_parse_path_in_pathname(std::string const &file_pathname)
225-
{
226-
return file_pathname.substr(0U, fileutl_parse_last_dir_pos(file_pathname));
227-
}
228-
229-
std::string fileutl_remove_extension(std::string const &filename)
230-
{
231-
return filename.substr(0U, filename.find_last_of('.'));
232-
}
233-
234-
void fileutl_create_directory(std::string const &pathname)
235-
{
236-
# if defined(WIN32)
237-
char path_sep='\\';
238-
#else
239-
char path_sep='/';
240-
#endif
241-
std::size_t search_from=0;
242-
while(search_from!=std::string::npos)
243-
{
244-
// Search from after the previous path separator, incidentally
245-
// skipping trying to create '/' if an absolute path is given
246-
search_from=pathname.find(path_sep, search_from+1);
247-
std::string truncated_pathname=pathname.substr(0, search_from);
248-
#if defined(WIN32)
249-
_mkdir(truncated_pathname.c_str());
250-
#else
251-
mkdir(truncated_pathname.c_str(), 0777);
252-
#endif
253-
// Ignore return-- regardless of why we can't create a
254-
// path prefix, we might as well keep trying down to more
255-
// specific paths.
256-
}
257-
}
258-
259-
std::string fileutl_concatenate_file_paths(
260-
std::string const &left_path,
261-
std::string const &right_path)
262-
{
263-
if(left_path.empty())
264-
return right_path;
265-
if(right_path.empty())
266-
return left_path;
267-
return left_path + "/" + right_path;
268-
}
269-
270-
std::string fileutl_absolute_path(std::string const &path)
271-
{
272-
#if defined(WIN32)
273-
DWORD buffer_length = GetFullPathName(path.c_str(), 0, nullptr, nullptr);
274-
std::vector<char> buffer(buffer_length);
275-
DWORD actual_length =
276-
GetFullPathName(path.c_str(), buffer_length, &(buffer[0]), nullptr);
277-
if(actual_length != buffer_length - 1)
278-
throw "fileutl_absolute_path: GetFullPathName failed";
279-
return std::string(&(buffer[0]));
280-
#else
281-
char *absolute = realpath(path.c_str(), nullptr);
282-
if(absolute==NULL)
283-
{
284-
std::string error=std::strerror(errno);
285-
throw std::ios::failure("Could not resolve absolute path ("+error+")");
286-
}
287-
std::string ret(absolute);
288-
free(absolute);
289-
return ret;
290-
#endif
291-
}
292-
293-
std::string fileutl_normalise_path(std::string const &path)
294-
{
295-
std::string result = path;
296-
std::replace(result.begin(), result.end(), '\\', '/');
297-
std::string::size_type pos = 0ULL;
298-
while((pos = result.find("//", 0)) != std::string::npos)
299-
result.replace(pos, 2, "/");
300-
while((pos = result.find("/./", 0)) != std::string::npos)
301-
result.replace(pos, 3, "/");
302-
while((pos = result.find("/../", 0)) != std::string::npos)
303-
{
304-
assert(pos != 0ULL);
305-
const std::string::size_type prev_pos = result.rfind("/", pos-1ULL);
306-
if(prev_pos == std::string::npos)
307-
break;
308-
result.replace(prev_pos, pos - prev_pos + 4ULL, "/");
309-
}
310-
return result;
311-
}
312-
313-
void fileutl_split_pathname(
314-
std::string const &pathname,
315-
std::vector<std::string> &output)
316-
{
317-
std::istringstream istr(fileutl_normalise_path(pathname));
318-
std::string token;
319-
while(std::getline(istr, token, '/'))
320-
output.push_back(token);
321-
}
322-
323-
std::string fileutl_join_path_parts(std::vector<std::string> const &parts)
324-
{
325-
if(parts.empty())
326-
return "";
327-
std::string result = parts.at(0);
328-
for(uint64_t i = 1ULL; i < parts.size(); ++i)
329-
{
330-
result.push_back('/');
331-
result.append(parts.at(i));
332-
}
333-
return result;
334-
}
335-
336-
std::string fileutl_get_common_prefix(
337-
std::string const &pathname1,
338-
std::string const &pathname2)
339-
{
340-
std::vector<std::string> split1;
341-
fileutl_split_pathname(pathname1, split1);
342-
343-
std::vector<std::string> split2;
344-
fileutl_split_pathname(pathname2, split2);
345-
346-
std::vector<std::string> common_split;
347-
for(uint64_t i = 0ULL, size = std::min(split1.size(), split2.size());
348-
i < size && split1.at(i) == split2.at(i);
349-
++i)
350-
common_split.push_back(split1.at(i));
351-
352-
std::string const result = fileutl_join_path_parts(common_split);
353-
return result;
354-
}
355-
356-
std::string fileutl_get_relative_path(
357-
std::string const &pathname,
358-
std::string const &directory)
359-
{
360-
std::vector<std::string> split1;
361-
fileutl_split_pathname(pathname, split1);
362-
std::reverse(split1.begin(), split1.end());
363-
364-
std::vector<std::string> split2;
365-
fileutl_split_pathname(directory, split2);
366-
std::reverse(split2.begin(), split2.end());
367-
368-
while(!split1.empty() && !split2.empty() && split1.back() == split2.back())
369-
{
370-
split1.pop_back();
371-
split2.pop_back();
372-
}
373-
374-
std::reverse(split1.begin(), split1.end());
375-
std::string const result = fileutl_join_path_parts(split1);
376-
return result;
377-
}
378-
379159
/// Replaces invalid characters in a file name using a hard-coded list of
380160
/// replacements.
381161
/// This is not designed to operate on path names and will replace folder

0 commit comments

Comments
 (0)