Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp

8 files changed, 245 insertions, 182 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 4f9d008b..8b86ec5a 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -812,10 +812,10 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Pxoriw rd rs n :: k)
-  | OEluiw n _, a1 :: nil =>
+  | OEluiw n, nil =>
       do rd <- ireg_of res;
       OK (Pluiw rd n :: k)
-  | OEaddiwr0 n _, a1 :: nil =>
+  | OEaddiwr0 n, nil =>
       do rd <- ireg_of res;
       OK (Paddiw rd X0 n :: k)
   | OEseql optR0, a1 :: a2 :: nil =>
@@ -860,10 +860,10 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Pxoril rd rs n :: k)
-  | OEluil n, a1 :: nil =>
+  | OEluil n, nil =>
       do rd <- ireg_of res;
       OK (Pluil rd n :: k)
-  | OEaddilr0 n, a1 :: nil =>
+  | OEaddilr0 n, nil =>
       do rd <- ireg_of res;
       OK (Paddil rd X0 n :: k)
   | OEloadli n, nil =>
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 6d83cf5a..0be56e47 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1258,11 +1258,11 @@ Opaque Int.eq.
   { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
      exists rs'; split. eexact A. eauto with asmgen. }
   (* Expanded instructions from RTL *)
-  7,8,15,16:
+  7,14:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
-    split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl;
+    split; intros; Simpl; simpl;
     try rewrite Int.add_commut; try rewrite Int64.add_commut;
-    destruct (rs (preg_of m0)); try discriminate; eauto.
+    auto.
   1-12:
     destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
     econstructor; split; try apply exec_straight_one; simpl; eauto;
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 23e3c38e..a61e5c95 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -20,14 +20,21 @@ open Asmgen
 open DebugPrint
 open RTLpath
 open! Integers
+open Camlcoq
+
+type sop = Sop of operation * P.t list
+
+type sval = Si of RTL.instruction | Sr of P.t
 
 let reg = ref 1
 
 let node = ref 1
 
-let r2p () = Camlcoq.P.of_int !reg
+let p2i r = P.to_int r
 
-let n2p () = Camlcoq.P.of_int !node
+let r2p () = P.of_int !reg
+
+let n2p () = P.of_int !node
 
 let r2pi () =
   reg := !reg + 1;
@@ -39,30 +46,69 @@ let n2pi () =
 
 type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
-let load_hilo32 a1 dest hi lo succ is_long k =
-  if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k
+let find_or_addnmove op args rd succ map_consts =
+  let sop = Sop (op, args) in
+  match Hashtbl.find_opt map_consts sop with
+  | Some r ->
+      Sr (P.of_int r)
+  | None ->
+      Hashtbl.add map_consts sop (p2i rd);
+      Si (Iop (op, args, rd, succ))
+
+let build_head_tuple head sv =
+  match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r)
+
+let load_hilo32 dest hi lo succ map_consts =
+  let op1 = OEluiw hi in
+  if Int.eq lo Int.zero then
+    let sv = find_or_addnmove op1 [] dest succ map_consts in
+    build_head_tuple [] sv
   else
     let r = r2pi () in
-    Iop (OEluiw (hi, is_long), [ a1 ], r, n2pi ())
-    :: Iop (Oaddimm lo, [ r ], dest, succ) :: k
-
-let load_hilo64 a1 dest hi lo succ k =
-  if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k
+    let op2 = Oaddimm lo in
+    match find_or_addnmove op1 [] r (n2pi ()) map_consts with
+    | Si i ->
+        let sv = find_or_addnmove op2 [ r ] dest succ map_consts in
+        build_head_tuple [ i ] sv
+    | Sr r' ->
+        let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in
+        build_head_tuple [] sv
+
+let load_hilo64 dest hi lo succ map_consts =
+  let op1 = OEluil hi in
+  if Int64.eq lo Int64.zero then
+    let sv = find_or_addnmove op1 [] dest succ map_consts in
+    build_head_tuple [] sv
   else
     let r = r2pi () in
