Skip to content

Commit bde0291

Browse files
NadrierilNadrieril
authored
Merge pull request #578 from Nadrieril/display-item-vis
Display item visibility in pretty output
2 parents d250df8 + 94f3aab commit bde0291

File tree

92 files changed

+1977
-1982
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

92 files changed

+1977
-1982
lines changed

‎charon/src/pretty/fmt_with_ctx.rs

Lines changed: 49 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -501,6 +501,7 @@ where
501501

502502
impl<C> FmtWithCtx<C> for FunDecl
503503
where
504+
C: AstFormatter,
504505
// For the signature
505506
C: for<'a> SetGenerics<'a>,
506507
for<'a> <C as SetGenerics<'a>>::C: AstFormatter,
@@ -509,18 +510,15 @@ where
509510
for<'a, 'b> <<C as SetGenerics<'a>>::C as SetLocals<'b>>::C: AstFormatter,
510511
{
511512
fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
512-
// Update the context
513-
let ctx = &ctx.set_generics(&self.signature.generics);
514-
515-
// Unsafe keyword
516-
let unsafe_kw = if self.signature.is_unsafe {
517-
"unsafe ".to_string()
513+
let keyword = if self.signature.is_unsafe {
514+
"unsafe fn"
518515
} else {
519-
"".to_string()
516+
"fn"
520517
};
518+
let intro = self.item_meta.fmt_item_intro(ctx, tab, keyword);
521519

522-
// Function name
523-
let name = self.item_meta.name.fmt_with_ctx(ctx);
520+
// Update the context
521+
let ctx = &ctx.set_generics(&self.signature.generics);
524522

525523
// Generic parameters
526524
let (params, preds) = self
@@ -558,7 +556,7 @@ where
558556
};
559557

560558
// Put everything together
561-
format!("{tab}{unsafe_kw}fn {name}{params}({args}){ret_ty}{preds}{body}",)
559+
format!("{intro}{params}({args}){ret_ty}{preds}{body}",)
562560
}
563561
}
564562

@@ -579,6 +577,8 @@ where
579577
for<'a, 'b, 'c> <<C as SetGenerics<'a>>::C as SetLocals<'b>>::C: AstFormatter,
580578
{
581579
fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
580+
let intro = self.item_meta.fmt_item_intro(ctx, tab, "global");
581+
582582
// Update the context with the generics
583583
let ctx = &ctx.set_generics(&self.generics);
584584

@@ -594,11 +594,10 @@ where
594594
};
595595

596596
// Decl name
597-
let name = self.item_meta.name.fmt_with_ctx(ctx);
598597
let initializer = ctx.format_object(self.init);
599598

600599
// Put everything together
601-
format!("{tab}global {name}{params}: {ty}{preds}{eq_space}= {initializer}()")
600+
format!("{intro}{params}: {ty}{preds}{eq_space}= {initializer}()")
602601
}
603602
}
604603

@@ -616,6 +615,18 @@ impl<C: AstFormatter> FmtWithCtx<C> for ImplElem {
616615
}
617616
}
618617

