increase validator precision for some Unspecified cases
#603
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 |
|---|---|---|
|
|
@@ -1916,7 +1916,10 @@ impl<'a> Typechecker<'a> { | |
|
|
||
| // Given an expression, if that expression is a literal or the `action` | ||
| // variable, return it as an EntityUID. Return `None` otherwise. | ||
| fn euid_from_euid_literal_or_action<T: Clone>( | ||
| request_env: &RequestEnv, | ||
| e: &Expr<T>, | ||
| ) -> Option<EntityUID> { | ||
| match Typechecker::replace_action_var_with_euid(request_env, e) | ||
| .as_ref() | ||
| .expr_kind() | ||
|
|
@@ -1929,17 +1932,17 @@ impl<'a> Typechecker<'a> { | |
| // Convert all expressions in the input to EntityUIDs if an EntityUID can be | ||
| // extracted by `euid_from_uid_literal_or_action`. Return `None` if any | ||
| // cannot be converted. | ||
| fn euids_from_euid_literals_or_action<'b, T: 'b + Clone>( | ||
| request_env: &RequestEnv, | ||
| exprs: impl IntoIterator<Item = &'b Expr<T>>, | ||
| ) -> Option<Vec<EntityUID>> { | ||
| exprs | ||
| .into_iter() | ||
| .map(|e| Self::euid_from_euid_literal_or_action(request_env, e)) | ||
| .collect::<Option<Vec<_>>>() | ||
| } | ||
|
|
||
| fn is_unspecified_entity<T>(query_env: &RequestEnv, expr: &Expr<T>) -> bool { | ||
| match expr.expr_kind() { | ||
| ExprKind::Var(Var::Principal) => matches!( | ||
| query_env.principal_entity_type(), | ||
|
|
@@ -1961,83 +1964,126 @@ impl<'a> Typechecker<'a> { | |
|
|
||
| /// Handles `in` expression where the `principal` or `resource` is `in` an | ||
| /// entity literal or set of entity literals. | ||
| fn type_of_var_in_entity_literals<'b, 'c, T: 'b + Clone>( | ||
| &self, | ||
| request_env: &RequestEnv, | ||
| lhs_var: Var, | ||
| rhs_elems: impl IntoIterator<Item = &'b Expr<T>> + Clone, | ||
| in_expr: &Expr, | ||
| lhs_expr: Expr<Option<Type>>, | ||
| rhs_expr: Expr<Option<Type>>, | ||
| ) -> TypecheckAnswer<'c> { | ||
| let var_etype = if matches!(lhs_var, Var::Principal) { | ||
| request_env.principal_entity_type() | ||
| } else { | ||
| request_env.resource_entity_type() | ||
| }; | ||
| match ( | ||
| var_etype, | ||
| Typechecker::euids_from_euid_literals_or_action( | ||
| request_env, | ||
| rhs_elems.clone().into_iter(), | ||
| ), | ||
| ) { | ||
| (None, _) => { | ||
| // We failed to get the principal/resource entity type because | ||
| // we are typechecking a request for some action which isn't | ||
| // declared in the schema. We don't know if the euid would be | ||
| // in the descendants or not, so give it type boolean. | ||
| let in_expr = ExprBuilder::with_data(Some(Type::primitive_boolean())) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr); | ||
| if self.mode.is_partial() { | ||
| TypecheckAnswer::success(in_expr) | ||
| } else { | ||
| // This should only happen when doing partial validation | ||
| // since we never construct the undeclared action | ||
| // request environment otherwise. | ||
| TypecheckAnswer::fail(in_expr) | ||
| } | ||
| } | ||
| (Some(EntityType::Specified(var_name)), Some(rhs)) => { | ||
| let all_known = |euids: &[EntityUID]| { | ||
| euids | ||
| .iter() | ||
| .all(|e| self.schema.euid_has_known_entity_type(e)) | ||
| }; | ||
| if self.schema.is_known_entity_type(&var_name) && all_known(&rhs) { | ||
| let descendants = self.schema.get_entity_types_in_set(rhs.iter()); | ||
| Typechecker::entity_in_descendants( | ||
| var_name, | ||
| descendants, | ||
| in_expr, | ||
| lhs_expr, | ||
| rhs_expr, | ||
| ) | ||
| } else { | ||
| let annotated_expr = ExprBuilder::with_data(Some(Type::primitive_boolean())) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr); | ||
| if self.mode.is_partial() { | ||
| // In partial schema mode, undeclared entity types are | ||
| // expected. | ||
| TypecheckAnswer::success(annotated_expr) | ||
| } else { | ||
| TypecheckAnswer::fail(annotated_expr) | ||
| } | ||
| } | ||
| } | ||
| (Some(EntityType::Specified(_)), None) => { | ||
| // One or more of the elements on the right is not an entity | ||
| // literal. The `in` is still valid, so typechecking succeeds | ||
| // with type Boolean. | ||
| TypecheckAnswer::success( | ||
| ExprBuilder::with_data(Some(Type::primitive_boolean())) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } | ||
| (Some(EntityType::Unspecified), Some(rhs)) => { | ||
| // It's perfectly valid for `principal` or `resource` to be `EntityType::Unspecified` | ||
khieta marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| if rhs | ||
| .iter() | ||
| .any(|euid| matches!(euid.entity_type(), EntityType::Unspecified)) | ||
| { | ||
| // something on the RHS is unspecified, so we have to type `unspecified in RHS` as Bool, | ||
| // because two unspecified entities are equal (and thus `in`) if they have the same `Eid`. | ||
| TypecheckAnswer::success( | ||
| ExprBuilder::with_data(Some(Type::primitive_boolean())) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } else { | ||
| // nothing on the RHS is unspecified, so `unspecified in RHS` is always false | ||
| TypecheckAnswer::success( | ||
| ExprBuilder::with_data(Some(Type::singleton_boolean(false))) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } | ||
| } | ||
| (Some(EntityType::Unspecified), None) => { | ||
| // It's perfectly valid for `principal` or `resource` to be `EntityType::Unspecified` | ||
| if rhs_elems | ||
| .into_iter() | ||
| .any(|expr| Typechecker::is_unspecified_entity(request_env, expr)) | ||
| { | ||
| // something on the RHS is unspecified, so we have to type `unspecified in RHS` as Bool, | ||
| // because two unspecified entities are equal (and thus `in`) if they have the same `Eid`. | ||
| TypecheckAnswer::success( | ||
| ExprBuilder::with_data(Some(Type::primitive_boolean())) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } else { | ||
| // nothing on the RHS can be unspecified, so `unspecified in RHS` is always false | ||
| TypecheckAnswer::success( | ||
|
There was a problem hiding this comment. This might change strict validation for something like There was a problem hiding this comment. I think you're right. That doesn't mean this precision increase is invalid, just that it's currently breaking (unless/until we change There was a problem hiding this comment. Actually I'm not sure if you're correct. I believe There was a problem hiding this comment. Agreed that earlier handling handles this case. But I'm not sure this new definition matches the spec -- the Dafny code will always return |
||
| ExprBuilder::with_data(Some(Type::singleton_boolean(false))) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } | ||
| } | ||
| } | ||
| } | ||
|
|
||
|
|
@@ -2050,65 +2096,71 @@ impl<'a> Typechecker<'a> { | |
| lhs_expr: Expr<Option<Type>>, | ||
| rhs_expr: Expr<Option<Type>>, | ||
| ) -> TypecheckAnswer<'c> { | ||
| match ( | ||
| lhs_euid.entity_type(), | ||
| Typechecker::euids_from_euid_literals_or_action(request_env, rhs_elems), | ||
| ) { | ||
| (EntityType::Specified(name), Some(rhs)) => { | ||
| // We don't want to apply the action hierarchy check to | ||
| // non-action entities, but now we have a set of entities. | ||
| // We can apply the check as long as any are actions. The | ||
| // non-actions are omitted from the check, but they can | ||
| // never be an ancestor of `Action`. | ||
| let (actions, non_actions): (Vec<_>, Vec<_>) = | ||
| rhs.into_iter().partition(|e| match e.entity_type() { | ||
| EntityType::Specified(e_name) => is_action_entity_type(e_name), | ||
| EntityType::Unspecified => false, | ||
| }); | ||
| if is_action_entity_type(name) && !actions.is_empty() { | ||
| self.type_of_action_in_actions( | ||
| lhs_euid, | ||
| actions.iter(), | ||
| in_expr, | ||
| lhs_expr, | ||
| rhs_expr, | ||
| ) | ||
| } else if !is_action_entity_type(name) && !non_actions.is_empty() { | ||
| self.type_of_non_action_in_entities( | ||
| lhs_euid, | ||
| &non_actions, | ||
| in_expr, | ||
| lhs_expr, | ||
| rhs_expr, | ||
| ) | ||
| } else { | ||
| // This hard codes the assumption that `Action` can | ||
| // never be a member of any other entity type, and no | ||
| // other entity type can ever be a member of `Action`, | ||
| // and by extension any particular action entity. | ||
| TypecheckAnswer::success( | ||
| ExprBuilder::with_data(Some(Type::False)) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } | ||
| } | ||
| (EntityType::Specified(_), None) => { | ||
| // One or more of the elements on the right is not an entity | ||
| // literal. The `in` is still valid, so typechecking succeeds | ||
| // with type Boolean. | ||
| TypecheckAnswer::success( | ||
| ExprBuilder::with_data(Some(Type::primitive_boolean())) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } | ||
| (EntityType::Unspecified, _) => { | ||
| // This is a `TypecheckFail` because entity literals (`lhs_euid` | ||
| // in this case) are not allowed to have `Unspecified` type. | ||
| // Note that `Unspecified` entities will be detected by a | ||
| // different part of the validator, so all we need to do here is | ||
| // return `TypecheckFail`. | ||
| TypecheckAnswer::fail( | ||
| ExprBuilder::with_data(Some(Type::primitive_boolean())) | ||
| .with_same_source_loc(in_expr) | ||
| .is_in(lhs_expr, rhs_expr), | ||
| ) | ||
| } | ||
| } | ||
| } | ||
|
|
||
|
|
@@ -2191,15 +2243,15 @@ impl<'a> Typechecker<'a> { | |
|
|
||
| /// Check if the entity is in the list of descendants. Return the singleton | ||
| /// type false if it is not, and boolean otherwise. | ||
| fn entity_in_descendants<'b, T>( | ||
| lhs_entity: T, | ||
| rhs_descendants: impl IntoIterator<Item = T>, | ||
| in_expr: &Expr, | ||
| lhs_expr: Expr<Option<Type>>, | ||
| rhs_expr: Expr<Option<Type>>, | ||
| ) -> TypecheckAnswer<'b> | ||
| where | ||
| T: 'a + PartialEq, | ||
| { | ||
| let is_var_in_descendants = rhs_descendants.into_iter().any(|e| e == lhs_entity); | ||
| TypecheckAnswer::success( | ||
|
|
@@ -2401,13 +2453,15 @@ impl<'a> Typechecker<'a> { | |
| /// If the `maybe_action_var` expression is `Expr::Var(Var::Action)`, return | ||
| /// a expression for the entity uid for the action variable in the request | ||
| /// environment. Otherwise, return the expression unchanged. | ||
| fn replace_action_var_with_euid<T: 'a + Clone>( | ||
| request_env: &RequestEnv, | ||
| maybe_action_var: &'a Expr<T>, | ||
| ) -> Cow<'a, Expr<T>> { | ||
| match maybe_action_var.expr_kind() { | ||
| ExprKind::Var(Var::Action) => match request_env.action_entity_uid() { | ||
| Some(action) => Cow::Owned( | ||
| ExprBuilder::with_data(maybe_action_var.data().clone()).val(action.clone()), | ||
| ), | ||
| None => Cow::Borrowed(maybe_action_var), | ||
| }, | ||
| _ => Cow::Borrowed(maybe_action_var), | ||
|
|
||
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
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.
No problem with this generalization, but I don't see where it's necessary.