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

@@ -72,14 +72,18 @@ namespace
   parse_aag_impl_(std::istream& iss, const std::string& filename)
   {
 
-    auto error_aig = [fn = filename](int line_src,
+    auto error_aig = [filename](const std::string_view& msg,
-                                     const std::string& msg,
+                                unsigned line_start = 0,
-                                     unsigned line_file)
+                                unsigned line_end = 0)
       {
-        throw parse_error("spot/twaalgos/aiger.cc:" + std::to_string(line_src)
+        std::ostringstream out;
-                          + ": in " + fn + " hit error: " + msg
+        out << filename;
-                          + " at line " + std::to_string(line_file)
+        if (line_start)
-                          + ".\n");
+          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;
+    unsigned line_number = 0;
+    std::unordered_set<std::string> names;
+
+    auto nextline = [&line, &line_number, &iss]() {
+      line.clear();
       getline(iss, line);
-    unsigned line_number = 1;
+      ++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",
+      error_aig("more variables than indicated by max var", line_number);
-                line_number);
 
     latches.reserve(nb_latches);
     outputs.reserve(nb_outputs);
@@ -108,113 +118,129 @@ namespace
 
     for (unsigned i = 0; i < nb_inputs; ++i)
       {
-        if (!iss)
+        nextline();
-          error_aig(__LINE__, "missing input", line_number);
+        unsigned expected = 2 * (i + 1);
-
+        unsigned num = 0;
-        line.clear();
+        int end = 0;
-        getline(iss, line);
+        const char* buf = line.c_str();
-        if ((unsigned)std::stoi(line) != 2*(i+1))
+        if (!line.empty()
-          error_aig(__LINE__, "invalid input numbering for input nbr "
+            && (sscanf(buf, "%u %n", &num, &end) != 1 || buf[end]))
-                    + std::to_string(i), line_number);
+          error_aig("invalid format for an input", line_number);
-        ++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)
+        nextline();
-          error_aig(__LINE__, "missing latch", line_number);
+        unsigned expected = 2 * (1 + nb_inputs + i);
-
+        unsigned latch_var = 0, next_state;
-        line.clear();
+        int end = 0;
-        getline(iss, line);
+        const char* buf = line.c_str();
-        ++line_number;
+        if (!line.empty()
-        unsigned latch_var, next_state;
+            && (sscanf(buf, "%u %u %n", &latch_var, &next_state, &end) != 2
-        if (sscanf(line.c_str(), "%u %u", &latch_var, &next_state) != 2)
+                || buf[end]))
-          error_aig(__LINE__, "invalid latch", line_number);
+          error_aig("invalid format for a latch", line_number);
-        if (latch_var != 2*(1 + nb_inputs + i))
+        if (latch_var != expected)
-          error_aig(__LINE__, "invalid latch numbering", line_number);
+          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)
+        nextline();
-          error_aig(__LINE__, "missing output", line_number);
+        if (line.empty())
-
+          error_aig("expecting an output", line_number);
-        line.clear();
-        getline(iss, line);
-        ++line_number;
         unsigned num_out;
-        if (sscanf(line.c_str(), "%u", &num_out) != 1)
+        const char* buf = line.c_str();
-          error_aig(__LINE__, "invalid output definition", line_number);
+        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;
+        nextline();
-        if (!iss)
+        unsigned and_gate = 0, lhs, rhs;
-          error_aig(__LINE__, "missing AND", line_number);
+        if (!line.empty())
-        line.clear();
+          {
-        getline(iss, line);
+            const char* buf = line.c_str();
-        ++line_number;
+            int end = 0;
-        if (sscanf(line.c_str(), "%u %u %u", &and_gate, &lhs, &rhs) != 3)
+            if (sscanf(buf, "%u %u %u %n", &and_gate, &lhs, &rhs, &end) != 3
-          error_aig(__LINE__, "invalid AND", line_number);
+                || buf[end])
-        if (and_gate != 2*(1 + nb_inputs + nb_latches + i))
+              error_aig("invalid format for an AND gate", line_number);
-          error_aig(__LINE__, "invalid gate numbering. Expected "
+          }
-                    + std::to_string((2*(1 + nb_inputs + nb_latches + i)))
+        unsigned expected = 2 * (1 + nb_inputs + nb_latches + i);
-                    + " got " + std::to_string(and_gate), line_number);
+        if (and_gate != expected)
+          error_aig("expecting AND gate number " + std::to_string(expected),
+                    line_number);
         gates.emplace_back(lhs, rhs);
       }
-    line.clear();
+    nextline();
-
-    getline(iss, line);
-    ++line_number;
     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)
+        int end;
+        const char* buf = line.c_str();
+        switch (buf[0])
           {
-        // latches names non supported
+          case 'l':               // latches names non supported
-        case 'l':
             {
-          line.clear();
+              nextline();
-          getline(iss, line);
-          ++line_number;
               continue;
             }
           case 'i':
             {
-          if (sscanf(line.c_str(), "i%u %255s", &pos_var_name, var_name) != 2
+              if (sscanf(buf, "i%u %255[^\n]%n",
-              || pos_var_name >= nb_inputs)
+                         &pos_var_name, var_name, &end) != 2
-            error_aig(__LINE__, "could not parse input name: "
+                  || !var_name[0] || buf[end])
-                      + line, line_number);
+                error_aig("could not parse as input name", line_number);
-          auto itn = std::find(input_names.begin(), input_names.end(),
+              unsigned expected = input_names.size();
-                               var_name);
+              if (pos_var_name >= nb_inputs)
-          if (itn != input_names.end())
+                error_aig("value " + std::to_string(pos_var_name)
-            error_aig(__LINE__, std::string("input name ") + var_name
+                          + " exceeds input count", line_number);
-                                + " appears twice", 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);
-          line.clear();
+              if (!first_input_line)
-          getline(iss, line);
+                first_input_line = line_number;
-          ++line_number;
+              else
+                last_input_line = line_number;
+              nextline();
               break;
             }
           case 'o':
             {
-          if (sscanf(line.c_str(), "o%u %255s", &pos_var_name, var_name) != 2
+              if (sscanf(buf, "o%u %255[^\n]%n",
-              || pos_var_name >= nb_outputs)
+                         &pos_var_name, var_name, &end) != 2
-          error_aig(__LINE__, "could not parse output name: "
+                  || !var_name[0] || buf[end])
-                    + line, line_number);
+                error_aig("could not parse as output name", line_number);
-          auto itn = std::find(output_names.begin(), output_names.end(),
+              unsigned expected = output_names.size();
-                               var_name);
+              if (pos_var_name >= nb_outputs)
-          if (itn != output_names.end())
+                error_aig("value " + std::to_string(pos_var_name)
-            error_aig(__LINE__, std::string("output name ") + var_name +
+                          + " exceeds output count", line_number);
-                                " appears twice", 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);
-          line.clear();
+              if (!first_output_line)
-          getline(iss, line);
+                first_output_line = line_number;
-          ++line_number;
+              else
+                last_output_line = line_number;
+              nextline();
               break;
             }
           case 'c':
@@ -224,28 +250,31 @@ namespace
             }
           default:
             {
-          error_aig(__LINE__, "invalid line", line_number);
+              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",
+          error_aig("either all or none of the inputs should be named",
-                  0);
+                    first_input_line, last_input_line);
       }
     else
+      {
         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",
+          error_aig("either all or none of the outputs should be named",
-                0);
+                    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);
+    return { input_names, output_names, latches, outputs, gates };
   }
 }
 

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

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