Helper functions for template analysis

cedar-policy-symcc/src/err.rs

@@ -16,7 +16,7 @@
 
 //! All error types in SymCC.
 
-use cedar_policy_core::validator::ValidationError;
+use cedar_policy_core::validator::{RequestValidationError, ValidationError};
 use miette::Diagnostic;
 use thiserror::Error;
 
@@ -51,6 +51,12 @@ pub enum Error {
     /// Errors during concretization.
     #[error("failed to recover a concrete counterexample")]
     ConcretizeError(#[from] ConcretizeError),
+    /// Template is not well-typed.
+    #[error("input template is not well typed with respect to the schema {errs:?}")]
+    TemplateNotWellTyped { errs: Vec<ValidationError> },
+    /// Request is not well-typed
+    #[error("request is not well typed with respect to the schema")]
+    RequestNotWellTyped(#[from] RequestValidationError),
 }
 
 pub type Result<T> = std::result::Result<T, Error>;

cedar-policy-symcc/src/lib.rs

@@ -19,7 +19,7 @@
 pub mod err;
 mod symcc;
 
-use cedar_policy::{Policy, PolicySet, RequestEnv, Schema};
+use cedar_policy::{Policy, PolicySet, Request, RequestEnv, Schema, Template};
 use std::fmt;
 
 use err::{Error, Result};
@@ -28,7 +28,8 @@ use symcc::Environment;
 use symcc::SymCompiler;
 use symcc::{
     verify_always_allows, verify_always_denies, verify_disjoint, verify_equivalent, verify_implies,
-    verify_never_errors, well_typed_policies, well_typed_policy,
+    verify_never_errors, well_typed_policies, well_typed_policy, well_typed_request,
+    well_typed_template,
 };
 
 pub use symcc::bitvec;
@@ -130,6 +131,71 @@ impl fmt::Display for WellTypedPolicies {
     }
 }
 
+#[derive(Debug)]
+pub struct WellTypedTemplate {
+    template: cedar_policy_core::ast::Template,
+}
+
+impl WellTypedTemplate {
+    /// Returns a reference to the underlying template
+    pub fn template(&self) -> &cedar_policy_core::ast::Template {
+        &self.template
+    }
+
+    /// Creates a well-typed template with respect to the given request environment and schema.
+    /// This ensures that the template satisfies the `WellTyped` constraints required by the
+    /// symbolic compiler, by applying Cedar's typechecker transformations.
+    pub fn from_template(
+        template: &Template,
+        env: &RequestEnv,
+        schema: &Schema,
+    ) -> Result<WellTypedTemplate> {
+        well_typed_template(template.as_ref(), env, schema)
+            .map(|t| WellTypedTemplate { template: t })
+    }
+
+    /// Converts a [`Template`] to a [`WellTypedTemplate`] unchecked.
+    /// Note that SymCC may fail on the template produced by this function.
+    pub fn from_template_unchecked(template: &Template) -> Self {
+        WellTypedTemplate {
+            template: template.as_ref().clone(),
+        }
+    }
+}
+
+impl fmt::Display for WellTypedTemplate {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}", self.template)
+    }
+}
+
+#[derive(Debug)]
+pub struct WellTypedRequest {
+    request: cedar_policy_core::ast::Request,
+}
+
+impl WellTypedRequest {
+    /// Returns a reference to the underlying request
+    pub fn request(&self) -> &cedar_policy_core::ast::Request {
+        &self.request
+    }
+
+    /// Creates a well-typed request with respect to the given schema.
+    /// This ensures that the request satisfies the `WellTyped` constraints required by the
+    /// symbolic compiler, by applying Cedar's typechecker transformations.
+    pub fn from_request(request: &Request, schema: &Schema) -> Result<WellTypedRequest> {
+        well_typed_request(request.as_ref(), schema).map(|r| WellTypedRequest { request: r })
+    }
+
+    /// Converts a [`Request`] to a [`WellTypedRequest`] unchecked.
+    /// Note that SymCC may fail on the request produced by this function.
+    pub fn from_request_unchecked(request: &Request) -> Self {
+        WellTypedRequest {
+            request: request.as_ref().clone(),
+        }
+    }
+}
+
 /// Cedar symbolic compiler, which takes your policies and schemas
 /// and converts them to SMT queries to perform various verification
 /// tasks such as checking if a policy set always allows/denies,

cedar-policy-symcc/src/symcc.rs

@@ -43,11 +43,15 @@ pub mod term_type;
 pub mod type_abbrevs;
 pub mod verifier;
 
