You have encountered a bug in uc-crux-llvm's implementation. Mac M1

[Sweetaroo]

Describe the bug I tried to use "uc-crux-llvm" following the Building step https://github.com/GaloisInc/crucible/tree/master/uc-crux-llvm#building-1, and when I run the command "cabal v2-build", it works fine.

However, when I run the command "cabal v2-run exe:uc-crux-llvm -- --entry-points call_non_function_pointer test/programs/call_non_function_pointer.c" , it output:

You have encountered a bug in uc-crux-llvm's implementation.
*** Please create an issue at https://github.com/GaloisInc/crucible/issues

%< ---------------------------------------------------
  Revision:  af9c12732f4ba75558decde1942c5d4eb12833bb
  Branch:    master
  Location:  toFullType
  Message:   Opaque pointer types in globals or arguments
             is not yet implemented as a feature of crux-llvm bugfinding mode.
             If this feature would be useful to you, please report this error.
CallStack (from HasCallStack):
  panic, called at src/UCCrux/LLVM/Errors/Unimplemented.hs:81:3 in uc-crux-llvm-0.3-inplace:UCCrux.LLVM.Errors.Unimplemented
  unimplemented, called at src/UCCrux/LLVM/FullType/Type.hs:536:7 in uc-crux-llvm-0.3-inplace:UCCrux.LLVM.FullType.Type
%< ---------------------------------------------------

Got the same output when run the command like:

cabal run exe:uc-crux-llvm -- --entry-points deref_arg_const_index test/programs/deref_arg_const_index.c
cabal v2-run exe:uc-crux-llvm -- --entry-points deref_arg_const_index test/programs/deref_arg_const_index.c

The reason why I didn't run the command "cabal v2-install exe:uc-crux-llvm --overwrite-policy=always" is because it's never worked and give the error as following:

Wrote tarball sdist to
/Users/sweetaroo/Workspace/crucible/dist-newstyle/sdist/crucible-0.7.0.99.tar.gz
Error: cabal: sdist of crucible-cli-0.1: invalid file glob
'test-data/**/*.cbl'. Using the double-star syntax requires 'cabal-version:
2.4' or greater. Alternatively, for compatibility with earlier Cabal versions,
list the included directories explicitly.

To Reproduce Steps to reproduce the behavior:

$ cabal v2-build
$ cabal v2-run exe:uc-crux-llvm -- --entry-points call_non_function_pointer test/programs/call_non_function_pointer.c

Expected behavior Run successfully the demo provided in the https://github.com/GaloisInc/crucible/tree/master/uc-crux-llvm#targeted-mode

System information

• macOS Monterey 12.6.5 M1 pro
• cabal, 3.10.2.1
• ghc , 9.4.8
• llvm , 15.0
• clang 15.0.0

Additional context It is my first time to use this tool and would be appreciated if anyone can helps me. Add any other context about the problem here.

[langston-barrett]

@Sweetaroo Thanks for the report! The problem is that UC-Crux doesn't yet support opaque pointers (see #1075), which were introduced in recent versions of LLVM/Clang. You can try working around the issue by using an older version of Clang to compile the program, but it's unlikely that UC-Crux will be upgraded to support opaque pointers in the near future.

[Sweetaroo]

@langston-barrett Thanks! When I downgrade the version of LLVM from 15 to 12, it works well! Thanks again!