Suggestion: Val.of_bool and partial evaluation

[roconnor-blockstream]

If Val.of_bool b were redefined as Vint (if b then Int.one else Int.zero) or even better Vint (Int.repr (Z.b2z b)), then more partial evaluation could proceed because the constructor Vint is exposed.

I think this would be particularly helpful because (at least for me) Val.of_bool ends up occuring inside force_val (both_int or similar such expressions when it appears, which can reduce away as long as Val.of_bool can be reduced to a Vint.

[andrew-appel]

Interesting. I can't literally change the definition of Val.of_bool, because Val is actually compcert.common.Values.Val.of_bool, and I can't change things inside CompCert.

And I can't simply replace using Val.of_bool with some better definition of my choosing, because some of those uses may come directly from the CompCert Clight semantics.

But what might be possible is to replace all the places where VST introduces an of_bool that did not come directly from CompCert, with the better definition. Perhaps worth an experiment.

[roconnor-blockstream]

Ah, I didn't realize that Val was part of Compcert.

[andrew-appel]

I have now implemented the thing I described above in my previous comment. You can find it in P.R. #661. In connection with this, I also improved the efficiency of the do_repr_inj tactic that is used by forward_if (and similar tactics) to clean up conditionals in the then- and else-branch.

Because (in some cases) conditionals are cleaned up better than they were before, some user proofs may need to be modified. You can see examples here (in files other than in floyd/ and veric/ ). Is it worth merging this improvement, given the incompatibility?

[roconnor-blockstream]

One option is to wait a few weeks and see of the AbsInt folks are interested in the change before deciding anything.

[andrew-appel]

That is not the difficulty. It doesn't matter that much whether CompCert uses Val.of_bool in its own Clight2 semantics, because it was not hard to adapt the Verifiable C proof rules to use a different (but provably equivalent) definition, and prove it sound. The only difficult is that it causes incompatibilities, in rare but real cases, that VST users will have to adapt to, if I merge the PR.

[roconnor-blockstream]

If AbsInt were to change its definition of Val.of_bool, then VST and VST users would both need to adapt their codebases to such a change.

[andrew-appel]

Well, yes, but that's not my point. In the PR, I have already done 90% of the work of adapting to that change. The question of whether we should ask VST users to adapt to this change is completely independent of whether AbsInt decides to change. That's what my PR demonstrates. So we are back to the pros and cons:

• pro: Your suggested "bool2val" is, indeed, more elegant, and leads to (a) more efficient VST processing of the usual cases, and (b) in the corner cases where the user has to deal with it, a more tractable hypothesis (for exactly the reasons you explained in your original issue report).
• con: Some existing VST proofs will have to be modified at the next VST release.

[lennartberinger]

If the changes are not too burdensome (and perhaps they are not, the effects should be rather local) I guess the "con" isn't too bad - and we've occasionally asked users to adjust their proofs anyway as VST (or CompCert/Coq underneath) evolves.

[roconnor-blockstream]

From my perspective this is similar to PR #242, where partial evaluation was unlocked for reptype in a similar way (by commuting match expressions inside branches to expose an existsT constructor). That PR likely also required user to modify some existing VST proofs.

[andrew-appel]

Right. So, once I get my PR fully debugged, I'll go ahead and merge it.