[sledge] Fix translation of Invoke retpolines

Summary:
A previous rebase fumble sometimes led to the wrong arguments being
passed to retpolines of Invoke instructions.

Reviewed By: ngorogiannis

Differential Revision: D15323950

fbshipit-source-id: f6eb6fbe2

sledge/src/llair/frontend.ml

@@ -825,7 +825,7 @@ let jump_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list =
 type code = Llair.inst list * Llair.term * Llair.block list
 
 let pp_code fs (insts, term, blocks) =
-  Format.fprintf fs "@[<hv>@[%a%t@]%t@[<hv>%a@]@]"
+  Format.fprintf fs "@[<hv>@,@[%a%t@]%t@[<hv>%a@]@]"
     (List.pp "@ " Llair.Inst.pp)
     insts
     (fun fs ->
@@ -1048,8 +1048,8 @@ let xlate_instr :
             | _ -> false
           in
           let return, blocks =
-            if not (need_return_trampoline instr return_blk) then
             let args = trampoline_args x instr return_blk in
+            if not (need_return_trampoline instr return_blk) then
               (Llair.Jump.mk return_dst args, [])
             else
               let lbl = name ^ ".ret" in

sledge/src/llair/llair.ml

@@ -248,7 +248,7 @@ module Jump = struct
   let pp = pp_jump
 
   let invariant ?(accept_return = false) jmp =
-    Invariant.invariant [%here] jmp [%sexp_of: t]
+    Invariant.invariant [%here] (jmp, accept_return) [%sexp_of: t * bool]
     @@ fun () ->
     let {dst= {params; parent}; args} = jmp in
     if parent == dummy_func then