Every existing name will be registered now

Author: The-Ray-Man

formver.compiler-plugin/viper/src/org/jetbrains/kotlin/formver/viper/ast/Program.kt

@@ -50,6 +50,7 @@ data class Program(
     context(nameResolver: NameResolver)
     fun toDebugOutput(): String = toSilver().toString()
 }
+
 context(nameResolver: NameResolver)
 private fun registerExpNames(exp: Exp) {
     when (exp) {
@@ -58,24 +59,114 @@ private fun registerExpNames(exp: Exp) {
             nameResolver.register(exp.field.name)
             registerExpNames(exp.rcv)
         }
+
         is Exp.PredicateAccess -> {
             nameResolver.register(exp.predicateName)
             exp.formalArgs.forEach { registerExpNames(it) }
         }
+
         is BinaryExp -> {
             registerExpNames(exp.left)
             registerExpNames(exp.right)
         }
+
         is Exp.FuncApp -> {
             nameResolver.register(exp.functionName)
             exp.args.forEach { registerExpNames(it) }
         }
+
         is Exp.DomainFuncApp -> {
             nameResolver.register(exp.function.name)
             exp.function.formalArgs.forEach { arg -> nameResolver.register(arg.name) }
             exp.args.forEach { registerExpNames(it) }
         }
-        else -> { }
+
+        is Exp.Forall -> {
+            exp.variables.forEach { nameResolver.register(it.name) }
+            registerExpNames(exp.exp)
+        }
+
+        is Exp.Exists -> {
+            exp.variables.forEach { nameResolver.register(it.name) }
+            registerExpNames(exp.exp)
+        }
+
+        is Exp.LetBinding -> {
+            nameResolver.register(exp.variable.name)
+            registerExpNames(exp.body)
+        }
+
+        is Exp.Old -> registerExpNames(exp.exp)
+        is Exp.TernaryExp -> {
+            registerExpNames(exp.thenExp)
+            registerExpNames(exp.elseExp)
+        }
+
+        is AccessPredicate.FieldAccessPredicate -> {}
+        is Exp.Acc -> registerExpNames(exp.field)
+        is Exp.ExplicitSeq -> exp.args.forEach { registerExpNames(it) }
+        is Exp.Minus -> registerExpNames(exp.arg)
+        is Exp.Not -> registerExpNames(exp.arg)
+        is Exp.SeqIndex -> {
+            registerExpNames(exp.seq)
+            registerExpNames(exp.idx)
+        }
+
+        is Exp.SeqLength -> registerExpNames(exp.seq)
+        is Exp.SeqTake -> {
+            registerExpNames(exp.seq)
+            registerExpNames(exp.idx)
+        }
+
+        is Exp.Unfolding -> {
+            registerExpNames(exp.predicateAccess)
+            registerExpNames(exp.body)
+        }
+        // no else branch to make decisions explicit.
+        is Exp.Result, is Exp.BoolLit, is Exp.EmptySeq, is Exp.IntLit, is Exp.NullLit -> {}
+    }
+}
+
+context(nameResolver: NameResolver)
+private fun Program.registerStmtNames(stmt: Stmt) = when (stmt) {
+    is Stmt.Label -> {
+        nameResolver.register(stmt.name)
+        stmt.invariants.forEach { registerExpNames(it) }
+    }
+
+    is Stmt.Seqn -> registerSeqnNames(stmt)
+    is Stmt.Goto -> nameResolver.register(stmt.name)
+    is Stmt.MethodCall -> {
+        stmt.args.forEach { registerExpNames(it) }
+        stmt.targets.forEach { registerExpNames(it) }
+        nameResolver.register(stmt.methodName)
+    }
+
+    is Stmt.If -> {
+        registerExpNames(stmt.cond)
+        registerSeqnNames(stmt.then)
+        stmt.els?.let { registerSeqnNames(it) }
+    }
+
+    is Stmt.While -> {
+        registerExpNames(stmt.cond)
+        registerSeqnNames(stmt.body)
+        stmt.invariants.forEach { registerExpNames(it) }
+    }
+
+    is Stmt.LocalVarAssign -> {
+        nameResolver.register(stmt.lhs.name)
+        registerExpNames(stmt.rhs)
+    }
+
+    is Stmt.Fold -> nameResolver.register(stmt.acc.predicateName)
+    is Stmt.Unfold -> nameResolver.register(stmt.acc.predicateName)
+    is Stmt.Assert -> registerExpNames(stmt.exp)
+    is Stmt.Exhale -> registerExpNames(stmt.exp)
+    is Stmt.Inhale -> registerExpNames(stmt.exp)
+    is Stmt.FieldAssign -> {
+        registerExpNames(stmt.lhs)
+        registerExpNames(stmt.rhs)
     }
 }
 
@@ -87,23 +178,7 @@ private fun Program.registerSeqnNames(seqn: Stmt.Seqn) {
             is Declaration.LabelDecl -> nameResolver.register(decl.name)
         }
     }
-    seqn.stmts.forEach { stmt ->
-        when (stmt) {
-            is Stmt.Label -> nameResolver.register(stmt.name)
-            is Stmt.Seqn -> registerSeqnNames(stmt)
-            is Stmt.Goto -> nameResolver.register(stmt.name)
-            is Stmt.MethodCall -> nameResolver.register(stmt.methodName)
-            is Stmt.If -> {
-                registerSeqnNames(stmt.then)
-                stmt.els?.let { registerSeqnNames(it) }
-            }
-            is Stmt.While -> registerSeqnNames(stmt.body)
-            is Stmt.LocalVarAssign -> nameResolver.register(stmt.lhs.name)
-            is Stmt.Fold -> nameResolver.register(stmt.acc.predicateName)
-            is Stmt.Unfold -> nameResolver.register(stmt.acc.predicateName)
-            else -> { }
-        }
-    }
+    seqn.stmts.forEach { registerStmtNames(it) }
 }
 
 context(nameResolver: NameResolver)
@@ -114,12 +189,20 @@ fun Program.registerAllNames() {
             nameResolver.register(function.name)
             function.formalArgs.forEach { arg -> nameResolver.register(arg.name) }
         }
+        domain.axioms.forEach { axiom ->
+            if (axiom.name is NamedDomainAxiomLabel) {
+                nameResolver.register(axiom.name)
+            }
+            registerExpNames(axiom.exp)
+        }
     }
     fields.forEach { nameResolver.register(it.name) }
 
     functions.forEach { function ->
         nameResolver.register(function.name)
         function.formalArgs.forEach { arg -> nameResolver.register(arg.name) }
+        function.pres.forEach { arg -> registerExpNames(arg) }
+        function.posts.forEach { arg -> registerExpNames(arg) }
         function.body?.let { exp -> registerExpNames(exp) }
     }
 
@@ -133,6 +216,8 @@ fun Program.registerAllNames() {
         nameResolver.register(method.name)
         method.formalArgs.forEach { arg -> nameResolver.register(arg.name) }
         method.formalReturns.forEach { ret -> nameResolver.register(ret.name) }
+        method.pres.forEach { arg -> registerExpNames(arg) }
+        method.posts.forEach { arg -> registerExpNames(arg) }
         method.body?.let { seqn -> registerSeqnNames(seqn) }
     }
 }