diff --git a/Cargo.lock b/Cargo.lock index 5ca5242..8e3e6e7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -86,9 +86,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.82" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f538837af36e6f6a9be0faa67f9a314f8119e4e4b5867c6ab40ed60360142519" +checksum = "b3d1d046238990b9cf5bcde22a3fb3584ee5cf65fb2765f454ed428c7a0063da" [[package]] name = "arc-swap" @@ -162,7 +162,7 @@ dependencies = [ "regex", "rustc-hash", "shlex", - "syn 2.0.60", + "syn 2.0.66", "which", ] @@ -201,9 +201,9 @@ checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c" [[package]] name = "cc" -version = "1.0.97" +version = "1.0.98" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "099a5357d84c4c61eb35fc8eafa9a79a902c2f76911e5747ced4e032edd8d9b4" +checksum = "41c270e7540d725e65ac7f1b212ac8ce349719624d7bcff99f8e2e488e8cf03f" dependencies = [ "jobserver", "libc", @@ -227,9 +227,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clang-sys" -version = "1.7.0" +version = "1.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67523a3b4be3ce1989d607a828d036249522dd9c1c8de7f4dd2dae43a37369d1" +checksum = "a483f3cbf7cec2e153d424d0e92329d816becc6421389bd494375c6065921b9b" dependencies = [ "glob", "libc", @@ -268,7 +268,7 @@ dependencies = [ "heck 0.5.0", "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] @@ -348,6 +348,7 @@ dependencies = [ "concrete_session", "itertools 0.12.1", "thiserror", + "tracing", ] [[package]] @@ -434,9 +435,9 @@ dependencies = [ [[package]] name = "crc32fast" -version = "1.4.0" +version = "1.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3855a8a784b474f333699ef2bbca9db2c4a1f6d9088a90a2d25b1eb53111eaa" +checksum = "a97769d94ddab943e4510d138150169a2758b5ef3eb191a9ee688de3e23ef7b3" dependencies = [ "cfg-if", ] @@ -456,9 +457,9 @@ dependencies = [ [[package]] name = "crossbeam-channel" -version = "0.5.12" +version = "0.5.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ab3db02a9c5b5121e1e42fbdb1aeb65f5e02624cc58c43f2884c6ccac0b82f95" +checksum = "33480d6946193aa8033910124896ca395333cae7e2d1113d1fef6c3272217df2" dependencies = [ "crossbeam-utils", ] @@ -493,9 +494,9 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.19" +version = "0.8.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "248e3bacc7dc6baa3b21e405ee045c3047101a49145e7e9eca583ab4c2ca5345" +checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80" [[package]] name = "crunchy" @@ -593,9 +594,9 @@ dependencies = [ [[package]] name = "deunicode" -version = "1.4.4" +version = "1.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "322ef0094744e63628e6f0eb2295517f79276a5b342a4c2ff3042566ca181d4e" +checksum = "339544cc9e2c4dc3fc7149fd630c5f22263a4fdf18a98afd0075784968b5cf00" [[package]] name = "dirs-next" @@ -627,20 +628,20 @@ dependencies = [ "enum-ordinalize", "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] name = "either" -version = "1.11.0" +version = "1.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a47c1c47d2f5964e29c61246e81db715514cd532db6b5116a25ea3c03d6780a2" +checksum = "3dca9240753cf90908d7e4aac30f630662b02aebaa1b58a3cadabdb23385b58b" [[package]] name = "ena" -version = "0.14.2" +version = "0.14.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c533630cf40e9caa44bd91aadc88a75d75a4c3a12b4cfde353cbed41daa1e1f1" +checksum = "3d248bdd43ce613d87415282f69b9bb99d947d290b10962dd6c56233312c2ad5" dependencies = [ "log", ] @@ -668,7 +669,7 @@ checksum = "0d28318a75d4aead5c4db25382e8ef717932d0346600cacae6357eb5941bc5ff" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] @@ -679,9 +680,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.8" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a258e46cdc063eb8519c00b9fc845fc47bcfca4130e2f08e88665ceda8474245" +checksum = "534c5cf6194dfab3db3242765c03bbe257cf92f22b38f6bc0c58d59108a820ba" dependencies = [ "libc", "windows-sys 0.52.0", @@ -746,9 +747,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.14" +version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94b22e06ecb0110981051723910cbf0b5f5e09a2062dd7663334ee79a9d1286c" +checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" dependencies = [ "cfg-if", "libc", @@ -958,9 +959,9 @@ checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55" [[package]] name = "libc" -version = "0.2.154" +version = "0.2.155" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae743338b92ff9146ce83992f766a31066a91a8c84a45e0e9f21e7cf6de6d346" +checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c" [[package]] name = "libgit2-sys" @@ -1012,9 +1013,9 @@ dependencies = [ [[package]] name = "libz-sys" -version = "1.1.16" +version = "1.1.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e143b5e666b2695d28f6bca6497720813f699c9602dd7f5cac91008b8ada7f9" +checksum = "c15da26e5af7e25c90b37a2d75cdbf940cf4a55316de9d84c679c9b8bfabf82e" dependencies = [ "cc", "libc", @@ -1036,9 +1037,9 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f" [[package]] name = "linux-raw-sys" -version = "0.4.13" +version = "0.4.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "01cda141df6706de531b6c46c3a33ecca755538219bd484262fa09410c13539c" +checksum = "78b3ae25bc7c8c38cec158d1f2757ee79e9b3740fbc7ccf0e59e4b08d793fa89" [[package]] name = "llvm-sys" @@ -1091,7 +1092,7 @@ dependencies = [ "proc-macro2", "quote", "regex-syntax 0.8.3", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] @@ -1136,7 +1137,7 @@ dependencies = [ "proc-macro2", "quote", "regex", - "syn 2.0.60", + "syn 2.0.66", "tblgen-alt", "unindent", ] @@ -1155,9 +1156,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" [[package]] name = "miniz_oxide" -version = "0.7.2" +version = "0.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9d811f3e15f28568be3407c8e7fdb6514c1cda3cb30683f15b6a1a1dc4ea14a7" +checksum = "87dfd01fe195c66b572b37921ad8803d010623c0aca821bea2302239d155cdae" dependencies = [ "adler", ] @@ -1263,9 +1264,9 @@ checksum = "caff54706df99d2a78a5a4e3455ff45448d81ef1bb63c22cd14052ca0e993a3f" [[package]] name = "parking_lot" -version = "0.12.2" +version = "0.12.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e4af0ca4f6caed20e900d564c242b8e5d4903fdacf31d3daf527b66fe6f42fb" +checksum = "f1bf18183cf54e8d6059647fc3063646a1801cf30896933ec2311622cc4b9a27" dependencies = [ "lock_api", "parking_lot_core", @@ -1286,9 +1287,9 @@ dependencies = [ [[package]] name = "paste" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de3145af08024dea9fa9914f381a17b8fc6034dfb00f3a84013f7ff43f29ed4c" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" [[package]] name = "percent-encoding" @@ -1298,9 +1299,9 @@ checksum = "e3148f5046208a5d56bcfc03053e3ca6334e51da8dfb19b6cdc8b306fae3283e" [[package]] name = "petgraph" -version = "0.6.4" +version = "0.6.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e1d3afd2628e69da2be385eb6f2fd57c8ac7977ceeff6dc166ff1657b0e386a9" +checksum = "b4c5cc86750666a3ed20bdaf5ca2a0344f9c67674cae0515bec2da16fbaa47db" dependencies = [ "fixedbitset", "indexmap", @@ -1361,19 +1362,19 @@ checksum = "925383efa346730478fb4838dbe9137d2a47675ad789c546d150a6e1dd4ab31c" [[package]] name = "prettyplease" -version = "0.2.19" +version = "0.2.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5ac2cf0f2e4f42b49f5ffd07dae8d746508ef7526c13940e5f524012ae6c6550" +checksum = "5f12335488a2f3b0a83b14edad48dca9879ce89b2edd10e80237e4e852dd645e" dependencies = [ "proc-macro2", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] name = "proc-macro2" -version = "1.0.81" +version = "1.0.84" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3d1597b0c024618f09a9c3b8655b7e430397a36d23fdafec26d6965e9eec3eba" +checksum = "ec96c6a92621310b51366f1e28d05ef11489516e93be030060e5fc12024a49d6" dependencies = [ "unicode-ident", ] @@ -1487,15 +1488,15 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.15" +version = "1.0.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "80af6f9131f277a45a3fba6ce8e2258037bb0477a67e610d3c1fe046ab31de47" +checksum = "955d28af4278de8121b7ebeb796b6a45735dc01436d898801014aced2773a3d6" [[package]] name = "ryu" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e86697c916019a8588c99b5fac3cead74ec0b4b819707a682fd4d23fa0ce1ba1" +checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f" [[package]] name = "salsa-2022" @@ -1544,35 +1545,35 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "semver" -version = "1.0.22" +version = "1.0.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "92d43fe69e652f3df9bdc2b85b2854a0825b86e4fb76bc44d945137d053639ca" +checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" [[package]] name = "serde" -version = "1.0.200" +version = "1.0.203" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ddc6f9cc94d67c0e21aaf7eda3a010fd3af78ebf6e096aa6e2e13c79749cce4f" +checksum = "7253ab4de971e72fb7be983802300c30b5a7f0c2e56fab8abfc6a214307c0094" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.200" +version = "1.0.203" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "856f046b9400cee3c8c94ed572ecdb752444c24528c035cd35882aad6f492bcb" +checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] name = "serde_json" -version = "1.0.116" +version = "1.0.117" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3e17db7126d17feb94eb3fad46bf1a96b034e8aacbc2e775fe81505f8b0b2813" +checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3" dependencies = [ "itoa", "ryu", @@ -1581,9 +1582,9 @@ dependencies = [ [[package]] name = "serde_spanned" -version = "0.6.5" +version = "0.6.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb3622f419d1296904700073ea6cc23ad690adbd66f13ea683df73298736f0c1" +checksum = "79e674e01f999af37c49f70a6ede167a8a60b2503e56c5599532a65baa5969a0" dependencies = [ "serde", ] @@ -1669,9 +1670,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.60" +version = "2.0.66" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "909518bc7b1c9b779f1bbf07f2929d35af9f0f37e47c6e9ef7f9dddc1e1821f3" +checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5" dependencies = [ "proc-macro2", "quote", @@ -1764,7 +1765,7 @@ dependencies = [ "cfg-if", "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] @@ -1775,28 +1776,28 @@ checksum = "5c89e72a01ed4c579669add59014b9a524d609c0c88c6a585ce37485879f6ffb" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", "test-case-core", ] [[package]] name = "thiserror" -version = "1.0.59" +version = "1.0.61" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f0126ad08bff79f29fc3ae6a55cc72352056dfff61e3ff8bb7129476d44b23aa" +checksum = "c546c80d6be4bc6a00c0f01730c08df82eaa7a7a61f11d656526506112cc1709" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.59" +version = "1.0.61" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d1cd413b5d558b4c5bf3680e324a6fa5014e7b7c067a51e69dbdf47eb7148b66" +checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] @@ -1866,9 +1867,9 @@ checksum = "1f3ccbac311fea05f86f61904b462b55fb3df8837a366dfc601a0161d0532f20" [[package]] name = "toml" -version = "0.8.12" +version = "0.8.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e9dd1545e8208b4a5af1aa9bbd0b4cf7e9ea08fabc5d0a5c67fcaafa17433aa3" +checksum = "a4e43f8cc456c9704c851ae29c67e17ef65d2c30017c17a9765b89c382dc8bba" dependencies = [ "serde", "serde_spanned", @@ -1878,18 +1879,18 @@ dependencies = [ [[package]] name = "toml_datetime" -version = "0.6.5" +version = "0.6.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3550f4e9685620ac18a50ed434eb3aec30db8ba93b0287467bca5826ea25baf1" +checksum = "4badfd56924ae69bcc9039335b2e017639ce3f9b001c393c1b2d1ef846ce2cbf" dependencies = [ "serde", ] [[package]] name = "toml_edit" -version = "0.22.12" +version = "0.22.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3328d4f68a705b2a4498da1d580585d39a6510f98318a2cec3018a7ec61ddef" +checksum = "c127785850e8c20836d49732ae6abfa47616e60bf9d9f57c43c250361a9db96c" dependencies = [ "indexmap", "serde", @@ -1917,7 +1918,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] [[package]] @@ -2097,7 +2098,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", "wasm-bindgen-shared", ] @@ -2119,7 +2120,7 @@ checksum = "e94f17b526d0a461a191c78ea52bbce64071ed5c04c9ffe424dcb38f74171bb7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -2410,20 +2411,20 @@ checksum = "cfe53a6657fd280eaa890a3bc59152892ffa3e30101319d168b781ed6529b049" [[package]] name = "zerocopy" -version = "0.7.33" +version = "0.7.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "087eca3c1eaf8c47b94d02790dd086cd594b912d2043d4de4bfdd466b3befb7c" +checksum = "ae87e3fcd617500e5d106f0380cf7b77f3c6092aae37191433159dda23cfb087" dependencies = [ "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.7.33" +version = "0.7.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f4b6c273f496d8fd4eaf18853e6b448760225dc030ff2c485a786859aea6393" +checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn 2.0.66", ] diff --git a/README.md b/README.md index c2274a7..1c5c32a 100644 --- a/README.md +++ b/README.md @@ -239,12 +239,12 @@ Features: - casts ✔️ - arrays 🏗️ - iterators :x: -- for :x: +- for 🏗️ - match :x: - option :x: - enums :x: - impl :x: -- linear type checker :x: +- linear type checker 🏗️ - borrow checker :x: - generics :x: - traits :x: diff --git a/crates/concrete_check/Cargo.toml b/crates/concrete_check/Cargo.toml index 8affcac..a5a20c2 100644 --- a/crates/concrete_check/Cargo.toml +++ b/crates/concrete_check/Cargo.toml @@ -12,3 +12,5 @@ concrete_ir = { version = "0.1.0", path = "../concrete_ir" } concrete_session = { version = "0.1.0", path = "../concrete_session" } itertools = "0.12.0" thiserror = "1.0.56" +tracing.workspace = true + diff --git a/crates/concrete_check/src/lib.rs b/crates/concrete_check/src/lib.rs index 25a3d44..7554c15 100644 --- a/crates/concrete_check/src/lib.rs +++ b/crates/concrete_check/src/lib.rs @@ -4,6 +4,8 @@ use ariadne::{ColorGenerator, Label, Report, ReportKind}; use concrete_ir::lowering::errors::LoweringError; use concrete_session::Session; +pub mod linearity_check; + /// Creates a report from a lowering error. pub fn lowering_error_to_report( error: LoweringError, diff --git a/crates/concrete_check/src/linearity_check.rs b/crates/concrete_check/src/linearity_check.rs new file mode 100644 index 0000000..11bf651 --- /dev/null +++ b/crates/concrete_check/src/linearity_check.rs @@ -0,0 +1,992 @@ +use std::collections::HashMap; + +use concrete_session::Session; + +use self::errors::LinearityError; +pub mod errors; + +use concrete_ast::expressions::{Expression, PathOp, StructInitField, ValueExpr}; +use concrete_ast::functions::{FunctionDecl, FunctionDef, Param}; +use concrete_ast::modules::ModuleDefItem; +use concrete_ast::statements::{AssignStmt, Binding, LetStmt, LetStmtTarget, Statement}; +use concrete_ast::Program; +use std::path::PathBuf; + +use concrete_ast::types::TypeSpec; + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +enum VarState { + Unconsumed, + Consumed, + _Borrowed, + _BorrowedMut, +} + +#[derive(Debug, Clone, PartialEq)] +pub struct VarInfo { + ty: String, //TODO Define 'Type' as a struct or enum? + depth: usize, + state: VarState, +} + +#[derive(Debug, Clone, Copy, PartialEq)] +enum CountResult { + Zero, + One, + MoreThanOne, +} + +#[derive(Debug, Clone, Copy)] +struct Appearances { + consumed: u32, + write: u32, + read: u32, + path: u32, +} + +#[allow(dead_code)] +enum BorrowMode { + ReadBorrow, + WriteBorrow, +} + +impl Appearances { + fn new(consumed: u32, write: u32, read: u32, path: u32) -> Self { + Appearances { + consumed, + write, + read, + path, + } + } + + fn partition(count: u32) -> CountResult { + match count { + 0 => CountResult::Zero, + 1 => CountResult::One, + _ => CountResult::MoreThanOne, + } + } + + fn zero() -> Self { + Self::new(0, 0, 0, 0) + } + + fn consumed_once() -> Self { + Self::new(1, 0, 0, 0) + } + + // When borrowed implemented + fn _read_once() -> Self { + Self::new(0, 0, 1, 0) + } + + fn _write_once() -> Self { + Self::new(0, 1, 0, 0) + } + + fn path_once() -> Self { + Self::new(0, 0, 0, 1) + } + + fn merge(&self, other: &Appearances) -> Self { + Appearances { + consumed: self.consumed + other.consumed, + write: self.write + other.write, + read: self.read + other.read, + path: self.path + other.path, + } + } + + fn _merge_list(appearances: Vec) -> Self { + appearances + .into_iter() + .fold(Self::zero(), |acc, x| acc.merge(&x)) + } +} + +#[derive(Debug, Clone)] +struct StateTbl { + vars: HashMap, +} + +/// StateTbl is a table that keeps track of the state of variables in a program for doing linearityCheck. The core of algorithm is decision table +impl StateTbl { + // Initialize with an empty state table + fn new() -> Self { + Self { + vars: HashMap::new(), + } + } + + fn init(&mut self, vars: Vec<(String, String)>, depth: usize) { + for (name, ty) in vars { + self.vars.insert( + name.to_string(), + VarInfo { + ty: ty.to_string(), + depth, + state: VarState::Unconsumed, + }, + ); + } + } + // Example of updating the state table + fn update_info(&mut self, var: &str, info: VarInfo) { + self.vars.insert(var.to_string(), info); + } + + // Remove a variable from the state table + fn _remove_entry(&mut self, var: &str) { + self.vars.remove(var); + } + + fn remove_entries(&mut self, vars: Vec) { + for var in vars { + self.vars.remove(&var); + } + } + + fn get_info_mut(&mut self, var: &str) -> Option<&mut VarInfo> { + if !self.vars.contains_key(var) { + self.vars.insert( + var.to_string(), + VarInfo { + ty: "".to_string(), + depth: 0, + state: VarState::Unconsumed, + }, + ); + tracing::debug!( + "Variable {} not found in state table. Inserting with default state", + var + ); + } + self.vars.get_mut(var) + } + + fn get_info(&self, var: &str) -> Option<&VarInfo> { + self.vars.get(var) + } + + // Retrieve a variable's state + fn _get_state(&mut self, var: &str) -> Option<&VarState> { + if let Some(info) = self.get_info(var) { + Some(&info.state) + } else { + None + } + } + + // Retrieve a variable's state + fn update_state(&mut self, var: &str, new_state: &VarState) { + let info = self.get_info_mut(var); + if let Some(info) = info { + //info.state = new_state.clone(); + info.state = *new_state; + } + } + + fn get_loop_depth(&mut self, name: &str) -> usize { + let state = self.get_info(name); + if let Some(state) = state { + state.depth + } else { + 0 + } + } + + pub fn _tables_are_consistent(&self, other: &StateTbl) -> Result<(), LinearityError> { + for (key, value) in &self.vars { + if let Some(other_value) = other.vars.get(key) { + if value != other_value { + return Err(LinearityError::StateInconsistency { + message: format!( + "Variable '{}' state mismatch: {:?} != {:?}", + key, value, other_value + ), + }); + } + } else { + return Err(LinearityError::StateInconsistency { + message: format!("Variable '{}' not found in the other table", key), + }); + } + } + // Also check for variables in `other` not present in `self` + for key in other.vars.keys() { + if !self.vars.contains_key(key) { + return Err(LinearityError::StateInconsistency { + message: format!("Variable '{}' not found in the first table", key), + }); + } + } + + Ok(()) + } +} + +struct LinearityChecker {} + +#[allow(dead_code)] +#[allow(unused_variables)] +impl LinearityChecker { + fn new() -> Self { + LinearityChecker {} + } + + fn consume_once( + &self, + mut state_tbl: StateTbl, + depth: usize, + name: &str, + ) -> Result { + let loop_depth = state_tbl.get_loop_depth(name); + tracing::debug!( + "Consuming variable: {} depth {} loop_depth {}", + name, + depth, + loop_depth + ); + if depth == state_tbl.get_loop_depth(name) { + // Consumed when a variable defined inside the loop is consumed + state_tbl.update_state(name, &VarState::Consumed); + tracing::debug!("Consumed variable: {}", name); + Ok(state_tbl) + } else { + Err(LinearityError::ConsumedVariableInLoop { + variable: name.to_string(), + }) + } + } + + fn check_expr( + &self, + mut state_tbl: StateTbl, + depth: usize, + expr: &Expression, + context: &str, + ) -> Result { + // Assuming you have a method to get all variable names and types + //let vars = &mut self.state_tbl.vars; + //TODO check if we can avoid cloning + let vars = state_tbl.vars.clone(); + println!("Check_expr vars {:?}", vars); + for (name, _info) in vars.iter() { + //self.check_var_in_expr(depth, &name, &info.ty, expr)?; + state_tbl = self + .check_var_in_expr(state_tbl, depth, name, expr, context) + .unwrap(); + } + Ok(state_tbl) + } + + fn count_in_statements(&self, name: &str, statements: &[Statement]) -> Appearances { + statements + .iter() + .map(|stmt| self.count_in_statement(name, stmt)) + .fold(Appearances::zero(), |acc, x| acc.merge(&x)) + } + + fn count_in_statement(&self, name: &str, statement: &Statement) -> Appearances { + match statement { + Statement::Let(binding) => { + // Handle let bindings, possibly involving pattern matching + self.count_in_expression(name, &binding.value) + } + Statement::If(if_stmt) => { + // Process all components of an if expression + let cond_apps = self.count_in_expression(name, &if_stmt.value); + let then_apps = self.count_in_statements(name, &if_stmt.contents); + let else_apps; + let else_statements = &if_stmt.r#else; + if let Some(else_statements) = else_statements { + else_apps = self.count_in_statements(name, else_statements); + } else { + else_apps = Appearances::zero(); + } + cond_apps.merge(&then_apps).merge(&else_apps) + } + Statement::While(while_expr) => { + let cond = &while_expr.value; + let block = &while_expr.contents; + // Handle while loops + self.count_in_expression(name, cond) + .merge(&self.count_in_statements(name, block)) + } + Statement::For(for_expr) => { + // Handle for loops + //init, cond, post, block + let init = &for_expr.init; + let cond = &for_expr.condition; + let post = &for_expr.post; + let block = &for_expr.contents; + let mut apps = Appearances::zero(); + if let Some(init) = init { + if let Some(cond) = cond { + if let Some(post) = post { + apps = self + .count_in_let_statements(name, init) + .merge(&self.count_in_expression(name, cond)) + .merge(&self.count_in_assign_statement(name, post)) + .merge(&self.count_in_statements(name, block)) + } + } + } + apps + } + Statement::Assign(assign_stmt) => { + // Handle assignments + self.count_in_assign_statement(name, assign_stmt) + } + Statement::Return(return_stmt) => { + // Handle return statements + if let Some(value) = &return_stmt.value { + self.count_in_expression(name, value) + } else { + Appearances::zero() + } + } + Statement::FnCall(fn_call_op) => { + // Process function call arguments + //fn_call_op.target.iter().map(|arg| self.count_in_path_op(name, arg)).fold(Appearances::zero(), |acc, x| acc.merge(&x)); + fn_call_op + .args + .iter() + .map(|arg| self.count_in_expression(name, arg)) + .fold(Appearances::zero(), |acc, x| acc.merge(&x)) + } + Statement::Match(_) => { + todo!("do not support match statement") + } //_ => Appearances::zero(), + } + } + + fn count_in_assign_statement(&self, name: &str, assign_stmt: &AssignStmt) -> Appearances { + let AssignStmt { + target, + derefs, + value, + span, + } = assign_stmt; + // Handle assignments + let ret = self.count_in_path_op(name, target, true); + ret.merge(&self.count_in_expression(name, value)); + ret + } + + fn count_in_path_op(&self, name: &str, path_op: &PathOp, lvalue: bool) -> Appearances { + if name == path_op.first.name { + if lvalue { + Appearances::consumed_once() + } else { + Appearances::path_once() + } + } else { + Appearances::zero() + } + } + + fn count_in_let_statements(&self, name: &str, let_stmt: &LetStmt) -> Appearances { + let LetStmt { + is_mutable, + target, + value, + span, + } = let_stmt; + self.count_in_expression(name, value) + } + + fn count_in_expression(&self, name: &str, expr: &Expression) -> Appearances { + match expr { + Expression::Value(value_expr, _) => { + // Handle value expressions, typically constant or simple values + match value_expr { + ValueExpr::Path(path) => { + if name == path.first.name { + Appearances::path_once() + // FIXME + // This is a stub implementation. The only call with path is as an lvalue + // But we should have a clever implementation. + // An approach is to difference when a path is an lvalue or an rvalue, contained in the Path itself + //Appearances::consumed_once() + } else { + Appearances::zero() + } + } + ValueExpr::ConstBool(_, _) + | ValueExpr::ConstChar(_, _) + | ValueExpr::ConstInt(_, _) + | ValueExpr::ConstFloat(_, _) + | ValueExpr::ConstStr(_, _) => Appearances::zero(), + } + } + Expression::FnCall(fn_call_op) => { + // Process function call arguments + fn_call_op + .args + .iter() + .map(|arg| self.count_in_expression(name, arg)) + .fold(Appearances::zero(), |acc, x| acc.merge(&x)) + } + Expression::Match(match_expr) => todo!("do not support match expression"), + //Match expressions should be implemented as an extension of if expressions + Expression::If(if_expr) => { + // Process all components of an if expression + // TODO review this code. If expressions should be processed counting both branches and comparing them + let cond_apps = self.count_in_expression(name, &if_expr.value); + let then_apps = self.count_in_statements(name, &if_expr.contents); + cond_apps.merge(&then_apps); + if let Some(else_block) = &if_expr.r#else { + let else_apps = self.count_in_statements(name, else_block); + cond_apps.merge(&then_apps).merge(&else_apps); + } + cond_apps + } + Expression::UnaryOp(_, expr) => { + // Unary operations likely don't change the count but process the inner expression + self.count_in_expression(name, expr) + } + Expression::BinaryOp(left, _, right) => { + // Handle binary operations by processing both sides + self.count_in_expression(name, left) + .merge(&self.count_in_expression(name, right)) + } + Expression::StructInit(struct_init_expr) => { + // Handle struct initialization + struct_init_expr + .fields + .values() + .map(|expr| self.count_struct_init(name, expr)) + .fold(Appearances::zero(), |acc, x| acc.merge(&x)) + } + Expression::ArrayInit(array_init_expr) => { + // Handle array initializations + array_init_expr + .values + .iter() + .map(|expr| self.count_in_expression(name, expr)) + .fold(Appearances::zero(), |acc, x| acc.merge(&x)) + } + Expression::Deref(expr, _) + | Expression::AsRef(expr, _, _) + | Expression::Cast(expr, _, _) => { + // Deref, AsRef, and Cast are handled by just checking the inner expression + self.count_in_expression(name, expr) + } // Add more cases as necessary based on the Expression types you expect + } + } + + fn count_struct_init(&self, name: &str, struct_init: &StructInitField) -> Appearances { + tracing::debug!("Checking struct init: {:?}", struct_init); + self.count_in_expression(name, &struct_init.value) + } + + fn check_stmt_let( + &self, + mut state_tbl: StateTbl, + depth: usize, + binding: &LetStmt, + context: &str, + ) -> Result { + // Handle let bindings, possibly involving pattern matching + let LetStmt { + is_mutable, + target, + value, + span, + } = binding; + match target { + LetStmtTarget::Simple { name, r#type } => { + match r#type { + TypeSpec::Simple { + name: variable_type, + qualifiers, + span, + } => { + state_tbl.update_info( + &name.name, + VarInfo { + ty: variable_type.name.clone(), + depth, + state: VarState::Unconsumed, + }, + ); + } + TypeSpec::Generic { + name: variable_type, + qualifiers, + type_params, + span, + } => { + state_tbl.update_info( + &name.name, + VarInfo { + ty: variable_type.name.clone(), + depth, + state: VarState::Unconsumed, + }, + ); + } + TypeSpec::Array { + of_type, + size, + qualifiers, + span, + } => { + let array_type = "Array<".to_string() + &of_type.get_name() + ">"; + state_tbl.update_info( + &name.name, + VarInfo { + ty: array_type, + depth, + state: VarState::Unconsumed, + }, + ); + } + } + self.check_var_in_expr(state_tbl, depth, &name.name, value, context) + } + LetStmtTarget::Destructure(bindings) => { + for binding in bindings { + let new_state_tbl = self.check_bindings(&state_tbl, depth, binding); + if let Ok(new_state_tbl) = new_state_tbl { + state_tbl = new_state_tbl; + } + } + Ok(state_tbl) + } + } + } + + fn check_bindings( + &self, + state_tbl: &StateTbl, + depth: usize, + binding: &Binding, + ) -> Result { + // TODO Do something with the bindings + tracing::debug!("TODO implement Checking bindings: {:?}", binding); + Ok(state_tbl.clone()) + } + + fn check_function( + &self, + mut state_tbl: StateTbl, + depth: usize, + function_def: &FunctionDef, + ) -> Result { + let decl = &function_def.decl; + // Handle function declarations + let FunctionDecl { + doc_string, + generic_params, + name, + params, + ret_type, + is_extern, + is_pub, + attributes, + span, + } = decl; + let errors: Vec = Vec::new(); + tracing::debug!("Checking function declaration: {:?}", decl); + let mut params_vec: Vec<(String, String)> = Vec::new(); + let mut params_clean_vec: Vec = Vec::new(); + for param in params { + let Param { name, r#type } = param; + let name = name.name.clone(); + let r#type = match r#type { + TypeSpec::Simple { + name: variable_type, + qualifiers, + span, + } => variable_type.name.clone(), + TypeSpec::Generic { + name: variable_type, + qualifiers, + type_params, + span, + } => variable_type.name.clone(), + TypeSpec::Array { + of_type, + size, + qualifiers, + span, + } => "Array<".to_string() + &of_type.get_name() + ">", + }; + params_vec.push((name.clone(), r#type)); + let var_clean = name.clone(); + params_clean_vec.push(var_clean); + } + state_tbl.init(params_vec, depth); + + //function.decl + for statement in &function_def.body { + //tracing::debug!("Checking linearity for function body: {:?}", function.body); + let stmt_context = format!("{:?}", statement); + state_tbl = self.check_stmt(state_tbl, 0, statement, &stmt_context)?; + } + tracing::debug!( + "Finished checking linearity for function: {} {:?}", + function_def.decl.name.name, + state_tbl + ); + state_tbl.remove_entries(params_clean_vec); + //if errors.len() > 0 { + if !errors.is_empty() { + //FIXME replace with Vec + Err(errors[0].clone()) + } else { + Ok(state_tbl) + } + } + + fn check_stmts( + &self, + mut state_tbl: StateTbl, + depth: usize, + stmts: &Vec, + context: &str, + ) -> Result { + for stmt in stmts { + state_tbl = self.check_stmt(state_tbl, depth, stmt, context)?; + } + Ok(state_tbl) + } + + fn check_stmt( + &self, + mut state_tbl: StateTbl, + depth: usize, + stmt: &Statement, + context: &str, + ) -> Result { + match stmt { + Statement::Let(binding) => { + // Handle let bindings, possibly involving pattern matching + self.check_stmt_let(state_tbl, depth, binding, context) + } + //Statement::If(cond, then_block, else_block) => { + Statement::If(if_stmt) => { + // Handle conditional statements + state_tbl = self.check_expr(state_tbl, depth, &if_stmt.value, context)?; + state_tbl = self.check_stmts(state_tbl, depth + 1, &if_stmt.contents, context)?; + if let Some(else_block) = &if_stmt.r#else { + state_tbl = self.check_stmts(state_tbl, depth + 1, else_block, context)?; + } + Ok(state_tbl) + } + //Statement::While(cond, block) => { + Statement::While(while_stmt) => { + // Handle while loops + state_tbl = self.check_expr(state_tbl, depth, &while_stmt.value, context)?; + state_tbl = + self.check_stmts(state_tbl, depth + 1, &while_stmt.contents, context)?; + Ok(state_tbl) + } + //Statement::For(init, cond, post, block) => { + Statement::For(for_stmt) => { + // Handle for loops + if let Some(init) = &for_stmt.init { + state_tbl = self.check_stmt_let(state_tbl, depth, init, context)?; + } + if let Some(condition) = &for_stmt.condition { + state_tbl = self.check_expr(state_tbl, depth, condition, context)?; + } + if let Some(post) = &for_stmt.post { + //TODO check assign statement + //self.check_stmt_assign(depth, post)?; + } + state_tbl = self.check_stmts(state_tbl, depth + 1, &for_stmt.contents, context)?; + Ok(state_tbl) + } + Statement::Assign(assign_stmt) => { + // Handle assignments + let AssignStmt { + target, + derefs, + value, + span, + } = assign_stmt; + tracing::debug!("Checking assignment: {:?}", assign_stmt); + let target_context = format!("target <{:?}>", target); + state_tbl = self.check_path_opt(state_tbl, depth, target, &target_context)?; + let value_context = format!("value <{:?}>", value); + state_tbl = self.check_expr(state_tbl, depth, value, &value_context)?; + + //state_tbl = self.check_var_in_expr(state_tbl, depth, name, expr, ""); + Ok(state_tbl) + } + Statement::Return(return_stmt) => { + let errors: Vec = Vec::new(); + for (name, var_info) in state_tbl.vars.iter() { + //FIXME implement Checking of consumed variables + /* + match var_info.state { + VarState::Consumed => (), // If consumed, do nothing. + _ => match var_info.ty { + Type::WriteRef(_) | Type::SpanMut(_) => (), // Write references and write spans can be dropped implicitly. + _ if self.universe_linear_ish(var_info.ty) => { + // If the type is linear-ish and the variable is not consumed, raise an error. + errors.push(Err(LinearityError::VariableNotConsumed { + variable_name: name.clone(), + message: format!("The variable {} is not consumed by the time of the return statement. Did you forget to call a destructor, or destructure the contents?", name), + })); + () + } + _ => () + } + } + */ + } + //if errors.len() > 0 { + if !errors.is_empty() { + Err(errors[0].clone()) + } else { + Ok(state_tbl) + } + } + Statement::FnCall(fn_call_op) => { + // Process function call arguments + for arg in &fn_call_op.args { + state_tbl = self.check_expr(state_tbl, depth, arg, context)?; + } + Ok(state_tbl) + } + Statement::Match(_) => { + tracing::debug!("Skipping linearity check for statement type: \n{:?}", stmt); + todo!("Implement linearity checkt for match statement") + } + } + } + + fn check_path_opt( + &self, + state_tbl: StateTbl, + depth: usize, + path_op: &PathOp, + context: &str, + ) -> Result { + tracing::debug!("Checking path: {:?}", path_op); + let var_expression = Expression::Value( + concrete_ast::expressions::ValueExpr::Path(path_op.clone()), + path_op.span, + ); + self.check_var_in_expr( + state_tbl, + depth, + &path_op.first.name, + &var_expression, + context, + ) + } + + fn check_var_in_expr( + &self, + state_tbl: StateTbl, + depth: usize, + name: &str, + expr: &Expression, + context: &str, + ) -> Result { + let info = state_tbl.get_info(name); // Assume default state + if let Some(info) = info { + //Only checks Linearity for types of name Linear + // TODO improve this approach + if info.ty == *"Linear".to_string() { + let state = &info.state; + let apps = self.count_in_expression(name, expr); // Assume count function implementation + let Appearances { + consumed, + write, + read, + path, + } = apps; + //tracing::debug!("Checking variable: {} with state: {:?} and appearances: {:?} in expression {:?}", name, state, apps, expr); + tracing::debug!( + "Checking state_tbl variable: {}: {:?} {:?} \n <<< context {:?} >>> \n << expression {:?} >>", + name, info, apps, context, expr + ); + match ( + state, + Appearances::partition(consumed), + Appearances::partition(write), + Appearances::partition(read), + Appearances::partition(path), + ) { + /*( State Consumed WBorrow RBorrow Path ) + (* ------------------|-------------------|-----------------|------------------|----------------)*/ + // Not yet consumed, and at most used through immutable borrows or path reads. + (VarState::Unconsumed, CountResult::Zero, CountResult::Zero, _, _) => { + Ok(state_tbl) + } + // Not yet consumed, borrowed mutably once, and nothing else. + ( + VarState::Unconsumed, + CountResult::Zero, + CountResult::One, + CountResult::Zero, + CountResult::Zero, + ) => Ok(state_tbl), + // Not yet consumed, borrowed mutably, then either borrowed immutably or accessed through a path. + (VarState::Unconsumed, CountResult::Zero, CountResult::One, _, _) => { + Err(LinearityError::BorrowedMutUsed { + variable: name.to_string(), + }) + } + // Not yet consumed, borrowed mutably more than once. + (VarState::Unconsumed, CountResult::Zero, CountResult::MoreThanOne, _, _) => { + Err(LinearityError::BorrowedMutMoreThanOnce { + variable: name.to_string(), + }) + } + // Not yet consumed, consumed once, and nothing else. Valid IF the loop depth matches. + ( + VarState::Unconsumed, + CountResult::One, + CountResult::Zero, + CountResult::Zero, + CountResult::Zero, + ) => self.consume_once(state_tbl, depth, name), + // Not yet consumed, consumed once, then either borrowed or accessed through a path. + (VarState::Unconsumed, CountResult::One, _, _, _) => { + Err(LinearityError::ConsumedAndUsed { + variable: name.to_string(), + }) + } + // Not yet consumed, consumed more than once. + (VarState::Unconsumed, CountResult::MoreThanOne, _, _, _) => { + Err(LinearityError::ConsumedMoreThanOnce { + variable: name.to_string(), + }) + } + // Read borrowed, and at most accessed through a path. + ( + VarState::_Borrowed, + CountResult::Zero, + CountResult::Zero, + CountResult::Zero, + _, + ) => Ok(state_tbl), + // Read borrowed, and either consumed or borrowed again. + (VarState::_Borrowed, _, _, _, _) => Err(LinearityError::ReadBorrowedAndUsed { + variable: name.to_string(), + }), + // Write borrowed, unused. + ( + VarState::_BorrowedMut, + CountResult::Zero, + CountResult::Zero, + CountResult::Zero, + CountResult::Zero, + ) => Ok(state_tbl), + // Write borrowed, used in some way. + (VarState::_BorrowedMut, _, _, _, _) => { + Err(LinearityError::WriteBorrowedAndUsed { + variable: name.to_string(), + }) + } + // Already consumed, and unused. + ( + VarState::Consumed, + CountResult::Zero, + CountResult::Zero, + CountResult::Zero, + CountResult::Zero, + ) => Ok(state_tbl), + // Already consumed, and used in some way. + (VarState::Consumed, _, _, _, _) => { + Err(LinearityError::AlreadyConsumedAndUsed { + variable: name.to_string(), + }) + } + } + } else { + //Only checks Linearity for types of name Linear + Ok(state_tbl) + } + } else { + Err(LinearityError::VariableNotFound { + variable: name.to_string(), + }) + } + } +} + +// This is because there is no warranty check_function returned state_tbl is readed once +//#[allow(unused_assignments)] +pub fn linearity_check_program( + programs: &Vec<(PathBuf, String, Program)>, + _session: &Session, +) -> Result { + tracing::debug!("Starting linearity check"); + let checker = LinearityChecker::new(); + for (_path, name, program) in programs { + tracing::debug!("Checking linearity for program: {}", name); + for module in &program.modules { + tracing::debug!("Checking linearity for module: {}", module.name.name); + for module_content in &module.contents { + let mut state_tbl = StateTbl::new(); + match module_content { + ModuleDefItem::Function(function) => { + //tracing::debug!("Checking linearity for function: {:?}", function); + //checker.check_function(&function)?; + //FIXME check function function.decl + state_tbl = checker.check_function(state_tbl, 0, function)?; + //checker.linearity_check(&function)?; + } + ModuleDefItem::FunctionDecl(function_decl) => { + tracing::debug!( + "Skipping linearity check for FunctionDecl: {:?}", + function_decl + ); + } + ModuleDefItem::Module(module) => { + tracing::debug!("Skipping linearity check for Module: {:?}", module); + } + ModuleDefItem::Struct(struc) => { + //tracing::debug!("Skipping linearity check for Struct: {:?}", module_content); + //checker. + state_tbl.update_info( + &struc.name.name, + VarInfo { + ty: "Struct".to_string(), + depth: 0, + state: VarState::Unconsumed, + }, + ); + } + ModuleDefItem::Enum(_) => { + tracing::debug!("Skipping linearity check for Enum: {:?}", module_content); + } + ModuleDefItem::Constant(_) => { + tracing::debug!( + "Skipping linearity check for Constant: {:?}", + module_content + ); + } + ModuleDefItem::Union(_) => { + tracing::debug!("Skipping linearity check for Uinon: {:?}", module_content); + } + ModuleDefItem::Type(_) => { + tracing::debug!( + "Skipping linearity check for module content: {:?}", + module_content + ); + } /*_ => + { + tracing::debug!("Skipping linearity check for module content: {:?}", module_content); + () + },*/ + } + tracing::debug!( + "Finished linearity check for module {} with resulting state_tbl {:?}", + module.name.name, + state_tbl + ); + } + } + } + Ok("OK".to_string()) +} diff --git a/crates/concrete_check/src/linearity_check/errors.rs b/crates/concrete_check/src/linearity_check/errors.rs new file mode 100644 index 0000000..d72968d --- /dev/null +++ b/crates/concrete_check/src/linearity_check/errors.rs @@ -0,0 +1,37 @@ +//use concrete_ir::Span; + +use thiserror::Error; + +#[derive(Debug, Error, Clone)] +pub enum LinearityError { + #[error("Variable {variable} not consumed")] + NotConsumed { variable: String }, + #[error("Borrowed mutably and used for variable {variable}")] + BorrowedMutUsed { variable: String }, + #[error("Variable {variable} borrowed mutably more than once")] + BorrowedMutMoreThanOnce { variable: String }, + #[error("Variable {variable} consumed once and then used again")] + ConsumedAndUsed { variable: String }, + #[error("Variable {variable} consumed more than once")] + ConsumedMoreThanOnce { variable: String }, + #[error("Variable {variable} read borrowed and used in other ways")] + ReadBorrowedAndUsed { variable: String }, + #[error("Variable {variable} write borrowed and used")] + WriteBorrowedAndUsed { variable: String }, + #[error("Variable {variable} already consumed and used again")] + AlreadyConsumedAndUsed { variable: String }, + #[error("Unhandled state or appearance count for Variable {variable}")] + UnhandledStateOrCount { variable: String }, + #[error("Consumed variable {variable} in loop created outside the loop")] + ConsumedVariableInLoop { variable: String }, + #[error("Unspecified Linearity error. Variable {variable} generated {message}")] + Unspecified { variable: String, message: String }, + #[error("Variable {variable} not found")] + VariableNotFound { variable: String }, + #[error("Inconsistent state {message}")] + StateInconsistency { message: String }, + #[error("Not implemented: {message}")] + NotImplemented { message: String }, + #[error("Unhandled statement type {r#type}")] + UnhandledStatementType { r#type: String }, +} diff --git a/crates/concrete_driver/src/lib.rs b/crates/concrete_driver/src/lib.rs index 48284ff..76ac10e 100644 --- a/crates/concrete_driver/src/lib.rs +++ b/crates/concrete_driver/src/lib.rs @@ -100,6 +100,10 @@ pub struct BuildArgs { /// Also output the object file. #[arg(long, default_value_t = false)] object: bool, + + /// This option is for checking the program for linearity. + #[arg(long, default_value_t = false)] + check: bool, } #[derive(Parser, Debug)] @@ -150,6 +154,10 @@ pub struct CompilerArgs { /// Also output the object file. #[arg(long, default_value_t = false)] object: bool, + + /// This option is for checking the program for linearity. + #[arg(long, default_value_t = false)] + check: bool, } pub fn main() -> Result<()> { @@ -298,6 +306,7 @@ fn handle_build( asm, object, lib, + check, }: BuildArgs, ) -> Result { match path { @@ -325,6 +334,7 @@ fn handle_build( asm, object, mlir, + check, }; println!( @@ -453,6 +463,7 @@ fn handle_build( asm, object, mlir, + check, }; let object = compile(&compile_args)?; @@ -592,6 +603,19 @@ pub fn compile(args: &CompilerArgs) -> Result { } }; + #[allow(unused_variables)] + if args.check { + let linearity_result = + match concrete_check::linearity_check::linearity_check_program(&programs, &session) { + Ok(ir) => ir, + Err(error) => { + //TODO improve reporting + println!("Linearity check failed: {:#?}", error); + std::process::exit(1); + } + }; + } + if args.ir { std::fs::write( session.output_file.with_extension("ir"), diff --git a/crates/concrete_driver/tests/examples.rs b/crates/concrete_driver/tests/examples.rs index 14e52b4..d2c73f4 100644 --- a/crates/concrete_driver/tests/examples.rs +++ b/crates/concrete_driver/tests/examples.rs @@ -22,6 +22,9 @@ mod common; #[test_case(include_str!("../../../examples/for_while.con"), "for_while", false, 10 ; "for_while.con")] #[test_case(include_str!("../../../examples/arrays.con"), "arrays", false, 5 ; "arrays.con")] #[test_case(include_str!("../../../examples/constants.con"), "constants", false, 20 ; "constants.con")] +#[test_case(include_str!("../../../examples/linearExample01.con"), "linearity", false, 2 ; "linearExample01.con")] +#[test_case(include_str!("../../../examples/linearExample02.con"), "linearity", false, 2 ; "linearExample02.con")] +#[test_case(include_str!("../../../examples/linearExample03if.con"), "linearity", false, 0 ; "linearExample03if.con")] fn example_tests(source: &str, name: &str, is_library: bool, status_code: i32) { assert_eq!( status_code, diff --git a/examples/linearExample01.con b/examples/linearExample01.con new file mode 100644 index 0000000..cc26c82 --- /dev/null +++ b/examples/linearExample01.con @@ -0,0 +1,18 @@ +mod LinearExampleStub { + + struct Linear { + x: i32, + y: i32, + } + + fn main() -> i32 { + let mut xy: Linear = + Linear { + x: 1, + y: 0, + }; + // linear value is written/consumed + xy.x = xy.x + 1; + return xy.x; + } +} \ No newline at end of file diff --git a/examples/linearExample02.con b/examples/linearExample02.con new file mode 100644 index 0000000..8365611 --- /dev/null +++ b/examples/linearExample02.con @@ -0,0 +1,23 @@ +mod LinearExampleStub { + + struct Linear { + x: i32, + y: i32, + } + + fn main() -> i32 { + let mut xy: Linear = + Linear { + x: 1, + y: 0, + }; + // linear value is written/consumed + consume_x(&mut xy); + return xy.x; + } + + fn consume_x(value: & mut Linear) { + value.x = value.x + 1; + } + +} \ No newline at end of file diff --git a/examples/linearExample03if.con b/examples/linearExample03if.con new file mode 100644 index 0000000..57566f0 --- /dev/null +++ b/examples/linearExample03if.con @@ -0,0 +1,27 @@ +mod LinearExampleIfStub { + + struct Linear { + x: i32, + y: i32, + } + + fn main() -> i32 { + let mut xy: Linear = + Linear { + x: 1, + y: 0, + }; + if xy.x < xy.y{ + consume_x(&mut xy, 1); + } + else { + consume_x(&mut xy, 0-1); + } + return xy.x; + } + + fn consume_x(value: & mut Linear, i: i32) { + value.x = value.x + i; + } + +} \ No newline at end of file