File tree Expand file tree Collapse file tree 11 files changed +75
-22
lines changed Expand file tree Collapse file tree 11 files changed +75
-22
lines changed Original file line number Diff line number Diff line change 3
3
4
4
//! This file contains the code necessary to interface with the compiler backend
5
5
6
- use crate :: overrides:: skip_monomorphize;
7
6
use crate :: GotocCtx ;
7
+
8
8
use bitflags:: _core:: any:: Any ;
9
9
use cbmc:: goto_program:: symtab_transformer;
10
10
use cbmc:: goto_program:: SymbolTable ;
@@ -46,9 +46,7 @@ impl CodegenBackend for GotocCodegenBackend {
46
46
Box :: new ( rustc_codegen_ssa:: back:: metadata:: DefaultMetadataLoader )
47
47
}
48
48
49
- fn provide ( & self , providers : & mut Providers ) {
50
- providers. skip_monomorphize = skip_monomorphize;
51
- }
49
+ fn provide ( & self , _providers : & mut Providers ) { }
52
50
53
51
fn provide_extern ( & self , _providers : & mut ty:: query:: ExternProviders ) { }
54
52
Original file line number Diff line number Diff line change @@ -326,6 +326,7 @@ struct MemSwap;
326
326
327
327
impl < ' tcx > GotocHook < ' tcx > for MemSwap {
328
328
fn hook_applies ( & self , tcx : TyCtxt < ' tcx > , instance : Instance < ' tcx > ) -> bool {
329
+ // We need to keep the old std / core functions here because we don't compile std yet.
329
330
let name = with_no_trimmed_paths ( || tcx. def_path_str ( instance. def_id ( ) ) ) ;
330
331
name == "core::mem::swap"
331
332
|| name == "std::mem::swap"
@@ -688,7 +689,3 @@ impl<'tcx> GotocHooks<'tcx> {
688
689
None
689
690
}
690
691
}
691
-
692
- pub fn skip_monomorphize < ' tcx > ( tcx : TyCtxt < ' tcx > , instance : Instance < ' tcx > ) -> bool {
693
- fn_hooks ( ) . hooks . iter ( ) . any ( |hook| hook. hook_applies ( tcx, instance) )
694
- }
Original file line number Diff line number Diff line change 8
8
9
9
mod hooks;
10
10
11
- pub use hooks:: { fn_hooks, skip_monomorphize , GotocHooks } ;
11
+ pub use hooks:: { fn_hooks, GotocHooks } ;
Original file line number Diff line number Diff line change @@ -874,7 +874,6 @@ impl CrateInfo {
874
874
}
875
875
876
876
pub fn provide ( providers : & mut Providers ) {
877
- providers. skip_monomorphize = |_, _| false ;
878
877
providers. backend_optimization_level = |tcx, cratenum| {
879
878
let for_speed = match tcx. sess . opts . optimize {
880
879
// If globally no optimisation is done, #[optimize] has no effect.
Original file line number Diff line number Diff line change @@ -1862,11 +1862,4 @@ rustc_queries! {
1862
1862
no_hash
1863
1863
desc { "performing HIR wf-checking for predicate {:?} at item {:?}" , key. 0 , key. 1 }
1864
1864
}
1865
-
1866
- query skip_monomorphize( key: ty:: Instance <' tcx>)
1867
- -> bool {
1868
- eval_always
1869
- no_hash
1870
- desc { "Check if we should skip monomorphization for `{}`" , key}
1871
- }
1872
1865
}
Original file line number Diff line number Diff line change @@ -317,7 +317,6 @@ pub fn collect_crate_mono_items(
317
317
( visited. into_inner ( ) , inlining_map. into_inner ( ) )
318
318
}
319
319
320
- // Temporary function that allow us to skip monomorphizing lang_start.
321
320
// Find all non-generic items by walking the HIR. These items serve as roots to
322
321
// start monomorphizing from.
323
322
fn collect_roots ( tcx : TyCtxt < ' _ > , mode : MonoItemCollectionMode ) -> Vec < MonoItem < ' _ > > {
@@ -922,10 +921,6 @@ fn visit_instance_use<'tcx>(
922
921
return ;
923
922
}
924
923
925
- if tcx. skip_monomorphize ( instance) {
926
- return ;
927
- }
928
-
929
924
match instance. def {
930
925
ty:: InstanceDef :: Virtual ( ..) | ty:: InstanceDef :: Intrinsic ( _) => {
931
926
if !is_direct_call {
Original file line number Diff line number Diff line change
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ use std:: mem;
5
+
6
+ pub fn main ( ) {
7
+ let mut var1 = rmc:: nondet :: < i32 > ( ) ;
8
+ let mut var2 = rmc:: nondet :: < i32 > ( ) ;
9
+ let old_var1 = var1;
10
+ unsafe {
11
+ assert_eq ! ( mem:: replace( & mut var1, var2) , old_var1) ;
12
+ }
13
+ assert_eq ! ( var1, var2) ;
14
+ }
Original file line number Diff line number Diff line change
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ use std:: mem;
5
+
6
+ pub fn main ( ) {
7
+ let mut var1 = rmc:: nondet :: < i32 > ( ) ;
8
+ let mut var2 = rmc:: nondet :: < i32 > ( ) ;
9
+ let old_var1 = var1;
10
+ let old_var2 = var2;
11
+ unsafe {
12
+ mem:: swap ( & mut var1, & mut var2) ;
13
+ }
14
+ assert_eq ! ( var1, old_var2) ;
15
+ assert_eq ! ( var2, old_var1) ;
16
+ }
Original file line number Diff line number Diff line change
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ use std:: ptr:: read;
5
+
6
+ pub fn main ( ) {
7
+ let var = 1 ;
8
+ unsafe {
9
+ assert_eq ! ( read( & var) , var) ;
10
+ }
11
+ }
Original file line number Diff line number Diff line change
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ use std:: ptr:: write;
5
+
6
+ pub fn main ( ) {
7
+ let mut var = 1 ;
8
+ unsafe {
9
+ write ( & mut var, 10 ) ;
10
+ }
11
+ assert_eq ! ( var, 10 ) ;
12
+ }
Original file line number Diff line number Diff line change
1
+ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2
+ // SPDX-License-Identifier: Apache-2.0 OR MIT
3
+
4
+ #![ feature( never_type) ]
5
+
6
+ /// Test using the never type
7
+ pub fn err ( ) -> ! {
8
+ panic ! ( "EXPECTED FAIL: Function should always fail" ) ;
9
+ }
10
+
11
+ // Give an empty main to make rustc happy.
12
+ #[ no_mangle]
13
+ pub fn main ( ) {
14
+ let var = rmc:: nondet :: < i32 > ( ) ;
15
+ if var > 0 {
16
+ err ( ) ;
17
+ }
18
+ }
You can’t perform that action at this time.
0 commit comments