Merge branch 'main' into new-cloud-settings

Author: andrii-a8c

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

@@ -290,8 +290,11 @@ impl<'env> BoogieTranslator<'env> {
                         parent: self,
                         struct_env,
                         type_inst: type_inst.as_slice(),
-                        is_opaque: !mono_info
-                            .is_used_datatype(self.env, &struct_env.get_qualified_id()),
+                        is_opaque: !mono_info.is_used_datatype(
+                            self.env,
+                            self.targets,
+                            &struct_env.get_qualified_id(),
+                        ),
                     }
                     .translate();
                 }
@@ -311,8 +314,11 @@ impl<'env> BoogieTranslator<'env> {
                         parent: self,
                         enum_env,
                         type_inst: type_inst.as_slice(),
-                        is_opaque: !mono_info
-                            .is_used_datatype(self.env, &enum_env.get_qualified_id()),
+                        is_opaque: !mono_info.is_used_datatype(
+                            self.env,
+                            self.targets,
+                            &enum_env.get_qualified_id(),
+                        ),
                     }
                     .translate();
                 }
@@ -1043,7 +1049,7 @@ impl<'env> StructTranslator<'env> {
         let struct_env = self.struct_env;
         let env = struct_env.module_env.env;
 
-        if struct_env.is_native() || struct_env.is_intrinsic() {
+        if struct_env.is_native() || (struct_env.is_intrinsic() && !self.is_opaque) {
             return;
         }
 

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

@@ -20,7 +20,7 @@ use move_model::{
 };
 use move_stackless_bytecode::{
     dynamic_field_analysis::{self, NameValueInfo},
-    function_target_pipeline::FunctionVariant,
+    function_target_pipeline::{FunctionTargetsHolder, FunctionVariant},
     mono_analysis::{self, MonoInfo},
 };
 
@@ -129,6 +129,7 @@ fn bv_helper() -> Vec<BvInfo> {
 /// Adds the prelude to the generated output.
 pub fn add_prelude(
     env: &GlobalEnv,
+    targets: &FunctionTargetsHolder,
     options: &BoogieOptions,
     writer: &CodeWriter,
 ) -> anyhow::Result<()> {
@@ -186,21 +187,25 @@ pub fn add_prelude(
         .collect_vec();
     let mut table_instances = vec![];
     if let Some(table_qid) = env.table_qid() {
-        table_instances.push(TableImpl::table(env, options, &mono_info, table_qid, false));
+        if mono_info.is_used_datatype(env, targets, &table_qid) {
+            table_instances.push(TableImpl::table(env, options, &mono_info, table_qid, false));
+        }
     }
     if let Some(object_table_qid) = env.object_table_qid() {
-        table_instances.push(TableImpl::object_table(
-            env,
-            options,
-            &mono_info,
-            object_table_qid,
-            false,
-        ));
+        if mono_info.is_used_datatype(env, targets, &object_table_qid) {
+            table_instances.push(TableImpl::object_table(
+                env,
+                options,
+                &mono_info,
+                object_table_qid,
+                false,
+            ));
+        }
     }
     let mut dynamic_field_instances = vec![];
     for info in dynamic_field_analysis::get_env_info(env).dynamic_fields() {
         let (struct_qid, type_inst) = info.0.get_datatype().unwrap();
-        if mono_info.is_used_datatype(env, &struct_qid)
+        if mono_info.is_used_datatype(env, targets, &struct_qid)
             && mono_info
                 .structs
                 .get(&struct_qid)
@@ -249,17 +254,18 @@ pub fn add_prelude(
         let option_env = option_module_env
             .find_struct(env.symbol_pool().make("Option"))
             .unwrap();
-        let option_instances = if mono_info.is_used_datatype(env, &option_env.get_qualified_id()) {
-            mono_info
-                .structs
-                .get(&option_env.get_qualified_id())
-                .unwrap_or(&BTreeSet::new())
-                .iter()
-                .map(|tys| TypeInfo::new(env, options, &tys[0], false))
-                .collect_vec()
-        } else {
-            vec![]
-        };
+        let option_instances =
+            if mono_info.is_used_datatype(env, targets, &option_env.get_qualified_id()) {
+                mono_info
+                    .structs
+                    .get(&option_env.get_qualified_id())
+                    .unwrap_or(&BTreeSet::new())
+                    .iter()
+                    .map(|tys| TypeInfo::new(env, options, &tys[0], false))
+                    .collect_vec()
+            } else {
+                vec![]
+            };
         context.insert("option_instances", &option_instances);
     }
 
@@ -268,7 +274,7 @@ pub fn add_prelude(
             .find_struct(env.symbol_pool().make("VecSet"))
             .unwrap();
         let vec_set_instances =
-            if mono_info.is_used_datatype(env, &vec_set_struct_env.get_qualified_id()) {
+            if mono_info.is_used_datatype(env, targets, &vec_set_struct_env.get_qualified_id()) {
                 mono_info
                     .structs
                     .get(&vec_set_struct_env.get_qualified_id())
@@ -287,7 +293,7 @@ pub fn add_prelude(
             .find_struct(env.symbol_pool().make("VecMap"))
             .unwrap();
         let vec_map_instances =
-            if mono_info.is_used_datatype(env, &vec_map_struct_env.get_qualified_id()) {
+            if mono_info.is_used_datatype(env, targets, &vec_map_struct_env.get_qualified_id()) {
                 mono_info
                     .structs
                     .get(&vec_map_struct_env.get_qualified_id())
@@ -312,7 +318,7 @@ pub fn add_prelude(
             .find_struct(env.symbol_pool().make("TableVec"))
             .unwrap();
         let table_vec_instances =
-            if mono_info.is_used_datatype(env, &table_vec_env.get_qualified_id()) {
+            if mono_info.is_used_datatype(env, targets, &table_vec_env.get_qualified_id()) {
                 mono_info
                     .structs
                     .get(&table_vec_env.get_qualified_id())

crates/move-prover-boogie-backend/src/generator.rs

@@ -540,7 +540,7 @@ pub fn generate_boogie(
 ) -> anyhow::Result<(CodeWriter, BiBTreeMap<Type, String>)> {
     let writer = CodeWriter::new(env.internal_loc());
     let types = RefCell::new(BiBTreeMap::new());
-    add_prelude(env, &options.backend, &writer)?;
+    add_prelude(env, targets, &options.backend, &writer)?;
     let mut translator = BoogieTranslator::new(env, &options.backend, targets, &writer, &types);
     translator.translate();
     Ok((writer, types.into_inner()))

crates/move-stackless-bytecode/src/borrow_analysis.rs

@@ -10,7 +10,7 @@ use itertools::Itertools;
 
 use move_binary_format::file_format::CodeOffset;
 use move_model::{
-    model::{FunctionEnv, GlobalEnv, QualifiedInstId, RefType},
+    model::{DatatypeId, FunctionEnv, GlobalEnv, QualifiedId, QualifiedInstId, RefType},
     ty::Type,
     well_known::{BORROW_CHILD_OBJECT_MUT, VECTOR_BORROW_MUT},
 };
@@ -25,6 +25,7 @@ use crate::{
     spec_global_variable_analysis,
     stackless_bytecode::{AssignKind, BorrowEdge, BorrowNode, Bytecode, IndexEdgeKind, Operation},
     stackless_control_flow_graph::StacklessControlFlowGraph,
+    verification_analysis::VerificationInfo,
 };
 
 #[derive(Debug, Clone, Eq, Ord, PartialEq, PartialOrd, Default)]
@@ -50,6 +51,11 @@ pub struct WriteBackAction {
     pub edge: BorrowEdge,
 }
 
+#[derive(Debug, Clone, Eq, Ord, PartialEq, PartialOrd)]
+pub struct WriteBackDatatypeInfo {
+    pub datatypes: Vec<QualifiedId<DatatypeId>>,
+}
+
 impl BorrowInfo {
     /// Gets the children of this node.
     fn get_children(&self, node: &BorrowNode) -> Vec<&BorrowNode> {
@@ -453,12 +459,51 @@ impl FunctionTargetProcessor for BorrowAnalysisProcessor {
         data
     }
 
-    fn finalize(&self, _env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
+    fn finalize(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
         for (fun_id, variant) in targets.get_funs_and_variants().collect_vec() {
             if let Some(data) = targets.get_data_mut(&fun_id, &variant) {
                 data.annotations.remove::<LiveVarAnnotation>();
             }
         }
+
+        // collect all writeback datatypes from all verified or inlined functions
+        let writeback_datatype_info = WriteBackDatatypeInfo {
+            datatypes: targets
+                .get_funs_and_variants()
+                .flat_map(|(fun_id, variant)| targets.get_data(&fun_id, &variant))
+                .filter(|data| {
+                    let verification_info = data.annotations.get::<VerificationInfo>().unwrap();
+                    verification_info.verified || verification_info.inlined
+                })
+                .flat_map(|data| {
+                    data.annotations
+                        .get::<BorrowAnnotation>()
+                        .unwrap()
+                        .code_map
+                        .values()
+                        .flat_map(|info| {
+                            info.before
+                                .dying_nodes(&info.after)
+                                .iter()
+                                .flat_map(|(_, actions)| actions)
+                                .flatten()
+                                .flat_map(|action| action.edge.flatten())
+                                .filter_map(|edge| match edge {
+                                    BorrowEdge::Field(qualified_inst_id, _)
+                                    | BorrowEdge::EnumField(qualified_inst_id, _, _)
+                                    | BorrowEdge::DynamicField(qualified_inst_id, _, _) => {
+                                        Some(qualified_inst_id.to_qualified_id())
+                                    }
+                                    BorrowEdge::Direct | BorrowEdge::Index(_) => None,
+                                    BorrowEdge::Hyper(borrow_edges) => unreachable!(),
+                                })
+                                .collect_vec()
+                        })
+                })
+                .unique()
+                .collect_vec(),
+        };
+        env.set_extension(writeback_datatype_info);
     }
 
     fn name(&self) -> String {

crates/move-stackless-bytecode/src/mono_analysis.rs

@@ -24,6 +24,7 @@ use move_model::{
 
 use crate::{
     ast::ExpData,
+    borrow_analysis::WriteBackDatatypeInfo,
     dynamic_field_analysis::{self, NameValueInfo},
     function_target::FunctionTarget,
     function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant},
@@ -46,19 +47,44 @@ pub struct MonoInfo {
 }
 
 impl MonoInfo {
-    pub fn is_used_datatype(&self, env: &GlobalEnv, dt_qid: &QualifiedId<DatatypeId>) -> bool {
+    pub fn is_used_datatype(
+        &self,
+        env: &GlobalEnv,
+        targets: &FunctionTargetsHolder,
+        dt_qid: &QualifiedId<DatatypeId>,
+    ) -> bool {
+        if env
+            .get_extension::<WriteBackDatatypeInfo>()
+            .unwrap()
+            .datatypes
+            .contains(dt_qid)
+        {
+            return true;
+        }
+
         if dt_qid == &env.option_qid().unwrap() {
-            return self.is_used_datatype_helper(dt_qid)
-                || self.is_used_datatype_helper(&env.vec_set_qid().unwrap())
-                || self.is_used_datatype_helper(&env.vec_map_qid().unwrap());
+            return self.is_used_datatype_helper(env, targets, dt_qid)
+                || self.is_used_datatype_helper(env, targets, &env.vec_set_qid().unwrap())
+                || self.is_used_datatype_helper(env, targets, &env.vec_map_qid().unwrap());
         } else {
-            return self.is_used_datatype_helper(dt_qid);
+            return self.is_used_datatype_helper(env, targets, dt_qid);
         }
     }
 
-    fn is_used_datatype_helper(&self, dt_qid: &QualifiedId<DatatypeId>) -> bool {
+    fn is_used_datatype_helper(
+        &self,
+        env: &GlobalEnv,
+        targets: &FunctionTargetsHolder,
+        dt_qid: &QualifiedId<DatatypeId>,
+    ) -> bool {
         self.funs
             .keys()
+            .filter(|(fun_qid, _)| {
+                verification_analysis::get_info(
+                    &targets.get_target(&env.get_function(*fun_qid), &FunctionVariant::Baseline),
+                )
+                .inlined
+            })
             .map(|(fun_qid, _)| fun_qid.module_id)
             .contains(&dt_qid.module_id)
     }