Remaining ctl insts except Pbuiltin (maps to error)

1 files changed, 493 insertions, 369 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 3c5cc9dd..25b9c5c5 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -59,6 +59,7 @@ Variable Ge: genv.
 Inductive value_wrap :=
   | Val (v: val)
   | Memstate (m: mem)
+  | Bool (b: bool)
 .
 
 Definition value := value_wrap.
@@ -68,13 +69,16 @@ Record CRflags := { _CN: val; _CZ:val; _CC: val; _CV: val }.
 Inductive control_op :=
   (*| Oj_l (l: label)*)
   | Ob (l: label)
-  (*| Ocb (bt: btest) (l: label)*)
-  (*| Ocbu (bt: btest) (l: label)*)
-  (*| Odiv*)
-  (*| Odivu*)
-  (*| OError*)
+  | Obc (c: testcond) (l: label)
+  | Obl (id: ident)
+  | Obs (id: ident)
+  | Ocbnz (sz: isize) (l: label)
+  | Ocbz (sz: isize) (l: label)
+  | Otbnz (sz: isize) (n: int) (l: label)
+  | Otbz (sz: isize) (n: int) (l: label)
+  | Obtbl (l: list label)
+  | OError
   | OIncremPC (sz: Z)
-  (*| Ojumptable (l: list label)*)
 .
 
 Inductive arith_op :=
@@ -127,12 +131,22 @@ Inductive allocf_op :=
   | OAllocf_Mem (sz: Z) (linkofs: ptrofs)
 .
 
+Inductive freef_op :=
+  | OFreef_SP (sz: Z) (linkofs: ptrofs)
+  | OFreef_Mem (sz: Z) (linkofs: ptrofs)
+.
+
 Inductive op_wrap :=
   (* arithmetic operation *)
   | Arith (op: arith_op)
   | Load (ld: load_op)
   | Store (st: store_op)
   | Allocframe (al: allocf_op)
+  | Freeframe (fr: freef_op)
+  | Loadsymbol (id: ident)
+  | Cvtsw2x
+  | Cvtuw2x
+  | Cvtx2w
   | Control (co: control_op)
   | Constant (v: val)
 .
@@ -266,12 +280,14 @@ Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) :=
       end
   end.
 
-Definition csetsel_eval (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) (is_set: bool) :=
+Definition cond_eval_is (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) (is: Z) :=
   let res := flags_testcond_value c vCN vCZ vCC vCV in
-  (if is_set then
-    (if_opt_bool_val res (Vint Int.one) (Vint Int.zero))
-  else
-    (if_opt_bool_val res v1 v2)).
+  match is, res with
+  | 0, res => Some (Val (if_opt_bool_val res (Vint Int.one) (Vint Int.zero)))
+  | 1, res => Some (Val (if_opt_bool_val res v1 v2))
+  | 2, Some b => Some (Bool (b))
+  | _, _ => None
+  end.
 
 Definition fmovi_eval (fsz: fsize) (v: val) :=
   match fsz with
@@ -291,20 +307,21 @@ Definition fnmul_eval (fsz: fsize) (v1 v2: val) :=
   | D => Val.negf (Val.mulf v1 v2)
   end.
 
-Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is_set: bool) :=
+Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is: Z) :=
+
   match c, l with
-  | TCeq, [Val vCZ] => Some (Val (csetsel_eval TCeq v1 v2 Vundef vCZ Vundef Vundef is_set))
-  | TCne, [Val vCZ] => Some (Val (csetsel_eval TCne v1 v2 Vundef vCZ Vundef Vundef is_set))
-  | TChs, [Val vCC] => Some (Val (csetsel_eval TChs v1 v2 Vundef Vundef vCC Vundef is_set))
-  | TClo, [Val vCC] => Some (Val (csetsel_eval TClo v1 v2 Vundef Vundef vCC Vundef is_set))
-  | TCmi, [Val vCN] => Some (Val (csetsel_eval TCmi v1 v2 vCN Vundef Vundef Vundef is_set))
-  | TCpl, [Val vCN] => Some (Val (csetsel_eval TCpl v1 v2 vCN Vundef Vundef Vundef is_set))
-  | TChi, [Val vCZ; Val vCC] => Some (Val (csetsel_eval TChi v1 v2 Vundef vCZ vCC Vundef is_set))
-  | TCls, [Val vCZ; Val vCC] => Some (Val (csetsel_eval TCls v1 v2 Vundef vCZ vCC Vundef is_set))
-  | TCge, [Val vCN; Val vCV] => Some (Val (csetsel_eval TCge v1 v2 vCN Vundef Vundef vCV is_set))
-  | TClt, [Val vCN; Val vCV] => Some (Val (csetsel_eval TClt v1 v2 vCN Vundef Vundef vCV is_set))
-  | TCgt, [Val vCN; Val vCZ; Val vCV] => Some (Val (csetsel_eval TCgt v1 v2 vCN vCZ Vundef vCV is_set))
-  | TCle, [Val vCN; Val vCZ; Val vCV] => Some (Val (csetsel_eval TCle v1 v2 vCN vCZ Vundef vCV is_set))
+  | TCeq, [Val vCZ] => cond_eval_is TCeq v1 v2 Vundef vCZ Vundef Vundef is
+  | TCne, [Val vCZ] => cond_eval_is TCne v1 v2 Vundef vCZ Vundef Vundef is
+  | TChs, [Val vCC] => cond_eval_is TChs v1 v2 Vundef Vundef vCC Vundef is
+  | TClo, [Val vCC] => cond_eval_is TClo v1 v2 Vundef Vundef vCC Vundef is
+  | TCmi, [Val vCN] => cond_eval_is TCmi v1 v2 vCN Vundef Vundef Vundef is
+  | TCpl, [Val vCN] => cond_eval_is TCpl v1 v2 vCN Vundef Vundef Vundef is
+  | TChi, [Val vCZ; Val vCC] => cond_eval_is TChi v1 v2 Vundef vCZ vCC Vundef is
+  | TCls, [Val vCZ; Val vCC] => cond_eval_is TCls v1 v2 Vundef vCZ vCC Vundef is
+  | TCge, [Val vCN; Val vCV] => cond_eval_is TCge v1 v2 vCN Vundef Vundef vCV is
+  | TClt, [Val vCN; Val vCV] => cond_eval_is TClt v1 v2 vCN Vundef Vundef vCV is
+  | TCgt, [Val vCN; Val vCZ; Val vCV] => cond_eval_is TCgt v1 v2 vCN vCZ Vundef vCV is
+  | TCle, [Val vCN; Val vCZ; Val vCV] => cond_eval_is TCle v1 v2 vCN vCZ Vundef vCV is
   | _, _ => None
   end.
 
@@ -335,10 +352,10 @@ Definition arith_op_eval (op: arith_op) (l: list value) :=
   | OArithComparisonP_CZ n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CZ)))
   | OArithComparisonP_CC n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CC)))
   | OArithComparisonP_CV n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CV)))
-  | Ocset c, l => cflags_eval c l Vundef Vundef true
+  | Ocset c, l => cflags_eval c l Vundef Vundef 0
   | Ofmovi fsz, [Val v] => Some (Val (fmovi_eval fsz v))
   | Ofmovi_XZR fsz, [] => Some (Val (fmovi_eval_xzr fsz))
-  | Ocsel c, Val v1 :: Val v2 :: l' => cflags_eval c l' v1 v2 false
+  | Ocsel c, Val v1 :: Val v2 :: l' => cflags_eval c l' v1 v2 1
   | Ofnmul fsz, [Val v1; Val v2] => Some (Val (fnmul_eval fsz v1 v2))
   | _, _ => None
   end.
