Grcov report - roundtrip

1

//! Regression tests for parser bugs fixed during the crate review, plus

2

//! randomized print/parse round-trip (string-fixpoint) property tests.

3

4

use std::ops::ControlFlow;

5

6

use rand::RngExt;

7

8

use merc_syntax::Bound;

9

use merc_syntax::PbesExpr;

10

use merc_syntax::ProcExprBinaryOp;

11

use merc_syntax::ProcessExpr;

12

use merc_syntax::Span;

13

use merc_syntax::StateFrm;

14

use merc_syntax::UntypedDataSpecification;

15

use merc_syntax::UntypedPbes;

16

use merc_syntax::UntypedPres;

17

use merc_syntax::UntypedProcessSpecification;

18

use merc_syntax::UntypedStateFrmSpec;

19

use merc_syntax::line_column;

20

use merc_syntax::make_process_specification;

21

use merc_syntax::random_lps;

22

use merc_syntax::random_pbes;

23

use merc_syntax::visit_statefrm;

24

use merc_utilities::random_test;

25

26

// --- Regression tests for the review fixes -------------------------------------------------------

27

28

/// PBES quantifiers used to panic because `forall`/`exists` were registered as

29

/// prefix operators but only handled in the postfix closure.

30

#[test]

31

1

fn pbes_quantifiers_parse() {

32

1

    let pbes = UntypedPbes::parse("pbes mu X = forall n: Nat . val(n < 3) => exists m: Nat . val(m < n); init X;")

33

1

        .expect("PBES with quantifiers should parse");

34

35

1

    let formula = &pbes.equations[0].formula;

36

1

    assert!(

37

1

        matches!(formula, PbesExpr::Quantifier { .. } | PbesExpr::Binary { .. }),

38

        "unexpected formula: {formula:?}"

39

);

40

1

41

42

/// `sum`/`inf`/`sup` state-formula operators used to all collapse to `Bound::Sup`.

43

#[test]

44

1

fn state_formula_bounds_are_distinct() {

45

3

    for (input, expected) in [

46

1

        ("sum n: Nat . val(n < 3)", Bound::Sum),

47

1

        ("inf n: Nat . val(n < 3)", Bound::Inf),

48

1

        ("sup n: Nat . val(n < 3)", Bound::Sup),

49

1

] {

50

3

        let spec = UntypedStateFrmSpec::parse(input).expect("state formula should parse");

51

3

        match spec.formula {

52

3

            StateFrm::Bound { bound, .. } => assert_eq!(bound, expected, "for input {input:?}"),

53

            other => panic!("expected a Bound for {input:?}, got {other:?}"),

54

55

56

1

57

58

/// The process `<<` (until) operator used to hit `unimplemented!`.

59

#[test]

60

1

fn process_until_operator_parses() {

61

1

    let spec = UntypedProcessSpecification::parse("init a << b;").expect("`<<` should parse");

62

1

    match spec.init.expect("init present") {

63

1

        ProcessExpr::Binary { op, .. } => assert_eq!(op, ProcExprBinaryOp::Until),

64

        other => panic!("expected a binary Until, got {other:?}"),

65

66

1

67

68

/// A bare `delay` / `yaled` (without `@time`) used to fail to parse.

69

#[test]

70

1

fn bare_delay_and_yaled_parse() {

71

1

    assert!(matches!(

72

1

        UntypedStateFrmSpec::parse("delay").unwrap().formula,

73

        StateFrm::Delay(None)

74

));

75

1

    assert!(matches!(

76

1

        UntypedStateFrmSpec::parse("yaled").unwrap().formula,

77

        StateFrm::Yaled(None)

78

));

79

1

    assert!(matches!(

80

1

        UntypedStateFrmSpec::parse("delay@(3)").unwrap().formula,

81

        StateFrm::Delay(Some(_))

82

));

83

1

84

85

/// The left-merge operator must print as `||_` so that the output reparses.

86

#[test]

87

1

fn left_merge_round_trips() {

88

1

    let printed = format!("{}", UntypedProcessSpecification::parse("init a ||_ b;").unwrap());

89

1

    assert!(printed.contains("||_"), "left merge should print as ||_: {printed}");

90

1

    UntypedProcessSpecification::parse(&printed).expect("printed left merge should reparse");

91

1

92

93

/// A PRES used the `pbes` keyword, dropped infix operators, and mismatched the

94

/// constant-multiply rules. Exercise a spec that touches all of those.

95

#[test]

96

1

fn pres_specification_parses() {

97

1

    let pres = UntypedPres::parse(

98

1

        "pres \

99

1

           mu X(n: Nat) = (val(n < 3) => X(n)) && eqinf(X(n)) + val(2) * X(n); \

100

1

           nu Y = sup m: Nat . (Y + condsm(Y, Y, Y)); \

101

1

         init X(0);",

102

103

1

    .expect("PRES should parse");

104

1

    assert_eq!(pres.equations.len(), 2);

105

1

106

107

/// `visit_*` must return a `Break` value produced by a nested (non-root) node.

108

#[test]

109

1

fn visitor_breaks_from_nested_node() {

110

    // The `Y` identifier only appears below the top-level conjunction.

111

1

    let spec = UntypedStateFrmSpec::parse("true && (mu X. (X && Y))").unwrap();

112

113

6

    let found = visit_statefrm(&spec.formula, |frm| {

114

6

        if let StateFrm::Id(name, _) = frm

115

2

            && name == "Y"

116

117

1

            return Ok(ControlFlow::Break(name.clone()));

118

5

119

5

        Ok(ControlFlow::Continue(()))

120

6

})

121

1

    .unwrap();

122

123

1

    assert_eq!(found.as_deref(), Some("Y"), "Break value from a nested node was lost");

124

1

125

126

/// `line_column` used to be `print_location`, which computed the next accumulator

127

/// value as `current - line.len()`. When `span.start` fell inside the first line

128

/// (e.g. offset 0), `current - line.len()` underflowed for `usize`, causing a

129

/// panic in debug builds and silent wrap-around in release.

130

#[test]

131

1

fn line_column_no_underflow() {

132

    // Single-line: offset 0 is the first character — the old code would attempt

133

    // `0usize - "hello".len()` = underflow.

134

1

    assert_eq!(

135

1

        line_column("hello", &Span { start: 0, end: 1 }),

136

        (1, 1),

137

        "first character of a single-line string"

138

);

139

    // Interior character on the first line.

140

1

    assert_eq!(

141

1

        line_column("hello", &Span { start: 4, end: 5 }),

142

        (1, 5),

143

        "last character of a single-line string"

144

);

145

1

146

147

#[test]

148

1

fn line_column_multi_line() {

149

    // Second line: offset 6 is 'w' (the first character after the '\n' in "hello\n").

150

1

    assert_eq!(

151

1

        line_column("hello\nworld", &Span { start: 6, end: 7 }),

152

        (2, 1),

153

        "first character of second line"

154

);

155

    // Interior character on the second line.

156

1

    assert_eq!(

157

1

        line_column("hello\nworld", &Span { start: 8, end: 9 }),

158

        (2, 3),

159

        "third character of second line"

160

);

161

1

162

163

#[test]

164

1

fn line_column_past_end_does_not_panic() {

165

    // Offset past the end of input must not panic (saturating_sub guards this).

166

1

    let (line, _col) = line_column("hi", &Span { start: 100, end: 101 });

167

1

    assert_eq!(line, 1, "past-end offset resolves to the last line");

168

1

169

170

/// An `EqnSpec` without a `var` declaration section must not emit an empty

171

/// `var` section when printed. The grammar requires at least one declaration

172

/// after `var`, so printing an empty `var\n` block produces output that cannot

173

/// be parsed back.

174

#[test]

175

1

fn eqn_spec_without_variables_no_empty_var_section() {

176

1

    let spec = UntypedDataSpecification::parse("eqn true = false;").expect("eqn without var should parse");

177

1

    let printed = format!("{spec}");

178

1

    assert!(

179

1

        !printed.contains("var\n"),

180

        "empty var section must not be emitted:\n{printed}"

181

);

182

1

    UntypedDataSpecification::parse(&printed).expect("re-printed form must parse");

183

1

184

185

/// Action declarations with sort arguments used to be printed as `id(s1, s2)`

186

/// instead of the correct `id: s1 # s2` form. The incorrect form would fail to

187

/// reparse because the grammar expects a colon-separated sort product.

188

#[test]

189

1

fn act_decl_with_args_prints_colon_hash() {

190

1

    let spec = UntypedProcessSpecification::parse("act a: Bool # Nat;")

191

1

        .expect("action declaration with sort args should parse");

192

1

    let printed = format!("{spec}");

193

1

    assert!(

194

1

        printed.contains("a: Bool # Nat"),

195

        "ActDecl with args must use ':' and '#':\n{printed}"

196

);

197

1

    UntypedProcessSpecification::parse(&printed).expect("printed form must reparse");

198

1

199

200

// --- Randomized print/parse round-trip properties ------------------------------------------------

201

202

/// Property: for every generated AST, the printed form parses, and printing the

203

/// reparsed AST yields exactly the same string (a fixpoint of `parse ∘ display`).

204

/// This catches Display/grammar mismatches without depending on `PartialEq`

205

/// surviving parenthesization.

206

207

#[test]

208

#[cfg_attr(miri, ignore)] // Test is too slow under miri

209

1

fn random_lps_print_parse_fixpoint() {

210

100

    random_test(100, |rng| {

211

100

        let spec = random_lps(rng, 4, 3, 0.6);

212

100

        let printed = format!("{spec}");

213

100

        let reparsed = UntypedProcessSpecification::parse(&printed)

214

100

            .unwrap_or_else(|e| panic!("failed to reparse generated LPS:\n{printed}\nerror: {e}"));

215

100

        assert_eq!(printed, format!("{reparsed}"), "LPS print/parse not a fixpoint");

216

100

});

217

1

218

219

#[test]

220

#[cfg_attr(miri, ignore)] // Test is too slow under miri

221

1

fn random_process_spec_print_parse_fixpoint() {

222

100

    random_test(100, |rng| {

223

100

        let use_integers = rng.random_bool(0.5);

224

100

        let spec = make_process_specification(rng, 3, 4, use_integers);

225

100

        let printed = format!("{spec}");

226

100

        let reparsed = UntypedProcessSpecification::parse(&printed)

227

100

            .unwrap_or_else(|e| panic!("failed to reparse generated process spec:\n{printed}\nerror: {e}"));

228

100

        assert_eq!(

229

            printed,

230

100

            format!("{reparsed}"),

231

            "process spec print/parse not a fixpoint"

232

);

233

100

});

234

1

235

236

#[test]

237

#[cfg_attr(miri, ignore)] // Test is too slow under miri

238

1

fn random_pbes_print_parse_fixpoint() {

239

100

    random_test(100, |rng| {

240

100

        let use_quantifiers = rng.random_bool(0.5);

241

100

        let use_integers = rng.random_bool(0.5);

242

100

        let pbes = random_pbes(rng, 3, 4, 4, use_quantifiers, use_integers);

243

100

        let printed = format!("{pbes}");

244

100

        let reparsed = UntypedPbes::parse(&printed)

245

100

            .unwrap_or_else(|e| panic!("failed to reparse generated PBES:\n{printed}\nerror: {e}"));

246

100

        assert_eq!(printed, format!("{reparsed}"), "PBES print/parse not a fixpoint");

247

100

});

248

1