Re: [isabelle] Isabelleâs getsettings somehow broken



Dear Makarius,

Am Mittwoch, den 10.02.2016, 17:54 +0100 schrieb Makarius:
> On Wed, 10 Feb 2016, Joachim Breitner wrote:
> 
> > After further digging, it turns out that it works if /bin/sh does pointÂ
> > to /bin/bash instead of /bin/dash. Bisecting the version ranges of dash,Â
> > the problem started to appear in 0.5.8. Likely contender:Â
> > http://git.kernel.org/cgit/utils/dash/dash.git/commit/?id=46d3c1a614f11f0d40a7e73376359618ff07abcd
> 
> That change is from 2012. My impression is that the bash guys have alreadyÂ
> taken measures against such "sanitised environments" some years ago: theÂ
> shell functions are represented as regular assignments of the form A=B,Â
> e.g. BASH_FUNC_isabelle_scala%%=() ...
> 
> 
> > I notified the dash developers about the problem, but dash 0.5.8
> 
> There must be a new problem in dash 0.5.8.Â

..as I said, itâs the commit above. If you look at
http://git.kernel.org/cgit/utils/dash/dash.git/log/
and press next you see that it is contained in the 0.5.8 tag, but not
the 0.5.7 tag datedÂ2011-07-08.

dashâs upstream (Erik Blake) says this is not a bug and POSIX conform:
http://www.mail-archive.com/dash at vger.kernel.org/msg01147.html

> > I suggest to either ensure that bash scripts within Isabelle call eachÂ
> > other via bash only, or (likely more reliable) do not rely on exportingÂ
> > bash functions via the environment, but source their definition in everyÂ
> > shell.
> 
> I've spent some years on variations on all that already, refining it overÂ
> and over again.
> 
> Isabelle exclusively uses bash wherever possible. Sometimes other systemÂ
> function sneak-in unreliable /bin/sh.

I digged deeper, assuming the poisonous 'sh -c "..."' pattern
somewhere, and using strace I saw these four calls going via /bin/sh:
[pid 19336] execve("/bin/sh", ["sh", "-c", "exec \"$EXEC_PROCESS\" '/tmp/isabelle-jojo19273/bash_pid995593' \"exec bash '/tmp/isabelle-jojo19273/bash_script995593' > '/tmp/isabelle-jojo19273/bash_out995593' 2> '/tmp/isabelle-jojo19273/bash_err995593'\""], [/* 187 vars */]) = 0
[pid 19352] execve("/bin/sh", ["sh", "-c", "exec \"$EXEC_PROCESS\" '/tmp/isabelle-jojo19273/bash_pid995594' \"exec bash '/tmp/isabelle-jojo19273/bash_script995594' > '/tmp/isabelle-jojo19273/bash_out995594' 2> '/tmp/isabelle-jojo19273/bash_err995594'\""], [/* 187 vars */]) = 0
[pid 19355] execve("/bin/sh", ["sh", "-c", "exec \"$EXEC_PROCESS\" '/tmp/isabelle-jojo19273/bash_pid995595' \"exec bash '/tmp/isabelle-jojo19273/bash_script995595' > '/tmp/isabelle-jojo19273/bash_out995595' 2> '/tmp/isabelle-jojo19273/bash_err995595'\""], [/* 187 vars */]) = 0
[pid 19358] execve("/bin/sh", ["sh", "-c", "exec \"$EXEC_PROCESS\" '/tmp/isabelle-jojo19273/bash_pid995596' \"exec bash '/tmp/isabelle-jojo19273/bash_script995596' > '/tmp/isabelle-jojo19273/bash_out995596' 2> '/tmp/isabelle-jojo19273/bash_err995596'\""], [/* 187 vars */]) = 0

So this points to these lines

      val _ = File.write script_path script;
ÂÂÂÂÂÂÂÂÂÂÂÂval bash_script =
ÂÂÂÂÂÂÂÂÂÂÂÂÂÂ"exec bash " ^
ÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂFile.shell_path script_path ^
ÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂ" > " ^ File.shell_path out_path ^
ÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂ" 2> " ^ File.shell_path err_path;
ÂÂÂÂÂÂÂÂÂÂÂÂval _ = getenv_strict "EXEC_PROCESS";
ÂÂÂÂÂÂÂÂÂÂÂÂval status =
ÂÂÂÂÂÂÂÂÂÂÂÂÂÂOS.Process.system
ÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂÂ("exec \"$EXEC_PROCESS\" " ^ File.shell_path pid_path ^ " " ^ quote bash_script);

in src/Pure/Concurrent/bash.ML.

In my naivety, I would immediately scold such code: Really, one should
not use the system-family of calls that needlessly go via a shell, with
all the worrying quoting involved. But, judging from a very brief web
search (http://sml-family.org/Basis/os-process.html), it seems that SML
does not provide the safe form taking a list of arguments, instead of a
single string, that I have seen in most other languages. Is there
really no way of executing a program from SML that does not go via the
shell?

One way out would be to give up on lib/scripts/getsettings doing the
caching and configure everything upon every invocation. This way,
functions would not have to be exported.

> What is your $SHELL actually?

The $SHELL is /bin/bash, but I donât expect that to make a difference
here.

Greetings,
Joachim
-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.