Reset namespace after symbolic execution

[tautschnig]

The state's symbol table may go out of scope, leaving the namespace with a
dangling pointer. This is a follow-up to e8eec2c.

This fix is factored out from #1868, which has regression tests that fail without this fix. The reason other regression tests don't catch this is that the namespace isn't used afterwards. Pinging @karkhaz and @kroening for discussion.

[karkhaz]

Thanks for this fix! Would it make sense to also include the tests in this commit?

[tautschnig]

@karkhaz Do you see ways of coming up with some even better fix? The current set-up is still dangerous as it requires this manual reset of the namespace. A test might have to be a unit test to enforce some namespace lookups.

[karkhaz]

@tautschnig I'm not sure why it's dangerous? I think symex_with_state is the only symex function that needs this setup and reset of ns, so now that you've fixed it I'm not sure what problems you anticipate in the future?

Tests: do you mean a unit test of the symex_with_state function? It seems like that test would need some fairly involved setup, since we would need to pass a partially-executed state plus a symbol table as parameters. We get all that stuff for free with the regression test you wrote. One approach that occurred to me is to implement __CPROVER_lookup_symbol(sym) that would print out or return the symbol table that sym was found in? Not sure if that makes sense, but if you did that you could do a string match of the symbol table you expect in the regression test. Anyway, I think the regression test you posted seems fine, it's checking for what we need as far as I can see...

[tautschnig]

What makes me slightly uncomfortable is the non-const ns member, which does get updated (and, in this PR, reset). But it's probably ok. @kroening appeared to be concerned (in #1868).

[karkhaz]

Oh, I see. Not sure how to deal with this apart from making the ns member const, and passing a namespacet &new_namespace to the function instead of a symbol_tablet &new_symbol_table. new_namespace would get its outer symbol table from the const ns member, and the inner symbol from the state...then BMC would be able to use both of those tables when symex returns. The only problem would be that we would have to pass new_namespace as an argument to whoever wants to update it, and not update the ns member anymore. Not sure if that's a good idea, it seems like overkill.

[tautschnig]

I'd agree that leaving things as they are should be ok. But hoping for @kroening to comment for a better understanding of concerns.

[tautschnig]

@kroening Ping?

[tautschnig]

This is blocking progress on another PR - added @peterschrammel in the hope to get this reviewed.