-use cedar_policy::Schema;
+use cedar_policy::{Request, Schema};
 use decoder::{parse_sexpr, IdMaps};
 use env::to_validator_request_env;
 
-use cedar_policy_core::ast::{Expr, ExprBuilder, Policy, PolicySet};
+use cedar_policy_core::ast::{
+    ActionConstraint, Annotations, Expr, ExprBuilder, Policy, PolicySet, PrincipalConstraint,
+    ResourceConstraint, Template,
+};
+use cedar_policy_core::extensions::Extensions;
 use cedar_policy_core::validator::{typecheck::Typechecker, types::RequestEnv, ValidationMode};
 use encoder::Encoder;
 use solver::{Decision, Solver};
@@ -468,3 +472,78 @@ pub fn well_typed_policies(
         Err(err) => Err(err),
     }
 }
+
+pub fn well_typed_template(
+    template: &Template,
+    env: &cedar_policy::RequestEnv,
+    schema: &Schema,
+) -> Result<Template> {
+    let env = to_validator_request_env(env, schema.as_ref())
+        .ok_or_else(|| Error::ActionNotInSchema(env.action().to_string()))?;
+    well_typed_template_inner(template, &env, schema)
+}
+
+fn well_typed_template_inner(
+    template: &Template,
+    env: &RequestEnv<'_>,
+    schema: &Schema,
+) -> Result<Template> {
+    let validator_schema = schema.as_ref();
+    let type_checker = Typechecker::new(validator_schema, ValidationMode::Strict);
+    let template_check = type_checker.typecheck_by_single_request_env(template, env);
+    match template_check {
+        cedar_policy_core::validator::typecheck::PolicyCheck::Success(expr) => Ok(Template::new(
+            template.id().clone(),
+            template.loc().cloned(),
+            Annotations::default(),
+            template.effect(),
+            PrincipalConstraint::any(),
+            ActionConstraint::any(),
+            ResourceConstraint::any(),
+            expr.into_expr::<ExprBuilder<()>>(),
+        )),
+        cedar_policy_core::validator::typecheck::PolicyCheck::Irrelevant(errs, expr) =>
+        // A template could be irrelevant just for this environment, so unless there were errors we don't want to fail.
+        // Note that if the template was irrelevant for all environments schema validation would have caught this
+        // before SymCC.
+        {
+            if errs.is_empty() {
+                Ok(Template::new(
+                    template.id().clone(),
+                    template.loc().cloned(),
+                    Annotations::default(),
+                    template.effect(),
+                    PrincipalConstraint::any(),
+                    ActionConstraint::any(),
+                    ResourceConstraint::any(),
+                    expr.into_expr::<ExprBuilder<()>>(),
+                ))
+            } else {
+                Err(Error::TemplateNotWellTyped { errs })
+            }
+        }
+        cedar_policy_core::validator::typecheck::PolicyCheck::Fail(errs) => {
+            Err(Error::TemplateNotWellTyped { errs })
+        }
+    }
+}
+
+pub fn well_typed_request(
+    request: &cedar_policy_core::ast::Request,
+    schema: &Schema,
+) -> Result<cedar_policy_core::ast::Request> {
+    let validator_schema = schema.as_ref();
+    let principal = request.principal().clone();
+    let action = request.action().clone();
+    let resource = request.action().clone();
+    let context = request.context();
+    cedar_policy_core::ast::Request::new_with_unknowns(
+        principal,
+        action,
+        resource,
+        context.cloned(),
+        Some(validator_schema),
+        Extensions::all_available(),
+    )
+    .map_err(|e| Error::RequestNotWellTyped(e))
+}

cedar-policy-symcc/src/symcc/authorizer.rs

@@ -14,7 +14,7 @@
  * limitations under the License.
  */
 use cedar_policy::Effect;
-use cedar_policy_core::ast::{Policy, PolicySet};
+use cedar_policy_core::ast::{Policy, PolicySet, Template};
 
 use crate::symcc::{
     compiler::compile,
@@ -59,3 +59,33 @@ pub fn is_authorized(policies: &PolicySet, env: &SymEnv) -> Result<Term, Compile
     let permits = satisfied_policies(Effect::Permit, policies, env)?;
     Ok(and(permits, not(forbids)))
 }
