Skip to content

Commit

Permalink
Fix unsound contract equality fast check (#1703)
Browse files Browse the repository at this point in the history
* Fix unsound ptr eq check in contract equality

For performance reason, the contract equality checker performs a quick
pointer check to see if the two terms to compare are physically equal.
In this case, it used to return `true` directly, eschewing more costly
recursive checks.

However, this is unsound, because the same term (physically) might be in two
different environments, and have two different values. This is typically
the case with function application: when evaluating `f 1` and `f 2`,
both terms will physically point to the body of `f`, but in a different
environment. Thus, we also need to ensure that environment are equals as
well in this quick check.

This commit adds a fast `ptr_eq` check to the environment as well, and
now checks that both terms and their respective environments are
pairwise physically equals.

Passing by, this commits also fix unrelated clippy warning, after the
udpate to clippy 1.73.

* Add regression test for #1700

* Implement env equality during typechecking

* Cosmetic renaming and slight rework of comments

* Fix contract test by deeply evaluating it

* Remove confusing comments
  • Loading branch information
yannham authored Oct 29, 2023
1 parent 1921c31 commit 11c8fab
Show file tree
Hide file tree
Showing 5 changed files with 51 additions and 17 deletions.
23 changes: 9 additions & 14 deletions cli/src/customize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,11 +72,6 @@ struct OverrideInterface {
}

impl TermInterface {
/// Create a new, empty interface.
fn new() -> Self {
Self::default()
}

/// Build a command description from this interface.
///
/// This method recursively lists all existing field paths, and reports input fields (as
Expand Down Expand Up @@ -219,7 +214,7 @@ impl From<&RecordData> for TermInterface {

impl From<&Term> for TermInterface {
fn from(term: &Term) -> Self {
term.extract_interface().unwrap_or_else(TermInterface::new)
term.extract_interface().unwrap_or_default()
}
}

Expand Down Expand Up @@ -566,16 +561,16 @@ impl Customize for CustomizeMode {
program.add_overrides(
arg_matches
.ids()
.filter_map(|id| -> Option<FieldOverride> {
(!matches!(
.filter(|id| {
!matches!(
arg_matches.value_source(id.as_str()),
Some(ValueSource::DefaultValue)
) && id.as_str() != "override")
.then(|| FieldOverride {
path: cmd.args.get(id).unwrap().clone(),
value: arg_matches.get_one::<String>(id.as_str()).unwrap().clone(),
priority: MergePriority::default(),
})
) && id.as_str() != "override"
})
.map(|id| FieldOverride {
path: cmd.args.get(id).unwrap().clone(),
value: arg_matches.get_one::<String>(id.as_str()).unwrap().clone(),
priority: MergePriority::default(),
})
.chain(force_overrides),
);
Expand Down
15 changes: 15 additions & 0 deletions core/src/environment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -151,6 +151,21 @@ impl<K: Hash + Eq, V: PartialEq> Environment<K, V> {
fn was_cloned(&self) -> bool {
Rc::strong_count(&self.current) > 1
}

/// Checks quickly if two environments are obviously equal (when their components are
/// physically equal as pointers or obviously equal such as being both empty).
pub(crate) fn ptr_eq(this: &Self, that: &Self) -> bool {
let prev_layers_eq = match (&*this.previous.borrow(), &*that.previous.borrow()) {
(Some(ptr_this), Some(ptr_that)) => Rc::ptr_eq(ptr_this, ptr_that),
(None, None) => true,
_ => false,
};

let curr_layers_eq = (this.current.is_empty() && that.current.is_empty())
|| Rc::ptr_eq(&this.current, &that.current);

prev_layers_eq && curr_layers_eq
}
}

impl<K: Hash + Eq, V: PartialEq> FromIterator<(K, V)> for Environment<K, V> {
Expand Down
5 changes: 3 additions & 2 deletions core/src/eval/cache/lazy.rs
Original file line number Diff line number Diff line change
Expand Up @@ -549,8 +549,9 @@ impl Thunk {
};

let as_function_closurized = RichTerm::from(Term::Closure(thunk_as_function));
let args =
fields.filter_map(|id| deps_filter(&id).then(|| RichTerm::from(Term::Var(id.into()))));
let args = fields
.filter(deps_filter)
.map(|id| RichTerm::from(Term::Var(id.into())));

args.fold(as_function_closurized, |partial_app, arg| {
RichTerm::from(Term::App(partial_app, arg))
Expand Down
14 changes: 13 additions & 1 deletion core/src/typecheck/eq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,10 @@ pub trait TermEnvironment: Clone {
where
F: FnOnce(Option<(&RichTerm, &Self)>) -> T;

/// Cheap check that two environment are physically equal. This check is used to avoid doing
/// extra work and usually boils down to pointer equality.
fn fast_eq(_this: &Self, _that: &Self) -> bool;

/// When comparing closure, we don't get an identifier, but a cache index (a thunk).
fn get_idx_then<F, T>(env: &Self, idx: &CacheIndex, f: F) -> T
where
Expand Down Expand Up @@ -115,6 +119,10 @@ impl TermEnvironment for SimpleTermEnvironment {
);
f(None)
}

fn fast_eq(this: &Self, that: &Self) -> bool {
GenericEnvironment::ptr_eq(&this.0, &that.0)
}
}

impl std::iter::FromIterator<(Ident, (RichTerm, SimpleTermEnvironment))> for SimpleTermEnvironment {
Expand Down Expand Up @@ -147,6 +155,10 @@ impl TermEnvironment for eval::Environment {

f(Some((&closure_ref.body, &closure_ref.env)))
}

fn fast_eq(this: &Self, that: &Self) -> bool {
Self::ptr_eq(this, that)
}
}

pub trait FromEnv<C: Cache> {
Expand Down Expand Up @@ -260,7 +272,7 @@ fn contract_eq_bounded<E: TermEnvironment>(
// Test for physical equality as both an optimization and a way to cheaply equate complex
// contracts that happen to point to the same definition (while the purposely limited
// structural checks below may reject the equality)
if term::SharedTerm::ptr_eq(&t1.term, &t2.term) {
if term::SharedTerm::ptr_eq(&t1.term, &t2.term) && E::fast_eq(env1, env2) {
return true;
}

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# test.type = 'error'
# eval = 'full'
#
# [test.metadata]
# error = 'EvalError::BlameError'

# Regression test for https://github.com/tweag/nickel/issues/1700
let False = std.contract.from_predicate (fun x => false) in
({ bli = {foo = 1} }
| { _| {..} })
| { _| False }

0 comments on commit 11c8fab

Please sign in to comment.