Incomplete behaviour for utilities

[benozol]

This PR brings incomplete behaviour to the utilities. A utility returns now a state and a bool result, where type α result = Ok α | Incomplete, and the possible behaviours are encoded as follows:

• success: Ok true,
• error: Ok false, and
• incomplete: Incomplete.

For the symbolic interpreter, this PR introduces the distinction between error, and incompleteness on the level of utilities (SymbolicUtility.{error,incomplete}) and on the level of specification cases (SymbolicUtility.{success,error,incomplete}_case). The latter ultimatively solves @yurug's problem to differentiate between known behaviour and incomplete behaviour depending on the state of the filesystem.

[benozol]

Before, utiltiies returned a boolean value to indicate success and error, and unsupported utilities generated a colis-level error or raised an ocaml exception, depending on a command line flag.

I would propose to get rid of the command line flag and always generate incomplete behaviour for known utilties and options that we know but don't implement (if not resolutely implemented as approximation) and generate an error for unknown, and possibly non-existing utiltiies and option. Do we have a complete list of known utilities (POSIX and standard installation)?

@Niols @claudemarche @treinen, what do you think?

[benozol]

Ping @Niols : What do you think of this PR; is clarifying incomplete utilities worth the modifications? In that case I would prefer to finalise this before attacking #116

[Niols]

I think the distinction @yurug wants is between things that we know exist but decided not to handle and things we don't know exist (or not). Say we encounter

mycmd --weird-option

Currently (before this PR), we do not make the difference between an unknown option, a known option that we decided not to support because of limits of our tool and a known option we decided not to support because of the Debian policy.

We do however – via the flag – propose two different ways of handling these weird options:

• either how the shell would handle an unknown option, by returning 1 (and writing on errout, which we don't modelise),
• or how we would (possibly) want an analysing tool to behave, by raising an exception.

The introduction of the incomplete behaviour is a good thing in my opinion as it allows to avoid raising exceptions. I think however both an unknown option (for which we don't actually know whether it's an error in the script or in our tool) and an option we decided not to handle (for which we know it's us). should be flagged as a source of incompleteness.

We can then continue to explore more traces, right? But then are you planning to handle them as "anything could happen", or to just pass them along (and basically stop the trace when we reach incompleteness)?

The incompleteness could also carry an extra information relating the reason of incompleteness (mainly, for Debian, I'd say unknown option, limit of our tool, POSIX Standard or Debian Policy).

I will try to read the source code shortly.

[benozol]

1. This PR now provides a nice place to specify the known unknown utilities as incomplete:

colis-language/src/symbolic/symbolicUtility.ml

Lines 240 to 243 in 315751f

	let table =
	let table = Hashtbl.create 10 in
	(* TODO Register all POSIX utilities as: incomplete ~descr:(name^": not implemented") *)
	table

2. Unknown unknowns still generate a colis-level error (i.e., normal behaviour with result 1, just as an unknown command in a shell):

colis-language/src/symbolic/symbolicUtility.ml

Lines 250 to 253 in 315751f

	let dispatch ~name =
	try Hashtbl.find table name
	with Not_found -> fun _ ->
	error ~msg:(name^": command not found") ()

3. @Niols do you still see the necessity for Options.fail_on_unknown_utilities?

[Niols]

Hum,

So we consider that the list we will provide in your 1. will cover all the utilities "allowed to be used" so that 2. makes sense? I am not so sure here, I think (and in particular in Debian) that we should never reach an unknown command (without having previously checked, which makes me think we could carry around a list of commands we know exist and that would allow to sort of specify which and command -v).

So in my opinion, this should always be incomplete. But maybe, if we carry different flags, incomplete because unknown, which is different from being incomplete because known to not be specified.

I think that 3. is indeed not needed anymore if computation continues with an incomplete trace.

[benozol]

consider that the list we will provide in your 1. will cover all the utilities "allowed to be used"

Exactly (and independently from the fact that they may be specified later)

that we should never reach an unknown command

So what about always raising an exception in this case of unknown unknown utilities (when the dispatch cannot find anything)?

This would tell us that either we either have to add a command to the list of unsupported utilities (under 1), or the script refers to an unknown command.

[Niols]

OK for the exception, it makes a lot of sense. For "completeness" of the tool I'd probably argue that we can keep an option that switches from one behaviour (exception) to the other (normal false), maybe defaulting to exception. But I don't have strong feelings about this.