Adjust STL label parsing

Changes the accepted format for labels and wraps instructions that have
a label in a code label.

Author: MatWise

src/statement-list/converters/convert_string_value.cpp

@@ -32,10 +32,12 @@ string_constantt convert_version(const std::string &src)
   return result;
 }
 
-code_labelt convert_label(const std::string &src)
+string_constantt convert_label(const std::string &src)
 {
   // Cut the trailing colon
   std::string value = src.substr(0, src.length() - 1);
 
-  return code_labelt{value, codet(ID_label)};
+  string_constantt result{value};
+  result.set(ID_statement_list_type, ID_label);
+  return result;
 }

src/statement-list/converters/convert_string_value.h

@@ -32,7 +32,7 @@ string_constantt convert_version(const std::string &src);
 
 /// Converts a string into a Statement List label.
 /// \param src: String returned by the parser.
-/// \return Code label expression representing the label.
-code_labelt convert_label(const std::string &src);
+/// \return String constant representing the label.
+string_constantt convert_label(const std::string &src);
 
 #endif // CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_STRING_VALUE_H

src/statement-list/parser.y

@@ -688,7 +688,7 @@ Oom_IL_Instruction:
     ;
 
 IL_Instruction: 
-    Opt_Label Opt_Instruction ';'
+    Opt_Label Instruction ';'
     {
       $$ = $2;
       parser_stack($$).add_to_operands(std::move(parser_stack($1)));
@@ -708,14 +708,9 @@ IL_Label:
     TOK_LABEL
     ;
 
-Opt_Instruction:
+Instruction:
     IL_Simple_Operation
     | IL_Invocation
-    | /* nothing */
-    {
-      newstack($$);
-      parser_stack($$).id(ID_statement_list_instruction);
-    }
     ;
 
 IL_Simple_Operation: 

src/statement-list/scanner.l

@@ -272,7 +272,7 @@ void statement_list_scanner_init()
                         return TOK_IDENTIFIER; 
                       }
 
-  [a-zA-Z_\.][a-zA-Z0-9_\.]*: {
+  [a-zA-Z_][a-zA-Z0-9_]*: {
                         newstack(yystatement_listlval);
                         parser_stack(yystatement_listlval) = 
                           convert_label(yytext);

src/statement-list/statement_list_parser.cpp

@@ -248,7 +248,7 @@ static exprt find_network_instructions(const exprt &network)
   UNREACHABLE; // Network expression should always have an instruction list
 }
 
-/// Adds all valid  instructions to the given network.
+/// Adds all valid instructions to the given network.
 /// \param network: The network to which the instructions belong.
 /// \param instructions: The root expression of a valid instruction list.
 static void find_instructions(
@@ -258,13 +258,24 @@ static void find_instructions(
   for(const exprt &instruction_expr : instructions.operands())
   {
     statement_list_parse_treet::instructiont instruction;
+
     codet code_token(to_multi_ary_expr(instruction_expr).op0().id());
-    for(const exprt &operand : instruction_expr.operands())
+    string_constantt label{ID_nil};
+    for(auto op_it = std::next(instruction_expr.operands().begin());
+        op_it != end(instruction_expr.operands());
+        ++op_it)
     {
-      if(operand.is_not_nil() && operand.id() != code_token.get_statement())
-        code_token.add_to_operands(operand);
+      if(op_it->get(ID_statement_list_type) == ID_label)
+        label = to_string_constant(*op_it);
+      else if(op_it->is_not_nil())
+        code_token.add_to_operands(*op_it);
     }
-    instruction.add_token(code_token);
+
+    if(label.get_value() == ID_nil)
+      instruction.add_token(code_token);
+    else
+      instruction.add_token(code_labelt{label.get_value(), code_token});
+
     network.add_instruction(instruction);
   }
 }