-    Iop (OEluil hi, [ a1 ], r, n2pi ())
-    :: Iop (Oaddlimm lo, [ r ], dest, succ) :: k
-
-let loadimm32 a1 dest n succ is_long k =
+    let op2 = Oaddlimm lo in
+    match find_or_addnmove op1 [] r (n2pi ()) map_consts with
+    | Si i ->
+        let sv = find_or_addnmove op2 [ r ] dest succ map_consts in
+        build_head_tuple [ i ] sv
+    | Sr r' ->
+        let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in
+        build_head_tuple [] sv
+
+let loadimm32 dest n succ map_consts =
   match make_immed32 n with
-  | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [ a1 ], dest, succ) :: k
-  | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k
+  | Imm32_single imm ->
+      let op1 = OEaddiwr0 imm in
+      let sv = find_or_addnmove op1 [] dest succ map_consts in
+      build_head_tuple [] sv
+  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts
 
-let loadimm64 a1 dest n succ k =
+let loadimm64 dest n succ map_consts =
   match make_immed64 n with
-  | Imm64_single imm -> Iop (OEaddilr0 imm, [ a1 ], dest, succ) :: k
-  | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k
-  | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k
+  | Imm64_single imm ->
+      let op1 = OEaddilr0 imm in
+      let sv = find_or_addnmove op1 [] dest succ map_consts in
+      build_head_tuple [] sv
+  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts
+  | Imm64_large imm ->
+      let op1 = OEloadli imm in
+      let sv = find_or_addnmove op1 [] dest succ map_consts in
+      build_head_tuple [] sv
 
 let get_opimm imm = function
   | Xoriw -> OExoriw imm
@@ -72,32 +118,42 @@ let get_opimm imm = function
   | Sltil -> OEsltil imm
   | Sltiul -> OEsltiul imm
 
-let opimm32 a1 dest n succ is_long k op opimm =
+let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r
+
+let opimm32 a1 dest n succ k op opimm map_consts =
   match make_immed32 n with
   | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm32_pair (hi, lo) ->
       let r = r2pi () in
-      load_hilo32 a1 r hi lo (n2pi ()) is_long
-        (Iop (op, [ a1; r ], dest, succ) :: k)
+      let ht = load_hilo32 r hi lo (n2pi ()) map_consts in
+      let r' = unzip_head_tuple ht r in
+      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
 
-let opimm64 a1 dest n succ k op opimm =
+let opimm64 a1 dest n succ k op opimm map_consts =
   match make_immed64 n with
   | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm64_pair (hi, lo) ->
       let r = r2pi () in
-      load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k)
+      let ht = load_hilo64 r hi lo (n2pi ()) map_consts in
+      let r' = unzip_head_tuple ht r in
+      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
   | Imm64_large imm ->
       let r = r2pi () in
-      Iop (OEloadli imm, [], r, n2pi ()) :: Iop (op, [ a1; r ], dest, succ) :: k
+      let op1 = OEloadli imm in
+      let inode = n2pi () in
+      let sv = find_or_addnmove op1 [] r inode map_consts in
+      let ht = build_head_tuple [] sv in
+      let r' = unzip_head_tuple ht r in
+      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
 
-let xorimm32 a1 dest n succ is_long k =
-  opimm32 a1 dest n succ is_long k Oxor Xoriw
+let xorimm32 a1 dest n succ k map_consts =
+  opimm32 a1 dest n succ k Oxor Xoriw map_consts
 
-let sltimm32 a1 dest n succ is_long k =
-  opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw
+let sltimm32 a1 dest n succ k map_consts =
+  opimm32 a1 dest n succ k (OEsltw None) Sltiw map_consts
 
-let sltuimm32 a1 dest n succ is_long k =
-  opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw
+let sltuimm32 a1 dest n succ k map_consts =
+  opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts
 
 let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
 
