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()