+
+pub fn satisfied_with_effect_template(
+    effect: Effect,
+    template: &Template,
+    env: &SymEnv,
+) -> Result<Option<Term>, CompileError> {
+    if template.effect() == effect {
+        Ok(Some(compile(&template.condition(), env)?))
+    } else {
+        Ok(None)
+    }
+}
+
+pub fn satsified_templates(
+    effect: Effect,
+    template: &Template,
+    env: &SymEnv,
+) -> Result<Term, CompileError> {
+    let terms = std::iter::once(template)
+        .filter_map(|t| satisfied_with_effect_template(effect, t, env).transpose())
+        .collect::<Result<Vec<Term>, CompileError>>()?
+        .into_iter();
+    Ok(any_satisfied(terms))
+}
+
+pub fn is_authorized_template(template: &Template, env: &SymEnv) -> Result<Term, CompileError> {
+    let forbids = satsified_templates(Effect::Forbid, template, env)?;
+    let permits = satsified_templates(Effect::Permit, template, env)?;
+    Ok(and(permits, not(forbids)))
+}

cedar-policy-symcc/src/symcc/compiler.rs

@@ -26,8 +26,8 @@
 
 use std::sync::Arc;
 
-use cedar_policy_core::ast::Var;
 use cedar_policy_core::ast::{BinaryOp, Expr, ExprKind, UnaryOp};
+use cedar_policy_core::ast::{SlotId, Var};
 
 use super::bitvec::BitVec;
 use super::env::{SymEntities, SymEnv, SymRequest};
@@ -61,6 +61,36 @@ fn compile_prim(p: &Prim, es: &SymEntities) -> Result<Term> {
     }
 }
 
+fn compile_slot(slot: &SlotId, req: &SymRequest) -> Result<Term> {
+    if slot.is_principal() {
+        match &req.principal_slot {
+            Some(term) => {
+                if term.type_of().is_entity_type() {
+                    Ok(some_of(term.clone()))
+                } else {
+                    Err(CompileError::TypeError)
+                }
+            }
+            None => Err(CompileError::PrincipalSlotTypeNotProvided),
+        }
+    } else if slot.is_resource() {
+        match &req.resource_slot {
+            Some(term) => {
+                if term.type_of().is_entity_type() {
+                    Ok(some_of(term.clone()))
+                } else {
+                    Err(CompileError::TypeError)
+                }
+            }
+            None => Err(CompileError::ResourceSlotTypeNotProvided),
+        }
+    } else {
+        Err(CompileError::UnsupportedFeature(
+            "generalized slots are not supported".to_string(),
+        ))
+    }
+}
+
 fn compile_var(v: Var, req: &SymRequest) -> Result<Term> {
     match v {
         Var::Principal => {
@@ -618,6 +648,7 @@ pub fn compile(x: &Expr, env: &SymEnv) -> Result<Term> {
     match x.expr_kind() {
         ExprKind::Lit(l) => compile_prim(l, &env.entities),
         ExprKind::Var(v) => compile_var(*v, &env.request),
+        ExprKind::Slot(s) => compile_slot(s, &env.request),
         ExprKind::If {
             test_expr: x1,
             then_expr: x2,
@@ -698,9 +729,6 @@ pub fn compile(x: &Expr, env: &SymEnv) -> Result<Term> {
                 .collect::<Result<Vec<_>>>()?;
             compile_call(fn_name, ts)
         }
-        ExprKind::Slot(_) => Err(CompileError::UnsupportedFeature(
-            "templates/slots are not supported".to_string(),
-        )),
         ExprKind::Unknown(_) => Err(CompileError::UnsupportedFeature(
             "partial evaluation is not supported".to_string(),
         )),

cedar-policy-symcc/src/symcc/enforcer.rs

@@ -92,7 +92,7 @@ pub(crate) fn footprint<'a>(x: &'a Expr, env: &'a SymEnv) -> Box<dyn Iterator<It
     // PANIC SAFETY
     #[allow(clippy::unimplemented, reason = "Should fail at an earlier stage")]
     match x.expr_kind() {
-        ExprKind::Lit(_) | ExprKind::Var(_) => of_entity(x),
+        ExprKind::Lit(_) | ExprKind::Var(_) | ExprKind::Slot(_) => of_entity(x),
         ExprKind::If {
             test_expr,
             then_expr,
@@ -132,7 +132,6 @@ pub(crate) fn footprint<'a>(x: &'a Expr, env: &'a SymEnv) -> Box<dyn Iterator<It
             Box::new(exprs.iter().flat_map(|x| footprint(x, env)))
         }
         ExprKind::Record(axs) => Box::new(axs.iter().flat_map(|(_, x)| footprint(x, env))),
-        ExprKind::Slot(_) => unimplemented!("analyzing templates is not currently supported"),
         ExprKind::Unknown(_) => {
             unimplemented!("analyzing partial expressions is not currently supported")
         }