cplusplus no exception support

[humeafo]

in some projects like llvm, no exception is required, even if I just want to link dynamicly, so is it possible for z3 to support no exception enabled usage case?
of course I can use c interface, but it's a bit hard to use than c++ interface, so at least no throws in z3++.h?

[NikolajBjorner]

reasonable. Then user is required to check the error.

[NikolajBjorner]

Will this do?

[humeafo]

user responsible for checking error is not the problem. the above fix is not adequate because some projects (llvm) may reject throw clause, eg, in z3++.h like:

    int get_numeral_int() const {             
        int result = 0;
        if (!is_numeral_i(result) && ctx().enable_exceptions()) {
            throw exception("numeral does not fit in machine int");
        }
        return result;
    }

in order to pass compilation, I had to manually comment out the throw statements. maybe a macro should be used to replace a direct throw statements, so users can opt to make compiler comfortable?
I tested it using Apple LLVM version 8.0.0 (clang-800.0.42.1) in a llvm library.

[NikolajBjorner]

pull request?
I misunderstood the requirement.

[humeafo]

it's my fault, I just mean this:

int get_numeral_int() const {
int result = 0;
if (!is_numeral_i(result) && ctx().enable_exceptions()) {
throw exception("numeral does not fit in machine int");
}
return result;
}

maybe shoud be changed to:

int get_numeral_int() const {
int result = 0;
if (!is_numeral_i(result) && ctx().enable_exceptions()) {
#ifndef CXX_NOTHROWS
throw exception("numeral does not fit in machine int");
#endif
}
return result;
}

or:
#ifndef CXX_NOTHROWS
#define THROW_EXCEPTION(msg) throw exception("numeral does not fit in machine int");
#else
#define THROW_EXCEPTION(msg)
#endif

int get_numeral_int() const {
int result = 0;
if (!is_numeral_i(result) && ctx().enable_exceptions()) {
THROW_EXCEPTION("numeral does not fit in machine int");
}
return result;
}

and this should be applied to entire z3++.h.

[wintersteiger]

Could you give us an example of a program that LLVM rejects? I can't imagine that it has a mode that allows C++ classes but not exceptions.

[humeafo]

to wintersteiger :

please see llvm documents for why llvm not using exceptions:
http://llvm.org/docs/CodingStandards.html#do-not-use-rtti-or-exceptions

or this question:
http://stackoverflow.com/questions/4080601/not-using-c-exceptions-by-design-in-llvm-clang

you can also see llvm compilation scripts:
http://llvm.org/svn/llvm-project/llvm/trunk/cmake/modules/AddLLVM.cmake line 23:

list(APPEND LLVM_COMPILE_FLAGS "-fno-exceptions")

with -fno-exceptions on commandline:

c++ codes that use throw, try, catch won't compile under gcc clang

In my case, I'm developing a llvm subproject which should obey to the rules llvm defined. I just want to dynamicly link to z3 shared lib, so if the compilation can pass, and I don't use z3 exceptions, everything should be ok.

[humeafo]

the throw xxx statements in z3++.h hindered my llvm sub projects from compiling, ctx().enable_exceptions() support have solved part of the problem I encountered, some conditional macros to hide throw statements at compilation time should help to arrival the final.

[wintersteiger]

Aha! I thought it's a technical problem, but it's more philosophical. Can we make that dependent on the -fno-exceptions flag? E.g. does it define a macro we can use?

[delcypher]

@wintersteiger

Could you give us an example of a program that LLVM rejects? I can't imagine that it has a mode that allows C++ classes but not exceptions.

Just be clear as there is a danger of confusing LLVM's internal requirements with what Clang can compile

• LLVM's source code does not use exceptions for performance reasons and so is compiled by default with -fno-exceptions. When using LLVM's libraries via it's C++ interface it is important to match how LLVM was built (i.e. do not mix code built with and without exception support).
• The Clang compiler which is built on top of LLVM is also compiled without exceptions by default. However the built Clang can compile C++ code with or without exceptions (using the -fno-exceptions). flag. Said another way Clang's implementation doesn't use exceptions but Clang itself can compile C++ code with or without exception support.

