Skip to content

Commit

Permalink
Fix types for codegen of intrinsic const (model-checking#268)
Browse files Browse the repository at this point in the history
  • Loading branch information
avanhatt authored and tedinski committed Apr 22, 2022
1 parent 29aba6a commit a7e245c
Show file tree
Hide file tree
Showing 3 changed files with 31 additions and 11 deletions.
14 changes: 4 additions & 10 deletions compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -153,17 +153,11 @@ impl<'tcx> GotocCtx<'tcx> {
() => {{
let value = self
.tcx
.const_eval_instance(ty::ParamEnv::reveal_all(), instance, None)
.const_eval_instance(ty::ParamEnv::reveal_all(), instance, span)
.unwrap();
// We may have an implicit cast between machine equivalent
// types where CBMC expects a different type than Rust.
let place_type = self.codegen_ty(self.place_ty(p));
let e = self
.codegen_const_value(value, self.tcx.types.usize, None)
.cast_to_machine_equivalent_type(
&place_type,
&self.symbol_table.machine_model(),
);
// We assume that the intrinsic has type checked at this point, so
// we can use the place type as the expression type.
let e = self.codegen_const_value(value, self.place_ty(p), span.as_ref());
self.codegen_expr_to_place(p, e)
}};
}
Expand Down
2 changes: 1 addition & 1 deletion src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ include!("../../rmc-prelude.rs");
fn takes_dyn_fun(fun: &dyn Fn() -> u32) {
let x = fun();
__VERIFIER_expect_fail(x != 5, "Wrong return");

/* The function dynamic object has no associated data */
__VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size");
}
Expand Down
26 changes: 26 additions & 0 deletions src/test/cbmc/Intrinsics/needs_drop.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Check that we get the expected results for needs_drop intrinsic

use std::mem;

pub struct Foo<T> {
_foo: T,
}

impl<T> Foo<T> {
fn call_needs_drop(&self) -> bool {
return mem::needs_drop::<T>();
}
}

fn main() {
// Integers don't need to be dropped
let int_foo = Foo::<i32> { _foo: 0 };
assert!(!int_foo.call_needs_drop());

// But strings do need to be dropped
let string_foo = Foo::<String> { _foo: "".to_string() };
assert!(string_foo.call_needs_drop());
}

0 comments on commit a7e245c

Please sign in to comment.