Expansion of Ccompimm in RTL [Admitted checker]

8 files changed, 383 insertions, 4 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index b431d63d..8d1e3a5c 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -393,7 +393,14 @@ Definition transl_cond_op
 
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
-
+  
+Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) :=
+  match optR0 with
+  | None => sem r1 r2
+  | Some true => sem X0 r1
+  | Some false => sem r1 X0
+  end.
+  
 Definition transl_op
               (op: operation) (args: list mreg) (res: mreg) (k: code) :=
   match op, args with
@@ -708,7 +715,36 @@ Definition transl_op
   | Ocmp cmp, _ =>
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
-
+      
+  | OEseqw optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Pseqw rd) rs1 rs2 :: k)
+  | OEsnew optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k)
+  | OEsltw optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psltw rd) rs1 rs2 :: k)
+  | OEsltiw n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltiw rd rs n :: k)
+  | OExoriw n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Pxoriw rd rs n :: k)
+  | OEluiw n, nil =>
+      do rd <- ireg_of res;
+      OK (Pluiw rd n :: k)
+  | OEaddiwr0 n, nil =>
+      do rd <- ireg_of res;
+      OK (Paddiw rd X0 n :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 8e9f022c..8aa3d3b2 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -292,6 +292,9 @@ Opaque Int.eq.
 - apply opimm64_label; intros; exact I.
 - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
 - eapply transl_cond_op_label; eauto.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
 Qed.
 
 Remark indexed_memory_access_label:
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index d2255e66..06b33592 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1138,6 +1138,17 @@ Opaque Int.eq.
 - (* cond *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
+- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
+  econstructor; split; try apply exec_straight_one; simpl; eauto;
+  split; intros; Simpl.
+- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
+  econstructor; split; try apply exec_straight_one; simpl; eauto;
+  split; intros; Simpl.
+- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
+  econstructor; split; try apply exec_straight_one; simpl; eauto;
+  split; intros; Simpl.
+- econstructor; split; try apply exec_straight_one; simpl; eauto;
+  split; intros; Simpl. rewrite Int.add_commut. auto.
 Qed.
 
 (** Memory accesses *)
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
new file mode 100644
index 00000000..15a418fd
--- /dev/null
+++ b/riscV/ExpansionOracle.ml
@@ -0,0 +1,174 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+open RTLpathLivegenaux
+open RTLpathCommon
+open Datatypes
+open Maps
+open RTL
+open Op
+open Asmgen
+open DebugPrint
+open PrintRTL
+open! Integers
+
+let reg = ref 1
+let node = ref 1
+
+let r2p () = Camlcoq.P.of_int !reg
+let n2p () = Camlcoq.P.of_int !node
+let n2pi () = node := !node + 1; n2p()
+
+type immt = Xori | Slti
+
+let load_hilo32 dest hi lo succ k =
+  if Int.eq lo Int.zero then
+    Iop (OEluiw hi, [], dest, succ) :: k
+  else (
+      Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k)
+
+let loadimm32 dest n succ 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
+
+let get_opimm imm = function
+  | Xori -> OExoriw imm
+  | Slti -> OEsltiw imm
+
+let opimm32 a1 dest n succ 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()) (Iop (op, [a1;r2p()], dest, succ) :: k)
+
+let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xori
+let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Slti
+
+let cond_int32s_x0 cmp a1 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k
+  | Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k
+  | Clt -> Iop (OEsltw (Some false), [a1;a1], dest, succ) :: k
+  | Cle -> Iop (OEsltw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltw (Some true), [a1;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let cond_int32s_reg cmp a1 a2 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k
+  | Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k
+  | Clt -> Iop (OEsltw None, [a1;a2], dest, succ) :: k
+  | Cle -> Iop (OEsltw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltw None, [a2;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let expanse_condimm_int32s cmp a1 n dest succ k =
+  if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k else
+  match cmp with
+  | Ceq | Cne ->
+      xorimm32 a1 dest n (n2pi()) (cond_int32s_x0 cmp dest dest succ k)
+  | Clt -> sltimm32 a1 dest n succ 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
+  | _   -> reg := !reg + 1;
+           loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k)
+
+let rec write_tree exp n code' =
+  match exp with
+  | (Iop (_,_,_,succ)) as inst :: k ->
+      print_instruction stderr (0,inst);
+      Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);
+      code' := PTree.set n inst !code';
+      Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);
+      write_tree k (Camlcoq.P.of_int ((Camlcoq.P.to_int n) + 1)) code'
+  | _ -> !code'
+
+let get_regindent = function
+  | Coq_inr _ -> []
+  | Coq_inl r -> [r]
+  
+let get_regs_inst = function
+  | Inop (_) -> []
+  | Iop (_,args,dest,_) -> dest :: args
+  | Iload (_,_,_,args,dest,_) -> dest :: args
+  | Istore (_,_,args,src,_) -> src :: args
+  | Icall (_,t,args,dest,_) -> dest :: ((get_regindent t) @ args)
+  | Itailcall (_,t,args) -> (get_regindent t) @ args
+  | Ibuiltin (_,args,dest,_) ->
+      (AST.params_of_builtin_res dest) @
+      AST.params_of_builtin_args args
+  | Icond (_,args,_,_,_) -> args
+  | Ijumptable (arg,_) -> [arg]
+  | Ireturn (Some r) -> [r]
+  | _ -> []
+
+let generate_head_order n start_node new_order =
+  Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n) (Camlcoq.P.to_int start_node) !node;
+  for i = !node downto (Camlcoq.P.to_int start_node) do
+    new_order := !new_order @ [Camlcoq.P.of_int i];
+  done;
+  new_order := n :: !new_order
+
+let expanse (sb: superblock) code =
+  debug_flag := true;
+  let new_order = ref [] in
+  let code' = ref code in
+  Array.iter (fun n ->
+    let inst = get_some @@ PTree.get n code in
+    match inst with
+    | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
+      Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;
+      Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;
+      Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);
+      Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);
+      debug "[EXPANSION] Replace this:\n";
+      print_instruction stderr (0,inst);
+      debug "[EXPANSION] With:\n";
+      let start_node = Camlcoq.P.of_int (!node + 1) in
+      let exp = expanse_condimm_int32s c a1 imm dest succ [] in
+      code' := write_tree (List.rev exp) start_node code';
+      let first = Inop (n2pi()) in
+      code' := PTree.set n first !code';
+      generate_head_order n start_node new_order;
+      (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
+      (*entry := n2p()*)
+    (*| Icond (cond,args,ifso,ifnot,info) -> (code' :=
+        match cond, args with
+        | Ccompimm (c, imm), a1 :: nil ->
+            expanse_condimm_int32s cond a1 imm info ifso ifnot
+            PTree.set n (Icond (cond,args,ifso,ifnot,info)) !code'
+        | (_, _) -> !code'*)
+        (*PTree.set node*))
+    | _ -> new_order := !new_order @ [n]
+  ) sb.instructions;
+  sb.instructions <- Array.of_list !new_order;
+  (*print_arrayp sb.instructions;*)
+  debug_flag := false;
+  !code'
+
+let rec find_last_node_reg = function
+  | [] -> ()
+  | (pc, i) :: k ->
+    let rec traverse_list var = function
+    | [] -> ()
+    | e :: t ->
+        (let e' = Camlcoq.P.to_int e in
+        if e' > !var then var := e';
+        traverse_list var t) in
+    traverse_list node [pc];
+    traverse_list reg (get_regs_inst i);
+    find_last_node_reg k
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 117bbcb4..da406d8a 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -87,6 +87,13 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
   | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
   | Ocmp c => needs_of_condition c
+  | OEseqw _ => op2 (default nv)
+  | OEsnew _ => op2 (default nv)
+  | OEsltw _ => op2 (default nv)
+  | OEsltiw n => op1 (default nv)
+  | OExoriw n => op1 (bitwise nv)
+  | OEluiw n => op1 (default nv)
+  | OEaddiwr0 n => op1 (modarith nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -154,6 +161,8 @@ Proof.
 - apply shlimm_sound; auto.
 - apply shrimm_sound; auto.
 - apply shruimm_sound; auto.
+- apply xor_sound; auto with na.
+- auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/riscV/Op.v b/riscV/Op.v
index 2271ecd2..c55479ff 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -152,7 +152,14 @@ Inductive operation : Type :=
   | Osingleoflong            (**r [rd = float32_of_signed_long(r1)] *)
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
-  | Ocmp (cond: condition).  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] (pseudo) *)
+  | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] (pseudo) *)
+  | OEsltw (optR0: option bool)                  (**r set-less-than *)
+  | OEsltiw (n: int)                             (**r set-less-than immediate *)
+  | OExoriw (n: int)                             (**r xor immediate *)
+  | OEluiw (n: int)                              (**r load upper-immediate *)
+  | OEaddiwr0 (n: int).                          (**r add immediate *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -179,8 +186,9 @@ Defined.
 
 Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition; intros.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros.
   decide equality.
+  all: destruct optR0, optR1; decide equality.
 Defined.
 
 (* Alternate definition: 
@@ -203,6 +211,15 @@ Global Opaque eq_condition eq_addressing eq_operation.
   to lists of values.  Return [None] when the computation can trigger an
   error, e.g. integer division by zero.  [eval_condition] returns a boolean,
   [eval_operation] and [eval_addressing] return a value. *)
+  
+Definition zero32 := (Vint Int.zero).
+  
+Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 vz: val): B :=
+  match optR0 with
+  | None => sem v1 v2
+  | Some true => sem vz v1
+  | Some false => sem v1 vz
+  end.
 
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
@@ -318,6 +335,13 @@ Definition eval_operation
   | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