[humeafo]

MSVC stl use _HAS_EXCEPTIONS macros to disable exceptions, but I'm not sure what other STL implementation used. I think a Z3 specific such as Z3_HAS_EXCEPTIONS is enough to let z3 users to infer this out.

I also noticed someone encountered this problem some time before as in this post:
http://stackoverflow.com/questions/29414355/z3-in-llvm-project-error-exception-handling-disabled-use-fexceptions-to-ena/29415497

[delcypher]

@wintersteiger

Can we make that dependent on the -fno-exceptions flag? E.g. does it define a macro we can use?

There is the __cpp_exceptions macro. E.g.

#if __cpp_exceptions
#error exceptions
#else
#error no_exceptions
#endif

Compiling with

• gcc -E -fno-exceptions test.cc
• gcc -E test.cc

Will give different outputs.

We need to be incredibly careful here though. Mixing code with exception handling and no exception handling is dangerous. If Z3's C++ interface is header only and it calls only into Z3's C interface then this is probably do-able because the C++ interface code would not be expecting to catch exceptions from Z3 internals.

If Z3's C++ interface works with internal Z3 exceptions or part of it's implementation is not in the header (i.e. part of its implementation is in libz3 which is built with exceptions) then we can't use macros to produce an exception handling/non-exception handling version of Z3's C++ interface.

[wintersteiger]

@humeafo: That stackoverflow post was about compiling Z3 itself with -fno-exceptions, which is something we won't support. Will there be any trouble with (dynamically) linking LLVM objects compiled with -fno-exceptions and Z3 objects compiled with exceptions?

[delcypher]

@wintersteiger

That stackoverflow post was about compiling Z3 itself with -fno-exceptions, which is something we won't support. Will there be any trouble with (dynamically) linking LLVM objects compiled with -fno-exceptions and Z3 objects compiled with exceptions?

AFAIK it is "okay" as long as no exceptions from Z3's code are ever propagated into code that is built without exception handling.

In KLEE we build without exceptions and we use LLVM (no exceptions) and Z3 (with exceptions) together. We use Z3 via it's C interface from which exceptions should never be thrown so I "think" we're okay.

[humeafo]

AFAIK it is "okay" as long as no exceptions from Z3's code are ever propagated into code that is built without exception handling.

@wintersteiger I agree with @delcypher on this, I'm not familiar with Z3's codebase, but if exceptions are all captured by the C++ api, everything should be ok.

[humeafo]

I looked into z3++.h if context::set_enable_exceptions(bool) can do what it claims, then we are sure that no exceptions are escaped from the libz3 code, only those in z3++.h have escaped exceptions, if exceptions are escaped from the libz3 code, context::set_enable_exceptions(bool) should be removed too.

[NikolajBjorner]

Exceptions should not escape. The C based API is set up to not produce exceptions unless there are some bugs.

[wintersteiger]

All our APIs are based on the C-API and internal exceptions should never cross that boundary, so I hope that would be OK then. This will still take some time though, as we'll have to check that the error flags are set correctly everywhere, etc.

[humeafo]

Yes, I noticed in current code when ctx().enable_exceptions() == false error code is not set correctly such as in get_numeral_int:

        if (!is_numeral_i(result) && ctx().enable_exceptions()) {
            throw exception("numeral does not fit in machine int");
        }

should be

        if (!is_numeral_i(result) ) {
            if(ctx().enable_exceptions())
                throw exception("numeral does not fit in machine int");
            else
                  set_error_code(xxx);
        }

[NikolajBjorner]

fair enough, but these functions should not be used in the non-exception mode unless the caller knows they can't fail. So I have updated the code to use assertions.

Other occurrences of check_error() should be OK, with the exception of methods that return std::string since failure in the methods that produce a string may end up with a NULL (0) string that, last time I checked, was unfriendly with the std::string constructor. For enabling this particular use of non-exceptions for C++, I would rather not change these places as a well-debugged application should never except those methods to fail.