read_aiger: Fix incorrect read of binary Aiger without outputs #4359
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
povik
reviewed
Apr 29, 2024
frontends/aiger/aigerparse.cc
Outdated
| @@ -722,7 +722,8 @@ 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 | |||
| if (O > 0) | |||
| std::getline(f, line); // Ignore up to start of next line | |||
There was a problem hiding this comment.
Thanks! Please move up the getline below f >> l1 so we consume the full line per every output.
There was a problem hiding this comment.
Oh sure I can do that, will do the same for the following if (B > 0) and the ascii parser while im at it
georgerennie
force-pushed
the
aiger_parse_bug
branch
2 times, most recently
from
8e20c64 to
69e6caa
Compare
povik
reviewed
Apr 29, 2024
tests/aiger/and_bad.aag
Outdated
| @@ -0,0 +1,8 @@ | |||
| aag 3 2 0 0 1 1 0 0 0 | |||
There was a problem hiding this comment.
Is this a malformed aiger file? What do the tests do with it then?
There was a problem hiding this comment.
Oh yeah in hindsight i did not give that file a very good name. its just an aiger file that has a bad state node instead of an output node (so would have caused the issue that this pr fixes). it is a valid aiger file though. will rename
There was a problem hiding this comment.
Yeah please do other than that the PR looks good
* Also makes all ascii parsing finish reading lines and adds a small test
georgerennie
force-pushed
the
aiger_parse_bug
branch
from
69e6caa to
4e6deb5
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This was unconditionally reading the rest of a line when parsing outputs, but if none exist that means an extra line is parsed. This causes the following bad state parsing to fail with the error "Line %u cannot be interpreted as a bad state property!" on a file with only bad state properties and no outputs
Fix does the same as the similar check in Line 738 to only finish reading the line if any outputs have been read.