LLVMParseError on LLVM 14.0.0

[computablee]

I was trying out some Copilot-Verifier stuff and encountered the following exception when I tried to run the heater example:

Build profile: -w ghc-8.8.4 -O1
In order, the following will be built (use -v for more details):
 - Copilot-Tester-0.0 (exe:Heater) (file Heater.hs changed)
Preprocessing executable 'Heater' for Copilot-Tester-0.0..
Building executable 'Heater' for Copilot-Tester-0.0..
[1 of 1] Compiling Main             ( Heater.hs, [snip]/Copilot-Tester-0.0/x/Heater/build/Heater/Heater-tmp/Main.o )

Heater.hs:18:49: warning: [-Wtype-defaults]
    • Defaulting the following constraints to type ‘Integer’
        (Integral a0)
          arising from a use of ‘fromIntegral’ at Heater.hs:18:49-62
        (Num a0) arising from the literal ‘5’ at Heater.hs:18:62
    • In the second argument of ‘(/)’, namely ‘fromIntegral 5’
      In the expression:
        (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
      In an equation for ‘avgTemp’:
          avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
   |
18 | avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
   |                                                 ^^^^^^^^^^^^^^
Linking [snip]/Copilot-Tester-0.0/x/Heater/build/Heater/Heater ...
[copilot-verifier] Generated "results/heater/heater.c"
[copilot-verifier] Compiled heater into results/heater/crux~heater.bc
Heater: LLVMParseError (Error {errContext = ["METADATA_GLOBAL_VAR","METADATA_BLOCK","METADATA_BLOCK_ID","value symbol table","MODULE_BLOCK","Bitstream"], errMessage = "Invalid record size: 13\nExpected one of: [11,12]\nAre you sure you're using a supported version of LLVM/Clang?\nCheck here: https://github.com/GaloisInc/llvm-pretty-bc-parser\n"})

Here's the software versions I'm running:

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.8.4

$ cabal --version
cabal-install version 3.0.0.0
compiled using version 3.0.1.0 of the Cabal library 

$ llvm-link --version
Ubuntu LLVM version 14.0.0
  
  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: skylake

$ clang --version
Ubuntu clang version 14.0.0-1ubuntu1.1
Target: x86_64-pc-linux-gnu
Thread model: posix
InstalledDir: /usr/bin

And here is the source code:

module Main where

{-# LANGUAGE RebindableSyntax #-}

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier

import qualified Prelude as P ()

temp :: Stream Word8
temp = extern "temperature" Nothing

ctemp :: Stream Float
ctemp = (unsafeCast temp) * constant (150.0 / 255.0) - constant 50.0

avgTemp :: Stream Float
avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5

spec :: Spec
spec = do
  trigger "heaton"  (avgTemp < constant 18.0) [arg avgTemp]
  trigger "heatoff" (avgTemp > constant 21.0) [arg avgTemp]

main :: IO ()
main = do
  spec' <- reify spec
  compile "heater" spec'
  verify mkDefaultCSettings [] "heater" spec'

Clang 14 appears to pass randomized tests, according to this repository's README. Downgrading to Clang/LLVM 11.1.0 solves the problem:

Resolving dependencies...
Build profile: -w ghc-8.8.4 -O1
In order, the following will be built (use -v for more details):
 - Copilot-Tester-0.0 (exe:Heater) (first run)
Configuring executable 'Heater' for Copilot-Tester-0.0..
Preprocessing executable 'Heater' for Copilot-Tester-0.0..
Building executable 'Heater' for Copilot-Tester-0.0..
[1 of 1] Compiling Main             ( Heater.hs, [snip]/Copilot-Tester-0.0/x/Heater/build/Heater/Heater-tmp/Main.o )

Heater.hs:18:49: warning: [-Wtype-defaults]
    • Defaulting the following constraints to type ‘Integer’
        (Integral a0)
          arising from a use of ‘fromIntegral’ at Heater.hs:18:49-62
        (Num a0) arising from the literal ‘5’ at Heater.hs:18:62
    • In the second argument of ‘(/)’, namely ‘fromIntegral 5’
      In the expression:
        (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
      In an equation for ‘avgTemp’:
          avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
   |
18 | avgTemp = (sum 5 (replicate 5 19.5 ++ ctemp)) / fromIntegral 5
   |                                                 ^^^^^^^^^^^^^^
Linking [snip]/Copilot-Tester-0.0/x/Heater/build/Heater/Heater ...
[copilot-verifier] Generated "results/heater/heater.c"
[copilot-verifier] Compiled heater into results/heater/crux~heater.bc
[copilot-verifier] Translated bitcode into Crucible
[copilot-verifier] Generating proof state data
[copilot-verifier] Computing initial state verification conditions
[copilot-verifier] Proving initial state verification conditions
[copilot-verifier] Proved 5 of 5 total goals
[copilot-verifier] Computing step bisimulation verification conditions
[copilot-verifier] Proving step bisimulation verification conditions
[copilot-verifier] Proved 44 of 44 total goals

I am running on Linux Mint 21.2, if that helps. Thank you!

[RyanGlScott]

Thanks for the bug report!

This is a known issue involving llvm-pretty-bc-parser's interaction with LLVM 14—see GaloisInc/llvm-pretty-bc-parser#188. This has been fixed in the master branch of llvm-pretty-bc-parser, but I have not yet had the time to update the llvm-pretty-bc-parser submodule commit used in copilot-verifier. As such, this is really more of a copilot-verifier issue than a llvm-pretty-bc-parser one. As such, I'll transfer this issue over to the copilot-verifier repo.

In the meantime, a workaround is to use Clang 12 or earlier, whose LLVM bitcode formats are supported by copilot-verifier.

[computablee]

Thank you so much for the quick response! Good to know that it's already been fixed. In the meantime I'll keep using LLVM 11 until I hear an update.

[RyanGlScott]

I've pushed a change in #41 that should allow copilot-verifier to work with LLVM versions up to 16. Let me know if you encounter any additional issues.