MPPA - 32-bits immediate eq/neq branches

8 files changed, 288 insertions, 946 deletions

diff --git a/extraction/debug/Asmgen.ml b/extraction/debug/Asmgen.ml
index 84faf75a..2ccc5948 100644
--- a/extraction/debug/Asmgen.ml
+++ b/extraction/debug/Asmgen.ml
@@ -195,3 +195,19 @@ let transl_instr f i x k =
   | Mcond _ -> (Printf.eprintf "Mcond\n"; thereal_transl_instr f i x k)
   | Mjumptable _ -> (Printf.eprintf "Mjumptable\n"; thereal_transl_instr f i x k)
   | Mreturn -> (Printf.eprintf "Mreturn\n"; thereal_transl_instr f i x k)
+
+let transl_cbranch c a l k =
+  match c, a with
+  | Ccomp       _, _ :: _ :: [] -> (Printf.eprintf "Ccomp\n"; thereal_transl_cbranch c a l k)
+  | Ccompu      _, _ :: _ :: [] -> (Printf.eprintf "Ccompu\n"; thereal_transl_cbranch c a l k)
+  | Ccompimm    (_, _), _ :: [] -> (Printf.eprintf "Ccompimm\n"; thereal_transl_cbranch c a l k)
+  | Ccompuimm   (_, _), _ :: [] -> (Printf.eprintf "Ccompuimm\n"; thereal_transl_cbranch c a l k)
+  | Ccompl      _, _ :: _ :: [] -> (Printf.eprintf "Ccompl\n"; thereal_transl_cbranch c a l k)
+  | Ccomplu     _, _ :: _ :: [] -> (Printf.eprintf "Ccomplu\n"; thereal_transl_cbranch c a l k)
+  | Ccomplimm   (_, _), _ :: [] -> (Printf.eprintf "Ccomplimm\n"; thereal_transl_cbranch c a l k)
+  | Ccompluimm  (_, _), _ :: [] -> (Printf.eprintf "Ccompulimm\n"; thereal_transl_cbranch c a l k)
+  | Ccompf      _, _ :: _ :: [] -> (Printf.eprintf "Ccompf\n"; thereal_transl_cbranch c a l k)
+  | Cnotcompf   _, _ :: _ :: [] -> (Printf.eprintf "Cnotcompf\n"; thereal_transl_cbranch c a l k)
+  | Ccompfs      _, _ :: _ :: [] -> (Printf.eprintf "Ccomps\n"; thereal_transl_cbranch c a l k)
+  | Cnotcompfs   _, _ :: _ :: [] -> (Printf.eprintf "Cnotcomps\n"; thereal_transl_cbranch c a l k)
+  | _                           -> (Printf.eprintf "OOPS\n"; thereal_transl_cbranch c a l k)
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 82ec101c..d769062f 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -92,6 +92,44 @@ Module Pregmap := EMap(PregEq).
 (** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
 
 Notation "'SP'" := GPR12 (only parsing) : asm.
+Notation "'RTMP'" := GPR31 (only parsing) : asm.
+
+Inductive btest: Type :=
+(*| BTdnez                              (**r Double Not Equal to Zero *)
+  | BTdeqz                              (**r Double Equal to Zero *)
+  | BTdltz                              (**r Double Less Than Zero *)
+  | BTdgez                              (**r Double Greater Than or Equal to Zero *)
+  | BTdlez                              (**r Double Less Than or Equal to Zero *)
+  | BTdgtz                              (**r Double Greater Than Zero *)
+  | BTodd                               (**r Odd (LSB Set) *)
+  | BTeven                              (**r Even (LSB Clear) *)
+*)| BTwnez                              (**r Word Not Equal to Zero *)
+  | BTweqz                              (**r Word Equal to Zero *)
+(*| BTwltz                              (**r Word Less Than Zero *)
+  | BTwgez                              (**r Word Greater Than or Equal to Zero *)
+  | BTwlez                              (**r Word Less Than or Equal to Zero *)
+  | BTwgtz                              (**r Word Greater Than Zero *)
+*).
+
+Inductive itest: Type :=
+  | ITne                                (**r Not Equal *)
+  | ITeq                                (**r Equal *)
+  | ITlt                                (**r Less Than *)
+  | ITge                                (**r Greater Than or Equal *)
+  | ITle                                (**r Less Than or Equal *)
+  | ITgt                                (**r Greater Than *)
+  | ITneu                               (**r Unsigned Not Equal *)
+  | ITequ                               (**r Unsigned Equal *)
+  | ITltu                               (**r Less Than Unsigned *)
+  | ITgeu                               (**r Greater Than or Equal Unsigned *)
+  | ITleu                               (**r Less Than or Equal Unsigned *)
+  | ITgtu                               (**r Greater Than Unsigned *)
+  (* Not used yet *)
+  | ITall                               (**r All Bits Set in Mask *)
+  | ITnall                              (**r Not All Bits Set in Mask *)
+  | ITany                               (**r Any Bits Set in Mask *)
+  | ITnone                              (**r Not Any Bits Set in Mask *)
+  .
 
 (** Offsets for load and store instructions.  An offset is either an
   immediate integer or the low part of a symbol. *)
@@ -136,121 +174,46 @@ Definition label := positive.
   [Asmgen]) is careful to respect this range. *)
 
 Inductive instruction : Type :=
+(** System Registers *)
+  | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)
+  | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)
 (** Branch Control Unit instructions *)
-  | Pget    (rd: ireg) (rs: preg)                    (**r get system register *)
-  | Pset    (rd: preg) (rs: ireg)                    (**r set system register *)
-  | Pret                                             (**r return *)
-  | Pcall   (l: label)                               (**r function call *)
-  | Pgoto   (l: label)                               (**r goto *)
-  | Pmv     (rd: ireg) (rs: ireg)                    (**r integer move *)
+  | Pret                                            (**r return *)
+  | Pcall   (l: label)                              (**r function call *)
+  | Pgoto   (l: label)                              (**r goto *)
+
+(** Register move *)
+  | Pmv     (rd: ireg) (rs: ireg)                   (**r integer move *)
+
+(** Comparisons *)
+  | Pcompw  (it: itest) (rd rs1 rs2: ireg)      (**r integer comparison *)
 
 (** 32-bit integer register-immediate instructions *)
   | Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add immediate *)
-(*| Psltiw  (rd: ireg) (rs: ireg) (imm: int)        (**r set-less-than immediate *)
-  | Psltiuw (rd: ireg) (rs: ireg) (imm: int)        (**r set-less-than unsigned immediate *)
-  | Pandiw  (rd: ireg) (rs: ireg) (imm: int)        (**r and immediate *)
-  | Poriw   (rd: ireg) (rs: ireg) (imm: int)        (**r or immediate *)
-  | Pxoriw  (rd: ireg) (rs: ireg) (imm: int)        (**r xor immediate *)
-  | Pslliw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift-left-logical immediate *)
-  | Psrliw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift-right-logical immediate *)
-  | Psraiw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift-right-arith immediate *)
-  | Pluiw   (rd: ireg)             (imm: int)        (**r load upper-immediate *)
+
 (** 32-bit integer register-register instructions *)
