isolate and report z3 segfault from Trezor drawing code

[invd]

This issue has come up during #321 and has been discussed there, but should be continued in an independent issue.

Problem: Ultimate triggers a segfault in z3 when run against partialmain_bmp_logo64_evil_Elim1Store.c with Bitvector precision. More details on the specific parameters can be found in issue #321.

The segfault was observed over the course of several months of Ultimate development and happens on the self-compiled z3 4.7.0 as well as the official z3 4.7.1 binaries (latest release, tested by swapping the executable).

As described in #321, the segfault is reliably reproducible with regards to the Ultimate runs. We have, however, so far not been able to isolate the .smt2 script input that triggers this segfault, despite time-consuming efforts to do so. Manual z3 runs over logged z3 smt2 script input do not appear to produce faulty output or crashes.

The crash has been confirmed with he newest 3cea2480e0162cca93f99c9f013b388aca0ca196 Ultimate version which includes Z3 version 4.7.0 - 64 bit:

z3[15276]: segfault at 0 ip 0000000000cf90f2 sp 00007ffe8537c9c0 error 4 in z3[400000+15c5000]

Due to lack of the specific crashing input and reproducibility on the z3 level, this segfault has not yet been reported to the z3 developers upstream, which is of course the goal here.

[invd]

I have done further debugging on the base of Ultimate 55903dff755ffb961c3d1e03797f004bb5b4d658. With the regular z3 4.7.0 version shipped at the moment and this Ultimate configuration, z3 is confirmed to crash with a segfault. (Earlier tests suggest that the official 4.7.1 version crashes as well, but this has not been tested on this configuration so far).

I have compiled Debug, Release and RelWithDebugInfo variants of z3 versions based on the recent z3 master branch from this week (e8a78ec6964cc8cb8476ef95f8bb23258f8773e5 to be exact) and tested them by swapping the z3 binary in the Ultimate folder. None of the three binaries produce a segfault. This does not necessarily mean that the underlying issue in z3 has been fixed already since the 4.7.1 release in late May, although it is a likely explanation.

Since testing each binary requires an Ultimate run that takes several hours, progress is slow.

[invd]

As expected, the self-compiled 4.7.1 z3 binary with debug infos (RelWithDebugInfo) behaves similar to the publicly available 4.7.1 release version with regards to performance and segfaults within 90 minutes of Ultimate runtime:

segfault at 0 ip 000055e25fe2d282 sp 00007ffcb23b3670 error 4 in z3_v4-7-1_relwithdebuginfo[55e25f5c8000+1323000]

[invd]

The newest Ultimate af96161e55b318c2d5f32d5c86caa05c47962602 still ships the z3 4.7.0 with identical hashsums to previously tested versions.

As expected from previous debugging, the z3 4.7.0 still segfaults:

[Mon Oct 29 13:57:24 2018] z3[4822]: segfault at 0 ip 0000000000cf8473 sp 00007fff09a702b0 error 4 in z3[400000+15c5000]

