Proof of fsval condition cmp ok

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, nil =>
+  | OEluiw n _, a1 :: nil =>
       do rd <- ireg_of res;
       OK (Pluiw rd n :: k)
-  | OEaddiwr0 n, nil =>
+  | OEaddiwr0 n _, a1 :: 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, nil =>
+  | OEluil n, a1 :: nil =>
       do rd <- ireg_of res;
       OK (Pluil rd n :: k)
-  | OEaddilr0 n, nil =>
+  | OEaddilr0 n, a1 :: nil =>
       do rd <- ireg_of res;
       OK (Paddil rd X0 n :: k)
   | OEloadli n, nil =>

riscV/Asmgenproof1.v

@@ -1258,10 +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: econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl; rewrite Int.add_commut; auto.
-  13: econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl; rewrite Int64.add_commut; auto.
+  7,8,15,16:
+    econstructor; split; try apply exec_straight_one; simpl; eauto;
+    split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl;
+    try rewrite Int.add_commut; try rewrite Int64.add_commut;
+    destruct (rs (preg_of m0)); try discriminate; eauto.
   all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
   econstructor; split; try apply exec_straight_one; simpl; eauto;
   split; intros; Simpl.

riscV/ExpansionOracle.ml

@@ -35,29 +35,29 @@ let n2pi () =
 
 type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
-let load_hilo32 dest hi lo succ k =
-  if Int.eq lo Int.zero then Iop (OEluiw hi, [], dest, succ) :: k
+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
   else
-    Iop (OEluiw hi, [], dest, n2pi ())
+    Iop (OEluiw (hi, is_long), [a1], dest, n2pi ())
     :: Iop (Oaddimm lo, [ dest ], dest, succ)
     :: k
 
