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::SideInfo;

19

use crate::utilities::SideInfoType;

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

/// The Set Automaton based Rewrite Engine implementation.

38

pub struct SabreRewriter {

39

    automaton: SetAutomaton<AnnouncementSabre>,

40

41

42

impl RewriteEngine for SabreRewriter {

43

42

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

44

42

        self.stack_based_normalise(term)

45

42

46

47

48

impl SabreRewriter {

49

26

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

50

26

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

51

52

26

        SabreRewriter { automaton }

53

26

54

55

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

56

42

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

57

42

        let mut stats = RewritingStatistics::default();

58

59

42

        let result = THREAD_TERM_POOL

60

42

            .with_borrow(|tp| SabreRewriter::stack_based_normalise_aux(tp, &self.automaton, t, &mut stats));

61

62

42

        info!(

63

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

64

            stats.recursions, stats.rewrite_steps, stats.symbol_comparisons

65

);

66

67

42

        result

68

42

69

70

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

71

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

72

239528

    fn stack_based_normalise_aux(

73

239528

        tp: &ThreadTermPool,

74

239528

        automaton: &SetAutomaton<AnnouncementSabre>,

75

239528

        t: &DataExpression,

76

239528

        stats: &mut RewritingStatistics,

77

239528

    ) -> DataExpression {

78

239528

        stats.recursions += 1;

79

80

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

81

239528

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

82

83

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

84

        'outer: loop {

85

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

86

            'skip_point: loop {

87

8371928

                debug_trace!("{}", cs);

88

89

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

90

8371928

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

91

8132400

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

92

8132400

                    let read_terms = cs.terms.read();

93

8132400

                    let leaf_term = &read_terms[leaf_index];

94

95

8132400

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

96

                        None => {

97

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

98

7408056

                            let pos: DataExpressionRef =

99

7408056

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

100

101

7408056

                            let function_symbol = pos.data_function_symbol();

102

7408056

                            stats.symbol_comparisons += 1;

103

104

                            // Get the transition belonging to the observed symbol

105

7408056

                            if let Some(tr) = automaton

106

7408056

                                .transitions()

107

7408056

                                .get(&(leaf.state, function_symbol.operation_id()))

108

109

                                // Loop over the match announcements of the transition

110

7408038

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

111

1241809

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

112

1098069

                                        if annotation.is_duplicating {

113

15698

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

114

15698

115

15698

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

116

15698

                                            cs.side_branch_stack.push(SideInfo {

117

15698

                                                corresponding_configuration: leaf_index,

118

15698

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

119

15698

});

120

15698

                                        } else {

121

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

122

1082371

                                            drop(read_terms);

123

1082371

                                            SabreRewriter::apply_rewrite_rule(

124

1082371

tp,

125

1082371

                                                automaton,

126

1082371

                                                announcement,

127

1082371

                                                annotation,

128

1082371

                                                leaf_index,

129

1082371

                                                &mut cs,

130

1082371

                                                stats,

131

);

132

1082371

                                            break 'skip_point;

133

134

143740

                                    } else {

135

143740

                                        // We delay the condition checks

136

143740

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

137

143740

138

143740

                                        cs.side_branch_stack.push(SideInfo {

139

143740

                                            corresponding_configuration: leaf_index,

140

143740

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

141

143740

});

142

143740

143

144

145

6325667

                                drop(read_terms);

146

6325667

                                if tr.destinations.is_empty() {

147

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

148

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

149

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

150

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

151

913016

                                    let prev = cs.get_prev_with_side_info();

152

913016

                                    cs.current_node = prev;

153

913016

                                    if let Some(n) = prev {

154

673491

                                        cs.jump_back(n, tp);

155

673491

156

5412651

                                } else {

157

5412651

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

158

5412651

                                    let tr_slice = tr.destinations.as_slice();

159

5412651

                                    cs.grow(leaf_index, tr_slice);

160

5412651

161

                            } else {

162

18

                                let prev = cs.get_prev_with_side_info();

163

18

                                cs.current_node = prev;

164

18

                                if let Some(n) = prev {

165

15

                                    drop(read_terms);

166

15

                                    cs.jump_back(n, tp);

167

15

168

169

170

724344

                        Some(sit) => {

171

724344

                            match sit {

172

588070

                                SideInfoType::SideBranch(sb) => {

173

588070

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

174

588070

                                    drop(read_terms);

175

588070

                                    cs.grow(leaf_index, sb);

176

588070

177

15674

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

178

15674

                                    drop(read_terms);

179

15674

                                    // apply the delayed rewrite rule

180

15674

                                    SabreRewriter::apply_rewrite_rule(

181

15674

tp,

182

15674

                                        automaton,

183

15674

                                        announcement,

184

15674

                                        annotation,

185

15674

                                        leaf_index,

186

15674

                                        &mut cs,

187

15674

                                        stats,

188

15674

);

189

15674

190

120600

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

191

                                    // Apply the delayed rewrite rule if the conditions hold

192

120600

                                    if check_equivalence_classes(leaf_term, &annotation.equivalence_classes)

193

120600

                                        && SabreRewriter::conditions_hold(

194

120600

tp,

195

120600

                                            automaton,

196

120600

                                            announcement,

197

120600

                                            annotation,

198

120600

                                            leaf_term,

199

120600

                                            stats,

200

201

69762

202

69762

                                        drop(read_terms);

203

69762

                                        SabreRewriter::apply_rewrite_rule(

204

69762

tp,

205

69762

                                            automaton,

206

69762

                                            announcement,

207

69762

                                            annotation,

208

69762

                                            leaf_index,

209

69762

                                            &mut cs,

210

69762

                                            stats,

211

69762

);

212

69762

213

214

215

216

217

                } else {

218

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

219

239528

                    break 'outer;

220

221

222

223

224

239528

        cs.compute_final_term(tp)

225

239528

226

227

    /// Apply a rewrite rule and prune back

228

1167807

    fn apply_rewrite_rule(

229

1167807

        tp: &ThreadTermPool,

230

1167807

        automaton: &SetAutomaton<AnnouncementSabre>,

231

1167807

        announcement: &MatchAnnouncement,

232

1167807

        annotation: &AnnouncementSabre,

233

1167807

        leaf_index: usize,

234

1167807

        cs: &mut ConfigurationStack<'_>,

235

1167807

        stats: &mut RewritingStatistics,

236

1167807

) {

237

1167807

        stats.rewrite_steps += 1;

238

239

1167807

        let read_terms = cs.terms.read();

240

1167807

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

241

242

        // Computes the new subterm of the configuration

243

1167807

        let new_subterm = annotation

244

1167807

            .rhs_term_stack

245

1167807

            .evaluate(&leaf_subterm.get_data_position(&announcement.position));

246

247

1167807

        debug_trace!(

248

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

249

            &leaf_subterm,

250

            &new_subterm,

251

            announcement.rule

252

);

253

254

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

255

1167807

        let prune_point = leaf_index - announcement.symbols_seen;

256

1167807

        drop(read_terms);

257

1167807

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

258

1167807

259

260

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

261

120600

    fn conditions_hold(

262

120600

        tp: &ThreadTermPool,

263

120600

        automaton: &SetAutomaton<AnnouncementSabre>,

264

120600

        announcement: &MatchAnnouncement,

265

120600

        annotation: &AnnouncementSabre,

266

120600

        subterm: &DataExpressionRef<'_>,

267

120600

        stats: &mut RewritingStatistics,

268

120600

    ) -> bool {

269

120824

        for c in &annotation.conditions {

270

120824

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

271

272

120824

            let rhs: DataExpression = c.rhs_term_stack.evaluate(&subterm);

273

120824

            let lhs: DataExpression = c.lhs_term_stack.evaluate(&subterm);

274

275

            // Equality => lhs == rhs.

276

120824

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

277

119743

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

278

119743

                let lhs_normal = SabreRewriter::stack_based_normalise_aux(tp, automaton, &lhs, stats);

279

280

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

281

119743

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

282

50838

                    return false;

283

68905

284

1081

285

286

287

69762

        true

288

120600

289