Skip to content

make ~solvert virtual #528

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed

make ~solvert virtual #528

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6fdd3b9
make ~solvert virtual
Feb 11, 2017
f775927
make make ~cbmc_solver_with_propt virtual / remove double free
Feb 12, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 1 addition & 5 deletions src/cbmc/cbmc_solvers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ class cbmc_solver_with_propt: public cbmc_solverst::solvert
assert(_prop!=NULL);
}

~cbmc_solver_with_propt()
virtual ~cbmc_solver_with_propt()
{
delete prop;
}
Expand Down Expand Up @@ -157,8 +157,6 @@ class cbmc_solver_with_aigpropt: public cbmc_solver_with_propt
~cbmc_solver_with_aigpropt()
{
// delete prop before the AIG
delete prop;
prop=NULL;
delete aig;
}

Expand Down Expand Up @@ -189,8 +187,6 @@ class cbmc_solver_with_filet:public cbmc_solverst::solvert
~cbmc_solver_with_filet()
{
// delete the prop before the file
delete prop_conv_ptr;
prop_conv_ptr=NULL;
delete out;
}

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suspect this is still needed, as otherwise prop has a ref to a deleted object. The assertion virtual ~solvert() needs to go away.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't solvert own all the objects? The comment says: "The solver class (that takes care of allocated objects)" - which appears to be far from true. My suggestion is for solvert to take a second argument propt *prop that my be a nullptr. solvert should then take care of deleting all non-null members. Otherwise it's rather impossible to get the order of cleanup right (as seems to be proven).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is that it is not only prop. Some solvers need prop+aig, others a file,...

The simplest fix for the concrete case would be to turn cbmc_solvers.h:62 into

if(prop_conv_ptr!=NULL)
  delete prop_conv_ptr;

More generally, solvert could provide a facility to store any number of pointers in a given order and it is then responsible to clean them up in reverse order.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

May I dare to say that this is a bit of a broken design? Multiple pointers that need to be allocated and de-allocated in a certain sequence, with no well-defined ownership. Shouldn't object A referencing object B assume ownership of B, and therefore do the cleanup? Yes, this will end up as a bit more work than @mgudemann may have set out to do on this, but we should rather be re-architecting than running around with memory leaks.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is that the deallocation order is reverse to the subclass relation and therefore overloading the destructor performs the deallocation in exactly the wrong order.

I'll discuss a solution for this with @mgudemann.

Expand Down
2 changes: 1 addition & 1 deletion src/cbmc/cbmc_solvers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ class cbmc_solverst:public messaget
prop_conv_ptr = _prop_conv;
}

~solvert()
virtual ~solvert()
{
assert(prop_conv_ptr!=NULL);
delete prop_conv_ptr;
Expand Down