-
Notifications
You must be signed in to change notification settings - Fork 269
Pointer static analysis #536
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
Merged
Merged
Changes from all commits
Commits
Show all changes
38 commits
Select commit
Hold shift + click to select a range
1082625
analyze: initial commit
spernsteiner 03c338f
analyze: run polonius and dump outputs
spernsteiner 7566581
analyze: generate var_defined/used_at facts
spernsteiner 9c8f495
analyze: generate path_assigned/moved/accessed_at facts
spernsteiner 66a550b
analyze: generate use_of_var_derefs_region facts
spernsteiner 0ba67e3
analyze: generate load_issued/invalidated_at facts
spernsteiner c2d619a
analyze: generate subset_base facts
spernsteiner 304b1c9
analyze: refactor: move polonius stuff into new borrowck module
spernsteiner e86eff8
analyze: run polonius on a hypothetical rewrite
spernsteiner 9500bdd
analyze: remove UNIQUE permission on error and propagate
spernsteiner 661188e
analyze: handle reborrows when updating UNIQUE
spernsteiner d75e429
analyze: infer READ and WRITE permissions
spernsteiner b76966f
analyze: propagate permissions through offset() calls
spernsteiner f7b329c
analyze: require OFFSET_ADD and OFFSET_SUB for offset() args
spernsteiner de2dcee
analyze: handle constructs seen in insertion_sort
spernsteiner b8d0dac
analyze: include variable names and source code in "final labeling" o…
spernsteiner f30b994
analyze: adjust "final labeling" output for long expressions
spernsteiner 168c24d
analyze: convert examples to a proper test suite
spernsteiner b17a294
analyze: add test for p.offset(..).offset(..)
spernsteiner 6e8ca3f
analyze: refactor dataflow update tracking
spernsteiner 35d8926
analyze: refactor dataflow propagation to allow pluggable update rules
spernsteiner f475677
analyze: determine which pointers should use &Cell<T>
spernsteiner c455f36
analyze: compute new types based on pointer permissions
spernsteiner 56e9b86
analyze: handle Deref and Field projections in Context::type_of
spernsteiner 2def6de
analyze: generate and print expr rewrites
spernsteiner f212c9a
analyze: fix filecheck test runner failing to find c2rust-analyze binary
spernsteiner e9c7f65
analyze: use shared rust-toolchain
spernsteiner dbe3e7b
analyze: remove /target/ from .gitignore
spernsteiner 72cbf53
analyze: add c2rust-analyze to workspace
spernsteiner 6356224
analyze: add rust-analyzer section to Cargo.toml
spernsteiner 722c0c0
Add `*.rlib` to the `c2rust-analyze` `.gitignore` as it's produced by…
kkysen 3dcade1
analyze: fix warnings
spernsteiner 0fa9ab3
analyze: fix warnings in tests
spernsteiner 5f70d42
analyze: use rustc-private-link to find rustc library paths
spernsteiner 6218531
analyze: update README
spernsteiner 0a0ab79
analyze: change cfg for extra debugging code in tests/filecheck/*.rs
spernsteiner d3a0dc2
analyze: autodetect path to FileCheck in tests
spernsteiner b5a15ce
analyze: cargo fmt
spernsteiner File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
/inspect/ | ||
*.rlib |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
[package] | ||
name = "c2rust-analyze" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | ||
|
||
[dependencies] | ||
polonius-engine = "0.13.0" | ||
rustc-hash = "1.1.0" | ||
bitflags = "1.3.2" | ||
|
||
[build-dependencies] | ||
rustc-private-link = { path = "../rustc-private-link" } | ||
print_bytes = "0.6" | ||
|
||
[package.metadata.rust-analyzer] | ||
rustc_private = true |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
```sh | ||
cargo run --bin c2rust-analyze -- tests/filecheck/insertion_sort.rs -L "$(rustc --print sysroot)/lib/rustlib/x86_64-unknown-linux-gnu/lib" --crate-type rlib | ||
``` | ||
|
||
This should produce a large amount of debug output, including a table at the | ||
end listing the type and expression rewrites the analysis has inferred for the | ||
`insertion_sort` function. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
use rustc_private_link::SysRoot; | ||
|
||
fn main() { | ||
let sysroot = SysRoot::resolve(); | ||
sysroot.link_rustc_private(); | ||
|
||
print!("cargo:rustc-env=C2RUST_TARGET_LIB_DIR="); | ||
print_bytes::println_bytes(&sysroot.rustlib()); | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,139 @@ | ||
''' | ||
Usage: `python3 rename_nll_facts.py src ref dest` | ||
kkysen marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
Renames atoms in `src/*.facts` to match the names used in `ref/*.facts`, then | ||
writes the renamed facts to `dest/`. | ||
''' | ||
|
||
import ast | ||
from collections import defaultdict | ||
import os | ||
import sys | ||
|
||
src_dir, ref_dir, dest_dir = sys.argv[1:] | ||
|
||
# Map `src` loan/origin/path names to `ref` loan/origin/path names. We don't | ||
# break this down by type because the names for each type don't collide anyway. | ||
name_map = {} | ||
# Set of `ref` names that appear as values in `name_map`. | ||
ref_names_seen = set() | ||
|
||
def match_name(src_name, ref_name): | ||
if src_name in name_map: | ||
old_ref_name = name_map[src_name] | ||
if ref_name != old_ref_name: | ||
print('error: %r matches both %r and %r' % ( | ||
src_name, old_ref_name, ref_name)) | ||
return | ||
else: | ||
if ref_name in ref_names_seen: | ||
print('error: %r matches %r, but %r is already used' % ( | ||
src_name, ref_name, ref_name)) | ||
return | ||
name_map[src_name] = ref_name | ||
ref_names_seen.add(ref_name) | ||
|
||
def match_loan(src_name, ref_name): | ||
match_name(src_name, ref_name) | ||
|
||
def match_origin(src_name, ref_name): | ||
match_name(src_name, ref_name) | ||
|
||
def match_path(src_name, ref_name): | ||
match_name(src_name, ref_name) | ||
|
||
|
||
def load(name): | ||
with open(os.path.join(src_dir, name + '.facts')) as f: | ||
src_rows = [[ast.literal_eval(s) for s in line.strip().split('\t')] | ||
for line in f] | ||
with open(os.path.join(ref_dir, name + '.facts')) as f: | ||
ref_rows = [[ast.literal_eval(s) for s in line.strip().split('\t')] | ||
for line in f] | ||
return src_rows, ref_rows | ||
|
||
|
||
# Match up paths using `path_is_var` and `path_assigned_at_base`. | ||
|
||
def match_path_is_var(): | ||
src, ref = load('path_is_var') | ||
ref_dct = {var: path for path, var in ref} | ||
for path, var in src: | ||
if var not in ref_dct: | ||
continue | ||
match_path(path, ref_dct[var]) | ||
|
||
match_path_is_var() | ||
|
||
def match_path_assigned_at_base(): | ||
src, ref = load('path_assigned_at_base') | ||
ref_dct = {point: path for path, point in ref} | ||
for path, point in src: | ||
if point not in ref_dct: | ||
continue | ||
match_path(path, ref_dct[point]) | ||
|
||
match_path_assigned_at_base() | ||
|
||
# Match up origins and loans using `loan_issued_at` | ||
|
||
def match_loan_issued_at(): | ||
src, ref = load('loan_issued_at') | ||
ref_dct = {point: (origin, loan) for origin, loan, point in ref} | ||
for origin, loan, point in src: | ||
if point not in ref_dct: | ||
continue | ||
match_origin(origin, ref_dct[point][0]) | ||
match_origin(loan, ref_dct[point][1]) | ||
|
||
match_loan_issued_at() | ||
|
||
# Match up origins using `use_of_var_derefs_origin` | ||
|
||
def match_use_of_var_derefs_origin(): | ||
src, ref = load('use_of_var_derefs_origin') | ||
src_dct = defaultdict(list) | ||
for var, origin in src: | ||
src_dct[var].append(origin) | ||
ref_dct = defaultdict(list) | ||
for var, origin in ref: | ||
ref_dct[var].append(origin) | ||
for var in set(src_dct.keys()) & set(ref_dct.keys()): | ||
src_origins = src_dct[var] | ||
ref_origins = ref_dct[var] | ||
if len(src_origins) != len(ref_origins): | ||
print('error: var %r has %d origins in src but %d in ref' % ( | ||
var, len(src_origins), len(ref_origins))) | ||
continue | ||
for src_origin, ref_origin in zip(src_origins, ref_origins): | ||
match_origin(src_origin, ref_origin) | ||
|
||
match_use_of_var_derefs_origin() | ||
|
||
|
||
# Rewrite `src` using the collected name mappings. | ||
|
||
os.makedirs(dest_dir, exist_ok=True) | ||
for name in os.listdir(src_dir): | ||
if name.startswith('.') or not name.endswith('.facts'): | ||
continue | ||
|
||
with open(os.path.join(src_dir, name)) as src, \ | ||
open(os.path.join(dest_dir, name), 'w') as dest: | ||
for line in src: | ||
src_parts = [ast.literal_eval(s) for s in line.strip().split('\t')] | ||
dest_parts = [] | ||
for part in src_parts: | ||
if part.startswith('_') or part.startswith('Start') or part.startswith('Mid'): | ||
dest_parts.append(part) | ||
continue | ||
|
||
dest_part = name_map.get(part) | ||
if dest_part is None: | ||
print('error: no mapping for %r (used in %s: %r)' % ( | ||
part, name, src_parts)) | ||
dest_part = 'OLD:' + part | ||
dest_parts.append(dest_part) | ||
|
||
dest.write('\t'.join('"%s"' % part for part in dest_parts) + '\n') | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
../rust-toolchain |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.