Project

General

Profile

News

MicroTESK 2.6.0 released

Added by Alexander Protsenko over 1 year 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 almost 5 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 almost 5 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 6 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 6 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

(1-10/135)

Also available in: Atom