Actions
MicroVer¶
This tool is built on composition of MicroTESK tool and AstraVer versions of Frama-C and Why3 tools. The main purpose is deductive verification of the machine code by high-level language function contract specification.
Installation¶
This instruction uses RISC-V as example of target processor.
- First, install MicroTesk (version from branch mir) tool using instruction [[https://forge.ispras.ru/projects/microtesk/wiki/Installation_Guide]] . Pay attention for setting up $MICROTESK_HOME environment variable and installing cvc4 1.6 smt-solver;
- Download or clone RISC-V nml model from this repository [[https://forge.ispras.ru/projects/microtesk-riscv]]. Then compile and generate it using MicroTESK (see instruction above);
- Add cvc4 to your $PATH;
- Next, install AstraVer toolset using instruction [[https://forge.ispras.ru/projects/astraver/wiki]] . Following this instruction you will also install opam than would be used for installing other dependences;
- Install grep:
sudo apt-get install grep
- Install readelf:
sudo apt-get install binutils
- Install Yojson :
opam install Yojson
- Install ocaml-containers :
opam install containters
- Optional install gcc for riscv form this repository: https://github.com/riscv/riscv-gnu-toolchain;
- Next download source code of MicroVer modules:
git clone https://forge.ispras.ru/git/microver.git
- Use
make
for compiling source code; - Use
make install
for installing machine code specific Why3 modules, theories and drivers.
Running¶
- Use run.sh script for verification of the machine code.
Script usage is.\run.sh model_id file_name.elf file_name.c func_name
where:
model_id is riscv
file_name.elf - address of executable file that contains target machine code
file_name.c - C file that contains C code + ACSL specification of the verification object
func_name - name of the target function.
- Use run-reuse.sh script for reusing results of the previous run.
Script usage is.\run-reuse.sh model_id func_name
where:
model_id is riscv
func_name - name of the target function
Tests¶
Tests are placed into the "microver/tests" directory. File test.c contains some common functions, that can be used for running the system. File riscv.elf compiled from the test.c using gcc for RISC-V. For example you can run this:
for verification on abs function:./run.sh riscv tests/riscv.elf tests/test.c abs_1
for verification on function with loop:./run.sh riscv tests/riscv.elf tests/test.c x2
Results¶
- The run.sh script creates a build dirrectory called "build_<func_name>". This dirrectory contains:
- <func_name>.bin - function machine code
- <func_name>.s - disassembled function
- <func_name>.bin.json - function CFG
- <func_name>.bin.smt2 - old version of smt-lib machine code representation
- <func_name>.bin.bb_<x>.smt2 - smt-lib representation of function basic blocks
- _current_machine.json - information about target architecture
- Theory.mlw - WhyML representation of function specification
- WP_parameter_<func_name>.smt2 - smt-lib representation of function specification
- fun_info.json - information for merging representations
- session.json - information about stack and positions of the local variables in machine code.
- <func_name>_merged - targets for solving, verdicts and counterexamples if possible.
Updated by Pavel Putro over 1 year ago ยท 5 revisions