add custom native options to move prover backend

Closes: diem#439

language/move-prover/boogie-backend/src/lib.rs

@@ -83,9 +83,6 @@ pub fn add_prelude(
     templates.push(templ("multiset-theory", MULTISET_ARRAY_THEORY));
     templates.push(templ("table-theory", TABLE_ARRAY_THEORY));
 
-    let mut tera = Tera::default();
-    tera.add_raw_templates(templates)?;
-
     let mut context = Context::new();
     context.insert("options", options);
 
@@ -151,6 +148,26 @@ pub fn add_prelude(
     context.insert("std", &std_addr);
     context.insert("Ext", &ext_addr);
 
+    // If a custom Boogie template is provided, add it as part of the templates and
+    // add all type instances that use generic functions in the provided modules to the context.
+    if let Some(custom_native_options) = options.custom_natives.clone() {
+        templates.push(templ(
+            "custom-natives",
+            &std::fs::read(&custom_native_options.template_path).unwrap_or_else(|_| {
+                panic!(
+                    "cannot read custom template file {}",
+                    &custom_native_options.template_path
+                )
+            }),
+        ));
+        for (module_name, instance_name) in custom_native_options.module_instance_names {
+            context.insert(instance_name, &filter_native(&module_name));
+        }
+    }
+
+    let mut tera = Tera::default();
+    tera.add_raw_templates(templates)?;
+
     let expanded_content = tera.render("prelude", &context)?;
     emitln!(writer, &expanded_content);
     Ok(())

language/move-prover/boogie-backend/src/options.rs

@@ -40,6 +40,16 @@ impl VectorTheory {
     }
 }
 
+/// Options to define custom native functions to include in generated Boogie file.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct CustomNativeOptions {
+    /// Path to the custom template file.
+    pub template_path: String,
+    /// List of (module name, module instance key) tuples, used to generate instantiated
+    /// versions of generic native functions.
+    pub module_instance_names: Vec<(String, String)>,
+}
+
 /// Boogie options.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 #[serde(default, deny_unknown_fields)]
@@ -105,6 +115,8 @@ pub struct BoogieOptions {
     pub vector_theory: VectorTheory,
     /// Whether to generate a z3 trace file and where to put it.
     pub z3_trace_file: Option<String>,
+    /// Options to define user-custom native funs.
+    pub custom_natives: Option<CustomNativeOptions>,
 }
 
 impl Default for BoogieOptions {
@@ -139,6 +151,7 @@ impl Default for BoogieOptions {
             hard_timeout_secs: 0,
             vector_theory: VectorTheory::BoogieArray,
             z3_trace_file: None,
+            custom_natives: None,
         }
     }
 }

language/move-prover/boogie-backend/src/prelude/prelude.bpl

@@ -20,7 +20,9 @@ options provided to the prover.
 {% include "vector-theory" %}
 {% include "multiset-theory" %}
 {% include "table-theory" %}
-
+{%- if options.custom_natives -%}
+{% include "custom-natives" %}
+{%- endif %}
 
 // ============================================================================================
 // Primitive Types