Report quantifier instantiations

[fpoli]

This PR makes Silicon recognize and log Z3's quantifier instantiation reports instead of crashing.

When smt.qi.profile is true, Z3 periodically reports to stdout a summary of the instantiations of each quantifier. The report is printed at least each smt.qi.profile_freq=<n> instantiations and its format is described here. It's not as precise and detailed as the axiom profiler, but it's much quicker to obtain and easier to interpret.

How to report quantifier instantiations

Run Silicon with ./silicon.sh --numberOfParallelVerifiers 1 --z3Args '"smt.qi.profile=true smt.qi.profile_freq=10000"' prog.vpr. The output will look like the following:

Silicon 1.1-SNAPSHOT
[quantifier_instances]  prog.l603 :     12 :   3 : 3
[quantifier_instances]  prog.l587 :     39 :   2 : 3
[quantifier_instances]  prog.l586 :     60 :   3 : 3
[quantifier_instances]  prog.l565 :     29 :   2 : 3
[quantifier_instances]  prog.l564 :     76 :   2 : 3
[quantifier_instances]  prog.l545 :     30 :   2 : 3
[quantifier_instances]  prog.l544 :    101 :   2 : 3
[quantifier_instances] prog.l1027 :    519 :   3 : 4
[quantifier_instances] prog.l1026 :    819 :   9 : 10
[quantifier_instances]  prog.l997 :    940 :   3 : 4
[quantifier_instances]  prog.l996 :   1013 :   9 : 10
[quantifier_instances]      k!521 :     24 :   9 : 10
[quantifier_instances]  prog.l932 :   3446 :   3 : 4
[quantifier_instances]  prog.l931 :   2054 :   9 : 10
[quantifier_instances]  prog.l905 :   3724 :   3 : 4
[quantifier_instances]  prog.l904 :   2675 :   9 : 10
[quantifier_instances]  prog.l854 :   3522 :   3 : 4
[quantifier_instances]  prog.l853 :   3094 :   9 : 10
[quantifier_instances]  prog.l829 :   3094 :   9 : 10
[quantifier_instances]  prog.l824 :   1698 :   3 : 4
[quantifier_instances]  prog.l823 :   3638 :   9 : 10
[quantifier_instances]  prog.l804 :   1798 :   3 : 4
[quantifier_instances]  prog.l803 :   4315 :   9 : 10
[quantifier_instances]  prog.l776 :   3106 :   3 : 4
[quantifier_instances]  prog.l775 :   5311 :   9 : 10
[quantifier_instances]  prog.l737 :   3154 :   3 : 4
[quantifier_instances]  prog.l736 :   5906 :   9 : 10
[quantifier_instances]  prog.l717 :   2056 :   3 : 4
[quantifier_instances]  prog.l716 :   4960 :   9 : 10
[quantifier_instances]  prog.l679 :    771 :   3 : 4
[quantifier_instances]  prog.l678 :   4108 :   9 : 10
Silicon found 1 error in 8.91s:
  [0] Assert might fail. Assertion (...) might not hold. (prog.vpr@1047.11--1047.12)

From the reported quantifier instantiations we can see that the quantifier at line 736 has been instantiated 5906 times, reaching the maximum instantiation depth 9 and cost 10. So, it's a pretty good suspect when looking for matching loops.

Indeed, the quantifier on line 736 had a clear matching loop. After fixing it:

Silicon 1.1-SNAPSHOT
[quantifier_instances]  prog.l594 :      1 :   1 : 2
[quantifier_instances]  prog.l577 :      4 :   2 : 3
[quantifier_instances]  prog.l576 :      8 :   1 : 2
[quantifier_instances]  prog.l555 :      4 :   2 : 3
[quantifier_instances]  prog.l554 :      3 :   1 : 2
[quantifier_instances]  prog.l535 :      3 :   1 : 2
[quantifier_instances]  prog.l534 :      3 :   1 : 2
[quantifier_instances]  prog.l923 :      2 :   1 : 1
[quantifier_instances]  prog.l896 :      2 :   1 : 1
[quantifier_instances]  prog.l895 :     31 :   2 : 3
[quantifier_instances]  prog.l845 :      1 :   1 : 1
[quantifier_instances]  prog.l844 :     32 :   8 : 9
[quantifier_instances]  prog.l820 :     53 :   8 : 9
[quantifier_instances]  prog.l815 :      1 :   1 : 1
[quantifier_instances]  prog.l814 :     57 :   8 : 9
[quantifier_instances]  prog.l795 :      1 :   1 : 2
[quantifier_instances]  prog.l794 :     84 :   7 : 8
[quantifier_instances]  prog.l766 :     94 :   6 : 7
[quantifier_instances]  prog.l727 :    110 :   5 : 6
[quantifier_instances]  prog.l707 :    117 :   4 : 5
[quantifier_instances]  prog.l670 :      2 :   1 : 2
[quantifier_instances]  prog.l669 :    131 :   3 : 4
Silicon found 1 error in 7.11s:
  [0] Assert might fail. Assertion getU32Snapshot_value(snapU32(data2)) >= 124 might not hold. (prog.vpr@929.11--929.12)

Additionally, running Silicon multiple times with --z3RandomizeSeeds gives an idea of how stable the quantifier instantiations are.

[Aurel300]

A longer-term goal perhaps, but it would be great if we could show this visually in the IDE, e.g. by colouring heavily instantiated quantifiers more red?

[mschwerhoff]

Looks good, thank you

[fpoli]

@bobismijnnaam this is the feature. We could try it on your programs during the hackathon, if you wish.

[bobismijnnaam]

Is the "--numberOfParallelVerifiers 1" option mandatory? I tried it without this flag and the output seemed sensible. The number don't have to be exact, as long as they're proportional.

[fpoli]

Without --numberOfParallelVerifiers 1 I think that the output would be the interleaving of the output of multiple Z3 processes. So, big numbers would still signal a potential issue and low numbers would still mean that everything looks good.