Skip to content

Commit

Permalink
Fix lint on range
Browse files Browse the repository at this point in the history
  • Loading branch information
Jacob Salzberg committed Aug 27, 2024
1 parent cda8657 commit db2c570
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 14 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -53,21 +53,31 @@ pub struct Cache {
cache: Vec<Instance>,
}

fn try_get_or_insert<T, P, F, E>(vec: &mut Vec<T>, p: P, f: F) -> Result<&mut T, E>
where F: FnOnce() -> Result<T, E>, P: Fn(&T) -> bool, T: PartialEq {
if let Some(i) = vec.iter().position(p) {
Ok(&mut vec[i])
} else {
vec.push(f()?);
Ok(vec.last_mut().unwrap())
}
}

impl Cache {

/// Register the signature the to the cache
/// in the given compilation context, ctx
pub fn register(&mut self, ctx: &TyCtxt, sig: Signature) -> Result<&MirInstance, MirError> {
pub fn register(&mut self, ctx: &TyCtxt, signature: Signature) -> Result<&MirInstance, MirError> {
let test_sig = signature.clone();
let Cache { cache } = self;
for item in &cache {
if sig == item.signature {
return Ok(item.instance);
}
}
let fndef = find_fn_def(*ctx, &sig.diagnostic)
.ok_or(MirError::new(format!("Not found: {}", &sig.diagnostic)))?;
let instance = MirInstance::resolve(fndef, &GenericArgs(sig.args.clone()))?;
cache.push(Instance::new(sig, instance));
Ok(&cache[cache.len() - 1].instance)
try_get_or_insert(cache, |item| item.signature == test_sig, ||
{
let fndef = find_fn_def(*ctx, &signature.diagnostic)
.ok_or(MirError::new(format!("Not found: {}", &signature.diagnostic)))?;
let instance = MirInstance::resolve(fndef, &GenericArgs(signature.args.clone()))?;
Ok(Instance::new(signature, instance))
}).map(|entry| &entry.instance)

}

/// Register the kani assertion function
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ impl<'tcx, 'cache> InstrumentationData<'tcx, 'cache> {
let tcx = &self.tcx;
let fn_pointers = &mut self.fn_pointers;
let body = &mut self.body;
let span = *self.span;
let span = self.span;
let instance = cache.register(tcx, callee)?;
let func_local = fn_pointers
.entry(*instance)
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/transform/check_aliasing/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -125,8 +125,8 @@ impl GlobalPass for GlobalAliasingPass {
.def
.all_attrs()
.into_iter()
.all(|attr| attr.as_str().contains("kanitool::proof")) &&
found.insert(instance)
.all(|attr| attr.as_str().contains("kanitool::proof"))
&& found.insert(instance)
{
queue.push_back(instance)
}
Expand Down

0 comments on commit db2c570

Please sign in to comment.