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

Towards Proving Memory Initialization #3264

Merged
merged 99 commits into from
Jul 2, 2024
Merged
Changes from 1 commit
Commits
Show all changes
99 commits
Select commit Hold shift + click to select a range
52c01aa
Towards implementing uninitialized memory detection in raw pointers
artemagvanian Jun 11, 2024
2b73af7
Implement uninitialized memory detection in raw pointers for certain …
artemagvanian Jun 12, 2024
f3edc52
Implement wide pointer decomposition as part of kani library
artemagvanian Jun 13, 2024
57c31d4
Ensure checks are executed before instructions and statements -- after
artemagvanian Jun 13, 2024
1006fbe
Move tests under tests/kani
artemagvanian Jun 14, 2024
fc224de
Implement drop blessing
artemagvanian Jun 14, 2024
c755ac9
Fix check insertion order
artemagvanian Jun 14, 2024
9b2be02
Autoinitialize extern in alloc::alloc
artemagvanian Jun 14, 2024
e901ebb
Implement support for vtable wide pointers
artemagvanian Jun 14, 2024
4e0c348
Clean up tests, preserve types in shadow memory calls
artemagvanian Jun 17, 2024
1d6e167
Skip analyzing pointers to trait objects for now
artemagvanian Jun 17, 2024
7e26dac
Slight cleanup
artemagvanian Jun 17, 2024
da8c891
Merge branch 'main' into main
artemagvanian Jun 17, 2024
c8a8d1f
Update code to work with nightly-2024-06-17
artemagvanian Jun 17, 2024
087090a
Add missing copyright statements
artemagvanian Jun 17, 2024
73a7ccb
Make clippy happy
artemagvanian Jun 17, 2024
1e55cb7
Make clippy even happier
artemagvanian Jun 17, 2024
97ce8a2
Implement an option to enable initialization checks as a part of func…
artemagvanian Jun 18, 2024
459acba
Separate `can_dereference` from `is_initialized` for now
artemagvanian Jun 18, 2024
d3ab562
Filter out all instances without body to fix MIR dumping
artemagvanian Jun 18, 2024
73ae723
Handle intrinsics exhaustively
artemagvanian Jun 18, 2024
54a3970
Fix code formatting
artemagvanian Jun 18, 2024
8aa56e3
Disable initializations checks in `std-checks` to make CI pass
artemagvanian Jun 19, 2024
d833c2b
Merge branch 'main' into main
artemagvanian Jun 19, 2024
aefec83
Automatically add global shadow memory to `modifies` contract clause
artemagvanian Jun 19, 2024
7a72bbd
Only inject shadow memory symbol if defined
artemagvanian Jun 19, 2024
09f8ecc
Make clippy happy
artemagvanian Jun 19, 2024
ca4da40
Remove stray unwrap
artemagvanian Jun 19, 2024
3bdc949
Add memory initialization checks to `std-verify`
artemagvanian Jun 19, 2024
55b62c4
Fix `expected` files
artemagvanian Jun 19, 2024
e983934
Adjust container size for the harness
artemagvanian Jun 19, 2024
0c8ec39
Skip initialization checks based on the attribute
artemagvanian Jun 20, 2024
2986704
Add comment explaining `skip_first`
artemagvanian Jun 20, 2024
4a43c95
Cache the result of `find_fn_def`
artemagvanian Jun 20, 2024
405e34a
Refactor code re: comments
artemagvanian Jun 20, 2024
ba2d5df
More refactoring for cleaner type layout
artemagvanian Jun 20, 2024
a729cd2
Undo temporary fix to `--emit mir`
artemagvanian Jun 20, 2024
c61b16d
Move `skip_first` from MutableBody to transformation pass
artemagvanian Jun 20, 2024
4feda97
Add some docs for `is_initialized_body`
artemagvanian Jun 20, 2024
d9eacd7
Remove `transmute` inside `shadow.rs`, document type layout, carve ou…
artemagvanian Jun 20, 2024
7174eba
Incorporate `is_initialized` into `can_dereference` and `can_read_una…
artemagvanian Jun 20, 2024
d4ced45
Add more comments to `UninitPass`
artemagvanian Jun 21, 2024
0ec8c3b
Merge branch 'main' into main
artemagvanian Jun 21, 2024
2640b3f
Fix bug when inserting a terminator after a terminator
artemagvanian Jun 21, 2024
98e8a37
Put memory initialization checking into a separate module
artemagvanian Jun 24, 2024
cc32650
Add initialization checks into `kani::mem`
artemagvanian Jun 24, 2024
3dbf70d
Perform FnDef caching inside instrumentation passes
artemagvanian Jun 24, 2024
226c502
Only expose byte mask for type layout
artemagvanian Jun 24, 2024
839a79c
Update a comment
artemagvanian Jun 24, 2024
d6423ce
Further changes to `ty_layout`
artemagvanian Jun 24, 2024
a74bad0
Further changed to`kani_intrinsics`
artemagvanian Jun 24, 2024
54f6284
Extract function resolution associated with `get_kani_sm_function` in…
artemagvanian Jun 24, 2024
1760369
Support determining type layout of enums with variants of the exact s…
artemagvanian Jun 24, 2024
4894296
`assert(false)` on using pointers to trait objects
artemagvanian Jun 24, 2024
db309e0
Make clippy happy
artemagvanian Jun 24, 2024
dc99603
Merge branch 'main' into main
artemagvanian Jun 24, 2024
1718666
Remove unnecessary call to `ty_size`
artemagvanian Jun 24, 2024
dd71adf
Move tests around, temporarily disable `std-checks`
artemagvanian Jun 24, 2024
224239f
Split `split_bb` into two functions
artemagvanian Jun 25, 2024
496bb8b
Merge branch 'main' into main
artemagvanian Jun 25, 2024
9706df2
Add missing `is_initialized` definition into `kani_core`
artemagvanian Jun 25, 2024
43f88c6
Temporarily decouple `is_initialized` and `can_dereference` so that C…
artemagvanian Jun 25, 2024
4d7a97f
Add missing flag
artemagvanian Jun 25, 2024
1a80d98
Formatting change
artemagvanian Jun 25, 2024
ab6fbc9
Disable memory initialization checks for `std-core`
artemagvanian Jun 25, 2024
438a3b4
Fix determining type layout for enums
artemagvanian Jun 25, 2024
e7f3972
Make `is_initialized` a noop if `-Z uninit-checks` flag is not set
artemagvanian Jun 25, 2024
58e62eb
Merge branch 'main' into main
artemagvanian Jun 25, 2024
910f555
Clean up test files
artemagvanian Jun 26, 2024
5966c81
Fix comments inside some tests
artemagvanian Jun 26, 2024
37c03c4
Fix function documentation
artemagvanian Jun 26, 2024
6a7ea31
Small formatting change
artemagvanian Jun 26, 2024
6146a4b
Changes to `slice.rs`
artemagvanian Jun 27, 2024
ce454a3
Merge `mem_swap` and `mem_replace` into `mem`
artemagvanian Jun 27, 2024
3dab8d3
Rename `try_mark_new_bb_as_skipped`
artemagvanian Jun 27, 2024
2e34fa5
Mark changing the initialization state of a trait object as unreachable
artemagvanian Jun 27, 2024
96238df
Add a better comment for `mk_layout_operand`
artemagvanian Jun 27, 2024
01fb654
Add a better doc comment to `Layout`
artemagvanian Jun 27, 2024
e42bdfd
Rename `SourceOp` to `MemoryInitOp`, add comments
artemagvanian Jun 27, 2024
2fe3c7c
Remove unnecessary fields in `MemoryInitOp::Get` and `MemoryInitOp::U…
artemagvanian Jun 27, 2024
d924a9b
Pre-filter intrinsics before instrumenting them
artemagvanian Jun 27, 2024
0136480
Add comment about instrumentation pass order
artemagvanian Jun 27, 2024
1996b05
Merge branch 'main' into main
artemagvanian Jun 27, 2024
9edcd6a
Assert that enum tag has the offset of zero
artemagvanian Jun 27, 2024
c75b616
Inline `scalar_ty_size`
artemagvanian Jun 27, 2024
f4ac75c
Merge branch 'main' into main
artemagvanian Jun 27, 2024
683d365
Apply changes from comments to `perf/uninit`
artemagvanian Jun 28, 2024
28b3a03
Merge branch 'main' into main
artemagvanian Jun 28, 2024
90af616
Add extra docs to `UninitVisitor`
artemagvanian Jun 28, 2024
4b8dcd5
Move some functions in `uninit_visitor.rs` around
artemagvanian Jun 28, 2024
1ab140b
Reorganize handling of intrinsics
artemagvanian Jun 28, 2024
f266ea9
Rename `MemoryInitOp::Get` to `MemoryInitOp::Check`
artemagvanian Jun 28, 2024
a1dccb2
Throw an error only if the unsize cast happens to a pointer to trait …
artemagvanian Jun 28, 2024
bbfd443
Add logic to track additional pointer dereferences in `StatementKind:…
artemagvanian Jun 28, 2024
b882bce
Merge branch 'main' into main
artemagvanian Jul 1, 2024
bda552e
Merge branch 'main' into main
artemagvanian Jul 1, 2024
ca62743
Merge branch 'main' into main
artemagvanian Jul 2, 2024
c91496f
Update kani-compiler/src/kani_middle/transform/check_uninit/uninit_vi…
artemagvanian Jul 2, 2024
839df71
Update incorrect comment in `uninit_visitor.rs`
artemagvanian Jul 2, 2024
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
Add missing copyright statements
  • Loading branch information
artemagvanian committed Jun 17, 2024
commit 087090a6a806586be0e4a39b726dd9715629c4bd
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
//! Utility functions that help calculate type layout.

use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape};
use stable_mir::target::{MachineInfo, MachineSize};
use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Ty, TyKind};
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
//! Visitor that collects all instructions relevant to uninitialized memory access.

use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
use stable_mir::mir::alloc::GlobalAlloc;
use stable_mir::mir::mono::{Instance, InstanceKind};
Loading