From ff2962832f7a7bacc93330b126a5d2015fc1a5c7 Mon Sep 17 00:00:00 2001
From: Teng Zhang <rahxephon89@163.com>
Date: Fri, 27 Sep 2024 11:30:48 -0700
Subject: [PATCH] fix code generation bug when inline spec is involved

---
 .../function_generator.rs                     | 35 +++++++++++++++++++
 .../boogie-backend/src/spec_translator.rs     |  5 ++-
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
index e35c6257716cb0..cf623fe1cb5c3a 100644
--- a/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
+++ b/third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs
@@ -887,6 +887,16 @@ impl<'a> FunctionGenerator<'a> {
     /// translation. In the actual Move bytecode, a `Nop` is inserted
     /// at the current code offset.
     fn gen_spec_block(&mut self, ctx: &BytecodeContext, spec: &Spec) {
+        let used_temps = self.collect_temps_from_spec(spec);
+        for temp in used_temps {
+            let live_after = ctx.is_alive_after(temp, &[], false);
+            let local = self.temps.get(&temp).expect("temp has mapping").local;
+            if !live_after && temp >= ctx.fun_ctx.fun.get_parameter_count() {
+                self.emit(FF::Bytecode::MoveLoc(local));
+                self.emit(FF::Bytecode::Pop);
+            }
+        }
+
         let mut replacer = |id: NodeId, target: RewriteTarget| {
             if let RewriteTarget::Temporary(temp) = target {
                 Some(
@@ -906,6 +916,31 @@ impl<'a> FunctionGenerator<'a> {
         self.emit(FF::Bytecode::Nop)
     }
 
+    fn collect_temps_from_spec(&mut self, spec: &Spec) -> BTreeSet<TempIndex> {
+        let mut temps = BTreeSet::new();
+        for cond in spec.conditions.iter() {
+            for exp in cond.all_exps() {
+                exp.visit_pre_order(&mut |inner: &ExpData| {
+                    if let ExpData::Temporary(_, temp_index) = inner {
+                        temps.insert(*temp_index);
+                    }
+                    true
+                })
+            }
+        }
+        for (_, cond) in spec.update_map.iter() {
+            for exp in cond.all_exps() {
+                exp.visit_pre_order(&mut |inner: &ExpData| {
+                    if let ExpData::Temporary(_, temp_index) = inner {
+                        temps.insert(*temp_index);
+                    }
+                    true
+                })
+            }
+        }
+        temps
+    }
+
     /// Emits a file-format bytecode.
     fn emit(&mut self, bc: FF::Bytecode) {
         self.code.push(bc)
diff --git a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
index 48bac0b40d94c3..5ce1e3c9d019d8 100644
--- a/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/spec_translator.rs
@@ -851,7 +851,10 @@ impl<'env> SpecTranslator<'env> {
             },
             Operation::Pack(mid, sid, None) => self.translate_pack(node_id, *mid, *sid, args),
             Operation::Tuple if args.len() == 1 => self.translate_exp(&args[0]),
-            Operation::Tuple => self.error(&loc, "Tuple not yet supported"),
+            Operation::Tuple => {
+                println!("args:{:?}", args);
+                self.error(&loc, "Tuple not yet supported")
+            },
             Operation::Select(module_id, struct_id, field_id) => {
                 self.translate_select(node_id, *module_id, *struct_id, *field_id, args)
             },