@@ -233,85 +289,101 @@ let cond_single cmp f1 f2 dest succ =
   | Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ)
   | Cge -> Iop (OEfles, [ f2; f1 ], dest, succ)
 
-let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts =
   if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm32 a1 r n (n2pi ()) false
-      (cbranch_int32s false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm32 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k
 
-let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts =
   if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm32 a1 r n (n2pi ()) false
-      (cbranch_int32u false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm32 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k
 
-let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts =
   if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm64 a1 r n (n2pi ())
-      (cbranch_int64s false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm64 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k
 
-let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts =
   if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm64 a1 r n (n2pi ())
-      (cbranch_int64u false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm64 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k
 
-let expanse_condimm_int32s cmp a1 n dest succ k =
+let expanse_condimm_int32s cmp a1 n dest succ k map_consts =
   if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
         let r = r2pi () in
-        xorimm32 a1 r n (n2pi ()) false (cond_int32s true cmp r r dest succ k)
-    | Clt -> sltimm32 a1 dest n succ false k
+        xorimm32 a1 r n (n2pi ())
+          (cond_int32s true cmp r r dest succ k)
+          map_consts
+    | Clt -> sltimm32 a1 dest n succ k map_consts
     | Cle ->
         if Int.eq n (Int.repr Int.max_signed) then
-          loadimm32 a1 dest Int.one succ false k
-        else sltimm32 a1 dest (Int.add n Int.one) succ false k
+          let ht = loadimm32 dest Int.one succ map_consts in
+          fst ht @ k
+        else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm32 a1 r n (n2pi ()) false
-          (cond_int32s false cmp a1 r dest succ k)
+        let ht = loadimm32 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int32s false cmp a1 r' dest succ k
 
-let expanse_condimm_int32u cmp a1 n dest succ k =
+let expanse_condimm_int32u cmp a1 n dest succ k map_consts =
   if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
   else
     match cmp with
-    | Clt -> sltuimm32 a1 dest n succ false k
+    | Clt -> sltuimm32 a1 dest n succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm32 a1 r n (n2pi ()) false
-          (cond_int32u false cmp a1 r dest succ k)
+        let ht = loadimm32 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int32u false cmp a1 r' dest succ k
 
-let expanse_condimm_int64s cmp a1 n dest succ k =
+let expanse_condimm_int64s cmp a1 n dest succ k map_consts =
   if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
         let r = r2pi () in
-        xorimm64 a1 r n (n2pi ()) (cond_int64s true cmp r r dest succ k)
-    | Clt -> sltimm64 a1 dest n succ k
+        xorimm64 a1 r n (n2pi ())
+          (cond_int64s true cmp r r dest succ k)
+          map_consts
+    | Clt -> sltimm64 a1 dest n succ k map_consts
     | Cle ->
         if Int64.eq n (Int64.repr Int64.max_signed) then
-          loadimm32 a1 dest Int.one succ true k
-        else sltimm64 a1 dest (Int64.add n Int64.one) succ k
+          let ht = loadimm32 dest Int.one succ map_consts in
+          fst ht @ k
+        else sltimm64 a1 dest (Int64.add n Int64.one) succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k)
+        let ht = loadimm64 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int64s false cmp a1 r' dest succ k
 
-let expanse_condimm_int64u cmp a1 n dest succ k =
+let expanse_condimm_int64u cmp a1 n dest succ k map_consts =
   if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k
   else
     match cmp with
-    | Clt -> sltuimm64 a1 dest n succ k
+    | Clt -> sltuimm64 a1 dest n succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm64 a1 r n (n2pi ()) (cond_int64u false cmp a1 r dest succ k)
+        let ht = loadimm64 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int64u false cmp a1 r' dest succ k
 
 let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
   let normal = is_normal_cmp cmp in
@@ -368,12 +440,12 @@ let write_pathmap initial esize pm' =
 let rec write_tree exp current code' new_order =
   match exp with
   | (Iop (_, _, _, succ) as inst) :: k ->
-      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
-      new_order := Camlcoq.P.of_int current :: !new_order;
+      code' := PTree.set (P.of_int current) inst !code';
+      new_order := P.of_int current :: !new_order;
       write_tree k (current - 1) code' new_order
   | (Icond (_, _, succ1, succ2, _) as inst) :: k ->
-      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
-      new_order := Camlcoq.P.of_int current :: !new_order;
+      code' := PTree.set (P.of_int current) inst !code';
+      new_order := P.of_int current :: !new_order;
       write_tree k (current - 1) code' new_order
   | [] -> ()
   | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
@@ -387,6 +459,7 @@ let expanse (sb : superblock) code pm =
   let was_exp = ref false in
   let code' = ref code in
   let pm' = ref pm in
+  let map_consts = Hashtbl.create 100 in
   Array.iter
     (fun n ->
       begin (
@@ -558,7 +631,7 @@ let rec find_last_node_reg = function
       let rec traverse_list var = function
         | [] -> ()
         | e :: t ->
-            let e' = Camlcoq.P.to_int e in
+            let e' = p2i e in
             if e' > !var then var := e';
             traverse_list var t
       in
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 4b309f5b..46d6ee73 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -96,8 +96,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEsltiw _ => op1 (default nv)
   | OEsltiuw _ => op1 (default nv)
   | OExoriw _ => op1 (bitwise nv)
-  | OEluiw _ _ => op1 (default nv)
-  | OEaddiwr0 _ _ => op1 (default nv) (* TODO gourdinl modarith impossible? *)
+  | OEluiw _ => op1 (default nv)
+  | OEaddiwr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *)
   | OEseql _ => op2 (default nv)
   | OEsnel _ => op2 (default nv)
   | OEsequl _ => op2 (default nv)
@@ -110,6 +110,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEluil _ => op1 (default nv)
   | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *)
   | OEloadli _ => op1 (default nv)
+  | OEmayundef _ => op2 (default nv)
   | OEfeqd => op2 (default nv)
   | OEfltd => op2 (default nv)
   | OEfled => op2 (default nv)
diff --git a/riscV/Op.v b/riscV/Op.v
index 8b4d444d..d902c907 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -181,8 +181,8 @@ Inductive operation : Type :=
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
   | OEsltiuw (n: int)                            (**r set-less-than unsigned immediate *)
   | OExoriw (n: int)                             (**r xor immediate *)
-  | OEluiw (n: int) (is_long: bool)              (**r load upper-immediate *)
-  | OEaddiwr0 (n: int) (is_long: bool)           (**r add immediate *)
+  | OEluiw (n: int)                              (**r load upper-immediate *)
+  | OEaddiwr0 (n: int)                           (**r add immediate *)
   | OEseql (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnel (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
   | OEsequl (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
@@ -195,6 +195,7 @@ Inductive operation : Type :=
   | OEluil (n: int64)                            (**r load upper-immediate *)
   | OEaddilr0 (n: int64)                         (**r add immediate *)
   | OEloadli (n: int64)                          (**r load an immediate int64 *)
+  | OEmayundef (is_long: bool)
   | OEfeqd                                       (**r compare equal *)
   | OEfltd                                       (**r compare less-than *)
   | OEfled                                       (**r compare less-than/equal *)
@@ -269,24 +270,18 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v
   | Some false => sem v1 vz
   end.
 
-Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val :=
+Definition may_undef_int (is_long: bool) (v1 v2: val): val :=
   if negb is_long then
     match v1 with
-    | Vint _ => sem vimm vz
+    | Vint _ => v2
     | _ => Vundef
     end
   else
     match v1 with
-    | Vlong _ => sem vimm vz
+    | Vlong _ => v2
     | _ => Vundef
     end.
 
-Definition may_undef_luil (v1: val) (n: int64): val :=
-  match v1 with
-  | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
-  | _ => Vundef
-  end.
-
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
@@ -432,8 +427,8 @@ Definition eval_operation
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
   | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
-  | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12)))
-  | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32)
+  | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12)))
+  | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
   | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64))
   | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64))
   | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
