Grcov report - assertions.rs

1

//! Debug-only structural assertions for AST/model integrity.

2

//!

3

//! The assertions in this module validate a few key invariants:

4

//! - `Root` exists exactly once, at the top-level model root, and nowhere else.

5

//! - all referenced names resolve to declarations present in reachable symbol tables.

6

//! - a combined model well-formedness check that applies all assertions.

7

8

use super::Model;

9

10

#[cfg(debug_assertions)]

11

use std::collections::{BTreeSet, HashSet};

12

13

#[cfg(debug_assertions)]

14

use super::{Expression, Name, Reference, SymbolTablePtr, serde::HasId};

15

#[cfg(debug_assertions)]

16

use uniplate::Biplate;

17

18

/// Debug-assert that a model is well-formed by applying all AST assertions in this module.

19

#[cfg(debug_assertions)]

20

467834

pub fn debug_assert_model_well_formed(model: &Model, origin: &str) {

21

467834

    debug_assert_root_at_top_level_only(model, origin);

22

467834

    debug_assert_all_names_resolved(model, origin);

23

467834

24

25

/// Debug-assert that a model is well-formed by applying all AST assertions in this module.

26

#[cfg(not(debug_assertions))]

27

pub fn debug_assert_model_well_formed(_model: &Model, _origin: &str) {}

28

29

/// Debug-assert that all names referenced by expressions/domains resolve to declared symbols.

30

#[cfg(debug_assertions)]

31

467834

pub fn debug_assert_all_names_resolved(model: &Model, origin: &str) {

32

467834

    let mut declared_names: BTreeSet<Name> = BTreeSet::new();

33

467834

    let mut referenced_names: BTreeSet<Name> = BTreeSet::new();

34

35

668400

    for table_ptr in collect_reachable_symbol_tables(model) {

36

668400

        let table = table_ptr.read();

37

38

27079607

        for (name, decl) in table.iter_local() {

39

27079607

            declared_names.insert(name.clone());

40

41

27079607

            if let Some(expr) = decl.as_value_letting() {

42

389838

                referenced_names.extend(Biplate::<Reference>::universe_bi(&*expr).into_iter().map(

43

468234

                    |reference| {

44

468234

                        let name = reference.name();

45

468234

                        canonical_resolution_name(&name).clone()

46

468234

},

47

));

48

26689769

49

50

27079607

            if let Some(domain) = decl.domain() {

51

27079297

                referenced_names.extend(

52

27079297

                    Biplate::<Reference>::universe_bi(domain.as_ref())

53

27079297

                        .into_iter()

54

27079297

                        .map(|reference| {

55

410582

                            let name = reference.name();

56

410582

                            canonical_resolution_name(&name).clone()

57

410582

}),

58

);

59

310

60

61

62

63

467834

    referenced_names.extend(

64

467834

        Biplate::<Reference>::universe_bi(model.root())

65

467834

            .into_iter()

66

10482075

            .map(|reference| {

67

10482075

                let name = reference.name();

68

10482075

                canonical_resolution_name(&name).clone()

69

10482075

}),

70

);

71

72

467834

    if let Some(dominance) = &model.dominance {

73

1280

        referenced_names.extend(

74

1280

            Biplate::<Reference>::universe_bi(dominance)

75

1280

                .into_iter()

76

20320

                .map(|reference| {

77

20320

                    let name = reference.name();

78

20320

                    canonical_resolution_name(&name).clone()

79

20320

}),

80

);

81

466554

82

83

97647007

    for clause in model.clauses() {

84

203581694

        for literal in clause.iter() {

85

203581694

            referenced_names.extend(Biplate::<Reference>::universe_bi(literal).into_iter().map(

86

203581694

                |reference| {

87

203581694

                    let name = reference.name();

88

203581694

                    canonical_resolution_name(&name).clone()

89

203581694

},

90

));

91

92

93

94

467834

    let unresolved: Vec<Name> = referenced_names

95

467834

        .difference(&declared_names)

96

467834

        .cloned()

97

467834

        .collect();

98

99

467834

    debug_assert!(

100

467834

        unresolved.is_empty(),

101

        "Model from '{origin}' contains unresolved names: {unresolved:?}"

102

);

103

467834

104

105

/// Debug-assert that all names referenced by expressions/domains resolve to declared symbols.

106

#[cfg(not(debug_assertions))]

107

pub fn debug_assert_all_names_resolved(_model: &Model, _origin: &str) {}

108

109

#[cfg(debug_assertions)]

110

215423413

fn canonical_resolution_name(name: &Name) -> &Name {

111

215423413

    match name {

112

        // Names wrapped in a selected representation still resolve through the source declaration.

113

460508

        Name::WithRepresentation(inner, _) => canonical_resolution_name(inner),

114

214962905

        _ => name,

115

116

215423413

117

118

/// Debug-assert that there is exactly one `Root` expression, and it is the model's top-level root.

119

#[cfg(debug_assertions)]

120

467834

pub fn debug_assert_root_at_top_level_only(model: &Model, origin: &str) {

121

467834

    debug_assert!(

122

467834

        matches!(model.root(), Expression::Root(_, _)),

123

        "Model from '{origin}' does not have Root at top-level"

124

);

125

126

467834

    let root_count_in_main_tree = Biplate::<Expression>::universe_bi(model)

127

467834

        .iter()

128

21542985

        .filter(|expr| matches!(expr, Expression::Root(_, _)))

129

467834

        .count();

130

131

467834

    let root_count_in_clauses = model

132

467834

        .clauses()

133

467834

        .iter()

134

97647007

        .flat_map(|clause| clause.iter())

135

203582565

        .map(|expr| {

136

203581694

            Biplate::<Expression>::universe_bi(expr)

137

203581694

                .iter()

138

358858226

                .filter(|inner| matches!(inner, Expression::Root(_, _)))

139

203581694

                .count()

140

203581694

})

141

467834

        .sum::<usize>();

142

143

467834

    let total_root_count = root_count_in_main_tree + root_count_in_clauses;

144

467834

    debug_assert_eq!(

145

        total_root_count, 1,

146

        "Model from '{origin}' should contain exactly one Root expression at top-level, found {total_root_count}"

147

);

148

467834

149

150

/// Debug-assert that there is exactly one `Root` expression, and it is the model's top-level root.

151

#[cfg(not(debug_assertions))]

152

pub fn debug_assert_root_at_top_level_only(_model: &Model, _origin: &str) {}

153

154

#[cfg(debug_assertions)]

155

467834

fn collect_reachable_symbol_tables(model: &Model) -> Vec<SymbolTablePtr> {

156

467834

    let mut pending_tables: Vec<SymbolTablePtr> = vec![model.symbols_ptr_unchecked().clone()];

157

467834

    pending_tables.extend(Biplate::<SymbolTablePtr>::universe_bi(model.root()));

158

159

467834

    if let Some(dominance) = &model.dominance {

160

1280

        pending_tables.extend(Biplate::<SymbolTablePtr>::universe_bi(dominance));

161

466554

162

163

97647007

    for clause in model.clauses() {

164

203581694

        for literal in clause.iter() {

165

203581694

            pending_tables.extend(Biplate::<SymbolTablePtr>::universe_bi(literal));

166

203581694

167

168

169

467834

    let mut seen_tables = HashSet::new();

170

467834

    let mut out = Vec::new();

171

172

1199868

    while let Some(table_ptr) = pending_tables.pop() {

173

732034

        if !seen_tables.insert(table_ptr.id()) {

174

63634

            continue;

175

668400

176

177

668400

        let parent = table_ptr.read().parent().clone();

178

668400

        if let Some(parent) = parent {

179

200566

            pending_tables.push(parent);

180

467834

181

182

668400

        out.push(table_ptr);

183

184

185

467834

out

186

467834