Grcov report - sabre

1

#![forbid(unsafe_code)]

2

3

use log::info;

4

5

use merc_aterm::storage::THREAD_TERM_POOL;

6

use merc_aterm::storage::ThreadTermPool;

7

use merc_data::DataExpression;

8

use merc_data::DataExpressionRef;

9

use merc_utilities::debug_trace;

10

11

use crate::RewriteSpecification;

12

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

13

use crate::set_automaton::MatchAnnouncement;

14

use crate::set_automaton::SetAutomaton;

15

use crate::utilities::AnnouncementSabre;

16

use crate::utilities::ConfigurationStack;

17

use crate::utilities::DataPositionIndexed;

18

use crate::utilities::DataSubstitutionBuilder;

19

use crate::utilities::SideInfo;

20

use crate::utilities::SideInfoType;

21

use crate::utilities::TermStackBuilder;

22

23

/// A shared trait for all the rewriters

24

pub trait RewriteEngine {

25

    /// Rewrites the given term into normal form.

26

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

27

28

29

#[derive(Default)]

30

pub struct RewritingStatistics {

31

    /// Count the number of rewrite rules applied

32

    pub rewrite_steps: usize,

33

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

34

    pub symbol_comparisons: usize,

35

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

36

    pub recursions: usize,

37

38

39

/// The Set Automaton based Rewrite Engine implementation.

40

pub struct SabreRewriter {

41

    automaton: SetAutomaton<AnnouncementSabre>,

42

    /// A reusable builder for evaluating right-hand side term stacks, kept to

43

    /// avoid allocating a fresh one on every rewrite step.

44

    builder: TermStackBuilder,

45

    /// A reusable substitution builder handed to the top-level configuration

46

    /// stack, kept to avoid registering a protected container on every call.

47

    substitution_builder: DataSubstitutionBuilder,

48

49

50

impl RewriteEngine for SabreRewriter {

51

132

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

52

132

        self.stack_based_normalise(term)

53

132

54

55

56

impl SabreRewriter {

57

84

