removed bash from ML system bootstrap, and past the Secure ML barrier;
authorwenzelm
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27)
changeset 40748591b6778d076
parent 40747 889b7545a408
child 40749 cb6698d2dbaf
removed bash from ML system bootstrap, and past the Secure ML barrier;
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash_sequential.ML
src/Pure/General/secure.ML
src/Pure/IsaMakefile
src/Pure/ML-Systems/bash.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/bash.ML	Sat Nov 27 16:29:53 2010 +0100
     1.3 @@ -0,0 +1,83 @@
     1.4 +(*  Title:      Pure/Concurrent/bash.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +GNU bash processes, with propagation of interrupts.
     1.8 +*)
     1.9 +
    1.10 +local
    1.11 +
    1.12 +fun read_file name =
    1.13 +  let val is = TextIO.openIn name
    1.14 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
    1.15 +
    1.16 +fun write_file name txt =
    1.17 +  let val os = TextIO.openOut name
    1.18 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    1.19 +
    1.20 +in
    1.21 +
    1.22 +fun bash_output script =
    1.23 +  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
    1.24 +    let
    1.25 +      val script_name = OS.FileSys.tmpName ();
    1.26 +      val _ = write_file script_name script;
    1.27 +
    1.28 +      val pid_name = OS.FileSys.tmpName ();
    1.29 +      val output_name = OS.FileSys.tmpName ();
    1.30 +
    1.31 +      (*result state*)
    1.32 +      datatype result = Wait | Signal | Result of int;
    1.33 +      val result = Unsynchronized.ref Wait;
    1.34 +      val lock = Mutex.mutex ();
    1.35 +      val cond = ConditionVar.conditionVar ();
    1.36 +      fun set_result res =
    1.37 +        (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
    1.38 +
    1.39 +      val _ = Mutex.lock lock;
    1.40 +
    1.41 +      (*system thread*)
    1.42 +      val system_thread = Thread.fork (fn () =>
    1.43 +        let
    1.44 +          val status =
    1.45 +            OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
    1.46 +              " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
    1.47 +          val res =
    1.48 +            (case Posix.Process.fromStatus status of
    1.49 +              Posix.Process.W_EXITED => Result 0
    1.50 +            | Posix.Process.W_EXITSTATUS 0wx82 => Signal
    1.51 +            | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
    1.52 +            | Posix.Process.W_SIGNALED s =>
    1.53 +                if s = Posix.Signal.int then Signal
    1.54 +                else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
    1.55 +            | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
    1.56 +        in set_result res end handle _ (*sic*) => set_result (Result 2), []);
    1.57 +
    1.58 +      (*main thread -- proxy for interrupts*)
    1.59 +      fun kill n =
    1.60 +        (case Int.fromString (read_file pid_name) of
    1.61 +          SOME pid =>
    1.62 +            Posix.Process.kill
    1.63 +              (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
    1.64 +                Posix.Signal.int)
    1.65 +        | NONE => ())
    1.66 +        handle OS.SysErr _ => () | IO.Io _ =>
    1.67 +          (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
    1.68 +
    1.69 +      val _ =
    1.70 +        while ! result = Wait do
    1.71 +          let val res =
    1.72 +            Multithreading.sync_wait (SOME orig_atts)
    1.73 +              (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
    1.74 +          in if Exn.is_interrupt_exn res then kill 10 else () end;
    1.75 +
    1.76 +      (*cleanup*)
    1.77 +      val output = read_file output_name handle IO.Io _ => "";
    1.78 +      val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    1.79 +      val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
    1.80 +      val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    1.81 +      val _ = Thread.interrupt system_thread handle Thread _ => ();
    1.82 +      val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
    1.83 +    in (output, rc) end);
    1.84 +
    1.85 +end;
    1.86 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Nov 27 16:29:53 2010 +0100
     2.3 @@ -0,0 +1,43 @@
     2.4 +(*  Title:      Pure/Concurrent/bash_sequential.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Generic GNU bash processes (no provisions to propagate interrupts, but
     2.8 +could work via the controlling tty).
     2.9 +*)
    2.10 +
    2.11 +local
    2.12 +
    2.13 +fun read_file name =
    2.14 +  let val is = TextIO.openIn name
    2.15 +  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
    2.16 +
    2.17 +fun write_file name txt =
    2.18 +  let val os = TextIO.openOut name
    2.19 +  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    2.20 +
    2.21 +in
    2.22 +
    2.23 +fun bash_output script =
    2.24 +  let
    2.25 +    val script_name = OS.FileSys.tmpName ();
    2.26 +    val _ = write_file script_name script;
    2.27 +
    2.28 +    val output_name = OS.FileSys.tmpName ();
    2.29 +
    2.30 +    val status =
    2.31 +      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
    2.32 +        " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
    2.33 +    val rc =
    2.34 +      (case Posix.Process.fromStatus status of
    2.35 +        Posix.Process.W_EXITED => 0
    2.36 +      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    2.37 +      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    2.38 +      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    2.39 +
    2.40 +    val output = read_file output_name handle IO.Io _ => "";
    2.41 +    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    2.42 +    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    2.43 +  in (output, rc) end;
    2.44 +
    2.45 +end;
    2.46 +
     3.1 --- a/src/Pure/General/secure.ML	Sat Nov 27 16:27:52 2010 +0100
     3.2 +++ b/src/Pure/General/secure.ML	Sat Nov 27 16:29:53 2010 +0100
     3.3 @@ -15,8 +15,6 @@
     3.4    val toplevel_pp: string list -> string -> unit
     3.5    val PG_setup: unit -> unit
     3.6    val commit: unit -> unit
     3.7 -  val bash_output: string -> string * int
     3.8 -  val bash: string -> int
     3.9  end;
    3.10  
    3.11  structure Secure: SECURE =
    3.12 @@ -58,20 +56,6 @@
    3.13  fun PG_setup () =
    3.14    use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
    3.15  
    3.16 -
    3.17 -(* shell commands *)
    3.18 -
    3.19 -fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
    3.20 -
    3.21 -val orig_bash_output = bash_output;
    3.22 -
    3.23 -fun bash_output s = (secure_shell (); orig_bash_output s);
    3.24 -
    3.25 -fun bash s =
    3.26 -  (case bash_output s of
    3.27 -    ("", rc) => rc
    3.28 -  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
    3.29 -
    3.30  end;
    3.31  
    3.32  (*override previous toplevel bindings!*)
    3.33 @@ -80,5 +64,4 @@
    3.34  fun use s = Secure.use_file ML_Parse.global_context true s
    3.35    handle ERROR msg => (writeln msg; error "ML error");
    3.36  val toplevel_pp = Secure.toplevel_pp;
    3.37 -val bash_output = Secure.bash_output;
    3.38 -val bash = Secure.bash;
    3.39 +
     4.1 --- a/src/Pure/IsaMakefile	Sat Nov 27 16:27:52 2010 +0100
     4.2 +++ b/src/Pure/IsaMakefile	Sat Nov 27 16:29:53 2010 +0100
     4.3 @@ -22,7 +22,6 @@
     4.4  BOOTSTRAP_FILES = 					\
     4.5    General/exn.ML					\
     4.6    General/timing.ML					\
     4.7 -  ML-Systems/bash.ML 					\
     4.8    ML-Systems/compiler_polyml-5.2.ML			\
     4.9    ML-Systems/compiler_polyml-5.3.ML			\
    4.10    ML-Systems/ml_name_space.ML				\
    4.11 @@ -55,6 +54,8 @@
    4.12  Pure: $(OUT)/Pure
    4.13  
    4.14  $(OUT)/Pure: $(BOOTSTRAP_FILES)				\
    4.15 +  Concurrent/bash.ML 					\
    4.16 +  Concurrent/bash_sequential.ML				\
    4.17    Concurrent/cache.ML					\
    4.18    Concurrent/future.ML					\
    4.19    Concurrent/lazy.ML					\
     5.1 --- a/src/Pure/ML-Systems/bash.ML	Sat Nov 27 16:27:52 2010 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,43 +0,0 @@
     5.4 -(*  Title:      Pure/ML-Systems/bash.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Generic GNU bash processes (no provisions to propagate interrupts, but
     5.8 -could work via the controlling tty).
     5.9 -*)
    5.10 -
    5.11 -local
    5.12 -
    5.13 -fun read_file name =
    5.14 -  let val is = TextIO.openIn name
    5.15 -  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
    5.16 -
    5.17 -fun write_file name txt =
    5.18 -  let val os = TextIO.openOut name
    5.19 -  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    5.20 -
    5.21 -in
    5.22 -
    5.23 -fun bash_output script =
    5.24 -  let
    5.25 -    val script_name = OS.FileSys.tmpName ();
    5.26 -    val _ = write_file script_name script;
    5.27 -
    5.28 -    val output_name = OS.FileSys.tmpName ();
    5.29 -
    5.30 -    val status =
    5.31 -      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
    5.32 -        " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
    5.33 -    val rc =
    5.34 -      (case Posix.Process.fromStatus status of
    5.35 -        Posix.Process.W_EXITED => 0
    5.36 -      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    5.37 -      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    5.38 -      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    5.39 -
    5.40 -    val output = read_file output_name handle IO.Io _ => "";
    5.41 -    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    5.42 -    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    5.43 -  in (output, rc) end;
    5.44 -
    5.45 -end;
    5.46 -
     6.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 16:27:52 2010 +0100
     6.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Nov 27 16:29:53 2010 +0100
     6.3 @@ -8,7 +8,6 @@
     6.4  sig
     6.5    val interruptible: ('a -> 'b) -> 'a -> 'b
     6.6    val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
     6.7 -  val bash_output: string -> string * int
     6.8    structure TimeLimit: TIME_LIMIT
     6.9  end;
    6.10  
    6.11 @@ -42,20 +41,6 @@
    6.12  fun enabled () = max_threads_value () > 1;
    6.13  
    6.14  
    6.15 -(* misc utils *)
    6.16 -
    6.17 -fun show "" = "" | show name = " " ^ name;
    6.18 -fun show' "" = "" | show' name = " [" ^ name ^ "]";
    6.19 -
    6.20 -fun read_file name =
    6.21 -  let val is = TextIO.openIn name
    6.22 -  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
    6.23 -
    6.24 -fun write_file name txt =
    6.25 -  let val os = TextIO.openOut name
    6.26 -  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
    6.27 -
    6.28 -
    6.29  (* thread attributes *)
    6.30  
    6.31  val no_interrupts =
    6.32 @@ -156,71 +141,6 @@
    6.33  end;
    6.34  
    6.35  
    6.36 -(* GNU bash processes, with propagation of interrupts *)
    6.37 -
    6.38 -fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
    6.39 -  let
    6.40 -    val script_name = OS.FileSys.tmpName ();
    6.41 -    val _ = write_file script_name script;
    6.42 -
    6.43 -    val pid_name = OS.FileSys.tmpName ();
    6.44 -    val output_name = OS.FileSys.tmpName ();
    6.45 -
    6.46 -    (*result state*)
    6.47 -    datatype result = Wait | Signal | Result of int;
    6.48 -    val result = ref Wait;
    6.49 -    val lock = Mutex.mutex ();
    6.50 -    val cond = ConditionVar.conditionVar ();
    6.51 -    fun set_result res =
    6.52 -      (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
    6.53 -
    6.54 -    val _ = Mutex.lock lock;
    6.55 -
    6.56 -    (*system thread*)
    6.57 -    val system_thread = Thread.fork (fn () =>
    6.58 -      let
    6.59 -        val status =
    6.60 -          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
    6.61 -            " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
    6.62 -        val res =
    6.63 -          (case Posix.Process.fromStatus status of
    6.64 -            Posix.Process.W_EXITED => Result 0
    6.65 -          | Posix.Process.W_EXITSTATUS 0wx82 => Signal
    6.66 -          | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
    6.67 -          | Posix.Process.W_SIGNALED s =>
    6.68 -              if s = Posix.Signal.int then Signal
    6.69 -              else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
    6.70 -          | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
    6.71 -      in set_result res end handle _ (*sic*) => set_result (Result 2), []);
    6.72 -
    6.73 -    (*main thread -- proxy for interrupts*)
    6.74 -    fun kill n =
    6.75 -      (case Int.fromString (read_file pid_name) of
    6.76 -        SOME pid =>
    6.77 -          Posix.Process.kill
    6.78 -            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
    6.79 -              Posix.Signal.int)
    6.80 -      | NONE => ())
    6.81 -      handle OS.SysErr _ => () | IO.Io _ =>
    6.82 -        (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
    6.83 -
    6.84 -    val _ =
    6.85 -      while ! result = Wait do
    6.86 -        let val res =
    6.87 -          sync_wait (SOME orig_atts)
    6.88 -            (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
    6.89 -        in if Exn.is_interrupt_exn res then kill 10 else () end;
    6.90 -
    6.91 -    (*cleanup*)
    6.92 -    val output = read_file output_name handle IO.Io _ => "";
    6.93 -    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    6.94 -    val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
    6.95 -    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    6.96 -    val _ = Thread.interrupt system_thread handle Thread _ => ();
    6.97 -    val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
    6.98 -  in (output, rc) end);
    6.99 -
   6.100 -
   6.101  (* critical section -- may be nested within the same thread *)
   6.102  
   6.103  local
   6.104 @@ -229,6 +149,9 @@
   6.105  val critical_thread = ref (NONE: Thread.thread option);
   6.106  val critical_name = ref "";
   6.107  
   6.108 +fun show "" = "" | show name = " " ^ name;
   6.109 +fun show' "" = "" | show' name = " [" ^ name ^ "]";
   6.110 +
   6.111  in
   6.112  
   6.113  fun self_critical () =
     7.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 27 16:27:52 2010 +0100
     7.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 27 16:29:53 2010 +0100
     7.3 @@ -14,7 +14,6 @@
     7.4  use "ML-Systems/multithreading.ML";
     7.5  use "ML-Systems/time_limit.ML";
     7.6  use "General/timing.ML";
     7.7 -use "ML-Systems/bash.ML";
     7.8  use "ML-Systems/ml_pretty.ML";
     7.9  use "ML-Systems/use_context.ML";
    7.10  
     8.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 16:27:52 2010 +0100
     8.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 27 16:29:53 2010 +0100
     8.3 @@ -14,7 +14,6 @@
     8.4  use "ML-Systems/thread_dummy.ML";
     8.5  use "ML-Systems/multithreading.ML";
     8.6  use "General/timing.ML";
     8.7 -use "ML-Systems/bash.ML";
     8.8  use "ML-Systems/ml_name_space.ML";
     8.9  use "ML-Systems/ml_pretty.ML";
    8.10  structure PolyML = struct end;
    8.11 @@ -170,11 +169,6 @@
    8.12  val pwd = OS.FileSys.getDir;
    8.13  
    8.14  
    8.15 -(* system command execution *)
    8.16 -
    8.17 -val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
    8.18 -
    8.19 -
    8.20  (* getenv *)
    8.21  
    8.22  fun getenv var =
     9.1 --- a/src/Pure/ROOT.ML	Sat Nov 27 16:27:52 2010 +0100
     9.2 +++ b/src/Pure/ROOT.ML	Sat Nov 27 16:29:53 2010 +0100
     9.3 @@ -72,6 +72,15 @@
     9.4  if Multithreading.available then ()
     9.5  else use "Concurrent/synchronized_sequential.ML";
     9.6  
     9.7 +if Multithreading.available
     9.8 +then use "Concurrent/bash.ML"
     9.9 +else use "Concurrent/bash_sequential.ML";
    9.10 +
    9.11 +fun bash s =
    9.12 +  (case bash_output s of
    9.13 +    ("", rc) => rc
    9.14 +  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
    9.15 +
    9.16  use "Concurrent/mailbox.ML";
    9.17  use "Concurrent/task_queue.ML";
    9.18  use "Concurrent/future.ML";