@@ -389,7 +406,43 @@ Definition control_eval (o: control_op) (l: list value) :=
   let (ge, fn, lk) := Ge in
   match o, l with
   | Ob lbl, [Val vpc] => goto_label_deps fn lbl vpc
+  | Obc c lbl, Val vpc :: l' => match cflags_eval c l' Vundef Vundef 2 with
+                                | Some (Bool true) => goto_label_deps fn lbl vpc
+                                | Some (Bool false) => Some (Val vpc)
+                                | _ => None
+                                end
+  | Obl id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
+  | Obs id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
+  | Ocbnz sz lbl, [Val v; Val vpc] => match eval_testzero sz v with
+                                      | Some (true) => Some (Val vpc)
+                                      | Some (false) => goto_label_deps fn lbl vpc
+                                      | None => None
+                                      end
+  | Ocbz sz lbl, [Val v; Val vpc] => match eval_testzero sz v with
+                                      | Some (true) => goto_label_deps fn lbl vpc
+                                      | Some (false) => Some (Val vpc)
+                                      | None => None
+                                     end
+  | Otbnz sz n lbl, [Val v; Val vpc] => match eval_testbit sz v n with
+                                        | Some (true) => goto_label_deps fn lbl vpc
+                                        | Some (false) => Some (Val vpc)
+                                        | None => None
+                                       end
+  | Otbz sz n lbl, [Val v; Val vpc] => match eval_testbit sz v n with
+                                        | Some (true) => Some (Val vpc)
+                                        | Some (false) => goto_label_deps fn lbl vpc
+                                        | None => None
+                                       end
+  | Obtbl tbl, [Val index; Val vpc] => match index with
+                                       | Vint n => 
+                                         match list_nth_z tbl (Int.unsigned n) with
+                                         | None => None
+                                         | Some lbl => goto_label_deps fn lbl vpc
+                                         end
+                                       | _ => None
+                                       end
   | OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz)))
+  | OError, _ => None
   | _, _ => None
   end.
 
@@ -457,12 +510,48 @@ Definition eval_allocf (o: allocf_op) (l: list value) :=
   | _, _ => None
   end.
 
+Definition eval_freef (o: freef_op) (l: list value) :=
+  match o, l with
+  | OFreef_Mem sz linkofs, [Val spv; Memstate m] =>
+      match call_ll_loadv Mint64 (fun v => v) m (Some (Val.offset_ptr spv linkofs)) with
+      | None => None
+      | Some v =>
+          match spv with
+          | Vptr stk ofs =>
+              match Mem.free m stk 0 sz with
+              | None => None
+              | Some m' => Some (Memstate m')
+              end
+          | _ => None
+          end
+      end
+  | OFreef_SP sz linkofs, [Val spv; Memstate m] =>
+      match call_ll_loadv Mint64 (fun v => v) m (Some (Val.offset_ptr spv linkofs)) with
+      | None => None
+      | Some v =>
+          match spv with
+          | Vptr stk ofs =>
+              match Mem.free m stk 0 sz with
+              | None => None
+              | Some m' => Some (v)
+              end
+          | _ => None
+          end
+      end
+  | _, _ => None
+  end.
+
 Definition op_eval (op: op) (l:list value) :=
   match op, l with
   | Arith op, l => arith_op_eval op l
   | Load o, l => load_eval o l
   | Store o, l => store_eval o l
   | Allocframe o, l => eval_allocf o l
+  | Freeframe o, l => eval_freef o l
+  | Loadsymbol id, [] => Some (Val (Genv.symbol_address Ge.(_genv) id Ptrofs.zero))
+  | Cvtsw2x, [Val v] => Some (Val (Val.longofint v))
+  | Cvtuw2x, [Val v] => Some (Val (Val.longofintu v))
+  | Cvtx2w, [Val v] => Some (Val (Val.loword v))
   | Control o, l => control_eval o l
   | Constant v, [] => Some (Val v)
   | _, _ => None
@@ -650,8 +739,22 @@ Definition control_op_eq (c1 c2: control_op): ?? bool :=
   match c1 with
   | Ob lbl1 =>
      match c2 with Ob lbl2 => phys_eq lbl1 lbl2 | _ => RET false end
-  (*| Ocb bt1 l1 =>*)
-     (*match c2 with Ocb bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end*)
+  | Obc c1 lbl1 =>
+     match c2 with Obc c2 lbl2 => iandb (struct_eq c1 c2) (phys_eq lbl1 lbl2) | _ => RET false end
+  | Obl id1 =>
+     match c2 with Obl id2 => phys_eq id1 id2 | _ => RET false end
+  | Obs id1 =>
+     match c2 with Obs id2 => phys_eq id1 id2 | _ => RET false end
+  | Ocbnz sz1 lbl1 =>
+     match c2 with Ocbnz sz2 lbl2 => iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2) | _ => RET false end
+  | Ocbz sz1 lbl1 =>
+     match c2 with Ocbz sz2 lbl2 => iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2) | _ => RET false end
+  | Otbnz sz1 n1 lbl1 =>
+     match c2 with Otbnz sz2 n2 lbl2 => iandb (RET (Int.eq n1 n2)) (iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2)) | _ => RET false end
+  | Otbz sz1 n1 lbl1 =>
+     match c2 with Otbz sz2 n2 lbl2 => iandb (RET (Int.eq n1 n2)) (iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2)) | _ => RET false end
+  | Obtbl tbl1 =>
+     match c2 with Obtbl tbl2 => (phys_eq tbl1 tbl2) | _ => RET false end
   (*| Ocbu bt1 l1 =>*)
      (*match c2 with Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end*)
   (*| Ojumptable tbl1 =>*)
@@ -662,14 +765,15 @@ Definition control_op_eq (c1 c2: control_op): ?? bool :=
      (*match c2 with Odivu => RET true | _ => RET false end*)
   | OIncremPC sz1 =>
       match c2 with OIncremPC sz2 => RET (Z.eqb sz1 sz2) | _ => RET false end
-  (*| OError =>*)
-     (*match c2 with OError => RET true | _ => RET false end*)
+  | OError =>
+     match c2 with OError => RET true | _ => RET false end
   end.
 
 Lemma control_op_eq_correct c1 c2:
   WHEN control_op_eq c1 c2 ~> b THEN b = true -> c1 = c2.
 Proof.
-  destruct c1, c2; wlp_simplify; try rewrite Z.eqb_eq in * |-; try congruence.
+  destruct c1, c2; wlp_simplify; try rewrite Z.eqb_eq in * |-; try congruence;
+  try apply Int.same_if_eq in H; try congruence.
 Qed.
 Hint Resolve control_op_eq_correct: wlp.
 Opaque control_op_eq_correct.
@@ -712,8 +816,39 @@ Qed.
 Hint Resolve load_op_eq_correct: wlp.
 Opaque load_op_eq_correct.
 
-(*Definition allocf_op_eq (al1 al2: allocf_op): ?? bool :=*)
-  
+Definition allocf_op_eq (al1 al2: allocf_op): ?? bool :=
+  match al1 with
+  | OAllocf_SP sz1 linkofs1 =>
+      match al2 with OAllocf_SP sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
+  | OAllocf_Mem sz1 linkofs1 =>
+      match al2 with OAllocf_Mem sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
+  end.
+
+Lemma allocf_op_eq_correct al1 al2:
+  WHEN allocf_op_eq al1 al2 ~> b THEN b = true -> al1 = al2.
+Proof.
+  destruct al1, al2; wlp_simplify; try congruence.
+  all: rewrite H2; rewrite Z.eqb_eq in H; rewrite H; reflexivity.
+Qed.
+Hint Resolve allocf_op_eq_correct: wlp.
+Opaque allocf_op_eq_correct.
+
+Definition freef_op_eq (fr1 fr2: freef_op): ?? bool :=
+  match fr1 with
+  | OFreef_SP sz1 linkofs1 =>
+      match fr2 with OFreef_SP sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
+  | OFreef_Mem sz1 linkofs1 =>
+      match fr2 with OFreef_Mem sz2 linkofs2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq linkofs1 linkofs2) | _ => RET false end
+  end.
+
+Lemma freef_op_eq_correct fr1 fr2:
+  WHEN freef_op_eq fr1 fr2 ~> b THEN b = true -> fr1 = fr2.
+Proof.
+  destruct fr1, fr2; wlp_simplify; try congruence.
+  all: rewrite H2; rewrite Z.eqb_eq in H; rewrite H; reflexivity.
+Qed.
+Hint Resolve freef_op_eq_correct: wlp.
+Opaque freef_op_eq_correct.
 
 Definition op_eq (o1 o2: op): ?? bool :=
   match o1 with
