run-benchmarks-lola.sh 1.71 KB
Newer Older
1 2
#!/bin/bash

3
benchmarks=( 'service-tech/ibm-soundness' )
4 5 6
extensions=( 'lola' )

properties=( 'safe' 'fin' )
7 8

tool='lola'
9 10
executable='lola'
options=''
11

12 13 14
#1 hour
time_soft=$(expr 1 \* 3600)
time_hard=$(expr $time_soft + 60)
15 16
#8 gigabyte
mem_soft=$(expr 8 \* 1024 \* 1024)
17 18
mem_hard=$(expr $mem_soft + 1024)

19
for benchmark in ${benchmarks[@]}; do
20 21 22 23 24 25 26
    benchmark_dir="$benchmark"
    for prop in ${properties[@]}; do
        >$benchmark_dir/$prop-positive-$tool.list
        >$benchmark_dir/$prop-negative-$tool.list
        >$benchmark_dir/$prop-timeout-$tool.list
        >$benchmark_dir/$prop-error-$tool.list
        for ext in ${extensions[@]}; do
27
            for file in `find $benchmark_dir -name "*.$ext"`; do
28 29 30 31 32 33 34
                timing="$(date +%s%N)"
                (
                    ulimit -S -t $time_soft
                    ulimit -H -t $time_hard
                    ulimit -S -v $mem_soft
                    ulimit -H -v $mem_hard
                    set -o pipefail;
35 36
                    echo $executable $options -f $file.$prop.task $file
                    $executable $options -f $file.$prop.task $file 2>&1 | tee $file.out
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
                )
                result=$?
                ryes=$(grep "result: yes" $file.out)
                rno=$(grep "result: no" $file.out)
                T=$(($(date +%s%N)-T))
                if [[ -n $ryes ]]; then
                    list='positive'
                elif [[ -n $rno ]]; then
                    list='negative'
                elif [[ result -eq 2 ]]; then
                    list='timeout'
                else
                    list='error'
                fi
                echo $T $file >>$benchmark_dir/$prop-$list-$tool.list
            done
        done
54 55
    done
done