C++ API replace assert

[zwimer]

In the C++ API, the assert function is frequently used; I propose replacing most all invocations of it with C++ exceptions. For example, take the function below. If the user passes in one FPA and one BV, assert will be called, terminating the program without raising an exception. For this reason, users of the API must read how this function is implemented then wrap it with the very same logic that the API is meant to obscure to decide wether or not it is 'safe' to call the function without fear of the program being terminated.

This is particularly troublesome in multi-threaded program. On failure assert failures invoke std::abort. Best case, the user installed a custom sigabrt handler and now has to deal with trying to fix up the stack frame before resuming that thread causing, which is difficult and slow since it requires signals. More likely, however, the signal will terminate the program and thus all threads.

I propose we change this behavior. A custom failure function is possible, but I believe C++ exceptions provide the best answer here. If nothing else, we could replace assert(false); with something similar to:

if (ctx().enable_exceptions()) {
    throw Z3_API_Exception("Argument mismatch between within <= operator");
}
else {
    assert(false);
}

Function mentioned above:

    inline expr operator<=(expr const & a, expr const & b) {
        check_context(a, b);
        Z3_ast r = 0;
        if (a.is_arith() && b.is_arith()) {
            r = Z3_mk_le(a.ctx(), a, b);
        }
        else if (a.is_bv() && b.is_bv()) {
            r = Z3_mk_bvsle(a.ctx(), a, b);
        }
        else if (a.is_fpa() && b.is_fpa()) {
            r = Z3_mk_fpa_leq(a.ctx(), a, b);
        }
        else {
            // operator is not supported by given arguments.
            assert(false);
        }
        a.check_error();
        return expr(a.ctx(), r);
    }

[zwimer]

From my understanding, check_error() already does something similar to this internally, except by reading an error code within the context. In that case, perhaps one solution could be to define a new error code, and replace assert(false); with setting this error code.

[NikolajBjorner]

You are right that "assert" is misused. For parameter validation an API function should really throw an exception.

[zwimer]

If I were to make a PR, do you have a desired 'method' to do so? I'm inclined to say that we should just set an error code in context and reuse existing machinery. One of the reasons for this is that if enable_exceptions is set to false, this still permits propagating the error information out to the user via the context, as is the current method from my understanding of the code.

[zwimer]

I want to use the error codes described here:
https://github.com/Z3Prover/z3/blob/518296dbc10267d4a4b8589212feaeefca800022/src/util/error_codes.h
Though I think some might need to be added. For example in one case we assert 0 <= i and i < m_size. There are many ways to do this:

1. One could be a new code ERR_SIZE or ERR_BOUNDCHECK or ERR_USAGE.
2. Alternatively, we could make a new error code ERR_API to denote that this error happens that the API level, and not within the guts of z3.
3. We could also do both with ERR_API_SIZE, ERR_API_USAGE, etc.
4. Another option could be that we define ERR_API as 2^7 then we could do error code = ERR_SIZE | ERR_API.

Personally, I think the method should make it clear that this is an API or a usage error. With exceptions enabled, this could just be ERR_API then raise an exception with a custom error message explaining in more detail the issue, rather than setting the error code then invoking check_error with no extra context. With exceptions disabled though, the user would only receive the error code.

In my personal opinion, this is probably fine? When writing C++, if the user doesn't want to let exceptions propagate up they should use try catch blocks; so if they explicitly disable exceptions I'd hope that no user would be parsing the errors that result directly. C++ exceptions are fundamentally better at conveying what went wrong and where than a single number error code.

But if we do want to support conveying all relevant information with exceptions disabled, then adding the singular error code ERR_API is probably not the way we want to go, unless there is some way to add an error message as well that I'm unaware of. Regardless, these are not the only options. If you have a preferred method let me know.

Somewhat related, but is there a reason we #define these codes rather than create an enum? Or rather, since this is C++, an enum struct for type safety? If it needs to be C compatible, why not just an enum?

[zwimer]

@NikolajBjorner ^ That message was primarily for you, though I welcome input from anyone. I just don't want to code a PR that will be flat out rejected before reviewed since it uses an 'undesired' method.

[nunoplopes]

Not everybody uses exception, as there's a price to pay. Visual Studio still builds C++ programs with exceptions turned off by default.
I don't see asserts as a bad thing. They should only trigger during development, not when deployed. Asserts are even better as they are much easier to catch with the debugger as execution stops right away.

Not that I care about Z3's C++ API, but if I did, I would be against using exceptions there.

[zwimer]

I disagree with the asserts point as people will sometimes want to build with z3, not purely use it in release mode.

