Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
authorwenzelm
Mon Mar 07 18:20:22 2016 +0100 (2016-03-07)
changeset 625458ebffdaf2ce2
parent 62544 efa178abe023
child 62546 973b12bccbc5
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
more robust File.bash_escape;
more robust treatment of ML_OPTIONS;
clarified prover args (again);
src/Pure/Concurrent/bash.scala
src/Pure/General/file.scala
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/ml_process.scala
src/Pure/Tools/check_sources.scala
src/Tools/jEdit/src/isabelle_logic.scala
     1.1 --- a/src/Pure/Concurrent/bash.scala	Mon Mar 07 15:21:50 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Mon Mar 07 18:20:22 2016 +0100
     1.3 @@ -26,20 +26,21 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
     1.8 -    new Process(cwd, env, redirect, args:_*)
     1.9 +  def process(script: String,
    1.10 +      cwd: JFile = null, env: Map[String, String] = null, redirect: Boolean = false): Process =
    1.11 +    new Process(script, cwd, env, redirect)
    1.12  
    1.13    class Process private [Bash](
    1.14 -      cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    1.15 +      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
    1.16      extends Prover.System_Process
    1.17    {
    1.18 +    val script_file = Isabelle_System.tmp_file("bash_script")
    1.19 +    File.write(script_file, script)
    1.20 +
    1.21      private val proc =
    1.22 -    {
    1.23 -      val params =
    1.24 -        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", "bash")
    1.25 -      Isabelle_System.process(
    1.26 -        cwd, Isabelle_System.settings(env), redirect, (params ::: args.toList):_*)
    1.27 -    }
    1.28 +      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
    1.29 +        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
    1.30 +          "bash", File.standard_path(script_file))
    1.31  
    1.32  
    1.33      // channels
    1.34 @@ -90,14 +91,20 @@
    1.35      try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
    1.36      catch { case _: IllegalStateException => }
    1.37  
    1.38 -    private def cleanup() =
    1.39 +
    1.40 +    /* join */
    1.41 +
    1.42 +    def join: Int =
    1.43 +    {
    1.44 +      val rc = proc.waitFor
    1.45 +
    1.46        try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
    1.47        catch { case _: IllegalStateException => }
    1.48  
    1.49 +      script_file.delete
    1.50  
    1.51 -    /* join */
    1.52 -
    1.53 -    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
    1.54 +      rc
    1.55 +    }
    1.56  
    1.57  
    1.58      /* result */
     2.1 --- a/src/Pure/General/file.scala	Mon Mar 07 15:21:50 2016 +0100
     2.2 +++ b/src/Pure/General/file.scala	Mon Mar 07 18:20:22 2016 +0100
     2.3 @@ -101,11 +101,34 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* shell path (bash) */
     2.8 +  /* bash path */
     2.9  
    2.10 -  def shell_quote(s: String): String = "'" + s + "'"
    2.11 -  def shell_path(path: Path): String = shell_quote(standard_path(path))
    2.12 -  def shell_path(file: JFile): String = shell_quote(standard_path(file))
    2.13 +  private def bash_escape(c: Byte): String =
    2.14 +  {
    2.15 +    val ch = c.toChar
    2.16 +    ch match {
    2.17 +      case '\t' => "$'\\t'"
    2.18 +      case '\n' => "$'\\n'"
    2.19 +      case '\f' => "$'\\f'"
    2.20 +      case '\r' => "$'\\r'"
    2.21 +      case _ =>
    2.22 +        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
    2.23 +          Symbol.ascii(ch)
    2.24 +        else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
    2.25 +        else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
    2.26 +        else if (c < 32) "$'\\x" + Integer.toHexString(c) + "'"
    2.27 +        else  "\\" + ch
    2.28 +    }
    2.29 +  }
    2.30 +
    2.31 +  def bash_escape(s: String): String =
    2.32 +    UTF8.bytes(s).iterator.map(bash_escape(_)).mkString
    2.33 +
    2.34 +  def bash_escape(args: List[String]): String =
    2.35 +    args.iterator.map(bash_escape(_)).mkString(" ")
    2.36 +
    2.37 +  def bash_path(path: Path): String = bash_escape(standard_path(path))
    2.38 +  def bash_path(file: JFile): String = bash_escape(standard_path(file))
    2.39  
    2.40  
    2.41    /* directory entries */
     3.1 --- a/src/Pure/PIDE/batch_session.scala	Mon Mar 07 15:21:50 2016 +0100
     3.2 +++ b/src/Pure/PIDE/batch_session.scala	Mon Mar 07 18:20:22 2016 +0100
     3.3 @@ -58,7 +58,7 @@
     3.4          case _ =>
     3.5        }
     3.6  
     3.7 -    prover_session.start("Isabelle", "-q " + quote(parent_session))
     3.8 +    prover_session.start("Isabelle", List("-q", parent_session))
     3.9  
    3.10      batch_session
    3.11    }
     4.1 --- a/src/Pure/PIDE/resources.scala	Mon Mar 07 15:21:50 2016 +0100
     4.2 +++ b/src/Pure/PIDE/resources.scala	Mon Mar 07 18:20:22 2016 +0100
     4.3 @@ -136,7 +136,7 @@
     4.4  
     4.5    /* prover process */
     4.6  
     4.7 -  def start_prover(receiver: Prover.Message => Unit, name: String, args: String): Prover =
     4.8 +  def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
     4.9      Isabelle_Process(receiver, args)
    4.10  }
    4.11  
     5.1 --- a/src/Pure/PIDE/session.scala	Mon Mar 07 15:21:50 2016 +0100
     5.2 +++ b/src/Pure/PIDE/session.scala	Mon Mar 07 18:20:22 2016 +0100
     5.3 @@ -212,7 +212,7 @@
     5.4  
     5.5    /* internal messages */
     5.6  
     5.7 -  private case class Start(name: String, args: String)
     5.8 +  private case class Start(name: String, args: List[String])
     5.9    private case object Stop
    5.10    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    5.11    private case class Protocol_Command(name: String, args: List[String])
    5.12 @@ -601,7 +601,7 @@
    5.13        pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
    5.14      global_state.value.snapshot(name, pending_edits)
    5.15  
    5.16 -  def start(name: String, args: String)
    5.17 +  def start(name: String, args: List[String])
    5.18    { manager.send(Start(name, args)) }
    5.19  
    5.20    def stop()
     6.1 --- a/src/Pure/System/isabelle_process.scala	Mon Mar 07 15:21:50 2016 +0100
     6.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Mar 07 18:20:22 2016 +0100
     6.3 @@ -11,16 +11,14 @@
     6.4  {
     6.5    def apply(
     6.6      receiver: Prover.Message => Unit = Console.println(_),
     6.7 -    prover_args: String = ""): Isabelle_Process =
     6.8 +    prover_args: List[String] = Nil): Isabelle_Process =
     6.9    {
    6.10      val system_channel = System_Channel()
    6.11      val system_process =
    6.12        try {
    6.13 -        val script =
    6.14 -          File.shell_quote(Isabelle_System.getenv_strict("ISABELLE_PROCESS")) +
    6.15 -            " -P " + system_channel.server_name +
    6.16 -            (if (prover_args == "") "" else " " + prover_args)
    6.17 -        val process = Bash.process(null, null, false, "-c", script)
    6.18 +        val process =
    6.19 +          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_escape(system_channel.server_name) +
    6.20 +            " " + File.bash_escape(prover_args))
    6.21          process.stdin.close
    6.22          process
    6.23        }
     7.1 --- a/src/Pure/System/isabelle_system.scala	Mon Mar 07 15:21:50 2016 +0100
     7.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Mar 07 18:20:22 2016 +0100
     7.3 @@ -167,7 +167,7 @@
     7.4  
     7.5    def mkdirs(path: Path): Unit =
     7.6      if (!path.is_dir) {
     7.7 -      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
     7.8 +      bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"")
     7.9        if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
    7.10      }
    7.11  
    7.12 @@ -308,11 +308,7 @@
    7.13      progress_limit: Option[Long] = None,
    7.14      strict: Boolean = true): Process_Result =
    7.15    {
    7.16 -    with_tmp_file("isabelle_script") { script_file =>
    7.17 -      File.write(script_file, script)
    7.18 -      Bash.process(cwd, env, false, File.standard_path(script_file)).
    7.19 -        result(progress_stdout, progress_stderr, progress_limit, strict)
    7.20 -    }
    7.21 +    Bash.process(script, cwd, env).result(progress_stdout, progress_stderr, progress_limit, strict)
    7.22    }
    7.23  
    7.24  
    7.25 @@ -342,7 +338,7 @@
    7.26      bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
    7.27  
    7.28    def hg(cmd_line: String, cwd: Path = Path.current): Process_Result =
    7.29 -    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    7.30 +    bash("cd " + File.bash_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    7.31  
    7.32  
    7.33  
     8.1 --- a/src/Pure/System/ml_process.scala	Mon Mar 07 15:21:50 2016 +0100
     8.2 +++ b/src/Pure/System/ml_process.scala	Mon Mar 07 18:20:22 2016 +0100
     8.3 @@ -66,13 +66,18 @@
     8.4      // options
     8.5      val isabelle_process_options = Isabelle_System.tmp_file("options")
     8.6      File.write(isabelle_process_options, YXML.string_of_body(options.encode))
     8.7 -    val bash_env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     8.8 +    val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     8.9      val eval_options = List("Options.load_default ()")
    8.10  
    8.11      val eval_process =
    8.12        if (process_socket == "") Nil
    8.13        else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
    8.14  
    8.15 +    // bash
    8.16 +    val bash_args =
    8.17 +      Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
    8.18 +      (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
    8.19 +        map(eval => List("--eval", eval)).flatten ::: args
    8.20      val bash_script =
    8.21        """
    8.22          [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
    8.23 @@ -83,7 +88,7 @@
    8.24          chmod $(umask -S) "$ISABELLE_TMP"
    8.25  
    8.26          librarypath "$ML_HOME"
    8.27 -        "$ML_HOME/poly" -q -i $ML_OPTIONS "$@"
    8.28 +        "$ML_HOME/poly" -q -i """ + File.bash_escape(bash_args) + """
    8.29          RC="$?"
    8.30  
    8.31          rm -f "$ISABELLE_PROCESS_OPTIONS"
    8.32 @@ -92,11 +97,6 @@
    8.33          exit "$RC"
    8.34        """
    8.35  
    8.36 -    val bash_args =
    8.37 -      List("-c", bash_script, "ml_process") :::
    8.38 -      (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
    8.39 -        map(eval => List("--eval", eval)).flatten ::: args
    8.40 -
    8.41 -    Bash.process(null, bash_env, false, bash_args:_*)
    8.42 +    Bash.process(bash_script, env = env)
    8.43    }
    8.44  }
     9.1 --- a/src/Pure/Tools/check_sources.scala	Mon Mar 07 15:21:50 2016 +0100
     9.2 +++ b/src/Pure/Tools/check_sources.scala	Mon Mar 07 18:20:22 2016 +0100
     9.3 @@ -41,7 +41,7 @@
     9.4    def check_hg(root: Path)
     9.5    {
     9.6      Output.writeln("Checking " + root + " ...")
     9.7 -    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
     9.8 +    Isabelle_System.hg("--repository " + File.bash_path(root) + " root").check
     9.9      for {
    9.10        file <- Isabelle_System.hg("manifest", root).check.out_lines
    9.11        if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
    10.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Mon Mar 07 15:21:50 2016 +0100
    10.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Mar 07 18:20:22 2016 +0100
    10.3 @@ -69,12 +69,11 @@
    10.4        dirs = session_dirs(), sessions = List(session_name()))
    10.5    }
    10.6  
    10.7 -  def session_args(): String =
    10.8 +  def session_args(): List[String] =
    10.9    {
   10.10 -    val print_modes =
   10.11 -      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
   10.12 -       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).map("-m " + _)
   10.13 -    (print_modes ::: List("-q", File.shell_quote(session_name()))).mkString(" ")
   10.14 +    (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
   10.15 +     space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).
   10.16 +      map(m => List("-m", m)).flatten ::: List("-q", session_name())
   10.17    }
   10.18  
   10.19    def session_start(): Unit = PIDE.session.start("Isabelle", session_args())