Missing Semantics

[naegling]

Greetings!
klee-native is failing with several missing semantics errors. Any thoughts on what I may have done wrong?

OS/Architecture

✔ rrutledge@nanshe:~
▶ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 19.04
Release:        19.04
Codename:       disco
✔ rrutledge@nanshe:~
▶ neofetch --off
rrutledge@nanshe
----------------
OS: Ubuntu 19.04 x86_64
Host: H370 WIFI
Kernel: 5.0.0-27-generic
Uptime: 2 days, 23 hours, 34 mins
Packages: 3021 (dpkg), 17 (flatpak), 14 (snap)
Shell: zsh 5.5.1
Terminal: /dev/pts/1
CPU: Intel i7-8700 (12) @ 4.600GHz
GPU: AMD ATI Radeon RX 470/480/570/570X/580/580X
Memory: 11255MiB / 32100MiB

Note that I have modified the build script to use the Ubuntu 18.04 libs

Program

✔ rrutledge@nanshe:~/projects/klee-native/test
▶ cat hello.c

#include <stdio.h>

int main(int argc, char *argv[])  {

  char *msg = NULL;
  int c = getc(stdin);
  if (c == '0') {
    msg = "hello";
  } else {
    msg = "goodbye";
  }
  printf("%s\n", msg);

  return 0;
}

build, native execution, and symbolic execution

▶ gcc -g -o hello hello.c
✔ rrutledge@nanshe:~/projects/klee-native/test
▶ ./hello
0
hello
✔ rrutledge@nanshe:~/projects/klee-native/test
▶ ./hello
1
goodbye
✔ rrutledge@nanshe:~/projects/klee-native/test
▶ klee-snapshot-7.0 --verbose --workspace_dir ws --dynamic --arch amd64_avx512  -- ./hello
✔ rrutledge@nanshe:~/projects/klee-native/test
▶ klee-exec-7.0 --workspace_dir ws --symbolic_stdin
I0909 10:54:44.545738  9670 Execute.cpp:149] Loading runtime bitcode file from /home/rrutledge/projects/arktos/remill/remill-build/tools/klee/runtime//linux_amd64_avx512.bc
KLEE: Using Z3 solver backend
I0909 10:54:44.624241  9670 Util.cpp:261] Loading amd64_avx512 semantics from file /home/rrutledge/projects/arktos/remill/remill-build/remill/Arch/X86/Runtime//amd64_avx512.bc
I0909 10:54:44.707460  9670 Workspace.cpp:329] Loading address space information from snapshot
I0909 10:54:44.707473  9670 Workspace.cpp:244] Initializing address space 1
I0909 10:54:44.707484  9670 AddressSpace.cpp:592] Mapping range [561fe7f89000, 561fe7f8a000)
I0909 10:54:44.707538  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/561fe7f89000_561fe7f8a000_r_p_00000000_00_2f_4233950_home_rrutledge_projects_klee_native_test_hello into range [561fe7f89000, 561fe7f8a000)
I0909 10:54:44.707621  9670 AddressSpace.cpp:592] Mapping range [561fe7f8a000, 561fe7f8b000)
I0909 10:54:44.707648  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/561fe7f8a000_561fe7f8b000_r_xp_00001000_00_2f_4233950_home_rrutledge_projects_klee_native_test_hello into range [561fe7f8a000, 561fe7f8b000)
I0909 10:54:44.707660  9670 AddressSpace.cpp:592] Mapping range [561fe7f8b000, 561fe7f8c000)
I0909 10:54:44.707684  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/561fe7f8b000_561fe7f8c000_r_p_00002000_00_2f_4233950_home_rrutledge_projects_klee_native_test_hello into range [561fe7f8b000, 561fe7f8c000)
I0909 10:54:44.707716  9670 AddressSpace.cpp:592] Mapping range [561fe7f8c000, 561fe7f8e000)
I0909 10:54:44.707727  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/561fe7f8c000_561fe7f8e000_rw_p_00002000_00_2f_4233950_home_rrutledge_projects_klee_native_test_hello into range [561fe7f8c000, 561fe7f8e000)
I0909 10:54:44.707742  9670 AddressSpace.cpp:592] Mapping range [7f2e97cb9000, 7f2e97cba000)
I0909 10:54:44.707767  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7f2e97cb9000_7f2e97cba000_r_p_00000000_103_05_262182_lib_x86_64_linux_gnu_ld_2_29_so into range [7f2e97cb9000, 7f2e97cba000)
I0909 10:54:44.707780  9670 AddressSpace.cpp:592] Mapping range [7f2e97cba000, 7f2e97cdb000)
I0909 10:54:44.707811  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7f2e97cba000_7f2e97cdb000_r_xp_00001000_103_05_262182_lib_x86_64_linux_gnu_ld_2_29_so into range [7f2e97cba000, 7f2e97cdb000)
I0909 10:54:44.707937  9670 AddressSpace.cpp:592] Mapping range [7f2e97cdb000, 7f2e97ce3000)
I0909 10:54:44.707988  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7f2e97cdb000_7f2e97ce3000_r_p_00022000_103_05_262182_lib_x86_64_linux_gnu_ld_2_29_so into range [7f2e97cdb000, 7f2e97ce3000)
I0909 10:54:44.708025  9670 AddressSpace.cpp:592] Mapping range [7f2e97ce3000, 7f2e97ce5000)
I0909 10:54:44.708060  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7f2e97ce3000_7f2e97ce5000_rw_p_00029000_103_05_262182_lib_x86_64_linux_gnu_ld_2_29_so into range [7f2e97ce3000, 7f2e97ce5000)
I0909 10:54:44.708109  9670 AddressSpace.cpp:592] Mapping range [7f2e97ce5000, 7f2e97ce6000)
I0909 10:54:44.708132  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7f2e97ce5000_7f2e97ce6000_rw_p_00000000_00_00_0_ into range [7f2e97ce5000, 7f2e97ce6000)
I0909 10:54:44.708163  9670 AddressSpace.cpp:592] Mapping range [7ffd7480b000, 7ffd7482c000)
I0909 10:54:44.708192  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7ffd7480b000_7ffd7482c000_rw_p_00000000_00_00_0_stack_ into range [7ffd7480b000, 7ffd7482c000)
I0909 10:54:44.708266  9670 AddressSpace.cpp:592] Mapping range [7ffd74838000, 7ffd7483b000)
I0909 10:54:44.708287  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7ffd74838000_7ffd7483b000_r_p_00000000_00_00_0_vvar_ into range [7ffd74838000, 7ffd7483b000)
I0909 10:54:44.708317  9670 AddressSpace.cpp:592] Mapping range [7ffd7483b000, 7ffd7483c000)
I0909 10:54:44.708335  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/7ffd7483b000_7ffd7483c000_r_xp_00000000_00_00_0_vdso_ into range [7ffd7483b000, 7ffd7483c000)
I0909 10:54:44.708359  9670 AddressSpace.cpp:592] Mapping range [ffffffffff600000, ffffffffff601000)
I0909 10:54:44.708379  9670 Workspace.cpp:209] Loading file /home/rrutledge/projects/klee-native/test/ws/memory/ffffffffff600000_ffffffffff601000_r_xp_00000000_00_00_0_vsyscall_ into range [ffffffffff600000, ffffffffff601000)
I0909 10:54:44.708407  9670 Workspace.cpp:337] Loading task information.
I0909 10:54:44.708411  9670 Workspace.cpp:347] Adding task starting execution at 7f2e97cba090 in address space 1
I0909 10:54:44.708415  9670 Executor.cpp:655] State size is 3376
I0909 10:54:44.708420  9670 Executor.cpp:678] Initialized snapshotted task state
I0909 10:54:44.708422  9670 Executor.cpp:684] Interpreting Tasks!
I0909 10:54:44.708425  9670 Executor.cpp:3874] Preparing to run main function
I0909 10:54:44.708432  9670 Executor.cpp:3893] Created New Execution State from kmodule
I0909 10:54:44.710012  9670 Executor.cpp:3962] Initialized globals in state
I0909 10:54:44.710650  9670 SpecialFunctionHandler.cpp:996] Copying address space 1 into state
KLEE: WARNING ONCE: Alignment of memory from call "_Znwm" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: vfprintf(140178329392992, 94396117976384, 94396105609472) at [no debug info]
sync_hyper_call:kX86ReadTSC eax=1f4 edx=0
sync_hyper_call:kX86ReadTSC eax=2af8 edx=0
 12:brk:addr=0, suppressed
