Merge branch 'main' into dynamic-field-uid-fix

Author: andrii-a8c

crates/move-model/src/model.rs

@@ -4073,6 +4073,11 @@ impl GlobalEnv {
             self.sui_tx_context_epoch_timestamp_ms_qid(),
             self.sui_tx_context_reference_gas_price_qid(),
             self.sui_tx_context_gas_price_qid(),
+            // std::type_name native functions
+            self.std_type_name_with_defining_ids_qid(),
+            self.std_type_name_with_original_ids_qid(),
+            self.std_type_name_defining_id_qid(),
+            self.std_type_name_original_id_qid(),
         ]
         .into_iter()
         .filter_map(|x| x)

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs

@@ -248,6 +248,51 @@ impl<'env> BoogieTranslator<'env> {
         emitln!(self.writer);
     }
 
+    /// Emit uninterpreted Boogie function declarations for std::type_name native functions.
+    /// These allow type_name functions to be used in quantifiers.
+    fn emit_type_name_functions(&self, fun_env: &FunctionEnv, mono_info: &MonoInfo) {
+        let type_name_fns = [
+            self.env.std_type_name_with_defining_ids_qid(),
+            self.env.std_type_name_with_original_ids_qid(),
+            self.env.std_type_name_defining_id_qid(),
+            self.env.std_type_name_original_id_qid(),
+        ];
+        if !type_name_fns
+            .into_iter()
+            .flatten()
+            .any(|id| id == fun_env.get_qualified_id())
+        {
+            return;
+        }
+
+        let empty = &BTreeSet::new();
+        for type_inst in mono_info
+            .funs
+            .get(&(fun_env.get_qualified_id(), FunctionVariant::Baseline))
+            .unwrap_or(empty)
+        {
+            emitln!(
+                self.writer,
+                "function {}() returns ({});",
+                boogie_function_name(fun_env, type_inst, FunctionTranslationStyle::Default),
+                fun_env
+                    .get_return_types()
+                    .iter()
+                    .enumerate()
+                    .map(|(idx, ty)| {
+                        let ty = ty.instantiate(type_inst);
+                        format!(
+                            "$ret{}: {}",
+                            idx,
+                            boogie_type(self.env, ty.skip_reference())
+                        )
+                    })
+                    .join(", "),
+            );
+            emitln!(self.writer);
+        }
+    }
+
     // Generate object::borrow_uid function
     fn translate_object_borrow_uid(&self, suffix: &str, obj_name: &str) {
         emitln!(
@@ -474,6 +519,7 @@ impl<'env> BoogieTranslator<'env> {
                             self.emit_uninterpreted_native_pure(fun_env, type_inst);
                         }
                     }
+                    self.emit_type_name_functions(fun_env, &mono_info);
                     continue;
                 }
 

crates/move-prover-boogie-backend/src/boogie_backend/runner.rs

