@@ -4,8 +4,7 @@ use rustc_middle::ty::ScalarInt;
4
4
use tracing:: info;
5
5
6
6
use super :: GenmcScalar ;
7
- use crate :: alloc_addresses:: EvalContextExt as _;
8
- use crate :: { BorTag , MiriInterpCx , Pointer , Provenance , Scalar , throw_unsup_format} ;
7
+ use crate :: { MiriInterpCx , Scalar , throw_unsup_format} ;
9
8
10
9
pub fn split_access ( address : Size , size : Size ) -> impl Iterator < Item = ( u64 , u64 ) > {
11
10
/// Maximum size memory access in bytes that GenMC supports.
@@ -70,66 +69,28 @@ pub fn option_scalar_to_genmc_scalar<'tcx>(
70
69
}
71
70
72
71
pub fn scalar_to_genmc_scalar < ' tcx > (
73
- ecx : & MiriInterpCx < ' tcx > ,
72
+ _ecx : & MiriInterpCx < ' tcx > ,
74
73
scalar : Scalar ,
75
74
) -> InterpResult < ' tcx , GenmcScalar > {
76
75
interp_ok ( match scalar {
77
76
rustc_const_eval:: interpret:: Scalar :: Int ( scalar_int) => {
78
77
// TODO GENMC: u128 support
79
78
let value: u64 = scalar_int. to_uint ( scalar_int. size ( ) ) . try_into ( ) . unwrap ( ) ; // TODO GENMC: doesn't work for size != 8
80
- GenmcScalar { value, extra : 0 , is_init : true }
81
- }
82
- rustc_const_eval:: interpret:: Scalar :: Ptr ( pointer, size) => {
83
- let addr = Pointer :: from ( pointer) . addr ( ) ;
84
- if let Provenance :: Wildcard = pointer. provenance {
85
- throw_unsup_format ! ( "Pointers with wildcard provenance not allowed in GenMC mode" ) ;
86
- }
87
- let ( alloc_id, _size, _prov_extra) =
88
- rustc_const_eval:: interpret:: Machine :: ptr_get_alloc ( ecx, pointer, size. into ( ) )
89
- . unwrap ( ) ;
90
- let base_addr = ecx. addr_from_alloc_id ( alloc_id, None ) ?;
91
- GenmcScalar { value : addr. bytes ( ) , extra : base_addr, is_init : true }
79
+ GenmcScalar { value, is_init : true }
92
80
}
81
+ rustc_const_eval:: interpret:: Scalar :: Ptr ( _pointer, _size) =>
82
+ throw_unsup_format ! (
83
+ "FIXME(genmc): Implement sending pointers (with provenance) to GenMC."
84
+ ) ,
93
85
} )
94
86
}
95
87
96
88
pub fn genmc_scalar_to_scalar < ' tcx > (
97
- ecx : & MiriInterpCx < ' tcx > ,
89
+ _ecx : & MiriInterpCx < ' tcx > ,
98
90
scalar : GenmcScalar ,
99
91
size : Size ,
100
92
) -> InterpResult < ' tcx , Scalar > {
101
- // TODO GENMC: proper handling of large integers
102
- // TODO GENMC: proper handling of pointers (currently assumes all integers)
103
-
104
- if scalar. extra != 0 {
105
- // We have a pointer!
106
-
107
- let addr = Size :: from_bytes ( scalar. value ) ;
108
- let base_addr = scalar. extra ;
109
-
110
- let alloc_size = 0 ; // TODO GENMC: what is the correct size here? Is 0 ok?
111
- let only_exposed_allocations = false ;
112
- let Some ( alloc_id) =
113
- ecx. alloc_id_from_addr ( base_addr, alloc_size, only_exposed_allocations)
114
- else {
115
- // TODO GENMC: what is the correct error in this case?
116
- throw_unsup_format ! (
117
- "Cannot get allocation id of pointer received from GenMC (base address: 0x{base_addr:x}, pointer address: 0x{:x})" ,
118
- addr. bytes( )
119
- ) ;
120
- } ;
121
-
122
- // TODO GENMC: is using `size: Size` ok here? Can we ever have `size != sizeof pointer`?
123
-
124
- // FIXME: Currently GenMC mode incompatible with aliasing model checking
125
- let tag = BorTag :: default ( ) ;
126
- let provenance = crate :: machine:: Provenance :: Concrete { alloc_id, tag } ;
127
- let offset = addr;
128
- let ptr = rustc_middle:: mir:: interpret:: Pointer :: new ( provenance, offset) ;
129
-
130
- let size = size. bytes ( ) . try_into ( ) . unwrap ( ) ;
131
- return interp_ok ( Scalar :: Ptr ( ptr, size) ) ;
132
- }
93
+ // FIXME(genmc): Add GencmScalar to Miri Pointer conversion.
133
94
134
95
// NOTE: GenMC always returns 64 bit values, and the upper bits are not yet truncated.
135
96
// FIXME(genmc): Rework if 128bit support is added to GenMC.
0 commit comments