dreal/dreal3

Memory leak in translate_enode_to_exprnode

Opened this issue · 2 comments

cgd8d commented

There is a memory leak in translate_enode_to_exprnode. I believe it exhibits itself in many different ways, but to be concrete, imagine the expression (+ 1 2) is being processed. This will reduce to the following pseudocode:

return &(*translate_enode_to_exprnode(“1”) + *translate_enode_to_exprnode(“2”));

which is essentially equivalent to (again, pseudocode):

return &ibex::ExprAdd::new_(ibex::ExprConstant::new_scalar([1,1]),
                            ibex::ExprConstant::new_scalar([2,2]))

For this particular realization, the memory leak is that ibex::ExprConstant::new_scalar allocates memory, ExprAdd takes ownership of that memory (as members “left” and “right”), but when the ExprAdd is deleted, it has no non-default destructor so it does not destroy those objects.

More generally, ibex::ExprBinaryOp has two references, but does not delete those references, so if it does have ownership then the memory is leaked.

In principle, since ibex::ExprBinaryOp exposes its members, a user program like dreal3 could work very hard to manage the memory itself. Thus, I submit this bug report to dreal3 even though I suspect it should be pushed upstream to ibex.

One complication I see with fixing the bug in ibex is that it is possible for functions to create an ExprBinaryOp where they do not want ExprBinaryOp to take ownership of those references, eg. someone could call ExprAdd::new_ with arguments they want to own. Maybe ibex does not intend to permit that kind of use, but it is not currently forbidden by the interface. If that is acceptable, then the easy fix in ibex may be to add the following destructor to ExprBinaryOp:

virtual ~ExprBinaryOp() {
    delete &left;
    delete &right;
}

At any rate, I have very limited familiarity with ibex, so I would be happy to submit a bug report there or to leave this bug in your hands, whatever you suggest.

Thanks for the report. As far as I know this is a known-issue in the ibex team. Last time I asked it, they gave me a workaround but I forget the details now. I'll check things up this weekend.

cgd8d commented

Thanks, much appreciated!