Skip to content

Commit 6b87bc7

Browse files
zhassan-awstedinski
zhassan-aws
authored and
tedinski
committed
Wrap returned value from codegen_place in a Result to account for the possibility of an error due to unsupported operations (rust-lang#1057)
1 parent 0a7661c commit 6b87bc7

File tree

5 files changed

+149
-61
lines changed

5 files changed

+149
-61
lines changed

‎src/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
44
use crate::codegen_cprover_gotoc::GotocCtx;
5+
use crate::unwrap_or_return_codegen_unimplemented;
56
use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
67
use cbmc::NO_PRETTY_NAME;
78
use rustc_ast::ast::Mutability;
@@ -27,7 +28,8 @@ impl<'tcx> GotocCtx<'tcx> {
2728
Operand::Copy(d) | Operand::Move(d) =>
2829
// TODO: move shouldn't be the same as copy
2930
{
30-
let projection = self.codegen_place(d);
31+
let projection =
32+
unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(d));
3133
// If the operand itself is a Dynamic (like when passing a boxed closure),
3234
// we need to pull off the fat pointer. In that case, the rustc kind() on
3335
// both the operand and the inner type are Dynamic.

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

Lines changed: 71 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
use super::typ::TypeExt;
99
use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
1010
use crate::codegen_cprover_gotoc::GotocCtx;
11-
use cbmc::goto_program::{Expr, Type};
11+
use cbmc::goto_program::{Expr, Location, Type};
1212
use rustc_hir::Mutability;
1313
use rustc_middle::ty::layout::LayoutOf;
1414
use rustc_middle::{
@@ -26,6 +26,19 @@ pub enum TypeOrVariant<'tcx> {
2626
Variant(&'tcx VariantDef),
2727
}
2828

29+
/// A struct for storing the data for passing to `codegen_unimplemented`
30+
#[derive(Debug)]
31+
pub struct UnimplementedData {
32+
/// The specific operation that is not supported
33+
pub operation: String,
34+
/// URL for issue on Kani github page
35+
pub bug_url: String,
36+
/// The resulting goto type of the operation
37+
pub goto_type: Type,
38+
/// Location of operation
39+
pub loc: Location,
40+
}
41+
2942
/// Relevent information about a projected place (i.e. an lvalue).
3043
#[derive(Debug)]
3144
pub struct ProjectedPlace<'tcx> {
@@ -290,9 +303,10 @@ impl<'tcx> GotocCtx<'tcx> {
290303
/// the return value is the expression after.
291304
fn codegen_projection(
292305
&mut self,
293-
before: ProjectedPlace<'tcx>,
306+
before: Result<ProjectedPlace<'tcx>, UnimplementedData>,
294307
proj: ProjectionElem<Local, Ty<'tcx>>,
295-
) -> ProjectedPlace<'tcx> {
308+
) -> Result<ProjectedPlace<'tcx>, UnimplementedData> {
309+
let before = before?;
296310
match proj {
297311
ProjectionElem::Deref => {
298312
let base_type = before.mir_typ();
@@ -360,18 +374,18 @@ impl<'tcx> GotocCtx<'tcx> {
360374
_ => inner_goto_expr.dereference(),
361375
};
362376
let typ = TypeOrVariant::Type(inner_mir_typ);
363-
ProjectedPlace::new(expr, typ, fat_ptr_goto_expr, fat_ptr_mir_typ, self)
377+
Ok(ProjectedPlace::new(expr, typ, fat_ptr_goto_expr, fat_ptr_mir_typ, self))
364378
}
365379
ProjectionElem::Field(f, t) => {
366380
let typ = TypeOrVariant::Type(t);
367381
let expr = self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f);
368-
ProjectedPlace::new(
382+
Ok(ProjectedPlace::new(
369383
expr,
370384
typ,
371385
before.fat_ptr_goto_expr,
372386
before.fat_ptr_mir_typ,
373387
self,
374-
)
388+
))
375389
}
376390
ProjectionElem::Index(i) => {
377391
let base_type = before.mir_typ();
@@ -385,21 +399,20 @@ impl<'tcx> GotocCtx<'tcx> {
385399
ty::Slice(..) => before.goto_expr.index(idxe),
386400
_ => unreachable!("must index an array"),
387401
};
388-
ProjectedPlace::new(
402+
Ok(ProjectedPlace::new(
389403
expr,
390404
typ,
391405
before.fat_ptr_goto_expr,
392406
before.fat_ptr_mir_typ,
393407
self,
394-
)
408+
))
395409
}
396410
ProjectionElem::ConstantIndex { offset, min_length, from_end } => {
397-
self.codegen_constant_index(before, offset, min_length, from_end)
411+
Ok(self.codegen_constant_index(before, offset, min_length, from_end))
398412
}
399413
// Best effort to codegen subslice projection.
400-
// This is known to fail with a CBMC invariant violation
401-
// in some cases. Full support to be added in
402-
// https://github.com/model-checking/kani/issues/357
414+
// Full support to be added in
415+
// https://github.com/model-checking/kani/issues/707
403416
ProjectionElem::Subslice { from, to, from_end } => {
404417
// https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
405418
match before.mir_typ().kind() {
@@ -425,13 +438,13 @@ impl<'tcx> GotocCtx<'tcx> {
425438
let from_elem = before.goto_expr.index(index);
426439
let data = from_elem.address_of();
427440
let fat_ptr = slice_fat_ptr(goto_type, data, len, &self.symbol_table);
428-
ProjectedPlace::new(
441+
Ok(ProjectedPlace::new(
429442
fat_ptr.clone(),
430443
TypeOrVariant::Type(ptr_typ),
431444
Some(fat_ptr),
432445
Some(ptr_typ),
433446
self,
434-
)
447+
))
435448
}
436449
_ => unreachable!("must be array or slice"),
437450
}
@@ -456,13 +469,13 @@ impl<'tcx> GotocCtx<'tcx> {
456469
TagEncoding::Niche { .. } => before.goto_expr,
457470
},
458471
};
459-
ProjectedPlace::new(
472+
Ok(ProjectedPlace::new(
460473
expr,
461474
typ,
462475
before.fat_ptr_goto_expr,
463476
before.fat_ptr_mir_typ,
464477
self,
465-
)
478+
))
466479
}
467480
_ => unreachable!("it's a bug to reach here!"),
468481
}
@@ -476,15 +489,18 @@ impl<'tcx> GotocCtx<'tcx> {
476489
/// This function follows the MIR projection to get the final useable lvalue.
477490
/// If it passes through a fat pointer along the way, it stores info about it,
478491
/// which can be useful in reconstructing fat pointer operations.
479-
pub fn codegen_place(&mut self, p: &Place<'tcx>) -> ProjectedPlace<'tcx> {
492+
pub fn codegen_place(
493+
&mut self,
494+
p: &Place<'tcx>,
495+
) -> Result<ProjectedPlace<'tcx>, UnimplementedData> {
480496
debug!(place=?p, "codegen_place");
481497
let initial_expr = self.codegen_local(p.local);
482498
let initial_typ = TypeOrVariant::Type(self.local_ty(p.local));
483499
debug!(?initial_typ, ?initial_expr, "codegen_place");
484500
let initial_projection = ProjectedPlace::new(initial_expr, initial_typ, None, None, self);
485501
p.projection
486502
.iter()
487-
.fold(initial_projection, |accum, proj| self.codegen_projection(accum, proj))
503+
.fold(Ok(initial_projection), |accum, proj| self.codegen_projection(accum, proj))
488504
}
489505

490506
// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html
@@ -550,3 +566,40 @@ impl<'tcx> GotocCtx<'tcx> {
550566
arr.member("0", &self.symbol_table).index_array(idx)
551567
}
552568
}
569+
570+
/// A convenience macro that unwraps a `Result<ProjectPlace<'tcx>,
571+
/// Err<UnimplementedData>` if it is `Ok` and returns an `codegen_unimplemented`
572+
/// expression otherwise.
573+
/// Note that this macro affects the control flow since it calls `return`
574+
#[macro_export]
575+
macro_rules! unwrap_or_return_codegen_unimplemented {
576+
($ctx:expr, $pp_result:expr) => {{
577+
if let Err(err) = $pp_result {
578+
return $ctx.codegen_unimplemented(
579+
err.operation.as_str(),
580+
err.goto_type,
581+
err.loc,
582+
err.bug_url.as_str(),
583+
);
584+
}
585+
$pp_result.unwrap()
586+
}};
587+
}
588+
589+
/// Same as the above macro, but returns a goto program `Stmt` instead
590+
#[macro_export]
591+
macro_rules! unwrap_or_return_codegen_unimplemented_stmt {
592+
($ctx:expr, $pp_result:expr) => {{
593+
if let Err(err) = $pp_result {
594+
return $ctx
595+
.codegen_unimplemented(
596+
err.operation.as_str(),
597+
err.goto_type,
598+
err.loc,
599+
err.bug_url.as_str(),
600+
)
601+
.as_stmt(err.loc);
602+
}
603+
$pp_result.unwrap()
604+
}};
605+
}

‎src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
use super::typ::{is_pointer, pointee_type, TypeExt};
44
use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
55
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
6+
use crate::unwrap_or_return_codegen_unimplemented;
67
use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
78
use cbmc::utils::BUG_REPORT_URL;
89
use cbmc::MachineModel;
@@ -81,7 +82,7 @@ impl<'tcx> GotocCtx<'tcx> {
8182
/// Given a mir object denoted by a mir place, codegen a pointer to this object.
8283
pub fn codegen_rvalue_ref(&mut self, place: &Place<'tcx>, result_mir_type: Ty<'tcx>) -> Expr {
8384
let place_mir_type = self.place_ty(place);
84-
let projection = self.codegen_place(place);
85+
let projection = unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(place));
8586

8687
debug!("codegen_rvalue_ref: place: {:?}", place);
8788
debug!("codegen_rvalue_ref: place type: {:?}", place_mir_type);
@@ -203,9 +204,10 @@ impl<'tcx> GotocCtx<'tcx> {
203204
let pt = self.place_ty(p);
204205
match pt.kind() {
205206
ty::Array(_, sz) => self.codegen_const(*sz, None),
206-
ty::Slice(_) => {
207-
self.codegen_place(p).fat_ptr_goto_expr.unwrap().member("len", &self.symbol_table)
208-
}
207+
ty::Slice(_) => unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p))
208+
.fat_ptr_goto_expr
209+
.unwrap()
210+
.member("len", &self.symbol_table),
209211
_ => unreachable!("Len(_) called on type that has no length: {:?}", pt),
210212
}
211213
}
@@ -411,7 +413,8 @@ impl<'tcx> GotocCtx<'tcx> {
411413
UnOp::Neg => self.codegen_operand(e).neg(),
412414
},
413415
Rvalue::Discriminant(p) => {
414-
let place = self.codegen_place(p).goto_expr;
416+
let place =
417+
unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p)).goto_expr;
415418
let pt = self.place_ty(p);
416419
self.codegen_get_discriminant(place, pt, res_ty)
417420
}