@@ -725,9 +860,21 @@ Definition op_eq (o1 o2: op): ?? bool :=
       match o2 with Load i2 => load_op_eq i1 i2 | _ => RET false end
   | Store i1 =>
       match o2 with Store i2 => store_op_eq i1 i2 | _ => RET false end
+  | Allocframe i1 =>
+      match o2 with Allocframe i2 => allocf_op_eq i1 i2 | _ => RET false end
+  | Freeframe i1 =>
+      match o2 with Freeframe i2 => freef_op_eq i1 i2 | _ => RET false end
+  | Loadsymbol id1 =>
+      match o2 with Loadsymbol id2 => phys_eq id1 id2 | _ => RET false end
+  | Cvtsw2x =>
+    match o2 with Cvtsw2x => RET true | _ => RET false end
+  | Cvtuw2x =>
+    match o2 with Cvtuw2x => RET true | _ => RET false end
+  | Cvtx2w =>
+    match o2 with Cvtx2w => RET true | _ => RET false end
   | Constant c1 =>
     match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end
-  | _ => RET false
+  (*| _ => RET false*)
   end.
 
 Lemma op_eq_correct o1 o2: 
@@ -826,6 +973,18 @@ Proof.
   intros k n n' H1 H2. apply H1; clear H1. eapply Pos.add_reg_l; eauto.
 Qed.
 
+Lemma ppos_equal: forall r r', r = r' <-> ppos r = ppos r'.
+Proof.
+  destruct r as [dr|cr|]; destruct r' as [dr'|cr'|];
+  try destruct dr as [ir|fr]; try destruct dr' as [ir'|fr'];
+  try destruct ir as [irr|]; try destruct ir' as [irr'|].
+  all: split; intros; try rewrite H; try discriminate; try contradiction; simpl; eauto;
+  try destruct irr; try destruct irr';
+  try destruct fr; try destruct fr';
+  try destruct cr; try destruct cr';
+  simpl; try discriminate; try reflexivity.
+Qed.
+
 Lemma ppos_discr: forall r r', r <> r' -> ppos r <> ppos r'.
 Proof.
   destruct r as [dr|cr|]; destruct r' as [dr'|cr'|];
@@ -892,25 +1051,6 @@ Notation "a @ b" := (Econs a b) (at level 102, right associativity).
 
 (** Translations of instructions *)
 
