Functorize symbolic engine, mixed case specs, and document basic symbolic utilities

[benozol]

Before #114 there was some confusion about the use of failure vs error in the implementation of symbolic utilities. This PR fixes the distinction between the different behaviours from #114 and clarifies the documentation as follows:

colis-language/src/symbolic/symbolicUtility.mli

Lines 79 to 87 in f335dc0

	utility behaviour:
	├─ [known]
	│  ├─ [ok] the call to the utility was executed (known known)
	│  │  ├─ [success] the call was valid and succeeded (i.e. exit 0)
	│  │  └─ [error] the call failed (i.e. exit >0)
	│  └─ [incomplete] the call is valid but the behaviour has not
	| (yet) been implemented (known unknown)
	└─ [unknown] we don't even know if this call is an error or
	incomplete behaviour (unknown unknown)

[Niols]

I appreciate the modification and think all this is going in a nice direction. As far as I am concerned, you can merge this PR.

[benozol]

@treinen could you please have a look at my modifications to "your" utilities since before the introduction of incompleteness to symbolic utilities. Here is a comparison: 64a40fd...f335dc0

I am specifically wondering about the previous cases of unsupported in dpkg.ml. unsupported previously conflated incomplete utilities and options with unknown utilities and options, which are now differentiated as follows:

colis-language/src/symbolic/symbolicUtility.mli

Lines 79 to 87 in f335dc0

	utility behaviour:
	├─ [known]
	│  ├─ [ok] the call to the utility was executed (known known)
	│  │  ├─ [success] the call was valid and succeeded (i.e. exit 0)
	│  │  └─ [error] the call failed (i.e. exit >0)
	│  └─ [incomplete] the call is valid but the behaviour has not
	| (yet) been implemented (known unknown)
	└─ [unknown] we don't even know if this call is an error or
	incomplete behaviour (unknown unknown)

[benozol]

Still more specifically I am wondering about:

colis-language/src/symbolic/utilities/dpkg.ml

Lines 25 to 28 in f335dc0

	| ["--compare-versions"; _v1; _v2] ->
	incomplete ~utility "support for --compare-versions not yet implemented"
	| "--compare-versions" :: _ ->
	error ~utility "option --compare-versions expects exactly two arguments"

where man dpkg specifies --compare-versions ver1 op ver2. Should the implementation be as follows?

 | ["--compare-versions"; _v1; _op; _v2] -> 
   incomplete ~utility "support for --compare-versions not yet implemented" 
 | "--compare-versions" :: _ -> 
   error ~utility "option --compare-versions expects exactly three arguments" 

[treinen]

Yes you are right @benozol, dpkg --compare-versions expects 3 arguments.

[treinen]

Yes you are right @benozol, dpkg --compare-versions expects 3 arguments.

[benozol]

Ok merci ! I have corrected dpkg

@Niols could you run again ginette?

[Niols]

For some reason, it seems that I cannot comment with links? But it is on its way.

[Niols]

http://ginette.informatique.univ-paris-diderot.fr/~niols/colis-batch/2020-02-27_16-07-03_acb30bf_fix-differentiate-symbolic-utilities/

[Niols]

Also, I have noticed that colis-anr/colis-batch@9985dd5 on b2175ee (that is the run whose link I just sent) runs significantly faster than colis-anr/colis-batch@09657ae (master) on 43429b1 (shadow-aware-printing) or d129924 (where this PR and shadow-aware-printing diverge). I am talking about something like 10 times faster.

Is there anything you did after d129924 that would explain such a speedup? Any idea? I didn't see any commit message that would explain this.

[Niols]

There are weird things like this but I think this is linked to #121.

[Niols]

I am talking about something like 10 times faster.

Actually, 18 times faster.

[Niols]

I think it has to do with your sentence that said in my mind: that you were considering unknown commands as errors? This creates a loooot of false positives in Ginette. I guess then you changed back to propagating incompletenesses without seeing them as errors? Is that true? In which commit would that have happened?

[benozol]

Uh that's strange indeed, no optimization was intended with this PR.

There are weird things like this

In 719f6f7 (and ddd4f64) I translated the old unsupported into error and unknown, mostly according to the message strings. I might have done things wrong there, in the case you refer to ([ERROR] dpkg-maintscript-helper rm_conffile: maintainer script arguments are missing), I am not sure if this should be incomplete or error. That was also the reason of my request for review in #125 (comment) :)

I think it has to do with your sentence that said in my mind: that you were considering unknown commands as errors?

No this behaviour didn't change – unknown commands still raise exceptions (with Options.unknown_behaviour = Exception as in colis-batch):

colis-language/src/symbolic/symbolicUtility.ml

Lines 97 to 102 in b2175ee

	let dispatch ~name =
	try Hashtbl.find table name
	with Not_found ->
	fun _ctx sta ->
	(* All known utilities should have incomplete behaviour as default *)
	unknown ~utility:name "command not found" sta

However, I suggested to register all POSIX (and Debian) utilities as incomplete by default (and known wrong commands as error, if any) to avoid false alarms.

BTW can we get a list of reasons for Errors.Unknown_behaviour (arguments to the exception) from colis-batch? That would tell us where what we have to add.

---

From the batch runs available at http://ginette.informatique.univ-paris-diderot.fr/~niols/colis-batch/ the outlier seems to me shadow-aware-printing with >10000 seconds, whereas all other runs were between 600s and 700s, even 2019-10-23_00-00-00_f80954d_TACAS ran only 1128s. Where are the other examples of long runtime?

[Niols]

Uh that's strange indeed, no optimization was intended with this PR.

