litex/runtime/
runtime_store_fact.rs1use crate::prelude::*;
2use std::collections::HashSet;
3
4impl Runtime {
5 pub fn verify_well_defined_and_store_and_infer(
6 &mut self,
7 fact: Fact,
8 verify_state: &VerifyState,
9 ) -> Result<InferResult, RuntimeError> {
10 if let Err(wd_err) = self.verify_fact_well_defined(&fact, verify_state) {
11 return Err(StoreFactRuntimeError(RuntimeErrorStruct::new(
12 Some(fact.clone().into_stmt()),
13 "cannot store fact: not well-defined".to_string(),
14 fact.line_file(),
15 Some(wd_err),
16 vec![],
17 ))
18 .into());
19 }
20 self.store_and_infer_fact_without_well_defined_verified(fact)
21 }
22
23 pub fn verify_well_defined_and_store_and_infer_with_default_verify_state(
24 &mut self,
25 fact: Fact,
26 ) -> Result<InferResult, RuntimeError> {
27 let verify_state = match fact {
28 Fact::ForallFact(_) => VerifyState::new(0, false),
29 Fact::ForallFactWithIff(_) => VerifyState::new(0, false),
30 _ => VerifyState::new_with_final_round(false),
31 };
32 self.verify_well_defined_and_store_and_infer(fact, &verify_state)
33 }
34
35 fn store_and_infer_fact_without_well_defined_verified(
36 &mut self,
37 fact: Fact,
38 ) -> Result<InferResult, RuntimeError> {
39 let mut infer_result = InferResult::new();
40
41 infer_result.new_fact(&fact);
42
43 let ret = match fact {
44 Fact::AtomicFact(_)
45 | Fact::ExistFact(_)
46 | Fact::OrFact(_)
47 | Fact::AndFact(_)
48 | Fact::ChainFact(_)
49 | Fact::NotForall(_) => self.store_whole_fact_update_cache_known_fact_and_infer(fact),
50 Fact::ForallFact(forall_fact) => {
51 self.store_forall_fact_without_well_defined_verified_and_infer(forall_fact)
52 }
53 Fact::ForallFactWithIff(forall_fact_with_iff) => self
54 .store_forall_fact_with_iff_without_well_defined_verified_and_infer(
55 forall_fact_with_iff,
56 ),
57 };
58
59 infer_result.new_infer_result_inside(ret?);
60
61 Ok(infer_result)
62 }
63
64 pub fn store_fact_without_forall_coverage_check_and_infer(
65 &mut self,
66 fact: Fact,
67 ) -> Result<InferResult, RuntimeError> {
68 self.store_whole_fact_update_cache_known_fact_and_infer(fact)
69 }
70
71 pub(crate) fn store_forall_fact_without_well_defined_verified_and_infer(
72 &mut self,
73 mut forall_fact: ForallFact,
74 ) -> Result<InferResult, RuntimeError> {
75 forall_fact.expand_then_facts_with_order_chain_closure()?;
76
77 let coverage_error_detail_lines =
78 forall_fact.error_messages_if_forall_param_missing_in_some_then_clause();
79
80 if coverage_error_detail_lines.is_empty() {
81 return self
82 .store_whole_fact_update_cache_known_fact_and_infer(Fact::ForallFact(forall_fact));
83 }
84
85 let warning_msg = forall_fact_coverage_warn_after_drop_then(&coverage_error_detail_lines);
86 let then_drop: HashSet<usize> = coverage_error_detail_lines
87 .iter()
88 .map(|(i, _)| *i)
89 .collect();
90
91 forall_fact.then_facts = forall_fact
92 .then_facts
93 .into_iter()
94 .enumerate()
95 .filter(|(i, _)| !then_drop.contains(i))
96 .map(|(_, f)| f)
97 .collect();
98
99 if forall_fact.then_facts.is_empty() {
100 let mut infer_result = InferResult::new();
101 infer_result.new_with_msg(warning_msg);
102 return Ok(infer_result);
103 }
104
105 let mut infer_result = InferResult::new();
106 infer_result.new_with_msg(warning_msg);
107 infer_result.new_infer_result_inside(
108 self.store_whole_fact_update_cache_known_fact_and_infer(Fact::ForallFact(forall_fact))?,
109 );
110 Ok(infer_result)
111 }
112
113 fn store_forall_fact_with_iff_without_well_defined_verified_and_infer(
114 &mut self,
115 forall_fact_with_iff: ForallFactWithIff,
116 ) -> Result<InferResult, RuntimeError> {
117 let (forall_then_implies_iff, forall_iff_implies_then) =
118 forall_fact_with_iff.to_two_forall_facts()?;
119 let mut infer_result = self
120 .store_forall_fact_without_well_defined_verified_and_infer(forall_then_implies_iff)?;
121 infer_result.new_infer_result_inside(
122 self.store_forall_fact_without_well_defined_verified_and_infer(
123 forall_iff_implies_then,
124 )?,
125 );
126 Ok(infer_result)
127 }
128
129 fn store_whole_fact_update_cache_known_fact_and_infer(
130 &mut self,
131 fact: Fact,
132 ) -> Result<InferResult, RuntimeError> {
133 let line_file = fact.line_file();
134 let fact_string: FactString = fact.to_string();
135 let fact_for_infer = fact.clone();
136 let transitive_chain_facts = match &fact {
137 Fact::ChainFact(chain_fact) => self.transitive_prop_chain_closure_facts(chain_fact)?,
138 _ => Vec::new(),
139 };
140 self.top_level_env().store_fact(fact)?;
141 self.store_transitive_prop_chain_atomic_facts(transitive_chain_facts)?;
142
143 self.top_level_env()
144 .store_fact_to_cache_known_fact(fact_string, line_file)?;
145
146 Ok(self.infer(&fact_for_infer)?)
147 }
148
149 pub fn store_and_chain_atomic_fact_without_well_defined_verified_and_infer(
150 &mut self,
151 fact: AndChainAtomicFact,
152 ) -> Result<InferResult, RuntimeError> {
153 let line_file = fact.line_file();
154 let fact_string: FactString = fact.to_string();
155 let fact_for_infer: Fact = fact.clone().into();
156 let transitive_chain_facts = match &fact {
157 AndChainAtomicFact::ChainFact(chain_fact) => {
158 self.transitive_prop_chain_closure_facts(chain_fact)?
159 }
160 _ => Vec::new(),
161 };
162 self.top_level_env().store_and_chain_atomic_fact(fact)?;
163 self.store_transitive_prop_chain_atomic_facts(transitive_chain_facts)?;
164
165 self.top_level_env()
166 .store_fact_to_cache_known_fact(fact_string, line_file)?;
167
168 Ok(self.infer(&fact_for_infer)?)
169 }
170
171 pub fn store_atomic_fact_without_well_defined_verified_and_infer(
172 &mut self,
173 fact: AtomicFact,
174 ) -> Result<InferResult, RuntimeError> {
175 let line_file = fact.line_file();
176 let fact_string: FactString = fact.to_string();
177 let infer_wrapped_fact: Fact = fact.clone().into();
178 self.top_level_env().store_atomic_fact(fact)?;
179
180 self.top_level_env()
181 .store_fact_to_cache_known_fact(fact_string, line_file)?;
182
183 Ok(self.infer(&infer_wrapped_fact)?)
184 }
185
186 pub fn store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
187 &mut self,
188 fact: ExistOrAndChainAtomicFact,
189 ) -> Result<InferResult, RuntimeError> {
190 let line_file = fact.line_file();
191 let fact_string: FactString = fact.to_string();
192 let fact_for_infer = fact.clone();
193 let transitive_chain_facts = match &fact {
194 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
195 self.transitive_prop_chain_closure_facts(chain_fact)?
196 }
197 _ => Vec::new(),
198 };
199 self.top_level_env()
200 .store_exist_or_and_chain_atomic_fact(fact)?;
201 self.store_transitive_prop_chain_atomic_facts(transitive_chain_facts)?;
202
203 self.top_level_env()
204 .store_fact_to_cache_known_fact(fact_string, line_file)?;
205
206 Ok(self.infer_exist_or_and_chain_atomic_fact(&fact_for_infer)?)
207 }
208
209 pub fn store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
210 &mut self,
211 fact: OrAndChainAtomicFact,
212 ) -> Result<InferResult, RuntimeError> {
213 let line_file = fact.line_file();
214 let fact_string: FactString = fact.to_string();
215 let fact_for_infer = fact.clone();
216 let transitive_chain_facts = match &fact {
217 OrAndChainAtomicFact::ChainFact(chain_fact) => {
218 self.transitive_prop_chain_closure_facts(chain_fact)?
219 }
220 _ => Vec::new(),
221 };
222 self.top_level_env().store_or_and_chain_atomic_fact(fact)?;
223 self.store_transitive_prop_chain_atomic_facts(transitive_chain_facts)?;
224
225 self.top_level_env()
226 .store_fact_to_cache_known_fact(fact_string, line_file)?;
227
228 Ok(self.infer_or_and_chain_atomic_fact(&fact_for_infer)?)
229 }
230
231 fn store_transitive_prop_chain_atomic_facts(
232 &mut self,
233 facts: Vec<AtomicFact>,
234 ) -> Result<(), RuntimeError> {
235 for atomic_fact in facts {
236 self.top_level_env().store_atomic_fact(atomic_fact)?;
237 }
238 Ok(())
239 }
240
241 fn transitive_prop_chain_closure_facts(
242 &self,
243 chain_fact: &ChainFact,
244 ) -> Result<Vec<AtomicFact>, RuntimeError> {
245 if chain_fact.prop_names.is_empty() || chain_fact.objs.len() < 3 {
246 return Ok(Vec::new());
247 }
248
249 let prop_name = chain_fact.prop_names[0].to_string();
250 for name in chain_fact.prop_names.iter() {
251 if name.to_string() != prop_name {
252 return Ok(Vec::new());
253 }
254 }
255 if !self.is_transitive_prop_name_known(&prop_name) {
256 return Ok(Vec::new());
257 }
258
259 let mut facts = Vec::new();
260 for i in 0..chain_fact.objs.len() {
261 for j in i + 2..chain_fact.objs.len() {
262 facts.push(
263 NormalAtomicFact::new(
264 chain_fact.prop_names[0].clone(),
265 vec![chain_fact.objs[i].clone(), chain_fact.objs[j].clone()],
266 chain_fact.line_file.clone(),
267 )
268 .into(),
269 );
270 }
271 }
272 Ok(facts)
273 }
274
275 fn is_transitive_prop_name_known(&self, prop_name: &str) -> bool {
276 for env in self.iter_environments_from_top() {
277 if env.known_transitive_props.contains_key(prop_name) {
278 return true;
279 }
280 }
281 false
282 }
283}
284fn forall_fact_coverage_warn_after_drop_then(
285 coverage_error_detail_lines: &[(usize, String)],
286) -> String {
287 let body = coverage_error_detail_lines
288 .iter()
289 .map(|(idx, msg)| format!("at index {}: {}", idx, msg))
290 .collect::<Vec<_>>()
291 .join("\n");
292 format!(
293 "Warning: forall missing forall parameter(s) in some then clause(s); dropped problematic clause(s):\n{}",
294 body
295 )
296}