tool: implement Viper export

We implement the `--viper-output` command line argument which lets
one dump the capability table of a PD into a Viper file for
verification purposes.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

Author: zaklogician

tool/microkit/src/argparse.rs

@@ -29,6 +29,7 @@ pub fn print_help(sdk: &Sdk) {
     );
     println!("  --config CONFIG");
     println!("  --capdl-json CAPDL_SPEC (JSON format)");
+    println!("  --viper-output DIRECTORY_PATH");
     println!("  --search-path [SEARCH_PATH ...]");
 }
 
@@ -69,6 +70,7 @@ pub struct Args {
     pub config: String,
     pub report_path: PathBuf,
     pub capdl_json_path: Option<PathBuf>,
+    pub viper_output_dir: Option<PathBuf>,
     pub output_path: PathBuf,
     pub search_paths: Vec<PathBuf>,
     pub requested_image_type: RequestedImageType,
@@ -167,6 +169,7 @@ impl Args {
         let mut output_path = PathBuf::from("loader.img");
         let mut report_path = PathBuf::from("report.txt");
         let mut capdl_json_path = None;
+        let mut viper_output_dir = None;
         let mut search_paths = Vec::new();
 
         let mut sdf_path = None;
@@ -205,6 +208,9 @@ impl Args {
                     let params = consume_parameters(&mut args);
                     search_paths.extend(params.into_iter().map(PathBuf::from));
                 }
+                "--viper-output" => {
+                    viper_output_dir = Some(consume_parameter(&mut args, "--viper-output")?.into());
+                }
                 "--image-type" => {
                     let value = consume_parameter(&mut args, "--image-type")?;
                     match RequestedImageType::parse(value.as_str()) {
@@ -262,6 +268,7 @@ impl Args {
             config,
             report_path,
             capdl_json_path,
+            viper_output_dir,
             output_path,
             search_paths,
             requested_image_type,

tool/microkit/src/lib.rs

@@ -23,6 +23,7 @@ pub mod sel4;
 pub mod symbols;
 pub mod uimage;
 pub mod util;
+pub mod viper;
 
 // Note that these values are used in the monitor so should also be changed there
 // if any of these were to change.

tool/microkit/src/main.rs

@@ -29,6 +29,7 @@ use microkit_tool::util::{
     get_full_path, human_size_strict, json_str, json_str_as_bool, json_str_as_u64, round_down,
     round_up,
 };
+use microkit_tool::viper;
 use microkit_tool::{DisjointMemoryRegion, MemoryRegion};
 use std::collections::HashMap;
 use std::fs::{self, metadata};
@@ -694,6 +695,33 @@ fn main() -> Result<(), String> {
                 fs::write(capdl_json, &serialised).unwrap();
             };
 
+            if let Some(viper_output_dir) = args.viper_output_dir {
+                // NB returns Ok if the directory already exists, that's fine
+                fs::create_dir_all(&viper_output_dir).unwrap_or_else(|source| {
+                    eprintln!(
+                        "ERROR: cannot write Viper output directory {}: {source}",
+                        &viper_output_dir.display()
+                    );
+                    std::process::exit(1);
+                });
+                for view in viper::get_combined_views(&spec_container, &system) {
+                    let mut output = format!(
+                        "// exported invariants for PD {} in {}\n",
+                        view.pd_name,
+                        &args.sdf_path.display(),
+                    );
+                    view.export(&mut output);
+                    let path = viper_output_dir.join(format!("{}.vpr", view.pd_name));
+                    fs::write(&path, output).unwrap_or_else(|source| {
+                        eprintln!(
+                            "ERROR: cannot write Viper output file {}: {source}",
+                            &path.display()
+                        );
+                        std::process::exit(1);
+                    });
+                }
+            }
+
             write_report(&spec_container, &kernel_config, &args.report_path);
             system_built = true;
             break;