Grcov report - bubble.rs

1

use conjure_cp::{

2

    ast::Metadata,

3

    ast::{

4

        Atom, DeclarationKind, Expression, Literal, Moo, Name, Reference, ReturnType, SymbolTable,

5

        Typeable, eval_constant,

6

},

7

    into_matrix_expr, matrix_expr,

8

    rule_engine::{

9

        ApplicationError::{self, RuleNotApplicable},

10

        ApplicationResult, RuleEffect, register_rule, register_rule_set,

11

},

12

};

13

use uniplate::Biplate;

14

15

use crate::shared::utils::rewrite_children;

16

17

register_rule_set!("Bubble", ("Base"));

18

19

// Bubble reduction rules

20

21

/*

22

    Reduce bubbles with a boolean expression to a conjunction with their condition.

23

24

    e.g. (a / b = c) @ (b != 0) => (a / b = c) & (b != 0)

25

*/

26

#[register_rule("Bubble", 8900, [Bubble])]

27

100437

fn expand_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

28

100437

    match expr {

29

95036

        Expression::Bubble(_, a, b) if a.return_type() == ReturnType::Bool => {

30

43217

            let a = Moo::unwrap_or_clone(Moo::clone(a));

31

43217

            let b = Moo::unwrap_or_clone(Moo::clone(b));

32

43217

            Ok(RuleEffect::pure(Expression::And(

33

43217

                Metadata::new(),

34

43217

                Moo::new(matrix_expr![a, b]),

35

43217

)))

36

37

57220

        _ => Err(ApplicationError::RuleNotApplicable),

38

39

100437

40

41

/*

42

    Bring bubbles with a non-boolean expression higher up the tree.

43

44

    E.g. ((a / b) @ (b != 0)) = c => (a / b = c) @ (b != 0)

45

*/

46

#[register_rule("Bubble", 8800, [* / Bubble, * / Atomic / Reference])]

47

11112783

fn bubble_up(expr: &Expression, syms: &SymbolTable) -> ApplicationResult {

48

    // catchUndef consumes definedness itself; lifting its bubble would bypass the fallback.

49

    // do not put root inside a bubble

50

//

51

    // also do not bubble bubbles inside bubbles, as this does nothing productive it just shuffles

52

    // the conditions around, shuffles them back, then gets stuck in a loop doing this ad infinitum

53

11112783

    if matches!(

54

11112783

        expr,

55

        Expression::Root(_, _) | Expression::Bubble(_, _, _) | Expression::CatchUndef(_, _, _)

56

) {

57

11781

        return Err(RuleNotApplicable);

58

11101002

59

60

11101002

    let mut bubbled_conditions = vec![];

61

11101002

    let mut followed_lettings = vec![];

62

29244613

    let (new_inner, num_changed) = rewrite_children(expr, |child| match child {

63

42819

        Expression::Bubble(_, a, b) if a.return_type() != ReturnType::Bool => {

64

42801

            let a = Moo::unwrap_or_clone(a);

65

42801

            let b = Moo::unwrap_or_clone(b);

66

42801

            bubbled_conditions.push(b);

67

42801

            (a, true)

68

69

        // A bubble in a value letting's body has nothing above it to escape into, so follow the

70

        // reference and lift it from here instead. Without this, `letting a be 2 / 0` leaves every

71

        // use of `a` an opaque reference all the way down to the solver adaptor.

72

        Expression::Atomic(_, Atom::Reference(ref reference)) => {

73

20815191

            let Some((inner, condition, name)) = bubbled_value_letting(reference) else {

74

20815189

                return (child, false);

75

};

76

2

            bubbled_conditions.push(condition);

77

2

            followed_lettings.push(name);

78

2

            (inner, true)

79

80

8386621

        child => (child, false),

81

29244613

});

82

11101002

    if num_changed == 0 {

83

11058621

        return Err(ApplicationError::RuleNotApplicable);

84

42381

85

86

    // The value-letting guard walks every referenced name in the subtree, so keep it behind the

87

    // cheap direct-child check above. Most `bubble_up` attempts fail before this point. Lettings

88

    // this call has just followed are exempt: their bubble is the one being lifted. Defined

89

    // constant lettings cannot hide another bubble and must not prevent index guards escaping.

90

463393

    if expr.universe_bi().iter().any(|x: &Name| {

91

463393

        !followed_lettings.contains(x)

92

463391

            && syms.lookup(x).is_some_and(|x| {

93

463391

                matches!(

94

463391

                    &x.kind() as &DeclarationKind,

95

854

                    DeclarationKind::ValueLetting(value, _) if eval_constant(value).is_none()

96

97

463391

})

98

463393

    }) {

99

        return Err(RuleNotApplicable);

100

42381

};

101

102

42381

    if bubbled_conditions.len() == 1 {

103

41959

        let new_expr = Expression::Bubble(

104

41959

            Metadata::new(),

105

41959

            Moo::new(new_inner),

106

41959

            Moo::new(bubbled_conditions[0].clone()),

107

41959

);

108

109

41959

        Ok(RuleEffect::pure(new_expr))

110

    } else {

111

422

        Ok(RuleEffect::pure(Expression::Bubble(

112

422

            Metadata::new(),

113

422

            Moo::new(new_inner),

114

422

            Moo::new(Expression::And(

115

422

                Metadata::new(),

116

422

                Moo::new(into_matrix_expr![bubbled_conditions]),

117

422

)),

118

422

)))

119

120

11112783

121

122

/// The inner expression, bubble condition and name of a value letting whose body is a non-boolean

123

/// bubble, e.g. `letting a be 2 / 0`.

124

20815191

fn bubbled_value_letting(reference: &Reference) -> Option<(Expression, Expression, Name)> {

125

20815191

    let declaration = reference.ptr();

126

20815191

    let value = declaration.as_value_letting()?;

127

10707

    let Expression::Bubble(_, inner, condition) = &*value else {

128

10705

        return None;

129

};

130

2

    if inner.return_type() == ReturnType::Bool {

131

        return None;

132

2

133

2

    Some((

134

2

        Moo::unwrap_or_clone(Moo::clone(inner)),

135

2

        Moo::unwrap_or_clone(Moo::clone(condition)),

136

2

        reference.name().clone(),

137

2

))

138

20815191

139

140

// Bubble applications

141

142

/// Converts an unsafe division to a safe division with a bubble condition.

143

///

144

/// ```text

145

///     a / b => (a / b) @ (b != 0)

146

/// ```

147

///

148

/// Division by zero is undefined and therefore not allowed, so we add a condition to check for it.

149

/// This condition is brought up the tree and expanded into a conjunction with the first

150

/// boolean-type expression it is paired with.

151

152

#[register_rule("Bubble", 6000, [UnsafeDiv])]

153

191279

fn div_to_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

154

191279

    if eval_constant(expr).is_some() {

155

267

        return Err(RuleNotApplicable);

156

191012

157

191012

    if let Expression::UnsafeDiv(_, a, b) = expr {

158

        // bubble bottom up

159

187575

        if !a.is_safe() || !b.is_safe() {

160

1533

            return Err(RuleNotApplicable);

161

186042

162

163

186042

        return Ok(RuleEffect::pure(Expression::Bubble(

164

186042

            Metadata::new(),

165

186042

            Moo::new(Expression::SafeDiv(Metadata::new(), a.clone(), b.clone())),

166

186042

            Moo::new(Expression::Neq(

167

186042

                Metadata::new(),

168

186042

                b.clone(),

169

186042

                Moo::new(Expression::from(0)),

170

186042

)),

171

186042

        )));

172

3437

173

3437

    Err(ApplicationError::RuleNotApplicable)

174

191279

175

176

/// Converts an unsafe mod to a safe mod with a bubble condition.

177

///

178

/// ```text

179

/// a % b => (a % b) @ (b != 0)

180

/// ```

181

///

182

/// Mod zero is undefined and therefore not allowed, so we add a condition to check for it.

183

/// This condition is brought up the tree and expanded into a conjunction with the first

184

/// boolean-type expression it is paired with.

185

///

186

#[register_rule("Bubble", 6000, [UnsafeMod])]

187

341134

fn mod_to_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

188

341134

    if eval_constant(expr).is_some() {

189

267

        return Err(RuleNotApplicable);

190

340867

191

340867

    if let Expression::UnsafeMod(_, a, b) = expr {

192

        // bubble bottom up

193

337430

        if !a.is_safe() || !b.is_safe() {

194

155905

            return Err(RuleNotApplicable);

195

181525

196

197

181525

        return Ok(RuleEffect::pure(Expression::Bubble(

198

181525

            Metadata::new(),

199

181525

            Moo::new(Expression::SafeMod(Metadata::new(), a.clone(), b.clone())),

200

181525

            Moo::new(Expression::Neq(

201

181525

                Metadata::new(),

202

181525

                b.clone(),

203

181525

                Moo::new(Expression::from(0)),

204

181525

)),

205

181525

        )));

206

3437

207

3437

    Err(ApplicationError::RuleNotApplicable)

208

341134

209

210

/// Converts an unsafe pow to a safe pow with a bubble condition.

211

///

212

/// ```text

213

/// a**b => (a ** b) @ ((a!=0 \/ b!=0) /\ b>=0

214

/// ```

215

///

216

/// Pow is only defined when `(a!=0 \/ b!=0) /\ b>=0`, so we add a condition to check for it.

217

/// This condition is brought up the tree and expanded into a conjunction with the first

218

/// boolean-type expression it is paired with.

219

///

220

#[register_rule("Bubble", 6000, [UnsafePow])]

221

12825

fn pow_to_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

222

12825

    if eval_constant(expr).is_some() {

223

267

        return Err(RuleNotApplicable);

224

12558

225

12558

    if let Expression::UnsafePow(_, a, b) = expr.clone() {

226

        // bubble bottom up

227

9139

        if !a.is_safe() || !b.is_safe() {

228

497

            return Err(RuleNotApplicable);

229

8642

230

231

8642

        return Ok(RuleEffect::pure(Expression::Bubble(

232

8642

            Metadata::new(),

233

8642

            Moo::new(Expression::SafePow(Metadata::new(), a.clone(), b.clone())),

234

8642

            Moo::new(Expression::And(

235

8642

                Metadata::new(),

236

8642

                Moo::new(matrix_expr![

237

8642

                    Expression::Or(

238

8642

                        Metadata::new(),

239

8642

                        Moo::new(matrix_expr![

240

8642

                            Expression::Neq(

241

8642

                                Metadata::new(),

242

8642

a,

243

8642

                                Moo::new(Atom::Literal(Literal::Int(0)).into()),

244

8642

),

245

8642

                            Expression::Neq(

246

8642

                                Metadata::new(),

247

8642

                                b.clone(),

248

8642

                                Moo::new(Atom::Literal(Literal::Int(0)).into()),

249

8642

),

250

8642

]),

251

8642

),

252

8642

                    Expression::Geq(

253

8642

                        Metadata::new(),

254

8642

b,

255

8642

                        Moo::new(Atom::Literal(Literal::Int(0)).into()),

256

8642

),

257

8642

]),

258

8642

)),

259

8642

        )));

260

3419

261

3419

    Err(ApplicationError::RuleNotApplicable)

262

12825

263

264

/// An enum endpoint has no predecessor/successor. Preserve that undefinedness until the

265

/// surrounding boolean expression (or catchUndef) consumes it.

266

#[register_rule("Bubble", 6000, [Pred, Succ])]

267

3708

fn enum_neighbour_to_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

268

3708

    let (Expression::Pred(_, operand) | Expression::Succ(_, operand)) = expr else {

269

3704

        return Err(RuleNotApplicable);

270

};

271

4

    let Some(Literal::EnumVariant(value)) = eval_constant(operand) else {

272

        return Err(RuleNotApplicable);

273

};

274

4

    let neighbour = if matches!(expr, Expression::Pred(_, _)) {

275

        value.pred()

276

    } else {

277

4

        value.succ()

278

};

279

4

    if neighbour.is_some() {

280

        return Err(RuleNotApplicable);

281

4

282

4

    Ok(RuleEffect::pure(Expression::Bubble(

283

4

        Metadata::new(),

284

4

        operand.clone(),

285

4

        Moo::new(false.into()),

286

4

)))

287

3708