-*)| Paddw   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
-(*| Psubw   (rd: ireg) (rs1 rs2: ireg)              (**r integer subtraction *)
-
-  | Pmulw   (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply low *)
-  | Pmulhw  (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply high signed *)
-  | Pmulhuw (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply high unsigned *)
-  | Pdivw   (rd: ireg) (rs1 rs2: ireg)              (**r integer division *)
-  | Pdivuw  (rd: ireg) (rs1 rs2: ireg)              (**r unsigned integer division *)
-  | Premw   (rd: ireg) (rs1 rs2: ireg)              (**r integer remainder *)
-  | Premuw  (rd: ireg) (rs1 rs2: ireg)              (**r unsigned integer remainder *)
-  | Psltw   (rd: ireg) (rs1 rs2: ireg)              (**r set-less-than *)
-  | Psltuw  (rd: ireg) (rs1 rs2: ireg)              (**r set-less-than unsigned *)
-  | Pseqw   (rd: ireg) (rs1 rs2: ireg)              (**r [rd <- rs1 == rs2] (pseudo) *)
-  | Psnew   (rd: ireg) (rs1 rs2: ireg)              (**r [rd <- rs1 != rs2] (pseudo) *)
-  | Pandw   (rd: ireg) (rs1 rs2: ireg)              (**r bitwise and *)
-  | Porw    (rd: ireg) (rs1 rs2: ireg)              (**r bitwise or *)
-  | Pxorw   (rd: ireg) (rs1 rs2: ireg)              (**r bitwise xor *)
-  | Psllw   (rd: ireg) (rs1 rs2: ireg)              (**r shift-left-logical *)
-  | Psrlw   (rd: ireg) (rs1 rs2: ireg)              (**r shift-right-logical *)
-  | Psraw   (rd: ireg) (rs1 rs2: ireg)              (**r shift-right-arith *)
+  | Paddw   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
 
 (** 64-bit integer register-immediate instructions *)
-*)| Paddil  (rd: ireg) (rs: ireg) (imm: int64)      (**r add immediate *) (*
-  | Psltil  (rd: ireg) (rs: ireg) (imm: int64)      (**r set-less-than immediate *)
-  | Psltiul (rd: ireg) (rs: ireg) (imm: int64)      (**r set-less-than unsigned immediate *)
-  | Pandil  (rd: ireg) (rs: ireg) (imm: int64)      (**r and immediate *)
-  | Poril   (rd: ireg) (rs: ireg) (imm: int64)      (**r or immediate *)
-  | Pxoril  (rd: ireg) (rs: ireg) (imm: int64)      (**r xor immediate *)
-  | Psllil  (rd: ireg) (rs: ireg) (imm: int)        (**r shift-left-logical immediate *)
-  | Psrlil  (rd: ireg) (rs: ireg) (imm: int)        (**r shift-right-logical immediate *)
-  | Psrail  (rd: ireg) (rs: ireg) (imm: int)        (**r shift-right-arith immediate *)
-  | Pluil   (rd: ireg)             (imm: int64)      (**r FIXME - remove it ; load upper-immediate *)
-*)| Pmake   (rd: ireg)             (imm: int)        (**r load immediate *)
-  | Pmakel  (rd: ireg)             (imm: int64)      (**r load immediate long *)
+  | Paddil  (rd: ireg) (rs: ireg) (imm: int64)      (**r add immediate *) 
+  | Pmake   (rd: ireg)            (imm: int)        (**r load immediate *)
+  | Pmakel  (rd: ireg)            (imm: int64)      (**r load immediate long *)
+
 (** 64-bit integer register-register instructions *)
-  | Paddl   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *) (*
-  | Psubl   (rd: ireg) (rs1 rs2: ireg)              (**r integer subtraction *)
-
-  | Pmull   (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply low *)
-  | Pmulhl  (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply high signed *)
-  | Pmulhul (rd: ireg) (rs1 rs2: ireg)              (**r integer multiply high unsigned *)
-  | Pdivl   (rd: ireg) (rs1 rs2: ireg)              (**r integer division *)
-  | Pdivul  (rd: ireg) (rs1 rs2: ireg)              (**r unsigned integer division *)
-  | Preml   (rd: ireg) (rs1 rs2: ireg)              (**r integer remainder *)
-  | Premul  (rd: ireg) (rs1 rs2: ireg)              (**r unsigned integer remainder *)
-  | Psltl   (rd: ireg) (rs1 rs2: ireg)              (**r set-less-than *)
-  | Psltul  (rd: ireg) (rs1 rs2: ireg)              (**r set-less-than unsigned *)
-  | Pseql   (rd: ireg) (rs1 rs2: ireg)              (**r [rd <- rs1 == rs2] (pseudo) *)
-  | Psnel   (rd: ireg) (rs1 rs2: ireg)              (**r [rd <- rs1 != rs2] (pseudo) *)
-  | Pandl   (rd: ireg) (rs1 rs2: ireg)              (**r bitwise and *)
-  | Porl    (rd: ireg) (rs1 rs2: ireg)              (**r bitwise or *)
-  | Pxorl   (rd: ireg) (rs1 rs2: ireg)              (**r bitwise xor *)
-  | Pslll   (rd: ireg) (rs1 rs2: ireg)              (**r shift-left-logical *)
-  | Psrll   (rd: ireg) (rs1 rs2: ireg)              (**r shift-right-logical *)
-  | Psral   (rd: ireg) (rs1 rs2: ireg)              (**r shift-right-arith *)
-
-  | Pcvtl2w (rd: ireg) (rs: ireg)                   (**r int64->int32 (pseudo) *)
-  | Pcvtw2l (r: ireg)                                (**r int32 signed -> int64 (pseudo) *)
+  | Paddl   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
 
   (* Unconditional jumps.  Links are always to X1/RA. *)
-*)| Pj_l    (l: label)                              (**r jump to label *)
-(*| Pj_s    (symb: ident) (sg: signature)           (**r jump to symbol *)
-  | Pj_r    (r: ireg)     (sg: signature)           (**r jump register *)
-  | Pjal_s  (symb: ident) (sg: signature)           (**r jump-and-link symbol *)
-  | Pjal_r  (r: ireg)     (sg: signature)           (**r jump-and-link register *)
-
-  (* Conditional branches, 32-bit comparisons *)
-  | Pbeqw   (rs1 rs2: ireg) (l: label)             (**r branch-if-equal *)
-  | Pbnew   (rs1 rs2: ireg) (l: label)             (**r branch-if-not-equal signed *)
-  | Pbltw   (rs1 rs2: ireg) (l: label)             (**r branch-if-less signed *)
-  | Pbltuw  (rs1 rs2: ireg) (l: label)             (**r branch-if-less unsigned *)
-  | Pbgew   (rs1 rs2: ireg) (l: label)             (**r branch-if-greater-or-equal signed *)
-  | Pbgeuw  (rs1 rs2: ireg) (l: label)             (**r branch-if-greater-or-equal unsigned *)
-
-  (* Conditional branches, 64-bit comparisons *)
-  | Pbeql   (rs1 rs2: ireg) (l: label)             (**r branch-if-equal *)
-  | Pbnel   (rs1 rs2: ireg) (l: label)             (**r branch-if-not-equal signed *)
-  | Pbltl   (rs1 rs2: ireg) (l: label)             (**r branch-if-less signed *)
-  | Pbltul  (rs1 rs2: ireg) (l: label)             (**r branch-if-less unsigned *)
-  | Pbgel   (rs1 rs2: ireg) (l: label)             (**r branch-if-greater-or-equal signed *)
-  | Pbgeul  (rs1 rs2: ireg) (l: label)             (**r branch-if-greater-or-equal unsigned *)
-
-  (* Loads and stores *)
-  | Plb     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load signed int8 *)
-  | Plbu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load unsigned int8 *)
-  | Plh     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load signed int16 *)
-  | Plhu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load unsigned int16 *)
-*)| Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)
+  | Pj_l    (l: label)                              (**r jump to label *)
+
+  (* Conditional branches *)
+  | Pcb     (bt: btest) (r: ireg) (l: label)        (**r branch based on btest *)
+
+  | Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)
   | Plw_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any32 *)
   | Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)
   | Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)
 
-(*| Psb     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int8 *)
-  | Psh     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int16 *)
-*)| Psw     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)
+  | Psw     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)
   | Psw_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any32 *)
   | Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)
   | Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)
