Drop for dynamic objects #402

avanhatt · 2021-08-06T19:08:01Z

Description of changes:

RMC does not current codegen calls to drop for dynamic objects. This PR does that, inserting vtable calls as necessary.

Resolved issues:

Resolves #66
Should also resolve #435

Call-outs:

Known issue with the SizeAndAlignOfDst tests. This patch has a workaround to insert a codegen_unimplemented call in the case that drop fails to typecheck, which maintains soundness (the current implementation is not sound because it does not call drop at all).

Testing:

How is this change tested?

Existing plus 7 new regressions.

Is this a refactor change?

Not really.

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.

chinmaydd · 2021-08-20T18:47:26Z

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs

+                let type_from_mir = ctx.codegen_ty(t);
+                if expr_ty != type_from_mir { Some((expr_ty, type_from_mir)) } else { None }
+            }
+            TypeOrVariant::Variant(_) => None, //TODO, what to do here?


Do we want to create an issue for this ? Not sure if this is tracked somewhere..

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs

danielsn · 2021-08-23T21:08:17Z

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/rvalue.rs

+                format!("drop_in_place for {}", drop_sym_name).as_str(),
+                trait_fn_ty,
+                Location::none(),
+                "https://github.com/model-checking/rmc/issues/202",


Is this the right link? #202

Oops no it should actually be #281.

The problem is when we skip functions in should_skip_current_fn, the thing we're skipping could be a drop that's called elsewhere. #202 is the first function we skip but bridge::client, #281, is where we actually see it

danielsn · 2021-08-25T13:48:53Z

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/rvalue.rs

-                self.readable_instance_name(drop_instance),
-            );
-            Type::void_pointer().null().cast_to(trait_fn_ty)
+            self.codegen_unimplemented(


Does this typecheck? We want a pointer to an unimplemented function, and instead we're getting an unimplemented function that returns a fn pointer.

It does type check, we cast to the same type in the if case. I don't think we have any unit tests that hit this, only the standard library regression.

The issue is that this code is called in a constructor, so it will always fail at CBMC time (which is sound, but not helpful). I think what we want is to make a function whose body is unimplemented, and put a pointer to that function into the vtable.

danielsn · 2021-08-25T13:49:48Z

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs

-        let instance = Instance::resolve_drop_in_place(self.tcx, loc_ty);
-        if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) {
+        let drop_instance = Instance::resolve_drop_in_place(self.tcx, loc_ty);
+        if let Some(hk) = self.hooks.hook_applies(self.tcx, drop_instance) {


Do we still need the hook here? Or could we just move its logic inside the regular codegen?

Without it, we fail on:

failures: [expected] expected/replace-hashmap/main.rs [expected] expected/replace-vec/main.rs

danielsn · 2021-08-25T13:52:02Z

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs

+                        }
+                        _ => {
+                            // Non-virtual, direct drop call
+                            assert!(!matches!(drop_instance.def, InstanceDef::Virtual(_, _)));


Can we assert this above? Would that be a better check than matching on loc_ty.kind()

The conditional doesn't work as a check, because asserting the inverse in the dynamic case fails whenever the instance def is InstanceDef::DropGlue instead of ::Virtual. This structure also matches how the Cranelift backend handles this case.

danielsn · 2021-08-25T13:52:42Z

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs

+                            let func = self.codegen_func_expr(drop_instance, None);
+                            let place = self.codegen_place(location);
+                            let arg = if let Some(fat_ptr) = place.fat_ptr_goto_expr {
+                                // Drop takes the fat pointer if it exists


This would be in the case of dropping a slice?

We've also seen it be a fat pointer to a nested dynamic object.

danielsn · 2021-08-25T13:57:32Z

src/test/cbmc/DynTrait/drop_nested_boxed_dyn_fail.rs

+        let _nested: Box<dyn Send> = Box::new(x);
+    }
+    unsafe {
+        assert!(CELL == 2); // Should fail


use the expect_fail macro

avanhatt force-pushed the dyn-drop branch from a5814a5 to 16a9037 Compare August 6, 2021 19:14

avanhatt changed the base branch from main-154-2021-08-02 to main-154-2021-08-06 August 6, 2021 19:14

avanhatt force-pushed the dyn-drop branch 2 times, most recently from db28d0b to bb160fc Compare August 11, 2021 13:47

avanhatt force-pushed the dyn-drop branch from bb160fc to e1eb201 Compare August 16, 2021 14:36

avanhatt changed the title ~~(draft) Drop for dynamic objects~~ Drop for dynamic objects Aug 16, 2021

avanhatt marked this pull request as ready for review August 16, 2021 14:38

avanhatt force-pushed the dyn-drop branch from d57a012 to 77d10fa Compare August 16, 2021 18:14

chinmaydd mentioned this pull request Aug 18, 2021

RMC incorrectly reports an assertion failure on a two-dimensional vector #435

Closed

avanhatt force-pushed the dyn-drop branch from c0eadf6 to 34b92bb Compare August 18, 2021 15:29

avanhatt changed the base branch from main-154-2021-08-06 to main-154-2021-08-17 August 19, 2021 13:13

avanhatt force-pushed the dyn-drop branch from 716b351 to 08396ea Compare August 19, 2021 13:13

chinmaydd reviewed Aug 20, 2021

View reviewed changes

compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs Show resolved Hide resolved

avanhatt force-pushed the dyn-drop branch 3 times, most recently from 15388e3 to 671b741 Compare August 24, 2021 13:33

danielsn reviewed Aug 25, 2021

View reviewed changes

danielsn changed the base branch from main-154-2021-08-17 to main-154-2021-08-24 August 25, 2021 18:04

avanhatt force-pushed the dyn-drop branch from 671b741 to 24272ba Compare August 25, 2021 18:20

avanhatt added 3 commits August 26, 2021 15:19

rebase

cd99a20

issue

dd11c22

fmt

23a135a

avanhatt force-pushed the dyn-drop branch from 9184047 to 23a135a Compare August 26, 2021 16:45

avanhatt requested a review from danielsn August 30, 2021 14:11

danielsn approved these changes Aug 30, 2021

View reviewed changes

danielsn merged commit ef758e2 into model-checking:main-154-2021-08-24 Aug 30, 2021

chinmaydd mentioned this pull request Aug 30, 2021

Range-based vector extension failure #191

Closed

avanhatt deleted the dyn-drop branch September 14, 2021 15:23

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 22, 2022

Drop for dynamic objects (model-checking#402)

e35aceb

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 25, 2022

Drop for dynamic objects (model-checking#402)

c499c9c

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Drop for dynamic objects (model-checking#402)

027a2bf

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

Drop for dynamic objects (#402)

061bede

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Drop for dynamic objects #402

Drop for dynamic objects #402

avanhatt commented Aug 6, 2021 •

edited

Loading

chinmaydd Aug 20, 2021

avanhatt Aug 30, 2021

danielsn Aug 23, 2021

avanhatt Aug 25, 2021 •

edited

Loading

danielsn Aug 25, 2021

avanhatt Aug 25, 2021

danielsn Aug 30, 2021

danielsn Aug 25, 2021

avanhatt Aug 25, 2021

danielsn Aug 25, 2021

avanhatt Aug 30, 2021

danielsn Aug 25, 2021

avanhatt Aug 25, 2021

danielsn Aug 25, 2021

Drop for dynamic objects #402

Drop for dynamic objects #402

Conversation

avanhatt commented Aug 6, 2021 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

avanhatt Aug 25, 2021 • 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

avanhatt commented Aug 6, 2021 •

edited

Loading

avanhatt Aug 25, 2021 •

edited

Loading