Enable fat pointer comparison for slices and add check for vtable ones #1195

celinval · 2022-05-12T20:21:11Z

Description of changes:

Currently, we don't support fat pointer comparison. This issue adds support for slice fat pointer comparison and a proper check that will fail the verification if its trying to compare vtable fat pointers.

Resolved issues:

Resolves #327

Call-outs:

I documented in the original issue #327 why I don't think we should compare vtable fat pointers. In a nutshell, this operation is not UB but it is unstable. I.e.: The behavior may depend on the compilation / linking process.

I kept a similar behavior to thin pointers when comparing the data pointer portion of the fat pointer. Comparing pointers that have different precedence will also fail.

We could add optional support to the operations mentioned above using uninterpreted functions, but I will defer that to when we see demand for it.

Testing:

How is this change tested? New 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.

zhassan-aws

Neat! Thanks Celina!

zhassan-aws · 2022-05-13T17:01:22Z

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

-            BinOp::Gt => self.codegen_operand(e1).gt(self.codegen_operand(e2)),
-            _ => unreachable!(),
-        }
+        let left = self.codegen_operand(e1);


Nice refactoring!

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

zhassan-aws · 2022-05-13T19:43:31Z

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

+            // Codegen an assertion failure since vtable comparison is not stable.
+            let ret_type = Type::Bool;
+            let body = vec![
+                self.codegen_assert_false(


Is it not possible to use codegen_unimplemented instead?

EDIT: I now see that this is due to the property class. Perhaps this needs refactoring to add a property-class parameter in a follow-up PR.

I don't think this should use codegen_unimplemented() though. This is by design and it's meant to alert users of behaviour instability.

I think we should only use codegen_unimplemented for things that Kani can't yet handle.

Perhaps we can put the code under codegen_unimplemented in a function with a more generic name (e.g. codegen_assert_assume_false), and call that function from codegen_unimplemented and codegen_unstable?

EDIT: Not necessarily in this PR.

My bad, I think we already have that. codegen_fatal_error() should do it. It uses Abort instead of assume.

It actually takes Span instead of Location. So I'll leave this change for another time. Sorry!

zhassan-aws · 2022-05-13T19:49:08Z

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

+                // It is different if any is different.
+                BinOp::Ne => data_cmp.or(metadata_cmp),
+                // If data is different, only compare data.
+                // If data is equal, apply operator to metadata.


Any references for this logic?

Sure. Let me find the PR that implemented this on the rust compiler side.

Yes, we need a reference here.

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

adpaco-aws · 2022-05-13T22:12:11Z

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

-            _ => unreachable!(),
-        }
+        let left = self.codegen_operand(e1);
+        let right = self.codegen_operand(e2);


Nit: left_op and right_op.

adpaco-aws · 2022-05-13T22:13:51Z

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

+                self.codegen_assert_false(
+                    PropertyClass::KaniCheck,
+                    format!("Reached unstable vtable comparison '{:?}'", op).as_str(),
+                    Location::None,


Is there a way to get the locations for these statements? If so, I suggest adding them.

I can try to refactor things a bit to pass down the location.

adpaco-aws · 2022-05-13T22:14:45Z

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

+                // It is different if any is different.
+                BinOp::Ne => data_cmp.or(metadata_cmp),
+                // If data is different, only compare data.
+                // If data is equal, apply operator to metadata.


Yes, we need a reference here.

1. This only works for pointers with the same provenance. 2. We should model vtable comparison a bit differently. Follow up commit

- Rename variables. - Add location to the assertion and other statements. - Added a link to the compiler PR that implemented fat pointer comparison. I did not change the assert / assume logic to a different function yet.

Co-authored-by: Zyad Hassan <[email protected]>

celinval requested a review from a team as a code owner May 12, 2022 20:21

zhassan-aws approved these changes May 13, 2022

View reviewed changes

adpaco-aws reviewed May 13, 2022

View reviewed changes

celinval added 4 commits May 14, 2022 15:34

Implement pointer comparison for fat pointers

105f3f2

1. This only works for pointers with the same provenance. 2. We should model vtable comparison a bit differently. Follow up commit

Use integer comparison for vtable.

0ac3290

Add check for unstable vtable pointer comparison

b66491a

Address the following PR comments

da4d81f

- Rename variables. - Add location to the assertion and other statements. - Added a link to the compiler PR that implemented fat pointer comparison. I did not change the assert / assume logic to a different function yet.

celinval force-pushed the issue-327-fix branch from 2b73e46 to da4d81f Compare May 14, 2022 22:56

adpaco-aws approved these changes May 16, 2022

View reviewed changes

adpaco-aws and others added 2 commits May 16, 2022 10:54

Merge branch 'main' into issue-327-fix

193007a

Apply suggestions from code review

04247ce

Co-authored-by: Zyad Hassan <[email protected]>

celinval merged commit 25dfce5 into model-checking:main May 16, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Enable fat pointer comparison for slices and add check for vtable ones #1195

Enable fat pointer comparison for slices and add check for vtable ones #1195

celinval commented May 12, 2022 •

edited

Loading

zhassan-aws left a comment

zhassan-aws May 13, 2022

zhassan-aws May 13, 2022

celinval May 13, 2022

celinval May 13, 2022

zhassan-aws May 13, 2022 •

edited

Loading

celinval May 14, 2022

celinval May 14, 2022

zhassan-aws May 13, 2022

celinval May 13, 2022

adpaco-aws May 13, 2022

adpaco-aws May 13, 2022

celinval May 13, 2022

adpaco-aws May 13, 2022

celinval May 13, 2022

adpaco-aws May 13, 2022

Enable fat pointer comparison for slices and add check for vtable ones #1195

Enable fat pointer comparison for slices and add check for vtable ones #1195

Conversation

celinval commented May 12, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

zhassan-aws left a 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

zhassan-aws May 13, 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval commented May 12, 2022 •

edited

Loading

zhassan-aws May 13, 2022 •

edited

Loading