-
Notifications
You must be signed in to change notification settings - Fork 263
Investigating slow verification performance
This is an advanced topic.
We can use the Axiom Profiler to debug Dafny performance issues.
Generate a Boogie (bpl) file using /print. We also generate a log XML file, which shows which verification tasks take a long time. The @FILE@ and @TIME@ placeholders are expanded by Boogie.
Dafny.exe file.dfy /print:file.bpl /xml:profile-@FILE@-@TIME@.xml
Handling timeouts: If Dafny takes too long and does not produce a helpful xml file you can kill the underlying SMT solver and Dafny will report back that verification was inconclusive followed by the name of the entity it could not prove.
If you want to just create a Boogie file without running verification and without producing other output you can run
Dafny.exe file.dfy /compile:0 /noVerify /print:file.bpl
We will now call z3 through Boogie to create the log that we then feed to the AxiomProfiler. Some flags are necessary to be passed to z3. More information at https://github.com/viperproject/axiom-profiler and https://github.com/microsoft/dafny/issues/229.
The parameter /proc limits Boogie to the slow (in verification time) method that we detected by inspecting the XML log. Using /proc is important for getting more valuable information from the AxiomProfiler.
It is important to use z3 version >= 4.8.5 for Axiom Profiler to work. At the time of writing this requires z3 to be built from source.
Boogie.exe /z3exe:'<path to z3>' /proc:'<name of slow Boogie task starting with 'Impl$$' or so>' /z3opt:TRACE=true /z3opt:PROOF=true /z3opt:trace-file-name=file.log /vcsCores:1 file.bpl
You may want to add the /timeLimit:<n> flag where n are seconds.
Run the AxiomProfiler on the log file we just obtained from z3.
AxiomProfiler /l:file.log
To understand the AxiomProfiler output we recommend reading the AxiomProfiler paper at:
And to read up on matching triggers, for example at: