Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
106 commits
Select commit Hold shift + click to select a range
e8fe9ae
Minimal changes to rustc to enable RMC
danielsn Apr 6, 2021
89a89dd
Renamed files to avoid name conflicts
danielsn Apr 6, 2021
fbb987e
initial rmc commit
danielsn Apr 6, 2021
df0e29a
Fix out-by-one errors in cargo-rmc-tests and run-make tests (#17)
adpaco-aws Apr 8, 2021
0165377
Add regression test for https://github.com/model-checking/rmc/issues/…
danielsn Apr 8, 2021
819884b
Refactor codegen_vtable and vtable_name (#24)
danielsn Apr 9, 2021
0f34cdb
Correctly track the type of boxed fat pointers when projecting throug…
danielsn Apr 9, 2021
e23c5d5
Fix issue where array types were recorded as [x; _] and hence aliasi…
danielsn Apr 9, 2021
0e38dbf
Conform with latest changes to `Binder` (used in closures) (#27)
adpaco-aws Apr 9, 2021
72cd753
Squashed a bunch of warnings (#28)
danielsn Apr 10, 2021
c9f05e1
Squash warnings: remove final use of insert_unchecked (#29)
danielsn Apr 12, 2021
3354e85
Properly handle Fat-ptr to Fat-ptr casts (#62)
danielsn Apr 14, 2021
27db8e6
Add RMC workflow file for GitHub Actions (#31)
adpaco-aws Apr 14, 2021
8f3dcdc
Add vtable well-formedness flag
nchong-at-aws Apr 15, 2021
58a2860
Add templates for Pull Requests and Issues (#81)
adpaco-aws Apr 16, 2021
1845d88
Add a couple of missing tests (nondet. vectors, offset) (#79)
adpaco-aws Apr 19, 2021
1411c8f
Complete and replace the unsized pointer cast implementation (#88)
markrtuttle Apr 21, 2021
26b349f
Add script and workflow for copyright checks in CI (#92)
adpaco-aws Apr 21, 2021
4d0479d
Add unsized pointer cast regression tests (#89)
markrtuttle Apr 22, 2021
445584e
update readme (#91)
danielsn Apr 22, 2021
b988803
Add nondet. bytes test (#94)
adpaco-aws Apr 23, 2021
9aa43cd
Enable regression workflow for macOS (#97)
adpaco-aws Apr 23, 2021
87db833
Allow cast of any pointer to cast to a trait pointer (#98)
markrtuttle Apr 24, 2021
38eb19c
Allow cast of fat pointers to thin pointers (#99)
markrtuttle Apr 24, 2021
1f6ba24
Minor tweaks to the documentation (#100)
danielsn Apr 24, 2021
8453c0a
Correct fat pointer generation by codegen_rvalue_ref (#101)
markrtuttle Apr 26, 2021
a5b7c57
Add box mut dyn trait regression test (#108)
markrtuttle Apr 27, 2021
46a2545
Avoid strict type comparison in statement assignment (#110)
adpaco-aws May 4, 2021
8d3caca
Extend `entry_fn` call to use local defid
adpaco-aws May 5, 2021
a32fadc
Implemented __VERIFIER_assume hook (#115)
danielsn May 14, 2021
30acf6b
Conform with latest changes in crate handling
adpaco-aws May 18, 2021
a92859b
Disable regression test failing in CI but not locally (#133)
adpaco-aws May 21, 2021
5da1207
Refactor: cleanup hooks.rs (#116)
danielsn May 21, 2021
99d1a23
Use num::BigInt instead of i128 in constants, as constants can be of …
danielsn May 21, 2021
90266c3
Added Location to stmt constructors(#139)
vecchiot-aws May 22, 2021
aea8079
Use canonical filenames in source locations (#142)
markrtuttle May 24, 2021
5b684be
Relax the requirements for is_rust_box() to enable crate compilation …
danielsn May 25, 2021
33dde06
Correctly handle the abort intrinsic (#151)
danielsn May 26, 2021
8d141d0
Improve some regression tests and add some more. (#154)
bdalrhm May 27, 2021
4a311bb
Added argument casting when type is same. (#137)
vecchiot-aws May 27, 2021
bfc28e3
Complete count intrinsics codegen and testing (#155)
adpaco-aws May 28, 2021
a15bb6e
Install CBMC viewer in CI (#162)
adpaco-aws May 31, 2021
c1ecdb6
Added fixme tests for 'Unable to find vtable symbol' bug. (#159)
vecchiot-aws May 31, 2021
b09967e
Import and use `LOCAL_CRATE` in `crate_name` call
adpaco-aws Jun 1, 2021
7bad1bb
Update CBMC version check to 5.30.0 (fix #164) #166
avanhatt Jun 2, 2021
2bf79c8
Move 1 rust-test to compiletest. (#163)
bdalrhm Jun 3, 2021
47cdb37
Move balloon standalone example to firecracker folder (#167)
adpaco-aws Jun 3, 2021
2351e86
Refactor pretty name to restore passable dyn trait functionality (#171)
avanhatt Jun 4, 2021
be509a9
Added v0 mangler as default for rmc, and added --mangler option. (#170)
vecchiot-aws Jun 4, 2021
7667eb7
Added --visualize flag to rmc. (#138)
vecchiot-aws Jun 4, 2021
9235d6b
Move all tests under rust-tests to compiletest. (#168)
bdalrhm Jun 7, 2021
406b6f6
Fix for duplicate vtable field names (#188)
avanhatt Jun 9, 2021
c39b869
Add --gen-c flag to cargo-rmc. (#192)
bdalrhm Jun 10, 2021
bb0f40a
Remove slow find_by_pretty_name vtable search (#193)
avanhatt Jun 11, 2021
e5d2800
Refactor: Cleanly seperate `CurrentFnCtx` from `GotocCtx`. (#195)
danielsn Jun 11, 2021
975ed93
Added check for cbmc-viewer version. (#174)
vecchiot-aws Jun 13, 2021
a50e399
Add runtime asserts and tests for vtable size/align (#197)
avanhatt Jun 15, 2021
31ce2f2
Move cargo tests to compiletest. (#198)
bdalrhm Jun 16, 2021
85b6a14
Move now-working boxed dyn trait test (#211)
avanhatt Jun 16, 2021
6d518bc
Initial changes required to codegen stdlib (#210)
danielsn Jun 16, 2021
d34ba89
Separate RMC sanity check function (#201)
avanhatt Jun 17, 2021
327e000
Conform with refactor of vtable codegen
adpaco-aws Jun 17, 2021
6518ecf
Move gotoc tests under run-make to their own test suite. (#217)
bdalrhm Jun 17, 2021
1f401b9
Add rmc-prelude.rs, and use it in tests (#226)
danielsn Jun 18, 2021
2791656
Use RMC prelude in all tests (#232)
adpaco-aws Jun 18, 2021
124cc3d
Add an __VERIFIER_expected_fail() intrinsic, and use it in a test (#229)
danielsn Jun 20, 2021
6e432dc
Codegen drop_in_place type and vtable pointer (#222)
avanhatt Jun 21, 2021
d379e7e
Handle copy on empty str/length zero data (#235)
avanhatt Jun 22, 2021
473a0b5
Enforce formatting of RMC tests. (#258)
bdalrhm Jun 23, 2021
fbfc16e
Added --function flag to cargo-rmc (#239)
vecchiot-aws Jun 23, 2021
ede14d0
Handle unsized dyn trait objects as source of casts (#233)
avanhatt Jun 24, 2021
830686b
Use a better binder/substs for vtable instance lookup. (#257)
avanhatt Jun 24, 2021
254c053
Implement sizeof for Code for vtable generation (fix crash) (#261)
avanhatt Jun 25, 2021
c75008f
Fix types for codegen of intrinsic const (#268)
avanhatt Jun 25, 2021
c6989f7
Support atomic exchange primitives (#266)
danielsn Jun 29, 2021
4cc64c3
Refactor: Use borrowed types for arguments (#269)
danielsn Jun 29, 2021
1ae82a8
use codegen_unimplemented() for the try intrinsic (#275)
danielsn Jun 30, 2021
e5dc4f9
Correct check for vtable pointer type (fix Firecracker regression) (#…
avanhatt Jul 1, 2021
279ac8d
Handle boxed closures as arguments (fix RMC std lib crash) (#278)
avanhatt Jul 1, 2021
c69c907
Add support for multiple expected failures. (#280)
bdalrhm Jul 2, 2021
e537b08
Codegen the rest of std lib and add a regression script
avanhatt Jul 5, 2021
eec6298
Update dyn trait tests from raw to ptr Rust APIs (#306)
avanhatt Jul 7, 2021
fa65496
Custom panic hook for RMC including current item (#304)
avanhatt Jul 8, 2021
20f1213
Conform with recent changes in rustc (limits, binders) (#318)
adpaco-aws Jul 9, 2021
a7795be
Fix codegen for dynamic `Fn::call` and `FnMut::call_mut` (#320)
avanhatt Jul 12, 2021
ea3c931
Use default CBMC flags in RMC (#263)
adpaco-aws Jul 13, 2021
4254b59
Improve setup scripts for development (#322)
tedinski Jul 13, 2021
9c90b22
C lib flag (#260)
vecchiot-aws Jul 14, 2021
9d65935
Emit an error message when rmc-rustc fails (#328)
tedinski Jul 14, 2021
e5f4672
Codegen new intrinsic `raw_eq` (#331)
adpaco-aws Jul 15, 2021
ff5cd92
Use Rust's vtable_entries (#329)
avanhatt Jul 16, 2021
9f4db77
Extract examples from reference and display their results in a dashbo…
bdalrhm Jul 19, 2021
053aafb
Symbol table transformer (#321)
vecchiot-aws Jul 20, 2021
9a19938
Use `x.py` to build and run the dashboard. (#333)
bdalrhm Jul 21, 2021
baebe0c
Fix dyn trait _fail tests compilation errors (#342)
avanhatt Jul 21, 2021
e7e6a13
Remove string that tripped open source alarm. (#344)
vecchiot-aws Jul 21, 2021
8f4a5bc
Differentiate between check, codegen, and verification errors. (#353)
bdalrhm Jul 22, 2021
09409f8
Generics in dyn trait fix: use vtable index to resolve functions (#352)
avanhatt Jul 22, 2021
63e39a9
Add support for simd insert/extract intrinsics (#354)
tedinski Jul 26, 2021
22d72ef
Conform with recent changes in rustc (alloc id, scalar ptr, vtable me…
adpaco-aws Jul 27, 2021
78f20f4
Cleanup rmc flags (#365)
vecchiot-aws Jul 28, 2021
cc7f935
Fix dry-run to print to stdout when output_to is not stdout. (#366)
vecchiot-aws Jul 28, 2021
a37593c
Detect which reference examples should check/codegen/verify. (#363)
bdalrhm Jul 28, 2021
72c9b37
Correct function type for vtable shim (fix some boxed closures) (#335)
avanhatt Jul 29, 2021
14eeec2
Support cargo rmc flags (#371)
vecchiot-aws Jul 29, 2021
6c46d9d
Removed incorrect special case for Rust bitwise operators
zhassan-aws Aug 5, 2021
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
4 changes: 0 additions & 4 deletions .github/ISSUE_TEMPLATE/blank_issue.md

This file was deleted.

50 changes: 23 additions & 27 deletions .github/ISSUE_TEMPLATE/bug_report.md
Original file line number Diff line number Diff line change
@@ -1,44 +1,40 @@
---
name: Bug Report
about: Create a bug report for Rust.
labels: C-bug
about: Create a bug report for RMC
labels: bug
---
<!--
Thank you for filing a bug report! 🐛 Please provide a short summary of the bug,
along with any information you feel relevant to replicating the bug.
Please report security concerns to us on the
[AWS vulnerability reporting](http://aws.amazon.com/security/vulnerability-reporting/) page.
-->

I tried this code:
<!--
Thank you for filing a bug report! 🐛
Please provide a short summary of the issue, along with the information necessary to replicate.
-->

I tried this code:
<!--
If the reproducing code is small, please post it here.
Otherwise, please attach the relevant files to this issue.
Alternatively, post a link to the repository and branch that exposes the issue.
-->
```rust
<code>
```

I expected to see this happen: *explanation*

Instead, this happened: *explanation*

### Meta
<!--
If you're using the stable version of the compiler, you should also check if the
bug also exists in the beta or nightly versions.
-->
using the following command line invocation:

`rustc --version --verbose`:
```
<version>
<command>
```

<!--
Include a backtrace in the code block by setting `RUST_BACKTRACE=1` in your
environment. E.g. `RUST_BACKTRACE=1 cargo build`.
-->
<details><summary>Backtrace</summary>
<p>
with RMC version:

```
<backtrace>
```
I expected to see this happen: *explanation*

</p>
</details>
<!--
If RMC crashed, please include a backtrace in the code block by setting
`RUST_BACKTRACE=1` in your environment. E.g. `RUST_BACKTRACE=1 rmc ...`
-->
Instead, this happened: *explanation*
8 changes: 0 additions & 8 deletions .github/ISSUE_TEMPLATE/config.yml

This file was deleted.

46 changes: 0 additions & 46 deletions .github/ISSUE_TEMPLATE/diagnostics.md

This file was deleted.

27 changes: 27 additions & 0 deletions .github/ISSUE_TEMPLATE/feature_request.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
---
name: Feature Request
about: Create a feature request for RMC
labels:
---
<!--
Please report security concerns to us on the
[AWS vulnerability reporting](http://aws.amazon.com/security/vulnerability-reporting/) page.
-->

<!--
Thank you for requesting an RMC feature!
Please include the following information if it applies to your case:
-->
Requested feature:
Use case:
Link to relevant documentation (Rust reference, Nomicon, RFC):
Is this a breaking change?

Test case:
<!--
If the test-case is small, please post it here.
Otherwise, please attach the relevant files to this issue.
-->
```rust
<code>
```
52 changes: 0 additions & 52 deletions .github/ISSUE_TEMPLATE/ice.md

This file was deleted.

83 changes: 0 additions & 83 deletions .github/ISSUE_TEMPLATE/library_tracking_issue.md

This file was deleted.

37 changes: 37 additions & 0 deletions .github/ISSUE_TEMPLATE/performance_issue.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
---
name: Performance Issue
about: Create a performance issue for RMC
labels: bug
---
<!--
Please report security concerns to us on the
[AWS vulnerability reporting](http://aws.amazon.com/security/vulnerability-reporting/) page.
-->

<!--
Thank you for filing a performance issue!
Please provide a short summary of the issue, along with the information necessary to replicate.
-->

I tried this code:
<!--
If the reproducing code is small, please post it here.
Otherwise, please attach the relevant files to this issue.
Alternatively, post a link to the repository and branch that exposes the issue.
-->
```rust
<code>
```

using the following command line invocation:

```
<command>
```

with RMC version:

If this is a performance regression, how long did it use to take?
Otherwise how much did you expect it to take?
How long did it take?
What stage appears to be the slowest (compilation, verification, code coverage)?
Loading