Grcov report - integration

1

#![allow(clippy::expect_used)]

2

use conjure_cp::bug;

3

use conjure_cp::rule_engine::get_rules_grouped;

4

5

use conjure_cp::defaults::DEFAULT_RULE_SETS;

6

use conjure_cp::parse::tree_sitter::parse_essence_file_native;

7

use conjure_cp::rule_engine::rewrite_naive;

8

use conjure_cp::solver::Solver;

9

use conjure_cp::solver::adaptors::*;

10

use conjure_cp_cli::utils::testing::{normalize_solutions_for_comparison, read_human_rule_trace};

11

use itertools::Itertools;

12

use std::collections::BTreeMap;

13

use std::env;

14

use std::error::Error;

15

use std::fs;

16

use std::fs::File;

17

use tracing_subscriber::{Layer, filter::EnvFilter, filter::FilterFn, fmt, layer::SubscriberExt};

18

use tree_morph::{helpers::select_panic, prelude::*};

19

20

#[cfg(feature = "smt")]

21

use conjure_cp::solver::adaptors::smt::TheoryConfig;

22

23

use std::sync::Arc;

24

use std::sync::RwLock;

25

26

use conjure_cp::ast::comprehension::set_quantified_expander_for_comprehensions;

27

use conjure_cp::ast::{Literal, Name};

28

use conjure_cp::context::Context;

29

use conjure_cp::parse::tree_sitter::parse_essence_file;

30

use conjure_cp::rule_engine::resolve_rule_sets;

31

use conjure_cp::settings::{Parser, QuantifiedExpander, Rewriter, SolverFamily};

32

use conjure_cp_cli::utils::conjure::solutions_to_json;

33

use conjure_cp_cli::utils::conjure::{get_solutions, get_solutions_from_conjure};

34

use conjure_cp_cli::utils::testing::save_stats_json;

35

use conjure_cp_cli::utils::testing::{read_solutions_json, save_solutions_json};

36

#[allow(clippy::single_component_path_imports, unused_imports)]

37

use conjure_cp_rules;

38

use pretty_assertions::assert_eq;

39

use tests_integration::TestConfig;

40

41

#[derive(Clone, Copy, Debug)]

42

struct RunCase<'a> {

43

    parser: Parser,

44

    rewriter: Rewriter,

45

    quantified_expander: QuantifiedExpander,

46

    solver: SolverFamily,

47

    case_name: &'a str,

48

49

50

261

