Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update the rust toolchain to nightly-2022-05-03 #1181

Merged
merged 6 commits into from
May 12, 2022
Merged

Update the rust toolchain to nightly-2022-05-03 #1181

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
1443181
Update rust toolchain to nightly-2022-05-03
celinval May 5, 2022
ddd6005
Handle change to Box<T> structure
celinval May 10, 2022
b378f72
Handle new statement kind Deinit
celinval May 10, 2022
08aeae3
Fix discriminant computation
celinval May 10, 2022
dbec9fc
Address PR comments:
celinval May 10, 2022
12cf423
Merge branch 'main' into issue-1162-toolchain
celinval May 11, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions cprover_bindings/src/goto_program/typ.rs
View file
Open in desktop
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> {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

let concrete = self.unwrap_typedef();
match concrete {
CInteger(CIntType::SSizeT) => Some(CInteger(CIntType::SizeT)),
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aren't there some other types that could go here too?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I could include Bool which would be a no-op and I could handle CBitField but I noticed that we don't handle that in neither signed() or unsigned() so we should probably add some logic there too. For us to add support to Char we would need access to the machine model. Is there any other type you would like to see?

Let me know what you prefer and I can add that as a follow up PR.

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
Open in desktop
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`).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there Rust documentation to point to here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nope... I can point to the code where I derived this comment from though.

//
// "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
Open in desktop
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:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need to ignore generators?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because we don't codegen them and they end up with size 0 despite what their layout says.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW, I changed the check to see if the size of the destination is 0, which today will exclude generators. The first check might be redundant now, but I guess it doesn't hurt 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
Open in desktop
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();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's cleaner :)

let rust_type = self.codegen_prim_typ(prim_type);
let cbmc_type = self.codegen_ty(rust_type);

Expand Down
Loading