| 1787 | } |
| 1788 | |
| 1789 | fn cfg_integrity( |
| 1790 | &self, |
| 1791 | cfg: &ControlFlowGraph, |
| 1792 | errors: &mut VerifierErrors, |
| 1793 | ) -> VerifierStepResult { |
| 1794 | let mut expected_succs = BTreeSet::<Block>::new(); |
| 1795 | let mut got_succs = BTreeSet::<Block>::new(); |
| 1796 | let mut expected_preds = BTreeSet::<Inst>::new(); |
| 1797 | let mut got_preds = BTreeSet::<Inst>::new(); |
| 1798 | |
| 1799 | for block in self.func.layout.blocks() { |
| 1800 | expected_succs.extend(self.expected_cfg.succ_iter(block)); |
| 1801 | got_succs.extend(cfg.succ_iter(block)); |
| 1802 | |
| 1803 | let missing_succs: Vec<Block> = |
| 1804 | expected_succs.difference(&got_succs).cloned().collect(); |
| 1805 | if !missing_succs.is_empty() { |
| 1806 | errors.report(( |
| 1807 | block, |
| 1808 | format!("cfg lacked the following successor(s) {missing_succs:?}"), |
| 1809 | )); |
| 1810 | continue; |
| 1811 | } |
| 1812 | |
| 1813 | let excess_succs: Vec<Block> = got_succs.difference(&expected_succs).cloned().collect(); |
| 1814 | if !excess_succs.is_empty() { |
| 1815 | errors.report(( |
| 1816 | block, |
| 1817 | format!("cfg had unexpected successor(s) {excess_succs:?}"), |
| 1818 | )); |
| 1819 | continue; |
| 1820 | } |
| 1821 | |
| 1822 | expected_preds.extend( |
| 1823 | self.expected_cfg |
| 1824 | .pred_iter(block) |
| 1825 | .map(|BlockPredecessor { inst, .. }| inst), |
| 1826 | ); |
| 1827 | got_preds.extend( |
| 1828 | cfg.pred_iter(block) |
| 1829 | .map(|BlockPredecessor { inst, .. }| inst), |
| 1830 | ); |
| 1831 | |
| 1832 | let missing_preds: Vec<Inst> = expected_preds.difference(&got_preds).cloned().collect(); |
| 1833 | if !missing_preds.is_empty() { |
| 1834 | errors.report(( |
| 1835 | block, |
| 1836 | format!("cfg lacked the following predecessor(s) {missing_preds:?}"), |
| 1837 | )); |
| 1838 | continue; |
| 1839 | } |
| 1840 | |
| 1841 | let excess_preds: Vec<Inst> = got_preds.difference(&expected_preds).cloned().collect(); |
| 1842 | if !excess_preds.is_empty() { |
| 1843 | errors.report(( |
| 1844 | block, |
| 1845 | format!("cfg had unexpected predecessor(s) {excess_preds:?}"), |
| 1846 | )); |