@@ -443,9 +438,10 @@ Definition eval_operation
   | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
   | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
   | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
-  | OEluil n, v1::nil => Some (may_undef_luil v1 n)
-  | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64)
+  | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
+  | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
   | OEloadli n, nil => Some (Vlong n)
+  | OEmayundef is_long, v1::v2::nil => Some (may_undef_int is_long v1 v2)
   | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
   | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
   | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2)
@@ -634,8 +630,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltiw _ => (Tint :: nil, Tint)
   | OEsltiuw _ => (Tint :: nil, Tint)
   | OExoriw _ => (Tint :: nil, Tint)
-  | OEluiw _ _ => (Tint :: nil, Tint)
-  | OEaddiwr0 _ _ => (Tint :: nil, Tint)
+  | OEluiw _ => (nil, Tint)
+  | OEaddiwr0 _ => (nil, Tint)
   | OEseql _ => (Tlong :: Tlong :: nil, Tint)
   | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
   | OEsequl _ => (Tlong :: Tlong :: nil, Tint)
@@ -645,9 +641,10 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltil _ => (Tlong :: nil, Tint)
   | OEsltiul _ => (Tlong :: nil, Tint)
   | OExoril _ => (Tlong :: nil, Tlong)
-  | OEluil _ => (Tlong :: nil, Tlong)
-  | OEaddilr0 _ => (Tlong :: nil, Tlong)
+  | OEluil _ => (nil, Tlong)
+  | OEaddilr0 _ => (nil, Tlong)
   | OEloadli _ => (nil, Tlong)