sync_hyper_call:kX86CPUID eax=0 ecx=97cd4c27 -> eax=0 ebx=0 ecx=0 edx=0
E0909 10:55:21.536890  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbc904 5 (BYTES 66 0f c6 c2 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM2)) (READ_OP (IMM_8 2)))
E0909 10:55:21.538571  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbcdde 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
E0909 10:55:21.568734  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbf78e 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
E0909 10:55:21.578965  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbf78e 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
E0909 10:55:21.674835  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97ccf652 8 (BYTES 62 f1 fd 48 7f 44 24 03) VMOVDQA64_MEMu64_MASKmskw_ZMMu64_AVX512 (WRITE_OP (QWORD_PTR (ADD (REG_64 RSP) (SIGNED_IMM_64 0xc0)))) (READ_OP (REG_64 K0)) (READ_OP (REG_512 ZMM0)))
E0909 10:55:35.439009  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbc904 5 (BYTES 66 0f c6 c2 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM2)) (READ_OP (IMM_8 2)))
E0909 10:55:35.440557  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbcdde 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
E0909 10:55:37.812862  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbc904 5 (BYTES 66 0f c6 c2 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM2)) (READ_OP (IMM_8 2)))
E0909 10:55:37.814560  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbcdde 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
E0909 10:55:40.252959  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbc904 5 (BYTES 66 0f c6 c2 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM2)) (READ_OP (IMM_8 2)))
E0909 10:55:40.254604  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbcdde 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
E0909 10:55:49.458709  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbc904 5 (BYTES 66 0f c6 c2 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM2)) (READ_OP (IMM_8 2)))
E0909 10:55:49.460409  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbcdde 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
E0909 10:55:55.814040  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbc904 5 (BYTES 66 0f c6 c2 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM2)) (READ_OP (IMM_8 2)))
E0909 10:55:55.815788  9670 Lifter.cpp:123] Missing semantics for instruction (AMD64 7f2e97cbcdde 5 (BYTES 66 0f c6 c1 02) SHUFPD_XMMpd_XMMpd_IMMb (WRITE_OP (REG_512 ZMM0)) (READ_OP (REG_512 ZMM0)) (READ_OP (REG_128 XMM1)) (READ_OP (IMM_8 2)))
sync_hyper_call:Unsupported instruction at 7f2e97cbc909
KLEE: ERROR: (location information missing) abort failure
KLEE: NOTE: now ignoring this error at this location
I0909 10:55:58.199036  9670 Executor.cpp:3081] Finished state, continuation stack size is 1
✔ rrutledge@nanshe:~/projects/klee-native/test