tool: add --viper-output option

docs/manual.md

@@ -482,6 +482,12 @@ It is important to note that this is largely just for debugging purposes and the
 highly tied to a specific version and configuration of the kernel. When using this option the kernel
 should be the same version and compiled with the same configuration options.
 
+If the `--viper-output PREFIX` argument is set, then for each protection domain `name` specified in
+the system description file, a file `PREFIX/name.vpr` will be output, containing a description of the
+capability table of the given PD in the Viper verification language. These output files can be used
+for verification purposes, but the exact format may change in future versions of the tool.
+
+
 ## Image format
 
 ### ARM

example/hello/Makefile

@@ -67,4 +67,4 @@ $(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS))
 	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
 
 $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) hello.system
-	$(MICROKIT_TOOL) hello.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+	$(MICROKIT_TOOL) hello.system --search-path $(BUILD_DIR) --viper-output ${BUILD_DIR}/viper --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

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};
@@ -122,7 +123,7 @@ fn main() -> Result<(), String> {
             std::process::exit(1);
         }
     };
-    args.search_paths.push(std::env::current_dir().unwrap());
+    args.search_paths.push(sdk.cwd.clone());
 
     // NB safe unwrap: argparse would already have bailed if the config did not
     // exist.
@@ -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;