multiple anomalies in coqchk on CompCert

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3026
From: @xavierleroy
Reported version: 8.4
CC: @barras, @pirbo, @letouzey

Depends on: BZ#2588, BZ#2933
See also: BZ#3243

[coqbot]

Comment author: @xavierleroy

I have been trying for several years to run "coqchk" on CompCert, for additional confidence. Below is the current status of my experiments, using the latest Coq release (8.4pl2) and the latest CompCert release (1.13). There are still multiple "anomalies" and several definitions where coqchk just loops or takes forever.

The existence of coqchk is an argument in favor of Coq for people who really care about high-assurance software. I would therefore very much appreciate that you make it work properly.

How to reproduce:

wget http://compcert.inria.fr/release/compcert-1.13.tgz
tar xzf compcert-1.13.tgz
cd compcert-1.13
./configure ia32-linux
make -j proof

Edit the "check-proof:" entry at end of ./Makefile to add or remove -admit options as described below. Then run "make check-proof".

1- Without any "-admit": loops or takes forever on
checking cst: Integers.Int.Z_mod_modulus_range

2- With "-admit Integers": loops or takes forever on
checking cst: Floats.Float.double_of_bits_of_double

3- With "-admit Integers -admit Floats": fails on
checking ind: AST.external_function
Failure: impredicative Type inductive type. Please report.

4- With "-admit Integers -admit Floats -admit AST": fails on
checking ind: Asm.instruction
Failure: impredicative Type inductive type. Please report.

5- With "-admit Integers -admit Floats -admit AST -admit Asm": fails on
checking ind: Mach.instruction
Failure: impredicative Type inductive type. Please report.
Note that I reported this exact 2nd bug years ago (#2588).

6- With "-admit Integers -admit Floats -admit AST -admit Asm -admit Mach": fails on
checking cst: UnionFind.UF.elt
Anomaly: Uncaught exception Reduction.NotConvertible. Please report.

7- With "-admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind": success! at last!

[coqbot]

Comment author: @letouzey

Hi Xavier

I've started looking at these issues

1. Integers:
   Unlike coqtop, the checker is also validating functor applications after expansion of the module parameters. So with these concrete parameters more reductions might occur, here for instance wordsize becomes convertible to 32%nat for Int, etc etc. I've a patch for giving a low priority during conversion to the expansion of constants coming from module parameter (see attachment), I'll see it this patch is ok with Bruno / Hugo.

2. Floats:
   Not fully investigated yet, but I bet this one comes from the intensive use of vm_compute in this file. Since Coqchk uses compute instead of the vm, this might take ages. As a workaround, it seems that many computations in Floats could be replaced by some rewrites, this might help a bit (?). To be continued...

3,4,5) Cf #2588 indeed (and maybe #2933). I'm no expert in universes, I'll see with Bruno and/or Hugo.

6. UnionFind:
   Another universe issue. There's something wrong with the Type typing elt in
   (UNIONFIND with Definition elt := M.elt). Maybe a missing universe constraint somewhere ? This will also have to be investigated more deeply. Meantime, a possible workaround is to use <: instead of : in the definition of UF.
   Separate issue: why this NotConvertible reach toplevel without being catched and turned into a nicer error message ?

Best,
Pierre L.

[coqbot]

Comment author: @letouzey

Created attachment 400
Patch solving issue 1 : a minimal conv oracle for delaying unfold of module params

Patch for branch 8.4

Attached file: 0001-Checker-conversion-heuristics-to-speed-up-validation.patch (text/plain, 4011 bytes)
Description: Patch solving issue 1 : a minimal conv oracle for delaying unfold of module params

[coqbot]

Comment author: @letouzey

Bruno, what do you think of this patch about conversion ?

[coqbot]

Comment author: @letouzey

Created attachment 401
Patch solving issue 6 : load inner mod constraints in coqchk

Attached file: 0001-Checker-add-some-missing-inner-mod-constraints-part-.patch (text/plain, 1455 bytes)
Description: Patch solving issue 6 : load inner mod constraints in coqchk

[coqbot]

Comment author: @letouzey

