Skip to content

Commit a05bf1e

Browse files
zhassan-awstedinski
authored andcommitted
Do not create a ProjectedPlace for unsupported fields (rust-lang#1071)
1 parent a484fa9 commit a05bf1e

File tree

1 file changed

+33
-18
lines changed
  • src/kani-compiler/src/codegen_cprover_gotoc/codegen

1 file changed

+33
-18
lines changed

src/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

Lines changed: 33 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,17 @@ pub struct UnimplementedData {
3939
pub loc: Location,
4040
}
4141

42+
impl UnimplementedData {
43+
pub fn new(operation: &str, bug_url: &str, goto_type: Type, loc: Location) -> Self {
44+
UnimplementedData {
45+
operation: operation.to_string(),
46+
bug_url: bug_url.to_string(),
47+
goto_type,
48+
loc,
49+
}
50+
}
51+
}
52+
4253
/// Relevent information about a projected place (i.e. an lvalue).
4354
#[derive(Debug)]
4455
pub struct ProjectedPlace<'tcx> {
@@ -193,7 +204,12 @@ impl<'tcx> TypeOrVariant<'tcx> {
193204
}
194205

195206
impl<'tcx> GotocCtx<'tcx> {
196-
fn codegen_field(&mut self, res: Expr, t: TypeOrVariant<'tcx>, f: &Field) -> Expr {
207+
fn codegen_field(
208+
&mut self,
209+
res: Expr,
210+
t: TypeOrVariant<'tcx>,
211+
f: &Field,
212+
) -> Result<Expr, UnimplementedData> {
197213
match t {
198214
TypeOrVariant::Type(t) => {
199215
match t.kind() {
@@ -216,7 +232,7 @@ impl<'tcx> GotocCtx<'tcx> {
216232
| ty::Infer(_)
217233
| ty::Error(_) => unreachable!("type {:?} does not have a field", t),
218234
ty::Tuple(_) => {
219-
res.member(&Self::tuple_fld_name(f.index()), &self.symbol_table)
235+
Ok(res.member(&Self::tuple_fld_name(f.index()), &self.symbol_table))
220236
}
221237
ty::Adt(def, _) if def.repr().simd() => {
222238
// this is a SIMD vector - the index represents one
@@ -229,27 +245,27 @@ impl<'tcx> GotocCtx<'tcx> {
229245
// assert!(v.1 == 2);
230246
// }
231247
let size_index = Expr::int_constant(f.index(), Type::size_t());
232-
res.index_array(size_index)
248+
Ok(res.index_array(size_index))
233249
}
234250
// if we fall here, then we are handling either a struct or a union
235251
ty::Adt(def, _) => {
236252
let field = &def.variants().raw[0].fields[f.index()];
237-
res.member(&field.name.to_string(), &self.symbol_table)
253+
Ok(res.member(&field.name.to_string(), &self.symbol_table))
238254
}
239-
ty::Closure(..) => res.member(&f.index().to_string(), &self.symbol_table),
240-
ty::Generator(..) => self.codegen_unimplemented(
255+
ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)),
256+
ty::Generator(..) => Err(UnimplementedData::new(
241257
"ty::Generator",
242-
Type::code(vec![], Type::empty()),
243-
res.location().clone(),
244258
"https://github.com/model-checking/kani/issues/416",
245-
),
259+
Type::code(vec![], Type::empty()),
260+
*res.location(),
261+
)),
246262
_ => unimplemented!(),
247263
}
248264
}
249265
// if we fall here, then we are handling an enum
250266
TypeOrVariant::Variant(v) => {
251267
let field = &v.fields[f.index()];
252-
res.member(&field.name.to_string(), &self.symbol_table)
268+
Ok(res.member(&field.name.to_string(), &self.symbol_table))
253269
}
254270
}
255271
}
@@ -375,7 +391,7 @@ impl<'tcx> GotocCtx<'tcx> {
375391
}
376392
ProjectionElem::Field(f, t) => {
377393
let typ = TypeOrVariant::Type(t);
378-
let expr = self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f);
394+
let expr = self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f)?;
379395
Ok(ProjectedPlace::new(
380396
expr,
381397
typ,
@@ -424,13 +440,12 @@ impl<'tcx> GotocCtx<'tcx> {
424440
let typ = self.tcx.mk_array(*ty, subarray_len);
425441
let goto_typ = self.codegen_ty(typ);
426442
// unimplemented
427-
Err(UnimplementedData {
428-
operation: "Sub-array binding".to_string(),
429-
bug_url: "https://github.com/model-checking/kani/issues/707"
430-
.to_string(),
431-
goto_type: goto_typ,
432-
loc: *before.goto_expr.location(),
433-
})
443+
Err(UnimplementedData::new(
444+
"Sub-array binding",
445+
"https://github.com/model-checking/kani/issues/707",
446+
goto_typ,
447+
*before.goto_expr.location(),
448+
))
434449
}
435450
ty::Slice(elemt) => {
436451
let len = if from_end {

0 commit comments

Comments
 (0)