Skip to content

MIR backend: Support nightly-2025-02-16 #2323

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 14 commits into
base: master
Choose a base branch
from
Draft

MIR backend: Support nightly-2025-02-16 #2323

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
b2c631d
Draft: Support verifying Rust 1.86
RyanGlScott May 6, 2025
f47baca
Fix remaining crux-mir-comp-test failures
RyanGlScott May 6, 2025
9b6f986
Adapt to mirRef_offsetSim losing a TypeRepr argument
RyanGlScott May 7, 2025
08f1899
Merge branch 'master' into saw-rust-1.86
RyanGlScott May 7, 2025
fb3fa42
Advertise mir-json schema version 2 support
RyanGlScott May 8, 2025
50f9d91
Account for lang_items from MIR JSON
RyanGlScott May 9, 2025
fe6fd84
Bump crucible, mir-json submodules
RyanGlScott May 9, 2025
0cdbe98
Bump crucible, mir-json submodules
RyanGlScott May 12, 2025
7536804
Docs: Use mir-json-translate-libs, not translate_libs.sh
RyanGlScott May 12, 2025
ffd2bda
intTests: Regenerate checked-in *.linked-mir.json files
RyanGlScott May 12, 2025
0e9489e
saw-python: Regenerate vendored-in *.linked-mir.json files
RyanGlScott May 12, 2025
31e8f99
Bump crucible, mir-json submodules
qsctr May 14, 2025
824d757
Bump mir-json submodule for dlmalloc
qsctr May 14, 2025
05ee92c
Bump crucible, mir-json submodules
RyanGlScott May 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
# next -- TBA

