Duplicate entries in executables file lead to undefined behavior

[andreasabel]

Discovered when looking at #5070. Ping @wenkokke.
Agda accepts silently executables with the same basename:

E.g. I can write this into .agda/executables:

/bin/echo
/Users/abel/foetus/sml/echo

(The second command does not echo, but crashes if called on the command line.)

This makes the example from the docs fail:

{-# OPTIONS --allow-exec #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Reflection.External
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Unit

_>>=_ = bindTC

macro
  echo : List String → Term → TC ⊤
  echo args hole = do
    (exitCode , (stdOut , stdErr)) ← execTC "echo" args ""
    unify hole (lit (string stdOut))

_ : echo ("hello" ∷ "world" ∷ []) ≡ "hello world\n"
_ = refl

Error:

"" != "hello world\n" of type String
when checking that the expression refl has type
"" ≡ "hello world\n"

It succeeds if I swap the entries in the executables file.
This behaviour can be explained by a use Map.fromList, which takes the last of the duplicate entries and throws the others away silently. (You have been warned by @gallais!)

agda/src/full/Agda/Interaction/Library.hs

Lines 387 to 388 in 6c56133

	parseExecutablesFile ef files =
	fmap (Map.fromList . catMaybes) . forM files $ \(ln, fp) -> do

This is a potential security problem!

Also, Agda swallows the OS error thrown by the second executable and simply returns the empty string. That's DOS/Windows-style error swallowing, not good...

Agda should report:

• conflicting entries in executables
• errors (or at least exitcodes) thrown by run executables.

[wenkokke]

Aiii, that shouldn’t be happening! I’ll draft a fix sometime next week!

[andreasabel]

I’ll draft a fix sometime next week!

Such "famous last words" abound on github... 😆

@wenkokke : A simple fix would be fine at this point, without tackling #5553.

[wenkokke]

@andreasabel: My apologies, I am still unable to type due to my wrist injury. Have been since May.

[andreasabel]

@andreasabel: My apologies, I am still unable to type due to my wrist injury. Have been since May.

@wenkokke : Ah, did not know, sorry to hear.

Thanks for the quick feedback. I unassign you so that others can jump in. I wish a good recovery!