+  | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
+  | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
+  | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32)
+  | OEsltiw n, v1::nil => Some (Val.cmp 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)
   | _, _ => None
   end.
 
@@ -474,6 +498,13 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Osingleoflongu => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
+  | OEseqw _ => (Tint :: Tint :: nil, Tint)
+  | OEsnew _ => (Tint :: Tint :: nil, Tint)
+  | OEsltw _ => (Tint :: Tint :: nil, Tint)
+  | OEsltiw _ => (Tint :: nil, Tint)
+  | OExoriw _ => (Tint :: nil, Tint)
+  | OEluiw _ => (nil, Tint)
+  | OEaddiwr0 _ => (nil, Tint)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -680,6 +711,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
+  
+- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+  destruct Val.cmpu_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+  destruct Val.cmpu_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmp;
+  destruct Val.cmp_bool... all: destruct b...
+- unfold Val.cmp; destruct Val.cmp_bool...
+  all: destruct b...
+- destruct v0...
+- trivial.
+- trivial.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -870,6 +913,8 @@ Definition cond_depends_on_memory (cond : condition) : bool :=
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
   | Ocmp cmp => cond_depends_on_memory cmp
+  | OEseqw _ => negb Archi.ptr64
+  | OEsnew _ => negb Archi.ptr64
   | _ => false
   end.
 
