Building Map2Check in our development environment

Using Docker

docker icon

Our Map2Check Docker is available by:

Dockerfile from Map2Check repository

Map2Check dockerfile to build the Map2Check tool image with our development environment is available at https://github.com/hbgit/Map2Check.git, you can build our docker image, as following:

$ git clone https://github.com/hbgit/Map2Check.git
$ cd Map2Check
$ git submodule update --init --recursive
$ docker build -t hrocha/mapdevel --no-cache -f Dockerfile .
$ docker run --rm -v $(pwd):/home/map2check/devel_tool/mygitclone:Z --user $(id -u):$(id -g) \
  hrocha/mapdevel /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-release.sh; \
  ./make-unit-test.sh"

  Building Map2Check release ... 

  -- Searching clang in /llvm/release/llvm600/bin
  -- Found /llvm/release/llvm600/bin/clang
  -- Searching clang++ in /llvm/release/llvm600/bin
  -- Found /llvm/release/llvm600/bin/clang++
  -- Searching llvm-config in /llvm/release/llvm600/bin
  -- Found /llvm/release/llvm600/bin/llvm-config
  clang version 6.0.0 (tags/RELEASE_600/final)
  Target: x86_64-unknown-linux-gnu
  Thread model: posix
  InstalledDir: /llvm/release/llvm600/bin
  
  -- Boost version: 1.58.0
  ... 
  -- Installing: /home/map2check/devel_tool/mygitclone/release/lib/TrackBBLog.bc
  -- Installing: /home/map2check/devel_tool/mygitclone/release/lib/WitnessGeneration.bc
  -- Installing: /home/map2check/devel_tool/mygitclone/release/lib/WitnessGenerationNone.bc
  -- Installing: /home/map2check/devel_tool/mygitclone/release/./map2check

  Copying external tools
  > Copying metaSMT deps ...
  > Crab-LLVM replacing PATH
  > Map2Check license
  > Extra tools licenses
  > Wrapper script
  > Module tool-info benchexec
  > README file

 Cleaning for SVCOMP

 DONE

 ... 

 Building Map2Check test ...
 ... 
 Test project /home/map2check/devel_tool/mygitclone/build
    Start 1: HelloGTest
  1/7 Test #1: HelloGTest .......................   Passed    0.00 sec
    Start 2: AllocationLogTest
  2/7 Test #2: AllocationLogTest ................   Passed    0.00 sec
    Start 3: HeapLogTest
  3/7 Test #3: HeapLogTest ......................   Passed    0.00 sec
    Start 4: ContainerReallocTest
  4/7 Test #4: ContainerReallocTest .............   Passed    0.01 sec
    Start 5: BTreeTest
  5/7 Test #5: BTreeTest ........................   Passed    0.14 sec
    Start 6: ContainerBTreeTest
  6/7 Test #6: ContainerBTreeTest ...............   Passed    0.16 sec
    Start 7: MemTrackTest
  7/7 Test #7: MemTrackTest .....................   Passed    0.00 sec

  100% tests passed, 0 tests failed out of 7

  Total Test time (real) =   0.32 sec

  

Docker Extra Information

Our docker user is "map2check" and the password is "map2check". Docker tips:

  • You can check that the container still exists by running: $ docker ps -a
  • You can restart the container by running: docker start -ai mapdevel
  • You can run any command in running container just knowing its ID (or name): docker exec echo "Hello from container!"

Running Regression Testing with Docker

In our regression testing, we have been adopted benchexec tools to execute our test cases from XML definition file . Map2Check provides a wrapper script make-regression-test.sh with the options:

t for travis    - small set of regression testing
m for map2check - set of regression testing
s for svcomp    - set of svcomp regression testing

Running our regression testing for Travis service:

$ ./make-regression-test.sh t
Adopting: map2check_regression_test_travis.xml
Found benchexec image to run tests ...
executing run set 'sv-comp19_map2check'     (35 files)
01:55:05   array-memsafety/add_last_unsafe.yml                 false(valid-deref)        0.90    0.77
01:55:06   array-memsafety/array01-alloca-2.yml                TIMEOUT                  10.88   11.02
... 
Statistics:             35 Files
  correct:              14
    correct true:        0
    correct false:      14
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:              21
  Score:                14 (max: 51)


real	2m42.873s
user	0m0.061s
sys	0m0.049s
Regression testing results is: 40 % of correct results from 35 test cases.