Project

General

Profile

News

MicroTESK 2.6.0 released

Added by Alexander Protsenko 8 days ago

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

MicroTESK 2.5.1 released

Added by Alexander Kamkin about 3 years ago

What's new?

  • Fixed the TokenSourceStack class and moved it to the Castle 0.1.4 library (see https://forge.ispras.ru/projects/castle)
  • Rearranged the documentation
  • Modified the mmuSL code generation scheme
  • Added a boot section to the miniMIPS test templates
  • Fixed a number of long-lived bugs
  • Used the QEMU4V 0.3.5 simulator for running tests

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

MicroTESK 2.5.0 released

Added by Alexander Kamkin about 3 years ago

What's new?

  • Introduced new internal representation, so-called MIR (Middle-level [or MicroTESK] IR)
    • Redesigned the constraint generator (for mark-based situations)
    • Redesigned the symbolic executor (for binary code analysis)
  • Unified the directives (alignment, data definition, and labels) for .text and .data sections:
    • Enabled a possibility to define data in .text
    • Implemented new directives: .balign, .p2align, and .option
    • Refactored the code/data allocation logic
  • Implemented a simple instruction-level coverage tracker (experimental)
  • Used the QEMU4V 0.3.4 simulator for running tests

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

MicroTESK 2.4.43 released

Added by Andrei Tatarnikov over 4 years ago

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

MicroTESK 2.4.42 released

Added by Andrei Tatarnikov over 4 years ago

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

MicroTESK 2.4.41 released

Added by Andrei Tatarnikov over 4 years ago

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

MicroTESK 2.4.40 released

Added by Andrei Tatarnikov almost 5 years ago

The new release contains the following changes:

  • Support for automated generation of test templates
  • Templates: methods rev_id and is_rev to get information on revisions supported by the model
  • Templates: support for global labels (the global_label method)
  • Templates: support for numeric labels
  • Templates: support for weak symbols (the weak method)
  • Templates: new method set_default_mode_allocator(allocator)
  • Templates: runtime methods to trace the state of registers and memory (instead of hand-written observers)
  • Number of bug fixes and code improvements

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

(1-10/133)

Also available in: Atom