-Definition trans_control (ctl: control) : inst :=
-  match ctl with
-  | Pb lbl => [(#PC, Op (Control (Ob lbl)) (PReg(#PC) @ Enil))]
-  | _ => []
-  (*| Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (PReg(#r) @ PReg(#PC) @ Enil))]*)
-  (*| Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (PReg(#r) @ PReg(#PC) @ Enil))]*)
-  (*| Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (PReg(#r) @ PReg(#PC) @ Enil));*)
-                            (*(#GPR62, Op (Constant Vundef) Enil);*)
-                            (*(#GPR63, Op (Constant Vundef) Enil) ]*)
-  (*| Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]*)
-  end.
-
-Definition trans_exit (ex: option control) : L.inst :=
-  match ex with
-  | None => []
-  | Some ctl => trans_control ctl
-  end
-.
-
 Definition get_testcond_rlocs (c: testcond) :=
   match c with
   | TCeq => (PReg(#CZ) @ Enil)
@@ -927,6 +1067,37 @@ Definition get_testcond_rlocs (c: testcond) :=
   | TCle => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil)
   end.
 
+Definition trans_control (ctl: control) : inst :=
+  match ctl with
+  | Pb lbl => [(#PC, Op (Control (Ob lbl)) (PReg(#PC) @ Enil))]
+  | Pbc c lbl =>
+      let lr := get_testcond_rlocs c in
+      [(#PC, Op (Control (Obc c lbl)) (PReg(#PC) @ lr))]
+  | Pbl id sg => [(#RA, PReg(#PC));
+                  (#PC, Op (Control (Obl id)) Enil)]
+  | Pbs id sg => [(#PC, Op (Control (Obs id)) Enil)]
+  | Pblr r sg => [(#RA, PReg(#PC));
+                  (#PC, Old (PReg(#r)))]
+  | Pbr r sg => [(#PC, PReg(#r))]
+  | Pret r => [(#PC, PReg(#r))]
+  | Pcbnz sz r lbl => [(#PC, Op (Control (Ocbnz sz lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
+  | Pcbz sz r lbl => [(#PC, Op (Control (Ocbz sz lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
+  | Ptbnz sz r n lbl => [(#PC, Op (Control (Otbnz sz n lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
+  | Ptbz sz r n lbl => [(#PC, Op (Control (Otbz sz n lbl)) (PReg(#r) @ PReg(#PC) @ Enil))]
+  | Pbtbl r tbl => [(#X16, Op (Constant Vundef) Enil);
+                    (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil));
+                    (#X16, Op (Constant Vundef) Enil);
+                    (#X17, Op (Constant Vundef) Enil)]
+  | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)]
+  end.
+
+Definition trans_exit (ex: option control) : L.inst :=
+  match ex with
+  | None => []
+  | Some ctl => trans_control ctl
+  end
+.
+
 Definition trans_arith (ai: ar_instruction) : inst :=
   match ai with
   | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)]
@@ -1020,57 +1191,19 @@ Definition trans_basic (b: basic) : inst :=
       let lr := eval_addressing_rlocs_ld ld a in [(#r, lr)]
   | PStore st r a => 
       let lr := eval_addressing_rlocs_st st r a in [(pmem, lr)]
-  (*| Pallocframe sz linkofs =>*)
-      (*[(#X29, PReg(#SP));*)
-       (*(#SP, Op (OAllocf_SP sz linkofs) (PReg (#SP) @ PReg pmem @ Enil));*)
-       (*(#X16, Op (Constant Vundef) Enil);*)
-       (*(pmem, Op (OAllocf_Mem ))]*)
-
-  | _ => []
-  (*| PLoadRRO trap n d a ofs => [(#d, Op (Load (OLoadRRO n trap ofs)) (PReg (#a) @ PReg pmem @ Enil))]*)
-  (*| PLoadRRR trap n d a ro =>  [(#d, Op (Load (OLoadRRR n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]*)
-  (*| PLoadRRRXS trap n d a ro =>  [(#d, Op (Load (OLoadRRRXS n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]*)
-  (*| PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))]*)
-  (*| PLoadQRRO qd a ofs =>*)
-    (*let (d0, d1) := gpreg_q_expand qd in*)
-      (*[(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil));*)
-       (*(#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil))]*)
-  (*| PLoadORRO od a ofs =>*)
-    (*match gpreg_o_expand od with*)
-    (*| (d0, d1, d2, d3) =>*)
-        (*[(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil));*)
-         (*(#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil));*)
-         (*(#d2, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 16)))) (Old(PReg (#a)) @ PReg pmem @ Enil));*)
-         (*(#d3, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 24)))) (Old(PReg (#a)) @ PReg pmem @ Enil))]*)
-    (*end*)
-  (*| PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]*)
-  (*| PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]*)
-  (*| PStoreQRRO qs a ofs =>*)
-    (*let (s0, s1) := gpreg_q_expand qs in *)
-    (*[(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil));*)
-     (*(pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))]*)
-  (*| PStoreORRO os a ofs =>*)
-    (*match gpreg_o_expand os with*)
-    (*| (s0, s1, s2, s3) =>*)
-      (*[(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil));*)
-       (*(pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil));*)
-       (*(pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (PReg (#s2) @ PReg (#a) @ PReg pmem @ Enil));*)
-       (*(pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (PReg (#s3) @ PReg (#a) @ PReg pmem @ Enil))]*)
-    (*end*)
-  (*| Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);*)
-                           (*(pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))]*)
-  (*| Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil));*)
-                          (*(#SP, Op (Freeframe2 sz pos) (PReg (#SP) @ Old (PReg pmem) @ Enil));*)
-                          (*(#RTMP, Op (Constant Vundef) Enil)]*)
-  (*| Pget rd ra => match ra with*)
-                  (*| RA => [(#rd, PReg(#ra))]*)
-                  (*| _ => [(#rd, Op Fail Enil)]*)
-                  (*end*)
-  (*| Pset ra rd => match ra with*)
-                  (*| RA => [(#ra, PReg(#rd))]*)
-                  (*| _ => [(#rd, Op Fail Enil)]*)
-                  (*end*)
-  (*| Pnop => []*)
+  | Pallocframe sz linkofs =>
+      [(#X29, PReg(#SP));
+       (#SP, Op (Allocframe (OAllocf_SP sz linkofs)) (PReg (#SP) @ PReg pmem @ Enil));
+       (#X16, Op (Constant Vundef) Enil);
+       (pmem, Op (Allocframe (OAllocf_Mem sz linkofs)) (Old(PReg(#SP)) @ PReg pmem @ Enil))]
+  | Pfreeframe sz linkofs =>
+      [(pmem, Op (Freeframe (OFreef_Mem sz linkofs)) (PReg (#SP) @ PReg pmem @ Enil));
+       (#SP, Op (Freeframe (OFreef_SP sz linkofs)) (PReg (#SP) @ Old (PReg pmem) @ Enil));
+       (#X16, Op (Constant Vundef) Enil)]
+  | Ploadsymbol rd id => [(#rd, Op (Loadsymbol id) Enil)]
+  | Pcvtsw2x rd r1 => [(#rd, Op (Cvtsw2x) (PReg (#r1) @ Enil))]
+  | Pcvtuw2x rd r1 => [(#rd, Op (Cvtuw2x) (PReg (#r1) @ Enil))]
+  | Pcvtx2w rd => [(#rd, Op (Cvtx2w) (PReg (#rd) @ Enil))]
   end.
 
 Fixpoint trans_body (b: list basic) : list L.inst :=
@@ -1146,6 +1279,12 @@ Proof.
   intros. simpl. reflexivity.
 Qed.
 
+Lemma ireg_not_pc: forall r,
+  (#PC) <> ireg_to_pos r.
+Proof.
+  intros; destruct r; discriminate.
+Qed.
+
 Lemma ireg_not_pmem: forall r,
   ireg_to_pos r <> pmem.
 Proof.
@@ -1251,12 +1390,18 @@ Proof.
     + simpl; try rewrite <- HEQV; unfold ppos; try congruence.
 Qed.
 
-Lemma sr_update_overwrite: forall sr pos v1 v2,
-  (sr <[ pos <- v1 ]>) <[ pos <- v2 ]> = (sr <[ pos <- v2 ]>).
+Lemma sr_pc_update_both: forall sr rsr rr v
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  (sr <[ #PC <- Val (v) ]>) (#rr) =
+  Val (rsr # PC <- v rr).
 Proof.
-  intros.
-  unfold assign. apply functional_extensionality; intros x.
-  destruct (R.eq_dec pos x); reflexivity.
+  intros. unfold assign.
+  destruct (PregEq.eq PC rr); subst.
+  - rewrite Pregmap.gss. simpl. reflexivity.
+  - rewrite Pregmap.gso; eauto.
+    destruct rr; try congruence.
+    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.
+    + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
 Qed.
 
 Lemma sr_gss: forall sr pos v,
@@ -1266,6 +1411,14 @@ Proof.
   destruct (R.eq_dec pos pos) eqn:REQ; try reflexivity; try congruence.
 Qed.
 
+Lemma sr_update_overwrite: forall sr pos v1 v2,
+  (sr <[ pos <- v1 ]>) <[ pos <- v2 ]> = (sr <[ pos <- v2 ]>).
+Proof.
+  intros.
+  unfold assign. apply functional_extensionality; intros x.
+  destruct (R.eq_dec pos x); reflexivity.
+Qed.
+
 (*Ltac Simplif :=*)
   (*[>((rewrite nextblock_inv by eauto with asmgen)<]*)
   (*[>|| (rewrite nextblock_inv1 by eauto with asmgen)<]*)
@@ -1315,6 +1468,11 @@ Ltac DPRF pr :=
       | destruct frDPRF]
       | destruct crDPRF|].
 
+Ltac DPRM pr :=
+  destruct pr as [drDPRF|crDPRF|]; 
+      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |]
+      | destruct crDPRF|].
+
 Ltac DPRI pr :=
   destruct pr as [drDPRI|crDPRI|]; 
       [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|]
@@ -1323,6 +1481,7 @@ Ltac DPRI pr :=
 
 Ltac discriminate_ppos :=
   try apply ireg_not_pmem;
+  try apply ireg_not_pc;
   try apply freg_not_pmem;
   try apply ireg_not_CN;
   try apply ireg_not_CZ;
@@ -1334,14 +1493,17 @@ Ltac discriminate_ppos :=
   try apply freg_not_CV;
   try(simpl; discriminate).
 
+Ltac replace_pc := try replace (6) with (#PC) by eauto.
+
 Ltac replace_regs_pos sr :=
   try replace (sr 7) with (sr (ppos XSP)) by eauto;
+  try replace (sr 6) with (sr (ppos PC)) by eauto;
   try replace (sr 2) with (sr (ppos CN)) by eauto;
   try replace (sr 3) with (sr (ppos CZ)) by eauto;
   try replace (sr 4) with (sr (ppos CC)) by eauto;
   try replace (sr 5) with (sr (ppos CV)) by eauto.
 
-Ltac TARITH sr :=
+Ltac Simpl_exists sr :=
   replace_ppos;
   replace_regs_pos sr;
   try sr_val_rwrt;
@@ -1351,10 +1513,24 @@ Ltac TARITH sr :=
       discriminate_ppos
   ).
 
-Ltac SRVUPDATE :=
+Ltac Simpl_rep sr :=
+  replace_ppos;
+  replace_regs_pos sr;
+  try sr_val_rwrt;
+  try (sr_memstate_rwrt; rewrite assign_diff;
+      try reflexivity;
+      discriminate_ppos
+  ).
+
+Ltac Simpl_update :=
   try eapply sr_ireg_update_both; eauto;
   try eapply sr_freg_update_both; eauto;
-  try eapply sr_xsp_update_both; eauto.
+  try eapply sr_xsp_update_both; eauto;
+  try eapply sr_pc_update_both; eauto.
+
+Ltac Simpl sr := Simpl_exists sr; intros rr; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr; Simpl_update.
+
+Ltac destruct_res_flag rsr := try (rewrite Pregmap.gso; discriminate_ppos); destruct (rsr _); simpl; try reflexivity.
 
 Ltac discriminate_preg_flags := rewrite !assign_diff; try rewrite !Pregmap.gso; discriminate_ppos; sr_val_rwrt; reflexivity.
 
@@ -1373,6 +1549,19 @@ Ltac validate_crbit_flags c :=
     rewrite sr_gss; rewrite Pregmap.gss; reflexivity
   ].
 
+
+Lemma reg_update_overwrite: forall rsr sr r rd v1 v2
+  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
+  ((sr <[ # rd <- Val (v1) ]>) <[ # rd <- Val (v2) ]>) (# r) =
+  Val ((rsr # rd <- v1) # rd <- v2 r).
+Proof.
+  intros.
+  unfold Pregmap.set; destruct (PregEq.eq r rd).
+  - rewrite e; apply sr_gss; reflexivity.
+  - rewrite sr_update_overwrite. rewrite assign_diff; eauto.
+    unfold not; intros. apply ppos_equal in H. congruence.
+Qed.
+
 Lemma compare_single_res_aux: forall sr mr rsr rr
   (HMEM: sr pmem = Memstate mr)
   (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
@@ -1528,7 +1717,7 @@ Qed.
 (*Definition bblock_para_check (p: Asmvliw.bblock) : bool :=*)
   (*PChk.is_parallelizable (trans_block p).*)
 
-(*Section SECT_PAR.*)
+Section SECT_SEQ.
 
 (*Import PChk.*)
 
@@ -1552,29 +1741,26 @@ Proof.
   induction i.
   all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr.
   - (* PArithP *)
-    DIRN1 rd; TARITH sr; intros rr; DPRF rr; SRVUPDATE.
+    DIRN1 rd; Simpl sr.
   - (* PArithPP *)
-    DIRN1 rs; DIRN1 rd; TARITH sr;
-    intros rr; DPRI rr; SRVUPDATE.
+    DIRN1 rs; DIRN1 rd; Simpl sr.
   - (* PArithPPP *)
-    DIRN1 r1; DIRN1 r2; DIRN1 rd; TARITH sr;
-    intros rr; DPRI rr; SRVUPDATE.
+    DIRN1 r1; DIRN1 r2; DIRN1 rd; Simpl sr.
   - (* PArithRR0R *) 
     simpl. destruct r1.
-    + (* OArithRR0R *) simpl; TARITH sr; intros rr; DPRI rr; SRVUPDATE.
-    + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); TARITH sr; intros rr; DPRI rr; SRVUPDATE.
+    + (* OArithRR0R *) simpl; Simpl sr.
+    + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); Simpl sr.
   - (* PArithRR0 *)
     simpl. destruct r1.
-    + (* OArithRR0 *) simpl; TARITH sr; intros rr; DPRI rr; SRVUPDATE.
-    + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); TARITH sr; intros rr; DPRI rr; SRVUPDATE.
+    + (* OArithRR0 *) simpl; Simpl sr.
+    + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); Simpl sr.
   - (* PArithARRRR0 *)
     simpl. destruct r3.
-    + (* OArithARRRR0 *) simpl; TARITH sr; intros rr; DPRI rr; SRVUPDATE.
-    + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); TARITH sr; intros rr; DPRI rr; SRVUPDATE.
+    + (* OArithARRRR0 *) simpl; Simpl sr.
+    + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); Simpl sr.
   - (* PArithComparisonPP *)
     DIRN1 r2; DIRN1 r1; destruct i;
-    repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
-    (eexists; split; [| split]; [reflexivity | eauto | idtac]);
+    repeat Simpl_rep sr; Simpl_exists sr;
     unfold arith_eval_comparison_pp; destruct arith_prepare_comparison_pp;
     simpl; intros rr; try destruct sz;
     try (eapply compare_single_res; eauto);
@@ -1583,42 +1769,44 @@ Proof.
   - (* PArithComparisonR0R *)
     simpl. destruct r1; (
       simpl; destruct i;
-      repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
-      (eexists; split; [| split]; [reflexivity | eauto | idtac]);
+      repeat Simpl_rep sr; Simpl_exists sr;
       unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize; destruct arith_prepare_comparison_r0r; destruct is;
       simpl; intros rr; try destruct sz;
       try (eapply compare_long_res; eauto);
       try (eapply compare_int_res; eauto)).
   - (* PArithComparisonP *)
     DIRN1 r1; destruct i;
-    repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
-    (eexists; split; [| split]; [reflexivity | eauto | idtac]);
+    repeat Simpl_rep sr; Simpl_exists sr;
     unfold arith_eval_comparison_p; destruct arith_prepare_comparison_p;
-    simpl; intros rr; try destruct sz;
+    simpl; try intros rr; try destruct sz;
     try (eapply compare_single_res; eauto);
     try (eapply compare_long_res; eauto);
     try (eapply compare_int_res; eauto);
     try (eapply compare_float_res; eauto).
   - (* Pcset *)
     simpl; (*DI0N0 rd.*) unfold eval_testcond, get_testcond_rlocs, cflags_eval;
-    unfold csetsel_eval; unfold flags_testcond_value, list_exp_eval; destruct c; simpl;
-    repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
-    destruct (rsr CZ); simpl;
-    (eexists; split; [| split]; [reflexivity | DI0N0 rd; eauto | idtac]);
-    intros rr; DPRI rr; SRVUPDATE;
-    rewrite Pregmap.gso; unfold assign; try destruct (R.eq_dec); sr_val_rwrt; auto; discriminate_ppos.
+    unfold cond_eval_is; unfold flags_testcond_value, list_exp_eval; destruct c; simpl;
+    repeat Simpl_rep sr; Simpl_exists sr;
+    destruct_res_flag rsr;
+    Simpl sr.
   - (* Pfmovi *)
-    simpl; destruct r1; simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE.
+    simpl; destruct r1; simpl; destruct fsz; Simpl sr.
   - (* Pcsel *)
     simpl.
     unfold eval_testcond, cflags_eval. DIRN1 r1; DIRN1 r2; destruct c; simpl;
-    repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos);
-    (eexists; split; [| split]; [reflexivity | DDRF rd; eauto | idtac]).
+    repeat Simpl_rep sr;
+    (eexists; split; [| split]; [reflexivity | DDRM rd; Simpl_exists sr | idtac]).
     all: intros rr; destruct (PregEq.eq rr rd);
     [ subst; erewrite Pregmap.gss; erewrite sr_gss; reflexivity |
     try erewrite Pregmap.gso; try erewrite assign_diff; try rewrite H0; try fold (ppos rd); try eapply ppos_discr; eauto ].
   - (* Pfnmul *)
-    simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE.
+    simpl; destruct fsz; Simpl sr.
+Qed.
+
+Lemma sp_xsp:
+  SP = XSP.
+Proof.
+  econstructor.
 Qed.
 
 Theorem bisimu_basic rsr mr sr bi:
@@ -1635,162 +1823,52 @@ Local Ltac preg_eq_discr r rd :=
 
   intros MS; inversion MS as (H & H0).
   destruct bi; simpl.
-(* Arith *)
-  exploit trans_arith_correct; eauto.
-
-  2: {
-    unfold exec_store, eval_addressing_rlocs_st, exp_eval;
-    destruct a; simpl; DIRN1 r; try destruct base; TARITH sr; erewrite H;
-    unfold exec_store1, exec_store2, exec_storeU; unfold call_ll_storev;
-    try destruct (Mem.storev _ _ _ _); simpl; auto.
-    all: eexists; split; [| split]; [ eauto | eauto |
-    intros rr; rewrite assign_diff; [ rewrite H0; auto | apply ppos_pmem_discr ]].
-    }
-
-  1: {
+  (* Loadsymbol / Cvtsw2x / Cvtuw2x / Cvtx2w *) 
+  6,7,8,9: Simpl sr.
+  - (* Arith *)
+    exploit trans_arith_correct; eauto.
+  - (* Load *)
     unfold exec_load, eval_addressing_rlocs_ld, exp_eval;
-    destruct a; simpl; try destruct base; TARITH sr; erewrite H;
+    destruct a; simpl; try destruct base; Simpl_exists sr; erewrite H;
     unfold exec_load1, exec_load2, exec_loadU; unfold call_ll_loadv;
     try destruct (Mem.loadv _ _ _); simpl; auto.
     all: eexists; split; [| split]; [ eauto | DDRF rd; eauto | idtac ];
     intros rr; destruct (PregEq.eq rr rd); subst; [ rewrite Pregmap.gss; rewrite sr_gss; reflexivity |
     rewrite assign_diff; try rewrite Pregmap.gso;
     try rewrite H0; try (fold (ppos rd); eapply ppos_discr); auto].
-    }
-
-    all: admit. (*
-(* Load *)
-  - destruct i.
-    (* Load Offset *)
-    + destruct i; simpl load_chunk. all:
-      unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0;
-      unfold eval_offset;
-      simpl; auto;
-      destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto;
-      eexists; split; try split; Simpl;
-      intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
-
-    (* Load Reg *)
-    + destruct i; simpl load_chunk. all:
-      unfold parexec_load_reg; simpl; unfold exec_load_deps_reg; rewrite H, H0; rewrite (H0 rofs);
-      destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto;
-      eexists; split; try split; Simpl;
-      intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
-
-    (* Load Reg XS *)
-    + destruct i; simpl load_chunk. all:
-      unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs);
-      destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto;
-      eexists; split; try split; Simpl;
-      intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
-
-    (* Load Quad word *)
-    + unfold parexec_load_q_offset.
-      destruct (gpreg_q_expand rd) as [rd0 rd1]; destruct Ge; simpl.
-      rewrite H0, H.
-      destruct (Mem.loadv Many64 mr _) as [load0 | ]; simpl; auto.
-      rewrite !(assign_diff _ _ pmem), H; auto.
-      destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ]; simpl; auto.
-      eexists; intuition eauto.
-      { rewrite !(assign_diff _ _ pmem); auto. }
-      { preg_eq_discr r rd1.
-        preg_eq_discr r rd0. }
-
-    (* Load Octuple word *)
-    + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core.
-      unfold parexec_load_o_offset.
-      destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]; destruct Ge; simpl.
-      rewrite H0, H.
-      destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) ofs)) as [load0 | ]; simpl; auto.
-      rewrite !(assign_diff _ _ pmem), !H; auto.
-      destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ]; simpl; auto.
-      rewrite !(assign_diff _ _ pmem), !H; auto.
-      destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 16)))) as [load2| ]; simpl; auto.
-      rewrite !(assign_diff _ _ pmem), !H; auto.
-      destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 24)))) as [load3| ]; simpl; auto.
-      eexists; intuition eauto.
-      { rewrite !(assign_diff _ _ pmem); auto. }
-      { preg_eq_discr r rd3.
-        preg_eq_discr r rd2.
-        preg_eq_discr r rd1.
-        preg_eq_discr r rd0. }
-
-(* Store *)
-  - destruct i.
-    (* Store Offset *)
-    + destruct i; simpl store_chunk. all:
-      unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra);
-      unfold eval_offset; simpl; auto;
-      destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto;
-      eexists; split; try split; Simpl;
-      intros rr; destruct rr; Simpl.
-
-    (* Store Reg *)
-    + destruct i; simpl store_chunk. all:
-      unfold parexec_store_reg; simpl; unfold exec_store_deps_reg; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs);
-      destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto;
-      eexists; split; try split; Simpl;
-      intros rr; destruct rr; Simpl.
-
-    (* Store Reg XS *)
-    + destruct i; simpl store_chunk. all:
-      unfold parexec_store_regxs; simpl; unfold exec_store_deps_regxs; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs);
-      destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto;
-      eexists; split; try split; Simpl;
-      intros rr; destruct rr; Simpl.
-
-    (* Store Quad Word *)
-    + unfold parexec_store_q_offset.
-      destruct (gpreg_q_expand rs) as [s0 s1]; destruct Ge; simpl.
-      rewrite !H0, !H.
-      destruct (Mem.storev _ _ _ (rsr s0)) as [mem0 | ]; simpl; auto.
-      rewrite !assign_diff, !H0; auto.
-      destruct (Mem.storev _ _ _ (rsr s1)) as [mem1 | ]; simpl; auto.
-      eexists; intuition eauto.
-      rewrite !assign_diff; auto.
-
-    (* Store Ocuple Word *)
-    + unfold parexec_store_o_offset.
-      destruct (gpreg_o_expand rs) as [[[s0 s1] s2] s3]; destruct Ge; simpl.
-      rewrite !H0, !H.
-      destruct (Mem.storev _ _ _ (rsr s0)) as [store0 | ]; simpl; auto.
-      rewrite !assign_diff, !H0; auto.
-      destruct (Mem.storev _ _ _ (rsr s1)) as [store1 | ]; simpl; auto.
-      rewrite !assign_diff, !H0; auto.
-      destruct (Mem.storev _ _ _ (rsr s2)) as [store2 | ]; simpl; auto.
-      rewrite !assign_diff, !H0; auto.
-      destruct (Mem.storev _ _ _ (rsr s3)) as [store3 | ]; simpl; auto.
-      eexists; intuition eauto.
-      rewrite !assign_diff; auto.
-
-  (* Allocframe *)
-  - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
-    * eexists; repeat split.
-      { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl.
-      rewrite H, MEMAL. rewrite MEMS. reflexivity. }
-      { Simpl. }
-      { intros rr; destruct rr; Simpl.
-        destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. }
-    * simpl; Simpl; erewrite !H0, H, MEMAL, MEMS; auto.
-  (* Freeframe *)
-  - erewrite !H0, H.
-    destruct (Mem.loadv _ _ _) eqn:MLOAD; simpl; auto.
-    destruct (rsr GPR12) eqn:SPeq; simpl; auto.
-    destruct (Mem.free _ _ _ _) eqn:MFREE; simpl; auto.
-    eexists; repeat split.
-    * simpl. Simpl. erewrite H0, SPeq, MLOAD, MFREE. reflexivity.
-    * Simpl.
-    * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl.
-(* Pget *)
-  - destruct rs eqn:rseq; simpl; auto.
-    eexists. repeat split. Simpl. intros rr; destruct rr; Simpl.
-    destruct (ireg_eq g rd); subst; Simpl.
-(* Pset *)
-  - destruct rd eqn:rdeq; simpl; auto.
-    eexists. repeat split. Simpl. intros rr; destruct rr; Simpl.
-(* Pnop *)
-  - eexists. repeat split; assumption.*)
-Admitted.
+  - (* Store *)
+    unfold exec_store, eval_addressing_rlocs_st, exp_eval;
+    destruct a; simpl; DIRN1 r; try destruct base; Simpl_exists sr; erewrite H;
+    unfold exec_store1, exec_store2, exec_storeU; unfold call_ll_storev;
+    try destruct (Mem.storev _ _ _ _); simpl; auto.
+    all: eexists; split; [| split]; [ eauto | eauto |
+    intros rr; rewrite assign_diff; [ rewrite H0; auto | apply ppos_pmem_discr ]].
+  - (* Alloc *)
+    destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
+    + eexists; repeat split. 
+      * rewrite !assign_diff; try discriminate_ppos; Simpl_exists sr;
+        rewrite H; destruct (Mem.alloc _ _ _) eqn:MEMAL2;
+        injection MEMAL; intros Hm Hb; try rewrite Hm, Hb;
+        rewrite sp_xsp in MEMS; rewrite MEMS.
+        rewrite !assign_diff; try discriminate_ppos; Simpl_exists sr; rewrite H;
+        destruct (Mem.alloc _ _ _) eqn:MEMAL3;
+        injection MEMAL2; intros Hm2 Hb2; try rewrite Hm2, Hb2;
+        rewrite Hm, Hb; rewrite MEMS; reflexivity.
+      * eauto.
+      * intros rr; DPRF rr; repeat Simpl_exists sr.
+    + simpl; repeat Simpl_exists sr. erewrite H. destruct (Mem.alloc _ _ _) eqn:HMEMAL2.
+        injection MEMAL; intros Hm Hb. 
+        try rewrite Hm, Hb; clear Hm Hb.
+        try rewrite sp_xsp in MEMS; rewrite MEMS. reflexivity.
+  - (* Free *)
+    destruct (Mem.loadv _ _ _) eqn:MLOAD; simpl; auto;
+    repeat Simpl_exists sr; rewrite H; simpl.
+    + destruct (rsr SP) eqn:EQSP; simpl; rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD; try reflexivity.
+      destruct (Mem.free _ _ _) eqn:EQFREE; try reflexivity. rewrite assign_diff; discriminate_ppos.
+      replace_regs_pos sr; sr_val_rwrt. rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD. rewrite EQFREE.
+      Simpl_exists sr. intros rr; DPRF rr; repeat Simpl_exists sr.
+    + rewrite <- sp_xsp; rewrite MLOAD; reflexivity.
+Qed.
 
 Theorem bisimu_body:
   forall bdy rsr mr sr,
@@ -1807,14 +1885,42 @@ Proof.
   - intros X; rewrite X; simpl; auto.
 Qed.
 
-Theorem bisimu_control ex sz rsr mr sr old:
+Theorem bisimu_control ex sz rsr mr sr:
   match_states (State rsr mr) sr ->
-  match_outcome (exec_cfi Ge.(_genv) Ge.(_fn) ex (incrPC (Ptrofs.repr sz) rsr) mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr old).
+  match_outcome (exec_cfi Ge.(_genv) Ge.(_fn) ex (incrPC (Ptrofs.repr sz) rsr) mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr sr).
 Proof.
   intros MS.
   simpl in *. inv MS.
   destruct ex.
-  1: { replace (6) with (#PC) by auto. rewrite (H0 PC). simpl.
+  (* Obr / Oret *)
+  6,7: unfold control_eval, incrPC; simpl; destruct Ge;
+       replace_pc; rewrite (H0 PC);
+       repeat Simpl_rep sr; Simpl_exists sr;
+       intros rr; destruct (preg_eq rr PC); [
+       rewrite e; rewrite sr_gss; rewrite Pregmap.gss;
+       try rewrite Pregmap.gso; discriminate_ppos; fold (ppos r); auto |
+       repeat Simpl_rep sr; try rewrite !Pregmap.gso; auto; apply ppos_discr in n; auto ].
+  (* Ocbnz / Ocbz *)
+  6,7,8,9: unfold control_eval; destruct Ge; simpl;
+           replace_pc; rewrite (H0 PC);
+           unfold eval_branch, eval_neg_branch, eval_testzero, eval_testbit,
+                  incrPC, goto_label_deps, goto_label;
+           destruct (PregEq.eq r PC);
+           [ rewrite e; destruct sz0; simpl; Simpl sr |
+             destruct sz0; simpl; replace_pc; rewrite Pregmap.gso; auto; repeat Simpl_rep sr; try rewrite H0;
+             try (destruct (Val_cmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+             try (destruct (Val_cmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+             try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+             try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+             try (Simpl_exists sr; intros rr; destruct (PregEq.eq rr PC); subst;
+                  [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ]);
+             try (destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss;
+                  destruct Val.offset_ptr; try reflexivity; Simpl_exists sr;
+                  intros rr; destruct (PregEq.eq rr PC); subst;
+                  [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ];
+                  rewrite Pregmap.gso; auto)].
+  - (* Ob *)
+    replace_pc. rewrite (H0 PC). simpl.
     unfold goto_label, control_eval. destruct Ge.
     unfold goto_label_deps. destruct (label_pos _ _ _); auto.
     + unfold incrPC. rewrite Pregmap.gss; eauto. destruct (Val.offset_ptr _ _); auto;
@@ -1824,69 +1930,72 @@ Proof.
       * intros. rewrite sr_update_overwrite. unfold Pregmap.set, assign.
         destruct r as [dr|cr|]; try destruct dr as [ir|fr]; try destruct ir as [irr|];
         try destruct irr; try destruct fr; try destruct cr; simpl; try rewrite <- H0; eauto.
-    + rewrite sr_gss; reflexivity. }
-  all: admit.
-
-
-
-
-  (*    destruct c; destruct i; try discriminate; simpl.
-    all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl).
-
-    (* Pjumptable *)
-    + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold incrPC. Simpl.
-      destruct (rsr r); simpl; auto. destruct (list_nth_z _ _); simpl; auto.
-      unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
-      destruct (Val.offset_ptr _ _); simpl; auto.
-      eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl.
-      destruct (preg_eq g GPR62). rewrite e. Simpl.
-      destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl.
-
-    (* Pj_l *)
-    + rewrite (H0 PC). Simpl. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
-      unfold incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
-      eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl.
-
-    (* Pcb *)
-    + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmp_for_btest _); simpl; auto. destruct o; simpl; auto.
-      unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i.
-      ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b.
-         +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
-             destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
-             intros rr; destruct rr; Simpl.
-         +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl.
-      ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b.
-         +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
-             destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
-             intros rr; destruct rr; Simpl.
-         +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl.
-
-    (* Pcbu *)
-    + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto.
-      unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i.
-      ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b.
-         +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
-             destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
-             intros rr; destruct rr; Simpl.
-         +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl.
-      ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b.
-         +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
-             destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
-             intros rr; destruct rr; Simpl.
-         +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl.
-
-  - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl.
-    intros rr; destruct rr; unfold incrPC; Simpl.
-Qed.*)
-Admitted.
+    + rewrite sr_gss; reflexivity.
+  - (* Obc *)
+    replace_pc. rewrite (H0 PC). simpl.
+    unfold eval_branch, goto_label, control_eval. destruct Ge.
+    unfold goto_label_deps, cflags_eval, eval_testcond, list_exp_eval.
+    destruct c; simpl; unfold incrPC;
+    repeat (replace_ppos; replace_pc; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos).
+    1,2,3,4,5,6: destruct_res_flag rsr.
+    7,8,9,10: do 2 (destruct_res_flag rsr).
+    11,12 : do 3 (destruct_res_flag rsr).
+    1,2,3,4,5,6,9,10: destruct (Int.eq _ _); [| Simpl sr ];
+                      destruct (label_pos _ _ _); [| reflexivity]; replace_pc; 
+                      rewrite !Pregmap.gss; destruct Val.offset_ptr;
+                      try (unfold Stuck; reflexivity); Simpl_exists sr; intros rr;
+                      apply reg_update_overwrite; eauto.
+    1,3: destruct (andb); [| Simpl sr ];
+         destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss;
+         destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr;
+         intros rr; apply reg_update_overwrite; eauto.
+    1,2: destruct (orb); [| Simpl sr ];
+         destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss;
+         destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr;
+         intros rr; apply reg_update_overwrite; eauto.
+  - (* Obl *)
+    replace_pc. rewrite (H0 PC). simpl.
+    unfold control_eval. destruct Ge.
+    rewrite sr_gss.
+    repeat Simpl_rep sr. Simpl_exists sr.
+    Simpl sr.
+    all: repeat (intros; replace_regs_pos sr; try replace (38) with (#X30) by eauto; unfold incrPC; Simpl_update).
+  - (* Obs *)
+    unfold control_eval. destruct Ge. replace_pc. rewrite (H0 PC). simpl; unfold incrPC.
+    replace_pc; Simpl_exists sr; intros rr; apply reg_update_overwrite; eauto.
+  - (* Oblr *)
+    replace_pc. rewrite (H0 PC).
+    unfold control_eval. destruct Ge. simpl. unfold incrPC.
+    try (eexists; split; [  | split ]); eauto.
+    intros rr; DPRF rr; Simpl_update.
+    68: rewrite sr_gss, Pregmap.gss;
+        try rewrite Pregmap.gso; discriminate_ppos; fold (ppos r); rewrite H0; auto.
+    all: repeat Simpl_rep sr; rewrite !Pregmap.gso; discriminate_ppos; auto.
+  - (* Obtbl *)
+    replace_pc. rewrite (H0 PC).
+    unfold control_eval. destruct Ge. simpl. unfold incrPC.
+    destruct r1.
+    17: rewrite Pregmap.gss, sr_gss; try reflexivity.
+    all: rewrite !Pregmap.gso, !assign_diff; discriminate_ppos;
+    rewrite ireg_pos_ppos; try erewrite H0; destruct (rsr _);
+    try destruct (list_nth_z _ _); try reflexivity;
+    unfold goto_label, goto_label_deps; destruct (label_pos _ _ _);
+    try rewrite 2Pregmap.gso, Pregmap.gss; destruct (Val.offset_ptr (rsr PC) (Ptrofs.repr sz));
+    try reflexivity; discriminate_ppos; simpl; Simpl_exists sr;
+    intros rr;
+    destruct (PregEq.eq X16 rr); [ subst; Simpl_update |];
+    destruct (PregEq.eq X17 rr); [ subst; Simpl_update |];
+    destruct (PregEq.eq PC rr); [ subst; Simpl_update |];
+    rewrite !Pregmap.gso; auto; apply ppos_discr in n; apply ppos_discr in n0; apply ppos_discr in n1;
+    simpl in *;repeat Simpl_rep sr; auto.
+Qed.
 
-Theorem bisimu_exit ex sz rsr mr sr old:
+Theorem bisimu_exit ex sz rsr mr sr:
   match_states (State rsr mr) sr ->
-  match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr old).
+  match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit (Some (PCtlFlow ex)))) sr sr).
 Proof.
   intros; unfold estep.
-  exploit (bisimu_control ex sz rsr mr sr sr); eauto.
-  intros. destruct ex; simpl; auto.
+  exploit (bisimu_control ex sz rsr mr sr); eauto.
 Qed.
 
 Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil).
@@ -1900,9 +2009,9 @@ Proof.
   destruct (exec_body _ _ _ _ _); simpl.
   - unfold match_states in *. intros (s' & X1 & X2). destruct s.
     erewrite run_app_Some; eauto.
-    exploit (bisimu_exit ex sz _rs _m s' s'); eauto.
+    exploit (bisimu_exit ex sz _rs _m s'); eauto.
     destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3).
-    replace (6) with (#PC) by auto. erewrite !X3; simpl.
+    replace_pc. erewrite !X3; simpl.
     destruct (inst_run _ _ _ _); simpl; auto.
   - intros X; erewrite run_app_None; eauto.
 Qed.
@@ -2036,15 +2145,15 @@ Qed.
   (*apply (bisimu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto.*)
 (*Qed.*)
 
-Lemma bbstep_is_exec_bblock: forall bb (cfi: cf_instruction) size_bb bdy rs m rs' m' t,
-  (body bb) = bdy ->
-  (exit bb) = Some (PCtlFlow cfi) ->
-  Ptrofs.repr (size bb) = size_bb ->
-  exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m'
-  <-> (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) (cfi) size_bb bdy rs m = Next rs' m' /\ t = E0).
-Proof.
-  intros.
-Admitted.
+(*Lemma bbstep_is_exec_bblock: forall bb (cfi: cf_instruction) size_bb bdy rs m rs' m' t,*)
+  (*(body bb) = bdy ->*)
+  (*(exit bb) = Some (PCtlFlow cfi) ->*)
+  (*Ptrofs.repr (size bb) = size_bb ->*)
+  (*exec_bblock Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rs m t rs' m'*)
+  (*<-> (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) (cfi) size_bb bdy rs m = Next rs' m' /\ t = E0).*)
+(*Proof.*)
+  (*intros.*)
+(*Admitted.*)
 
 (* TODO This is the lemma we should use if we want to modelize
 builtins in our scheduling process.
@@ -2123,7 +2232,7 @@ Qed.
       (*unfold trans_state in PRUN; rewrite EXEC in PRUN. discriminate.*)
 (*Qed.*)
 
-(*End SECT_PAR.*)
+End SECT_SEQ.
 
 Section SECT_BBLOCK_EQUIV.
 
@@ -2478,14 +2587,21 @@ Definition string_of_load (op: load_op) : pstring :=
 Definition string_of_control (op: control_op) : pstring :=
   match op with
   | Ob _ => "Ob"
+  | Obc _ _ => "Obc"
+  | Obl _ => "Obl"
+  | Obs _ => "Obs"
+  | Ocbnz _ _ => "Ocbnz"
+  | Ocbz _ _ => "Ocbz"
+  | Otbnz _ _ _ => "Otbnz"
+  | Otbz _ _ _ => "Otbz"
+  | Obtbl _ => "Obtbl"
   | OIncremPC _ => "OIncremPC"
   (*| Oj_l _ => "Oj_l"*)
-  (*| Ocb _ _ => "Ocb"*)
   (*| Ocbu _ _ => "Ocbu"*)
   (*| Odiv => "Odiv"*)
   (*| Odivu => "Odivu"*)
   (*| Ojumptable _ => "Ojumptable"*)
-  (*| OError => "OError"*)
+  | OError => "OError"
   (*| OIncremPC _ => "OIncremPC"*)
   end.
 
@@ -2495,6 +2611,12 @@ Definition string_of_allocf (op: allocf_op) : pstring :=
   | OAllocf_Mem _ _ => "OAllocf_Mem"
   end.
 
+Definition string_of_freef (op: freef_op) : pstring :=
+  match op with
+  | OFreef_SP _ _ => "OFreef_SP"
+  | OFreef_Mem _ _ => "OFreef_Mem"
+  end.
+
 Definition string_of_op (op: P.op): ?? pstring := 
   match op with
   | Arith op => RET (string_of_arith op)
@@ -2502,10 +2624,12 @@ Definition string_of_op (op: P.op): ?? pstring :=
   | Store op => RET (string_of_store op)
   | Control op => RET (string_of_control op)
   | Allocframe op => RET (string_of_allocf op)
-  (*| Allocframe2 _ _ => RET (Str "Allocframe2")*)
-  (*| Freeframe _ _ => RET (Str "Freeframe")*)
-  (*| Freeframe2 _ _ => RET (Str "Freeframe2")*)
+  | Freeframe op => RET (string_of_freef op)
+  | Loadsymbol _ => RET (Str "Loadsymbol")
   | Constant _ => RET (Str "Constant")
+  | Cvtsw2x => RET (Str "Cvtsw2x")
+  | Cvtuw2x => RET (Str "Cvtuw2x")
+  | Cvtx2w => RET (Str "Cvtx2w")
   (*| Fail => RET (Str "Fail")*)
   end.
 End SECT_BBLOCK_EQUIV.