Skip to content

Commit

Permalink
Upgrade toolchain to 2023-02-05 (model-checking#2347)
Browse files Browse the repository at this point in the history 
Co-authored-by: Celina G. Val <celinval@amazon.com>
  • Loading branch information
@tautschnig @celinval
tautschnig and celinval authored Apr 14, 2023
1 parent c4ed7ec commit 22b14f4
Show file tree
Hide file tree
Showing 6 changed files with 282 additions and 72 deletions.
11 changes: 11 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -624,6 +624,17 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Given a projection, generate an lvalue that represents the given variant index.
pub fn codegen_variant_lvalue(
&mut self,
initial_projection: ProjectedPlace<'tcx>,
variant_idx: VariantIdx,
) -> ProjectedPlace<'tcx> {
debug!(?initial_projection, ?variant_idx, "codegen_variant_lvalue");
let downcast = ProjectionElem::Downcast(None, variant_idx);
self.codegen_projection(Ok(initial_projection), downcast).unwrap()
}

// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html
// ConstantIndex
// [−]
Expand Down
153 changes: 144 additions & 9 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

use super::typ::pointee_type;
use crate::codegen_cprover_gotoc::codegen::place::{ProjectedPlace, TypeOrVariant};
use crate::codegen_cprover_gotoc::codegen::PropertyClass;
use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
Expand All @@ -17,9 +18,9 @@ use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place,
use rustc_middle::ty::adjustment::PointerCast;
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants};
use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants};
use std::collections::BTreeMap;
use tracing::{debug, warn};
use tracing::{debug, trace, warn};

