search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
438 stars 63 forks source link

indicate in the tutorial exactly which major LLVM versions and JVM bytecode versions are supported #903

Open kiniry opened 3 years ago

kiniry commented 3 years ago

E.g., I'm using macOS's built-in LLVM (Apple clang version 12.0.0 (clang-1200.0.32.27)) and SAW is unable to parse the bitcode. Installing llvm@7 from brew (clang version 7.1.0 (tags/RELEASE_710/final)) also results in a 

saw ffs_llvm.saw 
Loading module Cryptol
Loading file "ffs_llvm.saw"
Extracting reference term: ffs_ref
saw: user error (Bitcode parsing of ffs.bc failed:
match failed)
robdockins commented 3 years ago

Agreed that we should document the working versions.

However, I'm surprised that LLVM 7 doesn't work; that is one I expect to work; in fact, it's the version I have on my machine. Are you sure you're calling the clang version that you expect?

kiniry commented 3 years ago

I had an archived version of SAW to preserve an old project. Indeed, LLVM 7 does work.

I have updated the description to reflect my further testing, and to indicate we should do the same for JVM bytecode versions. That info is indeed buried in the SAW manual, but it'd be nice to ensure that first-time readers of the tutorial are not stymied by versioning problems early.

aogrcs commented 3 years ago

I get clang 9.0.0 and saw 7.0, but they do not work: /Users/wenlongxie/Downloads/examples/intro/swap_cryptol.saw" [06:58:42.025] Stack trace: "llvm_load_module" (/Users/wenlongxie/Downloads/examples/intro/swap_cryptol.saw:1:6-1:22): Invalid record size: 22 Expected size between 14 and 19 Are you sure you're using a supported version of LLVM/Clang? Check here: https://github.com/GaloisInc/llvm-pretty-bc-parser

from: METADATA_COMPILE_UNIT METADATA_BLOCK METADATA_BLOCK_ID value symbol table MODULE_BLOCK Bitstream