[consolidated] issues in floating point

[rainoftime]

z3 4cfc737

(set-option :trace true)
(declare-fun fpv6 () Float32)
(assert (fp.leq fpv6 (_ +zero 8 24)))
(push)

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 414
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

(set-option :trace true)
(set-option :rewriter.flat false)
(declare-fun fpv14 () Float64)
(push)
(assert (fp.isZero (fp.max fpv14 ((_ to_fp 11 53) RNE 42739))))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

It's not really floating point specific, it is about trace.

It would be great if @alexanderjsummers took a serious look at cleaning up the trace code that was added some time ago with a lot of copy-pasting. At points I have consolidated some of the patterns into reusable auxiliary functions in smt_theory for ease of use, but invariably left out opportunities for streamlining. Unfortunately I was way too permissive in taking pull requests on these trace updates given the quality of the code.

theory_fpa has tracing code of the form:

        if (m.has_trace_stream()) log_axiom_instantiation(e);
        ctx.internalize(e, false);
        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";  

At this point, the reference count to expression 'e' is 0.
A reference count is acquired inside log_axiom_instantation and then released on return.
So when ctx.internalize(e, false) is called, e has been deleted.
The fix is to ensure that 'e' has a reference count and before log_axiom_instantiation is called.
This is a stringent contract and could easily be broken elsewhere.
I would say a root cause is brittle design of the logging facility. It requires too many conditions many places.
In places I have been fixing these brittleness issues by using stack scoped features to initialize a local object that holds reference counts during the life-time of the object.

(Note that in longer term I don't want to continue the trace feature in the new core and instead just use proof logging a single means for mining search behavior)

[NikolajBjorner]

the same fix applies to all examples above.

[NikolajBjorner]

[aytey]

Shouldn't there be fireworks out of "GitHub issue for same bug" (for the other fuzzing team) as well? 🙈

[alexanderjsummers]

Hi @NikolajBjorner,

I'm very sorry to read about the issues in the tracing code - I'm not sure I fully understand them yet, but would like to. I'll send you an email - hopefully we could set up a call about what would be most useful for maintaining this workflow in the future. I'm happy to contribute code personally if that would be useful!

I don't know much about the subsequent work in the diagram, but your support back when we were working on the Axiom Profiler was certainly critical to us in getting the necessary information reliably into the tool, and I really appreciate it. I know that a few people are using the Axiom Profiler with Z3 and have found it very helpful since, too.

Thanks, Alex

[NikolajBjorner]

The main issue is that the tracing code is brittle. Some blame can be cast on pre-existing z3 code, but I found it brittle to evolve when it requires two calls, as illustrated with the example above, for a single trace entity. There are ways in C++ to live with requirements of this form (not sure why it should have been a requirement in the first place to have these being/close entities given that enode creation just tells the tracer what node identifiers expand into). So I ended up introducing a scoped class to deal with many of the two-calls-to-tracing-sprinkled-across-many-lines occurrences. My shorthands are accumulated in smt_theory.h. Also, you decided to trace formulas, not in clausal form but at some higher level. For example, if z3 generates two clauses (a or !b), (b or !a), then you trace (a <=> b) in some cases. Maybe it looks better in your front end, but you put these transformations all the way into the leaves (the place where the clauses are produced). Again a brittle approach because you will just miss some other places where clauses encode more succinct formulas and then the trace functionality also ends up creating new expressions that are created only during trace mode. Creating new expressions influences search so z3 can behave differently with or without tracing. You don't want to push complexity down into the leaves. There has to be some software engineering curriculum that contains material along these lines.
A desired state would have characteristics, such as:

1. each trace entity uses a single call into a trace abstraction.
2. the trace abstraction hides the tests whether tracing is enabled.
3. tracing does not introduce new expressions.
4. tracing happens in fewer places (moving tracing from each theory to the single place that creates theory axioms?)
5. It is dumb and simple.