Skip to content

Commit aad6aa5

Browse files
committed
Slight code cleanup, additional tests for more panics being tested
1 parent b97ed58 commit aad6aa5

File tree

2 files changed

+182
-37
lines changed

2 files changed

+182
-37
lines changed

chalk-engine/src/logic.rs

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -221,9 +221,7 @@ impl<C: Context> Forest<C> {
221221
self.tables.next_index(),
222222
goal
223223
);
224-
let coinductive_goal = context.is_coinductive(&goal);
225-
let mut table = Table::new(goal.clone(), coinductive_goal);
226-
Self::push_initial_strands(context, self.tables.next_index(), &mut table);
224+
let table = Self::build_table(context, self.tables.next_index(), goal);
227225
self.tables.insert(table)
228226
}
229227

@@ -238,12 +236,13 @@ impl<C: Context> Forest<C> {
238236
/// In terms of the NFTD paper, this corresponds to the *Program
239237
/// Clause Resolution* step being applied eagerly, as many times
240238
/// as possible.
241-
fn push_initial_strands(
239+
fn build_table(
242240
context: &impl ContextOps<C>,
243241
table_idx: TableIndex,
244-
table: &mut Table<C>,
245-
) {
242+
goal: C::UCanonicalGoalInEnvironment,
243+
) -> Table<C> {
246244
// Instantiate the table goal with fresh inference variables.
245+
let table = Table::<C>::new(goal.clone(), context.is_coinductive(&goal));
247246
let table_goal = table.table_goal.clone();
248247
let (infer, subst, environment, goal) = context.instantiate_ucanonical_goal(&table_goal);
249248
Self::push_initial_strands_instantiated(
@@ -254,18 +253,18 @@ impl<C: Context> Forest<C> {
254253
subst,
255254
environment,
256255
goal,
257-
);
256+
)
258257
}
259258

260259
fn push_initial_strands_instantiated(
261260
context: &impl ContextOps<C>,
262261
table_idx: TableIndex,
263-
table: &mut Table<C>,
262+
mut table: Table<C>,
264263
mut infer: C::InferenceTable,
265264
subst: C::Substitution,
266265
environment: C::Environment,
267266
goal: C::Goal,
268-
) {
267+
) -> Table<C> {
269268
match context.into_hh_goal(goal) {
270269
HhGoal::DomainGoal(domain_goal) => {
271270
match context.program_clauses(&environment, &domain_goal, &mut infer) {
@@ -326,6 +325,8 @@ impl<C: Context> Forest<C> {
326325
}
327326
}
328327
}
328+
329+
table
329330
}
330331

331332
/// Given a selected positive subgoal, applies the subgoal

tests/integration/panic.rs

Lines changed: 172 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -4,26 +4,53 @@ use chalk_rust_ir::*;
44
use chalk_solve::{RustIrDatabase, SolverChoice};
55
use std::sync::Arc;
66

7+
#[derive(Debug)]
8+
enum PanickingMethod {
9+
NoPanic,
10+
CustomClauses,
11+
TraitDatum,
12+
ImplDatum,
13+
ImplsForTrait,
14+
ProgramClausesForEnv,
15+
Interner,
16+
}
17+
18+
impl Default for PanickingMethod {
19+
fn default() -> Self {
20+
Self::NoPanic
21+
}
22+
}
23+
724
#[derive(Debug, Default)]
825
struct MockDatabase {
9-
panic: bool,
26+
panicking_method: PanickingMethod,
1027
}
1128

29+
/// This DB is representint lowered program:
30+
///
31+
/// struct Foo { }
32+
/// trait Bar { }
33+
/// impl Bar for Foo { }
1234
#[allow(unused_variables)]
1335
impl RustIrDatabase<ChalkIr> for MockDatabase {
1436
fn custom_clauses(&self) -> Vec<ProgramClause<ChalkIr>> {
15-
if self.panic {
16-
panic!("test panic");
17-
} else {
18-
vec![]
37+
if let PanickingMethod::CustomClauses = self.panicking_method {
38+
panic!("custom_clauses panic");
1939
}
40+
41+
vec![]
2042
}
2143

2244
fn associated_ty_data(&self, ty: AssocTypeId<ChalkIr>) -> Arc<AssociatedTyDatum<ChalkIr>> {
2345
unimplemented!()
2446
}
2547

48+
// `trait Bar`, id `0`
2649
fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
50+
if let PanickingMethod::TraitDatum = self.panicking_method {
51+
panic!("trait_datum panic");
52+
}
53+
2754
assert_eq!(id.0.index, 0);
2855
Arc::new(chalk_rust_ir::TraitDatum {
2956
id,
@@ -46,7 +73,12 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
4673
})
4774
}
4875

76+
// `impl Bar for Foo`, id `1`
4977
fn impl_datum(&self, id: ImplId<ChalkIr>) -> Arc<ImplDatum<ChalkIr>> {
78+
if let PanickingMethod::ImplDatum = self.panicking_method {
79+
panic!("impl_datum panic");
80+
}
81+
5082
assert_eq!(id.0.index, 1);
5183

5284
let substitution = Ty::new(
@@ -95,11 +127,16 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
95127
unimplemented!()
96128
}
97129

130+
// All `Bar` impls
98131
fn impls_for_trait(
99132
&self,
100133
trait_id: TraitId<ChalkIr>,
101134
parameters: &[GenericArg<ChalkIr>],
102135
) -> Vec<ImplId<ChalkIr>> {
136+
if let PanickingMethod::ImplsForTrait = self.panicking_method {
137+
panic!("impls_for_trait panic");
138+
}
139+
103140
assert_eq!(trait_id.0.index, 0);
104141
vec![ImplId(RawId { index: 1 })]
105142
}
@@ -124,10 +161,18 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
124161
&self,
125162
environment: &Environment<ChalkIr>,
126163
) -> ProgramClauses<ChalkIr> {
164+
if let PanickingMethod::ProgramClausesForEnv = self.panicking_method {
165+
panic!("program_clauses_for_env panic")
166+
}
167+
127168
ProgramClauses::new(&ChalkIr)
128169
}
129170

130171
fn interner(&self) -> &ChalkIr {
172+
if let PanickingMethod::Interner = self.panicking_method {
173+
panic!("interner panic")
174+
}
175+
131176
&ChalkIr
132177
}
133178

@@ -136,29 +181,14 @@ impl RustIrDatabase<ChalkIr> for MockDatabase {
136181
}
137182
}
138183

139-
#[test]
140-
fn unwind_safety() {
141-
use self::MockDatabase;
142-
use chalk_integration::interner::{self, ChalkIr};
184+
fn prepare_goal() -> UCanonical<InEnvironment<Goal<ChalkIr>>> {
185+
use chalk_integration::interner;
143186
use chalk_ir::*;
144-
use std::panic;
145-
146-
// lower program
147-
/*
148-
let mut db = lower_program_with_db! {
149-
program {
150-
struct Foo { }
151-
trait Bar { }
152-
impl Bar for Foo { }
153-
}
154-
database MockDatabase
155-
};
156187

157-
let program = db.chalk_db.checked_program().unwrap();
158-
*/
159-
let mut db = MockDatabase { panic: false };
160-
161-
let peeled_goal: UCanonical<InEnvironment<Goal<ChalkIr>>> = UCanonical {
188+
// Goal:
189+
//
190+
// Foo: Bar
191+
UCanonical {
162192
canonical: Canonical {
163193
binders: CanonicalVarKinds::new(&ChalkIr),
164194
value: InEnvironment {
@@ -180,17 +210,131 @@ fn unwind_safety() {
180210
},
181211
},
182212
universes: 1,
213+
}
214+
}
215+
216+
#[test]
217+
fn custom_clauses_panics() {
218+
use std::panic;
219+
220+
let peeled_goal = prepare_goal();
221+
let mut solver = SolverChoice::slg_default().into_solver();
222+
223+
// solve goal but this will panic
224+
let mut db = MockDatabase {
225+
panicking_method: PanickingMethod::CustomClauses,
226+
};
227+
let result = panic::catch_unwind(panic::AssertUnwindSafe(|| {
228+
solver.solve(&db, &peeled_goal);
229+
}));
230+
assert!(result.is_err());
231+
232+
// solve again but without panicking this time
233+
db.panicking_method = PanickingMethod::NoPanic;
234+
assert!(solver.solve(&db, &peeled_goal).is_some());
235+
}
236+
237+
#[test]
238+
fn trait_datum_panics() {
239+
use std::panic;
240+
241+
let peeled_goal = prepare_goal();
242+
let mut solver = SolverChoice::slg_default().into_solver();
243+
244+
// solve goal but this will panic
245+
let mut db = MockDatabase {
246+
panicking_method: PanickingMethod::TraitDatum,
247+
};
248+
let result = panic::catch_unwind(panic::AssertUnwindSafe(|| {
249+
solver.solve(&db, &peeled_goal);
250+
}));
251+
assert!(result.is_err());
252+
253+
// solve again but without panicking this time
254+
db.panicking_method = PanickingMethod::NoPanic;
255+
assert!(solver.solve(&db, &peeled_goal).is_some());
256+
}
257+
258+
#[test]
259+
fn impl_datum_panics() {
260+
use std::panic;
261+
262+
let peeled_goal = prepare_goal();
263+
let mut solver = SolverChoice::slg_default().into_solver();
264+
265+
// solve goal but this will panic
266+
let mut db = MockDatabase {
267+
panicking_method: PanickingMethod::ImplDatum,
268+
};
269+
let result = panic::catch_unwind(panic::AssertUnwindSafe(|| {
270+
solver.solve(&db, &peeled_goal);
271+
}));
272+
assert!(result.is_err());
273+
274+
// solve again but without panicking this time
275+
db.panicking_method = PanickingMethod::NoPanic;
276+
assert!(solver.solve(&db, &peeled_goal).is_some());
277+
}
278+
279+
#[test]
280+
fn impls_for_trait() {
281+
use std::panic;
282+
283+
let peeled_goal = prepare_goal();
284+
let mut solver = SolverChoice::slg_default().into_solver();
285+
286+
// solve goal but this will panic
287+
let mut db = MockDatabase {
288+
panicking_method: PanickingMethod::ImplsForTrait,
289+
};
290+
let result = panic::catch_unwind(panic::AssertUnwindSafe(|| {
291+
solver.solve(&db, &peeled_goal);
292+
}));
293+
assert!(result.is_err());
294+
295+
// solve again but without panicking this time
296+
db.panicking_method = PanickingMethod::NoPanic;
297+
assert!(solver.solve(&db, &peeled_goal).is_some());
298+
}
299+
300+
#[test]
301+
fn program_clauses_for_env() {
302+
use std::panic;
303+
304+
let peeled_goal = prepare_goal();
305+
let mut solver = SolverChoice::slg_default().into_solver();
306+
307+
// solve goal but this will panic
308+
let mut db = MockDatabase {
309+
panicking_method: PanickingMethod::ProgramClausesForEnv,
183310
};
311+
let result = panic::catch_unwind(panic::AssertUnwindSafe(|| {
312+
solver.solve(&db, &peeled_goal);
313+
}));
314+
assert!(result.is_err());
184315

316+
// solve again but without panicking this time
317+
db.panicking_method = PanickingMethod::NoPanic;
318+
assert!(solver.solve(&db, &peeled_goal).is_some());
319+
}
320+
321+
#[test]
322+
fn interner() {
323+
use std::panic;
324+
325+
let peeled_goal = prepare_goal();
185326
let mut solver = SolverChoice::slg_default().into_solver();
327+
186328
// solve goal but this will panic
187-
db.panic = true;
329+
let mut db = MockDatabase {
330+
panicking_method: PanickingMethod::Interner,
331+
};
188332
let result = panic::catch_unwind(panic::AssertUnwindSafe(|| {
189333
solver.solve(&db, &peeled_goal);
190334
}));
191335
assert!(result.is_err());
192336

193337
// solve again but without panicking this time
194-
db.panic = false;
338+
db.panicking_method = PanickingMethod::NoPanic;
195339
assert!(solver.solve(&db, &peeled_goal).is_some());
196340
}

0 commit comments

Comments
 (0)