Skip to content

Commit 65c52fb

Browse files
danielsntedinski
authored andcommitted
Use vector_map instead of btree_map in irep to save memory (rust-lang#620)
* Use vector_map instead of btree_map in irep to save memory * Implement Serde serializer for the vec map * remove to_json file
1 parent 37b4902 commit 65c52fb

File tree

10 files changed

+128
-130
lines changed

10 files changed

+128
-130
lines changed

Cargo.lock

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -506,6 +506,7 @@ dependencies = [
506506
"smallvec",
507507
"snap",
508508
"tracing",
509+
"vector-map",
509510
]
510511

511512
[[package]]
@@ -774,6 +775,17 @@ dependencies = [
774775
"winapi",
775776
]
776777

778+
[[package]]
779+
name = "contracts"
780+
version = "0.4.0"
781+
source = "registry+https://github.com/rust-lang/crates.io-index"
782+
checksum = "c9424f2ca1e42776615720e5746eed6efa19866fdbaac2923ab51c294ac4d1f2"
783+
dependencies = [
784+
"proc-macro2",
785+
"quote",
786+
"syn",
787+
]
788+
777789
[[package]]
778790
name = "core"
779791
version = "0.0.0"
@@ -5831,6 +5843,16 @@ version = "0.8.2"
58315843
source = "registry+https://github.com/rust-lang/crates.io-index"
58325844
checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191"
58335845

5846+
[[package]]
5847+
name = "vector-map"
5848+
version = "1.0.1"
5849+
source = "registry+https://github.com/rust-lang/crates.io-index"
5850+
checksum = "550f72ae94a45c0e2139188709e6c4179f0b5ff9bdaa435239ad19048b0cd68c"
5851+
dependencies = [
5852+
"contracts",
5853+
"rand 0.7.3",
5854+
]
5855+
58345856
[[package]]
58355857
name = "vergen"
58365858
version = "5.1.0"

compiler/cbmc/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ num = "0.4.0"
1919
serde = {version = "1", features = ["derive"]}
2020
snap = "1"
2121
tracing = "0.1"
22+
vector-map = "1.0.1"
2223
rustc_middle = { path = "../rustc_middle" }
2324
rustc-demangle = "0.1.21"
2425
rustc_arena = { path = "../rustc_arena" }

compiler/cbmc/src/irep/irep.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,17 +6,17 @@ use super::super::goto_program::{Location, Type};
66
use super::super::MachineModel;
77
use super::{IrepId, ToIrep};
88
use num::BigInt;
9-
use std::collections::BTreeMap;
109
use std::fmt::Debug;
10+
use vector_map::VecMap;
1111

1212
/// The CBMC serialization format for goto-programs.
1313
/// CBMC implementation code is at:
1414
/// https://github.com/diffblue/cbmc/blob/develop/src/util/irep.h
15-
#[derive(Clone, Debug, PartialEq, Eq)]
15+
#[derive(Clone, Debug, PartialEq)]
1616
pub struct Irep {
1717
pub id: IrepId,
1818
pub sub: Vec<Irep>,
19-
pub named_sub: BTreeMap<IrepId, Irep>,
19+
pub named_sub: VecMap<IrepId, Irep>,
2020
}
2121

2222
/// Getters
@@ -108,7 +108,7 @@ impl Irep {
108108
}
109109

110110
pub fn just_id(id: IrepId) -> Irep {
111-
Irep { id: id, sub: Vec::new(), named_sub: BTreeMap::new() }
111+
Irep { id: id, sub: Vec::new(), named_sub: VecMap::new() }
112112
}
113113

114114
pub fn just_int_id<T>(i: T) -> Irep
@@ -117,7 +117,7 @@ impl Irep {
117117
{
118118
Irep::just_id(IrepId::from_int(i))
119119
}
120-
pub fn just_named_sub(named_sub: BTreeMap<IrepId, Irep>) -> Irep {
120+
pub fn just_named_sub(named_sub: VecMap<IrepId, Irep>) -> Irep {
121121
Irep { id: IrepId::EmptyString, sub: vec![], named_sub: named_sub }
122122
}
123123

@@ -126,7 +126,7 @@ impl Irep {
126126
}
127127

128128
pub fn just_sub(sub: Vec<Irep>) -> Irep {
129-
Irep { id: IrepId::EmptyString, sub: sub, named_sub: BTreeMap::new() }
129+
Irep { id: IrepId::EmptyString, sub: sub, named_sub: VecMap::new() }
130130
}
131131

132132
pub fn nil() -> Irep {

compiler/cbmc/src/irep/mod.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ pub mod serialize;
2020
mod symbol;
2121
mod symbol_table;
2222
mod to_irep;
23-
mod to_json;
2423

2524
pub use irep::Irep;
2625
pub use irep_id::IrepId;

compiler/cbmc/src/irep/serialize.rs

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,23 @@
44
use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
55
use serde::ser::{SerializeMap, Serializer};
66
use serde::Serialize;
7+
use vector_map::VecMap;
8+
9+
// Wrapper type to allow impl of trait (otherwise impossible when both trait and type are external).
10+
struct MapWrapper<'a, K, V>(&'a VecMap<K, V>);
11+
12+
impl<K: serde::Serialize, V: serde::Serialize> Serialize for MapWrapper<'_, K, V> {
13+
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
14+
where
15+
S: Serializer,
16+
{
17+
let mut obj = serializer.serialize_map(None)?;
18+
for (k, v) in self.0 {
19+
obj.serialize_entry(k, v)?;
20+
}
21+
obj.end()
22+
}
23+
}
724

825
impl Serialize for Irep {
926
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
@@ -16,7 +33,7 @@ impl Serialize for Irep {
1633
obj.serialize_entry("sub", &self.sub)?;
1734
}
1835
if !self.named_sub.is_empty() {
19-
obj.serialize_entry("namedSub", &self.named_sub)?;
36+
obj.serialize_entry("namedSub", &MapWrapper(&self.named_sub))?;
2037
}
2138
obj.end()
2239
}

compiler/cbmc/src/irep/symbol.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use super::Irep;
55
/// A direct implementation of the CBMC serilization format for symbols implemented in
66
/// https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h
77
// TODO: do we want these members to be public?
8-
#[derive(Clone, Debug, PartialEq, Eq)]
8+
#[derive(Clone, Debug, PartialEq)]
99
pub struct Symbol {
1010
pub typ: Irep,
1111
pub value: Irep,

compiler/cbmc/src/irep/symbol_table.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use std::collections::BTreeMap;
55

66
/// A direct implementation of the CBMC serilization format for symbol tables implemented in
77
/// https://github.com/diffblue/cbmc/blob/develop/src/util/symbol_table.h
8-
#[derive(Debug, PartialEq, Eq)]
8+
#[derive(Debug, PartialEq)]
99
pub struct SymbolTable {
1010
pub symbol_table: BTreeMap<String, Symbol>,
1111
}

0 commit comments

Comments
 (0)