Audit for `ptr_guaranteed_<cmp>` #1090

adpaco-aws · 2022-04-21T21:45:10Z

Description of changes:

Completes the audit for ptr_guaranteed_<cmp>. These behave as regular pointer comparison at runtime.

Resolved issues:

Part of #727

Call-outs:

Testing:

How is this change tested? Adds 2 tests.
Is this a refactor change? No.

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.

danielsn · 2022-04-22T02:34:45Z

docs/src/rust-feature-support.md

-ptr_guaranteed_eq | Partial | |
-ptr_guaranteed_ne | Partial | |
+ptr_guaranteed_eq | Yes | Over-approximation: Returns nondet. value even if comparison is true |
+ptr_guaranteed_ne | Yes | Over-approximation: Returns nondet. value even if comparison is true |


Should one of these say "false"

No, these are not symmetric in the sense that if one returns true, the other one returns false. Under some circumstances, both may return false even if one of them would return true using standard (in)equality, which is the desired behavior. See https://doc.rust-lang.org/std/primitive.pointer.html#method.guaranteed_eq for more details.

danielsn · 2022-04-22T02:37:27Z

tests/kani/Repr/main_fixme.rs

@@ -17,5 +17,8 @@ fn mmap() -> *mut MyCVoid {
 fn main() {
    let v = mmap();
    assert!(v != MAP_FAILED);
+    // The assertion below fails because it must be using `ptr_guaranteed_eq` or


Why must it?

The test broke because the intrinsics changed here are less precise now. This is just a hint I wanted to include for when we come back to fix the test.

danielsn · 2022-04-22T02:37:57Z

tests/kani/Intrinsics/PtrGuaranteedCmp/ne_ok.rs

+// equal, which causes the test to pass in the `else` branch. The `if`
+// branch is unreachable.


Should we test that this branch is unreachable, maybe with an assert false?

Because we are assuming ptr1 == ptr2, the unreachable assertion is in practice assert!(false).

celinval · 2022-04-22T00:33:27Z

tests/kani/Intrinsics/PtrGuaranteedCmp/eq_fail.rs

+    if ptr_guaranteed_eq(ptr1, ptr2) {
+        assert!(ptr1 == ptr2);
+    } else {
+        assert!(ptr1 != ptr2);


Can you use expect_fail instead? Tests with kani-verify-fail would succeed even if CBMC crashes.

celinval · 2022-04-22T00:33:50Z

tests/kani/Intrinsics/PtrGuaranteedCmp/eq_fail.rs

+
+#[kani::proof]
+fn test_ptr_eq(ptr1: *const u8, ptr2: *const u8) {
+    kani::assume(ptr1 == ptr2);


I would remove this assumption. The assertion on line 14 should still hold.

celinval · 2022-04-22T00:34:45Z

tests/kani/Intrinsics/PtrGuaranteedCmp/eq_ok.rs

+
+#[kani::proof]
+fn test_ptr_eq(ptr1: *const u8, ptr2: *const u8) {
+    kani::assume(ptr1 != ptr2);


If you use expect_fail() this test can be merged with the one above.

celinval · 2022-04-22T00:39:45Z

tests/kani/Repr/main_fixme.rs

@@ -17,5 +17,8 @@ fn mmap() -> *mut MyCVoid {
 fn main() {
    let v = mmap();
    assert!(v != MAP_FAILED);
+    // The assertion below fails because it must be using `ptr_guaranteed_eq` or
+    // `ptr_guaranteed_eq`, which now returns a nondet. value if the result of
+    // the comparison is true
    assert!(v.is_null());


Humm... let's sync offline. We might have to revert the behavior. We don't want ptr::is_null() to become nondet. :(

adpaco-aws · 2022-04-26T20:24:04Z

The PR is ready to review again.

We had a discussion where we agreed that these intrinsics should be implemented as regular comparison instead of being over-approximated, otherwise we get nondet. results for comparison like ptr::is_null. This has been noted in both the Kani documentation and code.

zhassan-aws · 2022-04-26T21:46:46Z

tests/kani/Intrinsics/PtrGuaranteedCmp/eq.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail


Is kani-verify-fail required?

It was not needed, but I changed the tests to have (each) two positive harnesses instead.

zhassan-aws · 2022-04-26T21:50:40Z

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

+        // are used for regular comparison in `std` when they shouldn't. An earlier
+        // version that returned nondet. values when the result of the comparison


because they are used for regular comparison in std when they shouldn't

This sounds a bit too strong for me. The documentation (https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq) says that this may spuriously return false in compile-time evaluation, which I understood to mean that it may block some optimizations, etc., but it can never impact correctness since it behaves like ==/!= at run-time (which is what we're modeling).

Thanks for making this clear! Removed the comments here and in Kani docs.

danielsn · 2022-04-26T22:04:47Z

tests/kani/Intrinsics/PtrGuaranteedCmp/ne.rs

+fn test_ptr_eq(ptr1: *const u8, ptr2: *const u8) {
+    kani::assume(ptr1 != ptr2);
+    assert!(ptr_guaranteed_ne(ptr1, ptr2));
+    kani::expect_fail(ptr1 == ptr2, "Pointers aren't equal");


Should this use !ptr_guaranteed_ne? And will it even be reachable given how we turn assert into assert; assume

I changed the tests to have (each) two positive harnesses instead, please check.

zhassan-aws

Thanks @adpaco-aws!

adpaco-aws · 2022-04-27T12:59:53Z

Merging this PR now, but if you have any other concerns please let me know and I'll take care of them.

* Audit for `ptr_guaranteed_<cmp>` * Update docs * Add two tests

adpaco-aws requested a review from a team as a code owner April 21, 2022 21:45

adpaco-aws changed the title ~~Ptr guaranteed audit~~ Audit for ptr_guaranteed_<cmp> Apr 21, 2022

adpaco-aws force-pushed the ptr_guaranteed-audit branch from d036af4 to 17a9819 Compare April 21, 2022 21:56

danielsn reviewed Apr 22, 2022

View reviewed changes

celinval reviewed Apr 22, 2022

View reviewed changes

adpaco-aws added 7 commits April 26, 2022 19:25

Audit for ptr_guaranteed_<cmp>

852447e

Update docs

1b54674

Minor fix in test

c155674

Discard notes on rust support table

6758da4

Add notes on docs

7486d57

Restore regular comparison

4e743de

Add two tests, restore Repr one

2760dc8

adpaco-aws force-pushed the ptr_guaranteed-audit branch from befd424 to 2760dc8 Compare April 26, 2022 20:17

Minor fix to test

1254375

adpaco-aws requested review from danielsn and celinval April 26, 2022 20:24

zhassan-aws reviewed Apr 26, 2022

View reviewed changes

danielsn reviewed Apr 26, 2022

View reviewed changes

adpaco-aws added 4 commits April 27, 2022 00:30

Fix tests

7382f4d

Update documentation

8ec85ee

Remove warning

371bd3e

Fix format

980d3b1

zhassan-aws approved these changes Apr 27, 2022

View reviewed changes

Merge branch 'main' into ptr_guaranteed-audit

ba01efb

adpaco-aws merged commit 844a486 into model-checking:main Apr 27, 2022

adpaco-aws mentioned this pull request Apr 27, 2022

Intrinsics Audit #727

Closed

tedinski pushed a commit that referenced this pull request Apr 27, 2022

Audit for ptr_guaranteed_<cmp> (#1090)

571e269

* Audit for `ptr_guaranteed_<cmp>` * Update docs * Add two tests

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Audit for `ptr_guaranteed_<cmp>` #1090

Audit for `ptr_guaranteed_<cmp>` #1090

adpaco-aws commented Apr 21, 2022 •

edited

Loading

danielsn Apr 22, 2022

adpaco-aws Apr 22, 2022 •

edited

Loading

danielsn Apr 22, 2022

adpaco-aws Apr 22, 2022

danielsn Apr 22, 2022

adpaco-aws Apr 22, 2022

celinval Apr 22, 2022

celinval Apr 22, 2022

celinval Apr 22, 2022

celinval Apr 22, 2022

adpaco-aws commented Apr 26, 2022

zhassan-aws Apr 26, 2022

adpaco-aws Apr 27, 2022 •

edited

Loading

zhassan-aws Apr 26, 2022

adpaco-aws Apr 27, 2022

danielsn Apr 26, 2022

adpaco-aws Apr 27, 2022

zhassan-aws left a comment

adpaco-aws commented Apr 27, 2022

		// equal, which causes the test to pass in the `else` branch. The `if`
		// branch is unreachable.

		// are used for regular comparison in `std` when they shouldn't. An earlier
		// version that returned nondet. values when the result of the comparison

Audit for ptr_guaranteed_<cmp> #1090

Audit for ptr_guaranteed_<cmp> #1090

Conversation

adpaco-aws commented Apr 21, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Choose a reason for hiding this comment

adpaco-aws Apr 22, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adpaco-aws commented Apr 26, 2022

Choose a reason for hiding this comment

adpaco-aws Apr 27, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zhassan-aws left a comment

Choose a reason for hiding this comment

adpaco-aws commented Apr 27, 2022

Audit for `ptr_guaranteed_<cmp>` #1090

Audit for `ptr_guaranteed_<cmp>` #1090

adpaco-aws commented Apr 21, 2022 •

edited

Loading

adpaco-aws Apr 22, 2022 •

edited

Loading

adpaco-aws Apr 27, 2022 •

edited

Loading