Klee maze example (#369)

* In progress. Working on an example of using KLEE on a Maze, but with the maze program being compiled to x86, amd64, and aarch64. * Making lots of progress on getting lifting and runnning an aarch64 maze program on amd64, but using --explicit_args. The key thing I'm working through right now is a jump offset table, but where the offset is a block pc, rather than a table base. Also adding various bits of code here and there to making runnning with klee more directly doable, and working on a debugging facility to track down when the emulated program counter gets out of sync with the original program. * Fixed a subtle @PAGE and @PAGEOFF-related reference bug on AArch64. Partially disabled the special jump offset table handling I had in table.py, as it doesn't (yet) handle the shifted table values. However, I still have the code there, so that it can recognize that a basic block address is used as a possible offset, so that I can remove the block address as a reference, which permits a new heuristic on the C++ side to work. On the C++ side, when there's a jump instruction that isn't associated with a cross-reference flow, I try to auto-augment it with addition switch cases, targeting blocks with no predecessors (as present in the CFG). This seems to work reasonably well. * Improved the scripts and updated the READMEs. * Minor rephrase * Minor rephrase
2026-06-08 15:31:09 +00:00 · 2018-01-13 23:47:55 -05:00
parent bc17c7072c
commit 8a9856ada3
25 changed files with 1072 additions and 295 deletions
@@ -6,128 +6,37 @@ define print-rip
  dont-repeat
 end

-define print-reg-state-64
+set $__rax_offset = 2216
+set $__flags_offset = 2064
+set $__xmm0_offset = 16
+
+define print-reg-state-amd64
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
  printf "             emulated                   native\n"
-  printf "rip     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2408)), $rip
-  printf "rax     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2152)), $rax
-  printf "rbx     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2168)), $rbx
-  printf "rcx     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2184)), $rcx
-  printf "rdx     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2200)), $rdx
-  printf "rsi     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2216)), $rsi
-  printf "rdi     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2232)), $rdi
-  printf "rbp     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2264)), $rbp
-  printf "rsp     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2248)), $rsp
-  printf "r8      0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2280)), $r8
-  printf "r9      0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2296)), $r9
-  printf "r10     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2312)), $r10
-  printf "r11     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2328)), $r11
-  printf "r12     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2344)), $r12
-  printf "r13     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2360)), $r13
-  printf "r14     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2376)), $r14
-  printf "r15     0x%016lx        0x%016lx\n", *((unsigned long long *)($rptr + 2392)), $r15
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "rip     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 16 * 16)), $rip
+  printf "rax     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 0 * 16)), $rax
+  printf "rbx     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 1 * 16)), $rbx
+  printf "rcx     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 2 * 16)), $rcx
+  printf "rdx     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 3 * 16)), $rdx
+  printf "rsi     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 4 * 16)), $rsi
+  printf "rdi     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 5 * 16)), $rdi
+  printf "rsp     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 6 * 16)), $rsp
+  printf "rbp     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 7 * 16)), $rbp
+  printf "r8      0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 8 * 16)), $r8
+  printf "r9      0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 9 * 16)), $r9
+  printf "r10     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 10 * 16)), $r10
+  printf "r11     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 11 * 16)), $r11
+  printf "r12     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 12 * 16)), $r12
+  printf "r13     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 13 * 16)), $r13
+  printf "r14     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 14 * 16)), $r14
+  printf "r15     0x%016lx        0x%016lx\n", *((unsigned long long *)($__rax_ptr + 15 * 16)), $r15
  dont-repeat
 end

-define addr-of-xmm0-64
+define print-flags-amd64
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm0) = 0x%016lx\n", $rptr + 16
-  dont-repeat
-end
-
-define addr-of-xmm1-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm1) = 0x%016lx\n", $rptr + 80
-  dont-repeat
-end
-
-define addr-of-xmm2-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm2) = 0x%016lx\n", $rptr + 144
-  dont-repeat
-end
-
-define addr-of-xmm3-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm3) = 0x%016lx\n", $rptr + 208
-  dont-repeat
-end
-
-define addr-of-xmm4-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm4) = 0x%016lx\n", $rptr + 272
-  dont-repeat
-end
-
-define addr-of-xmm5-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm5) = 0x%016lx\n", $rptr + 336
-  dont-repeat
-end
-
-define addr-of-xmm6-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm6) = 0x%016lx\n", $rptr + 400
-  dont-repeat
-end
-
-define addr-of-xmm7-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm7) = 0x%016lx\n", $rptr + 464
-  dont-repeat
-end
-
-define addr-of-xmm8-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm8) = 0x%016lx\n", $rptr + 528
-  dont-repeat
-end
-
-define addr-of-xmm9-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm9) = 0x%016lx\n", $rptr + 592
-  dont-repeat
-end
-
-define addr-of-xmm10-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm10) = 0x%016lx\n", $rptr + 656
-  dont-repeat
-end
-
-define addr-of-xmm11-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm11) = 0x%016lx\n", $rptr + 720
-  dont-repeat
-end
-
-define addr-of-xmm12-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm12) = 0x%016lx\n", $rptr + 784
-  dont-repeat
-end
-
-define addr-of-xmm13-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm13) = 0x%016lx\n", $rptr + 848
-  dont-repeat
-end
-
-define addr-of-xmm14-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm14) = 0x%016lx\n", $rptr + 912
-  dont-repeat
-end
-
-define addr-of-xmm15-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&(RegState::xmm15) = 0x%016lx\n", $rptr + 976
-  dont-repeat
-end
-
-define print-flags-64
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  set $flptr = (char *) ($rptr + 0x810)
+  set $flptr = (char *) ($rptr + $__flags_offset)
  printf "eflags ["
  if $flptr[1]
    printf "CF "
@@ -154,122 +63,105 @@ define print-flags-64
  dont-repeat
 end

-define print-reg-state-32
-  set $rptr = ((unsigned (*)(void))__mcsema_debug_get_reg_state)()
-  printf "         emulated           native\n"
-  printf "eip     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2408)), $eip
-  printf "eax     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2152)), $eax
-  printf "ebx     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2168)), $ebx
-  printf "ecx     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2184)), $ecx
-  printf "edx     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2200)), $edx
-  printf "esi     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2216)), $esi
-  printf "edi     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2232)), $edi
-  printf "ebp     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2264)), $ebp
-  printf "esp     0x%08lx        0x%016lx\n", *((unsigned long long *)($rptr + 2248)), $esp
+define print-flags-x86
+  print-flags-amd64
+end
+
+define print-reg-state-x86
+  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
+  printf "             emulated                   native\n"
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "eip     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 16 * 16)), (unsigned) $pc
+  printf "eax     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 0 * 16)), $eax
+  printf "ebx     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 1 * 16)), $ebx
+  printf "ecx     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 2 * 16)), $ecx
+  printf "edx     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 3 * 16)), $edx
+  printf "esi     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 4 * 16)), $esi
+  printf "edi     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 5 * 16)), $edi
+  printf "esp     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 6 * 16)), $esp
+  printf "ebp     0x%08x        0x%08x\n", *((unsigned *)($__rax_ptr + 7 * 16)), $ebp
+  dont-repeat
+end
+
+set $__x0_offset = 544
+
+define print-reg-state-aarch64
+  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
+  printf "\temulated\n"
+  set $__x0_ptr = $rptr + $__x0_offset
+  set $__i = 0
+  while $__i < 31
+    printf "x%d\t0x%016lx\t&x%d = 0x%lx\n", $__i, *((unsigned long long *)($__x0_ptr + $__i * 16)), $__i, $__x0_ptr + $__i * 16
+    set $__i = $__i + 1
+  end
+  
+  printf "sp\t0x%016lx\n", *((unsigned long long *)($__x0_ptr + $__i * 16))
+  set $__i = $__i + 1
+  printf "pc\t0x%016lx\t&pc = 0x%lx\n", *((unsigned long long *)($__x0_ptr + $__i * 16)), $__x0_ptr + $__i * 16
  dont-repeat
 end


 define addr-of-rip
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rip = 0x%016lx\n", $rptr + 2408
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rip = 0x%016lx\n", $__rax_ptr + 16 * 16
  dont-repeat
 end

 define addr-of-rax
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rax = 0x%016lx\n", $rptr + 2152
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rax = 0x%016lx\n", $__rax_ptr + 0 * 16
  dont-repeat
 end

 define addr-of-rbx
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rbx = 0x%016lx\n", $rptr + 2168
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rbx = 0x%016lx\n", $__rax_ptr + 1 * 16
  dont-repeat
 end

 define addr-of-rcx
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rcx = 0x%016lx\n", $rptr + 2184
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rcx = 0x%016lx\n", $__rax_ptr + 2 * 16
  dont-repeat
 end

 define addr-of-rdx
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rdx = 0x%016lx\n", $rptr + 2200
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rdx = 0x%016lx\n", $__rax_ptr + 3 * 16
  dont-repeat
 end

 define addr-of-rsi
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rsi = 0x%016lx\n", $rptr + 2216
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rsi = 0x%016lx\n", $__rax_ptr + 4 * 16
  dont-repeat
 end

 define addr-of-rdi
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rdi = 0x%016lx\n", $rptr + 2232
-  dont-repeat
-end
-
-define addr-of-rbp
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rbp = 0x%016lx\n", $rptr + 2264
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rdi = 0x%016lx\n", $__rax_ptr + 5 * 16
  dont-repeat
 end

 define addr-of-rsp
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&rsp = 0x%016lx\n", $rptr + 2248
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rsp = 0x%016lx\n", $__rax_ptr + 6 * 16
  dont-repeat
 end

