Updates type checking to handle new assigns-clause constructs

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

src/ansi-c/c_typecheck_base.cpp

@@ -156,9 +156,44 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
     }
     else
     {
-      // we don't need the identifiers
-      for(auto &parameter : to_code_type(symbol.type).parameters())
-        parameter.set_identifier(irep_idt());
+      code_typet &code_type = to_code_type(symbol.type);
+
+      // Add the parameter declarations into the symbol table.
+      for(auto &parameter : code_type.parameters())
+      {
+        std::string symbol_name = id2string(symbol.name);
+
+        // CPROVER primitives, anonymous, builtin and atomics do not need identifiers
+        if(
+          symbol_name.find("__atomic_") != std::string::npos ||
+          symbol_name.find("__builtin_") != std::string::npos ||
+          symbol_name.find("__CPROVER_") != std::string::npos ||
+          symbol_name.find("__VERIFIER_") != std::string::npos ||
+          parameter.get_base_name().empty())
+        {
+          parameter.set_identifier(irep_idt());
+        }
+        else
+        {
+          // produce identifier
+          irep_idt identifier =
+            symbol_name + "::" + id2string(parameter.get_base_name());
+          parameter.set_identifier(identifier);
+
+          parameter_symbolt parameter_symbol;
+          parameter_symbol.type = parameter.type();
+          parameter_symbol.name = identifier;
+          parameter_symbol.base_name = parameter.get_base_name();
+          parameter_symbol.location = parameter.source_location();
+
+          symbolt *new_parameter_symbol;
+
+          symbol.mode = mode;
+          symbol.module = module;
+
+          move_symbol(parameter_symbol, new_parameter_symbol);
+        }
+      }
     }
   }
   else if(!symbol.is_macro)
@@ -341,7 +376,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
     }
 
     // do body
-
     if(new_symbol.value.is_not_nil())
     {
       if(old_symbol.value.is_not_nil())
@@ -379,6 +413,21 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
           throw 0;
         }
       }
+      else if(old_ct.parameters().size() > 0) // previous declaration
+      {
+        // remove parameter declarations to avoid conflicts
+        for(const auto &old_parameter : old_ct.parameters())
+        {
+          const irep_idt &identifier = old_parameter.get_identifier();
+
+          symbol_tablet::symbolst::const_iterator parameter_symbol_it =
+            symbol_table.symbols.find(identifier);
+          if(parameter_symbol_it != symbol_table.symbols.end())
+          {
+            symbol_table.erase(parameter_symbol_it);
+          }
+        }
+      }
       else if(inlined)
       {
         // preserve "extern inline" properties
@@ -402,6 +451,29 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
       // move body
       old_symbol.value.swap(new_symbol.value);
 
+      // Copy contract over, if it exists
+      const code_typet &old_type = to_code_type(old_symbol.type);
+      exprt old_assigns =
+        static_cast<const exprt &>(old_type.find(ID_C_spec_assigns));
+      exprt old_requires =
+        static_cast<const exprt &>(old_type.find(ID_C_spec_requires));
+      exprt old_ensures =
+        static_cast<const exprt &>(old_type.find(ID_C_spec_ensures));
+      if(old_assigns.is_not_nil())
+      {
+        new_symbol.type.get_named_sub().add(
+          ID_C_spec_assigns, std::move(old_assigns));
+      }
+      if(old_requires.is_not_nil())
+      {
+        new_symbol.type.get_named_sub().add(
+          ID_C_spec_requires, std::move(old_requires));
+      }
+      if(old_ensures.is_not_nil())
+      {
+        new_symbol.type.move_to_named_sub(ID_C_spec_ensures, old_ensures);
+      }
+
       // overwrite type (because of parameter names)
       old_symbol.type=new_symbol.type;
     }
@@ -729,13 +801,12 @@ void c_typecheck_baset::typecheck_declaration(
       declarator.set_name(identifier);
 
       // If the declarator is for a function definition, typecheck it.
+      typecheck_symbol(symbol);
       if(can_cast_type<code_typet>(declarator.type()))
       {
         typecheck_assigns(to_code_type(declarator.type()), contract);
       }
 
-      typecheck_symbol(symbol);
-
       // add code contract (if any); we typecheck this after the
       // function body done above, so as to have parameter symbols
       // available
@@ -754,15 +825,15 @@ void c_typecheck_baset::typecheck_declaration(
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
       parameter_map.clear();
 
-      irept assigns_to_add = contract.find(ID_C_spec_assigns);
-      if(assigns_to_add.is_not_nil())
-        new_symbol.type.add(ID_C_spec_assigns) = assigns_to_add;
-      irept requires_to_add = contract.find(ID_C_spec_requires);
-      if(requires_to_add.is_not_nil())
-        new_symbol.type.add(ID_C_spec_requires) = requires_to_add;
-      irept ensures_to_add = contract.find(ID_C_spec_ensures);
-      if(ensures_to_add.is_not_nil())
-        new_symbol.type.add(ID_C_spec_ensures) = ensures_to_add;
+      if(contract.find(ID_C_spec_assigns).is_not_nil())
+        new_symbol.type.add(ID_C_spec_assigns) =
+          contract.find(ID_C_spec_assigns);
+      if(contract.find(ID_C_spec_requires).is_not_nil())
+        new_symbol.type.add(ID_C_spec_requires) =
+          contract.find(ID_C_spec_requires);
+      if(contract.find(ID_C_spec_ensures).is_not_nil())
+        new_symbol.type.add(ID_C_spec_ensures) =
+          contract.find(ID_C_spec_ensures);
     }
   }
 }

src/ansi-c/c_typecheck_expr.cpp

@@ -491,6 +491,40 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   {
     // already type checked
   }
+  else if(expr.id() == ID_int_range)
+  {
+    // already type checked
+    exprt &lower = to_int_range_exprt(expr).op0();
+    exprt &upper = to_int_range_exprt(expr).op1();
+
+    if(lower.id() == ID_constant || lower.id() == ID_identifier)
+    {
+      dstringt c_type = lower.type().get(ID_C_c_type);
+      if(c_type != ID_signed_int.c_str() && c_type != ID_unsigned_int.c_str())
+      {
+        error().source_location = expr.source_location();
+        error() << "Lower bound of range should be an integer, but got: "
+                << lower.type().pretty() << eom;
+        throw 0;
+      }
+    }
+
+    if(upper.id() == ID_constant || upper.id() == ID_identifier)
+    {
+      dstringt upper_type = upper.type().get(ID_C_c_type);
+      if(upper_type != ID_signed_int.c_str() && upper_type != ID_unsigned_int.c_str())
+      {
+        error().source_location = expr.source_location();
+        error() << "Upper bound of range should be an integer, but got: "
+                << upper.pretty() << eom;
+        throw 0;
+      }
+    }
+  }
+  else if(expr.id() == ID_array_range)
+  {
+    // Already type checked
+  }
   else
   {
     error().source_location = expr.source_location();