‎src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

Lines changed: 37 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ use super::typ::FN_RETURN_VOID_VAR_NAME;
55
use super::PropertyClass;
66
use crate::codegen_cprover_gotoc::utils;
77
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
8+
use crate::unwrap_or_return_codegen_unimplemented_stmt;
89
use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
910
use cbmc::utils::BUG_REPORT_URL;
1011
use kani_queries::UserInput;
@@ -63,7 +64,9 @@ impl<'tcx> GotocCtx<'tcx> {
6364
self.codegen_ret_unit()
6465
} else {
6566
let p = Place::from(mir::RETURN_PLACE);
66-
let v = self.codegen_place(&p).goto_expr;
67+
let v =
68+
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(&p))
69+
.goto_expr;
6770
if self.place_ty(&p).is_bool() {
6871
v.cast_to(Type::c_bool()).ret(loc)
6972
} else {
@@ -151,7 +154,9 @@ impl<'tcx> GotocCtx<'tcx> {
151154
let loc_ty = self.place_ty(location);
152155
let drop_instance = Instance::resolve_drop_in_place(self.tcx, loc_ty);
153156
if let Some(hk) = self.hooks.hook_applies(self.tcx, drop_instance) {
154-
let le = self.codegen_place(location).goto_expr;
157+
let le =
158+
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(location))
159+
.goto_expr;
155160
hk.handle(self, drop_instance, vec![le], None, Some(*target), None)
156161
} else {
157162
let drop_implementation = match drop_instance.def {
@@ -163,8 +168,12 @@ impl<'tcx> GotocCtx<'tcx> {
163168
match loc_ty.kind() {
164169
ty::Dynamic(..) => {
165170
// Virtual drop via a vtable lookup
166-
let trait_fat_ptr =
167-
self.codegen_place(location).fat_ptr_goto_expr.unwrap();
171+
let trait_fat_ptr = unwrap_or_return_codegen_unimplemented_stmt!(
172+
self,
173+
self.codegen_place(location)
174+
)
175+
.fat_ptr_goto_expr
176+
.unwrap();
168177

169178
// Pull the function off of the fat pointer's vtable pointer
170179
let vtable_ref =
@@ -195,7 +204,10 @@ impl<'tcx> GotocCtx<'tcx> {
195204
assert!(!matches!(drop_instance.def, InstanceDef::Virtual(_, _)));
196205

197206
let func = self.codegen_func_expr(drop_instance, None);
198-
let place = self.codegen_place(location);
207+
let place = unwrap_or_return_codegen_unimplemented_stmt!(
208+
self,
209+
self.codegen_place(location)
210+
);
199211
let arg = if let Some(fat_ptr) = place.fat_ptr_goto_expr {
200212
// Drop takes the fat pointer if it exists
201213
fat_ptr
@@ -513,7 +525,9 @@ impl<'tcx> GotocCtx<'tcx> {
513525
if self.place_ty(p).is_unit() {
514526
e.as_stmt(Location::none())
515527
} else {
516-
self.codegen_place(&p).goto_expr.assign(e, Location::none())
528+
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(&p))
529+
.goto_expr
530+
.assign(e, Location::none())
517531
}
518532
}
519533

@@ -576,15 +590,17 @@ impl<'tcx> GotocCtx<'tcx> {
576590
// implicit address of a function pointer, e.g.
577591
// let fp: fn() -> i32 = foo;
578592
// where the reference is implicit.
579-
self.codegen_place(l)
593+
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
580594
.goto_expr
581595
.assign(self.codegen_rvalue(r).address_of(), Location::none())
582596
} else if rty.is_bool() {
583-
self.codegen_place(l)
597+
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
584598
.goto_expr
585599
.assign(self.codegen_rvalue(r).cast_to(Type::c_bool()), Location::none())
586600
} else {
587-
self.codegen_place(l).goto_expr.assign(self.codegen_rvalue(r), Location::none())
601+
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
602+
.goto_expr
603+
.assign(self.codegen_rvalue(r), Location::none())
588604
}
589605
}
590606
StatementKind::SetDiscriminant { place, variant_index } => {
@@ -624,10 +640,13 @@ impl<'tcx> GotocCtx<'tcx> {
624640
// DISCRIMINANT - val:0 ty:i8
625641
// DISCRIMINANT - val:1 ty:i8
626642
let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
627-
self.codegen_place(place)
628-
.goto_expr
629-
.member("case", &self.symbol_table)
630-
.assign(discr, Location::none())
643+
unwrap_or_return_codegen_unimplemented_stmt!(
644+
self,
645+
self.codegen_place(place)
646+
)
647+
.goto_expr
648+
.member("case", &self.symbol_table)
649+
.assign(discr, Location::none())
631650
}
632651
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
633652
if dataful_variant != variant_index {
@@ -647,7 +666,11 @@ impl<'tcx> GotocCtx<'tcx> {
647666
} else {
648667
Expr::int_constant(niche_value, discr_ty.clone())
649668
};
650-
let place = self.codegen_place(place).goto_expr;
669+
let place = unwrap_or_return_codegen_unimplemented_stmt!(
670+
self,
671+
self.codegen_place(place)
672+
)
673+
.goto_expr;
651674
self.codegen_get_niche(place, offset, discr_ty)
652675
.assign(value, Location::none())
653676
} else {

0 commit comments

Comments
 (0)