Predator

Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. The tool can be loaded into GCC as a plug-in. This way you can easily analyse C code sources, using the existing build system, without manually preprocessing them first. The analysis itself is, however, not ready for complex projects yet. The plug-in is based on Code Listener infrastructure (included). Although the tool is intended to be as portable as GCC is, we support only Linux for now. Current version of Predator is available on GitHub.

Recently, an extension of Predator for converting low-level pointer programs implementing list containers to high-level list container programs has been implemented. More information on this extension as well as its prototype implementation is available here.

Awards

  • SV-COMP 2016 — The 5th International Competition on Software Verification

    The Predator tool (Predator-HP) took part in the SV-COMP 2016 and won gold medal in category Heap.

  • SVCOMP'15 — The 4th International Competition on Software Verification

    The Predator tool (Predator-HP) took part in the SV-COMP'15 and won one gold and one silver medal.

  •  FLoC Olympic Games 2014

    The Predator tool has been awarded the Kurt Gödel medal at the FLoC Olympic Games 2014 for its successes in three consecutive years of the international competition in software verification SV-COMP.

  •  SVCOMP'14 — The 3rd International Competition on Software Verification

    Predator won the silver medal in category Heap Manipulation and the bronze medal in category Memory Safety. Moreover, in these categories, it achieved the best result among tools with a sound treatment of dynamic memory (i.e., it achieved the best result among the tools dealing with memory in an unbounded way). Predator was the only tool that achieved the maximal possible score on the ProductLines benchmark. The soundness of Predator's verification approach was again confirmed on the Overall benchmark (consisting of 2868 case studies). If you want to reproduce the competition results, please download predator-2013-10-30-d1bd405.tar.gz and follow the instructions in the file README-SVCOMP-2014, which is included in the archive. The release predator-2013-10-30-d1bd405 was tuned to achieve competitive results in SVCOMP'14. As usually, numerous bug fixes, compatibility fixes, and performance improvements were included.

  •  SVCOMP'13 — The 2nd International Competition on Software Verification

    The Predator tool won three categories of the SV-COMP'13 competition.

  •  SVCOMP'12 — The 1st International Competition on Software Verification

    The Predator tool won one of the categories of the SV-COMP'12 competition.

Build from Sources

Prerequisities to install on Ubuntu-14.04:

# apt-get install cmake g++ g++-multilib gcc-4.8-plugin-dev libboost-dev make git

Note: the version number in gcc-4.8-plugin-dev should be the same as /usr/bin/gcc version.

Next 3 commands should download and build the current version of Predator:

git clone https://github.com/kdudka/predator
cd predator
./switch-host-gcc.sh /usr/bin/gcc

Note: the regression test results depend on gcc version - do not expect 100% success for different gcc version.

textREADME - complete installation instructions

Usage

Basic usage using slgcc script:

/PATH-TO-predator-DIRECTORY/sl_build/slgcc  file-to-check.c

Recommended usage:

ln -s /PATH-TO-predator-DIRECTORY/sl_build/slgcc  /PATH-TO-YOUR-bin-DIRECTORY/predator
predator  file-to-check.c

You can use the same options as gcc.

Plotting of SMGs needs setting the environment variables before running predator:

export  SL_PLOT=1
export  SVG_VIEWER=chromium-browser  # Adjust for your SVG viewer

To employ the Predator plug-in in a build of an arbitrary project fully transparently, it is recommended to set certain environment variables. You can use the script register-paths.sh to do this automatically:

. sl_build/register-paths.sh

Then you can simply use the -fplugin option of GCC as documented in the gcc(1) man page:

gcc -fplugin=libsl.so ...

This will show you the available options of the Predator plug-in itself:

echo please help | gcc -fplugin=libsl.so -fplugin-arg-libsl-help -xc -

Source Code

Documentation

pdfTechnical Report 2012-04 (extended version of the SAS 2013 paper)

Conference Papers

  1. K. Dudka, P. Peringer, and T. Vojnar. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. In Proc. of 23rd International Conference on Computer Aided Verification — CAV'11, Cliff Lodge, Snowbird, Utah, USA, volume 6806 of LNCS, pages 372—378, 2011. Springer-Verlag.
  2. K. Dudka, P. Peringer, and T. Vojnar. Byte-Precise Verification of Low-Level List Manipulation. In Proc. of 20th Static Analysis Symposium — SAS'13, Seattle, USA, volume 7935 of LNCS, pages 214—237, 2013. Springer-Verlag.

Competition Contributions

  1. K. Dudka, P. Müller, P. Peringer, and T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'12, Talinn, Estonia, volume 7214 of LNCS, pages 545—548, 2012. Springer-Verlag.
  2. K. Dudka, P. Müller, P. Peringer, and T. Vojnar. A Tool for Verification of Low-level List Manipulation. In Proc. of 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'13, Rome, Italy, volume 7795 of LNCS, pages 627—629, 2013. Springer-Verlag.
  3. K. Dudka, P. Peringer, and T. Vojnar. Predator: A Shape Analyzer Based on Symbolic Memory Graphs. In Proc. of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'14, Grenoble, France, volume 8413 of LNCS, pages 412—414, 2014. Springer-Verlag.
  4. P. Muller, P. Peringer, and T. Vojnar. Predator Hunting Party (Competition Contribution). In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems-- TACAS'15, London, UK, volume 9035 of LNCS, pages 443-446, 2015. Springer-Verlag.

Predator Team

Acknowledgement

Over the years, the work on Predator was supported by the Czech Science Foundation (projecta P103/10/0306 and 14-11384S), the Czech Ministry of Education, Youth, and Sports (projects COST OC10009 and MSM 0021630528), the EU/Czech IT4Innovations Centre of Excellence CZ.1.05/1.1.00/02.0070, and the internal Brno University of Technology projects FIT-S-11-1, FIT-S-12-1, and FIT-S-14-2486.