From 9a5ad42548aa78694c738fbc75572d244e020ff4 Mon Sep 17 00:00:00 2001
From: Aalok Thakkar <aalok@Aaloks-MacBook-Pro.local>
Date: Thu, 28 Sep 2023 07:49:20 -0700
Subject: [PATCH] [move-model] fix internal assertion violation in definition
 analysis

---
 .../move-model/src/builder/module_builder.rs  | 43 +++++++++++++------
 .../duplicate_function_declarations.exp       |  6 +++
 .../duplicate_function_declarations.move      | 15 +++++++
 3 files changed, 50 insertions(+), 14 deletions(-)
 create mode 100644 third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.exp
 create mode 100644 third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.move

diff --git a/third_party/move/move-model/src/builder/module_builder.rs b/third_party/move/move-model/src/builder/module_builder.rs
index b85bd8b58c40b..8ccbc6be020b2 100644
--- a/third_party/move/move-model/src/builder/module_builder.rs
+++ b/third_party/move/move-model/src/builder/module_builder.rs
@@ -43,7 +43,7 @@ use move_bytecode_source_map::source_map::SourceMap;
 use move_compiler::{
     compiled_unit::{FunctionInfo, SpecInfo},
     expansion::ast as EA,
-    parser::ast as PA,
+    parser::{ast as PA, ast::FunctionName},
     shared::{unique_map::UniqueMap, Identifier, Name},
 };
 use move_ir_types::{ast::ConstantName, location::Spanned};
@@ -830,15 +830,14 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
         let mut visited = BTreeMap::new();
         for (idx, (name, _)) in module_def.functions.key_cloned_iter().enumerate() {
             let is_pure = self.propagate_function_impurity(&mut visited, SpecFunId::new(idx));
-            let full_name = self.qualified_by_module_from_name(&name.0);
             if is_pure {
                 // Modify the types of parameters, return values and expressions
                 // of pure Move functions so they no longer have references.
-                self.deref_move_fun_types(full_name.clone(), idx);
+                self.deref_move_fun_types(name, idx);
             }
             self.parent
                 .fun_table
-                .entry(full_name)
+                .entry(self.qualified_by_module_from_name(&name.0))
                 .and_modify(|e| e.is_pure = is_pure);
         }
 
@@ -1319,16 +1318,32 @@ impl<'env, 'translator> ModuleBuilder<'env, 'translator> {
         is_pure
     }
 
-    fn deref_move_fun_types(&mut self, full_name: QualifiedSymbol, spec_fun_idx: usize) {
-        self.parent.spec_fun_table.entry(full_name).and_modify(|e| {
-            assert!(e.len() == 1);
-            e[0].params = e[0]
-                .params
-                .iter()
-                .map(|Parameter(n, ty)| Parameter(*n, ty.skip_reference().clone()))
-                .collect_vec();
-            e[0].result_type = e[0].result_type.skip_reference().clone();
-        });
+    fn deref_move_fun_types(&mut self, name: FunctionName, spec_fun_idx: usize) {
+        if let Some(entry) = self
+            .parent
+            .spec_fun_table
+            .get_mut(&self.qualified_by_module_from_name(&name.0))
+        {
+            if entry.len() != 1 {
+                let error_msg = if entry.is_empty() {
+                    "missing"
+                } else {
+                    "duplicate"
+                };
+                self.parent.error(
+                    &self.parent.to_loc(&name.loc()),
+                    &format!("{} declaration of `{}`", error_msg, name.value()),
+                );
+            } else {
+                let e = &mut entry[0];
+                e.params = e
+                    .params
+                    .iter()
+                    .map(|Parameter(n, ty)| Parameter(*n, ty.skip_reference().clone()))
+                    .collect_vec();
+                e.result_type = e.result_type.skip_reference().clone();
+            }
+        };
 
         let spec_fun_decl = &mut self.spec_funs[spec_fun_idx];
         spec_fun_decl.params = spec_fun_decl
diff --git a/third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.exp b/third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.exp
new file mode 100644
index 0000000000000..df56f8a6e41e0
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.exp
@@ -0,0 +1,6 @@
+Move prover returns: exiting with model building errors
+error: duplicate declaration of `double`
+   ┌─ tests/sources/functional/duplicate_function_declarations.move:11:9
+   │
+11 │     fun double(x: u8): u8 {
+   │         ^^^^^^
\ No newline at end of file
diff --git a/third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.move b/third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.move
new file mode 100644
index 0000000000000..5518711d66af0
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/duplicate_function_declarations.move
@@ -0,0 +1,15 @@
+module 0x42::DuplicateFunction {
+    struct R0 { x: u8 }
+
+    spec R0 {
+        fun double(x: u8): u8 {
+            x * 2
+        }
+        invariant x > 0;
+    }
+
+    fun double(x: u8): u8 {
+        x * 2
+    }
+    spec double (x: u8) : u8 {}
+}