Skip to content

Commit

Permalink
Update the rust toolchain to nightly-2022-05-03 (#1181)
Browse files Browse the repository at this point in the history 
* Update rust toolchain to nightly-2022-05-03

This compiles but regression is failing due to unimplemented statement.

* Handle change to Box<T> structure

Box<T> now users NonNull<T> instead of raw pointer.

* Handle new statement kind Deinit

We codegen an assignment to non-det value per documentation. See more
information here:
 - rust-lang/rust#95125

* Fix discriminant computation

After the merge, the previous wrapping sub logic was triggering a panic
due to u128 -> i64 conversion. There were also other overflow issues
when trying to convert the `niche_value` to unsigned.

For now, I'm disabling the coversion check which I believe is too
strict. We should consider implementing a more flexible check later that
can be controlled by the user without affecting the internal compiler
codegen.

* Address PR comments:

 - Improve comments.
 - Remove wrong cast to i64.
 - Fix statement location.
 - Create util function to create unsigned type.
  • Loading branch information
@celinval
celinval authored May 12, 2022
1 parent 0805270 commit d0b74ca
Show file tree
Hide file tree
Showing 16 changed files with 258 additions and 202 deletions.
13 changes: 13 additions & 0 deletions cprover_bindings/src/goto_program/typ.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -973,6 +973,19 @@ impl Type {
Pointer { typ: Box::new(self) }
}

/// Convert type to its unsigned counterpart if possible.
/// For types that are already unsigned, this will return self.
/// Note: This will expand any typedef.
pub fn to_unsigned(&self) -> Option<Self> {
let concrete = self.unwrap_typedef();
match concrete {
CInteger(CIntType::SSizeT) => Some(CInteger(CIntType::SizeT)),
Signedbv { ref width } => Some(Unsignedbv { width: *width }),
Unsignedbv { .. } => Some(self.clone()),
_ => None,
}
}

pub fn signed_int<T>(w: T) -> Self
where
T: TryInto<u64>,
Expand Down
59 changes: 27 additions & 32 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -472,19 +472,27 @@ impl<'tcx> GotocCtx<'tcx> {
FieldsShape::Arbitrary { offsets, .. } => offsets[0].bytes_usize(),
_ => unreachable!("niche encoding must have arbitrary fields"),
};
let discr_ty = self.codegen_enum_discr_typ(ty);
let discr_ty = self.codegen_ty(discr_ty);
let niche_val = self.codegen_get_niche(e, offset, discr_ty.clone());
let relative_discr = if *niche_start == 0 {
niche_val
} else {
wrapping_sub(&niche_val, *niche_start)
};

// Compute relative discriminant value (`niche_val - niche_start`).
//
// "We remap `niche_start..=niche_start + n` (which may wrap around) to
// (non-wrap-around) `0..=n`, to be able to check whether the discriminant
// corresponds to a niche variant with one comparison."
// https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
//
// Note: niche_variants can only represent values that fit in a u32.
let discr_mir_ty = self.codegen_enum_discr_typ(ty);
let discr_type = self.codegen_ty(discr_mir_ty);
let niche_val = self.codegen_get_niche(e, offset, discr_type.clone());
let relative_discr =
wrapping_sub(&niche_val, u64::try_from(*niche_start).unwrap());
let relative_max =
niche_variants.end().as_u32() - niche_variants.start().as_u32();
let is_niche = if tag.value == Primitive::Pointer {
discr_ty.null().eq(relative_discr.clone())
let is_niche = if tag.primitive() == Primitive::Pointer {
tracing::trace!(?tag, "Primitive::Pointer");
discr_type.null().eq(relative_discr.clone())
} else {
tracing::trace!(?tag, "Not Primitive::Pointer");
relative_discr
.clone()
.le(Expr::int_constant(relative_max, relative_discr.typ().clone()))
Expand Down Expand Up @@ -1260,26 +1268,13 @@ impl<'tcx> GotocCtx<'tcx> {
/// Perform a wrapping subtraction of an Expr with a constant "expr - constant"
/// where "-" is wrapping subtraction, i.e., the result should be interpreted as
/// an unsigned value (2's complement).
fn wrapping_sub(expr: &Expr, constant: u128) -> Expr {
// While the wrapping subtraction can be done through a regular subtraction
// and then casting the result to an unsigned, doing so may result in CBMC
// flagging the operation with a signed to unsigned overflow failure (see
// https://github.com/model-checking/kani/issues/356).
// To avoid those overflow failures, the wrapping subtraction operation is
// computed as:
// if expr >= constant {
// // result is positive, so overflow may not occur
// expr - constant
// } else {
// // compute the 2's complement to avoid overflow
// expr - constant + 2^32
// }
let s64 = Type::signed_int(64);
let expr = expr.clone().cast_to(s64.clone());
let twos_complement: i64 = u32::MAX as i64 + 1 - i64::try_from(constant).unwrap();
let constant = Expr::int_constant(constant, s64.clone());
expr.clone().ge(constant.clone()).ternary(
expr.clone().sub(constant),
expr.plus(Expr::int_constant(twos_complement, s64.clone())),
)
fn wrapping_sub(expr: &Expr, constant: u64) -> Expr {
if constant == 0 {
// No need to subtract.
expr.clone()
} else {
let unsigned = expr.typ().to_unsigned().unwrap();
let constant = Expr::int_constant(constant, unsigned.clone());
expr.clone().cast_to(unsigned).sub(constant)
}
}
62 changes: 38 additions & 24 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -603,6 +603,7 @@ impl<'tcx> GotocCtx<'tcx> {
pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt {
let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered();
debug!("handling statement {:?}", stmt);
let location = self.codegen_span(&stmt.source_info.span);
match &stmt.kind {
StatementKind::Assign(box (l, r)) => {
let lty = self.place_ty(l);
Expand All @@ -617,15 +618,32 @@ impl<'tcx> GotocCtx<'tcx> {
// where the reference is implicit.
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
.goto_expr
.assign(self.codegen_rvalue(r).address_of(), Location::none())
.assign(self.codegen_rvalue(r).address_of(), location)
} else if rty.is_bool() {
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
.goto_expr
.assign(self.codegen_rvalue(r).cast_to(Type::c_bool()), Location::none())
.assign(self.codegen_rvalue(r).cast_to(Type::c_bool()), location)
} else {
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
.goto_expr
.assign(self.codegen_rvalue(r), Location::none())
.assign(self.codegen_rvalue(r), location)
}
}
StatementKind::Deinit(place) => {
// From rustc doc: "This writes `uninit` bytes to the entire place."
// Thus, we assign nondet() value to the entire place.
let dst_mir_ty = self.place_ty(place);
let dst_type = self.codegen_ty(dst_mir_ty);
let layout = self.layout_of(dst_mir_ty);
if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
// We ignore assignment for all zero size types
// Ignore generators too for now:
// https://github.com/model-checking/kani/issues/416
Stmt::skip(location)
} else {
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
.goto_expr
.assign(dst_type.nondet(), location)
}
}
StatementKind::SetDiscriminant { place, variant_index } => {
Expand All @@ -638,16 +656,16 @@ impl<'tcx> GotocCtx<'tcx> {
.codegen_unimplemented(
"ty::Generator",
Type::code(vec![], Type::empty()),
Location::none(),
location.clone(),
"https://github.com/model-checking/kani/issues/416",
)
.as_stmt(Location::none());
.as_stmt(location);
}
_ => unreachable!(),
};
let layout = self.layout_of(pt);
match &layout.variants {
Variants::Single { .. } => Stmt::skip(Location::none()),
Variants::Single { .. } => Stmt::skip(location),
Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let discr = def.discriminant_for_variant(self.tcx, *variant_index);
Expand All @@ -671,7 +689,7 @@ impl<'tcx> GotocCtx<'tcx> {
)
.goto_expr
.member("case", &self.symbol_table)
.assign(discr, Location::none())
.assign(discr, location)
}
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
if dataful_variant != variant_index {
Expand All @@ -686,27 +704,28 @@ impl<'tcx> GotocCtx<'tcx> {
let niche_value =
variant_index.as_u32() - niche_variants.start().as_u32();
let niche_value = (niche_value as u128).wrapping_add(*niche_start);
let value = if niche_value == 0 && tag.value == Primitive::Pointer {
discr_ty.null()
} else {
Expr::int_constant(niche_value, discr_ty.clone())
};
let value =
if niche_value == 0 && tag.primitive() == Primitive::Pointer {
discr_ty.null()
} else {
Expr::int_constant(niche_value, discr_ty.clone())
};
let place = unwrap_or_return_codegen_unimplemented_stmt!(
self,
self.codegen_place(place)
)
.goto_expr;
self.codegen_get_niche(place, offset, discr_ty)
.assign(value, Location::none())
.assign(value, location)
} else {
Stmt::skip(Location::none())
Stmt::skip(location)
}
}
},
}
}
StatementKind::StorageLive(_) => Stmt::skip(Location::none()), // TODO: fix me
StatementKind::StorageDead(_) => Stmt::skip(Location::none()), // TODO: fix me
StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping {
ref src,
ref dst,
Expand All @@ -719,26 +738,21 @@ impl<'tcx> GotocCtx<'tcx> {
let sz = Expr::int_constant(sz, Type::size_t());
let n = sz.mul(count);
let dst = dst.cast_to(Type::void_pointer());
let e = BuiltinFn::Memcpy.call(vec![dst, src, n.clone()], Location::none());
let e = BuiltinFn::Memcpy.call(vec![dst, src, n.clone()], location.clone());

// The C implementation of memcpy does not allow an invalid pointer for
// the src/dst, but the LLVM implementation specifies that a copy with
// length zero is a no-op. This comes up specifically when handling
// the empty string; CBMC will fail on passing a reference to empty
// string unless we codegen this zero check.
// https://llvm.org/docs/LangRef.html#llvm-memcpy-intrinsic
Stmt::if_then_else(
n.is_zero().not(),
e.as_stmt(Location::none()),
None,
Location::none(),
)
Stmt::if_then_else(n.is_zero().not(), e.as_stmt(location.clone()), None, location)
}
StatementKind::FakeRead(_)
| StatementKind::Retag(_, _)
| StatementKind::AscribeUserType(_, _)
| StatementKind::Nop
| StatementKind::Coverage { .. } => Stmt::skip(Location::none()),
| StatementKind::Coverage { .. } => Stmt::skip(location),
}
.with_location(self.codegen_span(&stmt.source_info.span))
}
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1206,7 +1206,7 @@ impl<'tcx> GotocCtx<'tcx> {
pub fn codegen_enum_discr_typ(&self, ty: Ty<'tcx>) -> Ty<'tcx> {
let layout = self.layout_of(ty);
match &layout.variants {
Variants::Multiple { tag, .. } => self.codegen_prim_typ(tag.value),
Variants::Multiple { tag, .. } => self.codegen_prim_typ(tag.primitive()),
_ => unreachable!("only enum has discriminant"),
}
}
Expand Down Expand Up @@ -1263,7 +1263,7 @@ impl<'tcx> GotocCtx<'tcx> {
_ => unreachable!(),
};

let rustc_target::abi::Scalar { value: prim_type, .. } = element;
let prim_type = element.primitive();
let rust_type = self.codegen_prim_typ(prim_type);
let cbmc_type = self.codegen_ty(rust_type);

Expand Down
Loading

0 comments on commit d0b74ca

Please sign in to comment.