Grcov report - sabre

1

use std::cell::RefCell;

2

use std::rc::Rc;

3

4

use log::info;

5

use log::trace;

6

use mcrl2::aterm::ATermRef;

7

use mcrl2::aterm::TermPool;

8

use mcrl2::data::DataExpression;

9

use mcrl2::data::DataExpressionRef;

10

11

use crate::matching::nonlinear::check_equivalence_classes;

12

use crate::set_automaton::MatchAnnouncement;

13

use crate::set_automaton::SetAutomaton;

14

use crate::utilities::AnnouncementSabre;

15

use crate::utilities::ConfigurationStack;

16

use crate::utilities::PositionIndexed;

17

use crate::utilities::SideInfo;

18

use crate::utilities::SideInfoType;

19

use crate::RewriteSpecification;

20

21

/// A shared trait for all the rewriters

22

pub trait RewriteEngine {

23

    /// Rewrites the given term into normal form.

24

    fn rewrite(&mut self, term: DataExpression) -> DataExpression;

25

26

27

#[derive(Default)]

28

pub struct RewritingStatistics {

29

    /// Count the number of rewrite rules applied

30

    pub rewrite_steps: usize,

31

    /// Counts the number of times symbols are compared.

32

    pub symbol_comparisons: usize,

33

    /// The number of times rewrite is called recursively (to rewrite conditions etc)

34

    pub recursions: usize,

35

36

37

// A set automaton based rewrite engine described in  Mark Bouwman, Rick Erkens:

38

// Term Rewriting Based On Set Automaton Matching. CoRR abs/2202.08687 (2022)

39

pub struct SabreRewriter {

40

    term_pool: Rc<RefCell<TermPool>>,

41

    automaton: SetAutomaton<AnnouncementSabre>,

42

43

44

impl RewriteEngine for SabreRewriter {

45

230

