Ralf Jung
bb6e5224da
handle array types
2017-07-25 10:22:11 +02:00
Ralf Jung
4457a52d4f
Re-do the way locking is done during verification
...
We now lock at the "leaves" on the types, rather than locking at references.
In particular, Validate for sth. of non-reference lvalue will also lock the "outer" memory.
Also change the way we release write locks, and some refactoring in the memory.
2017-07-25 10:22:11 +02:00
Ralf Jung
7c6e6cf492
for references, validate alignment and handle ZSTs
2017-07-25 10:22:10 +02:00
Ralf Jung
1f9153fac3
validate TyClosure, TyTuple, TyNever
2017-07-25 10:20:45 +02:00
Ralf Jung
dac51f41ad
various small fixes and tracing
2017-07-25 10:20:45 +02:00
Ralf Jung
046675d735
Also release locks on ReleaseValidation and EndRegion
2017-07-25 10:20:45 +02:00
Ralf Jung
aaae815b44
fix release_lock_until to no longer remove inactive locks
2017-07-25 10:20:45 +02:00
Ralf Jung
fda5cc9b4c
avoid downcasting for enum variants without further fields
2017-07-25 10:20:45 +02:00
Ralf Jung
a91ee4bb03
validate boxes
2017-07-25 10:20:45 +02:00
Ralf Jung
22f43e2d2b
implement checking for ADTs
2017-07-25 10:20:45 +02:00
Ralf Jung
02e802811b
implement stub validity check for basic types (bool, int, float); acquire locks for references
2017-07-25 10:20:45 +02:00
Ralf Jung
edc6ce30d5
implement acquiring and releasing locks
2017-07-25 10:19:27 +02:00
Ralf Jung
4372f1145f
add locking data structures and lock checks
...
This brings back some of the memory range ideas that were deleted with the packed refactoring.
2017-07-25 10:19:27 +02:00
Ralf Jung
d2a9235c63
update for rustc changes: treat new MIR commands as NOP
2017-07-25 10:15:00 +02:00
Oliver Schneider
03ca15e62d
Merge pull request #267 from RalfJung/cast
...
Fix ptr-int-casts
2017-07-24 11:31:25 +02:00
Oliver Schneider
4a34a1b50e
Pass HasDataLayout instead of the data layout itself
2017-07-24 09:56:02 +02:00
Oliver Schneider
9c07f424da
Use rustc traits instead of our own
2017-07-23 15:00:22 +02:00
Ralf Jung
4d38f8dffb
move pointer truncation to a common method in memory.rs
2017-07-22 11:28:48 -07:00
Oliver Schneider
6e10752fef
Merge pull request #269 from oli-obk/cleanups
...
Remove unused `IntoValTyPair` hack
2017-07-22 09:52:47 +02:00
Ralf Jung
40950b2cd1
fix nits
2017-07-21 20:02:48 -07:00
Ralf Jung
b174b786b6
refactor casting code to more clearly handle pointers
2017-07-21 20:02:48 -07:00
Ralf Jung
f960f4c537
fix casting integers to pointers
2017-07-21 20:02:48 -07:00
Oliver Schneider
202dd5a359
Remove unused IntoValTyPair hack
2017-07-21 14:59:58 +02:00
Oliver Schneider
6143ef03c3
Merge pull request #258 from oli-obk/upstream
...
Prep miri repository for rustc merger
2017-07-21 12:32:45 +02:00
Oliver Schneider
4cfa7c5d12
Prep miri repository for rustc merger
2017-07-21 11:30:56 +02:00
Oliver Schneider
b4e300d577
Merge pull request #266 from RalfJung/align
...
Always test alignment in memory.rs
2017-07-21 09:46:50 +02:00
Ralf Jung
14cb85809b
always test alignment in memory.rs
2017-07-20 13:24:06 -07:00
Oliver Schneider
308c7cadf1
Merge pull request #265 from oli-obk/optimize_prime
...
Also test optimized MIR
2017-07-20 22:08:02 +02:00
Oliver Schneider
f2d0101065
Also test optimized MIR
2017-07-20 20:25:43 +02:00
Oliver Schneider
9710ff481e
Merge pull request #264 from oli-obk/paths
...
Reduce the usage of global paths
2017-07-20 20:00:19 +02:00
Oliver Schneider
9b526d1c85
Reduce the usage of global paths
2017-07-20 16:40:57 +02:00
Oliver Schneider
f822ad5c63
Merge pull request #260 from RalfJung/tests
...
Split up test suite
2017-07-20 16:07:08 +02:00
Eduard-Mihai Burtescu
e79bb42ab3
Merge pull request #262 from RalfJung/never
...
remove ad-hoc 'never' type check in read_lvalue
2017-07-20 15:13:21 +03:00
Oliver Schneider
101e5a8ba0
Move rustc tests from tests to a binary, since they are only run manually anyway
2017-07-20 13:11:40 +02:00
Oliver Schneider
f02d9e63fd
Merge pull request #259 from RalfJung/ref-validate
...
No longer check aligment and non-NULLness on `&`
2017-07-20 07:09:52 +02:00
Ralf Jung
3b19c83c67
remove ad-hoc 'never' type check in read_lvalue
2017-07-19 20:32:51 -07:00
Ralf Jung
7648ccaae1
add test for misaligned pointer loads
2017-07-19 20:26:30 -07:00
Ralf Jung
ede055c2be
fix checking alignment of pointer loads
2017-07-19 20:24:09 -07:00
Ralf Jung
f9818bf818
fix a warning
2017-07-19 13:31:21 -07:00
Ralf Jung
e38ee0a30a
split up the test suite
2017-07-19 12:52:20 -07:00
Ralf Jung
e4ffab1754
enable test code that passes just fine
2017-07-19 11:38:15 -07:00
Ralf Jung
2424953055
Don't pretend that casts to bool are a thing
2017-07-19 11:35:06 -07:00
Ralf Jung
72664e42aa
No longer check aligment and non-NULLness on &
...
This breaks creating unaligned raw pointers via `&packed.field as *const _`, which needs to be legal.
Also it doesn't seem like LLVM still relies on this, see
* https://github.com/solson/miri/issues/244#issuecomment-315563640
* https://internals.rust-lang.org/t/rules-for-alignment-and-non-nullness-of-references/5430/16
We probably want to handle this invariant like the others that validation is concerned with, and only
check it on function boundaries for now.
2017-07-19 11:28:35 -07:00
Oliver Schneider
27c64479cd
Merge pull request #257 from oli-obk/cleanups
...
Export types and functions needed by priroda
2017-07-19 11:40:43 +02:00
Oliver Schneider
d9d792ba03
Export types and functions needed by priroda
2017-07-19 11:06:07 +02:00
Oliver Schneider
2d5c4196f1
Merge pull request #254 from RalfJung/dangling
...
Remove reundant dangling checks in {r,d}eallocate
2017-07-18 23:34:09 +02:00
Scott Olson
824438bda9
Merge pull request #255 from RalfJung/float
...
use libstd methods for floating-point <-> bytes conversion
2017-07-18 14:16:42 -07:00
Ralf Jung
9bccfd388c
use libstd methods for floating-point <-> bytes conversion
2017-07-18 13:56:01 -07:00
Ralf Jung
ff9192e346
remove reundant dangling checks in {r,d}eallocate
2017-07-18 13:50:54 -07:00
Oliver Schneider
5328c5d1b0
Merge pull request #245 from oli-obk/funky_allocs
...
Ensure that it is not possible to explicitly free stack memory
2017-07-18 14:09:15 +02:00