@@ -600,6 +563,45 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
     | None => Stuck
   end.
 
+Inductive signedness: Type := Signed | Unsigned.
+
+Definition itest_for_cmp (c: comparison) (s: signedness) :=
+  match c, s with
+  | Cne, Signed => ITne
+  | Ceq, Signed => ITeq
+  | Clt, Signed => ITlt
+  | Cge, Signed => ITge
+  | Cle, Signed => ITle
+  | Cgt, Signed => ITgt
+  | Cne, Unsigned => ITneu
+  | Ceq, Unsigned => ITequ
+  | Clt, Unsigned => ITltu
+  | Cge, Unsigned => ITgeu
+  | Cle, Unsigned => ITleu
+  | Cgt, Unsigned => ITgtu
+  end.
+
+(** Comparing integers *)
+Definition compare_int (t: itest) (v1 v2: val) (m: mem): val :=
+  match t with
+  | ITne  => Val.cmp Cne v1 v2
+  | ITeq  => Val.cmp Ceq v1 v2
+  | ITlt  => Val.cmp Clt v1 v2
+  | ITge  => Val.cmp Cge v1 v2
+  | ITle  => Val.cmp Cle v1 v2
+  | ITgt  => Val.cmp Cgt v1 v2
+  | ITneu => Val.cmpu (Mem.valid_pointer m) Cne v1 v2
+  | ITequ => Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
+  | ITltu => Val.cmpu (Mem.valid_pointer m) Clt v1 v2
+  | ITgeu => Val.cmpu (Mem.valid_pointer m) Cge v1 v2
+  | ITleu => Val.cmpu (Mem.valid_pointer m) Cle v1 v2
+  | ITgtu => Val.cmpu (Mem.valid_pointer m) Cgt v1 v2
+  | ITall
+  | ITnall
+  | ITany
+  | ITnone => Vundef
+  end.
+
 (** Execution of a single instruction [i] in initial state [rs] and
     [m].  Return updated state.  For instructions that correspond to
     actual RISC-V instructions, the cases are straightforward
@@ -633,90 +635,23 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmv d s =>
       Next (nextinstr (rs#d <- (rs#s))) m
 
+(** Comparisons *)
+  | Pcompw c d s1 s2 => 
+      (* Next (nextinstr (rs#d <- (Val.cmp Cne rs##s1 rs##s2))) m *)
+      Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m
+
 (** 32-bit integer register-immediate instructions *)
   | Paddiw d s i =>
       Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m
-(*| Psltiw d s i =>
-      Next (nextinstr (rs#d <- (Val.cmp Clt rs##s (Vint i)))) m
-  | Psltiuw d s i =>
-      Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Clt rs##s (Vint i)))) m
-  | Pandiw d s i =>
-      Next (nextinstr (rs#d <- (Val.and rs##s (Vint i)))) m
-  | Poriw d s i =>
-      Next (nextinstr (rs#d <- (Val.or rs##s (Vint i)))) m
-  | Pxoriw d s i =>
-      Next (nextinstr (rs#d <- (Val.xor rs##s (Vint i)))) m
-  | Pslliw d s i =>
-      Next (nextinstr (rs#d <- (Val.shl rs##s (Vint i)))) m
-  | Psrliw d s i =>
-      Next (nextinstr (rs#d <- (Val.shru rs##s (Vint i)))) m
-  | Psraiw d s i =>
-      Next (nextinstr (rs#d <- (Val.shr rs##s (Vint i)))) m
-  | Pluiw d i =>
-      Next (nextinstr (rs#d <- (Vint (Int.shl i (Int.repr 12))))) m
 
 (** 32-bit integer register-register instructions *)
-*)| Paddw d s1 s2 =>
+  | Paddw d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m
-(*| Psubw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.sub rs##s1 rs##s2))) m
-  | Pmulw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mul rs##s1 rs##s2))) m
-  | Pmulhw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mulhs rs##s1 rs##s2))) m
-  | Pmulhuw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mulhu rs##s1 rs##s2))) m
-  | Pdivw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.divs rs##s1 rs##s2)))) m
-  | Pdivuw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.divu rs##s1 rs##s2)))) m
-  | Premw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.mods rs##s1 rs##s2)))) m
-  | Premuw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.modu rs##s1 rs##s2)))) m
-  | Psltw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmp Clt rs##s1 rs##s2))) m
-  | Psltuw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Clt rs##s1 rs##s2))) m
-  | Pseqw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Ceq rs##s1 rs##s2))) m
-  | Psnew d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Cne rs##s1 rs##s2))) m
-  | Pandw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m
-  | Porw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.or rs##s1 rs##s2))) m
-  | Pxorw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.xor rs##s1 rs##s2))) m
-  | Psllw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shl rs##s1 rs##s2))) m
-  | Psrlw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shru rs##s1 rs##s2))) m
-  | Psraw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shr rs##s1 rs##s2))) m
 
 (** 64-bit integer register-immediate instructions *)
-*)| Paddil d s i =>
+  | Paddil d s i =>
       Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m
-(*| Psltil d s i =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.cmpl Clt rs###s (Vlong i))))) m
-  | Psltiul d s i =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt rs###s (Vlong i))))) m
-  | Pandil d s i =>
-      Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m
-  | Poril d s i =>
-      Next (nextinstr (rs#d <- (Val.orl rs###s (Vlong i)))) m
-  | Pxoril d s i =>
-      Next (nextinstr (rs#d <- (Val.xorl rs###s (Vlong i)))) m
-  | Psllil d s i =>
-      Next (nextinstr (rs#d <- (Val.shll rs###s (Vint i)))) m
-  | Psrlil d s i =>
-      Next (nextinstr (rs#d <- (Val.shrlu rs###s (Vint i)))) m
-  | Psrail d s i =>
-      Next (nextinstr (rs#d <- (Val.shrl rs###s (Vint i)))) m
-  | Pluil d i =>
-      Next (nextinstr (rs#d <- (Vlong (Int64.sign_ext 32 (Int64.shl i (Int64.repr 12)))))) m
-*)| Pmakel d i =>
+  | Pmakel d i =>
       Next (nextinstr (rs#d <- (Vlong i))) m
   | Pmake d i =>
       Next (nextinstr (rs#d <- (Vint i))) m
@@ -724,63 +659,18 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (** 64-bit integer register-register instructions *)
   | Paddl d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m
-(*| Psubl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m
-  | Pmull d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m
-  | Pmulhl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mullhs rs###s1 rs###s2))) m
-  | Pmulhul d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mullhu rs###s1 rs###s2))) m
-  | Pdivl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.divls rs###s1 rs###s2)))) m
-  | Pdivul d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.divlu rs###s1 rs###s2)))) m
-  | Preml d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.modls rs###s1 rs###s2)))) m
-  | Premul d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.modlu rs###s1 rs###s2)))) m
-  | Psltl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.cmpl Clt rs###s1 rs###s2)))) m
-  | Psltul d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt rs###s1 rs###s2)))) m
-  | Pseql d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Ceq rs###s1 rs###s2)))) m
-  | Psnel d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Cne rs###s1 rs###s2)))) m
-  | Pandl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m
-  | Porl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.orl rs###s1 rs###s2))) m
-  | Pxorl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.xorl rs###s1 rs###s2))) m
-  | Pslll d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m
-  | Psrll d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shrlu rs###s1 rs###s2))) m
-  | Psral d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shrl rs###s1 rs###s2))) m
-
-  | Pcvtl2w d s =>
-      Next (nextinstr (rs#d <- (Val.loword rs##s))) m
-  | Pcvtw2l r =>
-      Next (nextinstr (rs#r <- (Val.longofint rs#r))) m
-
-(** Unconditional jumps.  Links are always to X1/RA. *)
-*)| Pj_l l =>
+
+(** Unconditional jumps. *)
+  | Pj_l l =>
       goto_label f l rs m
-(*| Pj_s s sg =>
-      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-  | Pj_r r sg =>
-      Next (rs#PC <- (rs#r)) m
-  | Pjal_s s sg =>
-      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)
-              #RA <- (Val.offset_ptr rs#PC Ptrofs.one)
-           ) m
-  | Pjal_r r sg =>
-      Next (rs#PC <- (rs#r)
-              #RA <- (Val.offset_ptr rs#PC Ptrofs.one)
-           ) m
+
+(** Conditional branches *)
+  | Pcb bt r l =>
+      match bt with
+      | BTwnez => eval_branch f l rs m (Val.cmp_bool Cne rs##r (Vint (Int.repr 0)))
+      | _ => Stuck
+      end
+(*
 (** Conditional branches, 32-bit comparisons *)
   | Pbeqw s1 s2 l =>
       eval_branch f l rs m (Val.cmpu_bool (Mem.valid_pointer m) Ceq rs##s1 rs##s2)
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 69faf1f9..4b249f91 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -122,212 +122,18 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   else
     addimm64 rd rs (Ptrofs.to_int64 n) k.
 
-(*
 (** Translation of conditional branches. *)
 
-Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeqw r1 r2 lbl
-  | Cne => Pbnew r1 r2 lbl
-  | Clt => Pbltw r1 r2 lbl
-  | Cle => Pbgew r2 r1 lbl
-  | Cgt => Pbltw r2 r1 lbl
-  | Cge => Pbgew r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeqw  r1 r2 lbl
-  | Cne => Pbnew  r1 r2 lbl
-  | Clt => Pbltuw r1 r2 lbl
-  | Cle => Pbgeuw r2 r1 lbl
-  | Cgt => Pbltuw r2 r1 lbl
-  | Cge => Pbgeuw r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeql r1 r2 lbl
-  | Cne => Pbnel r1 r2 lbl
-  | Clt => Pbltl r1 r2 lbl
-  | Cle => Pbgel r2 r1 lbl
-  | Cgt => Pbltl r2 r1 lbl
-  | Cge => Pbgel r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeql  r1 r2 lbl
-  | Cne => Pbnel  r1 r2 lbl
-  | Clt => Pbltul r1 r2 lbl
-  | Cle => Pbgeul r2 r1 lbl
-  | Cgt => Pbltul r2 r1 lbl
-  | Cge => Pbgeul r1 r2 lbl
-  end.
+Definition transl_comp
+    (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
+  Pcompw (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k.
 
-Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
-  match cmp with
-  | Ceq => (Pfeqd rd fs1 fs2, true)
-  | Cne => (Pfeqd rd fs1 fs2, false)
-  | Clt => (Pfltd rd fs1 fs2, true)
-  | Cle => (Pfled rd fs1 fs2, true)
-  | Cgt => (Pfltd rd fs2 fs1, true)
-  | Cge => (Pfled rd fs2 fs1, true)
-  end.
-  
-Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
-  match cmp with
-  | Ceq => (Pfeqs rd fs1 fs2, true)
-  | Cne => (Pfeqs rd fs1 fs2, false)
-  | Clt => (Pflts rd fs1 fs2, true)
-  | Cle => (Pfles rd fs1 fs2, true)
-  | Cgt => (Pflts rd fs2 fs1, true)
-  | Cge => (Pfles rd fs2 fs1, true)
-  end.
-  
 Definition transl_cbranch
-           (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
+    (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) :=
   match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int32s c r1 r2 lbl :: k)
-  | Ccompu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int32u c r1 r2 lbl :: k)
-  | Ccompimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int.eq n Int.zero then
-            transl_cbranch_int32s c r1 GPR0 lbl :: k
-          else
-            loadimm32 GPR31 n (transl_cbranch_int32s c r1 GPR31 lbl :: k))
   | Ccompuimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (if Int.eq n Int.zero then
-            transl_cbranch_int32u c r1 GPR0 lbl :: k
-          else
-            loadimm32 GPR31 n (transl_cbranch_int32u c r1 GPR31 lbl :: k))
-  | Ccompl c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int64s c r1 r2 lbl :: k)
-  | Ccomplu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int64u c r1 r2 lbl :: k)
-  | Ccomplimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int64.eq n Int64.zero then
-            transl_cbranch_int64s c r1 GPR0 lbl :: k
-          else
-            loadimm64 GPR31 n (transl_cbranch_int64s c r1 GPR31 lbl :: k))
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int64.eq n Int64.zero then
-            transl_cbranch_int64u c r1 GPR0 lbl :: k
-          else
-            loadimm64 GPR31 n (transl_cbranch_int64u c r1 GPR31 lbl :: k))
-  | Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c GPR31 r1 r2 in
-      OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c GPR31 r1 r2 in
-      OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c GPR31 r1 r2 in
-      OK (insn :: (if normal then Pbnew GPR31 GPR0 lbl else Pbeqw GPR31 GPR0 lbl) :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c GPR31 r1 r2 in
-      OK (insn :: (if normal then Pbeqw GPR31 GPR0 lbl else Pbnew GPR31 GPR0 lbl) :: k)
-  | _, _ =>
-      Error(msg "Asmgen.transl_cond_branch")
-  end.
-
-(** Translation of a condition operator.  The generated code sets the
-  [rd] target register to 0 or 1 depending on the truth value of the
-  condition. *)
-
-Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg) (k: code) :=
-  match cmp with
-  | Ceq => Pseqw rd r1 r2 :: k
-  | Cne => Psnew rd r1 r2 :: k
-  | Clt => Psltw rd r1 r2 :: k
-  | Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltw rd r2 r1 :: k
-  | Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg) (k: code) :=
-  match cmp with
-  | Ceq => Pseqw rd r1 r2 :: k
-  | Cne => Psnew rd r1 r2 :: k
-  | Clt => Psltuw rd r1 r2 :: k
-  | Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltuw rd r2 r1 :: k
-  | Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg) (k: code) :=
-  match cmp with
-  | Ceq => Pseql rd r1 r2 :: k
-  | Cne => Psnel rd r1 r2 :: k
-  | Clt => Psltl rd r1 r2 :: k
-  | Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltl rd r2 r1 :: k
-  | Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg) (k: code) :=
-  match cmp with
-  | Ceq => Pseql rd r1 r2 :: k
-  | Cne => Psnel rd r1 r2 :: k
-  | Clt => Psltul rd r1 r2 :: k
-  | Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltul rd r2 r1 :: k
-  | Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
-  if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 GPR0 k else
-  match cmp with
-  | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd GPR0 k)
-  | Clt => sltimm32 rd r1 n k
-  | Cle => if Int.eq n (Int.repr Int.max_signed)
-           then loadimm32 rd Int.one k
-           else sltimm32 rd r1 (Int.add n Int.one) k
-  | _   => loadimm32 GPR31 n (transl_cond_int32s cmp rd r1 GPR31 k)
-  end.
-
-Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
-  if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 GPR0 k else
-  match cmp with
-  | Clt => sltuimm32 rd r1 n k
-  | _   => loadimm32 GPR31 n (transl_cond_int32u cmp rd r1 GPR31 k)
-  end.
-
-Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
-  if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 GPR0 k else
-  match cmp with
-  | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd GPR0 k)
-  | Clt => sltimm64 rd r1 n k
-  | Cle => if Int64.eq n (Int64.repr Int64.max_signed)
-           then loadimm32 rd Int.one k
-           else sltimm64 rd r1 (Int64.add n Int64.one) k
-  | _   => loadimm64 GPR31 n (transl_cond_int64s cmp rd r1 GPR31 k)
-  end.
-
-Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
-  if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 GPR0 k else
-  match cmp with
-  | Clt => sltuimm64 rd r1 n k
-  | _   => loadimm64 GPR31 n (transl_cond_int64u cmp rd r1 GPR31 k)
-  end.
-*)
-
-Definition transl_cond_op
-           (cond: condition) (rd: ireg) (args: list mreg) (k: code) : res (list instruction) :=
-  match cond, args with
+      OK (loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k))
 (*| Ccomp c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (transl_cond_int32s c rd r1 r2 k)
@@ -337,9 +143,6 @@ Definition transl_cond_op
   | Ccompimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (transl_condimm_int32s c rd r1 n k)
-  | Ccompuimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int32u c rd r1 n k)
   | Ccompl c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (transl_cond_int64s c rd r1 r2 k)
@@ -369,7 +172,7 @@ Definition transl_cond_op
       let (insn, normal) := transl_cond_single c rd r1 r2 in
       OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
 *)| _, _ =>
-      Error(msg "Asmgen.transl_cond_op")
+      Error(msg "Asmgen.transl_cbranch")
   end.
 
 (** Translation of the arithmetic operation [r <- op(args)].
@@ -839,9 +642,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       OK (Plabel lbl :: k)
   | Mgoto lbl =>
       OK (Pj_l lbl :: k)
-(*| Mcond cond args lbl =>
+  | Mcond cond args lbl =>
       transl_cbranch cond args lbl k
-  | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k)
+(*| Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k)
 *)| Mreturn =>
       OK (make_epilogue f (Pret :: k))
       (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*)
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 068a2731..dd495cd4 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -174,12 +174,16 @@ Remark transl_cond_single_nolabel:
 Proof.
   unfold transl_cond_single; intros. destruct c; inv H; exact I.
 Qed.
-
+*)
 Remark transl_cbranch_label:
   forall cond args lbl k c,
   transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
 Proof.
-  intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
+  intros. unfold transl_cbranch in H. (* unfold transl_cond_op in H. *) destruct cond; TailNoLabel.
+  - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
+Qed.
+
+(*
 - destruct c0; simpl; TailNoLabel.
 - destruct c0; simpl; TailNoLabel.
 - destruct (Int.eq n Int.zero).
@@ -212,8 +216,8 @@ Proof.
 - destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
   apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
   destruct normal; TailNoLabel.
-Qed.
 *)
+(*
 Remark transl_cond_op_label:
   forall cond args r k c,
   transl_cond_op cond r args k = OK c -> tail_nolabel k c.
@@ -270,7 +274,7 @@ Proof.
   destruct normal; TailNoLabel.
 *)
 Qed.
-
+*)
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c -> tail_nolabel k c.
@@ -373,6 +377,7 @@ Proof.
 - destruct s0; monadInv H; TailNoLabel.
 - destruct s0; monadInv H; eapply tail_nolabel_trans
   ; [eapply make_epilogue_label|TailNoLabel].
+- eapply transl_cbranch_label; eauto.
 - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
 Qed.
 (*
@@ -383,7 +388,6 @@ Qed.
 - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
 - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
 - destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
-- eapply transl_cbranch_label; eauto.
 - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
 *)
 
@@ -899,24 +903,20 @@ Local Transparent destroyed_by_op.
   left; eapply exec_straight_opt_steps_goto; eauto.
   intros. simpl in TR.
   inversion TR.
-(*
   exploit transl_cbranch_correct_true; eauto. intros (rs' & jmp & A & B & C).
   exists jmp; exists k; exists rs'.
   split. eexact A. 
   split. apply agree_exten with rs0; auto with asmgen.
   exact B. 
-*)
 - (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
   left; eapply exec_straight_steps; eauto. intros. simpl in TR.
   inversion TR.
-(*
   exploit transl_cbranch_correct_false; eauto. intros (rs' & A & B).
   exists rs'.
   split. eexact A.
   split. apply agree_exten with rs0; auto with asmgen.
   simpl. congruence.
-*)
 - (* Mjumptable *)
   assert (f0 = f) by congruence. subst f0.
   inv AT. monadInv H6.
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index b3965bb9..e16dbbaf 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -21,16 +21,16 @@ Require Import Op Locations Mach Conventions.
 Require Import Asm Asmgen Asmgenproof0.
 
 (** Decomposition of integer constants. *)
-(*
+
 Lemma make_immed32_sound:
   forall n,
   match make_immed32 n with
   | Imm32_single imm => n = imm
-  | Imm32_pair hi lo => n = Int.add (Int.shl hi (Int.repr 12)) lo
   end.
 Proof.
   intros; unfold make_immed32. set (lo := Int.sign_ext 12 n).
-  predSpec Int.eq Int.eq_spec n lo.
+  predSpec Int.eq Int.eq_spec n lo; auto.
+(*
 - auto.
 - set (m := Int.sub n lo).
   assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
@@ -54,8 +54,9 @@ Proof.
   rewrite Int.add_neg_zero. rewrite Int.add_zero. auto.
   rewrite (Int.modu_divu_Euclid m (Int.repr 4096)) at 1 by (vm_compute; congruence).
   rewrite D. apply Int.add_zero.
-Qed.
 *)
+Qed.
+
 Lemma make_immed64_sound:
   forall n,
   match make_immed64 n with
@@ -128,7 +129,7 @@ Proof.
   split. Simpl. 
   intros; Simpl.
 Qed.
-
+*)
 Lemma loadimm32_correct:
   forall rd n k rs m,
   exists rs',
@@ -140,11 +141,10 @@ Proof.
   destruct (make_immed32 n). 
 - subst imm. econstructor; split. 
   apply exec_straight_one. simpl; eauto. auto.
-  split. rewrite Int.add_zero_l; Simpl. 
+  split. Simpl.
   intros; Simpl.
-- rewrite E. apply load_hilo32_correct.
 Qed.
-
+(*
 Lemma opimm32_correct:
   forall (op: ireg -> ireg0 -> ireg0 -> instruction)
          (opi: ireg -> ireg0 -> int -> instruction)
@@ -281,7 +281,8 @@ Qed.
 
 Lemma addptrofs_correct_2:
   forall rd r1 n k (rs: regset) m b ofs,
-  r1 <> GPR31 -> rs#r1 = Vptr b ofs ->
+  r1 <> GPR31 -> rs#r1 = Vptr b of
+s ->
   exists rs',
      exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m
   /\ rs'#rd = Vptr b (Ptrofs.add ofs n)
@@ -294,91 +295,6 @@ Qed.
 
 (** Translation of conditional branches *)
 
-Lemma transl_cbranch_int32s_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H.
-- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
-  simpl; auto.
-- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
-  simpl; auto.
-- auto.
-- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
-- auto.
-Qed.
-
-Lemma transl_cbranch_int32u_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H; auto.
-- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
-Qed.
-
-Lemma transl_cbranch_int64s_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H.
-- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
-  simpl; auto.
-- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
-  simpl; auto.
-- auto.
-- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
-- auto.
-Qed.
-
-Lemma transl_cbranch_int64u_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H; auto.
-- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
-Qed.
-
-Lemma transl_cond_float_correct:
-  forall (rs: regset) m cmp rd r1 r2 insn normal v,
-  transl_cond_float cmp rd r1 r2 = (insn, normal) ->
-  v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) ->
-  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
-Proof.
-  intros. destruct cmp; simpl in H; inv H; auto. 
-- rewrite Val.negate_cmpf_eq. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
-  rewrite <- Float.cmp_swap. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
-  rewrite <- Float.cmp_swap. auto.
-Qed.
-
-Lemma transl_cond_single_correct:
-  forall (rs: regset) m cmp rd r1 r2 insn normal v,
-  transl_cond_single cmp rd r1 r2 = (insn, normal) ->
-  v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) ->
-  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
-Proof.
-  intros. destruct cmp; simpl in H; inv H; auto. 
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite <- Float32.cmp_swap. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite <- Float32.cmp_swap. auto.
-Qed.
-
 Remark branch_on_GPR31:
   forall normal lbl (rs: regset) m b,
   rs#GPR31 = Val.of_bool (eqb normal b) ->
@@ -388,6 +304,7 @@ Proof.
   intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
 Qed.
 *)
+
 Ltac ArgsInv :=
   repeat (match goal with
   | [ H: Error _ = OK _ |- _ ] => discriminate
@@ -417,7 +334,63 @@ Remark exec_straight_opt_right:
 Proof.
   destruct 1; intros. auto. eapply exec_straight_trans; eauto. 
 Qed.
-(*
+
+Lemma transl_comp_correct:
+  forall cmp r1 r2 lbl k rs m b,
+  exists rs',
+     exec_straight ge fn (transl_comp cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
+       exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_comp. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (nextinstr rs # GPR31 <- (compare_int (itest_for_cmp cmp Signed) rs ## r1 rs ## r2 m)) as rs'.
+    simpl. assert (Val.cmp_bool Cne rs' ## GPR31 (Vint (Int.repr 0)) = Some b).
+    { 
+      assert (rs' ## GPR31 = (compare_int (itest_for_cmp cmp Signed) rs ## r1 rs ## r2 m)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmp_bool cmp rs##r1 rs##r2) as cmpbool.
+      destruct cmp; simpl;
+      unfold Val.cmp; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+Lemma transl_compu_correct:
+  forall cmp r1 r2 lbl k rs m b,
+  exists rs',
+     exec_straight ge fn (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
+       exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
+  .
+Proof.
+  intros. esplit. split.
+- unfold transl_comp. apply exec_straight_one; simpl; eauto.
+- split.
+  + intros; Simpl.
+  + intros.
+    remember (nextinstr rs # GPR31 <- (compare_int (itest_for_cmp cmp Unsigned) rs ## r1 rs ## r2 m)) as rs'.
+    simpl. assert (Val.cmp_bool Cne rs' ## GPR31 (Vint (Int.repr 0)) = Some b).
+    { 
+      assert (rs' ## GPR31 = (compare_int (itest_for_cmp cmp Unsigned) rs ## r1 rs ## r2 m)).
+      { rewrite Heqrs'. auto. }
+      rewrite H0. rewrite <- H.
+      remember (Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2) as cmpubool.
+      destruct cmp; simpl; unfold Val.cmpu; rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
+      destruct b0; simpl; auto.
+    }
+    rewrite H0. simpl; auto.
+Qed.
+
+
 Lemma transl_cbranch_correct_1:
   forall cond args lbl k c m ms b sp rs m',
   transl_cbranch cond args lbl k = OK c ->
@@ -427,7 +400,7 @@ Lemma transl_cbranch_correct_1:
   exists rs', exists insn,
      exec_straight_opt c rs m' (insn :: k) rs' m'
   /\ exec_instr ge fn insn rs' m' = eval_branch fn lbl rs' m' (Some b)
-  /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
 Proof.
   intros until m'; intros TRANSL EVAL AG MEXT.
   set (vl' := map rs (map preg_of args)). 
@@ -435,84 +408,19 @@ Proof.
   { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
   clear EVAL MEXT AG.
   destruct cond; simpl in TRANSL; ArgsInv.
-- exists rs, (transl_cbranch_int32s c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
-- exists rs, (transl_cbranch_int32u c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
-- predSpec Int.eq Int.eq_spec n Int.zero.
-+ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
-+ exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int32s c0 x GPR31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int32s_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- predSpec Int.eq Int.eq_spec n Int.zero.
-+ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
-+ exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int32u c0 x GPR31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int32u_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- exists rs, (transl_cbranch_int64s c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
-- exists rs, (transl_cbranch_int64u c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
-- predSpec Int64.eq Int64.eq_spec n Int64.zero.
-+ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
-+ exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int64s c0 x GPR31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int64s_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- predSpec Int64.eq Int64.eq_spec n Int64.zero.
-+ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
-+ exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int64u c0 x GPR31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int64u_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- destruct (transl_cond_float c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (eqb normal b)).
-  { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_float c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)).
-  { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
-  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (xorb normal b)).
-  { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_single c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (eqb normal b)).
-  { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_single c0 GPR31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)).
-  { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
-  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (xorb normal b)).
-  { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
+- exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
+  exploit (transl_compu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
+  exists rs'2, (Pcb BTwnez GPR31 lbl).
+  split.
+  + constructor. apply exec_straight_trans 
+       with (c2 := (transl_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+    eexact A. eexact A'.
+  + split; auto.
+    * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen.
+    * intros. rewrite B'; eauto with asmgen.
 Qed.
 
+
 Lemma transl_cbranch_correct_true:
   forall cond args lbl k c m ms sp rs m',
   transl_cbranch cond args lbl k = OK c ->
@@ -543,7 +451,7 @@ Proof.
   split. eapply exec_straight_opt_right; eauto. apply exec_straight_one; auto.
   intros; Simpl. 
 Qed.
-
+(*
 (** Translation of condition operators *)
 
 Lemma transl_cond_int32s_correct:
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 280dd17b..2c7b8cc8 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -156,12 +156,36 @@ module Target : TARGET =
     | Ofsimm n -> ptrofs oc n
     | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs)
 
+    let icond_name = function
+      | ITne | ITneu -> "ne"
+      | ITeq | ITequ -> "eq"
+      | ITlt   -> "lt"
+      | ITge   -> "ge"
+      | ITle   -> "le"
+      | ITgt   -> "gt"
+      | ITltu  -> "ltu"
+      | ITgeu  -> "geu"
+      | ITleu  -> "leu"
+      | ITgtu  -> "gtu"
+      | ITall  -> "all"
+      | ITnall -> "nall"
+      | ITany  -> "any"
+      | ITnone -> "none"
+
+    let icond oc c = fprintf oc "%s" (icond_name c)
+  
+    let bcond_name = function
+      | BTwnez -> "wnez"
+      | BTweqz -> "weqz"
+
+    let bcond oc c = fprintf oc "%s" (bcond_name c)
+
 (* Printing of instructions *)
     let print_instruction oc = function
       | Pcall(s) ->
          fprintf oc "	call	%a\n;;\n" symbol s
       | Pgoto(s) | Pj_l(s) ->
-         fprintf oc "	goto	%a\n;;\n" symbol s
+         fprintf oc "	goto	%a\n;;\n" print_label s
       | Pret ->
          fprintf oc "	ret\n;;\n"
       | Pget (rd, rs) ->
@@ -171,352 +195,41 @@ module Target : TARGET =
       | Pmv(rd, rs) ->
          fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
 
-      (* 32-bit integer register-immediate instructions *)
       | Paddiw (rd, rs, imm) ->
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-    (*| Psltiw (rd, rs, imm) ->
-         fprintf oc "	slti	%a, %a, %a\n" ireg rd ireg rs coqint imm
-      | Psltiuw (rd, rs, imm) ->
-         fprintf oc "	sltiu	%a, %a, %a\n" ireg rd ireg rs coqint imm
-      | Pandiw (rd, rs, imm) ->
-         fprintf oc "	andi	%a, %a, %a\n" ireg rd ireg rs coqint imm
-      | Poriw (rd, rs, imm) ->
-         fprintf oc "	ori	%a, %a, %a\n" ireg rd ireg rs coqint imm
-      | Pxoriw (rd, rs, imm) ->
-         fprintf oc "	xori	%a, %a, %a\n" ireg rd ireg rs coqint imm
-      | Pslliw (rd, rs, imm) ->
-         fprintf oc "	slli%t	%a, %a, %a\n" w ireg rd ireg rs coqint imm
-      | Psrliw (rd, rs, imm) ->
-         fprintf oc "	srli%t	%a, %a, %a\n" w ireg rd ireg rs coqint imm
-      | Psraiw (rd, rs, imm) ->
-         fprintf oc "	srai%t	%a, %a, %a\n" w ireg rd ireg rs coqint imm
-      | Pluiw (rd, imm) ->
-         fprintf oc "	lui	%a, %a\n"     ireg rd coqint imm
-
-      (* 32-bit integer register-register instructions *)
-    *)| Paddw(rd, rs1, rs2) ->
+      | Paddw(rd, rs1, rs2) ->
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-    (*| Psubw(rd, rs1, rs2) ->
-         fprintf oc "	sub%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-
-      | Pmulw(rd, rs1, rs2) ->
-         fprintf oc "	mul%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-      | Pmulhw(rd, rs1, rs2) ->  assert (not Archi.ptr64);
-         fprintf oc "	mulh	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pmulhuw(rd, rs1, rs2) ->  assert (not Archi.ptr64);
-         fprintf oc "	mulhu	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-
-      | Pdivw(rd, rs1, rs2) ->
-         fprintf oc "	div%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-      | Pdivuw(rd, rs1, rs2) ->
-         fprintf oc "	divu%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-      | Premw(rd, rs1, rs2) ->
-         fprintf oc "	rem%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-      | Premuw(rd, rs1, rs2) ->
-         fprintf oc "	remu%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-
-      | Psltw(rd, rs1, rs2) ->
-         fprintf oc "	slt	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Psltuw(rd, rs1, rs2) ->
-         fprintf oc "	sltu	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-
-      | Pandw(rd, rs1, rs2) ->
-         fprintf oc "	and	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Porw(rd, rs1, rs2) ->
-         fprintf oc "	or	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pxorw(rd, rs1, rs2) ->
-         fprintf oc "	xor	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Psllw(rd, rs1, rs2) ->
-         fprintf oc "	sll%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-      | Psrlw(rd, rs1, rs2) ->
-         fprintf oc "	srl%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-      | Psraw(rd, rs1, rs2) ->
-         fprintf oc "	sra%t	%a, %a, %a\n" w ireg rd ireg rs1 ireg rs2
-
-    *)(* 64-bit integer register-immediate instructions *)
       | Paddil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-    (*| Psltil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	slti	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Psltiul (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	sltiu	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Pandil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	andi	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Poril (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	ori	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Pxoril (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	xori	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Psllil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	slli	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Psrlil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	srli	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Psrail (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	srai	%a, %a, %a\n" ireg rd ireg rs coqint64 imm
-      | Pluil (rd, imm) -> assert Archi.ptr64;
-         fprintf oc "	lui	%a, %a\n"     ireg rd coqint64 imm
-    *)
       | Pmake (rd, imm) ->
          fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint imm
       | Pmakel (rd, imm) ->
          fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint64 imm
-      (* 64-bit integer register-register instructions *)
       | Paddl(rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-    (*| Psubl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	sub	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-
-      | Pmull(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	mul	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pmulhl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	mulh	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pmulhul(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	mulhu	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-
-      | Pdivl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	div	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pdivul(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	divu	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Preml(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	rem	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Premul(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	remu	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-
-      | Psltl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	slt	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Psltul(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	sltu	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-
-      | Pandl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	and	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Porl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	or	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pxorl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	xor	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pslll(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	sll	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Psrll(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	srl	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Psral(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	sra	%a, %a, %a\n" ireg rd ireg rs1 ireg rs2
-  
-      (* Unconditional jumps.  Links are always to X1/RA. *)
-      (* TODO: fix up arguments for calls to variadics, to move *)
-      (* floating point arguments to integer registers.  How? *)
-      | Pj_l(l) ->
-         fprintf oc "	j	%a\n" print_label l
-      | Pj_s(s, sg) ->
-         fprintf oc "	j	%a\n" symbol s
-      | Pj_r(r, sg) ->
-         fprintf oc "	jr	%a\n" ireg r
-      | Pjal_s(s, sg) ->
-         fprintf oc "	call	%a\n" symbol s
-      | Pjal_r(r, sg) ->
-         fprintf oc "	jalr	%a\n" ireg r
-
-      (* Conditional branches, 32-bit comparisons *)
-      | Pbeqw(rs1, rs2, l) ->
-         fprintf oc "	beq	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbnew(rs1, rs2, l) ->
-         fprintf oc "	bne	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbltw(rs1, rs2, l) ->
-         fprintf oc "	blt	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbltuw(rs1, rs2, l) ->
-         fprintf oc "	bltu	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbgew(rs1, rs2, l) ->
-         fprintf oc "	bge	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbgeuw(rs1, rs2, l) ->
-         fprintf oc "	bgeu	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-
-      (* Conditional branches, 64-bit comparisons *)
-      | Pbeql(rs1, rs2, l) -> assert Archi.ptr64;
-         fprintf oc "	beq	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbnel(rs1, rs2, l) -> assert Archi.ptr64;
-         fprintf oc "	bne	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbltl(rs1, rs2, l) -> assert Archi.ptr64;
-         fprintf oc "	blt	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbltul(rs1, rs2, l) -> assert Archi.ptr64;
-         fprintf oc "	bltu	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbgel(rs1, rs2, l) -> assert Archi.ptr64;
-         fprintf oc "	bge	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-      | Pbgeul(rs1, rs2, l) -> assert Archi.ptr64;
-         fprintf oc "	bgeu	%a, %a, %a\n" ireg rs1 ireg rs2 print_label l
-
-      (* Loads and stores *)
-      | Plb(rd, ra, ofs) ->
-         fprintf oc "	lb	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Plbu(rd, ra, ofs) ->
-         fprintf oc "	lbu	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Plh(rd, ra, ofs) ->
-         fprintf oc "	lh	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Plhu(rd, ra, ofs) ->
-         fprintf oc "	lhu	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-    *)| Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
-         fprintf oc "	lws	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+
+      | Pcompw (it, rd, rs1, rs2) ->
+         fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
+      | Pcb (bt, r, lbl) ->
+         fprintf oc "	cb.%a	%a?%a\n;;\n" bcond bt ireg r print_label lbl
+
+      | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
+         fprintf oc "	lws	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Pld(rd, ra, ofs) | Pfld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64;
          fprintf oc "	ld	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
-
-    (*| Psb(rd, ra, ofs) ->
-         fprintf oc "	sb	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Psh(rd, ra, ofs) ->
-         fprintf oc "	sh	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-    *)| Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
-         fprintf oc "	sw	%a[%a] = %a\n" offset ofs ireg ra ireg rd
+      | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
+         fprintf oc "	sw	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
       | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) | Pfsd(rd, ra, ofs) -> assert Archi.ptr64;
          fprintf oc "	sd	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
 
-
-      (* Synchronization *)
-    (*| Pfence ->
-         fprintf oc "	fence\n"
-
-      (* floating point register move.
-         fmv.d preserves single-precision register contents, and hence
-         is applicable to both single- and double-precision moves.
-       *)
-      | Pfmv (fd,fs) ->
-         fprintf oc "	fmv.d	%a, %a\n"     freg fd freg fs
-      | Pfmvxs (rd,fs) ->
-         fprintf oc "	fmv.x.s	%a, %a\n"     ireg rd freg fs
-      | Pfmvxd (rd,fs) ->
-         fprintf oc "	fmv.x.d	%a, %a\n"     ireg rd freg fs
-
-      (* 32-bit (single-precision) floating point *)
-      | Pfls (fd, ra, ofs) ->
-         fprintf oc "	flw	%a, %a(%a)\n" freg fd offset ofs ireg ra
-      | Pfss (fs, ra, ofs) ->
-         fprintf oc "	fsw	%a, %a(%a)\n" freg fs offset ofs ireg ra
-
-      | Pfnegs (fd, fs) ->
-         fprintf oc "	fneg.s	%a, %a\n"     freg fd freg fs
-      | Pfabss (fd, fs) ->
-         fprintf oc "	fabs.s	%a, %a\n"     freg fd freg fs
-
-      | Pfadds (fd, fs1, fs2) ->
-         fprintf oc "	fadd.s	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfsubs (fd, fs1, fs2) ->
-         fprintf oc "	fsub.s	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfmuls (fd, fs1, fs2) ->
-         fprintf oc "	fmul.s	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfdivs (fd, fs1, fs2) ->
-         fprintf oc "	fdiv.s	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfmins (fd, fs1, fs2) ->
-         fprintf oc "	fmin.s	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfmaxs (fd, fs1, fs2) ->
-         fprintf oc "	fmax.s	%a, %a, %a\n" freg fd freg fs1 freg fs2
-
-      | Pfeqs (rd, fs1, fs2) ->
-         fprintf oc "	feq.s   %a, %a, %a\n" ireg rd freg fs1 freg fs2
-      | Pflts (rd, fs1, fs2) ->
-         fprintf oc "	flt.s   %a, %a, %a\n" ireg rd freg fs1 freg fs2
-      | Pfles (rd, fs1, fs2) ->
-         fprintf oc "	fle.s   %a, %a, %a\n" ireg rd freg fs1 freg fs2
-
-      | Pfsqrts (fd, fs) ->
-         fprintf oc "	fsqrt.s %a, %a\n"     freg fd freg fs
-
-      | Pfmadds (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fmadd.s	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-      | Pfmsubs (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fmsub.s	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-      | Pfnmadds (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fnmadd.s	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-      | Pfnmsubs (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fnmsub.s	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-
-      | Pfcvtws (rd, fs) ->
-         fprintf oc "	fcvt.w.s	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtwus (rd, fs) ->
-         fprintf oc "	fcvt.wu.s	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtsw (fd, rs) ->
-         fprintf oc "	fcvt.s.w	%a, %a\n" freg fd ireg rs
-      | Pfcvtswu (fd, rs) ->
-         fprintf oc "	fcvt.s.wu	%a, %a\n" freg fd ireg rs
-
-      | Pfcvtls (rd, fs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.l.s	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtlus (rd, fs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.lu.s	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtsl (fd, rs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.s.l	%a, %a\n" freg fd ireg rs
-      | Pfcvtslu (fd, rs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.s.lu	%a, %a\n" freg fd ireg rs
-
-      (* 64-bit (double-precision) floating point *)
-      | Pfld (fd, ra, ofs) | Pfld_a (fd, ra, ofs) ->
-         fprintf oc "	fld	%a, %a(%a)\n" freg fd offset ofs ireg ra
-      | Pfsd (fs, ra, ofs) | Pfsd_a (fs, ra, ofs) ->
-         fprintf oc "	fsd	%a, %a(%a)\n" freg fs offset ofs ireg ra
-
-      | Pfnegd (fd, fs) ->
-         fprintf oc "	fneg.d	%a, %a\n"     freg fd freg fs
-      | Pfabsd (fd, fs) ->
-         fprintf oc "	fabs.d	%a, %a\n"     freg fd freg fs
-
-      | Pfaddd (fd, fs1, fs2) ->
-         fprintf oc "	fadd.d	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfsubd (fd, fs1, fs2) ->
-         fprintf oc "	fsub.d	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfmuld (fd, fs1, fs2) ->
-         fprintf oc "	fmul.d	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfdivd (fd, fs1, fs2) ->
-         fprintf oc "	fdiv.d	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfmind (fd, fs1, fs2) ->
-         fprintf oc "	fmin.d	%a, %a, %a\n" freg fd freg fs1 freg fs2
-      | Pfmaxd (fd, fs1, fs2) ->
-         fprintf oc "	fmax.d	%a, %a, %a\n" freg fd freg fs1 freg fs2
-
-      | Pfeqd (rd, fs1, fs2) ->
-         fprintf oc "	feq.d	%a, %a, %a\n" ireg rd freg fs1 freg fs2
-      | Pfltd (rd, fs1, fs2) ->
-         fprintf oc "	flt.d	%a, %a, %a\n" ireg rd freg fs1 freg fs2
-      | Pfled (rd, fs1, fs2) ->
-         fprintf oc "	fle.d	%a, %a, %a\n" ireg rd freg fs1 freg fs2
-
-      | Pfsqrtd (fd, fs) ->
-         fprintf oc "	fsqrt.d	%a, %a\n" freg fd freg fs
-
-      | Pfmaddd (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fmadd.d	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-      | Pfmsubd (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fmsub.d	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-      | Pfnmaddd (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fnmadd.d	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-      | Pfnmsubd (fd, fs1, fs2, fs3) ->
-         fprintf oc "	fnmsub.d	%a, %a, %a, %a\n" freg fd freg fs1 freg fs2 freg fs3
-
-      | Pfcvtwd (rd, fs) ->
-         fprintf oc "	fcvt.w.d	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtwud (rd, fs) ->
-         fprintf oc "	fcvt.wu.d	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtdw (fd, rs) ->
-         fprintf oc "	fcvt.d.w	%a, %a\n" freg fd ireg rs
-      | Pfcvtdwu (fd, rs) ->
-         fprintf oc "	fcvt.d.wu	%a, %a\n" freg fd ireg rs
-
-      | Pfcvtld (rd, fs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.l.d	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtlud (rd, fs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.lu.d	%a, %a, rtz\n" ireg rd freg fs
-      | Pfcvtdl (fd, rs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.d.l	%a, %a\n" freg fd ireg rs
-      | Pfcvtdlu (fd, rs) -> assert Archi.ptr64;
-         fprintf oc "	fcvt.d.lu	%a, %a\n" freg fd ireg rs
-
-      | Pfcvtds (fd, fs) ->
-         fprintf oc "	fcvt.d.s	%a, %a\n" freg fd freg fs
-      | Pfcvtsd (fd, fs) ->
-         fprintf oc "	fcvt.s.d	%a, %a\n" freg fd freg fs
-
       (* Pseudo-instructions expanded in Asmexpand *)
-    *)| Pallocframe(sz, ofs) ->
+      | Pallocframe(sz, ofs) ->
          assert false
       | Pfreeframe(sz, ofs) ->
          assert false
-    (*| Pseqw _ | Psnew _ | Pseql _ | Psnel _ | Pcvtl2w _ | Pcvtw2l _ ->
-         assert false
 
       (* Pseudo-instructions that remain *)
-    *)| Plabel lbl ->
+      | Plabel lbl ->
          fprintf oc "%a:\n" print_label lbl
     (*| Ploadsymbol(rd, id, ofs) ->
          loadsymbol oc rd id ofs
diff --git a/test/mppa/Makefile b/test/mppa/Makefile
index 9078bdb9..e73dcb38 100644
--- a/test/mppa/Makefile
+++ b/test/mppa/Makefile
@@ -1,4 +1,4 @@
-ELF=simple.bin call.bin
+ELF=simple.bin call.bin branch.bin
 DEBUG:=$(if $(DEBUG),"-dall",)
 
 all: $(ELF)
@@ -8,7 +8,7 @@ all: $(ELF)
 
 .SECONDARY:
 %.s: %.c
-	ccomp $(DEBUG) -v -S $< -o $@
+	ccomp $(DEBUG) -O0 -v -S $< -o $@
 
 .PHONY:
 clean:
diff --git a/test/mppa/branch.c b/test/mppa/branch.c
new file mode 100644
index 00000000..dee15568
--- /dev/null
+++ b/test/mppa/branch.c
@@ -0,0 +1,12 @@
+int main(void){
+    int a=1;
+    int b;
+
+    if(a){
+        b = a+4;
+    } else {
+        b = a+2;
+    }
+
+    return b;
+}