litex/verify/
verify_helper.rs

1use crate::prelude::*;
2
3impl Runtime {
4    /// If the fact string is in the known-facts cache, return the cached verification result.
5    pub fn verify_fact_from_cache_using_display_string(&self, fact: &Fact) -> Option<StmtResult> {
6        let key = fact.to_string();
7        let (cache_ok, _) = self.cache_known_facts_contains(&key);
8        if cache_ok {
9            Some(
10                (FactualStmtSuccess::new_with_verified_by_known_fact(
11                    fact.clone(),
12                    VerifiedByResult::Fact(fact.clone(), key),
13                    Vec::new(),
14                ))
15                .into(),
16            )
17        } else {
18            None
19        }
20    }
21
22    /// If check_type_nonempty is true and param_type is Obj(set), verifies that the set is nonempty and stores the fact.
23    pub fn verify_param_type_nonempty_if_required(
24        &mut self,
25        param_type: &ParamType,
26        check_type_nonempty: bool,
27    ) -> Result<(), RuntimeError> {
28        if !check_type_nonempty {
29            return Ok(());
30        }
31        match param_type {
32            ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => Ok(()),
33            ParamType::Obj(param_set) => match param_set {
34                Obj::FnSet(fn_set) => {
35                    let ret_nonempty = IsNonemptySetFact::new(
36                        fn_set.body.ret_set.as_ref().clone(),
37                        default_line_file(),
38                    )
39                    .into();
40                    self.verify_fact_well_defined_and_store_and_infer(
41                        ret_nonempty,
42                        &VerifyState::new(2, false),
43                    )?;
44                    Ok(())
45                }
46                Obj::AnonymousFn(anon) => {
47                    let ret_nonempty = IsNonemptySetFact::new(
48                        anon.body.ret_set.as_ref().clone(),
49                        default_line_file(),
50                    )
51                    .into();
52                    self.verify_fact_well_defined_and_store_and_infer(
53                        ret_nonempty,
54                        &VerifyState::new(2, false),
55                    )?;
56                    Ok(())
57                }
58                Obj::SetBuilder(_) => Err(RuntimeError::ExecStmtError(RuntimeErrorStruct::new_with_just_msg("set builder param type is not supported yet in verify_param_type_nonempty_if_required"
59                        .to_string()))),
60                _ => {
61                    let nonempty_fact =
62                        IsNonemptySetFact::new(param_set.clone(), default_line_file());
63                    let ret=  self.verify_fact(
64                        &nonempty_fact.into(),
65                        &VerifyState::new(0, false),
66                    )?;
67                    if ret.is_unknown() {
68                        return Err(RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new_with_just_msg("param type is not nonempty".to_string()))));
69                    }
70                    Ok(())
71                }
72            },
73        }
74    }
75}
litex/verify/verify_helper.rs

litex/verify/
verify_helper.rs
