From befb26788a9475dcd65a7586db4e531a6614090f Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Tue, 30 Jul 2019 23:33:33 +0900 Subject: [PATCH 1/8] Add json library. --- src/element/Makefile.am | 3 +- src/element/element.h | 22 +-- src/element/json/conv.hpp | 98 +++++++++++ src/element/json/exception.hpp | 63 +++++++ src/element/json/value.cpp | 298 +++++++++++++++++++++++++++++++++ src/element/json/value.hpp | 127 ++++++++++++++ src/element/variant.hpp | 20 ++- 7 files changed, 610 insertions(+), 21 deletions(-) create mode 100644 src/element/json/conv.hpp create mode 100644 src/element/json/exception.hpp create mode 100644 src/element/json/value.cpp create mode 100644 src/element/json/value.hpp diff --git a/src/element/Makefile.am b/src/element/Makefile.am index f605b6235..96f9ee8b6 100644 --- a/src/element/Makefile.am +++ b/src/element/Makefile.am @@ -23,5 +23,6 @@ liblmn_elm_a_SOURCES = \ st.cpp st.h \ util.cpp util.h \ vector.cpp vector.h \ - life_time.cpp + life_time.cpp \ + json/value.cpp \ No newline at end of file diff --git a/src/element/element.h b/src/element/element.h index 7c371a335..2bf55e89b 100644 --- a/src/element/element.h +++ b/src/element/element.h @@ -44,29 +44,29 @@ */ #include "clock.h" +#include "conditional_ostream.hpp" #include "error.h" +#include "exception.hpp" #include "file_util.h" -#include "internal_hash.h" #include "instruction.hpp" +#include "internal_hash.h" +#include "life_time.hpp" #include "lmnstring.h" #include "lmntal_thread.h" #include "memory_pool.h" +#include "optional.hpp" #include "port.h" #include "process_util.h" #include "queue.h" -#include "st.h" -#include "util.h" -#include "vector.h" -#include "scope.hpp" +#include "range_remove_if.hpp" #include "re2c/buffer.hpp" #include "re2c/cfstream_buffer.hpp" #include "re2c/file_buffer.hpp" -#include "exception.hpp" -#include "variant.hpp" -#include "conditional_ostream.hpp" -#include "optional.hpp" -#include "range_remove_if.hpp" +#include "scope.hpp" +#include "st.h" #include "stack_trace.hpp" -#include "life_time.hpp" +#include "util.h" +#include "variant.hpp" +#include "vector.h" #endif /* LMN_ELEMENT_H */ diff --git a/src/element/json/conv.hpp b/src/element/json/conv.hpp new file mode 100644 index 000000000..c3ff39786 --- /dev/null +++ b/src/element/json/conv.hpp @@ -0,0 +1,98 @@ +/* + * conv.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SLIM_ELEMENT_JSON_CONV_HPP +#define SLIM_ELEMENT_JSON_CONV_HPP + +#include "value.hpp" + +namespace slim { +namespace element { +namespace json { + +/** + * Convert to JSON value. + * + * Allowed inputs are integers, floating points, booleans, std::string, + * std::vector, std::map, and std::unordered_map. + * + * Usage: + * json::value(42) --> 42 + * std::vector v = {1, 2, 3}; + * json::value(v) --> [1, 2, 3] + */ +template ::value && + !std::is_same::value, + std::nullptr_t>::type = nullptr> +inline json_t value(const T &v) { + return json::integer(v); +} +template ::value, + std::nullptr_t>::type = nullptr> +inline json_t value(const T &v) { + return json::real(v); +} +inline json_t value(bool v) { return json::boolean(v); } +inline json_t value(const std::string &v) { return json::string(v); } +template inline json_t value(const std::vector &v) { + array ary; + ary.value.reserve(v.size()); + for (auto &u : v) + ary.value.push_back(value(u)); + return ary; +} +template +inline json_t value(const std::unordered_map &v) { + object res; + for (auto &p : v) { + res[p.first] = value(p.second); + } + return res; +} +template inline json_t value(const std::map &v) { + object res; + for (auto &p : v) { + res[p.first] = value(p.second); + } + return res; +} + +} // namespace json +} // namespace element +} // namespace slim + +#endif /* SLIM_ELEMENT_JSON_CONV_HPP */ diff --git a/src/element/json/exception.hpp b/src/element/json/exception.hpp new file mode 100644 index 000000000..c22017051 --- /dev/null +++ b/src/element/json/exception.hpp @@ -0,0 +1,63 @@ +/* + * exception.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SLIM_ELEMENT_JSON_EXCEPTION_HPP +#define SLIM_ELEMENT_JSON_EXCEPTION_HPP + +#include +#include +#include + +namespace slim { +namespace element { +namespace json { +struct parse_error {}; + +struct overflow_error : parse_error, std::overflow_error { + overflow_error(std::istream::pos_type pos) + : std::overflow_error("occurred at " + std::to_string(pos)) {} +}; +struct syntax_error : parse_error, std::runtime_error { + syntax_error(const std::string &what_arg, std::istream::pos_type pos) + : std::runtime_error(what_arg + "(at " + std::to_string(pos) + ")") {} +}; + +} // namespace json +} // namespace element +} // namespace slim + +#endif /* SLIM_ELEMENT_JSON_EXCEPTION_HPP */ diff --git a/src/element/json/value.cpp b/src/element/json/value.cpp new file mode 100644 index 000000000..0ff350a44 --- /dev/null +++ b/src/element/json/value.cpp @@ -0,0 +1,298 @@ +/* + * value.cpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#include "value.hpp" + +#include "exception.hpp" + +#include +#include +#include + +// TODO: +// 一文字ずつ読むのはパフォーマンス的に問題あるかも？ +// エラー処理に入力位置を入れる（標準入力はtellgが効かない？） + +namespace slim { +namespace element { +namespace json { + +// for variant +namespace c17 = slim::element; + +using namespace slim::element; + +namespace { +constexpr bool is_sub_overflow_free(uint64_t a, uint64_t b) { + return a >= b; +} +constexpr bool is_add_overflow_free(uint64_t a, uint64_t b) { + return a <= std::numeric_limits::max() - b; +} +constexpr bool is_div_overflow_free(uint64_t a, uint64_t b) { + return b != 0u; +} +constexpr bool is_mul_overflow_free(uint64_t a, uint64_t b) { + return is_div_overflow_free(std::numeric_limits::max(), b) && + a <= std::numeric_limits::max() / b; +} + +// Read signed integral number with overflow check. +// throws json::overflow_error. +int64_t read_integral(std::istream &in, int &digits) { + uint64_t integral_part = 0; + digits = 0; + + // skip blanks + while (in && std::isspace(in.peek())) + in.ignore(); + + int sign = (in.peek() == '-') ? -1 : 1; + if (in.peek() == '+' || in.peek() == '-') { + in.ignore(); + } + + // skip blanks + while (in && std::isspace(in.peek())) + in.ignore(); + + while (in && std::isdigit(in.peek())) { + if (!is_mul_overflow_free(integral_part, 10)) + throw json::overflow_error(in.tellg()); + integral_part *= 10; + + char c = in.get(); + if (!is_add_overflow_free(integral_part, c - '0')) + throw json::overflow_error(in.tellg()); + integral_part += c - '0'; + digits++; + } + + // 値がint64_tで表せる範囲を超える + if (sign > 0 && integral_part > (uint64_t)std::numeric_limits::max()) + throw json::overflow_error(in.tellg()); + + // std::absをint64_tの最小値に適用するとint64_tで表せる範囲を超えてしまう. + // int64_tの負値表現が2の補数であることは規格により保証されているため、 + // ビット演算を用いて無理やり正しい絶対値を求める. + uint64_t min_abs = (((uint64_t)std::numeric_limits::min() - 1) ^ (uint64_t)(~0)); + if (sign < 0 && integral_part > min_abs) + throw json::overflow_error(in.tellg()); + + return sign * (int64_t)integral_part; +} +int64_t read_integral(std::istream &in) { + int digits; + return read_integral(in, digits); +} +} // namespace + +std::istream &operator>>(std::istream &in, value_type &value) { + char c = '\t'; + while (in && std::isspace(c)) + in.get(c); + + if (std::isdigit(c) || c == '+' || c == '-') { + in.unget(); + int64_t integral_part = read_integral(in); + + if (in.peek() != '.') { + value = json::integer(integral_part); + } else { + in.ignore(); + + // real number + if (in.peek() == '-' || in.peek() == '+') + throw json::syntax_error("fractional part must not be signed.", in.tellg()); + + int digits; + int64_t fractional_part = read_integral(in, digits); + + int exp = 0; + if (in.peek() == 'e') { + in.ignore(); + // read exponential part + + if (!std::isdigit(in.peek()) && in.peek() != '+' && in.peek() != '-') + throw json::syntax_error("unexpected character.", in.tellg()); + + exp = read_integral(in); + } + + int sign = std::signbit(integral_part) ? -1 : 1; + double ans = sign * + (std::abs((double)integral_part) + + (double)fractional_part * std::pow(10, -digits)) * + std::pow(10, exp); + value = json::real(ans); + } + + } else if (std::isalpha(c)) { // null, true, or false + std::string word; + while (in && isalpha(c)) { + word += c; + in.get(c); + } + + in.unget(); + + if (word == "null") + value = json::null(); + else if (word == "true") + value = json::boolean(true); + else if (word == "false") + value = json::boolean(false); + else + throw json::syntax_error("unexpected keyword '" + word + "'", in.tellg()); + + } else if (c == '\"') { + // TODO: escape sequence + std::string s; + in.get(c); + while (c != '\"') { + s += c; + if (!in) + throw json::syntax_error("unexpected end of file.", in.tellg()); + in.get(c); + } + value = json::string(s); + } else if (c == '{') { + std::unordered_map m; + while (true) { + json_t key; + in >> key; + + if (!c17::holds_alternative(key)) + throw json::syntax_error("a key of an object must be a string.", in.tellg()); + + do { + in.get(c); + } while (in && std::isspace(c)); + + if (c != ':') + throw json::syntax_error( + "elements of an object must be key-value pair.", in.tellg()); + + json_t value; + in >> value; + m[c17::get(key)] = value; + + do { + in.get(c); + } while (in && std::isspace(c)); + + if (c == '}') + break; + + if (!in) + throw json::syntax_error("unexpected end of file.", in.tellg()); + + if (c != ',') + throw json::syntax_error("expected ',' between key-value pairs.", in.tellg()); + } + + value = json::object(m); + } else if (c == '[') { + std::vector v; + while (true) { + json_t value; + in >> value; + v.push_back(value); + + do { + in.get(c); + } while (in && std::isspace(c)); + + if (c == ']') + break; + + if (!in) + throw json::syntax_error("unexpected end of file.", in.tellg()); + + if (c != ',') + throw json::syntax_error("expected ',' between elements.", in.tellg()); + } + + value = json::array(v); + } + + return in; +} + +struct pretty_printer { + std::ostream &os; + + pretty_printer(std::ostream &os) : os(os) {} + + void operator()(const json::null &value) { os << "null"; } + void operator()(const json::integer &value) { os << value.value; } + void operator()(const json::real &value) { os << value.value; } + void operator()(const json::string &value) { + os << "\"" << value.value << "\""; + } // TODO: escape sequences + void operator()(const json::boolean &value) { + os << (value.value ? "true" : "false"); + } + void operator()(const json::array &value) { + os << "["; + for (size_t i = 0; i < value.value.size(); i++) { + if (i > 0) + os << ", "; + c17::visit(*this, value.value[i]); + } + os << "]"; + } + void operator()(const json::object &value) { + os << "{"; + for (auto it = value.value.begin(); it != value.value.end(); ++it) { + if (it != value.value.begin()) + os << ", "; + os << "\"" << it->first << "\": "; + c17::visit(*this, it->second); + } + os << "}"; + } +}; + +std::ostream &operator<<(std::ostream &out, const json::value_type &value) { + c17::visit(pretty_printer(out), value); + return out; +} + +} // namespace json +} // namespace element +} // namespace slim diff --git a/src/element/json/value.hpp b/src/element/json/value.hpp new file mode 100644 index 000000000..e03e35ec8 --- /dev/null +++ b/src/element/json/value.hpp @@ -0,0 +1,127 @@ +/* + * value.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SLIM_ELEMENT_JSON_VALUE_HPP +#define SLIM_ELEMENT_JSON_VALUE_HPP + +#include "../variant.hpp" + +#include +#include +#include +#include +#include +#include +#include + +#include + +namespace slim { +namespace element { +namespace json { + +namespace c17 = ::slim::element; + +struct null; +struct integer; +struct real; +struct string; +struct boolean; +struct array; +struct object; + +using value_type = + c17::variant; + +struct null { + operator std::nullptr_t() { return nullptr; } +}; + +struct integer { + int64_t value; + + // 数値型は暗黙の型変換を行わない + explicit constexpr integer(int64_t v) : value(v) {} + operator int64_t() { return value; } +}; +struct real { + double value; + + // 数値型は暗黙の型変換は行わない + explicit constexpr real(double v) : value(v) {} + operator double() { return value; } +}; +struct boolean { + bool value; + + // 数値型は暗黙の型変換は行わない + constexpr explicit boolean(bool tf) : value(tf) {} + operator bool() { return value; } +}; +struct string { + std::string value; + + string(const std::string &str) : value(str) {} + operator std::string() { return value; } +}; +struct array { + std::vector value; + + array() {} + array(const std::vector &v) : value(v) {} + operator std::vector() { return value; } +}; +struct object { + std::unordered_map value; + + object() {} + object(const std::unordered_map &v) : value(v) {} + operator std::unordered_map() { return value; } +}; + +// throws json::syntax_error, json::overflow_error +std::istream &operator>>(std::istream &in, value_type &value); +std::ostream &operator<<(std::ostream &out, const value_type &value); + +} // namespace json + +using json_t = json::value_type; + +} // namespace element +} // namespace slim + +#endif /* SLIM_ELEMENT_JSON_VALUE_HPP */ diff --git a/src/element/variant.hpp b/src/element/variant.hpp index 35d72e05b..bb5931a6b 100644 --- a/src/element/variant.hpp +++ b/src/element/variant.hpp @@ -68,37 +68,37 @@ using variant_storage = template static constexpr auto variant_type_index() -> typename std::enable_if< - std::is_same::type, U>::value, size_t>::type { + std::is_convertible::type, U>::value, size_t>::type { return 0; } template static constexpr auto variant_type_index() -> typename std::enable_if< - !std::is_same::type, U>::value, size_t>::type { + !std::is_convertible::type, U>::value, size_t>::type { return 1 + variant_type_index(); } template static auto variant_store(void *p, T &&t) -> typename std::enable_if< - std::is_same::type>::value>::type { - ::new (p) typename std::decay::type(std::forward(t)); + std::is_convertible::type, U>::value>::type { + ::new (p) U(std::forward(t)); } template static auto variant_store(void *p, T &&t) -> typename std::enable_if< - !std::is_same::type>::value>::type { + !std::is_convertible::type, U>::value>::type { variant_store(p, std::forward(t)); } template static auto variant_store(void *p, const T &t) -> typename std::enable_if< - std::is_same::type>::value>::type { - ::new (p) typename std::decay::type(t); + std::is_convertible::type, U>::value>::type { + ::new (p) U(t); } template static auto variant_store(void *p, const T &t) -> typename std::enable_if< - !std::is_same::type>::value>::type { + !std::is_convertible::type, U>::value>::type { variant_store(p, t); } @@ -218,7 +218,9 @@ template struct variant { return *this; } - ~variant() { visit(deleter(), *this); } + ~variant() { + visit(deleter(), *this); + } size_t index() const { return index_; } From e7b8a4247fe22d37a3d121d7f618df069628b9ea Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Thu, 1 Aug 2019 00:57:57 +0900 Subject: [PATCH 2/8] Modify json::value_type. --- src/element/json/value.cpp | 37 +++++++++++++----------- src/element/json/value.hpp | 15 +++++----- src/element/variant.hpp | 58 ++++++++++++++++++-------------------- 3 files changed, 57 insertions(+), 53 deletions(-) diff --git a/src/element/json/value.cpp b/src/element/json/value.cpp index 0ff350a44..7b0dce5e9 100644 --- a/src/element/json/value.cpp +++ b/src/element/json/value.cpp @@ -39,6 +39,8 @@ #include "exception.hpp" +#include "../util.h" + #include #include #include @@ -54,6 +56,9 @@ namespace json { // for variant namespace c17 = slim::element; +// for make_unique +namespace c14 = slim::element; + using namespace slim::element; namespace { @@ -131,7 +136,7 @@ std::istream &operator>>(std::istream &in, value_type &value) { int64_t integral_part = read_integral(in); if (in.peek() != '.') { - value = json::integer(integral_part); + value = std::move(json::integer(integral_part)); } else { in.ignore(); @@ -207,9 +212,9 @@ std::istream &operator>>(std::istream &in, value_type &value) { throw json::syntax_error( "elements of an object must be key-value pair.", in.tellg()); - json_t value; - in >> value; - m[c17::get(key)] = value; + json_t v; + in >> v; + m[c17::get(key)] = std::move(v); do { in.get(c); @@ -225,13 +230,13 @@ std::istream &operator>>(std::istream &in, value_type &value) { throw json::syntax_error("expected ',' between key-value pairs.", in.tellg()); } - value = json::object(m); + value = c14::make_unique(std::move(m)); } else if (c == '[') { - std::vector v; + std::vector vs; while (true) { - json_t value; - in >> value; - v.push_back(value); + json_t v; + in >> v; + vs.push_back(std::move(v)); do { in.get(c); @@ -247,7 +252,7 @@ std::istream &operator>>(std::istream &in, value_type &value) { throw json::syntax_error("expected ',' between elements.", in.tellg()); } - value = json::array(v); + value = c14::make_unique(std::move(vs)); } return in; @@ -267,19 +272,19 @@ struct pretty_printer { void operator()(const json::boolean &value) { os << (value.value ? "true" : "false"); } - void operator()(const json::array &value) { + void operator()(const std::unique_ptr &value) { os << "["; - for (size_t i = 0; i < value.value.size(); i++) { + for (size_t i = 0; i < value->value.size(); i++) { if (i > 0) os << ", "; - c17::visit(*this, value.value[i]); + c17::visit(*this, value->value[i]); } os << "]"; } - void operator()(const json::object &value) { + void operator()(const std::unique_ptr &value) { os << "{"; - for (auto it = value.value.begin(); it != value.value.end(); ++it) { - if (it != value.value.begin()) + for (auto it = value->value.begin(); it != value->value.end(); ++it) { + if (it != value->value.begin()) os << ", "; os << "\"" << it->first << "\": "; c17::visit(*this, it->second); diff --git a/src/element/json/value.hpp b/src/element/json/value.hpp index e03e35ec8..3f2981ea0 100644 --- a/src/element/json/value.hpp +++ b/src/element/json/value.hpp @@ -43,13 +43,12 @@ #include #include #include +#include #include #include #include #include -#include - namespace slim { namespace element { namespace json { @@ -65,7 +64,8 @@ struct array; struct object; using value_type = - c17::variant; + c17::variant, + std::unique_ptr>; struct null { operator std::nullptr_t() { return nullptr; } @@ -102,15 +102,16 @@ struct array { std::vector value; array() {} - array(const std::vector &v) : value(v) {} - operator std::vector() { return value; } + array(std::vector &&v) : value(std::move(v)) {} + array(array &&v) : value(std::move(v.value)) {} + operator std::vector &&() { return std::move(value); } }; struct object { std::unordered_map value; object() {} - object(const std::unordered_map &v) : value(v) {} - operator std::unordered_map() { return value; } + object(std::unordered_map &&v) : value(std::move(v)) {} + operator std::unordered_map &&() { return std::move(value); } }; // throws json::syntax_error, json::overflow_error diff --git a/src/element/variant.hpp b/src/element/variant.hpp index bb5931a6b..8081ee4cc 100644 --- a/src/element/variant.hpp +++ b/src/element/variant.hpp @@ -74,7 +74,8 @@ static constexpr auto variant_type_index() -> typename std::enable_if< template static constexpr auto variant_type_index() -> typename std::enable_if< - !std::is_convertible::type, U>::value, size_t>::type { + !std::is_convertible::type, U>::value, + size_t>::type { return 1 + variant_type_index(); } @@ -90,41 +91,31 @@ static auto variant_store(void *p, T &&t) -> typename std::enable_if< variant_store(p, std::forward(t)); } -template -static auto variant_store(void *p, const T &t) -> typename std::enable_if< - std::is_convertible::type, U>::value>::type { - ::new (p) U(t); -} - -template -static auto variant_store(void *p, const T &t) -> typename std::enable_if< - !std::is_convertible::type, U>::value>::type { - variant_store(p, t); -} - template struct variant; template T &get(variant &v) { return *static_cast(static_cast(&v.storage_)); } +template T &&get(variant &&v) { + return std::move(*static_cast(static_cast(&v.storage_))); +} + template const T &get(const variant &v) { return *static_cast(static_cast(&v.storage_)); } -template +template ::type::type_tuple>::type> auto get(Variant &&v) - -> decltype(get::type::type_tuple>::type>( - std::forward(v))) { - return get::type::type_tuple>::type>( - std::forward(v)); + -> decltype(get(std::forward(v))) { + return get(std::forward(v)); } template ::type::type_tuple, + typename TypeTuple = typename std::remove_cv::type>::type::type_tuple, typename std::enable_if<(I == std::tuple_size::value - 1), std::nullptr_t>::type = nullptr> constexpr auto visit_impl(Visitor &&vis, Variant &&var) @@ -133,7 +124,7 @@ constexpr auto visit_impl(Visitor &&vis, Variant &&var) } template ::type::type_tuple, + typename TypeTuple = typename std::remove_cv::type>::type::type_tuple, typename std::enable_if<(I < std::tuple_size::value - 1), std::nullptr_t>::type = nullptr> constexpr auto visit_impl(Visitor &&vis, Variant &&var) @@ -162,9 +153,6 @@ template struct variant { template void operator()(T &&t) { variant_store(p, std::forward(t)); } - template void operator()(const T &t) { - variant_store(p, t); - } }; struct equalizer { @@ -195,8 +183,8 @@ template struct variant { } variant(variant &&other) noexcept { - visit(loader(&storage_), std::move(other)); index_ = other.index(); + visit(loader(&storage_), std::move(other)); } template struct variant { variant_store(&storage_, std::forward(t)); index_ = variant_type_index(); } + variant &operator=(const variant &rhs) { + visit(deleter(), *this); visit(loader(&storage_), rhs); index_ = rhs.index(); return *this; } - template variant &operator=(const variant &rhs) { + variant &operator=(variant &&rhs) { visit(deleter(), *this); - visit(loader(&storage_), rhs); index_ = rhs.index(); + visit(loader(&storage_), std::move(rhs)); return *this; } - - ~variant() { + template ::type>::value, + std::nullptr_t>::type = nullptr> + variant &operator=(T &&t) { visit(deleter(), *this); + variant_store(&storage_, std::forward(t)); + index_ = variant_type_index(); + return *this; } + ~variant() { visit(deleter(), *this); } + size_t index() const { return index_; } size_t index_; From 0f390110399dbdc71d9cc4c9ab435aa34051f412 Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Thu, 1 Aug 2019 20:26:31 +0900 Subject: [PATCH 3/8] Fix not reading an empty array or an empty object. --- src/element/json/conv.hpp | 63 +++++++++++++-------- src/element/json/value.cpp | 112 +++++++++++++++++++++---------------- 2 files changed, 105 insertions(+), 70 deletions(-) diff --git a/src/element/json/conv.hpp b/src/element/json/conv.hpp index c3ff39786..eb68fe2fe 100644 --- a/src/element/json/conv.hpp +++ b/src/element/json/conv.hpp @@ -40,9 +40,12 @@ #include "value.hpp" +#include "../util.h" + namespace slim { namespace element { -namespace json { + +namespace c14 = slim::element; // for make_unique /** * Convert to JSON value. @@ -54,44 +57,58 @@ namespace json { * json::value(42) --> 42 * std::vector v = {1, 2, 3}; * json::value(v) --> [1, 2, 3] + * + * If you want to convert user-defined types, all you have to do is to define + * 'to_json' function. + * + * Example: + * using namespace slim::element; + * struct Point { int x, y; }; + * json_t to_json(const Point &p) { + * return json::to_json(std::vector({p.x, p.y})); + * } */ template ::value && !std::is_same::value, std::nullptr_t>::type = nullptr> -inline json_t value(const T &v) { +inline json_t to_json(const T &v) { return json::integer(v); } template ::value, std::nullptr_t>::type = nullptr> -inline json_t value(const T &v) { +inline json_t to_json(const T &v) { return json::real(v); } -inline json_t value(bool v) { return json::boolean(v); } -inline json_t value(const std::string &v) { return json::string(v); } -template inline json_t value(const std::vector &v) { - array ary; - ary.value.reserve(v.size()); +inline json_t to_json(bool v) { return json::boolean(v); } +inline json_t to_json(const std::string &v) { return json::string(v); } + +// begin, endが定義されており, 要素がjson::valueで変換可能なデータ構造 +template +inline auto to_json(const Container &v) + -> decltype(begin(v), end(v), to_json(*begin(v)), json_t()) { + std::vector ary; + ary.reserve(v.size()); for (auto &u : v) - ary.value.push_back(value(u)); - return ary; + ary.push_back(to_json(u)); + return c14::make_unique(std::move(ary)); } -template -inline json_t value(const std::unordered_map &v) { - object res; - for (auto &p : v) { - res[p.first] = value(p.second); - } - return res; -} -template inline json_t value(const std::map &v) { - object res; + +// begin, endが定義されており, +// キーがstd::stringに変換可能で要素がjson::valueで変換可能なkey-value store +template < + class Container, + typename std::enable_if< + std::is_convertible::value, + std::nullptr_t>::type = nullptr> +inline auto to_json(const Container &v) + -> decltype(begin(v), end(v), to_json(begin(v)->second), json_t()) { + std::unordered_map res; for (auto &p : v) { - res[p.first] = value(p.second); + res[p.first] = to_json(p.second); } - return res; + return c14::make_unique(std::move(res)); } -} // namespace json } // namespace element } // namespace slim diff --git a/src/element/json/value.cpp b/src/element/json/value.cpp index 7b0dce5e9..d0f8daa74 100644 --- a/src/element/json/value.cpp +++ b/src/element/json/value.cpp @@ -41,8 +41,8 @@ #include "../util.h" -#include #include +#include #include // TODO: @@ -56,21 +56,16 @@ namespace json { // for variant namespace c17 = slim::element; -// for make_unique -namespace c14 = slim::element; +namespace c14 = slim::element; // for make_unique using namespace slim::element; namespace { -constexpr bool is_sub_overflow_free(uint64_t a, uint64_t b) { - return a >= b; -} +constexpr bool is_sub_overflow_free(uint64_t a, uint64_t b) { return a >= b; } constexpr bool is_add_overflow_free(uint64_t a, uint64_t b) { return a <= std::numeric_limits::max() - b; } -constexpr bool is_div_overflow_free(uint64_t a, uint64_t b) { - return b != 0u; -} +constexpr bool is_div_overflow_free(uint64_t a, uint64_t b) { return b != 0u; } constexpr bool is_mul_overflow_free(uint64_t a, uint64_t b) { return is_div_overflow_free(std::numeric_limits::max(), b) && a <= std::numeric_limits::max() / b; @@ -114,7 +109,8 @@ int64_t read_integral(std::istream &in, int &digits) { // std::absをint64_tの最小値に適用するとint64_tで表せる範囲を超えてしまう. // int64_tの負値表現が2の補数であることは規格により保証されているため、 // ビット演算を用いて無理やり正しい絶対値を求める. - uint64_t min_abs = (((uint64_t)std::numeric_limits::min() - 1) ^ (uint64_t)(~0)); + uint64_t min_abs = + (((uint64_t)std::numeric_limits::min() - 1) ^ (uint64_t)(~0)); if (sign < 0 && integral_part > min_abs) throw json::overflow_error(in.tellg()); @@ -142,7 +138,8 @@ std::istream &operator>>(std::istream &in, value_type &value) { // real number if (in.peek() == '-' || in.peek() == '+') - throw json::syntax_error("fractional part must not be signed.", in.tellg()); + throw json::syntax_error("fractional part must not be signed.", + in.tellg()); int digits; int64_t fractional_part = read_integral(in, digits); @@ -197,59 +194,80 @@ std::istream &operator>>(std::istream &in, value_type &value) { value = json::string(s); } else if (c == '{') { std::unordered_map m; - while (true) { - json_t key; - in >> key; - if (!c17::holds_alternative(key)) - throw json::syntax_error("a key of an object must be a string.", in.tellg()); + // skip blanks + while (in && std::isspace(in.peek())) + in.ignore(); + + if (in.peek() == '}') { + in.ignore(); + } else { + while (true) { + json_t key; + in >> key; - do { - in.get(c); - } while (in && std::isspace(c)); + if (!c17::holds_alternative(key)) + throw json::syntax_error("a key of an object must be a string.", + in.tellg()); - if (c != ':') - throw json::syntax_error( - "elements of an object must be key-value pair.", in.tellg()); + do { + in.get(c); + } while (in && std::isspace(c)); - json_t v; - in >> v; - m[c17::get(key)] = std::move(v); + if (c != ':') + throw json::syntax_error( + "elements of an object must be key-value pair.", in.tellg()); - do { - in.get(c); - } while (in && std::isspace(c)); + json_t v; + in >> v; + m[c17::get(key)] = std::move(v); - if (c == '}') - break; + do { + in.get(c); + } while (in && std::isspace(c)); - if (!in) - throw json::syntax_error("unexpected end of file.", in.tellg()); + if (c == '}') + break; - if (c != ',') - throw json::syntax_error("expected ',' between key-value pairs.", in.tellg()); + if (!in) + throw json::syntax_error("unexpected end of file.", in.tellg()); + + if (c != ',') + throw json::syntax_error("expected ',' between key-value pairs.", + in.tellg()); + } } value = c14::make_unique(std::move(m)); } else if (c == '[') { std::vector vs; - while (true) { - json_t v; - in >> v; - vs.push_back(std::move(v)); - do { - in.get(c); - } while (in && std::isspace(c)); + // skip blanks + while (in && std::isspace(in.peek())) + in.ignore(); + + if (in.peek() == ']') { + in.ignore(); + } else { + while (true) { + json_t v; + in >> v; + vs.push_back(std::move(v)); + + do { + in.get(c); + } while (in && std::isspace(c)); - if (c == ']') - break; + if (c == ']') + break; - if (!in) - throw json::syntax_error("unexpected end of file.", in.tellg()); + if (!in) + throw json::syntax_error("unexpected end of file.", in.tellg()); - if (c != ',') - throw json::syntax_error("expected ',' between elements.", in.tellg()); + if (c != ',') + throw json::syntax_error("expected ',' between elements.", + in.tellg()); + } } value = c14::make_unique(std::move(vs)); From 672ba7ce4733cdc8ce83976b3de6516456eec847 Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Fri, 2 Aug 2019 23:26:41 +0900 Subject: [PATCH 4/8] Add json::value_ptr. --- src/element/json/conv.hpp | 45 +++++++++++++++------------------- src/element/json/value.cpp | 8 +++--- src/element/json/value.hpp | 50 ++++++++++++++++++++++++++++++++------ 3 files changed, 66 insertions(+), 37 deletions(-) diff --git a/src/element/json/conv.hpp b/src/element/json/conv.hpp index eb68fe2fe..6d07f76e2 100644 --- a/src/element/json/conv.hpp +++ b/src/element/json/conv.hpp @@ -40,13 +40,9 @@ #include "value.hpp" -#include "../util.h" - namespace slim { namespace element { -namespace c14 = slim::element; // for make_unique - /** * Convert to JSON value. * @@ -81,33 +77,30 @@ inline json_t to_json(const T &v) { } inline json_t to_json(bool v) { return json::boolean(v); } inline json_t to_json(const std::string &v) { return json::string(v); } - -// begin, endが定義されており, 要素がjson::valueで変換可能なデータ構造 -template -inline auto to_json(const Container &v) - -> decltype(begin(v), end(v), to_json(*begin(v)), json_t()) { - std::vector ary; - ary.reserve(v.size()); +template inline json_t to_json(const std::vector &v) { + json::value_ptr ary(new json::array); + ary->value.reserve(v.size()); for (auto &u : v) - ary.push_back(to_json(u)); - return c14::make_unique(std::move(ary)); + ary->value.push_back(to_json(u)); + return ary; } - -// begin, endが定義されており, -// キーがstd::stringに変換可能で要素がjson::valueで変換可能なkey-value store -template < - class Container, - typename std::enable_if< - std::is_convertible::value, - std::nullptr_t>::type = nullptr> -inline auto to_json(const Container &v) - -> decltype(begin(v), end(v), to_json(begin(v)->second), json_t()) { - std::unordered_map res; +template +inline json_t to_json(const std::unordered_map &v) { + json::value_ptr res(new json::object); + for (auto &p : v) { + res->value[p.first] = to_json(p.second); + } + return res; +} +template inline json_t to_json(const std::map &v) { + json::value_ptr res(new json::object); for (auto &p : v) { - res[p.first] = to_json(p.second); + res->value[p.first] = to_json(p.second); } - return c14::make_unique(std::move(res)); + return res; } +inline json_t to_json(const json_t &v) { return v; } +inline json_t to_json(json_t &&v) { return std::move(v); } } // namespace element } // namespace slim diff --git a/src/element/json/value.cpp b/src/element/json/value.cpp index d0f8daa74..daf3ef422 100644 --- a/src/element/json/value.cpp +++ b/src/element/json/value.cpp @@ -238,7 +238,7 @@ std::istream &operator>>(std::istream &in, value_type &value) { } } - value = c14::make_unique(std::move(m)); + value = value_ptr(new json::object(m)); } else if (c == '[') { std::vector vs; @@ -270,7 +270,7 @@ std::istream &operator>>(std::istream &in, value_type &value) { } } - value = c14::make_unique(std::move(vs)); + value = value_ptr(new json::array(vs)); } return in; @@ -290,7 +290,7 @@ struct pretty_printer { void operator()(const json::boolean &value) { os << (value.value ? "true" : "false"); } - void operator()(const std::unique_ptr &value) { + void operator()(const value_ptr &value) { os << "["; for (size_t i = 0; i < value->value.size(); i++) { if (i > 0) @@ -299,7 +299,7 @@ struct pretty_printer { } os << "]"; } - void operator()(const std::unique_ptr &value) { + void operator()(const value_ptr &value) { os << "{"; for (auto it = value->value.begin(); it != value->value.end(); ++it) { if (it != value->value.begin()) diff --git a/src/element/json/value.hpp b/src/element/json/value.hpp index 3f2981ea0..fc3bc57b9 100644 --- a/src/element/json/value.hpp +++ b/src/element/json/value.hpp @@ -63,9 +63,43 @@ struct boolean; struct array; struct object; -using value_type = - c17::variant, - std::unique_ptr>; +// smart pointer which deeply copies a pointed object. +template struct value_ptr { + value_ptr() : ptr_(nullptr) {} + value_ptr(T *ptr) : ptr_(ptr) {} + ~value_ptr() { delete ptr_; } + + // copy constructor + value_ptr(const value_ptr &ptr) : ptr_(new T(*ptr)) {} + + // move constructor + value_ptr(value_ptr &&ptr) : ptr_(ptr.ptr_) { ptr.ptr_ = nullptr; } + + T &operator*() { return *ptr_; } + const T &operator*() const { return *ptr_; } + T *operator->() { return ptr_; } + const T *operator->() const { return ptr_; } + + // copy assignment operator + value_ptr &operator=(const value_ptr &ptr) { + delete ptr_; + ptr.ptr_ = new T(*ptr); + return *this; + } + + // move assignment operator + value_ptr &operator=(value_ptr &&ptr) { + delete ptr_; + ptr.ptr_ = ptr.ptr_; + return *this; + } + +private: + T *ptr_; +}; + +using value_type = c17::variant, value_ptr>; struct null { operator std::nullptr_t() { return nullptr; } @@ -102,16 +136,18 @@ struct array { std::vector value; array() {} + array(const std::vector &v) : value(v) {} array(std::vector &&v) : value(std::move(v)) {} - array(array &&v) : value(std::move(v.value)) {} - operator std::vector &&() { return std::move(value); } + operator std::vector() { return value; } }; struct object { std::unordered_map value; object() {} - object(std::unordered_map &&v) : value(std::move(v)) {} - operator std::unordered_map &&() { return std::move(value); } + object(const std::unordered_map &v) : value(v) {} + object(std::unordered_map &&v) + : value(std::move(v)) {} + operator std::unordered_map() { return value; } }; // throws json::syntax_error, json::overflow_error From 62ce000c390d83b8ca336123d54e2af57051fc31 Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Sat, 3 Aug 2019 00:15:47 +0900 Subject: [PATCH 5/8] Add conversion function from StateSpace to json. --- src/element/json/conv.hpp | 6 +- src/verifier/Makefile.am | 3 +- src/verifier/json.cpp | 132 ++++++++++++++++++++++++++++++++++++++ src/verifier/json.hpp | 51 +++++++++++++++ 4 files changed, 190 insertions(+), 2 deletions(-) create mode 100644 src/verifier/json.cpp create mode 100644 src/verifier/json.hpp diff --git a/src/element/json/conv.hpp b/src/element/json/conv.hpp index 6d07f76e2..69eb339b7 100644 --- a/src/element/json/conv.hpp +++ b/src/element/json/conv.hpp @@ -75,7 +75,11 @@ template ::value, inline json_t to_json(const T &v) { return json::real(v); } -inline json_t to_json(bool v) { return json::boolean(v); } +template ::value, + std::nullptr_t>::type = nullptr> +inline json_t to_json(T v) { + return json::boolean(v); +} inline json_t to_json(const std::string &v) { return json::string(v); } template inline json_t to_json(const std::vector &v) { json::value_ptr ary(new json::array); diff --git a/src/verifier/Makefile.am b/src/verifier/Makefile.am index db422c983..cf445f528 100644 --- a/src/verifier/Makefile.am +++ b/src/verifier/Makefile.am @@ -42,7 +42,8 @@ liblmn_verifier_a_SOURCES = \ visitlog.h \ stack_macro.h \ state_dumper.cpp \ - mem_encode/decoder.cpp mem_encode/binstr.cpp + mem_encode/decoder.cpp mem_encode/binstr.cpp \ + json.cpp EXTRA_DIST = $(PARSER_SOURCE) $(PARSER_HEADER) diff --git a/src/verifier/json.cpp b/src/verifier/json.cpp new file mode 100644 index 000000000..cdde0177f --- /dev/null +++ b/src/verifier/json.cpp @@ -0,0 +1,132 @@ +/* + * json.cpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#include "json.hpp" + +#include "statespace.h" + +#include "element/element.h" + +#include "element/json/conv.hpp" +#include "element/json/value.hpp" + +#include +#include +#include + +using namespace slim::element; + +json_t to_json(State *s) { + auto org_next_id = env_next_id(); + auto mem = s->restore_membrane_inner(FALSE); + env_set_next_id(org_next_id); + + json_t res = json::string(slim::to_string_membrane(mem)); + + if (s->is_binstr_user()) { + mem->free_rec(); + } + return res; +} + +json_t to_json(StateSpace *ss) { + std::unordered_map res; + auto states = ss->all_states(); + if (lmn_env.sp_dump_format != INCREMENTAL) { + std::vector> sts; + for (auto &s : states) { + /* Rehashが発生している場合, + * dummyフラグが真かつエンコード済みフラグが偽のStateオブジェクトが存在する. + * このようなStateオブジェクトのバイナリストリングは + * Rehashされた側のテーブルに存在するStateオブジェクトに登録されているためcontinueする. + */ + if (s->is_dummy() && !s->is_encoded()) + continue; + + /* この時点で状態は, ノーマル || (dummyフラグが立っている && + * エンコード済)である. dummyならば, + * バイナリストリング以外のデータはオリジナル側(parent)に記録している. */ + State *target = !s->is_dummy() ? s : state_get_parent(s); + auto print_id = ss ? state_format_id(target, ss->is_formatted()) : target->state_id; + BOOL has_property = ss && ss->has_property(); + std::unordered_map state; + state["id"] = json::integer(print_id); + state["process"] = to_json(s); + if (has_property) + state["property"] = json::string(ss->automata()->state_name(state_property_state(s))); + +#ifdef KWBT_OPT + state["cost"] = cost; +#endif + sts.push_back(state); + } + res["states"] = slim::element::to_json(sts); + } + res["init"] = slim::element::to_json( + state_format_id(ss->initial_state(), ss->is_formatted())); + + std::unordered_map>> + transitions; + for (auto &s : states) { + if (s->is_dummy() && s->is_encoded()) + continue; + + std::vector> succ; + if (s->successors) { + for (int i = 0; i < s->successor_num; i++) { + /* MEMO: rehashが発生していても, successorポインタを辿る先は, オリジナル + */ + std::unordered_map ts; + ts["succ"] = slim::element::to_json( + state_format_id(state_succ_state(s, i), ss->is_formatted())); + + if (s->has_trans_obj()) { + auto t = transition(s, i); + std::vector rules; + for (int j = 0; j < transition_rule_num(t); j++) + rules.push_back(lmn_id_to_name(transition_rule(t, j))); + ts["rules"] = slim::element::to_json(rules); + } + succ.push_back(ts); + } + } + transitions[std::to_string(state_format_id(s, ss->is_formatted()))] = succ; + } + res["transitions"] = slim::element::to_json(std::move(transitions)); + return to_json(res); +} diff --git a/src/verifier/json.hpp b/src/verifier/json.hpp new file mode 100644 index 000000000..b685ddd24 --- /dev/null +++ b/src/verifier/json.hpp @@ -0,0 +1,51 @@ +/* + * json.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SLIM_VERIFIER_JSON_HPP +#define SLIM_VERIFIER_JSON_HPP + +#include "element/json/value.hpp" + +struct State; +struct StateSpace; + +slim::element::json_t to_json(State *s); +slim::element::json_t to_json(StateSpace *ss); + +// TODO: グローバル名前空間ではなくADLを使える名前空間に移動する + +#endif /* SLIM_VERIFIER_JSON_HPP */ From b6bb840237c072204244900c761006eb1ead251a Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Tue, 8 Oct 2019 23:18:50 +0900 Subject: [PATCH 6/8] Add dump-json mode of state spaces. --- src/element/element.h | 4 + src/element/json/value.cpp | 34 ++++- src/element/json/value.hpp | 9 +- src/env.cpp | 2 +- src/lmntal.h | 8 +- src/main.cpp | 11 +- src/verifier/Makefile.am | 3 +- src/verifier/json.hpp | 51 ------- .../{json.cpp => json/statespace.hpp} | 129 ++++++++++++------ src/verifier/mc.cpp | 14 +- src/verifier/mc_worker.cpp | 2 +- src/verifier/state_dumper.cpp | 24 ++++ 12 files changed, 173 insertions(+), 118 deletions(-) delete mode 100644 src/verifier/json.hpp rename src/verifier/{json.cpp => json/statespace.hpp} (53%) diff --git a/src/element/element.h b/src/element/element.h index 2bf55e89b..ed2e88147 100644 --- a/src/element/element.h +++ b/src/element/element.h @@ -69,4 +69,8 @@ #include "variant.hpp" #include "vector.h" +#include "json/conv.hpp" +#include "json/exception.hpp" +#include "json/value.hpp" + #endif /* LMN_ELEMENT_H */ diff --git a/src/element/json/value.cpp b/src/element/json/value.cpp index daf3ef422..59c17b06a 100644 --- a/src/element/json/value.cpp +++ b/src/element/json/value.cpp @@ -56,7 +56,7 @@ namespace json { // for variant namespace c17 = slim::element; -namespace c14 = slim::element; // for make_unique +namespace c14 = slim::element; // for make_unique using namespace slim::element; @@ -277,9 +277,10 @@ std::istream &operator>>(std::istream &in, value_type &value) { } struct pretty_printer { + unsigned int indent; std::ostream &os; - pretty_printer(std::ostream &os) : os(os) {} + pretty_printer(std::ostream &os) : os(os), indent(0) {} void operator()(const json::null &value) { os << "null"; } void operator()(const json::integer &value) { os << value.value; } @@ -292,23 +293,48 @@ struct pretty_printer { } void operator()(const value_ptr &value) { os << "["; + + indent++; for (size_t i = 0; i < value->value.size(); i++) { if (i > 0) - os << ", "; + os << ","; + os << "\n"; + print_indent(); c17::visit(*this, value->value[i]); } + indent--; + + if (!value->value.empty()) { + os << "\n"; + print_indent(); + } os << "]"; } void operator()(const value_ptr &value) { os << "{"; + + indent++; for (auto it = value->value.begin(); it != value->value.end(); ++it) { if (it != value->value.begin()) - os << ", "; + os << ","; + os << "\n"; + print_indent(); os << "\"" << it->first << "\": "; c17::visit(*this, it->second); } + indent--; + + if (!value->value.empty()) { + os << "\n"; + print_indent(); + } os << "}"; } + + void print_indent() { + for (int i = 0; i < indent; i++) + os << " "; + } }; std::ostream &operator<<(std::ostream &out, const json::value_type &value) { diff --git a/src/element/json/value.hpp b/src/element/json/value.hpp index fc3bc57b9..88eebcbb6 100644 --- a/src/element/json/value.hpp +++ b/src/element/json/value.hpp @@ -98,8 +98,11 @@ template struct value_ptr { T *ptr_; }; -using value_type = c17::variant, value_ptr>; +using array_t = value_ptr; +using object_t = value_ptr; + +using value_type = + c17::variant; struct null { operator std::nullptr_t() { return nullptr; } @@ -148,6 +151,8 @@ struct object { object(std::unordered_map &&v) : value(std::move(v)) {} operator std::unordered_map() { return value; } + + value_type &operator[](const std::string &key) { return value[key]; } }; // throws json::syntax_error, json::overflow_error diff --git a/src/env.cpp b/src/env.cpp index ae1c65872..b5467c4eb 100644 --- a/src/env.cpp +++ b/src/env.cpp @@ -140,7 +140,7 @@ LmnEnv::LmnEnv() { this->show_chr = FALSE; this->show_ruleset = TRUE; this->output_format = DEFAULT; - this->mc_dump_format = CUI; + this->mc_dump_format = MCdumpFormat::CUI; this->sp_dump_format = SP_NONE; this->nd = FALSE; this->ltl = FALSE; diff --git a/src/lmntal.h b/src/lmntal.h index c8b1544b7..3a8cd6b46 100644 --- a/src/lmntal.h +++ b/src/lmntal.h @@ -220,7 +220,7 @@ LMN_EXTERN void lmn_free(void *p); /* 階層グラフ構造の出力形式 */ enum OutputFormat { DEFAULT = 1, DEV, DOT, JSON }; -enum MCdumpFormat { CUI, LaViT, Dir_DOT, LMN_FSM_GRAPH, LMN_FSM_GRAPH_MEM_NODE, LMN_FSM_GRAPH_HL_NODE }; +enum class MCdumpFormat { CUI, LaViT, Dir_DOT, LMN_FSM_GRAPH, LMN_FSM_GRAPH_MEM_NODE, LMN_FSM_GRAPH_HL_NODE, JSON }; enum SPdumpFormat { SP_NONE, INCREMENTAL, LMN_SYNTAX }; /* 最適化実行 */ @@ -551,6 +551,12 @@ static constexpr bool profile = true; #else static constexpr bool profile = false; #endif + +#ifdef KWBT_OPT +static constexpr bool kwbt_opt = true; +#else +static constexpr bool kwbt_opt = false; +#endif } // namespace config } // namespace slim diff --git a/src/main.cpp b/src/main.cpp index 9d600c9a9..01c1d9bdc 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -301,13 +301,13 @@ static void parse_options(int *optid, int argc, char *argv[]) { break; case 1100: lmn_env.output_format = DOT; - lmn_env.mc_dump_format = Dir_DOT; + lmn_env.mc_dump_format = MCdumpFormat::Dir_DOT; break; case 1101: - lmn_env.mc_dump_format = LMN_FSM_GRAPH_MEM_NODE; + lmn_env.mc_dump_format = MCdumpFormat::LMN_FSM_GRAPH_MEM_NODE; break; case 1102: - lmn_env.mc_dump_format = LaViT; + lmn_env.mc_dump_format = MCdumpFormat::LaViT; break; case 1103: lmn_env.sp_dump_format = INCREMENTAL; @@ -317,12 +317,13 @@ static void parse_options(int *optid, int argc, char *argv[]) { break; case 1105: lmn_env.output_format = JSON; + lmn_env.mc_dump_format = MCdumpFormat::JSON; break; case 1106: - lmn_env.mc_dump_format = LMN_FSM_GRAPH; + lmn_env.mc_dump_format = MCdumpFormat::LMN_FSM_GRAPH; break; case 1107: - lmn_env.mc_dump_format = LMN_FSM_GRAPH_HL_NODE; + lmn_env.mc_dump_format = MCdumpFormat::LMN_FSM_GRAPH_HL_NODE; break; case 1200: /* jni interactive mode */ #ifdef HAVE_JNI_H diff --git a/src/verifier/Makefile.am b/src/verifier/Makefile.am index cf445f528..db422c983 100644 --- a/src/verifier/Makefile.am +++ b/src/verifier/Makefile.am @@ -42,8 +42,7 @@ liblmn_verifier_a_SOURCES = \ visitlog.h \ stack_macro.h \ state_dumper.cpp \ - mem_encode/decoder.cpp mem_encode/binstr.cpp \ - json.cpp + mem_encode/decoder.cpp mem_encode/binstr.cpp EXTRA_DIST = $(PARSER_SOURCE) $(PARSER_HEADER) diff --git a/src/verifier/json.hpp b/src/verifier/json.hpp deleted file mode 100644 index b685ddd24..000000000 --- a/src/verifier/json.hpp +++ /dev/null @@ -1,51 +0,0 @@ -/* - * json.hpp - * - * Copyright (c) 2019, Ueda Laboratory LMNtal Group - * - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * 1. Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * - * 2. Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the - * distribution. - * - * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the - * names of its contributors may be used to endorse or promote - * products derived from this software without specific prior - * written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS - * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT - * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR - * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT - * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, - * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT - * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, - * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY - * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT - * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - */ - -#ifndef SLIM_VERIFIER_JSON_HPP -#define SLIM_VERIFIER_JSON_HPP - -#include "element/json/value.hpp" - -struct State; -struct StateSpace; - -slim::element::json_t to_json(State *s); -slim::element::json_t to_json(StateSpace *ss); - -// TODO: グローバル名前空間ではなくADLを使える名前空間に移動する - -#endif /* SLIM_VERIFIER_JSON_HPP */ diff --git a/src/verifier/json.cpp b/src/verifier/json/statespace.hpp similarity index 53% rename from src/verifier/json.cpp rename to src/verifier/json/statespace.hpp index cdde0177f..19da10005 100644 --- a/src/verifier/json.cpp +++ b/src/verifier/json/statespace.hpp @@ -1,5 +1,5 @@ /* - * json.cpp + * verifier/json/statespace.hpp * * Copyright (c) 2019, Ueda Laboratory LMNtal Group * @@ -35,39 +35,75 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ -#include "json.hpp" +#ifndef SLIM_VERIFIER_JSON_STATESPACE_HPP +#define SLIM_VERIFIER_JSON_STATESPACE_HPP -#include "statespace.h" +#include "../statespace.h" #include "element/element.h" -#include "element/json/conv.hpp" -#include "element/json/value.hpp" - -#include -#include #include -using namespace slim::element; +namespace slim { +namespace verifier { +namespace json { + +namespace c17 = slim::element; +using slim::element::json_t; + +/** + * 状態をjsonフォーマットで出力する. + * + * Example: + * { "string": (文字列表現) } + */ +element::json::object_t to_json(State &s) { + using slim::element::to_json; -json_t to_json(State *s) { auto org_next_id = env_next_id(); - auto mem = s->restore_membrane_inner(FALSE); + auto mem = s.restore_membrane_inner(FALSE); env_set_next_id(org_next_id); - json_t res = json::string(slim::to_string_membrane(mem)); + // 本当はJSONで出したいのだが文字列くらいしかダンプする方法がないので仕方なく + // いつかやりたいところ + lmn_env.output_format = DEFAULT; + json_t string_rep = to_json(slim::to_string_membrane(mem)); + lmn_env.output_format = JSON; - if (s->is_binstr_user()) { + if (s.is_binstr_user()) { mem->free_rec(); } - return res; + + std::unordered_map res; + res["string"] = string_rep; + return c17::get(to_json(res)); } -json_t to_json(StateSpace *ss) { +/** + * 状態空間をjsonフォーマットで出力する. + * + * Example: + * { + * "size": (状態数), + * "init": "(状態ID)": { "string": (文字列表現) }, ... + * } "transitions": { "(状態ID)": [ { "ID": "(状態ID)", + * "label": { ... } }, ...] } + * } + */ +inline element::json_t to_json(StateSpace &ss) { + using slim::element::to_json; std::unordered_map res; - auto states = ss->all_states(); + auto states = ss.all_states(); + + res["size"] = to_json(states.size()); + res["end_size"] = to_json(ss.num_of_ends()); + res["init"] = to_json( + std::to_string(state_format_id(ss.initial_state(), ss.is_formatted()))); + if (lmn_env.sp_dump_format != INCREMENTAL) { - std::vector> sts; + std::unordered_map states_json; + for (auto &s : states) { /* Rehashが発生している場合, * dummyフラグが真かつエンコード済みフラグが偽のStateオブジェクトが存在する. @@ -77,56 +113,61 @@ json_t to_json(StateSpace *ss) { if (s->is_dummy() && !s->is_encoded()) continue; - /* この時点で状態は, ノーマル || (dummyフラグが立っている && - * エンコード済)である. dummyならば, - * バイナリストリング以外のデータはオリジナル側(parent)に記録している. */ - State *target = !s->is_dummy() ? s : state_get_parent(s); - auto print_id = ss ? state_format_id(target, ss->is_formatted()) : target->state_id; - BOOL has_property = ss && ss->has_property(); - std::unordered_map state; - state["id"] = json::integer(print_id); - state["process"] = to_json(s); - if (has_property) - state["property"] = json::string(ss->automata()->state_name(state_property_state(s))); + // 状態をjsonに変換（ここは明示的に名前空間を指定する必要がある） + auto state = verifier::json::to_json(*s); + + // 状態空間における付加情報 + if (ss.has_property()) + (*state)["property"] = + std::string(ss.automata()->state_name(state_property_state(s))); #ifdef KWBT_OPT - state["cost"] = cost; + (*state)["cost"] = cost; #endif - sts.push_back(state); + + /* この時点で状態は, ノーマル || (dummyフラグが立っている && + * エンコード済)である. dummyならば, + * バイナリストリング以外のデータはオリジナル側(parent)に記録している. */ + auto original = s->is_dummy() ? state_get_parent(s) : s; + auto print_id = state_format_id(original, ss.is_formatted()); + states_json[std::to_string(print_id)] = state; } - res["states"] = slim::element::to_json(sts); + + res["states"] = to_json(states_json); } - res["init"] = slim::element::to_json( - state_format_id(ss->initial_state(), ss->is_formatted())); - std::unordered_map>> - transitions; + using transition_t = std::vector>; + std::unordered_map transitions; for (auto &s : states) { if (s->is_dummy() && s->is_encoded()) continue; - std::vector> succ; + transition_t succ; if (s->successors) { for (int i = 0; i < s->successor_num; i++) { - /* MEMO: rehashが発生していても, successorポインタを辿る先は, オリジナル - */ + /* MEMO: rehashが発生していてもsuccessorポインタを辿る先は変わらない */ std::unordered_map ts; - ts["succ"] = slim::element::to_json( - state_format_id(state_succ_state(s, i), ss->is_formatted())); + ts["succ"] = std::to_string( + state_format_id(state_succ_state(s, i), ss.is_formatted())); if (s->has_trans_obj()) { auto t = transition(s, i); std::vector rules; for (int j = 0; j < transition_rule_num(t); j++) rules.push_back(lmn_id_to_name(transition_rule(t, j))); - ts["rules"] = slim::element::to_json(rules); + ts["rules"] = to_json(rules); } succ.push_back(ts); } } - transitions[std::to_string(state_format_id(s, ss->is_formatted()))] = succ; + transitions[std::to_string(state_format_id(s, ss.is_formatted()))] = succ; } - res["transitions"] = slim::element::to_json(std::move(transitions)); + res["transitions"] = to_json(std::move(transitions)); + return to_json(res); } +} +} +} + +#endif /* SLIM_VERIFIER_JSON_STATESPACE_HPP */ diff --git a/src/verifier/mc.cpp b/src/verifier/mc.cpp index cf6be446e..7a64f0ae6 100644 --- a/src/verifier/mc.cpp +++ b/src/verifier/mc.cpp @@ -155,14 +155,14 @@ static void mc_dump(LmnWorkerGroup *wp) { auto out = ss->output(); if (wp->workers_are_do_search()) { mc_dump_all_errors(wp, out); - } else if (lmn_env.end_dump && lmn_env.mc_dump_format == CUI) { + } else if (lmn_env.end_dump && lmn_env.mc_dump_format == MCdumpFormat::CUI) { /* とりあえず最終状態集合の出力はCUI限定。(LaViTに受付フォーマットがない) */ ss->dump_ends(); } /* CUIモードの場合状態数などのデータも標準出力 */ - if (lmn_env.mc_dump_format == CUI) { + if (lmn_env.mc_dump_format == MCdumpFormat::CUI) { fprintf(out, "\'# of States\'(stored) = %lu.\n", ss->num()); fprintf(out, "\'# of States\'(end) = %lu.\n", @@ -815,13 +815,13 @@ void mc_print_vec_states(StateSpaceRef ss, Vector *v, State *seed) { void mc_dump_all_errors(LmnWorkerGroup *wp, FILE *f) { if (!wp->workers_have_error()) { fprintf(f, "%s\n", - lmn_env.mc_dump_format == CUI + lmn_env.mc_dump_format == MCdumpFormat::CUI ? "No Accepting Cycle (or Invalid State) exists." : ""); } else { switch (lmn_env.mc_dump_format) { - case LaViT: - case CUI: { + case MCdumpFormat::LaViT: + case MCdumpFormat::CUI: { st_table_t invalids_graph; unsigned int i, j; BOOL cui_dump; @@ -830,7 +830,7 @@ void mc_dump_all_errors(LmnWorkerGroup *wp, FILE *f) { lmn_env.sp_dump_format == LMN_SYNTAX ? "counter_exapmle." : "CounterExamplePaths"); - cui_dump = (lmn_env.mc_dump_format == CUI); + cui_dump = (lmn_env.mc_dump_format == MCdumpFormat::CUI); invalids_graph = cui_dump ? NULL : st_init_ptrtable(); /* state property */ @@ -909,7 +909,7 @@ void mc_dump_all_errors(LmnWorkerGroup *wp, FILE *f) { break; } - case Dir_DOT: /* TODO: + case MCdumpFormat::Dir_DOT: /* TODO: 反例パスをサブグラフとして指定させたら分かりやすくなりそう */; default: diff --git a/src/verifier/mc_worker.cpp b/src/verifier/mc_worker.cpp index c64460fd0..7535a81a5 100644 --- a/src/verifier/mc_worker.cpp +++ b/src/verifier/mc_worker.cpp @@ -443,7 +443,7 @@ BOOL LmnWorkerGroup::flags_init(AutomataRef property_a) {// this should be in Lm if (lmn_env.sp_dump_format == INCREMENTAL) { mc_set_dump(flags); lmn_env.dump = TRUE; - if (lmn_env.mc_dump_format != CUI && lmn_env.mc_dump_format != LaViT) { + if (lmn_env.mc_dump_format != MCdumpFormat::CUI && lmn_env.mc_dump_format != MCdumpFormat::LaViT) { lmn_fatal("unsupported incremental output format"); } fprintf(stdout, "States\n"); diff --git a/src/verifier/state_dumper.cpp b/src/verifier/state_dumper.cpp index d68a6cc0b..3d56500f3 100644 --- a/src/verifier/state_dumper.cpp +++ b/src/verifier/state_dumper.cpp @@ -38,6 +38,9 @@ #include "state_dumper.h" #include "statespace.h" +#include "json/statespace.hpp" + +#include namespace state_dumper { class CUI : public StateDumper { @@ -128,6 +131,25 @@ class LMN_FSM_GRAPH_HL_NODE : public StateDumper { void dump(StateSpace *ss) override; }; + +class JSON : public StateDumper { + friend StateDumper; + using StateDumper::StateDumper; + + void dump(StateSpace *ss) override { + std::stringstream os; + os << slim::verifier::json::to_json(*ss) << std::endl; + fprintf(_fp, "%s", os.str().c_str()); + } + + // 使わない + MCdumpFormat dump_format() const override { return MCdumpFormat::JSON; } + bool need_id_foreach_trans() const override { return true; } + std::string state_separator() const override { return ""; } + std::string trans_separator() const override { return ""; } + std::string label_begin() const override { return ""; } + std::string label_end() const override { return ""; } +}; } // namespace state_dumper StateDumper *StateDumper::from_env_ptr(FILE *fp) { @@ -144,6 +166,8 @@ StateDumper *StateDumper::from_env_ptr(FILE *fp) { return new state_dumper::LMN_FSM_GRAPH_MEM_NODE(fp); case MCdumpFormat::LMN_FSM_GRAPH_HL_NODE: return new state_dumper::LMN_FSM_GRAPH_HL_NODE(fp); + case MCdumpFormat::JSON: + return new state_dumper::JSON(fp); default: throw std::runtime_error("invalid mc dump format."); } From c3f1d2e07ba5478c8af0cb41078fe020f5d5b0f3 Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Fri, 11 Oct 2019 01:21:13 +0900 Subject: [PATCH 7/8] Add state space checker. --- num | 0 src/Makefile.am | 9 +- src/element/json/exception.hpp | 6 +- src/element/json/value.hpp | 17 +++ src/element/variant.hpp | 7 +- src/ssc/check_result.hpp | 70 ++++++++++ src/ssc/identity.hpp | 83 +++++++++++ src/ssc/isomorphism.hpp | 151 ++++++++++++++++++++ src/ssc/main.cpp | 242 +++++++++++++++++++++++++++++++++ src/ssc/state_space.hpp | 134 ++++++++++++++++++ 10 files changed, 713 insertions(+), 6 deletions(-) delete mode 100644 num create mode 100644 src/ssc/check_result.hpp create mode 100644 src/ssc/identity.hpp create mode 100644 src/ssc/isomorphism.hpp create mode 100644 src/ssc/main.cpp create mode 100644 src/ssc/state_space.hpp diff --git a/num b/num deleted file mode 100644 index e69de29bb..000000000 diff --git a/src/Makefile.am b/src/Makefile.am index 908212bae..57fdc4496 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,6 +1,6 @@ SUBDIRS = verifier vm loader element ffi -bin_PROGRAMS = slim +bin_PROGRAMS = slim sscheck slim_LDADD = -llmn_loader \ -llmn_verifier \ @@ -87,3 +87,10 @@ slim_OBJS = arch.h ../lib/config.lmn: genconfig $(SHELL) ./genconfig + +sscheck_SOURCES = ssc/main.cpp env.cpp + +sscheck_LDADD = ${slim_LDADD} +sscheck_LDFLAGS = ${slim_LDFLAGS} +sscheck_CXXFLAGS = -std=c++11 -DCOMMIT_ID=\"`git show -s --format=%h`\" +sscheck_DEPENDENCIES = ./element/liblmn_elm.a diff --git a/src/element/json/exception.hpp b/src/element/json/exception.hpp index c22017051..6b4cefb80 100644 --- a/src/element/json/exception.hpp +++ b/src/element/json/exception.hpp @@ -45,15 +45,19 @@ namespace slim { namespace element { namespace json { -struct parse_error {}; +struct parse_error { + virtual const char *what() const noexcept = 0; +}; struct overflow_error : parse_error, std::overflow_error { overflow_error(std::istream::pos_type pos) : std::overflow_error("occurred at " + std::to_string(pos)) {} + const char *what() const noexcept { return std::overflow_error::what(); } }; struct syntax_error : parse_error, std::runtime_error { syntax_error(const std::string &what_arg, std::istream::pos_type pos) : std::runtime_error(what_arg + "(at " + std::to_string(pos) + ")") {} + const char *what() const noexcept { return std::runtime_error::what(); } }; } // namespace json diff --git a/src/element/json/value.hpp b/src/element/json/value.hpp index 88eebcbb6..b9a011264 100644 --- a/src/element/json/value.hpp +++ b/src/element/json/value.hpp @@ -94,6 +94,10 @@ template struct value_ptr { return *this; } + bool operator==(const value_ptr &ptr) const { + return *ptr_ == *ptr.ptr_; + } + private: T *ptr_; }; @@ -106,6 +110,8 @@ using value_type = struct null { operator std::nullptr_t() { return nullptr; } + + bool operator==(const null &s) const { return true; } }; struct integer { @@ -114,6 +120,8 @@ struct integer { // 数値型は暗黙の型変換を行わない explicit constexpr integer(int64_t v) : value(v) {} operator int64_t() { return value; } + + bool operator==(const integer &v) const { return value == v.value; } }; struct real { double value; @@ -121,6 +129,8 @@ struct real { // 数値型は暗黙の型変換は行わない explicit constexpr real(double v) : value(v) {} operator double() { return value; } + + bool operator==(const real &v) const { return value == v.value; } }; struct boolean { bool value; @@ -128,12 +138,16 @@ struct boolean { // 数値型は暗黙の型変換は行わない constexpr explicit boolean(bool tf) : value(tf) {} operator bool() { return value; } + + bool operator==(const boolean &v) const { return value == v.value; } }; struct string { std::string value; string(const std::string &str) : value(str) {} operator std::string() { return value; } + + bool operator==(const string &v) const { return value == v.value; } }; struct array { std::vector value; @@ -142,6 +156,8 @@ struct array { array(const std::vector &v) : value(v) {} array(std::vector &&v) : value(std::move(v)) {} operator std::vector() { return value; } + + bool operator==(const array &v) const { return value == v.value; } }; struct object { std::unordered_map value; @@ -153,6 +169,7 @@ struct object { operator std::unordered_map() { return value; } value_type &operator[](const std::string &key) { return value[key]; } + bool operator==(const object &v) const { return value == v.value; } }; // throws json::syntax_error, json::overflow_error diff --git a/src/element/variant.hpp b/src/element/variant.hpp index 8081ee4cc..ad135bfe8 100644 --- a/src/element/variant.hpp +++ b/src/element/variant.hpp @@ -240,9 +240,6 @@ constexpr bool operator>=(monostate, monostate) noexcept { return true; } constexpr bool operator==(monostate, monostate) noexcept { return true; } constexpr bool operator!=(monostate, monostate) noexcept { return false; } -} // namespace element -} // namespace slim - template constexpr bool operator==(const slim::element::variant &v, const slim::element::variant &w) { @@ -251,7 +248,6 @@ constexpr bool operator==(const slim::element::variant &v, : slim::element::visit( typename slim::element::variant::equalizer(v), w); } - template constexpr bool operator!=(const slim::element::variant &v, const slim::element::variant &w) { @@ -267,4 +263,7 @@ constexpr bool operator<(const slim::element::variant &v, typename slim::element::variant::comparator(v), w)); } +} // namespace element +} // namespace slim + #endif /* SLIM_ELEMENT_VARINT_HPP */ diff --git a/src/ssc/check_result.hpp b/src/ssc/check_result.hpp new file mode 100644 index 000000000..8522b4d30 --- /dev/null +++ b/src/ssc/check_result.hpp @@ -0,0 +1,70 @@ +/* + * check_result.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SSC_CHECK_RESULT_HPP +#define SSC_CHECK_RESULT_HPP + +#include "state_space.hpp" + +#include +#include + +namespace ssc { + +// 等価性判定結果を格納する +// 失敗の場合は失敗理由を示す文字列、成功の場合は同型射 +struct check_result { + bool succeeded; + std::string reason; + std::unordered_map morphism; + + check_result() : succeeded(true) {} + check_result(bool s, const std::string &r) : succeeded(s), reason(r) {} + check_result(bool s, const state_space_homomorphism &r) + : succeeded(s), morphism(r) {} + static check_result success(const state_space_homomorphism &reason) { + return check_result(true, reason); + } + static check_result fail(const std::string &reason) { + return check_result(false, reason); + } + + explicit operator bool() { return succeeded; } +}; + +} // namespace ssc + +#endif /* SSC_CHECK_RESULT_HPP */ diff --git a/src/ssc/identity.hpp b/src/ssc/identity.hpp new file mode 100644 index 000000000..1cd7099de --- /dev/null +++ b/src/ssc/identity.hpp @@ -0,0 +1,83 @@ +/* + * identity.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SSC_IDENTITY_HPP +#define SSC_IDENTITY_HPP + +#include "check_result.hpp" +#include "state_space.hpp" + +#include + +namespace ssc { + +// idが全く同じかどうかで等価性を判定する +template +check_result identity_check(const slim::element::json_t &json1, + const slim::element::json_t &json2, + Comparator cmp) { + const state_space ss1(json1); + const state_space ss2(json2); + + if (ss1.states.size() != ss2.states.size()) + return check_result::fail("number of states are different"); + + if (!cmp(ss1.states.at(ss1.init), ss2.states.at(ss2.init))) + return check_result::fail("initial states are different"); + + for (state_space::state_id_t id = 0; id < ss1.states.size(); id++) { + auto &s1 = ss1.states[id]; + auto &s2 = ss2.states[id]; + if (!cmp(s1, s2)) + return check_result::fail("state " + ss1.id_to_key[id] + " and state " + + ss2.id_to_key[id] + " are different"); + } + + if (ss1.transitions != ss2.transitions) + return check_result::fail("transition sets are different"); + + std::unordered_map + isomorphism; + for (state_space::state_id_t id = 0; id < ss1.states.size(); id++) { + isomorphism[id] = id; + } + + return check_result::success(isomorphism); +} + +} // namespace ssc + +#endif /* SSC_IDENTITY_HPP */ diff --git a/src/ssc/isomorphism.hpp b/src/ssc/isomorphism.hpp new file mode 100644 index 000000000..04bf609d6 --- /dev/null +++ b/src/ssc/isomorphism.hpp @@ -0,0 +1,151 @@ +/* + * isomorphism.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SSC_ISOMORPHISM_HPP +#define SSC_ISOMORPHISM_HPP + +#include "check_result.hpp" +#include "state_space.hpp" + +#include +#include +#include +#include + +namespace ssc { + +// グラフ同型により等価性を判定する +// 正直なところ信頼性はアヤシイ +template +check_result isomorphism_check(const json_t &json1, const json_t &json2, + Comparator cmp) { + const state_space ss1(json1); + const state_space ss2(json2); + + if (ss1.states.size() != ss2.states.size()) + return check_result::fail("number of states are different"); + + std::unordered_map isomorphism; + isomorphism[ss1.init] = ss2.init; + if (!cmp(ss1.states.at(ss1.init), ss2.states.at(ss2.init))) + return check_result::fail("initial states are different"); + + std::function match_successors = + [&](state_space::state_id_t s1) -> check_result { + auto s2 = isomorphism[s1]; + auto &succs1 = ss1.transitions.at(s1); + auto &succs2 = ss2.transitions.at(s2); + + if (succs1.size() != succs2.size()) + return check_result::fail("number of successors are different"); + auto size = succs1.size(); + + bool all_matched = + std::all_of(succs1.begin(), succs1.end(), [&](state_space::state_id_t s) { + return isomorphism.find(s) != isomorphism.end(); + }); + if (all_matched) + return check_result(); + + std::vector permutation(succs1.size()); // successorの対応 + for (size_t i = 0; i < size; i++) + permutation[i] = i; + + // バックトラックするときのためにまだマッチしていないものを記録 + std::vector not_matched; + for (size_t i = 0; i < size; i++) + if (isomorphism.find(succs1[i]) == isomorphism.end()) + not_matched.push_back(i); + + do { + bool matched = true; + + // すでにマッチしたものと矛盾していないか確認 + for (size_t i = 0; i < size; i++) { + if (isomorphism.find(succs1[i]) != isomorphism.end() && + isomorphism[succs1[i]] != succs2[permutation[i]]) { + matched = false; + break; + } + } + + if (!matched) + continue; + + // 状態同士の比較 + for (auto idx : not_matched) { + if (!cmp(ss1.states.at(succs1[idx]), + ss2.states.at(succs2[permutation[idx]]))) { + matched = false; + break; + } + } + + if (!matched) + continue; + + // 暫定的にマッチングさせる + for (auto idx : not_matched) + isomorphism[succs1[idx]] = succs2[permutation[idx]]; + + // 以降のマッチングを試す + for (auto idx : not_matched) { + if (!match_successors(succs1[idx])) { + matched = false; + break; + } + } + + // マッチングに成功 + if (matched) + return check_result(); + + // どこかでマッチングに失敗したので巻き戻す + for (auto idx : not_matched) + isomorphism.erase(succs1[idx]); + + } while (std::next_permutation(permutation.begin(), permutation.end())); + + return check_result::fail("successors are not matched"); + }; + + auto result = match_successors(ss1.init); + return (result) ? check_result::success(isomorphism) : result; +} + +} + +#endif /* SSC_ISOMORPHISM_HPP */ diff --git a/src/ssc/main.cpp b/src/ssc/main.cpp new file mode 100644 index 000000000..2a5da025d --- /dev/null +++ b/src/ssc/main.cpp @@ -0,0 +1,242 @@ +/* + * main.cpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#include "../element/element.h" + +#include "check_result.hpp" +#include "identity.hpp" +#include "isomorphism.hpp" +#include "state_space.hpp" + +#include +#include +#include +#include + +#ifndef COMMIT_ID +#define COMMIT_ID "" +#endif + +// dummy +void slim_version(FILE *f) {} + +namespace ssc { + +std::istream *input1 = nullptr; +std::istream *input2 = nullptr; + +std::function state_comparator = + [](const json_t &, const json_t &) { return true; }; + +enum class EquivalenceMethod { identity, isomorphism }; +EquivalenceMethod equivalence_method = EquivalenceMethod::identity; + +enum PrintLevel { quiet = 0, info, verbose, debug }; +PrintLevel print_level = PrintLevel::info; + +static void usage(void) { + fprintf( + stderr, + "Usage: sscheck [OPTION]... FILE1 FILE2\n" + "options:\n" + " --stdin Read stndard input instead of FILE1.\n" + " -e, --equivalence=(identity | isomorphism)\n" + " Set how to decide equivalence of state spaces.\n" + " Default is identity." + " -c, --compare=(nothing | string)\n" + " Set how to decide equivalence of states.\n" + " Default is nothing (don't care what state is).\n" + " --quiet Print no information.\n" + " --info Print human-readable results (default).\n" + " --verbose Print more information.\n" + " -h, --help Print this message.\n" + " -v, --version Show version.\n"); + exit(1); +} + +static void parse_options(int argc, char *argv[]) { + int c, option_index; + + struct option long_options[] = { + {"version", no_argument, nullptr, 1000}, + {"help", no_argument, nullptr, 1001}, + {"stdin", no_argument, nullptr, 2000}, + {"equivalence", required_argument, nullptr, 3000}, + {"compare", required_argument, nullptr, 3001}, + {"quiet", no_argument, nullptr, 4000}, + {"info", no_argument, nullptr, 4001}, + {"verbose", no_argument, nullptr, 4002}, + {"debug", no_argument, nullptr, 4003}, + {0, 0, 0, 0}}; + + while ((c = getopt_long(argc, argv, "+vhe:c:", long_options, &option_index)) != + -1) { + switch (c) { + case 0: + printf("sscheck: log_options entries must have positive 4th member.\n"); + exit(1); + break; + + case 'v': + case 1000: + std::cout << "sscheck (State Space Checker) - version " << COMMIT_ID << std::endl; + exit(1); + break; + + case 'h': + case 1001: /* help */ /* FALLTHROUGH */ + case '?': + usage(); + break; + + case 2000: + input1 = &std::cin; + break; + + case 'e': + case 3000: + if (!optarg) + break; + else if (strcmp(optarg, "identity") == 0) + equivalence_method = EquivalenceMethod::identity; + else if (strcmp(optarg, "isomorphism") == 0) + equivalence_method = EquivalenceMethod::isomorphism; + break; + + case 'c': + case 3001: + if (!optarg) + break; + else if (strcmp(optarg, "nothing") == 0) + state_comparator = [](const json_t &, const json_t &) { return true; }; + else if (strcmp(optarg, "string") == 0) + state_comparator = [](const json_t &a, const json_t &b) { + return a == b; + }; + break; + + case 4000: + print_level = PrintLevel::quiet; + break; + + case 4001: + print_level = PrintLevel::info; + break; + + case 4002: + print_level = PrintLevel::verbose; + break; + + case 4003: + print_level = PrintLevel::debug; + break; + + default: + printf("?? getopt returned character code 0x%x ??\n", c); + exit(1); + break; + } + } +} + +} // namespace ssc + +using namespace ssc; + +int main(int argc, char *argv[]) { + if (argc == 1) { + usage(); + exit(1); + } + + parse_options(argc, argv); + + int index = optind; + while (index < argc) { + auto input = new std::fstream(argv[index++]); + if (!input1) { + input1 = input; + } else if (!input2) { + input2 = input; + } else { + std::cerr << "sscheck: too much inputs" << std::endl; + exit(1); + } + } + + if (!input1 || !input2) { + std::cerr << "sscheck: missing state spaces" << std::endl; + exit(1); + } + + slim::element::json_t json1, json2; + try { + (*input1) >> json1; + if (input1 != &std::cin) + delete input1; + (*input2) >> json2; + if (input2 != &std::cin) + delete input2; + } catch (slim::element::json::parse_error &error) { + std::cerr << "sscheck: " << error.what() << std::endl; + exit(1); + } + + check_result result; + switch (equivalence_method) { + case EquivalenceMethod::identity: + result = identity_check(json1, json2, state_comparator); + break; + case EquivalenceMethod::isomorphism: + result = isomorphism_check(json1, json2, state_comparator); + break; + } + + if (print_level >= PrintLevel::info) { + std::cout << "sscheck: " << (result ? "equivalent" : "different") + << std::endl; + } + + if (print_level >= PrintLevel::verbose) { + if (result) { + // result.morphismを出力する + } else { + std::cout << result.reason << std::endl; + } + } + + return (result) ? 0 : 1; +} \ No newline at end of file diff --git a/src/ssc/state_space.hpp b/src/ssc/state_space.hpp new file mode 100644 index 000000000..dd63d4f8b --- /dev/null +++ b/src/ssc/state_space.hpp @@ -0,0 +1,134 @@ +/* + * state_space.hpp + * + * Copyright (c) 2019, Ueda Laboratory LMNtal Group + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in + * the documentation and/or other materials provided with the + * distribution. + * + * 3. Neither the name of the Ueda Laboratory LMNtal Group nor the + * names of its contributors may be used to endorse or promote + * products derived from this software without specific prior + * written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +#ifndef SSC_STATE_SPACE_HPP +#define SSC_STATE_SPACE_HPP + +#include "element/element.h" + +using array_ptr = slim::element::json::value_ptr; +using object_ptr = slim::element::json::value_ptr; + +#include +#include +#include +#include + +namespace ssc { + +namespace c17 = slim::element; +using namespace slim::element; + +/// jsonデータを使いやすい形に変換するためのデータ型 +struct state_space { + /// 状態を0から始まる連番で管理するための添え字 + using state_id_t = size_t; + + state_space(const json_t &json) { + auto &ss = c17::get(json)->value; + auto &sts = c17::get(ss.at("states"))->value; + + // key -> state idの変換表 + std::unordered_map id_map; + + // state idとkeyの変換表を用意 + id_to_key.resize(sts.size()); + size_t index = 0; + for (auto &p : sts) { + auto key = p.first; + id_map[key] = index; + id_to_key[index] = key; + index++; + } + + // 状態数で検証 + auto size = c17::get(ss.at("size")).value; + if (size != sts.size()) + throw new std::runtime_error("number of states are incoherent (" + std::to_string(size) + " vs " + std::to_string(sts.size()) + ")"); + + // 初期状態 + init = id_map[c17::get(ss.at("init")).value]; + + // 状態表を作成 + states.resize(sts.size()); + for (auto &p : sts) + states[id_map[p.first]] = p.second; + + // 遷移表を作成 + auto &trs = c17::get(ss.at("transitions"))->value; + transitions.resize(trs.size()); + size_t end_count = 0; + for (auto &p : trs) { + if (id_map.find(p.first) == id_map.end()) + throw new std::runtime_error("unknown state '" + p.first + "' is found in transitions."); + + auto source = id_map[p.first]; + auto &succ = c17::get(p.second)->value; + + if (succ.empty()) + end_count++; + + for (auto &tr : succ) { + auto key = c17::get(c17::get(tr)->value.at("succ")).value; + if (id_map.find(key) == id_map.end()) + throw new std::runtime_error("unknown destination '" + key + "' from state '" + p.first + "'is found."); + + auto dest = id_map[key]; + + // 遷移ラベル（ルール名）は無視しているが良いのだろうか + transitions[source].push_back(dest); + } + } + + // 終状態の数で検証 + auto end_states = c17::get(ss.at("end_size")).value; + if (end_states != end_count) + throw new std::runtime_error("number of end states are incoherent (" + std::to_string(end_states) + " vs " + std::to_string(end_count) + ")"); + } + + state_id_t init; + std::vector states; + std::vector> transitions; + // state idから元の状態番号への表（復元用） + std::vector id_to_key; +}; + +using state_space_homomorphism = + std::unordered_map; + +} // namespace ssc + +#endif /* SSC_STATE_SPACE_HPP */ From 1302f4e41328c943ec3ad0d85abc2d9a15054106 Mon Sep 17 00:00:00 2001 From: Taichi Tomioka Date: Fri, 11 Oct 2019 21:23:54 +0900 Subject: [PATCH 8/8] Fix build errors. --- src/Makefile.am | 4 +-- src/element/alloc.cpp | 68 ++++--------------------------------------- src/vm/atom.cpp | 58 ++++++++++++++++++++++++++++++++++++ 3 files changed, 66 insertions(+), 64 deletions(-) diff --git a/src/Makefile.am b/src/Makefile.am index 57fdc4496..8ff04b9dd 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -90,7 +90,7 @@ arch.h ../lib/config.lmn: genconfig sscheck_SOURCES = ssc/main.cpp env.cpp -sscheck_LDADD = ${slim_LDADD} -sscheck_LDFLAGS = ${slim_LDFLAGS} +sscheck_LDADD = -llmn_elm +sscheck_LDFLAGS = -L./element sscheck_CXXFLAGS = -std=c++11 -DCOMMIT_ID=\"`git show -s --format=%h`\" sscheck_DEPENDENCIES = ./element/liblmn_elm.a diff --git a/src/element/alloc.cpp b/src/element/alloc.cpp index 7fabd5517..c1ea7f4f4 100644 --- a/src/element/alloc.cpp +++ b/src/element/alloc.cpp @@ -36,71 +36,13 @@ * $Id: alloc.c,v 1.3 2008/09/19 05:18:17 taisuke Exp $ */ -#include "error.h" -#include "lmntal.h" -#include "lmntal_thread.h" -#include "memory_pool.h" -#include "util.h" -#include "vector.h" -#include "vm/vm.h" - -/*---------------------------------------------------------------------- - * memory allocation for atom - */ - -static memory_pool **atom_memory_pools[128]; -void mpool_init() { - int i, core_num, arity_num; - arity_num = ARY_SIZEOF(atom_memory_pools); - core_num = lmn_env.core_num; - for (i = 0; i < arity_num; i++) { - atom_memory_pools[i] = - (memory_pool **)malloc(sizeof(memory_pool *) * core_num); - memset(atom_memory_pools[i], 0, sizeof(memory_pool *) * core_num); - } -} - -LmnSymbolAtomRef lmn_new_atom(LmnFunctor f) { - LmnSymbolAtomRef ap; - int arity, cid; - arity = LMN_FUNCTOR_ARITY(lmn_functor_table, f); - cid = env_my_thread_id(); - - if (atom_memory_pools[arity][cid] == 0) { - atom_memory_pools[arity][cid] = memory_pool_new(LMN_SATOM_SIZE(arity)); - } - ap = (LmnSymbolAtomRef)memory_pool_malloc(atom_memory_pools[arity][cid]); - ap->set_functor(f); - ap->set_id(0); - - return ap; -} - -void lmn_delete_atom(LmnSymbolAtomRef ap) { - int arity, cid; - - env_return_id(ap->get_id()); +#include "error.h" - arity = LMN_FUNCTOR_ARITY(lmn_functor_table, ap->get_functor()); - cid = env_my_thread_id(); - memory_pool_free(atom_memory_pools[arity][cid], ap); -} +#include "lmntal.h" -void free_atom_memory_pools(void) { - unsigned int i, j, arity_num, core_num; - - arity_num = ARY_SIZEOF(atom_memory_pools); - core_num = lmn_env.core_num; - for (i = 0; i < arity_num; i++) { - for (j = 0; j < core_num; j++) { - if (atom_memory_pools[i][j]) { - memory_pool_delete(atom_memory_pools[i][j]); - } - } - free(atom_memory_pools[i]); - } -} +#include +#include /*---------------------------------------------------------------------- * memory allocation for membrane @@ -156,6 +98,8 @@ void *lmn_realloc(void *p, size_t num) { void lmn_free(void *p) { free(p); } +// new, delete演算子オーバーロード + void* operator new(std::size_t num) { return lmn_malloc(num); } diff --git a/src/vm/atom.cpp b/src/vm/atom.cpp index 14e8d1390..78870c5c4 100644 --- a/src/vm/atom.cpp +++ b/src/vm/atom.cpp @@ -167,6 +167,64 @@ BOOL LMN_IS_EX_FUNCTOR(LmnFunctor FUNC) { return FUNC == LMN_HL_FUNC; } ///// +/*---------------------------------------------------------------------- + * memory allocation for atom + */ + +static memory_pool **atom_memory_pools[128]; + +void mpool_init() { + int i, core_num, arity_num; + arity_num = ARY_SIZEOF(atom_memory_pools); + core_num = lmn_env.core_num; + for (i = 0; i < arity_num; i++) { + atom_memory_pools[i] = + (memory_pool **)malloc(sizeof(memory_pool *) * core_num); + memset(atom_memory_pools[i], 0, sizeof(memory_pool *) * core_num); + } +} + +LmnSymbolAtomRef lmn_new_atom(LmnFunctor f) { + LmnSymbolAtomRef ap; + int arity, cid; + arity = LMN_FUNCTOR_ARITY(lmn_functor_table, f); + cid = env_my_thread_id(); + + if (atom_memory_pools[arity][cid] == 0) { + atom_memory_pools[arity][cid] = memory_pool_new(LMN_SATOM_SIZE(arity)); + } + ap = (LmnSymbolAtomRef)memory_pool_malloc(atom_memory_pools[arity][cid]); + ap->set_functor(f); + ap->set_id(0); + + return ap; +} + +void lmn_delete_atom(LmnSymbolAtomRef ap) { + int arity, cid; + + env_return_id(ap->get_id()); + + arity = LMN_FUNCTOR_ARITY(lmn_functor_table, ap->get_functor()); + cid = env_my_thread_id(); + memory_pool_free(atom_memory_pools[arity][cid], ap); +} + +void free_atom_memory_pools(void) { + unsigned int i, j, arity_num, core_num; + + arity_num = ARY_SIZEOF(atom_memory_pools); + core_num = lmn_env.core_num; + for (i = 0; i < arity_num; i++) { + for (j = 0; j < core_num; j++) { + if (atom_memory_pools[i][j]) { + memory_pool_delete(atom_memory_pools[i][j]); + } + } + free(atom_memory_pools[i]); + } +} + /* アトムをコピーして返す。 * atomがシンボルアトムの場合、リンク先のデータアトムもコピーする */ LmnAtomRef lmn_copy_atom(LmnAtomRef atom, LmnLinkAttr attr) {