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::smt::TheoryConfig;

10

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

11

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

12

use glob::glob;

13

use itertools::Itertools;

14

use std::collections::BTreeMap;

15

use std::env;

16

use std::error::Error;

17

use std::fs;

18

use std::fs::File;

19

use tracing::{Level, span};

20

use tracing_subscriber::{

21

    Layer, Registry, filter::EnvFilter, filter::FilterFn, fmt, layer::SubscriberExt,

22

};

23

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

24

25

use uniplate::Biplate;

26

27

use std::path::Path;

28

use std::sync::Arc;

29

use std::sync::Mutex;

30

use std::sync::RwLock;

31

32

use conjure_cp::ast::Atom;

33

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

34

use conjure_cp::context::Context;

35

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

36

use conjure_cp::rule_engine::resolve_rule_sets;

37

use conjure_cp::solver::SolverFamily;

38

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

39

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

40

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

41

use conjure_cp_cli::utils::testing::{

42

    REWRITE_SERIALISED_JSON_MAX_LINES, read_model_json, read_model_json_prefix,

43

    read_solutions_json, save_model_json, save_solutions_json,

44

};

45

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

46

use conjure_cp_rules;

47

use pretty_assertions::assert_eq;

48

use serde::Deserialize;

49

50

#[derive(Deserialize, Debug)]

51

#[serde(default)]

52

#[serde(deny_unknown_fields)]

53

struct TestConfig {

54

    extra_rewriter_asserts: Vec<String>,

55

56

    enable_native_parser: bool, // Stage 1a: Use the native parser instead of the legacy parser

57

    apply_rewrite_rules: bool,  // Stage 2a: Applies predefined rules to the model

58

    enable_extra_validation: bool, // Stage 2b: Runs additional validation checks

59

60

    // NOTE: when adding a new solver config, make sure to update num_solvers_enabled!

61

    solve_with_minion: bool, // Stage 3a: Solves the model using Minion

62

    solve_with_sat: bool,    // TODO - add stage mark

63

    solve_with_smt: bool,    // TODO - add stage mark

64

65

    compare_solver_solutions: bool, // Stage 3b: Compares Minion and Conjure solutions

66

    validate_rule_traces: bool,     // Stage 4a: Checks rule traces against expected outputs

67

68

    enable_morph_impl: bool,

69

    enable_naive_impl: bool,

70

    enable_rewriter_impl: bool,

71

72

73

impl Default for TestConfig {

74

