diff --git a/cedar-policy-symcc/src/err.rs b/cedar-policy-symcc/src/err.rs index 53377fc605..95e3595605 100644 --- a/cedar-policy-symcc/src/err.rs +++ b/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 }, + /// Request is not well-typed + #[error("request is not well typed with respect to the schema")] + RequestNotWellTyped(#[from] RequestValidationError), } pub type Result = std::result::Result; diff --git a/cedar-policy-symcc/src/lib.rs b/cedar-policy-symcc/src/lib.rs index 7cabe7e3c5..55c3500aa3 100644 --- a/cedar-policy-symcc/src/lib.rs +++ b/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 { + 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 { + 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, diff --git a/cedar-policy-symcc/src/symcc.rs b/cedar-policy-symcc/src/symcc.rs index 7a89d3b97f..aae7aa2134 100644 --- a/cedar-policy-symcc/src/symcc.rs +++ b/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