diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1edfc9936..79382ac4f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -15,7 +15,6 @@ jobs: matrix: toolchain: - stable - steps: - name: Checkout cedar-spec uses: actions/checkout@v3 @@ -44,6 +43,32 @@ jobs: dotnet tool restore dotnet tool run dafny-reportgenerator summarize-csv-results --max-resource-count 10000000 . || true + build_and_test_lean: + name: Build and Test Lean + runs-on: ubuntu-latest + strategy: + matrix: + toolchain: + - stable + steps: + - name: Checkout cedar-spec + uses: actions/checkout@v3 + with: + submodules: recursive + - name: Install Lean + shell: bash + run: | + wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh + bash elan-init.sh -y + - name: Build + working-directory: ./cedar-lean + shell: bash + run: source ~/.profile && lake build Cedar + - name: Test + working-directory: ./cedar-lean + shell: bash + run: source ~/.profile && lake exe CedarUnitTests + build_and_test_drt: name: Build and Test DRT runs-on: ubuntu-latest @@ -51,26 +76,22 @@ jobs: matrix: toolchain: - stable - steps: - name: Checkout cedar-spec uses: actions/checkout@v3 with: submodules: recursive + - name: Install Lean + shell: bash + run: | + wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh + bash elan-init.sh -y - name: Get Java 17 uses: actions/setup-java@v3 with: distribution: 'corretto' java-version: '17' cache: 'gradle' - - name: Build Dafny def engine - working-directory: ./cedar-dafny - shell: bash - run: make compile-difftest - - name: Build cedar-dafny-java-wrapper - working-directory: ./cedar-dafny-java-wrapper - shell: bash - run: ./gradlew build dumpClasspath - name: rustup run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }} - name: cargo fmt (cedar-policy-generators) @@ -85,46 +106,9 @@ jobs: - name: cargo rustc (cedar-policy-generators) working-directory: ./cedar-policy-generators run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose - - name: cargo rustc (cedar-drt) - working-directory: ./cedar-drt - run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose - - name: cargo rustc (cedar-drt/fuzz/) - working-directory: ./cedar-drt/fuzz - run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose - name: cargo test (cedar-policy-generators) working-directory: ./cedar-policy-generators run: cargo test --verbose - - name: cargo test (cedar-drt) - working-directory: ./cedar-drt - shell: bash - run: | - source ./set_env_vars.sh - export LD_LIBRARY_PATH=${LD_LIBRARY_PATH+$LD_LIBRARY_PATH:}$JAVA_HOME/lib/server - cargo test --verbose - - build_cedar_lean: - name: Build cedar-lean - runs-on: ubuntu-latest - strategy: - matrix: - toolchain: - - stable - - steps: - - name: Checkout cedar-spec - uses: actions/checkout@v3 - with: - submodules: recursive - - name: Install Lean - shell: bash - run: | - wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh - bash elan-init.sh -y - - name: Build - working-directory: ./cedar-lean - shell: bash - run: source ~/.profile && lake build Cedar - - name: Test - working-directory: ./cedar-lean + - name: build.sh shell: bash - run: source ~/.profile && lake exe CedarUnitTests + run: source ~/.profile && ./build.sh diff --git a/README.md b/README.md index d3f7c8a31..e06511bc1 100644 --- a/README.md +++ b/README.md @@ -15,14 +15,21 @@ This repository contains the Dafny formalization of Cedar and infrastructure for To build the Dafny formalization and proofs: -* Install Dafny 4.0, following the instructions [here](https://github.com/dafny-lang/dafny/wiki/INSTALL). Our proofs expect Z3 version 4.12.1, so if you have another copy of Z3 installed locally, you may need to adjust your PATH. +* Install Dafny, following the instructions [here](https://github.com/dafny-lang/dafny/wiki/INSTALL). Our proofs expect Z3 version 4.12.1, so if you have another copy of Z3 installed locally, you may need to adjust your PATH. * `cd cedar-dafny && make verify test` +To build the Lean formalization and proofs: + +* Install Lean, following the instructions [here](https://leanprover.github.io/lean4/doc/setup.html). +* `cd cedar-lean && lake build Cedar` + To build the DRT framework: -* Install Dafny, following the instructions above +* Install Dafny and Lean, following the instructions above. * `./build.sh` +Note that the build for DRT has only been tested on **Amazon Linux 2**. + ## Run To run DRT: diff --git a/build.sh b/build.sh index c06d65095..1eb531966 100755 --- a/build.sh +++ b/build.sh @@ -4,19 +4,33 @@ git submodule update --init # Set environment variables -cd cedar-drt && source ./set_env_vars.sh +cd cedar-drt +source set_env_vars.sh +cd .. + +# Build the Dafny formalization and extract to Java code +cd cedar-dafny +make compile-difftest cd .. -# Build the formalization and extract Java code -cd cedar-dafny && make compile-difftest +# Build the Dafny Java wrapper +cd cedar-dafny-java-wrapper +./gradlew build dumpClasspath cd .. -# Build the Java wrapper for DRT -cd cedar-dafny-java-wrapper && ./gradlew build dumpClasspath +# Build the Lean formalization and extract to static C libraries +cd cedar-lean +lake build Cedar:static DiffTest:static Std:static cd .. # Build DRT cd cedar-drt cargo build -cargo test -cd fuzz && RUSTFLAGS="--cfg=fuzzing" cargo build \ No newline at end of file + +# Run integration tests +source set_env_vars.sh +cargo test -- --nocapture + +# Build inner fuzz crate +cd fuzz && RUSTFLAGS="--cfg=fuzzing" cargo build +cargo test \ No newline at end of file diff --git a/cedar-drt/Cargo.toml b/cedar-drt/Cargo.toml index ee872c67d..df26838be 100644 --- a/cedar-drt/Cargo.toml +++ b/cedar-drt/Cargo.toml @@ -13,6 +13,7 @@ cedar-policy-core = { path = "../cedar/cedar-policy-core", version = "3.*", feat cedar-policy-validator = { path = "../cedar/cedar-policy-validator", version = "3.*", features = ["arbitrary"] } cedar-policy-formatter = { path = "../cedar/cedar-policy-formatter", version = "3.*" } jni = { version = "0.19.0", features = ["invocation"] } +lean-sys = { version = "0.0.5", features = ["small_allocator"], default-features = false } serde = { version = "1.0", features = ["derive"] } serde_json = "1.0" lazy_static = "1.4" diff --git a/cedar-drt/README.md b/cedar-drt/README.md index adfb1b57c..32a3bf872 100644 --- a/cedar-drt/README.md +++ b/cedar-drt/README.md @@ -26,5 +26,15 @@ The table below lists all available fuzz targets, including which component of t ## Logging -If the fuzz targets are compiled with the `log` features, then they will log their entire corpus to the file pointed at in the `LOGFILE` environment variable. +If the fuzz targets are compiled with the `log` features, then they will log their entire corpus to the file pointed at in the `LOGFILE` environment variable. The sampling rate can be controlled by the `RATE` environment variable, which defaults to 100% if not set. + + +## Debugging build failures + +If you run into weird build issues, +1. Make sure you have run `source set_env_vars.sh`, which sets all the environment variables needed to run the Dafny and Lean definitional code. +2. Try a `cargo clean` and rebuild. +3. If the steps above don't help, then file [an issue](https://github.com/cedar-policy/cedar-spec/issues). + +If everything builds, but the integration tests are failing, then it may be helpful to set `RUST_BACKTRACE=1` and run `cargo test -- --nocapture` to print additional test information. \ No newline at end of file diff --git a/cedar-drt/build.rs b/cedar-drt/build.rs new file mode 100644 index 000000000..82ed0b3c8 --- /dev/null +++ b/cedar-drt/build.rs @@ -0,0 +1,7 @@ +use std::env; +fn main() { + let lean_dir = env::var("LEAN_LIB_DIR").unwrap(); + println!("cargo:rustc-link-search=native=../cedar-lean/build/lib"); + println!("cargo:rustc-link-search=native={lean_dir}"); + println!("cargo:rustc-link-search=native=../cedar-lean/lake-packages/std/build/lib"); +} diff --git a/cedar-drt/fuzz/build.rs b/cedar-drt/fuzz/build.rs new file mode 100644 index 000000000..0c92dca61 --- /dev/null +++ b/cedar-drt/fuzz/build.rs @@ -0,0 +1,7 @@ +use std::env; +fn main() { + let lean_dir = env::var("LEAN_LIB_DIR").unwrap(); + println!("cargo:rustc-link-search=native=../../cedar-lean/build/lib"); + println!("cargo:rustc-link-search=native={lean_dir}"); + println!("cargo:rustc-link-search=native=../../cedar-lean/lake-packages/std/build/lib"); +} diff --git a/cedar-drt/lean-toolchain b/cedar-drt/lean-toolchain new file mode 120000 index 000000000..0eae579b0 --- /dev/null +++ b/cedar-drt/lean-toolchain @@ -0,0 +1 @@ +../cedar-lean/lean-toolchain \ No newline at end of file diff --git a/cedar-drt/set_env_vars.sh b/cedar-drt/set_env_vars.sh index 0a6f5effb..092fd620c 100644 --- a/cedar-drt/set_env_vars.sh +++ b/cedar-drt/set_env_vars.sh @@ -26,3 +26,9 @@ unset -f add_lib_to_path if [ -f "$(pwd)/../cedar-dafny-java-wrapper/build/libs/cedar-dafny-java-wrapper.jar" ]; then export CLASSPATH="$(< ../cedar-dafny-java-wrapper/build/runtimeClasspath.txt):$(pwd)/../cedar-dafny-java-wrapper/build/libs/cedar-dafny-java-wrapper.jar" fi + +# Set environment variables for Lean +export LEAN_LIB_DIR=$(lean --print-libdir) +export LD_LIBRARY_PATH=${LD_LIBRARY_PATH+$LD_LIBRARY_PATH:}$(lean --print-libdir) +export DYLD_LIBRARY_PATH=${DYLD_LIBRARY_PATH+$DYLD_LIBRARY_PATH:}$(lean --print-libdir) +export LD_PRELOAD=${LD_PRELOAD+$LD_PRELOAD:}$(lean --print-prefix)/lib/glibc/libm.so diff --git a/cedar-drt/src/dafny_java_impl.rs b/cedar-drt/src/dafny_java_impl.rs index c983d00de..04b052551 100644 --- a/cedar-drt/src/dafny_java_impl.rs +++ b/cedar-drt/src/dafny_java_impl.rs @@ -18,19 +18,18 @@ //! implementation extracted from the Dafny specification. use crate::cedar_test_impl::*; +use crate::definitional_request_types::*; use crate::logger::*; use cedar_policy::frontend::is_authorized::InterfaceResponse; use cedar_policy::integration_testing::{CustomCedarImpl, IntegrationTestValidationResult}; -pub use cedar_policy::Response; use cedar_policy_core::ast::{Expr, Value}; pub use cedar_policy_core::*; -pub use cedar_policy_validator::{ValidationMode, ValidationResult, ValidatorSchema}; +pub use cedar_policy_validator::{ValidationMode, ValidatorSchema}; pub use entities::Entities; use jni::objects::{JObject, JString, JValue}; use jni::{JNIVersion, JavaVM}; use lazy_static::lazy_static; use log::info; -use serde::{Deserialize, Serialize}; /// Times to (de)serialize JSON content sent to / received from the Dafny-Java /// implementation. @@ -67,50 +66,6 @@ lazy_static! { }; } -#[derive(Debug, Serialize)] -struct RequestForDefEngine<'a> { - request: &'a ast::Request, - policies: &'a ast::PolicySet, - entities: &'a Entities, -} - -#[derive(Debug, Serialize, Deserialize)] -pub struct DefinitionalAuthResponse { - serialization_nanos: i64, - deserialization_nanos: i64, - auth_nanos: i64, - response: InterfaceResponse, -} - -#[derive(Debug, Serialize)] -struct EvalRequestForDefEngine<'a> { - request: &'a ast::Request, - entities: &'a Entities, - expr: &'a ast::Expr, - expected: Option<&'a ast::Expr>, -} - -#[derive(Debug, Serialize, Deserialize, Clone, Copy)] -#[repr(transparent)] -struct DefinitionalEvalResponse { - matches: bool, -} - -#[derive(Debug, Serialize)] -struct RequestForDefValidator<'a> { - schema: &'a ValidatorSchema, - policies: &'a ast::PolicySet, - mode: ValidationMode, -} - -#[derive(Debug, Deserialize)] -pub struct DefinitionalValResponse { - serialization_nanos: i64, - deserialization_nanos: i64, - validation_nanos: i64, - response: ValidationInterfaceResponse, -} - /// The lifetime parameter 'j is the lifetime of the JVM instance pub struct JavaDefinitionalEngine<'j> { /// Thread attached to the JVM diff --git a/cedar-drt/src/definitional_request_types.rs b/cedar-drt/src/definitional_request_types.rs new file mode 100644 index 000000000..5a0bc00aa --- /dev/null +++ b/cedar-drt/src/definitional_request_types.rs @@ -0,0 +1,66 @@ +/* + * Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * https://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +use crate::cedar_test_impl::*; +use cedar_policy::frontend::is_authorized::InterfaceResponse; +pub use cedar_policy_core::*; +pub use cedar_policy_validator::{ValidationMode, ValidatorSchema}; +pub use entities::Entities; +use serde::{Deserialize, Serialize}; + +#[derive(Debug, Serialize)] +pub struct RequestForDefEngine<'a> { + pub request: &'a ast::Request, + pub policies: &'a ast::PolicySet, + pub entities: &'a Entities, +} + +#[derive(Debug, Serialize, Deserialize)] +pub struct DefinitionalAuthResponse { + pub serialization_nanos: i64, + pub deserialization_nanos: i64, + pub auth_nanos: i64, + pub response: InterfaceResponse, +} + +#[derive(Debug, Serialize)] +pub struct EvalRequestForDefEngine<'a> { + pub request: &'a ast::Request, + pub entities: &'a Entities, + pub expr: &'a ast::Expr, + pub expected: Option<&'a ast::Expr>, +} + +#[derive(Debug, Serialize, Deserialize, Clone, Copy)] +#[repr(transparent)] +pub struct DefinitionalEvalResponse { + pub matches: bool, +} + +#[derive(Debug, Serialize)] +pub struct RequestForDefValidator<'a> { + pub schema: &'a ValidatorSchema, + pub policies: &'a ast::PolicySet, + pub mode: ValidationMode, +} + +#[derive(Debug, Deserialize)] +pub struct DefinitionalValResponse { + pub serialization_nanos: i64, + pub deserialization_nanos: i64, + pub validation_nanos: i64, + pub response: ValidationInterfaceResponse, +} diff --git a/cedar-drt/src/lean_impl.rs b/cedar-drt/src/lean_impl.rs new file mode 100644 index 000000000..4f31dd480 --- /dev/null +++ b/cedar-drt/src/lean_impl.rs @@ -0,0 +1,281 @@ +/* + * Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * https://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +//! Implementation of the [`CedarTestImplementation`] trait for the Cedar Lean +//! implementation. + +// NOTE: We use the env var RUST_LEAN_INTERFACE_INIT to save the fact that +// we've already initialized. + +use core::panic; +use std::{collections::HashSet, env, ffi::CString}; + +use crate::cedar_test_impl::*; +use crate::definitional_request_types::*; +use cedar_policy::frontend::is_authorized::InterfaceResponse; +use cedar_policy::integration_testing::{CustomCedarImpl, IntegrationTestValidationResult}; +use cedar_policy_core::ast::{Expr, Value}; +pub use cedar_policy_core::*; +pub use cedar_policy_validator::{ValidationMode, ValidatorSchema}; +pub use entities::Entities; +pub use lean_sys::init::lean_initialize; +pub use lean_sys::lean_object; +pub use lean_sys::string::lean_mk_string; +use lean_sys::{ + lean_initialize_runtime_module, lean_io_mark_end_initialization, lean_io_mk_world, + lean_string_cstr, +}; +use serde::{Deserialize, Serialize}; +use std::ffi::CStr; +use std::str::FromStr; + +#[link(name = "Cedar", kind = "static")] +#[link(name = "Std", kind = "static")] +#[link(name = "DiffTest", kind = "static")] +extern "C" { + fn isAuthorizedDRT(req: *mut lean_object) -> *mut lean_object; + fn validateDRT(req: *mut lean_object) -> *mut lean_object; + fn initialize_DiffTest_Main(builtin: i8, ob: *mut lean_object) -> *mut lean_object; +} + +#[derive(Serialize, Deserialize)] +struct ListDef { + l: Vec, +} + +#[derive(Serialize, Deserialize)] +struct SetDef { + mk: ListDef, +} + +#[derive(Serialize, Deserialize)] +struct AuthorizationResponseInner { + policies: SetDef, + decision: String, +} + +#[derive(Serialize, Deserialize)] +enum AuthorizationResponse { + /// Successful execution of the `isAuthorized` function + #[serde(rename = "ok")] + Ok(AuthorizationResponseInner), + /// Failure due to an error in the testing harness (e.g., a parse error on the Lean side) + #[serde(rename = "error")] + Error(String), +} + +#[derive(Serialize, Deserialize)] +enum ValidationResponseInner { + /// Successful validation + #[serde(rename = "ok")] + Ok(()), + /// Validation error case + #[serde(rename = "error")] + Error(String), +} + +#[derive(Serialize, Deserialize)] +enum ValidationResponse { + /// Successful execution of the `validate` function + #[serde(rename = "ok")] + Ok(ValidationResponseInner), + /// Failure due to an error in the testing harness (e.g., a parse error on the Lean side) + #[serde(rename = "error")] + Error(String), +} + +pub struct LeanDefinitionalEngine {} + +fn lean_obj_to_string(o: *mut lean_object) -> String { + let lean_obj_p = unsafe { lean_string_cstr(o) }; + let lean_obj_cstr = unsafe { CStr::from_ptr(lean_obj_p as *const i8) }; + lean_obj_cstr + .to_str() + .expect("failed to convert Lean object to string") + .to_owned() +} + +impl LeanDefinitionalEngine { + pub fn new() -> Self { + if env::var("RUST_LEAN_INTERFACE_INIT").is_err() { + unsafe { lean_initialize_runtime_module() }; + unsafe { lean_initialize() }; + unsafe { initialize_DiffTest_Main(1, lean_io_mk_world()) }; + unsafe { lean_io_mark_end_initialization() }; + env::set_var("RUST_LEAN_INTERFACE_INIT", "1"); + } + Self {} + } + + fn serialize_authorization_request( + request: &ast::Request, + policies: &ast::PolicySet, + entities: &Entities, + ) -> *mut lean_object { + let request: String = serde_json::to_string(&RequestForDefEngine { + request, + policies, + entities, + }) + .expect("failed to serialize request, policies, or entities"); + let cstring = CString::new(request).expect("`CString::new` failed"); + unsafe { lean_mk_string(cstring.as_ptr() as *const u8) } + } + + fn deserialize_authorization_response(response: *mut lean_object) -> InterfaceResponse { + let response_string = lean_obj_to_string(response); + let resp: AuthorizationResponse = + serde_json::from_str(&response_string).expect("could not deserialize json"); + match resp { + AuthorizationResponse::Ok(resp) => { + let dec: authorizer::Decision = match resp.decision.as_str() { + "allow" => authorizer::Decision::Allow, + "deny" => authorizer::Decision::Deny, + _ => panic!("Lean code returned unknown decision {}", resp.decision), + }; + + let reason = resp + .policies + .mk + .l + .into_iter() + .map(|x| { + cedar_policy::PolicyId::from_str(&x).expect("could not coerce policyId") + }) + .collect(); + InterfaceResponse::new(dec, reason, HashSet::new()) + } + AuthorizationResponse::Error(err) => panic!("Error returned by Lean code: {err}"), + } + } + + /// Ask the definitional engine whether `isAuthorized` for the given `request`, + /// `policies`, and `entities` + pub fn is_authorized( + &self, + request: &ast::Request, + policies: &ast::PolicySet, + entities: &Entities, + ) -> InterfaceResponse { + let req = Self::serialize_authorization_request(request, policies, entities); + let response = unsafe { isAuthorizedDRT(req) }; + Self::deserialize_authorization_response(response) + } + + fn serialize_validation_request( + schema: &ValidatorSchema, + policies: &ast::PolicySet, + ) -> *mut lean_object { + let request: String = serde_json::to_string(&RequestForDefValidator { + schema, + policies, + mode: cedar_policy_validator::ValidationMode::default(), // == Strict + }) + .expect("failed to serialize schema or policies"); + let cstring = CString::new(request).expect("`CString::new` failed"); + unsafe { lean_mk_string(cstring.as_ptr() as *const u8) } + } + + fn deserialize_validation_response(response: *mut lean_object) -> ValidationInterfaceResponse { + let response_string = lean_obj_to_string(response); + let resp: ValidationResponse = + serde_json::from_str(&response_string).expect("could not deserialize json"); + match resp { + ValidationResponse::Ok(resp) => { + let validation_errors = match resp { + ValidationResponseInner::Ok(_) => Vec::new(), + ValidationResponseInner::Error(err) => vec![err], + }; + ValidationInterfaceResponse { + validation_errors, + parse_errors: Vec::new(), + } + } + ValidationResponse::Error(err) => panic!("Error returned by Lean code: {err}"), + } + } + + /// Use the definitional validator to validate the given `policies` given a `schema` + pub fn validate( + &self, + schema: &ValidatorSchema, + policies: &ast::PolicySet, + ) -> ValidationInterfaceResponse { + let req = Self::serialize_validation_request(schema, policies); + let response = unsafe { validateDRT(req) }; + Self::deserialize_validation_response(response) + } +} + +impl CedarTestImplementation for LeanDefinitionalEngine { + fn is_authorized( + &self, + request: ast::Request, + policies: &ast::PolicySet, + entities: &Entities, + ) -> InterfaceResponse { + self.is_authorized(&request, policies, entities) + } + + fn interpret( + &self, + _request: ast::Request, + _entities: &Entities, + _expr: &Expr, + _expected: Option, + ) -> bool { + // TODO + unimplemented!("Unimplemented: interpret"); + } + + fn validate( + &self, + schema: &cedar_policy_validator::ValidatorSchema, + policies: &ast::PolicySet, + mode: ValidationMode, + ) -> ValidationInterfaceResponse { + assert_eq!( + mode, + ValidationMode::Strict, + "Lean definitional validator only supports `Strict` mode" + ); + self.validate(schema, policies) + } +} + +/// Implementation of the trait used for integration testing. +impl CustomCedarImpl for LeanDefinitionalEngine { + fn is_authorized( + &self, + request: &ast::Request, + policies: &ast::PolicySet, + entities: &Entities, + ) -> InterfaceResponse { + self.is_authorized(request, policies, entities) + } + + fn validate( + &self, + schema: cedar_policy_validator::ValidatorSchema, + policies: &ast::PolicySet, + ) -> IntegrationTestValidationResult { + let result = self.validate(&schema, policies); + IntegrationTestValidationResult { + validation_passed: result.validation_passed(), + validation_errors_debug: format!("{:?}", result.validation_errors), + } + } +} diff --git a/cedar-drt/src/lib.rs b/cedar-drt/src/lib.rs index 8ea4f7ea7..a1383dd82 100644 --- a/cedar-drt/src/lib.rs +++ b/cedar-drt/src/lib.rs @@ -14,12 +14,15 @@ * limitations under the License. */ -#![forbid(unsafe_code)] mod cedar_test_impl; mod dafny_java_impl; +mod definitional_request_types; +mod lean_impl; mod logger; pub mod utils; pub use cedar_test_impl::*; pub use dafny_java_impl::*; +pub use definitional_request_types::*; +pub use lean_impl::*; pub use logger::*; diff --git a/cedar-drt/tests/integration_tests.rs b/cedar-drt/tests/integration_tests.rs index 871a4c9a1..a8c2babed 100644 --- a/cedar-drt/tests/integration_tests.rs +++ b/cedar-drt/tests/integration_tests.rs @@ -69,8 +69,14 @@ fn run_integration_tests(custom_impl: &dyn CustomCedarImpl) { } #[test] -fn integration_tests_on_java_def_impl() { +fn integration_tests_on_def_impl() { + //WARNING: We need to create lean def engine first so the JVM signal handlers are aware of it. + //If this needs to change at some point in the future, you'll need to add libjsig.so to LD_PRELOAD + //WARNING: Different tests run in new threads by default, so don't separate these. + let lean_def_impl = LeanDefinitionalEngine::new(); + run_integration_tests(&lean_def_impl); + let java_def_impl = - JavaDefinitionalEngine::new().expect("failed to create definitional engine"); - run_integration_tests(&java_def_impl) + JavaDefinitionalEngine::new().expect("failed to create Dafny definitional engine"); + run_integration_tests(&java_def_impl); }