diff --git a/.github/Dockerfile-crux-mir b/.github/Dockerfile-crux-mir index 4dc5231c4..b580a9b5f 100644 --- a/.github/Dockerfile-crux-mir +++ b/.github/Dockerfile-crux-mir @@ -1,6 +1,6 @@ # If you update this, make sure to also update RUST_TOOLCHAIN in # .github/workflows/crux-mir-build.yml -ARG RUST_TOOLCHAIN="nightly-2025-02-16" +ARG RUST_TOOLCHAIN="nightly-2025-09-14" ARG CRUX_BUILD_DIR=/crux-mir/build # Note that we intentionally do not use ubuntu:24.04 or later pending a diff --git a/.github/workflows/crux-mir-build.yml b/.github/workflows/crux-mir-build.yml index c51b5048d..1efe76a40 100644 --- a/.github/workflows/crux-mir-build.yml +++ b/.github/workflows/crux-mir-build.yml @@ -29,7 +29,7 @@ env: CARGO_CACHE_VERSION: 1 # If you update this, make sure to also update RUST_TOOLCHAIN in # .github/Dockerfile-crux-mir - RUST_TOOLCHAIN: "nightly-2025-02-16" + RUST_TOOLCHAIN: "nightly-2025-09-14" jobs: config: diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md index bd30f4262..521fb74f1 100644 --- a/crucible-mir/CHANGELOG.md +++ b/crucible-mir/CHANGELOG.md @@ -1,9 +1,10 @@ # next This release supports [version -5](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#5) of +6](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#6) of `mir-json`'s schema. +* Support simulating Rust code up to version 1.91. * Add an intrinsic for [`needs_drop`](https://doc.rust-lang.org/std/intrinsics/fn.needs_drop.html). * `TyConst` now has a `ConstVal` field to indicate the value of the constant used to instantiate a const generic parameter. This has no impact on the diff --git a/crucible-mir/src/Mir/JSON.hs b/crucible-mir/src/Mir/JSON.hs index 761895b7d..918d0aba3 100644 --- a/crucible-mir/src/Mir/JSON.hs +++ b/crucible-mir/src/Mir/JSON.hs @@ -266,7 +266,6 @@ instance FromJSON Fn where instance FromJSON Abi where parseJSON = withObject "Abi" $ \v -> case lookupKM "kind" v of Just (String "Rust") -> pure RustAbi - Just (String "RustIntrinsic") -> pure RustIntrinsic -- For `RustCall`, defaut to `RcNoBody`. The spread_arg info will be -- added while parsing the `Fn`, if this `Abi` is part of a `Fn`'s -- signature. diff --git a/crucible-mir/src/Mir/Mir.hs b/crucible-mir/src/Mir/Mir.hs index d81e52f9b..dabdd08ef 100644 --- a/crucible-mir/src/Mir/Mir.hs +++ b/crucible-mir/src/Mir/Mir.hs @@ -157,7 +157,6 @@ data FnSig = FnSig { data Abi = RustAbi | RustCall RustCallBodyInfo - | RustIntrinsic | OtherAbi deriving (Show, Eq, Ord, Generic) diff --git a/crucible-mir/src/Mir/ParseTranslate.hs b/crucible-mir/src/Mir/ParseTranslate.hs index c77470cad..b301c5d83 100644 --- a/crucible-mir/src/Mir/ParseTranslate.hs +++ b/crucible-mir/src/Mir/ParseTranslate.hs @@ -48,7 +48,7 @@ import Debug.Trace -- If you update the supported mir-json schema version below, make sure to also -- update the crux-mir README accordingly. supportedSchemaVersion :: Word64 -supportedSchemaVersion = 5 +supportedSchemaVersion = 6 -- | Parse a MIR JSON file to a 'Collection'. If parsing fails, attempt to give -- a more informative error message if the MIR JSON schema version is diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index 0e707b38e..1458b41da 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -31,6 +31,7 @@ module Mir.Trans(transCollection,transStatics,RustModule(..) , evalOperand , vectorCopy, aggregateCopy_constLen , ptrCopy, copyNonOverlapping + , isNonOverlapping , evalRval , callExp , callHandle @@ -3212,9 +3213,6 @@ copyNonOverlapping :: R.Expr MIR s UsizeType -> MirGenerator h s ret (MirExp s) copyNonOverlapping tpr src dest count = do - -- Assert that the two regions really are nonoverlapping. - maybeOffset <- mirRef_tryOffsetFrom dest src - -- `count` must not exceed isize::MAX, else the overlap check -- will misbehave. let sizeBits = fromIntegral $ C.intValue (C.knownNat @SizeBits) @@ -3222,21 +3220,32 @@ copyNonOverlapping tpr src dest count = do let countOk = R.App $ usizeLt count maxCount G.assertExpr countOk $ S.litExpr "count overflow in copy_nonoverlapping" - -- If `maybeOffset` is Nothing, then src and dest definitely - -- don't overlap, since they come from different allocations. - -- If it's Just, the value must be >= count or <= -count to put - -- the two regions far enough apart. - let count' = usizeToIsize R.App count - let destAbove = \offset -> R.App $ isizeLe count' offset - let destBelow = \offset -> R.App $ isizeLe offset (R.App $ isizeNeg count') - offsetOk <- G.caseMaybe maybeOffset C.BoolRepr $ G.MatchMaybe - (\offset -> return $ R.App $ E.Or (destAbove offset) (destBelow offset)) - (return $ R.App $ E.BoolLit True) - G.assertExpr offsetOk $ S.litExpr "src and dest overlap in copy_nonoverlapping" + nonOverlapping <- isNonOverlapping src dest count + G.assertExpr nonOverlapping $ S.litExpr "src and dest overlap in copy_nonoverlapping" ptrCopy tpr src dest count return $ MirExp C.UnitRepr $ R.App E.EmptyApp +-- | Check if two allocations of the given size are non-overlapping. +-- Assumes @size <= isize::MAX@. +isNonOverlapping :: + R.Expr MIR s MirReferenceType -> + R.Expr MIR s MirReferenceType -> + R.Expr MIR s UsizeType -> + MirGenerator h s ret (G.Expr MIR s C.BoolType) +isNonOverlapping src dest size = do + maybeOffset <- mirRef_tryOffsetFrom dest src + -- If `maybeOffset` is Nothing, then src and dest definitely + -- don't overlap, since they come from different allocations. + -- If it's Just, the value must be >= size or <= -size to put + -- the two regions far enough apart. + let size' = usizeToIsize R.App size + destAbove offset = R.App $ isizeLe size' offset + destBelow offset = R.App $ isizeLe offset (R.App $ isizeNeg size') + G.caseMaybe maybeOffset C.BoolRepr $ G.MatchMaybe + (\offset -> return $ R.App $ E.Or (destAbove offset) (destBelow offset)) + (return $ R.App $ E.BoolLit True) + -- LocalWords: params IndexMut FnOnce Fn IntoIterator iter impl -- LocalWords: tovec fromelem tmethsubst MirExp initializer callExp -- LocalWords: mkTraitObject mkCustomTraitObject TyClosure diff --git a/crucible-mir/src/Mir/TransCustom.hs b/crucible-mir/src/Mir/TransCustom.hs index 354f36e29..ecb3e4062 100644 --- a/crucible-mir/src/Mir/TransCustom.hs +++ b/crucible-mir/src/Mir/TransCustom.hs @@ -179,6 +179,8 @@ customOpDefs = Map.fromList $ [ , intrinsics_copy , intrinsics_copy_nonoverlapping + , cell_swap_is_nonoverlapping + , exit , abort , panicking_begin_panic @@ -761,6 +763,21 @@ intrinsics_copy_nonoverlapping = ( ["core", "intrinsics", "copy_nonoverlapping"] _ -> mirFail $ "bad arguments for intrinsics::copy_nonoverlapping: " ++ show ops _ -> Nothing) +cell_swap_is_nonoverlapping :: (ExplodedDefId, CustomRHS) +cell_swap_is_nonoverlapping = + ( ["core", "cell", "{impl}", "swap", "crucible_cell_swap_is_nonoverlapping_hook"] + , \case + Substs [ty] -> Just $ CustomOp $ \_ ops -> case ops of + [MirExp MirReferenceRepr src, + MirExp MirReferenceRepr dest] -> do + size <- getLayoutFieldAsExpr "crucible_cell_swap_is_nonoverlapping_hook" laySize ty + MirExp C.BoolRepr <$> isNonOverlapping src dest size + _ -> mirFail $ + "bad arguments for Cell::swap::crucible_cell_swap_is_nonoverlapping_hook: " + ++ show ops + _ -> Nothing + ) + ----------------------------------------------------------------------------------------------------- -- ** Custom: wrapping_mul diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md index a1e450b68..066c39ac7 100644 --- a/crux-mir/CHANGELOG.md +++ b/crux-mir/CHANGELOG.md @@ -1,9 +1,11 @@ # next This release supports [version -5](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#5) of +6](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#6) of `mir-json`'s schema. +* Support simulating Rust code up to version 1.91. + # 0.11 -- 2025-11-09 This release supports [version diff --git a/crux-mir/README.md b/crux-mir/README.md index 0cbfd9849..9fec415eb 100644 --- a/crux-mir/README.md +++ b/crux-mir/README.md @@ -49,7 +49,7 @@ Next, navigate to the `crucible/dependencies/mir-json` directory. Install [the `mir-json` README][mir-json-readme]. Currently, `crux-mir` supports [version -5](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#5) of +6](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#6) of `mir-json`'s schema. Note that the schema versions produced by `mir-json` can change over time as dictated by internal requirements and upstream changes. To help smooth this over: diff --git a/crux-mir/src/Mir/Generate.hs b/crux-mir/src/Mir/Generate.hs index 9530ee9fe..91224835c 100644 --- a/crux-mir/src/Mir/Generate.hs +++ b/crux-mir/src/Mir/Generate.hs @@ -16,6 +16,7 @@ module Mir.Generate(generateMIR) where import Control.Monad (when) +import Data.List (stripPrefix) import qualified Data.ByteString.Lazy as B import qualified Data.ByteString as BS @@ -25,7 +26,7 @@ import System.FilePath import System.IO import qualified System.Process as Proc import System.Exit (ExitCode(..)) -import System.Directory (doesFileExist, removeFile, getModificationTime) +import System.Directory (doesFileExist, removeFile, getModificationTime, listDirectory) import Data.Time.Clock (UTCTime) import GHC.Stack @@ -69,6 +70,7 @@ compileMirJson cruxOpts keepRlib rustFile = do let outFile = rustFile -<.> "bin" rlibsDir <- getRlibsDir + rlibsFiles <- listDirectory rlibsDir -- rustc produces colorful error messages, so preserve the colors whenever -- possible when printing the error messages back out to the user. let colorOpts @@ -81,10 +83,11 @@ compileMirJson cruxOpts keepRlib rustFile = do Proc.proc "mir-json" $ [rustFile, "-L", rlibsDir, "--crate-type=rlib", "--edition=2021"] ++ concat - [ [ "--extern" - , lib ++ "=" ++ rlibsDir "lib" ++ lib <.> "rlib" - ] - | lib <- libDependencies ] ++ + [ ["--extern", libName ++ "=" ++ rlibsDir file] + | file <- rlibsFiles + , (baseName, ".rlib") <- [splitExtension file] + , Just libName <- [stripPrefix "lib" baseName] + ] ++ colorOpts ++ [ "--cfg", "crux", "--cfg", "crux_top_level" , "-Z", "ub-checks=false" @@ -144,42 +147,6 @@ maybeLinkJson jsonFiles cacheFile = do else B.readFile cacheFile -libDependencies :: [FilePath] -libDependencies = - -- std and its dependencies - [ "addr2line" - , "adler2" - , "alloc" - , "cfg_if" - , "compiler_builtins" - , "core" - , "crucible" - , "getopts" - , "gimli" - , "hashbrown" - , "libc" - , "memchr" - , "miniz_oxide" - , "object" - , "panic_abort" - , "panic_unwind" - , "proc_macro" - , "rustc_demangle" - , "rustc_std_workspace_alloc" - , "rustc_std_workspace_core" - , "rustc_std_workspace_std" - , "std_detect" - , "std" - , "test" - , "unicode_width" - , "unwind" - -- additional libs - , "crucible" - , "int512" - , "byteorder" - , "bytes" - ] - -- | Run mir-json on the input, generating lib file on disk -- NOTE: If the rust file has not been modified since the @@ -197,7 +164,8 @@ generateMIR cruxOpts inputFile keepRlib let rustFile = inputFile maybeCompileMirJson cruxOpts keepRlib rustFile rlibsDir <- getRlibsDir - let libJsonPaths = [rlibsDir "lib" ++ lib <.> "mir" | lib <- libDependencies] + rlibsFiles <- listDirectory rlibsDir + let libJsonPaths = [rlibsDir file | file <- rlibsFiles, takeExtension file == ".mir"] b <- maybeLinkJson (mirJsonOutFile rustFile : libJsonPaths) (linkOutFile rustFile) parseMIR (linkOutFile rustFile) b | ext == ".json" = do diff --git a/crux-mir/test/conc_eval/hash_map/extract_if.rs b/crux-mir/test/conc_eval/hash_map/extract_if.rs new file mode 100644 index 000000000..c2977a6f2 --- /dev/null +++ b/crux-mir/test/conc_eval/hash_map/extract_if.rs @@ -0,0 +1,17 @@ +use std::collections::HashMap; +use std::convert::TryInto; + +#[cfg_attr(crux, crux::test)] +fn crux_test() -> ([i32; 4], [i32; 4]) { + let mut map: HashMap = (0..8).map(|x| (x, x)).collect(); + let extracted: HashMap = map.extract_if(|k, _v| k % 2 == 0).collect(); + let mut evens = extracted.keys().copied().collect::>(); + let mut odds = map.keys().copied().collect::>(); + evens.sort(); + odds.sort(); + (evens.try_into().unwrap(), odds.try_into().unwrap()) +} + +pub fn main() { + println!("{:?}", crux_test()); +} diff --git a/crux-mir/test/conc_eval/num/cmp.rs b/crux-mir/test/conc_eval/num/cmp.rs new file mode 100644 index 000000000..d1b63f939 --- /dev/null +++ b/crux-mir/test/conc_eval/num/cmp.rs @@ -0,0 +1,8 @@ +use std::cmp::Ordering; + +#[cfg_attr(crux, crux::test)] +pub fn crux_test() -> Ordering { + 1.cmp(&2) +} + +pub fn main() { println!("{:?}", crux_test()); } diff --git a/crux-mir/test/conc_eval/rc/rc_basic.rs b/crux-mir/test/conc_eval/rc/rc_basic.rs index 53e71c604..02316bf9c 100644 --- a/crux-mir/test/conc_eval/rc/rc_basic.rs +++ b/crux-mir/test/conc_eval/rc/rc_basic.rs @@ -1,4 +1,4 @@ -// FAIL: `Rc` uses `mem::size_of_val` +// FAIL: `Rc` uses `mem::align_of_val` use std::rc::Rc; #[cfg_attr(crux, crux::test)] diff --git a/crux-mir/test/conc_eval/vec/try_into_array.rs b/crux-mir/test/conc_eval/vec/try_into_array.rs new file mode 100644 index 000000000..0432d650b --- /dev/null +++ b/crux-mir/test/conc_eval/vec/try_into_array.rs @@ -0,0 +1,10 @@ +use std::convert::TryInto; + +#[cfg_attr(crux, crux::test)] +fn test() -> Result<[i32; 4], Vec> { + vec![1, 2, 3, 4].try_into() +} + +fn main() { + println!("{:?}", test()); +} diff --git a/crux-mir/test/symb_eval/bytes/put_overflow.good b/crux-mir/test/symb_eval/bytes/put_overflow.good index 03706b848..d20e0e470 100644 --- a/crux-mir/test/symb_eval/bytes/put_overflow.good +++ b/crux-mir/test/symb_eval/bytes/put_overflow.good @@ -5,7 +5,7 @@ failures: ---- put_overflow/::f[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/panic.rs:107:9: 107:73 !./libs/bytes.rs:201:9: 202:49: error: in bytes/::{impl#4}[0]::put_slice[0] +[Crux] ./libs/core/src/panic.rs:62:9: 62:73 !./libs/bytes.rs:201:9: 202:49: error: in bytes/::{impl#4}[0]::put_slice[0] [Crux] panicking::panic_fmt, called from bytes/::{impl#4}[0]::put_slice[0] [Crux-MIR] ---- FINAL RESULTS ---- diff --git a/crux-mir/test/symb_eval/crux/early_fail.good b/crux-mir/test/symb_eval/crux/early_fail.good index 3c1415f36..6d81f5b30 100644 --- a/crux-mir/test/symb_eval/crux/early_fail.good +++ b/crux-mir/test/symb_eval/crux/early_fail.good @@ -7,7 +7,7 @@ failures: ---- early_fail/::fail1[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/panic.rs:107:9: 107:73 !test/symb_eval/crux/early_fail.rs:11:5: 11:20: error: in early_fail/::fail1[0] +[Crux] ./libs/core/src/panic.rs:62:9: 62:73 !test/symb_eval/crux/early_fail.rs:11:5: 11:20: error: in early_fail/::fail1[0] [Crux] panicking::panic_fmt, called from early_fail/::fail1[0] ---- early_fail/::fail2[0] counterexamples ---- diff --git a/crux-mir/test/symb_eval/crux/multi.good b/crux-mir/test/symb_eval/crux/multi.good index 281d1cc10..df2579a0f 100644 --- a/crux-mir/test/symb_eval/crux/multi.good +++ b/crux-mir/test/symb_eval/crux/multi.good @@ -18,7 +18,7 @@ failures: ---- multi/::fail2[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/panic.rs:107:9: 107:73 !test/symb_eval/crux/multi.rs:15:9: 15:22: error: in multi/::fail2[0] +[Crux] ./libs/core/src/panic.rs:62:9: 62:73 !test/symb_eval/crux/multi.rs:15:9: 15:22: error: in multi/::fail2[0] [Crux] panicking::panic_fmt, called from multi/::fail2[0] ---- multi/::fail3[0] counterexamples ---- diff --git a/crux-mir/test/symb_eval/num/unchecked_arith.good b/crux-mir/test/symb_eval/num/unchecked_arith.good index b3fed2c3c..1b919f586 100644 --- a/crux-mir/test/symb_eval/num/unchecked_arith.good +++ b/crux-mir/test/symb_eval/num/unchecked_arith.good @@ -13,27 +13,27 @@ failures: ---- unchecked_arith/::add_test[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/num/uint_macros.rs:572:17: 572:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/::num[0]::{impl#6}[0]::unchecked_add[0] +[Crux] ./libs/core/src/num/uint_macros.rs:717:17: 717:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/::num[0]::{impl#6}[0]::unchecked_add[0] [Crux] Binary operation (+) would overflow ---- unchecked_arith/::mul_test[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/num/uint_macros.rs:945:17: 945:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/::num[0]::{impl#6}[0]::unchecked_mul[0] +[Crux] ./libs/core/src/num/uint_macros.rs:1105:17: 1105:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/::num[0]::{impl#6}[0]::unchecked_mul[0] [Crux] Binary operation (*) would overflow ---- unchecked_arith/::shl_test[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/num/uint_macros.rs:1558:17: 1558:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/::num[0]::{impl#6}[0]::unchecked_shl[0] +[Crux] ./libs/core/src/num/uint_macros.rs:1794:17: 1794:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/::num[0]::{impl#6}[0]::unchecked_shl[0] [Crux] Binary operation (<<) would overflow ---- unchecked_arith/::shr_test[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/num/uint_macros.rs:1679:17: 1679:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/::num[0]::{impl#6}[0]::unchecked_shr[0] +[Crux] ./libs/core/src/num/uint_macros.rs:1966:17: 1966:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/::num[0]::{impl#6}[0]::unchecked_shr[0] [Crux] Binary operation (>>) would overflow ---- unchecked_arith/::sub_test[0] counterexamples ---- [Crux] Found counterexample for verification goal -[Crux] ./libs/core/src/num/uint_macros.rs:762:17: 762:53 !./libs/core/src/num/mod.rs:436:5: 454:6: error: in core/::num[0]::{impl#6}[0]::unchecked_sub[0] +[Crux] ./libs/core/src/num/uint_macros.rs:896:17: 896:53 !./libs/core/src/num/mod.rs:447:5: 468:6: error: in core/::num[0]::{impl#6}[0]::unchecked_sub[0] [Crux] Binary operation (-) would overflow [Crux-MIR] ---- FINAL RESULTS ---- diff --git a/crux-mir/test/symb_eval/scalar/test1.good b/crux-mir/test/symb_eval/scalar/test1.good index 683bb6761..0ee0ba263 100644 --- a/crux-mir/test/symb_eval/scalar/test1.good +++ b/crux-mir/test/symb_eval/scalar/test1.good @@ -3,8 +3,8 @@ ok [Crux-MIR] ---- FINAL RESULTS ---- [Crux] Goal status: -[Crux] Total: 84 -[Crux] Proved: 84 +[Crux] Total: 77 +[Crux] Proved: 77 [Crux] Disproved: 0 [Crux] Incomplete: 0 [Crux] Unknown: 0 diff --git a/dependencies/mir-json b/dependencies/mir-json index d3b9e2338..c85c03d1b 160000 --- a/dependencies/mir-json +++ b/dependencies/mir-json @@ -1 +1 @@ -Subproject commit d3b9e2338064dcca9abc4824821c6613c3db5107 +Subproject commit c85c03d1bda4fdc2d3708818107695f7cd03a60f