Skip to content

Commit e282561

Browse files
fzaiserfzaiser
authored
Produce more pretty names (rust-lang#1310)
1 parent 13f7a98 commit e282561

File tree

21 files changed

+175
-110
lines changed

21 files changed

+175
-110
lines changed

‎cprover_bindings/src/goto_program/symbol.rs

Lines changed: 23 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -104,13 +104,20 @@ impl Symbol {
104104

105105
/// The symbol that defines the type of the struct or union.
106106
/// For a struct foo this is the symbol "tag-foo" that maps to the type struct foo.
107-
pub fn aggr_ty<T: Into<InternedString>>(t: Type, pretty_name: Option<T>) -> Symbol {
107+
pub fn aggr_ty<T: Into<InternedString>>(t: Type, pretty_name: T) -> Symbol {
108108
//TODO take location
109-
let pretty_name = pretty_name.intern();
109+
let pretty_name = pretty_name.into();
110110
let base_name = t.tag().unwrap();
111111
let name = aggr_tag(base_name);
112-
Symbol::new(name, Location::none(), t, SymbolValues::None, Some(base_name), pretty_name)
113-
.with_is_type(true)
112+
Symbol::new(
113+
name,
114+
Location::none(),
115+
t,
116+
SymbolValues::None,
117+
Some(base_name),
118+
Some(pretty_name),
119+
)
120+
.with_is_type(true)
114121
}
115122

116123
pub fn builtin_function<T: Into<InternedString>>(
@@ -123,7 +130,7 @@ impl Symbol {
123130
name,
124131
Type::code_with_unnamed_parameters(param_types, return_type),
125132
None,
126-
None::<InternedString>,
133+
name,
127134
Location::builtin_function(name, None),
128135
)
129136
}
@@ -150,18 +157,18 @@ impl Symbol {
150157
name: T,
151158
typ: Type,
152159
body: Option<Stmt>,
153-
pretty_name: Option<U>,
160+
pretty_name: U,
154161
loc: Location,
155162
) -> Symbol {
156163
let name = name.into();
157-
let pretty_name = pretty_name.intern();
164+
let pretty_name = pretty_name.into();
158165
Symbol::new(
159166
name.to_string(),
160167
loc,
161168
typ,
162169
body.map_or(SymbolValues::None, SymbolValues::Stmt),
163170
Some(name),
164-
pretty_name,
171+
Some(pretty_name),
165172
)
166173
.with_is_lvalue(true)
167174
}
@@ -209,7 +216,7 @@ impl Symbol {
209216

210217
pub fn struct_type<T: Into<InternedString>>(
211218
name: T,
212-
pretty_name: Option<InternedString>,
219+
pretty_name: InternedString,
213220
components: Vec<DatatypeComponent>,
214221
) -> Symbol {
215222
let name = name.into();
@@ -218,35 +225,35 @@ impl Symbol {
218225

219226
pub fn union_type<T: Into<InternedString>, U: Into<InternedString>>(
220227
name: T,
221-
pretty_name: Option<U>,
228+
pretty_name: U,
222229
components: Vec<DatatypeComponent>,
223230
) -> Symbol {
224231
let name = name.into();
225-
let pretty_name = pretty_name.intern();
232+
let pretty_name = pretty_name.into();
226233
Symbol::aggr_ty(Type::union_type(name, components), pretty_name)
227234
}
228235

229-
pub fn empty_struct(name: InternedString, pretty_name: Option<InternedString>) -> Symbol {
236+
pub fn empty_struct(name: InternedString, pretty_name: InternedString) -> Symbol {
230237
Symbol::aggr_ty(Type::empty_struct(name), pretty_name)
231238
}
232239

233-
pub fn empty_union(name: InternedString, pretty_name: Option<InternedString>) -> Symbol {
240+
pub fn empty_union(name: InternedString, pretty_name: InternedString) -> Symbol {
234241
Symbol::aggr_ty(Type::empty_union(name), pretty_name)
235242
}
236243

237244
pub fn incomplete_struct<T: Into<InternedString>, U: Into<InternedString>>(
238245
name: T,
239-
pretty_name: Option<U>,
246+
pretty_name: U,
240247
) -> Symbol {
241248
Symbol::aggr_ty(Type::incomplete_struct(name), pretty_name)
242249
}
243250

244251
pub fn incomplete_union<T: Into<InternedString>, U: Into<InternedString>>(
245252
name: T,
246-
pretty_name: Option<U>,
253+
pretty_name: U,
247254
) -> Symbol {
248255
let name = name.into();
249-
let pretty_name = pretty_name.intern();
256+
let pretty_name = pretty_name.into();
250257
Symbol::aggr_ty(Type::incomplete_union(name), pretty_name)
251258
}
252259
}

‎cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -255,7 +255,7 @@ impl Transformer for ExprTransformer {
255255
"main",
256256
Type::code(Vec::new(), Type::CInteger(CIntType::Int)),
257257
Some(Stmt::block(main_body, Location::none())),
258-
Some("main"),
258+
"main",
259259
Location::none(),
260260
);
261261

‎cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ impl Transformer for NondetTransformer {
127127

128128
// Add function to symbol table
129129
let func_sym =
130-
Symbol::function(&identifier, typ, Some(body), Some(&identifier), Location::none());
130+
Symbol::function(&identifier, typ, Some(body), &identifier, Location::none());
131131
self.mut_symbol_table().insert(func_sym);
132132
}
133133
}

‎cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -247,7 +247,7 @@ mod tests {
247247

248248
let struct_type = Symbol::struct_type(
249249
"s",
250-
None,
250+
"s".into(),
251251
vec![
252252
DatatypeComponent::field("a", Type::float()),
253253
DatatypeComponent::padding("b", 4),
@@ -283,7 +283,7 @@ mod tests {
283283

284284
let union_type = Symbol::union_type(
285285
"u",
286-
crate::NO_PRETTY_NAME,
286+
"u",
287287
vec![
288288
DatatypeComponent::field("a", Type::float()),
289289
DatatypeComponent::field("c", Type::double()),
@@ -330,7 +330,7 @@ mod tests {
330330
&name,
331331
Type::code_with_unnamed_parameters(vec![], Type::empty()),
332332
Some(body),
333-
crate::NO_PRETTY_NAME,
333+
&name,
334334
Location::none(),
335335
));
336336
curr_var += 1;

‎cprover_bindings/src/lib.rs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,3 @@ pub use irep::serialize;
3838
pub use machine_model::{MachineModel, RoundingMode};
3939
mod cbmc_string;
4040
pub use cbmc_string::{InternString, InternStringOption, InternedString};
41-
42-
// Rust has difficulty resolving types for None option values: this gives rustc a hint.
43-
pub const NO_PRETTY_NAME: Option<InternedString> = None;

‎kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ use kani_metadata::HarnessMetadata;
1111
use rustc_ast::ast;
1212
use rustc_ast::{Attribute, LitKind};
1313
use rustc_middle::mir::{HasLocalDecls, Local};
14+
use rustc_middle::ty::print::with_no_trimmed_paths;
1415
use rustc_middle::ty::{self, Instance};
1516
use std::collections::BTreeMap;
1617
use std::convert::TryInto;
@@ -20,7 +21,11 @@ use tracing::{debug, info_span};
2021
/// Utility to skip functions that can't currently be successfully codgenned.
2122
impl<'tcx> GotocCtx<'tcx> {
2223
fn should_skip_current_fn(&self) -> bool {
23-
match self.current_fn().readable_name() {
24+
let current_fn_name =
25+
with_no_trimmed_paths!(self.tcx.def_path_str(self.current_fn().instance().def_id()));
26+
// We cannot use self.current_fn().readable_name() because it gives the monomorphized type, which is more difficult to match on.
27+
// Ideally we should not rely on the pretty-printed name here. Tracked here: https://github.com/model-checking/kani/issues/1374
28+
match current_fn_name.as_str() {
2429
// https://github.com/model-checking/kani/issues/202
2530
"fmt::ArgumentV1::<'a>::as_usize" => true,
2631
// https://github.com/model-checking/kani/issues/282
@@ -233,7 +238,7 @@ impl<'tcx> GotocCtx<'tcx> {
233238
fname,
234239
ctx.fn_typ(),
235240
None,
236-
Some(ctx.current_fn().readable_name()),
241+
ctx.current_fn().readable_name(),
237242
ctx.codegen_span(&mir.span),
238243
)
239244
});

‎kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 19 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
44
use crate::codegen_cprover_gotoc::GotocCtx;
55
use crate::unwrap_or_return_codegen_unimplemented;
66
use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, Type};
7-
use cbmc::NO_PRETTY_NAME;
87
use rustc_ast::ast::Mutability;
98
use rustc_middle::mir::interpret::{
109
read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar,
@@ -317,6 +316,7 @@ impl<'tcx> GotocCtx<'tcx> {
317316

318317
fn codegen_direct_literal(&mut self, ty: Ty<'tcx>, init: Expr) -> Expr {
319318
let func_name = format!("gen-{}:direct", self.ty_mangled_name(ty));
319+
let pretty_name = format!("init_direct::<{}>", self.ty_pretty_name(ty));
320320
let cgt = self.codegen_ty(ty);
321321
self.ensure(&func_name, |tcx, _| {
322322
let target_ty = init.typ().clone(); // N
@@ -333,7 +333,7 @@ impl<'tcx> GotocCtx<'tcx> {
333333
&func_name,
334334
Type::code(vec![param.to_function_parameter()], cgt),
335335
Some(Stmt::block(body, Location::none())),
336-
NO_PRETTY_NAME,
336+
pretty_name,
337337
Location::none(),
338338
)
339339
});
@@ -500,28 +500,26 @@ impl<'tcx> GotocCtx<'tcx> {
500500
/// Codegen alloc as a static global variable with initial value
501501
fn codegen_alloc_in_memory(&mut self, alloc: &'tcx Allocation, name: String) {
502502
debug!("codegen_alloc_in_memory name: {}", name);
503+
let struct_name = &format!("{}::struct", name);
503504

504505
// The declaration of a static variable may have one type and the constant initializer for
505506
// a static variable may have a different type. This is because Rust uses bit patterns for
506507
// initializers. For example, for a boolean static variable, the variable will have type
507508
// CBool and the initializer will be a single byte (a one-character array) representing the
508509
// bit pattern for the boolean value.
509-
let alloc_typ_ref =
510-
self.ensure_struct(&format!("{}::struct", name), NO_PRETTY_NAME, |ctx, _| {
511-
ctx.codegen_allocation_data(alloc)
512-
.iter()
513-
.enumerate()
514-
.map(|(i, d)| match d {
515-
AllocData::Bytes(bytes) => DatatypeComponent::field(
516-
&i.to_string(),
517-
Type::unsigned_int(8).array_of(bytes.len()),
518-
),
519-
AllocData::Expr(e) => {
520-
DatatypeComponent::field(&i.to_string(), e.typ().clone())
521-
}
522-
})
523-
.collect()
524-
});
510+
let alloc_typ_ref = self.ensure_struct(&struct_name, &struct_name, |ctx, _| {
511+
ctx.codegen_allocation_data(alloc)
512+
.iter()
513+
.enumerate()
514+
.map(|(i, d)| match d {
515+
AllocData::Bytes(bytes) => DatatypeComponent::field(
516+
&i.to_string(),
517+
Type::unsigned_int(8).array_of(bytes.len()),
518+
),
519+
AllocData::Expr(e) => DatatypeComponent::field(&i.to_string(), e.typ().clone()),
520+
})
521+
.collect()
522+
});
525523

526524
// The global static variable may not be in the symbol table if we are dealing
527525
// with a literal that can be statically allocated.
@@ -606,6 +604,7 @@ impl<'tcx> GotocCtx<'tcx> {
606604
fn codegen_niche_literal(&mut self, ty: Ty<'tcx>, offset: usize, init: Expr) -> Expr {
607605
let cgt = self.codegen_ty(ty);
608606
let fname = self.codegen_niche_init_name(ty);
607+
let pretty_name = format!("init_niche<{}>", self.ty_pretty_name(ty));
609608
self.ensure(&fname, |tcx, _| {
610609
let target_ty = init.typ().clone(); // N
611610
let param = tcx.gen_function_local_variable(1, &fname, target_ty.clone());
@@ -620,7 +619,7 @@ impl<'tcx> GotocCtx<'tcx> {
620619
&fname,
621620
Type::code(vec![param.to_function_parameter()], cgt),
622621
Some(Stmt::block(body, Location::none())),
623-
NO_PRETTY_NAME,
622+
pretty_name,
624623
Location::none(),
625624
)
626625
});
@@ -642,7 +641,7 @@ impl<'tcx> GotocCtx<'tcx> {
642641
&func,
643642
funct.clone(),
644643
None,
645-
Some(ctx.readable_instance_name(instance)),
644+
ctx.readable_instance_name(instance),
646645
Location::none(),
647646
)
648647
.with_is_extern(true)

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ use crate::unwrap_or_return_codegen_unimplemented;
88
use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
99
use cbmc::utils::BUG_REPORT_URL;
1010
use cbmc::MachineModel;
11-
use cbmc::NO_PRETTY_NAME;
1211
use cbmc::{btree_string_map, InternString, InternedString};
1312
use num::bigint::BigInt;
1413
use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
@@ -211,6 +210,7 @@ impl<'tcx> GotocCtx<'tcx> {
211210
res_ty: Ty<'tcx>,
212211
) -> Expr {
213212
let func_name = format!("gen-repeat<{}>", self.ty_mangled_name(res_ty));
213+
let pretty_name = format!("init_array_repeat<{}>", self.ty_pretty_name(res_ty));
214214
self.ensure(&func_name, |tcx, _| {
215215
let paramt = tcx.codegen_ty(tcx.operand_ty(op));
216216
let res_t = tcx.codegen_ty(res_ty);
@@ -241,7 +241,7 @@ impl<'tcx> GotocCtx<'tcx> {
241241
&func_name,
242242
Type::code(vec![inp.to_function_parameter()], res_t),
243243
Some(Stmt::block(body, Location::none())),
244-
NO_PRETTY_NAME,
244+
&pretty_name,
245245
Location::none(),
246246
)
247247
});
@@ -851,7 +851,9 @@ impl<'tcx> GotocCtx<'tcx> {
851851
// We skip an entire submodule of the standard library, so drop is missing
852852
// for it. Build and insert a function that just calls an unimplemented block
853853
// to maintain soundness.
854-
let drop_sym_name = format!("{}_unimplemented", self.symbol_name(drop_instance));
854+
let drop_sym_name = format!("drop_unimplemented_{}", self.symbol_name(drop_instance));
855+
let pretty_name =
856+
format!("drop_unimplemented<{}>", self.readable_instance_name(drop_instance));
855857
let drop_sym = self.ensure(&drop_sym_name, |ctx, name| {
856858
// Function body
857859
let unimplemented = ctx
@@ -878,7 +880,7 @@ impl<'tcx> GotocCtx<'tcx> {
878880
name,
879881
Type::code(vec![param_sym.to_function_parameter()], Type::empty()),
880882
Some(Stmt::block(vec![unimplemented], Location::none())),
881-
NO_PRETTY_NAME,
883+
pretty_name,
882884
Location::none(),
883885
)
884886
});

0 commit comments

Comments
 (0)