From ab7233c5b889b5ed1d92adc1fa9c9c8d0c37705a Mon Sep 17 00:00:00 2001
From: Scott Owens <sowens@fb.com>
Date: Fri, 27 Sep 2019 02:15:28 -0700
Subject: [PATCH] [sledge sem] Refactor the way LLVM sem. does phis

Summary:
Previously the LLVM semantics did the phi instructions at the head of a
block as part of executing the branch into that block. This looked a bit
weird, but had the advantage that the semantics knew which block was
being jumped from, which is necessary to run the phi instructions.
However, it meant that the rules for doing phi instructions would need
to show up with each branching construct. It was also annoying for the
LLVM->llair proof, since the phis are removed and their effect happens as
a distinct step from the branch.

Here we add a distinct Phi_ip instruction pointer to indicate that the
phi instructions at the start of the block should execute next, and then
be incremented to the usual numeric instruction pointer that points to
the non-phi instructions. The Phi_ip contains the identity of the
previous block.

Reviewed By: jberdine

Differential Revision: D17452416

fbshipit-source-id: 78fef7cca
---
 sledge/semantics/llvmScript.sml      | 133 ++++++++++++-----
 sledge/semantics/llvm_liveScript.sml | 213 ++++++++++++++++-----------
 sledge/semantics/llvm_propScript.sml | 120 +++++++++++----
 sledge/semantics/miscScript.sml      |  13 ++
 sledge/semantics/settingsScript.sml  |   3 +
 5 files changed, 328 insertions(+), 154 deletions(-)

diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 6fc3d9244..8027b9bd4 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -68,6 +68,21 @@ Datatype:
   cond = Eq | Ult | Slt
 End
 
+Datatype:
+  phi = Phi reg ty ((label option, arg) alist)
+End
+
+(*
+ * The Exit instruction below models a system/libc call to exit the program. The
+ * semantics needs some way to tell the difference between normally terminated
+ * programs and stuck states, and this lets it do that. From a C++ perspective,
+ * a program could call this directly, in which case it's good to model, or it
+ * might simply return from main and then the code in libc that called main will
+ * call exit. However, adding special handling for main in the semantics will
+ * cruft things up a bit, and it's not very satisfying, because it's not really
+ * an LLVM concept.
+ *)
+
 Datatype:
   instr =
   (* Terminators *)
@@ -96,10 +111,6 @@ Datatype:
   | Cxa_get_exception_ptr reg arg
 End
 
-Datatype:
-  phi = Phi reg ty ((label option, arg) alist)
-End
-
 Datatype:
   clause = Catch targ
 End
@@ -160,8 +171,17 @@ Datatype:
   pv = <| poison : bool; value : v |>
 End
 
+(* Instruction pointer into a block. Phi_ip indicates to do the phi instruction,
+ * coming from the given label. Offset points to a normal (non-phi) instruction.
+ * *)
+Datatype:
+  bip =
+  | Phi_ip (label option)
+  | Offset num
+End
+
 Datatype:
-  pc = <| f : fun_name; b : label option; i : num |>
+  pc = <| f : fun_name; b : label option; i : bip |>
 End
 
 Datatype:
@@ -461,8 +481,13 @@ Definition update_result_def:
   update_result x v s = s with locals := s.locals |+ (x, v)
 End
 
+Definition inc_bip_def:
+  (inc_bip (Phi_ip _) = Offset 0) ∧
+  (inc_bip (Offset i) = Offset (i + 1))
+End
+
 Definition inc_pc_def:
-  inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
+  inc_pc s = s with ip := (s.ip with i := inc_bip s.ip.i)
 End
 
 Inductive get_obs:
@@ -488,27 +513,12 @@ Inductive step_instr:
           stack := st;
           heap := new_h |>)) ∧
 