+  | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64)
   | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfled => (Tfloat :: Tfloat :: nil, Tint)
@@ -892,10 +889,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0...
   (* OEluiw *)
   - unfold may_undef_int;
-    destruct v0, is_long; simpl; trivial;
     destruct (Int.ltu _ _); cbn; trivial.
   (* OEaddiwr0 *)
-  - destruct v0, is_long; simpl; trivial.
+  - simpl; trivial.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
     destruct Val.cmpl_bool... all: destruct b...
@@ -922,11 +918,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoril *)
   - destruct v0...
   (* OEluil *)
-  - destruct v0; simpl; trivial.
+  - simpl; trivial.
   (* OEaddilr0 *)
-  - destruct v0; simpl; trivial.
+  - simpl; trivial.
   (* OEloadli *)
   - trivial.
+  (* OEmayundef *)
+  - unfold may_undef_int;
+    destruct is_long, v0, v1; simpl; trivial.
   (* OEfeqd *)
   - destruct v0; destruct v1; cbn; auto.
     destruct Float.cmp; cbn; auto.
@@ -1740,14 +1739,7 @@ Proof.
   (* OExoriw *)
   - inv H4; simpl; auto.
   (* OEluiw *)
-  - unfold may_undef_int;
-    destruct is_long;
-    inv H4; simpl; auto;
-    destruct (Int.ltu _ _); auto.
-  (* OEaddiwr0 *)
-  - unfold may_undef_int;
-    destruct is_long;
-    inv H4; simpl; auto.
+  - destruct (Int.ltu _ _); auto.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
     inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
@@ -1772,11 +1764,10 @@ Proof.
   - apply eval_cmplu_bool_inj; auto.
   (* OExoril *)
   - inv H4; simpl; auto.
-  (* OEluil *)
-  - inv H4; simpl; auto.
-  (* OEaddilr0 *)
-  - unfold may_undef_int;
-    inv H4; simpl; auto.
+  (* OEmayundef *)
+  - destruct is_long; inv H4; inv H2;
+    unfold may_undef_int; simpl; auto;
+    eapply Val.inject_ptr; eauto.
   (* OEfeqd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 4734795a..aa609e15 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -202,8 +202,8 @@ let print_operation reg pp = function
   | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
-  | OEluiw (n, _), _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
-  | OEaddiwr0 (n, _), _ -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n)
+  | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
+  | OEaddiwr0 n, _ -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n)
   | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
   | OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0)
   | OEsequl optR0, [r1;r2] -> fprintf pp "OEsequl"; (get_optR0_s Ceq reg pp r1 r2 optR0)
