A symbolic execution engine for finding bugs in programs.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
svcomp19_config
.gitignore
LICENSE
LICENSE.Glucose-Syrup
LICENSE.Symex
README.md
bin.zip

README.md

Pinaka 0.1

INTRUCTIONS to configure Pinaka in Benchexec:

  • Clone this repository
     git clone https://github.com/sbjoshi/Pinaka.git
         cd Pinaka
         unzip bin.zip
         cd ..
    
  • Get Benchmarks and Benchexec
     git clone --depth=1 https://github.com/sosy-lab/sv-benchmarks
     git clone https://github.com/sosy-lab/benchexec
     cd benchexec
    
  • Copy relevant files to appropriate places in benchexec
     cp ../Pinaka/svcomp19_config/pinaka.xml ../Pinaka/svcomp19_config/pinaka-wrapper.sh .
     cp ../Pinaka/bin/pinaka .
     cp ../Pinaka/svcomp19_config/pinaka.py benchexec/tools
    
  • Ensure that you modify timelimit, memorylimit and cpuCores in pinaka.xml depending upon the resource limit you have.

INTRUCTIONS TO RUN BENCHMARKS:

  • Navigate back to top-level benchexec directory
  • To run a set of tasks :
     sed -i 's/witness.graphml/${logfile_path_abs}${inputfile_name}-witness.graphml/' pinaka.xml
     sudo chmod o+wt '/sys/fs/cgroup/cpuset/'
     sudo chmod o+wt '/sys/fs/cgroup/cpu,cpuacct/'
     sudo chmod o+wt '/sys/fs/cgroup/freezer/'
     sudo chmod o+wt '/sys/fs/cgroup/memory/'
     sudo swapoff -a
     bin/benchexec pinaka.xml --tasks="ReachSafety-TASKSET"
    

NOTE:

  • TASKSET needs to be replaced for the particular task to be run whose names can be found in pinaka.xml file.
    Example: bin/benchexec pinaka.xml --tasks="ReachSafety-BitVectors"
  • 'tasks' option may be removed to run the tool on all verification tasks at once.

Results i.e. graphml witnesses will be stored in results directory (wrt. pwd).

  • To validate violation-witnesses:
     wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/cpa-seq-validate-correctness-witnesses.xml
     wget https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/cpa-seq-validate-violation-witnesses.xml
     git clone --depth=1 https://github.com/sosy-lab/cpachecker.git
     cd cpachecker
     ant
     cd ..
     ln -s cpachecker/scripts/cpa.sh cpa.sh
     ln -s cpachecker/config/ config
     ### manually tweak the requiredfiles and option name=-witness lines in cpa-seq-validate*.xml
     bin/benchexec cpa-seq-validate-correctness-witnesses.xml
     bin/benchexec cpa-seq-validate-violation-witnesses.xml
    

REQUIREMENTS:

libstdc++.so.6 & gcc 7.3.0 are required on Ubuntu 18.04

RELEASE:

Source code for the tool to be made public by the end of this year