search

stedolan / malfunction

Malfunctional Programming
Other
336 stars 19 forks source link

Miscompilation under 4.14+flambda #36

Closed yforster closed 10 months ago

yforster commented 11 months ago

The spec asks to file a report If a program runs to completion in the interpreter producing a result, it is a bug in Malfunction if the compiled version of the same program either crashes or produces a different value

I have such a situation: a program (obtained through extraction from Coq):

compare : bytestring -> bytestring -> comparison

with string from https://github.com/MetaCoq/metacoq/blob/coq-8.16/utils/theories/bytestring.v#L32 and type comparison = Eq | Lt | Gt.

Running compare "" "diff" correctly yields 1 (corresponding to Lt) in the interpreter. The compiled program yields

inspecting the actual value using Obj tools shows that the return value is not really 2 (Gt), but the full string "diff".

See https://github.com/yforster/malfunction-malfunctioning/actions/runs/6533871602/job/17739907316

The error can alternatively be circumvented by disabling optimisation passes in malfunction cmx (the linked repository uses a patched version where optimisation has to be explicitly enabled via malfunction cmx -O2).

stedolan commented 10 months ago

Thanks for reporting this! This is absolutely a bug. I've just pushed a fix with an explanation in the commit message - the short version is that the Lifthenelse constructor of Lambda in 4.14 has stricter requirements of its input than 4.13 does. Malfunction copied an optimisation from OCaml but its copy wasn't updated to meet the stricter requirements, causing miscompilation in weird cases.