-let load_hilo64 dest hi lo succ k =
-  if Int64.eq lo Int64.zero then Iop (OEluil hi, [], 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
   else
-    Iop (OEluil hi, [], dest, n2pi ())
+    Iop (OEluil hi, [a1], dest, n2pi ())
     :: Iop (Oaddlimm lo, [ dest ], dest, succ)
     :: k
 
-let loadimm32 dest n succ k =
+let loadimm32 a1 dest n succ is_long k =
   match make_immed32 n with
-  | Imm32_single imm -> Iop (OEaddiwr0 imm, [], dest, succ) :: k
-  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k
+  | 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
 
-let loadimm64 dest n succ k =
+let loadimm64 a1 dest n succ k =
   match make_immed64 n with
-  | Imm64_single imm -> Iop (OEaddilr0 imm, [], dest, succ) :: k
-  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k
+  | 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
 
 let get_opimm imm = function
@@ -68,12 +68,12 @@ let get_opimm imm = function
   | Sltil -> OEsltil imm
   | Sltiul -> OEsltiul imm
 
-let opimm32 a1 dest n succ k op opimm =
+let opimm32 a1 dest n succ is_long k op opimm =
   match make_immed32 n with
   | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm32_pair (hi, lo) ->
       reg := !reg + 1;
-      load_hilo32 (r2p ()) hi lo (n2pi ())
+      load_hilo32 a1 (r2p ()) hi lo (n2pi ()) is_long
         (Iop (op, [ a1; r2p () ], dest, succ) :: k)
 
 let opimm64 a1 dest n succ k op opimm =
@@ -81,7 +81,7 @@ let opimm64 a1 dest n succ k op opimm =
   | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm64_pair (hi, lo) ->
       reg := !reg + 1;
-      load_hilo64 (r2p ()) hi lo (n2pi ())
+      load_hilo64 a1 (r2p ()) hi lo (n2pi ())
         (Iop (op, [ a1; r2p () ], dest, succ) :: k)
   | Imm64_large imm ->
       reg := !reg + 1;
@@ -89,11 +89,11 @@ let opimm64 a1 dest n succ k op opimm =
       :: Iop (op, [ a1; r2p () ], dest, succ)
       :: k
 
-let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw
+let xorimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k Oxor Xoriw
 
-let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw
+let sltimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw
 
-let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw
+let sltuimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw
 
 let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
 
@@ -233,28 +233,28 @@ let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
   if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm32 (r2p ()) n (n2pi ())
+    loadimm32 a1 (r2p ()) n (n2pi ()) false
       (cbranch_int32s false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
   if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm32 (r2p ()) n (n2pi ())
+    loadimm32 a1 (r2p ()) n (n2pi ()) false
       (cbranch_int32u false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
   if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm64 (r2p ()) n (n2pi ())
+    loadimm64 a1 (r2p ()) n (n2pi ())
       (cbranch_int64s false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
   if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
   else (
     reg := !reg + 1;
-    loadimm64 (r2p ()) n (n2pi ())
+    loadimm64 a1 (r2p ()) n (n2pi ())
       (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 k))
 
 let expanse_condimm_int32s cmp a1 n dest succ k =
@@ -262,25 +262,25 @@ let expanse_condimm_int32s cmp a1 n dest succ k =
   else
     match cmp with
     | Ceq | Cne ->
-        xorimm32 a1 dest n (n2pi ())
+        xorimm32 a1 dest n (n2pi ()) false
           (cond_int32s true cmp dest dest dest succ k)
-    | Clt -> sltimm32 a1 dest n succ k
+    | Clt -> sltimm32 a1 dest n succ false k
     | Cle ->
-        if Int.eq n (Int.repr Int.max_signed) then loadimm32 dest Int.one succ k
-        else sltimm32 a1 dest (Int.add n Int.one) succ k
+        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
     | _ ->
         reg := !reg + 1;
-        loadimm32 (r2p ()) n (n2pi ())
+        loadimm32 a1 (r2p ()) n (n2pi ()) false
           (cond_int32s false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int32u cmp a1 n dest succ k =
   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 k
+    | Clt -> sltuimm32 a1 dest n succ false k
     | _ ->
         reg := !reg + 1;
-        loadimm32 (r2p ()) n (n2pi ())
+        loadimm32 a1 (r2p ()) n (n2pi ()) false
           (cond_int32u false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int64s cmp a1 n dest succ k =
@@ -294,11 +294,11 @@ let expanse_condimm_int64s cmp a1 n dest succ k =
     | Clt -> sltimm64 a1 dest n succ k
     | Cle ->
         if Int64.eq n (Int64.repr Int64.max_signed) then
-          loadimm32 dest Int.one succ k
+          loadimm32 a1 dest Int.one succ true k
         else sltimm64 a1 dest (Int64.add n Int64.one) succ k
     | _ ->
         reg := !reg + 1;
-        loadimm64 (r2p ()) n (n2pi ())
+        loadimm64 a1 (r2p ()) n (n2pi ())
           (cond_int64s false cmp a1 (r2p ()) dest succ k)
 
 let expanse_condimm_int64u cmp a1 n dest succ k =
@@ -308,7 +308,7 @@ let expanse_condimm_int64u cmp a1 n dest succ k =
     | Clt -> sltuimm64 a1 dest n succ k
     | _ ->
         reg := !reg + 1;
-        loadimm64 (r2p ()) n (n2pi ())
+        loadimm64 a1 (r2p ()) n (n2pi ())
           (cond_int64u false cmp a1 (r2p ()) dest succ k)
 
 let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
@@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order =
   | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
 
 let expanse (sb : superblock) code pm =
-  debug_flag := true;
+  (*debug_flag := true;*)
   let new_order = ref [] in
   let liveins = ref sb.liveins in
   let exp = ref [] in
@@ -510,7 +510,8 @@ let expanse (sb : superblock) code pm =
     sb.instructions;
   sb.instructions <- Array.of_list (List.rev !new_order);
   sb.liveins <- !liveins;
-  debug_flag := false;
+  print_ptree_regset !liveins;
+  (*debug_flag := false;*)
   (!code', !pm')
 
 let rec find_last_node_reg = function

riscV/NeedOp.v

@@ -93,23 +93,23 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEsneuw _ => op2 (default nv)
   | OEsltw _ => op2 (default nv)
   | OEsltuw _ => op2 (default nv)
-  | OEsltiw n => op1 (default nv)
-  | OEsltiuw n => op1 (default nv)
-  | OExoriw n => op1 (bitwise nv)
-  | OEluiw n => op1 (default nv)
-  | OEaddiwr0 n => op1 (modarith nv)
+  | OEsltiw _ => op1 (default nv)
+  | OEsltiuw _ => op1 (default nv)
+  | OExoriw _ => op1 (bitwise nv)
+  | OEluiw _ _ => op1 (default nv)
+  | OEaddiwr0 _ _ => op1 (default nv) (* TODO gourdinl modarith impossible? *)
   | OEseql _ => op2 (default nv)
   | OEsnel _ => op2 (default nv)
   | OEsequl _ => op2 (default nv)
   | OEsneul _ => op2 (default nv)
   | OEsltl _ => op2 (default nv)
   | OEsltul _ => op2 (default nv)
-  | OEsltil n => op1 (default nv)
-  | OEsltiul n => op1 (default nv)
-  | OExoril n => op1 (default nv)
-  | OEluil n => op1 (default nv)
-  | OEaddilr0 n => op1 (modarith nv)
-  | OEloadli n => op1 (default nv)
+  | OEsltil _ => op1 (default nv)
+  | OEsltiul _ => op1 (default nv)
+  | OExoril _ => op1 (default nv)
+  | OEluil _ => op1 (default nv)
+  | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *)
+  | OEloadli _ => op1 (default nv)
   | OEfeqd => op2 (default nv)
   | OEfltd => op2 (default nv)
   | OEfled => op2 (default nv)
@@ -184,8 +184,6 @@ Proof.
 - apply shrimm_sound; auto.
 - apply shruimm_sound; auto.
 - apply xor_sound; auto with na.
-- auto with na.
-- auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:

riscV/Op.v

@@ -173,19 +173,19 @@ Inductive operation : Type :=
   (* Expansed conditions *)
   | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
-  | OEsequw (optR0: option bool)                  (**r [rd <- rs1 == rs2] unsigned *)
-  | OEsneuw (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
+  | OEsequw (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneuw (optR0: option bool)                 (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltw (optR0: option bool)                  (**r set-less-than *)
   | OEsltuw (optR0: option bool)                 (**r set-less-than unsigned *)
   | 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)                              (**r load upper-immediate *)
-  | OEaddiwr0 (n: int)                           (**r add immediate *)
+  | OEluiw (n: int) (is_long: bool)              (**r load upper-immediate *)
+  | OEaddiwr0 (n: int) (is_long: bool)           (**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 *)
-  | OEsneul (optR0: option bool)                  (**r [rd <- rs1 != rs2] unsigned *)
+  | OEsequl (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
+  | OEsneul (optR0: option bool)                 (**r [rd <- rs1 != rs2] unsigned *)
   | OEsltl (optR0: option bool)                  (**r set-less-than *)
   | OEsltul (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltil (n: int64)                           (**r set-less-than immediate *)
@@ -263,6 +263,24 @@ 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 :=
+  if negb is_long then
+    match v1 with
+    | Vint _ => sem vimm vz
+    | _ => Vundef
+    end
+  else
+    match v1 with
+    | Vlong _ => sem vimm vz
+    | _ => 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
@@ -404,8 +422,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, nil => Some(Vint (Int.shl n (Int.repr 12)))
-  | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
+  | 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)
   | 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))
@@ -415,8 +433,8 @@ 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, nil => Some(Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
-  | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
+  | 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)
   | OEloadli n, nil => Some (Vlong n)
   | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
   | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
@@ -605,8 +623,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltiw _ => (Tint :: nil, Tint)
   | OEsltiuw _ => (Tint :: nil, Tint)
   | OExoriw _ => (Tint :: nil, Tint)
-  | OEluiw _ => (nil, Tint)
-  | OEaddiwr0 _ => (nil, Tint)
+  | OEluiw _ _ => (Tint :: nil, Tint)
+  | OEaddiwr0 _ _ => (Tint :: nil, Tint)
   | OEseql _ => (Tlong :: Tlong :: nil, Tint)
   | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
   | OEsequl _ => (Tlong :: Tlong :: nil, Tint)
@@ -616,8 +634,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltil _ => (Tlong :: nil, Tint)
   | OEsltiul _ => (Tlong :: nil, Tint)
   | OExoril _ => (Tlong :: nil, Tlong)
-  | OEluil _ => (nil, Tlong)
-  | OEaddilr0 _ => (nil, Tlong)
+  | OEluil _ => (Tlong :: nil, Tlong)
+  | OEaddilr0 _ => (Tlong :: nil, Tlong)
   | OEloadli _ => (nil, Tlong)
   | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
@@ -857,9 +875,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoriw *)
   - destruct v0...
   (* OEluiw *)
-  - trivial.
+  - unfold may_undef_int;
+    destruct v0, is_long; simpl; trivial;
+    destruct (Int.ltu _ _); cbn; trivial.
   (* OEaddiwr0 *)
-  - trivial.
+  - destruct v0, is_long; simpl; trivial.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
     destruct Val.cmpl_bool... all: destruct b...
@@ -886,9 +906,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoril *)
   - destruct v0...
   (* OEluil *)
-  - trivial.
+  - destruct v0; simpl; trivial.
   (* OEaddilr0 *)
-  - trivial.
+  - destruct v0; simpl; trivial.
   (* OEloadli *)
   - trivial.
   (* OEfeqd *)
@@ -1691,6 +1711,15 @@ Proof.
   - apply eval_cmpu_bool_inj; auto.
   (* 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.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
     inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
@@ -1715,6 +1744,11 @@ 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.
   (* OEfeqd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.

riscV/PrintOp.ml

@@ -192,8 +192,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)
   | OEsltl optR0, [r1;r2] -> fprintf pp "OEsltl"; (get_optR0_s Clt reg pp r1 r2 optR0)

riscV/ValueAOp.v

@@ -27,6 +27,24 @@ 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 :=
+  if negb is_long then
+    match v1 with
+    | I _ => sem vimm vz
+    | _ => Ifptr Ptop
+    end
+  else
+    match v1 with
+    | L _ => sem vimm vz
+    | _ => 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
@@ -172,8 +190,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, nil => I (Int.shl n (Int.repr 12))
-  | OEaddiwr0 n, nil => add (I n) zero32
+  | 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
   | 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)
@@ -183,8 +201,8 @@ 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, nil => L (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
-  | OEaddilr0 n, nil => addl (L n) zero64
+  | OEluil n, v1::nil => may_undef_luil v1 n
+  | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64
   | OEloadli n, nil => L (n)
   | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
   | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2)
@@ -340,6 +358,13 @@ Proof.
   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.
+
   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.