Klever 1.1 includes quite many high demanded features and fixes of the most annoying bugs:
- Improving coverage calculation and visualization. Now one can easily navigate through covered and uncovered functions.
- Updating CPALockator used for finding data races.
- Proper processing of wall timeouts that is especially important for highly overloaded machines.
- Advanced verification tasks scheduling allows:
- Solving verification tasks faster by means of adaptation of computational resource limits.
- Solving more verification tasks when having free computational resources after ensuring a minimally required quality of service.
- Getting rid of some database caches helps to avoid unpleasant bugs in various statistics.
- Considerable fixing and improving local and OpenStack deployments.
- Numerous minor bug fixes, optimizations and improvements.
The new release contains the following changes:
- Templates: the
nitems generator was established
- Templates: blocks with no attributes are now allowed (
block {})
- Code generation facilities moved to the Castle library
- Bug fixes and code improvements
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
We are happy to announce the first release of the Castle library.
Castle (Control flow & Abstract Syntax Tree Library, Etc.) is a library for developing translators and code generators.
The release includes the following features:
- ANTLR-based utilities: include file search engine;
- ANTLR-based utilities: token source stack for hierarchical structures;
- AST: symbol table, walker, visitor;
- AST: assignment, ranged variable, use-def interface;
- StringTemplate-based code generation utilities;
- General Utils: system, file processing, logging.
The package can be downloaded from here
The new release contains the following changes:
- Enhancements in type calculation logic
- New method
DataType.isTypeId
- New methods
Data.getString and NodeValue.getString
- Methods
Data.newArray and NodeValue.newArray were renamed to newMap
- Other bug fixes and code improvements
The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files
MicroTESK for RISC-V 0.0.5 has been released:
- Specifications: Bug fixes
- Test Templates: Test templates for generating torture tests
- Test Templates: Test templates for validating floating-point instructions
- Tool Functions: Improved floating-point support
- Tool Functions: Improved register allocation mechanism
- Tool Functions: Support for operations with dynamic immediate values in test templates (
_AND, _OR, _XOR, _ADD, _SUB, _PLUS, _MINUS, _NOT, _SLL)
- Tests: Improved Make scripts for running test templates
- Tests: Specification code coverage is measured
- Tests: Test suite uses QEMU4V 0.2.2
MicroTESK for RISC-V can be downloaded from http://forge.ispras.ru/projects/microtesk-riscv/files
The new release contains the following changes:
- Improved template facilities: support for addressing modes (registers) in printing functions (such as
trace)
- Improved template facilities: support for the
_SLL operation with dynamic immediate values
- Improved register allocation: support for the
retain attribute
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The new release contains the following changes:
- Support for floating-point types in data sections
- Support for formatted printing of values in data sections
- Support for register reservation
- Support for basic operations (
_AND, _OR, _XOR, _ADD, _SUB, _PLUS, _MINUS, _NOT) with dynamic immediate values in test templates
- Improved register allocation strategies
- New permutator
exhaustive (aliased as full)
- Support for i386 in x86 specifications
- Support for the NASM and GNU assembler in x86 specifications and test templates
- miniMIPS test programs are compiled with the GNU assembler and simulated in QEMU
- x86 test programs are compiled with the GNU and NASM assemblers and simulated in QEMU
- New option
--model-name to allow building several ISA models from the same specifications
- New option
--base-template-path for automated template generation
- Bug fixes and code improvements
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The complete list of closed issues is available here
The source code can be downloaded from here
The new release is based on the 75507f1a commit of the QEMU project.
The complete list of closed issues is available here
The source code can be downloaded from here
Klever:
Klever 1.1
