crocus/
main.rs

1//! Prototype verification tool for Cranelift's ISLE lowering rules.
2
3use clap::{ArgAction, Parser};
4use cranelift_codegen_meta::{generate_isle, isle::get_isle_compilations};
5use std::path::PathBuf;
6use std::{env, fs};
7use veri_engine_lib::verify::verify_rules;
8use veri_engine_lib::Config;
9
10#[derive(Parser)]
11#[clap(about, version, author)]
12struct Args {
13    /// Path to codegen crate directory.
14    #[clap(long, required = true)]
15    codegen: std::path::PathBuf,
16
17    /// Sets the input file
18    #[clap(short, long)]
19    input: Option<String>,
20
21    /// Which LHS root to verify
22    #[clap(short, long, default_value = "lower")]
23    term: String,
24
25    /// Which width types to verify
26    #[clap(long)]
27    widths: Option<Vec<String>>,
28
29    /// Which named rule to verify
30    #[clap(long)]
31    names: Option<Vec<String>>,
32
33    /// Don't use the prelude ISLE files
34    #[clap(short, long, action=ArgAction::SetTrue)]
35    noprelude: bool,
36
37    /// Include the aarch64 files
38    #[clap(short, long, action=ArgAction::SetTrue)]
39    aarch64: bool,
40
41    /// Include the x64 files
42    #[clap(short, long, action=ArgAction::SetTrue)]
43    x64: bool,
44
45    /// Don't check for distinct possible models
46    #[clap(long, action=ArgAction::SetTrue)]
47    nodistinct: bool,
48}
49
50impl Args {
51    fn isle_input_files(&self) -> anyhow::Result<Vec<std::path::PathBuf>> {
52        // Generate ISLE files.
53        let cur_dir = env::current_dir().expect("Can't access current working directory");
54        let gen_dir = cur_dir.join("output");
55        if !std::path::Path::new(gen_dir.as_path()).exists() {
56            fs::create_dir_all(gen_dir.as_path()).unwrap();
57        }
58        generate_isle(gen_dir.as_path()).expect("Can't generate ISLE");
59
60        let inst_specs_isle = self.codegen.join("src").join("inst_specs.isle");
61
62        // Lookup ISLE compilations.
63        let compilations = get_isle_compilations(&self.codegen, gen_dir.as_path());
64
65        let name = match (self.aarch64, self.x64) {
66            (true, false) => "aarch64",
67            (false, true) => "x64",
68            _ => panic!("aarch64 of x64 backend must be provided"),
69        };
70
71        let mut inputs = compilations
72            .lookup(name)
73            .ok_or(anyhow::format_err!("unknown ISLE compilation: {}", name))?
74            .inputs();
75        inputs.push(inst_specs_isle);
76
77        // Return inputs from the matching compilation, if any.
78        Ok(inputs)
79    }
80}
81
82fn main() -> anyhow::Result<()> {
83    env_logger::init();
84    let args = Args::parse();
85
86    let valid_widths = ["I8", "I16", "I32", "I64"];
87    if let Some(widths) = &args.widths {
88        for w in widths {
89            let w_str = w.as_str();
90            if !valid_widths.contains(&w_str) {
91                panic!("Invalid width type: {}", w);
92            }
93        }
94    }
95
96    let inputs = if args.noprelude {
97        vec![PathBuf::from(
98            args.input.expect("Missing input file in noprelude mode"),
99        )]
100    } else {
101        args.isle_input_files()?
102    };
103
104    let names = if let Some(names) = args.names {
105        let mut names = names;
106        names.sort();
107        names.dedup();
108        Some(names)
109    } else {
110        None
111    };
112
113    let config = Config {
114        term: args.term,
115        names,
116        distinct_check: !args.nodistinct,
117        custom_verification_condition: None,
118        custom_assumptions: None,
119    };
120
121    verify_rules(inputs, &config, &args.widths)
122        .map_err(|e| anyhow::anyhow!("failed to compile ISLE: {:?}", e))
123}
crocus/main.rs

crocus/
main.rs
