Merge pull request diffblue#338 from diffblue/bugfix/restrict_length_of_file_names_of_summaries

SEC-16: Bugfix/restrict length of file names of summaries

Author: marek-trtik

cbmc/src/util/file_util.cpp

@@ -161,7 +161,11 @@ std::string concat_dir_file(
 /// This is not designed to operate on path names and will replace folder
 /// seperator characters.
 /// \param file_name: The file name to sanitize.
-std::string make_valid_filename(std::string file_name)
+/// \param max_length: The maximum length for the file name. If the name is
+///                    longer, then its length will be cut to the max_length.
+std::string make_valid_filename(
+  std::string file_name,
+  const std::size_t max_length)
 {
   std::replace(file_name.begin(), file_name.end(), '#', '_');
   std::replace(file_name.begin(), file_name.end(), '$', '_');
@@ -170,5 +174,7 @@ std::string make_valid_filename(std::string file_name)
   std::replace(file_name.begin(), file_name.end(), '\\', '.');
   std::replace(file_name.begin(), file_name.end(), '<', '[');
   std::replace(file_name.begin(), file_name.end(), '>', ']');
+  if(file_name.size() > max_length)
+    file_name.resize(max_length);
   return file_name;
 }

cbmc/src/util/file_util.h

@@ -12,13 +12,21 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
+/// This constant defines the maximum name length of any file created by
+/// any module of the CProver. The value of the constant was derived
+/// from the most restrictive file system we use on our workstations:
+/// 'ecryptfs'.
+const std::size_t MAX_FILE_NAME_LENGTH = 140;
+
 void delete_directory(const std::string &path);
 
 std::string get_current_working_directory();
 
 std::string concat_dir_file(const std::string &directory,
                             const std::string &file_name);
 
-std::string make_valid_filename(std::string filename);
+std::string make_valid_filename(
+  std::string filename,
+  const std::size_t max_length = MAX_FILE_NAME_LENGTH);
 
 #endif // CPROVER_UTIL_FILE_UTIL_H

src/util/json_map_serializer.h

@@ -254,7 +254,12 @@ class json_map_serializert:public virtual_map_iterated_by_keyt<keyt, valuet>
       path=get_existing_path(key);
     else
     {
-      std::string file_name=make_valid_filename(key_converter(key));
+      const std::size_t max_size =
+        MAX_FILE_NAME_LENGTH // The general length limit.
+        - 15 // Save space for unique ID integer.
+        - std::strlen(suffix); // Save space for '.json' extension
+      std::string file_name =
+        make_valid_filename(key_converter(key), max_size);
       unsigned long uniqueness=file_name==index_file_name ? 1 : 0;
       while(index.right.count(uniqueify(file_name, uniqueness)) != 0)
         ++uniqueness;