Grcov report - settings.rs

1

use std::{cell::Cell, fmt::Display, str::FromStr};

2

3

use schemars::JsonSchema;

4

use serde::{Deserialize, Serialize};

5

use strum_macros::{Display as StrumDisplay, EnumIter};

6

7

use crate::bug;

8

9

use crate::solver::adaptors::smt::{IntTheory, MatrixTheory, TheoryConfig};

10

11

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default)]

12

pub enum Parser {

13

    #[default]

14

    TreeSitter,

15

    ViaConjure,

16

17

18

impl Display for Parser {

19

93310

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

20

93310

        match self {

21

54740

            Parser::TreeSitter => write!(f, "tree-sitter"),

22

38570

            Parser::ViaConjure => write!(f, "via-conjure"),

23

24

93310

25

26

27

impl FromStr for Parser {

28

    type Err = String;

29

30

14820

    fn from_str(s: &str) -> Result<Self, Self::Err> {

31

14820

        match s.trim().to_ascii_lowercase().as_str() {

32

14820

            "tree-sitter" => Ok(Parser::TreeSitter),

33

7856

            "via-conjure" => Ok(Parser::ViaConjure),

34

            other => Err(format!(

35

                "unknown parser: {other}; expected one of: tree-sitter, via-conjure"

36

)),

37

38

14820

39

40

41

thread_local! {

42

    /// Thread-local setting for which parser is currently active.

43

///

44

    /// Must be explicitly set before use.

45

    static CURRENT_PARSER: Cell<Option<Parser>> = const { Cell::new(None) };

46

47

48

45110

pub fn set_current_parser(parser: Parser) {

49

45110

    CURRENT_PARSER.with(|current| current.set(Some(parser)));

50

45110

51

52

pub fn current_parser() -> Parser {

53

    CURRENT_PARSER.with(|current| {

54

        current.get().unwrap_or_else(|| {

55

            // loud failure on purpose, so we don't end up using the default

56

            bug!("current parser not set for this thread; call set_current_parser first")

57

})

58

})

59

60

61

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]

62

pub struct MorphConfig {

63

    pub cache: MorphCachingStrategy,

64

    pub prefilter: bool,

65

    /// Use naive (no-levels) traversal (`morph_naive`). Enabled with `levelsoff`, disabled with `levelson`.

66

    pub naive: bool,

67

    pub fixedpoint: bool,

68

69

70

impl Default for MorphConfig {

71

5770

    fn default() -> Self {

72

5770

        Self {

73

5770

            cache: MorphCachingStrategy::NoCache,

74

5770

            prefilter: false,

75

5770

            naive: true,

76

5770

            fixedpoint: false,

77

5770

78

5770

79

80

81

impl Display for MorphConfig {

82

44400

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

83

44400

        write!(f, "morph")?;

84

85

44400

        let mut features = Vec::new();

86

44400

        if !self.naive {

87

            features.push("levelson");

88

44400

89

44400

        match self.cache {

90

44400

            MorphCachingStrategy::NoCache => {}

91

            MorphCachingStrategy::Cache => features.push("cache"),

92

            MorphCachingStrategy::IncrementalCache => features.push("inccache"),

93

94

44400

        if self.prefilter {

95

            features.push("prefilteron");

96

44400

97

44400

        if self.fixedpoint {

98

            features.push("fixedpoint");

99

44400

100

101

44400

        if !features.is_empty() {

102

            write!(f, "-{}", features.join("-"))?;

103

44400

104

105

44400

        Ok(())

106

44400

107

108

109

#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]

110

pub enum MorphCachingStrategy {

111

    NoCache,

112

    Cache,

113

    #[default]

114

    IncrementalCache,

115

116

117

impl FromStr for MorphCachingStrategy {

118

    type Err = String;

119

120

    fn from_str(s: &str) -> Result<Self, Self::Err> {

121

        match s.trim().to_ascii_lowercase().as_str() {

122

            "no-cache" => Ok(Self::NoCache),

123

            "cache" => Ok(Self::Cache),

124

            "inc-cache" => Ok(Self::IncrementalCache),

125

            other => Err(format!(

126

                "unknown cache strategy: {other}; expected one of: no-cache, cahce, inc-cache"

127

)),

128

129

130

131

132

impl Display for MorphCachingStrategy {

133

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

134

        match self {

135

            MorphCachingStrategy::NoCache => write!(f, "nocache"),

136

            MorphCachingStrategy::Cache => write!(f, "cache"),

137

            MorphCachingStrategy::IncrementalCache => write!(f, "inccache"),

138

139

140

141

142

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]

143

pub enum Rewriter {

144

    Naive,

145

    Morph(MorphConfig),

146

147

148

thread_local! {

149

    /// Thread-local setting for which rewriter is currently active.

150

///

151

    /// Must be explicitly set before use.

152

    static CURRENT_REWRITER: Cell<Option<Rewriter>> = const { Cell::new(None) };

153

154

155

impl Display for Rewriter {

156

90130

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

157

90130

        match self {

158

45730

            Rewriter::Naive => write!(f, "naive"),

159

44400

            Rewriter::Morph(config) => write!(f, "{config}"),

160

161

90130

162

163

164

impl FromStr for Rewriter {

165

    type Err = String;

166

167

11840

    fn from_str(s: &str) -> Result<Self, Self::Err> {

168

11840

        let trimmed = s.trim().to_ascii_lowercase();

169

11840

        match trimmed.as_str() {

170

11840

            "naive" => Ok(Rewriter::Naive),

171

5770

            "morph" => Ok(Rewriter::Morph(MorphConfig::default())),

172

10

            other => {

173

10

                if !other.starts_with("morph-") {

174

                    return Err(format!(

175

                        "unknown rewriter: {other}; expected one of: naive, morph, morph-[levelson]-[cache|inccache]-[prefilteron]-[fixedpoint]"

176

));

177

10

178

179

10

                let parts = other.split('-').skip(1);

180

10

                Ok(Rewriter::Morph(parse_morph_config_tokens(parts)?))

181

182

183

11840

184

185

186

10

fn parse_morph_config_tokens<'a>(

187

10

    tokens: impl IntoIterator<Item = &'a str>,

188

10

) -> Result<MorphConfig, String> {

189

10

    let mut config = MorphConfig::default();

190

10

    let mut cache_set = false;

191

10

    let mut levels_set = false;

192

10

    let mut prefilter_set = false;

193

194

20

    for token in tokens {

195

20

        match token {

196

20

            "" => (),

197

20

            "levelson" => {

198

10

                if levels_set {

199

                    return Err(

200

                        "conflicting levels options: only one levels setting is allowed"

201

                            .to_string(),

202

);

203

10

204

10

                config.naive = false;

205

10

                levels_set = true;

206

207

10

            "cache" | "inccache" => {

208

                if cache_set {

209

                    return Err(

210

                        "conflicting cache options: only one of cache|inccache is allowed"

211

                            .to_string(),

212

);

213

214

                config.cache = match token {

215

                    "cache" => MorphCachingStrategy::Cache,

216

                    "inccache" => MorphCachingStrategy::IncrementalCache,

217

                    _ => unreachable!(),

218

};

219

                cache_set = true;

220

221

10

            "prefilteron" => {

222

                if prefilter_set {

223

                    return Err(

224

                        "conflicting prefilter options: only one prefilter setting is allowed"

225

                            .to_string(),

226

);

227

228

                config.prefilter = true;

229

                prefilter_set = true;

230

231

10

            "fixedpoint" => {

232

10

                config.fixedpoint = true;

233

10

234

            other_token => {

235

                return Err(format!(

236

                    "unknown morph option '{other_token}', must be one of levelson|cache|inccache|prefilteron|fixedpoint"

237

));

238

239

240

241

242

10

    Ok(config)

243

10

244

245

125494

pub fn set_current_rewriter(rewriter: Rewriter) {

246

125494

    CURRENT_REWRITER.with(|current| current.set(Some(rewriter)));

247

125494

248

249

35227

pub fn current_rewriter() -> Rewriter {

250

35227

    CURRENT_REWRITER.with(|current| {

251

35227

        current.get().unwrap_or_else(|| {

252

            // loud failure on purpose, so we don't end up using the default

253

            bug!("current rewriter not set for this thread; call set_current_rewriter first")

254

})

255

35227

})

256

35227

257

258

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]

259

pub enum QuantifiedExpander {

260

    Native,

261

    ViaSolver,

262

    ViaSolverAc,

263

264

265

impl Display for QuantifiedExpander {

266

90142

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

267

90142

        match self {

268

9942

            QuantifiedExpander::Native => write!(f, "native"),

269

8640

            QuantifiedExpander::ViaSolver => write!(f, "via-solver"),

270

71560

            QuantifiedExpander::ViaSolverAc => write!(f, "via-solver-ac"),

271

272

90142

273

274

275

impl FromStr for QuantifiedExpander {

276

    type Err = String;

277

278

6920

    fn from_str(s: &str) -> Result<Self, Self::Err> {

279

6920

        match s.trim().to_ascii_lowercase().as_str() {

280

6920

            "native" => Ok(QuantifiedExpander::Native),

281

6066

            "via-solver" => Ok(QuantifiedExpander::ViaSolver),

282

5566

            "via-solver-ac" => Ok(QuantifiedExpander::ViaSolverAc),

283

            _ => Err(format!(

284

                "unknown comprehension expander: {s}; expected one of: \

285

                 native, via-solver, via-solver-ac"

286

)),

287

288

6920

289

290

291

thread_local! {

292

    /// Thread-local setting for which comprehension expansion strategy is currently active.

293

///

294

    /// Must be explicitly set before use.

295

    static COMPREHENSION_EXPANDER: Cell<Option<QuantifiedExpander>> = const { Cell::new(None) };

296

297

298

45188

pub fn set_comprehension_expander(expander: QuantifiedExpander) {

299

45188

    COMPREHENSION_EXPANDER.with(|current| current.set(Some(expander)));

300

45188

301

302

3268500

pub fn comprehension_expander() -> QuantifiedExpander {

303

3268500

    COMPREHENSION_EXPANDER.with(|current| {

304

3268500

        current.get().unwrap_or_else(|| {

305

            // loud failure on purpose, so we don't end up using the default

306

            bug!(

307

                "comprehension expander not set for this thread; call set_comprehension_expander first"

308

309

})

310

3268500

})

311

3268500

312

313

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Default, Serialize, Deserialize, JsonSchema)]

314

pub enum SatEncoding {

315

    #[default]

316

    Log,

317

    Direct,

318

    Order,

319

320

321

impl SatEncoding {

322

96720

    pub const fn as_str(self) -> &'static str {

323

96720

        match self {

324

34080

            SatEncoding::Log => "log",

325

44440

            SatEncoding::Direct => "direct",

326

18200

            SatEncoding::Order => "order",

327

328

96720

329

330

13800

    pub const fn as_rule_set(self) -> &'static str {

331

13800

        match self {

332

4860

            SatEncoding::Log => "SAT_Log",

333

6340

            SatEncoding::Direct => "SAT_Direct",

334

2600

            SatEncoding::Order => "SAT_Order",

335

336

13800

337

338

339

impl Display for SatEncoding {

340

    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

341

        match self {

342

            SatEncoding::Log => write!(f, "log"),

343

            SatEncoding::Direct => write!(f, "direct"),

344

            SatEncoding::Order => write!(f, "order"),

345

346

347

348

349

impl FromStr for SatEncoding {

350

    type Err = String;

351

352

    fn from_str(s: &str) -> Result<Self, Self::Err> {

353

        match s.trim().to_ascii_lowercase().as_str() {

354

            "log" => Ok(SatEncoding::Log),

355

            "direct" => Ok(SatEncoding::Direct),

356

            "order" => Ok(SatEncoding::Order),

357

            other => Err(format!(

358

                "unknown sat-encoding: {other}; expected one of: log, direct, order"

359

)),

360

361

362

363

364

#[derive(

365

    Debug,

366

    EnumIter,

367

    StrumDisplay,

368

    PartialEq,

369

Eq,

370

    Hash,

371

    Clone,

372

    Copy,

373

    Serialize,

374

    Deserialize,

375

    JsonSchema,

376

)]

377

pub enum SolverFamily {

378

    Minion,

379

    Sat(SatEncoding),

380

    Smt(TheoryConfig),

381

382

383

thread_local! {

384

    /// Thread-local setting for which solver family is currently active.

385

///

386

    /// Must be explicitly set before use.

387

    static CURRENT_SOLVER_FAMILY: Cell<Option<SolverFamily>> = const { Cell::new(None) };

388

389

390

pub const DEFAULT_MINION_DISCRETE_THRESHOLD: usize = 10;

391

392

thread_local! {

393

    /// Thread-local setting controlling when Minion int domains are emitted as `DISCRETE`.

394

///

395

    /// If an int domain size is <= this threshold, the Minion adaptor uses `DISCRETE`; otherwise

396

    /// it uses `BOUND`, unless another constraint requires `DISCRETE`.

397

    static MINION_DISCRETE_THRESHOLD: Cell<usize> =

398

        const { Cell::new(DEFAULT_MINION_DISCRETE_THRESHOLD) };

399

400

    /// Thread-local setting controlling whether rule-trace outputs are active in this phase.

401

///

402

    /// This is intentionally off by default and can be disabled before solver-time rewrites so

403

    /// follow-up dominance-blocking rewrites do not pollute the initial rewrite trace.

404

    static RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

405

406

    /// Thread-local setting controlling whether default rule traces are configured.

407

    static DEFAULT_RULE_TRACE_ENABLED: Cell<bool> = const { Cell::new(false) };

408

409

    /// Thread-local setting controlling whether verbose rule-attempt traces are configured.

410

    static RULE_TRACE_VERBOSE_ENABLED: Cell<bool> = const { Cell::new(false) };

411

412

    /// Thread-local setting controlling whether aggregate rule-application traces are configured.

413

    static RULE_TRACE_AGGREGATES_ENABLED: Cell<bool> = const { Cell::new(false) };

414

415

416

45110

pub fn set_current_solver_family(solver_family: SolverFamily) {

417

45110

    CURRENT_SOLVER_FAMILY.with(|current| current.set(Some(solver_family)));

418

45110

419

420

pub fn current_solver_family() -> SolverFamily {

421

    CURRENT_SOLVER_FAMILY.with(|current| {

422

        current.get().unwrap_or_else(|| {

423

            // loud failure on purpose, so we don't end up using the default

424

            bug!(

425

                "current solver family not set for this thread; call set_current_solver_family first"

426

427

})

428

})

429

430

431

45110

pub fn set_minion_discrete_threshold(threshold: usize) {

432

45110

    MINION_DISCRETE_THRESHOLD.with(|current| current.set(threshold));

433

45110

434

435

196766

pub fn minion_discrete_threshold() -> usize {

436

196766

    MINION_DISCRETE_THRESHOLD.with(|current| current.get())

437

196766

438

439

90160

pub fn set_rule_trace_enabled(enabled: bool) {

440

90160

    RULE_TRACE_ENABLED.with(|current| current.set(enabled));

441

90160

442

443

347169067

pub fn rule_trace_enabled() -> bool {

444

347169067

    RULE_TRACE_ENABLED.with(|current| current.get())

445

347169067

446

447

45110

pub fn set_default_rule_trace_enabled(enabled: bool) {

448

45110

    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.set(enabled));

449

45110

450

451

656900

pub fn default_rule_trace_enabled() -> bool {

452

656900

    DEFAULT_RULE_TRACE_ENABLED.with(|current| current.get())

453

656900

454

455

45110

pub fn set_rule_trace_verbose_enabled(enabled: bool) {

456

45110

    RULE_TRACE_VERBOSE_ENABLED.with(|current| current.set(enabled));

457

45110

458

459

338012026

pub fn rule_trace_verbose_enabled() -> bool {

460

338012026

    RULE_TRACE_VERBOSE_ENABLED.with(|current| current.get())

461

338012026

462

463

45110

pub fn set_rule_trace_aggregates_enabled(enabled: bool) {

464

45110

    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.set(enabled));

465

45110

466

467

604808

pub fn rule_trace_aggregates_enabled() -> bool {

468

604808

    RULE_TRACE_AGGREGATES_ENABLED.with(|current| current.get())

469

604808

470

471

pub fn configured_rule_trace_enabled() -> bool {

472

    default_rule_trace_enabled() || rule_trace_verbose_enabled() || rule_trace_aggregates_enabled()

473

474

475

impl FromStr for SolverFamily {

476

    type Err = String;

477

478

10480

    fn from_str(s: &str) -> Result<Self, Self::Err> {

479

10480

        let s = s.trim().to_ascii_lowercase();

480

481

10480

        match s.as_str() {

482

10480

            "minion" => Ok(SolverFamily::Minion),

483

5330

            "sat" | "sat-log" => Ok(SolverFamily::Sat(SatEncoding::Log)),

484

4210

            "sat-direct" => Ok(SolverFamily::Sat(SatEncoding::Direct)),

485

2650

            "sat-order" => Ok(SolverFamily::Sat(SatEncoding::Order)),

486

2030

            "smt" => Ok(SolverFamily::Smt(TheoryConfig::default())),

487

2030

            other => {

488

                // allow forms like `smt-bv-atomic` or `smt-lia-arrays`

489

2030

                if other.starts_with("smt-") {

490

2030

                    let parts = other.split('-').skip(1);

491

2030

                    let mut ints = IntTheory::default();

492

2030

                    let mut matrices = MatrixTheory::default();

493

2030

                    let mut unwrap_alldiff = false;

494

495

4620

                    for token in parts {

496

4620

                        match token {

497

4620

                            "" => {}

498

4620

                            "lia" => ints = IntTheory::Lia,

499

2990

                            "bv" => ints = IntTheory::Bv,

500

2590

                            "arrays" => matrices = MatrixTheory::Arrays,

501

1120

                            "atomic" => matrices = MatrixTheory::Atomic,

502

560

                            "nodiscrete" => unwrap_alldiff = true,

503

                            other_token => {

504

                                return Err(format!(

505

                                    "unknown SMT theory option '{other_token}', must be one of bv|lia|arrays|atomic|nodiscrete"

506

));

507

508

509

510

511

2030

                    return Ok(SolverFamily::Smt(TheoryConfig {

512

2030

                        ints,

513

2030

                        matrices,

514

2030

                        unwrap_alldiff,

515

2030

                    }));

516

517

                Err(format!(

518

                    "unknown solver family '{other}', expected one of: minion, sat-log, sat-direct, sat-order, smt[(bv|lia)-(arrays|atomic)][-nodiscrete]"

519

))

520

521

522

10480

523

524

525

impl SolverFamily {

526

315760

    pub fn as_str(&self) -> String {

527

315760

        match self {

528

152280

            SolverFamily::Minion => "minion".to_owned(),

529

96720

            SolverFamily::Sat(encoding) => format!("sat-{}", encoding.as_str()),

530

66760

            SolverFamily::Smt(theory_config) => format!("smt-{}", theory_config.as_str()),

531

532

315760

533

534

535

#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]

536

pub struct SolverArgs {

537

    pub timeout_ms: Option<u64>,

538