diff --git a/src/config.inc b/src/config.inc index 84a7749ee07..1fb0a49886a 100644 --- a/src/config.inc +++ b/src/config.inc @@ -9,7 +9,7 @@ BUILD_ENV = AUTO # Select optimisation or debug info #CXXFLAGS += -O2 -DNDEBUG -#CXXFLAGS += -O0 -g +CXXFLAGS += -O0 -g ifeq ($(shell uname),Linux) CXXFLAGS += -DUSE_BOOST diff --git a/src/util/dstring.cpp b/src/util/dstring.cpp index 4fa9769be23..08f798b5b89 100644 --- a/src/util/dstring.cpp +++ b/src/util/dstring.cpp @@ -7,3 +7,33 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "dstring.h" +#include "serializer.h" + + +/*******************************************************************\ + + Function: dstring::serialize + + Inputs: + serializer: The serializer to read from/write to + + Outputs: + + Purpose: + Serializes this instance to/from the given serializer. + +\*******************************************************************/ +void dstringt::serialize(serializert &serializer) +{ + if(serializer.is_for_reading()) + { + std::string str; + serializer.serialize("dstring", str); + no=string_container[str]; + } + else + { + std::string str=as_string(); + serializer.serialize("dstring", str); + } +} diff --git a/src/util/dstring.h b/src/util/dstring.h index 9fdfd1ecddd..c2efaad4662 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -13,6 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "string_container.h" +class serializert; + + class dstringt { public: @@ -123,6 +126,8 @@ class dstringt return out << as_string(); } + void serialize(serializert &serializer); + // non-standard unsigned get_no() const diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp index e175e3b1d39..6e4a16eb50a 100644 --- a/src/util/file_util.cpp +++ b/src/util/file_util.cpp @@ -371,3 +371,31 @@ std::string fileutl_get_relative_path( std::string const result = fileutl_join_path_parts(split1); return result; } + +/*******************************************************************\ + + Function: make_valid_filename + + Inputs: + file_name: The file name to sanitize. + + Outputs: + + Purpose: + Replaces invalid characters in a file name using a hard-coded list of + replacements. + This is not designed to operate on path names and will replace folder + seperator characters. + +\*******************************************************************/ +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(), ':', '.'); + std::replace(file_name.begin(), file_name.end(), '/', '.'); + std::replace(file_name.begin(), file_name.end(), '\\', '.'); + std::replace(file_name.begin(), file_name.end(), '<', '['); + std::replace(file_name.begin(), file_name.end(), '>', ']'); + return file_name; +} diff --git a/src/util/file_util.h b/src/util/file_util.h index ce104a70200..9c01c15f951 100644 --- a/src/util/file_util.h +++ b/src/util/file_util.h @@ -62,4 +62,6 @@ std::string fileutl_get_relative_path( std::string const &pathname, std::string const &directory); +std::string make_valid_filename(std::string filename); + #endif // CPROVER_UTIL_FILE_UTIL_H diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 886f8ce9d7b..21480aadd8a 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "string2int.h" #include "irep.h" #include "string_hash.h" +#include "serializer.h" #include "irep_hash.h" #ifdef SUB_IS_LIST @@ -1003,3 +1004,24 @@ std::string irept::pretty(unsigned indent, unsigned max_indent) const return result; } + +/*******************************************************************\ + + Function: irept::serialize + + Inputs: + serializer: The serializer to read from/write to + + Outputs: + + Purpose: + Serializes this instance to/from the given serializer. + +\*******************************************************************/ +void irept::serialize(serializert &serializer) +{ + serializer.serialize("id", write().data); + serializer.serialize("subs", get_sub()); + serializer.serialize("named_subs", get_named_sub()); + serializer.serialize("comments", get_comments()); +} diff --git a/src/util/irep.h b/src/util/irep.h index af0b68ac26e..32567c82a94 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -45,6 +45,9 @@ typedef std::string irep_namet; typedef string_hash irep_id_hash; #endif +class serializert; + + inline const std::string &id2string(const irep_idt &d) { #ifdef USE_DSTRING @@ -257,6 +260,8 @@ class irept std::string pretty(unsigned indent=0, unsigned max_indent=0) const; + void serialize(serializert &serializer); + protected: static bool is_comment(const irep_namet &name) { return !name.empty() && name[0]=='#'; } diff --git a/src/util/serializer.h b/src/util/serializer.h new file mode 100755 index 00000000000..8647292948a --- /dev/null +++ b/src/util/serializer.h @@ -0,0 +1,879 @@ +/*******************************************************************\ + +Module: Serializer + +Author: Nathan.Phillips@diffblue.com + +Purpose: Generic serialization of object hierarchies. + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_SERIALIZER_H +#define CPROVER_UTIL_SERIALIZER_H + +#include +#include +#include +#include +#include +#include +#include +#ifdef USE_BOOST +#include +#endif + + +/*******************************************************************\ + +Class: serializer_traitst + +Purpose: + A base class for classes that define traits that can be attached to a + serializer. + This is used to augment the behaviour of a family of serializers, typically + by passing data that is required for serializing a particular type of object + through to a sub-object serialization routine. + +\*******************************************************************/ +class serializer_traitst +{ +public: + // The virtual destructor ensures sub-classes are disposed correctly. + virtual ~serializer_traitst()=default; +}; + + +/*******************************************************************\ + +Class: serializert + +Purpose: + A base class for all serializers. + This is used to implement serialization by being passed to the serialize + method of classes to be serialized. + Defines pure virtual methods for serializing basic types. + Implements methods for serializing collection types. + +\*******************************************************************/ +class serializert +{ + ///////////////////////////////////////////////////////////////////////////// + // Section: Data used in this class + +private: + // The serializer for a containing object, if any + serializert *parent; + // Whether this serializer is used for reading rather than writing + bool is_read; + // Traits attached to this serializer + serializer_traitst *traits; + + ///////////////////////////////////////////////////////////////////////////// + // Section: Constructors/destructors + +protected: + /*******************************************************************\ + + Function: serializert::serializert + + Inputs: + parent: The serializer for the containing object. + is_read: Whether this serializer is used for reading rather than writing. + + Outputs: + + Purpose: + Creates a serializert for a sub-object of a larger serialization. + This is only called internally by sub-class implementations. + + \*******************************************************************/ + serializert(serializert *parent, bool is_read) + : parent(parent), is_read(is_read), traits(nullptr) + { + } + + /*******************************************************************\ + + Function: serializert::serializert + + Inputs: + is_read: Whether this serializer is used for reading rather than writing. + + Outputs: + + Purpose: + Creates a serializert. + This will be exposed externally by sub-class implementations but is not + itself public. + + \*******************************************************************/ + explicit serializert(bool is_read) + : parent(nullptr), is_read(is_read), traits(nullptr) + { + } + + // The virtual destructor ensures sub-classes are disposed correctly. + virtual ~serializert()=default; + + ///////////////////////////////////////////////////////////////////////////// + // Section: Accessors + +public: + /*******************************************************************\ + + Function: serializert::is_for_reading + + Inputs: + + Outputs: + Whether this serializer is used for reading rather than writing. + + Purpose: + Gets whether this serializer is used for reading rather than writing. + + \*******************************************************************/ + bool is_for_reading() { return is_read; } + + /*******************************************************************\ + + Function: serializert::get_traits + + Template parameters: + traitst: + The type of traits to return. Must be derived from serializer_traitst + + Inputs: + + Outputs: + A reference to traits attached to this serializer or one of its parents of + type traitst. + + Exceptions: + std::logic_error: + If there were no traits of type traitst attached to this serializer or + one of its parents + + Purpose: + Gets traits attached to this serializer of a specific type. + + \*******************************************************************/ + template + traitst &get_traits() const + { + traitst * result=dynamic_cast(traits); + if(result!=nullptr) + return *result; + assert(parent!=nullptr); // In release build allow undefined behaviour + return parent->get_traits(); + } + + /*******************************************************************\ + + Function: serializert::set_traits + + Inputs: + traits: + Traits to attach to this serializer + + Outputs: + + Exceptions: + std::logic_error: + If there were already traits attached to this serializer + + Purpose: + Sets traits attached to this serializer. + + \*******************************************************************/ + void set_traits(serializer_traitst &serializer_traits) + { + assert(traits==nullptr); + traits=&serializer_traits; + } + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serialization of basic data types + +public: + /*******************************************************************\ + + Function: serializert::serialize + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + virtual void serialize(const char *name, bool &field)=0; + + /*******************************************************************\ + + Function: serializert::serialize + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + virtual void serialize(const char *name, char &field)=0; + + /*******************************************************************\ + + Function: serializert::serialize + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + virtual void serialize(const char *name, std::string &field)=0; + + /*******************************************************************\ + + Function: serializert::serialize + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + virtual void serialize(const char *name, int &field)=0; + + /*******************************************************************\ + + Function: serializert::serialize + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + virtual void serialize(const char *name, unsigned int &field)=0; + + /*******************************************************************\ + + Function: serializert::serialize + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + virtual void serialize(const char *name, unsigned long long &field)=0; + + /*******************************************************************\ + + Function: serializert::serialize + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + virtual void serialize(const char *name, float &field)=0; + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing objects that implement a serialize method + +protected: + // This is a non-templated function so that it can be virtual + // It therefore can't take an object of the type to be serialized + // Instead it takes a function that writes to such an object + virtual void serialize_object( + const char *name, + std::function serialize)=0; + +public: + /*******************************************************************\ + + Function: serializert::serialize + + Template parameters: + T: + The type of the field to serialize. Must implement a serialize method. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field. + + \*******************************************************************/ + template + void serialize(const char *name, T &field) + { + serialize_object( + name, + [&field] (serializert &serializer) + { + field.serialize(serializer); + }); + } + + /*******************************************************************\ + + Function: serializert::read_object + + Template parameters: + T: + The type of the field to read. + Must implement a serialize method and have a default constructor. + + Inputs: + + Outputs: + An object of the type T read from the serializer. + + Purpose: + Serializes a field. + + \*******************************************************************/ + template + T read_object() + { + T result; + result.serialize(*this); + return result; + } + + /*******************************************************************\ + + Function: serializert::read_object + + Template parameters: + T: + The type of the field to read. + Must be serializable and have a default constructor. + + Inputs: + name: The name of the field to serialize. + + Outputs: + An object of the type T read from the field serializer. + + Purpose: + Serializes a field. + + \*******************************************************************/ + template + T read_object(const char *name) + { + T result; + serialize(name, result); + return result; + } + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing rvalue references + +public: + /*******************************************************************\ + + Function: serializert::serialize + + Template parameters: + T: + The type of the field to serialize. Must be serializable. + + Inputs: + name: The name of the field to serialize. + field: An rvalue reference to the field to serialize. + + Outputs: + + Purpose: + Serializes a field. + Since the field is an rvalue reference this override is useful for writing + temporary objects or reading into temporary objects that store their + values in a non-temporary. + + \*******************************************************************/ + template + void serialize(const char *name, T &&field) + { + serialize(name, static_cast(field)); + } + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing pairs of serializable values + +private: + /*******************************************************************\ + + Class serializable_pairt + + Template parameters: + pairt: + The type of the underlying pair to serialize. + Must have member types first_type and second_type that are serializable. + + Purpose: + Wraps a pair in a serializable object that removes const from the + component members. Obviously this should not be used to read into a const + value but is useful for writing const values such as are found in the + value_type of maps. + + \*******************************************************************/ + template + class serializable_pairt + { + private: + pairt &value; + + public: + // This allows conversion from pairt + // NOLINTNEXTLINE(runtime/explicit) + serializable_pairt(pairt &value) + : value(value) + { + } + + // This is an implicit conversion back to pairt + operator pairt &() const { return value; } + + void serialize(serializert &serializer) + { + serializer.serialize( + "first", + const_cast::type &>(value.first)); + serializer.serialize( + "second", + const_cast::type &>(value.second)); + } + }; + +public: + /*******************************************************************\ + + Function: serializert::serialize + + Template parameters: + firstt: The type of the first element of the pair. Must be serializable. + secondt: The type of the second element of the pair. Must be serializable. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field of type std::pair. + + \*******************************************************************/ + template + void serialize(const char *name, std::pair &field) + { + serialize(name, serializable_pairt>(field)); + } + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing vectors + +public: + // A helper base class for writing vectors + class collection_writert + { + public: + virtual bool is_end() const=0; + virtual void write(serializert &serializer)=0; + }; + + // Virtual function that must be implemented to support reading vectors + virtual void read_array( + const char *name, + std::function read_elt)=0; + + // Virtual function that must be implemented to support writing vectors + virtual void write_array( + const char *name, collection_writert &collection_writer)=0; + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing vectors of objects that implement a serialize method + +public: + // A helper class for writing vectors of objects that implement a serialize + // method + template + class serializable_obj_collection_writert:public collection_writert + { + public: + typedef typename collectiont::iterator iteratort; + typedef typename collectiont::reference referencet; + + private: + iteratort it; + iteratort end_it; + + public: + explicit serializable_obj_collection_writert(collectiont &collection) + : it(collection.begin()), end_it(collection.end()) + { + } + + serializable_obj_collection_writert(iteratort it, iteratort end_it) + : it(it), end_it(end_it) + { + } + + bool is_end() const { return it==end_it; } + + void write(serializert &serializer) + { + it->serialize(serializer); + ++it; + } + }; + +public: + /*******************************************************************\ + + Function: serializert::serialize_objects + + Template parameters: + eltt: + The type of elements of the vector. + Must implement a serialize method and have a default constructor. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field of type std::vector. + One can just use serialize instead of serialize_objects, but then each + object will be wrapped in another object with a single member + + \*******************************************************************/ + template + void serialize_objects(const char *name, std::vector &field) + { + if(is_read) + { + read_array( + name, + [&field] (serializert &serializer) + { + field.emplace_back(); + field.back().serialize(serializer); + }); + } + else + { + serializable_obj_collection_writert> writer(field); + write_array(name, writer); + } + } + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing vectors of serializable values + +protected: + // A helper class for writing vectors of serializable objects (wrapped in a + // value field) + template + class serializable_collection_writert:public collection_writert + { + public: + typedef typename collectiont::iterator iteratort; + typedef typename collectiont::reference referencet; + + private: + iteratort it; + iteratort end_it; + + public: + explicit serializable_collection_writert(collectiont &collection) + : it(collection.begin()), end_it(collection.end()) + { + } + + serializable_collection_writert(iteratort it, iteratort end_it) + : it(it), end_it(end_it) + { + } + + bool is_end() const { return it==end_it; } + + void write(serializert &serializer) + { + serializer.serialize("value", *it); + ++it; + } + }; + +public: + /*******************************************************************\ + + Function: serializert::serialize + + Template parameters: + eltt: + The type of elements of the vector. + Must be serializable and have a default constructor. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field of type std::vector. + + \*******************************************************************/ + template + void serialize(const char *name, std::vector &field) + { + if(is_read) + { + read_array( + name, + [&field] (serializert &serializer) + { + field.emplace_back(); + serializer.serialize("value", field.back()); + }); + } + else + { + serializable_collection_writert> writer(field); + write_array(name, writer); + } + } + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing sets of serializable values + +public: + /*******************************************************************\ + + Function: serializert::serialize_set + + Template parameters: + sett: + The type of set to be serialized. + Must have a member type value_type that is serializable and can be + inserted into the set. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + create_elt: A function that returns new set elements. + + Outputs: + + Purpose: + Serializes a set field. + + \*******************************************************************/ + template + void serialize_set( + const char *name, + sett &field, + const std::function &create_elt) + { + if(is_read) + { + read_array( + name, + [&field, &create_elt](serializert &serializer) + { + typename sett::value_type elt=create_elt(); + serializer.serialize("value", elt); + field.insert(elt); + }); + } + else + { + serializable_collection_writert writer(field); + write_array(name, writer); + } + } + +private: + /*******************************************************************\ + + Function: serializert::serialize_set + + Template parameters: + sett: + The type of set to be serialized. + Must have a member type value_type that is serializable, has a default + constructor and can be inserted into the set. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Helper function to serialize a set field. + + \*******************************************************************/ + template + void serialize_set(const char *name, sett &field) + { + serialize_set(name, field, [] () { return typename sett::value_type(); }); + } + +public: + /*******************************************************************\ + + Function: serializert::serialize + + Template parameters: + eltt: + The type of elements of the set. + Must be serializable and have a default constructor. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field of type std::set. + + \*******************************************************************/ + template + void serialize(const char *name, std::set &field) + { + serialize_set(name, field); + } + + ///////////////////////////////////////////////////////////////////////////// + // Section: Serializing maps of serializable values + +private: + // This helper function can serialize any type of map (mapt) that has member + // types key_type, mapped_type, value_type and reference, an insert method + // that takes std::pair and can be + // enumerated to get elements of type mapt::reference from which a + // serializable_pairt can be created. + template + void serialize_map(const char *name, mapt &field) + { + if(is_read) + { + read_array( + name, + [&field](serializert &serializer) + { + typedef std::pair + pairt; + pairt key_value_pair; + serializable_pairt wrapper(key_value_pair); + wrapper.serialize(serializer); + field.insert(key_value_pair); + }); + } + else + { + typedef serializable_pairt wrappert; + std::vector wrapper_vector; + for(typename mapt::reference elt : field) + wrapper_vector.emplace_back(elt); + serializable_obj_collection_writert> + writer(wrapper_vector); + write_array(name, writer); + } + } + +public: + /*******************************************************************\ + + Function: serializert::serialize + + Template parameters: + keyt: The type of keys of the map. Must be serializable. + valuet: The type of values of the map. Must be serializable. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field of type std::map. + + \*******************************************************************/ + template + void serialize(const char *name, std::map &field) + { + serialize_map(name, field); + } + +#ifdef USE_BOOST + /*******************************************************************\ + + Function: serializert::serialize + + Template parameters: + keyt: The type of keys of the map. Must be serializable. + valuet: The type of values of the map. Must be serializable. + + Inputs: + name: The name of the field to serialize. + field: The field to serialize. + + Outputs: + + Purpose: + Serializes a field of type boost::bimap. + + \*******************************************************************/ + template + void serialize(const char *name, boost::bimap &field) + { + serialize_map(name, field.left); + } +#endif +}; + +#endif