diff --git a/perforate.sh b/perforate.sh index cb09a713bac525cfb8703b2bc444b14b86ac20ec..9bdb7c7bc47861ceb66842e24e5f1e46752f8680 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"