That said, what you said about VS just blew my mind. That's a kind of terrifying default given the docs from msft itself say to use them in most cases, as in encourage their usage. Exceptions costs, when not using them, can be mitigated with proper noexcept syntax; more importantly shared libraries can throw them up to the user, so disabling them outright by default seems like a very interesting design decision.

Wow, I tested this if you use cl directly indeed the unwinding portion is disabled. I did not get this result when using a VS C++ project, but still. That's insane. This blew my mind.

[NikolajBjorner]

There have been asks not to have exception behavior in the API. Hence the Z3_THROW macro.

[zwimer]

I see. Ok then.

[NikolajBjorner]

How about:

#define Z3_PARAM(x) { if (ctx().enable_exception() && !(x)) Z3_THROW(exception(#x)); assert(x); }

The argument that assertions don't get lost is more the onus of the consumer:
If the consumer catches exceptions and ignores them wholesale, it is the consumer's fault.

[zwimer]

Correct me if I'm wrong here, but assuming you are using the version of assert I think you are, assert is only used if _NDEBUG or some similar macro is not included, which I presume it is for release builds? But if assert is enabled when invoked and exceptions disabled, the assert will still terminate the program.

In my case, I am considering building z3 into my system directly for various reasons ranging from the PLT / GOT to inlining optimization benefits, which means when I am not building a release build these asserts will trigger. In my case I'll be using exceptions, but not everyone would.

In my opinion, we should be consistent about when the program is terminated regardless of if exceptions are enabled or not; assuming the consumer properly handles whatever comes out be it and error code or exception. I.e. termination of the program should not be determined by exceptions_enabled() if the consumer is properly handling error codes / exceptions.

[nunoplopes]

You need to listen to what people are tying to tell you: exceptions are not possible or desirable in many scenarios.
I've been using Z3 for more than a decade and the number of times I've passed wrong parameters to an API is quite small. Z3 is a tool for experts and it doesn't consume input from end-users directly. There's no need for fancy parameter checking. An assertion is sufficient.
Also, the more interesting argument checking is done inside Z3 and that terminates the program (or calls a callback).

[zwimer]

Whether or not we want error checking is a different question than how we should error check. assert is just the wrong tool in an API. The API already supports exceptions, but for error checking without exceptions we can do it some other way. And if we don't want it that's fine too.

Assert lacks the ability to call a callback, it just terminates; and it is being used for input validation the the API level. It is fundamentally just the wrong tool regardless if how you feel about exceptions or if we want error checking in the first place.

[NikolajBjorner]

It's all valid argument, but we have to preserve bandwidth on what really matters. Given how Z3 is used, the discussion about asserts seems not too important.

[zwimer]

I started this discussion because the asserts are blocking me from integrating Z3 currently because they crash the program anytime a thread or user makes a mistake rather than leaving it in a recoverable state. I can do the coding and make the PR, I just want to make sure my PR isn't dead on arrival.

I suppose I could just do

#define _NDEBUG
#include "z3++.h"
#undef _NDEBUG

Or something like that. I was just hoping to contribute back to z3 since this seems like a design flaw, even more so given there is existing machinery for a context-local exit code that propagates to an exception automatically if desired. If this would be too big a PR to approve though you can go ahead and close this discussion and I can just maintain a hard-fork of this file for my system.

[zwimer]

If we want these checks enabled, which I suppose is something worth asking itself (personally I think we should as the relative overhead of the check vs z3 internal computations should be tiny), I think they should be done so in a way that doesn't just crash all threads of the program / send a signal.

assert should be used for sanity checks that are fatal if invalid; not just for the local function / context, but fatal across the entire program, including every thread. I don't really think assert therefore should exist in an API file short of something like: assert(thread_shared_internals_are_unrecoverably_broken()).

[NikolajBjorner]

blocking me from integrating Z3 currently because they crash the program anytime a thread or user makes a mistake rather than leaving it in a recoverable state.

You have a real use case where assert crashes your program but want to recover?

My thought was that the code above Z3 should be fixed to not create mal-formed arguments to the functions that assert.

[zwimer]

I see. I was originally going to do that, but I'd be reimplementing externally all of the error checking logic that is already implemented internally; so instead I started to make a hard fork but stopped after I figured I should upstream things. I thought the error code thing wouldn't be an issue since it uses the existing machinery, it doesn't introduce anything 'new' other than a new exit code.

Also, regarding usage:
Not all of the assertion pre-conditions are documented, and some are consistently undocumented like assert(ctx().enable_exceptions());. The more I read the code the more I found things like this too:

// operator is not supported by given arguments.
assert(false);

Which just seemed perfect for error message propagation if any design could support it, which I figured it could since Z3_THROW(exception("xyz")); is used throughout the API.