Add support for constants in STL function calls

The STL grammar allows the direct use of constants when calling a
function. This commit implements this behaviour in order to simplify
function calls and to provide a better compatibility to existing STL
code.

Author: MatWise

src/statement-list/parser.y

@@ -1080,7 +1080,7 @@ Oom_Param_Assignment:
     ;
 
 Param_Assignment:
-    Variable_Name TOK_ASSIGNMENT Variable_Access
+    Variable_Name TOK_ASSIGNMENT IL_Operand
     {
       newstack($$);
       parser_stack($$) = equal_exprt{std::move(parser_stack($1)), 

src/statement-list/statement_list_parse_tree_io.cpp

@@ -15,6 +15,7 @@ Author: Matthias Weiss, [email protected]
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
 
+/// String to indicate that there is no value.
 #define NO_VALUE "(none)"
 
 /// Prints a constant to the given output stream.
@@ -35,6 +36,21 @@ static void output_constant(std::ostream &out, const constant_exprt &constant)
     out << constant.get_value();
 }
 
+/// Prints the assignment of a module parameter to the given output stream.
+/// \param [out] out: Stream that should receive the result.
+/// \param assignment: Assignment that shall be printed.
+static void
+output_parameter_assignment(std::ostream &out, const equal_exprt &assignment)
+{
+  out << assignment.lhs().get(ID_identifier) << " := ";
+  const constant_exprt *const constant =
+    expr_try_dynamic_cast<constant_exprt>(assignment.rhs());
+  if(constant)
+    output_constant(out, *constant);
+  else
+    out << assignment.rhs().get(ID_identifier);
+}
+
 void output_parse_tree(
   std::ostream &out,
   const statement_list_parse_treet &parse_tree)
@@ -214,9 +230,11 @@ void output_instruction(
     out << token.get_statement();
     for(const auto &expr : token.operands())
     {
-      if(expr.id() == ID_symbol)
+      const symbol_exprt *const symbol =
+        expr_try_dynamic_cast<symbol_exprt>(expr);
+      if(symbol)
       {
-        out << '\t' << expr.get(ID_identifier);
+        out << '\t' << symbol->get_identifier();
         continue;
       }
       const constant_exprt *const constant =
@@ -227,14 +245,14 @@ void output_instruction(
         output_constant(out, *constant);
         continue;
       }
-      const equal_exprt *const eq = expr_try_dynamic_cast<equal_exprt>(expr);
-      if(eq)
+      const equal_exprt *const equal = expr_try_dynamic_cast<equal_exprt>(expr);
+      if(equal)
       {
-        out << "\n\t" << eq->lhs().get(ID_identifier)
-            << " := " << eq->rhs().get(ID_identifier);
+        out << "\n\t";
+        output_parameter_assignment(out, *equal);
+        continue;
       }
-      else
-        out << '\t' << expr.id();
+      out << '\t' << expr.id();
     }
   }
 }

src/statement-list/statement_list_typecheck.cpp

@@ -1272,11 +1272,8 @@ void statement_list_typecheckt::typecheck_CPROVER_assert(
     expr_try_dynamic_cast<equal_exprt>(op_code.op1());
   if(assignment)
   {
-    const symbol_exprt &rhs{to_symbol_expr(assignment->rhs())};
-    // Check if identifier is present, create assertion and add it to the
-    // function body.
-    const exprt op{typecheck_identifier(tia_element, rhs.get_identifier())};
-    const code_assertt assertion{op};
+    const code_assertt assertion{
+      typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
     tia_element.value.add_to_operands(assertion);
   }
   else
@@ -1294,11 +1291,8 @@ void statement_list_typecheckt::typecheck_CPROVER_assume(
     expr_try_dynamic_cast<equal_exprt>(op_code.op1());
   if(assignment)
   {
-    const symbol_exprt &rhs{to_symbol_expr(assignment->rhs())};
-    // Check if identifier is present, create assumption and add it to the
-    // function body.
-    const exprt op{typecheck_identifier(tia_element, rhs.get_identifier())};
-    const code_assumet assumption{op};
+    const code_assumet assumption{
+      typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
     tia_element.value.add_to_operands(assumption);
   }
   else
@@ -1354,18 +1348,12 @@ void statement_list_typecheckt::typecheck_called_function(
   for(const auto &expr : op_code.operands())
   {
     if(can_cast_expr<equal_exprt>(expr))
-    {
-      const equal_exprt &assignment{to_equal_expr(expr)};
-      assignments.push_back(assignment);
-    }
+      assignments.push_back(to_equal_expr(expr));
   }
 
   for(const code_typet::parametert &param : params)
-  {
-    const exprt &arg{
-      typecheck_function_call_arguments(assignments, param, tia_element)};
-    args.push_back(arg);
-  }
+    args.emplace_back(
+      typecheck_function_call_arguments(assignments, param, tia_element));
 
   // Check the return value if present.
   if(called_type.return_type().is_nil())
@@ -1404,9 +1392,9 @@ exprt statement_list_typecheckt::typecheck_function_call_arguments(
     const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
     if(param_name == lhs.get_identifier())
     {
-      const symbol_exprt &rhs{to_symbol_expr(assignment.rhs())};
-      const exprt assigned_variable{
-        typecheck_identifier(tia_element, rhs.get_identifier())};
+      exprt assigned_variable{
+        typecheck_function_call_argument_rhs(tia_element, assignment.rhs())};
+
       if(param_type == assigned_variable.type())
         return assigned_variable;
       else
@@ -1423,6 +1411,21 @@ exprt statement_list_typecheckt::typecheck_function_call_arguments(
   throw TYPECHECK_ERROR;
 }
 
+exprt statement_list_typecheckt::typecheck_function_call_argument_rhs(
+  const symbolt &tia_element,
+  const exprt &rhs)
+{
+  exprt assigned_operand;
+  const symbol_exprt *const symbol_rhs =
+    expr_try_dynamic_cast<symbol_exprt>(rhs);
+  if(symbol_rhs)
+    assigned_operand =
+      typecheck_identifier(tia_element, symbol_rhs->get_identifier());
+  else // constant_exprt.
+    assigned_operand = rhs;
+  return assigned_operand;
+}
+
 exprt statement_list_typecheckt::typecheck_return_value_assignment(
   const std::vector<equal_exprt> &assignments,
   const typet &return_type,

src/statement-list/statement_list_typecheck.h

@@ -592,6 +592,15 @@ class statement_list_typecheckt : public typecheckt
     const code_typet::parametert &param,
     const symbolt &tia_element);
 
+  /// Checks if the given assigned expression is a variable or a constant and
+  /// returns the typechecked version.
+  /// \param tia_element: Symbol representation of the TIA element.
+  /// \param rhs: Expression that the function parameter got assigned to.
+  /// \return: Expression of either a symbol or a constant.
+  exprt typecheck_function_call_argument_rhs(
+    const symbolt &tia_element,
+    const exprt &rhs);
+
   /// Checks if there is a return value assignment inside of the assignment
   /// list of a function call and returns the expression of the assigned
   /// variable.