From 553381bd6ef9758dc936af6429290af40181e4ae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Nov 2021 23:00:18 +0100 Subject: [PATCH] aiger: improve parse errors and test them * spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh (parse_aag_impl_): Do not display source filename in user facing errors. Use GNU-style "file:line: " prefixes for locations. Adjust all sscanf() calls to check for ignored trailing data. Add some missing checks about the order of input and output names, checks that output names do no intersect input names. Fix incorrect line number for unexpected input variable number, and avoid using std::stoi as that throws an std::invalid_argument on parse error. * tests/python/aiger.py: Add test cases for each error message. --- spot/twaalgos/aiger.cc | 287 +++++++++++++------------ spot/twaalgos/aiger.hh | 4 +- tests/python/aiger.py | 466 ++++++++++++++++++++++++++++++++++++++++- 3 files changed, 624 insertions(+), 133 deletions(-) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 983113c2e..60336be33 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -72,14 +72,18 @@ namespace parse_aag_impl_(std::istream& iss, const std::string& filename) { - auto error_aig = [fn = filename](int line_src, - const std::string& msg, - unsigned line_file) + auto error_aig = [filename](const std::string_view& msg, + unsigned line_start = 0, + unsigned line_end = 0) { - throw parse_error("spot/twaalgos/aiger.cc:" + std::to_string(line_src) - + ": in " + fn + " hit error: " + msg - + " at line " + std::to_string(line_file) - + ".\n"); + std::ostringstream out; + out << filename; + if (line_start) + out << ':' << line_start; + if (line_end && line_end > line_start) + out << '-' << line_end; + out << ": " << msg; + throw parse_error(out.str()); }; //results @@ -92,15 +96,21 @@ namespace unsigned max_index, nb_inputs, nb_latches, nb_outputs, nb_and; std::string line; - getline(iss, line); - unsigned line_number = 1; + unsigned line_number = 0; + std::unordered_set names; + + auto nextline = [&line, &line_number, &iss]() { + line.clear(); + getline(iss, line); + ++line_number; + }; + + nextline(); if (sscanf(line.c_str(), "aag %u %u %u %u %u", &max_index, &nb_inputs, &nb_latches, &nb_outputs, &nb_and) != 5) - error_aig(__LINE__, "invalid header", line_number); - + error_aig("invalid header line", line_number); if (max_index < nb_inputs + nb_latches + nb_and) - error_aig(__LINE__, "More variables than indicated by max var", - line_number); + error_aig("more variables than indicated by max var", line_number); latches.reserve(nb_latches); outputs.reserve(nb_outputs); @@ -108,144 +118,163 @@ namespace for (unsigned i = 0; i < nb_inputs; ++i) { - if (!iss) - error_aig(__LINE__, "missing input", line_number); - - line.clear(); - getline(iss, line); - if ((unsigned)std::stoi(line) != 2*(i+1)) - error_aig(__LINE__, "invalid input numbering for input nbr " - + std::to_string(i), line_number); - ++line_number; + nextline(); + unsigned expected = 2 * (i + 1); + unsigned num = 0; + int end = 0; + const char* buf = line.c_str(); + if (!line.empty() + && (sscanf(buf, "%u %n", &num, &end) != 1 || buf[end])) + error_aig("invalid format for an input", line_number); + if (num != expected) + error_aig("expecting input number " + std::to_string(expected), + line_number); } for (unsigned i = 0; i < nb_latches; ++i) { - if (!iss) - error_aig(__LINE__, "missing latch", line_number); - - line.clear(); - getline(iss, line); - ++line_number; - unsigned latch_var, next_state; - if (sscanf(line.c_str(), "%u %u", &latch_var, &next_state) != 2) - error_aig(__LINE__, "invalid latch", line_number); - if (latch_var != 2*(1 + nb_inputs + i)) - error_aig(__LINE__, "invalid latch numbering", line_number); - + nextline(); + unsigned expected = 2 * (1 + nb_inputs + i); + unsigned latch_var = 0, next_state; + int end = 0; + const char* buf = line.c_str(); + if (!line.empty() + && (sscanf(buf, "%u %u %n", &latch_var, &next_state, &end) != 2 + || buf[end])) + error_aig("invalid format for a latch", line_number); + if (latch_var != expected) + error_aig("expecting latch number " + std::to_string(expected), + line_number); latches.push_back(next_state); } for (unsigned i = 0; i < nb_outputs; ++i) { - if (!iss) - error_aig(__LINE__, "missing output", line_number); - - line.clear(); - getline(iss, line); - ++line_number; + nextline(); + if (line.empty()) + error_aig("expecting an output", line_number); unsigned num_out; - if (sscanf(line.c_str(), "%u", &num_out) != 1) - error_aig(__LINE__, "invalid output definition", line_number); + const char* buf = line.c_str(); + int end = 0; + if (sscanf(buf, "%u %n", &num_out, &end) != 1 || buf[end]) + error_aig("invalid format for an output", line_number); outputs.push_back(num_out); } for (unsigned i = 0; i < nb_and; ++i) { - unsigned and_gate, lhs, rhs; - if (!iss) - error_aig(__LINE__, "missing AND", line_number); - line.clear(); - getline(iss, line); - ++line_number; - if (sscanf(line.c_str(), "%u %u %u", &and_gate, &lhs, &rhs) != 3) - error_aig(__LINE__, "invalid AND", line_number); - if (and_gate != 2*(1 + nb_inputs + nb_latches + i)) - error_aig(__LINE__, "invalid gate numbering. Expected " - + std::to_string((2*(1 + nb_inputs + nb_latches + i))) - + " got " + std::to_string(and_gate), line_number); + nextline(); + unsigned and_gate = 0, lhs, rhs; + if (!line.empty()) + { + const char* buf = line.c_str(); + int end = 0; + if (sscanf(buf, "%u %u %u %n", &and_gate, &lhs, &rhs, &end) != 3 + || buf[end]) + error_aig("invalid format for an AND gate", line_number); + } + unsigned expected = 2 * (1 + nb_inputs + nb_latches + i); + if (and_gate != expected) + error_aig("expecting AND gate number " + std::to_string(expected), + line_number); gates.emplace_back(lhs, rhs); } - line.clear(); - - getline(iss, line); - ++line_number; + nextline(); bool comment_sec = false; + unsigned first_input_line = 0; + unsigned last_input_line = 0; + unsigned first_output_line = 0; + unsigned last_output_line = 0; while (iss && !comment_sec) - { - unsigned pos_var_name; - char first_char = line[0]; - char var_name[256]; - switch (first_char) { - // latches names non supported - case 'l': - { - line.clear(); - getline(iss, line); - ++line_number; - continue; - } - case 'i': - { - if (sscanf(line.c_str(), "i%u %255s", &pos_var_name, var_name) != 2 - || pos_var_name >= nb_inputs) - error_aig(__LINE__, "could not parse input name: " - + line, line_number); - auto itn = std::find(input_names.begin(), input_names.end(), - var_name); - if (itn != input_names.end()) - error_aig(__LINE__, std::string("input name ") + var_name - + " appears twice", line_number); - input_names.push_back(var_name); - line.clear(); - getline(iss, line); - ++line_number; - break; - } - case 'o': - { - if (sscanf(line.c_str(), "o%u %255s", &pos_var_name, var_name) != 2 - || pos_var_name >= nb_outputs) - error_aig(__LINE__, "could not parse output name: " - + line, line_number); - auto itn = std::find(output_names.begin(), output_names.end(), - var_name); - if (itn != output_names.end()) - error_aig(__LINE__, std::string("output name ") + var_name + - " appears twice", line_number); - output_names.push_back(var_name); - line.clear(); - getline(iss, line); - ++line_number; - break; - } - case 'c': - { - comment_sec = true; - break; - } - default: - { - error_aig(__LINE__, "invalid line", line_number); - } + unsigned pos_var_name; + char var_name[256]; + int end; + const char* buf = line.c_str(); + switch (buf[0]) + { + case 'l': // latches names non supported + { + nextline(); + continue; + } + case 'i': + { + if (sscanf(buf, "i%u %255[^\n]%n", + &pos_var_name, var_name, &end) != 2 + || !var_name[0] || buf[end]) + error_aig("could not parse as input name", line_number); + unsigned expected = input_names.size(); + if (pos_var_name >= nb_inputs) + error_aig("value " + std::to_string(pos_var_name) + + " exceeds input count", line_number); + if (pos_var_name != expected) + error_aig("expecting name for input " + + std::to_string(expected), line_number); + if (!names.insert(var_name).second) + error_aig(std::string("name '") + var_name + + "' already used", line_number); + input_names.push_back(var_name); + if (!first_input_line) + first_input_line = line_number; + else + last_input_line = line_number; + nextline(); + break; + } + case 'o': + { + if (sscanf(buf, "o%u %255[^\n]%n", + &pos_var_name, var_name, &end) != 2 + || !var_name[0] || buf[end]) + error_aig("could not parse as output name", line_number); + unsigned expected = output_names.size(); + if (pos_var_name >= nb_outputs) + error_aig("value " + std::to_string(pos_var_name) + + " exceeds output count", line_number); + if (pos_var_name != expected) + error_aig("expecting name for output " + + std::to_string(expected), line_number); + if (!names.insert(var_name).second) + error_aig(std::string("name '") + var_name + + "' already used", line_number); + output_names.push_back(var_name); + if (!first_output_line) + first_output_line = line_number; + else + last_output_line = line_number; + nextline(); + break; + } + case 'c': + { + comment_sec = true; + break; + } + default: + { + error_aig("unsupported line type", line_number); + } + } } - } if (!input_names.empty()) - { - if (input_names.size() != nb_inputs) - error_aig(__LINE__, "Either all or none of the inputs can be named", - 0); - } + { + if (input_names.size() != nb_inputs) + error_aig("either all or none of the inputs should be named", + first_input_line, last_input_line); + } else - input_names = name_vector(nb_inputs, "i"); + { + input_names = name_vector(nb_inputs, "i"); + } if (!output_names.empty()) - { - if (output_names.size() != nb_outputs) - error_aig(__LINE__, "Either all or none of the outputs can be named", - 0); - } + { + if (output_names.size() != nb_outputs) + error_aig("either all or none of the outputs should be named", + first_output_line, last_output_line); + } else - output_names = name_vector(nb_outputs, "o"); - - return std::make_tuple(input_names, output_names, latches, outputs, gates); + { + output_names = name_vector(nb_outputs, "o"); + } + return { input_names, output_names, latches, outputs, gates }; } } diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index e4682ac6b..4ba831b61 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -352,10 +352,10 @@ namespace spot /// \brief Create a circuit from an aag file with restricted syntax. /// /// \note Additional constraints are: - /// - Gates have to appear in an ordered fashion. + /// - inputs, latches, and gates have to appear in increasing order. /// - Inputs are expected to have variable numbers from 2-2*n_i+1 /// with n_i being the number of inputs - /// - Latches can not be named + /// - Latches cannot be named static aig_ptr parse_aag(const std::string& aig_file, bdd_dict_ptr dict = make_bdd_dict()); diff --git a/tests/python/aiger.py b/tests/python/aiger.py index edf7e1563..d6c8f2c93 100644 --- a/tests/python/aiger.py +++ b/tests/python/aiger.py @@ -3391,9 +3391,9 @@ assert(spot.aiger_circuit("""aag 2 2 0 2 0 2 1 i0 a -i1 b +i1 b c c -""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b\no0 o0\no1 o1') +""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b c\no0 o0\no1 o1') assert(spot.aiger_circuit("""aag 2 2 0 2 0 2 @@ -3404,3 +3404,465 @@ o0 x o1 y c """).to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 i0\ni1 i1\no0 x\no1 y') + + +def report_missing_exception(): + raise RuntimeError("missing exception") + +try: + spot.aiger_circuit("""aag 2 2 0 2 +0 +""") +except SyntaxError as e: + assert str(e) == "\n:1: invalid header line" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 2 2 3 2 0 +""") +except SyntaxError as e: + assert str(e) == "\n:1: more variables than indicated by max var" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 2 2 0 2 0\n""") +except SyntaxError as e: + assert str(e) == "\n:2: expecting input number 2" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 2 2 0 2 0 +3 +""") +except SyntaxError as e: + assert str(e) == "\n:2: expecting input number 2" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 2 2 0 2 0 +3 4 5 +""") +except SyntaxError as e: + assert str(e) == "\n:2: invalid format for an input" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 2 2 0 2 0 +2 +""") +except SyntaxError as e: + assert str(e) == "\n:3: expecting input number 4" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 4 2 2 0 0 +2 +4 +1 +""") +except SyntaxError as e: + assert str(e) == "\n:4: invalid format for a latch" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 4 2 2 0 0 +2 +4 +1 1 +""") +except SyntaxError as e: + assert str(e) == "\n:4: expecting latch number 6" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 4 2 2 0 0 +2 +4 +6 1 +""") +except SyntaxError as e: + assert str(e) == "\n:5: expecting latch number 8" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 5 2 2 1 0 +2 +4 +6 1 +8 7 +""") +except SyntaxError as e: + assert str(e) == "\n:6: expecting an output" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 5 2 2 1 0 +2 +4 +6 1 +8 7 +9 9 9 +""") +except SyntaxError as e: + assert str(e) == "\n:6: invalid format for an output" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 5 2 2 1 0 +2 +4 +6 1 +8 7 +9 9 9 +""") +except SyntaxError as e: + assert str(e) == "\n:6: invalid format for an output" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +""") +except SyntaxError as e: + assert str(e) == "\n:7: expecting AND gate number 10" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 8 9 +""") +except SyntaxError as e: + assert str(e) == "\n:7: invalid format for an AND gate" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 +""") +except SyntaxError as e: + assert str(e) == "\n:7: invalid format for an AND gate" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 8 +""") +except SyntaxError as e: + assert str(e) == "\n:8: expecting AND gate number 12" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 8 +12 8 10 +i0 +""") +except SyntaxError as e: + assert str(e) == "\n:9: could not parse as input name" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 8 +12 8 10 +i0 foo +i3 bar +""") +except SyntaxError as e: + assert str(e) == "\n:10: value 3 exceeds input count" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 8 +12 8 10 +i1 bar +i0 foo +""") +except SyntaxError as e: + assert str(e) == "\n:9: expecting name for input 0" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 8 +12 8 10 +i0 name with spaces +i1 name with spaces +""") +except SyntaxError as e: + assert str(e) == \ + "\n:10: name 'name with spaces' already used" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 1 2 +2 +4 +6 1 +8 7 +9 +10 3 8 +12 8 10 +i0 name with spaces +i1 bar +o0 +""") +except SyntaxError as e: + assert str(e) == "\n:11: could not parse as output name" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 2 2 +2 +4 +6 1 +8 7 +9 +10 +10 3 8 +12 8 10 +i0 name with spaces +i1 bar +o1 hmm +o0 foo bar baz +""") +except SyntaxError as e: + assert str(e) == "\n:12: expecting name for output 0" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 2 2 +2 +4 +6 1 +8 7 +9 +10 +10 3 8 +12 8 10 +i0 name with spaces +i1 bar +o0 hmm +o2 foo bar baz +""") +except SyntaxError as e: + assert str(e) == "\n:13: value 2 exceeds output count" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 2 2 +2 +4 +6 1 +8 7 +9 +10 +10 3 8 +12 8 10 +i0 name with spaces +i1 bar +o0 foo +o1 foo +""") +except SyntaxError as e: + assert str(e) == "\n:13: name 'foo' already used" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 2 2 +2 +4 +6 1 +8 7 +9 +10 +10 3 8 +12 8 10 +i0 name with spaces +i1 bar +o0 foo +o1 bar +""") +except SyntaxError as e: + assert str(e) == "\n:13: name 'bar' already used" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 2 2 +2 +4 +6 1 +8 7 +9 +10 +10 3 8 +12 8 10 +i0 name with spaces +i1 bar +o0 foo +o1 baz +this is a bug +""") +except SyntaxError as e: + assert str(e) == "\n:14: unsupported line type" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 2 2 2 2 +2 +4 +6 1 +8 7 +9 +10 +10 3 8 +12 8 10 +i0 name with spaces +o0 foo +o1 baz +c +this is not a bug +""") +except SyntaxError as e: + assert str(e) == \ + "\n:10: either all or none of the inputs should be named" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 3 2 2 2 +2 +4 +6 +8 1 +10 7 +9 +10 +12 3 8 +14 8 10 +i0 name0 +i1 name1 +o0 foo +o1 baz +c +this is not a bug +""") +except SyntaxError as e: + assert str(e) == \ + "\n:11-12: either all or none of the inputs should be named" +else: + report_missing_exception() + +try: + spot.aiger_circuit("""aag 7 3 2 3 2 +2 +4 +6 +8 1 +10 7 +9 +10 +8 +12 3 8 +14 8 10 +i0 name0 +i1 name1 +o0 foo +i2 name2 +o1 baz +c +this is not a bug +""") +except SyntaxError as e: + assert str(e) == \ + "\n:14-16: either all or none of the outputs should be named" +else: + report_missing_exception() + +x = spot.aiger_circuit("""aag 7 3 2 3 2 +2 +4 +6 +8 1 +10 7 +9 +10 +8 +12 3 8 +14 8 10 +i0 name0 space +i1 name1 +o0 foo space +i2 name2 +o1 baz +o2 bar +c +this is not a bug +""").to_str() +assert x == spot.aiger_circuit(x).to_str()