Skip to content

Commit

Permalink
codegen_scalar: support tuples with more than one element
Browse files Browse the repository at this point in the history
With toolchain versions from 2023-02-05 onwards we have multi-element
tuples in a Scalar (seen for the `(DropMe, Yielded(()))` tuple of
tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs).
  • Loading branch information
tautschnig committed Apr 13, 2023
1 parent a85f77c commit 22cd176
Showing 1 changed file with 12 additions and 10 deletions.
22 changes: 12 additions & 10 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ impl<'tcx> GotocCtx<'tcx> {
/// 1. integers
/// 2. ZST, or transparent structs of one (scalar) value
/// 3. enums that don't carry data
/// 4. unit, 1-ary tuples, or size-0 arrays
/// 4. unit, tuples (may be multi-ary!), or size-0 arrays
/// 5. pointers to an allocation
fn codegen_scalar(&mut self, s: Scalar, ty: Ty<'tcx>, span: Option<&Span>) -> Expr {
debug!(scalar=?s, ?ty, kind=?ty.kind(), ?span, "codegen_scalar");
Expand Down Expand Up @@ -394,15 +394,17 @@ impl<'tcx> GotocCtx<'tcx> {
}
}
}
(s, ty::Tuple(substs)) => {
// here we have tuples of at most one length
if substs.len() == 1 {
let overall_t = self.codegen_ty(ty);
let t = substs[0];
self.codegen_single_variant_single_field(s, span, overall_t, t)
} else {
unreachable!()
}
(Scalar::Int(int), ty::Tuple(_)) => {
// A ScalarInt has a u128-typed data field, so the result can never be larger than
// that and the conversion to a uint (of an actual size that may be smaller than
// 128 bits) will succeed.
let int_u128 = int.try_to_uint(int.size()).ok().unwrap();
let overall_t = self.codegen_ty(ty);
let expr_int = Expr::int_constant(
int_u128,
Type::unsigned_int(overall_t.sizeof_in_bits(&self.symbol_table)),
);
expr_int.transmute_to(overall_t, &self.symbol_table)
}
(_, ty::Array(_, _)) => {
// we must have zero size array here
Expand Down

0 comments on commit 22cd176

Please sign in to comment.