fix bit logic operators #395

zhassan-aws · 2021-08-06T00:32:40Z

Minimal changes to rustc to enable RMC
Renamed files to avoid name conflicts
initial rmc commit
Fix out-by-one errors in cargo-rmc-tests and run-make tests (Fix out-by-one errors in tests #17)
Add regression test for Codegen issue: Can't cast error Expr to StructTag #21 (Add regression test for https://github.com/model-checking/rmc/issues/21 #22)
Refactor codegen_vtable and vtable_name (Refactor codegen_vtable and vtable_name #24)
Correctly track the type of boxed fat pointers when projecting through them (Correctly track the type of boxed fat pointers when projecting through them #23)
Fix issue where array types were recorded as [x; _] and hence aliasing (Fix issue where array types were aliasing #15)
Conform with latest changes to Binder (used in closures) (Conform with latest changes to Binder (used in closures) #27)
Squashed a bunch of warnings (Squashed a bunch of warnings #28)
Squash warnings: remove final use of insert_unchecked (Squash warnings: remove final use of insert_unchecked #29)
Properly handle Fat-ptr to Fat-ptr casts (Properly handle Fat-ptr to Fat-ptr casts #62)
Add RMC workflow file for GitHub Actions (Add RMC workflow file for GitHub Actions #31)
Add vtable well-formedness flag
Add templates for Pull Requests and Issues (Add templates for Pull Requests and Issues #81)
Add a couple of missing tests (nondet. vectors, offset) (Add a couple of missing tests (nondet. vectors, offset) #79)
Complete and replace the unsized pointer cast implementation (Complete and replace the unsized pointer cast implementation #88)
Add script and workflow for copyright checks in CI (Enable copyright checks in CI #92)
Add unsized pointer cast regression tests (Add unsized pointer cast regression tests #89)
update readme (update readme #91)
Add nondet. bytes test (Add nondet. bytes regression test #94)
Enable regression workflow for macOS (Enable regression workflow for macOS #97)
Allow cast of any pointer to cast to a trait pointer (Allow cast of any pointer to cast to a trait pointer #98)
Allow cast of fat pointers to thin pointers (Allow cast of fat pointers to thin pointers #99)
Minor tweaks to the documentation (Minor tweaks to the documentation #100)
Correct fat pointer generation by codegen_rvalue_ref (Correct fat pointer generation by codegen_rvalue_ref #101)
Add box mut dyn trait regression test (Add box mut dyn trait regression test #108)
Avoid strict type comparison in statement assignment (Avoid strict type comparison in statement assignment #110)
Extend entry_fn call to use local defid
Implemented __VERIFIER_assume hook (Implemented __VERIFIER_assume hook #115)
Conform with latest changes in crate handling
Disable regression test failing in CI but not locally (Disable regression test failing in CI but not locally #133)
Refactor: cleanup hooks.rs (Refactor: cleanup hooks.rs #116)
Use num::BigInt instead of i128 in constants, as constants can be of arbitrary size. (Use num::BigInt instead of i128 in constants, as constants can be of arbitrary size. #141)
Added Location to stmt constructors(Added explicit Location parameter to various constructors for Expr and Stmt #139)
Use canonical filenames in source locations (Use canonical filenames in source locations #142)
Relax the requirements for is_rust_box() to enable crate compilation (Relax the requirements for is_rust_box() to enable crate compilation #153)
Correctly handle the abort intrinsic (Correctly handle the abort intrinsic #151)
Improve some regression tests and add some more. (Improve some regression tests and add some more. #154)
Added argument casting when type is same. (Added argument casting when type is same. #137)
Complete count intrinsics codegen and testing (Complete count intrinsics codegen and testing #155)
Install CBMC viewer in CI (Install CBMC viewer in CI #162)
Added fixme tests for 'Unable to find vtable symbol' bug. (Added fixme tests for 'Unable to find vtable symbol' bug. #159)
Import and use LOCAL_CRATE in crate_name call
Update CBMC version check to 5.30.0 (fix Update CBMC version check to 5.30 in rmc-regression.sh #164) Update CBMC version check to 5.30.0 (#164) #166
Move 1 rust-test to compiletest. (Move 1 rust-test to compiletest. #163)
Move balloon standalone example to firecracker folder (Move balloon standalone example to firecracker folder #167)
Refactor pretty name to restore passable dyn trait functionality (Refactor pretty name to restore passable dyn trait functionality #171)
Added v0 mangler as default for rmc, and added --mangler option. (Added v0 mangler as default for rmc, and added --mangler rmc option. #170)
Added --visualize flag to rmc. (Added --visualize flag to rmc and cargo-rmc. #138)
Move all tests under rust-tests to compiletest. (Move all tests under rust-tests to compiletest. #168)
Fix for duplicate vtable field names (Fix for duplicate vtable field names #188)
Add --gen-c flag to cargo-rmc. (Add --gen-c flag to cargo-rmc. #192)
Remove slow find_by_pretty_name vtable search (Remove slow find_by_pretty_name vtable search #193)
Refactor: Cleanly seperate CurrentFnCtx from GotocCtx. (Refactor: Cleanly seperate CurrentFnCtx from GotocCtx. #195)
Added check for cbmc-viewer version. (Added check for cbmc-viewer version. #174)
Add runtime asserts and tests for vtable size/align (Add runtime asserts and tests for vtable size/align #197)
Move cargo tests to compiletest. (Move cargo tests to compiletest. #198)
Move now-working boxed dyn trait test (Move now-working boxed dyn trait test #211)
Initial changes required to codegen stdlib (Initial changes required to codegen stdlib #210)
Separate RMC sanity check function (Separate RMC sanity check function #201)
Conform with refactor of vtable codegen
Move gotoc tests under run-make to their own test suite. (Move gotoc tests under run-make to their own test suite. #217)
Add rmc-prelude.rs, and use it in tests (Add rmc-prelude.rs, and use it in tests #226)
Use RMC prelude in all tests (Use RMC prelude in all tests #232)
Add an __VERIFIER_expected_fail() intrinsic, and use it in a test (Add an __VERIFIER_expected_fail() intrinsic, and use it in a test #229)
Codegen drop_in_place type and vtable pointer (Codegen drop_in_place type and vtable pointer #222)
Handle copy on empty str/length zero data (Handle copy on empty str/length zero data #235)
Enforce formatting of RMC tests. (Enforce formatting of RMC tests. #258)
Added --function flag to cargo-rmc (Added --function flag to cargo-rmc #239)
Handle unsized dyn trait objects as source of casts ( Handle unsized dyn trait objects as source of casts #233)
Use a better binder/substs for vtable instance lookup. (Use better binder for vtable lookup. #257)
Implement sizeof for Code for vtable generation (fix crash) (Implement sizeof for Code for vtable generation (fix crash) #261)
Fix types for codegen of intrinsic const (Fix types for codegen of intrinsic const #268)
Support atomic exchange primitives (Support atomic exchange primitives #266)
Refactor: Use borrowed types for arguments (Refactor: Use borrowed types for arguments #269)
use codegen_unimplemented() for the try intrinsic (use codegen_unimplemented() for the try intrinsic #275)
Correct check for vtable pointer type (fix Firecracker regression) (Correct check for vtable pointer type (fix Firecracker regression) #279)
Handle boxed closures as arguments (fix RMC std lib crash) (Handle boxed closures as arguments (fix RMC std lib crash) #278)
Add support for multiple expected failures. (Add support for multiple expected failures. #280)
Codegen the rest of std lib and add a regression script
Update dyn trait tests from raw to ptr Rust APIs (Update dyn trait tests from raw to ptr Rust APIs #306)
Custom panic hook for RMC including current item (Custom panic hook for RMC including current item #304)
Conform with recent changes in rustc (limits, binders) (Conform with recent changes in rustc (limits, binders) #318)
Fix codegen for dynamic Fn::call and FnMut::call_mut (Fix codegen for dynamic Fn::call and FnMut::call_mut #320)
Use default CBMC flags in RMC (Use default CBMC flags in RMC #263)
Improve setup scripts for development (Improve setup scripts for development #322)
C lib flag (C lib flag #260)
Emit an error message when rmc-rustc fails (Emit an error message when rmc-rustc fails #328)
Codegen new intrinsic raw_eq (Codegen new intrinsic raw_eq #331)
Use Rust's vtable_entries (Use new vtable_entries API #329)
Extract examples from reference and display their results in a dashboard. (Extract examples from reference and display their results in a dashboard. #325)
Symbol table transformer (Symbol table transformer #321)
Use x.py to build and run the dashboard. (Use x.py to build and run the dashboard. #333)
Fix dyn trait _fail tests compilation errors (Fix dyn trait _fail tests compilation errors #342)
Remove string that tripped open source alarm. (Remove string that tripped open source alarm. #344)
Differentiate between check, codegen, and verification errors. (Differentiate between check, codegen, and verification errors. #353)
Generics in dyn trait fix: use vtable index to resolve functions (Generics in dyn trait fix: use vtable index to resolve functions #352)
Add support for simd insert/extract intrinsics (Add support for simd insert/extract intrinsics #354)
Conform with recent changes in rustc (alloc id, scalar ptr, vtable method) (Conform with recent changes in rustc (alloc id, scalar ptr, vtable method) #361)
Cleanup rmc flags (Cleanup rmc flags #365)
Fix dry-run to print to stdout when output_to is not stdout. (Fix dry-run to print to stdout when output_to is not stdout. #366)
Detect which reference examples should check/codegen/verify. (Detect which reference examples should check/codegen/verify. #363)
Correct function type for vtable shim (fix some boxed closures) (Correct function type for vtable shim (fix some boxed closures) #335)
Support cargo rmc flags (Support cargo rmc flags #371)
Removed incorrect special case for Rust bitwise operators

Description of changes:

Describe RMC's current behavior and how your code changes that behavior. If there are no issues this PR is resolving, explain why this change is necessary.

Resolved issues:

Resolves #ISSUE-NUMBER

Call-outs:

Testing:

How is this change tested?
Is this a refactor change?

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

…h them (#23)

…ng (#15)

* Squash warnings: remove final use of insert_unchecked * wWe only use ensure_global_var as an expr, so make it return that * cleanup how codegen_alloc_in_memory generates global vars

* Special case fat-ptr to fat-ptr casts * Fix issues in rvalue computation related to ADT fat pointers * Assign statements now always type-check. Remove the special casing for when they didn't

* Add RMC workflow file for GitHub Actions * Add multiple setup scripts used by workflow * Improvements for Actions worflow and setup scripts

This is a temporary workaround for the vtable duplicate field issue (#30). Since we can detect this case at translation time, we mark the vtable as ill-formed. This is checked at proof-time so any code that relies on using an ill-formed vtable function will fail. Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

…ng#79) * Add a couple of missing tests (nondet. vectors, offset) * Add `test_offset_str` to BinOp_Offset test * Add assertions in `NondetVectors` test Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

…hecking#88) * Complete and replace the unsized pointer cast implementation * Respond to code review of unsized pointer cast implementation Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

Add fat-pointer regression tests

* Update README.md * Split off a separate DEVELOPER-GUIDE

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

* Allow cast of any pointer to cast to a trait pointer Also: * Add predicates `use_*_pointer(mir_type)` to use mir pointer metadata to identify the correct type of pointer to a mir type. * Use predicates `use_*_pointer(mir_type)` in fat pointer construction Resolves model-checking#83 Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

Also: * Correctly cast before dereferencing a thin pointer to a flexible struct * Correct search for trait type in adt (ignore primitive types and pointers) * Correct the choice between thin and fat pointers in codegen_fat_ptr and codegen_ty_ref (and rewrite to use mir pointer metadata) Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

) * Correct fat pointer generation by codegen_rvalue_ref Also restore the SizeAndAlignOfDst regression that now passes. * Respond to code review on correct fat pointer in codegen rvalue ref Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

This resolves issue model-checking#34 Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

) * Workaround for issue model-checking#95 * Print types in assert statement Co-authored-by: Nathan Chong <ncchong@amazon.com>

* Add support for multiple expected failures. * Check for expected failures on RMC's output instead of test file. * Address concerns.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

…g#318) For branch `main-153-2021-07-09`

…ing#320) * Fix codegen local for Fn::call and FnMut::call_mut * Review comments * Whitesapce * Typo

* Use `--unwinding-assertions` flag by default * Scan CBMC output and make recommendations (unwinding) * Use `--no-default-flags` in Leibniz's test to avoid failure * Split checks into groups. Add flags for groups. Print flags. * Allow dry runs for rmc and cargo-rmc * Add starter-kit checks and fix tests * Add expected test for dry-run feature * Dry-run: Emulate running proc. instead of just printing * Add explanations for checks disabled. Other minor fixes. * Order. Rename. Cover flags.

* Define dependencies with an array Among other things, this will allow us to comment on them in the future. * Add missing (non-CI) dependency Running setup scripts on the default Ubuntu AMI results in this error message: ``` + sudo python3 -m pip install --upgrade cbmc_viewer-2.5-py3-none-any.whl /usr/bin/python3: No module named pip ``` This fixes the issue. * Use the downloaded file, if already downloaded wget has a default behavior that causes downloads like this to get new unexpected filenames if the file already exists. The switch to curl is simply personal preference. * swap back to wget * keep deps in alpha order for now

* Added --c-lib flag to rmc and cargo-rmc. * Added rmc test for extern C files. * Added cargo-rmc example for extern C files. * PR fixes. * Fixups after rebase. * PR fixes.

* Emit an error message when rmc-rustc fails * indicate what was missing in rmc-rustc error message

…ard. (model-checking#325) * Extract examples from The Rust Reference and display their results in a terminal dashboard. * Address PR comments. * Clarify comment. * Replace `rfind` with `rsplitn`.

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

* Use `x.py` to build and run the dashboard. * Stop looking for copyright notice in markdown files. Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

…-checking#353) * Differentiate between check, codegen, and verification errors. * Fix typo. * Rename tests. * Address concerns. * Remove unnecessary code and fix typos.

…el-checking#352) Use vtable index passed at call site to resolve functions Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

* support simd_extract intrinsic * support simd_insert intrinsic * move insert/extract tests to their own tile * extract codegen_intrinsic_simd_insert Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

…thod) (model-checking#361) * Refactor for alloc_id iterators * Access scalar pointer values via `into_parts` * Trait compile fixes * Vtable field name workaround * Remove `unused doc comment` warning

* Rearranges common flags between `rmc` and `cargo rmc` into groups in a shared file to allow better organization and easier changes in the future. * Adds help strings to all of the flags to explain their purpose.

…hecking#366)

…hecking#363) * Copy options from the rust code blocks in the markdown files. * Fix typos and add comments.

…l-checking#335) Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

* Support gen-symbols. * Support allow-cbmc-verification-failure

danielsn and others added 30 commits July 26, 2021 14:32

Minimal changes to rustc to enable RMC

e8fe9ae

Renamed files to avoid name conflicts

89a89dd

initial rmc commit

fbb987e

Fix out-by-one errors in cargo-rmc-tests and run-make tests (#17)

df0e29a

Add regression test for model-checking#21 (#22)

0165377

Refactor codegen_vtable and vtable_name (#24)

819884b

Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

Correctly track the type of boxed fat pointers when projecting throug…

0f34cdb

…h them (#23)

Fix issue where array types were recorded as [x; _] and hence aliasi…

e23c5d5

…ng (#15)

Conform with latest changes to Binder (used in closures) (#27)

0e38dbf

Squashed a bunch of warnings (#28)

72cd753

Squash warnings: remove final use of insert_unchecked (#29)

c9f05e1

* Squash warnings: remove final use of insert_unchecked * wWe only use ensure_global_var as an expr, so make it return that * cleanup how codegen_alloc_in_memory generates global vars

Properly handle Fat-ptr to Fat-ptr casts (model-checking#62)

3354e85

* Special case fat-ptr to fat-ptr casts * Fix issues in rvalue computation related to ADT fat pointers * Assign statements now always type-check. Remove the special casing for when they didn't

Add RMC workflow file for GitHub Actions (#31)

27db8e6

* Add RMC workflow file for GitHub Actions * Add multiple setup scripts used by workflow * Improvements for Actions worflow and setup scripts

Add templates for Pull Requests and Issues (model-checking#81)

58a2860

Complete and replace the unsized pointer cast implementation (model-c…

1411c8f

…hecking#88) * Complete and replace the unsized pointer cast implementation * Respond to code review of unsized pointer cast implementation Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

Add script and workflow for copyright checks in CI (model-checking#92)

26b349f

Add unsized pointer cast regression tests (model-checking#89)

4d0479d

Add fat-pointer regression tests

update readme (model-checking#91)

445584e

* Update README.md * Split off a separate DEVELOPER-GUIDE

Add nondet. bytes test (model-checking#94)

b988803

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

Enable regression workflow for macOS (model-checking#97)

9aa43cd

Minor tweaks to the documentation (model-checking#100)

1f6ba24

Add box mut dyn trait regression test (model-checking#108)

a5b7c57

This resolves issue model-checking#34 Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>

Avoid strict type comparison in statement assignment (model-checking#110

46a2545

) * Workaround for issue model-checking#95 * Print types in assert statement Co-authored-by: Nathan Chong <ncchong@amazon.com>

Extend entry_fn call to use local defid

8d3caca

Implemented __VERIFIER_assume hook (model-checking#115)

a32fadc

bdalrhm and others added 27 commits July 26, 2021 14:34

Add support for multiple expected failures. (model-checking#280)

c69c907

* Add support for multiple expected failures. * Check for expected failures on RMC's output instead of test file. * Address concerns.

Codegen the rest of std lib and add a regression script

e537b08

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

Update dyn trait tests from raw to ptr Rust APIs (model-checking#306)

eec6298

Custom panic hook for RMC including current item (model-checking#304)

fa65496

Conform with recent changes in rustc (limits, binders) (model-checkin…

20f1213

…g#318) For branch `main-153-2021-07-09`

Fix codegen for dynamic Fn::call and FnMut::call_mut (model-check…

a7795be

…ing#320) * Fix codegen local for Fn::call and FnMut::call_mut * Review comments * Whitesapce * Typo

C lib flag (model-checking#260)

9c90b22

* Added --c-lib flag to rmc and cargo-rmc. * Added rmc test for extern C files. * Added cargo-rmc example for extern C files. * PR fixes. * Fixups after rebase. * PR fixes.

Emit an error message when rmc-rustc fails (model-checking#328)

9d65935

* Emit an error message when rmc-rustc fails * indicate what was missing in rmc-rustc error message

Codegen new intrinsic raw_eq (model-checking#331)

e5f4672

Use Rust's vtable_entries (model-checking#329)

ff5cd92

Extract examples from reference and display their results in a dashbo…

9f4db77

…ard. (model-checking#325) * Extract examples from The Rust Reference and display their results in a terminal dashboard. * Address PR comments. * Clarify comment. * Replace `rfind` with `rsplitn`.

Symbol table transformer (model-checking#321)

053aafb

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

Use x.py to build and run the dashboard. (model-checking#333)

9a19938

* Use `x.py` to build and run the dashboard. * Stop looking for copyright notice in markdown files. Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

Fix dyn trait _fail tests compilation errors (model-checking#342)

baebe0c

Remove string that tripped open source alarm. (model-checking#344)

e7e6a13

Differentiate between check, codegen, and verification errors. (model…

8f4a5bc

…-checking#353) * Differentiate between check, codegen, and verification errors. * Fix typo. * Rename tests. * Address concerns. * Remove unnecessary code and fix typos.

Generics in dyn trait fix: use vtable index to resolve functions (mod…

09409f8

…el-checking#352) Use vtable index passed at call site to resolve functions Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

Conform with recent changes in rustc (alloc id, scalar ptr, vtable me…

22d72ef

…thod) (model-checking#361) * Refactor for alloc_id iterators * Access scalar pointer values via `into_parts` * Trait compile fixes * Vtable field name workaround * Remove `unused doc comment` warning

Cleanup rmc flags (model-checking#365)

78f20f4

* Rearranges common flags between `rmc` and `cargo rmc` into groups in a shared file to allow better organization and easier changes in the future. * Adds help strings to all of the flags to explain their purpose.

Fix dry-run to print to stdout when output_to is not stdout. (model-c…

cc7f935

…hecking#366)

Detect which reference examples should check/codegen/verify. (model-c…

a37593c

…hecking#363) * Copy options from the rust code blocks in the markdown files. * Fix typos and add comments.

Correct function type for vtable shim (fix some boxed closures) (mode…

72c9b37

…l-checking#335) Correct vtable shim self type (add fixme for other cases) Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>

Support cargo rmc flags (model-checking#371)

14eeec2

* Support gen-symbols. * Support allow-cbmc-verification-failure

Removed incorrect special case for Rust bitwise operators

6c46d9d

zhassan-aws closed this Aug 6, 2021

chinmaydd mentioned this pull request Aug 6, 2021

Fix failing codegen in due to incorrect boolean types #396

Closed

4 tasks

zhassan-aws deleted the fix-bit-logic-operators branch January 6, 2023 17:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix bit logic operators #395

fix bit logic operators #395

zhassan-aws commented Aug 6, 2021

fix bit logic operators #395

fix bit logic operators #395

Conversation

zhassan-aws commented Aug 6, 2021

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist