Bug 2580 - vm_compute does not reduce terms correctly -> assumption-free proof of False
: vm_compute does not reduce terms correctly -> assumption-free proof of False
Status: RESOLVED FIXED
Product: Coq
Classification: Unclassified
Component: VM
: unspecified
: Macintosh Mac OS
: P5 critical
: ---
Assigned To: Benjamin Gregoire
Depends on:
Blocks:
  Show dependency treegraph
 
Reported: 2011-07-26 18:06 CEST by Damien Pous
Modified: 2011-08-01 15:47 CEST (History)
3 users (show)

See Also:


Attachments
file used to produce the bug (4.98 KB, text/plain)
2011-07-26 18:08 CEST, Damien Pous
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Damien Pous 2011-07-26 18:06:17 CEST
There is a bug with vm_compute and values obtained from functors applications: using the attached code, I can produce an assumption-free proof of False, or Bus errors. 

- [coqcheck] detects that the proof is wrong.
- The use of functors seems required to get the bug.
- The behaviour is the same with v8.3 and trunk.

I put "critical" severity because the code is not so contrived (similar problems could certainly arise with the functors from FMap/FSet), and it can be quite disappointing to see ones fully certified decision procedure returning wrong results...

Best,
Damien Pous
Comment 1 Damien Pous 2011-07-26 18:08:30 CEST
Created attachment 268 [details]
file used to produce the bug
Comment 2 Pierre Boutillier 2011-07-27 09:41:56 CEST
If Benjamin isn't able to see the problem, maybe Bruno will be.
Comment 3 Thomas Braibant 2011-07-27 16:40:21 CEST
Incidentally, this bug does not hold in Coq 8.2 -r 12142. So maybe this also has to deal with the changes in the module system between 8.2 and 8.3 ...
Comment 4 Bruno Barras 2011-07-29 21:04:57 CEST
Reduced example:

Set Implicit Arguments.
Module Type MAP.
 Parameter find: bool.
 Parameter add: nat.
End MAP.
Declare Module M : MAP.
Module F(H: MAP) <: MAP.
  Parameter find : bool.
  Definition add := if H.find then 0 else S H.add.
End F.
Module Make (D:MAP). (* dummy functor arg *)
 Module M1 := F M.
 Module M2 := F M1.
 (* commenting this command makes the bug disappear! *)
 (* --> A side-effect of vm_compute is causing the problem
        (propagation of module substitutions ?) *)
 Eval vm_compute in M2.add. (* OK *)
End Make.
Module Import B := Make M.
(* uncommenting this command makes the bug disappear! *)
(*Eval vm_compute in M1.add.*)

Eval vm_compute in M2.add. (* --> wrong! M1.find is replaced by M.find *)
Comment 5 Bruno Barras 2011-08-01 15:47:21 CEST
Fixed (quickly) by copying the bytecodes *before* patching them. (trunk and v8.3)

Problem was: when evaluating M2.add (referring to M1.find and M1.add),
reference to M1.find is written in the code, then M1.add has to be written, but if it has not been evaluated yet, the code of add is patched, M.find and M.add are overwrite the previous values. Code is executed, producing the value for M1.add. But then, the code of add is evaluated (for the value of M2.add) with find<-M.find and add<-M1.add, hence the wrong result.

By copying the code before, the 2 invocations (and the corresponding patches) of add occur on different pieces of code.
 
Note:
- this does not happen within the functor by accident because patches are reversed by functor closure. So, within the functor find is patched after add, find is not overwritten, and after the closure, find is patched first, and the overwriting produces the bug. This should be the reason the bug appeared with the commit about modules.
- code is copied before patching it (this fix), but it is also copied (and somewhat checked for consistency) after patching it. The second copy could be avoided. I let Benjamin see what to do about this minor problem.