perforate.sh: pluto

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"