Check for multiple init/next blocks

Remove code that picks only one init block when combining modules

this was previously misleading because the order the init block statements were combined in isn't obvious to the user.

Author: polgreen

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

@@ -258,6 +258,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"))

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);
+  }
+}