This release supports [version
2](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#2) of
`mir-json`'s schema.

The way git information gets compiled in (so it can be reported with
e.g. saw --version) has been changed.
You must build with build.sh after git changes for those changes to
Expand Down Expand Up @@ -36,6 +40,8 @@ Note that build.sh is in any case the recommended way to build.

* Support `bmux` gates in exported Yosys directly to avoid reliance on `bmuxmap`

* Support verifying Rust code up to version 1.86.

## Bug fixes

* The `head` and `tail` primitives are now implemented in the SAW-Core
Expand Down
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ compile Rust code using [`mir-json`](https://github.com/GaloisInc/mir-json), a
tool which compiles Rust code to a machine-readable, JSON-based format.

Currently, SAW supports [version
1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
2](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#2) 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:
Expand Down
4 changes: 2 additions & 2 deletions crucible-mir-comp/src/Mir/Compositional/Builder.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,7 @@ addArg tpr argRef msb =
svPairs <- forM [0 .. len - 1] $ \i -> do
-- Record a points-to entry
iSym <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral i
ref' <- lift $ mirRef_offsetSim (fr ^. frType) (fr ^. frRef) iSym
ref' <- lift $ mirRef_offsetSim (fr ^. frRef) iSym
rv <- lift $ readMirRefSim (fr ^. frType) ref'
let shp = tyToShapeEq col (fr ^. frMirType) (fr ^. frType)
sv <- regToSetup bak Pre (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
Expand Down Expand Up @@ -304,7 +304,7 @@ setReturn tpr argRef msb =
svs <- forM [0 .. len - 1] $ \i -> do
-- Record a points-to entry
iSym <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral i
ref' <- lift $ mirRef_offsetSim (fr ^. frType) (fr ^. frRef) iSym
ref' <- lift $ mirRef_offsetSim (fr ^. frRef) iSym
rv <- lift $ readMirRefSim (fr ^. frType) ref'
let shp = tyToShapeEq col (fr ^. frMirType) (fr ^. frType)
regToSetup bak Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv
Expand Down
4 changes: 2 additions & 2 deletions crucible-mir-comp/src/Mir/Compositional/Override.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
"impossible: alloc mentioned in csPointsTo is absent from csAllocs?"
forM_ (zip svs [0 .. len - 1]) $ \(sv, i) -> do
iSym <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral i
ref' <- lift $ mirRef_offsetSim (ptr ^. mpType) (ptr ^. mpRef) iSym
ref' <- lift $ mirRef_offsetSim (ptr ^. mpRef) iSym
rv <- lift $ readMirRefSim (ptr ^. mpType) ref'
let shp = tyToShapeEq col ty (ptr ^. mpType)
matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) md shp rv sv
Expand Down Expand Up @@ -328,7 +328,7 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->

forM_ (zip svs [0 .. len - 1]) $ \(sv, i) -> do
iSym <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral i
ref' <- mirRef_offsetSim (ptr ^. mpType) (ptr ^. mpRef) iSym
ref' <- mirRef_offsetSim (ptr ^. mpRef) iSym
rv <- liftIO $ setupToReg sym sc termSub w4VarMap allocMap shp sv
writeMirRefSim (ptr ^. mpType) ref' rv

Expand Down
4 changes: 2 additions & 2 deletions crux-mir-comp/test/symb_eval/comp/alias_array_bad.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ failures:
[Crux] test/symb_eval/comp/alias_array_bad.rs:45:5: 45:17: error: in alias_array_bad/<DISAMB>::use_f[0]
[Crux] references AllocIndex 0 and AllocIndex 1 must not overlap
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:37: error: in alias_array_bad/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:37: error: in alias_array_bad/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/alias_array_bad.rs:46:5:
[Crux] 0 < b[0].get()
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:38: error: in alias_array_bad/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:38: error: in alias_array_bad/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/alias_array_bad.rs:47:5:
[Crux] b[0].get() < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ failures:
[Crux] test/symb_eval/comp/alias_array_bad2.rs:45:5: 45:17: error: in alias_array_bad2/<DISAMB>::use_f[0]
[Crux] references AllocIndex 0 and AllocIndex 1 must not overlap
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:38: error: in alias_array_bad2/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:38: error: in alias_array_bad2/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/alias_array_bad2.rs:47:5:
[Crux] b[0].get() < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/alias_array_ok.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- alias_array_ok/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:38: error: in alias_array_ok/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:38: error: in alias_array_ok/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/alias_array_ok.rs:48:5:
[Crux] b[0].get() < 10

Expand Down
4 changes: 2 additions & 2 deletions crux-mir-comp/test/symb_eval/comp/alias_bad.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ failures:
[Crux] test/symb_eval/comp/alias_bad.rs:45:5: 45:14: error: in alias_bad/<DISAMB>::use_f[0]
[Crux] references AllocIndex 0 and AllocIndex 1 must not overlap
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/alias_bad.rs:46:5: 46:34: error: in alias_bad/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/alias_bad.rs:46:5: 46:34: error: in alias_bad/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/alias_bad.rs:46:5:
[Crux] 0 < b.get()
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/alias_bad.rs:47:5: 47:35: error: in alias_bad/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/alias_bad.rs:47:5: 47:35: error: in alias_bad/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/alias_bad.rs:47:5:
[Crux] b.get() < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/alias_ok.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- alias_ok/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/alias_ok.rs:49:5: 49:35: error: in alias_ok/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/alias_ok.rs:49:5: 49:35: error: in alias_ok/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/alias_ok.rs:49:5:
[Crux] b.get() < 10

Expand Down
4 changes: 2 additions & 2 deletions crux-mir-comp/test/symb_eval/comp/clobber_globals.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,13 +5,13 @@ failures:

---- clobber_globals/<DISAMB>::f_test[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/clobber_globals.rs:15:5: 16:71: error: in clobber_globals/<DISAMB>::f_test[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/clobber_globals.rs:15:5: 16:71: error: in clobber_globals/<DISAMB>::f_test[0]
[Crux] MIR assertion at test/symb_eval/comp/clobber_globals.rs:15:5:
[Crux] expected failure; ATOMIC was clobbered by clobber_globals()

---- clobber_globals/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/clobber_globals.rs:37:5: 38:62: error: in clobber_globals/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/clobber_globals.rs:37:5: 38:62: error: in clobber_globals/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/clobber_globals.rs:37:5:
[Crux] expected failure; ATOMIC was clobbered by f's spec

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/override_test_indep.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ failures:

---- override_test_indep/<DISAMB>::use_f2[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:29: error: in override_test_indep/<DISAMB>::use_f2[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:29: error: in override_test_indep/<DISAMB>::use_f2[0]
[Crux] MIR assertion at test/symb_eval/comp/override_test_indep.rs:57:5:
[Crux] d < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/ptr_offset.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- ptr_offset/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:30: error: in ptr_offset/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:30: error: in ptr_offset/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/ptr_offset.rs:64:5:
[Crux] b2 < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- ptr_offset_rev/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:30: error: in ptr_offset_rev/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:30: error: in ptr_offset_rev/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/ptr_offset_rev.rs:64:5:
[Crux] b2 < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/spec_array.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- spec_array/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/spec_array.rs:43:5: 43:29: error: in spec_array/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/spec_array.rs:43:5: 43:29: error: in spec_array/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/spec_array.rs:43:5:
[Crux] d < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/spec_box.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- spec_box/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/spec_box.rs:58:5: 58:29: error: in spec_box/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/spec_box.rs:58:5: 58:29: error: in spec_box/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/spec_box.rs:58:5:
[Crux] d < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- spec_immut_cell/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:35: error: in spec_immut_cell/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:35: error: in spec_immut_cell/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/spec_immut_cell.rs:68:5:
[Crux] d.get() < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/spec_mut.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- spec_mut/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/spec_mut.rs:61:5: 61:29: error: in spec_mut/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/spec_mut.rs:61:5: 61:29: error: in spec_mut/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/spec_mut.rs:61:5:
[Crux] d < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- spec_mut_slice/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:29: error: in spec_mut_slice/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:29: error: in spec_mut_slice/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/spec_mut_slice.rs:48:5:
[Crux] d < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/spec_struct.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- spec_struct/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/spec_struct.rs:51:5: 51:29: error: in spec_struct/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/spec_struct.rs:51:5: 51:29: error: in spec_struct/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/spec_struct.rs:51:5:
[Crux] d < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/spec_tuple.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ failures:

---- spec_tuple/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:29: error: in spec_tuple/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:29: error: in spec_tuple/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/spec_tuple.rs:55:5:
[Crux] d < 10

Expand Down
2 changes: 1 addition & 1 deletion crux-mir-comp/test/symb_eval/comp/subst_output.good
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ failures:

---- subst_output/<DISAMB>::use_f[0] counterexamples ----
[Crux] Found counterexample for verification goal
[Crux] ./libs/crucible/lib.rs:41:9: 41:79 !test/symb_eval/comp/subst_output.rs:32:5: 32:30: error: in subst_output/<DISAMB>::use_f[0]
[Crux] ./libs/crucible/lib.rs:44:9: 44:79 !test/symb_eval/comp/subst_output.rs:32:5: 32:30: error: in subst_output/<DISAMB>::use_f[0]
[Crux] MIR assertion at test/symb_eval/comp/subst_output.rs:32:5:
[Crux] b0 == a

Expand Down
2 changes: 1 addition & 1 deletion deps/crucible
Open in desktop
Submodule crucible updated 71 files
+3 −3 .github/Dockerfile-crux-mir
+3 −3 .github/workflows/crux-mir-build.yml
+2 −1 crucible-mir/CHANGELOG.md
+31 −20 crucible-mir/src/Mir/Generator.hs
+1 −0 crucible-mir/src/Mir/GenericOps.hs
+19 −16 crucible-mir/src/Mir/Intrinsics.hs
+95 −53 crucible-mir/src/Mir/JSON.hs
+84 −33 crucible-mir/src/Mir/Mir.hs
+13 −4 crucible-mir/src/Mir/PP.hs
+2 −2 crucible-mir/src/Mir/ParseTranslate.hs
+1 −1 crucible-mir/src/Mir/Pass/AllocateEnum.hs
+392 −126 crucible-mir/src/Mir/Trans.hs
+118 −58 crucible-mir/src/Mir/TransCustom.hs
+10 −8 crucible-mir/src/Mir/TransTy.hs
+5 −0 crux-mir/CHANGELOG.md
+1 −1 crux-mir/README.md
+1 −0 crux-mir/libs
+1 −0 crux-mir/rust-toolchain.toml
+43 −34 crux-mir/src/Mir/Generate.hs
+3 −3 crux-mir/src/Mir/Language.hs
+2 −2 crux-mir/src/Mir/Overrides.hs
+1 −6 crux-mir/test/conc_eval/array/wick1.rs
+1 −5 crux-mir/test/conc_eval/array/wick3.rs
+0 −2 crux-mir/test/conc_eval/box/struct.rs
+26 −0 crux-mir/test/conc_eval/box/subtype.rs
+13 −0 crux-mir/test/conc_eval/cell/from_mut.rs
+15 −0 crux-mir/test/conc_eval/cell/slice.rs
+17 −0 crux-mir/test/conc_eval/cell/slice_from_mut.rs
+14 −0 crux-mir/test/conc_eval/cell/swap.rs
+0 −2 crux-mir/test/conc_eval/clos/as_fn_ptr.rs
+11 −0 crux-mir/test/conc_eval/clos/closure_to_fn_ptr_const.rs
+1 −3 crux-mir/test/conc_eval/clos/fo.rs
+1 −1 crux-mir/test/conc_eval/fnptr/custom.rs
+23 −0 crux-mir/test/conc_eval/hash_map/insert_get_disjoint_mut.rs
+12 −0 crux-mir/test/conc_eval/mem/bswap_integral.rs
+12 −0 crux-mir/test/conc_eval/mem/transmute_bytes.rs
+32 −0 crux-mir/test/conc_eval/num/ctpop.rs
+9 −0 crux-mir/test/conc_eval/num/from_bytes.rs
+13 −0 crux-mir/test/conc_eval/num/overflow_usize.rs
+16 −0 crux-mir/test/conc_eval/prim/bool_then.rs
+0 −22 crux-mir/test/conc_eval/prim/shift_exceeding.rs
+1 −2 crux-mir/test/conc_eval/ptr/is_null_slice.rs
+14 −0 crux-mir/test/conc_eval/ptr/unsize_slice_null.rs
+1 −1 crux-mir/test/coverage/coverage.good
+3 −3 crux-mir/test/coverage/coverage_cond.good
+36 −0 crux-mir/test/coverage/coverage_loop.good
+6 −6 crux-mir/test/coverage/coverage_macro.good
+4 −4 crux-mir/test/coverage/coverage_macro.rs
+6 −6 crux-mir/test/coverage/coverage_match.good
+1 −7 crux-mir/test/coverage/coverage_shortcircuit.good
+2 −2 crux-mir/test/coverage/coverage_try.good
+1 −1 crux-mir/test/symb_eval/bytes/put_overflow.good
+1 −1 crux-mir/test/symb_eval/concretize/assert.good
+2 −2 crux-mir/test/symb_eval/crux/early_fail.good
+4 −4 crux-mir/test/symb_eval/crux/fail_return.good
+4 −4 crux-mir/test/symb_eval/crux/mixed_fail.good
+4 −4 crux-mir/test/symb_eval/crux/multi.good
+5 −5 crux-mir/test/symb_eval/crypto/bytes.good
+1 −1 crux-mir/test/symb_eval/num/checked_add.good
+3 −3 crux-mir/test/symb_eval/num/checked_div.good
+1 −1 crux-mir/test/symb_eval/num/checked_mul.good
+1 −1 crux-mir/test/symb_eval/num/checked_mul_signed.good
+10 −0 crux-mir/test/symb_eval/num/checked_shift.good
+11 −0 crux-mir/test/symb_eval/num/checked_shift.rs
+1 −1 crux-mir/test/symb_eval/overrides/bad_symb1.good
+1 −1 crux-mir/test/symb_eval/overrides/bad_symb2.good
+1 −1 crux-mir/test/symb_eval/overrides/override2.good
+1 −1 crux-mir/test/symb_eval/overrides/override5.good
+1 −1 crux-mir/test/symb_eval/sym_bytes/construct.good
+1 −1 crux-mir/test/symb_eval/sym_bytes/deserialize.good
+1 −1 dependencies/mir-json
2 changes: 1 addition & 1 deletion deps/mir-json
Open in desktop
Submodule mir-json updated 2762 files
Binary file modified doc/pdfs/rust-verification-with-saw.pdf
View file
Open in desktop
Binary file not shown.
Binary file modified doc/pdfs/saw-user-manual.pdf
View file
Open in desktop
Binary file not shown.
4 changes: 2 additions & 2 deletions doc/rust-verification-with-saw/about-mir-json.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,10 +103,10 @@ libraries is to perform the following steps:
instructions](https://github.com/GaloisInc/mir-json#installation-instructions)
in order to install `mir-json`.

3. Run the `translate_libs.sh` script:
3. Run the `mir-json-translate-libs` utility:

:::{code-block} console
$ ./translate_libs.sh
$ mir-json-translate-libs
:::

This will compile the custom versions of the Rust standard libraries using
Expand Down
4 changes: 2 additions & 2 deletions doc/saw-user-manual/loading-code.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,10 +154,10 @@ following steps:
instructions](https://github.com/GaloisInc/mir-json#installation-instructions)
in order to install `mir-json`.

4. Run the `translate_libs.sh` script in the `mir-json` submodule:
4. Run the `mir-json-translate-libs` script in the `mir-json` submodule:

:::{code-block} console
$ ./translate_libs.sh
$ mir-json-translate-libs
:::

This will compile the custom versions of the Rust standard libraries using
Expand Down
2 changes: 1 addition & 1 deletion intTests/test1973/test.linked-mir.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"version":1,"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::72fda5b91c47396c"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::72fda5b91c47396c"}},"pos":"test.rs:5:5: 5:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::72fda5b91c47396c"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::72fda5b91c47396c"}]},"name":"test/0d75de25::f","return_ty":"ty::Ref::72fda5b91c47396c","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/0d75de25::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/0d75de25::S","orig_substs":[],"repr_transparent":true,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/0d75de25::S::0","ty":"ty::u8"}],"inhabited":true,"name":"test/0d75de25::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/0d75de25::f","kind":"Item","substs":[]},"name":"test/0d75de25::f"}],"tys":[{"name":"ty::Adt::a8a1a3466e211b44","ty":{"kind":"Adt","name":"test/0d75de25::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/0d75de25::S","substs":[]}},{"name":"ty::Ref::72fda5b91c47396c","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::a8a1a3466e211b44"}},{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}}],"roots":["test/0d75de25::f"]}
{"version":2,"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::a1598f0a5cd0010b"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::a1598f0a5cd0010b"}},"pos":"test.rs:5:5: 5:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::a1598f0a5cd0010b"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::a1598f0a5cd0010b"}]},"name":"test/6c2ff28f::f","return_ty":"ty::Ref::a1598f0a5cd0010b","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/6c2ff28f::S::_adtc5a5405abab57fd5[0]","orig_args":[],"orig_def_id":"test/6c2ff28f::S","repr_transparent":true,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/6c2ff28f::S::0","ty":"ty::u8"}],"inhabited":true,"name":"test/6c2ff28f::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"args":[],"def_id":"test/6c2ff28f::f","kind":"Item"},"name":"test/6c2ff28f::f"}],"tys":[{"name":"ty::Adt::10a8d3b99e1d4d09","ty":{"args":[],"kind":"Adt","name":"test/6c2ff28f::S::_adtc5a5405abab57fd5[0]","orig_def_id":"test/6c2ff28f::S"}},{"name":"ty::Ref::a1598f0a5cd0010b","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::10a8d3b99e1d4d09"}},{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}}],"lang_items":[],"roots":["test/6c2ff28f::f"]}
4 changes: 2 additions & 2 deletions intTests/test1998_mir/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# The current checked-in linked-mir.json file was generated by:
# rustc 1.69.0-nightly (5e37043d6 2023-01-22)
# mir-json c52b16bf26af2f5b98157ebf9975aa0021982bbc from 2024-09-11
# rustc 1.86.0-nightly (9cd60bd2c 2025-02-15)
# mir-json 7524ae4842a380b37785c1994f4aed147db162ca from 2025-05-11

all: test.linked-mir.json

Expand Down
2 changes: 1 addition & 1 deletion intTests/test1998_mir/test.linked-mir.json
View file
Open in desktop

Large diffs are not rendered by default.

Loading
Loading