# HG changeset patch # User wenzelm # Date 1290871793 -3600 # Node ID 591b6778d076658a1d31aaf639ec936cf6ee3411 # Parent 889b7545a408098b92801065cfe0f8d3af32ef1c removed bash from ML system bootstrap, and past the Secure ML barrier; diff -r 889b7545a408 -r 591b6778d076 src/Pure/Concurrent/bash.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 16:29:53 2010 +0100 @@ -0,0 +1,83 @@ +(* Title: Pure/Concurrent/bash.ML + Author: Makarius + +GNU bash processes, with propagation of interrupts. +*) + +local + +fun read_file name = + let val is = TextIO.openIn name + in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; + +fun write_file name txt = + let val os = TextIO.openOut name + in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; + +in + +fun bash_output script = + Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts => + let + val script_name = OS.FileSys.tmpName (); + val _ = write_file script_name script; + + val pid_name = OS.FileSys.tmpName (); + val output_name = OS.FileSys.tmpName (); + + (*result state*) + datatype result = Wait | Signal | Result of int; + val result = Unsynchronized.ref Wait; + val lock = Mutex.mutex (); + val cond = ConditionVar.conditionVar (); + fun set_result res = + (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock); + + val _ = Mutex.lock lock; + + (*system thread*) + val system_thread = Thread.fork (fn () => + let + val status = + OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^ + " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); + val res = + (case Posix.Process.fromStatus status of + Posix.Process.W_EXITED => Result 0 + | Posix.Process.W_EXITSTATUS 0wx82 => Signal + | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) + | Posix.Process.W_SIGNALED s => + if s = Posix.Signal.int then Signal + else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) + | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); + in set_result res end handle _ (*sic*) => set_result (Result 2), []); + + (*main thread -- proxy for interrupts*) + fun kill n = + (case Int.fromString (read_file pid_name) of + SOME pid => + Posix.Process.kill + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), + Posix.Signal.int) + | NONE => ()) + handle OS.SysErr _ => () | IO.Io _ => + (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ()); + + val _ = + while ! result = Wait do + let val res = + Multithreading.sync_wait (SOME orig_atts) + (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock + in if Exn.is_interrupt_exn res then kill 10 else () end; + + (*cleanup*) + val output = read_file output_name handle IO.Io _ => ""; + val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); + val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => (); + val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); + val _ = Thread.interrupt system_thread handle Thread _ => (); + val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc); + in (output, rc) end); + +end; + diff -r 889b7545a408 -r 591b6778d076 src/Pure/Concurrent/bash_sequential.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 16:29:53 2010 +0100 @@ -0,0 +1,43 @@ +(* Title: Pure/Concurrent/bash_sequential.ML + Author: Makarius + +Generic GNU bash processes (no provisions to propagate interrupts, but +could work via the controlling tty). +*) + +local + +fun read_file name = + let val is = TextIO.openIn name + in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; + +fun write_file name txt = + let val os = TextIO.openOut name + in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; + +in + +fun bash_output script = + let + val script_name = OS.FileSys.tmpName (); + val _ = write_file script_name script; + + val output_name = OS.FileSys.tmpName (); + + val status = + OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ + " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); + val rc = + (case Posix.Process.fromStatus status of + Posix.Process.W_EXITED => 0 + | Posix.Process.W_EXITSTATUS w => Word8.toInt w + | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) + | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s)); + + val output = read_file output_name handle IO.Io _ => ""; + val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); + val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); + in (output, rc) end; + +end; + diff -r 889b7545a408 -r 591b6778d076 src/Pure/General/secure.ML --- a/src/Pure/General/secure.ML Sat Nov 27 16:27:52 2010 +0100 +++ b/src/Pure/General/secure.ML Sat Nov 27 16:29:53 2010 +0100 @@ -15,8 +15,6 @@ val toplevel_pp: string list -> string -> unit val PG_setup: unit -> unit val commit: unit -> unit - val bash_output: string -> string * int - val bash: string -> int end; structure Secure: SECURE = @@ -58,20 +56,6 @@ fun PG_setup () = use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;"; - -(* shell commands *) - -fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode"; - -val orig_bash_output = bash_output; - -fun bash_output s = (secure_shell (); orig_bash_output s); - -fun bash s = - (case bash_output s of - ("", rc) => rc - | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc)); - end; (*override previous toplevel bindings!*) @@ -80,5 +64,4 @@ fun use s = Secure.use_file ML_Parse.global_context true s handle ERROR msg => (writeln msg; error "ML error"); val toplevel_pp = Secure.toplevel_pp; -val bash_output = Secure.bash_output; -val bash = Secure.bash; + diff -r 889b7545a408 -r 591b6778d076 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Nov 27 16:27:52 2010 +0100 +++ b/src/Pure/IsaMakefile Sat Nov 27 16:29:53 2010 +0100 @@ -22,7 +22,6 @@ BOOTSTRAP_FILES = \ General/exn.ML \ General/timing.ML \ - ML-Systems/bash.ML \ ML-Systems/compiler_polyml-5.2.ML \ ML-Systems/compiler_polyml-5.3.ML \ ML-Systems/ml_name_space.ML \ @@ -55,6 +54,8 @@ Pure: $(OUT)/Pure $(OUT)/Pure: $(BOOTSTRAP_FILES) \ + Concurrent/bash.ML \ + Concurrent/bash_sequential.ML \ Concurrent/cache.ML \ Concurrent/future.ML \ Concurrent/lazy.ML \ diff -r 889b7545a408 -r 591b6778d076 src/Pure/ML-Systems/bash.ML --- a/src/Pure/ML-Systems/bash.ML Sat Nov 27 16:27:52 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,43 +0,0 @@ -(* Title: Pure/ML-Systems/bash.ML - Author: Makarius - -Generic GNU bash processes (no provisions to propagate interrupts, but -could work via the controlling tty). -*) - -local - -fun read_file name = - let val is = TextIO.openIn name - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; - -fun write_file name txt = - let val os = TextIO.openOut name - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; - -in - -fun bash_output script = - let - val script_name = OS.FileSys.tmpName (); - val _ = write_file script_name script; - - val output_name = OS.FileSys.tmpName (); - - val status = - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); - val rc = - (case Posix.Process.fromStatus status of - Posix.Process.W_EXITED => 0 - | Posix.Process.W_EXITSTATUS w => Word8.toInt w - | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) - | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s)); - - val output = read_file output_name handle IO.Io _ => ""; - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); - in (output, rc) end; - -end; - diff -r 889b7545a408 -r 591b6778d076 src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 16:27:52 2010 +0100 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 16:29:53 2010 +0100 @@ -8,7 +8,6 @@ sig val interruptible: ('a -> 'b) -> 'a -> 'b val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b - val bash_output: string -> string * int structure TimeLimit: TIME_LIMIT end; @@ -42,20 +41,6 @@ fun enabled () = max_threads_value () > 1; -(* misc utils *) - -fun show "" = "" | show name = " " ^ name; -fun show' "" = "" | show' name = " [" ^ name ^ "]"; - -fun read_file name = - let val is = TextIO.openIn name - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; - -fun write_file name txt = - let val os = TextIO.openOut name - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; - - (* thread attributes *) val no_interrupts = @@ -156,71 +141,6 @@ end; -(* GNU bash processes, with propagation of interrupts *) - -fun bash_output script = with_attributes no_interrupts (fn orig_atts => - let - val script_name = OS.FileSys.tmpName (); - val _ = write_file script_name script; - - val pid_name = OS.FileSys.tmpName (); - val output_name = OS.FileSys.tmpName (); - - (*result state*) - datatype result = Wait | Signal | Result of int; - val result = ref Wait; - val lock = Mutex.mutex (); - val cond = ConditionVar.conditionVar (); - fun set_result res = - (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock); - - val _ = Mutex.lock lock; - - (*system thread*) - val system_thread = Thread.fork (fn () => - let - val status = - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^ - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); - val res = - (case Posix.Process.fromStatus status of - Posix.Process.W_EXITED => Result 0 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) - | Posix.Process.W_SIGNALED s => - if s = Posix.Signal.int then Signal - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) - | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); - in set_result res end handle _ (*sic*) => set_result (Result 2), []); - - (*main thread -- proxy for interrupts*) - fun kill n = - (case Int.fromString (read_file pid_name) of - SOME pid => - Posix.Process.kill - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), - Posix.Signal.int) - | NONE => ()) - handle OS.SysErr _ => () | IO.Io _ => - (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ()); - - val _ = - while ! result = Wait do - let val res = - sync_wait (SOME orig_atts) - (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock - in if Exn.is_interrupt_exn res then kill 10 else () end; - - (*cleanup*) - val output = read_file output_name handle IO.Io _ => ""; - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); - val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => (); - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); - val _ = Thread.interrupt system_thread handle Thread _ => (); - val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc); - in (output, rc) end); - - (* critical section -- may be nested within the same thread *) local @@ -229,6 +149,9 @@ val critical_thread = ref (NONE: Thread.thread option); val critical_name = ref ""; +fun show "" = "" | show name = " " ^ name; +fun show' "" = "" | show' name = " [" ^ name ^ "]"; + in fun self_critical () = diff -r 889b7545a408 -r 591b6778d076 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 16:27:52 2010 +0100 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 16:29:53 2010 +0100 @@ -14,7 +14,6 @@ use "ML-Systems/multithreading.ML"; use "ML-Systems/time_limit.ML"; use "General/timing.ML"; -use "ML-Systems/bash.ML"; use "ML-Systems/ml_pretty.ML"; use "ML-Systems/use_context.ML"; diff -r 889b7545a408 -r 591b6778d076 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 16:27:52 2010 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 16:29:53 2010 +0100 @@ -14,7 +14,6 @@ use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML"; use "General/timing.ML"; -use "ML-Systems/bash.ML"; use "ML-Systems/ml_name_space.ML"; use "ML-Systems/ml_pretty.ML"; structure PolyML = struct end; @@ -170,11 +169,6 @@ val pwd = OS.FileSys.getDir; -(* system command execution *) - -val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output; - - (* getenv *) fun getenv var = diff -r 889b7545a408 -r 591b6778d076 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Nov 27 16:27:52 2010 +0100 +++ b/src/Pure/ROOT.ML Sat Nov 27 16:29:53 2010 +0100 @@ -72,6 +72,15 @@ if Multithreading.available then () else use "Concurrent/synchronized_sequential.ML"; +if Multithreading.available +then use "Concurrent/bash.ML" +else use "Concurrent/bash_sequential.ML"; + +fun bash s = + (case bash_output s of + ("", rc) => rc + | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc)); + use "Concurrent/mailbox.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML";