veri_engine_lib/
verify.rs

1use crate::type_inference::type_rules_with_term_and_types;
2use crate::Config;
3use cranelift_isle::error::Errors;
4use cranelift_isle::{self as isle};
5use isle::compile::create_envs;
6use isle::sema::{Pattern, RuleId, TermEnv, TypeEnv};
7use std::collections::HashMap;
8use std::path::PathBuf;
9
10use crate::annotations::parse_annotations;
11use crate::solver::run_solver;
12use crate::type_inference::RuleSemantics;
13use crate::{interp::Context, termname::pattern_contains_termname};
14use veri_ir::{ConcreteTest, TermSignature, VerificationResult};
15
16pub fn verify_rules(
17    inputs: Vec<PathBuf>,
18    config: &Config,
19    widths: &Option<Vec<String>>,
20) -> Result<(), Errors> {
21    // Produces environments including terms, rules, and maps from symbols and
22    // names to types
23    let (typeenv, termenv, defs) = create_envs(inputs).unwrap();
24
25    let annotation_env = parse_annotations(&defs, &termenv, &typeenv);
26
27    // Get the types/widths for this particular term
28    let types = annotation_env
29        .get_term_signatures_by_name(&termenv, &typeenv)
30        .get(&config.term as &str)
31        .unwrap_or_else(|| panic!("Missing term type instantiation for {}", config.term))
32        .clone();
33
34    let types_filtered = if let Some(widths) = widths {
35        let mut width_types = Vec::new();
36
37        for w in widths {
38            let width_type = match w.as_str() {
39                "I8" => veri_ir::Type::BitVector(Some(8)),
40                "I16" => veri_ir::Type::BitVector(Some(16)),
41                "I32" => veri_ir::Type::BitVector(Some(32)),
42                "I64" => veri_ir::Type::BitVector(Some(64)),
43                _ => panic!("Invalid width type: {}", w),
44            };
45            width_types.push(width_type);
46        }
47
48        types
49            .into_iter()
50            .filter(|t| {
51                if let Some(canonical_type) = &t.canonical_type {
52                    width_types.contains(canonical_type)
53                } else {
54                    false
55                }
56            })
57            .collect::<Vec<_>>()
58    } else {
59        types
60    };
61
62    for type_instantiation in types_filtered {
63        let type_sols = type_rules_with_term_and_types(
64            &termenv,
65            &typeenv,
66            &annotation_env,
67            config,
68            &type_instantiation,
69            &None,
70        );
71        verify_rules_for_term(
72            &termenv,
73            &typeenv,
74            &type_sols,
75            type_instantiation,
76            &None,
77            config,
78        );
79    }
80    Ok(())
81}
82
83pub fn verify_rules_for_term(
84    termenv: &TermEnv,
85    typeenv: &TypeEnv,
86    typesols: &HashMap<RuleId, RuleSemantics>,
87    types: TermSignature,
88    concrete: &Option<ConcreteTest>,
89    config: &Config,
90) -> VerificationResult {
91    let mut rules_checked = 0;
92    for rule in &termenv.rules {
93        // Only type rules with the given term on the LHS
94        if !pattern_contains_termname(
95            // Hack for now: typeid not used
96            &Pattern::Term(
97                cranelift_isle::sema::TypeId(0),
98                rule.root_term,
99                rule.args.clone(),
100            ),
101            &config.term,
102            termenv,
103            typeenv,
104        ) {
105            continue;
106        }
107        if let Some(names) = &config.names {
108            if rule.name.is_none() {
109                continue;
110            }
111            let name = &typeenv.syms[rule.name.unwrap().index()];
112            if !names.contains(name) {
113                continue;
114            } else {
115                log::debug!("Verifying rule: {}", name);
116            }
117        }
118        let ctx = Context::new(typesols);
119        if ctx.typesols.get(&rule.id).is_none() {
120            continue;
121        }
122        let rule_sem = &ctx.typesols[&rule.id];
123        log::debug!("Term: {}", config.term);
124        log::debug!("Type instantiation: {}", types);
125        let result = run_solver(rule_sem, rule, termenv, typeenv, concrete, config, &types);
126        rules_checked += 1;
127        if result != VerificationResult::Success {
128            return result;
129        }
130    }
131    if rules_checked > 0 {
132        VerificationResult::Success
133    } else {
134        panic!("No rules checked!")
135    }
136}
veri_engine_lib/verify.rs

veri_engine_lib/
verify.rs