fn integration_test(path: &str, essence_base: &str, extension: &str) -> Result<(), Box<dyn Error>> {

51

261

    let accept = env::var("ACCEPT").unwrap_or("false".to_string()) == "true";

52

53

261

    if accept {

54

        clean_test_dir_for_accept(path, essence_base, extension)?;

55

261

56

57

261

    let file_config: TestConfig =

58

261

        if let Ok(config_contents) = fs::read_to_string(format!("{path}/config.toml")) {

59

261

            toml::from_str(&config_contents).unwrap()

60

        } else {

61

            Default::default()

62

};

63

64

261

    let config = file_config;

65

66

261

    let parsers = config

67

261

        .configured_parsers()

68

261

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

69

261

    let rewriters = config

70

261

        .configured_rewriters()

71

261

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

72

261

    let quantified_expanders = config

73

261

        .configured_quantified_expanders()

74

261

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

75

261

    let solvers = config

76

261

        .configured_solvers()

77

261

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

78

    // Conjure output depends only on the input model, so cache it once per test case.

79

261

    let conjure_solutions = if accept {

80

        Some(Arc::new(get_solutions_from_conjure(

81

            &format!("{path}/{essence_base}.{extension}"),

82

            Default::default(),

83

        )?))

84

    } else {

85

261

        None

86

};

87

88

279

    for parser in parsers {

89

279

        for rewriter in rewriters.clone() {

90

279

            for quantified_expander in quantified_expanders.clone() {

91

279

                for solver in solvers.clone() {

92

279

                    let case_name = run_case_name(parser, rewriter, quantified_expander);

93

279

                    let run_case = RunCase {

94

279

                        parser,

95

279

                        rewriter,

96

279

                        quantified_expander,

97

279

                        solver,

98

279

                        case_name: case_name.as_str(),

99

279

};

100

279

                    let file = File::create(format!(

101

                        "{path}/{}-{}-generated-rule-trace.txt",

102

                        run_case.case_name,

103

279

                        run_case.solver.as_str()

104

                    ))?;

105

279

                    let subscriber = Arc::new(

106

279

                        tracing_subscriber::registry().with(

107

279

                            fmt::layer()

108

279

                                .with_writer(file)

109

279

                                .with_level(false)

110

279

                                .without_time()

111

279

                                .with_target(false)

112

279

                                .with_filter(EnvFilter::new("rule_engine_human=trace"))

113

20699

                                .with_filter(FilterFn::new(|meta| {

114

20699

                                    meta.target() == "rule_engine_human"

115

20699

                                })),

116

),

117

118

279

                        as Arc<dyn tracing::Subscriber + Send + Sync>;

119

279

                    tracing::subscriber::with_default(subscriber, || {

120

279

                        integration_test_inner(

121

279

                            path,

122

279

                            essence_base,

123

279

                            extension,

124

279

                            run_case,

125

279

                            conjure_solutions.clone(),

126

279

                            accept,

127

128

279

                    })?;

129

130

131

132

133

134

261

    Ok(())

135

261

136

137

/// Runs an integration test for a given Conjure model by:

138

/// 1. Parsing the model from an Essence file.

139

/// 2. Rewriting the model according to predefined rule sets.

140

/// 3. Solving the model using the Minion solver and validating the solutions.

141

/// 4. Comparing generated rule traces with expected outputs.

142

///

143

/// This function operates in multiple stages:

144

///

145

/// - **Parsing Stage**

146

///   - **Stage 1a (Default)**: Reads the Essence model file and verifies that it parses correctly using `parser = "tree-sitter"`.

147

///   - **Stage 1b (Optional)**: Reads the Essence model file and verifies that it parses correctly using `parser = "via-conjure"`.

148

///

149

/// - **Rewrite Stage**

150

///   - **Stage 2a**: Applies a set of rules to the parsed model and validates the result.

151

///

152

/// - **Solution Stage**

153

///   - **Stage 3a (Default)**: Uses Minion to solve the model and save the solutions.

154

///   - **Stage 3b (ACCEPT only)**: Compares solutions against Conjure-generated solutions.

155

///

156

/// - **Rule Trace Validation Stage**

157

///   - **Stage 4a (Default)**: Checks that the generated rules match expected traces.

158

///

159

/// # Arguments

160

///

161

/// * `path` - The file path where the Essence model and other resources are located.

162

/// * `essence_base` - The base name of the Essence model file.

163

/// * `extension` - The file extension for the Essence model.

164

///

165

/// # Errors

166

///

167

/// Returns an error if any stage fails due to a mismatch with expected results or file I/O issues.

168

#[allow(clippy::unwrap_used)]

169

279

fn integration_test_inner(

170

279

    path: &str,

171

279

    essence_base: &str,

172

279

    extension: &str,

173

279

    run_case: RunCase<'_>,

174

279

    conjure_solutions: Option<Arc<Vec<BTreeMap<Name, Literal>>>>,

175

279

    accept: bool,

176

279

) -> Result<(), Box<dyn Error>> {

177

279

    let solver_fam = run_case.solver;

178

279

    let rewriter = run_case.rewriter;

179

279

    let quantified_expander = run_case.quantified_expander;

180

279

    let parser = run_case.parser;

181

279

    let case_name = run_case.case_name;

182

183

279

    let context: Arc<RwLock<Context<'static>>> = Default::default();

184

185

279

    set_quantified_expander_for_comprehensions(quantified_expander);

186

187

    // File path

188

279

    let file_path = format!("{path}/{essence_base}.{extension}");

189

190

    // Stage 1a/1b: Parse the model using the selected parser.

191

279

    let parsed_model = match parser {

192

        Parser::TreeSitter => {

193

18

            let mut ctx = context.as_ref().write().unwrap();

194

18

            ctx.file_name = Some(format!("{path}/{essence_base}.{extension}"));

195

18

            parse_essence_file_native(&file_path, context.clone())?

196

197

261

        Parser::ViaConjure => parse_essence_file(&file_path, context.clone())?,

198

};

199

    // Stage 2a: Rewrite the model using the rule engine

200

279

    let mut extra_rules = vec![];

201

202

    // TODO (ss504): figure out why this is only here for sat

203

279

    if let SolverFamily::Sat(sat_encoding) = solver_fam {

204

        extra_rules.push(sat_encoding.as_rule_set());

205

279

206

207

279

    let mut rules_to_load = DEFAULT_RULE_SETS.to_vec();

208

279

    rules_to_load.extend(extra_rules);

209

210

279

    let rule_sets = resolve_rule_sets(solver_fam, &rules_to_load)?;

211

212

279

    let mut model = parsed_model;

213

214

279

    let rewritten_model = match rewriter {

215

279

        Rewriter::Naive => rewrite_naive(&model, &rule_sets, false, false)?,

216

        Rewriter::Morph => {

217

            let submodel = model.as_submodel_mut();

218

            let rules_grouped = get_rules_grouped(&rule_sets)

219

                .unwrap_or_else(|_| bug!("get_rule_priorities() failed!"))

220

                .into_iter()

221

                .map(|(_, rule)| rule.into_iter().map(|f| f.rule).collect_vec())

222

                .collect_vec();

223

224

            let engine = EngineBuilder::new()

225

                .set_selector(select_panic)

226

                .append_rule_groups(rules_grouped)

227

                .build();

228

            let (expr, symbol_table) =

229

                engine.morph(submodel.root().clone(), submodel.symbols().clone());

230

231

            *submodel.symbols_mut() = symbol_table;

232

            submodel.replace_root(expr);

233

            model.clone()

234

235

};

236

279

    let solver_input_file = None;

237

238

279

    let solver = match solver_fam {

239

234

        SolverFamily::Minion => Solver::new(Minion::default()),

240

        SolverFamily::Sat(_) => Solver::new(Sat::default()),

241

        #[cfg(feature = "smt")]

242

45

        SolverFamily::Smt(_) => Solver::new(Smt::default()),

243

};

244

245

279

    let solutions = {

246

279

        let solved = get_solutions(solver, rewritten_model, 0, &solver_input_file)?;

247

279

        save_solutions_json(&solved, path, case_name, solver_fam)?;

248

279

        solved

249

};

250

251

    // Stage 3b: Check solutions against Conjure when ACCEPT=true

252

279

    if accept {

253

        let conjure_solutions = conjure_solutions

254

            .as_deref()

255

            .expect("conjure solutions should be cached when ACCEPT=true");

256

257

        let username_solutions = normalize_solutions_for_comparison(&solutions);

258

        let conjure_solutions = normalize_solutions_for_comparison(conjure_solutions);

259

260

        let mut conjure_solutions_json = solutions_to_json(&conjure_solutions);

261

        let mut username_solutions_json = solutions_to_json(&username_solutions);

262

263

        conjure_solutions_json.sort_all_objects();

264

        username_solutions_json.sort_all_objects();

265

266

        assert_eq!(

267

            username_solutions_json, conjure_solutions_json,

268

            "Solutions (<) do not match conjure (>)!"

269

);

270

279

271

272

    // When ACCEPT=true, copy all generated files to expected

273

279

    if accept {

274

        // Always overwrite these ones. Unlike the rest, we don't need to selectively do these

275

        // based on the test results, so they don't get done later.

276

277

        copy_generated_to_expected(path, case_name, "solutions", "json", Some(solver_fam))?;

278

279

        copy_human_trace_generated_to_expected(path, case_name, solver_fam)?;

280

279

281

282

    // Check Stage 3a (solutions)

283

279

    match solver_fam {

284

        SolverFamily::Minion => {

285

234

            let expected_solutions_json =

286

234

                read_solutions_json(path, case_name, "expected", SolverFamily::Minion)?;

287

234

            let username_solutions_json = solutions_to_json(&solutions);

288

234

            assert_eq!(username_solutions_json, expected_solutions_json);

289

290

        SolverFamily::Sat(_) => {

291

            let expected_solutions_json = read_solutions_json(

292

                path,

293

                case_name,

294

                "expected",

295

                SolverFamily::Sat(Default::default()),

296

)?;

297

            let username_solutions_json = solutions_to_json(&solutions);

298

            assert_eq!(username_solutions_json, expected_solutions_json);

299

300

        #[cfg(feature = "smt")]

301

        SolverFamily::Smt(_) => {

302

45

            let expected_solutions_json = read_solutions_json(

303

45

                path,

304

45

                case_name,

305

45

                "expected",

306

45

                SolverFamily::Smt(TheoryConfig::default()),

307

)?;

308

45

            let username_solutions_json = solutions_to_json(&solutions);

309

45

            assert_eq!(username_solutions_json, expected_solutions_json);

310

311

312

313

    // // TODO: Implement rule trace validation for morph

314

279

    match rewriter {

315

        Rewriter::Morph => {}

316

        Rewriter::Naive => {

317

279

            let generated = read_human_rule_trace(path, case_name, "generated", &solver_fam)?;

318

279

            let expected = read_human_rule_trace(path, case_name, "expected", &solver_fam)?;

319

320

279

            assert_eq!(

321

                expected, generated,

322

                "Generated rule trace does not match the expected trace!"

323

);

324

325

326

327

279

    save_stats_json(context, path, case_name, solver_fam)?;

328

329

279

    Ok(())

330

279

331

332

279

fn run_case_name(

333

279

    parser: Parser,

334

279

    rewriter: Rewriter,

335

279

    quantified_expander: QuantifiedExpander,

336

279

) -> String {

337

279

    format!("{parser}-{rewriter}-{quantified_expander}")

338

279

339

340

fn clean_test_dir_for_accept(

341

    path: &str,

342

    essence_base: &str,

343

    extension: &str,

344

) -> Result<(), std::io::Error> {

345

    let input_filename = format!("{essence_base}.{extension}");

346

347

    for entry in std::fs::read_dir(path)? {

348

        let entry = entry?;

349

        let file_name = entry.file_name();

350

        let file_name = file_name.to_string_lossy();

351

        let entry_path = entry.path();

352

353

        if file_name == input_filename || file_name == "config.toml" {

354

            continue;

355

356

357

        if entry_path.is_dir() {

358

            std::fs::remove_dir_all(entry_path)?;

359

        } else {

360

            std::fs::remove_file(entry_path)?;

361

362

363

364

    Ok(())

365

366

367

fn copy_human_trace_generated_to_expected(

368

    path: &str,

369

    test_name: &str,

370

    solver: SolverFamily,

371

) -> Result<(), std::io::Error> {

372

    let solver_name = solver.as_str();

373

    std::fs::copy(

374

        format!("{path}/{test_name}-{solver_name}-generated-rule-trace.txt"),

375

        format!("{path}/{test_name}-{solver_name}-expected-rule-trace.txt"),

376

)?;

377

    Ok(())

378

379

380

fn copy_generated_to_expected(

381

    path: &str,

382

    test_name: &str,

383

    stage: &str,

384

    extension: &str,

385

    solver: Option<SolverFamily>,

386

) -> Result<(), std::io::Error> {

387

    let marker = solver.map_or("agnostic", |s| s.as_str());

388

389

    std::fs::copy(

390

        format!("{path}/{test_name}-{marker}.generated-{stage}.{extension}"),

391

        format!("{path}/{test_name}-{marker}.expected-{stage}.{extension}"),

392

)?;

393

    Ok(())

394

395

396

#[test]

397

1

fn assert_conjure_present() {

398

1

    conjure_cp_cli::find_conjure::conjure_executable().unwrap();

399

1

400

401

include!(concat!(env!("OUT_DIR"), "/gen_tests.rs"));