impl<'tcx> GotocCtx<'tcx> {
fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand<'tcx>, e2: &Operand<'tcx>) -> Expr {
Expand Down Expand Up @@ -279,13 +280,112 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Create an initializer for a generator struct.
fn codegen_rvalue_generator(&mut self, operands: &[Operand<'tcx>], ty: Ty<'tcx>) -> Expr {
let layout = self.layout_of(ty);
let discriminant_field = match &layout.variants {
Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field,
_ => unreachable!(
"Expected generators to have multiple variants and direct encoding, but found: {layout:?}"
),
};
let overall_t = self.codegen_ty(ty);
let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap();
let mut operands_iter = operands.iter();
let direct_fields_expr = Expr::struct_expr_from_values(
direct_fields.typ(),
layout
.fields
.index_by_increasing_offset()
.map(|idx| {
let field_ty = layout.field(self, idx).ty;
if idx == *discriminant_field {
Expr::int_constant(0, self.codegen_ty(field_ty))
} else {
self.codegen_operand(operands_iter.next().unwrap())
}
})
.collect(),
&self.symbol_table,
);
assert!(operands_iter.next().is_none());
Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table)
}

/// This code will generate an expression that initializes an enumeration.
///
/// It will first create a temporary variant with the same enum type.
/// Initialize the case structure and set its discriminant.
/// Finally, it will return the temporary value.
fn codegen_rvalue_enum_aggregate(
&mut self,
variant_index: VariantIdx,
operands: &[Operand<'tcx>],
res_ty: Ty<'tcx>,
loc: Location,
) -> Expr {
let mut stmts = vec![];
let typ = self.codegen_ty(res_ty);
// 1- Create a temporary value of the enum type.
tracing::debug!(?typ, ?res_ty, "aggregate_enum");
let (temp_var, decl) = self.decl_temp_variable(typ.clone(), None, loc);
stmts.push(decl);
if !operands.is_empty() {
// 2- Initialize the members of the temporary variant.
let initial_projection = ProjectedPlace::try_new(
temp_var.clone(),
TypeOrVariant::Type(res_ty),
None,
None,
self,
)
.unwrap();
let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index);
let variant_expr = variant_proj.goto_expr.clone();
let layout = self.layout_of(res_ty);
let fields = match &layout.variants {
Variants::Single { index } => {
if *index != variant_index {
// This may occur if all variants except for the one pointed by
// index can never be constructed. Generic code might still try
// to initialize the non-existing invariant.
trace!(?res_ty, ?variant_index, "Unreachable invariant");
return Expr::nondet(typ);
}
&layout.fields
}
Variants::Multiple { variants, .. } => &variants[variant_index].fields,
};

trace!(?variant_expr, ?fields, ?operands, "codegen_aggregate enum");
let init_struct = Expr::struct_expr_from_values(
variant_expr.typ().clone(),
fields
.index_by_increasing_offset()
.map(|idx| self.codegen_operand(&operands[idx]))
.collect(),
&self.symbol_table,
);
let assign_case = variant_proj.goto_expr.assign(init_struct, loc);
stmts.push(assign_case);
}
// 3- Set discriminant.
let set_discriminant =
self.codegen_set_discriminant(res_ty, temp_var.clone(), variant_index, loc);
stmts.push(set_discriminant);
// 4- Return temporary variable.
stmts.push(temp_var.as_stmt(loc));
Expr::statement_expression(stmts, typ)
}

fn codegen_rvalue_aggregate(
&mut self,
k: &AggregateKind<'tcx>,
aggregate: &AggregateKind<'tcx>,
operands: &[Operand<'tcx>],
res_ty: Ty<'tcx>,
loc: Location,
) -> Expr {
match *k {
match *aggregate {
AggregateKind::Array(et) => {
if et.is_unit() {
Expr::struct_expr_from_values(
Expand All @@ -304,7 +404,44 @@ impl<'tcx> GotocCtx<'tcx> {
)
}
}
AggregateKind::Tuple => {
AggregateKind::Adt(_, _, _, _, Some(active_field_index)) => {
assert!(res_ty.is_union());
assert_eq!(operands.len(), 1);
let typ = self.codegen_ty(res_ty);
let components = typ.lookup_components(&self.symbol_table).unwrap();
Expr::union_expr(
typ,
components[active_field_index].name(),
self.codegen_operand(&operands[0]),
&self.symbol_table,
)
}
AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => {
let typ = self.codegen_ty(res_ty);
let layout = self.layout_of(res_ty);
let vector_element_type = typ.base_type().unwrap().clone();
Expr::vector_expr(
typ,
layout
.fields
.index_by_increasing_offset()
.map(|idx| {
let cgo = self.codegen_operand(&operands[idx]);
// The input operand might actually be a one-element array, as seen
// when running assess on firecracker.
if *cgo.typ() == vector_element_type {
cgo
} else {
cgo.transmute_to(vector_element_type.clone(), &self.symbol_table)
}
})
.collect(),
)
}
AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => {
self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc)
}
AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => {
let typ = self.codegen_ty(res_ty);
let layout = self.layout_of(res_ty);
Expr::struct_expr_from_values(
Expand All @@ -317,9 +454,7 @@ impl<'tcx> GotocCtx<'tcx> {
&self.symbol_table,
)
}
AggregateKind::Adt(_, _, _, _, _) => unimplemented!(),
AggregateKind::Closure(_, _) => unimplemented!(),
AggregateKind::Generator(_, _, _) => unimplemented!(),
AggregateKind::Generator(_, _, _) => self.codegen_rvalue_generator(&operands, res_ty),
}
}

Expand Down Expand Up @@ -406,7 +541,7 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_get_discriminant(place, pt, res_ty)
}
Rvalue::Aggregate(ref k, operands) => {
self.codegen_rvalue_aggregate(k, operands, res_ty)
self.codegen_rvalue_aggregate(k, operands, res_ty, loc)
}
Rvalue::ThreadLocalRef(def_id) => {
// Since Kani is single-threaded, we treat a thread local like a static variable:
Expand Down
126 changes: 64 additions & 62 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ use rustc_middle::ty;
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{Instance, InstanceDef, Ty};
use rustc_span::Span;
use rustc_target::abi::VariantIdx;
use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
use tracing::{debug, debug_span, trace};

Expand Down Expand Up @@ -55,68 +56,11 @@ impl<'tcx> GotocCtx<'tcx> {
}
StatementKind::Deinit(place) => self.codegen_deinit(place, location),
StatementKind::SetDiscriminant { place, variant_index } => {
// this requires place points to an enum type.
let pt = self.place_ty(place);
let layout = self.layout_of(pt);
match &layout.variants {
Variants::Single { .. } => Stmt::skip(location),
Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let discr =
pt.discriminant_for_variant(self.tcx, *variant_index).unwrap();
let discr_t = self.codegen_enum_discr_typ(pt);
// The constant created below may not fit into the type.
// https://github.com/model-checking/kani/issues/996
//
// It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)`
// or `discr.ty`. It looks like something is wrong with `discriminat_for_variant`
// because when it tries to codegen `std::cmp::Ordering` (which should produce
// discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types:
//
// debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty);
// DISCRIMINANT - val:255 ty:i8
// DISCRIMINANT - val:0 ty:i8
// DISCRIMINANT - val:1 ty:i8
let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!(
self,
self.codegen_place(place)
)
.goto_expr;
self.codegen_discriminant_field(place_goto_expr, pt)
.assign(discr, location)
}
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
if untagged_variant != variant_index {
let offset = match &layout.fields {
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
_ => unreachable!("niche encoding must have arbitrary fields"),
};
let discr_ty = self.codegen_enum_discr_typ(pt);
let discr_ty = self.codegen_ty(discr_ty);
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
&& matches!(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)
} else {
Stmt::skip(location)
}
}
},
}
let dest_ty = self.place_ty(place);
let dest_expr =
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
.goto_expr;
self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
}
StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
Expand Down Expand Up @@ -259,6 +203,64 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Create a statement that sets the variable discriminant to the value that corresponds to the
/// variant index.
pub fn codegen_set_discriminant(
&mut self,
dest_ty: Ty<'tcx>,
dest_expr: Expr,
variant_index: VariantIdx,
location: Location,
) -> Stmt {
// this requires place points to an enum type.
let layout = self.layout_of(dest_ty);
match &layout.variants {
Variants::Single { .. } => Stmt::skip(location),
Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let discr = dest_ty.discriminant_for_variant(self.tcx, variant_index).unwrap();
let discr_t = self.codegen_enum_discr_typ(dest_ty);
// The constant created below may not fit into the type.
// https://github.com/model-checking/kani/issues/996
//
// It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)`
// or `discr.ty`. It looks like something is wrong with `discriminat_for_variant`
// because when it tries to codegen `std::cmp::Ordering` (which should produce
// discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types:
//
// debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty);
// DISCRIMINANT - val:255 ty:i8
// DISCRIMINANT - val:0 ty:i8
// DISCRIMINANT - val:1 ty:i8
let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr, location)
}
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
if *untagged_variant != variant_index {
let offset = match &layout.fields {
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
_ => unreachable!("niche encoding must have arbitrary fields"),
};
let discr_ty = self.codegen_enum_discr_typ(dest_ty);
let discr_ty = self.codegen_ty(discr_ty);
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
&& matches!(tag.primitive(), Primitive::Pointer(_))
{
discr_ty.null()
} else {
Expr::int_constant(niche_value, discr_ty.clone())
};
self.codegen_get_niche(dest_expr, offset, discr_ty).assign(value, location)
} else {
Stmt::skip(location)
}
}
},
}
}

/// From rustc doc: "This writes `uninit` bytes to the entire place."
/// Our model of GotoC has a similar statement, which is later lowered
/// to assigning a Nondet in CBMC, with a comment specifying that it
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2023-02-04"
channel = "nightly-2023-02-05"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
Loading

0 comments on commit 22b14f4

Please sign in to comment.