Concerning 6) (the NotConvertible in UnionFind), here is a minimal test-case:

Module Type FOO. Parameter t : Type. End FOO.
Module Type BAR. Parameter t : Type. End BAR.

Module M (X : BAR) : FOO with Definition t := X.t.
 Definition t := X.t.
End M.

It seems the universe constraints are simply not loaded by coqchk when inside a functor, see my second patch that appears to solve this... I wonder whether we should also add constraints appearing in module_type_body and in constant_body ?
For constant_body this used to be done but that was stopped by the fix for #1927...

One more time, I'll try to have feedback about this patch before inclusion...

Pierre

[coqbot]

Comment author: @maximedenes

This patch doesn't seem necessary today (constraints carried by fields of a module are included in the ones of the module itself).

The minimal example extracted from UnionFind goes through since 8.4 pl4, probably due to Enrico's fix of #3243.

[coqbot]

Comment author: @Zimmi48

From what I read here https://github.com/AbsInt/CompCert/blob/0b4bcebe701b9cf8756f583768831ad48a7cc79e/Makefile#L280-L285, coqchk still has issues with CompCert. Can this bug be updated to reflect the current limitations?

[ppedrot]

From what I understand from the problems encountered in CompCert, the file compcert.lib.Integers does not compile with the checker because the latter does not implement the Strategy feature of the kernel. Note that @robbertkrebbers has the very same issue in stdpp. Either they rewrite their code in a way that does not exploit strategies, or we implement it in the checker.

[maximedenes]

It is not just that the checker doesn't implement it. It is also that it should do something special when defunctorialization removes opacity (of a parameter).

[ppedrot]

What's the status of this bug report? I know that I fixed the bug due to Integers but I am unaware of the remaining issues.

[ppedrot]

Let me correct myself: the Integer module from CompCert still blows up when evaluated by the checker. The reason is the one mentioned by @letouzey, namely that the checker unfolds the functor application before checking them. A minimal example that kills the checker is the following:

Fixpoint big (n : nat) :=
match n with
| 0 => tt
| S n =>
  match big n with tt =>
    match big n with tt => tt end
  end
end.

Definition big' := big.

Module Type S.
Parameter n : nat.
End S.

Module Make(M : S).

Lemma boom : big M.n = big' M.n.
Proof.
reflexivity.
Qed.

End Make.

Module S32 <: S.
Definition n := 32.
End S32.

Module X := Make(S32).

[xavierleroy]

Right. According to my notes there are two problems remaining:

Integers.Int.Z_mod_modulus_range takes forever to check
SelectDivproof.divs_mul_shift_2 takes forever to check

[maximedenes]

@ppedrot When we discussed this at POPL, we thought about making the checker treat fields opacified by module signatures as Opaque. Now that you ported the oracle to the checker, do you think it would make sense to try it?

[ppedrot]

@maximedenes I had a look at that yesterday, and it is actually way harder to do this properly than I originally thought. For instance there is no way to distinguish the use of a constant as an instance of a functor argument or as a standard global variable, which might result in fancy conversion checks.

[ppedrot]

@SkySkimmer @maximedenes How far are we from solving this bug since the merge of the checker code base?

[SkySkimmer]

I don't understand what the status of the bug is, there seem to be several separate bugs involved (anomalies as the title says but also perf issues from functor unfolding?)

[SkySkimmer]

For instance there is no way to distinguish the use of a constant as an instance of a functor argument or as a standard global variable, which might result in fancy conversion checks.

You mean something like

Definition big := 2.
Module Type T. Parameter x : nat. End T.
Module F(A:T).
Definition one : big = 2 := eq_refl.
Definition two : A.x = A.x := eq_refl.
End F.
Module A. Definition x := big. End A.
Module M := F A. (* when checking M we need to unfold the "big" in "one" but not the one in "two" *)

[ppedrot]

@SkySkimmer indeed.

[vbgl]

There might still be issues with the checker and with tactics, but the original problem motivating this PR is gone. Closing then.

For the record: to make CompCert go through the checker, a few calls to omega have been replaced by lia, and a few calls to f_equal by apply f_equal.