-
Notifications
You must be signed in to change notification settings - Fork 84
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.
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 Kani to Rust nightly-2022-10-11 #1788
Changes from 4 commits
a9fdfa7
8b2bb88
840bfad
4f88c33
579b8bd
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -9,7 +9,7 @@ use rustc_ast::ast::Mutability; | |
use rustc_middle::mir::interpret::{ | ||
read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar, | ||
}; | ||
use rustc_middle::mir::{Constant, ConstantKind, Operand}; | ||
use rustc_middle::mir::{Constant, ConstantKind, Operand, UnevaluatedConst}; | ||
use rustc_middle::ty::layout::LayoutOf; | ||
use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy}; | ||
use rustc_span::def_id::DefId; | ||
|
@@ -47,28 +47,37 @@ impl<'tcx> GotocCtx<'tcx> { | |
|
||
fn codegen_constant(&mut self, c: &Constant<'tcx>) -> Expr { | ||
trace!(constant=?c, "codegen_constant"); | ||
let const_ = match self.monomorphize(c.literal) { | ||
ConstantKind::Ty(ct) => ct, | ||
ConstantKind::Val(val, ty) => return self.codegen_const_value(val, ty, Some(&c.span)), | ||
}; | ||
let span = Some(&c.span); | ||
match self.monomorphize(c.literal) { | ||
ConstantKind::Ty(ct) => self.codegen_const(ct, span), | ||
ConstantKind::Val(val, ty) => self.codegen_const_value(val, ty, span), | ||
ConstantKind::Unevaluated(unevaluated, ty) => { | ||
self.codegen_const_unevaluated(unevaluated, ty, span) | ||
} | ||
} | ||
} | ||
|
||
self.codegen_const(const_, Some(&c.span)) | ||
fn codegen_const_unevaluated( | ||
&mut self, | ||
unevaluated: UnevaluatedConst<'tcx>, | ||
ty: Ty<'tcx>, | ||
span: Option<&Span>, | ||
) -> Expr { | ||
debug!("The literal was a Unevaluated"); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can you please add the constant? debug!(?unevaluated, "codegen_const_unevaluated"); Nit: I usually add the name of the function to the log so it's easy to find it in the code. But I don't think we have any guidelines on this. So just a suggestion. |
||
let const_val = | ||
self.tcx.const_eval_resolve(ty::ParamEnv::reveal_all(), unevaluated, None).unwrap(); | ||
self.codegen_const_value(const_val, ty, span) | ||
} | ||
|
||
pub fn codegen_const(&mut self, lit: Const<'tcx>, span: Option<&Span>) -> Expr { | ||
debug!("found literal: {:?}", lit); | ||
let lit = self.monomorphize(lit); | ||
|
||
match lit.kind() { | ||
// evaluate constant if it has no been evaluated yet | ||
ConstKind::Unevaluated(unevaluated) => { | ||
debug!("The literal was a Unevaluated"); | ||
let const_val = self | ||
.tcx | ||
.const_eval_resolve(ty::ParamEnv::reveal_all(), unevaluated, None) | ||
.unwrap(); | ||
self.codegen_const_value(const_val, lit.ty(), span) | ||
} | ||
// A `ConstantKind::Ty(ConstKind::Unevaluated)` should no longer show up | ||
// and should be a `ConstantKind::Unevaluated` instead (and thus handled | ||
// in `codegen_constant` not here.) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. in |
||
ConstKind::Unevaluated(_) => unreachable!(), | ||
|
||
ConstKind::Value(valtree) => { | ||
let value = self.tcx.valtree_to_const_val((lit.ty(), valtree)); | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -5,11 +5,11 @@ | |
#![feature(core_intrinsics)] | ||
use std::intrinsics; | ||
|
||
// The code below attempts to leave type `bool` uninitialized, causing the | ||
// The code below attempts to leave type `!` uninitialized, causing the | ||
// intrinsic `assert_uninit_valid` to generate a panic during compilation. | ||
#[kani::proof] | ||
fn main() { | ||
let _var: () = unsafe { | ||
intrinsics::assert_uninit_valid::<bool>(); | ||
intrinsics::assert_uninit_valid::<!>(); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The problem is that this triggers the same path as
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yep! Fixed. |
||
}; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,10 +2,6 @@ | |
// | ||
// Modifications Copyright Kani Contributors | ||
// See GitHub history for details. | ||
// | ||
// NOTE: The initial fix for this has been reverted from rustc. I'm keeping this test here so we | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Hopefully this was useful. :) |
||
// will know when it has been reverted back. | ||
// kani-check-fail | ||
|
||
//! Tests that check handling of opaque casts. Tests were adapted from the rustc repository. | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,6 +1,6 @@ | ||
module/mod.rs:10:5 in function module::not_empty | ||
main.rs:13:5 in function same_file | ||
/toolchains/ | ||
alloc/src/vec/mod.rs:2921:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop | ||
alloc/src/vec/mod.rs:3031:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop | ||
|
||
VERIFICATION:- SUCCESSFUL |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the heads-up! I'll figure this out as part of the work being done in #1148.