feat(util/serializer): simple serialization infrastructure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/tests/util/CMakeLists.txt

@@ -61,3 +61,6 @@ add_test(optional ${CMAKE_CURRENT_BINARY_DIR}/optional)
 add_executable(stackinfo stackinfo.cpp)
 target_link_libraries(stackinfo ${EXTRA_LIBS})
 add_test(stackinfo ${CMAKE_CURRENT_BINARY_DIR}/stackinfo)
+add_executable(serializer serializer.cpp)
+target_link_libraries(serializer ${EXTRA_LIBS})
+add_test(serializer ${CMAKE_CURRENT_BINARY_DIR}/serializer)

src/tests/util/serializer.cpp

@@ -0,0 +1,128 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iostream>
+#include <sstream>
+#include <string>
+#include <cstring>
+#include <vector>
+#include <functional>
+#include "util/test.h"
+#include "util/object_serializer.h"
+#include "util/debug.h"
+#include "util/list.h"
+using namespace lean;
+
+template<typename T>
+struct list_ptr_hash { unsigned operator()(list<T> const & l) const { return std::hash<typename list<T>::cell*>()(l.raw()); } };
+template<typename T>
+struct list_ptr_eq { bool operator()(list<T> const & l1, list<T> const & l2) const { return l1.raw() == l2.raw(); } };
+
+class list_int_serializer : public object_serializer<list<int>, list_ptr_hash<int>, list_ptr_eq<int>> {
+    typedef object_serializer<list<int>, list_ptr_hash<int>, list_ptr_eq<int>> super;
+public:
+    void write(list<int> const & l) {
+        super::write(l, [&]() {
+                serializer & s = get_owner();
+                if (l) {
+                    s.write_bool(true);
+                    s.write_int(head(l));
+                    write(tail(l));
+                } else {
+                    s.write_bool(false);
+                }
+            });
+    }
+};
+
+class list_int_deserializer : public object_deserializer<list<int>> {
+    typedef object_deserializer<list<int>> super;
+public:
+    list<int> read() {
+        return super::read([&]() {
+                deserializer & d = get_owner();
+                if (d.read_bool()) {
+                    int h       = d.read_int();
+                    list<int> t = read();
+                    return list<int>(h, t);
+                } else {
+                    return list<int>();
+                }
+            });
+    }
+};
+
+struct list_int_initializer {
+    unsigned m_serializer_extid;
+    unsigned m_deserializer_extid;
+    list_int_initializer() {
+        m_serializer_extid   = serializer::register_extension([](){ return std::unique_ptr<serializer::extension>(new list_int_serializer()); });
+        m_deserializer_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new list_int_deserializer()); });
+    }
+};
+
+static list_int_initializer g_list_int_initializer;
+
+serializer & operator<<(serializer & s, list<int> const & l) {
+    s.get_extension<list_int_serializer>(g_list_int_initializer.m_serializer_extid).write(l);
+    return s;
+}
+
+deserializer & operator>>(deserializer & d, list<int> & l) {
+    l = d.get_extension<list_int_deserializer>(g_list_int_initializer.m_deserializer_extid).read();
+    return d;
+}
+
+static void tst1() {
+    std::ostringstream out;
+    serializer s(out);
+    s.write_int(10); s.write_int(20); s.write_bool(false); s.write_string("hello"); s.write_int(30);
+    std::istringstream in(out.str());
+    deserializer d(in);
+    lean_assert(d.read_int() == 10);
+    lean_assert(d.read_int() == 20);
+    lean_assert(!d.read_bool());
+    lean_assert(d.read_string() == "hello");
+    lean_assert(d.read_int() == 30);
+}
+
+static void tst2() {
+    std::ostringstream out;
+    serializer s(out);
+    list<int> l1{1, 2, 3, 4};
+    list<int> l2;
+    l2 = cons(10, l1);
+    list<int> l3;
+    l3 = cons(20, cons(30, l2));
+    s << l1 << l2 << l3 << l2 << l3;
+
+    std::cout << "OUT: ";
+    auto str = out.str();
+    for (auto c : str) {
+        std::cout << static_cast<int>(c) << " ";
+    }
+    std::cout << "\n";
+
+    std::istringstream in(out.str());
+    deserializer d(in);
+    list<int> new_l1, new_l2, new_l3, new_l4, new_l5;
+    d >> new_l1 >> new_l2 >> new_l3 >> new_l4 >> new_l5;
+    lean_assert_eq(l1, new_l1);
+    lean_assert_eq(l2, new_l2);
+    lean_assert_eq(l3, new_l3);
+    lean_assert_eq(l2, new_l4);
+    lean_assert_eq(l3, new_l5);
+    lean_assert(is_eqp(new_l1, tail(new_l2)));
+    lean_assert(is_eqp(new_l2, tail(tail(new_l3))));
+    lean_assert(is_eqp(new_l4, new_l2));
+    lean_assert(is_eqp(new_l5, new_l3));
+}
+
+int main() {
+    tst1();
+    tst2();
+    return has_violations() ? 1 : 0;
+}

src/util/CMakeLists.txt