@@ -216,6 +216,7 @@ let print_operation reg pp = function
   | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
   | OEaddilr0 n, _ -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n)
   | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
+  | OEmayundef isl, [r1;r2] -> fprintf pp "OEmayundef (%b,%a,%a)" isl reg r1 reg r2
   | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
   | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
   | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 29389850..9b91c5a2 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -31,48 +31,44 @@ Definition make_lhsv_single (hvs: hsval) : list_hsval :=
 
 (* Immediate loads *)
 
-Definition load_hilo32 (hv1: hsval) (hi lo: int) (is_long: bool) :=
-  let hl := make_lhsv_single hv1 in
+Definition load_hilo32 (hi lo: int) :=
   if Int.eq lo Int.zero then
-    fSop (OEluiw hi is_long) hl
+    fSop (OEluiw hi) fSnil
   else
-    let hvs := fSop (OEluiw hi is_long) hl in
-    let hl' := make_lhsv_single hvs in
-    fSop (Oaddimm lo) hl'.
+    let hvs := fSop (OEluiw hi) fSnil in
+    let hl := make_lhsv_single hvs in
+    fSop (Oaddimm lo) hl.
 
-Definition load_hilo64 (hv1: hsval) (hi lo: int64) :=
-  let hl := make_lhsv_single hv1 in
+Definition load_hilo64 (hi lo: int64) :=
   if Int64.eq lo Int64.zero then
-    fSop (OEluil hi) hl
+    fSop (OEluil hi) fSnil
   else
-    let hvs := fSop (OEluil hi) hl in
+    let hvs := fSop (OEluil hi) fSnil in
     let hl := make_lhsv_single hvs in
     fSop (Oaddlimm lo) hl.
 
-Definition loadimm32 (hv1: hsval) (n: int) (is_long: bool) :=
+Definition loadimm32 (n: int) :=
   match make_immed32 n with
   | Imm32_single imm =>
-      let hl := make_lhsv_single hv1 in
-      fSop (OEaddiwr0 imm is_long) hl
-  | Imm32_pair hi lo => load_hilo32 hv1 hi lo is_long
+      fSop (OEaddiwr0 imm) fSnil
+  | Imm32_pair hi lo => load_hilo32 hi lo
   end.
 
-Definition loadimm64 (hv1: hsval) (n: int64) :=
+Definition loadimm64 (n: int64) :=
   match make_immed64 n with
   | Imm64_single imm =>
-      let hl := make_lhsv_single hv1 in
-      fSop (OEaddilr0 imm) hl
-  | Imm64_pair hi lo => load_hilo64 hv1 hi lo
+      fSop (OEaddilr0 imm) fSnil
+  | Imm64_pair hi lo => load_hilo64 hi lo
   | Imm64_large imm => fSop (OEloadli imm) fSnil
   end.
 
-Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) (is_long: bool) :=
+Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) :=
   match make_immed32 n with
   | Imm32_single imm =>
       let hl := make_lhsv_single hv1 in
       fSop (opimm imm) hl
   | Imm32_pair hi lo =>
-      let hvs := load_hilo32 hv1 hi lo is_long in
+      let hvs := load_hilo32 hi lo in
       let hl := make_lhsv_cmp false hv1 hvs in
       fSop op hl
   end.
@@ -83,7 +79,7 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
       let hl := make_lhsv_single hv1 in
       fSop (opimm imm) hl
   | Imm64_pair hi lo =>
-      let hvs := load_hilo64 hv1 hi lo in
+      let hvs := load_hilo64 hi lo in
       let hl := make_lhsv_cmp false hv1 hvs in
       fSop op hl
   | Imm64_large imm =>
