Skip to content
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.

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

crux-mir: Support nightly-2023-01-23 #1096

Merged
merged 114 commits into from
Jul 14, 2023
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
114 commits
Select commit Hold shift + click to select a range
73df4f6
Normalize naming and organization of rust crates
m10f Mar 2, 2023
b121efe
WIP mir-json
m10f Mar 11, 2023
b4f6235
[WIP] more bugfixes
m10f Mar 16, 2023
82c3cd0
Update `mir-json` submodule
m10f Mar 16, 2023
26d1dc5
re-add missing libs to linker and libs dir
m10f Mar 22, 2023
e4e3a65
build.sh: Set STD_ENV_ARCH
RyanGlScott Mar 22, 2023
1cc32ba
Add `test_output.log`
m10f Mar 22, 2023
e208e98
Remove unneeded RustcRenderedConst newtype
RyanGlScott Apr 3, 2023
b3e74d1
initFnState: Remove unused argument
RyanGlScott Apr 3, 2023
0df0660
genFn/transDefine: Replace unused patterns with wildcards
RyanGlScott Apr 4, 2023
14ce2da
Replace currentFn with a more general FnTransContext
RyanGlScott Apr 4, 2023
6f97467
Translate statics with constant initializers properly
RyanGlScott Apr 4, 2023
cc8d3f2
Add custom op for ctpop
RyanGlScott Apr 5, 2023
0eacf40
lib: Replace RawVec's allocator
RyanGlScott Apr 14, 2023
fa7292a
Translate more types of ConstArrays
RyanGlScott May 2, 2023
370cacc
Update mir-json submodule
RyanGlScott May 2, 2023
6b4370f
patch `core::fmt`
m10f May 2, 2023
8c590e4
crux-mir: Note fmt reimplementation in lib/Patches.md
RyanGlScott May 2, 2023
8a680c4
Mir.TransCustom: Use {impl} consistently
RyanGlScott May 2, 2023
0653a31
lib/crucible: Don't loop infinitely in zeroed()
RyanGlScott May 2, 2023
592b2a1
crux-mir: Regenerate test_output.log
RyanGlScott May 2, 2023
c1f8060
crucible-mir: Translate all ConstTuples, not just unit tuples
RyanGlScott May 2, 2023
0bba133
crucible-mir: Translate constant tuples
RyanGlScott May 3, 2023
b639790
crucible-mir: Add seqcst variants of some atomic intrinsics
RyanGlScott May 3, 2023
07add62
crucible-mir: Add some more {extern}s to custom ops
RyanGlScott May 3, 2023
b57531c
Regenerate test_output.log
RyanGlScott May 4, 2023
6aebf2d
Reapply "implement HashMap in terms of Vec"
RyanGlScott May 4, 2023
70e1387
Implement ptr::invalid/invalid_mut in terms of casts
RyanGlScott May 9, 2023
93c8031
Reapply "Avoid pointer arithmetic in slice iterators"
RyanGlScott May 9, 2023
e7415d0
Stub out ThreadLocalRef
RyanGlScott May 4, 2023
c5b8f25
Permit non-isize-typed enum discriminants
RyanGlScott May 9, 2023
a84dc47
crucible-mir: Infer zero-sized fields in enum variants
RyanGlScott May 10, 2023
2995603
update `mir-json` submodule
m10f May 10, 2023
0f293cf
Add missing pretty-printer case for ThreadLocalRef
RyanGlScott May 11, 2023
621ffc6
Translate slice constants
RyanGlScott May 16, 2023
0f52c5d
Reapply implement str::as_bytes via crucible_identity_transmute
RyanGlScott May 16, 2023
54f7db6
Compute lengths of &str constants properly
RyanGlScott May 17, 2023
0b5105b
Tighten up treatment of atomic intrinsics
RyanGlScott May 17, 2023
b54a15e
boxed.rs: Use crucible's allocator
RyanGlScott May 17, 2023
26de044
lib/Patches.md: Document "boxed.rs: Use crucible's allocator"
RyanGlScott May 17, 2023
7274762
Don't deallocate in box_free and drop
RyanGlScott May 17, 2023
e59402c
Make {sub,mul}_with_overflow use {extern}
RyanGlScott May 18, 2023
b9fec04
Reapply "reimplement from_{le,be}_bytes"
RyanGlScott May 18, 2023
7db42e7
Reapply "reimplement to_{le,be}_bytes"
RyanGlScott May 18, 2023
7b2f924
Use {extern} in transmute custom op
RyanGlScott May 18, 2023
c2aa083
raw_vec.rs: Make sure to always set capacity
RyanGlScott May 18, 2023
0043537
Expunge uses of `rustc_box` and the `box` keyword
RyanGlScott May 18, 2023
a7988e8
Update test_output.log
RyanGlScott May 18, 2023
76c5d19
crux-mir: Repair some test cases with &dyn
RyanGlScott May 18, 2023
098d341
fn_dyn.rs: Use &dyn
RyanGlScott May 18, 2023
ea56c95
crux-mir: Repair checked_* test cases
RyanGlScott May 18, 2023
ea9066b
conditional.rs: Modernize crux::test usage
RyanGlScott May 18, 2023
643ce40
Remove normDefId, compare against ExplodedDefIds
RyanGlScott May 22, 2023
5d35c27
crux-mir: Accept new golden output for some symbolic tests
RyanGlScott May 23, 2023
a29b2ff
crux-mir: Update test_output.log
RyanGlScott May 23, 2023
d7a4776
crux-mir: Override ctlz properly
RyanGlScott May 23, 2023
0be2b4a
build.sh: Use --remap-path-prefix
RyanGlScott May 24, 2023
b7a30ef
crux-mir: Update test_output.log
RyanGlScott May 24, 2023
917fb76
Handle closure constants properly
RyanGlScott May 24, 2023
141803b
Reapply "implement allocate_zeroed to fix vec![0; len]"
RyanGlScott May 24, 2023
b153e90
crucible-mir: Handle constant function pointers
RyanGlScott May 25, 2023
5df73b3
Reapply "reenable old override for slice::len"
RyanGlScott May 25, 2023
8d99d39
crucible-mir: Add sub_ptr custom ops
RyanGlScott May 25, 2023
6308cc8
Remove invalid inline pragmas
RyanGlScott May 25, 2023
22e1e07
crux-mir: Override const and mut slice len as well
RyanGlScott May 26, 2023
2272bc3
Reapply "update &[T] -> &[T; N] TryFrom impl"
RyanGlScott May 26, 2023
e629734
Disable `IsRawEqComparable`-based `SpecArrayEq` instances
RyanGlScott May 26, 2023
6dde646
Reapply "disable bytewise equality comparisons for [T]"
RyanGlScott May 26, 2023
8db861e
crucible-mir: Compute discriminant for initial enum values properly
RyanGlScott May 26, 2023
087ec43
crux-mir-test: Update symbolic golden test output
RyanGlScott May 26, 2023
e9dac28
Update test_output.log
RyanGlScott May 26, 2023
faef7f1
Use crucible_null_hook to implement null/null_mut
RyanGlScott May 30, 2023
8a599bc
crux-mir-test: Accept new coverage output
RyanGlScott May 31, 2023
d6ab13a
crucible-mir: Override clone/clone_from properly
RyanGlScott May 31, 2023
29f737d
Implement Demand using PhantomData instead of a DST
RyanGlScott Jun 1, 2023
b703544
crux-mir: Re-implement timing
RyanGlScott Jun 1, 2023
9e34725
crucible-mir: Translate ThreadLocalRefs properly
RyanGlScott Jun 1, 2023
550bb9c
Replace sys::{condvar,mutex,rwlock} with Crux-specific implementations
RyanGlScott Jun 1, 2023
76784e1
crux-mir-test: Update golden output for symbolic tests
RyanGlScott Jun 1, 2023
74c7e1b
Update test_output.log
RyanGlScott Jun 1, 2023
519f321
crux-mir-test: Sanitize disambiguators in golden test output
RyanGlScott Jun 2, 2023
afbf939
crux-mir-test: Update golden test output
RyanGlScott Jun 2, 2023
65e75fe
Regenerate test_output.log
RyanGlScott Jun 2, 2023
d29bb61
Upgrade to byteorder v1.4.3
RyanGlScott Jun 2, 2023
2236a8e
Use Crucible-friendly implementations of byteorder functions
RyanGlScott Jun 2, 2023
e526e9a
Bump mir-json submodule
RyanGlScott Jun 2, 2023
d8853f0
Accept new golden output for byteorder tests
RyanGlScott Jun 2, 2023
2302923
Hackily support `&dyn Trait` references
RyanGlScott Jun 21, 2023
5a11535
Track crate names and their hashes, use it to look up wired-in names
RyanGlScott Jun 21, 2023
2740aac
Update test_output.log
RyanGlScott Jun 21, 2023
370cb61
crux-mir: Include test crate
RyanGlScott Jun 29, 2023
537dfbe
build.sh: Produce a proper sysroot
RyanGlScott Jun 29, 2023
d4f5074
CI: Re-enable macOS build for crux-mir
RyanGlScott Jul 3, 2023
044ad3d
Remove temporary test_output.log file
RyanGlScott Jul 3, 2023
5d4453f
build.sh: Make rlibs a symlink to rlibs_real/.../lib
RyanGlScott Jul 3, 2023
85e59a9
Remove translate_libs.sh
RyanGlScott Jul 3, 2023
a7c2f6d
Make build.sh the new translate_libs.sh
RyanGlScott Jul 3, 2023
4658042
Document inferElidedVariantFields
RyanGlScott Jul 5, 2023
a1c0bbc
report-coverage: Avoid triggering rust-lang/rust#79813 warning
RyanGlScott Jul 5, 2023
352fed4
crux-mir: Add Box stress test
RyanGlScott Jul 5, 2023
ed718aa
CI: Use up-to-date Rust nightly
RyanGlScott Jul 5, 2023
42a3606
crux-mir/lib/Patches.md: Fill in some TODOs
RyanGlScott Jul 5, 2023
ef8fc37
crucible-mir: Parenthesize some equality constraints
RyanGlScott Jul 5, 2023
9ae78ed
crucible-mir: Avoid some failable do-block matches on ST
RyanGlScott Jul 5, 2023
ee39bf0
crucible-mir: More parentheses
RyanGlScott Jul 6, 2023
e0d77af
Use crux::test instead of crux_test
RyanGlScott Jul 7, 2023
c8eb7b6
crucible-mir: Remove some commented-out old code
RyanGlScott Jul 13, 2023
b794aca
crucible-mir: Document reasoning for some evalRval cases
RyanGlScott Jul 13, 2023
8c11bca
crux-mir: Add test case for ConstKind::Unevaluated
RyanGlScott Jul 13, 2023
0afbb96
Properly implement transStatement case for StmtIntrinsic
RyanGlScott Jul 13, 2023
d2ff2cc
crucible-mir: Expunge defaultDisambiguator and anything that uses it
RyanGlScott Jul 13, 2023
331de03
crucible-mir: ShallowInitBox is unsupported for now
RyanGlScott Jul 13, 2023
e8ac077
Bump mir-json submodule
RyanGlScott Jul 13, 2023
0515e64
crux-mir: Use simpler #[crux::test] attribute for symbolic tests
RyanGlScott Jul 13, 2023
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
Prev Previous commit
Next Next commit
Reapply "update &[T] -> &[T; N] TryFrom impl"
Originally from commit e645cee
  • Loading branch information
