Commit 50468710 authored by Etienne Renault's avatar Etienne Renault
Browse files

Add RERS benchmark

* benchs/RERS/2016-Problem10.go,
benchs/RERS/2016-Problem11.go,
benchs/RERS/2016-Problem12.go,
benchs/RERS/2016-Problem14.go,
benchs/RERS/2016-Problem15.go,
benchs/RERS/2017-Problem10.go,
benchs/RERS/2017-Problem11.go,
benchs/RERS/2017-Problem12.go,
benchs/RERS/2017-Problem14.go,
benchs/RERS/2017-Problem15.go,
benchs/RERS/2018-Problem10.go,
benchs/RERS/2018-Problem11.go,
benchs/RERS/2019-Problem11.go,
benchs/RERS/2019-Problem12.go,
benchs/RERS/2019-Problem14.go,
benchs/RERS/2019-Problem15.go,
benchs/RERS/rers2go.sh,
benchs/run-benchmark.sh: Here.
parent ef351ebe
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
#! /bin/bash
# 1er arg : file.c
# Script dedicated to work on RERS challenge. Takes a C file in
# parameter and convert it into a go program that can then be processed
# by the Go2Pins tool.
filename=$(basename -- "$1")
filename="${filename%.*}"
echo Converting $filename
cat $1 | sed 's/#include <stdio.h>//g' | \
sed 's/#include <assert.h>//g' | \
sed 's/#include <math.h>//g' | \
sed 's/#include <stdlib.h>//g' | \
sed 's/extern void __VERIFIER_error(int);/void __VERIFIER_error(int n){}/g' | \
sed 's/int input;/int __RERS__;/g' | sed 's/(input !=/(__RERS__ !=/g' | \
sed 's/calculate_output(input);/calculate_output(__RERS__);/g' | \
sed "s/scanf(\"%d\", &input);/__RERS__ = __RERS__ + 1;/g" | \
sed "s/return -2;/break;/g"| sed "s#fprintf#;//fprintf#g" | \
sed "s#printf#;//printf#g">/tmp/$filename.c
# Requires C to Go transpiler https://github.com/Konstantin8105/c4go
./c4go transpile /tmp/$filename.c
# This last step is mandatory to handle the tranduction of the C instruction
# "a ? b : c" which is translated using closure.
sed -i 's/int32/int/g' $filename.go
# /bin/zsh
# This script runs the benchmark as presented in the paper
# Files from RERSchallenge, category "Sequential Reachability Problems"
# Note that we exclude from this benchmark all files that fall in the
# category "Sequential Reachability Problems/data structures, hard" since
# they require complex array manipulation that are not yet supported by
# the Go2Pins tool.
FILES="RERS/2016-Problem10.go \
RERS/2016-Problem11.go \
RERS/2016-Problem12.go \
RERS/2016-Problem14.go \
RERS/2016-Problem15.go \
RERS/2017-Problem10.go \
RERS/2017-Problem11.go \
RERS/2017-Problem12.go \
RERS/2017-Problem14.go \
RERS/2017-Problem15.go \
RERS/2018-Problem10.go \
RERS/2018-Problem11.go \
RERS/2019-Problem11.go \
RERS/2019-Problem12.go \
RERS/2019-Problem14.go \
RERS/2019-Problem15.go "
OUTPUT=benchs.csv
echo "#filename,loc,transpile_time,compile_time,total_time,final_num_var,final_loc" > $OUTPUT
for model in $FILES; do
echo "==> Processing $model"
loc=$(wc -l $model| awk '{print $1}')
echo " - Line of code (original file):\t$loc"
filename=$(basename -- "$model")
filename="${filename%.*}"
rers_inputs=$(cat $model | grep 'var inputs \[\]int' | \
sed 's/var inputs \[\]int = \[\]int{//g' | \
sed 's/}//g' | sed 's/ *//g' | sed 's/,/;/g')
start=$(date +%s.%N)
../go2pins -f -o $filename -rers "$rers_inputs" $model > /dev/null 2>&1
end=$(date +%s.%N)
transpile_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo " - Go2Pins processing:\t\t$transpile_time seconds"
start=$(date +%s.%N)
make -C $filename > /dev/null 2>&1
end=$(date +%s.%N)
compile_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo " - Compiling output:\t\t\t$compile_time seconds"
total_time=`echo "$compile_time + $transpile_time"| bc`
echo " - Total Time:\t\t\t$total_time seconds"
final_num_var=$($filename/main --displaylist | grep '\-' | wc -l)
echo " - Number of variables:\t\t$final_num_var"
loc2=$(wc -l $filename/$filename.go| tail -n1|awk '{print $1}')
echo " - Line of code generated:\t\t$loc2"
echo
echo "$filename,$loc,$transpile_time,$compile_time,$total_time,$final_num_var,$loc2" >> benchs.csv
done
echo file : $OUTPUT contains the CSV of all previous values
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment