Skip to content

Commit 7db6a0c

Browse files
cache implementation from branch
1 parent df4e0a6 commit 7db6a0c

7 files changed

Lines changed: 116 additions & 84 deletions

File tree

cprover_bindings/src/goto_program/location.rs

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,23 @@ impl Location {
124124
}
125125
}
126126

127+
/// Tries to set the `function` field of a [Location::Loc], but returns `None` if the location
128+
/// is of a different variant and the field couldn't be set.
129+
pub fn try_set_function(
130+
&mut self,
131+
new_function: Option<impl Into<InternedString>>,
132+
) -> Option<()> {
133+
if let Location::Loc { function, .. } = self {
134+
if let Some(new_function) = new_function {
135+
*function = Some(new_function.into());
136+
}
137+
138+
Some(())
139+
} else {
140+
None
141+
}
142+
}
143+
127144
/// Create a Property type Location
128145
pub fn property_location<T, U>(
129146
file: Option<U>,
Lines changed: 73 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,14 @@
1-
use std::hash::Hash;
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
23

3-
use std::collections::hash_map::Entry as HashMapEntry;
4+
use std::{cell::RefCell, hash::Hash};
45

5-
use cbmc::goto_program::{Location, Type};
66
use fxhash::FxHashMap;
7+
use std::any::type_name;
78

8-
use crate::codegen_cprover_gotoc::context::SpanWrapper;
9-
10-
// #[derive(Default)]
11-
// pub struct CodegenCache {
12-
13-
// types: FxHashMap<rustc_public::ty::Ty, Type>,
14-
// spans: FxHashMap<SpanWrapper, Location>,
15-
// }
9+
thread_local! {
10+
pub static CACHE: RefCell<CodegenCache> = RefCell::new(Default::default());
11+
}
1612

1713
type HashImpl<K, V> = FxHashMap<K, V>;
1814

@@ -21,109 +17,104 @@ where
2117
Self: Sized,
2218
{
2319
type Key: Hash + Eq;
24-
fn get_individual_cache(cache: &mut CodegenCache) -> &mut HashImpl<Self::Key, Self>;
20+
fn get_individual_cache(cache: &CodegenCache) -> &HashImpl<Self::Key, Self>;
21+
fn get_individual_cache_mut(cache: &mut CodegenCache) -> &mut HashImpl<Self::Key, Self>;
2522
}
2623

27-
// impl CodegenCacheEl for Type {
28-
// type Key = rustc_public::ty::Ty;
29-
// fn get_individual_cache(cache: &mut CodegenCache) -> &mut HashImpl<Self::Key, Self> {
30-
// &mut cache.types
31-
// }
32-
// }
33-
34-
// impl CodegenCacheEl for Location {
35-
// type Key = SpanWrapper;
36-
// fn get_individual_cache(cache: &mut CodegenCache) -> &mut HashImpl<Self::Key, Self> {
37-
// &mut cache.spans
24+
// impl Drop for CodegenCache {
25+
// fn drop(&mut self) {
26+
// self.calc_size();
3827
// }
3928
// }
4029

4130
macro_rules! generate_cache {
42-
($name:tt -- $([$field_name:tt] $key:path => $el:path),+) => {
31+
($name:tt -- $($(@$global:tt)? [$field_name:tt] $key:path => $el:path),+) => {
4332
#[derive(Default)]
4433
pub struct $name {
4534
$($field_name: HashImpl<$key, $el>,)*
4635
}
4736

37+
impl $name {
38+
#[allow(dead_code)]
39+
fn calc_size(&self) {
40+
let mut total = 0;
41+
$(
42+
let key_size = size_of::<$key>();
43+
let el_size = size_of::<$el>();
44+
let cap = self.$field_name.capacity();
45+
let field_total = (key_size + el_size) * cap;
46+
println!("for {:?} map -- key: {key_size}, el: {el_size}, cap: {cap} => {field_total}", type_name::<$el>());
47+
total += field_total;
48+
)*
49+
println!("{total} in total!");
50+
}
51+
}
52+
53+
pub fn clear_codegen_cache() {
54+
CACHE.with_borrow_mut(|cache|{
55+
$(
56+
clear_cache!($($global)? cache, $field_name);
57+
)*
58+
})
59+
}
60+
4861
$(
4962
impl CodegenCacheEl for $el {
5063
type Key = $key;
51-
fn get_individual_cache(cache: &mut CodegenCache) -> &mut HashImpl<Self::Key, Self> {
64+
fn get_individual_cache(cache: &CodegenCache) -> &HashImpl<Self::Key, Self> {
65+
&cache.$field_name
66+
}
67+
fn get_individual_cache_mut(cache: &mut CodegenCache) -> &mut HashImpl<Self::Key, Self> {
5268
&mut cache.$field_name
5369
}
5470
}
5571
)*
5672
};
5773
}
5874

75+
// TODO: add more granularity here...
76+
macro_rules! clear_cache {
77+
( $cache:tt, $field_name:tt) => {
78+
$cache.$field_name.clear();
79+
};
80+
(global $cache:tt, $field_name:tt) => {
81+
/* global field, don't clear cache */
82+
};
83+
}
84+
5985
generate_cache!(CodegenCache --
60-
[types] rustc_public::ty::Ty => cbmc::goto_program::Type,
61-
[spans] SpanWrapper => cbmc::goto_program::Location
86+
[types] rustc_public::ty::Ty => cbmc::goto_program::Type,
87+
@global [spans] rustc_public::ty::Span => cbmc::goto_program::Location
6288
);
6389

64-
// you give me a key i tell you if it's there
65-
66-
// if it's there, you may want to modify before taking it
90+
pub struct FinalEntry<T: CodegenCacheEl>(Option<T>, T::Key);
6791

68-
// if it's not, you want to insert it by running some code
69-
70-
// they you want a ref to the newly inserted
71-
72-
impl CodegenCache {
73-
pub fn entry<E: CodegenCacheEl + Clone>(&mut self, key: E::Key) -> Entry<'_, E::Key, E> {
74-
Entry(E::get_individual_cache(self).entry(key))
75-
}
76-
77-
pub fn entry_ref<E: CodegenCacheEl>(&mut self, key: E::Key) -> EntryRef<'_, E::Key, E> {
78-
EntryRef(E::get_individual_cache(self).entry(key))
79-
}
92+
pub fn cache_entry<E: CodegenCacheEl + Clone>(key: E::Key) -> FinalEntry<E> {
93+
let found_value = CACHE.with_borrow(|cache| E::get_individual_cache(cache).get(&key).cloned());
94+
FinalEntry(found_value, key)
8095
}
8196

82-
// an entry that we inevitably want to clone
83-
struct Entry<'a, K, V: Clone>(HashMapEntry<'a, K, V>);
84-
struct EntryRef<'a, K, V>(HashMapEntry<'a, K, V>);
85-
86-
// an [Entry] that will have a function applied
87-
struct TweakedEntry<'a, K, V: Clone>(Option<V>, HashMapEntry<'a, K, V>);
88-
89-
impl<'a, K, V: Clone> EntryRef<'a, K, V> {
90-
pub fn or_insert_with<F: FnOnce() -> V>(self, f: F) -> &'a V {
91-
match self.0 {
92-
HashMapEntry::Occupied(existing) => existing.into_mut(),
93-
HashMapEntry::Vacant(vacant) => vacant.insert(f()),
97+
impl<E: CodegenCacheEl> FinalEntry<E> {
98+
pub fn tweak<F: FnOnce(&mut E)>(mut self, f: F) -> FinalEntry<E> {
99+
if let Some(found_val) = &mut self.0 {
100+
f(found_val)
94101
}
95-
}
96-
}
97-
98-
impl<'a, K, V: Clone> Entry<'a, K, V> {
99-
pub fn tweak_from_cache<F: FnOnce(&mut V)>(self, f: F) -> TweakedEntry<'a, K, V> {
100-
TweakedEntry(
101-
match &self.0 {
102-
HashMapEntry::Occupied(o) => {
103-
let mut new_val = o.get().clone();
104-
f(&mut new_val);
105-
Some(new_val)
106-
}
107-
HashMapEntry::Vacant(_) => None,
108-
},
109-
self.0,
110-
)
111-
}
112102

113-
pub fn or_insert_with<F: FnOnce() -> V>(self, f: F) -> V {
114-
match self.0 {
115-
HashMapEntry::Occupied(existing) => existing.get().clone(),
116-
HashMapEntry::Vacant(vacant) => vacant.insert(f()).clone(),
117-
}
103+
self
118104
}
119105
}
120106

121-
impl<'a, K, V: Clone> TweakedEntry<'a, K, V> {
122-
pub fn or_insert_with<F: FnOnce() -> V>(self, f: F) -> V {
123-
match (self.0, self.1) {
124-
(Some(tweaked), HashMapEntry::Occupied(_)) => tweaked,
125-
(None, HashMapEntry::Vacant(vacant)) => vacant.insert(f()).clone(),
126-
_ => unreachable!(),
107+
impl<E: CodegenCacheEl + Clone> FinalEntry<E> {
108+
pub fn or_insert_with<F: FnOnce() -> E>(self, f: F) -> E {
109+
match self.0 {
110+
Some(cached) => cached,
111+
None => {
112+
let calculated = f();
113+
CACHE.with_borrow_mut(|cache| {
114+
E::get_individual_cache_mut(cache).insert(self.1, calculated.clone())
115+
});
116+
calculated
117+
}
127118
}
128119
}
129120
}

kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
77
mod assert;
88
mod block;
9+
pub(crate) mod cache;
910
mod foreign_function;
1011
mod function;
1112
mod intrinsic;

kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
//! MIR Span related functions
55
66
use crate::codegen_cprover_gotoc::GotocCtx;
7+
use crate::codegen_cprover_gotoc::codegen::cache::cache_entry;
78
use cbmc::goto_program::Location;
89
use lazy_static::lazy_static;
910
use rustc_hir::Attribute;
@@ -37,6 +38,17 @@ impl GotocCtx<'_> {
3738
}
3839

3940
pub fn codegen_span_stable(&self, sp: SpanStable) -> Location {
41+
cache_entry::<Location>(sp)
42+
.tweak(|res| {
43+
res.try_set_function(
44+
self.current_fn.as_ref().map(|x| x.readable_name().to_string()),
45+
)
46+
.unwrap();
47+
})
48+
.or_insert_with(|| self.codegen_span_stable_inner(sp))
49+
}
50+
51+
pub fn codegen_span_stable_inner(&self, sp: SpanStable) -> Location {
4052
// Attribute to mark functions as where automatic pointer checks should not be generated.
4153
let should_skip_ptr_checks_attr = vec![
4254
rustc_span::symbol::Symbol::intern("kanitool"),
@@ -66,6 +78,7 @@ impl GotocCtx<'_> {
6678
.leak() // This is to preserve `Location` being Copy, but could blow up the memory utilization of compiler.
6779
};
6880
let loc = sp.get_lines();
81+
6982
Location::new(
7083
sp.get_filename().to_string(),
7184
self.current_fn.as_ref().map(|x| x.readable_name().to_string()),

kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
//! `typ.rs`.
88
99
use crate::codegen_cprover_gotoc::GotocCtx;
10+
use crate::codegen_cprover_gotoc::codegen::cache::cache_entry;
1011
use crate::kani_middle::abi::LayoutOf;
1112
use cbmc::goto_program::Type;
1213
use rustc_middle::ty::layout::{LayoutOf as _, TyAndLayout};
@@ -20,8 +21,15 @@ impl<'tcx> GotocCtx<'tcx> {
2021
place.ty(self.current_fn().locals()).unwrap()
2122
}
2223

24+
// pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type {
25+
// cache_entry::<Type>(ty).or_insert_with(||{
26+
// self.codegen_ty_stable_inner(ty)
27+
// })
28+
// }
29+
2330
pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type {
24-
self.codegen_ty(rustc_internal::internal(self.tcx, ty))
31+
cache_entry::<Type>(ty)
32+
.or_insert_with(|| self.codegen_ty(rustc_internal::internal(self.tcx, ty)))
2533
}
2634

2735
pub fn codegen_ty_ref_stable(&mut self, ty: Ty) -> Type {

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@
1616
//! this structure as input.
1717
use super::current_fn::CurrentFnCtx;
1818
use super::vtable_ctx::VtableCtx;
19-
use crate::codegen_cprover_gotoc::UnsupportedConstructs;
2019
use crate::codegen_cprover_gotoc::overrides::{GotocHooks, fn_hooks};
2120
use crate::codegen_cprover_gotoc::utils::full_crate_name;
21+
use crate::codegen_cprover_gotoc::{UnsupportedConstructs, clear_codegen_cache};
2222
use crate::kani_middle::transform::BodyTransformation;
2323
use crate::kani_queries::QueryDb;
2424
use cbmc::goto_program::{
@@ -108,6 +108,7 @@ impl<'tcx> GotocCtx<'tcx> {
108108
machine_model: &MachineModel,
109109
transformer: BodyTransformation,
110110
) -> GotocCtx<'tcx> {
111+
clear_codegen_cache();
111112
let fhks = fn_hooks();
112113
let symbol_table = SymbolTable::new(machine_model.clone());
113114
let emit_vtable_restrictions = queries.args().emit_vtable_restrictions;

kani-compiler/src/codegen_cprover_gotoc/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ mod context;
66
mod overrides;
77
mod utils;
88

9+
pub use codegen::cache::clear_codegen_cache;
910
pub use compiler_interface::{GotocCodegenBackend, UnsupportedConstructs};
1011
pub use context::GotocCtx;
1112
pub use context::VtableCtx;

0 commit comments

Comments
 (0)