    pub fn new(spec: &RewriteSpecification) -> Self {

58

84

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

59

60

84

        SabreRewriter {

61

84

            automaton,

62

84

            builder: TermStackBuilder::new(),

63

84

            substitution_builder: DataSubstitutionBuilder::default(),

64

84

65

84

66

67

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

68

132

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

69

132

        let mut stats = RewritingStatistics::default();

70

71

132

        let result = THREAD_TERM_POOL.with(|tp| {

72

132

            SabreRewriter::stack_based_normalise_aux(

73

132

tp,

74

132

                &self.automaton,

75

132

                &mut self.builder,

76

132

                &mut self.substitution_builder,

77

132

t,

78

132

                &mut stats,

79

80

132

});

81

82

132

        info!(

83

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

84

            stats.recursions, stats.rewrite_steps, stats.symbol_comparisons

85

);

86

87

132

        result

88

132

89

90

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

91

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

92

716538

    fn stack_based_normalise_aux(

93

716538

        tp: &ThreadTermPool,

94

716538

        automaton: &SetAutomaton<AnnouncementSabre>,

95

716538

        builder: &mut TermStackBuilder,

96

716538

        substitution_builder: &mut DataSubstitutionBuilder,

97

716538

        t: &DataExpression,

98

716538

        stats: &mut RewritingStatistics,

99

716538

    ) -> DataExpression {

100

716538

        stats.recursions += 1;

101

102

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

103

716538

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

104

105

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

106

        'outer: loop {

107

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

108

            'skip_point: loop {

109

25063608

                debug_trace!("{}", cs);

110

111

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

112

25063608

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

113

24347070

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

114

24347070

                    let read_terms = cs.terms.read();

115

24347070

                    let leaf_term = &read_terms[leaf_index];

116

117

24347070

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

118

                        None => {

119

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

120

22189404

                            let pos: DataExpressionRef =

121

22189404

                                leaf_term.get_data_position(automaton.states()[leaf.state].label());

122

123

22189404

                            let function_symbol = pos.data_function_symbol();

124

22189404

                            stats.symbol_comparisons += 1;

125

126

                            // Get the transition belonging to the observed symbol

127

22189404

                            if let Some(tr) = automaton.get_transition(leaf.state, function_symbol.operation_id()) {

128

                                // Loop over the match announcements of the transition

129

22189338

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

130

3724563

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

131

3294099

                                        if annotation.is_duplicating {

132

47094

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

133

47094

134

47094

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

135

47094

                                            cs.side_branch_stack.push(SideInfo {

136

47094

                                                corresponding_configuration: leaf_index,

137

47094

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

138

47094

});

139

47094

                                        } else {

140

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

141

3247005

                                            drop(read_terms);

142

3247005

                                            SabreRewriter::apply_rewrite_rule(

143

3247005

tp,

144

3247005

                                                automaton,

145

3247005

                                                builder,

146

3247005

                                                announcement,

147

3247005

                                                annotation,

148

3247005

                                                leaf_index,

149

3247005

                                                &mut cs,

150

3247005

                                                stats,

151

);

152

3247005

                                            break 'skip_point;

153

154

430464

                                    } else {

155

430464

                                        // We delay the condition checks

156

430464

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

157

430464

158

430464

                                        cs.side_branch_stack.push(SideInfo {

159

430464

                                            corresponding_configuration: leaf_index,

160

430464

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

161

430464

});

162

430464

163

164

165

18942333

                                drop(read_terms);

166

18942333

                                if tr.destinations.is_empty() {

167

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

168

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

169

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

170

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

171

2722158

                                    let prev = cs.get_prev_with_side_info();

172

2722158

                                    cs.current_node = prev;

173

2722158

                                    if let Some(n) = prev {

174

2005638

                                        cs.jump_back(n, tp);

175

2005638

176

16220175

                                } else {

177

16220175

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

178

16220175

                                    let tr_slice = tr.destinations.as_slice();

179

16220175

                                    cs.grow(leaf_index, tr_slice);

180

16220175

181

                            } else {

182

66

                                let prev = cs.get_prev_with_side_info();

183

66

                                cs.current_node = prev;

184

66

                                if let Some(n) = prev {

185

54

                                    drop(read_terms);

186

54

                                    cs.jump_back(n, tp);

187

54

188

189

190

2157666

                        Some(sit) => {

191

2157666

                            match sit {

192

1749759

                                SideInfoType::SideBranch(sb) => {

193

1749759

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

194

1749759

                                    drop(read_terms);

195

1749759

                                    cs.grow(leaf_index, sb);

196

1749759

197

47022

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

198

47022

                                    drop(read_terms);

199

47022

                                    // apply the delayed rewrite rule

200

47022

                                    SabreRewriter::apply_rewrite_rule(

201

47022

tp,

202

47022

                                        automaton,

203

47022

                                        builder,

204

47022

                                        announcement,

205

47022

                                        annotation,

206

47022

                                        leaf_index,

207

47022

                                        &mut cs,

208

47022

                                        stats,

209

47022

);

210

47022

211

360885

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

212

                                    // The equivalence classes and conditions are checked relative to

213

                                    // the match root, which sits at `announcement.position` inside the

214

                                    // leaf term (the same root used by `apply_rewrite_rule`).

215

360885

                                    let matched = leaf_term.get_data_position(&announcement.position);

216

217

                                    // Apply the delayed rewrite rule if the conditions hold

218

360885

                                    if check_equivalence_classes(&matched, &annotation.equivalence_classes)

219

360882

                                        && SabreRewriter::conditions_hold(

220

360882

                                            tp, automaton, builder, annotation, &matched, stats,

221

222

208905

223

208905

                                        drop(read_terms);

224

208905

                                        SabreRewriter::apply_rewrite_rule(

225

208905

tp,

226

208905

                                            automaton,

227

208905

                                            builder,

228

208905

                                            announcement,

229

208905

                                            annotation,

230

208905

                                            leaf_index,

231

208905

                                            &mut cs,

232

208905

                                            stats,

233

208905

);

234

208905

                                    } else {

235

                                        // The check failed, so this announcement does not apply. The

236

                                        // side info was already popped, so move back to the previous

237

                                        // configuration that still has side info.

238

151980

                                        drop(read_terms);

239

151980

                                        let prev = cs.get_prev_with_side_info();

240

151980

                                        cs.current_node = prev;

241

151980

                                        if let Some(n) = prev {

242

151974

                                            cs.jump_back(n, tp);

243

151974

244

245

246

247

248

249

                } else {

250

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

251

716538

                    break 'outer;

252

253

254

255

256

716538

        cs.compute_final_term(tp)

257

716538

258

259

    /// Apply a rewrite rule and prune back

260

    #[allow(clippy::too_many_arguments)]

261

3502932

    fn apply_rewrite_rule(

262

3502932

        tp: &ThreadTermPool,

263

3502932

        automaton: &SetAutomaton<AnnouncementSabre>,

264

3502932

        builder: &mut TermStackBuilder,

265

3502932

        announcement: &MatchAnnouncement,

266

3502932

        annotation: &AnnouncementSabre,

267

3502932

        leaf_index: usize,

268

3502932

        cs: &mut ConfigurationStack<'_, '_>,

269

3502932

        stats: &mut RewritingStatistics,

270

3502932

) {

271

3502932

        stats.rewrite_steps += 1;

272

273

3502932

        let read_terms = cs.terms.read();

274

3502932

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

275

276

        // Computes the new subterm of the configuration

277

3502932

        let new_subterm = annotation

278

3502932

            .rhs_term_stack

279

3502932

            .evaluate_with(&leaf_subterm.get_data_position(&announcement.position), builder);

280

281

3502932

        debug_trace!(

282

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

283

            &leaf_subterm,

284

            &new_subterm,

285

            announcement.rule

286

);

287

288

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

289

3502932

        let prune_point = leaf_index - announcement.symbols_seen;

290

3502932

        drop(read_terms);

291

3502932

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

292

3502932

293

294

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

295

///

296

    /// `matched` is the subterm at the match root (`announcement.position`), which

297

    /// the caller has already resolved.

298

360882

    fn conditions_hold(

299

360882

        tp: &ThreadTermPool,

300

360882

        automaton: &SetAutomaton<AnnouncementSabre>,

301

360882

        builder: &mut TermStackBuilder,

302

360882

        annotation: &AnnouncementSabre,

303

360882

        matched: &DataExpressionRef<'_>,

304

360882

        stats: &mut RewritingStatistics,

305

360882

    ) -> bool {

306

        // The parent configuration stack still borrows the caller's substitution

307

        // builder, so the recursive normalisation of conditions needs its own.

308

360882

        let mut substitution_builder = DataSubstitutionBuilder::default();

309

310

361554

        for c in &annotation.conditions {

311

361554

            let rhs: DataExpression = c.rhs_term_stack.evaluate_with(matched, builder);

312

361554

            let lhs: DataExpression = c.lhs_term_stack.evaluate_with(matched, builder);

313

314

            // Equality => lhs == rhs.

315

361554

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

316

358203

                let rhs_normal = SabreRewriter::stack_based_normalise_aux(

317

358203

tp,

318

358203

                    automaton,

319

358203

                    builder,

320

358203

                    &mut substitution_builder,

321

358203

                    &rhs,

322

358203

                    stats,

323

);

324

358203

                let lhs_normal = SabreRewriter::stack_based_normalise_aux(

325

358203

tp,

326

358203

                    automaton,

327

358203

                    builder,

328

358203

                    &mut substitution_builder,

329

358203

                    &lhs,

330

358203

                    stats,

331

);

332

333

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

334

358203

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

335

151977

                    return false;

336

206226

337

3351

338

339

340

208905

        true

341

360882

342