SMV: grammar for asynchronous processes

This adds the grammar for "process" module instantiations.  They are errored
as unsupported by the type checker.

Author: kroening

regression/smv/process/process1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 process1.smv
 
-^EXIT=0$
+^file .* line 8: no support for asynchronous processes$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This does not parse.

src/hw_cbmc_irep_ids.h

@@ -39,6 +39,7 @@ IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_signed_cast)
 IREP_ID_ONE(smv_sizeof)
 IREP_ID_ONE(smv_module_instance)
+IREP_ID_ONE(smv_process_module_instance)
 IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)

src/smvlang/parser.y

@@ -598,16 +598,26 @@ simple_type_specifier:
            ;
 
 module_type_specifier:
-             module_name
+             module_name parameter_list_paren_opt
            {
              init($$, ID_smv_module_instance);
              to_smv_module_instance_type(stack_type($$)).base_name(stack_expr($1).id());
+             stack_expr($$).operands().swap(stack_expr($2).operands());
            }
-           | module_name '(' parameter_list ')'
+           | process_Token module_name parameter_list_paren_opt
            {
-             init($$, ID_smv_module_instance);
-             to_smv_module_instance_type(stack_type($$)).base_name(stack_expr($1).id());
-             stack_expr($$).operands().swap(stack_expr($3).operands());
+             init($$, ID_smv_process_module_instance);
+           }
+           ;
+
+parameter_list_paren_opt:
+             /* optional */
+           {
+             init($$);
+           }
+           | '(' parameter_list ')'
+           {
+             $$ = $2;
            }
            ;
 

src/smvlang/smv_typecheck.cpp

@@ -261,6 +261,14 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
         instance.arguments(),
         instance.source_location());
     }
+
+    if(
+      element.is_var() &&
+      element.expr.type().id() == ID_smv_process_module_instance)
+    {
+      throw errort().with_location(element.expr.source_location())
+        << "no support for asynchronous processes";
+    }
   }
 }
 
@@ -2226,8 +2234,12 @@ void smv_typecheckt::create_var_symbols(
       else
         symbol.pretty_name = strip_smv_prefix(symbol.name);
 
-      if(symbol.type.id() == ID_smv_module_instance)
+      if(
+        symbol.type.id() == ID_smv_module_instance ||
+        symbol.type.id() == ID_smv_process_module_instance)
+      {
         symbol.is_input = false;
+      }
       else
         symbol.is_input = true;