@@ -92,9 +88,9 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
       fSop op hl
   end.
 
-Definition xorimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n Oxor OExoriw is_long.
-Definition sltimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltw None) OEsltiw is_long.
-Definition sltuimm32 (hv1: hsval) (n: int) (is_long: bool) := opimm32 hv1 n (OEsltuw None) OEsltiuw is_long.
+Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
+Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
+Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
 Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
 Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
 Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
@@ -155,17 +151,19 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
     match cmp with
     | Ceq | Cne =>
         let optR0 := make_optR0 true is_inv in
-        let hvs := xorimm32 hv1 n false in
+        let hvs := xorimm32 hv1 n in
         let hl := make_lhsv_cmp false hvs hvs in
         cond_int32s cmp hl optR0
-    | Clt => sltimm32 hv1 n false
+    | Clt => sltimm32 hv1 n
     | Cle =>
         if Int.eq n (Int.repr Int.max_signed) then
-          loadimm32 hv1 Int.one false
-        else sltimm32 hv1 (Int.add n Int.one) false
+          let hvs := loadimm32 Int.one in
+          let hl := make_lhsv_cmp false hv1 hvs in
+          fSop (OEmayundef false) hl
+        else sltimm32 hv1 (Int.add n Int.one)
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm32 hv1 n false in
+        let hvs := loadimm32 n in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int32s cmp hl optR0
     end.
@@ -178,10 +176,10 @@ Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) :=
     cond_int32u cmp hl optR0
   else
     match cmp with
-    | Clt => sltuimm32 hv1 n false
+    | Clt => sltuimm32 hv1 n
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm32 hv1 n false in
+        let hvs := loadimm32 n in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int32u cmp hl optR0
     end.
@@ -202,11 +200,13 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
     | Clt => sltimm64 hv1 n
     | Cle =>
         if Int64.eq n (Int64.repr Int64.max_signed) then
-          loadimm32 hv1 Int.one true
+          let hvs := loadimm32 Int.one in
+          let hl := make_lhsv_cmp false hv1 hvs in
+          fSop (OEmayundef true) hl
         else sltimm64 hv1 (Int64.add n Int64.one)
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm64 hv1 n in
+        let hvs := loadimm64 n in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int64s cmp hl optR0
     end.
@@ -222,7 +222,7 @@ Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
     | Clt => sltuimm64 hv1 n
     | _ =>
         let optR0 := make_optR0 false is_inv in
-        let hvs := loadimm64 hv1 n in
+        let hvs := loadimm64 n in
         let hl := make_lhsv_cmp is_inv hv1 hvs in
         cond_int64u cmp hl optR0
     end.
@@ -403,7 +403,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm32 hv1 n false in
+        let hvs := loadimm32 n in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
         Some (cond, lhsv))
@@ -415,7 +415,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm32 hv1 n false in
+        let hvs := loadimm32 n in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
          Some (cond, lhsv))
@@ -441,7 +441,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm64 hv1 n in
+        let hvs := loadimm64 n in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
         Some (cond, lhsv))
@@ -453,7 +453,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm64 hv1 n in
+        let hvs := loadimm64 n in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
         Some (cond, lhsv))
@@ -850,7 +850,6 @@ Proof.
     try rewrite OKv1;
     try rewrite OK2;
     try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst;
-    try rewrite xor_neg_ltle_cmp; trivial;
     unfold Val.cmp, may_undef_int, zero32, Val.add; simpl;
     destruct v; auto.
   all:
@@ -904,12 +903,12 @@ Proof.
     rewrite HMEM;
     unfold may_undef_int, Val.cmpu;
     destruct v; simpl; auto;
-    try rewrite EQIMM; try destruct (Archi.ptr64); simpl;
+    try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl;
     try rewrite ltu_12_wordsize; trivial;
