aiger: Use new JSON code for writing aiger witness map files

3 files changed, 96 insertions, 55 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 513f9d95a..5cfdff3fb 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -19,6 +19,7 @@
 
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
+#include "kernel/json.h"
 #include "libs/json11/json11.hpp"
 
 USING_YOSYS_NAMESPACE
@@ -721,18 +722,19 @@ struct AigerWriter
 		return path;
 	}
 
-	void write_ywmap(std::ostream &f)
+	void write_ywmap(PrettyJson &json)
 	{
-		f << "{\n";
-		f << "  \"version\": \"Yosys Witness Aiger Map\",\n";
-		f << stringf("  \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str());
-		f << stringf("  \"latch_count\": %d,\n", aig_l);
-		f << stringf("  \"input_count\": %d,\n", aig_i);
+		json.begin_object();
+		json.entry("version", "Yosys Witness Aiger map");
+		json.entry("gennerator", yosys_version_str);
 
-		dict<int, string> clock_lines;
-		dict<int, string> input_lines;
-		dict<int, string> init_lines;
-		dict<int, string> seq_lines;
+		json.entry("latch_count", aig_l);
+		json.entry("input_count", aig_i);
+
+		dict<int, Json> clock_lines;
+		dict<int, Json> input_lines;
+		dict<int, Json> init_lines;
+		dict<int, Json> seq_lines;
 
 		for (auto cell : module->cells())
 		{
@@ -751,21 +753,21 @@ struct AigerWriter
 					if (init_inputs.count(sig[i])) {
 						int a = init_inputs.at(sig[i]);
 						log_assert((a & 1) == 0);
-						init_lines[a] += json11::Json(json11::Json::object {
+						init_lines[a] = json11::Json(json11::Json::object {
 							{ "path", witness_path(wire) },
 							{ "input", (a >> 1) - 1 },
 							{ "offset", sig_qy[i].offset },
-						}).dump();
+						});
 					}
 
 					if (input_bits.count(sig[i])) {
 						int a = aig_map.at(sig[i]);
 						log_assert((a & 1) == 0);
-						seq_lines[a] += json11::Json(json11::Json::object {
+						seq_lines[a] = json11::Json(json11::Json::object {
 							{ "path", witness_path(wire) },
 							{ "input", (a >> 1) - 1 },
 							{ "offset", sig_qy[i].offset },
-						}).dump();
+						});
 					}
 				}
 			}
@@ -783,60 +785,55 @@ struct AigerWriter
 
 					int a = aig_map.at(sig[i]);
 					log_assert((a & 1) == 0);
-					input_lines[a] += json11::Json(json11::Json::object {
+					input_lines[a] = json11::Json(json11::Json::object {
 						{ "path", path },
 						{ "input", (a >> 1) - 1 },
 						{ "offset", i },
-					}).dump();
+					});
 
 					if (ywmap_clocks.count(sig[i])) {
 						int clock_mode = ywmap_clocks[sig[i]];
 						if (clock_mode != 3) {
-							clock_lines[a] += json11::Json(json11::Json::object {
+							clock_lines[a] = json11::Json(json11::Json::object {
 								{ "path", path },
 								{ "input", (a >> 1) - 1 },
 								{ "offset", i },
 								{ "edge", clock_mode == 1 ? "posedge" : "negedge" },
-							}).dump();
+							});
 						}
 					}
 				}
 			}
 		}
 
-		f << "  \"clocks\": [";
+		json.name("clocks");
+		json.begin_array();
 		clock_lines.sort();
-		const char *sep = "\n    ";
-		for (auto &it : clock_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ],\n";
+		for (auto &it : clock_lines)
+			json.value(it.second);
+		json.end_array();
 
-		f << "  \"inputs\": [";
+		json.name("inputs");
+		json.begin_array();
 		input_lines.sort();
-		sep = "\n    ";
-		for (auto &it : input_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ],\n";
+		for (auto &it : input_lines)
+			json.value(it.second);
+		json.end_array();
 
-		f << "  \"seqs\": [";
-		sep = "\n    ";
-		for (auto &it : seq_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ],\n";
+		json.name("seqs");
+		json.begin_array();
+		input_lines.sort();
+		for (auto &it : seq_lines)
+			json.value(it.second);
+		json.end_array();
 
