@@ -11,6 +11,7 @@ use cbmc::goto_program::SymbolTable;
11
11
use cbmc:: InternedString ;
12
12
use rmc_restrictions:: VtableCtxResults ;
13
13
use rustc_codegen_ssa:: traits:: CodegenBackend ;
14
+ use rustc_codegen_ssa:: { CodegenResults , CrateInfo } ;
14
15
use rustc_data_structures:: fx:: FxHashMap ;
15
16
use rustc_errors:: ErrorReported ;
16
17
use rustc_metadata:: EncodedMetadata ;
@@ -28,15 +29,6 @@ use std::iter::FromIterator;
28
29
use std:: path:: PathBuf ;
29
30
use tracing:: { debug, warn} ;
30
31
31
- // #[derive(RustcEncodable, RustcDecodable)]
32
- pub struct GotocCodegenResult {
33
- pub crate_name : rustc_span:: Symbol ,
34
- pub metadata : RmcMetadata ,
35
- pub symtab : SymbolTable ,
36
- pub type_map : BTreeMap < InternedString , InternedString > ,
37
- pub vtable_restrictions : Option < VtableCtxResults > ,
38
- }
39
-
40
32
#[ derive( Clone ) ]
41
33
pub struct GotocCodegenBackend ( ) ;
42
34
@@ -58,14 +50,12 @@ impl CodegenBackend for GotocCodegenBackend {
58
50
fn codegen_crate < ' tcx > (
59
51
& self ,
60
52
tcx : TyCtxt < ' tcx > ,
61
- _metadata : EncodedMetadata ,
62
- _need_metadata_module : bool ,
53
+ rustc_metadata : EncodedMetadata ,
54
+ need_metadata_module : bool ,
63
55
) -> Box < dyn Any > {
64
- use rustc_hir:: def_id:: LOCAL_CRATE ;
65
-
66
56
super :: utils:: init ( ) ;
67
57
68
- check_options ( & tcx. sess ) ;
58
+ check_options ( & tcx. sess , need_metadata_module ) ;
69
59
70
60
let codegen_units: & ' tcx [ CodegenUnit < ' _ > ] = tcx. collect_and_partition_mono_items ( ( ) ) . 1 ;
71
61
let mut c = GotocCtx :: new ( tcx) ;
@@ -134,7 +124,7 @@ impl CodegenBackend for GotocCodegenBackend {
134
124
) ;
135
125
136
126
// Map MIR types to GotoC types
137
- let type_map =
127
+ let type_map: BTreeMap < InternedString , InternedString > =
138
128
BTreeMap :: from_iter ( c. type_map . into_iter ( ) . map ( |( k, v) | ( k, v. to_string ( ) . into ( ) ) ) ) ;
139
129
140
130
// Get the vtable function pointer restrictions if requested
@@ -146,51 +136,53 @@ impl CodegenBackend for GotocCodegenBackend {
146
136
147
137
let metadata = RmcMetadata { proof_harnesses : c. proof_harnesses } ;
148
138
149
- Box :: new ( GotocCodegenResult {
150
- crate_name : tcx. crate_name ( LOCAL_CRATE ) as rustc_span:: Symbol ,
151
- metadata,
152
- symtab,
153
- type_map,
154
- vtable_restrictions,
155
- } )
139
+ // No output should be generated if user selected no_codegen.
140
+ if !tcx. sess . opts . debugging_opts . no_codegen && tcx. sess . opts . output_types . should_codegen ( ) {
141
+ let outputs = tcx. output_filenames ( ( ) ) ;
142
+ let base_filename = outputs. output_path ( OutputType :: Object ) ;
143
+ write_file ( & base_filename, "symtab.json" , & symtab) ;
144
+ write_file ( & base_filename, "type_map.json" , & type_map) ;
145
+ write_file ( & base_filename, "rmc-metadata.json" , & metadata) ;
146
+ // If they exist, write out vtable virtual call function pointer restrictions
147
+ if let Some ( restrictions) = vtable_restrictions {
148
+ write_file ( & base_filename, "restrictions.json" , & restrictions) ;
149
+ }
150
+ }
151
+
152
+ let work_products = FxHashMap :: < WorkProductId , WorkProduct > :: default ( ) ;
153
+ Box :: new ( (
154
+ CodegenResults {
155
+ modules : vec ! [ ] ,
156
+ allocator_module : None ,
157
+ metadata_module : None ,
158
+ metadata : rustc_metadata,
159
+ crate_info : CrateInfo :: new ( tcx, symtab. machine_model ( ) . architecture ( ) . to_string ( ) ) ,
160
+ } ,
161
+ work_products,
162
+ ) )
156
163
}
157
164
158
165
fn join_codegen (
159
166
& self ,
160
167
ongoing_codegen : Box < dyn Any > ,
161
168
_sess : & Session ,
162
- ) -> Result < ( Box < dyn Any > , FxHashMap < WorkProductId , WorkProduct > ) , ErrorReported > {
163
- Ok ( ( ongoing_codegen, FxHashMap :: default ( ) ) )
169
+ ) -> Result < ( CodegenResults , FxHashMap < WorkProductId , WorkProduct > ) , ErrorReported > {
170
+ Ok ( * ongoing_codegen
171
+ . downcast :: < ( CodegenResults , FxHashMap < WorkProductId , WorkProduct > ) > ( )
172
+ . unwrap ( ) )
164
173
}
165
174
166
175
fn link (
167
176
& self ,
168
- sess : & Session ,
169
- codegen_results : Box < dyn Any > ,
170
- outputs : & OutputFilenames ,
177
+ _sess : & Session ,
178
+ _codegen_results : CodegenResults ,
179
+ _outputs : & OutputFilenames ,
171
180
) -> Result < ( ) , ErrorReported > {
172
- let result = codegen_results
173
- . downcast :: < GotocCodegenResult > ( )
174
- . expect ( "in link: codegen_results is not a GotocCodegenResult" ) ;
175
-
176
- // No output should be generated if user selected no_codegen.
177
- if !sess. opts . debugging_opts . no_codegen && sess. opts . output_types . should_codegen ( ) {
178
- // "path.o"
179
- let base_filename = outputs. path ( OutputType :: Object ) ;
180
- write_file ( & base_filename, "symtab.json" , & result. symtab ) ;
181
- write_file ( & base_filename, "type_map.json" , & result. type_map ) ;
182
- write_file ( & base_filename, "rmc-metadata.json" , & result. metadata ) ;
183
- // If they exist, write out vtable virtual call function pointer restrictions
184
- if let Some ( restrictions) = result. vtable_restrictions {
185
- write_file ( & base_filename, "restrictions.json" , & restrictions) ;
186
- }
187
- }
188
-
189
181
Ok ( ( ) )
190
182
}
191
183
}
192
184
193
- fn check_options ( session : & Session ) {
185
+ fn check_options ( session : & Session , need_metadata_module : bool ) {
194
186
if !session. overflow_checks ( ) {
195
187
session. err ( "RMC requires overflow checks in order to provide a sound analysis." ) ;
196
188
}
@@ -202,6 +194,10 @@ fn check_options(session: &Session) {
202
194
) ;
203
195
}
204
196
197
+ if need_metadata_module {
198
+ session. err ( "RMC cannot generate metadata module." )
199
+ }
200
+
205
201
session. abort_if_errors ( ) ;
206
202
}
207
203
0 commit comments