25 verifier tests fails with 'instruction code 62 is unknown'

[yaitskov]

Hi,

I tried to build copilot (tag 4.6) and noticed an issue with failing tests of verifier package.

I suspect llvm is misconfigured (so many tests fail in the same way) but changing llvm version does not make difference (tested with llvms of 16, 20 and 21).

buildPhase completed in 41 seconds
Running phase: checkPhase
Running 1 test suites...
Test suite copilot-verifier-test: RUNNING...
copilot-verifier-examples tests
should-fail tests
AbsIntMin-fail: FAIL (expected)FAIL (expected)FAIL (expected) (0.10s)
Exception: instruction code 62 is unknown
from:
@step
FUNCTION_BLOCK
FUNCTION_BLOCK_ID
value symbol table
MODULE_BLOCK
Bitstream
(expected failure)
MulSignedWrap-fail: FAIL (expected)FAIL (expected)FAIL (expected)FAIL (expected) (0.09s)
Exception: instruction code 62 is unknown
from:
@step
FUNCTION_BLOCK
FUNCTION_BLOCK_ID
value symbol table
MODULE_BLOCK
Bitstream
(expected failure)
should-pass tests
AbsIntMin-pass: FAIL
Exception: instruction code 62 is unknown
from:
@step
FUNCTION_BLOCK
FUNCTION_BLOCK_ID
value symbol table
MODULE_BLOCK
Bitstream

  Use -p '/AbsIntMin-pass/' to rerun this test only.
AddSignedWrap-pass:    FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/AddSignedWrap-pass/' to rerun this test only.
Arith:                 FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/Arith/' to rerun this test only.
Array:                 FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '$0=="copilot-verifier-examples tests.should-pass tests.Array"' to rerun this test only.
ArrayGen:              FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/ArrayGen/' to rerun this test only.
ArrayOfStructs:        FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/ArrayOfStructs/' to rerun this test only.
ArrayTriggerArgument:  FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/ArrayTriggerArgument/' to rerun this test only.
Clock:                 FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/Clock/' to rerun this test only.
Counter:               FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/Counter/' to rerun this test only.
DivByZero-pass:        FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/DivByZero-pass/' to rerun this test only.
Engine:                FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/Engine/' to rerun this test only.
FPNegation:            FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/FPNegation/' to rerun this test only.
FPOps:                 FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/FPOps/' to rerun this test only.
Heater:                FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/Heater/' to rerun this test only.
IndexOutOfBounds-pass: FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/IndexOutOfBounds-pass/' to rerun this test only.
IntOps:                FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/IntOps/' to rerun this test only.
ModByZero-pass:        FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/ModByZero-pass/' to rerun this test only.
MulSignedWrap-pass:    FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/MulSignedWrap-pass/' to rerun this test only.
ShiftLTooLarge-pass:   FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/ShiftLTooLarge-pass/' to rerun this test only.
ShiftRTooLarge-pass:   FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/ShiftRTooLarge-pass/' to rerun this test only.
Structs:               FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/should-pass tests.Structs/' to rerun this test only.
SubSignedWrap-pass:    FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/SubSignedWrap-pass/' to rerun this test only.
UpdateArray:           FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/UpdateArray/' to rerun this test only.
UpdateStruct:          FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/UpdateStruct/' to rerun this test only.
Voting:                FAIL
  Exception: instruction code 62 is unknown
  from:
    @step
    FUNCTION_BLOCK
    FUNCTION_BLOCK_ID
    value symbol table
    MODULE_BLOCK
    Bitstream

  Use -p '/Voting/' to rerun this test only.
WCV:                   OK (0.17s)

25 out of 35 tests failed (5.11s)
Test suite copilot-verifier-test: FAIL
Test suite logged to: dist/test/copilot-verifier-4.6-copilot-verifier-test.log
0 of 1 test suites (0 of 1 test cases) passed.

[RyanGlScott]

I don't think this is a bug on your end, but rather a limitation in the LLVM bitcode parser that copilot-verifier is using. Specifically, this is an issue involving recent versions of LLVM, as documented in GaloisInc/llvm-pretty-bc-parser#277. We have fixed this issue upstream, but this has not yet appeared in a Hackage release.

In the meantime, you can work around the issue by using an older version of LLVM (e.g., 14).

[yaitskov]

Failing test can be reproduced at #686

[RyanGlScott]

Huh, that is interesting. If I'm reading #686 correctly, you are using Clang/LLVM 16? I am unable to reproduce this test failure locally when I use those Clang/LLVM versions. (I wonder if the Nix version of Clang is somehow passing different sets of flags to Clang by default...)

[RyanGlScott]

As an experiment, could I have you perform the following with your Nix version of Clang?

$ echo 'int main(void) { return 0; }' > test.c
$ NIX_DEBUG=1 clang test.c

My suspicion is that Nix's version of Clang is passing a flag like fno-strict-overflow or -fwrapv by default, which would omit the signed integer overflow check that is crucible for the SubSignedWrap-fail test case to work. (I suspect that this may be happening based on the NIX_DEBUG-related output seen in this blog post.)

[yaitskov]

Thanks. Active wrapv flag was failing the test.

[RyanGlScott]

I see, thank you for confirming!

It's a bit unfortunate that Nix's version of Clang passes semantics-changing flags like -fwrapv by default. That being said, it would be nice if we could make the copilot-verifier tests work with all versions of Clang out of the box. Perhaps one way to do so would be to modify copilot-verifier such that when it invokes a Clang subprocess, it also passes -fstrict-overflow -fno-wrapv to be absolutely sure that signed integer overflow checking happens by default, even if the compiler itself would normally assume otherwise.