@@ -893,6 +938,11 @@ Proof.
   intros until m2. destruct op; simpl; try congruence.
   intro DEPEND.
   f_equal. f_equal. apply cond_depends_on_memory_correct; trivial.
+  all: intros; repeat (destruct args; auto);
+       unfold Val.cmpu, Val.cmpu_bool;
+       destruct optR0 as [[]|]; simpl;
+       destruct v, v0; simpl; auto;
+       apply negb_false_iff in H; try rewrite H; auto.
 Qed.
 
 Lemma cond_valid_pointer_eq:
@@ -913,6 +963,10 @@ Proof.
   intros until m2. destruct op; simpl; try congruence.
   intros MEM; destruct cond; repeat (destruct args; simpl; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+  all: intros MEM; repeat (destruct args; simpl; try congruence);
+       try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto;
+       unfold Val.cmpu;
+       erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -1040,6 +1094,34 @@ Proof.
 - inv H3; inv H2; simpl in H0; inv H0; auto.
 Qed.
 
+Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0',
+  Val.inject f v v' ->
+  Val.inject f v0 v0' ->
+  Val.cmpu_bool (Mem.valid_pointer m1) c v v0 = Some b ->
+  Val.cmpu_bool (Mem.valid_pointer m2) c v' v0' = Some b.
+Proof.
+  intros.
+  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+Qed.
+
+Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0 optR0,
+  Val.inject f v v' ->
+  Val.inject f v0 v'0 ->
+  Val.inject f (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32)
+  (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32).
+Proof.
+  intros until optR0. intros HV1 HV2.
+  destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmpu; 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto;
+  assert (HVI: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int.
+  + exploit eval_cmpu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+  + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+  + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+Qed.
+
 Ltac TrivialExists :=
   match goal with
   | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
@@ -1246,6 +1328,14 @@ Proof.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
     destruct b; simpl; constructor.
     simpl; constructor.
+
+  - apply eval_cmpu_bool_inj; auto.
+  - apply eval_cmpu_bool_inj; auto.
+  - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
+    inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto;
+    try apply Val.inject_int.
+  - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int.
+  - inv H4; simpl; auto.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 9ec474b3..7492b01c 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -30,6 +30,11 @@ let comparison_name = function
   | Cgt -> ">"
   | Cge -> ">="
 
+let get_optR0_s c reg pp r1 r2 = function
+  | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2
+  | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
+  | Some false -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c)
+
 let print_condition reg pp = function
   | (Ccomp c, [r1;r2]) ->
       fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2
@@ -156,6 +161,13 @@ let print_operation reg pp = function
   | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1
   | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1
   | Ocmp c, args -> print_condition reg pp (c, args)
+  | OEseqw optR0, [r1;r2] -> fprintf pp "OEseqw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
+  | OEsnew optR0, [r1;r2] -> fprintf pp "OEsnew"; (get_optR0_s Cne reg pp r1 r2 optR0)
+  | OEsltw optR0, [r1;r2] -> fprintf pp "OEsltw"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%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)
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index f4b7b4d6..ec4492ff 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -17,6 +17,15 @@ Require Import Zbits.
 
 (** Value analysis for RISC V operators *)
 