618+
impl ItemMeta {
619+
/// Format the start of an item definition, up to the name.
620+
pub fn fmt_item_intro<C>(&self, ctx: &C, tab: &str, keyword: &str) -> String
621+
where
622+
C: AstFormatter,
623+
{
624+
let name = self.name.fmt_with_ctx(ctx);
625+
let vis = if self.attr_info.public { "pub " } else { "" };
626+
format!("{tab}{vis}{keyword} {name}")
627+
}
628+
}
629+
619630
impl<C: AstFormatter> FmtWithCtx<C> for LiteralTy {
620631
fn fmt_with_ctx(&self, _ctx: &C) -> String {
621632
match self {
@@ -1192,10 +1203,11 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitClause {
11921203

11931204
impl<C: AstFormatter> FmtWithCtx<C> for TraitDecl {
11941205
fn fmt_with_ctx(&self, ctx: &C) -> String {
1206+
let intro = self.item_meta.fmt_item_intro(ctx, "", "trait");
1207+
11951208
// Update the context
11961209
let ctx = &ctx.set_generics(&self.generics);
11971210

1198-
let name = self.item_meta.name.fmt_with_ctx(ctx);
11991211
let (generics, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "");
12001212

12011213
let items = {
@@ -1242,7 +1254,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitDecl {
12421254
}
12431255
};
12441256

1245-
format!("trait {name}{generics}{clauses}{items}")
1257+
format!("{intro}{generics}{clauses}{items}")
12461258
}
12471259
}
12481260

@@ -1256,10 +1268,11 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitDeclRef {
12561268

12571269
impl<C: AstFormatter> FmtWithCtx<C> for TraitImpl {
12581270
fn fmt_with_ctx(&self, ctx: &C) -> String {
1271+
let intro = self.item_meta.fmt_item_intro(ctx, "", "impl");
1272+
12591273
// Update the context
12601274
let ctx = &ctx.set_generics(&self.generics);
12611275

1262-
let name = self.item_meta.name.fmt_with_ctx(ctx);
12631276
let (generics, clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, "");
12641277

12651278
let items = {
@@ -1306,7 +1319,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitImpl {
13061319
};
13071320

13081321
let impl_trait = self.impl_trait.fmt_with_ctx(ctx);
1309-
format!("impl{generics} {name}{generics} : {impl_trait}{clauses}{items}")
1322+
format!("{intro}{generics} : {impl_trait}{clauses}{items}")
13101323
}
13111324
}
13121325

@@ -1437,74 +1450,56 @@ impl<C: AstFormatter> FmtWithCtx<C> for Ty {
14371450

14381451
impl<C: AstFormatter> FmtWithCtx<C> for TypeDecl {
14391452
fn fmt_with_ctx(&self, ctx: &C) -> String {
1453+
let keyword = match &self.kind {
1454+
TypeDeclKind::Struct(..) => "struct",
1455+
TypeDeclKind::Union(..) => "union",
1456+
TypeDeclKind::Enum(..) => "enum",
1457+
TypeDeclKind::Alias(..) => "type",
1458+
TypeDeclKind::Opaque | TypeDeclKind::Error(..) => "opaque type",
1459+
};
1460+
let intro = self.item_meta.fmt_item_intro(ctx, "", keyword);
1461+
14401462
let ctx = &ctx.set_generics(&self.generics);
14411463

14421464
let (params, preds) = self.generics.fmt_with_ctx_with_trait_clauses(ctx, " ");
14431465
// Predicates
1444-
let eq_space = if !self.generics.has_predicates() {
1466+
let nl_or_space = if !self.generics.has_predicates() {
14451467
" ".to_string()
14461468
} else {
14471469
"\n ".to_string()
14481470
};
14491471

1450-
match &self.kind {
1472+
let contents = match &self.kind {
14511473
TypeDeclKind::Struct(fields) => {
14521474
if !fields.is_empty() {
14531475
let fields = fields
14541476
.iter()
14551477
.map(|f| format!("\n {},", f.fmt_with_ctx(ctx)))
14561478
.format("");
1457-
format!(
1458-
"struct {}{params}{preds}{eq_space}=\n{{{fields}\n}}",
1459-
self.item_meta.name.fmt_with_ctx(ctx)
1460-
)
1479+
format!("{nl_or_space}=\n{{{fields}\n}}")
14611480
} else {
1462-
format!(
1463-
"struct {}{params}{preds}{eq_space}= {{}}",
1464-
self.item_meta.name.fmt_with_ctx(ctx)
1465-
)
1481+
format!("{nl_or_space}= {{}}")
14661482
}
14671483
}
14681484
TypeDeclKind::Union(fields) => {
14691485
let fields = fields
14701486
.iter()
14711487
.map(|f| format!("\n {},", f.fmt_with_ctx(ctx)))
14721488
.format("");
1473-
format!(
1474-
"union {}{params}{preds}{eq_space}=\n{{{fields}\n}}",
1475-
self.item_meta.name.fmt_with_ctx(ctx)
1476-
)
1489+
format!("{nl_or_space}=\n{{{fields}\n}}")
14771490
}
14781491
TypeDeclKind::Enum(variants) => {
14791492
let variants = variants
14801493
.iter()
14811494
.map(|v| format!("| {}", v.fmt_with_ctx(ctx)))
14821495
.format("\n");
1483-
format!(
1484-
"enum {}{params}{preds}{eq_space}=\n{variants}\n",
1485-
self.item_meta.name.fmt_with_ctx(ctx)
1486-
)
1496+
format!("{nl_or_space}=\n{variants}\n")
14871497
}
1488-
TypeDeclKind::Alias(ty) => {
1489-
format!(
1490-
"type {}{params}{preds} = {}",
1491-
self.item_meta.name.fmt_with_ctx(ctx),
1492-
ty.fmt_with_ctx(ctx),
1493-
)
1494-
}
1495-
TypeDeclKind::Opaque => {
1496-
format!(
1497-
"opaque type {}{params}{preds}",
1498-
self.item_meta.name.fmt_with_ctx(ctx)
1499-
)
1500-
}
1501-
TypeDeclKind::Error(msg) => {
1502-
format!(
1503-
"opaque type {}{params}{preds} = ERROR({msg})",
1504-
self.item_meta.name.fmt_with_ctx(ctx),
1505-
)
1506-
}
1507-
}
1498+
TypeDeclKind::Alias(ty) => format!(" = {}", ty.fmt_with_ctx(ctx)),
1499+
TypeDeclKind::Opaque => format!(""),
1500+
TypeDeclKind::Error(msg) => format!(" = ERROR({msg})"),
1501+
};
1502+
format!("{intro}{params}{preds}{contents}")
15081503
}
15091504
}
15101505

‎charon/tests/cargo/build-script.out

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
# Final LLBC before serialization:
22

3-
fn test_cargo_build_script::FOO() -> u8
3+
pub fn test_cargo_build_script::FOO() -> u8
44
{
55
let @0: u8; // return
66

77
@0 := const (42 : u8)
88
return
99
}
1010

11-
global test_cargo_build_script::FOO: u8 = test_cargo_build_script::FOO()
11+
pub global test_cargo_build_script::FOO: u8 = test_cargo_build_script::FOO()
1212

1313
fn test_cargo_build_script::main()
1414
{

‎charon/tests/cargo/dependencies.out

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,11 @@ fn test_cargo_dependencies::silly_incr::closure(@1: (), @2: u32) -> u32
1313
return
1414
}
1515

16-
trait core::marker::Sized<Self>
16+
pub trait core::marker::Sized<Self>
1717

18-
trait core::marker::Tuple<Self>
18+
pub trait core::marker::Tuple<Self>
1919

20-
trait core::ops::function::FnOnce<Self, Args>
20+
pub trait core::ops::function::FnOnce<Self, Args>
2121
{
2222
parent_clause0 : [@TraitClause0]: core::marker::Sized<Args>
2323
parent_clause1 : [@TraitClause1]: core::marker::Tuple<Args>
@@ -26,7 +26,7 @@ trait core::ops::function::FnOnce<Self, Args>
2626
fn call_once = core::ops::function::FnOnce::call_once<Self, Args>
2727
}
2828

29-
fn take_mut::take<'_0, T, F>(@1: &'_0 mut (T), @2: F)
29+
pub fn take_mut::take<'_0, T, F>(@1: &'_0 mut (T), @2: F)
3030
where
3131
[@TraitClause0]: core::marker::Sized<T>,
3232
[@TraitClause1]: core::marker::Sized<F>,
@@ -52,21 +52,21 @@ fn test_cargo_dependencies::silly_incr<'_0>(@1: &'_0 mut (u32))
5252
return
5353
}
5454

55-
enum core::panicking::AssertKind =
55+
pub enum core::panicking::AssertKind =
5656
| Eq()
5757
| Ne()
5858
| Match()
5959

6060

61-
enum core::option::Option<T>
61+
pub enum core::option::Option<T>
6262
where
6363
[@TraitClause0]: core::marker::Sized<T>,
6464
=
6565
| None()
6666
| Some(T)
6767

6868

69-
opaque type core::fmt::Arguments<'a>
69+
pub opaque type core::fmt::Arguments<'a>
7070
where
7171
'a : 'a,
7272

@@ -144,7 +144,7 @@ fn test_cargo_dependencies::main()
144144
return
145145
}
146146

147-
fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
147+
pub fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
148148

149149

150150

‎charon/tests/cargo/toml.out

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
# Final LLBC before serialization:
22

3-
trait core::marker::Sized<Self>
3+
pub trait core::marker::Sized<Self>
44

5-
enum core::option::Option<T>
5+
pub enum core::option::Option<T>
66
where
77
[@TraitClause0]: core::marker::Sized<T>,
88
=
99
| None()
1010
| Some(T)
1111

1212

13-
fn core::option::{core::option::Option<T>[@TraitClause0]}::is_some<'_0, T>(@1: &'_0 (core::option::Option<T>[@TraitClause0])) -> bool
13+
pub fn core::option::{core::option::Option<T>[@TraitClause0]}::is_some<'_0, T>(@1: &'_0 (core::option::Option<T>[@TraitClause0])) -> bool
1414
where
1515
[@TraitClause0]: core::marker::Sized<T>,
1616
{

‎charon/tests/cargo/unsafe_.out

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
# Final LLBC before serialization:
22

3-
opaque type core::fmt::Arguments<'a>
3+
pub opaque type core::fmt::Arguments<'a>
44
where
55
'a : 'a,
66

7-
fn core::fmt::{core::fmt::Arguments<'a>}#2::new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : usize>)) -> core::fmt::Arguments<'a>
7+
pub fn core::fmt::{core::fmt::Arguments<'a>}#2::new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : usize>)) -> core::fmt::Arguments<'a>
88

9-
fn std::io::stdio::_print<'_0>(@1: core::fmt::Arguments<'_0>)
9+
pub fn std::io::stdio::_print<'_0>(@1: core::fmt::Arguments<'_0>)
1010

1111
fn unsafe::main()
1212
{

‎charon/tests/cargo/workspace.out

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
# Final LLBC before serialization:
22

3-
fn crate1::random_number() -> u32
3+
pub fn crate1::random_number() -> u32
44
{
55
let @0: u32; // return
66

77
@0 := const (4 : u32)
88
return
99
}
1010

11-
fn crate2::extra_random_number() -> u32
11+
pub fn crate2::extra_random_number() -> u32
1212
{
1313
let @0: u32; // return
1414
let @1: u32; // anonymous local

0 commit comments

Comments
 (0)