I’m trying to generate bitcode for each libs and modules in OpenSSL. The official command to compile OpenSSL is

git clone https://github.com/openssl/openssl.git
cd openssl
export CC=clang
./config -no-asm -no-shared -no-module -no-des -no-threads -g -O0 -fembed-bitcode
make all

The flag -fembed-bitcode will embed the llvm bitcode in .llvmbc section in each object file
and I use the below command to extract the bitcode

llvm-objcopy --dump-section .llvmbc=extracted.bc source.o

Some extracted bitcode are not aligned based on llvm-bcanalyzer so I remove them. I use the same program name for the bitcode from the original object code and got something below

...
libcrypto-lib-bn_mont.bc                                        libcrypto-lib-p_lib.bc                  libdefault-lib-securitycheck.bc                  x509_acert_test-bin-x509_acert_test.bc
libcrypto-lib-bn_mpi.bc                                         libcrypto-lib-p_open.bc                 libdefault-lib-securitycheck_default.bc          x509_check_cert_pkey_test-bin-x509_check_cert_pkey_test.bc
libcrypto-lib-bn_mul.bc                                         libcrypto-lib-p_seal.bc                 libdefault-lib-seed_src.bc                       x509_dup_cert_test-bin-x509_dup_cert_test.bc
libcrypto-lib-bn_nist.bc                                        libcrypto-lib-p_sign.bc                 libdefault-lib-sha2_prov.bc                      x509_internal_test-bin-x509_internal_test.bc
libcrypto-lib-bn_prime.bc                                       libcrypto-lib-p_verify.bc               libdefault-lib-sha3_prov.bc                      x509_load_cert_file_test-bin-x509_load_cert_file_test.bc
libcrypto-lib-bn_print.bc                                       libcrypto-lib-packet.bc                 libdefault-lib-siphash_prov.bc                   x509_test-bin-x509_test.bc
libcrypto-lib-bn_rand.bc                                        libcrypto-lib-param_build.bc            libdefault-lib-sm2_enc.bc                        x509_time_test-bin-x509_time_test.bc
libcrypto-lib-bn_recp.bc                                        libcrypto-lib-param_build_set.bc        libdefault-lib-sm2_sig.bc                        x509aux-bin-x509aux.bc
libcrypto-lib-bn_rsa_fips186_4.bc                               libcrypto-lib-params.bc                 libdefault-lib-sm3_prov.bc

Then I tried to run KLEE(a symbolic execution engine) on those bitcode.
For single bitcode, KLEE failed because there wasn’t an entry function. I know underconstraint KLEE can start from any functions but that’s not the KLEE I’m using.

I tried to combine all the bitcode together but got redefinition of symbols.

Then I tried to combine bitcode with same prefix together like libdefault-lib, libcrypto-lib. I tested in one of them and got below errors

KLEE: WARNING: undefined reference to function: wait_for_async
KLEE: WARNING: undefined reference to function: x509_ctrl_string
KLEE: WARNING: Unable to find size for global variable: OPT_SECTION_STR (use will result in out of bounds access)
KLEE: WARNING: Unable to find size for global variable: OPT_MORE_STR (use will result in out of bounds access)
KLEE: WARNING: Unable to find size for global variable: OPT_HELP_STR (use will result in out of bounds access)
KLEE: WARNING: Unable to find size for global variable: OPT_PARAM_STR (use will result in out of bounds access)
KLEE: ERROR: unable to load symbol(verify_args) while initializing globals.

verify_args is an external global

@.str.400.4526 = private unnamed_addr constant [59 x i8] c"%s: Intermixed protocol flags (internet and unix domains)A0", align 1
@.str.401.4527 = private unnamed_addr constant [39 x i8] c"Cannot supply multiple protocol flagsA0", align 1
@.str.402.4528 = private unnamed_addr constant [53 x i8] c"Cannot supply both a protocol flag and '-no_<prot>'A0", align 1
@.str.403.4529 = private unnamed_addr constant [28 x i8] c"%s: Use -help for summary.A0", align 1
@verify_args = external global %struct.verify_options_st, align 4
@.str.404.4530 = private unnamed_addr constant [20 x i8] c"verify depth is %dA0", align 1
@sess_out = internal global i8* null, align 8, !dbg !3373

VERIFY_ARGS is not defined in any bitcode with my script

# Navigate to the directory containing the bitcode files
cd "$BITCODE_DIR"

# Check if the directory change was successful
if [ $? -ne 0 ]; then
    echo "Failed to navigate to bitcode directory. Check if the path exists."
    exit 1
fi

# Loop through all bitcode files in the directory
for bc_file in *.bc; do
    echo "Inspecting $bc_file for symbol '$SYMBOL_NAME'..."
    # Use llvm-nm to search for the symbol and check if it is defined in this file
    if llvm-nm "$bc_file" | grep -q " T $SYMBOL_NAME"; then
        echo "'$SYMBOL_NAME' is defined in $bc_file"
    fi
done

I guess I made some errors in the bitcode generation step.
Can anyone give me some advice? Why LLVM doesn’t have a flag support to generate bitcode and interfere the original compilation process?