@@ -44,6 +44,7 @@ pub fn run_with_timeout(args: &[String], timeout: Duration) -> Result<Output> {
     use nix::sys::signal::{self, Signal};
     use nix::unistd::Pid;
     use std::os::unix::process::CommandExt;
+    use std::time::Instant;
 
     let mut child = Command::new(&args[0])
         .args(&args[1..])
@@ -54,26 +55,48 @@ pub fn run_with_timeout(args: &[String], timeout: Duration) -> Result<Output> {
 
     let pid = child.id() as i32;
 
-    match child.wait_timeout(timeout)? {
-        Some(status) => {
-            let stdout = child.stdout.take().unwrap();
-            let stderr = child.stderr.take().unwrap();
-
-            use std::io::Read;
-            let mut stdout_bytes = Vec::new();
-            let mut stderr_bytes = Vec::new();
-            std::io::BufReader::new(stdout).read_to_end(&mut stdout_bytes)?;
-            std::io::BufReader::new(stderr).read_to_end(&mut stderr_bytes)?;
-
-            Ok(Output {
-                status,
-                stdout: stdout_bytes,
-                stderr: stderr_bytes,
-            })
-        }
-        None => {
+    let stdout = child.stdout.take().unwrap();
+    let stderr = child.stderr.take().unwrap();
+
+    let stdout_thread = std::thread::spawn(move || {
+        use std::io::Read;
+        let mut bytes = Vec::new();
+        std::io::BufReader::new(stdout).read_to_end(&mut bytes).ok();
+        bytes
+    });
+
+    let stderr_thread = std::thread::spawn(move || {
+        use std::io::Read;
+        let mut bytes = Vec::new();
+        std::io::BufReader::new(stderr).read_to_end(&mut bytes).ok();
+        bytes
+    });
+
+    let start = Instant::now();
+    loop {
+        let elapsed = start.elapsed();
+        if elapsed >= timeout {
             let _ = signal::killpg(Pid::from_raw(pid), Signal::SIGKILL);
-            Err(Error::new(ErrorKind::TimedOut, "Process timed out"))
+            let _ = stdout_thread.join();
+            let _ = stderr_thread.join();
+            return Err(Error::new(ErrorKind::TimedOut, "Process timed out"));
+        }
+
+        let remaining = timeout - elapsed;
+        let poll = remaining.min(Duration::from_millis(100));
+
+        match child.wait_timeout(poll)? {
+            Some(status) => {
+                let stdout_bytes = stdout_thread.join().unwrap_or_default();
+                let stderr_bytes = stderr_thread.join().unwrap_or_default();
+
+                return Ok(Output {
+                    status,
+                    stdout: stdout_bytes,
+                    stderr: stderr_bytes,
+                });
+            }
+            None => {}
         }
     }
 }
@@ -165,6 +188,7 @@ pub fn run_with_timeout_and_line_callback<F: FnMut(&str) + Send>(
 #[cfg(windows)]
 pub fn run_with_timeout(args: &[String], timeout: Duration) -> Result<Output> {
     use std::os::windows::process::CommandExt;
+    use std::time::Instant;
 
     const CREATE_NEW_PROCESS_GROUP: u32 = 0x00000200;
 
@@ -177,28 +201,50 @@ pub fn run_with_timeout(args: &[String], timeout: Duration) -> Result<Output> {
 
     let pid = child.id();
 
-    match child.wait_timeout(timeout)? {
-        Some(status) => {
-            let stdout = child.stdout.take().unwrap();
-            let stderr = child.stderr.take().unwrap();
-
-            use std::io::Read;
-            let mut stdout_bytes = Vec::new();
-            let mut stderr_bytes = Vec::new();
-            std::io::BufReader::new(stdout).read_to_end(&mut stdout_bytes)?;
-            std::io::BufReader::new(stderr).read_to_end(&mut stderr_bytes)?;
-
-            Ok(Output {
-                status,
-                stdout: stdout_bytes,
-                stderr: stderr_bytes,
-            })
-        }
-        None => {
+    let stdout = child.stdout.take().unwrap();
+    let stderr = child.stderr.take().unwrap();
+
+    let stdout_thread = std::thread::spawn(move || {
+        use std::io::Read;
+        let mut bytes = Vec::new();
+        std::io::BufReader::new(stdout).read_to_end(&mut bytes).ok();
+        bytes
+    });
+
+    let stderr_thread = std::thread::spawn(move || {
+        use std::io::Read;
+        let mut bytes = Vec::new();
+        std::io::BufReader::new(stderr).read_to_end(&mut bytes).ok();
+        bytes
+    });
+
+    let start = Instant::now();
+    loop {
+        let elapsed = start.elapsed();
+        if elapsed >= timeout {
             let _ = Command::new("taskkill")
                 .args(&["/F", "/T", "/PID", &pid.to_string()])
                 .output();
-            Err(Error::new(ErrorKind::TimedOut, "Process timed out"))
+            let _ = stdout_thread.join();
+            let _ = stderr_thread.join();
+            return Err(Error::new(ErrorKind::TimedOut, "Process timed out"));
+        }
+
+        let remaining = timeout - elapsed;
+        let poll = remaining.min(Duration::from_millis(100));
+
+        match child.wait_timeout(poll)? {
+            Some(status) => {
+                let stdout_bytes = stdout_thread.join().unwrap_or_default();
+                let stderr_bytes = stderr_thread.join().unwrap_or_default();
+
+                return Ok(Output {
+                    status,
+                    stdout: stdout_bytes,
+                    stderr: stderr_bytes,
+                });
+            }
+            None => {}
         }
     }
 }

crates/sui-prover/tests/inputs/type_name/type_name_pure.ok.move

@@ -0,0 +1,74 @@
+/// Test that type_name functions can be used as Boogie functions in specs.
+/// The type_name functions are marked #[ext(pure)] and called from non-pure
+/// functions, which are then verified.
+module 0x42::type_name_pure;
+
+use std::type_name;
+#[spec_only]
+use prover::prover::ensures;
+
+public struct MyCoin has drop {}
+
+#[ext(pure)]
+public fun get_type_name(): type_name::TypeName {
+    type_name::with_defining_ids<MyCoin>()
+}
+
+#[ext(pure)]
+public fun get_original_type_name(): type_name::TypeName {
+    type_name::with_original_ids<MyCoin>()
+}
+
+#[ext(pure)]
+public fun get_defining_id(): address {
+    type_name::defining_id<MyCoin>()
+}
+
+#[ext(pure)]
+public fun get_original_id(): address {
+    type_name::original_id<MyCoin>()
+}
+
+public fun use_type_name(): type_name::TypeName {
+    get_type_name()
+}
+
+public fun use_original_type_name(): type_name::TypeName {
+    get_original_type_name()
+}
+
+public fun use_defining_id(): address {
+    get_defining_id()
+}
+
+public fun use_original_id(): address {
+    get_original_id()
+}
+
+#[spec(prove)]
+fun use_type_name_spec(): type_name::TypeName {
+    let result = use_type_name();
+    ensures(result == get_type_name());
+    result
+}
+
+#[spec(prove)]
+fun use_original_type_name_spec(): type_name::TypeName {
+    let result = use_original_type_name();
+    ensures(result == get_original_type_name());
+    result
+}
+
+#[spec(prove)]
+fun use_defining_id_spec(): address {
+    let result = use_defining_id();
+    ensures(result == get_defining_id());
+    result
+}
+
+#[spec(prove)]
+fun use_original_id_spec(): address {
+    let result = use_original_id();
+    ensures(result == get_original_id());
+    result
+}

crates/sui-prover/tests/snapshots/type_name/type_name_pure.ok.move.snap

@@ -0,0 +1,6 @@
+---
+source: crates/sui-prover/tests/integration.rs
+assertion_line: 297
+expression: output
+---
+Verification successful