Checks for multiple init and next blocks and throws a parser error if encountered

src/main/scala/uclid/UclidMain.scala

@@ -389,21 +389,10 @@ object UclidMain {
           (acc, module) => {
             val declsP = {
               val nonInitAccDecls = acc.decls.filter(p => !p.isInstanceOf[InitDecl])
-              val initAccDecls = acc.decls.filter(p => p.isInstanceOf[InitDecl]).headOption
+              val initAccDecls = acc.decls.filter(p => p.isInstanceOf[InitDecl])
               val nonInitModuleDecls = module.decls.filter(p => !p.isInstanceOf[InitDecl])
-              val initModuleDecls = module.decls.filter(p => p.isInstanceOf[InitDecl]).headOption
-              val newInitDecl = initAccDecls match {
-                case Some(initAcc) => initModuleDecls match {
-                  case Some(initMod) => List(InitDecl(BlockStmt(List[BlockVarsDecl](), 
-                    List(initAcc.asInstanceOf[InitDecl].body, initMod.asInstanceOf[InitDecl].body))))
-                  case None => List(initAcc)
-                }
-                case None => initModuleDecls match {
-                  case Some(initMod) => List(initMod)
-                  case None => List[Decl]()
-                }
-              }
-              newInitDecl ++ nonInitAccDecls ++ nonInitModuleDecls
+              val initModuleDecls = module.decls.filter(p => p.isInstanceOf[InitDecl])
+              initAccDecls ++ initModuleDecls ++ nonInitAccDecls ++ nonInitModuleDecls
             }
             val cmdsP = (acc.cmds ++ module.cmds)
             Utils.assert(module.notes.size == 1 && module.notes.head.asInstanceOf[InstanceVarMapAnnotation].iMap.size == 0, "Expected module to initially have empty annotations.")

src/main/scala/uclid/lang/ModuleCanonicalizer.scala

@@ -42,9 +42,28 @@ package lang
 
 class ModuleCanonicalizerPass extends RewritePass {
   override def rewriteModule(moduleIn : Module, ctx : Scope) : Option[Module] = {
+    // Currently we only allow one init and one next block in a module.
+    // we could alternatively, combine multiple init (or next) blocks into a single init (or next) block.
+    var errors: List[(String, lang.ASTPosition)] = List.empty
+    val initdecls = moduleIn.decls.filter(_.isInstanceOf[InitDecl]).map(_.asInstanceOf[InitDecl])
+    if(initdecls.size > 1) {
+      val msg = "Module has multiple init blocks. This is not allowed."
+      val position = initdecls(1).position
+      errors = errors :+ (msg, position)
+    }
+    val nextdecls = moduleIn.decls.filter(_.isInstanceOf[NextDecl]).map(_.asInstanceOf[NextDecl])
+    if(nextdecls.size > 1) {
+      val msg = "Module has multiple next blocks. This is not allowed."
+      val position = nextdecls(1).position
+      errors = errors :+ (msg, position)
+    }
+    if(errors.nonEmpty) {
+      throw throw new Utils.ParserErrorList(errors)
+    }
+
     val initP = moduleIn.init match {
       case None => Some(InitDecl(SkipStmt()))
-      case Some(_) => None
+      case Some(_) =>  None
     }
     val nextP = moduleIn.next match {
       case None => Some(NextDecl(SkipStmt()))

src/test/scala/ParserSpec.scala

@@ -211,18 +211,6 @@ class ParserSpec extends AnyFlatSpec {
     val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
     assert (instantiatedModules.size == 1)
   }
-  "test-type1.ucl" should "not parse successfully." in {
-    try {
-      val filename = "test/test-type1.ucl"
-      val fileModules = UclidMain.compile(ConfigCons.createConfig(filename), lang.Identifier("main"))
-      assert (fileModules.size == 1)
-    }
-    catch {
-      case p : Utils.ParserErrorList =>
-        assert (p.errors.size == 1)
-        assert (p.errors(0)._1.contains("Redeclaration of identifier 'test'."))
-    }
-  }
   "test-typechecker-0.ucl" should "not parse successfully." in {
     try {
       val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-typechecker-0.ucl"), lang.Identifier("main"))
@@ -258,6 +246,28 @@ class ParserSpec extends AnyFlatSpec {
         assert (p.errors.size == 5)
     }
   }
+  "test-multiple-init-blocks.ucl" should "not parse successfully." in {
+    try {
+      val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-multiple-init-blocks.ucl"), lang.Identifier("main"))
+      // should never get here.
+      assert (false);
+    }
+    catch {
+      case p : Utils.ParserErrorList =>
+        assert (p.errors.size == 1)
+    }
+  }
+  "test-multiple-next-blocks.ucl" should "not parse successfully." in {
+    try {
+      val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-multiple-next-blocks.ucl"), lang.Identifier("main"))
+      // should never get here.
+      assert (false);
+    }
+    catch {
+      case p : Utils.ParserErrorList =>
+        assert (p.errors.size == 1)
+    }
+  }
   "test-typechecker-6.ucl" should "not parse successfully." in {
     try {
       val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-typechecker-6.ucl"), lang.Identifier("main"))
@@ -414,26 +424,34 @@ class ParserSpec extends AnyFlatSpec {
     val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
     assert (instantiatedModules.size == 1)
   }
-  "test-concat-modules-w-init-1.ucl" should "parse successfully" in {
-    val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-concat-modules-w-init-1.ucl"), lang.Identifier("main"))
-    val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
-    assert (instantiatedModules.size == 1)
+  // multiple inits not allowed
+  "test-concat-modules-w-init-1.ucl" should "not parse successfully" in {
+    try {
+      val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-concat-modules-w-init-1.ucl"), lang.Identifier("main"))
+      // should never get here.
+      assert (false);
+    }
+    catch {
+      // this list has all the errors from parsing
+      case p : Utils.ParserErrorList =>
+        assert (p.errors.size == 1)
+        assert (p.errors.exists(p => p._1.contains("Module has multiple init blocks.")))
+    }
   }
-  "test-concat-modules-w-init-2-fab.ucl" should "parse successfully" in {
-    val fileModules = UclidMain.compile(UclidMain.Config(files=List(
+  "test-concat-modules-w-init-2-fab.ucl" should "not parse successfully" in {
+    try{
+      val fileModules = UclidMain.compile(UclidMain.Config(files=List(
       new File("test/test-concat-modules-w-init-2-fa.ucl"), new File("test/test-concat-modules-w-init-2-fb.ucl"))
     ), lang.Identifier("main"))
-    assert (fileModules.size == 2)
-    val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
-    assert (instantiatedModules.size == 1)
-  }
-  "test-concat-modules-w-init-2-fba.ucl" should "parse successfully" in {
-    val fileModules = UclidMain.compile(UclidMain.Config(files=List(
-      new File("test/test-concat-modules-w-init-2-fb.ucl"), new File("test/test-concat-modules-w-init-2-fa.ucl"))
-    ), lang.Identifier("main"))
-    assert (fileModules.size == 2)
-    val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
-    assert (instantiatedModules.size == 1)
+      // should never get here.
+      assert (false);
+    }
+    catch {
+      // this list has all the errors from parsing
+      case p : Utils.ParserErrorList =>
+        assert (p.errors.size == 1)
+        assert (p.errors.exists(p => p._1.contains("Module has multiple init blocks")))
+    }
   }
   "test-mod-set-analysis-0.ucl" should "parse successfully." in {
     val fileModules = UclidMain.compile(ConfigCons.createConfigWithMSA("test/test-mod-set-analysis-0.ucl"), lang.Identifier("main"))

src/test/scala/VerifierSpec.scala

@@ -977,16 +977,19 @@ class PrintCexSpec extends AnyFlatSpec {
     VerifierSpec.expectedFails("./test/test-record-naming-16.ucl", 2)
   }
 }
-class ModuleConcatSpec extends AnyFlatSpec {
-  "test-concat-modules-w-init-2-fab.ucl" should "verify all assertions." in {
-    VerifierSpec.expectedFailsMultipleFiles(List(
-      "test/test-concat-modules-w-init-2-fa.ucl", "test/test-concat-modules-w-init-2-fb.ucl"
-    ), 0)
-  }
-  "test-concat-modules-w-init-2-fba.ucl" should "fail to verify assertion." in {
-    VerifierSpec.expectedFailsMultipleFiles(List(
-      "test/test-concat-modules-w-init-2-fb.ucl", "test/test-concat-modules-w-init-2-fa.ucl"
-    ), 2)
-  }
-}
+// Now disabled as multiple init blocks are no longer supported
+// because the order of concatenation is not deterministic if both blocks are in the same module.
+
+// class ModuleConcatSpec extends AnyFlatSpec {
+//   "test-concat-modules-w-init-2-fab.ucl" should "verify all assertions." in {
+//     VerifierSpec.expectedFailsMultipleFiles(List(
+//       "test/test-concat-modules-w-init-2-fa.ucl", "test/test-concat-modules-w-init-2-fb.ucl"
+//     ), 0)
+//   }
+//   "test-concat-modules-w-init-2-fba.ucl" should "fail to verify assertion." in {
+//     VerifierSpec.expectedFailsMultipleFiles(List(
+//       "test/test-concat-modules-w-init-2-fb.ucl", "test/test-concat-modules-w-init-2-fa.ucl"
+//     ), 2)
+//   }
+// }
 

test/test-concat-modules-w-init-2-fa.ucl

@@ -1,8 +1,12 @@
 /* 
-    Test where variable declarations, init and next blocks are in different declaring modules.
-    Extended test where the blocks are in different files, and the order of specifying files is important.
+   EDIT: this is now disabled because the order of the init blocks is nondeterministic
+   when concatenating init blocks within the same file. 
+   Duplicate init blocks are no longer allowed.
+
+  Test where variable declarations, init and next blocks are in different declaring modules.
+  Extended test where the blocks are in different files, and the order of specifying files is important.
 
-    This is the first file; also checkout test/test-concat-modules-w-init-2-fb.ucl
+  This is the first file; also checkout test/test-concat-modules-w-init-2-fb.ucl
 */
 module A {
     var x, y, z: integer;

test/test-concat-modules-w-init-2-fb.ucl

@@ -1,8 +1,12 @@
 /* 
-    Test where variable declarations, init and next blocks are in different declaring modules.
-    Extended test where the blocks are in different files, and the order of specifying files is important.
+  EDIT: this is now disabled because the order of the init blocks is nondeterministic
+  when concatenating init blocks within the same file. 
+  Duplicate init blocks are no longer allowed.
 
-    This is the second file; also checkout test/test-concat-modules-w-init-2-fa.ucl
+  Test where variable declarations, init and next blocks are in different declaring modules.  
+  Extended test where the blocks are in different files, and the order of specifying files is important.
+
+  This is the second file; also checkout test/test-concat-modules-w-init-2-fa.ucl
 */
 
 module A {

test/test-multiple-init-blocks.ucl

@@ -0,0 +1,25 @@
+// should throw an error because there are multiple init blocks in the module
+module main {
+  var x : integer;
+
+  init {
+    x = 0;
+  }
+
+  init {
+    x = 1;
+  }
+
+  next{
+
+  }
+
+  invariant prop_eq: x == 0;
+
+  control {
+    v = bmc(5);
+    check;
+    print_results;
+  }
+
+}

test/test-multiple-next-blocks.ucl

@@ -0,0 +1,26 @@
+// should throw an error because there are multiple next blocks in the module
+module main {
+  var x : integer;
+  var y : integer;
+
+  init {
+    x = 0;
+    y = 0;
+  }
+
+  next {
+    x' = x + 1;
+  }
+
+  next {
+    y' = y + 2;
+  }
+    invariant prop_eq: x != 0;
+
+  control {
+    v = bmc(5);
+    check;
+    print_results;
+    v.print_cex(x);
+  }
+}