Open-Source Projects

The new release contains the following changes:

• Oracle tool:
  - Added option to use masks when comparing registers
  - Updated diagnostic messages

Download: http://forge.ispras.ru/projects/microtesk/files

This release publishes improvements that were made mostly before January 2022.

Since this time the development was actually stopped.

The new release includes the following changes:

• CFG-GADD-Transformer: '--no-phase' option to produce phase-free GADD;
• CFG-Model: general support of SVA properties;
• Distribution: self-made RTL models and demo scripts are added;
• Documentation: ChangeLog and README files are rewritten into `Markdown` format;
• EFSM-GraphML-Printer: `--detailed` option for EFSM detailed/limited printing;
• Tool: `--check` option to check if tool dependencies were installed properly;
• Tool: migration to JDK 11;
• Tool: `--version` option;
• VCD-Printer: a new engine to print test sequences into VCD format;
• Verilog-Parser: `--library-file` option for path to system tasks/functions file.

The complete list of resolved issues is available here

The binary distribution of the tool can be downloaded from here

The new release contains the following changes:

• Added the tool for list the model operations.
  To use enter the command: `--list-operations <model name>`
• Oracle tool:
  - Refactoring the tool settings and options
• Trace adapter tool:
  - Refactoring the tool structure

Download: http://forge.ispras.ru/projects/microtesk/files

The release contains the following changes:

• Specifications:
  - Added data processing (immediate) instructions: 38
  - Added data processing (register) instructions: 70
  - Added branches, exception generating, and system instructions: 47
  - Added loads and stores instructions: 34
• Test Templates:
  - Added new base template
  - Added new test template for bubble sort algorithm
  - Added new test template 'blocks.rb'
  - Added new test template 'branch_generation.rb'
  - Added new test template 'combinatorial_generation.rb'
  - Added new test template 'dependencies.rb'
  - Added new test template 'int_exception.rb'
  - Added new test template 'random_sequence.rb'

Download: https://forge.ispras.ru/projects/microtesk-arm-demo/files

The new release contains the following changes:

• nML:
  - Language extension: recursive functions
• MIR:
  - Extended the intrinsic instruction set
  - Experimental support for path constraint generation for MIR programs
• Symbolic executor:
  - Support generating SMT-LIB constraints in functional style
  - Experimental support for extraction of the CFG of a binary program
• Experimental `all_paths` generator
• Disassembler:
  - Fixed issues with decoding of mixed-size instruction streams
  - Performance improvements due to removal of excessive memory allocation in decoders
• Added the trace adapter tool for collecting execution trace
  (see https://forge.ispras.ru/projects/microtesk/wiki/Trace_adapter)
• Added the oracle tool for checking test execution traces
  (see https://forge.ispras.ru/projects/microtesk/wiki/Oracle)
• Used the QEMU4V 0.3.6 simulator for running tests
  (see https://forge.ispras.ru/projects/qemu4v)
• Bug fixes and code improvements

Download: http://forge.ispras.ru/projects/microtesk/files

• The data model:
  - Support for arbitrary function definition and application, including recursive functions
  - Support for datatypes
• SMT-LIB interoperation layer:
  - Support for assertion levels
  - Support for multiple constraints in a single solver invocation
• Fixed several issues leading to runtime exceptions

The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files

Klever 3.7 was primarily devoted to improving a quality of verification results for Linux kernel drivers. After all about 43% of original false alarms issued when checking memory safety have gone.

Following fixes and improvements in Klever 3.7 deserve an attention:

• Adding new environment models for the Linux kernel:
  • Modeling the list API.
  • Modeling the kref API.
  • Adding model for the input_ff_create_memless() function.
  • Adding models for check_add_overflow(), check_sub_overflow() and check_mul_overflow() macros that fixes the struct_size() model for new versions of the Linux kernel.
  • Modeling v4l2_device(un)register()_ functions.
  • Modeling the i2c_match_id() function.
  • Adding model for the dev_err_probe() function.
  • Adding models for the dynamic debug printing API.
• Fixing existing environment models for the Linux kernel:
  • Modeling failures for calloc() and zalloc().
  • Fixing the off-by-one error when choosing a device from MODULE_DEVICE_TABLE.
  • Passing the same resource to probe and remove for HID drivers.
  • Allocating memory for inode for file_operations callbacks.
  • Allocating memory for tty_struct for tty_operations callbacks.
  • Avoiding using implicit resources in environment model specifications.
• Adding a new section to the user documentation: Verifying New Program.
• Fixing tests for environment model specifications and Environment Model Generator.
• Updating CIF which main file was rewritten in C++ and that started to print keyword static for local variables.
• Updating CPAchecker that supports packed/aligned attributes and issues violation witnesses more efficiently.
• Updating Python dependencies.

We would like to thank very much everybody who made this great job possible!

The major enhancement for CIF 1.2 is that the main CIF source file was rewritten in C++. The new version is more abstract and it is easier to maintain and develop it further. Using C++ allows to avoid a lot of potential memory errors that we encountered and fixed earlier. Besides, the execution time was reduced by using another way of launching subprocesses. The latter made redundant escaping double quotes in command-line options passed to CIF.

We would like to thank Ilya Shchepetkov for this awesome job!

CIF 1.1 was released!

There are following important changes and fixes:

• Supporting additional special directive for source code queries:
  • $storage_class that allows to get storage classes for functions and variables.
  • $var_init_list_json that allows to print global variable initializers in JSON.
• Fixing Aspectator to keep storage classes for variables.
• Improving and fixing Aspectator’s C back-end:
  • Fixing initialization of anonymous unions.
  • Fixing conversion for strings containing hexadecimal escape sequences.
  • Increasing recursion limit from 10 to 100 to handle deeply nested expressions.
• Simplifying the main CIF source file and avoiding errors of its compilation with GCC 12.
• Adding new test cases and making the test framework more robust.

This release was done at the beginning of June.

Klever 3.6 was released pretty soon after Klever 3.5 since we updated Clade and CIF in the backward incompatible manner. This means that the new version of Klever requires all build bases to be regenerated with the new version of Clade and CIF installed together with Klever. You can download build bases for Linux 5.5.19, 5.10.120 and 5.17.13 as well as sample build bases prepared ahead of time. Corresponding files are available either directly from the "Files" tab or from the Klever tutorial.

Other changes in Klever 3.6 are new models for struct_size() and underlying __ab_c_size() for the Linux kernel.