Skip to content

Commit

Permalink
Some comments and refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
@zgrannan
zgrannan committed Nov 29, 2023
1 parent 4de5ba9 commit 93f8c5d
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 43 deletions.
51 changes: 29 additions & 22 deletions prusti-viper/src/encoder/definition_collector.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,29 @@ impl<'p, 'v: 'p, 'tcx: 'v> Collector<'p, 'v, 'tcx> {
functions.sort_by_cached_key(|f| f.get_identifier());
Ok(functions)
}

fn get_domain_functions_used_in_axioms(axioms: &Vec<vir::DomainAxiom>) -> FxHashSet<String> {
struct Walker {
function_names: FxHashSet<String>,
}

impl ExprWalker for Walker {
fn walk_domain_func_app(&mut self, function_call: &vir::DomainFuncApp) {
self.function_names
.insert(function_call.domain_function.get_identifier());
}
}
let mut functions_in_axioms: FxHashSet<String> = Default::default();
for axiom in axioms {
let mut walker = Walker {
function_names: Default::default(),
};
walker.walk(&axiom.expr);
functions_in_axioms.extend(walker.function_names);
}
functions_in_axioms
}

fn get_used_domains(&self) -> Vec<vir::Domain> {
let mut domains: Vec<_> = self
.used_domains
Expand Down Expand Up @@ -269,34 +292,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> Collector<'p, 'v, 'tcx> {
let retain_type_invariant = axiom.name.ends_with("$valid") && used;
let retain_injectivity = used_snap_domain_constructor
&& axiom.name.ends_with("$injectivity");
let retain_field_axiom = used_snap_domain_constructor
&& axiom.name.ends_with("$axiom");
let retain_field_axiom =
used_snap_domain_constructor && axiom.name.ends_with("$axiom");

retain_type_invariant || retain_injectivity || retain_field_axiom
});
struct Walker {
function_names: FxHashSet<String>
}

impl ExprWalker for Walker {
fn walk_domain_func_app(&mut self, function_call: &vir::DomainFuncApp) {
self.function_names.insert(function_call.domain_function.get_identifier());
}
}
let mut functions_in_axioms: FxHashSet<String> = Default::default();
for axiom in domain.axioms.iter() {
let mut walker = Walker {
function_names: Default::default()
};
walker.walk(&axiom.expr);
functions_in_axioms.extend(walker.function_names);
}
let functions_in_axioms =
Self::get_domain_functions_used_in_axioms(&domain.axioms);
domain.functions.retain(|function| {
let function_name = function.get_identifier();
self
.used_snap_domain_functions
self.used_snap_domain_functions
.contains(&function_name.clone().into())
|| functions_in_axioms.contains(&function_name)
|| functions_in_axioms.contains(&function_name)
});
}
}
Expand Down
40 changes: 19 additions & 21 deletions prusti-viper/src/encoder/snapshot/encoder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1691,10 +1691,10 @@ impl SnapshotEncoder {
// * the constructor, which takes the flattened value-only
// representation of the variant and returns an instance of the
// snapshot domain
// * the injectivity axiom for that constructor:
// * the injectivity axiom for that variant:
// ```plain
// forall _l_args..., _r_args... :: {cons(_l_args...), cons(_r_args)}
// cons(_l_args...) == cons(_r_args) ==> _l_args... == _r_args...
// forall this: Variant :: {field1(this), field2(this), ...}
// this == cons(field1(this), field2(this), ...)
// ```
// * the discriminant axiom for that constructor:
// ```plain
Expand All @@ -1704,7 +1704,7 @@ impl SnapshotEncoder {
// * field access function
// * field access axiom:
// ```plain
// forall args... :: {field(cons(arg_field, other_args...))}
// forall args... :: {cons(arg_field, other_args...)}
// field(cons(arg_field, other_args...)) == arg_field
// ```
for (variant_idx, variant) in variants.iter().enumerate() {
Expand All @@ -1715,8 +1715,6 @@ impl SnapshotEncoder {
.enumerate()
.map(|(idx, field)| vir::LocalVar::new(format!("_{idx}"), field.typ.clone()))
.collect::<Vec<vir::LocalVar>>();
// TODO: filter out Units to reduce constructor size
let has_args = !args.is_empty();

// record name to index mapping
if let Some(name) = &variant.name {
Expand Down Expand Up @@ -1745,7 +1743,6 @@ impl SnapshotEncoder {
constructor.apply(args.iter().cloned().map(Expr::local).collect())
};


if has_multiple_variants {
// encode discriminant axiom
domain_axioms.push({
Expand Down Expand Up @@ -1837,23 +1834,24 @@ impl SnapshotEncoder {
}
}

if has_args {
let field_access_apps: Vec<_> = variant.fields.iter().map(
|f| {
let field_access_func = field_access_funcs.get(&f.name).expect(&format!("No accessor for field {}", f.name));
if !args.is_empty() {
let field_access_apps: Vec<_> = variant
.fields
.iter()
.map(|f| {
let field_access_func = field_access_funcs
.get(&f.name)
.expect(&format!("No accessor for field {}", f.name));
field_access_func.apply(vec![self_expr.clone()])
}
).collect();
})
.collect();
let expr = Expr::forall(
vec![self_local.clone()],
field_access_apps.iter().map(|e|
vir::Trigger::new(
vec![e.clone()]
)).collect(),
Expr::eq_cmp(
self_expr.clone(),
constructor.apply(field_access_apps)
)
field_access_apps
.iter()
.map(|e| vir::Trigger::new(vec![e.clone()]))
.collect(),
Expr::eq_cmp(self_expr.clone(), constructor.apply(field_access_apps)),
);

domain_axioms.push(vir::DomainAxiom {
Expand Down

0 comments on commit 93f8c5d

Please sign in to comment.