From 4e6deb53b64d4acd2046d2826ede02c5cd35d22f Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Fri, 26 Apr 2024 19:16:01 +0100
Subject: [PATCH] read_aiger: Fix incorrect read of binary Aiger without
 outputs

* Also makes all ascii parsing finish reading lines and adds a small
  test
---
 frontends/aiger/aigerparse.cc  | 12 +++++-------
 tests/aiger/and_to_bad_out.aag |  8 ++++++++
 tests/aiger/and_to_bad_out.aig |  5 +++++
 3 files changed, 18 insertions(+), 7 deletions(-)
 create mode 100644 tests/aiger/and_to_bad_out.aag
 create mode 100644 tests/aiger/and_to_bad_out.aig

diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index cb19b8413..0178514e1 100644
--- a/frontends/aiger/aigerparse.cc
+++ b/frontends/aiger/aigerparse.cc
@@ -590,6 +590,7 @@ void AigerReader::parse_aiger_ascii()
 	for (unsigned i = 0; i < O; ++i, ++line_count) {
 		if (!(f >> l1))
 			log_error("Line %u cannot be interpreted as an output!\n", line_count);
+		std::getline(f, line); // Ignore up to start of next line
 
 		log_debug2("%d is an output\n", l1);
 		RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
@@ -597,20 +598,18 @@ void AigerReader::parse_aiger_ascii()
 		module->connect(wire, createWireIfNotExists(module, l1));
 		outputs.push_back(wire);
 	}
-	//std::getline(f, line); // Ignore up to start of next line
 
 	// Parse bad properties
 	for (unsigned i = 0; i < B; ++i, ++line_count) {
 		if (!(f >> l1))
 			log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
+		std::getline(f, line); // Ignore up to start of next line
 
 		log_debug2("%d is a bad state property\n", l1);
 		RTLIL::Wire *wire = createWireIfNotExists(module, l1);
 		wire->port_output = true;
 		bad_properties.push_back(wire);
 	}
-	//if (B > 0)
-	//	std::getline(f, line); // Ignore up to start of next line
 
 	// TODO: Parse invariant constraints
 	for (unsigned i = 0; i < C; ++i, ++line_count)
@@ -628,6 +627,7 @@ void AigerReader::parse_aiger_ascii()
 	for (unsigned i = 0; i < A; ++i) {
 		if (!(f >> l1 >> l2 >> l3))
 			log_error("Line %u cannot be interpreted as an AND!\n", line_count);
+		std::getline(f, line); // Ignore up to start of next line
 
 		log_debug2("%d %d %d is an AND\n", l1, l2, l3);
 		log_assert(!(l1 & 1));
@@ -636,7 +636,6 @@ void AigerReader::parse_aiger_ascii()
 		RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3);
 		module->addAndGate("$and" + o_wire->name.str(), i1_wire, i2_wire, o_wire);
 	}
-	std::getline(f, line); // Ignore up to start of next line
 }
 
 static unsigned parse_next_delta_literal(std::istream &f, unsigned ref)
@@ -715,6 +714,7 @@ void AigerReader::parse_aiger_binary()
 	for (unsigned i = 0; i < O; ++i, ++line_count) {
 		if (!(f >> l1))
 			log_error("Line %u cannot be interpreted as an output!\n", line_count);
+		std::getline(f, line); // Ignore up to start of next line
 
 		log_debug2("%d is an output\n", l1);
 		RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
@@ -722,20 +722,18 @@ void AigerReader::parse_aiger_binary()
 		module->connect(wire, createWireIfNotExists(module, l1));
 		outputs.push_back(wire);
 	}
-	std::getline(f, line); // Ignore up to start of next line
 
 	// Parse bad properties
 	for (unsigned i = 0; i < B; ++i, ++line_count) {
 		if (!(f >> l1))
 			log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
+		std::getline(f, line); // Ignore up to start of next line
 
 		log_debug2("%d is a bad state property\n", l1);
 		RTLIL::Wire *wire = createWireIfNotExists(module, l1);
 		wire->port_output = true;
 		bad_properties.push_back(wire);
 	}
-	if (B > 0)
-		std::getline(f, line); // Ignore up to start of next line
 
 	// TODO: Parse invariant constraints
 	for (unsigned i = 0; i < C; ++i, ++line_count)
diff --git a/tests/aiger/and_to_bad_out.aag b/tests/aiger/and_to_bad_out.aag
new file mode 100644
index 000000000..96f1e7cad
--- /dev/null
+++ b/tests/aiger/and_to_bad_out.aag
@@ -0,0 +1,8 @@
+aag 3 2 0 0 1 1 0 0 0
+2
+4
+6
+6 2 4
+i0 pi0
+i1 pi1
+b0 b0
diff --git a/tests/aiger/and_to_bad_out.aig b/tests/aiger/and_to_bad_out.aig
new file mode 100644
index 000000000..3be65ae89
--- /dev/null
+++ b/tests/aiger/and_to_bad_out.aig
@@ -0,0 +1,5 @@
+aig 3 2 0 0 1 1
+6
+i0 pi0
+i1 pi1
+b0 b0