@@ -8,6 +8,6 @@ add_library(util trace.cpp debug.cpp name.cpp name_set.cpp
   exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
   safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp
   script_state.cpp script_exception.cpp splay_map.cpp lua.cpp
-  luaref.cpp stackinfo.cpp lean_path.cpp ${THREAD_CPP})
+  luaref.cpp stackinfo.cpp lean_path.cpp serializer.cpp ${THREAD_CPP})
 
 target_link_libraries(util ${LEAN_LIBS})

src/util/object_serializer.h

@@ -0,0 +1,61 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <unordered_map>
+#include <vector>
+#include "util/serializer.h"
+
+#ifndef LEAN_OBJECT_SERIALIZER_BUCKET_SIZE
+#define LEAN_OBJECT_SERIALIZER_BUCKET_SIZE 8
+#endif
+
+namespace lean {
+/**
+   \brief Helper class for serializing objects.
+*/
+template<class T, class HashFn, class EqFn>
+class object_serializer : public serializer::extension {
+    std::unordered_map<T, unsigned, HashFn, EqFn> m_table;
+public:
+    object_serializer(HashFn const & h = HashFn(), EqFn const & e = EqFn()):m_table(LEAN_OBJECT_SERIALIZER_BUCKET_SIZE, h, e) {}
+    template<typename F>
+    void write(T const & v, F && f) {
+        auto it = m_table.find(v);
+        serializer & s = get_owner();
+        if (it == m_table.end()) {
+            s.write_bool(true);
+            f();
+            m_table.insert(std::make_pair(v, m_table.size()));
+        } else {
+            s.write_bool(false);
+            s.write_unsigned(it->second);
+        }
+    }
+};
+
+/**
+   \brief Helper class for deserializing objects.
+*/
+template<class T>
+class object_deserializer : public deserializer::extension {
+    std::vector<T> m_table;
+public:
+    template<typename F>
+    T read(F && f) {
+        deserializer & d = get_owner();
+        if (d.read_bool()) {
+            T r = f();
+            m_table.push_back(r);
+            return r;
+        } else {
+            unsigned i = d.read_unsigned();
+            lean_assert(i < m_table.size());
+            return m_table[i];
+        }
+    }
+};
+}

src/util/serializer.cpp

@@ -0,0 +1,21 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "util/serializer.h"
+
+namespace lean {
+std::string deserializer_core::read_string() {
+    std::string r;
+    while (true) {
+        char c = m_in.get();
+        if (c == 0)
+            break;
+        r += c;
+    }
+    return r;
+}
+}

src/util/serializer.h

@@ -0,0 +1,58 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <iostream>
+#include <string>
+#include <sstream>
+#include <cstring>
+#include "util/extensible_object.h"
+
+namespace lean {
+/**
+   \brief Low-tech serializer.
+   The actual functionality is implemented using extensions.
+*/
+class serializer_core {
+    std::ostream & m_out;
+public:
+    serializer_core(std::ostream & out):m_out(out) {}
+    void write_string(char const * str) { m_out.write(str, strlen(str) + 1); }
+    void write_string(std::string const & str) { m_out.write(str.c_str(), str.size() + 1); }
+    void write_unsigned(unsigned i) { m_out.write(reinterpret_cast<char*>(&i), sizeof(i)); }
+    void write_int(int i) { m_out.write(reinterpret_cast<char*>(&i), sizeof(i)); }
+    void write_bool(bool b) { m_out.put(b ? 1 : 0); }
+};
+
+typedef extensible_object<serializer_core> serializer;
+
+inline serializer & operator<<(serializer & s, char const * str) { s.write_string(str); return s; }
+inline serializer & operator<<(serializer & s, std::string const & str) { s.write_string(str); return s; }
+inline serializer & operator<<(serializer & s, unsigned i) { s.write_unsigned(i); return s; }
+inline serializer & operator<<(serializer & s, int i) { s.write_int(i); return s; }
+inline serializer & operator<<(serializer & s, bool b) { s.write_bool(b); return s; }
+
+/**
+   \brief Low-tech serializer.
+   The actual functionality is implemented using extensions.
+*/
+class deserializer_core {
+    std::istream & m_in;
+public:
+    deserializer_core(std::istream & in):m_in(in) {}
+    std::string read_string();
+    int read_int() { int r; m_in.read(reinterpret_cast<char*>(&r), sizeof(r)); return r; }
+    unsigned read_unsigned() { unsigned r; m_in.read(reinterpret_cast<char*>(&r), sizeof(r)); return r; }
+    bool read_bool() { return m_in.get() != 0; }
+};
+
+typedef extensible_object<deserializer_core> deserializer;
+
+inline deserializer & operator>>(deserializer & d, std::string & str) { str = d.read_string(); return d; }
+inline deserializer & operator>>(deserializer & d, unsigned & i) { i = d.read_unsigned(); return d; }
+inline deserializer & operator>>(deserializer & d, int & i) { i = d.read_int(); return d; }
+inline deserializer & operator>>(deserializer & d, bool & b) { b = d.read_bool(); return d; }
+}