Skip to content

Commit 5ecadef

Browse files
danielsntedinski
authored andcommitted
Move codegen code out of mod.rs into properly named files (rust-lang#415)
1 parent 1a0e1fe commit 5ecadef

File tree

5 files changed

+349
-300
lines changed

5 files changed

+349
-300
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//! This file contains functions related to codegenning MIR blocks into gotoc
5+
6+
use super::metadata::*;
7+
use rustc_middle::mir::{BasicBlock, BasicBlockData};
8+
9+
impl<'tcx> GotocCtx<'tcx> {
10+
pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) {
11+
self.current_fn_mut().set_current_bb(bb);
12+
let label: String = self.current_fn().find_label(&bb);
13+
// the first statement should be labelled. if there is no statements, then the
14+
// terminator should be labelled.
15+
match bbd.statements.len() {
16+
0 => {
17+
let term = bbd.terminator();
18+
let tcode = self.codegen_terminator(term);
19+
self.current_fn_mut().push_onto_block(tcode.with_label(label));
20+
}
21+
_ => {
22+
let stmt = &bbd.statements[0];
23+
let scode = self.codegen_statement(stmt);
24+
self.current_fn_mut().push_onto_block(scode.with_label(label));
25+
26+
for s in &bbd.statements[1..] {
27+
let stmt = self.codegen_statement(s);
28+
self.current_fn_mut().push_onto_block(stmt);
29+
}
30+
let term = self.codegen_terminator(bbd.terminator());
31+
self.current_fn_mut().push_onto_block(term);
32+
}
33+
}
34+
self.current_fn_mut().reset_current_bb();
35+
}
36+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//! This file contains functionality that makes RMC easier to debug
5+
6+
use super::metadata::*;
7+
use rustc_middle::mir::Body;
8+
use rustc_middle::ty::print::with_no_trimmed_paths;
9+
use rustc_middle::ty::Instance;
10+
use std::cell::RefCell;
11+
use std::lazy::SyncLazy;
12+
use std::panic;
13+
use tracing::debug;
14+
15+
// Use a thread-local global variable to track the current codegen item for debugging.
16+
// If RMC panics during codegen, we can grab this item to include the problematic
17+
// codegen item in the panic trace.
18+
thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<Option<String>> = RefCell::new(None));
19+
20+
// Include RMC's bug reporting URL in our panics.
21+
const BUG_REPORT_URL: &str =
22+
"https://github.com/model-checking/rmc/issues/new?labels=bug&template=bug_report.md";
23+
24+
// Custom panic hook.
25+
pub static DEFAULT_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
26+
SyncLazy::new(|| {
27+
let hook = panic::take_hook();
28+
panic::set_hook(Box::new(|info| {
29+
// Invoke the default handler, which prints the actual panic message and
30+
// optionally a backtrace. This also prints Rustc's "file a bug here" message:
31+
// it seems like the only way to remove that is to use rustc_driver::report_ice;
32+
// however, adding that dependency to this crate causes a circular dependency.
33+
// For now, just print our message after the Rust one and explicitly point to
34+
// our bug template form.
35+
(*DEFAULT_HOOK)(info);
36+
37+
// Separate the output with an empty line
38+
eprintln!();
39+
40+
// Print the current function if available
41+
CURRENT_CODEGEN_ITEM.with(|cell| {
42+
if let Some(current_item) = cell.borrow().clone() {
43+
eprintln!("[RMC] current codegen item: {}", current_item);
44+
} else {
45+
eprintln!("[RMC] no current codegen item.");
46+
}
47+
});
48+
49+
// Separate the output with an empty line
50+
eprintln!();
51+
52+
// Print the RMC message
53+
eprintln!("RMC unexpectedly panicked during code generation.\n");
54+
eprintln!(
55+
"If you are seeing this message, please file an issue here instead of on the Rust compiler: {}",
56+
BUG_REPORT_URL
57+
);
58+
}));
59+
hook
60+
});
61+
62+
impl<'tcx> GotocCtx<'tcx> {
63+
// Calls the closure while updating the tracked global variable marking the
64+
// codegen item for panic debugging.
65+
pub fn call_with_panic_debug_info<F: FnOnce(&mut GotocCtx<'tcx>) -> ()>(
66+
&mut self,
67+
call: F,
68+
panic_debug: String,
69+
) {
70+
CURRENT_CODEGEN_ITEM.with(|odb_cell| {
71+
odb_cell.replace(Some(panic_debug));
72+
call(self);
73+
odb_cell.replace(None);
74+
});
75+
}
76+
77+
pub fn print_instance(&self, instance: Instance<'_>, mir: &'tcx Body<'tcx>) {
78+
if cfg!(debug_assertions) {
79+
debug!(
80+
"handling {}, {}",
81+
instance,
82+
with_no_trimmed_paths(|| self.tcx.def_path_str(instance.def_id()))
83+
);
84+
debug!("variables: ");
85+
for l in mir.args_iter().chain(mir.vars_and_temps_iter()) {
86+
debug!("let {:?}: {:?}", l, self.local_ty(l));
87+
}
88+
for (bb, bbd) in mir.basic_blocks().iter_enumerated() {
89+
debug!("block {:?}", bb);
90+
for stmt in &bbd.statements {
91+
debug!("{:?}", stmt);
92+
}
93+
debug!("{:?}", bbd.terminator().kind);
94+
}
95+
}
96+
}
97+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//! This file contains functions related to codegenning MIR functions into gotoc
5+
6+
use super::cbmc::goto_program::{Expr, Stmt, Symbol};
7+
use super::metadata::*;
8+
use rustc_middle::mir::{HasLocalDecls, Local};
9+
use rustc_middle::ty::{self, Instance, TyS};
10+
use tracing::{debug, warn};
11+
12+
impl<'tcx> GotocCtx<'tcx> {
13+
fn codegen_declare_variables(&mut self) {
14+
let mir = self.current_fn().mir();
15+
let ldecls = mir.local_decls();
16+
ldecls.indices().for_each(|lc| {
17+
if Some(lc) == mir.spread_arg {
18+
// We have already added this local in the function prelude, so
19+
// skip adding it again here.
20+
return;
21+
}
22+
let base_name = self.codegen_var_base_name(&lc);
23+
let name = self.codegen_var_name(&lc);
24+
let ldata = &ldecls[lc];
25+
let t = self.monomorphize(ldata.ty);
26+
let t = self.codegen_ty(t);
27+
let loc = self.codegen_span2(&ldata.source_info.span);
28+
let sym =
29+
Symbol::variable(name, base_name, t, self.codegen_span2(&ldata.source_info.span));
30+
let sym_e = sym.to_expr();
31+
self.symbol_table.insert(sym);
32+
33+
// Index 0 represents the return value, which does not need to be
34+
// declared in the first block
35+
if lc.index() < 1 || lc.index() > mir.arg_count {
36+
self.current_fn_mut().push_onto_block(Stmt::decl(sym_e, None, loc));
37+
}
38+
});
39+
}
40+
41+
pub fn codegen_function(&mut self, instance: Instance<'tcx>) {
42+
self.set_current_fn(instance);
43+
let name = self.current_fn().name();
44+
let old_sym = self.symbol_table.lookup(&name).unwrap();
45+
assert!(old_sym.is_function());
46+
if old_sym.is_function_definition() {
47+
warn!("Double codegen of {:?}", old_sym);
48+
} else if self.should_skip_current_fn() {
49+
debug!("Skipping function {}", self.current_fn().readable_name());
50+
let loc = self.codegen_span2(&self.current_fn().mir().span);
51+
let body = Stmt::assert_false(
52+
&format!(
53+
"The function {} is not currently supported by RMC",
54+
self.current_fn().readable_name()
55+
),
56+
loc,
57+
);
58+
self.symbol_table.update_fn_declaration_with_definition(&name, body);
59+
} else {
60+
let mir = self.current_fn().mir();
61+
self.print_instance(instance, mir);
62+
let labels = self
63+
.current_fn()
64+
.mir()
65+
.basic_blocks()
66+
.indices()
67+
.map(|bb| format!("{:?}", bb))
68+
.collect();
69+
self.current_fn_mut().set_labels(labels);
70+
self.codegen_function_prelude();
71+
self.codegen_declare_variables();
72+
73+
mir.basic_blocks().iter_enumerated().for_each(|(bb, bbd)| self.codegen_block(bb, bbd));
74+
75+
let loc = self.codegen_span2(&mir.span);
76+
let stmts = self.current_fn_mut().extract_block();
77+
let body = Stmt::block(stmts, loc);
78+
self.symbol_table.update_fn_declaration_with_definition(&name, body);
79+
}
80+
self.reset_current_fn();
81+
}
82+
83+
/// MIR functions have a `spread_arg` field that specifies whether the
84+
/// final argument to the function is "spread" at the LLVM/codegen level
85+
/// from a tuple into its individual components. (Used for the "rust-
86+
/// call" ABI, necessary because dynamic trait closure cannot have an
87+
/// argument list in MIR that is both generic and variadic, so Rust
88+
/// allows a generic tuple).
89+
///
90+
/// If `spread_arg` is Some, then the wrapped value is the local that is
91+
/// to be "spread"/untupled. However, the MIR function body itself expects
92+
/// the tuple instead of the individual components, so we need to generate
93+
/// a function prelude that _retuples_, that is, writes the components
94+
/// back to the tuple local for use in the body.
95+
///
96+
/// See:
97+
/// https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Determine.20untupled.20closure.20args.20from.20Instance.3F
98+
fn codegen_function_prelude(&mut self) {
99+
let mir = self.current_fn().mir();
100+
if mir.spread_arg.is_none() {
101+
// No special tuple argument, no work to be done.
102+
return;
103+
}
104+
let spread_arg = mir.spread_arg.unwrap();
105+
let spread_data = &mir.local_decls()[spread_arg];
106+
let loc = self.codegen_span2(&spread_data.source_info.span);
107+
108+
// When we codegen the function signature elsewhere, we will codegen the
109+
// untupled version. So, the tuple argument itself needs to have a
110+
// symbol declared for it outside of the function signature, we do that
111+
// here.
112+
let tup_typ = self.codegen_ty(self.monomorphize(spread_data.ty));
113+
let tup_sym = Symbol::variable(
114+
self.codegen_var_name(&spread_arg),
115+
self.codegen_var_base_name(&spread_arg),
116+
tup_typ.clone(),
117+
loc.clone(),
118+
);
119+
self.symbol_table.insert(tup_sym.clone());
120+
121+
// Get the function signature from MIR, _before_ we untuple
122+
let fntyp = self.current_fn().instance().ty(self.tcx, ty::ParamEnv::reveal_all());
123+
let sig = match fntyp.kind() {
124+
ty::FnPtr(..) | ty::FnDef(..) => fntyp.fn_sig(self.tcx).skip_binder(),
125+
// Closures themselves will have their arguments already untupled,
126+
// see Zulip link above.
127+
ty::Closure(..) => unreachable!(
128+
"Unexpected `spread arg` set for closure, got: {:?}, {:?}",
129+
fntyp,
130+
self.current_fn().readable_name()
131+
),
132+
_ => unreachable!(
133+
"Expected function type for `spread arg` prelude, got: {:?}, {:?}",
134+
fntyp,
135+
self.current_fn().readable_name()
136+
),
137+
};
138+
139+
// Now that we have the tuple, write the individual component locals
140+
// back to it as a GotoC struct.
141+
let tupe = sig.inputs().last().unwrap();
142+
let args: Vec<&TyS<'tcx>> = match tupe.kind() {
143+
ty::Tuple(substs) => substs.iter().map(|s| s.expect_ty()).collect(),
144+
_ => unreachable!("a function's spread argument must be a tuple"),
145+
};
146+
147+
// Convert each arg to a GotoC expression.
148+
let mut arg_exprs = Vec::new();
149+
let starting_idx = sig.inputs().len();
150+
for (arg_i, arg_t) in args.iter().enumerate() {
151+
// The components come at the end, so offset by the untupled length.
152+
let lc = Local::from_usize(arg_i + starting_idx);
153+
let (name, base_name) = self.codegen_spread_arg_name(&lc);
154+
let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc.clone());
155+
self.symbol_table.insert(sym.clone());
156+
arg_exprs.push(sym.to_expr());
157+
}
158+
159+
// Finally, combine the expression into a struct.
160+
let tuple_expr = Expr::struct_expr_from_values(tup_typ, arg_exprs, &self.symbol_table)
161+
.with_location(loc.clone());
162+
self.current_fn_mut().push_onto_block(Stmt::decl(tup_sym.to_expr(), Some(tuple_expr), loc));
163+
}
164+
165+
pub fn declare_function(&mut self, instance: Instance<'tcx>) {
166+
debug!("declaring {}; {:?}", instance, instance);
167+
self.set_current_fn(instance);
168+
self.ensure(&self.current_fn().name(), |ctx, fname| {
169+
let mir = ctx.current_fn().mir();
170+
Symbol::function(
171+
fname,
172+
ctx.fn_typ(),
173+
None,
174+
Some(ctx.current_fn().readable_name().to_string()),
175+
ctx.codegen_span2(&mir.span),
176+
)
177+
});
178+
self.reset_current_fn();
179+
}
180+
}

0 commit comments

Comments
 (0)