-
Notifications
You must be signed in to change notification settings - Fork 121
Empirical constraints suggestions #3468
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Draft
Schaeff
wants to merge
2
commits into
collect-empirical-constraints
Choose a base branch
from
empirical-constraints-simplification
base: collect-empirical-constraints
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,38 +1,35 @@ | ||
| use std::collections::btree_map::Entry; | ||
| use std::collections::{BTreeMap, BTreeSet, HashMap}; | ||
| use std::collections::{BTreeMap, HashMap}; | ||
| use std::fmt::Debug; | ||
| use std::hash::Hash; | ||
|
|
||
| use itertools::Itertools; | ||
| use serde::{Deserialize, Serialize}; | ||
|
|
||
| pub use crate::equivalence_classes::{EquivalenceClass, EquivalenceClasses}; | ||
|
|
||
| /// "Constraints" that were inferred from execution statistics. They hold empirically | ||
| /// (most of the time), but are not guaranteed to hold in all cases. | ||
| #[derive(Serialize, Deserialize, Clone, Default, Debug)] | ||
| #[derive(Serialize, Default, Debug)] | ||
| pub struct EmpiricalConstraints { | ||
| /// For each program counter, the range constraints for each column. | ||
| /// The range might not hold in 100% of cases. | ||
| pub column_ranges_by_pc: BTreeMap<u32, Vec<(u32, u32)>>, | ||
| /// For each basic block (identified by its starting PC), the equivalence classes of columns. | ||
| /// Each equivalence class is a list of (instruction index in block, column index). | ||
| pub equivalence_classes_by_block: BTreeMap<u64, BTreeSet<BTreeSet<(usize, usize)>>>, | ||
| pub equivalence_classes_by_block: BTreeMap<u64, EquivalenceClasses<BlockCell>>, | ||
| pub debug_info: DebugInfo, | ||
| } | ||
|
|
||
| /// Debug information mapping AIR ids to program counters and column names. | ||
| #[derive(Serialize, Deserialize, Default)] | ||
| #[derive(Serialize, Deserialize, Default, Debug)] | ||
| pub struct DebugInfo { | ||
| /// Mapping from program counter to AIR id. | ||
| pub air_id_by_pc: BTreeMap<u32, usize>, | ||
| /// Mapping from AIR id to column names. | ||
| pub column_names_by_air_id: BTreeMap<usize, Vec<String>>, | ||
| } | ||
|
|
||
| #[derive(Serialize, Deserialize)] | ||
| pub struct EmpiricalConstraintsJson { | ||
| pub empirical_constraints: EmpiricalConstraints, | ||
| pub debug_info: DebugInfo, | ||
| } | ||
|
|
||
| impl EmpiricalConstraints { | ||
| pub fn combine_with(&mut self, other: EmpiricalConstraints) { | ||
| // Combine column ranges by PC | ||
|
|
@@ -52,15 +49,14 @@ impl EmpiricalConstraints { | |
|
|
||
| // Combine equivalence classes by block | ||
| for (block_pc, classes) in other.equivalence_classes_by_block { | ||
| self.equivalence_classes_by_block | ||
| let existing = self | ||
| .equivalence_classes_by_block | ||
| .entry(block_pc) | ||
| .and_modify(|existing_classes| { | ||
| let combined = | ||
| intersect_partitions(&[existing_classes.clone(), classes.clone()]); | ||
| *existing_classes = combined; | ||
| }) | ||
| .or_insert(classes); | ||
| .or_default(); | ||
|
|
||
| *existing = intersect_partitions(vec![std::mem::take(existing), classes]); | ||
| } | ||
| self.debug_info.combine_with(other.debug_info); | ||
| } | ||
| } | ||
|
|
||
|
|
@@ -88,16 +84,32 @@ fn merge_maps<K: Ord, V: Eq + Debug>(map1: &mut BTreeMap<K, V>, map2: BTreeMap<K | |
| } | ||
| } | ||
|
|
||
| #[derive(PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize, Debug, Copy, Clone)] | ||
| pub struct BlockCell { | ||
|
Collaborator
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Introduce type for the equivalence class members, aka cells of a block execution |
||
| /// The row index which is also the instruction index within the basic block | ||
| row_idx: usize, | ||
| /// The column index within the instruction air | ||
| column_idx: usize, | ||
| } | ||
|
|
||
| impl BlockCell { | ||
| pub fn new(row_idx: usize, column_idx: usize) -> Self { | ||
| Self { | ||
| row_idx, | ||
| column_idx, | ||
| } | ||
| } | ||
| } | ||
|
|
||
| /// Intersects multiple partitions of the same universe into a single partition. | ||
| /// In other words, two elements are in the same equivalence class in the resulting partition | ||
| /// if and only if they are in the same equivalence class in all input partitions. | ||
| /// Singleton equivalence classes are omitted from the result. | ||
| pub fn intersect_partitions<Id>(partitions: &[BTreeSet<BTreeSet<Id>>]) -> BTreeSet<BTreeSet<Id>> | ||
| where | ||
| Id: Eq + Hash + Copy + Ord, | ||
| { | ||
| pub fn intersect_partitions<T: Eq + Hash + Copy + Ord>( | ||
| partitions: Vec<EquivalenceClasses<T>>, | ||
|
Collaborator
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. move |
||
| ) -> EquivalenceClasses<T> { | ||
| // For each partition, build a map: Id -> class_index | ||
| let class_ids: Vec<HashMap<Id, usize>> = partitions | ||
| let class_ids: Vec<HashMap<T, usize>> = partitions | ||
| .iter() | ||
| .map(|partition| { | ||
| partition | ||
|
|
@@ -112,14 +124,14 @@ where | |
| partitions | ||
| .iter() | ||
| .flat_map(|partition| partition.iter()) | ||
| .flat_map(|class| class.iter().copied()) | ||
| .flat_map(|class| class.iter()) | ||
| .unique() | ||
| .filter_map(|id| { | ||
| // Build the signature of the element: the list of class indices it belongs to | ||
| // (one index per partition) | ||
| class_ids | ||
| .iter() | ||
| .map(|m| m.get(&id).cloned()) | ||
| .map(|m| m.get(id).cloned()) | ||
| // If an element did not appear in any one of the partitions, it is | ||
| // a singleton and we skip it. | ||
| .collect::<Option<Vec<usize>>>() | ||
|
|
@@ -128,16 +140,16 @@ where | |
| // Group elements by their signatures | ||
| .into_group_map() | ||
| .into_values() | ||
| // Remove singletons and convert to Set | ||
| .filter_map(|ids| (ids.len() > 1).then_some(ids.into_iter().collect())) | ||
| // Convert to set | ||
| .map(|ids| ids.into_iter().copied().collect()) | ||
| .collect() | ||
| } | ||
|
|
||
| #[cfg(test)] | ||
| mod tests { | ||
| use std::collections::BTreeSet; | ||
| use crate::empirical_constraints::EquivalenceClasses; | ||
|
|
||
| fn partition(sets: Vec<Vec<u32>>) -> BTreeSet<BTreeSet<u32>> { | ||
| fn partition(sets: Vec<Vec<u32>>) -> EquivalenceClasses<u32> { | ||
| sets.into_iter().map(|s| s.into_iter().collect()).collect() | ||
| } | ||
|
|
||
|
|
@@ -156,7 +168,7 @@ mod tests { | |
| vec![6, 7, 8], | ||
| ]); | ||
|
|
||
| let result = super::intersect_partitions(&[partition1, partition2]); | ||
| let result = super::intersect_partitions(vec![partition1, partition2]); | ||
|
|
||
| let expected = partition(vec![vec![2, 3], vec![6, 7, 8]]); | ||
|
|
||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,36 @@ | ||
| use std::collections::BTreeSet; | ||
|
|
||
| use serde::Serialize; | ||
|
|
||
| /// An equivalence class | ||
| pub type EquivalenceClass<T> = BTreeSet<T>; | ||
|
|
||
| /// A collection of equivalence classes where all classes are guaranteed to have at least two elements | ||
| #[derive(Serialize, Debug, PartialEq, Eq)] | ||
| pub struct EquivalenceClasses<T> { | ||
| inner: BTreeSet<EquivalenceClass<T>>, | ||
| } | ||
|
|
||
| // TODO: derive | ||
| impl<T> Default for EquivalenceClasses<T> { | ||
| fn default() -> Self { | ||
| Self { | ||
| inner: Default::default(), | ||
| } | ||
| } | ||
| } | ||
|
|
||
| impl<T: Ord> FromIterator<EquivalenceClass<T>> for EquivalenceClasses<T> { | ||
| fn from_iter<I: IntoIterator<Item = EquivalenceClass<T>>>(iter: I) -> Self { | ||
| // When collecting, we ignore classes with 0 or 1 elements as they are useless | ||
| Self { | ||
| inner: iter.into_iter().filter(|class| class.len() > 1).collect(), | ||
| } | ||
| } | ||
| } | ||
|
|
||
| impl<T> EquivalenceClasses<T> { | ||
| pub fn iter(&self) -> impl Iterator<Item = &EquivalenceClass<T>> { | ||
| self.inner.iter() | ||
| } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Merge DebugInfo into
EmpiricalConstraintsto simplify return types