-    try rewrite Int.add_commut, Int.add_zero_l;
+    try rewrite Int.add_commut, Int.add_zero_l in *;
     try destruct (Int.ltu _ _) eqn:EQLTU; simpl;
-    try rewrite EQLTU; simpl;
-    trivial.
+    try rewrite EQLTU; simpl; try rewrite EQIMM;
+    try rewrite EQARCH; trivial.
 Qed.
 
 Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall
@@ -1016,12 +1015,11 @@ Proof.
     try erewrite !fsi_sreg_get_correct; eauto;
     try rewrite OKv1;
     try rewrite OK2;
-    unfold may_undef_luil;
     try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst;
     try fold (Val.cmpl Clt v (Vlong imm));
     try rewrite xor_neg_ltge_cmpl; trivial;
     try rewrite xor_neg_ltle_cmpl; trivial;
-    unfold Val.cmpl, may_undef_luil, Val.addl;
+    unfold Val.cmpl, Val.addl;
     try rewrite xorl_zero_eq_cmpl; trivial;
     try rewrite optbool_mktotal; trivial;
     unfold may_undef_int, zero32, Val.add; simpl;
@@ -1301,7 +1299,7 @@ Proof.
     try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
     try apply Int.same_if_eq in EQLO; simpl; trivial;
     try apply Int64.same_if_eq in EQLO; simpl; trivial;
-    unfold may_undef_int, may_undef_luil; 
+    unfold may_undef_int; 
     try erewrite !fsi_sreg_get_correct; eauto;
     try rewrite OKv1; simpl; trivial;
     try destruct v; try rewrite H;
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 97f3ff61..d50bd00f 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -27,24 +27,18 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2
   | Some false => sem v1 vz
   end.
 
-Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval :=
+Definition may_undef_int (is_long: bool) (v1 v2: aval): aval :=
   if negb is_long then
     match v1 with
-    | I _ => sem vimm vz
+    | I _ => v2
     | _ => Ifptr Ptop
     end
   else
     match v1 with
-    | L _ => sem vimm vz
+    | L _ => v2
     | _ => Ifptr Ptop
     end.
 
-Definition may_undef_luil (v1: aval) (n: int64): aval :=
-  match v1 with
-  | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
-  | _ => Ifptr Ptop
-  end.
-
 Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
@@ -223,8 +217,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
   | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n))
   | OExoriw n, v1::nil => xor v1 (I n)
-  | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12))
-  | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32
+  | OEluiw n, nil => shl (I n) (I (Int.repr 12))
+  | OEaddiwr0 n, nil => add (I n) zero32
   | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64)
   | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64)
   | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64)
@@ -234,9 +228,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
   | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
   | OExoril n, v1::nil => xorl v1 (L n)
-  | OEluil n, v1::nil => may_undef_luil v1 n
-  | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64
+  | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
+  | OEaddilr0 n, nil => addl (L n) zero64
   | OEloadli n, nil => L (n)
+  | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2
   | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
   | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2)
   | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2)
@@ -464,14 +459,18 @@ Proof.
   1,2,3: apply eval_cmp_sound; auto.
   unfold Val.cmp; apply of_optbool_sound; eauto with va.
   unfold Val.cmpu; apply of_optbool_sound; eauto with va.
-  unfold zero32; simpl; eauto with va.
-
-  1,2,11,12:
-    try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64;
-    try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1;
-    inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va;
-    try apply vmatch_ifptr_i; try apply vmatch_ifptr_l.
-
+  
+  simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1;
+  try apply vmatch_ifptr_undef.
+  10:
+    simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
+    apply vmatch_ifptr_l.
+  1,10: simpl; eauto with va.
+  9:
+    unfold Op.may_undef_int, may_undef_int; destruct is_long;
+    simpl; inv H0; inv H1; eauto with va; inv H;
+    apply vmatch_ifptr_p; eauto with va.
+  
   3,4,6: apply eval_cmplu_sound; auto.
   1,2,3: apply eval_cmpl_sound; auto.
   unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va.