delete widths.rs

Author: mmcloughlin

cranelift/isle/veri/veri_engine/src/annotations.rs

@@ -36,6 +36,20 @@ impl AnnotationEnv {
         }
         None
     }
+
+    pub fn get_term_signatures_by_name(
+        &self,
+        termenv: &TermEnv,
+        typeenv: &TypeEnv,
+    ) -> HashMap<String, Vec<TermTypeSignature>> {
+        let mut term_signatures_by_name = HashMap::new();
+        for (term_id, term_sigs) in &self.instantiations_map {
+            let sym = termenv.terms[term_id.index()].name;
+            let name = typeenv.syms[sym.index()].clone();
+            term_signatures_by_name.insert(name, term_sigs.clone());
+        }
+        term_signatures_by_name
+    }
 }
 
 pub fn spec_to_annotation_bound_var(i: &Ident) -> BoundVar {

cranelift/isle/veri/veri_engine/src/lib.rs

@@ -12,7 +12,6 @@ pub mod solver;
 pub mod termname;
 pub mod type_inference;
 pub mod verify;
-pub mod widths;
 
 pub const REG_WIDTH: usize = 64;
 

cranelift/isle/veri/veri_engine/src/verify.rs

@@ -1,5 +1,4 @@
 use crate::type_inference::type_rules_with_term_and_types;
-use crate::widths::isle_inst_types;
 use crate::Config;
 use cranelift_isle as isle;
 use isle::compile::create_envs;
@@ -26,7 +25,8 @@ pub fn verify_rules(inputs: Vec<PathBuf>, config: &Config) {
     let annotation_env = parse_annotations(&defs, &termenv, &typeenv);
 
     // Get the types/widths for this particular term
-    let types = isle_inst_types(&termenv, &typeenv, &annotation_env)
+    let types = annotation_env
+        .get_term_signatures_by_name(&termenv, &typeenv)
         .get(&config.term as &str)
         .expect(format!("Missing term width for {}", config.term).as_str())
         .clone();

cranelift/isle/veri/veri_engine/src/widths.rs

@@ -8,7 +8,6 @@ use veri_engine_lib::annotations::parse_annotations;
 use veri_engine_lib::build_clif_lower_isle;
 use veri_engine_lib::type_inference::type_rules_with_term_and_types;
 use veri_engine_lib::verify::verify_rules_for_term;
-use veri_engine_lib::widths::isle_inst_types;
 use veri_engine_lib::Config;
 use veri_ir::{ConcreteTest, Counterexample, TermSignature, VerificationResult};
 
@@ -116,7 +115,8 @@ fn test_rules_with_term(inputs: Vec<PathBuf>, tr: TestResult, config: Config) ->
     let (typeenv, termenv) = create_envs(&defs).unwrap();
     let annotation_env = parse_annotations(&defs, &termenv, &typeenv);
 
-    let term_signatures = isle_inst_types(&termenv, &typeenv, &annotation_env)
+    let term_signatures = annotation_env
+        .get_term_signatures_by_name(&termenv, &typeenv)
         .get(config.term.as_str())
         .expect(format!("Missing term width for {}", config.term).as_str())
         .clone();