fix bit logic operators#395

Closed

zhassan-aws wants to merge 106 commits into

model-checking:main-154-2021-08-02from

zhassan-aws:fix-bit-logic-operators

Commits on Jul 26, 2021

Minimal changes to rustc to enable RMC

danielsn
authored and
adpaco
committed
Renamed files to avoid name conflicts

danielsn
authored and
adpaco
committed
initial rmc commit

danielsn
authored and
adpaco
committed
Fix out-by-one errors in cargo-rmc-tests and run-make tests (#17)
adpaco
committed
Add regression test for https://github.com/model-checking/rmc/issues/21 (#22)

danielsn
authored and
adpaco
committed
Refactor codegen_vtable and vtable_name (#24)

authored and
adpaco
committed
Correctly track the type of boxed fat pointers when projecting through them (#23)

danielsn
authored and
adpaco
committed
Fix issue where array types were recorded as [x; _] and hence aliasing (#15)

danielsn
authored and
adpaco
committed
Conform with latest changes to `Binder` (used in closures) (#27)
adpaco
committed
Squashed a bunch of warnings (#28)

danielsn
authored and
adpaco
committed
Squash warnings: remove final use of insert_unchecked (#29)

danielsn
authored and
adpaco
committed
Properly handle Fat-ptr to Fat-ptr casts (#62)

danielsn
authored and
adpaco
committed
Add RMC workflow file for GitHub Actions (#31)
adpaco
committed
Add vtable well-formedness flag

authored and
adpaco
committed
Add templates for Pull Requests and Issues (#81)
adpaco
committed
Add a couple of missing tests (nondet. vectors, offset) (#79)

adpaco
and
danielsn
committed
Complete and replace the unsized pointer cast implementation (#88)

authored and
adpaco
committed
Add script and workflow for copyright checks in CI (#92)
adpaco
committed
Add unsized pointer cast regression tests (#89)

markrtuttle
authored and
adpaco
committed
update readme (#91)

danielsn
authored and
adpaco
committed
Add nondet. bytes test (#94)

adpaco
and
danielsn
committed
Enable regression workflow for macOS (#97)
adpaco
committed
Allow cast of any pointer to cast to a trait pointer (#98)

authored and
adpaco
committed
Allow cast of fat pointers to thin pointers (#99)

authored and
adpaco
committed
Minor tweaks to the documentation (#100)

danielsn
authored and
adpaco
committed
Correct fat pointer generation by codegen_rvalue_ref (#101)

authored and
adpaco
committed
Add box mut dyn trait regression test (#108)

authored and
adpaco
committed
Avoid strict type comparison in statement assignment (#110)

adpaco
and
nchong-at-aws
committed
Extend `entry_fn` call to use local defid
adpaco
committed
Implemented __VERIFIER_assume hook (#115)

danielsn
authored and
adpaco
committed
Conform with latest changes in crate handling
adpaco
committed
Disable regression test failing in CI but not locally (#133)
adpaco
committed
Refactor: cleanup hooks.rs (#116)

danielsn
authored and
adpaco
committed
Use num::BigInt instead of i128 in constants, as constants can be of arbitrary size. (#141)

danielsn
authored and
adpaco
committed
Added Location to stmt constructors(#139)

vecchiot-aws
authored and
adpaco
committed
Use canonical filenames in source locations (#142)

authored and
adpaco
committed
Relax the requirements for is_rust_box() to enable crate compilation (#153)

danielsn
authored and
adpaco
committed
Correctly handle the abort intrinsic (#151)

danielsn
authored and
adpaco
committed
Improve some regression tests and add some more. (#154)

bdalrhm
authored and
adpaco
committed
Added argument casting when type is same. (#137)

vecchiot-aws
and
adpaco
committed
Complete count intrinsics codegen and testing (#155)
adpaco
committed
Install CBMC viewer in CI (#162)
adpaco
committed
Added fixme tests for 'Unable to find vtable symbol' bug. (#159)

authored and
adpaco
committed
Import and use `LOCAL_CRATE` in `crate_name` call
adpaco
committed
Update CBMC version check to 5.30.0 (fix #164) #166

authored and
adpaco
committed
Move 1 rust-test to compiletest. (#163)

bdalrhm
and
adpaco
committed
Move balloon standalone example to firecracker folder (#167)
adpaco
committed
Refactor pretty name to restore passable dyn trait functionality (#171)

avanhatt
authored and
adpaco
committed
Added v0 mangler as default for rmc, and added --mangler option. (#170)

vecchiot-aws
authored and
adpaco
committed
Added --visualize flag to rmc. (#138)

vecchiot-aws
authored and
adpaco
committed
Move all tests under rust-tests to compiletest. (#168)

bdalrhm
authored and
adpaco
committed
Fix for duplicate vtable field names (#188)

avanhatt
authored and
adpaco
committed
Add --gen-c flag to cargo-rmc. (#192)

bdalrhm
and
adpaco
committed
Remove slow find_by_pretty_name vtable search (#193)

avanhatt
authored and
adpaco
committed
Refactor: Cleanly seperate `CurrentFnCtx` from `GotocCtx`. (#195)

danielsn
authored and
adpaco
committed
Added check for cbmc-viewer version. (#174)

vecchiot-aws
authored and
adpaco
committed
Add runtime asserts and tests for vtable size/align (#197)

avanhatt
authored and
adpaco
committed
Move cargo tests to compiletest. (#198)

bdalrhm
and
adpaco
committed
Move now-working boxed dyn trait test (#211)

avanhatt
authored and
adpaco
committed
Initial changes required to codegen stdlib (#210)

danielsn
authored and
adpaco
committed
Separate RMC sanity check function (#201)

authored and
adpaco
committed
Conform with refactor of vtable codegen
adpaco
committed
Move gotoc tests under run-make to their own test suite. (#217)

bdalrhm
authored and
adpaco
committed
Add rmc-prelude.rs, and use it in tests (#226)

danielsn
authored and
adpaco
committed
Use RMC prelude in all tests (#232)
adpaco
committed
Add an __VERIFIER_expected_fail() intrinsic, and use it in a test (#229)

danielsn
authored and
adpaco
committed
Codegen drop_in_place type and vtable pointer (#222)

avanhatt
authored and
adpaco
committed
Handle copy on empty str/length zero data (#235)

avanhatt
authored and
adpaco
committed
Enforce formatting of RMC tests. (#258)

bdalrhm
authored and
adpaco
committed
Added --function flag to cargo-rmc (#239)

vecchiot-aws
authored and
adpaco
committed
Handle unsized dyn trait objects as source of casts (#233)

avanhatt
authored and
adpaco
committed
Use a better binder/substs for vtable instance lookup. (#257)

avanhatt
authored and
adpaco
committed
Implement sizeof for Code for vtable generation (fix crash) (#261)

avanhatt
authored and
adpaco
committed
Fix types for codegen of intrinsic const (#268)

avanhatt
authored and
adpaco
committed
Support atomic exchange primitives (#266)

danielsn
authored and
adpaco
committed
Refactor: Use borrowed types for arguments (#269)

danielsn
and
adpaco
committed
use codegen_unimplemented() for the try intrinsic (#275)

danielsn
authored and
adpaco
committed
Correct check for vtable pointer type (fix Firecracker regression) (#279)

avanhatt
authored and
adpaco
committed
Handle boxed closures as arguments (fix RMC std lib crash) (#278)

avanhatt
authored and
adpaco
committed
Add support for multiple expected failures. (#280)

bdalrhm
authored and
adpaco
committed
Codegen the rest of std lib and add a regression script

avanhatt
and
adpaco
committed
Update dyn trait tests from raw to ptr Rust APIs (#306)

avanhatt
authored and
adpaco
committed
Custom panic hook for RMC including current item (#304)

avanhatt
authored and
adpaco
committed
Conform with recent changes in rustc (limits, binders) (#318)
adpaco
committed
Fix codegen for dynamic `Fn::call` and `FnMut::call_mut` (#320)

avanhatt
authored and
adpaco
committed
Use default CBMC flags in RMC (#263)
adpaco
committed
Improve setup scripts for development (#322)

tedinski
authored and
adpaco
committed
C lib flag (#260)

vecchiot-aws
authored and
adpaco
committed
Emit an error message when rmc-rustc fails (#328)

tedinski
authored and
adpaco
committed
Codegen new intrinsic `raw_eq` (#331)
adpaco
committed
Use Rust's vtable_entries (#329)

avanhatt
authored and
adpaco
committed
Extract examples from reference and display their results in a dashboard. (#325)

bdalrhm
authored and
adpaco
committed
Symbol table transformer (#321)

vecchiot-aws
authored and
adpaco
committed
Use `x.py` to build and run the dashboard. (#333)

bdalrhm
and
adpaco
committed
Fix dyn trait _fail tests compilation errors (#342)

avanhatt
authored and
adpaco
committed
Remove string that tripped open source alarm. (#344)

vecchiot-aws
authored and
adpaco
committed
Differentiate between check, codegen, and verification errors. (#353)

bdalrhm
authored and
adpaco
committed
Generics in dyn trait fix: use vtable index to resolve functions (#352)

authored and
adpaco
committed
Add support for simd insert/extract intrinsics (#354)

tedinski
and
adpaco
committed

Commits on Jul 27, 2021

Conform with recent changes in rustc (alloc id, scalar ptr, vtable method) (#361)
adpaco
authored

Commits on Jul 28, 2021

Commits on Jul 29, 2021

Commits on Aug 5, 2021

Removed incorrect special case for Rust bitwise operators
zhassan-aws
committed