From f6fadf4ad1b10c61e2e8da2f513ec4bf2178dbcf Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 20 Dec 2025 12:03:49 -0800
Subject: [PATCH] SMV: grammar for asynchronous processes

This adds the grammar for "process" module instantiations.  They are errored
as unsupported by the type checker.
---
 regression/smv/process/process1.desc |  6 +++---
 src/hw_cbmc_irep_ids.h               |  1 +
 src/smvlang/parser.y                 | 20 +++++++++++++++-----
 src/smvlang/smv_typecheck.cpp        | 14 +++++++++++++-
 4 files changed, 32 insertions(+), 9 deletions(-)

diff --git a/regression/smv/process/process1.desc b/regression/smv/process/process1.desc
index 55a48b851..268f47784 100644
--- a/regression/smv/process/process1.desc
+++ b/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.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index c56f6fd4b..fc1bdcf6a 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -42,6 +42,7 @@ IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_signed_cast)
 IREP_ID_ONE(smv_signed_word)
 IREP_ID_ONE(smv_sizeof)
+IREP_ID_ONE(smv_process_module_instance)
 IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 5a798f80b..d71ea3c96 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -589,16 +589,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;
            }
            ;
 
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 1994bc966..e80f10e30 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/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";
+    }
   }
 }
 
@@ -2277,8 +2285,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;