Unfortunately, there is no official z3 post-4.7.1 release before the 4.8.1 which apparently includes major API changes (I'm guessing that Ultimate does not support them yet), so this issue will likely stay unresolved for a while.

[danieldietsch]

Good point. I will upgrade to the newest z3 and we will see what breaks. @Heizmann This might also interest you.

For reference, here are the release notes:

Version 4.8.0
=============

- New requirements:
  - A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of 
    formulas as opposed to a conjunction of formulas. The vector of formulas correspond to 
    the set of "assert" instructions in the SMT-LIB input.

- New features
   - A parallel mode is available for select theories, including QF_BV. 
     By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the 
     number of available CPU cores to apply cube and conquer solving on the goal.
   - The SAT solver by default handle cardinality and PB constraints using a custom plugin 
     that operates directly on cardinality and PB constraints.
   - A "cube" interface is exposed over the solver API. 
   - Model conversion is first class over the textual API, such that subgoals created from running a 
     solver can be passed in text files and a model for the original formula can be recreated from the result.
   - This has also led to changes in how models are tracked over tactic subgoals. The API for 
     extracting models from apply_result have been replaced.
   - An optional mode handles xor constraints using a custom xor propagator. 
     It is off by default and its value not demonstrated.
   - The SAT solver includes new inprocessing techniques that are available during simplification.
     It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques 
     (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs.
     Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged
     as lemmas (redundant) and are garbage collected if their glue level is high.
   - Substantial overhaul of the spacer horn clause engine.
   - Added basic features to support Lambda bindings.
   - Added model compression to eliminate local function definitions in models when
     inlining them does not incur substantial overhead. The old behavior, where models are left
     uncompressed can be replayed by setting the top-level parameter model_compress=false.
   - Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson.
     It incorporates several improvements to QF_LIA solving based on
     . using a better LP engine, which is already the foundation for QF_LRA
     . including cuts based on Hermite Normal Form (thanks to approaches described 
       in "cuts from proofs" and "cutting the mix").
     . extracting integer solutions from LP solutions by tightening bounds selectively.
       We use a generalization of Bromberger and Weidenbach that allows avoiding selected
       bounds tighthenings (https://easychair.org/publications/paper/qGfG).
     It solves significantly more problems in the QF_LIA category and may at this point also 
     be the best solver for your problem as well.
     The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA.
     Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting
     the parameter smt.arith.solver=6 to give it a spin.

- Removed features:
  - interpolation API
  - duality engine for constrained Horn clauses.
  - pdr engine for constrained Horn clauses. The engine's functionality has been 
    folded into spacer as one of optional strategies.
  - long deprecated API functions have been removed from z3_api.h

[Heizmann]

@danieldietsch Thanks. Do you have something particular in mind that is interesting for me?

[danieldietsch]

No, only in case something breaks -- so that you know it might be the new z3 version. I am not sure about their API breaking change. I just realized that our nightly build does not use the external tools from our adds directory, but the ones installed on the system.

I will fix that and then restart the nightly build.

[danieldietsch]

Our nightly build now uses the correct solver versions. I observed no breakage, so the new version of z3 should be good. @invd do you want to recheck?

[invd]

@danieldietsch: new test is running now.

For the record, Ultimate now ships

./z3 --version
Z3 version 4.8.2 - 64 bit

sha256sum z3
ed34df586e467d3aa928a2b977f7d2e0cd35decbeea1daecc6aeebb1267c2b0f  z3

[invd]

After roughly 5 hours of runtime, Ultimate aborts since z3 appears to run out of memory, but no segfault behavior is visible:

[2018-10-31 17:46:19,590 INFO  L336   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * CDTParser took 0.12 ms. Allocated memory is still 514.9 MB. Free memory is still 477.4 MB. There was no memory consumed. Max. memory is 11.5 GB.
 * CACSL2BoogieTranslator took 365.97 ms. Allocated memory is still 514.9 MB. Free memory was 454.8 MB in the beginning and 420.9 MB in the end (delta: 33.8 MB). Peak memory consumption was 33.8 MB. Max. memory is 11.5 GB.
 * Boogie Preprocessor took 197.59 ms. Allocated memory was 514.9 MB in the beginning and 608.7 MB in the end (delta: 93.8 MB). Free memory was 420.9 MB in the beginning and 580.0 MB in the end (delta: -159.0 MB). Peak memory consumption was 30.2 MB. Max. memory is 11.5 GB.
 * RCFGBuilder took 3616.69 ms. Allocated memory was 608.7 MB in the beginning and 633.3 MB in the end (delta: 24.6 MB). Free memory was 580.0 MB in the beginning and 543.4 MB in the end (delta: 36.6 MB). Peakmemory consumption was 169.8 MB. Max. memory is 11.5 GB.
 * TraceAbstraction took 18857448.58 ms. Allocated memory was 633.3 MB in the beginning and 1.3 GB in the end (delta: 674.8 MB). Free memory was 543.4 MB in the beginning and 1.0 GB in the end (delta: -460.2 MB). Peak memory consumption was 875.5 MB. Max. memory is 11.5 GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - ExceptionOrErrorResult: SMTLIBException: External (z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000)Received EOF on stdin. stderr output: (error "out of memory")

    de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction: SMTLIBException: External (z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000)Received EOF on stdin. stderr output: (error "outof memory")
: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.parse(Executor.java:208)
RESULT: Ultimate could not prove your program: Toolchain returned no result.

According to my interpretation, the previous segfault error is not longer present in z3 4.8.2 which solves this issue in my opinion. However, there is now another problems that previously was not reachable, namely z3 exiting after exhausting its 2GB ? of working memory. A related, more generic question is: can Ultimate manage/mitigate such subprocess-exits better to prevent such an unclean abort of the overall Ultimate verification task?

The target VM has about 17.5 GByte of free RAM, which should be well within reasonable requirements for Ultimate (11.5GB Ultimate "max memory" + 2GB for z3 also fits in well).

[invd]

For reference: I've restarted the relevant run with Automizer_Default.epf settings instead of the Automizer_Bitvector.epf settings that caused the segfault in previous configurations.

After 10-12 hours, this run is still ongoing, with Ultimate at about 3.7GB main memory and two z3 processes, one of which consumes about 4.9GB and is now at 100% cpu time for at least 8 hours:

mastera+  3274  0.2  0.1  55012 39200 pts/17   S+   Oct31   2:08 /shortened/z3 SMTLIB2_COMPLIANT true -memory 2024 -smt2 -in -t 2000
mastera+ 12518 99.9 24.2 5114576 4875708 pts/17 R+  03:10 512:48 /shortened/z3 -smt2 -in SMTLIB2_COMPLIANT true

Is it expected that the "unbounded" (no -t -memory settings) z3 process behaves like this? Would it make sense to add at least some -memory limits to make the failure mode more graceful?

[invd]

Also, somewhat unrelated (should I open a new issue?): the z3 changelog mentions parallelization ( parallel.enable=true) and improved processing techniques (sat.acce=true) that have to be enabled with explicit flags, but there are limitations to where they can be used. Are they relevant for the tasks that z3 is doing here? Spreading the z3 runtime over several cores might result in drastic reduction in runtime for more complex problems.

[invd]

After over 36 hours of runtime, and a singular z3 process that has run over a day, I have aborted the Automizer_Default.epf run.

For reference, those were the last log outputs:

[2018-11-01 03:10:24,873 INFO  L141       PredicateUnifier]: Initialized classic predicate unifier
[2018-11-01 03:10:24,873 INFO  L82        PathProgramCache]: Analyzing trace with hash 1389623306, now seen corresponding path program 2 times
[2018-11-01 03:10:24,873 INFO  L225   ckRefinementStrategy]: Switched to mode SMTINTERPOL_TREE_INTERPOLANTS
[2018-11-01 03:10:24,873 INFO  L69    tionRefinementEngine]: Using refinement strategy CamelRefinementStrategy
[2018-11-01 03:10:24,873 INFO  L119   rtionOrderModulation]: Craig_TreeInterpolation forces the order to NOT_INCREMENTALLY
[2018-11-01 03:10:24,873 INFO  L103   rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2018-11-01 03:10:24,873 INFO  L119   rtionOrderModulation]: Craig_TreeInterpolation forces the order to NOT_INCREMENTALLY
[2018-11-01 03:10:25,007 ERROR L235   seRefinementStrategy]: Caught known exception: Unsupported non-linear arithmetic
[2018-11-01 03:10:25,007 INFO  L258   seRefinementStrategy]: Advancing trace checker
[2018-11-01 03:10:25,007 INFO  L225   ckRefinementStrategy]: Switched to mode Z3_FP
No working directory specified, using /home/masterarbeit/ultimate/releaseScripts/default/UAutomizer-linux/z3
Starting monitored process 19 with z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
Waiting until toolchain timeout for monitored process 19 with z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2018-11-01 03:10:25,015 INFO  L103   rtionOrderModulation]: Keeping assertion order OUTSIDE_LOOP_FIRST1

Ultimate does not appear to be ready to check partialmain_bmp_logo64_evil_Elim1Store.c within reasonable time or memory requirements.

[danieldietsch]

Can you rerun this with CAMEL_NO_AM ? It seems that the assertion order modulation for this trace is the culprit.

[invd]

Plot twist: with these new settings, z3 v.4.8.2 segfaults again!

[Sat Nov  3 04:13:46 2018] z3[23981]: segfault at 402fcb9ff ip 0000000000bdc983 sp 00007ffe9332fde0 error 4 in z3[400000+15aa000]

Ultimate configuration: ./Ultimate -tc ~/ultimate/releaseScripts/default/UAutomizer-linux/config/AutomizerMemDerefMemtrack.xml -s ~/ultimate/trunk/examples/settings/default/automizer/svcomp-DerefFreeMemtrack-32bit-Automizer_Default.epf -i ~/shortened/partialmain_bmp_logo64_evil_Elim1Store.c --traceabstraction.trace.refinement.strategy CAMEL_NO_AM

At this point, I think we have to involve the z3 devs and see if they want to help with this one. I've simply spent too many hours chasing this bug without really getting anywhere.

[danieldietsch]

Do you have the last lines of the log before the crash happens?

We could still try and produce a SMT script that reproduces the crash in z3 alone.

[danieldietsch]

I will try and dump the script; I am unsure if the file code/regression/partialmain_bmp_logo64_evil_Elim1Store.c from your repository is the correct one. Can you confirm?

[invd]

@danieldietsch it is, but the program has been uploaded to this repository as well: partialmain_bmp_logo64_evil_Elim1Store.c

Log:

[2018-11-03 01:21:37,524 INFO  L424      AbstractCegarLoop]: === Iteration 24 === [oledDrawBitmapErr4REQUIRES_VIOLATION, oledDrawBitmapErr3REQUIRES_VIOLATION, oledDrawBitmapErr2REQUIRES_VIOLATION, oledDrawBitmap
Err7REQUIRES_VIOLATION, oledDrawBitmapErr8REQUIRES_VIOLATION, oledDrawBitmapErr1REQUIRES_VIOLATION, oledDrawBitmapErr6REQUIRES_VIOLATION, oledDrawBitmapErr9REQUIRES_VIOLATION, oledDrawBitmapErr0REQUIRES_VIOLATIO
N, oledDrawBitmapErr5REQUIRES_VIOLATION, ULTIMATE.initErr0REQUIRES_VIOLATION, ULTIMATE.initErr1REQUIRES_VIOLATION, oledDrawPixelErr1REQUIRES_VIOLATION, oledDrawPixelErr2REQUIRES_VIOLATION, oledDrawPixelErr0REQUI
RES_VIOLATION, oledDrawPixelErr3REQUIRES_VIOLATION, mainErr0ENSURES_VIOLATIONMEMORY_LEAK, oledClearPixelErr3REQUIRES_VIOLATION, oledClearPixelErr0REQUIRES_VIOLATION, oledClearPixelErr1REQUIRES_VIOLATION, oledCle
arPixelErr2REQUIRES_VIOLATION]===  
[2018-11-03 01:21:37,524 INFO  L141       PredicateUnifier]: Initialized classic predicate unifier                                                                                                                 
[2018-11-03 01:21:37,524 INFO  L82        PathProgramCache]: Analyzing trace with hash 14908967, now seen corresponding path program 1 times                                                                       
[2018-11-03 01:21:37,524 INFO  L225   ckRefinementStrategy]: Switched to mode SMTINTERPOL_TREE_INTERPOLANTS                                                                                                        
[2018-11-03 01:21:37,524 INFO  L69    tionRefinementEngine]: Using refinement strategy CamelRefinementStrategy                                                                                                     
[2018-11-03 01:21:37,525 INFO  L119   rtionOrderModulation]: Craig_TreeInterpolation forces the order to NOT_INCREMENTALLY                                                                                         
[2018-11-03 01:21:37,525 INFO  L103   rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY                                                                                                             
[2018-11-03 01:21:37,525 INFO  L119   rtionOrderModulation]: Craig_TreeInterpolation forces the order to NOT_INCREMENTALLY                                                                                         
[2018-11-03 01:21:37,651 ERROR L235   seRefinementStrategy]: Caught known exception: Unsupported non-linear arithmetic                                                                                             
[2018-11-03 01:21:37,651 INFO  L258   seRefinementStrategy]: Advancing trace checker                                                                                                                               
[2018-11-03 01:21:37,651 INFO  L225   ckRefinementStrategy]: Switched to mode Z3_FP                                                                                                                                
No working directory specified, using /home/masterarbeit/ultimate/releaseScripts/default/UAutomizer-linux/z3                                                                                                       
Starting monitored process 20 with z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)                                                                                                
Waiting until toolchain timeout for monitored process 20 with z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2018-11-03 01:21:37,657 INFO  L103   rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2018-11-03 04:09:37,661 INFO  L136    AnnotateAndAsserter]: Conjunction of SSA is unsat
[...]
[2018-11-03 04:11:03,413 INFO  L267         ElimStorePlain]: Start of recursive call 3:  End of recursive call:  and 1 xjuncts.
[2018-11-03 04:11:03,415 INFO  L267         ElimStorePlain]: Start of recursive call 2: 1 dim-1 vars,  End of recursive call:  and 1 xjuncts.
[2018-11-03 04:11:03,426 INFO  L267         ElimStorePlain]: Start of recursive call 1: 4 dim-0 vars, 1 dim-2 vars,  End of recursive call: 4 dim-0 vars,  and 1 xjuncts.
[2018-11-03 04:11:03,426 INFO  L202         ElimStorePlain]: Needed 3 recursive calls to eliminate 5 variables, input treesize:70, output treesize:52
[2018-11-03 04:11:05,539 INFO  L134       CoverageAnalysis]: Checked inductivity of 20 backedges. 0 proven. 20 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[MP z3 -smt2 -in SMTLIB2_COMPLIANT=true (20)] Forcibly destroying the process                                           
[2018-11-03 04:11:05,740 INFO  L312   seRefinementStrategy]: Constructing automaton from 0 perfect and 1 imperfect interpolant sequences.
[2018-11-03 04:11:05,740 INFO  L327   seRefinementStrategy]: Number of different interpolants: perfect sequences [] imperfect sequences [23] total 23
[2018-11-03 04:11:05,741 INFO  L460      AbstractCegarLoop]: Interpolant automaton has 24 states                              
[2018-11-03 04:11:05,741 INFO  L142   InterpolantAutomaton]: Constructing interpolant automaton starting with 24 interpolants.
[2018-11-03 04:11:05,741 INFO  L144   InterpolantAutomaton]: CoverageRelationStatistics Valid=56, Invalid=489, Unknown=7, NotChecked=0, Total=552
[2018-11-03 04:11:05,741 INFO  L87              Difference]: Start difference. First operand 1250 states and 1295 transitions. Second operand 24 states.
[2018-11-03 04:11:25,250 WARN  L179               SmtUtils]: Spent 101.00 ms on a formula simplification. DAG size of input: 105 DAG size of output: 93
[2018-11-03 04:11:25,444 WARN  L179               SmtUtils]: Spent 108.00 ms on a formula simplification. DAG size of input: 107 DAG size of output: 95
[2018-11-03 04:13:29,177 WARN  L179               SmtUtils]: Spent 40.43 s on a formula simplification. DAG size of input: 120 DAG size of output: 108
[2018-11-03 04:13:42,542 INFO  L142   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 22 states.
[2018-11-03 04:13:42,543 FATAL L265        ToolchainWalker]: An unrecoverable error occured during an interaction with an SMT solver:                                                                              de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: External (z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000)Received EOF on stdin. No stderr output.

Crash info:

 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - ExceptionOrErrorResult: SMTLIBException: External (z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000)Received EOF on stdin. No stderr output.
    de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction: SMTLIBException: External (z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000)Received EOF on stdin. No stderr output.: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.parse(Executor.java:208)

[danieldietsch]

1794bfb9236da73b004fc73ac5fff1ddba660d04 and 9cc8901501f8e89fd3ca37140648fd09da64176d update z3 to the newest head where this segfault is fixed.

[invd]

I'll run some additional tests before closing this issue.

[invd]

TheAutomizer_Default.epf / CAMEL_NO_AM run from yesterday is still in progress, so this is still slower than previous mid-2018 Ultimate versions, but it is now at iteration 37 and has likely passed the point of the previous crash.

[invd]

After roughly 48 hours of runtime, I'm stopping this process at Iteration 48, which has been going on for about 14 hours at 100% cpu load (1 core) for z3, which is started without time/memory limits.

No segfault was visible so far, so I'm closing this issue.