diff --git a/Cargo.lock b/Cargo.lock index 26a44dbe1a7f..86134ce48123 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8,7 +8,7 @@ version = "0.21.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8a30b2e23b9e17a9f90641c7ab1549cd9b44f296d3ccbf309d2863cfe398a0cb" dependencies = [ - "gimli", + "gimli 0.28.0", ] [[package]] @@ -17,6 +17,17 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" +[[package]] +name = "ahash" +version = "0.7.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a824f2aa7e75a0c98c5a504fceb80649e9c35265d44525b5f94de4771a395cd" +dependencies = [ + "getrandom 0.2.10", + "once_cell", + "version_check", +] + [[package]] name = "ahash" version = "0.8.3" @@ -112,6 +123,21 @@ dependencies = [ "derive_arbitrary", ] +[[package]] +name = "arrayvec" +version = "0.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b" + +[[package]] +name = "ascii-canvas" +version = "3.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8824ecca2e851cec16968d54a01dd372ef8f95b244fb84b84e70128be347c3c6" +dependencies = [ + "term", +] + [[package]] name = "async-trait" version = "0.1.73" @@ -197,13 +223,34 @@ version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b4682ae6287fcf752ecaabbfcc7b6f9b72aa33933dc23a554d853aea8eea8635" +[[package]] +name = "block-buffer" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c0940dc441f31689269e10ac70eb1002a3a1d3ad1390e030043662eb7fe4688b" +dependencies = [ + "block-padding", + "byte-tools", + "byteorder", + "generic-array 0.12.4", +] + [[package]] name = "block-buffer" version = "0.10.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3078c7629b62d3f0439517fa394996acacc5cbc91c5a20d8c658e77abd503a71" dependencies = [ - "generic-array", + "generic-array 0.14.7", +] + +[[package]] +name = "block-padding" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fa79dedbb091f449f1f39e53edf88d5dbe95f895dae6135a8d7b881fb5af73f5" +dependencies = [ + "byte-tools", ] [[package]] @@ -227,6 +274,12 @@ checksum = "7f30e7476521f6f8af1a1c4c0b8cc94f0bee37d91763d0ca2665f299b6cd8aec" name = "byte-array-literals" version = "14.0.0" +[[package]] +name = "byte-tools" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e3b5ca7a04898ad4bcd41c90c5285445ff5b791899bb1b0abdd2a2aa791211d7" + [[package]] name = "byteorder" version = "1.4.3" @@ -296,7 +349,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "577de6cff7c2a47d6b13efe5dd28bf116bd7f8f7db164ea95b7cc2640711f522" dependencies = [ "ambient-authority", - "rand", + "rand 0.8.5", ] [[package]] @@ -318,7 +371,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7b9e3348a3510c4619b4c7a7bcdef09a71221da18f266bda3ed6b9aea2c509e2" dependencies = [ "cap-std", - "rand", + "rand 0.8.5", "rustix", "uuid", ] @@ -527,7 +580,7 @@ name = "command-tests" version = "0.0.0" dependencies = [ "anyhow", - "getrandom", + "getrandom 0.2.10", "wit-bindgen", ] @@ -630,13 +683,13 @@ dependencies = [ "cranelift-entity", "cranelift-isle", "criterion", - "gimli", + "gimli 0.28.0", "hashbrown 0.14.1", "log", "regalloc2", "serde", "serde_derive", - "sha2", + "sha2 0.10.8", "similar", "smallvec", "souper-ir", @@ -686,7 +739,7 @@ dependencies = [ "cranelift-wasm", "file-per-thread-logger", "filecheck", - "gimli", + "gimli 0.28.0", "log", "num_cpus", "serde", @@ -741,8 +794,11 @@ dependencies = [ name = "cranelift-isle" version = "0.101.0" dependencies = [ + "clap 4.4.6", "codespan-reporting", + "env_logger 0.10.0", "log", + "pretty", "tempfile", ] @@ -924,6 +980,30 @@ dependencies = [ "itertools", ] +[[package]] +name = "crossbeam" +version = "0.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2801af0d36612ae591caa9568261fddce32ce6e08a7275ea334a06a4ad021a2c" +dependencies = [ + "cfg-if", + "crossbeam-channel", + "crossbeam-deque", + "crossbeam-epoch", + "crossbeam-queue", + "crossbeam-utils", +] + +[[package]] +name = "crossbeam-channel" +version = "0.5.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a33c2bf77f2df06183c3aa30d1e96c0695a313d4f9c453cc3762a6db39f99200" +dependencies = [ + "cfg-if", + "crossbeam-utils", +] + [[package]] name = "crossbeam-deque" version = "0.8.3" @@ -948,6 +1028,16 @@ dependencies = [ "scopeguard", ] +[[package]] +name = "crossbeam-queue" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d1cfb3ea8a53f37c40dea2c7bedcbd88bdfae54f5e2175d6ecaff1c988353add" +dependencies = [ + "cfg-if", + "crossbeam-utils", +] + [[package]] name = "crossbeam-utils" version = "0.8.16" @@ -957,13 +1047,19 @@ dependencies = [ "cfg-if", ] +[[package]] +name = "crunchy" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7a81dae078cea95a014a339291cec439d2f232ebe854a9d672b796c6afafa9b7" + [[package]] name = "crypto-common" version = "0.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1bfb12502f3fc46cca1bb51ac28df9d618d813cdc3d2f25b9fe775a34af26bb3" dependencies = [ - "generic-array", + "generic-array 0.14.7", "typenum", ] @@ -993,13 +1089,28 @@ dependencies = [ "syn 2.0.37", ] +[[package]] +name = "diff" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "56254986775e3233ffa9c4d7d3faaf6d36a2c09d30b20687e9f88bc8bafc16c8" + +[[package]] +name = "digest" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3d0c8c8752312f9713efd397ff63acb9f85585afbf179282e720e7704954dd5" +dependencies = [ + "generic-array 0.12.4", +] + [[package]] name = "digest" version = "0.10.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" dependencies = [ - "block-buffer", + "block-buffer 0.10.4", "crypto-common", ] @@ -1022,6 +1133,16 @@ dependencies = [ "dirs-sys", ] +[[package]] +name = "dirs-next" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b98cf8ebf19c3d1b223e151f99a4f9f0690dca41414773390fc824184ac833e1" +dependencies = [ + "cfg-if", + "dirs-sys-next", +] + [[package]] name = "dirs-sys" version = "0.3.7" @@ -1079,6 +1200,15 @@ version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07" +[[package]] +name = "ena" +version = "0.14.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c533630cf40e9caa44bd91aadc88a75d75a4c3a12b4cfde353cbed41daa1e1f1" +dependencies = [ + "log", +] + [[package]] name = "encode_unicode" version = "0.3.6" @@ -1159,6 +1289,18 @@ version = "0.0.0" name = "example-wasi-wasm" version = "0.0.0" +[[package]] +name = "fake-simd" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e88a8acf291dafb59c2d96e8f59828f3838bb1a70398823ade51a84de6a6deed" + +[[package]] +name = "fallible-iterator" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4443176a9f2c162692bd3d352d745ef9413eec5782a80d8fd6f8a1ac692a07f7" + [[package]] name = "fallible-iterator" version = "0.3.0" @@ -1214,6 +1356,18 @@ dependencies = [ "windows-sys 0.48.0", ] +[[package]] +name = "fixedbitset" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "37ab347416e802de484e4d03c7316c48f1ecb56574dfd4a46a80f173ce1de04d" + +[[package]] +name = "fixedbitset" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" + [[package]] name = "flagset" version = "0.4.4" @@ -1339,6 +1493,15 @@ dependencies = [ "serde_json", ] +[[package]] +name = "generic-array" +version = "0.12.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ffdf9f34f1447443d37393cc6c2b8313aebddcd96906caf34e54c68d8e57d7bd" +dependencies = [ + "typenum", +] + [[package]] name = "generic-array" version = "0.14.7" @@ -1349,6 +1512,26 @@ dependencies = [ "version_check", ] +[[package]] +name = "getopts" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5" +dependencies = [ + "unicode-width", +] + +[[package]] +name = "getrandom" +version = "0.1.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fc3cb4d91f53b50155bdcfd23f6a4c39ae1969c2ae85982b135750cccaf5fce" +dependencies = [ + "cfg-if", + "libc", + "wasi 0.9.0+wasi-snapshot-preview1", +] + [[package]] name = "getrandom" version = "0.2.10" @@ -1357,7 +1540,18 @@ checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427" dependencies = [ "cfg-if", "libc", - "wasi", + "wasi 0.11.0+wasi-snapshot-preview1", +] + +[[package]] +name = "gimli" +version = "0.26.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "22030e2c5a68ec659fde1e949a745124b48e6fa8b045b7ed5bd1fe4ccc5c4e5d" +dependencies = [ + "fallible-iterator 0.2.0", + "indexmap 1.9.3", + "stable_deref_trait", ] [[package]] @@ -1366,7 +1560,7 @@ version = "0.28.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6fb8d784f27acf97159b40fc4db5ecd8aa23b9ad5ef69cdd136d3bc80665f0c0" dependencies = [ - "fallible-iterator", + "fallible-iterator 0.3.0", "indexmap 2.0.2", "stable_deref_trait", ] @@ -1377,6 +1571,17 @@ version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" +[[package]] +name = "goblin" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32401e89c6446dcd28185931a01b1093726d0356820ac744023e6850689bf926" +dependencies = [ + "log", + "plain", + "scroll", +] + [[package]] name = "h2" version = "0.3.21" @@ -1414,7 +1619,7 @@ version = "0.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "43a3c133739dddd0d2990f9a4bdf8eb4b21ef50e4851ca85ab661199821d510e" dependencies = [ - "ahash", + "ahash 0.8.3", ] [[package]] @@ -1423,7 +1628,7 @@ version = "0.14.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dfda62a12f55daeae5015f81b0baea145391cb4520f86c248fc615d72640d12" dependencies = [ - "ahash", + "ahash 0.8.3", ] [[package]] @@ -1639,6 +1844,113 @@ dependencies = [ "windows-sys 0.48.0", ] +[[package]] +name = "isla" +version = "0.2.0" +source = "git+https://github.com/rems-project/isla.git?rev=2a4bd429b56634db52d59707b83090a535b5c4bc#2a4bd429b56634db52d59707b83090a535b5c4bc" +dependencies = [ + "bincode", + "crossbeam", + "getopts", + "id-arena", + "isla-axiomatic", + "isla-cat", + "isla-elf", + "isla-lib", + "isla-mml", + "rand 0.7.3", + "serde", + "sha2 0.8.2", + "toml", +] + +[[package]] +name = "isla-axiomatic" +version = "0.2.0" +source = "git+https://github.com/rems-project/isla.git?rev=2a4bd429b56634db52d59707b83090a535b5c4bc#2a4bd429b56634db52d59707b83090a535b5c4bc" +dependencies = [ + "crossbeam", + "goblin", + "isla-cat", + "isla-lib", + "isla-mml", + "isla-sexp", + "lalrpop", + "lalrpop-util", + "lazy_static", + "regex", + "serde", + "toml", +] + +[[package]] +name = "isla-cat" +version = "0.2.0" +source = "git+https://github.com/rems-project/isla.git?rev=2a4bd429b56634db52d59707b83090a535b5c4bc#2a4bd429b56634db52d59707b83090a535b5c4bc" +dependencies = [ + "lalrpop", + "lalrpop-util", + "lazy_static", + "regex", +] + +[[package]] +name = "isla-elf" +version = "0.2.0" +source = "git+https://github.com/rems-project/isla.git?rev=2a4bd429b56634db52d59707b83090a535b5c4bc#2a4bd429b56634db52d59707b83090a535b5c4bc" +dependencies = [ + "gimli 0.26.2", + "goblin", + "isla-lib", + "lazy_static", +] + +[[package]] +name = "isla-lib" +version = "0.2.0" +source = "git+https://github.com/rems-project/isla.git?rev=2a4bd429b56634db52d59707b83090a535b5c4bc#2a4bd429b56634db52d59707b83090a535b5c4bc" +dependencies = [ + "ahash 0.7.7", + "bincode", + "crossbeam", + "lalrpop", + "lalrpop-util", + "lazy_static", + "lexgen", + "lexgen_util", + "libc", + "petgraph 0.5.1", + "regex", + "serde", + "sha2 0.8.2", + "toml", + "z3-sys", +] + +[[package]] +name = "isla-mml" +version = "0.2.0" +source = "git+https://github.com/rems-project/isla.git?rev=2a4bd429b56634db52d59707b83090a535b5c4bc#2a4bd429b56634db52d59707b83090a535b5c4bc" +dependencies = [ + "id-arena", + "isla-lib", + "lalrpop", + "lalrpop-util", + "lazy_static", + "regex", +] + +[[package]] +name = "isla-sexp" +version = "0.2.0" +source = "git+https://github.com/rems-project/isla.git?rev=2a4bd429b56634db52d59707b83090a535b5c4bc#2a4bd429b56634db52d59707b83090a535b5c4bc" +dependencies = [ + "isla-mml", + "proc-macro2", + "quote", + "syn 1.0.109", +] + [[package]] name = "isle-fuzz" version = "0.0.0" @@ -1711,6 +2023,37 @@ dependencies = [ "wasm-bindgen", ] +[[package]] +name = "lalrpop" +version = "0.19.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0a1cbf952127589f2851ab2046af368fd20645491bb4b376f04b7f94d7a9837b" +dependencies = [ + "ascii-canvas", + "bit-set", + "diff", + "ena", + "is-terminal", + "itertools", + "lalrpop-util", + "petgraph 0.6.4", + "regex", + "regex-syntax 0.6.29", + "string_cache", + "term", + "tiny-keccak", + "unicode-xid", +] + +[[package]] +name = "lalrpop-util" +version = "0.19.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3c48237b9604c5a4702de6b824e02006c3214327564636aef27c1028a8fa0ed" +dependencies = [ + "regex", +] + [[package]] name = "lazy_static" version = "1.4.0" @@ -1723,6 +2066,27 @@ version = "0.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "884e2677b40cc8c339eaefcb701c32ef1fd2493d71118dc0ca4b6a736c93bd67" +[[package]] +name = "lexgen" +version = "0.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "05c12789f263e189cfcffff7adaee754498e359c5fefe337f716a8122c5c55a4" +dependencies = [ + "fxhash", + "proc-macro2", + "quote", + "syn 1.0.109", +] + +[[package]] +name = "lexgen_util" +version = "0.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4e726a67f1b0f16040843b1f12868e2e1ee6c3086a18b7502cb5046fb18da8f0" +dependencies = [ + "unicode-width", +] + [[package]] name = "libc" version = "0.2.148" @@ -1773,6 +2137,16 @@ dependencies = [ "winapi", ] +[[package]] +name = "lock_api" +version = "0.4.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45" +dependencies = [ + "autocfg", + "scopeguard", +] + [[package]] name = "log" version = "0.4.20" @@ -1852,10 +2226,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "927a765cd3fc26206e66b296465fa9d3e5ab003e651c1b3c060e7956d96b19d2" dependencies = [ "libc", - "wasi", + "wasi 0.11.0+wasi-snapshot-preview1", "windows-sys 0.48.0", ] +[[package]] +name = "new_debug_unreachable" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e4a24736216ec316047a1fc4252e27dabb04218aa4a3f37c6e7ddbf1f9782b54" + [[package]] name = "num-traits" version = "0.2.16" @@ -1935,6 +2315,12 @@ version = "11.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0ab1bc2a289d34bd04a330323ac98a1b4bc82c9d9fcb1e66b63caa84da26b575" +[[package]] +name = "opaque-debug" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2839e79665f131bdb5782e51f2c6c9599c133c6098982a54c794358bf432529c" + [[package]] name = "openvino" version = "0.5.0" @@ -1974,6 +2360,29 @@ version = "6.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4d5d9eb14b174ee9aa2ef96dc2b94637a2d4b6e7cb873c7e171f0c20c6cf3eac" +[[package]] +name = "parking_lot" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f" +dependencies = [ + "lock_api", + "parking_lot_core", +] + +[[package]] +name = "parking_lot_core" +version = "0.9.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4c42a9226546d68acdd9c0a280d17ce19bfe27a46bf68784e4066115788d008e" +dependencies = [ + "cfg-if", + "libc", + "redox_syscall 0.4.1", + "smallvec", + "windows-targets 0.48.5", +] + [[package]] name = "paste" version = "1.0.14" @@ -1986,6 +2395,35 @@ version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b2a4787296e9989611394c33f193f676704af1686e70b8f8033ab5ba9a35a94" +[[package]] +name = "petgraph" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "467d164a6de56270bd7c4d070df81d07beace25012d5103ced4e9ff08d6afdb7" +dependencies = [ + "fixedbitset 0.2.0", + "indexmap 1.9.3", +] + +[[package]] +name = "petgraph" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e1d3afd2628e69da2be385eb6f2fd57c8ac7977ceeff6dc166ff1657b0e386a9" +dependencies = [ + "fixedbitset 0.4.2", + "indexmap 2.0.2", +] + +[[package]] +name = "phf_shared" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6796ad771acdc0123d2a88dc428b5e38ef24456743ddb1744ed628f9815c096" +dependencies = [ + "siphasher", +] + [[package]] name = "pin-project-lite" version = "0.2.13" @@ -2004,6 +2442,12 @@ version = "0.3.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "26072860ba924cbfa98ea39c8c19b4dd6a4a25423dbdf219c1eca91aa0cf6964" +[[package]] +name = "plain" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6" + [[package]] name = "plotters" version = "0.3.5" @@ -2038,6 +2482,23 @@ version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" +[[package]] +name = "precomputed-hash" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "925383efa346730478fb4838dbe9137d2a47675ad789c546d150a6e1dd4ab31c" + +[[package]] +name = "pretty" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b55c4d17d994b637e2f4daf6e5dc5d660d209d5642377d675d7a1c3ab69fa579" +dependencies = [ + "arrayvec", + "typed-arena", + "unicode-width", +] + [[package]] name = "pretty_env_logger" version = "0.4.0" @@ -2102,8 +2563,8 @@ dependencies = [ "bitflags 2.4.0", "lazy_static", "num-traits", - "rand", - "rand_chacha", + "rand 0.8.5", + "rand_chacha 0.3.1", "rand_xorshift", "regex-syntax 0.7.5", "rusty-fork", @@ -2146,6 +2607,19 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "rand" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6a6b1679d49b24bbfe0c803429aa1874472f50d9b363131f0e89fc356b544d03" +dependencies = [ + "getrandom 0.1.16", + "libc", + "rand_chacha 0.2.2", + "rand_core 0.5.1", + "rand_hc", +] + [[package]] name = "rand" version = "0.8.5" @@ -2153,8 +2627,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" dependencies = [ "libc", - "rand_chacha", - "rand_core", + "rand_chacha 0.3.1", + "rand_core 0.6.4", +] + +[[package]] +name = "rand_chacha" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f4c8ed856279c9737206bf725bf36935d8666ead7aa69b52be55af369d193402" +dependencies = [ + "ppv-lite86", + "rand_core 0.5.1", ] [[package]] @@ -2164,7 +2648,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" dependencies = [ "ppv-lite86", - "rand_core", + "rand_core 0.6.4", +] + +[[package]] +name = "rand_core" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "90bde5296fc891b0cef12a6d03ddccc162ce7b2aff54160af9338f8d40df6d19" +dependencies = [ + "getrandom 0.1.16", ] [[package]] @@ -2173,7 +2666,16 @@ version = "0.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" dependencies = [ - "getrandom", + "getrandom 0.2.10", +] + +[[package]] +name = "rand_hc" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ca3129af7b92a17112d59ad498c6f81eaf463253766b90396d39ea7a39d6613c" +dependencies = [ + "rand_core 0.5.1", ] [[package]] @@ -2182,7 +2684,7 @@ version = "0.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d25bf25ec5ae4a3f1b92f929810509a2f53d7dca2f50b794ff57e3face536c8f" dependencies = [ - "rand_core", + "rand_core 0.6.4", ] [[package]] @@ -2230,13 +2732,22 @@ dependencies = [ "bitflags 1.3.2", ] +[[package]] +name = "redox_syscall" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa" +dependencies = [ + "bitflags 1.3.2", +] + [[package]] name = "redox_users" version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b033d837a7cf162d7993aded9304e30a83213c648b6e389db233191f891e5c2b" dependencies = [ - "getrandom", + "getrandom 0.2.10", "redox_syscall 0.2.16", "thiserror", ] @@ -2317,7 +2828,7 @@ version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9166d72162de3575f950507683fac47e30f6f2c3836b71b7fbc61aa517c9c5f4" dependencies = [ - "rand", + "rand 0.8.5", ] [[package]] @@ -2423,6 +2934,26 @@ version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" +[[package]] +name = "scroll" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fda28d4b4830b807a8b43f7b0e6b5df875311b3e7621d84577188c175b6ec1ec" +dependencies = [ + "scroll_derive", +] + +[[package]] +name = "scroll_derive" +version = "0.10.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aaaae8f38bb311444cfb7f1979af0bc9240d95795f75f9ceddf6a59b79ceffa0" +dependencies = [ + "proc-macro2", + "quote", + "syn 1.0.109", +] + [[package]] name = "sct" version = "0.7.0" @@ -2473,6 +3004,18 @@ dependencies = [ "serde", ] +[[package]] +name = "sha2" +version = "0.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a256f46ea78a0c0d9ff00077504903ac881a1dafdc20da66545699e7776b3e69" +dependencies = [ + "block-buffer 0.7.3", + "digest 0.8.1", + "fake-simd", + "opaque-debug", +] + [[package]] name = "sha2" version = "0.10.8" @@ -2481,7 +3024,7 @@ checksum = "793db75ad2bcafc3ffa7c68b215fee268f537982cd901d132f89c6343f3a3dc8" dependencies = [ "cfg-if", "cpufeatures", - "digest", + "digest 0.10.7", ] [[package]] @@ -2510,7 +3053,7 @@ checksum = "4ee9977fa98489d9006f4ab26fc5cbe2a139985baed09d2ec08dee6e506fc496" dependencies = [ "cfg-if", "libc", - "rand", + "rand 0.8.5", "winapi", ] @@ -2529,6 +3072,12 @@ version = "2.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "420acb44afdae038210c99e69aae24109f32f15500aa708e81d46c9f29d55fcf" +[[package]] +name = "siphasher" +version = "0.3.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "38b58827f4464d87d377d175e90bf58eb00fd8716ff0a62f80356b5e61555d0d" + [[package]] name = "slab" version = "0.4.9" @@ -2611,6 +3160,19 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" +[[package]] +name = "string_cache" +version = "0.8.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f91138e76242f575eb1d3b38b4f1362f10d3a43f47d182a5b359af488a02293b" +dependencies = [ + "new_debug_unreachable", + "once_cell", + "parking_lot", + "phf_shared", + "precomputed-hash", +] + [[package]] name = "strsim" version = "0.10.0" @@ -2699,6 +3261,17 @@ dependencies = [ "windows-sys 0.48.0", ] +[[package]] +name = "term" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c59df8ac95d96ff9bede18eb7300b0fda5e5d8d90960e76f8e14ae765eedbf1f" +dependencies = [ + "dirs-next", + "rustversion", + "winapi", +] + [[package]] name = "termcolor" version = "1.3.0" @@ -2784,6 +3357,15 @@ dependencies = [ "once_cell", ] +[[package]] +name = "tiny-keccak" +version = "2.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2c9d3793400a45f954c52e73d068316d76b6f4e36977e3fcebb13a2721e80237" +dependencies = [ + "crunchy", +] + [[package]] name = "tinytemplate" version = "1.2.1" @@ -2925,6 +3507,12 @@ version = "0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3528ecfd12c466c6f163363caf2d02a71161dd5e1cc6ae7b34207ea2d42d81ed" +[[package]] +name = "typed-arena" +version = "2.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" + [[package]] name = "typenum" version = "1.17.0" @@ -3014,7 +3602,7 @@ version = "1.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "79daa5ed5740825c40b389c5e50312b9c86df53fccd33f281df655642b43869d" dependencies = [ - "getrandom", + "getrandom 0.2.10", ] [[package]] @@ -3033,15 +3621,21 @@ dependencies = [ name = "veri_engine" version = "0.1.0" dependencies = [ + "anyhow", "clap 3.2.25", "cranelift-codegen", "cranelift-codegen-meta", "cranelift-isle", + "cranelift-reader", + "crossbeam", "easy-smt", "env_logger 0.10.0", + "isla", + "isla-lib", "itertools", "log", "retry", + "sha2 0.8.2", "strum", "strum_macros", "veri_ir", @@ -3094,6 +3688,12 @@ dependencies = [ "try-lock", ] +[[package]] +name = "wasi" +version = "0.9.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cccddf32554fecc6acb585f82a32a72e28b48f8c4c1883ddfeeeaa96f7d8e519" + [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" @@ -3161,7 +3761,7 @@ version = "14.0.0" dependencies = [ "byte-array-literals", "object", - "wasi", + "wasi 0.11.0+wasi-snapshot-preview1", "wasm-encoder", "wit-bindgen", ] @@ -3180,7 +3780,7 @@ version = "0.0.0" dependencies = [ "libc", "once_cell", - "wasi", + "wasi 0.11.0+wasi-snapshot-preview1", "wit-bindgen", ] @@ -3287,7 +3887,7 @@ checksum = "ee038ee28c816dfeabb992ba765d801f721a6d1b097cba0f941c184454616d92" dependencies = [ "egg", "log", - "rand", + "rand 0.8.5", "thiserror", "wasm-encoder", "wasmparser", @@ -3479,7 +4079,7 @@ dependencies = [ "rustix", "serde", "serde_derive", - "sha2", + "sha2 0.10.8", "tempfile", "toml", "windows-sys 0.48.0", @@ -3583,7 +4183,7 @@ dependencies = [ "cranelift-frontend", "cranelift-native", "cranelift-wasm", - "gimli", + "gimli 0.28.0", "log", "object", "target-lexicon", @@ -3602,7 +4202,7 @@ dependencies = [ "cranelift-codegen", "cranelift-control", "cranelift-native", - "gimli", + "gimli 0.28.0", "object", "target-lexicon", "wasmtime-environ", @@ -3616,7 +4216,7 @@ dependencies = [ "clap 4.4.6", "cranelift-entity", "env_logger 0.10.0", - "gimli", + "gimli 0.28.0", "indexmap 2.0.2", "log", "object", @@ -3693,7 +4293,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "rand", + "rand 0.8.5", "smallvec", "target-lexicon", "wasmparser", @@ -3711,7 +4311,7 @@ dependencies = [ "component-test-util", "env_logger 0.10.0", "log", - "rand", + "rand 0.8.5", "rayon", "target-lexicon", "tempfile", @@ -3737,7 +4337,7 @@ dependencies = [ "bincode", "cfg-if", "cpp_demangle", - "gimli", + "gimli 0.28.0", "ittapi", "log", "object", @@ -3789,7 +4389,7 @@ dependencies = [ "once_cell", "paste", "proptest", - "rand", + "rand 0.8.5", "rustix", "sptr", "wasm-encoder", @@ -3898,7 +4498,7 @@ version = "14.0.0" dependencies = [ "anyhow", "log", - "rand", + "rand 0.8.5", "wasi-common", "wasmtime", "wasmtime-wasi", @@ -3920,7 +4520,7 @@ version = "14.0.0" dependencies = [ "anyhow", "cranelift-codegen", - "gimli", + "gimli 0.28.0", "object", "target-lexicon", "wasmparser", @@ -4104,7 +4704,7 @@ version = "0.12.0" dependencies = [ "anyhow", "cranelift-codegen", - "gimli", + "gimli 0.28.0", "regalloc2", "smallvec", "target-lexicon", @@ -4410,6 +5010,12 @@ dependencies = [ "wast 35.0.2", ] +[[package]] +name = "z3-sys" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae57b4c31eabc2620fbf2ea3e4deac2cd8a12522ccc0ebcc29e60dff8137de31" + [[package]] name = "zstd" version = "0.11.2+zstd.1.5.2" diff --git a/cranelift/codegen/build.rs b/cranelift/codegen/build.rs index 3ebb1c18c96e..21f10fd9abf0 100644 --- a/cranelift/codegen/build.rs +++ b/cranelift/codegen/build.rs @@ -187,7 +187,8 @@ fn get_isle_compilations( make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("prelude_opt.isle")); let prelude_lower_isle = make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("prelude_lower.isle")); - let inst_specs = make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("inst_specs.isle")); + let inst_specs = + make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("inst_specs.isle")); // Directory for mid-end optimizations. let src_opts = make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("opts")); @@ -253,6 +254,7 @@ fn get_isle_compilations( prelude_lower_isle.clone(), src_isa_aarch64.join("inst.isle"), src_isa_aarch64.join("inst_neon.isle"), + src_isa_aarch64.join("inst_specs.isle"), inst_specs.clone(), src_isa_aarch64.join("lower.isle"), src_isa_aarch64.join("lower_dynamic_neon.isle"), diff --git a/cranelift/codegen/src/isa/aarch64/inst.isle b/cranelift/codegen/src/isa/aarch64/inst.isle index fb497367f79b..8d376e386141 100644 --- a/cranelift/codegen/src/isa/aarch64/inst.isle +++ b/cranelift/codegen/src/isa/aarch64/inst.isle @@ -2018,23 +2018,32 @@ (spec (alu_rrr op t a b) (provide (= result (switch op + ((ALUOp.Add) + (if (<= t 32) + (zero_ext 64 (bvadd (extract 31 0 a) (extract 31 0 b))) + (bvadd a b))) ((ALUOp.Lsr) (if (<= t 32) - (conv_to 64 (bvlshr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b)))) + (zero_ext 64 (bvlshr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b)))) (bvlshr a (bvand (bvsub (int2bv 64 64) #x0000000000000001) b)))) ((ALUOp.Asr) (if (<= t 32) - (conv_to 64 (bvashr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b)))) + (zero_ext 64 (bvashr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b)))) (bvashr a (bvand (bvsub (int2bv 64 64) #x0000000000000001) b)))) ((ALUOp.Lsl) (if (<= t 32) - (conv_to 64 (bvshl (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b)))) + (zero_ext 64 (bvshl (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b)))) (bvshl a (bvand (bvsub (int2bv 64 64) #x0000000000000001) b))))))) (require - (or (= op (ALUOp.Lsr)) (= op (ALUOp.Asr)) (= op (ALUOp.Lsl))) - (or (= t 8) (= t 16) (= t 32) (= t 64)))) + (or (= op (ALUOp.Add)) (= op (ALUOp.Lsr)) (= op (ALUOp.Asr)) (= op (ALUOp.Lsl))) + (or (= t 8) (= t 16) (= t 32) (= t 64))) + ;(or (= t 32) (= t 64))) + ) (decl alu_rrr (ALUOp Type Reg Reg) Reg) -(rule (alu_rrr op ty src1 src2) +(instantiate alu_rrr + ((args (bv 8) Int (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64))) +) +(rule alu_rrr_emit (alu_rrr op ty src1 src2) (let ((dst WritableReg (temp_writable_reg $I64)) (_ Unit (emit (MInst.AluRRR op (operand_size ty) dst src1 src2)))) dst)) @@ -2633,10 +2642,14 @@ (provide (= result (if (<= ty 32) - (conv_to 64 (bvadd (extract 31 0 a) (extract 31 0 b))) - (bvadd a b))))) + (zero_ext 64 (bvadd (extract 31 0 a) (extract 31 0 b))) + (bvadd a b)))) + (require (or (= ty 8) (= ty 16) (= ty 32) (= ty 64)))) (decl add (Type Reg Reg) Reg) -(rule (add ty x y) (alu_rrr (ALUOp.Add) ty x y)) +(instantiate add + ((args Int (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64))) +) +(rule add_alu_rrr (add ty x y) (alu_rrr (ALUOp.Add) ty x y)) (spec (add_imm ty a b) (provide diff --git a/cranelift/codegen/src/isa/aarch64/inst/mod.rs b/cranelift/codegen/src/isa/aarch64/inst/mod.rs index e916d9e72359..811ce71693d7 100644 --- a/cranelift/codegen/src/isa/aarch64/inst/mod.rs +++ b/cranelift/codegen/src/isa/aarch64/inst/mod.rs @@ -15,14 +15,14 @@ use smallvec::{smallvec, SmallVec}; use std::fmt::Write; use std::string::{String, ToString}; -pub(crate) mod regs; -pub(crate) use self::regs::*; +pub mod regs; +pub use self::regs::*; pub mod imms; pub use self::imms::*; pub mod args; pub use self::args::*; pub mod emit; -pub(crate) use self::emit::*; +pub use self::emit::*; use crate::isa::aarch64::abi::AArch64MachineDeps; pub(crate) mod unwind; @@ -1191,7 +1191,11 @@ fn mem_finalize_for_show(mem: &AMode, state: &EmitState) -> (String, AMode) { } impl Inst { - fn print_with_state(&self, state: &mut EmitState, allocs: &mut AllocationConsumer) -> String { + pub fn print_with_state( + &self, + state: &mut EmitState, + allocs: &mut AllocationConsumer, + ) -> String { let mut empty_allocs = AllocationConsumer::default(); fn op_name(alu_op: ALUOp) -> &'static str { diff --git a/cranelift/codegen/src/isa/aarch64/inst_specs.isle b/cranelift/codegen/src/isa/aarch64/inst_specs.isle new file mode 100644 index 000000000000..6cb44fa423d8 --- /dev/null +++ b/cranelift/codegen/src/isa/aarch64/inst_specs.isle @@ -0,0 +1,450 @@ +(spec + (MInst.AluRRR alu_op size rd rn rm) + (provide + (= result #b1) + (=> + (and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size32))) + (and + (= rn v0_536) + (= rm v0_538) + (= + v0_581 + (zero_ext + 64 + (bvadd + (extract 31 0 (zero_ext 128 (extract 31 0 v0_536))) + (extract 31 0 (zero_ext 128 (extract 31 0 v0_538)))))) + (= rd v0_581))) + (=> + (and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size64))) + (and + (= rn v1_536) + (= rm v1_538) + (= + v1_581 + (bvadd + (extract 63 0 (zero_ext 128 (extract 63 0 v1_536))) + (extract 63 0 (zero_ext 128 (extract 63 0 v1_538))))) + (= rd v1_581))) + (=> + (and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size32))) + (and + (= rn v2_536) + (= rm v2_538) + (= + v2_584 + (zero_ext + 64 + (bvadd + (extract + 31 + 0 + (bvadd + (zero_ext 128 (extract 31 0 v2_536)) + (zero_ext 128 (bvnot (extract 31 0 v2_538))))) + #x00000001))) + (= rd v2_584))) + (=> + (and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size64))) + (and + (= rn v3_536) + (= rm v3_538) + (= + v3_584 + (bvadd + (extract + 63 + 0 + (bvadd + (zero_ext 128 (extract 63 0 v3_536)) + (zero_ext 128 (bvnot (extract 63 0 v3_538))))) + #x0000000000000001)) + (= rd v3_584))) + (=> + (and (= alu_op (ALUOp.Orr)) (= size (OperandSize.Size32))) + (and + (= rn v4_544) + (= rm v4_546) + (= v4_550 (zero_ext 64 (bvor (extract 31 0 v4_544) (extract 31 0 v4_546)))) + (= rd v4_550))) + (=> + (and (= alu_op (ALUOp.Orr)) (= size (OperandSize.Size64))) + (and + (= rn v5_544) + (= rm v5_546) + (= v5_550 (bvor (extract 63 0 v5_544) (extract 63 0 v5_546))) + (= rd v5_550))) + (=> + (and (= alu_op (ALUOp.OrrNot)) (= size (OperandSize.Size32))) + (and + (= rn v6_544) + (= rm v6_546) + (= v6_551 (zero_ext 64 (bvor (extract 31 0 v6_544) (bvnot (extract 31 0 v6_546))))) + (= rd v6_551))) + (=> + (and (= alu_op (ALUOp.OrrNot)) (= size (OperandSize.Size64))) + (and + (= rn v7_544) + (= rm v7_546) + (= v7_551 (bvor (extract 63 0 v7_544) (bvnot (extract 63 0 v7_546)))) + (= rd v7_551))) + (=> + (and (= alu_op (ALUOp.And)) (= size (OperandSize.Size32))) + (and + (= rn v8_544) + (= rm v8_546) + (= v8_550 (zero_ext 64 (bvand (extract 31 0 v8_544) (extract 31 0 v8_546)))) + (= rd v8_550))) + (=> + (and (= alu_op (ALUOp.And)) (= size (OperandSize.Size64))) + (and + (= rn v9_544) + (= rm v9_546) + (= v9_550 (bvand (extract 63 0 v9_544) (extract 63 0 v9_546))) + (= rd v9_550))) + (=> + (and (= alu_op (ALUOp.AndNot)) (= size (OperandSize.Size32))) + (and + (= rn v10_544) + (= rm v10_546) + (= + v10_551 + (zero_ext 64 (bvand (extract 31 0 v10_544) (bvnot (extract 31 0 v10_546))))) + (= rd v10_551))) + (=> + (and (= alu_op (ALUOp.AndNot)) (= size (OperandSize.Size64))) + (and + (= rn v11_544) + (= rm v11_546) + (= v11_551 (bvand (extract 63 0 v11_544) (bvnot (extract 63 0 v11_546)))) + (= rd v11_551))) + (=> + (and (= alu_op (ALUOp.Eor)) (= size (OperandSize.Size32))) + (and + (= rn v12_544) + (= rm v12_546) + (= v12_550 (zero_ext 64 (bvxor (extract 31 0 v12_544) (extract 31 0 v12_546)))) + (= rd v12_550))) + (=> + (and (= alu_op (ALUOp.Eor)) (= size (OperandSize.Size64))) + (and + (= rn v13_544) + (= rm v13_546) + (= v13_550 (bvxor (extract 63 0 v13_544) (extract 63 0 v13_546))) + (= rd v13_550))) + (=> + (and (= alu_op (ALUOp.EorNot)) (= size (OperandSize.Size32))) + (and + (= rn v14_544) + (= rm v14_546) + (= + v14_551 + (zero_ext 64 (bvxor (extract 31 0 v14_544) (bvnot (extract 31 0 v14_546))))) + (= rd v14_551))) + (=> + (and (= alu_op (ALUOp.EorNot)) (= size (OperandSize.Size64))) + (and + (= rn v15_544) + (= rm v15_546) + (= v15_551 (bvxor (extract 63 0 v15_544) (bvnot (extract 63 0 v15_546)))) + (= rd v15_551))) + (=> + (and (= alu_op (ALUOp.Lsr)) (= size (OperandSize.Size32))) + (and + (= rm v16_535) + (= v16_537 (zero_ext 128 (extract 31 0 v16_535))) + (= rn v16_541) + (= + v16_544 + (zero_ext + 64 + (bvlshr + (extract 31 0 v16_541) + (extract + 31 + 0 + (sign_ext + 128 + (extract + 63 + 0 + (if + (bvslt + (bvsrem + v16_537 + (concat #x0000000000000000 #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000000)) + (if + (bvslt + (concat #x0000000000000000 #x0000000000000020) + (concat #x0000000000000000 #x0000000000000000)) + (bvsub + (bvsrem + v16_537 + (concat + #x0000000000000000 + #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000020)) + (bvadd + (bvsrem + v16_537 + (concat + #x0000000000000000 + #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000020))) + (bvsrem + v16_537 + (concat + #x0000000000000000 + #x0000000000000020))))))))) + (= rd v16_544))) + (=> + (and (= alu_op (ALUOp.Lsr)) (= size (OperandSize.Size64))) + (and + (= rm v17_535) + (= v17_537 (zero_ext 128 (extract 63 0 v17_535))) + (= rn v17_541) + (= + v17_544 + (bvlshr + (extract 63 0 v17_541) + (extract + 63 + 0 + (sign_ext + 128 + (extract + 63 + 0 + (if + (bvslt + (bvsrem + v17_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000000)) + (if + (bvslt + (concat #x0000000000000000 #x0000000000000040) + (concat #x0000000000000000 #x0000000000000000)) + (bvsub + (bvsrem + v17_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000040)) + (bvadd + (bvsrem + v17_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000040))) + (bvsrem + v17_537 + (concat #x0000000000000000 #x0000000000000040)))))))) + (= rd v17_544))) + (=> + (and (= alu_op (ALUOp.Asr)) (= size (OperandSize.Size32))) + (and + (= rm v18_535) + (= v18_537 (zero_ext 128 (extract 31 0 v18_535))) + (= rn v18_541) + (= + v18_544 + (zero_ext + 64 + (bvashr + (extract 31 0 v18_541) + (extract + 31 + 0 + (sign_ext + 128 + (extract + 63 + 0 + (if + (bvslt + (bvsrem + v18_537 + (concat #x0000000000000000 #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000000)) + (if + (bvslt + (concat #x0000000000000000 #x0000000000000020) + (concat #x0000000000000000 #x0000000000000000)) + (bvsub + (bvsrem + v18_537 + (concat + #x0000000000000000 + #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000020)) + (bvadd + (bvsrem + v18_537 + (concat + #x0000000000000000 + #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000020))) + (bvsrem + v18_537 + (concat + #x0000000000000000 + #x0000000000000020))))))))) + (= rd v18_544))) + (=> + (and (= alu_op (ALUOp.Asr)) (= size (OperandSize.Size64))) + (and + (= rm v19_535) + (= v19_537 (zero_ext 128 (extract 63 0 v19_535))) + (= rn v19_541) + (= + v19_544 + (bvashr + (extract 63 0 v19_541) + (extract + 63 + 0 + (sign_ext + 128 + (extract + 63 + 0 + (if + (bvslt + (bvsrem + v19_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000000)) + (if + (bvslt + (concat #x0000000000000000 #x0000000000000040) + (concat #x0000000000000000 #x0000000000000000)) + (bvsub + (bvsrem + v19_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000040)) + (bvadd + (bvsrem + v19_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000040))) + (bvsrem + v19_537 + (concat #x0000000000000000 #x0000000000000040)))))))) + (= rd v19_544))) + (=> + (and (= alu_op (ALUOp.Lsl)) (= size (OperandSize.Size32))) + (and + (= rm v20_535) + (= v20_537 (zero_ext 128 (extract 31 0 v20_535))) + (= rn v20_541) + (= + v20_544 + (zero_ext + 64 + (bvshl + (extract 31 0 v20_541) + (extract + 31 + 0 + (sign_ext + 128 + (extract + 63 + 0 + (if + (bvslt + (bvsrem + v20_537 + (concat #x0000000000000000 #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000000)) + (if + (bvslt + (concat #x0000000000000000 #x0000000000000020) + (concat #x0000000000000000 #x0000000000000000)) + (bvsub + (bvsrem + v20_537 + (concat + #x0000000000000000 + #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000020)) + (bvadd + (bvsrem + v20_537 + (concat + #x0000000000000000 + #x0000000000000020)) + (concat #x0000000000000000 #x0000000000000020))) + (bvsrem + v20_537 + (concat + #x0000000000000000 + #x0000000000000020))))))))) + (= rd v20_544))) + (=> + (and (= alu_op (ALUOp.Lsl)) (= size (OperandSize.Size64))) + (and + (= rm v21_535) + (= v21_537 (zero_ext 128 (extract 63 0 v21_535))) + (= rn v21_541) + (= + v21_544 + (bvshl + (extract 63 0 v21_541) + (extract + 63 + 0 + (sign_ext + 128 + (extract + 63 + 0 + (if + (bvslt + (bvsrem + v21_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000000)) + (if + (bvslt + (concat #x0000000000000000 #x0000000000000040) + (concat #x0000000000000000 #x0000000000000000)) + (bvsub + (bvsrem + v21_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000040)) + (bvadd + (bvsrem + v21_537 + (concat #x0000000000000000 #x0000000000000040)) + (concat #x0000000000000000 #x0000000000000040))) + (bvsrem + v21_537 + (concat #x0000000000000000 #x0000000000000040)))))))) + (= rd v21_544)))) + (require + (or + (and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.Orr)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.Orr)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.OrrNot)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.OrrNot)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.And)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.And)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.AndNot)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.AndNot)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.Eor)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.Eor)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.EorNot)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.EorNot)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.Lsr)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.Lsr)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.Asr)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.Asr)) (= size (OperandSize.Size64))) + (and (= alu_op (ALUOp.Lsl)) (= size (OperandSize.Size32))) + (and (= alu_op (ALUOp.Lsl)) (= size (OperandSize.Size64)))))) diff --git a/cranelift/codegen/src/isa/riscv64/inst/mod.rs b/cranelift/codegen/src/isa/riscv64/inst/mod.rs index 4c10191eccfc..8d30451a972c 100644 --- a/cranelift/codegen/src/isa/riscv64/inst/mod.rs +++ b/cranelift/codegen/src/isa/riscv64/inst/mod.rs @@ -9,7 +9,7 @@ use crate::binemit::{Addend, CodeOffset, Reloc}; pub use crate::ir::condcodes::IntCC; use crate::ir::types::{self, F32, F64, I128, I16, I32, I64, I8, I8X16, R32, R64}; -pub use crate::ir::{ExternalName, MemFlags, Opcode, SourceLoc, Type, ValueLabel}; +pub use crate::ir::{ExternalName, MemFlags, Opcode, Type}; use crate::isa::{CallConv, FunctionAlignment}; use crate::machinst::*; use crate::{settings, CodegenError, CodegenResult}; diff --git a/cranelift/codegen/src/isa/x64/inst/regs.rs b/cranelift/codegen/src/isa/x64/inst/regs.rs index ce7f1ff72a0b..f564d140c978 100644 --- a/cranelift/codegen/src/isa/x64/inst/regs.rs +++ b/cranelift/codegen/src/isa/x64/inst/regs.rs @@ -51,7 +51,7 @@ pub(crate) fn rax() -> Reg { pub(crate) fn rcx() -> Reg { gpr(ENC_RCX) } -pub(crate) fn rdx() -> Reg { +pub fn rdx() -> Reg { gpr(ENC_RDX) } pub(crate) fn r8() -> Reg { @@ -69,7 +69,7 @@ pub(crate) fn r11() -> Reg { pub(crate) fn r12() -> Reg { gpr(ENC_R12) } -pub(crate) fn r13() -> Reg { +pub fn r13() -> Reg { gpr(ENC_R13) } pub(crate) fn r14() -> Reg { @@ -79,7 +79,7 @@ pub(crate) fn rbx() -> Reg { gpr(ENC_RBX) } -pub(crate) fn r15() -> Reg { +pub fn r15() -> Reg { gpr(ENC_R15) } diff --git a/cranelift/codegen/src/isa/x64/mod.rs b/cranelift/codegen/src/isa/x64/mod.rs index 75fbe2980abb..2a7d63e182c9 100644 --- a/cranelift/codegen/src/isa/x64/mod.rs +++ b/cranelift/codegen/src/isa/x64/mod.rs @@ -22,7 +22,7 @@ use target_lexicon::Triple; mod abi; pub mod encoding; -mod inst; +pub mod inst; mod lower; pub mod settings; diff --git a/cranelift/codegen/src/lib.rs b/cranelift/codegen/src/lib.rs index c856e1a1b645..1a5993ee0ad5 100644 --- a/cranelift/codegen/src/lib.rs +++ b/cranelift/codegen/src/lib.rs @@ -1,5 +1,5 @@ //! Cranelift code generation library. -#![deny(missing_docs, trivial_numeric_casts, unused_extern_crates)] +#![deny(trivial_numeric_casts, unused_extern_crates)] #![warn(unused_import_braces)] #![cfg_attr(feature = "std", deny(unstable_features))] #![no_std] @@ -60,9 +60,9 @@ pub use crate::machinst::buffer::{ MachTextSectionBuilder, MachTrap, }; pub use crate::machinst::{ - CompiledCode, Final, MachBuffer, MachBufferFinalized, MachInst, MachInstEmit, - MachInstEmitState, MachLabel, Reg, TextSectionBuilder, VCodeConstantData, VCodeConstants, - Writable, + AllocationConsumer, CompiledCode, Final, MachBuffer, MachBufferFinalized, MachInst, + MachInstEmit, MachInstEmitState, MachLabel, Reg, TextSectionBuilder, VCodeConstantData, + VCodeConstants, Writable, }; mod alias_analysis; diff --git a/cranelift/codegen/src/machinst/isle.rs b/cranelift/codegen/src/machinst/isle.rs index 13c1792314b5..c3be76f0b070 100644 --- a/cranelift/codegen/src/machinst/isle.rs +++ b/cranelift/codegen/src/machinst/isle.rs @@ -7,12 +7,14 @@ use std::cell::Cell; pub use super::MachLabel; use super::RetPair; pub use crate::ir::{ - condcodes, condcodes::CondCode, dynamic_to_fixed, Constant, DynamicStackSlot, ExternalName, - FuncRef, GlobalValue, Immediate, SigRef, StackSlot, + condcodes, condcodes::CondCode, dynamic_to_fixed, ArgumentExtension, Constant, + DynamicStackSlot, ExternalName, FuncRef, GlobalValue, Immediate, SigRef, StackSlot, }; +pub use crate::isa::unwind::UnwindInst; pub use crate::isa::TargetIsa; pub use crate::machinst::{ - ABIArg, ABIArgSlot, Lower, LowerBackend, RealReg, Reg, RelocDistance, Sig, VCodeInst, Writable, + ABIArg, ABIArgSlot, InputSourceInst, Lower, LowerBackend, RealReg, Reg, RelocDistance, Sig, + VCodeInst, Writable, }; pub use crate::settings::TlsModel; diff --git a/cranelift/codegen/src/prelude_lower.isle b/cranelift/codegen/src/prelude_lower.isle index f6eb20e419b5..a1a4a42865b7 100644 --- a/cranelift/codegen/src/prelude_lower.isle +++ b/cranelift/codegen/src/prelude_lower.isle @@ -107,6 +107,7 @@ ;; Get a temporary register for writing. (decl temp_writable_reg (Type) WritableReg) (extern constructor temp_writable_reg temp_writable_reg) +(spec (temp_writable_reg ty) (provide (= ty (widthof result)))) ;; Get a temporary register for reading. (decl temp_reg (Type) Reg) @@ -266,6 +267,7 @@ ;; Turn a `Writable` into a `Reg` via `Writable::to_reg`. (decl pure writable_reg_to_reg (WritableReg) Reg) (extern constructor writable_reg_to_reg writable_reg_to_reg) +(spec (writable_reg_to_reg reg) (provide (= result reg))) ;; Extract the result values for the given instruction. (decl inst_results (ValueSlice) Inst) @@ -332,6 +334,8 @@ (decl emit (MInst) Unit) (extern constructor emit emit) +; TODO(mbm): what is the right spec for emit? +(spec (emit inst) (provide (= result #b1))) ;; Sink an instruction. ;; diff --git a/cranelift/isle/isle/Cargo.toml b/cranelift/isle/isle/Cargo.toml index db802bf0f06d..17b317291caf 100644 --- a/cranelift/isle/isle/Cargo.toml +++ b/cranelift/isle/isle/Cargo.toml @@ -11,6 +11,9 @@ version = "0.101.0" [dependencies] codespan-reporting = { version = "0.11.1", optional = true } log = { workspace = true, optional = true } +pretty = "0.12.3" +clap = { workspace = true } +env_logger = { workspace = true } [dev-dependencies] tempfile = "3" diff --git a/cranelift/isle/isle/build.rs b/cranelift/isle/isle/build.rs index 96aa9ec06d44..191c4b0e63e1 100644 --- a/cranelift/isle/isle/build.rs +++ b/cranelift/isle/isle/build.rs @@ -1,4 +1,4 @@ -use std::fmt::Write; +use std::{fmt::Write, path::PathBuf}; fn main() { println!("cargo:rerun-if-changed=build.rs"); @@ -15,12 +15,20 @@ fn main() { emit_tests(&mut out, "isle_examples/link", "run_link"); emit_tests(&mut out, "isle_examples/run", "run_run"); + emit_tests(&mut out, "isle_examples/pass", "run_print"); + emit_tests(&mut out, "../../codegen/src/opts", "run_print"); + emit_tests(&mut out, "../../codegen/src/isa/x64", "run_print"); + emit_tests(&mut out, "../../codegen/src/isa/aarch64", "run_print"); + emit_tests(&mut out, "../../codegen/src/isa/riscv64", "run_print"); + let output = out_dir.join("isle_tests.rs"); std::fs::write(output, out).unwrap(); } fn emit_tests(out: &mut String, dir_name: &str, runner_func: &str) { - for test_file in std::fs::read_dir(dir_name).unwrap() { + let dir_path = PathBuf::from(dir_name); + let test_name = dir_path.file_name().unwrap().to_string_lossy(); + for test_file in std::fs::read_dir(&dir_path).unwrap() { let test_file = test_file.unwrap().file_name().into_string().unwrap(); if !test_file.ends_with(".isle") { continue; @@ -28,7 +36,12 @@ fn emit_tests(out: &mut String, dir_name: &str, runner_func: &str) { let test_file_base = test_file.replace(".isle", ""); writeln!(out, "#[test]").unwrap(); - writeln!(out, "fn test_{}_{}() {{", runner_func, test_file_base).unwrap(); + writeln!( + out, + "fn test_{}_{}_{}() {{", + runner_func, test_name, test_file_base + ) + .unwrap(); writeln!(out, " {}(\"{}/{}\");", runner_func, dir_name, test_file).unwrap(); writeln!(out, "}}").unwrap(); } diff --git a/cranelift/isle/isle/isle_examples/pass/veri_spec.isle b/cranelift/isle/isle/isle_examples/pass/veri_spec.isle index d9b4cfe16059..886f1ffcf81d 100644 --- a/cranelift/isle/isle/isle_examples/pass/veri_spec.isle +++ b/cranelift/isle/isle/isle_examples/pass/veri_spec.isle @@ -2,14 +2,14 @@ (form unary_bv_8_to_64 - (args ((bv 8)) (return (bv 8)) (canon (bv 8))) - (args ((bv 16)) (return (bv 16)) (canon (bv 16))) - (args ((bv 32)) (return (bv 32)) (canon (bv 32))) - (args ((bv 64)) (return (bv 64)) (canon (bv 64))) + ((args (bv 8)) (ret (bv 8)) (canon (bv 8))) + ((args (bv 16)) (ret (bv 16)) (canon (bv 16))) + ((args (bv 32)) (ret (bv 32)) (canon (bv 32))) + ((args (bv 64)) (ret (bv 64)) (canon (bv 64))) ) (spec (A i j) (provide (= (if true (= i j) (= i (bvneg j)))))) -(instantiate A (args ((bv 8)) (return (bv 8)) (canon (bv 8)))) +(instantiate A ((args (bv 8)) (ret (bv 8)) (canon (bv 8)))) (decl A (u8 u8) u8) (spec (B i) diff --git a/cranelift/isle/isle/src/ast.rs b/cranelift/isle/isle/src/ast.rs index 5aefba303add..88bd92d260d5 100644 --- a/cranelift/isle/isle/src/ast.rs +++ b/cranelift/isle/isle/src/ast.rs @@ -102,6 +102,7 @@ pub enum SpecExpr { }, /// An operator that matches a constant bitvector value. ConstBitVec { + // TODO(mbm): support arbitrary length bitvectors val: i128, width: i8, pos: Pos, @@ -141,6 +142,7 @@ pub enum SpecOp { And, Or, Not, + Imp, // Integer comparisons Lt, diff --git a/cranelift/isle/isle/src/bin/isleprint.rs b/cranelift/isle/isle/src/bin/isleprint.rs new file mode 100644 index 000000000000..19d42e1bbed3 --- /dev/null +++ b/cranelift/isle/isle/src/bin/isleprint.rs @@ -0,0 +1,28 @@ +use clap::Parser; +use cranelift_isle as isle; +use std::path::PathBuf; + +#[derive(Parser)] +struct Opts { + /// The input ISLE DSL source files. + #[clap(required = true)] + inputs: Vec, + + /// Line length. + #[clap(long, default_value = "78")] + width: usize, +} + +fn main() -> Result<(), isle::error::Errors> { + let _ = env_logger::try_init(); + + let opts = Opts::parse(); + + let lexer = isle::lexer::Lexer::from_files(&opts.inputs)?; + let defs = isle::parser::parse(lexer)?; + + let mut stdout = std::io::stdout(); + isle::printer::print(&defs, opts.width, &mut stdout)?; + + Ok(()) +} diff --git a/cranelift/isle/isle/src/error.rs b/cranelift/isle/isle/src/error.rs index f9c8468c8aec..f0274febc68e 100644 --- a/cranelift/isle/isle/src/error.rs +++ b/cranelift/isle/isle/src/error.rs @@ -5,6 +5,7 @@ use std::sync::Arc; use crate::lexer::Pos; /// A collection of errors from attempting to compile some ISLE source files. +#[derive(Debug)] pub struct Errors { /// The individual errors. pub errors: Vec, @@ -12,7 +13,9 @@ pub struct Errors { pub(crate) file_texts: Vec>, } -impl std::fmt::Debug for Errors { +impl std::error::Error for Errors {} + +impl std::fmt::Display for Errors { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { if self.errors.is_empty() { return Ok(()); diff --git a/cranelift/isle/isle/src/lib.rs b/cranelift/isle/isle/src/lib.rs index 3171848a44ca..f56b90a469ee 100644 --- a/cranelift/isle/isle/src/lib.rs +++ b/cranelift/isle/isle/src/lib.rs @@ -267,6 +267,7 @@ pub mod lexer; mod log; pub mod overlap; pub mod parser; +pub mod printer; pub mod sema; pub mod serialize; pub mod trie_again; diff --git a/cranelift/isle/isle/src/parser.rs b/cranelift/isle/isle/src/parser.rs index 1f3978bf7cf4..cc8d73f901d8 100644 --- a/cranelift/isle/isle/src/parser.rs +++ b/cranelift/isle/isle/src/parser.rs @@ -1,5 +1,7 @@ //! Parser for ISLE language. +#![allow(missing_docs)] + use crate::ast::*; use crate::error::{Error, Errors, Span}; use crate::lexer::{Lexer, Pos, Token}; @@ -16,8 +18,11 @@ pub fn parse(lexer: Lexer) -> Result { /// /// Takes in a lexer and creates an AST. #[derive(Clone, Debug)] -struct Parser<'a> { +pub struct Parser<'a> { lexer: Lexer<'a>, + + // HACK: allow positions to be disabled to support testing + populate_pos: bool, } /// Used during parsing a `(rule ...)` to encapsulate some form that @@ -31,7 +36,15 @@ enum IfLetOrExpr { impl<'a> Parser<'a> { /// Construct a new parser from the given lexer. pub fn new(lexer: Lexer<'a>) -> Parser<'a> { - Parser { lexer } + Parser { + lexer, + populate_pos: true, + } + } + + // HACK: allow positions to be disabled to support testing + pub fn disable_pos(&mut self) { + self.populate_pos = false; } fn error(&self, pos: Pos, msg: String) -> Errors { @@ -76,9 +89,13 @@ impl<'a> Parser<'a> { } fn pos(&self) -> Pos { - self.lexer - .peek() - .map_or_else(|| self.lexer.pos(), |(pos, _)| *pos) + if self.populate_pos { + self.lexer + .peek() + .map_or_else(|| self.lexer.pos(), |(pos, _)| *pos) + } else { + Pos::default() + } } fn is_lparen(&self) -> bool { @@ -150,7 +167,7 @@ impl<'a> Parser<'a> { } } - fn parse_defs(mut self) -> Result { + pub fn parse_defs(mut self) -> Result { let mut defs = vec![]; while !self.lexer.eof() { defs.push(self.parse_def()?); @@ -458,6 +475,7 @@ impl<'a> Parser<'a> { "and" => Ok(SpecOp::And), "not" => Ok(SpecOp::Not), "or" => Ok(SpecOp::Or), + "=>" => Ok(SpecOp::Imp), "<=" => Ok(SpecOp::Lte), "<" => Ok(SpecOp::Lt), ">=" => Ok(SpecOp::Gte), diff --git a/cranelift/isle/isle/src/printer.rs b/cranelift/isle/isle/src/printer.rs new file mode 100644 index 000000000000..231eb21eee67 --- /dev/null +++ b/cranelift/isle/isle/src/printer.rs @@ -0,0 +1,415 @@ +//! Printer for ISLE language. + +#![allow(missing_docs)] + +use crate::ast::*; +use crate::error::Errors; +use pretty::{Doc, Pretty, RcAllocator, RcDoc}; +use std::io::Write; + +pub trait Printable { + fn to_doc(&self) -> RcDoc<()>; +} + +pub fn print(node: &N, width: usize, out: &mut W) -> Result<(), Errors> +where + N: Printable, + W: ?Sized + Write, +{ + node.to_doc() + .render(width, out) + .map_err(|e| Errors::from_io(e, "failed to print isle")) +} + +pub fn dump(node: &N) -> Result<(), Errors> { + let mut stdout = std::io::stdout(); + print(node, 78, &mut stdout) +} + +impl Printable for Defs { + fn to_doc(&self) -> RcDoc<()> { + let sep = RcDoc::hardline().append(Doc::hardline()); + RcDoc::intersperse(self.defs.iter().map(|d| d.to_doc()), sep).append(Doc::hardline()) + } +} + +impl Printable for Def { + fn to_doc(&self) -> RcDoc<()> { + match self { + Def::Pragma(_) => unimplemented!("pragmas not supported"), + Def::Type(ref t) => { + let mut parts = vec![RcDoc::text("type")]; + parts.push(t.name.to_doc()); + if t.is_extern { + parts.push(RcDoc::text("extern")); + } + if t.is_nodebug { + parts.push(RcDoc::text("nodebug")); + } + parts.push(t.ty.to_doc()); + sexp(parts) + } + Def::Rule(ref r) => { + let mut parts = Vec::new(); + parts.push(RcDoc::text("rule")); + if let Some(name) = &r.name { + parts.push(name.to_doc()); + } + if let Some(prio) = &r.prio { + parts.push(RcDoc::as_string(prio)); + } + parts.push(r.pattern.to_doc()); + parts.extend(r.iflets.iter().map(|il| il.to_doc())); + parts.push(r.expr.to_doc()); + sexp(parts) + } + Def::Extractor(ref e) => sexp(vec![ + RcDoc::text("extractor"), + sexp( + Vec::from([e.term.to_doc()]) + .into_iter() + .chain(e.args.iter().map(|v| v.to_doc())), + ), + e.template.to_doc(), + ]), + Def::Decl(ref d) => { + let mut parts = Vec::new(); + parts.push(RcDoc::text("decl")); + if d.pure { + parts.push(RcDoc::text("pure")); + } + if d.multi { + parts.push(RcDoc::text("multi")); + } + if d.partial { + parts.push(RcDoc::text("partial")); + } + parts.push(d.term.to_doc()); + parts.push(sexp(d.arg_tys.iter().map(|ty| ty.to_doc()))); + parts.push(d.ret_ty.to_doc()); + sexp(parts) + } + Def::Spec(ref s) => s.to_doc(), + Def::Model(ref m) => sexp(vec![RcDoc::text("model"), m.name.to_doc(), m.val.to_doc()]), + Def::Form(ref f) => { + let mut parts = vec![RcDoc::text("form")]; + parts.push(f.name.to_doc()); + parts.extend(f.signatures.iter().map(|s| s.to_doc())); + sexp(parts) + } + Def::Instantiation(ref i) => { + let mut parts = vec![RcDoc::text("instantiate"), i.term.to_doc()]; + if let Some(form) = &i.form { + parts.push(form.to_doc()); + } else { + parts.extend(i.signatures.iter().map(|s| s.to_doc())); + } + sexp(parts) + } + Def::Extern(ref e) => e.to_doc(), + Def::Converter(ref c) => sexp(vec![ + RcDoc::text("convert"), + c.inner_ty.to_doc(), + c.outer_ty.to_doc(), + c.term.to_doc(), + ]), + } + } +} + +impl Printable for Ident { + fn to_doc(&self) -> RcDoc<()> { + RcDoc::text(self.0.clone()) + } +} + +impl Printable for TypeValue { + fn to_doc(&self) -> RcDoc<()> { + match self { + TypeValue::Primitive(ref name, _) => { + sexp(vec![RcDoc::text("primitive"), name.to_doc()]) + } + TypeValue::Enum(ref variants, _) => sexp( + // TODO(mbm): convenience for sexp with a fixed first element + Vec::from([RcDoc::text("enum")]) + .into_iter() + .chain(variants.iter().map(|v| v.to_doc())), + ), + } + } +} + +impl Printable for Variant { + fn to_doc(&self) -> RcDoc<()> { + sexp( + // TODO(mbm): convenience for sexp with a fixed first element + Vec::from([self.name.to_doc()]) + .into_iter() + .chain(self.fields.iter().map(|f| f.to_doc())), + ) + } +} + +impl Printable for Field { + fn to_doc(&self) -> RcDoc<()> { + sexp(vec![self.name.to_doc(), self.ty.to_doc()]) + } +} + +impl Printable for ModelValue { + fn to_doc(&self) -> RcDoc<()> { + match self { + ModelValue::TypeValue(ref mt) => sexp(vec![RcDoc::text("type"), mt.to_doc()]), + ModelValue::EnumValues(ref values) => sexp( + Vec::from([RcDoc::text("enum")]).into_iter().chain( + values + .iter() + .map(|(name, expr)| sexp(vec![name.to_doc(), expr.to_doc()])), + ), + ), + } + } +} + +impl Printable for ModelType { + fn to_doc(&self) -> RcDoc<()> { + match self { + ModelType::Int => RcDoc::text("Int"), + ModelType::Bool => RcDoc::text("Bool"), + ModelType::BitVec(Some(size)) => sexp(vec![RcDoc::text("bv"), RcDoc::as_string(size)]), + ModelType::BitVec(None) => sexp(vec![RcDoc::text("bv")]), + } + } +} + +impl Printable for Signature { + fn to_doc(&self) -> RcDoc<()> { + sexp(vec![ + sexp( + Vec::from([RcDoc::text("args")]) + .into_iter() + .chain(self.args.iter().map(|a| a.to_doc())), + ), + sexp(vec![RcDoc::text("ret"), self.ret.to_doc()]), + sexp(vec![RcDoc::text("canon"), self.canonical.to_doc()]), + ]) + } +} + +impl Printable for SpecExpr { + fn to_doc(&self) -> RcDoc<()> { + match self { + SpecExpr::ConstInt { val, .. } => RcDoc::as_string(val), + SpecExpr::ConstBitVec { val, width, .. } => RcDoc::text(if width % 4 == 0 { + format!("#x{val:0width$x}", width = *width as usize / 4) + } else { + format!("#b{val:0width$b}", width = *width as usize) + }), + SpecExpr::ConstBool { val, .. } => { + RcDoc::text(if *val != 0 { "true" } else { "false" }) + } + SpecExpr::Var { var, .. } => var.to_doc(), + SpecExpr::Op { op, args, .. } => sexp( + Vec::from([op.to_doc()]) + .into_iter() + .chain(args.iter().map(|a| a.to_doc())), + ), + SpecExpr::Pair { l, r } => sexp(vec![l.to_doc(), r.to_doc()]), + SpecExpr::Enum { name } => sexp(vec![name.to_doc()]), + } + } +} + +impl Printable for SpecOp { + fn to_doc(&self) -> RcDoc<()> { + RcDoc::text(match self { + SpecOp::Eq => "=", + SpecOp::And => "and", + SpecOp::Not => "not", + SpecOp::Or => "or", + SpecOp::Imp => "=>", + SpecOp::Lte => "<=", + SpecOp::Lt => "<", + SpecOp::Gte => ">=", + SpecOp::Gt => ">", + SpecOp::BVNot => "bvnot", + SpecOp::BVAnd => "bvand", + SpecOp::BVOr => "bvor", + SpecOp::BVXor => "bvxor", + SpecOp::BVNeg => "bvneg", + SpecOp::BVAdd => "bvadd", + SpecOp::BVSub => "bvsub", + SpecOp::BVMul => "bvmul", + SpecOp::BVUdiv => "bvudiv", + SpecOp::BVUrem => "bvurem", + SpecOp::BVSdiv => "bvsdiv", + SpecOp::BVSrem => "bvsrem", + SpecOp::BVShl => "bvshl", + SpecOp::BVLshr => "bvlshr", + SpecOp::BVAshr => "bvashr", + SpecOp::BVSaddo => "bvsaddo", + SpecOp::BVUle => "bvule", + SpecOp::BVUlt => "bvult", + SpecOp::BVUgt => "bvugt", + SpecOp::BVUge => "bvuge", + SpecOp::BVSlt => "bvslt", + SpecOp::BVSle => "bvsle", + SpecOp::BVSgt => "bvsgt", + SpecOp::BVSge => "bvsge", + SpecOp::Rotr => "rotr", + SpecOp::Rotl => "rotl", + SpecOp::Extract => "extract", + SpecOp::ZeroExt => "zero_ext", + SpecOp::SignExt => "sign_ext", + SpecOp::Concat => "concat", + SpecOp::ConvTo => "conv_to", + SpecOp::Int2BV => "int2bv", + SpecOp::BV2Int => "bv2int", + SpecOp::WidthOf => "widthof", + SpecOp::If => "if", + SpecOp::Switch => "switch", + SpecOp::Subs => "subs", + SpecOp::Popcnt => "popcnt", + SpecOp::Rev => "rev", + SpecOp::Cls => "cls", + SpecOp::Clz => "clz", + }) + } +} + +impl Printable for Spec { + fn to_doc(&self) -> RcDoc<()> { + let mut parts = vec![RcDoc::text("spec")]; + parts.push(sexp( + Vec::from([self.term.to_doc()]) + .into_iter() + .chain(self.args.iter().map(|a| a.to_doc())), + )); + if !self.provides.is_empty() { + parts.push(sexp( + Vec::from([RcDoc::text("provide")]) + .into_iter() + .chain(self.provides.iter().map(|e| e.to_doc())), + )); + } + if !self.requires.is_empty() { + parts.push(sexp( + Vec::from([RcDoc::text("require")]) + .into_iter() + .chain(self.requires.iter().map(|e| e.to_doc())), + )); + } + sexp(parts) + } +} + +impl Printable for Pattern { + fn to_doc(&self) -> RcDoc<()> { + match self { + Pattern::Var { var, .. } => var.to_doc(), + Pattern::BindPattern { var, subpat, .. } => RcDoc::intersperse( + vec![var.to_doc(), RcDoc::text("@"), subpat.to_doc()], + Doc::space(), + ), + Pattern::ConstInt { val, .. } => RcDoc::as_string(val), + Pattern::ConstPrim { val, .. } => RcDoc::text("$").append(val.to_doc()), + Pattern::Wildcard { .. } => RcDoc::text("_"), + Pattern::Term { sym, args, .. } => sexp( + // TODO(mbm): convenience for sexp with a fixed first element + Vec::from([sym.to_doc()]) + .into_iter() + .chain(args.iter().map(|f| f.to_doc())), + ), + Pattern::And { subpats, .. } => sexp( + Vec::from([RcDoc::text("and")]) + .into_iter() + .chain(subpats.iter().map(|p| p.to_doc())), + ), + Pattern::MacroArg { .. } => unimplemented!("macro arguments are for internal use only"), + } + } +} + +impl Printable for IfLet { + fn to_doc(&self) -> RcDoc<()> { + // TODO(mbm): `if` shorthand when pattern is wildcard + sexp(vec![ + RcDoc::text("if-let"), + self.pattern.to_doc(), + self.expr.to_doc(), + ]) + } +} + +impl Printable for Expr { + fn to_doc(&self) -> RcDoc<()> { + match self { + Expr::Term { sym, args, .. } => sexp( + // TODO(mbm): convenience for sexp with a fixed first element + Vec::from([sym.to_doc()]) + .into_iter() + .chain(args.iter().map(|f| f.to_doc())), + ), + Expr::Var { name, .. } => name.to_doc(), + Expr::ConstInt { val, .. } => RcDoc::as_string(val), + Expr::ConstPrim { val, .. } => RcDoc::text("$").append(val.to_doc()), + Expr::Let { defs, body, .. } => { + let mut parts = Vec::new(); + parts.push(RcDoc::text("let")); + parts.push(sexp(defs.iter().map(|d| d.to_doc()))); + parts.push(body.to_doc()); + sexp(parts) + } + } + } +} + +impl Printable for LetDef { + fn to_doc(&self) -> RcDoc<()> { + sexp(vec![self.var.to_doc(), self.ty.to_doc(), self.val.to_doc()]) + } +} + +impl Printable for Extern { + fn to_doc(&self) -> RcDoc<()> { + match self { + Extern::Extractor { + term, + func, + pos: _, + infallible, + } => { + let mut parts = vec![RcDoc::text("extern"), RcDoc::text("extractor")]; + if *infallible { + parts.push(RcDoc::text("infallible")); + } + parts.push(term.to_doc()); + parts.push(func.to_doc()); + sexp(parts) + } + Extern::Constructor { term, func, .. } => sexp(vec![ + RcDoc::text("extern"), + RcDoc::text("constructor"), + term.to_doc(), + func.to_doc(), + ]), + Extern::Const { name, ty, .. } => sexp(vec![ + RcDoc::text("extern"), + RcDoc::text("const"), + RcDoc::text("$").append(name.to_doc()), + ty.to_doc(), + ]), + } + } +} + +fn sexp<'a, I, A>(docs: I) -> RcDoc<'a, A> +where + I: IntoIterator, + I::Item: Pretty<'a, RcAllocator, A>, + A: Clone, +{ + RcDoc::text("(") + .append(RcDoc::intersperse(docs, Doc::line()).nest(4).group()) + .append(RcDoc::text(")")) +} diff --git a/cranelift/isle/isle/tests/run_tests.rs b/cranelift/isle/isle/tests/run_tests.rs index 1b347b9454ce..2c25b8f1f133 100644 --- a/cranelift/isle/isle/tests/run_tests.rs +++ b/cranelift/isle/isle/tests/run_tests.rs @@ -1,8 +1,20 @@ //! Helper for autogenerated unit tests. +use cranelift_isle::ast::Defs; use cranelift_isle::compile; use cranelift_isle::error::Errors; +use cranelift_isle::lexer::{self, Lexer}; +use cranelift_isle::parser::Parser; +use cranelift_isle::printer; use std::default::Default; +use std::io::BufWriter; +use std::iter::zip; + +fn parse(lexer: Lexer) -> Result { + let mut parser = Parser::new(lexer); + parser.disable_pos(); + parser.parse_defs() +} fn build(filename: &str) -> Result { compile::from_files(&[filename], &Default::default()) @@ -63,6 +75,28 @@ pub fn run_link(isle_filename: &str) { build_and_link_isle(isle_filename); } +pub fn run_print(isle_filename: &str) { + // Parse. + let lexer = lexer::Lexer::from_files(&[isle_filename]).unwrap(); + let original = parse(lexer).unwrap(); + + // Print. + let mut buf = BufWriter::new(Vec::new()); + printer::print(&original, 78, &mut buf).unwrap(); + let bytes = buf.into_inner().unwrap(); + let isle_source = String::from_utf8(bytes).unwrap(); + + // Round trip. + let lexer = lexer::Lexer::from_str(&isle_source, "").unwrap(); + let round_trip = parse(lexer).unwrap(); + + // Ensure equal. + assert_eq!(original.defs.len(), round_trip.defs.len()); + for (orig, rt) in zip(original.defs, round_trip.defs) { + assert_eq!(orig, rt); + } +} + pub fn run_run(isle_filename: &str) { let (_tempdir, exe) = build_and_link_isle(isle_filename); diff --git a/cranelift/isle/veri/veri_engine/Cargo.toml b/cranelift/isle/veri/veri_engine/Cargo.toml index 6894eab445a5..18debe0bfc58 100644 --- a/cranelift/isle/veri/veri_engine/Cargo.toml +++ b/cranelift/isle/veri/veri_engine/Cargo.toml @@ -13,10 +13,26 @@ path = "src/lib.rs" name = "veri_engine_bin" path = "src/main.rs" +[[bin]] +name = "isla" +path = "src/isla.rs" + +[[bin]] +name = "emit" +path = "src/emit.rs" + +[[bin]] +name = "x64" +path = "src/x64.rs" + [dependencies] cranelift-isle = { path = "../../isle" } cranelift-codegen = { path = "../../../codegen" } +cranelift-reader = { path = "../../../reader" } cranelift-codegen-meta = { path = "../../../codegen/meta" } +isla = { git = "https://github.com/rems-project/isla.git", rev = "2a4bd429b56634db52d59707b83090a535b5c4bc" } +isla-lib = { git = "https://github.com/rems-project/isla.git", rev = "2a4bd429b56634db52d59707b83090a535b5c4bc" } +anyhow = { workspace = true } veri_ir = { path = "../veri_ir" } easy-smt = { git = "https://github.com/elliottt/easy-smt.git" } clap = { version = "3.0.0", features = ["derive"] } @@ -24,7 +40,12 @@ itertools = "0.10.3" log = "0.4.17" env_logger = "0.10.0" retry = "2.0.0" +sha2 = "0.8.1" +crossbeam = "0.8.1" [dev-dependencies] strum = "0.24.0" strum_macros = "0.24.0" + +[features] +default = ["cranelift-codegen/all-arch", "cranelift-codegen/trace-log"] diff --git a/cranelift/isle/veri/veri_engine/src/annotations.rs b/cranelift/isle/veri/veri_engine/src/annotations.rs index 4e4dafef2988..c796dc1d7a7d 100644 --- a/cranelift/isle/veri/veri_engine/src/annotations.rs +++ b/cranelift/isle/veri/veri_engine/src/annotations.rs @@ -141,6 +141,7 @@ fn spec_op_to_expr(s: &SpecOp, args: &Vec, pos: &Pos, env: &ParsingEnv SpecOp::Lte => binop(|x, y| Expr::Lte(x, y), args, pos, env), SpecOp::Gt => binop(|x, y| Expr::Lt(y, x), args, pos, env), SpecOp::Gte => binop(|x, y| Expr::Lte(y, x), args, pos, env), + SpecOp::Imp => binop(|x, y| Expr::Imp(x, y), args, pos, env), SpecOp::BVAnd => binop(|x, y| Expr::BVAnd(x, y), args, pos, env), SpecOp::BVOr => binop(|x, y| Expr::BVOr(x, y), args, pos, env), SpecOp::BVXor => binop(|x, y| Expr::BVXor(x, y), args, pos, env), diff --git a/cranelift/isle/veri/veri_engine/src/bin/isaspec.rs b/cranelift/isle/veri/veri_engine/src/bin/isaspec.rs new file mode 100644 index 000000000000..c80b570164fb --- /dev/null +++ b/cranelift/isle/veri/veri_engine/src/bin/isaspec.rs @@ -0,0 +1,1026 @@ +use cranelift_codegen::isa::aarch64::inst::*; +use cranelift_codegen::settings; +use cranelift_codegen::AllocationConsumer; +use cranelift_codegen::MachBuffer; +use cranelift_codegen::MachInstEmit; +use cranelift_isle::ast::{Def, Defs, Ident, Spec, SpecExpr, SpecOp}; +use cranelift_isle::lexer::Pos; +use cranelift_isle::printer; +use crossbeam::queue::SegQueue; +use isla::opts; +use isla_lib::bitvector::{b64::B64, BV}; +use isla_lib::error::IslaError; +use isla_lib::executor::{self, LocalFrame, TaskState}; +use isla_lib::init::{initialize_architecture, Initialized}; +use isla_lib::ir::Name; +use isla_lib::ir::{AssertionMode, Val}; +use isla_lib::memory::Memory; +use isla_lib::simplify::{self, WriteOpts}; +use isla_lib::smt::smtlib; +use isla_lib::smt::{self, Checkpoint, Event, Solver, Sym}; +use isla_lib::zencode; +use itertools::Itertools; +use sha2::{Digest, Sha256}; +use std::collections::{HashMap, HashSet}; +use std::io::prelude::*; +use std::io::BufWriter; +use std::path::PathBuf; +use std::sync::Arc; + +fn main() -> anyhow::Result<()> { + // Command-line options. + let mut opts = opts::common_opts(); + opts.optopt("", "spec", "path to output spec", ""); + opts.optopt("", "width", "line length for output spec", ""); + + // Build ISLA architecture. + let mut hasher = Sha256::new(); + let (matches, arch) = opts::parse::(&mut hasher, &opts); + let opts::CommonOpts { + num_threads: _, + mut arch, + symtab, + type_info, + isa_config, + source_path: _, + } = opts::parse_with_arch(&mut hasher, &opts, &matches, &arch); + let use_model_reg_init = true; + let iarch = initialize_architecture( + &mut arch, + symtab, + type_info, + &isa_config, + AssertionMode::Optimistic, + use_model_reg_init, + ); + + // Spec configuration. + let cfgs = define(); + + // Generate specs. + let spec_converter = SpecConverter::new(cfgs, &iarch); + let spec = spec_converter.generate()?; + + // Output. + let width = matches.opt_get_default("width", 78)?; + if let Some(path) = matches.opt_str("spec") { + let mut file = std::fs::File::create(path)?; + printer::print(&spec, width, &mut file)?; + } else { + let mut stdout = std::io::stdout(); + printer::print(&spec, width, &mut stdout)?; + }; + + Ok(()) +} + +/// Define specificiations to generate. +fn define() -> Vec { + // ALUOp + let alu_ops = vec![ + ALUOp::Add, + ALUOp::Sub, + ALUOp::Orr, + ALUOp::OrrNot, + ALUOp::And, + ALUOp::AndNot, + ALUOp::Eor, + ALUOp::EorNot, + ALUOp::Lsr, + ALUOp::Asr, + ALUOp::Lsl, + //ALUOp::AndS, // 2 code paths + //ALUOp::AddS, + //ALUOp::SubS, + //ALUOp::SMulH, + //ALUOp::UMulH, + //ALUOp::SDiv, + //ALUOp::UDiv, + //ALUOp::RotR, + //ALUOp::Adc, + //ALUOp::AdcS, + //ALUOp::Sbc, + //ALUOp::SbcS, + ]; + + // OperandSize + let sizes = vec![OperandSize::Size32, OperandSize::Size64]; + + // AluRRR + let alu_rrr = SpecConfig { + // Spec signature. + term: "MInst.AluRRR".to_string(), + args: ["alu_op", "size", "rd", "rn", "rm"] + .map(String::from) + .to_vec(), + + cases: alu_ops + .iter() + .copied() + .cartesian_product(sizes) + .map(|(alu_op, size)| InstConfig { + inst: Inst::AluRRR { + alu_op, + size, + rd: writable_xreg(4), + rn: xreg(5), + rm: xreg(6), + }, + + // Requires. + require: vec![ + spec_eq( + spec_var("alu_op".to_string()), + spec_enum("ALUOp".to_string(), format!("{alu_op:?}")), + ), + spec_eq( + spec_var("size".to_string()), + spec_enum("OperandSize".to_string(), format!("{size:?}")), + ), + ], + + // Register read/write bindings. + reg_read: HashMap::from([ + ("R5".to_string(), "rn".to_string()), + ("R6".to_string(), "rm".to_string()), + ]), + reg_write: HashMap::from([("R4".to_string(), "rd".to_string())]), + }) + .collect(), + }; + + // Inst::Extend { + // rd: writable_xreg(1), + // rn: xreg(2), + // signed: true, + // from_bits: 8, + // to_bits: 32, + // }, + + vec![alu_rrr] +} + +fn assemble(inst: &Inst) -> Vec { + let flags = settings::Flags::new(settings::builder()); + let emit_info = EmitInfo::new(flags); + let mut buffer = MachBuffer::new(); + inst.emit(&[], &mut buffer, &emit_info, &mut Default::default()); + let buffer = buffer.finish(&Default::default(), &mut Default::default()); + return buffer.data().to_vec(); +} + +fn opcodes(inst: &Inst) -> Vec { + let machine_code = assemble(&inst); + let mut opcodes = Vec::new(); + for opcode_bytes in machine_code.chunks(4) { + assert_eq!(opcode_bytes.len(), 4); + opcodes.push(u32::from_le_bytes(opcode_bytes.try_into().unwrap())); + } + opcodes +} + +fn trace_opcode<'ir, B: BV>( + opcode: u32, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result>>> { + let shared_state = &&iarch.shared_state; + + let initial_checkpoint = Checkpoint::new(); + let solver_cfg = smt::Config::new(); + let solver_ctx = smt::Context::new(solver_cfg); + let mut solver = Solver::from_checkpoint(&solver_ctx, initial_checkpoint); + let checkpoint = smt::checkpoint(&mut solver); + + let opcode_val = Val::Bits(B::from_u32(opcode)); + + let footprint_function = zencode::encode("isla_footprint_no_init"); + let function_id = shared_state.symtab.lookup(&footprint_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + let memory = Memory::new(); + let task_state = TaskState::::new(); + let task = LocalFrame::new(function_id, args, ret_ty, Some(&[opcode_val]), instrs) + .add_lets(&iarch.lets) + .add_regs(&iarch.regs) + .set_memory(memory) + .task_with_checkpoint(0, &task_state, checkpoint); + + let num_threads = 1; + let queue = Arc::new(SegQueue::new()); + executor::start_multi( + num_threads, + None, + vec![task], + shared_state, + queue.clone(), + &executor::trace_collector, + ); + + let mut paths = Vec::new(); + loop { + match queue.pop() { + Some(Ok((_, mut events))) => { + simplify::hide_initialization(&mut events); + simplify::remove_extra_register_fields(&mut events); + simplify::remove_repeated_register_reads(&mut events); + simplify::remove_unused_register_assumptions(&mut events); + simplify::remove_unused(&mut events); + simplify::propagate_forwards_used_once(&mut events); + simplify::commute_extract(&mut events); + simplify::eval(&mut events); + + let events: Vec> = events.drain(..).rev().collect(); + paths.push(events); + } + + // Error during execution + Some(Err(err)) => { + let msg = format!("{}", err); + eprintln!( + "{}", + err.source_loc().message::( + None, + shared_state.symtab.files(), + &msg, + true, + true + ) + ); + anyhow::bail!("{}", err); + } + // Empty queue + None => break, + } + } + + Ok(paths) +} + +fn event_writes(event: &Event) -> HashSet { + match event { + Event::Smt(def, _, _) => match def { + smtlib::Def::DefineConst(v, _) => HashSet::from([*v]), + _ => HashSet::new(), + }, + Event::ReadReg(_, _, val) => val_uses(val), + _ => HashSet::new(), + } +} + +fn defns(events: &Vec>) -> HashMap { + let mut defn_idx = HashMap::new(); + for (i, event) in events.iter().enumerate() { + for sym in event_writes(event) { + defn_idx.insert(sym, i); + } + } + defn_idx +} + +fn exp_uses(exp: &smtlib::Exp) -> HashSet { + use smtlib::Exp::*; + match exp { + Var(sym) => HashSet::from([*sym]), + Bits(_) | Bits64(_) | Enum(_) | Bool(_) | FPConstant(..) | FPRoundingMode(_) => { + HashSet::new() + } + Not(exp) + | Bvnot(exp) + | Bvneg(exp) + | Extract(_, _, exp) + | ZeroExtend(_, exp) + | SignExtend(_, exp) + | FPUnary(_, exp) => exp_uses(exp), + Eq(lhs, rhs) + | Neq(lhs, rhs) + | And(lhs, rhs) + | Or(lhs, rhs) + | Bvand(lhs, rhs) + | Bvor(lhs, rhs) + | Bvxor(lhs, rhs) + | Bvnand(lhs, rhs) + | Bvnor(lhs, rhs) + | Bvxnor(lhs, rhs) + | Bvadd(lhs, rhs) + | Bvsub(lhs, rhs) + | Bvmul(lhs, rhs) + | Bvudiv(lhs, rhs) + | Bvsdiv(lhs, rhs) + | Bvurem(lhs, rhs) + | Bvsrem(lhs, rhs) + | Bvsmod(lhs, rhs) + | Bvult(lhs, rhs) + | Bvslt(lhs, rhs) + | Bvule(lhs, rhs) + | Bvsle(lhs, rhs) + | Bvuge(lhs, rhs) + | Bvsge(lhs, rhs) + | Bvugt(lhs, rhs) + | Bvsgt(lhs, rhs) + | Bvshl(lhs, rhs) + | Bvlshr(lhs, rhs) + | Bvashr(lhs, rhs) + | Concat(lhs, rhs) + | FPBinary(_, lhs, rhs) => { + let lhs_uses = exp_uses(lhs); + let rhs_uses = exp_uses(rhs); + &lhs_uses | &rhs_uses + } + Ite(cond, then_exp, else_exp) => { + let cond_uses = exp_uses(cond); + let then_uses = exp_uses(then_exp); + let else_uses = exp_uses(else_exp); + let uses = &cond_uses | &then_uses; + &uses | &else_uses + } + //App(f, args) => { + // uses.insert(*f, uses.get(f).unwrap_or(&0) + 1); + // for arg in args { + // uses_in_exp(uses, arg); + // } + //} + //Select(array, index) => { + // uses_in_exp(uses, array); + // uses_in_exp(uses, index) + //} + //Store(array, index, val) => { + // uses_in_exp(uses, array); + // uses_in_exp(uses, index); + // uses_in_exp(uses, val) + //} + //Distinct(exps) => { + // for exp in exps { + // uses_in_exp(uses, exp); + // } + //} + //FPRoundingUnary(_, rm, exp) => { + // uses_in_exp(uses, rm); + // uses_in_exp(uses, exp); + //} + //FPRoundingBinary(_, rm, lhs, rhs) => { + // uses_in_exp(uses, rm); + // uses_in_exp(uses, lhs); + // uses_in_exp(uses, rhs) + //} + //FPfma(rm, x, y, z) => { + // uses_in_exp(uses, rm); + // uses_in_exp(uses, x); + // uses_in_exp(uses, y); + // uses_in_exp(uses, z) + //} + _ => todo!("not yet implemented expression: {:?}", exp), + } +} + +fn smt_def_uses(def: &smtlib::Def) -> HashSet { + match def { + // DeclareConst(Sym, Ty), + // DeclareFun(Sym, Vec, Ty), + smtlib::Def::DefineConst(_, exp) => exp_uses(&exp), + // DefineEnum(Name, usize), + // Assert(Exp), + _ => HashSet::new(), + } +} + +fn val_uses(val: &Val) -> HashSet { + // See: simplify::uses_in_value + use Val::*; + match val { + Symbolic(sym) => HashSet::from([*sym]), + // MixedBits(segments) => segments.iter().for_each(|segment| match segment { + // BitsSegment::Symbolic(v) => { + // uses.insert(*v, uses.get(v).unwrap_or(&0) + 1); + // } + // BitsSegment::Concrete(_) => (), + // }), + I64(_) | I128(_) | Bool(_) | Bits(_) | Enum(_) | String(_) | Unit | Ref(_) | Poison => { + HashSet::new() + } + // List(vals) | Vector(vals) => vals.iter().for_each(|val| uses_in_value(uses, val)), + Struct(fields) => fields + .iter() + .map(|(_, val)| val_uses(val)) + .fold(HashSet::new(), |acc, uses| &acc | &uses), + // Ctor(_, val) => uses_in_value(uses, val), + // SymbolicCtor(v, possibilities) => { + // uses.insert(*v, uses.get(v).unwrap_or(&0) + 1); + // possibilities + // .iter() + // .for_each(|(_, val)| uses_in_value(uses, val)) + // } + _ => todo!("not yet implemented value: {:?}", val), + } +} + +fn uses(event: &Event) -> HashSet { + match event { + Event::Smt(def, _, _) => smt_def_uses(&def), + Event::WriteReg(_, _, val) => val_uses(val), + _ => HashSet::new(), + } +} + +fn tree_shake(events: &Vec>) -> Vec> { + // Definitions. + let defn_idx = defns(events); + + // Work list: populate with register writes. + let mut work_list = Vec::new(); + let mut live = HashSet::new(); + for (i, event) in events.iter().enumerate() { + match event { + Event::WriteReg(_, _, val) => val_uses(val).iter().for_each(|sym| { + // Mark live. + live.insert(i); + + // Push the variable to be visited. + let d = defn_idx[&sym]; + live.insert(d); + work_list.push(d); + }), + _ => continue, + }; + } + + // Process. + while !work_list.is_empty() { + let i = work_list.pop().unwrap(); + assert!(live.contains(&i), "visited events should be live"); + let event = &events[i]; + + // Mark uses live. + for u in uses(&event) { + // Lookup definition of this dependency. + assert!(defn_idx.contains_key(&u), "no definition for {:?}", u); + let ui = defn_idx[&u]; + if live.contains(&ui) { + continue; + } + + live.insert(ui); + work_list.push(ui); + } + } + + // Filter down to live events. + let mut events: Vec<_> = events + .iter() + .enumerate() + .filter_map(|(i, event)| if live.contains(&i) { Some(event) } else { None }) + .cloned() + .collect(); + + // Simplify pass. + events.reverse(); + simplify::propagate_forwards_used_once(&mut events); + events.reverse(); + + events +} + +fn write_events<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result<()> { + // Print. + let stdout = std::io::stdout(); + let mut handle = BufWriter::with_capacity(5 * usize::pow(2, 20), stdout.lock()); + let write_opts = WriteOpts::default(); + simplify::write_events_with_opts(&mut handle, &events, &iarch.shared_state, &write_opts) + .unwrap(); + handle.flush().unwrap(); + + Ok(()) +} + +#[derive(Clone)] +struct Conditions { + requires: Vec, + provides: Vec, +} + +impl Conditions { + fn new() -> Self { + Self { + requires: Vec::new(), + provides: Vec::new(), + } + } + + fn merge(cs: Vec) -> Self { + match cs.len() { + 0 => Self::new(), + 1 => cs[0].clone(), + _ => Self { + requires: vec![spec_or( + cs.iter().map(|c| spec_and(c.requires.clone())).collect(), + )], + provides: cs + .iter() + .map(|c| { + spec_binary( + SpecOp::Imp, + spec_and(c.requires.clone()), + spec_and(c.provides.clone()), + ) + }) + .collect(), + }, + } + } +} + +#[derive(Debug, Clone)] +struct SpecConfig { + term: String, + args: Vec, + cases: Vec, +} + +#[derive(Debug, Clone)] +struct InstConfig { + inst: Inst, + require: Vec, + reg_read: HashMap, + reg_write: HashMap, +} + +struct SpecConverter<'ir, B: BV> { + cfgs: Vec, + iarch: &'ir Initialized<'ir, B>, +} + +impl<'ir, B: BV> SpecConverter<'ir, B> { + fn new(cfgs: Vec, iarch: &'ir Initialized<'ir, B>) -> Self { + Self { + cfgs: cfgs.clone(), + iarch, + } + } + + fn generate(&self) -> anyhow::Result { + let defs: Vec = self + .cfgs + .iter() + .map(|cfg| Ok(Def::Spec(self.spec(cfg)?))) + .collect::>()?; + + Ok(Defs { + defs, + filenames: vec![], + file_texts: vec![], + }) + } + + fn spec(&self, cfg: &SpecConfig) -> anyhow::Result { + // Derive conditions for each case. + let conds: Vec = cfg + .cases + .iter() + .enumerate() + .map(|(i, c)| self.case(i, c)) + .collect::>()?; + let mut cond = Conditions::merge(conds); + + // Assert the result is fixed 1-bit vector. + // TODO(mbm): decide on verification model for MInst, or explicitly model as void or Unit + cond.provides.insert( + 0, + spec_eq(spec_var("result".to_string()), spec_const_bit_vector(1, 1)), + ); + + let spec = Spec { + term: spec_ident(cfg.term.clone()), + args: cfg.args.iter().cloned().map(spec_ident).collect(), + requires: cond.requires, + provides: cond.provides, + }; + + Ok(spec) + } + + fn case(&self, i: usize, case: &InstConfig) -> anyhow::Result { + let mut converter = TraceConverter::new(case.clone(), &self.iarch); + converter.set_var_prefix(format!("v{i}_")); + let conds = converter.convert()?; + Ok(conds) + } +} + +struct TraceConverter<'ir, B: BV> { + cfg: InstConfig, + iarch: &'ir Initialized<'ir, B>, + var_prefix: String, + + // Keep track of registers read and written in the trace. + reg_reads: HashSet, + reg_writes: HashSet, + + // Types of SMT variables and functions. Required for ISLA type inference. + ty: HashMap, + funty: HashMap, smtlib::Ty)>, +} + +impl<'ir, B: BV> TraceConverter<'ir, B> { + fn new(cfg: InstConfig, iarch: &'ir Initialized<'ir, B>) -> Self { + Self { + cfg: cfg.clone(), + iarch, + var_prefix: "v".to_string(), + + reg_reads: HashSet::new(), + reg_writes: HashSet::new(), + ty: HashMap::new(), + funty: HashMap::new(), + } + } + + fn set_var_prefix(&mut self, prefix: String) { + self.var_prefix = prefix; + } + + fn convert(&mut self) -> anyhow::Result { + let inst = &self.cfg.inst; + + // Assemble instruction. + let opcodes = opcodes(inst); + assert_eq!(opcodes.len(), 1); + let opcode = opcodes[0]; + + // Debugging. + let asm = + inst.print_with_state(&mut EmitState::default(), &mut AllocationConsumer::new(&[])); + + println!("inst = {inst:#?}"); + println!("opcode = {opcode:08x}"); + println!("asm = {asm}"); + println!("----"); + + // ISLA trace. + let paths = trace_opcode(opcode, &self.iarch)?; + + // TODO(mbm): handle multiple paths + assert_eq!(paths.len(), 1); + let events = &paths[0]; + + // Debugging. + write_events(events, self.iarch)?; + println!("--------------------------------------------------"); + + // Filter. + let events = tree_shake(events); + + // Convert into conditions. + let mut conds = Conditions { + provides: Vec::new(), + requires: self.cfg.require.clone(), + }; + + for event in events { + if let Some(exp) = self.event(&event)? { + conds.provides.push(exp); + } + } + + Ok(conds) + } + + fn event(&mut self, event: &Event) -> anyhow::Result> { + match event { + Event::Smt(def, attr, ..) if !attr.is_uninteresting() => self.smt(def), + + Event::ReadReg(name, acc, val) => { + if !acc.is_empty() { + anyhow::bail!("register read accessors unimplemented"); + } + + if let Val::Symbolic(sym) = val { + self.read_reg(name, sym) + } else { + anyhow::bail!("non-symbolic register reads are unimplemented"); + } + } + + Event::WriteReg(name, acc, val) => { + if !acc.is_empty() { + anyhow::bail!("register write accessors unimplemented"); + } + + if let Val::Symbolic(sym) = val { + self.write_reg(name, sym) + } else { + anyhow::bail!("non-symbolic register writes are unimplemented"); + } + } + + _ => anyhow::bail!("unsupported event type: {:?}", event), + } + } + + fn read_reg(&mut self, name: &Name, sym: &Sym) -> anyhow::Result> { + // Map to a string name. + let reg = self.lookup_name(name); + + // Expect to find a configured mapping for this register read. + let mapped_var = match self.cfg.reg_read.get(®) { + Some(v) => v.clone(), + None => anyhow::bail!("no mapping for read of register {}", reg), + }; + + // Expect register to be read only once. + if self.reg_reads.contains(®) { + anyhow::bail!("multiple reads of register {}", reg); + } + self.reg_reads.insert(reg.clone()); + + // Emit expression binding the ISLA variable to mapped ISLE term. + Ok(Some(spec_eq(spec_var(mapped_var), self.sym(sym)))) + } + + fn write_reg(&mut self, name: &Name, sym: &Sym) -> anyhow::Result> { + // Map to a string name. + let reg = self.lookup_name(name); + + // Expect to find a configured mapping for this register write. + let mapped_var = match self.cfg.reg_write.get(®) { + Some(v) => v.clone(), + None => anyhow::bail!("no mapping for write of register {}", reg), + }; + + // Expect register to be written only once. + if self.reg_writes.contains(®) { + anyhow::bail!("multiple writes of register {}", reg); + } + self.reg_writes.insert(reg.clone()); + + // Emit expression binding the ISLA variable to mapped ISLE term. + Ok(Some(spec_eq(spec_var(mapped_var), self.sym(sym)))) + } + + fn smt(&mut self, def: &smtlib::Def) -> anyhow::Result> { + match def { + smtlib::Def::DefineConst(v, exp) => { + let ty = self.infer(exp).expect("SMT expression was badly-typed"); + self.ty.insert(*v, ty.clone()); + + Ok(Some(spec_eq(self.sym(v), self.exp(exp)))) + } + + smtlib::Def::DeclareConst(v, ty) => { + self.ty.insert(*v, ty.clone()); + Ok(None) + } + + smtlib::Def::DeclareFun(v, params, ret) => { + self.funty.insert(*v, (params.clone(), ret.clone())); + Ok(None) + } + + smtlib::Def::DefineEnum(..) => Ok(None), + + _ => anyhow::bail!("unsupported smt def: {:?}", def), + } + } + + fn exp(&self, exp: &smtlib::Exp) -> SpecExpr { + use smtlib::Exp::*; + match exp { + Var(v) => self.sym(v), + Bits(bits) => spec_bits(bits), + Bits64(bv) => spec_const_bit_vector( + bv.lower_u64().try_into().unwrap(), + bv.len().try_into().unwrap(), + ), + // Enum(EnumMember), + Bool(b) => spec_const_bool(*b), + // Neq(Box>, Box>), + Not(x) | Bvnot(x) => spec_unary(exp_spec_op(exp), self.exp(x)), + + // Bvnot(Box>), + // Bvnand(Box>, Box>), + // Bvnor(Box>, Box>), + // Bvxnor(Box>, Box>), + // Bvneg(Box>), + Eq(lhs, rhs) + | And(lhs, rhs) + | Or(lhs, rhs) + | Bvand(lhs, rhs) + | Bvor(lhs, rhs) + | Bvxor(lhs, rhs) + | Bvadd(lhs, rhs) + | Bvsub(lhs, rhs) + | Bvmul(lhs, rhs) + | Bvshl(lhs, rhs) + | Bvlshr(lhs, rhs) + // Bvudiv(Box>, Box>), + // Bvsdiv(Box>, Box>), + // Bvurem(Box>, Box>), + | Bvsrem(lhs, rhs) + // Bvsmod(Box>, Box>), + // Bvult(Box>, Box>), + | Bvslt(lhs, rhs) + // Bvule(Box>, Box>), + // Bvsle(Box>, Box>), + // Bvuge(Box>, Box>), + // Bvsge(Box>, Box>), + // Bvugt(Box>, Box>), + // Bvsgt(Box>, Box>), + // Bvlshr(Box>, Box>), + | Bvashr(lhs, rhs) + | Concat(lhs, rhs) => spec_binary(exp_spec_op(exp), self.exp(lhs), self.exp(rhs)), + + // TODO: elide no-op extract ops for example (extract 63 0 x) for a 64-bit x + Extract(i, j, exp) => spec_ternary( + SpecOp::Extract, + spec_const_int(*i), + spec_const_int(*j), + self.exp(exp), + ), + + ZeroExtend(0, x) | SignExtend(0, x) => self.exp(x), + ZeroExtend(n, x) | SignExtend(n, x) => match self.infer(x).unwrap() { + smtlib::Ty::BitVec(w) => { + spec_binary(exp_spec_op(exp), spec_const_int(n + w), self.exp(x)) + } + _ => panic!("extension applies to bitvector types"), + } + + Ite(c, t, e) => spec_ternary(SpecOp::If, self.exp(c), self.exp(t), self.exp(e)), + + // App(Sym, Vec>), + // Select(Box>, Box>), + // Store(Box>, Box>, Box>), + // Distinct(Vec>), + // FPConstant(FPConstant, u32, u32), + // FPRoundingMode(FPRoundingMode), + // FPUnary(FPUnary, Box>), + // FPRoundingUnary(FPRoundingUnary, Box>, Box>), + // FPBinary(FPBinary, Box>, Box>), + // FPRoundingBinary(FPRoundingBinary, Box>, Box>, Box>), + // FPfma(Box>, Box>, Box>, Box>), + _ => todo!("expression: {:?}", exp), + } + } + + fn sym(&self, s: &Sym) -> SpecExpr { + spec_var(format!("{}{}", self.var_prefix, s)) + } + + fn infer(&self, exp: &smtlib::Exp) -> Option { + exp.infer(&self.ty, &self.funty) + } + + fn lookup_name(&self, name: &Name) -> String { + zencode::decode(self.iarch.shared_state.symtab.to_str(name.clone())) + } +} + +fn exp_spec_op(exp: &smtlib::Exp) -> SpecOp { + use smtlib::Exp::*; + match exp { + // Bits(Vec), + // Bits64(B64), + // Enum(EnumMember), + // Bool(bool), + Eq(..) => SpecOp::Eq, + // Neq(Box>, Box>), + And(..) => SpecOp::And, + Or(..) => SpecOp::Or, + Not(..) => SpecOp::Not, + Bvnot(..) => SpecOp::BVNot, + Bvand(..) => SpecOp::BVAnd, + Bvor(..) => SpecOp::BVOr, + Bvxor(..) => SpecOp::BVXor, + // Bvnand(Box>, Box>), + // Bvnor(Box>, Box>), + // Bvxnor(Box>, Box>), + // Bvneg(Box>), + Bvadd(..) => SpecOp::BVAdd, + Bvsub(..) => SpecOp::BVSub, + Bvmul(..) => SpecOp::BVMul, + // Bvudiv(Box>, Box>), + // Bvsdiv(Box>, Box>), + // Bvurem(Box>, Box>), + Bvsrem(..) => SpecOp::BVSrem, + // Bvsmod(Box>, Box>), + // Bvult(Box>, Box>), + Bvslt(..) => SpecOp::BVSlt, + // Bvule(Box>, Box>), + // Bvsle(Box>, Box>), + // Bvuge(Box>, Box>), + // Bvsge(Box>, Box>), + // Bvugt(Box>, Box>), + // Bvsgt(Box>, Box>), + ZeroExtend(..) => SpecOp::ZeroExt, + SignExtend(..) => SpecOp::SignExt, + Bvshl(..) => SpecOp::BVShl, + Bvlshr(..) => SpecOp::BVLshr, + Bvashr(..) => SpecOp::BVAshr, + Concat(..) => SpecOp::Concat, + // Ite(Box>, Box>, Box>), + // App(Sym, Vec>), + // Select(Box>, Box>), + // Store(Box>, Box>, Box>), + // Distinct(Vec>), + // FPConstant(FPConstant, u32, u32), + // FPRoundingMode(FPRoundingMode), + // FPUnary(FPUnary, Box>), + // FPRoundingUnary(FPRoundingUnary, Box>, Box>), + // FPBinary(FPBinary, Box>, Box>), + // FPRoundingBinary(FPRoundingBinary, Box>, Box>, Box>), + // FPfma(Box>, Box>, Box>, Box>), + _ => todo!("spec op: {:?}", exp), + } +} + +fn spec_const_int(x: I) -> SpecExpr +where + i128: From, +{ + SpecExpr::ConstInt { + val: x.try_into().unwrap(), + pos: Pos::default(), + } +} + +fn spec_const_bool(b: bool) -> SpecExpr { + SpecExpr::ConstBool { + val: if b { 1 } else { 0 }, + pos: Pos::default(), + } +} + +fn spec_const_bit_vector(val: i128, width: i8) -> SpecExpr { + assert!(width >= 0); + SpecExpr::ConstBitVec { + val, + width, + pos: Pos::default(), + } +} + +fn spec_bits(bits: &[bool]) -> SpecExpr { + // TODO(mbm): verify endianness assumption about Vec and test multi-chunk case + bits.chunks(64) + .map(|chunk| { + let mut val: i128 = 0; + for (i, bit) in chunk.iter().enumerate() { + if *bit { + val |= 1 << i; + } + } + spec_const_bit_vector(val, 64) + }) + .rev() + .reduce(|acc, bv| spec_binary(SpecOp::Concat, acc, bv)) + .unwrap() +} + +fn spec_and(args: Vec) -> SpecExpr { + spec_op(SpecOp::And, args) +} + +fn spec_or(args: Vec) -> SpecExpr { + spec_op(SpecOp::Or, args) +} + +fn spec_unary(op: SpecOp, x: SpecExpr) -> SpecExpr { + spec_op(op, vec![x]) +} + +fn spec_binary(op: SpecOp, x: SpecExpr, y: SpecExpr) -> SpecExpr { + spec_op(op, vec![x, y]) +} + +fn spec_eq(x: SpecExpr, y: SpecExpr) -> SpecExpr { + spec_binary(SpecOp::Eq, x, y) +} + +fn spec_ternary(op: SpecOp, x: SpecExpr, y: SpecExpr, z: SpecExpr) -> SpecExpr { + spec_op(op, vec![x, y, z]) +} + +fn spec_op(op: SpecOp, args: Vec) -> SpecExpr { + SpecExpr::Op { + op, + args: args, + pos: Pos::default(), + } +} + +fn spec_enum(name: String, variant: String) -> SpecExpr { + SpecExpr::Enum { + name: spec_ident(format!("{}.{}", name, variant)), + } +} + +fn spec_var(id: String) -> SpecExpr { + SpecExpr::Var { + var: spec_ident(id), + pos: Pos::default(), + } +} + +fn spec_ident(id: String) -> Ident { + Ident(id, Pos::default()) +} diff --git a/cranelift/isle/veri/veri_engine/src/bin/specfunc.rs b/cranelift/isle/veri/veri_engine/src/bin/specfunc.rs new file mode 100644 index 000000000000..608e2fab5f5f --- /dev/null +++ b/cranelift/isle/veri/veri_engine/src/bin/specfunc.rs @@ -0,0 +1,194 @@ +use crossbeam::queue::SegQueue; +use isla::opts; +use isla_lib::bitvector::{b64::B64, BV}; +use isla_lib::error::IslaError; +use isla_lib::executor::{self, LocalFrame, TaskState}; +use isla_lib::init::{initialize_architecture, Initialized}; +use isla_lib::ir::{AssertionMode, Val}; +use isla_lib::memory::Memory; +use isla_lib::simplify::{self, WriteOpts}; +use isla_lib::smt::{self, Checkpoint, Event, Solver}; +use isla_lib::zencode; +use sha2::{Digest, Sha256}; +use std::io::prelude::*; +use std::io::BufWriter; +use std::path::PathBuf; +use std::sync::Arc; + +fn main() -> anyhow::Result<()> { + // Command-line options. + let opts = opts::common_opts(); + + // Build ISLA architecture. + let mut hasher = Sha256::new(); + let (matches, arch) = opts::parse::(&mut hasher, &opts); + let opts::CommonOpts { + num_threads: _, + mut arch, + symtab, + type_info, + isa_config, + source_path: _, + } = opts::parse_with_arch(&mut hasher, &opts, &matches, &arch); + let use_model_reg_init = true; + let iarch = initialize_architecture( + &mut arch, + symtab, + type_info, + &isa_config, + AssertionMode::Optimistic, + use_model_reg_init, + ); + + // ISLA trace. + let paths = trace_execute_function(&iarch)?; + + // Dump. + for events in paths { + write_events_to_stdout(&events, &iarch)?; + } + + Ok(()) +} + +fn trace_execute_function<'ir, B: BV>( + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result>>> { + let shared_state = &&iarch.shared_state; + + let initial_checkpoint = Checkpoint::new(); + let solver_cfg = smt::Config::new(); + let solver_ctx = smt::Context::new(solver_cfg); + let mut solver = Solver::from_checkpoint(&solver_ctx, initial_checkpoint); + let checkpoint = smt::checkpoint(&mut solver); + + // // val execute_aarch64_instrs_integer_conditional_compare_register : forall 'datasize 'm 'n ('sub_op : Bool), + // // (0 <= 'n & 'n <= 31 & 0 <= 'm & 'm <= 31 & 'datasize in {32, 64}). + // // (bits(4), int('datasize), bits(4), int('m), int('n), bool('sub_op)) -> unit + // // function execute_aarch64_instrs_integer_conditional_compare_register (condition, datasize, flags__arg, m, n, sub_op) = { + + // let execute_function = + // zencode::encode("execute_aarch64_instrs_integer_conditional_compare_register"); + // // condition: bits(4) + // let condition = Val::Bits(B::new(7, 4)); + // // datasize: int('datasize) + // let datasize = Val::I64(64); + // // flags__arg + // let flags_arg = Val::Bits(B::new(3, 4)); + // // m + // let rm = Val::I64(3); + // // n + // let rn = Val::I64(4); + // // sub_op + // let sub_op = Val::Bool(false); + + // val execute_aarch64_instrs_integer_arithmetic_add_sub_carry : forall 'd 'datasize 'm 'n ('setflags : Bool) ('sub_op : Bool), + // (0 <= 'n & 'n <= 31 & 0 <= 'm & 'm <= 31 & 'datasize in {32, 64} & 0 <= 'd & 'd <= 31). + // (int('d), int('datasize), int('m), int('n), bool('setflags), bool('sub_op)) -> unit + // + // function execute_aarch64_instrs_integer_arithmetic_add_sub_carry (d, datasize, m, n, setflags, sub_op) = { + + let execute_function = + zencode::encode("execute_aarch64_instrs_integer_arithmetic_add_sub_carry"); + // d + let rd = Val::I64(2); + // datasize + let datasize = Val::I64(64); + // m + let rm = Val::I64(3); + // n + let rn = Val::I64(4); + // setflags + let setflags = Val::Bool(true); + // sub_op + let sub_op = Val::Bool(false); + + let function_id = shared_state.symtab.lookup(&execute_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + let memory = Memory::new(); + let task_state = TaskState::::new(); + let task = LocalFrame::new( + function_id, + args, + ret_ty, + Some(&[rd, datasize, rm, rn, setflags, sub_op]), + instrs, + ) + .add_lets(&iarch.lets) + .add_regs(&iarch.regs) + .set_memory(memory) + .task_with_checkpoint(0, &task_state, checkpoint); + + let num_threads = 1; + let queue = Arc::new(SegQueue::new()); + executor::start_multi( + num_threads, + None, + vec![task], + shared_state, + queue.clone(), + &executor::trace_collector, + ); + + let mut paths = Vec::new(); + loop { + match queue.pop() { + Some(Ok((_, mut events))) => { + //simplify::hide_initialization(&mut events); + simplify::remove_extra_register_fields(&mut events); + simplify::remove_repeated_register_reads(&mut events); + simplify::remove_unused_register_assumptions(&mut events); + simplify::remove_unused(&mut events); + simplify::propagate_forwards_used_once(&mut events); + simplify::commute_extract(&mut events); + simplify::eval(&mut events); + + let events: Vec> = events.drain(..).rev().collect(); + paths.push(events); + } + + // Error during execution + Some(Err(err)) => { + let msg = format!("{}", err); + eprintln!( + "{}", + err.source_loc().message::( + None, + shared_state.symtab.files(), + &msg, + true, + true + ) + ); + anyhow::bail!("{}", err); + } + // Empty queue + None => break, + } + } + + Ok(paths) +} + +/// Write ISLA trace events to stdout. +fn write_events_to_stdout<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result<()> { + let stdout = std::io::stdout().lock(); + write_events(events, iarch, stdout) +} + +fn write_events<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, + w: impl Sized + Write, +) -> anyhow::Result<()> { + let mut handle = BufWriter::with_capacity(5 * usize::pow(2, 20), w); + let write_opts = WriteOpts::default(); + simplify::write_events_with_opts(&mut handle, &events, &iarch.shared_state, &write_opts) + .unwrap(); + handle.flush().unwrap(); + + Ok(()) +} diff --git a/cranelift/isle/veri/veri_engine/src/bin/x64footprint.rs b/cranelift/isle/veri/veri_engine/src/bin/x64footprint.rs new file mode 100644 index 000000000000..17d58b8c9416 --- /dev/null +++ b/cranelift/isle/veri/veri_engine/src/bin/x64footprint.rs @@ -0,0 +1,545 @@ +use clap::Parser; +use crossbeam::queue::SegQueue; +use isla_lib::init::{initialize_architecture, Initialized}; +use isla_lib::ir::{AssertionMode, Def, IRTypeInfo, Name, Symtab, Ty, Val}; +use isla_lib::ir_lexer::new_ir_lexer; +use isla_lib::ir_parser; +use isla_lib::log; +use isla_lib::memory::{Memory, SmtKind}; +use isla_lib::simplify::{self, WriteOpts}; +use isla_lib::smt::smtlib::{self, bits64}; +use isla_lib::smt::{self, Checkpoint, Event, ReadOpts, Solver, Sym}; +use isla_lib::source_loc::SourceLoc; +use isla_lib::{ + bitvector::{b64::B64, BV}, + zencode, +}; +use isla_lib::{config::ISAConfig, executor::unfreeze_frame}; +use isla_lib::{ + error::{ExecError, IslaError}, + memory::Address, +}; +use isla_lib::{ + executor::{self, freeze_frame, LocalFrame, TaskState}, + ir::linearize, +}; +use sha2::{Digest, Sha256}; +use std::io::prelude::*; +use std::io::BufWriter; +use std::path::PathBuf; +use std::sync::Arc; + +#[derive(Parser)] +struct Options { + /// Architecture definition. + #[clap(long)] + arch: PathBuf, + + /// ISA config file. + #[clap(long)] + isa_config: PathBuf, + + /// Trace output directory. + #[clap(long, default_value = ".")] + output_dir: PathBuf, +} + +fn main() -> anyhow::Result<()> { + let options = Options::parse(); + log::set_flags(log::VERBOSE); + + // Parse ISLA Architecture. + let contents = std::fs::read_to_string(&options.arch)?; + let mut symtab = Symtab::new(); + let mut arch = parse_ir::(&contents, &mut symtab)?; + + // ISLA ISA Config. + let mut hasher = Sha256::new(); + let type_info = IRTypeInfo::new(&arch); + let isa_config = match ISAConfig::::from_file( + &mut hasher, + &options.isa_config, + None, + &symtab, + &type_info, + ) { + Ok(isa_config) => isa_config, + Err(msg) => anyhow::bail!(msg), + }; + + let linearize_functions = vec![ + // See: https://github.com/rems-project/isla-testgen/blob/a9759247bfdff9c9c39d95a4cfd85318e5bf50fe/c86-command + //"fdiv_int", + "bool_to_bits", + "bits_to_bool", + //"bit_to_bool", + //"isEven", + "signed_byte_p_int", + "zf_spec", + //"b_xor", + //"logand_int", + //"not_bit", + //"floor2", + ]; + for name in linearize_functions { + linearize_function(&mut arch, name, &mut symtab)?; + } + + let use_model_reg_init = true; + let iarch = initialize_architecture( + &mut arch, + symtab, + type_info, + &isa_config, + AssertionMode::Optimistic, + use_model_reg_init, + ); + + // Setup machine code. + let machine_code = vec![0x4c, 0x01, 0xea]; + println!("machine code = {:02x?}", machine_code); + + // ISLA trace. + let paths = trace_opcode(&machine_code, &iarch)?; + + // Dump. + for (i, events) in paths.iter().enumerate() { + let filename = format!("trace{i:04}.out"); + let path = options.output_dir.join(filename); + log!(log::VERBOSE, format!("write trace to {}", path.display())); + + let file = std::fs::File::create(path)?; + write_events(&events, &iarch, file)?; + } + + log!( + log::VERBOSE, + format!("generated {} trace paths", paths.len()) + ); + + Ok(()) +} + +fn trace_opcode<'ir, B: BV>( + opcode: &Vec, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result>>> { + let shared_state = &&iarch.shared_state; + let symtab = &shared_state.symtab; + + let initial_checkpoint = Checkpoint::new(); + let solver_cfg = smt::Config::new(); + let solver_ctx = smt::Context::new(solver_cfg); + let mut solver = Solver::from_checkpoint(&solver_ctx, initial_checkpoint); + let memory = Memory::new(); + + // Initialization ----------------------------------------------------------- + // - run initialization function to set processor in 64-bit mode + + let init_function = zencode::encode("initialise_64_bit_mode"); + let function_id = shared_state.symtab.lookup(&init_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + + let task_state = TaskState::::new(); + let checkpoint = smt::checkpoint(&mut solver); + let task = LocalFrame::new(function_id, args, ret_ty, None, instrs) + .add_lets(&iarch.lets) + .add_regs(&iarch.regs) + .set_memory(memory) + .task_with_checkpoint(0, &task_state, checkpoint); + + let queue = Arc::new(SegQueue::new()); + executor::start_single( + task, + &shared_state, + &queue, + &move |_tid, _task_id, result, _shared_state, mut solver, queue| match result { + Ok((_, frame)) => { + queue.push((freeze_frame(&frame), smt::checkpoint(&mut solver))); + } + Err(err) => panic!("Initialisation failed: {:?}", err), + }, + ); + assert_eq!(queue.len(), 1); + let (frame, checkpoint) = queue.pop().expect("pop failed"); + + let mut solver = Solver::from_checkpoint(&solver_ctx, checkpoint); + + // Initialize registers ----------------------------------------------------- + // - set symbolic values for all general-purpose registers + + let mut local_frame = executor::unfreeze_frame(&frame); + for (n, ty) in &shared_state.registers { + // Only handle general-purpose registers. + if let Ty::Bits(bits) = ty { + let var = solver.fresh(); + solver.add(smtlib::Def::DeclareConst(var, smtlib::Ty::BitVec(*bits))); + let val = Val::Symbolic(var); + local_frame.regs_mut().assign(*n, val, shared_state); + } + } + + let frame = freeze_frame(&local_frame); + + // Setup memory ------------------------------------------------------------- + + let mut local_frame = unfreeze_frame(&frame); + + const INIT_PC: Address = 0x401000; + local_frame + .memory_mut() + .add_symbolic_code_region(INIT_PC..INIT_PC + 0x10000); + + let memory_var = solver.fresh(); + solver.add(smtlib::Def::DeclareConst( + memory_var, + smtlib::Ty::Array( + Box::new(smtlib::Ty::BitVec(64)), + Box::new(smtlib::Ty::BitVec(8)), + ), + )); + + let memory_client_info: Box> = + Box::new(SeqMemory { memory_var }); + local_frame.memory_mut().set_client_info(memory_client_info); + + let frame = freeze_frame(&local_frame); + + // Set initial program counter ---------------------------------------------- + + let local_frame = unfreeze_frame(&frame); + + let pc_name = zencode::encode("rip"); + let pc_id = symtab.lookup(&pc_name); + let pc = local_frame.regs().get_last_if_initialized(pc_id).unwrap(); + + solver.add(smtlib::Def::Assert(smtlib::Exp::Eq( + Box::new(smt_value(pc).unwrap()), + Box::new(smtlib::Exp::Bits64(B64::from_u64(INIT_PC))), + ))); + + let frame = freeze_frame(&local_frame); + + // Setup opcode ------------------------------------------------------------- + + let local_frame = unfreeze_frame(&frame); + + let read_val = local_frame + .memory() + .read( + Val::Unit, /* read_kind */ + pc.clone(), + Val::I128(opcode.len() as i128), + &mut solver, + false, + ReadOpts::ifetch(), + ) + .unwrap(); + + let opcode_var = solver.fresh(); + solver.add(smtlib::Def::DeclareConst( + opcode_var, + smtlib::Ty::BitVec(8 * opcode.len() as u32), + )); + solver.add(smtlib::Def::Assert(smtlib::Exp::Eq( + Box::new(smtlib::Exp::Var(opcode_var)), + Box::new(smt_bytes(opcode)), + ))); + + let read_exp = smt_value(&read_val).unwrap(); + solver.add(smtlib::Def::Assert(smtlib::Exp::Eq( + Box::new(smtlib::Exp::Var(opcode_var)), + Box::new(read_exp), + ))); + + let frame = freeze_frame(&local_frame); + + // Debug dump --------------------------------------------------------------- + + assert_eq!(solver.check_sat(), smt::SmtResult::Sat); + let checkpoint = smt::checkpoint(&mut solver); + dump_checkpoint(&checkpoint, iarch)?; + + // Execute fetch and decode ------------------------------------------------- + + let local_frame = unfreeze_frame(&frame); + + local_frame.memory().log(); + + let run_instruction_function = zencode::encode("x86_fetch_decode_execute"); + let function_id = shared_state.symtab.lookup(&run_instruction_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + + let task_state = TaskState::::new(); + let task = local_frame + .new_call(function_id, args, ret_ty, None, instrs) + .task_with_checkpoint(1, &task_state, checkpoint); + + let num_threads = 1; + let queue = Arc::new(SegQueue::new()); + executor::start_multi( + num_threads, + None, + vec![task], + shared_state, + queue.clone(), + &executor::trace_collector, + ); + + let mut paths = Vec::new(); + loop { + match queue.pop() { + Some(Ok((_, mut events))) => { + // simplify::hide_initialization(&mut events); + simplify::remove_extra_register_fields(&mut events); + simplify::remove_repeated_register_reads(&mut events); + simplify::remove_unused_register_assumptions(&mut events); + simplify::remove_unused(&mut events); + simplify::propagate_forwards_used_once(&mut events); + simplify::commute_extract(&mut events); + simplify::eval(&mut events); + + let events: Vec> = events.drain(..).rev().collect(); + paths.push(events); + } + + // Error during execution + Some(Err(err)) => { + let msg = format!("{}", err); + eprintln!( + "{}", + err.source_loc().message::( + None, + shared_state.symtab.files(), + &msg, + true, + true + ) + ); + anyhow::bail!("{}", err); + } + // Empty queue + None => break, + } + } + + Ok(paths) +} + +#[derive(Debug, Clone)] +struct SeqMemory { + memory_var: Sym, +} + +impl isla_lib::memory::MemoryCallbacks for SeqMemory { + fn symbolic_read( + &self, + regions: &[isla_lib::memory::Region], + solver: &mut Solver, + value: &Val, + _read_kind: &Val, + address: &Val, + bytes: u32, + _tag: &Option>, + opts: &ReadOpts, + ) { + use isla_lib::smt::smtlib::{Def, Exp}; + + let read_exp = smt_value(value) + .unwrap_or_else(|err| panic!("Bad memory read value {:?}: {}", value, err)); + let addr_exp = smt_value(address) + .unwrap_or_else(|err| panic!("Bad read address value {:?}: {}", address, err)); + let read_prop = Exp::Eq( + Box::new(read_exp.clone()), + Box::new(smt_read_exp(self.memory_var, &addr_exp, bytes as u64)), + ); + let kind = if opts.is_ifetch { + SmtKind::ReadInstr + } else if opts.is_exclusive { + // We produce a dummy read so that failed store exclusives still get address + // constraints, but the memory must be writable. + SmtKind::WriteData + } else { + SmtKind::ReadData + }; + let address_constraint = + isla_lib::memory::smt_address_constraint(regions, &addr_exp, bytes, kind, solver, None); + + let full_constraint = Exp::And(Box::new(address_constraint), Box::new(read_prop)); + + solver.add(Def::Assert(full_constraint)); + } + + fn symbolic_write( + &mut self, + regions: &[isla_lib::memory::Region], + solver: &mut Solver, + _value: Sym, + _read_kind: &Val, + address: &Val, + data: &Val, + bytes: u32, + _tag: &Option>, + _opts: &smt::WriteOpts, + ) { + use isla_lib::smt::smtlib::{Def, Exp}; + + let data_exp = smt_value(data) + .unwrap_or_else(|err| panic!("Bad memory write value {:?}: {}", data, err)); + let addr_exp = smt_value(address) + .unwrap_or_else(|err| panic!("Bad write address value {:?}: {}", address, err)); + // TODO: endianness? + let mut mem_exp = Exp::Store( + Box::new(Exp::Var(self.memory_var)), + Box::new(addr_exp.clone()), + Box::new(Exp::Extract(7, 0, Box::new(data_exp.clone()))), + ); + for i in 1..bytes { + mem_exp = Exp::Store( + Box::new(mem_exp), + Box::new(Exp::Bvadd( + Box::new(addr_exp.clone()), + Box::new(bits64(i as u64, 64)), + )), + Box::new(Exp::Extract(i * 8 + 7, i * 8, Box::new(data_exp.clone()))), + ) + } + self.memory_var = solver.fresh(); + solver.add(Def::DefineConst(self.memory_var, mem_exp)); + let kind = SmtKind::WriteData; + let address_constraint = + isla_lib::memory::smt_address_constraint(regions, &addr_exp, bytes, kind, solver, None); + solver.add(Def::Assert(address_constraint)); + } + + fn symbolic_write_tag( + &mut self, + _regions: &[isla_lib::memory::Region], + _solver: &mut Solver, + _value: Sym, + _write_kind: &Val, + _address: &Val, + _tag: &Val, + ) { + } +} + +fn smt_value(v: &Val) -> Result, ExecError> { + isla_lib::primop_util::smt_value(v, SourceLoc::unknown()) +} + +fn smt_read_exp(memory: Sym, addr_exp: &smtlib::Exp, bytes: u64) -> smtlib::Exp { + use smtlib::Exp; + // TODO: endianness? + let mut mem_exp = Exp::Select(Box::new(Exp::Var(memory)), Box::new(addr_exp.clone())); + for i in 1..bytes { + mem_exp = Exp::Concat( + Box::new(Exp::Select( + Box::new(Exp::Var(memory)), + Box::new(Exp::Bvadd( + Box::new(addr_exp.clone()), + Box::new(bits64(i as u64, 64)), + )), + )), + Box::new(mem_exp), + ) + } + mem_exp +} + +fn smt_bytes(bytes: &Vec) -> smtlib::Exp { + let mut bits = Vec::with_capacity(bytes.len() * 8); + for byte in bytes { + for i in 0..8 { + bits.push((byte >> i) & 1 == 1); + } + } + smtlib::Exp::Bits(bits) +} + +fn dump_checkpoint<'ir, B: BV>( + checkpoint: &Checkpoint, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result<()> { + if let Some(trace) = checkpoint.trace() { + let events: Vec> = trace.to_vec().into_iter().cloned().collect(); + write_events_to_stdout(&events, iarch)?; + } + Ok(()) +} + +/// Write ISLA trace events to stdout. +fn write_events_to_stdout<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result<()> { + let stdout = std::io::stdout().lock(); + write_events(events, iarch, stdout) +} + +fn write_events<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, + w: impl Sized + Write, +) -> anyhow::Result<()> { + let mut handle = BufWriter::with_capacity(5 * usize::pow(2, 20), w); + let write_opts = WriteOpts::default(); + simplify::write_events_with_opts(&mut handle, &events, &iarch.shared_state, &write_opts) + .unwrap(); + handle.flush().unwrap(); + + Ok(()) +} + +/// Parse Jib IR. +fn parse_ir<'a, 'input, B: BV>( + contents: &'input str, + symtab: &'a mut Symtab<'input>, +) -> anyhow::Result>> { + match ir_parser::IrParser::new().parse(symtab, new_ir_lexer(&contents)) { + Ok(ir) => Ok(ir), + Err(_) => Err(anyhow::Error::msg("bad")), + } +} + +fn linearize_function<'ir, B: BV>( + arch: &mut Vec>, + name: &str, + symtab: &mut Symtab<'ir>, +) -> anyhow::Result<()> { + log!(log::VERBOSE, format!("linearize function {}", name)); + + // Lookup function name. + let target = match symtab.get(&zencode::encode(name)) { + Some(t) => t, + None => anyhow::bail!("function {} could not be found", name), + }; + + // Find signature. + let (_args, ret) = lookup_signature(arch, target)?; + + // Rewrite. + for def in arch.iter_mut() { + if let Def::Fn(f, _, body) = def { + if *f == target { + let rewritten = linearize::linearize(body.to_vec(), &ret, symtab); + *body = rewritten; + } + } + } + + Ok(()) +} + +fn lookup_signature( + arch: &Vec>, + target: Name, +) -> anyhow::Result<(Vec>, Ty)> { + for def in arch { + match def { + Def::Val(f, args, ret) if *f == target => return Ok((args.clone(), ret.clone())), + _ => (), + } + } + anyhow::bail!("could not find type signature") +} diff --git a/cranelift/isle/veri/veri_engine/src/emit.rs b/cranelift/isle/veri/veri_engine/src/emit.rs new file mode 100644 index 000000000000..60393071120c --- /dev/null +++ b/cranelift/isle/veri/veri_engine/src/emit.rs @@ -0,0 +1,824 @@ +use cranelift_codegen::ir::types::I32; +use cranelift_codegen::isa::aarch64::inst::*; +use cranelift_codegen::settings; +use cranelift_codegen::AllocationConsumer; +use cranelift_codegen::MachBuffer; +use cranelift_codegen::MachInstEmit; +use cranelift_isle::ast::{Ident, Spec, SpecExpr, SpecOp}; +use cranelift_isle::lexer::Pos; +use cranelift_isle::printer; +use crossbeam::queue::SegQueue; +use isla::opts; +use isla_lib::bitvector::{b64::B64, BV}; +use isla_lib::error::IslaError; +use isla_lib::executor::{self, LocalFrame, TaskState}; +use isla_lib::init::{initialize_architecture, Initialized}; +use isla_lib::ir::{AssertionMode, Val}; +use isla_lib::memory::Memory; +use isla_lib::simplify::{self, WriteOpts}; +use isla_lib::smt::smtlib; +use isla_lib::smt::{self, Checkpoint, Event, Solver}; +use sha2::{Digest, Sha256}; +use std::collections::{HashMap, HashSet}; +use std::io::prelude::*; +use std::io::BufWriter; +use std::path::PathBuf; +use std::sync::Arc; + +fn main() -> anyhow::Result<()> { + // Command-line options. + let mut opts = opts::common_opts(); + opts.optflag("", "filter", "filter relevant events from the trace"); + opts.optflag("", "spec", "convert traces to veri-isle specs"); + + // Build ISLA architecture. + let mut hasher = Sha256::new(); + let (matches, arch) = opts::parse::(&mut hasher, &opts); + let opts::CommonOpts { + num_threads: _, + mut arch, + symtab, + type_info, + isa_config, + source_path: _, + } = opts::parse_with_arch(&mut hasher, &opts, &matches, &arch); + let use_model_reg_init = true; + let iarch = initialize_architecture( + &mut arch, + symtab, + type_info, + &isa_config, + AssertionMode::Optimistic, + use_model_reg_init, + ); + + // Assemble and trace instructions. + let insts = vec![ + Inst::AluRRR { + alu_op: ALUOp::Add, + size: OperandSize::Size64, + rd: writable_xreg(4), + rn: xreg(5), + rm: xreg(6), + }, + Inst::AluRRRR { + alu_op: ALUOp3::MSub, + size: OperandSize::Size32, + rd: writable_xreg(1), + rn: xreg(2), + rm: xreg(3), + ra: xreg(4), + }, + Inst::AluRRImmLogic { + alu_op: ALUOp::Eor, + size: OperandSize::Size32, + rd: writable_xreg(1), + rn: xreg(5), + imml: ImmLogic::maybe_from_u64(0x00007fff, I32).unwrap(), + }, + Inst::AluRRRShift { + alu_op: ALUOp::SubS, + size: OperandSize::Size64, + rd: writable_xreg(10), + rn: xreg(11), + rm: xreg(12), + shiftop: ShiftOpAndAmt::new( + ShiftOp::LSL, + ShiftOpShiftImm::maybe_from_shift(23).unwrap(), + ), + }, + Inst::AluRRRExtend { + alu_op: ALUOp::SubS, + size: OperandSize::Size64, + rd: writable_xreg(10), + rn: xreg(11), + rm: xreg(12), + extendop: ExtendOp::UXTX, + }, + // TODO: BitRR + // Inst::BitRR { + // op: BitOp::Rev64, + // size: OperandSize::Size64, + // rd: writable_xreg(1), + // rn: xreg(10), + // }, + Inst::Mov { + size: OperandSize::Size64, + rd: writable_xreg(8), + rm: xreg(9), + }, + Inst::CSel { + rd: writable_xreg(10), + rn: xreg(12), + rm: xreg(14), + cond: Cond::Hs, + }, + Inst::CCmp { + size: OperandSize::Size64, + rn: xreg(22), + rm: xreg(1), + nzcv: NZCV::new(false, false, true, true), + cond: Cond::Eq, + }, + Inst::AluRRImmShift { + alu_op: ALUOp::Lsr, + size: OperandSize::Size64, + rd: writable_xreg(10), + rn: xreg(11), + immshift: ImmShift::maybe_from_u64(57).unwrap(), + }, + Inst::AluRRImm12 { + alu_op: ALUOp::SubS, + size: OperandSize::Size32, + rd: writable_xreg(7), + rn: xreg(8), + imm12: Imm12 { + bits: 0x123, + shift12: false, + }, + }, + Inst::Extend { + rd: writable_xreg(1), + rn: xreg(2), + signed: true, + from_bits: 8, + to_bits: 32, + }, + ]; + + for inst in insts { + let opcodes = opcodes(&inst); + assert_eq!(opcodes.len(), 1); + let opcode = opcodes[0]; + + // Show assembly. + let asm = + inst.print_with_state(&mut EmitState::default(), &mut AllocationConsumer::new(&[])); + + println!("--------------------------------------------------"); + println!("inst = {inst:?}"); + println!("opcode = {opcode:08x}"); + println!("asm = {asm}"); + println!(""); + + // ISLA trace. + let paths = trace_opcode(opcode, &iarch)?; + println!("num paths = {}", paths.len()); + + // Dump. + for events in paths { + let events = if matches.opt_present("filter") { + tree_shake(&events) + } else { + events + }; + write_events(&events, &iarch)?; + + // Generate spec. + if matches.opt_present("spec") { + match trace_to_spec(&events) { + Ok(spec) => printer::dump(&spec)?, + Err(err) => println!("spec conversion failed: {}", err), + }; + } + + println!(""); + } + } + + Ok(()) +} + +fn assemble(inst: &Inst) -> Vec { + let flags = settings::Flags::new(settings::builder()); + let emit_info = EmitInfo::new(flags); + let mut buffer = MachBuffer::new(); + inst.emit(&[], &mut buffer, &emit_info, &mut Default::default()); + let buffer = buffer.finish(&Default::default(), &mut Default::default()); + return buffer.data().to_vec(); +} + +fn opcodes(inst: &Inst) -> Vec { + let machine_code = assemble(&inst); + let mut opcodes = Vec::new(); + for opcode_bytes in machine_code.chunks(4) { + assert_eq!(opcode_bytes.len(), 4); + opcodes.push(u32::from_le_bytes(opcode_bytes.try_into().unwrap())); + } + opcodes +} + +fn trace_opcode<'ir, B: BV>( + opcode: u32, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result>>> { + let shared_state = &&iarch.shared_state; + + let initial_checkpoint = Checkpoint::new(); + let solver_cfg = smt::Config::new(); + let solver_ctx = smt::Context::new(solver_cfg); + let mut solver = Solver::from_checkpoint(&solver_ctx, initial_checkpoint); + let checkpoint = smt::checkpoint(&mut solver); + + let opcode_val = Val::Bits(B::from_u32(opcode)); + + let footprint_function = "zisla_footprint_no_init"; + let function_id = shared_state.symtab.lookup(&footprint_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + let memory = Memory::new(); + let task_state = TaskState::::new(); + let task = LocalFrame::new(function_id, args, ret_ty, Some(&[opcode_val]), instrs) + .add_lets(&iarch.lets) + .add_regs(&iarch.regs) + .set_memory(memory) + .task_with_checkpoint(0, &task_state, checkpoint); + + let num_threads = 1; + let queue = Arc::new(SegQueue::new()); + executor::start_multi( + num_threads, + None, + vec![task], + shared_state, + queue.clone(), + &executor::trace_collector, + ); + + let mut paths = Vec::new(); + loop { + match queue.pop() { + Some(Ok((_, mut events))) => { + simplify::hide_initialization(&mut events); + simplify::remove_extra_register_fields(&mut events); + simplify::remove_repeated_register_reads(&mut events); + simplify::remove_unused_register_assumptions(&mut events); + simplify::remove_unused(&mut events); + simplify::propagate_forwards_used_once(&mut events); + simplify::commute_extract(&mut events); + simplify::eval(&mut events); + + let events: Vec> = events.drain(..).rev().collect(); + paths.push(events); + } + + // Error during execution + Some(Err(err)) => { + let msg = format!("{}", err); + eprintln!( + "{}", + err.source_loc().message::( + None, + shared_state.symtab.files(), + &msg, + true, + true + ) + ); + anyhow::bail!("{}", err); + } + // Empty queue + None => break, + } + } + + Ok(paths) +} + +fn event_writes(event: &Event) -> HashSet { + match event { + Event::Smt(def, _, _) => match def { + smtlib::Def::DefineConst(v, _) => HashSet::from([*v]), + _ => HashSet::new(), + }, + Event::ReadReg(_, _, val) => val_uses(val), + _ => HashSet::new(), + } +} + +fn defns(events: &Vec>) -> HashMap { + let mut defn_idx = HashMap::new(); + for (i, event) in events.iter().enumerate() { + for sym in event_writes(event) { + defn_idx.insert(sym, i); + } + } + defn_idx +} + +fn exp_uses(exp: &smtlib::Exp) -> HashSet { + use smtlib::Exp::*; + match exp { + Var(sym) => HashSet::from([*sym]), + Bits(_) | Bits64(_) | Enum(_) | Bool(_) | FPConstant(..) | FPRoundingMode(_) => { + HashSet::new() + } + Not(exp) + | Bvnot(exp) + | Bvneg(exp) + | Extract(_, _, exp) + | ZeroExtend(_, exp) + | SignExtend(_, exp) + | FPUnary(_, exp) => exp_uses(exp), + Eq(lhs, rhs) + | Neq(lhs, rhs) + | And(lhs, rhs) + | Or(lhs, rhs) + | Bvand(lhs, rhs) + | Bvor(lhs, rhs) + | Bvxor(lhs, rhs) + | Bvnand(lhs, rhs) + | Bvnor(lhs, rhs) + | Bvxnor(lhs, rhs) + | Bvadd(lhs, rhs) + | Bvsub(lhs, rhs) + | Bvmul(lhs, rhs) + | Bvudiv(lhs, rhs) + | Bvsdiv(lhs, rhs) + | Bvurem(lhs, rhs) + | Bvsrem(lhs, rhs) + | Bvsmod(lhs, rhs) + | Bvult(lhs, rhs) + | Bvslt(lhs, rhs) + | Bvule(lhs, rhs) + | Bvsle(lhs, rhs) + | Bvuge(lhs, rhs) + | Bvsge(lhs, rhs) + | Bvugt(lhs, rhs) + | Bvsgt(lhs, rhs) + | Bvshl(lhs, rhs) + | Bvlshr(lhs, rhs) + | Bvashr(lhs, rhs) + | Concat(lhs, rhs) + | FPBinary(_, lhs, rhs) => { + let lhs_uses = exp_uses(lhs); + let rhs_uses = exp_uses(rhs); + &lhs_uses | &rhs_uses + } + Ite(cond, then_exp, else_exp) => { + let cond_uses = exp_uses(cond); + let then_uses = exp_uses(then_exp); + let else_uses = exp_uses(else_exp); + let uses = &cond_uses | &then_uses; + &uses | &else_uses + } + //App(f, args) => { + // uses.insert(*f, uses.get(f).unwrap_or(&0) + 1); + // for arg in args { + // uses_in_exp(uses, arg); + // } + //} + //Select(array, index) => { + // uses_in_exp(uses, array); + // uses_in_exp(uses, index) + //} + //Store(array, index, val) => { + // uses_in_exp(uses, array); + // uses_in_exp(uses, index); + // uses_in_exp(uses, val) + //} + //Distinct(exps) => { + // for exp in exps { + // uses_in_exp(uses, exp); + // } + //} + //FPRoundingUnary(_, rm, exp) => { + // uses_in_exp(uses, rm); + // uses_in_exp(uses, exp); + //} + //FPRoundingBinary(_, rm, lhs, rhs) => { + // uses_in_exp(uses, rm); + // uses_in_exp(uses, lhs); + // uses_in_exp(uses, rhs) + //} + //FPfma(rm, x, y, z) => { + // uses_in_exp(uses, rm); + // uses_in_exp(uses, x); + // uses_in_exp(uses, y); + // uses_in_exp(uses, z) + //} + _ => todo!("not yet implemented expression: {:?}", exp), + } +} + +fn smt_def_uses(def: &smtlib::Def) -> HashSet { + match def { + // DeclareConst(Sym, Ty), + // DeclareFun(Sym, Vec, Ty), + smtlib::Def::DefineConst(_, exp) => exp_uses(&exp), + // DefineEnum(Name, usize), + // Assert(Exp), + _ => HashSet::new(), + } +} + +fn val_uses(val: &Val) -> HashSet { + // See: simplify::uses_in_value + use Val::*; + match val { + Symbolic(sym) => HashSet::from([*sym]), + // MixedBits(segments) => segments.iter().for_each(|segment| match segment { + // BitsSegment::Symbolic(v) => { + // uses.insert(*v, uses.get(v).unwrap_or(&0) + 1); + // } + // BitsSegment::Concrete(_) => (), + // }), + I64(_) | I128(_) | Bool(_) | Bits(_) | Enum(_) | String(_) | Unit | Ref(_) | Poison => { + HashSet::new() + } + // List(vals) | Vector(vals) => vals.iter().for_each(|val| uses_in_value(uses, val)), + Struct(fields) => fields + .iter() + .map(|(_, val)| val_uses(val)) + .fold(HashSet::new(), |acc, uses| &acc | &uses), + // Ctor(_, val) => uses_in_value(uses, val), + // SymbolicCtor(v, possibilities) => { + // uses.insert(*v, uses.get(v).unwrap_or(&0) + 1); + // possibilities + // .iter() + // .for_each(|(_, val)| uses_in_value(uses, val)) + // } + _ => todo!("not yet implemented value: {:?}", val), + } +} + +fn uses(event: &Event) -> HashSet { + match event { + Event::Smt(def, _, _) => smt_def_uses(&def), + Event::WriteReg(_, _, val) => val_uses(val), + _ => HashSet::new(), + } +} + +fn tree_shake(events: &Vec>) -> Vec> { + // Definitions. + let defn_idx = defns(events); + + // Work list: populate with register writes. + let mut work_list = Vec::new(); + let mut live = HashSet::new(); + for (i, event) in events.iter().enumerate() { + match event { + Event::WriteReg(_, _, val) => val_uses(val).iter().for_each(|sym| { + // Mark live. + live.insert(i); + + // Push the variable to be visited. + let d = defn_idx[&sym]; + live.insert(d); + work_list.push(d); + }), + _ => continue, + }; + } + + // Process. + while !work_list.is_empty() { + let i = work_list.pop().unwrap(); + assert!(live.contains(&i), "visited events should be live"); + let event = &events[i]; + + // Mark uses live. + for u in uses(&event) { + // Lookup definition of this dependency. + assert!(defn_idx.contains_key(&u), "no definition for {:?}", u); + let ui = defn_idx[&u]; + if live.contains(&ui) { + continue; + } + + live.insert(ui); + work_list.push(ui); + } + } + + // Filter down to live events. + let mut events: Vec<_> = events + .iter() + .enumerate() + .filter_map(|(i, event)| if live.contains(&i) { Some(event) } else { None }) + .cloned() + .collect(); + + // Simplify pass. + events.reverse(); + simplify::propagate_forwards_used_once(&mut events); + events.reverse(); + + events +} + +fn write_events<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result<()> { + // Print. + let stdout = std::io::stdout(); + let mut handle = BufWriter::with_capacity(5 * usize::pow(2, 20), stdout.lock()); + let write_opts = WriteOpts::default(); + simplify::write_events_with_opts(&mut handle, &events, &iarch.shared_state, &write_opts) + .unwrap(); + handle.flush().unwrap(); + + Ok(()) +} + +struct TypeContext { + ty: HashMap, + fun: HashMap, smtlib::Ty)>, +} + +impl TypeContext { + fn new() -> TypeContext { + TypeContext { + ty: HashMap::new(), + fun: HashMap::new(), + } + } + + fn infer(&self, exp: &smtlib::Exp) -> Option { + exp.infer(&self.ty, &self.fun) + } +} + +fn trace_to_spec(events: &Vec>) -> anyhow::Result { + Ok(Spec { + term: spec_ident("placeholder".to_string()), + args: vec![], + requires: vec![], + provides: trace_provides(events)?, + }) +} + +fn trace_provides(events: &Vec>) -> anyhow::Result> { + let mut provides = Vec::new(); + let mut tctx = TypeContext::new(); + for event in events { + if let Some(exp) = event_to_spec(event, &mut tctx)? { + provides.push(exp); + } + } + Ok(provides) +} + +fn event_to_spec( + event: &Event, + tctx: &mut TypeContext, +) -> anyhow::Result> { + match event { + Event::Smt(def, attr, ..) if !attr.is_uninteresting() => smt_to_spec(def, tctx), + _ => Ok(None), + } +} + +fn smt_to_spec(def: &smtlib::Def, tctx: &mut TypeContext) -> anyhow::Result> { + match def { + smtlib::Def::DefineConst(v, exp) => { + let ty = tctx.infer(exp).expect("SMT expression was badly-typed"); + tctx.ty.insert(*v, ty.clone()); + + Ok(Some(SpecExpr::Op { + op: SpecOp::Eq, + args: vec![ + exp_to_spec(&smtlib::Exp::Var(*v), tctx), + exp_to_spec(exp, tctx), + ], + pos: Pos::default(), + })) + } + + smtlib::Def::DeclareConst(v, ty) => { + tctx.ty.insert(*v, ty.clone()); + Ok(None) + } + + smtlib::Def::DeclareFun(v, params, ret) => { + tctx.fun.insert(*v, (params.clone(), ret.clone())); + Ok(None) + } + + smtlib::Def::DefineEnum(..) => Ok(None), + + _ => anyhow::bail!("unsupported smt def: {:?}", def), + } +} + +fn exp_to_spec(exp: &smtlib::Exp, tctx: &TypeContext) -> SpecExpr { + use smtlib::Exp::*; + match exp { + Var(v) => SpecExpr::Var { + var: spec_ident(format!("v{}", v)), + pos: Pos::default(), + }, + Bits(bits) => spec_bits(bits), + Bits64(bv) => spec_const_bit_vector( + bv.lower_u64().try_into().unwrap(), + bv.len().try_into().unwrap(), + ), + // Enum(EnumMember), + Bool(b) => spec_const_bool(*b), + // Neq(Box>, Box>), + Not(x) | Bvnot(x) => spec_unary(exp_spec_op(exp), exp_to_spec(x, tctx)), + + // Bvnot(Box>), + // Bvnand(Box>, Box>), + // Bvnor(Box>, Box>), + // Bvxnor(Box>, Box>), + // Bvneg(Box>), + Eq(lhs, rhs) + | And(lhs, rhs) + | Or(lhs, rhs) + | Bvand(lhs, rhs) + | Bvor(lhs, rhs) + | Bvxor(lhs, rhs) + | Bvadd(lhs, rhs) + | Bvsub(lhs, rhs) + | Bvmul(lhs, rhs) + | Bvshl(lhs, rhs) + | Bvlshr(lhs, rhs) + | Concat(lhs, rhs) => spec_binary( + exp_spec_op(exp), + exp_to_spec(lhs, tctx), + exp_to_spec(rhs, tctx), + ), + + // Bvudiv(Box>, Box>), + // Bvsdiv(Box>, Box>), + // Bvurem(Box>, Box>), + // Bvsrem(Box>, Box>), + // Bvsmod(Box>, Box>), + // Bvult(Box>, Box>), + // Bvslt(Box>, Box>), + // Bvule(Box>, Box>), + // Bvsle(Box>, Box>), + // Bvuge(Box>, Box>), + // Bvsge(Box>, Box>), + // Bvugt(Box>, Box>), + // Bvsgt(Box>, Box>), + Extract(i, j, exp) => spec_ternary( + SpecOp::Extract, + spec_const_int(*i), + spec_const_int(*j), + exp_to_spec(exp, tctx), + ), + + ZeroExtend(n, x) | SignExtend(n, x) => match tctx.infer(x).unwrap() { + smtlib::Ty::BitVec(w) => spec_binary( + exp_spec_op(exp), + spec_const_int(n + w), + exp_to_spec(x, tctx), + ), + _ => panic!("extension applies to bitvector types"), + }, + + // Bvlshr(Box>, Box>), + // Bvashr(Box>, Box>), + Ite(c, t, e) => spec_ternary( + SpecOp::If, + exp_to_spec(c, tctx), + exp_to_spec(t, tctx), + exp_to_spec(e, tctx), + ), + + // App(Sym, Vec>), + // Select(Box>, Box>), + // Store(Box>, Box>, Box>), + // Distinct(Vec>), + // FPConstant(FPConstant, u32, u32), + // FPRoundingMode(FPRoundingMode), + // FPUnary(FPUnary, Box>), + // FPRoundingUnary(FPRoundingUnary, Box>, Box>), + // FPBinary(FPBinary, Box>, Box>), + // FPRoundingBinary(FPRoundingBinary, Box>, Box>, Box>), + // FPfma(Box>, Box>, Box>, Box>), + _ => todo!("expression: {:?}", exp), + } +} + +fn exp_spec_op(exp: &smtlib::Exp) -> SpecOp { + use smtlib::Exp::*; + match exp { + // Bits(Vec), + // Bits64(B64), + // Enum(EnumMember), + // Bool(bool), + Eq(..) => SpecOp::Eq, + // Neq(Box>, Box>), + And(..) => SpecOp::And, + Or(..) => SpecOp::Or, + Not(..) => SpecOp::Not, + Bvnot(..) => SpecOp::BVNot, + Bvand(..) => SpecOp::BVAnd, + Bvor(..) => SpecOp::BVOr, + Bvxor(..) => SpecOp::BVXor, + // Bvnand(Box>, Box>), + // Bvnor(Box>, Box>), + // Bvxnor(Box>, Box>), + // Bvneg(Box>), + Bvadd(..) => SpecOp::BVAdd, + Bvsub(..) => SpecOp::BVSub, + Bvmul(..) => SpecOp::BVMul, + // Bvudiv(Box>, Box>), + // Bvsdiv(Box>, Box>), + // Bvurem(Box>, Box>), + // Bvsrem(Box>, Box>), + // Bvsmod(Box>, Box>), + // Bvult(Box>, Box>), + // Bvslt(Box>, Box>), + // Bvule(Box>, Box>), + // Bvsle(Box>, Box>), + // Bvuge(Box>, Box>), + // Bvsge(Box>, Box>), + // Bvugt(Box>, Box>), + // Bvsgt(Box>, Box>), + ZeroExtend(..) => SpecOp::ZeroExt, + SignExtend(..) => SpecOp::SignExt, + Bvshl(..) => SpecOp::BVShl, + Bvlshr(..) => SpecOp::BVLshr, + // Bvashr(Box>, Box>), + Concat(..) => SpecOp::Concat, + // Ite(Box>, Box>, Box>), + // App(Sym, Vec>), + // Select(Box>, Box>), + // Store(Box>, Box>, Box>), + // Distinct(Vec>), + // FPConstant(FPConstant, u32, u32), + // FPRoundingMode(FPRoundingMode), + // FPUnary(FPUnary, Box>), + // FPRoundingUnary(FPRoundingUnary, Box>, Box>), + // FPBinary(FPBinary, Box>, Box>), + // FPRoundingBinary(FPRoundingBinary, Box>, Box>, Box>), + // FPfma(Box>, Box>, Box>, Box>), + _ => todo!("spec op: {:?}", exp), + } +} + +fn spec_const_int(x: I) -> SpecExpr +where + i128: From, +{ + SpecExpr::ConstInt { + val: x.try_into().unwrap(), + pos: Pos::default(), + } +} + +fn spec_const_bool(b: bool) -> SpecExpr { + SpecExpr::ConstBool { + val: if b { 1 } else { 0 }, + pos: Pos::default(), + } +} + +fn spec_const_bit_vector(val: i128, width: i8) -> SpecExpr { + assert!(width >= 0); + SpecExpr::ConstBitVec { + val, + width, + pos: Pos::default(), + } +} + +fn spec_bits(bits: &[bool]) -> SpecExpr { + // TODO(mbm): verify endianness assumption about Vec and test multi-chunk case + bits.chunks(64) + .map(|chunk| { + let mut val: i128 = 0; + for (i, bit) in chunk.iter().enumerate() { + if *bit { + val |= 1 << i; + } + } + spec_const_bit_vector(val, 64) + }) + .rev() + .reduce(|acc, bv| spec_binary(SpecOp::Concat, acc, bv)) + .unwrap() +} + +fn spec_unary(op: SpecOp, x: SpecExpr) -> SpecExpr { + SpecExpr::Op { + op, + args: vec![x], + pos: Pos::default(), + } +} + +fn spec_binary(op: SpecOp, x: SpecExpr, y: SpecExpr) -> SpecExpr { + SpecExpr::Op { + op, + args: vec![x, y], + pos: Pos::default(), + } +} + +fn spec_ternary(op: SpecOp, x: SpecExpr, y: SpecExpr, z: SpecExpr) -> SpecExpr { + SpecExpr::Op { + op, + args: vec![x, y, z], + pos: Pos::default(), + } +} + +fn spec_ident(id: String) -> Ident { + Ident(id, Pos::default()) +} diff --git a/cranelift/isle/veri/veri_engine/src/isla.rs b/cranelift/isle/veri/veri_engine/src/isla.rs new file mode 100644 index 000000000000..f21bebf9c4c7 --- /dev/null +++ b/cranelift/isle/veri/veri_engine/src/isla.rs @@ -0,0 +1,230 @@ +use anyhow::Context as _; +use clap::Parser; +use cranelift_codegen::print_errors::pretty_error; +use cranelift_codegen::Context; +use cranelift_reader::{parse_sets_and_triple, parse_test, ParseOptions}; +use crossbeam::queue::SegQueue; +use isla_lib::bitvector::{b129::B129, BV}; +use isla_lib::config::ISAConfig; +use isla_lib::error::IslaError; +use isla_lib::executor::{self, LocalFrame, TaskState}; +use isla_lib::init::initialize_architecture; +use isla_lib::ir::{AssertionMode, Def, IRTypeInfo, Name, Symtab, Val}; +use isla_lib::ir_lexer::new_ir_lexer; +use isla_lib::ir_parser; +use isla_lib::memory::Memory; +use isla_lib::simplify::{self, WriteOpts}; +use isla_lib::smt::{self, Checkpoint, Event, Solver}; +use sha2::{Digest, Sha256}; +use std::fs::File; +use std::io::prelude::*; +use std::io::{self, BufWriter, Read}; +use std::path::{Path, PathBuf}; +use std::sync::Arc; + +#[derive(Parser)] +struct Options { + /// Configure Cranelift settings. + #[clap(long = "set")] + settings: Vec, + + /// Specify the Cranelift target. + #[clap(long = "target")] + target: String, + + /// Architecture definition. + #[clap(long)] + arch: PathBuf, + + /// ISA config file. + #[clap(long)] + isa_config: PathBuf, + + /// Specify an input file to be used. Use '-' for stdin. + file: PathBuf, +} + +fn main() -> anyhow::Result<()> { + let options = Options::parse(); + + // Parse input CLIF test file. + let buffer = read_to_string(&options.file)?; + let test_file = parse_test(&buffer, ParseOptions::default()) + .with_context(|| format!("failed to parse {}", options.file.to_string_lossy()))?; + + // Determine ISA settings. + let parsed = parse_sets_and_triple(&options.settings, &options.target)?; + let fisa = parsed.as_fisa(); + let isa = fisa.isa.or(test_file.isa_spec.unique_isa()); + + let isa = match isa { + None => anyhow::bail!("compilation requires a target isa"), + Some(isa) => isa, + }; + + // Parse ISLA Architecture. + let contents = read_to_string(&options.arch)?; + let mut symtab = Symtab::new(); + let mut arch = parse_ir::(&contents, &mut symtab)?; + + // ISLA ISA Config. + let mut hasher = Sha256::new(); + let type_info = IRTypeInfo::new(&arch); + let isa_config = match ISAConfig::::from_file( + &mut hasher, + &options.isa_config, + None, + &symtab, + &type_info, + ) { + Ok(isa_config) => isa_config, + Err(msg) => return Err(anyhow::Error::msg(msg)), + }; + + // Compile functions. + for (func, _) in test_file.functions { + let mut context = Context::for_function(func); + let mut mem = vec![]; + let _compiled_code = context + .compile_and_emit(isa, &mut mem, &mut Default::default()) + .map_err(|err| anyhow::anyhow!("{}", pretty_error(&err.func, err.inner)))?; + trace_function( + &mem, + &mut arch, + symtab.clone(), + type_info.clone(), + &isa_config, + )?; + } + + Ok(()) +} + +fn trace_function( + mc: &[u8], + arch: &mut Vec>, + symtab: Symtab, + type_info: IRTypeInfo, + isa_config: &ISAConfig, +) -> anyhow::Result<()> { + let use_model_reg_init = true; + let iarch = initialize_architecture( + arch, + symtab, + type_info, + &isa_config, + AssertionMode::Optimistic, + use_model_reg_init, + ); + let shared_state = &&iarch.shared_state; + + let initial_checkpoint = Checkpoint::new(); + let solver_cfg = smt::Config::new(); + let solver_ctx = smt::Context::new(solver_cfg); + let mut solver = Solver::from_checkpoint(&solver_ctx, initial_checkpoint); + let checkpoint = smt::checkpoint(&mut solver); + + let opcode_vals = opcode_vals(mc)?; + print!("opcode vals = {:?}", opcode_vals); + + let footprint_function = "zisla_footprint"; + let function_id = shared_state.symtab.lookup(&footprint_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + let memory = Memory::new(); + let task_state = TaskState::::new(); + let task = LocalFrame::new(function_id, args, ret_ty, Some(&opcode_vals), instrs) + .add_lets(&iarch.lets) + .add_regs(&iarch.regs) + .set_memory(memory) + .task_with_checkpoint(0, &task_state, checkpoint); + + let num_threads = 1; + let queue = Arc::new(SegQueue::new()); + executor::start_multi( + num_threads, + None, + vec![task], + shared_state, + queue.clone(), + &executor::trace_collector, + ); + + loop { + match queue.pop() { + Some(Ok((_, mut events))) => { + simplify::hide_initialization(&mut events); + simplify::remove_unused(&mut events); + simplify::propagate_forwards_used_once(&mut events); + simplify::commute_extract(&mut events); + simplify::eval(&mut events); + + let events: Vec> = events.drain(..).rev().collect(); + let stdout = std::io::stdout(); + let mut handle = BufWriter::with_capacity(5 * usize::pow(2, 20), stdout.lock()); + let write_opts = WriteOpts::default(); + simplify::write_events_with_opts(&mut handle, &events, &shared_state, &write_opts) + .unwrap(); + handle.flush().unwrap() + } + + // Error during execution + Some(Err(err)) => { + let msg = format!("{}", err); + eprintln!( + "{}", + err.source_loc().message::( + None, + shared_state.symtab.files(), + &msg, + true, + true + ) + ); + anyhow::bail!("{}", err); + } + // Empty queue + None => break, + } + } + + Ok(()) +} + +fn opcode_vals(mc: &[u8]) -> anyhow::Result>> { + let mut vals = Vec::new(); + for opcode_bytes in mc.chunks(4) { + let val = Val::Bits(B::from_u32(u32::from_le_bytes( + opcode_bytes.try_into().unwrap(), + ))); + vals.push(val); + } + Ok(vals) +} + +fn parse_ir<'a, 'input, B: BV>( + contents: &'input str, + symtab: &'a mut Symtab<'input>, +) -> anyhow::Result>> { + match ir_parser::IrParser::new().parse(symtab, new_ir_lexer(&contents)) { + Ok(ir) => Ok(ir), + Err(_) => Err(anyhow::Error::msg("bad")), + } +} + +/// Read an entire file into a string. +fn read_to_string>(path: P) -> anyhow::Result { + let mut buffer = String::new(); + let path = path.as_ref(); + if path == Path::new("-") { + let stdin = io::stdin(); + let mut stdin = stdin.lock(); + stdin + .read_to_string(&mut buffer) + .context("failed to read stdin to string")?; + } else { + let mut file = File::open(path)?; + file.read_to_string(&mut buffer) + .with_context(|| format!("failed to read {} to string", path.display()))?; + } + Ok(buffer) +} diff --git a/cranelift/isle/veri/veri_engine/src/lib.rs b/cranelift/isle/veri/veri_engine/src/lib.rs index dfc315b9ee36..1ce4a4863c4c 100644 --- a/cranelift/isle/veri/veri_engine/src/lib.rs +++ b/cranelift/isle/veri/veri_engine/src/lib.rs @@ -16,7 +16,7 @@ pub mod verify; pub const REG_WIDTH: usize = 64; // Use a distinct with as the maximum width any value should have within type inference -pub const MAX_WIDTH: usize = 4*REG_WIDTH; +pub const MAX_WIDTH: usize = 2 * REG_WIDTH; pub const FLAGS_WIDTH: usize = 4; diff --git a/cranelift/isle/veri/veri_engine/src/type_inference.rs b/cranelift/isle/veri/veri_engine/src/type_inference.rs index 67dfad805fcf..92dcd947fb89 100644 --- a/cranelift/isle/veri/veri_engine/src/type_inference.rs +++ b/cranelift/isle/veri/veri_engine/src/type_inference.rs @@ -26,8 +26,8 @@ struct RuleParseTree { bv_constraints: HashSet, ty_vars: HashMap, - quantified_vars: HashSet<(String, u32)>, - free_vars: HashSet<(String, u32)>, + quantified_vars: HashMap, + free_vars: HashMap, // Used to check distinct models term_input_bvs: Vec, // Used for custom verification conditions @@ -178,8 +178,8 @@ fn type_annotations_using_rule<'a>( var_constraints: HashSet::new(), bv_constraints: HashSet::new(), ty_vars: HashMap::new(), - quantified_vars: HashSet::new(), - free_vars: HashSet::new(), + quantified_vars: HashMap::new(), + free_vars: HashMap::new(), term_input_bvs: vec![], term_args: vec![], assumptions: vec![], @@ -380,6 +380,13 @@ fn add_annotation_constraints( tree.next_type_var += 1; } let name = format!("{}__{}__{}", annotation_info.term, x, t); + + // Support the introduction of extra variables in the specification. + // + // TODO(mbm): understand whether this needs to be in quantified, free or both? + tree.quantified_vars.insert(name.clone(), t); + tree.free_vars.insert(name.clone(), t); + (veri_ir::Expr::Terminal(veri_ir::Terminal::Var(name)), t) } annotation_ir::Expr::Const(c, ..) => { @@ -446,6 +453,24 @@ fn add_annotation_constraints( t, ) } + annotation_ir::Expr::Imp(x, y) => { + let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info); + let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info); + let t = tree.next_type_var; + + tree.concrete_constraints + .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Bool)); + tree.concrete_constraints + .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Bool)); + tree.concrete_constraints + .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool)); + + tree.next_type_var += 1; + ( + veri_ir::Expr::Binary(veri_ir::BinaryOp::Imp, Box::new(e1), Box::new(e2)), + t, + ) + } annotation_ir::Expr::Lte(x, y) => { let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info); let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info); @@ -1358,12 +1383,8 @@ fn add_annotation_constraints( tree.next_type_var += 1; (veri_ir::Expr::BVPopcnt(Box::new(e1)), t) } - - _ => todo!("expr {:#?} not yet implemented", expr), }; tree.ty_vars.insert(e.clone(), t); - // let fmt = format!("{}:\t{:?}", t, e); - // dbg!(fmt); (e, t) } @@ -1445,8 +1466,8 @@ fn add_rule_constraints( let e = match &curr.construct { TypeVarConstruct::Var => { tree.quantified_vars - .insert((curr.ident.clone(), curr.type_var)); - tree.free_vars.insert((curr.ident.clone(), curr.type_var)); + .insert(curr.ident.clone(), curr.type_var); + tree.free_vars.insert(curr.ident.clone(), curr.type_var); Some(veri_ir::Expr::Terminal(veri_ir::Terminal::Var( curr.ident.clone(), ))) @@ -1475,7 +1496,7 @@ fn add_rule_constraints( } TypeVarConstruct::And => { tree.quantified_vars - .insert((curr.ident.clone(), curr.type_var)); + .insert(curr.ident.clone(), curr.type_var); let first = &children[0]; for (i, e) in children.iter().enumerate() { if i != 0 { @@ -1490,7 +1511,7 @@ fn add_rule_constraints( } TypeVarConstruct::Let(bound) => { tree.quantified_vars - .insert((curr.ident.clone(), curr.type_var)); + .insert(curr.ident.clone(), curr.type_var); for (e, s) in children.iter().zip(bound) { tree.assumptions.push(veri_ir::Expr::Binary( veri_ir::BinaryOp::Eq, @@ -1510,7 +1531,7 @@ fn add_rule_constraints( print!(" {}", term_name); tree.quantified_vars - .insert((curr.ident.clone(), curr.type_var)); + .insert(curr.ident.clone(), curr.type_var); let a = annotation_env.get_annotation_for_term(term_id); if a.is_none() { println!("\nSkipping rule with unannotated term: {}", term_name); @@ -1601,7 +1622,7 @@ fn add_rule_constraints( annotation_info.term, arg.name, annotation_type_var ); tree.quantified_vars - .insert((arg_name.clone(), annotation_type_var)); + .insert(arg_name.clone(), annotation_type_var); tree.assumptions.push(veri_ir::Expr::Binary( veri_ir::BinaryOp::Eq, Box::new(child.clone()), @@ -1616,7 +1637,7 @@ fn add_rule_constraints( "{}__{}__{}", annotation_info.term, annotation.sig.ret.name, ret_var ); - tree.quantified_vars.insert((ret_name.clone(), ret_var)); + tree.quantified_vars.insert(ret_name.clone(), ret_var); tree.assumptions.push(veri_ir::Expr::Binary( veri_ir::BinaryOp::Eq, Box::new(veri_ir::Expr::Terminal(veri_ir::Terminal::Var( @@ -2258,7 +2279,7 @@ fn create_parse_tree_expr( tree.varid_to_type_var_map.insert(*varid, ty_var); children.push(subpat_node); let ident = format!("{}__clif{}__{}", var, varid.index(), ty_var); - tree.quantified_vars.insert((ident.clone(), ty_var)); + tree.quantified_vars.insert(ident.clone(), ty_var); bound.push(ident); } let body = create_parse_tree_expr(rule, body, tree, typeenv, termenv); diff --git a/cranelift/isle/veri/veri_engine/src/x64.rs b/cranelift/isle/veri/veri_engine/src/x64.rs new file mode 100644 index 000000000000..2acd6dcf4319 --- /dev/null +++ b/cranelift/isle/veri/veri_engine/src/x64.rs @@ -0,0 +1,573 @@ +use clap::Parser; +use cranelift_codegen::isa::x64::{ + self, + inst::{args::*, *}, +}; +use cranelift_codegen::{settings, MachBuffer, MachInstEmit, Reg, Writable}; +use crossbeam::queue::SegQueue; +use isla_lib::init::{initialize_architecture, Initialized}; +use isla_lib::ir::{AssertionMode, Def, IRTypeInfo, Name, Symtab, Ty, Val}; +use isla_lib::ir_lexer::new_ir_lexer; +use isla_lib::ir_parser; +use isla_lib::log; +use isla_lib::memory::{Memory, SmtKind}; +use isla_lib::simplify::{self, WriteOpts}; +use isla_lib::smt::smtlib::{self, bits64}; +use isla_lib::smt::{self, Checkpoint, Event, ReadOpts, Solver, Sym}; +use isla_lib::source_loc::SourceLoc; +use isla_lib::{ + bitvector::{b64::B64, BV}, + zencode, +}; +use isla_lib::{config::ISAConfig, executor::unfreeze_frame}; +use isla_lib::{ + error::{ExecError, IslaError}, + memory::Address, +}; +use isla_lib::{ + executor::{self, freeze_frame, LocalFrame, TaskState}, + ir::linearize, +}; +use sha2::{Digest, Sha256}; +use std::io::prelude::*; +use std::io::BufWriter; +use std::path::PathBuf; +use std::sync::Arc; + +#[derive(Parser)] +struct Options { + /// Architecture definition. + #[clap(long)] + arch: PathBuf, + + /// ISA config file. + #[clap(long)] + isa_config: PathBuf, + + /// Trace output directory. + #[clap(long, default_value = ".")] + output_dir: PathBuf, +} + +fn main() -> anyhow::Result<()> { + let options = Options::parse(); + log::set_flags(log::VERBOSE); + + // Parse ISLA Architecture. + let contents = std::fs::read_to_string(&options.arch)?; + let mut symtab = Symtab::new(); + let mut arch = parse_ir::(&contents, &mut symtab)?; + + // ISLA ISA Config. + let mut hasher = Sha256::new(); + let type_info = IRTypeInfo::new(&arch); + let isa_config = match ISAConfig::::from_file( + &mut hasher, + &options.isa_config, + None, + &symtab, + &type_info, + ) { + Ok(isa_config) => isa_config, + Err(msg) => anyhow::bail!(msg), + }; + + let linearize_functions = vec![ + // See: https://github.com/rems-project/isla-testgen/blob/a9759247bfdff9c9c39d95a4cfd85318e5bf50fe/c86-command + //"fdiv_int", + "bool_to_bits", + "bits_to_bool", + //"bit_to_bool", + //"isEven", + "signed_byte_p_int", + "zf_spec", + //"b_xor", + //"logand_int", + //"not_bit", + //"floor2", + ]; + for name in linearize_functions { + linearize_function(&mut arch, name, &mut symtab)?; + } + + let use_model_reg_init = true; + let iarch = initialize_architecture( + &mut arch, + symtab, + type_info, + &isa_config, + AssertionMode::Optimistic, + use_model_reg_init, + ); + + // Assemble x64 instruction. + let rdx = regs::rdx(); + let r13 = regs::r13(); + let w_rdx = Writable::::from_reg(rdx); + let inst = Inst::AluRmiR { + size: OperandSize::Size64, + op: AluRmiROpcode::Add, + src1: Gpr::new(rdx).unwrap(), + src2: GprMemImm::new(RegMemImm::reg(r13)).unwrap(), + dst: WritableGpr::from_writable_reg(w_rdx).unwrap(), + }; + + let machine_code = assemble(&inst); + println!("machine code = {:02x?}", machine_code); + + // ISLA trace. + let paths = trace_opcode(&machine_code, &iarch)?; + + // Dump. + for (i, events) in paths.iter().enumerate() { + let filename = format!("trace{i:04}.out"); + let path = options.output_dir.join(filename); + log!(log::VERBOSE, format!("write trace to {}", path.display())); + + let file = std::fs::File::create(path)?; + write_events(&events, &iarch, file)?; + } + + log!( + log::VERBOSE, + format!("generated {} trace paths", paths.len()) + ); + + Ok(()) +} + +/// Assemble x64 instruction. +fn assemble(inst: &Inst) -> Vec { + let flags = settings::Flags::new(settings::builder()); + let isa_flag_builder = x64::settings::builder(); + let isa_flags = x64::settings::Flags::new(&flags, &isa_flag_builder); + let emit_info = EmitInfo::new(flags, isa_flags); + let mut buffer = MachBuffer::new(); + inst.emit(&[], &mut buffer, &emit_info, &mut Default::default()); + let buffer = buffer.finish(&Default::default(), &mut Default::default()); + return buffer.data().to_vec(); +} + +fn trace_opcode<'ir, B: BV>( + opcode: &Vec, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result>>> { + let shared_state = &&iarch.shared_state; + let symtab = &shared_state.symtab; + + let initial_checkpoint = Checkpoint::new(); + let solver_cfg = smt::Config::new(); + let solver_ctx = smt::Context::new(solver_cfg); + let mut solver = Solver::from_checkpoint(&solver_ctx, initial_checkpoint); + let memory = Memory::new(); + + // Initialization ----------------------------------------------------------- + // - run initialization function to set processor in 64-bit mode + + let init_function = zencode::encode("initialise_64_bit_mode"); + let function_id = shared_state.symtab.lookup(&init_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + + let task_state = TaskState::::new(); + let checkpoint = smt::checkpoint(&mut solver); + let task = LocalFrame::new(function_id, args, ret_ty, None, instrs) + .add_lets(&iarch.lets) + .add_regs(&iarch.regs) + .set_memory(memory) + .task_with_checkpoint(0, &task_state, checkpoint); + + let queue = Arc::new(SegQueue::new()); + executor::start_single( + task, + &shared_state, + &queue, + &move |_tid, _task_id, result, _shared_state, mut solver, queue| match result { + Ok((_, frame)) => { + queue.push((freeze_frame(&frame), smt::checkpoint(&mut solver))); + } + Err(err) => panic!("Initialisation failed: {:?}", err), + }, + ); + assert_eq!(queue.len(), 1); + let (frame, checkpoint) = queue.pop().expect("pop failed"); + + let mut solver = Solver::from_checkpoint(&solver_ctx, checkpoint); + + // Initialize registers ----------------------------------------------------- + // - set symbolic values for all general-purpose registers + + let mut local_frame = executor::unfreeze_frame(&frame); + for (n, ty) in &shared_state.registers { + // Only handle general-purpose registers. + if let Ty::Bits(bits) = ty { + let var = solver.fresh(); + solver.add(smtlib::Def::DeclareConst(var, smtlib::Ty::BitVec(*bits))); + let val = Val::Symbolic(var); + local_frame.regs_mut().assign(*n, val, shared_state); + } + } + + let frame = freeze_frame(&local_frame); + + // Setup memory ------------------------------------------------------------- + + let mut local_frame = unfreeze_frame(&frame); + + const INIT_PC: Address = 0x401000; + local_frame + .memory_mut() + .add_symbolic_code_region(INIT_PC..INIT_PC + 0x10000); + + let memory_var = solver.fresh(); + solver.add(smtlib::Def::DeclareConst( + memory_var, + smtlib::Ty::Array( + Box::new(smtlib::Ty::BitVec(64)), + Box::new(smtlib::Ty::BitVec(8)), + ), + )); + + let memory_client_info: Box> = + Box::new(SeqMemory { memory_var }); + local_frame.memory_mut().set_client_info(memory_client_info); + + let frame = freeze_frame(&local_frame); + + // Set initial program counter ---------------------------------------------- + + let local_frame = unfreeze_frame(&frame); + + let pc_name = zencode::encode("rip"); + let pc_id = symtab.lookup(&pc_name); + let pc = local_frame.regs().get_last_if_initialized(pc_id).unwrap(); + + solver.add(smtlib::Def::Assert(smtlib::Exp::Eq( + Box::new(smt_value(pc).unwrap()), + Box::new(smtlib::Exp::Bits64(B64::from_u64(INIT_PC))), + ))); + + let frame = freeze_frame(&local_frame); + + // Setup opcode ------------------------------------------------------------- + + let local_frame = unfreeze_frame(&frame); + + let read_val = local_frame + .memory() + .read( + Val::Unit, /* read_kind */ + pc.clone(), + Val::I128(opcode.len() as i128), + &mut solver, + false, + ReadOpts::ifetch(), + ) + .unwrap(); + + let opcode_var = solver.fresh(); + solver.add(smtlib::Def::DeclareConst( + opcode_var, + smtlib::Ty::BitVec(8 * opcode.len() as u32), + )); + solver.add(smtlib::Def::Assert(smtlib::Exp::Eq( + Box::new(smtlib::Exp::Var(opcode_var)), + Box::new(smt_bytes(opcode)), + ))); + + let read_exp = smt_value(&read_val).unwrap(); + solver.add(smtlib::Def::Assert(smtlib::Exp::Eq( + Box::new(smtlib::Exp::Var(opcode_var)), + Box::new(read_exp), + ))); + + let frame = freeze_frame(&local_frame); + + // Debug dump --------------------------------------------------------------- + + assert_eq!(solver.check_sat(), smt::SmtResult::Sat); + let checkpoint = smt::checkpoint(&mut solver); + dump_checkpoint(&checkpoint, iarch)?; + + // Execute fetch and decode ------------------------------------------------- + + let local_frame = unfreeze_frame(&frame); + + local_frame.memory().log(); + + let run_instruction_function = zencode::encode("x86_fetch_decode_execute"); + let function_id = shared_state.symtab.lookup(&run_instruction_function); + let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); + + let task_state = TaskState::::new(); + let task = local_frame + .new_call(function_id, args, ret_ty, None, instrs) + .task_with_checkpoint(1, &task_state, checkpoint); + + let num_threads = 1; + let queue = Arc::new(SegQueue::new()); + executor::start_multi( + num_threads, + None, + vec![task], + shared_state, + queue.clone(), + &executor::trace_collector, + ); + + let mut paths = Vec::new(); + loop { + match queue.pop() { + Some(Ok((_, mut events))) => { + // simplify::hide_initialization(&mut events); + simplify::remove_extra_register_fields(&mut events); + simplify::remove_repeated_register_reads(&mut events); + simplify::remove_unused_register_assumptions(&mut events); + simplify::remove_unused(&mut events); + simplify::propagate_forwards_used_once(&mut events); + simplify::commute_extract(&mut events); + simplify::eval(&mut events); + + let events: Vec> = events.drain(..).rev().collect(); + paths.push(events); + } + + // Error during execution + Some(Err(err)) => { + let msg = format!("{}", err); + eprintln!( + "{}", + err.source_loc().message::( + None, + shared_state.symtab.files(), + &msg, + true, + true + ) + ); + anyhow::bail!("{}", err); + } + // Empty queue + None => break, + } + } + + Ok(paths) +} + +#[derive(Debug, Clone)] +struct SeqMemory { + memory_var: Sym, +} + +impl isla_lib::memory::MemoryCallbacks for SeqMemory { + fn symbolic_read( + &self, + regions: &[isla_lib::memory::Region], + solver: &mut Solver, + value: &Val, + _read_kind: &Val, + address: &Val, + bytes: u32, + _tag: &Option>, + opts: &ReadOpts, + ) { + use isla_lib::smt::smtlib::{Def, Exp}; + + let read_exp = smt_value(value) + .unwrap_or_else(|err| panic!("Bad memory read value {:?}: {}", value, err)); + let addr_exp = smt_value(address) + .unwrap_or_else(|err| panic!("Bad read address value {:?}: {}", address, err)); + let read_prop = Exp::Eq( + Box::new(read_exp.clone()), + Box::new(smt_read_exp(self.memory_var, &addr_exp, bytes as u64)), + ); + let kind = if opts.is_ifetch { + SmtKind::ReadInstr + } else if opts.is_exclusive { + // We produce a dummy read so that failed store exclusives still get address + // constraints, but the memory must be writable. + SmtKind::WriteData + } else { + SmtKind::ReadData + }; + let address_constraint = + isla_lib::memory::smt_address_constraint(regions, &addr_exp, bytes, kind, solver, None); + + let full_constraint = Exp::And(Box::new(address_constraint), Box::new(read_prop)); + + solver.add(Def::Assert(full_constraint)); + } + + fn symbolic_write( + &mut self, + regions: &[isla_lib::memory::Region], + solver: &mut Solver, + _value: Sym, + _read_kind: &Val, + address: &Val, + data: &Val, + bytes: u32, + _tag: &Option>, + _opts: &smt::WriteOpts, + ) { + use isla_lib::smt::smtlib::{Def, Exp}; + + let data_exp = smt_value(data) + .unwrap_or_else(|err| panic!("Bad memory write value {:?}: {}", data, err)); + let addr_exp = smt_value(address) + .unwrap_or_else(|err| panic!("Bad write address value {:?}: {}", address, err)); + // TODO: endianness? + let mut mem_exp = Exp::Store( + Box::new(Exp::Var(self.memory_var)), + Box::new(addr_exp.clone()), + Box::new(Exp::Extract(7, 0, Box::new(data_exp.clone()))), + ); + for i in 1..bytes { + mem_exp = Exp::Store( + Box::new(mem_exp), + Box::new(Exp::Bvadd( + Box::new(addr_exp.clone()), + Box::new(bits64(i as u64, 64)), + )), + Box::new(Exp::Extract(i * 8 + 7, i * 8, Box::new(data_exp.clone()))), + ) + } + self.memory_var = solver.fresh(); + solver.add(Def::DefineConst(self.memory_var, mem_exp)); + let kind = SmtKind::WriteData; + let address_constraint = + isla_lib::memory::smt_address_constraint(regions, &addr_exp, bytes, kind, solver, None); + solver.add(Def::Assert(address_constraint)); + } + + fn symbolic_write_tag( + &mut self, + _regions: &[isla_lib::memory::Region], + _solver: &mut Solver, + _value: Sym, + _write_kind: &Val, + _address: &Val, + _tag: &Val, + ) { + } +} + +fn smt_value(v: &Val) -> Result, ExecError> { + isla_lib::primop_util::smt_value(v, SourceLoc::unknown()) +} + +fn smt_read_exp(memory: Sym, addr_exp: &smtlib::Exp, bytes: u64) -> smtlib::Exp { + use smtlib::Exp; + // TODO: endianness? + let mut mem_exp = Exp::Select(Box::new(Exp::Var(memory)), Box::new(addr_exp.clone())); + for i in 1..bytes { + mem_exp = Exp::Concat( + Box::new(Exp::Select( + Box::new(Exp::Var(memory)), + Box::new(Exp::Bvadd( + Box::new(addr_exp.clone()), + Box::new(bits64(i as u64, 64)), + )), + )), + Box::new(mem_exp), + ) + } + mem_exp +} + +fn smt_bytes(bytes: &Vec) -> smtlib::Exp { + let mut bits = Vec::with_capacity(bytes.len() * 8); + for byte in bytes { + for i in 0..8 { + bits.push((byte >> i) & 1 == 1); + } + } + smtlib::Exp::Bits(bits) +} + +fn dump_checkpoint<'ir, B: BV>( + checkpoint: &Checkpoint, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result<()> { + if let Some(trace) = checkpoint.trace() { + let events: Vec> = trace.to_vec().into_iter().cloned().collect(); + write_events_to_stdout(&events, iarch)?; + } + Ok(()) +} + +/// Write ISLA trace events to stdout. +fn write_events_to_stdout<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, +) -> anyhow::Result<()> { + let stdout = std::io::stdout().lock(); + write_events(events, iarch, stdout) +} + +fn write_events<'ir, B: BV>( + events: &Vec>, + iarch: &'ir Initialized<'ir, B>, + w: impl Sized + Write, +) -> anyhow::Result<()> { + let mut handle = BufWriter::with_capacity(5 * usize::pow(2, 20), w); + let write_opts = WriteOpts::default(); + simplify::write_events_with_opts(&mut handle, &events, &iarch.shared_state, &write_opts) + .unwrap(); + handle.flush().unwrap(); + + Ok(()) +} + +/// Parse Jib IR. +fn parse_ir<'a, 'input, B: BV>( + contents: &'input str, + symtab: &'a mut Symtab<'input>, +) -> anyhow::Result>> { + match ir_parser::IrParser::new().parse(symtab, new_ir_lexer(&contents)) { + Ok(ir) => Ok(ir), + Err(_) => Err(anyhow::Error::msg("bad")), + } +} + +fn linearize_function<'ir, B: BV>( + arch: &mut Vec>, + name: &str, + symtab: &mut Symtab<'ir>, +) -> anyhow::Result<()> { + log!(log::VERBOSE, format!("linearize function {}", name)); + + // Lookup function name. + let target = match symtab.get(&zencode::encode(name)) { + Some(t) => t, + None => anyhow::bail!("function {} could not be found", name), + }; + + // Find signature. + let (_args, ret) = lookup_signature(arch, target)?; + + // Rewrite. + for def in arch.iter_mut() { + if let Def::Fn(f, _, body) = def { + if *f == target { + let rewritten = linearize::linearize(body.to_vec(), &ret, symtab); + *body = rewritten; + } + } + } + + Ok(()) +} + +fn lookup_signature( + arch: &Vec>, + target: Name, +) -> anyhow::Result<(Vec>, Ty)> { + for def in arch { + match def { + Def::Val(f, args, ret) if *f == target => return Ok((args.clone(), ret.clone())), + _ => (), + } + } + anyhow::bail!("could not find type signature") +} diff --git a/cranelift/isle/veri/veri_engine/tests/utils/mod.rs b/cranelift/isle/veri/veri_engine/tests/utils/mod.rs index ed87cfe81359..13f6d772a06c 100644 --- a/cranelift/isle/veri/veri_engine/tests/utils/mod.rs +++ b/cranelift/isle/veri/veri_engine/tests/utils/mod.rs @@ -231,6 +231,11 @@ pub fn test_aarch64_rule_with_lhs_termname(rulename: &str, termname: &str, tr: T .join("../../../codegen/src/isa/aarch64") .join("inst.isle"), ); + inputs.push( + cur_dir + .join("../../../codegen/src/isa/aarch64") + .join("inst_specs.isle"), + ); inputs.push( cur_dir .join("../../../codegen/src/isa/aarch64") diff --git a/cranelift/isle/veri/veri_engine/tests/veri.rs b/cranelift/isle/veri/veri_engine/tests/veri.rs index 2d5d00c68209..91253b7e0ebe 100644 --- a/cranelift/isle/veri/veri_engine/tests/veri.rs +++ b/cranelift/isle/veri/veri_engine/tests/veri.rs @@ -3200,6 +3200,32 @@ fn test_broken_imm_udiv_cve_underlying_32() { }) } +// ISA spec test: +// 1. add_alu_rrr lowers and to alu_rrr +// 2. alu_rrr lowers to MInst.AluRRR + +#[test] +fn test_named_add_alu_rrr() { + run_and_retry(|| { + test_aarch64_rule_with_lhs_termname_simple( + "add_alu_rrr", + "add", + vec![(Bitwidth::I64, VerificationResult::Success)], + ) + }) +} + +#[test] +fn test_named_alu_rrr_emit() { + run_and_retry(|| { + test_aarch64_rule_with_lhs_termname_simple( + "alu_rrr_emit", + "alu_rrr", + vec![(Bitwidth::I64, VerificationResult::Success)], + ) + }) +} + // x64 #[test]