From 85c1a1ab1016d9b85de29c24ab4ea2a53f216377 Mon Sep 17 00:00:00 2001
From: Daniel Maier <daniel.maier@tu-berlin.de>
Date: Mon, 5 Nov 2018 09:29:47 +0100
Subject: [PATCH] perforate.sh: pluto
---
perforate.sh | 19 +++++++++++++++++--
1 file changed, 17 insertions(+), 2 deletions(-)
diff --git a/perforate.sh b/perforate.sh
index cb09a71..9bdb7c7 100755
--- a/perforate.sh
+++ b/perforate.sh
@@ -16,6 +16,7 @@ usage() {
printf -- "-s, --statement statement to perforate\n"
printf -- "-l, --level level to perforate\n"
printf -- "-P, --pluto run pluto\n"
+ printf -- "--parallelize pluto parallelize\n"
}
extract_scop() {
@@ -27,8 +28,15 @@ perforate() {
}
run_pluto() {
+ if [ "$1" = "yes" ]; then
+ args="--parallelize"
+ shift
+ else
+ args=""
+ fi
+
# FIXME: what pluto options should be used?
- $PLUTO -o "$2" "$1" > /dev/null
+ $PLUTO "$args" -o "$2" "$1" > /dev/null
}
generate() {
@@ -76,6 +84,9 @@ while true; do
-P|--pluto)
cmd_pluto=yes
;;
+ --parallelize)
+ cmd_pluto_parallelize=yes
+ ;;
*)
break
esac
@@ -125,7 +136,11 @@ fi
if [ "$cmd_pluto" = "yes" ]; then
printf "running pluto on %s output %s\n" "$pluto_input" "$output_src"
- run_pluto "$pluto_input" "$output_src"
+ if [ "$cmd_pluto_parallelize" = "yes" ]; then
+ run_pluto --parallelize "$pluto_input" "$output_src"
+ else
+ run_pluto "$pluto_input" "$output_src"
+ fi
elif [ "$cmd_generate" = "yes" ]; then
# no pluto, just copy to output_src
cat "$pluto_input" > "$output_src"
--
GitLab