Skip to content
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions Cargo.lock
Original file line number Diff line number Diff line change
Expand Up @@ -190,6 +190,12 @@ dependencies = [
"which",
]

[[package]]
name = "byteorder"
version = "1.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"

[[package]]
name = "bytes"
version = "1.10.1"
Expand Down Expand Up @@ -406,6 +412,7 @@ dependencies = [
name = "cprover_bindings"
version = "0.62.0"
dependencies = [
"fxhash",
"lazy_static",
"linear-map",
"memuse",
Expand Down Expand Up @@ -681,6 +688,15 @@ dependencies = [
"percent-encoding",
]

[[package]]
name = "fxhash"
version = "0.2.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c31b6d751ae2c7f11320402d34e41349dd1016f8d5d45e48c4312bc8625af50c"
dependencies = [
"byteorder",
]

[[package]]
name = "getopts"
version = "0.2.21"
Expand Down
1 change: 1 addition & 0 deletions cprover_bindings/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ serde = {version = "1", features = ["derive"]}
string-interner = "0.19"
tracing = "0.1"
linear-map = {version = "1.2", features = ["serde_impl"]}
fxhash = "0.2.1"

[dev-dependencies]
serde_test = "1"
Expand Down
61 changes: 47 additions & 14 deletions cprover_bindings/src/irep/goto_binary_serde.rs
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,9 @@

use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
use crate::{InternString, InternedString};
#[cfg(not(test))]
use fxhash::FxHashMap;
#[cfg(test)]
use std::collections::HashMap;
use std::fs::File;
use std::hash::Hash;
Expand Down Expand Up @@ -199,6 +202,23 @@ impl IrepNumberingInv {
}
}

#[cfg(not(test))]
/// A numbering of [InternedString], [IrepId] and [Irep] based on their contents.
struct IrepNumbering {
/// Map from [InternedString] to their unique numbers.
string_cache: FxHashMap<InternedString, usize>,

/// Inverse string cache.
inv_string_cache: Vec<NumberedString>,

/// Map from [IrepKey] to their unique numbers.
cache: FxHashMap<IrepKey, usize>,

/// Inverse cache, allows to get a NumberedIrep from its unique number.
inv_cache: IrepNumberingInv,
}

#[cfg(test)]
/// A numbering of [InternedString], [IrepId] and [Irep] based on their contents.
struct IrepNumbering {
/// Map from [InternedString] to their unique numbers.
Expand All @@ -214,16 +234,31 @@ struct IrepNumbering {
inv_cache: IrepNumberingInv,
}

#[cfg(not(test))]
impl IrepNumbering {
fn new() -> Self {
IrepNumbering {
string_cache: HashMap::new(),
string_cache: FxHashMap::default(),
inv_string_cache: Vec::new(),
cache: HashMap::new(),
cache: FxHashMap::default(),
inv_cache: IrepNumberingInv::new(),
}
}
}

#[cfg(test)]
impl IrepNumbering {
fn new() -> Self {
IrepNumbering {
string_cache: HashMap::default(),
inv_string_cache: Vec::new(),
cache: HashMap::default(),
inv_cache: IrepNumberingInv::new(),
}
}
}

impl IrepNumbering {
/// Returns a [NumberedString] from its number if it exists, None otherwise.
fn numbered_string_from_number(&mut self, string_number: usize) -> Option<NumberedString> {
self.inv_string_cache.get(string_number).copied()
Expand All @@ -248,7 +283,7 @@ impl IrepNumbering {
/// Turns a [IrepId] to a [NumberedString]. The [IrepId] gets the number of its
/// string representation.
fn number_irep_id(&mut self, irep_id: &IrepId) -> NumberedString {
self.number_string(&irep_id.to_string().intern())
self.number_string(&irep_id.to_string_cow().intern())
}

/// Turns an [Irep] into a [NumberedIrep]. The [Irep] is recursively traversed
Expand All @@ -264,20 +299,18 @@ impl IrepNumbering {
.map(|(key, value)| (self.number_irep_id(key).number, self.number_irep(value).number))
.collect();
let key = IrepKey::new(id, &sub, &named_sub);
self.get_or_insert(&key)
self.get_or_insert(key)
}

/// Gets the existing [NumberedIrep] from the [IrepKey] or inserts a fresh
/// one and returns it.
fn get_or_insert(&mut self, key: &IrepKey) -> NumberedIrep {
if let Some(number) = self.cache.get(key) {
// Return the NumberedIrep from the inverse cache
return self.inv_cache.index[*number];
}
// This is where the key gets its unique number assigned.
let number = self.inv_cache.add_key(key);
self.cache.insert(key.clone(), number);
self.inv_cache.index[number]
fn get_or_insert(&mut self, key: IrepKey) -> NumberedIrep {
let number = self.cache.entry(key).or_insert_with_key(|key| {
// This is where the key gets its unique number assigned.
self.inv_cache.add_key(key)
});

self.inv_cache.index[*number]
}

/// Returns the unique number of the `id` field of the given [NumberedIrep].
Expand Down Expand Up @@ -794,7 +827,7 @@ where
let key = IrepKey::new(id, &sub, &named_sub);

// Insert key in the numbering
let numbered = self.numbering.get_or_insert(&key);
let numbered = self.numbering.get_or_insert(key);

// Map number from the binary to new number
self.add_irep_mapping(irep_number, numbered.number);
Expand Down
43 changes: 27 additions & 16 deletions cprover_bindings/src/irep/irep_id.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use crate::cbmc_string::InternedString;
use crate::utils::NumUtils;
use num::bigint::{BigInt, BigUint, Sign};

use std::fmt::Display;
use std::borrow::Cow;

#[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)]
pub enum IrepId {
Expand Down Expand Up @@ -877,22 +877,34 @@ impl IrepId {
}
}

impl Display for IrepId {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
// Implementing `ToString` rather than `Display` because display only has the interface
// to write to a formatter which seems to be slower when you just need the string.
#[allow(clippy::to_string_trait_impl)]
impl ToString for IrepId {
fn to_string(&self) -> String {
self.to_string_cow().into_owned()
}
}

impl IrepId {
pub fn to_string_cow(&self) -> Cow<str> {
match self.to_owned_string() {
Some(owned) => Cow::Owned(owned),
None => Cow::Borrowed(self.to_static_string()),
}
}

fn to_owned_string(&self) -> Option<String> {
match self {
IrepId::FreeformString(s) => {
return write!(f, "{s}");
}
IrepId::FreeformInteger(i) => {
return write!(f, "{i}");
}
IrepId::FreeformBitPattern(i) => {
return write!(f, "{i:X}");
}
_ => {}
IrepId::FreeformString(s) => Some(s.to_string()),
IrepId::FreeformInteger(i) => Some(i.to_string()),
IrepId::FreeformBitPattern(i) => Some(format!("{i:X}")),
_ => None,
}
}

let s = match self {
fn to_static_string(&self) -> &'static str {
match self {
IrepId::FreeformString(_)
| IrepId::FreeformInteger(_)
| IrepId::FreeformBitPattern { .. } => unreachable!(),
Expand Down Expand Up @@ -1719,8 +1731,7 @@ impl Display for IrepId {
IrepId::VectorGt => "vector->",
IrepId::VectorLt => "vector-<",
IrepId::FloatbvRoundToIntegral => "floatbv_round_to_integral",
};
write!(f, "{s}")
}
}
}

Expand Down
Loading