    fn rewrite(&mut self, term: DataExpression) -> DataExpression {

46

230

        self.stack_based_normalise(term)

47

230

48

49

50

impl SabreRewriter {

51

150

    pub fn new(tp: Rc<RefCell<TermPool>>, spec: &RewriteSpecification) -> Self {

52

150

        let automaton = SetAutomaton::new(spec, AnnouncementSabre::new, false);

53

150

54

150

        info!("ATerm pool: {}", tp.borrow());

55

150

        SabreRewriter {

56

150

            term_pool: tp.clone(),

57

150

            automaton,

58

150

59

150

60

61

    /// Function to rewrite a term. See the module documentation.

62

230

    pub fn stack_based_normalise(&mut self, t: DataExpression) -> DataExpression {

63

230

        let mut stats = RewritingStatistics::default();

64

230

65

230

        let result =

66

230

            SabreRewriter::stack_based_normalise_aux(&mut self.term_pool.borrow_mut(), &self.automaton, t, &mut stats);

67

230

        info!(

68

            "{} rewrites, {} single steps and {} symbol comparisons",

69

            stats.recursions, stats.rewrite_steps, stats.symbol_comparisons

70

);

71

230

        result

72

230

73

74

    /// The _aux function splits the [TermPool] pool and the [SetAutomaton] to make borrow checker happy.

75

    /// We can now mutate the term pool and read the state and transition information at the same time

76

1289000

    fn stack_based_normalise_aux(

77

1289000

        tp: &mut TermPool,

78

1289000

        automaton: &SetAutomaton<AnnouncementSabre>,

79

1289000

        t: DataExpression,

80

1289000

        stats: &mut RewritingStatistics,

81

1289000

    ) -> DataExpression {

82

1289000

        stats.recursions += 1;

83

1289000

84

1289000

        // We explore the configuration tree depth first using a ConfigurationStack

85

1289000

        let mut cs = ConfigurationStack::new(0, t);

86

87

        // Big loop until we know we have a normal form

88

        'outer: loop {

89

            // Inner loop so that we can easily break; to the next iteration

90

            'skip_point: loop {

91

93099545

                trace!("{}", cs);

92

93

                // Check if there is any configuration leaf left to explore, if not we have found a normal form

94

93099545

                if let Some(leaf_index) = cs.get_unexplored_leaf() {

95

91810545

                    let leaf = &mut cs.stack[leaf_index];

96

91810545

                    let read_terms = cs.terms.read();

97

91810545

                    let leaf_term = &read_terms[leaf_index];

98

91810545

99

91810545

                    match ConfigurationStack::pop_side_branch_leaf(&mut cs.side_branch_stack, leaf_index) {

100

                        None => {

101

                            // Observe a symbol according to the state label of the set automaton.

102

86891870

                            let pos: DataExpressionRef =

103

86891870

                                leaf_term.get_position(&automaton.states[leaf.state].label).into();

104

86891870

105

86891870

                            let function_symbol = pos.data_function_symbol();

106

86891870

                            stats.symbol_comparisons += 1;

107

108

                            // Get the transition belonging to the observed symbol

109

86891870

                            if let Some(tr) = automaton.transitions.get(&(leaf.state, function_symbol.operation_id())) {

110

                                // Loop over the match announcements of the transition

111

87760745

                                for (announcement, annotation) in &tr.announcements {

112

7183085

                                    if annotation.conditions.is_empty() && annotation.equivalence_classes.is_empty() {

113

6393620

                                        if annotation.is_duplicating {

114

79500

                                            trace!("Delaying duplicating rule {}", announcement.rule);

115

116

                                            // We do not want to apply duplicating rules straight away

117

79500

                                            cs.side_branch_stack.push(SideInfo {

118

79500

                                                corresponding_configuration: leaf_index,

119

79500

                                                info: SideInfoType::DelayedRewriteRule(announcement, annotation),

120

79500

});

121

                                        } else {

122

                                            // For a rewrite rule that is not duplicating or has a condition we just apply it straight away

123

6314120

                                            SabreRewriter::apply_rewrite_rule(

124

6314120

tp,

125

6314120

                                                automaton,

126

6314120

                                                announcement,

127

6314120

                                                annotation,

128

6314120

                                                leaf_index,

129

6314120

                                                &mut cs,

130

6314120

                                                stats,

131

6314120

);

132

6314120

                                            break 'skip_point;

133

134

                                    } else {

135

                                        // We delay the condition checks

136

789465

                                        trace!("Delaying condition check for rule {}", announcement.rule);

137

789465

                                        cs.side_branch_stack.push(SideInfo {

138

789465

                                            corresponding_configuration: leaf_index,

139

789465

                                            info: SideInfoType::EquivalenceAndConditionCheck(announcement, annotation),

140

789465

});

141

142

143

144

80577660

                                if tr.destinations.is_empty() {

145

                                    // If there is no destination we are done matching and go back to the previous

146

                                    // configuration on the stack with information on the side stack.

147

                                    // Note, it could be that we stay at the same configuration and apply a rewrite

148

                                    // rule that was just discovered whilst exploring this configuration.

149

5943900

                                    let prev = cs.get_prev_with_side_info();

150

5943900

                                    cs.current_node = prev;

151

5943900

                                    if let Some(n) = prev {

152

4654915

                                        cs.jump_back(n, tp);

153

4654915

154

74633760

                                } else {

155

74633760

                                    // Grow the bud; if there is more than one destination a SideBranch object will be placed on the side stack

156

74633760

                                    let tr_slice = tr.destinations.as_slice();

157

74633760

                                    cs.grow(leaf_index, tr_slice);

158

74633760

159

                            } else {

160

90

                                let prev = cs.get_prev_with_side_info();

161

90

                                cs.current_node = prev;

162

90

                                if let Some(n) = prev {

163

75

                                    cs.jump_back(n, tp);

164

75

165

166

167

4918675

                        Some(sit) => {

168

4918675

                            match sit {

169

4191420

                                SideInfoType::SideBranch(sb) => {

170

4191420

                                    // If there is a SideBranch pick the next child configuration

171

4191420

                                    cs.grow(leaf_index, sb);

172

4191420

173

79380

                                SideInfoType::DelayedRewriteRule(announcement, annotation) => {

174

79380

                                    // apply the delayed rewrite rule

175

79380

                                    SabreRewriter::apply_rewrite_rule(

176

79380

tp,

177

79380

                                        automaton,

178

79380

                                        announcement,

179

79380

                                        annotation,

180

79380

                                        leaf_index,

181

79380

                                        &mut cs,

182

79380

                                        stats,

183

79380

);

184

79380

185

647875

                                SideInfoType::EquivalenceAndConditionCheck(announcement, annotation) => {

186

647875

                                    // Apply the delayed rewrite rule if the conditions hold

187

647875

                                    let t: &ATermRef<'_> = leaf_term;

188

647875

                                    if check_equivalence_classes(t, &annotation.equivalence_classes)

189

647875

                                        && SabreRewriter::conditions_hold(

190

647875

tp,

191

647875

                                            automaton,

192

647875

                                            announcement,

193

647875

                                            annotation,

194

647875

                                            leaf_term,

195

647875

                                            stats,

196

647875

197

384190

198

384190

                                        SabreRewriter::apply_rewrite_rule(

199

384190

tp,

200

384190

                                            automaton,

201

384190

                                            announcement,

202

384190

                                            annotation,

203

384190

                                            leaf_index,

204

384190

                                            &mut cs,

205

384190

                                            stats,

206

384190

);

207

384190

208

209

210

211

212

                } else {

213

                    // No configuration left to explore, we have found a normal form

214

1289000

                    break 'outer;

215

1289000

216

1289000

217

1289000

218

1289000

219

1289000

        cs.compute_final_term(tp)

220

1289000

221

222

    /// Apply a rewrite rule and prune back

223

6777690

    fn apply_rewrite_rule(

224

6777690

        tp: &mut TermPool,

225

6777690

        automaton: &SetAutomaton<AnnouncementSabre>,

226

6777690

        announcement: &MatchAnnouncement,

227

6777690

        annotation: &AnnouncementSabre,

228

6777690

        leaf_index: usize,

229

6777690

        cs: &mut ConfigurationStack<'_>,

230

6777690

        stats: &mut RewritingStatistics,

231

6777690

) {

232

6777690

        stats.rewrite_steps += 1;

233

6777690

234

6777690

        let read_terms = cs.terms.read();

235

6777690

        let leaf_subterm: &DataExpressionRef<'_> = &read_terms[leaf_index];

236

6777690

237

6777690

        // Computes the new subterm of the configuration

238

6777690

        let new_subterm = annotation

239

6777690

            .semi_compressed_rhs

240

6777690

            .evaluate(&leaf_subterm.get_position(&announcement.position), tp)

241

6777690

            .into();

242

6777690

243

6777690

        trace!(

244

            "rewrote {} to {} using rule {}",

245

            &leaf_subterm,

246

            &new_subterm,

247

            announcement.rule

248

);

249

250

        // The match announcement tells us how far we need to prune back.

251

6777690

        let prune_point = leaf_index - announcement.symbols_seen;

252

6777690

        cs.prune(tp, automaton, prune_point, new_subterm);

253

6777690

254

255

    /// Checks conditions and subterm equality of non-linear patterns.

256

647875

    fn conditions_hold(

257

647875

        tp: &mut TermPool,

258

647875

        automaton: &SetAutomaton<AnnouncementSabre>,

259

647875

        announcement: &MatchAnnouncement,

260

647875

        annotation: &AnnouncementSabre,

261

647875

        subterm: &DataExpressionRef<'_>,

262

647875

        stats: &mut RewritingStatistics,

263

647875

    ) -> bool {

264

1034160

        for c in &annotation.conditions {

265

649970

            let subterm = subterm.get_position(&announcement.position);

266

649970

267

649970

            let rhs: DataExpression = c.semi_compressed_rhs.evaluate(&subterm, tp).into();

268

649970

            let lhs: DataExpression = c.semi_compressed_lhs.evaluate(&subterm, tp).into();

269

649970

270

649970

            // Equality => lhs == rhs.

271

649970

            if !c.equality || lhs != rhs {

272

644385

                let rhs_normal = SabreRewriter::stack_based_normalise_aux(tp, automaton, rhs, stats);

273

644385

                let lhs_normal = if &lhs == tp.true_term() {

274

                    // TODO: Store the conditions in a better way. REC now uses a list of equalities while mCRL2 specifications have a simple condition.

275

lhs

276

                } else {

277

644385

                    SabreRewriter::stack_based_normalise_aux(tp, automaton, lhs, stats)

278

};

279

280

                // If lhs != rhs && !equality OR equality && lhs == rhs.

281

644385

                if (!c.equality && lhs_normal == rhs_normal) || (c.equality && lhs_normal != rhs_normal) {

282

263685

                    return false;

283

380700

284

5585

285

286

287

384190

        true

288

647875

289