-		f << "  \"inits\": [";
-		sep = "\n    ";
-		for (auto &it : init_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ]\n}\n";
+		json.name("inits");
+		json.begin_array();
+		input_lines.sort();
+		for (auto &it : init_lines)
+			json.value(it.second);
+		json.end_array();
+		json.end_object();
 	}
 
 };
@@ -991,9 +988,12 @@ struct AigerBackend : public Backend {
 		if (!yw_map_filename.empty()) {
 			std::ofstream mapf;
 			mapf.open(yw_map_filename.c_str(), std::ofstream::trunc);
-			if (mapf.fail())
-				log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
-			writer.write_ywmap(mapf);
+
+			PrettyJson json;
+
+			if (!json.write_to_file(yw_map_filename))
+				log_error("Can't open file `%s' for writing: %s\n", yw_map_filename.c_str(), strerror(errno));
+			writer.write_ywmap(json);
 		}
 	}
 } AigerBackend;
diff --git a/kernel/json.cc b/kernel/json.cc
index 6ea873329..59f782e5e 100644
--- a/kernel/json.cc
+++ b/kernel/json.cc
@@ -23,13 +23,38 @@ USING_YOSYS_NAMESPACE
 
 void PrettyJson::emit_to_log()
 {
-    targets.push_back([](const char *raw_json) { log("%s", raw_json); });
+    struct LogTarget : public Target {
+        void emit(const char *data) override { log("%s", data); }
+    };
+
+    targets.push_back(std::unique_ptr<Target>(new LogTarget));
 }
 
 void PrettyJson::append_to_string(std::string &target)
 {
-    std::string *target_p = &target;
-    targets.push_back([=](const char *raw_json) { *target_p += raw_json; });
+    struct AppendStringTarget : public Target {
+        std::string &target;
+        AppendStringTarget(std::string &target) : target(target) {}
+        void emit(const char *data) override { target += data; }
+    };
+
+    targets.push_back(std::unique_ptr<Target>(new AppendStringTarget(target)));
+}
+
+bool PrettyJson::write_to_file(const std::string &path)
+{
+    struct WriteFileTarget : public Target {
+        std::ofstream target;
+        void emit(const char *data) override { target << data; }
+        void flush() override { target.flush(); }
+    };
+
+    auto target = std::unique_ptr<WriteFileTarget>(new WriteFileTarget);
+    target->target.open(path);
+    if (target->target.fail())
+        return false;
+    targets.push_back(std::unique_ptr<Target>(target.release()));
+    return true;
 }
 
 void PrettyJson::line()
@@ -42,7 +67,13 @@ void PrettyJson::line()
 void PrettyJson::raw(const char *raw_json)
 {
     for (auto &target : targets)
-        target(raw_json);
+        target->emit(raw_json);
+}
+
+void PrettyJson::flush()
+{
+    for (auto &target : targets)
+        target->flush();
 }
 
 void PrettyJson::begin_object()
@@ -110,8 +141,10 @@ void PrettyJson::begin_value()
 
 void PrettyJson::end_value()
 {
-    if (state.empty())
+    if (state.empty()) {
         raw("\n");
+        flush();
+    }
 }
 
 void PrettyJson::value_json(const Json &value)
diff --git a/kernel/json.h b/kernel/json.h
index 3ba355327..ae86b3aa6 100644
--- a/kernel/json.h
+++ b/kernel/json.h
@@ -38,18 +38,26 @@ class PrettyJson
         ARRAY,
     };
 
+    struct Target {
+        virtual void emit(const char *data) = 0;
+        virtual void flush() {};
+        virtual ~Target() {};
+    };
+
     std::string newline_indent = "\n";
-    std::vector<std::function<void(const char *)>> targets;
+    std::vector<std::unique_ptr<Target>> targets;
     std::vector<Scope> state = {VALUE};
 public:
 
     void emit_to_log();
     void append_to_string(std::string &target);
+    bool write_to_file(const std::string &path);
 
     bool active() { return !targets.empty(); }
 
     void line();
     void raw(const char *raw_json);
+    void flush();
     void begin_object();
     void begin_array();
     void end_object();