+Definition zero32 := (I Int.zero).
+  
+Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 vz: aval): B :=
+  match optR0 with
+  | None => sem v1 v2
+  | Some true => sem vz v1
+  | Some false => sem v1 vz
+  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
@@ -137,6 +146,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32)
+  | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32)
+  | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32)
+  | OEsltiw n, v1::nil => of_optbool (cmp_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
   | _, _ => Vbot
   end.
 
@@ -201,6 +217,29 @@ Proof.
   rewrite Ptrofs.add_zero_l; eauto with va.
 Qed.
 
+Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m,
+  c = Ceq \/ c = Cne ->
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc (Op.apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32)
+  (of_optbool (apply_bin_r0 optR0 (cmpu_bool c) b1 b0 zero32)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
+Qed.
+
+Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0,
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp Clt) a1 a0 Op.zero32)
+  (of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) b1 b0 zero32)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
+Qed.
+
 Theorem eval_static_operation_sound:
   forall op vargs m vres aargs,
   eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
@@ -213,6 +252,11 @@ Proof.
   destruct (propagate_float_constants tt); constructor.
   rewrite Ptrofs.add_zero_l; eauto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  
+  1,2: apply eval_cmpu_sound; auto.
+  apply eval_cmp_sound; auto.
+  unfold Val.cmp; apply of_optbool_sound; eauto with va.
+  unfold zero32; simpl. eauto with va.
 Qed.
 
 End SOUNDNESS.