Ranger: A Tool for Bounds Analysis of Heap-Manipulating Programs

  1. About
  2. Download
  3. Compilation
  4. Usage
  5. Evaluation
  6. Contact

About

Ranger is an extension of the Forester tool to support a resource bounds analysis of heap-manipulating programs. Ranger takes as an input a program in C and transforms it to a corresponding arithmetic program. Such program is then analysed using an underlying bounds analyzer (in our case the Loopus tool) and compute the complexities of functions and loops.

Prerequisities

Following packages are needed in order to compile and run the Ranger toolchain on your system:

Download

In order to compile and work with our tool we highly recommend to clone the repository to the local repository. You need to have the git version control system installed.

To download the library, run

$ git clone https://pajda.fit.vutbr.cz/ifiedortom/forester-resource-bounds.git

Compilation

In order to prepare the tool for compilation issue the following command in the root directory of the tool, where $PATH_TO_GCC is a path to a gcc version 4.8:

$ ./switch-host-gcc.sh $PATH_TO_GCC

The compilation might end with an error (the actual failure is in different module, which is not used by Ranger), then run the following (to compile libfa.so and ranger):

$ make -C ./fa_build/

To run the Ranger run the following command, which for file.c will generate the corresponding integer program in file called int_file.c:

$ ./fa_build/fagcc file.c

Finally, compile the resulting aritmetic program using clang-3.5, and then run loopus:

$ clang-3.5 -g -emit-llvm -DCLOOPUS -c int_file.c
$ loopus -zPrintComplexity int_file.bc

Evaluation

Our experimental evaluation can be found in the following paper [1]


  1. Fiedor, T., Holik, L., Rogalewicz, A., Sinn, M., Vojnar, T., and Zuleger, F.: From Shapes to Amortized Complexity. In: Proceedings of VMCAI'18. Heidelberg: Springer Verlag, 2018, s. 205-225. ISBN 978-3-319-73720-1.

Contact

If you have any questions, do not hesitate to contact the tool/method authors:


Copyright (c) 2018 Tomas Fiedor <ifiedortom@fit.vutbr.cz>