Skip to content

Commit

Permalink
Fix some pick dependency issues
Browse files Browse the repository at this point in the history
  • Loading branch information
Alasdair committed Apr 17, 2024
1 parent 90c95b7 commit a9b68f3
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions isla-axiomatic/src/footprint_analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ pub struct Footprint {
register_writes_ignored: HashSet<(Option<Name>, Name)>,
/// If we see `mark_register(R, "pick")` then we have internal
/// pick dependencies from all registers affecting the intrinsic
/// control order up till that point to R
/// control order from R
register_pick_deps: HashMap<Name, HashSet<RegisterField>>,
/// A store is any instruction with a WriteMem event
is_store: bool,
Expand Down Expand Up @@ -388,7 +388,7 @@ fn advance_deps(footprint: &Footprint, touched: &mut HashSet<RegisterField>) {
}

pub fn pick_dep<B: BV>(from: usize, to: usize, instrs: &[B], footprints: &HashMap<B, Footprint>) -> bool {
let to_footprint = footprints.get(&instrs[from]).unwrap();
let to_footprint = footprints.get(&instrs[to]).unwrap();
if !(to_footprint.is_load || to_footprint.is_store) || (from >= to) {
return false;
}
Expand Down

0 comments on commit a9b68f3

Please sign in to comment.