RyanGlScott committed Jul 3, 2023
commit 2272bc374f770c6b409b0dfa599a70777b15af70
4 changes: 4 additions & 0 deletions crux-mir/lib/Patches.md
Original file line number Diff line number Diff line change
Expand Up @@ -83,3 +83,7 @@ identify all of the code that was changed in each patch.
type. Currently, `crucible-mir` does not support Rust unions, so we instead
implement slice `len` in terms of our own `crucible_slice_len_hook` function
that we override.

* Use `crucible_array_from_slice_hook` in `&[T] -> &[T; N]` `TryFrom` impl (last applied: May 26, 2023)

The actual implementation uses a pointer cast that Crucible can't handle.
20 changes: 14 additions & 6 deletions crux-mir/lib/core/src/array/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -262,13 +262,20 @@ impl<'a, T, const N: usize> TryFrom<&'a [T]> for &'a [T; N] {
type Error = TryFromSliceError;

fn try_from(slice: &[T]) -> Result<&[T; N], TryFromSliceError> {
if slice.len() == N {
let ptr = slice.as_ptr() as *const [T; N];
// SAFETY: ok because we just checked that the length fits
unsafe { Ok(&*ptr) }
} else {
Err(TryFromSliceError(()))
fn crucible_array_from_slice_hook<T, const N: usize>(
slice: &[T],
len: usize,
) -> Option<&[T; N]> {
if slice.len() == N {
let ptr = slice.as_ptr() as *const [T; N];
// SAFETY: ok because we just checked that the length fits
unsafe { Some(&*ptr) }
} else {
None
}
}
crucible_array_from_slice_hook(slice, N)
.ok_or(TryFromSliceError(()))
}
}

Expand All @@ -289,6 +296,7 @@ impl<'a, T, const N: usize> TryFrom<&'a mut [T]> for &'a mut [T; N] {
type Error = TryFromSliceError;

fn try_from(slice: &mut [T]) -> Result<&mut [T; N], TryFromSliceError> {
// Mut version is not supported by crucible - see comment in TransCustom.array_from_slice
if slice.len() == N {
let ptr = slice.as_mut_ptr() as *mut [T; N];
// SAFETY: ok because we just checked that the length fits
Expand Down