-
-define addr-of-r8
+define addr-of-rbp
  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r8 = 0x%016lx\n", $rptr + 2280
-  dont-repeat
-end
-
-define addr-of-r9
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r9 = 0x%016lx\n", $rptr + 2296
-  dont-repeat
-end
-
-define addr-of-r10
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r10 = 0x%016lx\n", $rptr + 2312
-  dont-repeat
-end
-
-define addr-of-r11
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r11 = 0x%016lx\n", $rptr + 2328
-  dont-repeat
-end
-
-define addr-of-r12
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r12 = 0x%016lx\n", $rptr + 2344
-  dont-repeat
-end
-
-define addr-of-r13
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r13 = 0x%016lx\n", $rptr + 2360
-  dont-repeat
-end
-
-define addr-of-r14
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r14 = 0x%016lx\n", $rptr + 2376
-  dont-repeat
-end
-
-define addr-of-r15
-  set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
-  printf "&r15 = 0x%016lx\n", $rptr + 2392
+  set $__rax_ptr = $rptr + $__rax_offset
+  printf "&rbp = 0x%016lx\n", $__rax_ptr + 7 * 16
  dont-repeat
 end

@@ -105,3 +105,6 @@ install(

 install(CODE
    "execute_process(COMMAND python ${PROJECT_SOURCE_DIR}/tools/setup.py install -f --prefix=${CMAKE_INSTALL_PREFIX})")
+
+add_subdirectory(examples)
+    
@@ -31,7 +31,7 @@ Why would anyone translate binaries *back* to bitcode?

 * **Binary Patching And Modification**. Lifting to LLVM IR lets you cleanly modify the target program. You can run obfuscation or hardening passes, add features, remove features, rewrite features, or even fix that pesky typo, grammatical error, or insane logic. When done, your new creation can be recompiled to a new binary sporting all those changes. In the [Cyber Grand Challenge](https://blog.trailofbits.com/2015/07/15/how-we-fared-in-the-cyber-grand-challenge/), we were able to use McSema to translate challenge binaries to bitcode, insert memory safety checks, and then re-emit working binaries.

-* **Symbolic Execution with KLEE**. [KLEE](https://klee.github.io/) operates on LLVM bitcode, usually generated by providing source to the LLVM toolchain. McSema can lift a binary to LLVM bitcode, [permitting KLEE to operate on previously unavailable targets](https://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/).
+* **Symbolic Execution with KLEE**. [KLEE](https://klee.github.io/) operates on LLVM bitcode, usually generated by providing source to the LLVM toolchain. McSema can lift a binary to LLVM bitcode, [permitting KLEE to operate on previously unavailable targets](https://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/). See our [walkthrough](examples/Maze/README.md) showing how to run KLEE on a symbolic maze.

 * **Re-use existing LLVM-based tools**. KLEE is not the only tool that becomes available for use on bitcode. It is possible to run LLVM optimization passes and other LLVM-based tools like [libFuzzer](http://llvm.org/docs/LibFuzzer.html) on [lifted bitcode](docs/UsingLibFuzzer.md).

@@ -71,8 +71,11 @@ sudo apt-get install \
     git \
     cmake \
     python2.7 python-pip \
+     wget \
     build-essential \
     gcc-multilib g++-multilib \
+     libtinfo-dev \
+     lsb-release \
     realpath

 sudo pip install --upgrade pip
@@ -0,0 +1,18 @@
+# Copyright (c) 2017 Trail of Bits, Inc.
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+project(examples)
+cmake_minimum_required (VERSION 3.2)
+
+add_executable(maze Maze/Maze.c)
@@ -0,0 +1,2 @@
+bc/*
+klee-*
@@ -0,0 +1,157 @@
+/*
+ * Copyright (c) 2018 Trail of Bits, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/*
+ * It's a maze!
+ * Use a,s,d,w to move "through" it.
+ */
+
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+/* Dimensions of the Maze */
+enum {
+  kWidth = 11,
+  kHeight = 7
+};
+
+/* Hard-coded maze */
+char maze[kHeight][kWidth] = {
+    {'+', '-', '+', '-', '-', '-', '+', '-', '-', '-', '+'},
+    {'|', ' ', '|', ' ', ' ', ' ', ' ', ' ', '|', '#', '|'},
+    {'|', ' ', '|', ' ', '-', '-', '+', ' ', '|', ' ', '|'},
+    {'|', ' ', '|', ' ', ' ', ' ', '|', ' ', '|', ' ', '|'},
+    {'|', ' ', '+', '-', '-', ' ', '|', ' ', '|', ' ', '|'},
+    {'|', ' ', ' ', ' ', ' ', ' ', '|', ' ', ' ', ' ', '|'},
+    {'+', '-', '-', '-', '-', '-', '+', '-', '-', '-', '+'},
+};
+
+/**
+ * Draw the maze state in the screen!
+ */
+void draw(void) {
+  int i, j;
+  for (i = 0; i < kHeight; i++) {
+    for (j = 0; j < kWidth; j++) {
+      printf("%c", maze[i][j]);
+    }
+    printf("\n");
+  }
+  printf("\n");
+}
+
+enum {
+  kMaxNumPlayerMoves = 28
+};
+
+/**
+ * The main function
+ */
+int main(int argc, char *argv[]) {
+  int x, y;     /* Player position */
+  int ox, oy;   /* Old player position */
+  int i = 0;    /* Iteration number */
+
+  char program[kMaxNumPlayerMoves];
+
+  /* Initial position */
+  x = 1;
+  y = 1;
+  maze[y][x] = 'X';
+
+  /* Print some info. */
+  printf("Maze dimensions: %dx%d\n", kWidth, kHeight);
+  printf("Player position: %dx%d\n", x, y);
+  printf("Iteration no. %d\n", i);
+  printf("Program the player moves with a sequence of 'w', 's', 'a' and 'd'\n");
+  printf("Try to reach the price(#)!\n");
+
+  /* Draw the maze */
+  draw();
+
+  /* Read the directions 'program' to execute... */
+  read(STDIN_FILENO, program, kMaxNumPlayerMoves);
+
+  /* Iterate and run 'program'. */
+  while (i < kMaxNumPlayerMoves) {
+    /* Save old player position */
+    ox = x;
+    oy = y;
+
+    /* Move player position depending on the actual command */
+    switch (program[i]) {
+      case 'w':
+        y--;
+        break;
+      case 's':
+        y++;
+        break;
+      case 'a':
+        x--;
+        break;
+      case 'd':
+        x++;
+        break;
+      default:
+        printf("Wrong command, only w,s,a,d are accepted!)\n");
+        printf("You lose!\n");
+        exit(EXIT_FAILURE);
+    }
+
+    /* If hit the price, You Win!! */
+    if (maze[y][x] == '#') {
+      printf("You win!\n");
+      printf("Your solution <%42s>\n", program);
+      exit(EXIT_SUCCESS);
+    }
+
+    /* If something is wrong do not advance. */
+    if (maze[y][x] != ' '
+        && !((y == 2 && maze[y][x] == '|' && x > 0 && x < kWidth))) {
+      x = ox;
+      y = oy;
+    }
+
+    /* Print new maze state and info... */
+    printf("Player position: %dx%d\n", x, y);
+    printf("Iteration no. %d. Action: %c. %s\n", i, program[i],
+           ((ox == x && oy == y) ? "Blocked!" : ""));
+
+    /* If crashed to a wall! Exit, you lose */
+    if (ox == x && oy == y) {
+      printf("You lose\n");
+      exit(EXIT_FAILURE);
+    }
+
+    /* put the player on the maze... */
+    maze[y][x] = 'X';
+
+    /* draw it */
+    draw();
+
+    /* increment iteration */
+    i++;
+
+    /* me wait to human */
+    sleep(1);
+  }
+
+  /* You couldn't make it! You lose! */
+  printf("You lose\n");
+  return EXIT_FAILURE;
+}
@@ -0,0 +1,156 @@
+# Solving a Maze with KLEE and McSema
+
+This walkthrough describes how to run KLEE on a simple Maze program. The instructions here have been tested on Ubuntu 16.04. Your mileage may vary if you are using another operating system. What is unique about this walkthrough is that it will show that KLEE runs equally well on lifted bitcode produced from the same program compiled to x86-64 (amd64) and AArch64 (64-bit ARMv8).
+
+The program, [Maze.c](Maze.c), can be found in this directory, along with the [binaries](bin) and [control-flow graph files](cfg) for the Maze program.
+
+## The Maze
+
+The Maze program presents its user with the following challenge: type in a sequence of `w`, `s`, `a`, or `d` characters to guide the `X` through the maze and reach the destination denoted by `#`.
+
+The characters `w`, `s`, `a`, and `d` are used in place of the keyboard's arrow keys, that is:
+
+```
+    +---+               +---+    
+    | w |               | ^ |    
+---+---+---+  <=>  +---+---+---+
+| a | s | d |       | < | v | > |
+---+---+---+       +---+---+---+
+```
+
+Initially, the program displays the maze, and asks the user to type in their directions for how to complete it.
+
+```
+Maze dimensions: 11x7
+Player position: 1x1
+Iteration no. 0
+Program the player moves with a sequence of 'w', 's', 'a' and 'd'
+Try to reach the price(#)!
+-+---+---+
+|X|     |#|
+| | --+ | |
+| |   | | |
+| +-- | | |
+|     |   |
+-----+---+
+```
+
+The winning directions for the maze are `ssssddddwwaawwddddssssddwwww`. The winning output looks like this:
+
+```
+Player position: 9x2
+Iteration no. 26. Action: w. 
+-+---+---+
+|X|XXXXX|#|
+|X|X--+X|X|
+|X|XXX|X|X|
+|X+--X|X|X|
+|XXXXX|XXX|
+-----+---+
+
+You win!
+Your solution <              ssssddddwwaawwddddssssddwwww>
+```
+
+Let's jump in and see if we KLEE, acting as the user, can win this maze!
+
+## Running KLEE
+
+### Step 1: Get dependencies
+
+The first step is to make sure that we have all the dependencies that we need.
+
+```bash
+sudo apt-get update
+sudo apt-get upgrade
+
+sudo apt-get install \
+     git \
+     cmake \
+     python2.7 python-pip \
+     wget \
+     build-essential \
+     gcc-multilib g++-multilib \
+     libtinfo-dev \
+     lsb-release \
+     realpath \
+     z3
+
+sudo pip install --upgrade pip
+sudo pip install 'protobuf==3.2.0'
+```
+
+Now that we have the dependencies we need, we should clone [Remill](https://github.com/trailofbits/remill).
+
+```bash
+cd /data
+git clone git@github.com:trailofbits/remill.git
+```
+
+### Step 2: Build Remill, McSema, and KLEE
+
+We have provided a convenient [script](https://github.com/trailofbits/remill/blob/master/scripts/build_klee.sh) for this walkthrough. The script will clone the latest version of McSema into the Remill checkout, as well as clone a version of KLEE that is compatible with Remill. You might already have McSema installed, and it might be a version that is not compatible with KLEE. That is not a problem. The script will ensure that the proper toolchain is built *within* the directory in which you invoke the script.
+
+```bash
+mkdir /tmp/klee_ws
+cd /tmp/klee_ws
+```
+
+Now to invoke our build script within `/tmp/klee_ws`, which is where Remill, McSema, and KLEE will be compiled.
+
+```bash
+/data/remill/scripts/build_klee.sh
+```
+
+### Step 3: Lift the Maze binaries
+
+From within the KLEE workspace `/tmp/klee_ws`, run the [lifting script](scripts/lift.sh). This script invokes `mcsema-lift-3.9` on the provided [CFG files](cfg). If you have IDA Pro, then you can reproduce these steps manually by invoking the [disassembly script](scripts/disass.sh).
+
+```bash
+/data/remill/tools/mcsema/examples/Maze/scripts/lift.sh
+```
+
+This script will likely print out some error messages. That is okay. McSema will always try to produce bitcode, and it will warn you when something seems erroneous in the CFG file.
+
+### Step 4: Run KLEE
+
+The build script from step 2 will have compiled KLEE into the `/tmp/klee_ws/klee-build/` directory. We can run the KLEE using the following commands. If things work, then there will be a lot of funny looking output.
+
+```bash
+./klee-build/bin/klee -posix-runtime -libc=uclibc -allow-external-sym-calls /data/remill/tools/mcsema/examples/Maze/bc/maze.amd64.bc -sym-stdin 28
+```
+
+```bash
+./klee-build/bin/klee -posix-runtime -libc=uclibc -allow-external-sym-calls /data/remill/tools/mcsema/examples/Maze/bc/maze.aarch64.bc -sym-stdin 28
+```
+
+### Step 5: Example ouput
+
+We know that the answer to the maze is `ssssddddwwaawwddddssssddwwww`, so we can check to see if KLEE found it by running `ktest-tool` on all of the `.ktest`-suffixed files in the KLEE's output file directory (`klee-last` is a symlink to the most recently produced output directory).
+
+```bash
+for f in /data/remill/tools/mcsema/examples/Maze/bc/klee-last/*.ktest ; do
+  ./klee-build/bin/ktest-tool $f | grep ssssddddwwaawwddddssssddwwww &>/dev/null ;
+  if [[ $? -eq 0 ]] ; then
+    FOUND_TEST=$f
+  fi
+done
+./klee-build/bin/ktest-tool $FOUND_TEST
+```
+
+The output we get should be something like the following:
+
+```
+ktest file : '/data/remill/tools/mcsema/examples/Maze/bc/klee-last/test000301.ktest'
+args       : ['/data/remill/tools/mcsema/examples/Maze/bc/maze.aarch64.bc', '-sym-stdin', '28']
+num objects: 3
+object    0: name: 'stdin'
+object    0: size: 28
+object    0: data: 'ssssddddwwaawwddddssssddwwww'
+object    1: name: 'stdin-stat'
+object    1: size: 144
+object    1: data: '\x02\x08\x00\x00\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x01\x01\x01\x01\x00\x00\x00\x00\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\x00\x10\x00\x00\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01R\x06XZ\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\xbb\x1dXZ\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\xbb\x1dXZ\x00\x00\x00\x00\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01\x01'
+object    2: name: 'model_version'
+object    2: size: 4
+object    2: data: '\x01\x00\x00\x00'
+```
@@ -0,0 +1,92 @@
+#!/usr/bin/env bash
+# Copyright (c) 2017 Trail of Bits, Inc.
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+SCRIPTS_DIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
+MAZE_DIR=$( cd "$( dirname "${SCRIPTS_DIR}" )" && pwd )
+DISASSEMBLER=/opt/ida-6.9/idal64
+
+function Disassemble {
+
+  printf "[+] Disassembling ${MAZE_DIR}/bin/maze.amd64\n"
+  mcsema-disass \
+      --os linux \
+      --arch amd64 \
+      --disassembler "${DISASSEMBLER}" \
+      --log_file /tmp/log \
+      --entrypoint main \
+      --output "${MAZE_DIR}/cfg/maze.amd64.cfg" \
+      --binary "${MAZE_DIR}/bin/maze.amd64"
+
+  if [[ $? -ne 0 ]] ; then
+    printf "[x] Error disassembling ${MAZE_DIR}/bin/maze.amd64\n"
+    return 1
+  else
+    printf " i  Saved CFG to ${MAZE_DIR}/cfg/maze.amd64.cfg\n"
+  fi
+
+  printf "[+] Disassembling ${MAZE_DIR}/bin/maze.aarch64\n"
+  mcsema-disass \
+      --os linux \
+      --arch aarch64 \
+      --disassembler "${DISASSEMBLER}" \
+      --log_file /tmp/log \
+      --entrypoint main \
+      --output "${MAZE_DIR}/cfg/maze.aarch64.cfg" \
+      --binary "${MAZE_DIR}/bin/maze.aarch64"
+
+  if [[ $? -ne 0 ]] ; then
+    printf "[x] Error disassembling ${MAZE_DIR}/bin/maze.aarch64\n"
+    return 1
+  else
+    printf " i  Saved CFG to ${MAZE_DIR}/cfg/maze.aarch64.cfg\n"
+  fi
+
+  return 0
+}
+
+function main {
+  while [[ $# -gt 0 ]] ; do
+    key="$1"
+
+    case $key in
+
+      # Change the default installation prefix.
+      --disassembler)
+        DISASSEMBLER=$(python -c "import os; import sys; sys.stdout.write(os.path.abspath('${2}'))")
+        printf "[+] New disassembler path is ${DISASSEMBLER}\n"
+        shift # past argument
+      ;;
+
+      *)
+        # unknown option
+        printf "[x] Unknown option: ${key}\n"
+        return 1
+      ;;
+    esac
+
+    shift # past argument or value
+  done
+
+  if [[ ! -f "${DISASSEMBLER}" ]] ; then
+    printf "[x] Disassembler ${DISASSEMBLER} does not exist. Please specify it manually using --disassembler.\n"
+    return 1
+  fi
+
+  Disassemble
+  return $?
+}
+
+main $@
+exit $?
@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# Copyright (c) 2017 Trail of Bits, Inc.
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+SCRIPTS_DIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
+MAZE_DIR=$( cd "$( dirname "${SCRIPTS_DIR}" )" && pwd )
+KLEE_WS_DIR=$(pwd)
+
+mkdir -p "${MAZE_DIR}/bc"
+
+# Look for `libc.bc`. This file is automatically created by the `build_klee.sh`
+# script in Remill, so that we can make the lifted bitcode more dependable via
+# the `--library` option.
+LIB_ARGS=
+if [[ -f "${KLEE_WS_DIR}/libc.bc" ]] ; then
+  LIB_ARGS="--library ${KLEE_WS_DIR}/libc.bc"
+else
+  printf "[x] WARNING: Could not find klee-uclibc library bitcode.\n"
+fi
+
+printf "[+] Lifting ${MAZE_DIR}/cfg/maze.amd64.cfg\n"
+
+mcsema-lift-3.9 \
+    --os linux \
+    --arch amd64 \
+    --cfg "${MAZE_DIR}/cfg/maze.amd64.cfg" \
+    --output "${MAZE_DIR}/bc/maze.amd64.bc" \
+    --explicit_args \
+    ${LIB_ARGS}
+
+if [[ $? -ne 0 ]] ; then
+  printf "[x] Could not lift ${MAZE_DIR}/cfg/maze.amd64.cfg\n"
+else
+  printf " i  Saved bitcode to ${MAZE_DIR}/bc/maze.amd64.bc\n"
+fi
+
+printf "[+] Lifting ${MAZE_DIR}/cfg/maze.aarch64.cfg\n"
+
+mcsema-lift-3.9 \
+    --os linux \
+    --arch aarch64 \
+    --cfg "${MAZE_DIR}/cfg/maze.aarch64.cfg" \
+    --output "${MAZE_DIR}/bc/maze.aarch64.bc" \
+    --explicit_args \
+    ${LIB_ARGS}
+
+if [[ $? -ne 0 ]] ; then
+  printf "[x] Could not lift ${MAZE_DIR}/cfg/maze.aarch64.cfg\n"
+else
+  printf " i  Saved bitcode to ${MAZE_DIR}/bc/maze.aarch64.bc\n"
+fi
@@ -421,6 +421,40 @@ const char *CallingConvention::GetVarForNextArgument(llvm::Type *val_type) {
  return nullptr;
 }

+static llvm::Function *ReadIntFromMemFunc(uint64_t size_bytes) {
+  if (8 == size_bytes) {
+    return gModule->getFunction("__remill_read_memory_64");
+  } else if (4 == size_bytes) {
+    return gModule->getFunction("__remill_read_memory_32");
+  } else if (2 == size_bytes) {
+    return gModule->getFunction("__remill_read_memory_16");
+  } else if (1 == size_bytes) {
+    return gModule->getFunction("__remill_read_memory_8");
+  } else {
+    LOG(FATAL)
+        << "Cannot find function to read " << size_bytes
+        << "-byte integer from memory.";
+    return nullptr;
+  }
+}
+
+static llvm::Function *WriteIntToMemFunc(uint64_t size_bytes) {
+  if (8 == size_bytes) {
+    return gModule->getFunction("__remill_write_memory_64");
+  } else if (4 == size_bytes) {
+    return gModule->getFunction("__remill_write_memory_32");
+  } else if (2 == size_bytes) {
+    return gModule->getFunction("__remill_write_memory_16");
+  } else if (1 == size_bytes) {
+    return gModule->getFunction("__remill_write_memory_8");
+  } else {
+    LOG(FATAL)
+        << "Cannot find function to read " << size_bytes
+        << "-byte integer from memory.";
+    return nullptr;
+  }
+}
+
 llvm::Value *CallingConvention::LoadNextArgument(llvm::BasicBlock *block,
                                                 llvm::Type *goal_type) {
  if (!goal_type) {
@@ -466,28 +500,8 @@ llvm::Value *CallingConvention::LoadNextArgument(llvm::BasicBlock *block,
    val = ir.CreateCall(gModule->getFunction("__remill_read_memory_f32"), args);

  } else if (goal_type->isIntegerTy()) {
-    llvm::Function *func = nullptr;
-    if (8 == alloc_size) {
-      func = gModule->getFunction("__remill_read_memory_64");
-
-    } else if (4 == alloc_size) {
-      func = gModule->getFunction("__remill_read_memory_32");
-
-    } else if (2 == alloc_size) {
-      func = gModule->getFunction("__remill_read_memory_16");
-
-    } else if (1 == alloc_size) {
-      func = gModule->getFunction("__remill_read_memory_8");
-
-    } else {
-      LOG(FATAL)
-          << "Can't handle reading an " << alloc_size << "-byte integer "
-          << "argument from the stack (base type: "
-          << remill::LLVMThingToString(goal_type) << ")";
-      return nullptr;
-    }
-
-    val = ir.CreateCall(func, args);
+    auto read_mem = ReadIntFromMemFunc(alloc_size);
+    val = ir.CreateCall(read_mem, args);
    if (dl.getTypeSizeInBits(goal_type) <
        dl.getTypeAllocSizeInBits(goal_type)) {
      val = ir.CreateTrunc(val, goal_type);
@@ -552,11 +566,15 @@ void CallingConvention::StoreReturnValue(llvm::BasicBlock *block,
    if (size < gArch->address_size) {
      val_type = gWordType;
      ret_val = ir.CreateZExt(ret_val, val_type);
-    } else {
-      CHECK(size <= gArch->address_size)
-          << "Cannot store value of type "
+
+    } else if (size > gArch->address_size) {
+      LOG(ERROR)
+          << "Truncating value of type "
          << remill::LLVMThingToString(val_type)
-          << " into variable " << val_var;
+          << " to store it into variable " << val_var
+          << " of type " << remill::LLVMThingToString(gWordType);
+      ret_val = ir.CreateTrunc(ret_val, gWordType);
+      val_type = gWordType;
    }

  // Storing a `float` into an x87 register, convert it to a `double`.
@@ -631,18 +649,7 @@ void CallingConvention::StoreArguments(
      func = gModule->getFunction("__remill_write_memory_f32");

    } else if (arg_type->isIntegerTy()) {
-      if (8 == alloc_size) {
-        func = gModule->getFunction("__remill_write_memory_64");
-
-      } else if (4 == alloc_size) {
-        func = gModule->getFunction("__remill_write_memory_32");
-
-      } else if (2 == alloc_size) {
-        func = gModule->getFunction("__remill_write_memory_16");
-
-      } else if (1 == alloc_size) {
-        func = gModule->getFunction("__remill_write_memory_8");
-      }
+      func = WriteIntToMemFunc(alloc_size);

      if (dl.getTypeSizeInBits(arg_type) <
          dl.getTypeAllocSizeInBits(arg_type)) {
@@ -730,15 +737,24 @@ void CallingConvention::AllocateReturnAddress(llvm::BasicBlock *block) {

 void CallingConvention::FreeReturnAddress(llvm::BasicBlock *block) {
  if (gArch->IsAArch64()) {
-    return;  // Return address is passed through the link pointer.
+    auto x30 = remill::FindVarInFunction(block, "X30");
+    llvm::IRBuilder<> ir(block);
+    auto ret_addr = ir.CreateLoad(ir.CreateLoad(x30));
+    remill::StoreProgramCounter(block, ret_addr);

  // The stack grows down on x86/amd64.
  } else if (gArch->IsX86() || gArch->IsAMD64()) {
    llvm::IRBuilder<> ir(block);
    auto addr_size = gArch->address_size / 8;
    auto addr_size_bytes = llvm::ConstantInt::get(gWordType, addr_size);
+    auto sp = LoadStackPointer(block);
+    auto read_ret_addr = ReadIntFromMemFunc(addr_size);
+    llvm::Value *read_ret_addr_args[] = {remill::LoadMemoryPointer(block), sp};
+    auto ret_addr = ir.CreateCall(read_ret_addr, read_ret_addr_args);
+    remill::StoreProgramCounter(block, ret_addr);
+
    StoreStackPointer(
-        block, ir.CreateAdd(LoadStackPointer(block), addr_size_bytes));
+        block, ir.CreateAdd(sp, addr_size_bytes));

  } else {
    LOG(FATAL)
@@ -771,9 +787,25 @@ llvm::Value *CallingConvention::LoadStackPointer(llvm::BasicBlock *block) {
 void CallingConvention::StoreStackPointer(llvm::BasicBlock *block,
                                          llvm::Value *new_val) {
  llvm::IRBuilder<> ir(block);
+  auto val_type = new_val->getType();
+  if (val_type->isPointerTy()) {
+    new_val = ir.CreatePtrToInt(new_val, gWordType);
+  }
  ir.CreateStore(
      new_val,
-      ir.CreateLoad(remill::FindVarInFunction(block, sp_name)));
+      ir.CreateLoad(remill::FindVarInFunction(block, StackPointerVarName())));
+}
+
+void CallingConvention::StoreThreadPointer(llvm::BasicBlock *block,
+                                           llvm::Value *new_val) {
+  llvm::IRBuilder<> ir(block);
+  auto val_type = new_val->getType();
+  if (val_type->isPointerTy()) {
+    new_val = ir.CreatePtrToInt(new_val, gWordType);
+  }
+  ir.CreateStore(
+      new_val,
+      ir.CreateLoad(remill::FindVarInFunction(block, ThreadPointerVarName())));
 }

 // Return the address of the base of the TLS data.
@@ -59,6 +59,8 @@ class CallingConvention {
    return sp_name;
  }

+  void StoreThreadPointer(llvm::BasicBlock *block, llvm::Value *new_val);
+
  const char *ThreadPointerVarName(void) const {
    return tp_name;
  }
@@ -223,6 +223,35 @@ static llvm::Constant *InitialStackPointerValue(void) {
  return llvm::ConstantExpr::getPtrToInt(gep, gWordType);
 }

+// Create an array of data for holding thread-local storage.
+static llvm::Constant *InitialThreadLocalStorage(void) {
+  static llvm::Constant *tls = nullptr;
+  if (tls) {
+    return tls;
+  }
+
+  auto tls_type = llvm::ArrayType::get(
+      gWordType, 4096 / (gArch->address_size / 8));
+
+  auto tls_var = new llvm::GlobalVariable(
+    *gModule, tls_type, false, llvm::GlobalValue::InternalLinkage,
+    llvm::Constant::getNullValue(tls_type), "__mcsema_tls");
+
+  std::vector<llvm::Constant *> indexes(2);
+  indexes[0] = llvm::ConstantInt::get(gWordType, 0);
+  indexes[1] = indexes[0];
+
+#if LLVM_VERSION_NUMBER <= LLVM_VERSION(3, 6)
+  auto gep = llvm::ConstantExpr::getInBoundsGetElementPtr(tls_var, indexes);
+#else
+  auto gep = llvm::ConstantExpr::getInBoundsGetElementPtr(
+      nullptr, tls_var, indexes);
+#endif
+
+  tls = llvm::ConstantExpr::getPtrToInt(gep, gWordType);
+  return tls;
+}
+
 // Create a state structure with everything zero-initialized, except for the
 // stack pointer.
 static llvm::Constant *CreateInitializedState(
@@ -419,6 +448,8 @@ static llvm::Function *ImplementExplicitArgsEntryPoint(

  CallingConvention loader(gArch->DefaultCallingConv());

+  loader.StoreThreadPointer(block, InitialThreadLocalStorage());
+
  // Save off the old stack pointer for later.
  auto old_sp = loader.LoadStackPointer(block);

@@ -432,18 +463,6 @@ static llvm::Function *ImplementExplicitArgsEntryPoint(
  // Allocate any space needed on the stack for a return address.
  loader.AllocateReturnAddress(block);

-//  // Set up the thread pointer, if any.
-//  if (auto tp_name = loader.ThreadPointerVarName()) {
-//    auto get_tp = llvm::Intrinsic::getDeclaration(
-//        gModule, llvm::Intrinsic::thread_pointer);
-//    if (get_tp) {
-//      llvm::IRBuilder<> ir(block);
-//      ir.CreateStore(
-//          ir.CreatePtrToInt(ir.CreateCall(get_tp), gWordType),
-//          ir.CreateLoad(remill::FindVarInFunction(func, tp_name)));
-//    }
-//  }
-
  // Call the lifted function.
  std::vector<llvm::Value *> args(3);
  args[remill::kMemoryPointerArgNum] = remill::LoadMemoryPointer(block);
@@ -543,7 +562,8 @@ static void ImplementExplicitArgsExitPoint(

  auto block = &(callback_func->back());

-  // create call to function and args
+  // The emulated code already set up the machine state with the arguments for
+  // the external, so we need to go and read out the arguments.
  std::vector<llvm::Value *> call_args;
  for (auto i = 0U; i < cfg_func->num_args; i++) {
    llvm::Type *param_type = nullptr;
@@ -553,6 +573,9 @@ static void ImplementExplicitArgsExitPoint(
    call_args.push_back(loader.LoadNextArgument(block, param_type));
  }

+  // Now that we've read the argument values, we want to free up the space that
+  // the emulated caller set up, so that when we eventually return, things are
+  // in the expected state.
  loader.FreeReturnAddress(block);
  loader.FreeArguments(block);

@@ -101,10 +101,10 @@ void DeclareExternals(const NativeModule *cfg_module) {
      auto var_type = llvm::Type::getIntNTy(
          *gContext, static_cast<unsigned>(cfg_var->size * 8));

+      auto linkage = llvm::GlobalValue::ExternalLinkage;
      ll_var = new llvm::GlobalVariable(*gModule, var_type, false,
-                                        llvm::GlobalValue::ExternalLinkage,
-                                        nullptr, cfg_var->name, nullptr,
-                                        ThreadLocalMode(cfg_var));
+                                        linkage, nullptr, cfg_var->name,
+                                        nullptr, ThreadLocalMode(cfg_var));
    }

    if (!cfg_var->address) {
@@ -21,6 +21,8 @@
 #include <llvm/IR/DataLayout.h>
 #include <llvm/IR/DebugInfo.h>
 #include <llvm/IR/InstIterator.h>
+#include <llvm/IR/InlineAsm.h>
+#include <llvm/IR/Intrinsics.h>
 #include <llvm/IR/IRBuilder.h>
 #include <llvm/IR/LegacyPassManager.h>
 #include <llvm/IR/LLVMContext.h>
@@ -65,7 +67,11 @@ DEFINE_bool(add_reg_tracer, false,
 DEFINE_bool(add_breakpoints, false,
            "Add 'breakpoint' functions between every lifted instruction. This "
            "allows one to set a breakpoint, in the lifted code, just before a "
-            "specific lifted instruction is executed.");
+            "specific lifted instruction is executed. This is a debugging aid.");
+
+DEFINE_bool(check_pc_at_breakpoints, false,
+            "Check whether or not the emulated program counter is correct at "
+            "each injected 'breakpoint' function. This is a debugging aid.");

 namespace mcsema {
 namespace {
@@ -85,21 +91,59 @@ static llvm::Function *GetBreakPoint(uint64_t pc) {
  ss << "breakpoint_" << std::hex << pc;

  auto func_name = ss.str();
-  auto bp = gModule->getFunction(func_name);
-  if (!bp) {
-    bp = llvm::Function::Create(
-        LiftedFunctionType(), llvm::GlobalValue::ExternalLinkage,
-        func_name, gModule);
-
-    // Make sure to keep this function around (along with `ExternalLinkage`).
-    bp->addFnAttr(llvm::Attribute::OptimizeNone);
-    bp->addFnAttr(llvm::Attribute::NoInline);
-    bp->removeFnAttr(llvm::Attribute::ReadNone);
-
-    llvm::IRBuilder<> ir(llvm::BasicBlock::Create(*gContext, "", bp));
-    ir.CreateRet(remill::NthArgument(bp, remill::kMemoryPointerArgNum));
+  auto func = gModule->getFunction(func_name);
+  if (func) {
+    return func;
  }
-  return bp;
+
+  func = llvm::Function::Create(
+      LiftedFunctionType(), llvm::GlobalValue::ExternalLinkage,
+      func_name, gModule);
+
+  // Make sure to keep this function around (along with `ExternalLinkage`).
+  func->addFnAttr(llvm::Attribute::OptimizeNone);
+  func->addFnAttr(llvm::Attribute::NoInline);
+  func->removeFnAttr(llvm::Attribute::ReadNone);
+
+#if LLVM_VERSION_NUMBER < LLVM_VERSION(3, 7)
+  func->addFnAttr(llvm::Attribute::ReadOnly);
+#else
+  func->addFnAttr(llvm::Attribute::ArgMemOnly);
+#endif
+
+  auto state_ptr = remill::NthArgument(func, remill::kStatePointerArgNum);
+  auto state_ptr_type = state_ptr->getType();
+
+  llvm::IRBuilder<> ir(llvm::BasicBlock::Create(*gContext, "", func));
+
+  if (FLAGS_check_pc_at_breakpoints) {
+    auto trap = llvm::Intrinsic::getDeclaration(gModule, llvm::Intrinsic::trap);
+    auto are_eq = ir.CreateICmpEQ(
+        remill::NthArgument(func, remill::kPCArgNum),
+        llvm::ConstantInt::get(gWordType, pc));
+
+    auto not_eq_bb = llvm::BasicBlock::Create(*gContext, "", func);
+    auto eq_bb = llvm::BasicBlock::Create(*gContext, "", func);
+    ir.CreateCondBr(are_eq, eq_bb, not_eq_bb);
+
+    ir.SetInsertPoint(not_eq_bb);
+    ir.CreateCall(trap);
+    ir.CreateUnreachable();
+
+    ir.SetInsertPoint(eq_bb);
+  }
+
+  // Basically some empty inline assembly that tells the compiler not to
+  // optimize away the `state` pointer before each `breakpoint_XXX` function.
+  auto asm_func_type = llvm::FunctionType::get(
+      llvm::Type::getVoidTy(*gContext), state_ptr_type);
+
+  auto asm_func = llvm::InlineAsm::get(
+      asm_func_type, "", "*m,~{dirflag},~{fpsr},~{flags}", true);
+
+  ir.CreateCall(asm_func, state_ptr);
+  ir.CreateRet(remill::NthArgument(func, remill::kMemoryPointerArgNum));
+  return func;
 }

 // Tries to get the lifted function beginning at `pc`.
@@ -122,7 +166,7 @@ static void InlineSubFuncCall(llvm::BasicBlock *block,
  (void) new llvm::StoreInst(call, mem_ptr, block);
 }

-// Find an external function associated with
+// Find an external function associated with this indirect jump.
 static llvm::Function *DevirtualizeIndirectFlow(
    TranslationContext &ctx, llvm::Function *fallback) {
  if (ctx.cfg_inst->flow) {
@@ -236,8 +280,8 @@ static void LiftIndirectJump(TranslationContext &ctx,
                             llvm::BasicBlock *block,
                             remill::Instruction &inst) {

-  auto fallback = DevirtualizeIndirectFlow(
-      ctx, GetLiftedToNativeExitPoint(kExitPointJump));
+  auto exit_point = GetLiftedToNativeExitPoint(kExitPointJump);
+  auto fallback = DevirtualizeIndirectFlow(ctx, exit_point);

  std::unordered_map<uint64_t, llvm::BasicBlock *> block_map;
  for (auto target_ea : ctx.cfg_block->successor_eas) {
@@ -245,6 +289,38 @@ static void LiftIndirectJump(TranslationContext &ctx,
    fallback = ctx.lifter->intrinsics->missing_block;
  }

+  if (exit_point == fallback) {
+
+    // If we have no targets, then a reasonable target turns out to be the next
+    // program counter.
+    if (block_map.empty()) {
+      block_map[inst.next_pc] = GetOrCreateBlock(ctx, inst.next_pc);
+    }
+
+    // Build up a set of all reachable blocks that were known at disassembly
+    // time so that we can find blocks that have no predecessors.
+    std::unordered_set<uint64_t> succ_eas;
+    succ_eas.insert(ctx.cfg_func->ea);
+    for (auto block_entry : ctx.cfg_func->blocks) {
+      auto cfg_block = block_entry.second;
+      succ_eas.insert(cfg_block->successor_eas.begin(),
+                      cfg_block->successor_eas.end());
+    }
+
+    // We'll augment our block map to also target unreachable blocks, just in
+    // case our disassembly failed to find some of the targets.
+    for (auto block_entry : ctx.cfg_func->blocks) {
+      auto target_ea = block_entry.first;
+      if (!succ_eas.count(target_ea)) {
+        LOG(WARNING)
+            << "Adding block " << std::hex << target_ea
+            << " with no predecessors as additional target of the "
+            << " indirect jump at " << inst.pc << std::dec;
+        block_map[target_ea] = GetOrCreateBlock(ctx, target_ea);
+      }
+    }
+  }
+
  // We have no jump table information, so assume that it's an indirect tail
  // call, so just go native.
  if (block_map.empty()) {
@@ -544,7 +620,6 @@ static llvm::Function *LiftFunction(
  lifted_func->removeFnAttr(llvm::Attribute::NoReturn);
  lifted_func->addFnAttr(llvm::Attribute::NoInline);
  lifted_func->setVisibility(llvm::GlobalValue::DefaultVisibility);
-  lifted_func->setLinkage(llvm::GlobalValue::InternalLinkage);

  TranslationContext ctx;
  std::unique_ptr<remill::InstructionLifter> lifter(
@@ -557,6 +632,10 @@ static llvm::Function *LiftFunction(
  ctx.cfg_inst = nullptr;
  ctx.lifted_func = lifted_func;

+  std::unordered_set<uint64_t> referenced_blocks;
+  referenced_blocks.insert(cfg_func->ea);
+
+
  // Create basic blocks for each basic block in the original function.
  for (auto block_info : cfg_func->blocks) {
    auto cfg_block = block_info.second;
@@ -20,7 +20,9 @@
 #include <llvm/IR/Constants.h>
 #include <llvm/IR/DataLayout.h>
 #include <llvm/IR/DebugInfo.h>
+#include <llvm/IR/Function.h>
 #include <llvm/IR/InstIterator.h>
+#include <llvm/IR/Intrinsics.h>
 #include <llvm/IR/IRBuilder.h>
 #include <llvm/IR/LegacyPassManager.h>
 #include <llvm/IR/LLVMContext.h>
@@ -45,6 +47,7 @@
 #include "remill/BC/ABI.h"
 #include "remill/BC/IntrinsicTable.h"
 #include "remill/BC/Lifter.h"
+#include "remill/BC/Util.h"

 #include "mcsema/Arch/Arch.h"
 #include "mcsema/BC/Callback.h"
@@ -58,6 +61,7 @@
 #include "mcsema/CFG/CFG.h"

 DECLARE_bool(legacy_mode);
+DECLARE_bool(explicit_args);
 DECLARE_string(pc_annotation);

 namespace mcsema {
@@ -96,6 +100,64 @@ static void ExportVariables(const NativeModule *cfg_module) {
  }
 }

+// Handle the GCC stack protector. Normally we'd do this in `External.cpp`,
+// but it seems like optimizing a global that is `AvailableExternallyLinkage`
+// with an initializer somewhere in the code (in our case, a `LazyInitXref`),
+// results in the linkage being changed to `ExternalLinkage`. We want
+// `AvailableExternallyLinkage` for the sake of something like KLEE.
+static void DefineGCCStackGuard(void) {
+  if (auto stack_guard = gModule->getGlobalVariable("__stack_chk_guard")) {
+    stack_guard->setInitializer(
+        llvm::Constant::getNullValue(stack_guard->getType()->getElementType()));
+    stack_guard->setLinkage(llvm::GlobalValue::ExternalWeakLinkage);
+  }
+}
+
+// Define the function `__mcsema_debug_get_reg_state`. Normally this is part of
+// the McSema runtime, but if we are lifting with `--explicit_args`, and are
+// also compiling the lifted bitcode back to native, then we may not use the
+// runtime and so might not have this useful debugging function available to us.
+static void DefineDebugGetRegState(void) {
+  auto get_reg_state = gModule->getFunction("__mcsema_debug_get_reg_state");
+  if (get_reg_state) {
+    return;
+  }
+
+  auto reg_state = gModule->getGlobalVariable("__mcsema_reg_state", true);
+  if (!reg_state) {
+    return;
+  }
+
+  auto state_ptr_type = reg_state->getType();
+  auto reg_func_type = llvm::FunctionType::get(state_ptr_type, false);
+  get_reg_state = llvm::Function::Create(
+      reg_func_type, llvm::GlobalValue::ExternalWeakLinkage,
+      "__mcsema_debug_get_reg_state", gModule);
+
+  llvm::IRBuilder<> ir(llvm::BasicBlock::Create(*gContext, "", get_reg_state));
+  ir.CreateRet(reg_state);
+
+  get_reg_state->addFnAttr(llvm::Attribute::NoInline);
+  get_reg_state->addFnAttr(llvm::Attribute::OptimizeNone);
+}
+
+// Define some of the remill error intrinsics.
+static void DefineErrorIntrinsics(llvm::FunctionType *lifted_func_type) {
+  const char *func_names[] = {"__remill_error", "__remill_missing_block"};
+  auto trap = llvm::Intrinsic::getDeclaration(gModule, llvm::Intrinsic::trap);
+  for (auto func_name : func_names) {
+    auto func = gModule->getFunction(func_name);
+    if (!func) {
+      continue;
+    }
+    if (func->isDeclaration()) {
+      llvm::IRBuilder<> ir(llvm::BasicBlock::Create(*gContext, "", func));
+      ir.CreateCall(trap);
+      ir.CreateUnreachable();
+    }
+  }
+}
+
 }  // namespace

 bool LiftCodeIntoModule(const NativeModule *cfg_module) {
@@ -106,6 +168,8 @@ bool LiftCodeIntoModule(const NativeModule *cfg_module) {
  // so that cross-references to lifted code are handled.
  AddDataSegments(cfg_module);

+  auto lifted_func_type = remill::LiftedFunctionType(gModule);
+
  // Lift the blocks of instructions into the declared functions.
  if (!DefineLiftedFunctions(cfg_module)) {
    return false;
@@ -127,6 +191,12 @@ bool LiftCodeIntoModule(const NativeModule *cfg_module) {

  OptimizeModule();

+  if (FLAGS_explicit_args) {
+    DefineGCCStackGuard();
+    DefineDebugGetRegState();
+    DefineErrorIntrinsics(lifted_func_type);
+  }
+
  if (!FLAGS_pc_annotation.empty()) {
    legacy::PropagateInstAnnotations();
  }
@@ -79,8 +79,7 @@ static void ReplaceUndefIntrinsic(llvm::Function *function) {

 static void RemoveFunction(llvm::Function *func) {
  if (!func->hasNUsesOrMore(1)) {
-    func->removeFromParent();
-    delete func;
+    func->eraseFromParent();
  }
 }

@@ -177,21 +176,38 @@ static void RemoveIntrinsics(void) {
  // we'll try to get the optimizer to inline it on our behalf, which should
  // drop some references :-D
  if (auto remill_used = gModule->getFunction("__remill_mark_as_used")) {
-    if (remill_used->isDeclaration()) {
-      remill_used->setLinkage(llvm::GlobalValue::InternalLinkage);
-      remill_used->removeFnAttr(llvm::Attribute::NoInline);
-      remill_used->addFnAttr(llvm::Attribute::InlineHint);
-      remill_used->addFnAttr(llvm::Attribute::AlwaysInline);
-      auto block = llvm::BasicBlock::Create(*gContext, "", remill_used);
-      (void) llvm::ReturnInst::Create(*gContext, block);
+    std::vector<llvm::CallInst *> uses;
+    for (auto use : remill_used->users()) {
+      if (auto call = llvm::dyn_cast<llvm::CallInst>(use)) {
+        uses.push_back(call);
+      }
    }
+
+    for (auto call : uses) {
+      call->eraseFromParent();
+    }
+
+    if (remill_used->hasNUsesOrMore(1)) {
+      if (remill_used->isDeclaration()) {
+        remill_used->setLinkage(llvm::GlobalValue::InternalLinkage);
+        remill_used->removeFnAttr(llvm::Attribute::NoInline);
+        remill_used->addFnAttr(llvm::Attribute::InlineHint);
+        remill_used->addFnAttr(llvm::Attribute::AlwaysInline);
+        auto block = llvm::BasicBlock::Create(*gContext, "", remill_used);
+        (void) llvm::ReturnInst::Create(*gContext, block);
+      }
+    }
+
+    RemoveFunction(remill_used);
  }

-  RemoveFunction("__remill_intrinsics");
+//  if (auto intrinsics = gModule->getFunction("__remill_intrinsics")) {
+//    intrinsics->eraseFromParent();
+//  }
+
  RemoveFunction("__remill_basic_block");
-  RemoveFunction("__remill_mark_as_used");
  RemoveFunction("__remill_defer_inlining");
-  RemoveFunction("__remill_mark_as_used");
+  RemoveFunction("__remill_intrinsics");
 }

 static void ReplaceBarrier(const char *name) {
@@ -165,6 +165,67 @@ _HAS_NO_REFS = set()
 _NO_REFS = tuple()
 _ENABLE_CACHING = False
 _BAD_ARM_REF_OFF = (idc.BADADDR, 0)
+_NOT_A_REF = set()
+
+# Remove a reference from `from_ea` to `to_ea`.
+def remove_instruction_reference(from_ea, to_ea):
+  global _REFS, _NOT_A_REF
+
+  _NOT_A_REF.add((from_ea, to_ea))
+
+  try:
+    idaapi.del_dref(from_ea, to_ea)
+    idaapi.del_cref(from_ea, to_ea, False)
+    idaapi.del_cref(from_ea, to_ea, True)
+  except:
+    pass
+
+  if not _ENABLE_CACHING or from_ea not in _REFS:
+    return
+
+  new_refs = []
+  found = False
+  for old_ref in _REFS[from_ea]:
+    if old_ref.ea != to_ea:
+      new_refs.append(old_ref)
+    else:
+      found = True
+
+  if found:
+    _REFS[from_ea] = tuple(new_refs)
+
+def _get_arm_ref_candidate(mask, op_val, op_str, all_refs):
+  global _BAD_ARM_REF_OFF
+
+  try:
+    op_name = op_str.split("@")[0][1:]  # `#asc_400E5C@PAGE` -> `asc_400E5C`.
+    ref_ea = idc.LocByName(op_name)
+    if (ref_ea & mask) == op_val:
+      return ref_ea, mask
+  except:
+    pass
+
+  # NOTE(pag): We deal with candidates because it's possible that this
+  #            instruction will have multiple references. In the case of
+  #            `@PAGE`-based offsets, it's problematic when the wrong base
+  #            is matched, because it really throws off the C++ side of things
+  #            because the arrangement of the lifted data being on the same
+  #            page is not guaranteed.
+
+  candidates = set()
+  for ref_ea in all_refs:
+    if (ref_ea & mask) == op_val:
+      candidates.add(ref_ea)
+      return ref_ea, mask
+
+  if len(candidates):
+    for candidate_ea in candidates:
+      if candidate_ea == op_val:
+        return candidate_ea, mask
+
+    return candidates.pop(), mask
+
+  return _BAD_ARM_REF_OFF

 # Try to handle `@PAGE` and `@PAGEOFF` references, resolving them to their
 # 'intended' address.
@@ -181,18 +242,13 @@ def _try_get_arm_ref_addr(inst, op, op_val, all_refs):
  op_str = idc.GetOpnd(inst.ea, op.n)

  if '@PAGEOFF' in op_str:
-    mask = 0x0fff
-    for ref_ea in all_refs:
-      if (ref_ea & mask) == op_val:
-        return ref_ea, mask
-    DEBUG("Found @PAGEOFF-based reference at {:x} but could not match it in all_refs".format(inst.ea));
+    return _get_arm_ref_candidate(0x0fff, op_val, op_str, all_refs)

  elif '@PAGE' in op_str:
-    mask = 0x0fffff000
-    for ref_ea in all_refs:
-      if (ref_ea & mask) == op_val:
-        return ref_ea, mask
-    DEBUG("Found @PAGE-based reference at {:x} but could not match it in all_refs".format(inst.ea));
+    return _get_arm_ref_candidate(0x0fffff000, op_val, op_str, all_refs)
+
+  elif not is_invalid_ea(op_val) and inst.get_canon_mnem().lower() == "adr":
+    return op_val, 0

  return _BAD_ARM_REF_OFF

@@ -238,8 +294,9 @@ def _get_ref_candidate(inst, op, all_refs, binary_is_pie):
  #              will avoid these awkward `if IS_ARM` and the comments about
  #              x86 / amd64 stuff.
  if IS_ARM:
+    old_addr_val = addr_val
    addr_val, mask = _try_get_arm_ref_addr(inst, op, addr_val, all_refs)
-  
+
  info = idaapi.refinfo_t()
  has_ref_info = idaapi.get_refinfo(inst.ea, op.n, info) == 1

@@ -343,7 +400,7 @@ def enable_reference_caching():

 # Get a list of references from an instruction.
 def get_instruction_references(arg, binary_is_pie=False):
-  global _ENABLE_CACHING
+  global _ENABLE_CACHING, _NOT_A_REF

  inst = arg
  if isinstance(arg, (int, long)):
@@ -447,7 +504,8 @@ def get_instruction_references(arg, binary_is_pie=False):
    # Note: idc.o_phrase is ignored because it doesn't have a displacement,
    #       and so can't reference a specific symbol.

-    refs.append(ref)
+    if (inst.ea, ref.ea) not in _NOT_A_REF:
+      refs.append(ref)

  for ref in refs:
    assert not is_invalid_ea(ref.ea)
@@ -147,7 +147,17 @@ def get_num_jump_table_entries(builder):
  # now lets go and check all the targets
  max_i = max(curr_num_targets, 1024)
  entry_addr = builder.table_ea
+  table_seg_ea = idc.SegStart(builder.table_ea)
  for i in xrange(max_i):
+
+    # Make sure we don't read across a segment (e.g. if the jump table is the
+    # last thing in our current segment).
+    try:
+      if table_seg_ea != idc.SegStart(entry_addr):
+        break
+    except:
+      break
+
    entry_data = builder.read_entry(entry_addr)
    next_entry_addr = entry_addr + (builder.entry_size * builder.entry_mult)

@@ -209,7 +219,7 @@ def try_get_simple_jump_table_reader(builder):

  # Try the offset table based approach first, as it's likely to be more
  # constrained.
-  for offset in (builder.table_ea, builder.table_ea, 0):
+  for offset in (builder.table_ea, builder.table_ea, builder.offset):
    for offset_mult in (1, -1):
      for entry_mult in (1, -1):
        for size in sizes:
@@ -319,16 +329,22 @@ def get_manual_jump_table_reader(builder):
  of the table base address that happens before the actual `jmp`."""
  ret = False
  next_inst_ea = builder.jump_ea
+  found_ref_eas = set()
  for i in xrange(5):
    inst_ea = next_inst_ea
    next_inst_ea = idc.PrevHead(inst_ea)
    if inst_ea == idc.BADADDR:
      break

+    elif builder.jump_ea != inst_ea and is_control_flow(inst_ea):
+      break
+
    refs = get_instruction_references(inst_ea, builder.binary_is_pie)
    if not len(refs):
      continue

+    found_ref_eas.add((inst_ea, refs[0].ea))
+
    builder.table_ea = refs[0].ea
    builder.offset = 0

@@ -345,8 +361,80 @@ def get_manual_jump_table_reader(builder):
    DEBUG("Reader inferred jump table base: {:x}".format(builder.table_ea))
    if builder.offset:
      DEBUG("Reader inferred jump table offset: {:x}".format(builder.offset))
+    return ret

-  return ret
+  if len(found_ref_eas) < 2:
+    return ret
+
+  # We're going to try to recognize a jump table of the form:
+  #
+  #    .text:00000000004009AC ADRP            X1, #asc_400E5C@PAGE ; "\b"
+  #    .text:00000000004009B0 ADD             X1, X1, #asc_400E5C@PAGEOFF ; "\b"
+  #    .text:00000000004009B4 LDR             W0, [X1,W0,UXTW#2]
+  #    .text:00000000004009B8 ADR             X1, loc_4009C4
+  #    .text:00000000004009BC ADD             X0, X1, W0,SXTW#2
+  #    .text:00000000004009C0 BR              X0
+  #
+  # Where it's a table of offsets (`asc_400E5C`), and the base offset is
+  # the basic block `loc_4009C4`.
+  min_ea, max_ea = get_function_bounds(builder.jump_ea)
+
+  inst_block_ea = idc.BADADDR
+  block_ea = idc.BADADDR
+
+  for inst_ea, ref_ea in found_ref_eas:
+    if is_code_by_flags(ref_ea) and min_ea <= ref_ea < max_ea:
+      inst_block_ea = inst_ea
+      block_ea = ref_ea
+      break
+
+  if idc.BADADDR == block_ea:
+    return ret
+
+  found_ref_eas.remove((inst_block_ea, block_ea))
+
+  # The idea here is that we want to trick the jump table reader into thinking
+  # that the offset of the jump table is a basic block.
+  for inst_ea, ref_ea in found_ref_eas:
+    builder.table_ea = ref_ea
+    builder.offset = block_ea
+    ret = try_get_simple_jump_table_reader(builder)
+    if ret:
+      break
+
+  if ret:
+    DEBUG("Reader inferred jump table base: {:x}".format(builder.table_ea))
+    if builder.offset == block_ea:
+      DEBUG("Reader inferred jump table offset is the block {:x}".format(
+          builder.offset))
+      
+      # McSema-lifted bitcode doesn't really have a good way of getting the
+      # address of a basic block, and even so, we don't really want that either.
+      # The way our jump table lifting works is to preserve the original
+      # addresses and computation, and `switch` based on that, so we need to
+      # make sure that the original basic block address shows up in the lifted
+      # bitcode.
+
+      DEBUG("WARNING: Removing reference from {:x} to block {:x}".format(
+          inst_block_ea, block_ea))
+      remove_instruction_reference(inst_block_ea, block_ea)
+
+  # NOTE(pag): For now we disable this jump table detection, even if it seems
+  #            like we find the table. This is because we don't yet have a good
+  #            way of dealing with the `ADD X0, X1, W0,SXTW#2`, which scales
+  #            the read table entry out by shifting it left by two. Besides
+  #            that, the following code actually works reasonably well. To
+  #            account for this, on the C++ side, we augment jump table
+  #            `switch`es to target blocks that are not referenced by the
+  #            successor lists of any other blocks.
+  #
+  #            It is also pretty important to make sure that we remove the
+  #            instruction reference. If/when we have good support for this
+  #            kind of jump table, then the above call to
+  #            `remove_instruction_reference` has to be removed so that the
+  #            various things that the C++ side of things does to handle offset-
+  #            based jump tables works. 
+  return False

 def get_jump_table_reader(builder):
  """Returns the size of a jump table entry, as well as a reader function
@@ -87,15 +87,16 @@ static void PrintSupportedInstructions(void) {
                      });
 }

+static std::unique_ptr<llvm::Module> gLibrary;
+
 // Load in a separate bitcode or IR library, and copy function and variable
 // declarations from that library into our module. We can use this feature
 // to provide better type information to McSema.
 static void LoadLibraryIntoModule(void) {
-  std::unique_ptr<llvm::Module> lib(
-      remill::LoadModuleFromFile(mcsema::gContext, FLAGS_library));
+  gLibrary.reset(remill::LoadModuleFromFile(mcsema::gContext, FLAGS_library));

  // Declare the functions from the library in McSema's target module.
-  for (auto &func : *lib) {
+  for (auto &func : *gLibrary) {
    auto func_name = func.getName();
    if (func_name.startswith("__mcsema") || func_name.startswith("__remill")) {
      continue;
@@ -118,7 +119,7 @@ static void LoadLibraryIntoModule(void) {
  }

  // Declare the global variables from the library in McSema's target module.
-  for (auto &var : lib->globals()) {
+  for (auto &var : gLibrary->globals()) {
    auto var_name = var.getName();
    if (var_name.startswith("__mcsema") || var_name.startswith("__remill")) {
      continue;
@@ -142,6 +143,23 @@ static void LoadLibraryIntoModule(void) {
  }
 }

+// Remove unused functions and globals brought in from the library.
+static void UnloadLibraryFromModule(void) {
+  for (auto &func : *gLibrary) {
+    auto our_func = mcsema::gModule->getFunction(func.getName());
+    if (our_func && !our_func->hasNUsesOrMore(1)) {
+      our_func->eraseFromParent();
+    }
+  }
+
+  for (auto &var : gLibrary->globals()) {
+    auto our_var = mcsema::gModule->getGlobalVariable(var.getName());
+    if (our_var && !our_var->hasNUsesOrMore(1)) {
+      our_var->eraseFromParent();
+    }
+  }
+}
+
 }  // namespace

 int main(int argc, char *argv[]) {
@@ -282,7 +300,13 @@ int main(int argc, char *argv[]) {
      << "Unable to lift CFG from " << FLAGS_cfg << " into module "
      << FLAGS_output;

+  if (!FLAGS_library.empty()) {
+    UnloadLibraryFromModule();
+    gLibrary.reset(nullptr);
+  }
+
  remill::StoreModuleToFile(mcsema::gModule, FLAGS_output);
+
  google::ShutDownCommandLineFlags();
  google::ShutdownGoogleLogging();