Merge pull request #5054 from MatWise/feature/statement-list-jumps

Statement List: Jump instructions

Author: tautschnig

regression/statement-list/Jump1/main.awl

@@ -0,0 +1,37 @@
+FUNCTION_BLOCK "Main"
+VERSION : 0.1
+   VAR_TEMP 
+      temp1 : Bool;
+      temp2 : Bool;
+   END_VAR
+BEGIN
+NETWORK
+TITLE =
+      SET;
+      = temp1;
+      = temp2;
+      JU lab0;
+      CALL "__CPROVER_assert"
+      (  condition := FALSE
+      );
+lab0: SET;
+lab1: A temp1;
+      A temp2;
+      NOT;
+      = temp2;
+      A temp2;
+
+      JCN lab1;
+      CALL "__CPROVER_assert"
+      (  condition := #temp2
+      );
+
+      JC lab2;
+      CALL "__CPROVER_assert"
+      (  condition := FALSE
+      );
+
+lab2: NOP 0;
+
+END_FUNCTION_BLOCK
+

regression/statement-list/Jump1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.awl
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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/converters/expr2statement_list.cpp

@@ -59,7 +59,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 /// such. This can reduce complexity in some cases.
 /// \param lhs: Left side of the binary expression.
 /// \param rhs: Right side of the binary expression.
-/// \return: List of instrumented operands.
+/// \return List of instrumented operands.
 static std::vector<exprt>
 instrument_equal_operands(const exprt &lhs, const exprt &rhs)
 {
@@ -93,7 +93,7 @@ instrument_equal_operands(const exprt &lhs, const exprt &rhs)
 
 /// Checks if the expression or one of its parameters is not of type bool.
 /// \param expr: Expression to verify.
-/// \return: True if the expression and its operands are not or only partially
+/// \return True if the expression and its operands are not or only partially
 ///   of type bool, false otherwise.
 static bool is_not_bool(const exprt &expr)
 {

src/statement-list/converters/expr2statement_list.h

@@ -62,7 +62,7 @@ class expr2stlt
   /// recursively in the process.
   /// \param expr: Expression to convert. Operands of this expression will be
   ///   converted as well via recursion.
-  /// \return: String containing human-readable STL code for the expression.
+  /// \return String containing human-readable STL code for the expression.
   std::string convert(const exprt &expr);
 
 private:
@@ -147,7 +147,7 @@ class expr2stlt
   /// Returns the given identifier in a form that is compatible with STL by
   /// looking up the symbol or cutting the scope when needed.
   /// \param identifier: Identifier that should be converted.
-  /// \return: Converted identifier.
+  /// \return Converted identifier.
   irep_idt id_shorthand(const irep_idt &identifier);
 };
 

src/statement-list/parser.y

@@ -128,6 +128,9 @@ extern char *yystatement_listtext;
 %token TOK_ACCU_DINT_GTE        ">=D"
 %token TOK_ACCU_DINT_LTE        "<=D"
 %token TOK_ASSIGNMENT           ":="
+%token TOK_JUMP_UNCONDITIONAL   "JU"
+%token TOK_JUMP_CONDITIONAL     "JC"
+%token TOK_JUMP_CONDITIONAL_NOT "JCN"
 
 /*** Value tokens ***/
 %token TOK_INT_LITERAL
@@ -668,7 +671,7 @@ Opt_Instruction_List:
     }
     ;
 
-// Structured Text grammar
+// Statement List grammar
 Instruction_List: 
     Oom_IL_Instruction
     ;
@@ -688,7 +691,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 +711,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: 
@@ -932,12 +930,12 @@ IL_Simple_Operator:
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_xor);
-    }  
+    }
     | TOK_XOR_NOT
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_xor_not);
-    } 
+    }
     | TOK_AND_NESTED 
     {
       $$ = $1;
@@ -947,22 +945,22 @@ IL_Simple_Operator:
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_and_not_nested);
-    } 
+    }
     | TOK_OR_NESTED
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_or_nested);
-    } 
+    }
     | TOK_OR_NOT_NESTED
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_or_not_nested);
-    }  
+    }
     | TOK_XOR_NESTED 
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_xor_nested);
-    }  
+    }
     | TOK_XOR_NOT_NESTED
     {
       $$ = $1;
@@ -972,7 +970,7 @@ IL_Simple_Operator:
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_nesting_closed);
-    }  
+    }
     | TOK_ASSIGN
     {
       $$ = $1;
@@ -987,7 +985,7 @@ IL_Simple_Operator:
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_clr_rlo);
-    } 
+    }
     | TOK_SET
     {
       $$ = $1;
@@ -997,12 +995,27 @@ IL_Simple_Operator:
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_reset);
-    } 
+    }
     | TOK_NOT
     {
       $$ = $1;
       parser_stack($$).id(ID_statement_list_not);
-    }  
+    }
+    | TOK_JUMP_UNCONDITIONAL
+    {
+      $$ = $1;
+      parser_stack($$).id(ID_statement_list_jump_unconditional);
+    }
+    | TOK_JUMP_CONDITIONAL
+    {
+      $$ = $1;
+      parser_stack($$).id(ID_statement_list_jump_conditional);
+    }
+    | TOK_JUMP_CONDITIONAL_NOT
+    {
+      $$ = $1;
+      parser_stack($$).id(ID_statement_list_jump_conditional_not);
+    }
     ;
 
 IL_Operand:

src/statement-list/scanner.l

@@ -165,6 +165,9 @@ void statement_list_scanner_init()
   \<D                 { loc(); return TOK_ACCU_DINT_LT; }
   \>=D                { loc(); return TOK_ACCU_DINT_GTE; }
   \<=D                { loc(); return TOK_ACCU_DINT_LTE; }
+  JU                  { loc(); return TOK_JUMP_UNCONDITIONAL; }
+  JC                  { loc(); return TOK_JUMP_CONDITIONAL; }
+  JCN                 { loc(); return TOK_JUMP_CONDITIONAL_NOT; }
 
   (10#)?[\+-]?[0-9]+ { 
                         newstack(yystatement_listlval);
@@ -272,7 +275,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_language.h

@@ -32,7 +32,7 @@ class statement_list_languaget : public languaget
   /// instance's parse tree.
   /// \param instream: Input to parse.
   /// \param path: Path of the input.
-  /// \return: False if successful.
+  /// \return False if successful.
   bool parse(std::istream &instream, const std::string &path) override;
 
   /// Currently unused.
@@ -45,7 +45,7 @@ class statement_list_languaget : public languaget
   /// \param module: Name of the file that has been parsed.
   /// \param keep_file_local: Set to true if local variables of this module
   ///   should be included in the table.
-  /// \return: False if no errors occurred, true otherwise.
+  /// \return False if no errors occurred, true otherwise.
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,

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