Asmblock: First attempt at completing PArith/ar_instruction/...

Pmovk is currently missing. (Pmovk aloways uses a register as both
source and desintation)

1 files changed, 626 insertions, 38 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 19e8dd85..50c1a387 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -25,8 +25,6 @@ NOTE: this file is inspired from
    - aarch64/Asm.v
    - kvx/Asmvliw.v (only the Asmblock syntax)
    - kvx/Asmblock.v
-
-
 *)
 
 
@@ -229,6 +227,7 @@ Inductive load_rd_a: Type :=
   | Pldrsh (sz: isize)                      (**r load int16, sign-extend *)
   | Pldrzw                                  (**r load int32, zero-extend to int64 *)
   | Pldrsw                                  (**r load int32, sign-extend to int64 *)
+  (* TODO floating point loads *)
   .
 
 (* Actually, Pldp is not used in the aarch64/Asm semantics!
@@ -251,6 +250,7 @@ Inductive store_rs_a : Type :=
   | Pstrx_a                                 (**r store int64 as any64 *)
   | Pstrb                                   (**r store int8 *)
   | Pstrh                                   (**r store int16 *)
+  (* TODO: floating stores *)
   .
 (* Actually, Pstp is not used in the aarch64/Asm semantics!
  * Thus we skip this particular case:
@@ -260,9 +260,301 @@ Inductive store_rs_a : Type :=
  *     .
  *   Coercion PStore : st_instruction >-> basic.
  *)
+
+Inductive arith_name_r : Type :=
+  (** PC-relative addressing *)
+  | Padrp (id: ident) (ofs: ptrofs)                        (**r set [rd] to high address of [id + ofs] *)
+.
+
+(* Arithmetic instructions with conditional execution *)
+Inductive arith_name_c_r : Type :=
+  (** Conditional data processing *)
+  | Pcset (c: testcond)                                    (**r set to 1/0 if cond is true/false *)
+(*
+  | Pcsetm (c: testcond)                                   (**r set to -1/0 if cond is true/false *)
+*)
+.
+
+Inductive arith_name_comparison_f : Type :=
+  (** Floating-point comparison *)
+  | Pfcmp0 (sz: fsize)                                     (**r compare [r1] and [+0.0] *)
+.
+
+Inductive arith_name_rr : Type :=
+  (** Move integer register *)
+  | Pmov
+  (** PC-relative addressing *)
+  | Paddadr (id: ident) (ofs: ptrofs)           (**r add the low address of [id + ofs] *)
+  (** Bit-field operations *)
+  | Psbfiz (sz: isize) (r: int) (s: Z)          (**r sign extend and shift left *)
+  | Psbfx (sz: isize) (r: int) (s: Z)           (**r shift right and sign extend *)
+  | Pubfiz (sz: isize) (r: int) (s: Z)          (**r zero extend and shift left *)
+  | Pubfx (sz: isize) (r: int) (s: Z)           (**r shift right and zero extend *)
+(* Bit operations are not used in the aarch64/asm semantics
+  (** Bit operations *)
+  | Pcls (sz: isize)                            (**r count leading sign bits *)
+  | Pclz (sz: isize)                            (**r count leading zero bits *)
+  | Prev (sz: isize)                            (**r reverse bytes *)
+  | Prev16 (sz: isize)                          (**r reverse bytes in each 16-bit word *)
+*)
+.
+
+Inductive arith_name_comparison_w_r0r : Type :=
+  (** Integer arithmetic, shifted register *)
+  | PcmpW (s: shift_op)             (**r compare *)
+  | PcmnW (s: shift_op)             (**r compare negative *)
+  (** Logical, shifted register *)
+  | PtstW (s: shift_op)             (**r and, then set flags *)
+.
+
+Inductive arith_name_comparison_x_r0r : Type :=
+  (** Integer arithmetic, shifted register *)
+  | PcmpX (s: shift_op)             (**r compare *)
+  | PcmnX (s: shift_op)             (**r compare negative *)
+  (** Logical, shifted register *)
+  | PtstX (s: shift_op)             (**r and, then set flags *)
+.
+
+Inductive arith_name_comparison_rr : Type :=
+  (** Integer arithmetic, extending register *)
+  | Pcmpext (x: extend_op)                      (**r int64-int32 cmp *)
+  | Pcmnext (x: extend_op)                      (**r int64-int32 cmn *)
+.
+
+Inductive arith_name_ff : Type :=
+  (** Floating-point move *)
+  | Pfmov
+  (** Floating-point conversions *)
+  | Pfcvtds                                           (**r convert float32 to float64 *)
+  | Pfcvtsd                                           (**r convert float64 to float32 *)
+  (** Floating-point arithmetic *)
+  | Pfabs (sz: fsize)                                 (**r absolute value *)
+  | Pfneg (sz: fsize)                                 (**r negation *)
+  (* Pfsqrt is not used in the semantics of aarch64/asm
+  | Pfsqrt (sz: fsize)                                (**r square root *) *)
+.
+
+Inductive arith_name_comparison_ff : Type :=
+  (** Floating-point comparison *)
+  | Pfcmp (sz: fsize)                                 (**r compare [r1] and [r2] *)
+.
+
+(* TODO? Can arith_name_fr and arith_name_rf be collapsed into one type
+ * (switching the argument order when evaluating for one of them)?
+ * Or must these be two different types since the target register is
+ * either an integer or a floating point register? *)
+Inductive arith_name_fr : Type :=
+  (** Floating-point conversions *)
+  | Pscvtf (fsz: fsize) (isz: isize)                  (**r convert signed int to float *)
+  | Pucvtf (fsz: fsize) (isz: isize)                  (**r convert unsigned int to float *)
+.
+
+Inductive arith_name_sw_fr0 : Type :=
+  (** Floating-point move *)
+  | PfmoviSW                                          (**r copy int reg to FP reg *)
+.
+
+Inductive arith_name_dx_fr0 : Type :=
+  (** Floating-point move *)
+  | PfmoviDX                                          (**r copy int reg to FP reg *)
+.
+
+Inductive arith_name_rf : Type := 
+  (** Floating-point conversions *)
+  | Pfcvtzs (isz: isize) (fsz: fsize)                 (**r convert float to signed int *)
+  | Pfcvtzu (isz: isize) (fsz: fsize)                 (**r convert float to unsigned int *)
+.
+
+Inductive arith_name_ri : Type :=
+  (** Move wide immediate *)
+  | Pmovz (sz: isize) (pos: Z)                        (**r move [n << pos] to [rd] *)
+  | Pmovn (sz: isize) (pos: Z)                        (**r move [NOT(n << pos)] to [rd] *)
+  (* TODO? move to rri since we need the value of rd
+  | Pmovk (sz: isize) (pos: Z)                        (**r insert 16 bits of [n] at [pos] in rd *) *)
+.
+
+Inductive arith_name_comparison_ri : Type :=
+  (** Integer arithmetic, immediate *)
+  | Pcmpimm (sz: isize)                               (**r compare *)
+  | Pcmnimm (sz: isize)                               (**r compare negative *)
+  (** Logical, immediate *)
+  | Ptstimm (sz: isize)                               (**r and, then set flags *)
+.
+
+Inductive arith_name_ff32 : Type :=
+  (** Floating-point move *)
+  | Pfmovimms                                         (**r load float32 constant *)
+.
+
+Inductive arith_name_ff64 : Type :=
+  (** Floating-point move *)
+  | Pfmovimmd                                         (**r load float64 constant *)
+.
+
+Inductive arith_name_rrr : Type :=
+  (** Variable shifts *)
+  | Pasrv (sz: isize)                                 (**r arithmetic right shift *)
+  | Plslv (sz: isize)                                 (**r left shift *)
+  | Plsrv (sz: isize)                                 (**r logical right shift *)
+  | Prorv (sz: isize)                                 (**r rotate right *)
+  (** Integer multiply/divide *)
+  | Psmulh                                            (**r signed multiply high *)
+  | Pumulh                                            (**r unsigned multiply high *)
+  | Psdiv (sz: isize)                                 (**r signed division *)
+  | Pudiv (sz: isize)                                 (**r unsigned division *)
+.
+
+Inductive arith_name_c_rrr : Type :=
+  (** Conditional data processing *)
+  | Pcsel (c: testcond)                               (**r int conditional move *)
+.
+
+Inductive arith_name_rsprspr : Type :=
+  (** Integer arithmetic, extending register *)
+  | Paddext (x: extend_op)                            (**r int64-int32 add *)
+  | Psubext (x: extend_op)                            (**r int64-int32 sub *)
+.
+
+Inductive arith_name_w_rr0r : Type :=
+  (** Integer arithmetic, shifted register *)
+  | PaddW (s: shift_op)                               (**r addition *)
+  | PsubW (s: shift_op)                               (**r subtraction *)
+  (** Logical, shifted register *)
+  | PandW (s: shift_op)                               (**r and *)
+  | PbicW (s: shift_op)                               (**r and-not *)
+  | PeonW (s: shift_op)                               (**r xor-not *)
+  | PeorW (s: shift_op)                               (**r xor *)
+  | PorrW (s: shift_op)                               (**r or *)
+  | PornW (s: shift_op)                               (**r or-not *)
+.
+
+Inductive arith_name_x_rr0r : Type :=
+  (** Integer arithmetic, shifted register *)
+  | PaddX (s: shift_op)                               (**r addition *)
+  | PsubX (s: shift_op)                               (**r subtraction *)
+  (** Logical, shifted register *)
+  | PandX (s: shift_op)                               (**r and *)
+  | PbicX (s: shift_op)                               (**r and-not *)
+  | PeonX (s: shift_op)                               (**r xor-not *)
+  | PeorX (s: shift_op)                               (**r xor *)
+  | PorrX (s: shift_op)                               (**r or *)
+  | PornX (s: shift_op)                               (**r or-not *)
+.
+
+Inductive arith_name_fff : Type :=
+  (** Floating-point arithmetic *)
+  | Pfadd (sz: fsize)                                (**r addition *)
+  | Pfdiv (sz: fsize)                                (**r division *)
+  | Pfmul (sz: fsize)                                (**r multiplication *)
+  | Pfsub (sz: fsize)                                (**r subtraction *)
+.
+
+Inductive arith_name_c_fff : Type :=
+  (** Floating-point conditional select *)
+  | Pfsel (cond: testcond)
+.
+
+Inductive arith_name_rsprspi : Type :=
+  (** Integer arithmetic, immediate *)
+  | Paddimm (sz: isize)                             (**r addition *)
+  | Psubimm (sz: isize)                             (**r subtraction *)
+.
+
+Inductive arith_name_w_rr0i : Type :=
+  (** Logical, immediate *)
+  | PandimmW                                        (**r and *)
+  | PeorimmW                                        (**r xor *)
+  | PorrimmW                                        (**r or *)
+.
+
+Inductive arith_name_x_rr0i : Type :=
+  (** Logical, immediate *)
+  | PandimmX                                        (**r and *)
+  | PeorimmX                                        (**r xor *)
+  | PorrimmX                                        (**r or *)
+.
+
+
+Inductive arith_name_w_arrrr0 : Type :=
+  (** Integer multiply/divide *)
+  | PmaddW                                          (**r multiply-add *)
+  | PmsubW                                          (**r multiply-sub *)
+.
+
+Inductive arith_name_x_arrrr0 : Type :=
+  (** Integer multiply/divide *)
+  | PmaddX                                          (**r multiply-add *)
+  | PmsubX                                          (**r multiply-sub *)
+.
+
+Inductive arith_name_afff : Type :=
+  (** Floating-point arithmetic *)
+  | Pfnmul (sz: fsize)                              (**r multiply-negate *)
+.
+
+Inductive arith_name_affff : Type :=
+  (** Floating-point arithmetic *)
+  | Pfmadd (sz: fsize)                              (**r [rd = r3 + r1 * r2] *)
+  | Pfmsub (sz: fsize)                              (**r [rd = r3 - r1 * r2] *)
+.
+
+Inductive arith_name_aaffff : Type :=
+  (** Floating-point arithmetic *)
+  | Pfnmadd (sz: fsize)                             (**r [rd = - r3 - r1 * r2] *)
+  | Pfnmsub (sz: fsize)                             (**r [rd = - r3 + r1 * r2] *)
+.
+
+(* Notes on the naming scheme used here:
+ * R: ireg
+ * R0: ireg0
+ * Rsp: iregsp
+ * F: freg
+ * W/X: Occur in conjunction with R0, says whether an ireg0 should be evaluated
+ *      as W regsiter (32 bit) or X register (64 bit)
+ * S/D: Used for completeness sake. Only used for copying an integer register
+ *      to a floating point register. Could be removed.
+ * A: These instructions perform an additional arithmetic operation
+      XXX Does this interpretation match the use in kvx/Asmvliw?
+ * Comparison: For these instructions the first register is not the target.
+ *             Instead, the condition register is mutated.
+ *)
+Inductive ar_instruction : Type :=
+  | PArithR (i : arith_name_r) (rd : ireg)
+  | PArithRR (i : arith_name_rr) (rd rs : ireg)
+  | PArithRI (i : arith_name_ri) (rd : ireg) (n : Z)
+  | PArithRF (i : arith_name_rf) (rd : ireg) (rs : freg)
+  | PArithRRR (i : arith_name_rrr) (rd r1 r2 : ireg)
+  | PArithWRR0R (i : arith_name_w_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
+  | PArithXRR0R (i : arith_name_x_rr0r) (rd : ireg) (r1 : ireg0) (r2 : ireg)
+  | PArithWRR0I (i : arith_name_w_rr0i) (rd : ireg) (r1 : ireg0) (n : Z)
+  | PArithXRR0I (i : arith_name_x_rr0i) (rd : ireg) (r1 : ireg0) (n : Z)
+  | PArithRspRspR (i : arith_name_rsprspr) (rd r1 : iregsp) (r2 : ireg)
+  | PArithRspRspI (i : arith_name_rsprspi) (rd r1 : iregsp) (n : Z)
+  | PArithWARRRR0 (i : arith_name_w_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
+  | PArithXARRRR0 (i : arith_name_x_arrrr0) (rd r1 r2 : ireg) (r3 : ireg0)
+  | PArithFF (i : arith_name_ff) (rd rs : freg)
+  | PArithFF32 (i : arith_name_ff32) (rd : freg) (f : float32)
+  | PArithFF64 (i : arith_name_ff64) (rd : freg) (f : float)
+  | PArithFR (i : arith_name_fr) (rd : freg) (rs : ireg)
+  | PArithSWFR0 (i : arith_name_sw_fr0) (rd : freg) (rs : ireg0)
+  | PArithDXFR0 (i : arith_name_dx_fr0) (rd : freg) (rs : ireg0)
+  | PArithFFF (i : arith_name_fff) (rd r1 r2 : freg)
+  | PArithAFFF (i : arith_name_afff) (rd r1 r2 : freg)
+  (* Pfmadd and Pfmsub are currently not used by the semantics of aarch64/Asm
+  | PArithAFFFF (i : arith_name_affff) (rd r1 r2 r3 : freg) *)
+  (* Pfnmadd and Pfnmsub are currently not used by the semantics of aarch64/Asm
+  | PArithAAFFFF (i : arith_name_aaffff) (rd r1 r2 r3 : freg) *)
+  | PArithComparisonRR (i : arith_name_comparison_rr) (r1 r2 : ireg)
+  | PArithComparisonWR0R (i : arith_name_comparison_w_r0r) (r1 : ireg0) (r2 : ireg)
+  | PArithComparisonXR0R (i : arith_name_comparison_x_r0r) (r1 : ireg0) (r2 : ireg)
+  | PArithComparisonRI (i : arith_name_comparison_ri) (r1 : ireg) (n : Z)
+  | PArithComparisonF (i: arith_name_comparison_f) (r1 : freg)
+  | PArithComparisonFF (i : arith_name_comparison_ff) (rd rs : freg)
+.
+
 Inductive basic : Type :=
-  (* | PArith          (i: ar_instruction) *) (* TODO *)
-  | PLoad (ld: load_rd_a) (rd: ireg) (a: addressing)
+  | PArith (i: ar_instruction)                                        (**r TODO *)
+  | PLoad (ld: load_rd_a) (rd: ireg) (a: addressing)                  (**r TODO *)
   | PStore (st: store_rs_a) (r: ireg) (a: addressing)                 (**r TODO *)
   | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
   | Pfreeframe (sz: Z) (linkofs: ptrofs)                              (**r deallocate stack frame and restore previous frame *)
@@ -275,8 +567,7 @@ Inductive basic : Type :=
   | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
   | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
 *)
-  .
-
+.
 
 (** * Definition of a bblock
 
@@ -889,36 +1180,6 @@ Definition interp_load_rd_a (ld: load_rd_a): val -> val :=
   | _ => fun v => v
   end.
 
-
-(* basic exec *)
-Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
-  match b with
-  | PLoad ld rd a => exec_load (chunk_load_rd_a ld) (interp_load_rd_a ld) a rd rs m
-  | PStore st r a => exec_store (chunk_store_rs_a st) a rs#r rs m
-  | Pallocframe sz pos =>
-      let (m1, stk) := Mem.alloc m 0 sz in
-      let sp := (Vptr stk Ptrofs.zero) in
-      SOME m2 <- Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP IN
-      Next (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef) m2
-  | Pfreeframe sz pos =>
-      SOME v <- Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) IN
-      match rs#SP with
-      | Vptr stk ofs =>
-        SOME m' <- Mem.free m stk 0 sz IN
-        Next (rs#SP <- v #X16 <- Vundef) m'
-      | _ => Stuck
-      end
-  | Ploadsymbol rd id =>
-      Next (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero)) m
-  | Pcvtsw2x rd r1 =>
-      Next (rs#rd <- (Val.longofint rs#r1)) m
-  | Pcvtuw2x rd r1 =>
-      Next (rs#rd <- (Val.longofintu rs#r1)) m
-  | Pcvtx2w rd =>
-      Next (rs#rd <- (Val.loword rs#rd)) m
-  end
-.
-
 (** TODO: redundant w.r.t Machblock ?? *)
 Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
 Proof.
@@ -966,7 +1227,7 @@ Definition eval_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: o
   SOME res <- ores IN
   if res then goto_label f lbl rs m else Next rs m.
 
-Definition eval_neg_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
+Definition  eval_neg_branch (f: function) (lbl: label) (rs: regset) (m: mem) (ores: option bool) :=
   SOME res <- ores IN
   if res then Next rs m else goto_label f lbl rs m.
 
@@ -1005,6 +1266,332 @@ Definition exec_cfi (f: function) (cfi: cf_instruction) (rs: regset) (m: mem) :
       end
   end.
 
+Definition arith_eval_r n :=
+  match n with
+  (* XXX change from ge to lk similar to ADadr change *)
+  | Padrp id ofs => symbol_high lk id ofs
+  end.
+
+Definition arith_eval_rr n v :=
+  match n with
+  | Pmov => v
+  (* XXX change from ge to lk *)
+  | Paddadr id ofs => Val.addl v (symbol_low lk id ofs)
+  | Psbfiz W r s => Val.shl (Val.sign_ext s v) (Vint r)
+  | Psbfiz X r s => Val.shll (Val.sign_ext_l s v) (Vint r)
+  | Psbfx W r s => Val.sign_ext s (Val.shr v (Vint r))
+  | Psbfx X r s => Val.sign_ext_l s (Val.shrl v (Vint r))
+  | Pubfiz W r s => Val.shl (Val.zero_ext s v) (Vint r)
+  | Pubfiz X r s => Val.shll (Val.zero_ext_l s v) (Vint r)
+  | Pubfx W r s => Val.zero_ext s (Val.shru v (Vint r))
+  | Pubfx X r s => Val.zero_ext_l s (Val.shrlu v (Vint r))
+  end.
+
+Definition arith_eval_ri n i :=
+  match n with
+  | Pmovz W pos => Vint (Int.repr (Z.shiftl i pos))
+  | Pmovz X pos => Vlong (Int64.repr (Z.shiftl i pos))
+  | Pmovn W pos => Vint (Int.repr (Z.lnot (Z.shiftl i pos)))
+  | Pmovn X pos => Vlong (Int64.repr (Z.lnot (Z.shiftl i pos)))
+  (* TODO need to move Pmovk to rri to make rd's old value available
+  | Pmovk W pos => insert_in_int rs#rd n pos 16
+  | Pmovk X pos => insert_in_long rs#rd n pos 16 *)
+  end.
+
+Definition arith_eval_rf n v :=
+  match n with
+  | Pfcvtzs W S => Val.maketotal (Val.intofsingle v)
+  | Pfcvtzs W D => Val.maketotal (Val.intoffloat v)
+  | Pfcvtzs X S => Val.maketotal (Val.longofsingle v)
+  | Pfcvtzs X D => Val.maketotal (Val.longoffloat v)
+  | Pfcvtzu W S => Val.maketotal (Val.intuofsingle v)
+  | Pfcvtzu W D => Val.maketotal (Val.intuoffloat v)
+  | Pfcvtzu X S => Val.maketotal (Val.longuofsingle v)
+  | Pfcvtzu X D => Val.maketotal (Val.longuoffloat v)
+  end.
+
+Definition arith_eval_rrr n v1 v2 :=
+  match n with
+  | Pasrv W => Val.shr v1 v2
+  | Pasrv X => Val.shrl v1 v2
+  | Plslv W => Val.shl v1 v2
+  | Plslv X => Val.shll v1 v2
+  | Plsrv W => Val.shru v1 v2
+  | Plsrv X => Val.shrlu v1 v2
+  | Prorv W => Val.ror v1 v2
+  | Prorv X => Val.rorl v1 v2
+  | Psmulh => Val.mullhs v1 v2
+  | Pumulh => Val.mullhu v1 v2
+  | Psdiv W => Val.maketotal (Val.divs v1 v2)
+  | Psdiv X => Val.maketotal (Val.divls v1 v2)
+  | Pudiv W => Val.maketotal (Val.divu v1 v2)
+  | Pudiv X => Val.maketotal (Val.divlu v1 v2)
+  end.
+
+(* obtain v1 by rs##r1 *)
+Definition arith_eval_w_rr0r n v1 v2 :=
+  match n with
+  | PaddW s => Val.add v1 (eval_shift_op_int v2 s)
+  | PsubW s => Val.sub v1 (eval_shift_op_int v2 s)
+  | PandW s => Val.and v1 (eval_shift_op_int v2 s)
+  | PbicW s => Val.and v1 (Val.notint (eval_shift_op_int v2 s))
+  | PeonW s => Val.xor v1 (Val.notint (eval_shift_op_int v2 s))
+  | PeorW s => Val.xor v1 (eval_shift_op_int v2 s)
+  | PorrW s => Val.or v1 (eval_shift_op_int v2 s)
+  | PornW s => Val.or v1 (Val.notint (eval_shift_op_int v2 s))
+  end.
+
+(* obtain v1 by rs###r1 *)
+Definition arith_eval_x_rr0r n v1 v2 :=
+  match n with
+  | PaddX s => Val.addl v1 (eval_shift_op_long v2 s)
+  | PsubX s => Val.subl v1 (eval_shift_op_long v2 s)
+  | PandX s => Val.andl v1 (eval_shift_op_long v2 s)
+  | PbicX s => Val.andl v1 (Val.notl (eval_shift_op_long v2 s))
+  | PeonX s => Val.xorl v1 (Val.notl (eval_shift_op_long v2 s))
+  | PeorX s => Val.xorl v1 (eval_shift_op_long v2 s)
+  | PorrX s => Val.orl v1 (eval_shift_op_long v2 s)
+  | PornX s => Val.orl v1 (Val.notl (eval_shift_op_long v2 s))
+  end.
+
+(* obtain v by rs##r1 *)
+Definition arith_eval_w_rr0i n v i :=
+  match n with
+  | PandimmW => Val.and v (Vint (Int.repr i))
+  | PeorimmW => Val.xor v (Vint (Int.repr i))
+  | PorrimmW => Val.or v (Vint (Int.repr i))
+  end.
+
+(* obtain v by rs###r1 *)
+Definition arith_eval_x_rr0i n v i :=
+  match n with
+  | PandimmX => Val.andl v (Vlong (Int64.repr i))
+  | PeorimmX => Val.xorl v (Vlong (Int64.repr i))
+  | PorrimmX => Val.orl v (Vlong (Int64.repr i))
+  end.
+
+Definition arith_eval_rsprspr n v1 v2 :=
+  match n with
+  | Paddext x => Val.addl v1 (eval_extend v2 x)
+  | Psubext x => Val.subl v2 (eval_extend v2 x)
+  end.
+
+Definition arith_eval_rsprspi n v i :=
+  match n with
+  | Paddimm W => Val.add v (Vint (Int.repr i))
+  | Paddimm X => Val.addl v (Vlong (Int64.repr i))
+  | Psubimm W => Val.sub v (Vint (Int.repr i))
+  | Psubimm X => Val.subl v (Vlong (Int64.repr i))
+  end.
+
+(* obtain v3 by rs##r3 *)
+Definition arith_eval_w_arrrr0 n v1 v2 v3 :=
+  match n with
+  | PmaddW => Val.add v3 (Val.mul v1 v2)
+  | PmsubW => Val.sub v3 (Val.mul v1 v2)
+  end.
+
+(* obtain v3 by rs###r3 *)
+Definition arith_eval_x_arrrr0 n v1 v2 v3 :=
+  match n with
+  | PmaddX => Val.addl v3 (Val.mull v1 v2)
+  | PmsubX => Val.subl v3 (Val.mull v1 v2)
+  end.
+
+Definition arith_eval_ff n v :=
+  match n with
+  | Pfmov => v
+  | Pfcvtds => Val.floatofsingle v
+  | Pfcvtsd => Val.singleoffloat v
+  | Pfabs S => Val.absfs v
+  | Pfabs D => Val.absf v
+  | Pfneg S => Val.negfs v
+  | Pfneg D => Val.negf v
+  end.
+
+Definition arith_eval_ff32 n i :=
+  match n with
+  | Pfmovimms => Vsingle i
+  end.
+
+Definition arith_eval_ff64 n i :=
+  match n with
+  | Pfmovimmd => Vfloat i
+  end.
+
+Definition arith_eval_fr n v :=
+  match n with
+  | Pscvtf S W => Val.maketotal (Val.singleofint v)
+  | Pscvtf D W => Val.maketotal (Val.floatofint v)
+  | Pscvtf S X => Val.maketotal (Val.singleoflong v)
+  | Pscvtf D X => Val.maketotal (Val.floatoflong v)
+  | Pucvtf S W => Val.maketotal (Val.singleofintu v)
+  | Pucvtf D W => Val.maketotal (Val.floatofintu v)
+  | Pucvtf S X => Val.maketotal (Val.singleoflongu v)
+  | Pucvtf D X => Val.maketotal (Val.floatoflongu v)
+  end.
+
+(* obtain v via rs##r1 *)
+Definition arith_eval_sw_fr0 n v :=
+  match n with
+  | PfmoviSW => float32_of_bits v
+  end.
+
+(* obtain v via rs###r1 *)
+Definition arith_eval_dx_fr0 n v :=
+  match n with
+  | PfmoviDX => float64_of_bits v
+  end.
+
+Definition arith_eval_fff n v1 v2 :=
+  match n with
+  | Pfadd S => Val.addfs v1 v2
+  | Pfadd D => Val.addf v1 v2
+  | Pfdiv S => Val.divfs v1 v2
+  | Pfdiv D => Val.divf v1 v2
+  | Pfmul S => Val.mulfs v1 v2
+  | Pfmul D => Val.mulf v1 v2
+  | Pfsub S => Val.subfs v1 v2
+  | Pfsub D => Val.subf v1 v2
+  end.
+
+Definition arith_eval_afff n v1 v2 :=
+  match n with
+  | Pfnmul S => Val.negfs (Val.mulfs v1 v2)
+  | Pfnmul D => Val.negf (Val.mulf v1 v2)
+  end.
+
+Definition arith_prepare_comparison_rr n (v1 v2 : val) :=
+  match n with
+  | Pcmpext x => (v1, (eval_extend v2 x))
+  | Pcmnext x => (v1, (Val.negl (eval_extend v2 x)))
+  end.
+
+Definition arith_prepare_comparison_w_r0r n v1 v2 :=
+  match n with
+  | PcmpW s => (v1, (eval_shift_op_int v2 s))
+  | PcmnW s => (v1, (Val.neg (eval_shift_op_int v2 s)))
+  | PtstW s => ((Val.and v1 (eval_shift_op_int v2 s)), (Vint Int.zero))
+  end.
+
+Definition arith_prepare_comparison_x_r0r n v1 v2 :=
+  match n with
+  | PcmpX s => (v1, (eval_shift_op_long v2 s))
+  | PcmnX s => (v1, (Val.negl (eval_shift_op_long v2 s)))
+  | PtstX s => ((Val.andl v1 (eval_shift_op_long v2 s)), (Vlong Int64.zero))
+  end.
+
+Definition arith_prepare_comparison_ri n v i :=
+  match n with
+  | Pcmpimm W => (v, (Vint (Int.repr i)))
+  | Pcmpimm X => (v, (Vlong (Int64.repr i)))
+  | Pcmnimm W => (v, (Vint (Int.neg (Int.repr i))))
+  | Pcmnimm X => (v, (Vlong (Int64.neg (Int64.repr i))))
+  | Ptstimm W => ((Val.and v (Vint (Int.repr i))), (Vint Int.zero))
+  | Ptstimm X => ((Val.andl v (Vlong (Int64.repr i))), (Vlong Int64.zero))
+  end.
+
+(* Without val annotation unification fails *)
+Definition arith_prepare_comparison_f n (v : val) :=
+  match n with
+  | Pfcmp0 S => (v, (Vsingle Float32.zero))
+  | Pfcmp0 D => (v, (Vfloat Float.zero))
+  end.
+
+Definition arith_prepare_comparison_ff n (v1 v2 : val) :=
+  match n with
+  | Pfcmp _ => (v1, v2)
+  end.
+
+Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
+  match ai with
+  | PArithR n d => rs#d <- (arith_eval_r n)
+  | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s)
+  | PArithRI n d i => rs#d <- (arith_eval_ri n i)
+  | PArithRF n d s => rs#d <- (arith_eval_rf n rs#s)
+  | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2)
+
+  | PArithWRR0R n d s1 s2 => rs#d <- (arith_eval_w_rr0r n rs##s1 rs#s2)
+  | PArithXRR0R n d s1 s2 => rs#d <- (arith_eval_x_rr0r n rs###s1 rs#s2)
+
+  | PArithWRR0I n d s i => rs#d <- (arith_eval_w_rr0i n rs##s i)
+  | PArithXRR0I n d s i => rs#d <- (arith_eval_x_rr0i n rs###s i)
+
+  | PArithRspRspR n d s1 s2 => rs#d <- (arith_eval_rsprspr n rs#s1 rs#s2)
+  | PArithRspRspI n d s i => rs#d <- (arith_eval_rsprspi n rs#s i)
+
+  | PArithWARRRR0 n d s1 s2 s3 => rs#d <- (arith_eval_w_arrrr0 n rs#s1 rs#s2 rs##s3)
+  | PArithXARRRR0 n d s1 s2 s3 => rs#d <- (arith_eval_x_arrrr0 n rs#s1 rs#s2 rs###s3)
+
+  | PArithFF n d s => rs#d <- (arith_eval_ff n rs#s)
+  | PArithFF32 n d i => rs#d <- (arith_eval_ff32 n i)
+  | PArithFF64 n d i => rs#d <- (arith_eval_ff64 n i)
+  | PArithFR n d s => rs#d <- (arith_eval_fr n rs#s)
+
+  | PArithSWFR0 n d s => rs#d <- (arith_eval_sw_fr0 n rs##s)
+  | PArithDXFR0 n d s => rs#d <- (arith_eval_dx_fr0 n rs###s)
+
+  | PArithFFF n d s1 s2 => rs#d <- (arith_eval_fff n rs#s1 rs#s2)
+  | PArithAFFF n d s1 s2 => rs#d <- (arith_eval_afff n rs#s1 rs#s2)
+
+  | PArithComparisonRR n s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_rr n rs#s1 rs#s2 in
+      compare_long rs v1 v2
+  | PArithComparisonWR0R n s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_w_r0r n rs##s1 rs#s2 in
+      compare_int rs v1 v2
+  | PArithComparisonXR0R n s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_x_r0r n rs###s1 rs#s2 in
+      compare_long rs v1 v2
+  | PArithComparisonRI n s i =>
+    let (v1, v2) := arith_prepare_comparison_ri n rs#s i in
+      (match n with
+      | Pcmpimm W | Pcmnimm W | Ptstimm W => compare_int rs v1 v2
+      | Pcmpimm X | Pcmnimm X | Ptstimm X => compare_long rs v1 v2
+      end)
+  | PArithComparisonF n s =>
+    let (v1, v2) := arith_prepare_comparison_f n rs#s in
+    (match n with
+    | Pfcmp0 S => compare_single rs v1 v2
+    | Pfcmp0 D => compare_float rs v1 v2
+    end)
+  | PArithComparisonFF n s1 s2 =>
+    let (v1, v2) := arith_prepare_comparison_ff n rs#s1 rs#s2 in
+    (match n with
+    | Pfcmp S => compare_single rs v1 v2
+    | Pfcmp D => compare_float rs v1 v2
+    end)
+  end.
+
+(* basic exec *)
+Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
+  match b with
+  | PArith ai => Next (exec_arith_instr ai rs) m
+  | PLoad ld rd a => exec_load (chunk_load_rd_a ld) (interp_load_rd_a ld) a rd rs m
+  | PStore st r a => exec_store (chunk_store_rs_a st) a rs#r rs m
+  | Pallocframe sz pos =>
+      let (m1, stk) := Mem.alloc m 0 sz in
+      let sp := (Vptr stk Ptrofs.zero) in
+      SOME m2 <- Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP IN
+      Next (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef) m2
+  | Pfreeframe sz pos =>
+      SOME v <- Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) IN
+      match rs#SP with
+      | Vptr stk ofs =>
+        SOME m' <- Mem.free m stk 0 sz IN
+        Next (rs#SP <- v #X16 <- Vundef) m'
+      | _ => Stuck
+      end
+  | Ploadsymbol rd id =>
+      Next (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero)) m
+  | Pcvtsw2x rd r1 =>
+      Next (rs#rd <- (Val.longofint rs#r1)) m
+  | Pcvtuw2x rd r1 =>
+      Next (rs#rd <- (Val.longofintu rs#r1)) m
+  | Pcvtx2w rd =>
+      Next (rs#rd <- (Val.loword rs#rd)) m
+  end.
+
 (* TODO: ORIGINAL EXECUTION OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !
 
 (** Execution of a single instruction [i] in initial state
@@ -1261,7 +1848,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#rd <- v)) m
   | Pcset rd cond =>
       let v :=
-        match eval_testcond cond rs with
+        match 
+ cond rs with
         | Some true => Vint Int.one
         | Some false => Vint Int.zero
         | None => Vundef