Linux Driver Verification » BLAST

You may download sources and binaries on the Files page of the project. See also the original project page.

Release notes¶

Analysis speedup¶

• Speedup ranges from 8 times on small-sized programs to 30 times on medium-sized programs
• Logarithmic algorithm for useful-blocks (significantly speedup of trace analysis)
• Improved integration with SMT solvers
  • efficient string concatenation
  • caching of converted formulae
  • optimization of CVC3 options for BLAST use cases
• Formulae normalization has been moved to solvers since solvers do it faster (option -skipnorm)
• Alias analysis speedup
  • must-aliases are handled separately and faster than may-aliases (option -nomusts)
  • removed unnecessary debug prints from alias iteration (even a check for debug flag impacts performance significantly in hot places)
• BLAST-specific tuning of OCaml virtual machine options (script "ocamltune")

Important bug fixes¶

• Fixed unsound analysis when lattices are used (options -stop-sep and -merge) (Time of analysis has been increased by a factor of 1.5, but the inherent imprecision in lattices no longer makes BLAST miss bugs). See bug #330
• bool-to-int casting in function calls fixed. See bug #334

Frontend¶

• C frontend (CIL) uplift, fixes and workarounds (see -ignoredupfn and -nosserr options)
• Some errors have been made warnings

New features¶

• constrain stack depth to be analyzed; see options -fdepth, -important-attrs, and -inline-attrs
• treat constant pointers as must aliases (see option -const)

Infrastructure improvements¶

• Regression test suite improved
• Got rid of non-free software (Simplify solver was replaced by CVC3, ditched unused Vampyre, FOCI, and CLPprover)