    fn default() -> Self {

75

        Self {

76

            extra_rewriter_asserts: vec!["vector_operators_have_partially_evaluated".into()],

77

            enable_naive_impl: true,

78

            solve_with_sat: false,

79

            solve_with_smt: false,

80

            enable_morph_impl: false,

81

            enable_rewriter_impl: true,

82

            enable_native_parser: true,

83

            apply_rewrite_rules: true,

84

            enable_extra_validation: false,

85

            solve_with_minion: true,

86

            compare_solver_solutions: true,

87

            validate_rule_traces: true,

88

89

90

91

92

fn env_var_override_bool(key: &str, default: bool) -> bool {

93

    env::var(key).ok().map(|s| s == "true").unwrap_or(default)

94

95

impl TestConfig {

96

    fn merge_env(self) -> Self {

97

        Self {

98

            enable_morph_impl: env_var_override_bool("ENABLE_MORPH_IMPL", self.enable_morph_impl),

99

            enable_naive_impl: env_var_override_bool("ENABLE_NAIVE_IMPL", self.enable_naive_impl),

100

            enable_native_parser: env_var_override_bool(

101

                "ENABLE_NATIVE_PARSER",

102

                self.enable_native_parser,

103

),

104

            apply_rewrite_rules: env_var_override_bool(

105

                "APPLY_REWRITE_RULES",

106

                self.apply_rewrite_rules,

107

),

108

            enable_extra_validation: env_var_override_bool(

109

                "ENABLE_EXTRA_VALIDATION",

110

                self.enable_extra_validation,

111

),

112

            solve_with_minion: env_var_override_bool("SOLVE_WITH_MINION", self.solve_with_minion),

113

            solve_with_sat: env_var_override_bool("SOLVE_WITH_SAT", self.solve_with_sat),

114

            solve_with_smt: env_var_override_bool("SOLVE_WITH_SMT", self.solve_with_smt),

115

            compare_solver_solutions: env_var_override_bool(

116

                "COMPARE_SOLVER_SOLUTIONS",

117

                self.compare_solver_solutions,

118

),

119

            validate_rule_traces: env_var_override_bool(

120

                "VALIDATE_RULE_TRACES",

121

                self.validate_rule_traces,

122

),

123

            enable_rewriter_impl: env_var_override_bool(

124

                "ENABLE_REWRITER_IMPL",

125

                self.enable_rewriter_impl,

126

),

127

            extra_rewriter_asserts: self.extra_rewriter_asserts, // Not overridden by env vars

128

129

130

131

    fn num_solvers_enabled(&self) -> usize {

132

        let mut num = 0;

133

        num += self.solve_with_minion as usize;

134

        num += self.solve_with_sat as usize;

135

        num += self.solve_with_smt as usize;

136

num

137

138

139

140

fn main() {

141

    let _guard = create_scoped_subscriber("./logs", "test_log");

142

143

    // creating a span and log a message

144

    let test_span = span!(Level::TRACE, "test_span");

145

    let _enter: span::Entered<'_> = test_span.enter();

146

147

    for entry in glob("conjure_cp_cli/tests/integration/*").expect("Failed to read glob pattern") {

148

        match entry {

149

            Ok(path) => println!("File: {path:?}"),

150

            Err(e) => println!("Error: {e:?}"),

151

152

153

154

    let file_path = Path::new("conjure_cp_cli/tests/integration/*"); // using relative path

155

156

    let base_name = file_path.file_stem().and_then(|stem| stem.to_str());

157

158

    match base_name {

159

        Some(name) => println!("Base name: {name}"),

160

        None => println!("Could not extract the base name"),

161

162

163

164

// run tests in sequence not parallel when verbose logging, to ensure the logs are ordered

165

// correctly

166

static GUARD: Mutex<()> = Mutex::new(());

167

168

// wrapper to conditionally enforce sequential execution

169

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

170

    let verbose = env::var("VERBOSE").unwrap_or("false".to_string()) == "true";

171

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

172

173

    let subscriber = create_scoped_subscriber(path, essence_base);

174

    // run tests in sequence not parallel when verbose logging, to ensure the logs are ordered

175

    // correctly

176

//

177

    // also with ACCEPT=true, as the conjure checking seems to get confused when ran too much at

178

    // once.

179

    if verbose || accept {

180

        let _guard = GUARD.lock().unwrap_or_else(|e| e.into_inner());

181

182

        // set the subscriber as default

183

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

184

            integration_test_inner(path, essence_base, extension)

185

})

186

    } else {

187

        let subscriber = create_scoped_subscriber(path, essence_base);

188

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

189

            integration_test_inner(path, essence_base, extension)

190

})

191

192

193

194

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

195

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

196

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

197

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

198

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

199

///

200

/// This function operates in multiple stages:

201

///

202

/// - **Parsing Stage**

203

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

204

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

205

///

206

/// - **Rewrite Stage**

207

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

208

///   - **Stage 2b (Optional)**: Runs additional validation checks on the rewritten model if enabled.

209

///

210

/// - **Solution Stage**

211

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

212

///   - **Stage 3b (Optional)**: Compares the Minion solutions against Conjure-generated solutions if enabled.

213

///

214

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

215

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

216

///

217

/// # Arguments

218

///

219

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

220

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

221

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

222

///

223

/// # Errors

224

///

225

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

226

#[allow(clippy::unwrap_used)]

227

fn integration_test_inner(

228

    path: &str,

229

    essence_base: &str,

230

    extension: &str,

231

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

232

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

233

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

234

    let verbose = env::var("VERBOSE").unwrap_or("false".to_string()) == "true";

235

236

    if verbose {

237

        println!("Running integration test for {path}/{essence_base}, ACCEPT={accept}");

238

239

240

    let file_config: TestConfig =

241

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

242

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

243

        } else {

244

            Default::default()

245

};

246

247

    let config = file_config.merge_env();

248

249

    // TODO: allow either Minion or SAT but not both; eventually allow both sovlers to be tested

250

251

    if config.num_solvers_enabled() > 1 {

252

        todo!("Not yet implemented simultaneous testing of multiple solvers")

253

254

255

    // File path

256

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

257

258

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

259

    let parsed_model = if config.enable_native_parser {

260

        let model = parse_essence_file_native(&file_path, context.clone())?;

261

        if verbose {

262

            println!("Parsed model (native): {model:#?}");

263

264

        save_model_json(&model, path, essence_base, "parse")?;

265

266

267

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

268

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

269

270

271

        model

272

    // Stage 1b: Parse the model using the legacy parser

273

    } else {

274

        let model = parse_essence_file(&file_path, context.clone())?;

275

        if verbose {

276

            println!("Parsed model (legacy): {model:#?}");

277

278

        save_model_json(&model, path, essence_base, "parse")?;

279

        model

280

};

281

282

    // Stage 2a: Rewrite the model using the rule engine (run unless explicitly disabled)

283

    let rewritten_model = if config.apply_rewrite_rules {

284

        // rule set selection based on solver

285

286

        let solver_fam = if config.solve_with_sat {

287

            SolverFamily::Sat

288

        } else if config.solve_with_smt {

289

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

290

        } else {

291

            SolverFamily::Minion

292

};

293

294

        let rule_sets = resolve_rule_sets(solver_fam, DEFAULT_RULE_SETS)?;

295

296

        let mut model = parsed_model;

297

298

        let rewritten = if config.enable_naive_impl {

299

            rewrite_naive(&model, &rule_sets, false, false)?

300

        } else if config.enable_morph_impl {

301

            let submodel = model.as_submodel_mut();

302

            let rules_grouped = get_rules_grouped(&rule_sets)

303

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

304

                .into_iter()

305

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

306

                .collect_vec();

307

308

            let engine = EngineBuilder::new()

309

                .set_selector(select_panic)

310

                .append_rule_groups(rules_grouped)

311

                .build();

312

            let (expr, symbol_table) =

313

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

314

315

            *submodel.symbols_mut() = symbol_table;

316

            submodel.replace_root(expr);

317

            model.clone()

318

        } else {

319

            panic!("No rewriter implementation specified")

320

};

321

        if verbose {

322

            println!("Rewritten model: {rewritten:#?}");

323

324

325

        save_model_json(&rewritten, path, essence_base, "rewrite")?;

326

        Some(rewritten)

327

    } else {

328

        None

329

};

330

331

    // Stage 2b: Check model properties (extra_asserts) (Verify additional model properties)

332

    // (e.g., ensure vector operators are evaluated). (only if explicitly enabled)

333

    if config.enable_extra_validation {

334

        for extra_assert in config.extra_rewriter_asserts.clone() {

335

            match extra_assert.as_str() {

336

                "vector_operators_have_partially_evaluated" => {

337

                    assert_vector_operators_have_partially_evaluated(

338

                        rewritten_model.as_ref().expect("Rewritten model required"),

339

);

340

341

                x => println!("Unrecognised extra assert: {x}"),

342

};

343

344

345

346

    let solver_input_file = env::var("OXIDE_TEST_SAVE_INPUT_FILE").ok().map(|_| {

347

        let name = format!("{essence_base}.generated-input.txt");

348

        Path::new(path).join(Path::new(&name))

349

});

350

351

    let solver = if config.solve_with_minion {

352

        Some(Solver::new(Minion::default()))

353

    } else if config.solve_with_sat {

354

        Some(Solver::new(Sat::default()))

355

    } else if config.solve_with_smt {

356

        Some(Solver::new(Smt::default()))

357

    } else {

358

        None

359

};

360

361

    let solutions = if let Some(solver) = solver {

362

        let name = solver.get_name();

363

        let family = solver.get_family();

364

365

        let solved = get_solutions(

366

            solver,

367

            rewritten_model

368

                .as_ref()

369

                .expect("Rewritten model must be present in 2a")

370

                .clone(),

371

0,

372

            &solver_input_file,

373

)?;

374

        let solutions_json = save_solutions_json(&solved, path, essence_base, family)?;

375

        if verbose {

376

            println!("{name} solutions: {solutions_json:#?}");

377

378

        solved

379

    } else {

380

        println!("Warning: no solver specified");

381

        Vec::new()

382

};

383

384

    // Stage 3b: Check solutions against Conjure (only if explicitly enabled)

385

    if config.compare_solver_solutions && config.num_solvers_enabled() > 0 {

386

        let conjure_solutions: Vec<BTreeMap<Name, Literal>> = get_solutions_from_conjure(

387

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

388

            Arc::clone(&context),

389

)?;

390

391

        let username_solutions = normalize_solutions_for_comparison(&solutions);

392

        let conjure_solutions = normalize_solutions_for_comparison(&conjure_solutions);

393

394

        let mut conjure_solutions_json = solutions_to_json(&conjure_solutions);

395

        let mut username_solutions_json = solutions_to_json(&username_solutions);

396

397

        conjure_solutions_json.sort_all_objects();

398

        username_solutions_json.sort_all_objects();

399

400

        assert_eq!(

401

            username_solutions_json, conjure_solutions_json,

402

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

403

);

404

405

406

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

407

    if accept {

408

        copy_generated_to_expected(path, essence_base, "parse", "serialised.json")?;

409

410

        if config.apply_rewrite_rules {

411

            copy_generated_to_expected(path, essence_base, "rewrite", "serialised.json")?;

412

413

414

        if config.solve_with_minion {

415

            copy_generated_to_expected(path, essence_base, "minion", "solutions.json")?;

416

        } else if config.solve_with_sat {

417

            copy_generated_to_expected(path, essence_base, "sat", "solutions.json")?;

418

        } else if config.solve_with_smt {

419

            copy_generated_to_expected(path, essence_base, "smt", "solutions.json")?;

420

421

422

        if config.validate_rule_traces {

423

            copy_human_trace_generated_to_expected(path, essence_base)?;

424

            save_stats_json(context.clone(), path, essence_base)?;

425

426

427

428

    // Check Stage 1: Compare parsed model with expected

429

    let expected_model = read_model_json(&context, path, essence_base, "expected", "parse")?;

430

    let model_from_file = read_model_json(&context, path, essence_base, "generated", "parse")?;

431

    assert_eq!(model_from_file, expected_model);

432

433

    // Check Stage 2a (rewritten model)

434

    if config.apply_rewrite_rules {

435

        let expected_rewrite = read_model_json_prefix(

436

            path,

437

            essence_base,

438

            "expected",

439

            "rewrite",

440

            REWRITE_SERIALISED_JSON_MAX_LINES,

441

)?;

442

        let generated_rewrite = read_model_json_prefix(

443

            path,

444

            essence_base,

445

            "generated",

446

            "rewrite",

447

            REWRITE_SERIALISED_JSON_MAX_LINES,

448

)?;

449

        assert_eq!(generated_rewrite, expected_rewrite);

450

451

452

    // Check Stage 3a (solutions)

453

    if config.solve_with_minion {

454

        let expected_solutions_json =

455

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

456

        let username_solutions_json = solutions_to_json(&solutions);

457

        assert_eq!(username_solutions_json, expected_solutions_json);

458

    } else if config.solve_with_sat {

459

        let expected_solutions_json =

460

            read_solutions_json(path, essence_base, "expected", SolverFamily::Sat)?;

461

        let username_solutions_json = solutions_to_json(&solutions);

462

        assert_eq!(username_solutions_json, expected_solutions_json);

463

    } else if config.solve_with_smt {

464

        let expected_solutions_json = read_solutions_json(

465

            path,

466

            essence_base,

467

            "expected",

468

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

469

)?;

470

        let username_solutions_json = solutions_to_json(&solutions);

471

        assert_eq!(username_solutions_json, expected_solutions_json);

472

473

474

    // Stage 4a: Check that the generated rules trace matches the expected.

475

    // We don't check rule trace when morph is enabled.

476

    // TODO: Implement rule trace validation for morph

477

    if config.validate_rule_traces && !config.enable_morph_impl {

478

        let generated = read_human_rule_trace(path, essence_base, "generated")?;

479

        let expected = read_human_rule_trace(path, essence_base, "expected")?;

480

481

        assert_eq!(

482

            expected, generated,

483

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

484

);

485

};

486

487

    save_stats_json(context, path, essence_base)?;

488

489

    Ok(())

490

491

492

fn copy_human_trace_generated_to_expected(

493

    path: &str,

494

    test_name: &str,

495

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

496

    std::fs::copy(

497

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

498

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

499

)?;

500

    Ok(())

501

502

503

fn copy_generated_to_expected(

504

    path: &str,

505

    test_name: &str,

506

    stage: &str,

507

    extension: &str,

508

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

509

    std::fs::copy(

510

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

511

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

512

)?;

513

    Ok(())

514

515

516

fn assert_vector_operators_have_partially_evaluated(model: &conjure_cp::Model) {

517

    for node in model.universe_bi() {

518

        use conjure_cp::ast::Expression::*;

519

        match node {

520

            Sum(_, ref vec) => assert_constants_leq_one_vec_lit(&node, vec),

521

            Min(_, ref vec) => assert_constants_leq_one_vec_lit(&node, vec),

522

            Max(_, ref vec) => assert_constants_leq_one_vec_lit(&node, vec),

523

            Or(_, ref vec) => assert_constants_leq_one_vec_lit(&node, vec),

524

            And(_, ref vec) => assert_constants_leq_one_vec_lit(&node, vec),

525

            _ => (),

526

};

527

528

529

530

fn assert_constants_leq_one_vec_lit(parent_expr: &Expression, expr: &Expression) {

531

    if let Some(exprs) = expr.clone().unwrap_list() {

532

        assert_constants_leq_one(parent_expr, &exprs);

533

};

534

535

536

fn assert_constants_leq_one(parent_expr: &Expression, exprs: &[Expression]) {

537

    let count = exprs.iter().fold(0, |i, x| match x {

538

        Expression::Atomic(_, Atom::Literal(_)) => i + 1,

539

        _ => i,

540

});

541

542

    assert!(

543

        count <= 1,

544

        "assert_vector_operators_have_partially_evaluated: expression {parent_expr} is not partially evaluated"

545

);

546

547

548

pub fn create_scoped_subscriber(

549

    path: &str,

550

    test_name: &str,

551

) -> impl tracing::Subscriber + Send + Sync {

552

    let layer = create_file_layer_human(path, test_name);

553

    let subscriber = Arc::new(tracing_subscriber::registry().with(layer))

554

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

555

    // setting this subscriber as the default

556

    let _default = tracing::subscriber::set_default(subscriber.clone());

557

558

    subscriber

559

560

561

fn create_file_layer_human(path: &str, test_name: &str) -> impl Layer<Registry> + Send + Sync {

562

    let file = File::create(format!("{path}/{test_name}-generated-rule-trace-human.txt"))

563

        .expect("Unable to create log file");

564

565

    fmt::layer()

566

        .with_writer(file)

567

        .with_level(false)

568

        .without_time()

569

        .with_target(false)

570

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

571

        .with_filter(FilterFn::new(|meta| meta.target() == "rule_engine_human"))

572

573

574

#[test]

575

fn assert_conjure_present() {

576

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

577

578

579

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