-(* Do the phi assignments in parallel. The manual says "For the purposes of the
- * SSA form, the use of each incoming value is deemed to occur on the edge from
- * the corresponding predecessor block to the current block (but after any
- * definition of an 'invoke' instruction's return value on the same edge)".
- * So treat these two as equivalent
- * %r1 = phi [0, %l]
- * %r2 = phi [%r1, %l]
- * and
- * %r2 = phi [%r1, %l]
- * %r1 = phi [0, %l]
- *)
   (eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
-   l = Some (if tf = 1w then l1 else l2) ∧
-   alookup prog s.ip.f = Some d ∧
-   alookup d.blocks l = Some <| h := Head phis None; body := b |> ∧
-   map (do_phi l s) phis = map Some updates
+   l = Some (if tf = 1w then l1 else l2)
    ⇒
    step_instr prog s
      (Br a l1 l2) Tau
-     (s with <| ip := <| f := s.ip.f; b := l; i := 0 |>;
-                locals := s.locals |++ updates |>)) ∧
+     (s with ip := <| f := s.ip.f; b := l; i := Phi_ip s.ip.b |>)) ∧
 
   (* TODO *)
   (step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧
@@ -623,11 +633,12 @@ Inductive step_instr:
    ⇒
    step_instr prog s
      (Call r t fname targs) Tau
-     <| ip := <| f := fname; b := None; i := 0 |>;
+     (* Jump to the entry block of the function which has no phis *)
+     <| ip := <| f := fname; b := None; i := Offset 0 |>;
         locals := alist_to_fmap (zip (map snd d.params, vs));
         globals := s.globals;
         stack :=
-          <| ret := s.ip with i := s.ip.i + 1;
+          <| ret := s.ip with i := inc_bip s.ip.i;
              saved_locals := s.locals;
              result_var := r;
              stack_allocs := [] |> :: s.stack;
@@ -647,24 +658,49 @@ Inductive step_instr:
 End
 
 Inductive get_instr:
-  (∀prog ip.
-   alookup prog ip.f = Some d ∧
-   alookup d.blocks ip.b = Some b ∧
-   ip.i < length b.body
-   ⇒
-   get_instr prog ip (el ip.i b.body))
+ (∀prog ip.
+  alookup prog ip.f = Some d ∧
+  alookup d.blocks ip.b = Some b ∧
+  ip.i = Offset idx ∧
+  idx < length b.body
+  ⇒
+  get_instr prog ip (Inl (el idx b.body))) ∧
+ (∀prog ip.
+  alookup prog ip.f = Some d ∧
+  alookup d.blocks ip.b = Some b ∧
+  ip.i = Phi_ip from_l ∧
+  b.h = Head phis landing
+  ⇒
+  get_instr prog ip (Inr (from_l, phis)))
 End
 
 Inductive step:
-  get_instr p s.ip i ∧
+ (get_instr p s.ip (Inl i) ∧
   step_instr p s i l s'
   ⇒
-  step p s l s'
+  step p s l s') ∧
+
+(* Do the phi assignments in parallel. The manual says "For the purposes of the
+ * SSA form, the use of each incoming value is deemed to occur on the edge from
+ * the corresponding predecessor block to the current block (but after any
+ * definition of an 'invoke' instruction's return value on the same edge)".
+ * So treat these two as equivalent
+ * %r1 = phi [0, %l]
+ * %r2 = phi [%r1, %l]
+ * and
+ * %r2 = phi [%r1, %l]
+ * %r1 = phi [0, %l]
+ *)
+ (get_instr p s.ip (Inr (from_l, phis)) ∧
+  map (do_phi from_l s) phis = map Some updates
+  ⇒
+  step p s Tau (inc_pc (s with locals := locals |++ updates)))
+
 End
 
 Definition get_observation_def:
   get_observation prog last_s =
-    if get_instr prog last_s.ip Exit then
+    if get_instr prog last_s.ip (Inl Exit) then
       Complete
     else if ∃s l. step prog last_s l s then
       Partial
@@ -695,20 +731,39 @@ End
 (* Instruction pointer points to an instruction *)
 Definition ip_ok_def:
   ip_ok p ip ⇔
-    ∃dec block. alookup p ip.f = Some dec ∧ alookup dec.blocks ip.b = Some block ∧ ip.i < length block.body
+    ∃dec block.
+      alookup p ip.f = Some dec ∧ alookup dec.blocks ip.b = Some block ∧
+      ((∃idx. ip.i = Offset idx ∧ idx < length block.body) ∨
+       (∃from_l. ip.i = Phi_ip from_l ∧ block.h ≠ Entry ∧ alookup dec.blocks from_l ≠ None))
+End
+
+Definition instr_to_labs_def:
+  (instr_to_labs (Br _ l1 l2) = [l1; l2]) ∧
+  (instr_to_labs _ = [])
 End
 
 Definition prog_ok_def:
   prog_ok p ⇔
-    ((* All blocks end with terminators *)
+    ((* All blocks end with terminators and terminators only appear at the end.
+      * All labels mentioned in instructions actually exist *)
      ∀fname dec bname block.
        alookup p fname = Some dec ∧
        alookup dec.blocks bname = Some block
        ⇒
-       block.body ≠ [] ∧ terminator (last block.body)) ∧
+       block.body ≠ [] ∧ terminator (last block.body) ∧
+       every (λi. ¬terminator i) (front block.body) ∧
+       every (λlab. alookup dec.blocks (Some lab) ≠ None)
+             (instr_to_labs (last block.body)) ∧
+       (∀phis lands. block.h = Head phis lands ⇒
+         every (λx. case x of Phi _ _ l => every (λ(lab, _). alookup dec.blocks lab ≠ None) l) phis)) ∧
     ((* All functions have an entry block *)
      ∀fname dec.
-       alookup p fname = Some dec ⇒ ∃block. alookup dec.blocks None = Some block) ∧
+       alookup p fname = Some dec ⇒
+       ∃block. alookup dec.blocks None = Some block ∧ block.h = Entry) ∧
+    ((* All non-entry blocks have a proper header *)
+     ∀fname dec l b.
+       alookup p fname = Some dec ∧ alookup dec.blocks (Some l) = Some b ⇒
+       b.h ≠ Entry) ∧
      (* There is a main function *)
      ∃dec. alookup p (Fn "main") = Some dec
 End
@@ -740,7 +795,7 @@ Definition is_init_state_def:
   is_init_state s (global_init : glob_var |-> ty # v) ⇔
     s.ip.f = Fn "main" ∧
     s.ip.b = None ∧
-    s.ip.i = 0 ∧
+    s.ip.i = Offset 0 ∧
     s.locals = fempty ∧
     s.stack = [] ∧
     globals_ok s ∧
diff --git a/sledge/semantics/llvm_liveScript.sml b/sledge/semantics/llvm_liveScript.sml
index 76a9d069d..5bf85a761 100644
--- a/sledge/semantics/llvm_liveScript.sml
+++ b/sledge/semantics/llvm_liveScript.sml
@@ -16,35 +16,47 @@ new_theory "llvm_live";
 numLib.prefer_num ();
 
 Definition inc_pc_def:
-  inc_pc ip = ip with i := ip.i + 1
+  inc_pc ip = ip with i := inc_bip ip.i
 End
 
 (* The set of program counters the given instruction and starting point can
  * immediately reach, within a function *)
-Definition next_ips_def:
-  (next_ips (Ret _) ip = {}) ∧
-  (next_ips (Br _ l1 l2) ip =
-    { <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧
-  (next_ips (Invoke _ _ _ _ l1 l2) ip =
-    { <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧
-  (next_ips Unreachable ip = {}) ∧
-  (next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Alloca _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Load _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Store _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧
+Definition instr_next_ips_def:
+  (instr_next_ips (Ret _) ip = {}) ∧
+  (instr_next_ips (Br _ l1 l2) ip =
+    { <| f := ip.f; b := Some l; i := Phi_ip ip.b |> | l | l ∈ {l1; l2} }) ∧
+  (instr_next_ips (Invoke _ _ _ _ l1 l2) ip =
+    { <| f := ip.f; b := Some l; i := Phi_ip ip.b |> | l | l ∈ {l1; l2} }) ∧
+  (instr_next_ips Unreachable ip = {}) ∧
+  (instr_next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Alloca _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Load _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Store _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧
   (* TODO: revisit throw when dealing with exceptions *)
-  (next_ips (Cxa_throw _ _ _) ip = {  }) ∧
-  (next_ips (Cxa_begin_catch _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Cxa_end_catch) ip = { inc_pc ip }) ∧
-  (next_ips (Cxa_get_exception_ptr _ _) ip = { inc_pc ip })
+  (instr_next_ips (Cxa_throw _ _ _) ip = {  }) ∧
+  (instr_next_ips (Cxa_begin_catch _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Cxa_end_catch) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Cxa_get_exception_ptr _ _) ip = { inc_pc ip })
+End
+
+Inductive next_ips:
+ (∀prog ip i l.
+    get_instr prog ip (Inl i) ∧
+    l ∈ instr_next_ips i ip
+    ⇒
+    next_ips prog ip l) ∧
+ (∀prog ip from_l phis.
+    get_instr prog ip (Inr (from_l, phis))
+    ⇒
+    next_ips prog ip (inc_pc ip))
 End
 
 (* The path is a list of program counters that represent a statically feasible
@@ -52,14 +64,13 @@ End
 Inductive good_path:
   (∀prog. good_path prog []) ∧
 
-  (∀ip i.
+  (∀prog ip i.
     get_instr prog ip i
     ⇒
     good_path prog [ip]) ∧
 
-  (∀prog path ip1 i1 ip2.
-    get_instr prog ip1 i1 ∧
-    ip2 ∈ next_ips i1 ip1 ∧
+  (∀prog path ip1 ip2.
+    ip2 ∈ next_ips prog ip1 ∧
     good_path prog (ip2::path)
     ⇒
     good_path prog (ip1::ip2::path))
@@ -71,65 +82,102 @@ Definition arg_to_regs_def:
 End
 
 (* The registers that an instruction uses *)
-Definition uses_def:
-  (uses (Ret (_, a)) = arg_to_regs a) ∧
-  (uses (Br a _ _) = arg_to_regs a) ∧
-  (uses (Invoke _ _ a targs _ _) =
+Definition instr_uses_def:
+  (instr_uses (Ret (_, a)) = arg_to_regs a) ∧
+  (instr_uses (Br a _ _) = arg_to_regs a) ∧
+  (instr_uses (Invoke _ _ a targs _ _) =
     arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
-  (uses Unreachable = {}) ∧
-  (uses (Sub _ _ _ _ a1 a2) =
+  (instr_uses Unreachable = {}) ∧
+  (instr_uses (Sub _ _ _ _ a1 a2) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧
-  (uses (Insertvalue _ (_, a1) (_, a2) _) =
+  (instr_uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧
+  (instr_uses (Insertvalue _ (_, a1) (_, a2) _) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Alloca _ _ (_, a)) = arg_to_regs a) ∧
-  (uses (Load _ _ (_, a)) = arg_to_regs a) ∧
-  (uses (Store (_, a1) (_, a2)) =
+  (instr_uses (Alloca _ _ (_, a)) = arg_to_regs a) ∧
+  (instr_uses (Load _ _ (_, a)) = arg_to_regs a) ∧
+  (instr_uses (Store (_, a1) (_, a2)) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Gep _ _ (_, a) targs) =
+  (instr_uses (Gep _ _ (_, a) targs) =
     arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
-  (uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧
-  (uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧
-  (uses (Icmp _ _ _ a1 a2) =
+  (instr_uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧
+  (instr_uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧
+  (instr_uses (Icmp _ _ _ a1 a2) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Call _ _ _ targs) =
+  (instr_uses (Call _ _ _ targs) =
     BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
-  (uses (Cxa_allocate_exn _ a) = arg_to_regs a) ∧
-  (uses (Cxa_throw a1 a2 a3) =
+  (instr_uses (Cxa_allocate_exn _ a) = arg_to_regs a) ∧
+  (instr_uses (Cxa_throw a1 a2 a3) =
     arg_to_regs a1 ∪ arg_to_regs a2 ∪ arg_to_regs a3) ∧
-  (uses (Cxa_begin_catch _ a) = arg_to_regs a) ∧
-  (uses (Cxa_end_catch) = {  }) ∧
-  (uses (Cxa_get_exception_ptr _ a) = arg_to_regs a)
+  (instr_uses (Cxa_begin_catch _ a) = arg_to_regs a) ∧
+  (instr_uses (Cxa_end_catch) = {  }) ∧
+  (instr_uses (Cxa_get_exception_ptr _ a) = arg_to_regs a)
+End
+
+Definition phi_uses_def:
+  phi_uses from_l (Phi _ _ entries) =
+    case alookup entries from_l of
+    | None => {}
+    | Some a => arg_to_regs a
+End
+
+Inductive uses:
+ (∀prog ip i r.
+    get_instr prog ip (Inl i) ∧
+    r ∈ instr_uses i
+    ⇒
+    uses prog ip r) ∧
+ (∀prog ip from_l phis r.
+   get_instr prog ip (Inr (from_l, phis)) ∧
+    r ∈ BIGUNION (set (map (phi_uses from_l) phis))
+    ⇒
+    uses prog ip r)
 End
 
 (* The registers that an instruction assigns *)
-Definition assigns_def:
-  (assigns (Invoke r _ _ _ _ _) = {r}) ∧
-  (assigns (Sub r _ _ _ _ _) = {r}) ∧
-  (assigns (Extractvalue r _ _) = {r}) ∧
-  (assigns (Insertvalue r _ _ _) = {r}) ∧
-  (assigns (Alloca r _ _) = {r}) ∧
-  (assigns (Load r _ _) = {r}) ∧
-  (assigns (Gep r _ _ _) = {r}) ∧
-  (assigns (Ptrtoint r _ _) = {r}) ∧
-  (assigns (Inttoptr r _ _) = {r}) ∧
-  (assigns (Icmp r _ _ _ _) = {r}) ∧
-  (assigns (Call r _ _ _) = {r}) ∧
-  (assigns (Cxa_allocate_exn r _) = {r}) ∧
-  (assigns (Cxa_begin_catch r _) = {r}) ∧
-  (assigns (Cxa_get_exception_ptr r _) = {r}) ∧
-  (assigns _ = {})
+Definition instr_assigns_def:
+  (instr_assigns (Invoke r _ _ _ _ _) = {r}) ∧
+  (instr_assigns (Sub r _ _ _ _ _) = {r}) ∧
+  (instr_assigns (Extractvalue r _ _) = {r}) ∧
+  (instr_assigns (Insertvalue r _ _ _) = {r}) ∧
+  (instr_assigns (Alloca r _ _) = {r}) ∧
+  (instr_assigns (Load r _ _) = {r}) ∧
+  (instr_assigns (Gep r _ _ _) = {r}) ∧
+  (instr_assigns (Ptrtoint r _ _) = {r}) ∧
+  (instr_assigns (Inttoptr r _ _) = {r}) ∧
+  (instr_assigns (Icmp r _ _ _ _) = {r}) ∧
+  (instr_assigns (Call r _ _ _) = {r}) ∧
+  (instr_assigns (Cxa_allocate_exn r _) = {r}) ∧
+  (instr_assigns (Cxa_begin_catch r _) = {r}) ∧
+  (instr_assigns (Cxa_get_exception_ptr r _) = {r}) ∧
+  (instr_assigns _ = {})
+End
+
+Definition phi_assigns_def:
+  phi_assigns (Phi r _ _) = {r}
+End
+
+Inductive assigns:
+ (∀prog ip i r.
+    get_instr prog ip (Inl i) ∧
+    r ∈ instr_assigns i
+    ⇒
+    assigns prog ip r) ∧
+ (∀prog ip from_l phis r.
+    get_instr prog ip (Inr (from_l, phis)) ∧
+    r ∈ BIGUNION (set (map phi_assigns phis))
+    ⇒
+    assigns prog ip r)
 End
 
 Definition live_def:
-  live prog ip ⇔
-    { r | ∃path instr.
+  live prog ip =
+    { r | ∃path.
             good_path prog (ip::path) ∧
-            get_instr prog (last (ip::path)) instr ∧
-            r ∈ uses instr ∧
-            ∀ip2 instr2. ip2 ∈ set (front (ip::path)) ∧ get_instr prog ip2 instr2 ⇒ r ∉ assigns instr2 }
+            r ∈ uses prog (last (ip::path)) ∧
+            ∀ip2. ip2 ∈ set (front (ip::path)) ⇒ r ∉ assigns prog ip2 }
 End
 
+(*
 Theorem get_instr_live:
   ∀prog ip instr.
     get_instr prog ip instr
@@ -140,6 +188,7 @@ Proof
   qexists_tac `[]` >> rw [Once good_path_cases] >>
   qexists_tac `instr` >> simp [] >> metis_tac [IN_DEF]
 QED
+*)
 
 Triviality set_rw:
   !s P. (!x. x ∈ s ⇔ P x) ⇔ s = P
@@ -148,28 +197,24 @@ Proof
 QED
 
 Theorem live_gen_kill:
-  ∀prog ip instr ip'.
-    get_instr prog ip instr
-    ⇒
-    live prog ip = BIGUNION {live prog ip' | ip' ∈ next_ips instr ip} DIFF assigns instr ∪ uses instr
+  ∀prog ip ip'.
+    live prog ip =
+    BIGUNION {live prog ip' | ip' | ip' ∈ next_ips prog ip} DIFF assigns prog ip ∪ uses prog ip
 Proof
   rw [live_def, EXTENSION] >> eq_tac >> rw []
   >- (
-    Cases_on `path` >> fs []
-    >- metis_tac [get_instr_func] >>
+    Cases_on `path` >> fs [] >>
     rename1 `ip::ip2::path` >>
     qpat_x_assum `good_path _ _` mp_tac >> simp [Once good_path_cases] >> rw [] >>
-    Cases_on `x ∈ uses instr` >> fs [] >> simp [set_rw, PULL_EXISTS] >>
-    qexists_tac `ip2` >> qexists_tac `path` >> qexists_tac `instr'` >> rw [] >>
-    metis_tac [get_instr_func])
+    Cases_on `x ∈ uses prog ip` >> fs [] >> simp [set_rw, PULL_EXISTS] >>
+    qexists_tac `ip2` >> qexists_tac `path` >> rw [])
   >- (
     fs [] >>
-    qexists_tac `ip'::path` >> qexists_tac `instr'` >> rw []
-    >- (simp [Once good_path_cases] >> metis_tac []) >>
-    metis_tac [get_instr_func])
+    qexists_tac `ip'::path` >> rw [] >>
+    simp [Once good_path_cases])
   >- (
-    qexists_tac `[]` >> qexists_tac `instr` >> rw [] >>
-    simp [Once good_path_cases] >>
+    qexists_tac `[]` >> rw [] >>
+    fs [Once good_path_cases, uses_cases, IN_DEF] >>
     metis_tac [])
 QED
 
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 895453b61..a5f199b78 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -293,19 +293,20 @@ QED
 Theorem get_instr_func:
   ∀p ip i1 i2. get_instr p ip i1 ∧ get_instr p ip i2 ⇒ i1 = i2
 Proof
-  rw [get_instr_cases] >>
-  metis_tac [optionTheory.SOME_11]
+  rw [get_instr_cases] >> fs [] >> rw [] >> fs [] >> rw [] >> fs []
 QED
 
 Theorem inc_pc_invariant:
-  ∀p s i. prog_ok p ∧ get_instr p s.ip i ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s)
+  ∀p s i. prog_ok p ∧ get_instr p s.ip (Inl i) ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s)
 Proof
   rw [state_invariant_def, inc_pc_def, allocations_ok_def, globals_ok_def,
-      stack_ok_def, frame_ok_def, heap_ok_def, EVERY_EL, ip_ok_def]
+      stack_ok_def, frame_ok_def, heap_ok_def, EVERY_EL, ip_ok_def, inc_bip_def,
+      METIS_PROVE [] ``x ∨ y ⇔ ~x ⇒ y``]
   >- (
     qexists_tac `dec` >> qexists_tac `block'` >> rw [] >>
     fs [prog_ok_def, get_instr_cases] >> res_tac >> rw [] >>
-    `s.ip.i ≠ length block'.body - 1` suffices_by decide_tac >>
+    Cases_on `s.ip.i` >> fs [] >> rw [] >> fs [inc_bip_def] >>
+    `idx ≠ length block'.body - 1` suffices_by decide_tac >>
     CCONTR_TAC >> fs [] >> rfs [LAST_EL, PRE_SUB1]) >>
   metis_tac []
 QED
@@ -327,7 +328,8 @@ Theorem allocate_invariant:
   ∀p s1 v1 t v2 h2.
     state_invariant p s1 ∧ allocate s1.heap v1 t (v2,h2) ⇒ state_invariant p (s1 with heap := h2)
 Proof
-  rw [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def]
+  rw [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def,
+      METIS_PROVE [] ``x ∨ y ⇔ ~x ⇒ y``]
   >- metis_tac [allocate_heap_ok]
   >- (fs [is_allocated_def] >> metis_tac [allocate_unchanged, SUBSET_DEF])
   >- (
@@ -347,9 +349,15 @@ Proof
   >- (fs [stack_ok_def, EVERY_EL, frame_ok_def, set_bytes_unchanged])
 QED
 
+Triviality not_none_eq:
+  !x. x ≠ None ⇔ ?y. x = Some y
+Proof
+  Cases >> rw []
+QED
+
 Theorem step_instr_invariant:
   ∀i l s2.
-    step_instr p s1 i l s2 ⇒ prog_ok p ∧ get_instr p s1.ip i ∧ state_invariant p s1
+    step_instr p s1 i l s2 ⇒ prog_ok p ∧ get_instr p s1.ip (Inl i) ∧ state_invariant p s1
     ⇒
     state_invariant p s2
 Proof
@@ -384,17 +392,39 @@ Proof
   >- ( (* Br *)
     fs [state_invariant_def] >> rw []
     >- (
-      rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
+      rw [ip_ok_def] >> fs [prog_ok_def] >>
       qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
-      last_x_assum drule >> disch_then drule >> fs [])
+      fs [get_instr_cases] >>
+      last_x_assum drule >> disch_then drule >> fs [] >> rw [] >>
+      `terminator (el idx b.body)` by metis_tac [terminator_def] >>
+      `last b.body = el idx b.body`
+      by (
+        Cases_on `idx = PRE (length b.body)` >> fs [EL_PRE_LENGTH] >>
+        `Suc idx < length b.body` by decide_tac >>
+        drule mem_el_front >> rw [] >> fs [EVERY_MEM] >>
+        metis_tac []) >>
+      qpat_x_assum `Br _ _ _ = _` (assume_tac o GSYM) >> fs [] >>
+      fs [instr_to_labs_def, not_none_eq] >>
+      metis_tac [])
     >- (fs [globals_ok_def] >> metis_tac [])
     >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
   >- ( (* Br *)
     fs [state_invariant_def] >> rw []
     >- (
-      rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
+      rw [ip_ok_def] >> fs [prog_ok_def] >>
       qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
-      last_x_assum drule >> disch_then drule >> fs [])
+      fs [get_instr_cases] >>
+      last_x_assum drule >> disch_then drule >> fs [] >> rw [] >>
+      `terminator (el idx b.body)` by metis_tac [terminator_def] >>
+      `last b.body = el idx b.body`
+      by (
+        Cases_on `idx = PRE (length b.body)` >> fs [EL_PRE_LENGTH] >>
+        `Suc idx < length b.body` by decide_tac >>
+        drule mem_el_front >> rw [] >> fs [EVERY_MEM] >>
+        metis_tac []) >>
+      qpat_x_assum `Br _ _ _ = _` (assume_tac o GSYM) >> fs [] >>
+      fs [instr_to_labs_def, not_none_eq] >>
+      metis_tac [])
     >- (fs [globals_ok_def] >> metis_tac [])
     >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
   >- (
@@ -438,21 +468,40 @@ Proof
     >- (
       fs [state_invariant_def, stack_ok_def] >> rw []
       >- (
-        rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def] >>
+        rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def, inc_bip_def] >>
         last_x_assum drule >> disch_then drule >> rw [] >>
         CCONTR_TAC >> fs [] >> rfs [LAST_EL] >>
-        Cases_on `length block'.body = s1.ip.i + 1` >> fs [PRE_SUB1] >>
+        Cases_on `length block'.body = idx + 1` >> fs [PRE_SUB1] >>
         fs [get_instr_cases] >>
         metis_tac [terminator_def])
       >- (fs [EVERY_MEM, frame_ok_def] >> metis_tac [])))
 QED
 
+Theorem step_invariant:
+  ∀p s1 l s2.
+    prog_ok p ∧ step p s1 l s2 ∧ state_invariant p s1
+    ⇒
+    state_invariant p s2
+Proof
+  rw [step_cases]
+  >- metis_tac [step_instr_invariant] >>
+  fs [get_instr_cases, inc_pc_def, inc_bip_def, state_invariant_def] >>
+  rw []
+  >- (
+    fs [ip_ok_def, prog_ok_def] >>
+    metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
+  >- (fs [globals_ok_def] >> metis_tac [])
+  >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac [])
+QED
+
 Theorem exit_no_step:
-  !p s1. get_instr p s1.ip Exit ⇒ ¬?l s2. step p s1 l s2
+  !p s1. get_instr p s1.ip (Inl Exit) ⇒ ¬?l s2. step p s1 l s2
 Proof
-  rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
-  `i = Exit` by metis_tac [get_instr_func] >>
-  rw [step_instr_cases]
+  rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``]
+  >- (
+    `i = Exit` by metis_tac [get_instr_func, sumTheory.INL_11] >>
+    rw [step_instr_cases]) >>
+  metis_tac [get_instr_func, sumTheory.sum_distinct]
 QED
 
 Definition is_call_def:
@@ -461,13 +510,17 @@ Definition is_call_def:
 End
 
 Theorem step_same_block:
-  ∀p s1 l s2 i.
-    get_instr p s1.ip i ∧ step_instr p s1 i l s2 ∧ ¬terminator i ∧ ~is_call i⇒
+  ∀p s1 l s2.
+    get_instr p s1.ip i ∧ step p s1 l s2 ∧
+    (∀i'. i = Inl i' ⇒ ¬terminator i' ∧ ¬is_call i') ⇒
     s1.ip.f = s2.ip.f ∧
     s1.ip.b = s2.ip.b ∧
-    s2.ip.i = s1.ip.i + 1
+    s2.ip.i = inc_bip s1.ip.i
 Proof
-  rw [step_instr_cases] >>
+  simp [step_cases] >>
+  rpt gen_tac >> disch_tac >> fs [inc_pc_def] >>
+  `i = Inl i'` by metis_tac [get_instr_func] >>
+  fs [step_instr_cases] >> rfs [] >>
   fs [terminator_def, is_call_def, inc_pc_def, update_result_def]
 QED
 
@@ -488,10 +541,13 @@ Definition last_step_def:
   last_step p s1 l s2 ⇔
    ∃i.
      step p s1 l s2 ∧ get_instr p s1.ip i ∧
-     (terminator i ∨ is_call i ∨ ¬∃l s3. step p s2 l s3)
+     ((∃x. i = Inr x) ∨
+      (∃i'. i = Inl i' ∧ (terminator i' ∨ is_call i')) ∨
+      ¬∃l s3. step p s2 l s3)
 End
 
-(* Run all of the instructions up-to-and-including the next Call or terminator
+(* Run all of the instructions up-to-and-including the next Call or terminator.
+ * Stop after the phis too.
  * *)
 Inductive multi_step:
 
@@ -502,7 +558,7 @@ Inductive multi_step:
 
   (∀p s1 s2 s3 i l ls.
    step p s1 l s2 ∧
-   get_instr p s1.ip i ∧
+   get_instr p s1.ip (Inl i) ∧
    ¬(terminator i ∨ is_call i) ∧
    multi_step p s2 ls s3
    ⇒
@@ -598,7 +654,10 @@ Definition instrs_left_def:
     | Some d =>
       case alookup d.blocks s.ip.b of
       | None => 0
-      | Some b => length b.body - s.ip.i
+      | Some b =>
+        case s.ip.i of
+        | Phi_ip _ => length b.body + 1
+        | Offset idx => length b.body - idx
 End
 
 Theorem extend_step_path:
@@ -635,8 +694,8 @@ Proof
       fs [finite_length] >>
       qexists_tac `n` >> rw []
       >- (
-        rw [last_step_def] >> fs [step_cases] >>
-        metis_tac []) >>
+        qpat_x_assum `step _ _ _ _` mp_tac >>
+        rw [last_step_def, step_cases] >> metis_tac []) >>
       `length (plink p' (pcons (last p') l (stopped_at s))) = Some (n + Suc 1 - 1)`
       by metis_tac [length_plink, alt_length_thm, optionTheory.OPTION_MAP_DEF] >>
       rw []
@@ -668,11 +727,10 @@ Proof
     pop_assum mp_tac >> simp [] >>
     `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
     disch_then (qspec_then `i` mp_tac) >> simp [] >>
-    pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
-    rw [] >>
-    `i' = i` by metis_tac [get_instr_func] >> rw [] >>
     drule step_same_block >> disch_then drule >> simp [] >>
-    rw [] >> fs [step_cases, get_instr_cases]) >>
+    pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
+    rw [] >> fs [get_instr_cases, inc_bip_def] >> rw [] >> fs [] >>
+    rw [inc_bip_def] >> fs []) >>
  `last path = first path1`
   by (
     unabbrev_all_tac >> simp [Once unfold_thm] >>
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index 18515eff3..a17ff8e9e 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -123,6 +123,19 @@ Proof
   fs [INJ_IFF] >> metis_tac []
 QED
 
+Theorem is_prefix_subset:
+  ∀l1 l2. l1 ≼ l2 ⇒ set l1 ⊆ set l2
+Proof
+  Induct_on `l1` >> rw [] >>
+  Cases_on `l2` >> fs [SUBSET_DEF]
+QED
+
+Theorem mem_el_front:
+  ∀n l. Suc n < length l ⇒ mem (el n l) (front l)
+Proof
+  Induct >> rw [] >> Cases_on `l` >> fs [FRONT_DEF] >> rw [] >> fs []
+QED
+
 (* ----- Theorems about log ----- *)
 
 Theorem mul_div_bound:
diff --git a/sledge/semantics/settingsScript.sml b/sledge/semantics/settingsScript.sml
index 21b8e0464..95726c64c 100644
--- a/sledge/semantics/settingsScript.sml
+++ b/sledge/semantics/settingsScript.sml
@@ -56,5 +56,8 @@ overload_on ("foldl", ``FOLDL``);
 overload_on ("foldr", ``FOLDR``);
 overload_on ("option_rel", ``OPTREL``);
 overload_on ("front", ``FRONT``);
+overload_on ("Inl", ``INL``);
+overload_on ("Inr", ``INR``);
+overload_on ("mem", ``MEM``);
 
 export_theory ();