If I had to guess, I would say your modifications first introduced a lot of new traces (that would explain the slow down) and then fixed it. And I happened to take a commit in the middle to branch and create shadow-aware-printing.

There are weird things like this

I am not sure if this should be incomplete or error. That was also the reason of my request for review in #125 (comment) :)

So, I am not so sure about the taxonomy anymore. What you call "error" is a known ok error, right? What do you do with all those things? Am I right to say the following? (Probably not.)

Utility behaviour	Engine behaviour
known ok success	run normally as success
known ok error	run normally as error
known incomplete	run normally as error, or raise exception depending on flag
unknown	raise exception depending on flag

Now don't get me wrong, I'm happy that we easily see this "weird thing". Here, it comes from a bug in our tool, but we still detect bugs, and would have detected a bad usage of dpkg. But I think we're mostly lucky, because the execution kept running normally but ended up in a non-acceptable dpkg state, and that's how I saw it. Had the dpkg call been in a test, we might very well have missed it.

Note that I might be totally wrong in what I am saying. But I'm trying to be as exact as possible in what I think happened so that you can correct what I haven't understood.

BTW can we get a list of reasons for Errors.Unknown_behaviour (arguments to the exception) from colis-batch? That would tell us where what we have to add.

That has been on my todo list for a while and is near the top. Just after something that requires me to have a fast run of Ginette before all your modifications but with the shadow-aware printing. Hence why I'm very interested in the following:

From the batch runs available at http://ginette.informatique.univ-paris-diderot.fr/~niols/colis-batch/ the outlier seems to me shadow-aware-printing with >10000 seconds, whereas all other runs were between 600s and 700s, even 2019-10-23_00-00-00_f80954d_TACAS ran only 1128s. Where are the other examples of long runtime?

This also happens with d129924, but I've never let the tool run completely because it's so long. I've just started a new run and it should end in a few hours. The result should be here.

By the way, @treinen, do you think it would make sense to add a redirection of the kind http://colis.irif.fr/batch/<url> into http://ginette.informatique.univ-paris-diderot.fr/~niols/colis-batch/<url> (or even a reverse proxy)? I would say it'd allow for much cleaner URIs and would allow us to move runs from Ginette to somewhere else if we want to.

[benozol]

Am I right to say the following? [...]

success corresponds to exit 0 and error corresponds to exit >0, that's easy.

incomplete refers to incompleteness of the symbolic utilities or the symbolic engine (loop limits or stack limits), which introduces incompleteness states in the symbolic execution. This allows for tracing back which initial states yield to semantics that is not covered by the symbolic engine.

unknown raises an OCaml exception, generated incomplete or error depending on the flag.

Maybe I should put more info in the documentation here:

colis-language/src/symbolic/symbolicUtility.mli

Lines 79 to 87 in f335dc0

	utility behaviour:
	├─ [known]
	│  ├─ [ok] the call to the utility was executed (known known)
	│  │  ├─ [success] the call was valid and succeeded (i.e. exit 0)
	│  │  └─ [error] the call failed (i.e. exit >0)
	│  └─ [incomplete] the call is valid but the behaviour has not
	| (yet) been implemented (known unknown)
	└─ [unknown] we don't even know if this call is an error or
	incomplete behaviour (unknown unknown)

This also happens with d129924

Yes dispatch created errors in d129924 (since 90b4969) but is corrected since 57367ab

colis-language/src/symbolic/symbolicUtility.ml

Lines 250 to 254 in d129924

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

So it seems that you branched shadow-aware-printing at the wrong moment :(

[Niols]

Am I right to say the following? [...]

success corresponds to exit 0 and error corresponds to exit >0, that's easy.

incomplete refers to incompleteness of the symbolic utilities or the symbolic engine (loop limits or stack limits), which introduces incompleteness states in the symbolic execution. This allows for tracing back which initial states yield to semantics that is not covered by the symbolic engine.

unknown raises an OCaml exception, generated incomplete or error depending on the flag.

So I guess my question is then: what happens to incomplete states in the semantics? Do we simply stop their execution?

So it seems that you branched shadow-aware-printing at the wrong moment :(

OK indeed. I have tried going to a much earlier commit and cherry pick my commits. This is now in the branch shadow-aware-printing-fixed and in PR #131. No need to merge it right away though. And again (as asked in the PR), I think this is all very independent from your changes as it only touches the constraints.

[benozol]

So I guess my question is then: what happens to incomplete states in the semantics? Do we simply stop their execution?

Incomplete behaviour is modelled in the concrete semantics, and yes, it stop further evaluation on that execution path. But – in advantage to using unknown with exception behaviour – incomplete execution paths are tracked and other execution paths are further evaluated.

[benozol]

@Niols did you run batch since b2175ee, or could you please do so? I would like to compare again the results with those from master before all those changes (~ 64a40fd, that seems to be in the batch archive). If you have time to have another look on it – your comments would also be very welcome before finally merging this PR

[Niols]

I just did, for b2175ee.

[Niols]

And here if the one for 64a40fd, indeed taken out of the archives.

[Niols]

Very similar numbers in the summary. And the few package reports I peeked on seem fine, except that they are hardly usable, but that's what's being fixed in #131.

[benozol]

Many thanks.

Do you think its better to wait for #131 to compare the results?

[Niols]

#131 is ready. And I think that the changes are independent, so we could probably merge one in the other. But no, I think it is safe to merge this one first into master.

[benozol]

The reports look ok to me – any last words for this PR @Niols ?

[Niols]

Nope, let's merge this. Be my guest!