diff options
Diffstat (limited to 'aarch64/Asmblockdeps.v')
| -rw-r--r-- | aarch64/Asmblockdeps.v | 2688 |
1 files changed, 2688 insertions, 0 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v new file mode 100644 index 00000000..5cd049c5 --- /dev/null +++ b/aarch64/Asmblockdeps.v @@ -0,0 +1,2688 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(** * Translation from [Asmblock] to [AbstractBB] *) + +(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmblock] into [L]. + [AbstractBB] will then define a sequential semantics for [L]. + We prove a bisimulation between the sequential semantics of [L] and [Asmblock]. + Then, the checker on [Asmblock] is deduced from those of [L]. + *) + +Require Import AST. +Require Import Asm Asmblock. +Require Import Asmblockprops. +Require Import Values. +Require Import Globalenvs. +Require Import Memory. +Require Import Errors. +Require Import Integers. +Require Import Floats. +Require Import ZArith. +Require Import Coqlib. +Require Import ImpSimuTest. +Require Import Axioms. +Require Import Permutation. +Require Import Events. + +Require Import Lia. + +Import ListNotations. +Local Open Scope list_scope. + +Open Scope impure. +(** auxiliary treatments of builtins *) + +Definition is_builtin(ex: option control): bool := + match ex with + | Some (Pbuiltin _ _ _) => true + | _ => false + end. + +Definition has_builtin(bb: bblock): bool := + is_builtin (exit bb). + +Remark builtin_arg_eq_dreg: forall (a b: builtin_arg dreg), {a=b} + {a<>b}. +Proof. + intros. + apply (builtin_arg_eq dreg_eq). +Qed. + +Remark builtin_res_eq_dreg: forall (a b: builtin_res dreg), {a=b} + {a<>b}. +Proof. + intros. + apply (builtin_res_eq dreg_eq). +Qed. + +Definition assert_same_builtin (bb1 bb2: bblock): ?? unit := + match exit bb1 with + | Some (Pbuiltin ef1 lbar1 brr1) => + match exit bb2 with + | Some (Pbuiltin ef2 lbar2 brr2) => + if (external_function_eq ef1 ef2) then + if (list_eq_dec builtin_arg_eq_dreg lbar1 lbar2) then + if (builtin_res_eq_dreg brr1 brr2) then RET tt + else FAILWITH "Different brr in Pbuiltin" + else FAILWITH "Different lbar in Pbuiltin" + else FAILWITH "Different ef in Pbuiltin" + | _ => FAILWITH "Expected a builtin: found something else" (* XXX: on peut raffiner le message d'erreur si nécessaire *) + end + | _ => match exit bb2 with + | Some (Pbuiltin ef2 lbar2 brr2) => FAILWITH "Expected a something else: found a builtin" + | _ => RET tt (* ok *) + end + end. + +Lemma assert_same_builtin_correct (bb1 bb2: bblock): + WHEN assert_same_builtin bb1 bb2 ~> _ THEN + has_builtin bb1 = true \/ has_builtin bb2 = true -> exit bb1 = exit bb2. +Proof. + unfold assert_same_builtin, has_builtin. + destruct (exit bb1) as [[]|]; simpl; + destruct (exit bb2) as [[]|]; wlp_simplify; try congruence. +Qed. +Global Opaque assert_same_builtin. +Local Hint Resolve assert_same_builtin_correct: wlp. + +(** Definition of [L] *) + +Module P<: ImpParam. +Module R := Pos. + +Section IMPPARAM. + +Definition env := Genv.t fundef unit. + +Record genv_wrap := { _genv: env; _fn: function; _lk: aarch64_linker }. +Definition genv := genv_wrap. + +Variable Ge: genv. + +Inductive value_wrap := + | Val (v: val) + | Memstate (m: mem) + | Bool (b: bool) +. + +Definition value := value_wrap. + +Record CRflags := { _CN: val; _CZ:val; _CC: val; _CV: val }. + +Inductive control_op := + | Ob (l: label) + | 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) +. + +Inductive arith_op := + | OArithP (n: arith_p) + | OArithPP (n: arith_pp) + | OArithPPP (n: arith_ppp) + | OArithRR0R (n: arith_rr0r) + | OArithRR0R_XZR (n: arith_rr0r) (vz: val) + | OArithRR0 (n: arith_rr0) + | OArithRR0_XZR (n: arith_rr0) (vz: val) + | OArithARRRR0 (n: arith_arrrr0) + | OArithARRRR0_XZR (n: arith_arrrr0) (vz: val) + | OArithComparisonPP_CN (n: arith_comparison_pp) + | OArithComparisonPP_CZ (n: arith_comparison_pp) + | OArithComparisonPP_CC (n: arith_comparison_pp) + | OArithComparisonPP_CV (n: arith_comparison_pp) + | OArithComparisonR0R_CN (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CZ (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CC (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CV (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CN_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) + | OArithComparisonR0R_CZ_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) + | OArithComparisonR0R_CC_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) + | OArithComparisonR0R_CV_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) + | OArithComparisonP_CN (n: arith_comparison_p) + | OArithComparisonP_CZ (n: arith_comparison_p) + | OArithComparisonP_CC (n: arith_comparison_p) + | OArithComparisonP_CV (n: arith_comparison_p) + | Ocset (c: testcond) + | Ofmovi (fsz: fsize) + | Ofmovi_XZR (fsz: fsize) + | Ocsel (c: testcond) + | Ofnmul (fsz: fsize) +. + +Inductive store_op := + | Ostore1 (st: store_rs_a) (chunk: memory_chunk) (a: addressing) + | Ostore2 (st: store_rs_a) (chunk: memory_chunk) (a: addressing) + | OstoreU (st: store_rs_a) (chunk: memory_chunk) (a: addressing) +. + +Inductive load_op := + | Oload1 (ld: load_rd_a) (chunk: memory_chunk) (a: addressing) + | Oload2 (ld: load_rd_a) (chunk: memory_chunk) (a: addressing) + | OloadU (ld: load_rd_a) (chunk: memory_chunk) (a: addressing) +. + +Inductive allocf_op := + | OAllocf_SP (sz: Z) (linkofs: ptrofs) + | 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) +. + +Definition op:=op_wrap. + +Coercion Arith: arith_op >-> op_wrap. +Coercion Control: control_op >-> op_wrap. + +Definition v_compare_int (v1 v2: val) : CRflags := + {| _CN := (Val.negative (Val.sub v1 v2)); + _CZ := (Val.mxcmpu Ceq v1 v2); + _CC := (Val.mxcmpu Cge v1 v2); + _CV := (Val.sub_overflow v1 v2) |}. + +Definition v_compare_long (v1 v2: val) : CRflags := + {| _CN := (Val.negativel (Val.subl v1 v2)); + _CZ := (Val.mxcmplu Ceq v1 v2); + _CC := (Val.mxcmplu Cge v1 v2); + _CV := (Val.subl_overflow v1 v2) |}. + +Definition v_compare_float (v1 v2: val) : CRflags := + match v1, v2 with + | Vfloat f1, Vfloat f2 => + {| _CN := (Val.of_bool (Float.cmp Clt f1 f2)); + _CZ := (Val.of_bool (Float.cmp Ceq f1 f2)); + _CC := (Val.of_bool (negb (Float.cmp Clt f1 f2))); + _CV := (Val.of_bool (negb (Float.ordered f1 f2))) |} + | _, _ => + {| _CN := Vundef; + _CZ := Vundef; + _CC := Vundef; + _CV := Vundef |} + end. + +Definition v_compare_single (v1 v2: val) : CRflags := + match v1, v2 with + | Vsingle f1, Vsingle f2 => + {| _CN := (Val.of_bool (Float32.cmp Clt f1 f2)); + _CZ := (Val.of_bool (Float32.cmp Ceq f1 f2)); + _CC := (Val.of_bool (negb (Float32.cmp Clt f1 f2))); + _CV := (Val.of_bool (negb (Float32.ordered f1 f2))) |} + | _, _ => + {| _CN := Vundef; + _CZ := Vundef; + _CC := Vundef; + _CV := Vundef |} + end. + +Definition arith_eval_comparison_pp (n: arith_comparison_pp) (v1 v2: val) := + let (v1',v2') := arith_prepare_comparison_pp n v1 v2 in + match n with + | Pcmpext _ | Pcmnext _ => v_compare_long v1' v2' + | Pfcmp S => v_compare_single v1' v2' + | Pfcmp D => v_compare_float v1' v2' + end. + +Definition arith_eval_comparison_p (n: arith_comparison_p) (v: val) := + let (v1',v2') := arith_prepare_comparison_p n v in + match n with + | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => v_compare_int v1' v2' + | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => v_compare_long v1' v2' + | Pfcmp0 S => v_compare_single v1' v2' + | Pfcmp0 D => v_compare_float v1' v2' + end. + +Definition arith_eval_comparison_r0r (n: arith_comparison_r0r) (v1 v2: val) (is: isize) := + let (v1',v2') := arith_prepare_comparison_r0r n v1 v2 in + if is then v_compare_int v1' v2' else v_compare_long v1' v2'. + +Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) := + match c with + | TCeq => (**r equal *) + match vCZ with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TCne => (**r not equal *) + match vCZ with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TClo => (**r unsigned less than *) + match vCC with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCls => (**r unsigned less or equal *) + match vCC, vCZ with + | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one) + | _, _ => None + end + | TChs => (**r unsigned greater or equal *) + match vCC with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TChi => (**r unsigned greater *) + match vCC, vCZ with + | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero) + | _, _ => None + end + | TClt => (**r signed less than *) + match vCV, vCN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one) + | _, _ => None + end + | TCle => (**r signed less or equal *) + match vCV, vCN, vCZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one) + | _, _, _ => None + end + | TCge => (**r signed greater or equal *) + match vCV, vCN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero) + | _, _ => None + end + | TCgt => (**r signed greater *) + match vCV, vCN, vCZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero) + | _, _, _ => None + end + | TCpl => (**r positive *) + match vCN with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCmi => (**r negative *) + match vCN with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + end. + +(* The is argument is used to identify the source inst and avoid rewriting some code + 0 -> Ocset + 1 -> Ocsel + 2 -> Obc *) +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 + 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 + | S => float32_of_bits v + | D => float64_of_bits v + end. + +Definition fmovi_eval_xzr (fsz: fsize) := + match fsz with + | S => float32_of_bits (Vint Int.zero) + | D => float64_of_bits (Vlong Int64.zero) + end. + +Definition fnmul_eval (fsz: fsize) (v1 v2: val) := + match fsz with + | S => Val.negfs (Val.mulfs v1 v2) + | D => Val.negf (Val.mulf v1 v2) + end. + +Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is: Z) := + match c, l with + | 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. + +Definition arith_op_eval (op: arith_op) (l: list value) := + match op, l with + | OArithP n, [] => Some (Val (arith_eval_p Ge.(_lk) n)) + | OArithPP n, [Val v] => Some (Val (arith_eval_pp Ge.(_lk) n v)) + | OArithPPP n, [Val v1; Val v2] => Some (Val (arith_eval_ppp n v1 v2)) + | OArithRR0R n, [Val v1; Val v2] => Some (Val (arith_eval_rr0r n v1 v2)) + | OArithRR0R_XZR n vz, [Val v] => Some (Val (arith_eval_rr0r n vz v)) + | OArithRR0 n, [Val v] => Some (Val (arith_eval_rr0 n v)) + | OArithRR0_XZR n vz, [] => Some (Val (arith_eval_rr0 n vz)) + | OArithARRRR0 n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrrr0 n v1 v2 v3)) + | OArithARRRR0_XZR n vz, [Val v1; Val v2] => Some (Val (arith_eval_arrrr0 n v1 v2 vz)) + | OArithComparisonPP_CN n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CN))) + | OArithComparisonPP_CZ n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CZ))) + | OArithComparisonPP_CC n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CC))) + | OArithComparisonPP_CV n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CV))) + | OArithComparisonR0R_CN n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CN))) + | OArithComparisonR0R_CZ n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CZ))) + | OArithComparisonR0R_CC n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CC))) + | OArithComparisonR0R_CV n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CV))) + | OArithComparisonR0R_CN_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CN))) + | OArithComparisonR0R_CZ_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CZ))) + | OArithComparisonR0R_CC_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CC))) + | OArithComparisonR0R_CV_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CV))) + | OArithComparisonP_CN n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CN))) + | 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 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 1 + | Ofnmul fsz, [Val v1; Val v2] => Some (Val (fnmul_eval fsz v1 v2)) + | _, _ => None + end. + +Definition call_ll_storev (c: memory_chunk) (m: mem) (v: option val) (vs: val) := + match v with + | Some va => match Mem.storev c m va vs with + | Some m' => Some (Memstate m') + | None => None + end + | None => None (* should never occurs *) + end. + +Definition exec_store1 (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr vs: val) := + let v := + match a with + | ADimm _ n => Some (Val.addl vs (Vlong n)) + | ADadr _ id ofs => Some (Val.addl vs (symbol_low Ge.(_lk) id ofs)) + | _ => None + end in + call_ll_storev chunk m v vr. + +Definition exec_store2 (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr vs1 vs2: val) := + let v := + match a with + | ADreg _ _ => Some (Val.addl vs1 vs2) + | ADlsl _ _ n => Some (Val.addl vs1 (Val.shll vs2 (Vint n))) + | ADsxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofint vs2) (Vint n))) + | ADuxt _ _ n => Some (Val.addl vs1 (Val.shll (Val.longofintu vs2) (Vint n))) + | _ => None + end in + call_ll_storev chunk m v vr. + +Definition exec_storeU (n: store_rs_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vr: val) := + call_ll_storev chunk m None vr. + +Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := + match label_pos lbl 0 (fn_blocks f) with + | None => None + | Some pos => + match vpc with + | Vptr b ofs => Some (Val (Vptr b (Ptrofs.repr pos))) + | _ => None + end + end. + +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. + +Definition store_eval (o: store_op) (l: list value) := + match o, l with + | Ostore1 st chunk a, [Val vr; Val vs; Memstate m] => exec_store1 st m chunk a vr vs + | Ostore2 st chunk a, [Val vr; Val vs1; Val vs2; Memstate m] => exec_store2 st m chunk a vr vs1 vs2 + | OstoreU st chunk a, [Val vr; Memstate m] => exec_storeU st m chunk a vr + | _, _ => None + end. + +Definition call_ll_loadv (c: memory_chunk) (transf: val -> val) (m: mem) (v: option val) := + match v with + | Some va => match Mem.loadv c m va with + | Some v' => Some (Val (transf v')) + | None => None + end + | None => None (* should never occurs *) + end. + +Definition exec_load1 (ld: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vl: val) := + let v := + match a with + | ADimm _ n => Some (Val.addl vl (Vlong n)) + | ADadr _ id ofs => Some (Val.addl vl (symbol_low Ge.(_lk) id ofs)) + | _ => None + end in + call_ll_loadv chunk (interp_load ld) m v. + +Definition exec_load2 (ld: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) (vl1 vl2: val) := + let v := + match a with + | ADreg _ _ => Some (Val.addl vl1 vl2) + | ADlsl _ _ n => Some (Val.addl vl1 (Val.shll vl2 (Vint n))) + | ADsxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofint vl2) (Vint n))) + | ADuxt _ _ n => Some (Val.addl vl1 (Val.shll (Val.longofintu vl2) (Vint n))) + | _ => None + end in + call_ll_loadv chunk (interp_load ld) m v. + +Definition exec_loadU (n: load_rd_a) (m: mem) (chunk: memory_chunk) (a: addressing) := + call_ll_loadv chunk (interp_load n) m None. + +Definition load_eval (o: load_op) (l: list value) := + match o, l with + | Oload1 ld chunk a, [Val vs; Memstate m] => exec_load1 ld m chunk a vs + | Oload2 ld chunk a, [Val vs1; Val vs2; Memstate m] => exec_load2 ld m chunk a vs1 vs2 + | OloadU st chunk a, [Memstate m] => exec_loadU st m chunk a + | _, _ => None + end. + +Definition eval_allocf (o: allocf_op) (l: list value) := + match o, l with + | OAllocf_Mem sz linkofs, [Val spv; Memstate m] => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + call_ll_storev Mint64 m1 (Some (Val.offset_ptr sp linkofs)) spv + | OAllocf_SP sz linkofs, [Val spv; Memstate m] => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + match call_ll_storev Mint64 m1 (Some (Val.offset_ptr sp linkofs)) spv with + | None => None + | Some ms => Some (Val sp) + end + | _, _ => 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 + end. + +Definition vz_eq (vz1 vz2: val) : ?? bool := + RET (match vz1 with + | Vint i1 => match vz2 with + | Vint i2 => Int.eq i1 i2 + | _ => false + end + | Vlong l1 => match vz2 with + | Vlong l2 => Int64.eq l1 l2 + | _ => false + end + | _ => false + end). + +Lemma vz_eq_correct vz1 vz2: + WHEN vz_eq vz1 vz2 ~> b THEN b = true -> vz1 = vz2. +Proof. + wlp_simplify. + destruct vz1; destruct vz2; trivial; try discriminate. + - eapply f_equal; apply Int.same_if_eq; auto. + - eapply f_equal. apply Int64.same_if_eq; auto. +Qed. +Hint Resolve vz_eq_correct: wlp. + +Definition is_eq (is1 is2: isize) : ?? bool := + RET (match is1 with + | W => match is2 with + | W => true + | _ => false + end + | X => match is2 with + | X => true + | _ => false + end + end). + +Lemma is_eq_correct is1 is2: + WHEN is_eq is1 is2 ~> b THEN b = true -> is1 = is2. +Proof. + wlp_simplify; destruct is1; destruct is2; trivial; try discriminate. +Qed. +Hint Resolve is_eq_correct: wlp. + +Definition arith_op_eq (o1 o2: arith_op): ?? bool := + match o1 with + | OArithP n1 => + match o2 with OArithP n2 => phys_eq n1 n2 | _ => RET false end + | OArithPP n1 => + match o2 with OArithPP n2 => phys_eq n1 n2 | _ => RET false end + | OArithPPP n1 => + match o2 with OArithPPP n2 => phys_eq n1 n2 | _ => RET false end + | OArithRR0R n1 => + match o2 with OArithRR0R n2 => phys_eq n1 n2 | _ => RET false end + | OArithRR0R_XZR n1 vz1 => + match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end + | OArithRR0 n1 => + match o2 with OArithRR0 n2 => phys_eq n1 n2 | _ => RET false end + | OArithRR0_XZR n1 vz1 => + match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end + | OArithARRRR0 n1 => + match o2 with OArithARRRR0 n2 => phys_eq n1 n2 | _ => RET false end + | OArithARRRR0_XZR n1 vz1 => + match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end + | OArithComparisonPP_CN n1 => + match o2 with OArithComparisonPP_CN n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonPP_CZ n1 => + match o2 with OArithComparisonPP_CZ n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonPP_CC n1 => + match o2 with OArithComparisonPP_CC n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonPP_CV n1 => + match o2 with OArithComparisonPP_CV n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonR0R_CN n1 is1 => + match o2 with OArithComparisonR0R_CN n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end + | OArithComparisonR0R_CZ n1 is1 => + match o2 with OArithComparisonR0R_CZ n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end + | OArithComparisonR0R_CC n1 is1 => + match o2 with OArithComparisonR0R_CC n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end + | OArithComparisonR0R_CV n1 is1 => + match o2 with OArithComparisonR0R_CV n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end + | OArithComparisonR0R_CN_XZR n1 is1 vz1 => + match o2 with OArithComparisonR0R_CN_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end + | OArithComparisonR0R_CZ_XZR n1 is1 vz1 => + match o2 with OArithComparisonR0R_CZ_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end + | OArithComparisonR0R_CC_XZR n1 is1 vz1 => + match o2 with OArithComparisonR0R_CC_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end + | OArithComparisonR0R_CV_XZR n1 is1 vz1 => + match o2 with OArithComparisonR0R_CV_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end + | OArithComparisonP_CN n1 => + match o2 with OArithComparisonP_CN n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonP_CZ n1 => + match o2 with OArithComparisonP_CZ n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonP_CC n1 => + match o2 with OArithComparisonP_CC n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonP_CV n1 => + match o2 with OArithComparisonP_CV n2 => phys_eq n1 n2 | _ => RET false end + | Ocset c1 => + match o2 with Ocset c2 => struct_eq c1 c2 | _ => RET false end + | Ofmovi fsz1 => + match o2 with Ofmovi fsz2 => phys_eq fsz1 fsz2 | _ => RET false end + | Ofmovi_XZR fsz1 => + match o2 with Ofmovi_XZR fsz2 => phys_eq fsz1 fsz2 | _ => RET false end + | Ocsel c1 => + match o2 with Ocsel c2 => struct_eq c1 c2 | _ => RET false end + | Ofnmul fsz1 => + match o2 with Ofnmul fsz2 => phys_eq fsz1 fsz2 | _ => RET false end + end. + +Ltac my_wlp_simplify := wlp_xsimplify ltac:(intros; subst; simpl in * |- *; congruence || intuition eauto with wlp). + +Lemma arith_op_eq_correct o1 o2: + WHEN arith_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. +Proof. + destruct o1, o2; my_wlp_simplify; try congruence; + try (destruct vz; destruct vz0); try (destruct is; destruct is0); + repeat apply f_equal; try congruence; + try apply Int.same_if_eq; try apply Int64.same_if_eq; try auto. +Qed. +Hint Resolve arith_op_eq_correct: wlp. +Opaque arith_op_eq_correct. + +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 + | 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 + | 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 + 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; + try apply Int.same_if_eq in H; try congruence. +Qed. +Hint Resolve control_op_eq_correct: wlp. +Opaque control_op_eq_correct. + +Definition store_op_eq (s1 s2: store_op): ?? bool := + match s1 with + | Ostore1 st1 chk1 a1 => + match s2 with Ostore1 st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end + | Ostore2 st1 chk1 a1 => + match s2 with Ostore2 st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end + | OstoreU st1 chk1 a1 => + match s2 with OstoreU st2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq st1 st2) (struct_eq a1 a2)) | _ => RET false end + end. + +Lemma store_op_eq_correct s1 s2: + WHEN store_op_eq s1 s2 ~> b THEN b = true -> s1 = s2. +Proof. + destruct s1, s2; wlp_simplify; try congruence. + all: rewrite H1 in H0; rewrite H0, H; reflexivity. +Qed. +Hint Resolve store_op_eq_correct: wlp. +Opaque store_op_eq_correct. + +Definition load_op_eq (l1 l2: load_op): ?? bool := + match l1 with + | Oload1 ld1 chk1 a1 => + match l2 with Oload1 ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end + | Oload2 ld1 chk1 a1 => + match l2 with Oload2 ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end + | OloadU ld1 chk1 a1 => + match l2 with OloadU ld2 chk2 a2 => iandb (struct_eq chk1 chk2) (iandb (struct_eq ld1 ld2) (struct_eq a1 a2)) | _ => RET false end + end. + +Lemma load_op_eq_correct l1 l2: + WHEN load_op_eq l1 l2 ~> b THEN b = true -> l1 = l2. +Proof. + destruct l1, l2; wlp_simplify; try congruence. + all: rewrite H1 in H0; rewrite H, H0; reflexivity. +Qed. +Hint Resolve load_op_eq_correct: wlp. +Opaque load_op_eq_correct. + +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 + | Arith i1 => + match o2 with Arith i2 => arith_op_eq i1 i2 | _ => RET false end + | Control i1 => + match o2 with Control i2 => control_op_eq i1 i2 | _ => RET false end + | Load i1 => + 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 + end. + +Lemma op_eq_correct o1 o2: + WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. +Proof. + destruct o1, o2; wlp_simplify; congruence. +Qed. + +End IMPPARAM. + +End P. + +Module L <: ISeqLanguage with Module LP:=P. + +Module LP:=P. + +Include MkSeqLanguage P. + +End L. + +Module IST := ImpSimu L ImpPosDict. + +Import L. +Import P. + +(** Compilation from [Asmblock] to [L] *) + +Local Open Scope positive_scope. + +Definition pmem : R.t := 1. + +Definition ireg_to_pos (ir: ireg) : R.t := + match ir with + | X0 => 8 | X1 => 9 | X2 => 10 | X3 => 11 | X4 => 12 | X5 => 13 | X6 => 14 | X7 => 15 + | X8 => 16 | X9 => 17 | X10 => 18 | X11 => 19 | X12 => 20 | X13 => 21 | X14 => 22 | X15 => 23 + | X16 => 24 | X17 => 25 | X18 => 26 | X19 => 27 | X20 => 28 | X21 => 29 | X22 => 30 | X23 => 31 + | X24 => 32 | X25 => 33 | X26 => 34 | X27 => 35 | X28 => 36 | X29 => 37 | X30 => 38 + end +. + +Definition freg_to_pos (fr: freg) : R.t := + match fr with + | D0 => 39 | D1 => 40 | D2 => 41 | D3 => 42 | D4 => 43 | D5 => 44 | D6 => 45 | D7 => 46 + | D8 => 47 | D9 => 48 | D10 => 49 | D11 => 50 | D12 => 51 | D13 => 52 | D14 => 53 | D15 => 54 + | D16 => 55 | D17 => 56 | D18 => 57 | D19 => 58 | D20 => 59 | D21 => 60 | D22 => 61 | D23 => 62 + | D24 => 63 | D25 => 64 | D26 => 65 | D27 => 66 | D28 => 67 | D29 => 68 | D30 => 69 | D31 => 70 + end +. + +Lemma ireg_to_pos_discr: forall r r', r <> r' -> ireg_to_pos r <> ireg_to_pos r'. +Proof. + destruct r; destruct r'; try contradiction; discriminate. +Qed. + +Lemma freg_to_pos_discr: forall r r', r <> r' -> freg_to_pos r <> freg_to_pos r'. +Proof. + destruct r; destruct r'; try contradiction; discriminate. +Qed. + +Definition ppos (r: preg) : R.t := + match r with + | CR c => match c with + | CN => 2 + | CZ => 3 + | CC => 4 + | CV => 5 + end + | PC => 6 + | DR d => match d with + | IR i => match i with + | XSP => 7 + | RR1 ir => ireg_to_pos ir + end + | FR fr => freg_to_pos fr + end + end +. + +Notation "# r" := (ppos r) (at level 100, right associativity). + +Lemma not_eq_add: + forall k n n', n <> n' -> k + n <> k + n'. +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. + split; unfold not; try intros; try apply ppos_equal in H0; try discriminate; try contradiction. +Qed. + +Lemma ppos_pmem_discr: forall r, pmem <> ppos r. +Proof. + intros. destruct r as [dr|cr|]. + - destruct dr as [ir|fr]; try destruct ir as [irr|]; try destruct irr; try destruct fr; + unfold ppos; unfold pmem; discriminate. + - unfold ppos; unfold pmem; destruct cr; discriminate. + - unfold ppos; unfold pmem; discriminate. +Qed. + +(** Inversion functions, used for debug traces *) + +Definition pos_to_ireg (p: R.t) : option ireg := + match p with + | 8 => Some (X0) | 9 => Some (X1) | 10 => Some (X2) | 11 => Some (X3) | 12 => Some (X4) | 13 => Some (X5) | 14 => Some (X6) | 15 => Some (X7) + | 16 => Some (X8) | 17 => Some (X9) | 18 => Some (X10) | 19 => Some (X11) | 20 => Some (X12) | 21 => Some (X13) | 22 => Some (X14) | 23 => Some (X15) + | 24 => Some (X16) | 25 => Some (X17) | 26 => Some (X18) | 27 => Some (X19) | 28 => Some (X20) | 29 => Some (X21) | 30 => Some (X22) | 31 => Some (X23) + | 32 => Some (X24) | 33 => Some (X25) | 34 => Some (X26) | 35 => Some (X27) | 36 => Some (X28) | 37 => Some (X29) | 38 => Some (X30) | _ => None + end. + +Definition pos_to_freg (p: R.t) : option freg := + match p with + | 39 => Some(D0) | 40 => Some(D1) | 41 => Some(D2) | 42 => Some(D3) | 43 => Some(D4) | 44 => Some(D5) | 45 => Some(D6) | 46 => Some(D7) + | 47 => Some(D8) | 48 => Some(D9) | 49 => Some(D10) | 50 => Some(D11) | 51 => Some(D12) | 52 => Some(D13) | 53 => Some(D14) | 54 => Some(D15) + | 55 => Some(D16) | 56 => Some(D17) | 57 => Some(D18) | 58 => Some(D19) | 59 => Some(D20) | 60 => Some(D21) | 61 => Some(D22) | 62 => Some(D23) + | 63 => Some(D24) | 64 => Some(D25) | 65 => Some(D26) | 66 => Some(D27) | 67 => Some(D28) | 68 => Some(D29) | 69 => Some(D30) | 70 => Some(D31) | _ => None + end. + +Definition inv_ppos (p: R.t) : option preg := + match p with + | 1 => None + | 2 => Some (CR CN) + | 3 => Some (CR CZ) + | 4 => Some (CR CC) + | 5 => Some (CR CV) + | 6 => Some (PC) + | 7 => Some (DR (IR XSP)) + | n => match pos_to_ireg n with + | None => match pos_to_freg n with + | None => None + | Some fr => Some (DR (FR fr)) + end + | Some ir => Some (DR (IR ir)) + end + end. + +Notation "a @ b" := (Econs a b) (at level 102, right associativity). + +(** Translations of instructions *) + +Definition get_testcond_rlocs (c: testcond) := + match c with + | TCeq => (PReg(#CZ) @ Enil) + | TCne => (PReg(#CZ) @ Enil) + | TChs => (PReg(#CC) @ Enil) + | TClo => (PReg(#CC) @ Enil) + | TCmi => (PReg(#CN) @ Enil) + | TCpl => (PReg(#CN) @ Enil) + | TChi => (PReg(#CZ) @ PReg(#CC) @ Enil) + | TCls => (PReg(#CZ) @ PReg(#CC) @ Enil) + | TCge => (PReg(#CN) @ PReg(#CV) @ Enil) + | TClt => (PReg(#CN) @ PReg(#CV) @ Enil) + | TCgt => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil) + | 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)] + | Pbuiltin ef args res => [] + 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 => + if destroy_X16 n then [(#rd, Op(Arith (OArithP n)) Enil); (#X16, Op (Constant Vundef) Enil)] + else [(#rd, Op(Arith (OArithP n)) Enil)] + | PArithPP n rd r1 => [(#rd, Op(Arith (OArithPP n)) (PReg(#r1) @ Enil))] + | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))] + | PArithRR0R n rd r1 r2 => + let lr := match r1 with + | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil) + | XZR => let vz := if arith_rr0r_isize n then Vint Int.zero else Vlong Int64.zero in + Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil) + end in + [(#rd, lr)] + | PArithRR0 n rd r1 => + let lr := match r1 with + | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil) + | XZR => let vz := if arith_rr0_isize n then Vint Int.zero else Vlong Int64.zero in + Op(Arith (OArithRR0_XZR n vz)) (Enil) + end in + [(#rd, lr)] + | PArithARRRR0 n rd r1 r2 r3 => + let lr := match r3 with + | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil) + | XZR => let vz := if arith_arrrr0_isize n then Vint Int.zero else Vlong Int64.zero in + Op(Arith (OArithARRRR0_XZR n vz)) (PReg(#r1) @ PReg(#r2) @ Enil) + end in + [(#rd, lr)] + | PArithComparisonPP n r1 r2 => + [(#CN, Op(Arith (OArithComparisonPP_CN n)) (PReg(#r1) @ PReg(#r2) @ Enil)); + (#CZ, Op(Arith (OArithComparisonPP_CZ n)) (PReg(#r1) @ PReg(#r2) @ Enil)); + (#CC, Op(Arith (OArithComparisonPP_CC n)) (PReg(#r1) @ PReg(#r2) @ Enil)); + (#CV, Op(Arith (OArithComparisonPP_CV n)) (PReg(#r1) @ PReg(#r2) @ Enil))] + | PArithComparisonR0R n r1 r2 => + let is := arith_comparison_r0r_isize n in + match r1 with + | RR0 r1' => [(#CN, Op(Arith (OArithComparisonR0R_CN n is)) (PReg(#r1') @ PReg(#r2) @ Enil)); + (#CZ, Op(Arith (OArithComparisonR0R_CZ n is)) (PReg(#r1') @ PReg(#r2) @ Enil)); + (#CC, Op(Arith (OArithComparisonR0R_CC n is)) (PReg(#r1') @ PReg(#r2) @ Enil)); + (#CV, Op(Arith (OArithComparisonR0R_CV n is)) (PReg(#r1') @ PReg(#r2) @ Enil))] + | XZR => let vz := if is then Vint Int.zero else Vlong Int64.zero in + [(#CN, Op(Arith (OArithComparisonR0R_CN_XZR n is vz)) (PReg(#r2) @ Enil)); + (#CZ, Op(Arith (OArithComparisonR0R_CZ_XZR n is vz)) (PReg(#r2) @ Enil)); + (#CC, Op(Arith (OArithComparisonR0R_CC_XZR n is vz)) (PReg(#r2) @ Enil)); + (#CV, Op(Arith (OArithComparisonR0R_CV_XZR n is vz)) (PReg(#r2) @ Enil))] + end + | PArithComparisonP n r1 => + [(#CN, Op(Arith (OArithComparisonP_CN n)) (PReg(#r1) @ Enil)); + (#CZ, Op(Arith (OArithComparisonP_CZ n)) (PReg(#r1) @ Enil)); + (#CC, Op(Arith (OArithComparisonP_CC n)) (PReg(#r1) @ Enil)); + (#CV, Op(Arith (OArithComparisonP_CV n)) (PReg(#r1) @ Enil))] + | Pcset rd c => + let lr := get_testcond_rlocs c in + [(#rd, Op(Arith (Ocset c)) lr)] + | Pfmovi fsz rd r1 => + let lr := match r1 with + | RR0 r1' => Op(Arith (Ofmovi fsz)) (PReg(#r1') @ Enil) + | XZR => Op(Arith (Ofmovi_XZR fsz)) Enil + end in + [(#rd, lr)] + | Pcsel rd r1 r2 c => + let lr := get_testcond_rlocs c in + [(#rd, Op(Arith (Ocsel c)) (PReg(#r1) @ PReg (#r2) @ lr))] + | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))] + end. + +Definition eval_addressing_rlocs_st (st: store_rs_a) (chunk: memory_chunk) (rs: dreg) (a: addressing) := + match a with + | ADimm base n => Op (Store (Ostore1 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil) + | ADreg base r => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADlsl base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADsxt base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADuxt base r n => Op (Store (Ostore2 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADadr base id ofs => Op (Store (Ostore1 st chunk a)) (PReg (#rs) @ PReg (#base) @ PReg (pmem) @ Enil) + | ADpostincr base n => Op (Store (OstoreU st chunk a)) (PReg (#rs) @ PReg (pmem) @ Enil) (* not modeled yet *) + end. + +Definition eval_addressing_rlocs_ld (ld: load_rd_a) (chunk: memory_chunk) (a: addressing) := + match a with + | ADimm base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil) + | ADreg base r => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADlsl base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADsxt base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADuxt base r n => Op (Load (Oload2 ld chunk a)) (PReg (#base) @ PReg(#r) @ PReg (pmem) @ Enil) + | ADadr base id ofs => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil) + | ADpostincr base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil) + end. + +Definition trans_ldp_chunk (chunk: memory_chunk) (r: dreg): load_rd_a := + match chunk with + | Mint32 => Pldrw + | Mint64 => Pldrx + | Mfloat32 => Pldrs + | Mfloat64 => Pldrd + | Many32 => Pldrw_a + | _ => (* This case should always correspond to Many64 *) + match r with + | IR _ => Pldrx_a + | FR _ => Pldrd_a + end + end. + +Definition trans_stp_chunk (chunk: memory_chunk) (r: dreg): store_rs_a := + match chunk with + | Mint32 => Pstrw + | Mint64 => Pstrx + | Mfloat32 => Pstrs + | Mfloat64 => Pstrd + | Many32 => Pstrw_a + | _ => (* This case should always correspond to Many64 *) + match r with + | IR _ => Pstrx_a + | FR _ => Pstrd_a + end + end. + +Definition trans_load (ldi: ld_instruction) := + match ldi with + | PLd_rd_a ld r a => + let lr := eval_addressing_rlocs_ld ld (chunk_load ld) a in [(#r, lr)] + | Pldp ld r1 r2 chk1 chk2 a => + let ldi1 := trans_ldp_chunk chk1 r1 in + let ldi2 := trans_ldp_chunk chk2 r1 in + let lr := eval_addressing_rlocs_ld ldi1 chk1 a in + let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4%Z | _ => 8%Z end in + match a with + | ADimm base n => + let a' := (get_offset_addr a ofs) in + [(#r1, lr); + (#r2, Op (Load (Oload1 ldi2 chk2 a')) + (Old(PReg (#base)) @ PReg (pmem) @ Enil))] + | _ => [(#PC, (Op (OError)) Enil)] + end + end. + +Definition trans_store (sti: st_instruction) := + match sti with + | PSt_rs_a st r a => + let lr := eval_addressing_rlocs_st st (chunk_store st) r a in [(pmem, lr)] + | Pstp st r1 r2 chk1 chk2 a => + let sti1 := trans_stp_chunk chk1 r1 in + let sti2 := trans_stp_chunk chk2 r1 in + let lr := eval_addressing_rlocs_st sti1 chk1 r1 a in + let ofs := match chk1 with | Mint32 | Mfloat32| Many32 => 4%Z | _ => 8%Z end in + match a with + | ADimm base n => + let a' := (get_offset_addr a ofs) in + [(pmem, lr); + (pmem, Op (Store (Ostore1 sti2 chk2 a')) + (PReg (#r2) @ Old(PReg (#base)) @ PReg (pmem) @ Enil))] + | _ => [(#PC, (Op (OError)) Enil)] + end + end. + +Definition trans_basic (b: basic) : inst := + match b with + | PArith ai => trans_arith ai + | PLoad ld => trans_load ld + | PStore st => trans_store st + | 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))] + | Pnop => [] + end. + +Fixpoint trans_body (b: list basic) : list L.inst := + match b with + | nil => nil + | b :: lb => (trans_basic b) :: (trans_body lb) + end. + +Definition trans_pcincr (sz: Z) (k: L.inst) := (#PC, Op (Control (OIncremPC sz)) (PReg(#PC) @ Enil)) :: k. + +Definition trans_block (b: Asmblock.bblock) : L.bblock := + trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil). + +(*Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb.*) +(*Proof.*) + (*intros. destruct bb as [hd bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.*) +(*Qed.*) + +(*Theorem trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb.*) +(*Proof.*) + (*intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity.*) +(*Qed.*) + +(** Lemmas on the translation *) + +Definition state := L.mem. +Definition exec := L.run. + +Definition match_states (s: Asm.state) (s': state) := + let (rs, m) := s in + s' pmem = Memstate m + /\ forall r, s' (#r) = Val (rs r). + +Definition match_outcome (o:outcome) (s: option state) := + match o with + | Some n => exists s', s=Some s' /\ match_states n s' + | None => s=None + end. + +Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity). + +Definition trans_state (s: Asm.state) : state := + let (rs, m) := s in + fun x => if (Pos.eq_dec x pmem) then Memstate m + else match (inv_ppos x) with + | Some r => Val (rs r) + | None => Val Vundef + end. + +Lemma not_eq_IR: + forall r r', r <> r' -> IR r <> IR r'. +Proof. + intros. congruence. +Qed. + +Lemma ireg_pos_ppos: forall r, + ireg_to_pos r = # r. +Proof. + intros. simpl. reflexivity. +Qed. + +Lemma freg_pos_ppos: forall r, + freg_to_pos r = # r. +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. + intros; destruct r; discriminate. +Qed. + +Lemma ireg_not_CN: forall r, + 2 <> ireg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma ireg_not_CZ: forall r, + 3 <> ireg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma ireg_not_CC: forall r, + 4 <> ireg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma ireg_not_CV: forall r, + 5 <> ireg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma freg_not_pmem: forall r, + freg_to_pos r <> pmem. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma freg_not_CN: forall r, + 2 <> freg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma freg_not_CZ: forall r, + 3 <> freg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma freg_not_CC: forall r, + 4 <> freg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma freg_not_CV: forall r, + 5 <> freg_to_pos r. +Proof. + intros; destruct r; discriminate. +Qed. + +Lemma dreg_not_pmem: forall (r: dreg), + (# r) <> pmem. +Proof. + intros; destruct r as [i|f]. + - destruct i. apply ireg_not_pmem. discriminate. + - apply freg_not_pmem. +Qed. + +Ltac DPRM pr := + destruct pr as [drDPRF|crDPRF|]; + [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |] + | destruct crDPRF|]. + +Ltac DPRF pr := + destruct pr as [drDPRF|crDPRF|]; + [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|] + | destruct frDPRF] + | destruct crDPRF|]. + +Lemma preg_not_pmem: forall r, + pmem <> # r. +Proof. + intros. DPRF r; simpl; discriminate. +Qed. + +Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl. + +Lemma dreg_not_CN: forall (r: dreg), + 2 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CN | discriminate | apply freg_not_CN]. +Qed. + +Lemma dreg_not_CZ: forall (r: dreg), + 3 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CZ | discriminate | apply freg_not_CZ]. +Qed. + +Lemma dreg_not_CC: forall (r: dreg), + 4 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CC | discriminate | apply freg_not_CC]. +Qed. + +Lemma dreg_not_CV: forall (r: dreg), + 5 <> (#r). +Proof. + intros; DIRN1 r; [ apply ireg_not_CV | discriminate | apply freg_not_CV]. +Qed. + +Lemma sr_update_both: forall sr rsr r1 rr v + (HEQV: forall r : preg, sr (# r) = Val (rsr r)), + (sr <[ (#r1) <- Val (v) ]>) (#rr) = + Val (rsr # r1 <- v rr). +Proof. + intros. unfold assign. + destruct (R.eq_dec (#r1) (#rr)); subst. + - apply ppos_equal in e; subst; rewrite Pregmap.gss; reflexivity. + - rewrite Pregmap.gso; eapply ppos_discr in n; auto. +Qed. + +Lemma sr_gss: forall sr pos v, + (sr <[ pos <- v ]>) pos = v. +Proof. + intros. unfold assign. + 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 sr_val_rwrt := + repeat match goal with + | [H: forall r: preg, ?sr (# r) = Val (?rsr r) |- _ ] + => rewrite H + end. + +Ltac sr_memstate_rwrt := + repeat match goal with + | [H: ?sr pmem = Memstate ?mr |- _ ] + => rewrite <- H + end. + +Ltac replace_ppos := + try erewrite !ireg_pos_ppos; + try erewrite !freg_pos_ppos; + try replace (7) with (#XSP) by eauto; + try replace (24) with (#X16) by auto. + +Ltac DDRM dr := + destruct dr as [irsDDRF|frDDRF]; + [destruct irsDDRF + | idtac ]. + +(* Ltac DDRF dr := + destruct dr as [irsDDRF|frDDRF]; + [destruct irsDDRF as [irsDDRF|]; [destruct irsDDRF|] + | destruct frDDRF]. *) + +(* Ltac DPRI pr := + destruct pr as [drDPRI|crDPRI|]; + [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|] + | idtac + | idtac ]. *) + +Ltac discriminate_ppos := + try apply ireg_not_pmem; + try apply ireg_not_pc; + try apply freg_not_pmem; + try apply dreg_not_pmem; + try apply ireg_not_CN; + try apply ireg_not_CZ; + try apply ireg_not_CC; + try apply ireg_not_CV; + try apply freg_not_CN; + try apply freg_not_CZ; + try apply freg_not_CC; + try apply freg_not_CV; + try apply dreg_not_CN; + try apply dreg_not_CZ; + try apply dreg_not_CC; + try apply dreg_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 Simpl_exists sr := + replace_ppos; + replace_regs_pos sr; + try sr_val_rwrt; + try (eexists; split; [| split]); eauto; + try (sr_memstate_rwrt; rewrite assign_diff; + try reflexivity; + discriminate_ppos + ). + +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_update_both; eauto. + +Ltac Simpl sr := Simpl_exists sr; try (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. *) + +(* Ltac destruct_reg_neq r1 r2 := + destruct (PregEq.eq r1 r2); subst; + [ rewrite sr_gss; rewrite Pregmap.gss; reflexivity | + rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto]. *) + +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. + +Ltac replace_regs_cond_force := + try replace (5) with (#CV) in * by auto; + try replace (4) with (#CC) in * by auto; + try replace (3) with (#CZ) in * by auto; + try replace (2) with (#CN) in * by auto. + +Ltac validate_crbit_flags rr v1 v2 := + destruct (R.eq_dec 5 (#rr)) as [e0|n0]; + destruct (R.eq_dec 4 (#rr)) as [e1|n1]; + destruct (R.eq_dec 3 (#rr)) as [e2|n2]; + destruct (R.eq_dec 2 (#rr)) as [e3|n3]; + replace_regs_cond_force; + try apply ppos_equal in e0; + try apply ppos_equal in e1; + try apply ppos_equal in e2; + try apply ppos_equal in e3; + try apply ppos_discr in n0; + try apply ppos_discr in n1; + try apply ppos_discr in n2; + try apply ppos_discr in n3; + subst. + +Ltac Simpl_flags := + try (rewrite Pregmap.gss; reflexivity); + try (rewrite Pregmap.gso, Pregmap.gss; [reflexivity|]; try auto); + try (rewrite Pregmap.gso; try auto); + try (rewrite !Pregmap.gso; try auto). + +Lemma compare_single_res: forall sr mr rsr rr v1 v2 + (HMEM: sr pmem = Memstate mr) + (HEQV: forall r : preg, sr (# r) = Val (rsr r)), + ((((sr <[ 2 <- Val (_CN (v_compare_single v1 v2)) ]>) <[ 3 <- + Val (_CZ (v_compare_single v1 v2)) ]>) <[ 4 <- + Val (_CC (v_compare_single v1 v2)) ]>) <[ 5 <- + Val (_CV (v_compare_single v1 v2)) ]>) (# rr) = +Val + ((compare_single rsr v1 v2) rr). +Proof. + intros. unfold v_compare_single, compare_single, assign. + validate_crbit_flags rr v1 v2. + all: destruct v1; destruct v2; Simpl_flags. +Qed. + +Lemma compare_float_res: forall sr mr rsr rr v1 v2 + (HMEM: sr pmem = Memstate mr) + (HEQV: forall r : preg, sr (# r) = Val (rsr r)), + ((((sr <[ 2 <- Val (_CN (v_compare_float v1 v2)) ]>) <[ 3 <- + Val (_CZ (v_compare_float v1 v2)) ]>) <[ 4 <- + Val (_CC (v_compare_float v1 v2)) ]>) <[ 5 <- + Val (_CV (v_compare_float v1 v2)) ]>) (# rr) = +Val + ((compare_float rsr v1 v2) rr). +Proof. + intros. unfold v_compare_float, compare_float, assign. + validate_crbit_flags rr v1 v2. + all: destruct v1; destruct v2; Simpl_flags. +Qed. + +Lemma compare_long_res: forall sr mr rsr rr v1 v2 + (HMEM: sr pmem = Memstate mr) + (HEQV: forall r : preg, sr (# r) = Val (rsr r)), + ((((sr <[ 2 <- Val (_CN (v_compare_long v1 v2)) ]>) <[ 3 <- + Val (_CZ (v_compare_long v1 v2)) ]>) <[ 4 <- + Val (_CC (v_compare_long v1 v2)) ]>) <[ 5 <- + Val (_CV (v_compare_long v1 v2)) ]>) (# rr) = +Val + ((compare_long rsr v1 v2) rr). +Proof. + intros. unfold v_compare_long, compare_long, assign. + validate_crbit_flags rr v1 v2. + all: Simpl_flags. +Qed. + +Lemma compare_int_res: forall sr mr rsr rr v1 v2 + (HMEM: sr pmem = Memstate mr) + (HEQV: forall r : preg, sr (# r) = Val (rsr r)), + ((((sr <[ 2 <- Val (_CN (v_compare_int v1 v2)) ]>) <[ 3 <- + Val (_CZ (v_compare_int v1 v2)) ]>) <[ 4 <- + Val (_CC (v_compare_int v1 v2)) ]>) <[ 5 <- + Val (_CV (v_compare_int v1 v2)) ]>) (# rr) = +Val + ((compare_int rsr v1 v2) rr). +Proof. + intros. unfold v_compare_int, compare_int, assign. + validate_crbit_flags rr v1 v2. + all: Simpl_flags. +Qed. + +Section SECT_SEQ. + +Variable Ge: genv. + +Lemma trans_arith_correct rsr mr sr rsw' old i: + match_states (State rsr mr) sr -> + exec_arith_instr Ge.(_lk) i rsr = rsw' -> + exists sw, + inst_run Ge (trans_arith i) sr old = Some sw + /\ match_states (State rsw' mr) sw. +Proof. + induction i. + all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr. + - (* PArithP *) + destruct i. + 1,2,3: DIRN1 rd; Simpl sr. + (* Special case for Pmovimms/Pmovimmd *) + all: simpl; + try(destruct (negb (is_immediate_float32 _))); + try(destruct (negb (is_immediate_float64 _))); + DIRN1 rd; Simpl sr; + try (rewrite assign_diff; discriminate_ppos; reflexivity); + try (intros rr'; Simpl_update). + - (* PArithPP *) + DIRN1 rs; DIRN1 rd; Simpl sr. + - (* PArithPPP *) + DIRN1 r1; DIRN1 r2; DIRN1 rd; Simpl sr. + - (* PArithRR0R *) + simpl. destruct r1. + + (* OArithRR0R *) simpl; Simpl sr. + + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); Simpl sr. + - (* PArithRR0 *) + simpl. destruct r1. + + (* OArithRR0 *) simpl; Simpl sr. + + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); Simpl sr. + - (* PArithARRRR0 *) + simpl. destruct r3. + + (* OArithARRRR0 *) simpl; Simpl sr. + + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); Simpl sr. + - (* PArithComparisonPP *) + simpl; destruct i; + unfold arith_eval_comparison_pp, arith_prepare_comparison_pp; simpl; + fold (ppos r2); fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr; + Simpl sr; + try destruct sz; + try (eapply compare_single_res; eauto); + try (eapply compare_long_res; eauto); + try (eapply compare_float_res; eauto). + - (* PArithComparisonR0R *) + simpl; destruct r1; simpl; destruct i; + repeat (replace_regs_cond_force; try fold (ppos r); try fold(ppos r2); + try rewrite !assign_diff; discriminate_ppos; try rewrite !H0); + Simpl sr; unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize; + destruct arith_prepare_comparison_r0r; destruct is; + try (eapply compare_long_res; eauto); + try (eapply compare_int_res; eauto). + - (* PArithComparisonP *) + simpl; destruct i; + unfold arith_eval_comparison_p, arith_prepare_comparison_p; simpl; + fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr; + Simpl sr; + try destruct sz; + try (eapply compare_int_res; eauto); + try (eapply compare_single_res; eauto); + try (eapply compare_long_res; eauto); + try (eapply compare_float_res; eauto). + - (* Pcset *) + simpl; unfold eval_testcond, get_testcond_rlocs, cflags_eval; + 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; Simpl sr. + - (* Pcsel *) + destruct c; simpl; DIRN1 rd; fold (ppos r2); fold (ppos r1); Simpl sr. + - (* Pfnmul *) + simpl; destruct fsz; Simpl sr. +Qed. + +Lemma sp_xsp: + SP = XSP. +Proof. + econstructor. +Qed. + +Lemma load_chunk_neutral: forall chk v r, + interp_load (trans_ldp_chunk chk r) v = v. +Proof. + intros; destruct chk; destruct r; simpl; reflexivity. +Qed. + +Theorem bisimu_basic rsr mr sr bi: + match_states (State rsr mr) sr -> + match_outcome (exec_basic Ge.(_lk) Ge.(_genv) bi rsr mr) (inst_run Ge (trans_basic bi) sr sr). +Proof. +(* a little tactic to automate reasoning on preg_eq *) +Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core. +Local Ltac preg_eq_discr r rd := + destruct (preg_eq r rd); try (subst r; rewrite assign_eq, Pregmap.gss; auto); + rewrite (assign_diff _ (#rd) (#r) _); auto; + rewrite Pregmap.gso; auto. + + intros MS; inversion MS as (H & H0). + destruct bi; simpl. + (* Loadsymbol / Cvtsw2x / Cvtuw2x / Cvtx2w *) + 6,7,8,9: Simpl sr. + - (* Arith *) + exploit trans_arith_correct; eauto. + - (* Load *) + destruct ld. + + unfold exec_load, exec_load_rd_a, eval_addressing_rlocs_ld, exp_eval; + destruct ld; destruct a; simpl; + try fold (ppos base); try fold (ppos r); + erewrite !H0, H; simpl; + unfold exec_load1, exec_load2, chunk_load; unfold call_ll_loadv; + try destruct (Mem.loadv _ _ _); simpl; auto. + all: try (fold (ppos rd); Simpl_exists sr; auto; intros rr; Simpl_update). + + + unfold exec_load, exec_load_double, eval_addressing_rlocs_ld, exp_eval; + destruct ld; destruct a; simpl; unfold control_eval; destruct Ge; auto; + try fold (ppos base); + try erewrite !H0, H; simpl; + unfold exec_load1, exec_load2; unfold call_ll_loadv; + destruct (Mem.loadv _ _ _); simpl; auto; + fold (ppos rd1); rewrite assign_diff; discriminate_ppos; rewrite H; + try destruct (Mem.loadv _ _ _); simpl; auto; Simpl_exists sr; + rewrite !load_chunk_neutral; + try (rewrite !assign_diff; discriminate_ppos; reflexivity); + try (destruct rd1 as [ir1|fr1]; try destruct ir1; destruct rd2 as [ir2|fr2]; try destruct ir2; + destruct base; discriminate_ppos); + repeat (try fold (ppos r); try fold (ppos r0); + try fold (ppos fr1); try fold (ppos fr2); intros; Simpl_update). + - (* Store *) + destruct st. + + unfold exec_store, exec_store_rs_a, eval_addressing_rlocs_st, exp_eval; + destruct st; destruct a; simpl; + try fold (ppos base); try fold (ppos rs); try fold (ppos r); + erewrite !H0, H; simpl; + unfold exec_store1, exec_store2, chunk_store; unfold call_ll_storev; + try destruct (Mem.storev _ _ _ _); simpl; auto. + all: eexists; split; [| split]; eauto; + intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos. + + unfold exec_store, exec_store_double, eval_addressing_rlocs_st, exp_eval; + destruct st; destruct a; simpl; unfold control_eval; destruct Ge; auto; + try fold (ppos base); try fold (ppos rs1); + erewrite !H0, H; simpl; + unfold exec_store1, exec_store2; unfold call_ll_storev; + try destruct (Mem.storev _ _ _ _); simpl; auto; + fold (ppos rs2); rewrite assign_diff; try congruence; try rewrite H0; simpl; + try destruct (Mem.storev _ _ _ _); simpl; auto. + all: eexists; split; [| split]; eauto; + repeat (try intros rr; rewrite assign_diff; try rewrite H0; auto; discriminate_ppos). + - (* 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. rewrite assign_diff; try apply preg_not_pmem; try rewrite sp_xsp. + replace 37 with (#X29) by auto; repeat (Simpl_update; intros). + + 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. + replace 24 with (#X16) by auto; rewrite sp_xsp; Simpl sr. + intros rr'; destruct (PregEq.eq XSP rr'). + * rewrite e; rewrite Pregmap.gss, sr_gss; auto. + * rewrite Pregmap.gso, !assign_diff; auto; apply ppos_discr in n; auto. + + rewrite <- sp_xsp; rewrite MLOAD; reflexivity. + - (* Nop *) + Simpl sr. +Qed. + +Theorem bisimu_body: + forall bdy rsr mr sr, + match_states (State rsr mr) sr -> + match_outcome (exec_body Ge.(_lk) Ge.(_genv) bdy rsr mr) (exec Ge (trans_body bdy) sr). +Proof. + induction bdy as [|i bdy]; simpl; eauto. + intros. + exploit (bisimu_basic rsr mr sr i); eauto. + destruct (exec_basic _ _ _ _ _); simpl. + - intros (s' & X1 & X2). + rewrite X1; simpl; eauto. eapply IHbdy; eauto; simpl. + unfold match_states in *. destruct s. unfold Asm._m. eauto. + - intros X; rewrite X; simpl; auto. +Qed. + +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 sr). +Proof. + intros MS. + simpl in *. inv MS. + destruct ex. + (* 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.mxcmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); + try (destruct (Val.mxcmplu_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; rewrite sr_update_overwrite; replace_pc; Simpl sr); + destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss; + destruct Val.offset_ptr; try reflexivity; rewrite sr_update_overwrite; + simpl; Simpl sr; (destruct (PregEq.eq rr PC); subst; + [ rewrite sr_gss, Pregmap.gss; reflexivity | + rewrite !assign_diff, !Pregmap.gso; replace_pc; auto; apply ppos_discr; 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; + try (rewrite sr_gss; unfold Stuck; reflexivity). + simpl. eexists; split; split. + * rewrite sr_update_overwrite. unfold pmem, assign in *. simpl. rewrite H; reflexivity. + * 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. + - (* 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; rewrite sr_update_overwrite; replace_pc; 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; rewrite sr_update_overwrite; replace_pc; 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; rewrite sr_update_overwrite; replace_pc; 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. Simpl sr. + replace_pc; try replace (38) with (#X30) by eauto; unfold incrPC. Simpl_update. + repeat (intros; 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; destruct (PregEq.eq PC rr). + + replace_pc; rewrite e; rewrite !Pregmap.gss, !sr_gss; + rewrite Pregmap.gso; fold (ppos r); try rewrite H0; auto. + rewrite <- e; destruct r; discriminate. + + replace_pc; rewrite Pregmap.gso, assign_diff; auto; apply ppos_discr in n; auto; + rewrite Pregmap.gss, sr_gss. destruct (PregEq.eq X30 rr); replace 38 with (#X30) by auto. + * rewrite e; rewrite Pregmap.gss, sr_gss; auto. + * replace_pc; rewrite !Pregmap.gso, !assign_diff; auto; apply ppos_discr in n0; auto; + apply ppos_discr; eauto. + - (* Obtbl *) + replace_pc; rewrite (H0 PC); + unfold control_eval; destruct Ge; simpl; unfold incrPC. + destruct (PregEq.eq X16 r1). + + fold (ppos r1); rewrite <- e; rewrite Pregmap.gss, sr_gss; reflexivity. + + rewrite !Pregmap.gso; auto; rewrite ppos_discr in n; + fold (ppos r1); replace 24 with (#X16) by auto; try rewrite !assign_diff; auto; + discriminate_ppos; rewrite H0; destruct (rsr r1) eqn:EQR; + try (try rewrite EQR; reflexivity). + 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 sr. + destruct (PregEq.eq X16 rr); [ subst; Simpl_update |]; + destruct (PregEq.eq PC rr); [ subst; Simpl_update |]. + rewrite !Pregmap.gso; auto; + apply ppos_discr in n0; apply ppos_discr in n1; + rewrite !assign_diff; auto. +Qed. + +Theorem bisimu_exit ex sz rsr mr sr: + match_states (State rsr mr) sr -> + (*is_builtin ex = false ->*) + match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit ex)) sr sr). +Proof. + intros MS; unfold estep. + destruct ex. + - destruct c. + + exploit (bisimu_control i sz rsr mr sr); eauto. + + simpl. inv MS. eexists; split; [| split]. + unfold control_eval; destruct Ge. + replace_pc; rewrite (H0 PC); eauto. + rewrite assign_diff; auto. + intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst. + * rewrite sr_gss, Pregmap.gss. reflexivity. + * rewrite assign_diff, Pregmap.gso; try rewrite H0; + auto; try rewrite ppos_discr in n; auto. + - simpl. inv MS. eexists; split; [| split]. + + unfold control_eval; destruct Ge. + replace_pc; rewrite (H0 PC); eauto. + + rewrite assign_diff; auto. + + intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst. + * rewrite sr_gss, Pregmap.gss. reflexivity. + * rewrite assign_diff, Pregmap.gso; try rewrite H0; auto; try rewrite ppos_discr in n; auto. +Qed. + +(* Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). *) + +Theorem bisimu rsr mr sr bb: + match_states (State rsr mr) sr -> + match_outcome (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) bb rsr mr) (exec Ge (trans_block bb) sr). +Proof. + intros MS. unfold bbstep, trans_block. + exploit (bisimu_body (body bb) rsr mr sr); eauto. + destruct (exec_body _ _ _ _ _); simpl. + - unfold match_states in *. intros (s' & X1 & X2). destruct s. + erewrite run_app_Some; eauto. + exploit (bisimu_exit (exit bb) (size bb) _rs _m s'); eauto. + destruct Ge; simpl. destruct MS as (Y1 & Y2). destruct X2 as (X2 & X3). + replace_pc. erewrite !X3; simpl. + destruct (inst_run _ _ _ _); simpl; auto. + - intros X; erewrite run_app_None; eauto. +Qed. + +Theorem trans_state_match: forall S, match_states S (trans_state S). +Proof. + intros. destruct S as (rs & m). simpl. + split. reflexivity. + intro. destruct r as [dr|cr|]; try destruct dr as [ir|fr]; try destruct cr; + try destruct ir as [irr|]; try destruct irr; try destruct fr; try reflexivity. +Qed. + +Lemma state_eq_decomp: + forall rs1 m1 rs2 m2, rs1 = rs2 -> m1 = m2 -> State rs1 m1 = State rs2 m2. +Proof. + intros. congruence. +Qed. + +Theorem state_equiv S1 S2 S': match_states S1 S' -> match_states S2 S' -> S1 = S2. +Proof. + unfold match_states; intros H0 H1. destruct S1 as (rs1 & m1). destruct S2 as (rs2 & m2). inv H0. inv H1. + apply state_eq_decomp. + - apply functional_extensionality. intros. assert (Val (rs1 x) = Val (rs2 x)) by congruence. congruence. + - congruence. +Qed. + +End SECT_SEQ. + +Section SECT_BBLOCK_EQUIV. + +Variable Ge: genv. + +Local Hint Resolve trans_state_match: core. + +Lemma bblock_simu_reduce_aux: + forall p1 p2, + L.bblock_simu Ge (trans_block p1) (trans_block p2) -> + Asmblockprops.bblock_simu_aux Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2. +Proof. + intros p1 p2 H0 rs m EBB. + generalize (H0 (trans_state (State rs m))); clear H0. + intro H0. + exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto. + exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto. + destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence). + intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0. + destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1. + destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1. + * unfold match_states in H1, MS'. destruct s, s0. + destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'. + replace (_rs0) with (_rs). + - replace (_m0) with (_m); auto. congruence. + - apply functional_extensionality. intros r. + generalize (H1 r). intros Hr. congruence. + * discriminate. +Qed. + +Lemma incrPC_set_res_commut res: forall d vres rs, + incrPC d (set_res (map_builtin_res DR res) vres rs) = + set_res (map_builtin_res DR res) vres (incrPC d rs). +Proof. + induction res; simpl; auto. + - intros; apply functional_extensionality. + unfold incrPC; intros x0. + destruct (PregEq.eq x0 PC). + + subst; rewrite! Pregmap.gss; auto. + + rewrite Pregmap.gso; auto. + destruct (PregEq.eq x x0). + * subst; rewrite! Pregmap.gss; auto. + * rewrite !Pregmap.gso; auto. + - intros; rewrite IHres2. f_equal. auto. +Qed. + +Lemma incrPC_undef_regs_commut l : forall d rs, + incrPC d (undef_regs l rs) = undef_regs l (incrPC d rs). +Proof. + induction l; simpl; auto. + intros. rewrite IHl. unfold incrPC. + destruct (PregEq.eq a PC). + - rewrite e. rewrite Pregmap.gss. + simpl. apply f_equal. unfold Pregmap.set. + apply functional_extensionality. intros x. + destruct (PregEq.eq x PC); auto. + - rewrite Pregmap.gso; auto. + apply f_equal. unfold Pregmap.set. + apply functional_extensionality. intros x. + destruct (PregEq.eq x PC). + + subst. destruct a; simpl; auto. congruence. + + auto. +Qed. + +Lemma bblock_simu_reduce: + forall p1 p2, + L.bblock_simu Ge (trans_block p1) (trans_block p2) -> + (has_builtin p1 = true \/ has_builtin p2 = true -> exit p1 = exit p2) -> + Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2. +Proof. + unfold bblock_simu. intros p1 p2 H0 BLT rs m EBB. + unfold exec_bblock. + generalize (bblock_simu_reduce_aux p1 p2 H0). + unfold bblock_simu_aux. clear H0. + unfold exec_bblock, bbstep. intros H0 m' t0 (rs1 & m1 & H1 & H2). + assert ((has_builtin p1 = false /\ has_builtin p2 = false) \/ (has_builtin p1 = true \/ has_builtin p2 = true)). { repeat destruct (has_builtin _); simpl; intuition. } + destruct H as [[X1 X2]|H]. + - (* Not a builtin *) + exploit (H0); eauto; erewrite H1; simpl; (*gen*) + unfold estep; unfold has_builtin in *. + { destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *. + inversion H2; subst. rewrite H3; discriminate. } + destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *. + { inversion H2; subst. rewrite H3. + destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. + intros H4. eexists; eexists; split; try reflexivity. + destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto. + inversion H4. econstructor. } + { inversion H2; subst. + destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. +intros H4. eexists; eexists; split; try reflexivity. + destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto. + inversion H4. rewrite H3. econstructor. } + - (* Builtin *) + exploit (BLT); eauto. + intros EXIT. + unfold has_builtin in H. + assert (is_builtin (exit p1) = true). { rewrite <- EXIT in H; intuition. } + clear H. + generalize (H0 rs m); eauto; erewrite H1; simpl; + unfold estep. destruct (exit p1) as [[]|] eqn:EQEX1; try discriminate. + rewrite <- EXIT. + intros CONTRA. + exploit (CONTRA); try discriminate. + destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate. + intros H4. eexists; eexists; split; try reflexivity. + inversion H2; subst. inversion H4; subst. + econstructor; eauto. + + unfold incrPC in H5. + replace (rs2 SP) with (rs1 SP). + replace (fun r : dreg => rs2 r) with (fun r : dreg => rs1 r); auto. + * apply functional_extensionality. + intros r; destruct (PregEq.eq r PC); try discriminate. + replace (rs1 r) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) r) by auto. + rewrite H5; rewrite Pregmap.gso; auto. + * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto. + rewrite H5; rewrite Pregmap.gso; auto; try discriminate. + + rewrite !incrPC_set_res_commut. + rewrite !incrPC_undef_regs_commut. + rewrite H5. + reflexivity. +Qed. + +(** Used for debug traces *) + +Definition ireg_name (ir: ireg) : pstring := + match ir with + | X0 => Str ("X0") | X1 => Str ("X1") | X2 => Str ("X2") | X3 => Str ("X3") | X4 => Str ("X4") | X5 => Str ("X5") | X6 => Str ("X6") | X7 => Str ("X7") + | X8 => Str ("X8") | X9 => Str ("X9") | X10 => Str ("X10") | X11 => Str ("X11") | X12 => Str ("X12") | X13 => Str ("X13") | X14 => Str ("X14") | X15 => Str ("X15") + | X16 => Str ("X16") | X17 => Str ("X17") | X18 => Str ("X18") | X19 => Str ("X19") | X20 => Str ("X20") | X21 => Str ("X21") | X22 => Str ("X22") | X23 => Str ("X23") + | X24 => Str ("X24") | X25 => Str ("X25") | X26 => Str ("X26") | X27 => Str ("X27") | X28 => Str ("X28") | X29 => Str ("X29") | X30 => Str ("X30") + end +. + +Definition freg_name (fr: freg) : pstring := + match fr with + | D0 => Str ("D0") | D1 => Str ("D1") | D2 => Str ("D2") | D3 => Str ("D3") | D4 => Str ("D4") | D5 => Str ("D5") | D6 => Str ("D6") | D7 => Str ("D7") + | D8 => Str ("D8") | D9 => Str ("D9") | D10 => Str ("D10") | D11 => Str ("D11") | D12 => Str ("D12") | D13 => Str ("D13") | D14 => Str ("D14") | D15 => Str ("D15") + | D16 => Str ("D16") | D17 => Str ("D17") | D18 => Str ("D18") | D19 => Str ("D19") | D20 => Str ("D20") | D21 => Str ("D21") | D22 => Str ("D22") | D23 => Str ("D23") + | D24 => Str ("D24") | D25 => Str ("D25") | D26 => Str ("D26") | D27 => Str ("D27") | D28 => Str ("D28") | D29 => Str ("D29") | D30 => Str ("D30") | D31 => Str ("D31") + end +. + +Definition iregsp_name (irsp: iregsp) : pstring := + match irsp with + | RR1 ir => ireg_name ir + | XSP => Str ("XSP") + end. + +Definition dreg_name (dr: dreg) : ?? pstring := + match dr with + | IR ir => match ir with + | XSP => RET (Str ("XSP")) + | RR1 irr => RET (ireg_name irr) + end + | FR fr => RET (freg_name fr) + end. + +Definition string_of_name (x: P.R.t): ?? pstring := + if (Pos.eqb x pmem) then + RET (Str "MEM") + else + match inv_ppos x with + | Some (CR cr) => match cr with + | CN => RET (Str ("CN")) + | CZ => RET (Str ("CZ")) + | CC => RET (Str ("CC")) + | CV => RET (Str ("CV")) + end + | Some (PC) => RET (Str ("PC")) + | Some (DR dr) => dreg_name dr + | _ => RET (Str ("UNDEFINED")) + end. + +Definition string_of_name_ArithP (n: arith_p) : pstring := + match n with + | Padrp _ _ => "Padrp" + | Pmovz _ _ _ => "Pmov" + | Pmovn _ _ _ => "Pmov" + | Pfmovimms _ => "Pfmovimm" + | Pfmovimmd _ => "Pfmovimm" + end. + +Definition string_of_name_ArithPP (n: arith_pp) : pstring := + match n with + | Pmov => "Pmov" + | Pmovk _ _ _ => "Pmovk" + | Paddadr _ _ => "Paddadr" + | Psbfiz _ _ _ => "Psbfiz" + | Psbfx _ _ _ => "Psbfx" + | Pubfiz _ _ _ => "Pubfiz" + | Pubfx _ _ _ => "Pubfx" + | Pfmov => "Pfmov" + | Pfcvtds => "Pfcvtds" + | Pfcvtsd => "Pfcvtsd" + | Pfabs _ => "Pfabs" + | Pfneg _ => "Pfneg" + | Pscvtf _ _ => "Pscvtf" + | Pucvtf _ _ => "Pucvtf" + | Pfcvtzs _ _ => "Pfcvtzs" + | Pfcvtzu _ _ => "Pfcvtzu" + | Paddimm _ _ => "Paddimm" + | Psubimm _ _ => "Psubimm" + end. + +Definition string_of_name_ArithPPP (n: arith_ppp) : pstring := + match n with + | Pasrv _ => "Pasrv" + | Plslv _ => "Plslv" + | Plsrv _ => "Plsrv" + | Prorv _ => "Prorv" + | Psmulh => "Psmulh" + | Pumulh => "Pumulh" + | Psdiv _ => "Psdiv" + | Pudiv _ => "Pudiv" + | Paddext _ => "Paddext" + | Psubext _ => "Psubext" + | Pfadd _ => "Pfadd" + | Pfdiv _ => "Pfdiv" + | Pfmul _ => "Pfmul" + | Pfsub _ => "Pfsub" + end. + +Definition string_of_name_ArithRR0R (n: arith_rr0r) : pstring := + match n with + | Padd _ _ => "ArithRR0R=>Padd" + | Psub _ _ => "ArithRR0R=>Psub" + | Pand _ _ => "ArithRR0R=>Pand" + | Pbic _ _ => "ArithRR0R=>Pbic" + | Peon _ _ => "ArithRR0R=>Peon" + | Peor _ _ => "ArithRR0R=>Peor" + | Porr _ _ => "ArithRR0R=>Porr" + | Porn _ _ => "ArithRR0R=>Porn" + end. + +Definition string_of_name_ArithRR0R_XZR (n: arith_rr0r) : pstring := + match n with + | Padd _ _ => "ArithRR0R_XZR=>Padd" + | Psub _ _ => "ArithRR0R_XZR=>Psub" + | Pand _ _ => "ArithRR0R_XZR=>Pand" + | Pbic _ _ => "ArithRR0R_XZR=>Pbic" + | Peon _ _ => "ArithRR0R_XZR=>Peon" + | Peor _ _ => "ArithRR0R_XZR=>Peor" + | Porr _ _ => "ArithRR0R_XZR=>Porr" + | Porn _ _ => "ArithRR0R_XZR=>Porn" + end. + +Definition string_of_name_ArithRR0 (n: arith_rr0) : pstring := + match n with + | Pandimm _ _ => "ArithRR0=>Pandimm" + | Peorimm _ _ => "ArithRR0=>Peorimm" + | Porrimm _ _ => "ArithRR0=>Porrimm" + end. + +Definition string_of_name_ArithRR0_XZR (n: arith_rr0) : pstring := +match n with + | Pandimm _ _ => "ArithRR0_XZR=>Pandimm" + | Peorimm _ _ => "ArithRR0_XZR=>Peorimm" + | Porrimm _ _ => "ArithRR0_XZR=>Porrimm" + end. + +Definition string_of_name_ArithARRRR0 (n: arith_arrrr0) : pstring := + match n with + | Pmadd _ => "ArithARRRR0=>Pmadd" + | Pmsub _ => "ArithARRRR0=>Pmsub" + end. + +Definition string_of_name_ArithARRRR0_XZR (n: arith_arrrr0) : pstring := + match n with + | Pmadd _ => "ArithARRRR0_XZR=>Pmadd" + | Pmsub _ => "ArithARRRR0_XZR=>Pmsub" + end. + +Definition string_of_name_ArithComparisonPP_CN (n: arith_comparison_pp) : pstring := + match n with + | Pcmpext _ => "ArithComparisonPP_CN=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CN=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CN=>Pfcmp" + end. + +Definition string_of_name_ArithComparisonPP_CZ (n: arith_comparison_pp) : pstring := + match n with + | Pcmpext _ => "ArithComparisonPP_CZ=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CZ=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CZ=>Pfcmp" + end. + +Definition string_of_name_ArithComparisonPP_CC (n: arith_comparison_pp) : pstring := +match n with + | Pcmpext _ => "ArithComparisonPP_CC=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CC=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CC=>Pfcmp" + end. + +Definition string_of_name_ArithComparisonPP_CV (n: arith_comparison_pp) : pstring := +match n with + | Pcmpext _ => "ArithComparisonPP_CV=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CV=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CV=>Pfcmp" + end. + +Definition string_of_name_ArithComparisonR0R_CN (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CN=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CN=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CN=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CZ (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CZ=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CZ=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CZ=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CC (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CC=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CC=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CC=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CV (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CV=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CV=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CV=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CN_XZR (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CN_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CN_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CN_XZR=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CZ_XZR (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CZ_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CZ_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CZ_XZR=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CC_XZR (n: arith_comparison_r0r) : pstring := +match n with + | Pcmp _ _ => "ArithComparisonR0R_CC_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CC_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CC_XZR=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CV_XZR (n: arith_comparison_r0r) : pstring := +match n with + | Pcmp _ _ => "ArithComparisonR0R_CV_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CV_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CV_XZR=>Ptst" + end. + +Definition string_of_name_ArithComparisonP_CN (n: arith_comparison_p) : pstring := + match n with + | Pfcmp0 _ => "ArithComparisonP_CN=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CN=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CN=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CN=>Ptstimm" + end. + +Definition string_of_name_ArithComparisonP_CZ (n: arith_comparison_p) : pstring := + match n with + | Pfcmp0 _ => "ArithComparisonP_CZ=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CZ=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CZ=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CZ=>Ptstimm" + end. + +Definition string_of_name_ArithComparisonP_CC (n: arith_comparison_p) : pstring := + match n with + | Pfcmp0 _ => "ArithComparisonP_CC=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CC=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CC=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CC=>Ptstimm" + end. + +Definition string_of_name_ArithComparisonP_CV (n: arith_comparison_p) : pstring := + match n with + | Pfcmp0 _ => "ArithComparisonP_CV=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CV=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CV=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CV=>Ptstimm" + end. + +Definition string_of_name_cset (c: testcond) : pstring := + match c with + | TCeq => "Cset=>TCeq" + | TCne => "Cset=>TCne" + | TChs => "Cset=>TChs" + | TClo => "Cset=>TClo" + | TCmi => "Cset=>TCmi" + | TCpl => "Cset=>TCpl" + | TChi => "Cset=>TChi" + | TCls => "Cset=>TCls" + | TCge => "Cset=>TCge" + | TClt => "Cset=>TClt" + | TCgt => "Cset=>TCgt" + | TCle => "Cset=>TCle" + end. + +Definition string_of_arith (op: arith_op): pstring := + match op with + | OArithP n => string_of_name_ArithP n + | OArithPP n => string_of_name_ArithPP n + | OArithPPP n => string_of_name_ArithPPP n + | OArithRR0R n => string_of_name_ArithRR0R n + | OArithRR0R_XZR n _ => string_of_name_ArithRR0R_XZR n + | OArithRR0 n => string_of_name_ArithRR0 n + | OArithRR0_XZR n _ => string_of_name_ArithRR0_XZR n + | OArithARRRR0 n => string_of_name_ArithARRRR0 n + | OArithARRRR0_XZR n _ => string_of_name_ArithARRRR0_XZR n + | OArithComparisonPP_CN n => string_of_name_ArithComparisonPP_CN n + | OArithComparisonPP_CZ n => string_of_name_ArithComparisonPP_CZ n + | OArithComparisonPP_CC n => string_of_name_ArithComparisonPP_CC n + | OArithComparisonPP_CV n => string_of_name_ArithComparisonPP_CV n + | OArithComparisonR0R_CN n _ => string_of_name_ArithComparisonR0R_CN n + | OArithComparisonR0R_CZ n _ => string_of_name_ArithComparisonR0R_CZ n + | OArithComparisonR0R_CC n _ => string_of_name_ArithComparisonR0R_CC n + | OArithComparisonR0R_CV n _ => string_of_name_ArithComparisonR0R_CV n + | OArithComparisonR0R_CN_XZR n _ _ => string_of_name_ArithComparisonR0R_CN_XZR n + | OArithComparisonR0R_CZ_XZR n _ _ => string_of_name_ArithComparisonR0R_CZ_XZR n + | OArithComparisonR0R_CC_XZR n _ _ => string_of_name_ArithComparisonR0R_CC_XZR n + | OArithComparisonR0R_CV_XZR n _ _ => string_of_name_ArithComparisonR0R_CV_XZR n + | OArithComparisonP_CN n => string_of_name_ArithComparisonP_CN n + | OArithComparisonP_CZ n => string_of_name_ArithComparisonP_CZ n + | OArithComparisonP_CC n => string_of_name_ArithComparisonP_CC n + | OArithComparisonP_CV n => string_of_name_ArithComparisonP_CV n + | Ocset c => string_of_name_cset c + | Ofmovi _ => "Ofmovi" + | Ofmovi_XZR _ => "Ofmovi_XZR" + | Ocsel _ => "Ocsel" + | Ofnmul _ => "Ofnmul" + end. + +Definition string_of_ofs (ofs: ptrofs) : ?? pstring := + (string_of_Z (Ptrofs.signed ofs)). + +Definition string_of_int (n: int) : ?? pstring := + (string_of_Z (Int.signed n)). + +Definition string_of_int64 (n: int64) : ?? pstring := + (string_of_Z (Int64.signed n)). + +Notation "x +; y" := (Concat x y). + +Definition string_of_addressing (a: addressing) : ?? pstring := + match a with + | ADimm base n => + DO n' <~ string_of_int64 n;; + RET ((Str "[ADimm ") +; (iregsp_name base) +; " " +; n' +; "]") + | ADreg base r => + RET ((Str "[ADreg ") +; (iregsp_name base) +; " " +; (ireg_name r) +; "]") + | ADlsl base r n => + DO n' <~ string_of_int n;; + RET ((Str "[ADlsl ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]") + | ADsxt base r n => + DO n' <~ string_of_int n;; + RET ((Str "[ADsxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]") + | ADuxt base r n => + DO n' <~ string_of_int n;; + RET ((Str "[ADuxt ") +; (iregsp_name base) +; " " +; (ireg_name r) +; " " +; n' +; "]") + | ADadr base id ofs => + DO id' <~ string_of_Z (Zpos id);; + DO ofs' <~ string_of_ofs ofs;; + RET ((Str "[ADadr ") +; (iregsp_name base) +; " " +; id' +; " " +; ofs' +; "]") + | ADpostincr base n => + DO n' <~ string_of_int64 n;; + RET ((Str "[ADpostincr ") +; (iregsp_name base) +; " " +; n' +; "]") + end. + +Definition string_of_ld_rd_a (ld: load_rd_a) : pstring := + match ld with + | Pldrw => Str "Pldrw" + | Pldrw_a => Str "Pldrw_a" + | Pldrx => Str "Pldrx" + | Pldrx_a => Str "Pldrx_a" + | Pldrb _ => Str "Pldrb" + | Pldrsb _ => Str "Pldrsb" + | Pldrh _ => Str "Pldrh" + | Pldrsh _ => Str "Pldrsh" + | Pldrzw => Str "Pldrzw" + | Pldrsw => Str "Pldrsw" + | Pldrs => Str "Pldrs" + | Pldrd => Str "Pldrd" + | Pldrd_a => Str "Pldrd_a" + end. + +Definition string_of_ldi (ldi: ld_instruction) : ?? pstring:= + match ldi with + | PLd_rd_a ld rd a => + DO a' <~ string_of_addressing a;; + DO rd' <~ dreg_name rd;; + RET (Str "PLd_rd_a (" +; (string_of_ld_rd_a ld) +; " " +; rd' +; " " +; a' +; ")") + | Pldp _ _ _ _ _ a => + DO a' <~ string_of_addressing a;; + RET (Str "Pldp (" +; a' +; ")") + end. + +Definition string_of_load (op: load_op) : ?? pstring := + match op with + | Oload1 ld _ a => + DO a' <~ string_of_addressing a;; + (*DO ld' <~ string_of_ldi ld;;*) + RET((Str "Oload1 ") +; " " +; string_of_ld_rd_a ld +; " " +; a' +; " ") + | Oload2 ld _ a => + DO a' <~ string_of_addressing a;; + (*DO ld' <~ string_of_ldi ld;;*) + RET((Str "Oload2 ") +; " " +; string_of_ld_rd_a ld +; " " +; a' +; " ") + | OloadU _ _ _ => RET (Str "OloadU") + end. + +Definition string_of_st_rs_a (st: store_rs_a) : pstring := + match st with + | Pstrw => Str "Pstrw" + | Pstrw_a => Str "Pstrw_a" + | Pstrx => Str "Pstrx" + | Pstrx_a => Str "Pstrx_a" + | Pstrb => Str "Pstrb" + | Pstrh => Str "Pstrh" + | Pstrs => Str "Pstrs" + | Pstrd => Str "Pstrd" + | Pstrd_a => Str "Pstrd_a" + end. + +Definition string_of_sti (sti: st_instruction) : ?? pstring:= + match sti with + | PSt_rs_a st rs a => + DO a' <~ string_of_addressing a;; + DO rs' <~ dreg_name rs;; + RET (Str "PSt_rs_a (" +; (string_of_st_rs_a st) +; " " +; rs' +; " " +; a' +; ")") + | Pstp _ _ _ _ _ a => + DO a' <~ string_of_addressing a;; + RET (Str "Pstp (" +; a' +; ")") + end. + +Definition string_of_store (op: store_op) : ?? pstring := + match op with + | Ostore1 st _ a => + DO a' <~ string_of_addressing a;; + (*DO st' <~ string_of_sti st;;*) + RET((Str "Ostore1 ") +; " " +; string_of_st_rs_a st +; " " +; a' +; " ") + | Ostore2 st _ a => + DO a' <~ string_of_addressing a;; + (*DO st' <~ string_of_sti st;;*) + RET((Str "Ostore2 ") +; " " +; string_of_st_rs_a st +; " " +; a' +; " ") + | OstoreU _ _ _ => RET (Str "OstoreU") + end. + +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" + | OError => "OError" + end. + +Definition string_of_allocf (op: allocf_op) : pstring := + match op with + | OAllocf_SP _ _ => "OAllocf_SP" + | 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) + | Load op => string_of_load op + | Store op => string_of_store op + | Control op => RET (string_of_control op) + | Allocframe op => RET (string_of_allocf op) + | 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. + +(** REWRITE RULES *) + +Definition is_constant (o: op): bool := + match o with + | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ | Loadsymbol _ | Constant _ | Obl _ | Obs _ => true + | _ => false + end. + +Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None. +Proof. + destruct o; simpl in * |- *; try congruence. + destruct op0; simpl in * |- *; try congruence. + destruct co; simpl in * |- *; try congruence; + unfold control_eval; destruct ge; simpl in * |- *; try congruence. +Qed. + +Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t). + +Local Hint Resolve is_constant_correct: wlp. + +Lemma main_reduce_correct t: + WHEN main_reduce t ~> pt THEN Terms.match_pt t pt. +Proof. + wlp_simplify. +Qed. + +Definition reduce := {| Terms.result := main_reduce; Terms.result_correct := main_reduce_correct |}. + +Definition bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool := + assert_same_builtin p1 p2;; + if verb then + IST.verb_bblock_simu_test reduce string_of_name string_of_op (trans_block p1) (trans_block p2) + else + IST.bblock_simu_test reduce (trans_block p1) (trans_block p2). + +Local Hint Resolve IST.bblock_simu_test_correct IST.verb_bblock_simu_test_correct: wlp. + +(** Main simulation (Impure) theorem *) +Theorem bblock_simu_test_correct verb p1 p2 : + WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn lk, Asmblockprops.bblock_simu lk ge fn p1 p2. +Proof. + wlp_simplify; eapply bblock_simu_reduce with (Ge:={| _genv := ge; _fn := fn; _lk := lk |}); eauto; + intros; destruct H; auto. +Qed. + +Hint Resolve bblock_simu_test_correct: wlp. + +(** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) + +Import UnsafeImpure. + +Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock): bool := + match unsafe_coerce (bblock_simu_test verb p1 p2) with + | Some b => b + | None => false + end. + +Theorem pure_bblock_simu_test_correct verb p1 p2 lk ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu lk ge fn p1 p2. +Proof. + unfold pure_bblock_simu_test. + destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate. + intros; subst. eapply bblock_simu_test_correct; eauto. + apply unsafe_coerce_not_really_correct; eauto. +Qed. + +Definition bblock_simub: Asmblock.bblock -> Asmblock.bblock -> bool := pure_bblock_simu_test true. + +Lemma bblock_simub_correct p1 p2 lk ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu lk ge fn p1 p2. +Proof. + eapply (pure_bblock_simu_test_correct true). +Qed. |