From 241da496839a9101e843ce7b1da4a668f998498a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 2 Nov 2020 17:13:50 +0100 Subject: Preparation for postpass in aarch64 and refactoring --- aarch64/Asmblockdeps.v | 1841 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1841 insertions(+) create mode 100644 aarch64/Asmblockdeps.v (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v new file mode 100644 index 00000000..1acbdf1e --- /dev/null +++ b/aarch64/Asmblockdeps.v @@ -0,0 +1,1841 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(** * Translation from [Asmvliw] to [AbstractBB] *) + +(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmvliw] into [L]. + [AbstractBB] will then define two semantics for [L]: a sequential and a parallel one. + We prove a bisimulation between the parallel semantics of [L] and [AsmVLIW]. + We also prove a bisimulation between the sequential semantics of [L] and [Asmblock]. + Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L]. + *) + + (* +Require Import AST. +Require Import Asmblock. +Require Import Asmblockgenproof0 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 Parallelizability. +Require Import Asmvliw Permutation. +Require Import Chunks. + +Require Import Lia. + +Open Scope impure. + +(** Definition of [L] *) + +Module P<: ImpParam. +Module R := Pos. + +Section IMPPARAM. + +Definition env := Genv.t fundef unit. + +Inductive genv_wrap := Genv (ge: env) (fn: function). +Definition genv := genv_wrap. + +Variable Ge: genv. + +Inductive value_wrap := + | Val (v: val) + | Memstate (m: mem) +. + +Definition value := value_wrap. + +Inductive control_op := + | Oj_l (l: label) + | Ocb (bt: btest) (l: label) + | Ocbu (bt: btest) (l: label) + | Odiv + | Odivu + | OError + | OIncremPC (sz: Z) + | Ojumptable (l: list label) +. + +Inductive arith_op := + | OArithR (n: arith_name_r) + | OArithRR (n: arith_name_rr) + | OArithRI32 (n: arith_name_ri32) (imm: int) + | OArithRI64 (n: arith_name_ri64) (imm: int64) + | OArithRF32 (n: arith_name_rf32) (imm: float32) + | OArithRF64 (n: arith_name_rf64) (imm: float) + | OArithRRR (n: arith_name_rrr) + | OArithRRI32 (n: arith_name_rri32) (imm: int) + | OArithRRI64 (n: arith_name_rri64) (imm: int64) + | OArithARRR (n: arith_name_arrr) + | OArithARR (n: arith_name_arr) + | OArithARRI32 (n: arith_name_arri32) (imm: int) + | OArithARRI64 (n: arith_name_arri64) (imm: int64) +. + +Coercion OArithR: arith_name_r >-> arith_op. +Coercion OArithRR: arith_name_rr >-> arith_op. +Coercion OArithRI32: arith_name_ri32 >-> Funclass. +Coercion OArithRI64: arith_name_ri64 >-> Funclass. +Coercion OArithRF32: arith_name_rf32 >-> Funclass. +Coercion OArithRF64: arith_name_rf64 >-> Funclass. +Coercion OArithRRR: arith_name_rrr >-> arith_op. +Coercion OArithRRI32: arith_name_rri32 >-> Funclass. +Coercion OArithRRI64: arith_name_rri64 >-> Funclass. + +Inductive load_op := + | OLoadRRO (n: load_name) (trap: trapping_mode) (ofs: offset) + | OLoadRRR (n: load_name) (trap: trapping_mode) + | OLoadRRRXS (n: load_name) (trap: trapping_mode) +. + +Coercion OLoadRRO: load_name >-> Funclass. + +Inductive store_op := + | OStoreRRO (n: store_name) (ofs: offset) + | OStoreRRR (n: store_name) + | OStoreRRRXS (n: store_name) +. + +Coercion OStoreRRO: store_name >-> Funclass. + +Inductive op_wrap := + | Arith (ao: arith_op) + | Load (lo: load_op) + | Store (so: store_op) + | Control (co: control_op) + | Allocframe (sz: Z) (pos: ptrofs) + | Allocframe2 (sz: Z) (pos: ptrofs) + | Freeframe (sz: Z) (pos: ptrofs) + | Freeframe2 (sz: Z) (pos: ptrofs) + | Constant (v: val) + | Fail +. + +Coercion Arith: arith_op >-> op_wrap. +Coercion Load: load_op >-> op_wrap. +Coercion Store: store_op >-> op_wrap. +Coercion Control: control_op >-> op_wrap. + +Definition op := op_wrap. + +Definition arith_eval (ao: arith_op) (l: list value) := + let (ge, fn) := Ge in + match ao, l with + | OArithR n, [] => Some (Val (arith_eval_r ge n)) + + | OArithRR n, [Val v] => Some (Val (arith_eval_rr n v)) + + | OArithRI32 n i, [] => Some (Val (arith_eval_ri32 n i)) + | OArithRI64 n i, [] => Some (Val (arith_eval_ri64 n i)) + | OArithRF32 n i, [] => Some (Val (arith_eval_rf32 n i)) + | OArithRF64 n i, [] => Some (Val (arith_eval_rf64 n i)) + + | OArithRRR n, [Val v1; Val v2] => Some (Val (arith_eval_rrr n v1 v2)) + | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i)) + | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i)) + + | OArithARR n, [Val v1; Val v2] => Some (Val (arith_eval_arr n v1 v2)) + | OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3)) + | OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i)) + | OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i)) + + | _, _ => None + end. + +Definition exec_incorrect_load trap chunk := + match trap with + | TRAP => None + | NOTRAP => Some (Val (concrete_default_notrap_load_value chunk)) + end. + +Definition exec_load_deps_offset (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := + let (ge, fn) := Ge in + match (eval_offset ofs) with + | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with + | None => exec_incorrect_load trap chunk + | Some vl => Some (Val vl) + end + | _ => None + end. + +Definition exec_load_deps_reg (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) := + match Mem.loadv chunk m (Val.addl v vo) with + | None => exec_incorrect_load trap chunk + | Some vl => Some (Val vl) + end. + +Definition exec_load_deps_regxs (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) := + match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with + | None => exec_incorrect_load trap chunk + | Some vl => Some (Val vl) + end. + +Definition load_eval (lo: load_op) (l: list value) := + match lo, l with + | OLoadRRO n trap ofs, [Val v; Memstate m] => exec_load_deps_offset trap (load_chunk n) m v ofs + | OLoadRRR n trap, [Val v; Val vo; Memstate m] => exec_load_deps_reg trap (load_chunk n) m v vo + | OLoadRRRXS n trap, [Val v; Val vo; Memstate m] => exec_load_deps_regxs trap (load_chunk n) m v vo + | _, _ => None + end. + +Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) := + let (ge, fn) := Ge in + match (eval_offset ofs) with + | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with + | None => None + | Some m' => Some (Memstate m') + end + | _ => None + end. + +Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) := + match Mem.storev chunk m (Val.addl va vo) vs with + | None => None + | Some m' => Some (Memstate m') + end. + +Definition exec_store_deps_regxs (chunk: memory_chunk) (m: mem) (vs va vo: val) := + match Mem.storev chunk m (Val.addl va (Val.shll vo (scale_of_chunk chunk))) vs with + | None => None + | Some m' => Some (Memstate m') + end. + +Definition store_eval (so: store_op) (l: list value) := + match so, l with + | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => exec_store_deps_offset (store_chunk n) m vs va ofs + | OStoreRRR n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_reg (store_chunk n) m vs va vo + | OStoreRRRXS n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_regxs (store_chunk n) m vs va vo + | _, _ => None + end. + +Local Open Scope Z. + +Remark size_chunk_positive: forall chunk, + (size_chunk chunk) > 0. +Proof. + destruct chunk; simpl; lia. +Qed. + +Remark size_chunk_small: forall chunk, + (size_chunk chunk) <= 8. +Proof. + destruct chunk; simpl; lia. +Qed. + +Definition disjoint_chunks + (ofs1 : offset) (chunk1 : memory_chunk) + (ofs2 : offset) (chunk2 : memory_chunk) := + Intv.disjoint ((Ptrofs.unsigned ofs1), + ((Ptrofs.unsigned ofs1) + (size_chunk chunk1))) + ((Ptrofs.unsigned ofs2), + ((Ptrofs.unsigned ofs2) + (size_chunk chunk2))). + +Definition small_offset_threshold := 18446744073709551608. + +Lemma store_store_disjoint_offsets : + forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1' m2', + (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) -> + (Ptrofs.unsigned ofs1) < small_offset_threshold -> + (Ptrofs.unsigned ofs2) < small_offset_threshold -> + store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0] = Some (Memstate m1') -> + store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m1'] = Some (Memstate m2') -> + m2 = m2'. +Proof. + intros until m2'. + intros DISJOINT SMALL1 SMALL2 STORE0 STORE1 STORE0' STORE1'. + unfold disjoint_chunks in DISJOINT. + destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence. + destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence. + destruct va as [base | ]; try congruence. + unfold exec_store_deps_offset in *. + destruct Ge. + unfold eval_offset in *; simpl in *. + unfold Mem.storev in *. + unfold Val.offset_ptr in *. + destruct base as [ | | | | | wblock wpofs] in * ; try congruence. + destruct (Mem.store _ _ _ _ _) eqn:E0; try congruence. + inv STORE0. + destruct (Mem.store (store_chunk n2) _ _ _ _) eqn:E1; try congruence. + inv STORE1. + destruct (Mem.store (store_chunk n2) m0 _ _ _) eqn:E0'; try congruence. + inv STORE0'. + destruct (Mem.store _ m1' _ _ _) eqn:E1'; try congruence. + inv STORE1'. + assert (Some m2 = Some m2'). + 2: congruence. + rewrite <- E1. + rewrite <- E1'. + eapply Mem.store_store_other. + 2, 3: eassumption. + + right. + pose proof (size_chunk_positive (store_chunk n1)). + pose proof (size_chunk_positive (store_chunk n2)). + pose proof (size_chunk_small (store_chunk n1)). + pose proof (size_chunk_small (store_chunk n2)). + destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; + unfold Intv.empty in DIS; simpl in DIS. + 1, 2: lia. + pose proof (Ptrofs.unsigned_range ofs1). + pose proof (Ptrofs.unsigned_range ofs2). + unfold small_offset_threshold in *. + destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; + destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2; + change Ptrofs.modulus with 18446744073709551616 in *; + lia. +Qed. + +Lemma load_store_disjoint_offsets : + forall n1 n2 tm ofs1 ofs2 vs va m0 m1, + (disjoint_chunks ofs1 (store_chunk n1) ofs2 (load_chunk n2)) -> + (Ptrofs.unsigned ofs1) < small_offset_threshold -> + (Ptrofs.unsigned ofs2) < small_offset_threshold -> + store_eval (OStoreRRO n1 ofs1) [vs; va; Memstate m0] = Some (Memstate m1) -> + load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m1] = + load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m0]. +Proof. + intros until m1. + intros DISJOINT SMALL1 SMALL2 STORE0. + destruct vs as [v | ]; simpl in STORE0; try congruence. + destruct va as [base | ]; try congruence. + unfold exec_store_deps_offset in *. + unfold eval_offset in *; simpl in *. + unfold exec_load_deps_offset. + unfold Mem.storev, Mem.loadv in *. + destruct Ge in *. + unfold eval_offset in *. + unfold Val.offset_ptr in *. + destruct base as [ | | | | | wblock wpofs] in * ; try congruence. + destruct (Mem.store _ _ _ _) eqn:E0; try congruence. + inv STORE0. + assert ( + (Mem.load (load_chunk n2) m1 wblock + (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) = + (Mem.load (load_chunk n2) m0 wblock + (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) ) as LOADS. + { + eapply Mem.load_store_other. + eassumption. + right. + pose proof (size_chunk_positive (store_chunk n1)). + pose proof (size_chunk_positive (load_chunk n2)). + pose proof (size_chunk_small (store_chunk n1)). + pose proof (size_chunk_small (load_chunk n2)). + destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; + unfold Intv.empty in DIS; simpl in DIS. + 1,2: lia. + + pose proof (Ptrofs.unsigned_range ofs1). + pose proof (Ptrofs.unsigned_range ofs2). + unfold small_offset_threshold in *. + destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; + destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2; + change Ptrofs.modulus with 18446744073709551616 in *; + lia. + } + destruct (Mem.load _ m1 _ _) in *; destruct (Mem.load _ m0 _ _) in *; congruence. +Qed. + +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 eval_branch_deps (f: function) (l: label) (vpc: val) (res: option bool) := + match res with + | Some true => goto_label_deps f l vpc + | Some false => Some (Val vpc) + | None => None + end. + +Definition control_eval (o: control_op) (l: list value) := + let (ge, fn) := Ge in + match o, l with + | (Ojumptable 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 + | Oj_l l, [Val vpc] => goto_label_deps fn l vpc + | Ocb bt l, [Val v; Val vpc] => + match cmp_for_btest bt with + | (Some c, Int) => eval_branch_deps fn l vpc (Val.cmp_bool c v (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch_deps fn l vpc (Val.cmpl_bool c v (Vlong (Int64.repr 0))) + | (None, _) => None + end + | Ocbu bt l, [Val v; Val vpc] => + match cmpu_for_btest bt with + | (Some c, Int) => eval_branch_deps fn l vpc (Val_cmpu_bool c v (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0))) + | (None, _) => None + end + | Odiv, [Val v1; Val v2] => + match Val.divs v1 v2 with + | Some v => Some (Val v) + | None => None + end + | Odivu, [Val v1; Val v2] => + match Val.divu v1 v2 with + | Some v => Some (Val v) + | None => None + end + | OIncremPC sz, [Val vpc] => Some (Val (Val.offset_ptr vpc (Ptrofs.repr sz))) + | OError, _ => None + | _, _ => None + end. + +Definition op_eval (o: op) (l: list value) := + match o, l with + | Arith o, l => arith_eval o l + | Load o, l => load_eval o l + | Store o, l => store_eval o l + | Control o, l => control_eval o l + | Allocframe sz pos, [Val spv; Memstate m] => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + match Mem.storev Mptr m1 (Val.offset_ptr sp pos) spv with + | None => None + | Some m => Some (Memstate m) + end + | Allocframe2 sz pos, [Val spv; Memstate m] => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + match Mem.storev Mptr m1 (Val.offset_ptr sp pos) spv with + | None => None + | Some m => Some (Val sp) + end + | Freeframe sz pos, [Val spv; Memstate m] => + match Mem.loadv Mptr m (Val.offset_ptr spv pos) 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 + | Freeframe2 sz pos, [Val spv; Memstate m] => + match Mem.loadv Mptr m (Val.offset_ptr spv pos) with + | None => None + | Some v => + match spv with + | Vptr stk ofs => + match Mem.free m stk 0 sz with + | None => None + | Some m' => Some (Val v) + end + | _ => None + end + end + | Constant v, [] => Some (Val v) + | Fail, _ => None + | _, _ => None + end. + + +Definition arith_op_eq (o1 o2: arith_op): ?? bool := + match o1 with + | OArithR n1 => + match o2 with OArithR n2 => struct_eq n1 n2 | _ => RET false end + | OArithRR n1 => + match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithRI32 n1 i1 => + match o2 with OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRI64 n1 i1 => + match o2 with OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRF32 n1 i1 => + match o2 with OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRF64 n1 i1 => + match o2 with OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRRR n1 => + match o2 with OArithRRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithRRI32 n1 i1 => + match o2 with OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithRRI64 n1 i1 => + match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithARRR n1 => + match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end + | OArithARR n1 => + match o2 with OArithARR n2 => phys_eq n1 n2 | _ => RET false end + | OArithARRI32 n1 i1 => + match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end + | OArithARRI64 n1 i1 => + match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => 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. +Qed. +Hint Resolve arith_op_eq_correct: wlp. +Opaque arith_op_eq_correct. + +Definition offset_eq (ofs1 ofs2 : offset): ?? bool := + RET (Ptrofs.eq ofs1 ofs2). + +Lemma offset_eq_correct ofs1 ofs2: + WHEN offset_eq ofs1 ofs2 ~> b THEN b = true -> ofs1 = ofs2. +Proof. + wlp_simplify. + pose (Ptrofs.eq_spec ofs1 ofs2). + rewrite H in *. + trivial. +Qed. +Hint Resolve offset_eq_correct: wlp. + +Definition trapping_mode_eq trap1 trap2 := + RET (match trap1, trap2 with + | TRAP, TRAP | NOTRAP, NOTRAP => true + | TRAP, NOTRAP | NOTRAP, TRAP => false + end). +Lemma trapping_mode_eq_correct t1 t2: + WHEN trapping_mode_eq t1 t2 ~> b THEN b = true -> t1 = t2. +Proof. + wlp_simplify. + destruct t1; destruct t2; trivial; discriminate. +Qed. +Hint Resolve trapping_mode_eq_correct: wlp. + +Definition load_op_eq (o1 o2: load_op): ?? bool := + match o1 with + | OLoadRRO n1 trap ofs1 => + match o2 with + | OLoadRRO n2 trap2 ofs2 => iandb (phys_eq n1 n2) (iandb (offset_eq ofs1 ofs2) (trapping_mode_eq trap trap2)) + | _ => RET false + end + | OLoadRRR n1 trap => + match o2 with + | OLoadRRR n2 trap2 => iandb (phys_eq n1 n2) (trapping_mode_eq trap trap2) + | _ => RET false + end + | OLoadRRRXS n1 trap => + match o2 with + | OLoadRRRXS n2 trap2 => iandb (phys_eq n1 n2) (trapping_mode_eq trap trap2) + | _ => RET false + end + end. + +Lemma load_op_eq_correct o1 o2: + WHEN load_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. +Proof. + destruct o1, o2; wlp_simplify; try discriminate. + { f_equal. + destruct trap, trap0; simpl in *; trivial; discriminate. + pose (Ptrofs.eq_spec ofs ofs0). + rewrite H in *. trivial. } + all: destruct trap, trap0; simpl in *; trivial; discriminate. +Qed. +Hint Resolve load_op_eq_correct: wlp. +Opaque load_op_eq_correct. + +Definition store_op_eq (o1 o2: store_op): ?? bool := + match o1 with + | OStoreRRO n1 ofs1 => + match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (offset_eq ofs1 ofs2) | _ => RET false end + | OStoreRRR n1 => + match o2 with OStoreRRR n2 => phys_eq n1 n2 | _ => RET false end + | OStoreRRRXS n1 => + match o2 with OStoreRRRXS n2 => phys_eq n1 n2 | _ => RET false end + end. + +Lemma store_op_eq_correct o1 o2: + WHEN store_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. +Proof. + destruct o1, o2; wlp_simplify; try discriminate. + - f_equal. pose (Ptrofs.eq_spec ofs ofs0). + rewrite H in *. trivial. + - congruence. + - congruence. +Qed. +Hint Resolve store_op_eq_correct: wlp. +Opaque store_op_eq_correct. + +Definition control_op_eq (c1 c2: control_op): ?? bool := + match c1 with + | Oj_l l1 => + match c2 with Oj_l l2 => phys_eq l1 l2 | _ => RET false end + | Ocb bt1 l1 => + match c2 with Ocb bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end + | Ocbu bt1 l1 => + match c2 with Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end + | Ojumptable tbl1 => + match c2 with Ojumptable tbl2 => phys_eq tbl1 tbl2 | _ => RET false end + | Odiv => + match c2 with Odiv => RET true | _ => RET false end + | Odivu => + match c2 with Odivu => RET true | _ => RET false end + | OIncremPC sz1 => + match c2 with OIncremPC sz2 => RET (Z.eqb sz1 sz2) | _ => RET false end + | OError => + match c2 with OError => RET true | _ => RET false end + 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. +Qed. +Hint Resolve control_op_eq_correct: wlp. +Opaque control_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 + | 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 + | Control i1 => + match o2 with Control i2 => control_op_eq i1 i2 | _ => RET false end + | Allocframe sz1 pos1 => + match o2 with Allocframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Allocframe2 sz1 pos1 => + match o2 with Allocframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Freeframe sz1 pos1 => + match o2 with Freeframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Freeframe2 sz1 pos1 => + match o2 with Freeframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Constant c1 => + match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end + | Fail => + match o2 with Fail => RET true | _ => RET false end + end. + +Theorem op_eq_correct o1 o2: + WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. +Proof. + destruct o1, o2; wlp_simplify; try rewrite Z.eqb_eq in * |- ; try congruence. +Qed. +Hint Resolve op_eq_correct: wlp. +Global Opaque op_eq_correct. + +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 [Asmvliw] to [L] *) + +Local Open Scope positive_scope. + +Definition pmem : R.t := 1. + +Definition ireg_to_pos (ir: ireg) : R.t := + match ir with + | GPR0 => 1 | GPR1 => 2 | GPR2 => 3 | GPR3 => 4 | GPR4 => 5 | GPR5 => 6 | GPR6 => 7 | GPR7 => 8 | GPR8 => 9 | GPR9 => 10 + | GPR10 => 11 | GPR11 => 12 | GPR12 => 13 | GPR13 => 14 | GPR14 => 15 | GPR15 => 16 | GPR16 => 17 | GPR17 => 18 | GPR18 => 19 | GPR19 => 20 + | GPR20 => 21 | GPR21 => 22 | GPR22 => 23 | GPR23 => 24 | GPR24 => 25 | GPR25 => 26 | GPR26 => 27 | GPR27 => 28 | GPR28 => 29 | GPR29 => 30 + | GPR30 => 31 | GPR31 => 32 | GPR32 => 33 | GPR33 => 34 | GPR34 => 35 | GPR35 => 36 | GPR36 => 37 | GPR37 => 38 | GPR38 => 39 | GPR39 => 40 + | GPR40 => 41 | GPR41 => 42 | GPR42 => 43 | GPR43 => 44 | GPR44 => 45 | GPR45 => 46 | GPR46 => 47 | GPR47 => 48 | GPR48 => 49 | GPR49 => 50 + | GPR50 => 51 | GPR51 => 52 | GPR52 => 53 | GPR53 => 54 | GPR54 => 55 | GPR55 => 56 | GPR56 => 57 | GPR57 => 58 | GPR58 => 59 | GPR59 => 60 + | GPR60 => 61 | GPR61 => 62 | GPR62 => 63 | GPR63 => 64 + 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. + +Definition ppos (r: preg) : R.t := + match r with + | RA => 2 + | PC => 3 + | IR ir => 3 + ireg_to_pos ir + 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_discr: forall r r', r <> r' -> ppos r <> ppos r'. +Proof. + destruct r; destruct r'. + all: try discriminate; try contradiction. + - intros. apply not_eq_add. apply ireg_to_pos_discr. congruence. + - intros. unfold ppos. cutrewrite (3 + ireg_to_pos g = (1 + ireg_to_pos g) + 2). apply Pos.add_no_neutral. + apply eq_sym. rewrite Pos.add_comm. rewrite Pos.add_assoc. reflexivity. + - intros. unfold ppos. rewrite Pos.add_comm. apply Pos.add_no_neutral. + - intros. unfold ppos. apply not_eq_sym. + cutrewrite (3 + ireg_to_pos g = (1 + ireg_to_pos g) + 2). apply Pos.add_no_neutral. + apply eq_sym. rewrite Pos.add_comm. rewrite Pos.add_assoc. reflexivity. + - intros. unfold ppos. apply not_eq_sym. rewrite Pos.add_comm. apply Pos.add_no_neutral. +Qed. + +Lemma ppos_pmem_discr: forall r, pmem <> ppos r. +Proof. + intros. destruct r. + - unfold ppos. unfold pmem. apply not_eq_sym. rewrite Pos.add_comm. cutrewrite (3 = 2 + 1). rewrite Pos.add_assoc. apply Pos.add_no_neutral. + reflexivity. + - unfold ppos. unfold pmem. discriminate. + - unfold ppos. unfold pmem. discriminate. +Qed. + +(** Inversion functions, used for debug traces *) + +Definition pos_to_ireg (p: R.t) : option gpreg := + match p with + | 1 => Some GPR0 | 2 => Some GPR1 | 3 => Some GPR2 | 4 => Some GPR3 | 5 => Some GPR4 | 6 => Some GPR5 | 7 => Some GPR6 | 8 => Some GPR7 | 9 => Some GPR8 | 10 => Some GPR9 + | 11 => Some GPR10 | 12 => Some GPR11 | 13 => Some GPR12 | 14 => Some GPR13 | 15 => Some GPR14 | 16 => Some GPR15 | 17 => Some GPR16 | 18 => Some GPR17 | 19 => Some GPR18 | 20 => Some GPR19 + | 21 => Some GPR20 | 22 => Some GPR21 | 23 => Some GPR22 | 24 => Some GPR23 | 25 => Some GPR24 | 26 => Some GPR25 | 27 => Some GPR26 | 28 => Some GPR27 | 29 => Some GPR28 | 30 => Some GPR29 + | 31 => Some GPR30 | 32 => Some GPR31 | 33 => Some GPR32 | 34 => Some GPR33 | 35 => Some GPR34 | 36 => Some GPR35 | 37 => Some GPR36 | 38 => Some GPR37 | 39 => Some GPR38 | 40 => Some GPR39 + | 41 => Some GPR40 | 42 => Some GPR41 | 43 => Some GPR42 | 44 => Some GPR43 | 45 => Some GPR44 | 46 => Some GPR45 | 47 => Some GPR46 | 48 => Some GPR47 | 49 => Some GPR48 | 50 => Some GPR49 + | 51 => Some GPR50 | 52 => Some GPR51 | 53 => Some GPR52 | 54 => Some GPR53 | 55 => Some GPR54 | 56 => Some GPR55 | 57 => Some GPR56 | 58 => Some GPR57 | 59 => Some GPR58 | 60 => Some GPR59 + | 61 => Some GPR60 | 62 => Some GPR61 | 63 => Some GPR62 | 64 => Some GPR63 + | _ => None + end. + +Definition inv_ppos (p: R.t) : option preg := + match p with + | 1 => None + | 2 => Some RA | 3 => Some PC + | n => match pos_to_ireg (n-3) with + | None => None + | Some gpr => Some (IR gpr) + end + end. + +Notation "a @ b" := (Econs a b) (at level 102, right associativity). + +(** Translations of instructions *) + +Definition trans_control (ctl: control) : inst := + match ctl with + | Pret => [(#PC, PReg(#RA))] + | Pcall s => [(#RA, PReg(#PC)); (#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)] + | Picall r => [(#RA, PReg(#PC)); (#PC, PReg(#r))] + | Pgoto s => [(#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)] + | Pigoto r => [(#PC, PReg(#r))] + | Pj_l l => [(#PC, Op (Control (Oj_l l)) (PReg(#PC) @ Enil))] + | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (PReg(#r) @ PReg(#PC) @ Enil))] + | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (PReg(#r) @ PReg(#PC) @ Enil))] + | Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (PReg(#r) @ PReg(#PC) @ Enil)); + (#GPR62, Op (Constant Vundef) Enil); + (#GPR63, Op (Constant Vundef) Enil) ] + | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] + end. + +Definition trans_exit (ex: option control) : L.inst := + match ex with + | None => [] + | Some ctl => trans_control ctl + end +. + +Definition trans_arith (ai: ar_instruction) : inst := + match ai with + | PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)] + | PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))] + | PArithRI32 n d i => [(#d, Op (Arith (OArithRI32 n i)) Enil)] + | PArithRI64 n d i => [(#d, Op (Arith (OArithRI64 n i)) Enil)] + | PArithRF32 n d i => [(#d, Op (Arith (OArithRF32 n i)) Enil)] + | PArithRF64 n d i => [(#d, Op (Arith (OArithRF64 n i)) Enil)] + | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (PReg(#s1) @ PReg(#s2) @ Enil))] + | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (PReg(#s) @ Enil))] + | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (PReg(#s) @ Enil))] + | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (PReg(#d) @ PReg(#s1) @ PReg(#s2) @ Enil))] + | PArithARR n d s => [(#d, Op (Arith (OArithARR n)) (PReg(#d) @ PReg(#s) @ Enil))] + | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (PReg(#d) @ PReg(#s) @ Enil))] + | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (PReg(#d) @ PReg(#s) @ Enil))] + end. + + +Definition trans_basic (b: basic) : inst := + match b with + | PArith ai => trans_arith ai + | PLoadRRO trap n d a ofs => [(#d, Op (Load (OLoadRRO n trap ofs)) (PReg (#a) @ PReg pmem @ Enil))] + | PLoadRRR trap n d a ro => [(#d, Op (Load (OLoadRRR n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PLoadRRRXS trap n d a ro => [(#d, Op (Load (OLoadRRRXS n trap)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))] + | PLoadQRRO qd a ofs => + let (d0, d1) := gpreg_q_expand qd in + [(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil)); + (#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil))] + | PLoadORRO od a ofs => + match gpreg_o_expand od with + | (d0, d1, d2, d3) => + [(#d0, Op (Load (OLoadRRO Pld_a TRAP ofs)) (PReg (#a) @ PReg pmem @ Enil)); + (#d1, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); + (#d2, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 16)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); + (#d3, Op (Load (OLoadRRO Pld_a TRAP (Ptrofs.add ofs (Ptrofs.repr 24)))) (Old(PReg (#a)) @ PReg pmem @ Enil))] + end + | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PStoreQRRO qs a ofs => + let (s0, s1) := gpreg_q_expand qs in + [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))] + | PStoreORRO os a ofs => + match gpreg_o_expand os with + | (s0, s1, s2, s3) => + [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (PReg (#s2) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (PReg (#s3) @ PReg (#a) @ PReg pmem @ Enil))] + end + | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil); + (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))] + | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil)); + (#SP, Op (Freeframe2 sz pos) (PReg (#SP) @ Old (PReg pmem) @ Enil)); + (#RTMP, Op (Constant Vundef) Enil)] + | Pget rd ra => match ra with + | RA => [(#rd, PReg(#ra))] + | _ => [(#rd, Op Fail Enil)] + end + | Pset ra rd => match ra with + | RA => [(#ra, PReg(#rd))] + | _ => [(#rd, Op Fail Enil)] + end + | Pnop => [] + 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: Asmvliw.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: Asmvliw.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 + | Next rs m => exists s', s=Some s' /\ match_states (State rs m) s' + | Stuck => s=None + end. + +Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity). + +Definition trans_state (s: Asmvliw.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. + +(** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *) + +Module PChk := ParallelChecks L PosPseudoRegSet. + +Definition bblock_para_check (p: Asmvliw.bblock) : bool := + PChk.is_parallelizable (trans_block p). + +Section SECT_PAR. + +Import PChk. + +Ltac Simplif := + ((rewrite nextblock_inv by eauto with asmgen) + || (rewrite nextblock_inv1 by eauto with asmgen) + || (rewrite Pregmap.gss) + || (rewrite nextblock_pc) + || (rewrite Pregmap.gso by eauto with asmgen) + || (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); + try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto)) + || (rewrite assign_eq) + ); auto with asmgen. + +Ltac Simpl := repeat Simplif. + +Arguments Pos.add: simpl never. +Arguments ppos: simpl never. + +Variable Ge: genv. + +Lemma trans_arith_par_correct ge fn rsr mr sr rsw mw sw rsw' i: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_arith_instr ge i rsr rsw = rsw' -> + exists sw', + inst_prun Ge (trans_arith i) sw sr sr = Some sw' + /\ match_states (State rsw' mw) sw'. +Proof. + intros GENV MSR MSW PARARITH. subst. inv MSR. inv MSW. + unfold parexec_arith_instr. destruct i. +(* Ploadsymbol *) + - destruct i. eexists; split; [| split]. + * simpl. reflexivity. + * Simpl. + * simpl. intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRR *) + - eexists; split; [| split]. + * simpl. rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRI32 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRI64 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRF32 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRF64 *) + - eexists; split; [|split]. + * simpl. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRRR *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rs1). rewrite (H0 rs2). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRRI32 *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRRI64 *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRR *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs1). rewrite (H0 rs2). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARR *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRI32 *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithARRI64 *) + - eexists; split; [|split]. + * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +Qed. + + + +Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (bstep ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw 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 GENV MSR MSW; inversion MSR as (H & H0); inversion MSW as (H1 & H2). + destruct bi; simpl. +(* Arith *) + - exploit trans_arith_par_correct. 5: eauto. all: eauto. +(* Load *) + - destruct i. + (* Load Offset *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; + unfold eval_offset; + simpl; auto; + destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + + (* Load Reg *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_reg; simpl; unfold exec_load_deps_reg; rewrite H, H0; rewrite (H0 rofs); + destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + + (* Load Reg XS *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs); + destruct (Mem.loadv _ _ _) eqn:MEML; destruct trap; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + + (* Load Quad word *) + + unfold parexec_load_q_offset. + destruct (gpreg_q_expand rd) as [rd0 rd1]; destruct Ge; simpl. + rewrite H0, H. + destruct (Mem.loadv Many64 mr _) as [load0 | ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ]; simpl; auto. + eexists; intuition eauto. + { rewrite !(assign_diff _ _ pmem); auto. } + { preg_eq_discr r rd1. + preg_eq_discr r rd0. } + + (* Load Octuple word *) + + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core. + unfold parexec_load_o_offset. + destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]; destruct Ge; simpl. + rewrite H0, H. + destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) ofs)) as [load0 | ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), !H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), !H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 16)))) as [load2| ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), !H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 24)))) as [load3| ]; simpl; auto. + eexists; intuition eauto. + { rewrite !(assign_diff _ _ pmem); auto. } + { preg_eq_discr r rd3. + preg_eq_discr r rd2. + preg_eq_discr r rd1. + preg_eq_discr r rd0. } + +(* Store *) + - destruct i. + (* Store Offset *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra); + unfold eval_offset; simpl; auto; + destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl. + + (* Store Reg *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_reg; simpl; unfold exec_store_deps_reg; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs); + destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl. + + (* Store Reg XS *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_regxs; simpl; unfold exec_store_deps_regxs; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs); + destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl. + + (* Store Quad Word *) + + unfold parexec_store_q_offset. + destruct (gpreg_q_expand rs) as [s0 s1]; destruct Ge; simpl. + rewrite !H0, !H. + destruct (Mem.storev _ _ _ (rsr s0)) as [mem0 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s1)) as [mem1 | ]; simpl; auto. + eexists; intuition eauto. + rewrite !assign_diff; auto. + + (* Store Ocuple Word *) + + unfold parexec_store_o_offset. + destruct (gpreg_o_expand rs) as [[[s0 s1] s2] s3]; destruct Ge; simpl. + rewrite !H0, !H. + destruct (Mem.storev _ _ _ (rsr s0)) as [store0 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s1)) as [store1 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s2)) as [store2 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s3)) as [store3 | ]; simpl; auto. + eexists; intuition eauto. + rewrite !assign_diff; auto. + + (* Allocframe *) + - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. + * eexists; repeat split. + { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl. + rewrite H, MEMAL. rewrite MEMS. reflexivity. } + { Simpl. } + { intros rr; destruct rr; Simpl. + destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. } + * simpl; Simpl; erewrite !H0, H, MEMAL, MEMS; auto. + (* Freeframe *) + - erewrite !H0, H. + destruct (Mem.loadv _ _ _) eqn:MLOAD; simpl; auto. + destruct (rsr GPR12) eqn:SPeq; simpl; auto. + destruct (Mem.free _ _ _ _) eqn:MFREE; simpl; auto. + eexists; repeat split. + * simpl. Simpl. erewrite H0, SPeq, MLOAD, MFREE. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. +(* Pget *) + - destruct rs eqn:rseq; simpl; auto. + eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* Pset *) + - destruct rd eqn:rdeq; simpl; auto. + eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. +(* Pnop *) + - eexists. repeat split; assumption. +Qed. + + +Theorem bisimu_par_body: + forall bdy ge fn rsr mr sr rsw mw sw, + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (parexec_wio_body ge bdy rsr rsw mr mw) (prun_iw Ge (trans_body bdy) sw sr). +Proof. + induction bdy as [|i bdy]; simpl; eauto. + intros. + exploit (bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw i); eauto. + destruct (bstep _ _ _ _ _ _); simpl. + - intros (s' & X1 & X2). rewrite X1; simpl; eauto. + - intros X; rewrite X; simpl; auto. +Qed. + +Theorem bisimu_par_control ex sz aux ge fn rsr rsw mr mw sr sw: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) (rsw#PC <- aux) mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). +Proof. + intros GENV MSR MSW; unfold estep. + simpl in *. inv MSR. inv MSW. + destruct ex. + - destruct c; destruct i; try discriminate; simpl. + all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl). + + (* Pjumptable *) + + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold incrPC. Simpl. + destruct (rsr r); simpl; auto. destruct (list_nth_z _ _); simpl; auto. + unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. + eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. + destruct (preg_eq g GPR62). rewrite e. Simpl. + destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl. + + (* Pj_l *) + + rewrite (H0 PC). Simpl. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. + unfold incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. + eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. + + (* Pcb *) + + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmp_for_btest _); simpl; auto. destruct o; simpl; auto. + unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. + ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. + ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. + + (* Pcbu *) + + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto. + unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. + ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. + ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b. + +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. + destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. + intros rr; destruct rr; Simpl. + +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. + + - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl. + intros rr; destruct rr; unfold incrPC; Simpl. +Qed. + +Theorem bisimu_par_exit ex sz ge fn rsr rsw mr mw sr sw: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + match_outcome (estep ge fn ex (Ptrofs.repr sz) rsr rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). +Proof. + intros; unfold estep. + exploit (bisimu_par_control ex sz rsw#PC ge fn rsr rsw mr mw sr sw); eauto. + cutrewrite (rsw # PC <- (rsw PC) = rsw); auto. + apply extensionality. intros; destruct x; simpl; auto. +Qed. + +Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). + +Theorem bisimu_par_wio ge fn rsr mr sr bdy ex sz: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_outcome (parexec_wio ge fn bdy ex (Ptrofs.repr sz) rsr mr) (prun_iw Ge (trans_block_aux bdy sz ex) sr sr). +Proof. + intros GENV MSR. unfold parexec_wio, trans_block_aux. + exploit (bisimu_par_body bdy ge fn rsr mr sr rsr mr sr); eauto. + destruct (parexec_wio_body _ _ _ _ _ _); simpl. + - intros (s' & X1 & X2). + erewrite prun_iw_app_Some; eauto. + exploit (bisimu_par_exit ex sz ge fn rsr rs mr m sr s'); eauto. + subst Ge; simpl. destruct MSR as (Y1 & Y2). erewrite Y2; simpl. + destruct (inst_prun _ _ _ _ _); simpl; auto. + - intros X; erewrite prun_iw_app_None; eauto. +Qed. + +Theorem bisimu_par_wio_bblock ge fn rsr mr sr bdy1 bdy2 ex sz: + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_outcome + match parexec_wio ge fn bdy1 ex (Ptrofs.repr sz) rsr mr with + | Next rs' m' => parexec_wio_body ge bdy2 rsr rs' mr m' + | Stuck => Stuck + end + (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr). +Proof. + intros. + exploit (bisimu_par_wio ge fn rsr mr sr bdy1 ex sz); eauto. + destruct (parexec_wio _ _ _ _ _ _); simpl. + - intros (s' & X1 & X2). + erewrite prun_iw_app_Some; eauto. + eapply bisimu_par_body; eauto. + - intros; erewrite prun_iw_app_None; eauto. +Qed. + +Lemma trans_body_perserves_permutation bdy1 bdy2: + Permutation bdy1 bdy2 -> + Permutation (trans_body bdy1) (trans_body bdy2). +Proof. + induction 1; simpl; econstructor; eauto. +Qed. + +Lemma trans_body_app bdy1: forall bdy2, + trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2). +Proof. + induction bdy1; simpl; congruence. +Qed. + +Theorem trans_block_perserves_permutation bdy1 bdy2 b: + Permutation (bdy1 ++ bdy2) (body b) -> + Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)). +Proof. + intro H; unfold trans_block, trans_block_aux. + eapply perm_trans. + - eapply Permutation_app_tail. + apply trans_body_perserves_permutation. + apply Permutation_sym; eapply H. + - rewrite trans_body_app. rewrite <-! app_assoc. + apply Permutation_app_head. + apply Permutation_app_comm. +Qed. + +Theorem bisimu_par rs1 m1 s1' b ge fn o2: + Ge = Genv ge fn -> + match_states (State rs1 m1) s1' -> + parexec_bblock ge fn b rs1 m1 o2 -> + exists o2', + prun Ge (trans_block b) s1' o2' + /\ match_outcome o2 o2'. +Proof. + intros GENV MS PAREXEC. + inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO). + exploit trans_block_perserves_permutation; eauto. + intros Perm. + exploit (bisimu_par_wio_bblock ge fn rs1 m1 s1' bdy1 bdy2 (exit b) (size b)); eauto. + rewrite <- WIO. clear WIO. + intros H; eexists; split. 2: eapply H. + unfold prun; eexists; split; eauto. + destruct (prun_iw _ _ _ _); simpl; eauto. +Qed. + +(** sequential execution *) +Theorem bisimu_basic ge fn bi rs m s: + Ge = Genv ge fn -> + match_states (State rs m) s -> + match_outcome (exec_basic_instr ge bi rs m) (inst_run Ge (trans_basic bi) s s). +Proof. + intros; unfold exec_basic_instr. rewrite inst_run_prun. + eapply bisimu_par_wio_basic; eauto. +Qed. + +Lemma bisimu_body: + forall bdy ge fn rs m s, + Ge = Genv ge fn -> + match_states (State rs m) s -> + match_outcome (exec_body ge bdy rs m) (exec Ge (trans_body bdy) s). +Proof. + induction bdy as [|i bdy]; simpl; eauto. + intros. + exploit (bisimu_basic ge fn i rs m s); eauto. + destruct (exec_basic_instr _ _ _ _); simpl. + - intros (s' & X1 & X2). rewrite X1; simpl; eauto. + - intros X; rewrite X; simpl; auto. +Qed. + +Theorem bisimu_exit ge fn b rs m s: + Ge = Genv ge fn -> + match_states (State rs m) s -> + match_outcome (exec_control ge fn (exit b) (nextblock b rs) m) (inst_run Ge (trans_pcincr (size b) (trans_exit (exit b))) s s). +Proof. + intros; unfold exec_control, nextblock. rewrite inst_run_prun. + apply (bisimu_par_control (exit b) (size b) (Val.offset_ptr (rs PC) (Ptrofs.repr (size b))) ge fn rs rs m m s s); auto. +Qed. + +Theorem bisimu rs m b ge fn s: + Ge = Genv ge fn -> + match_states (State rs m) s -> + match_outcome (exec_bblock ge fn b rs m) (exec Ge (trans_block b) s). +Proof. + intros GENV MS. unfold exec_bblock. + exploit (bisimu_body (body b) ge fn rs m s); eauto. + unfold exec, trans_block; simpl. + destruct (exec_body _ _ _ _); simpl. + - intros (s' & X1 & X2). + erewrite run_app_Some; eauto. + exploit (bisimu_exit ge fn b rs0 m0 s'); eauto. + subst Ge; simpl. destruct X2 as (Y1 & Y2). erewrite Y2; 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; try reflexivity. + destruct g; 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. + +Lemma bblock_para_check_correct ge fn bb rs m rs' m': + Ge = Genv ge fn -> + exec_bblock ge fn bb rs m = Next rs' m' -> + bblock_para_check bb = true -> + det_parexec ge fn bb rs m rs' m'. +Proof. + intros H H0 H1 o H2. unfold bblock_para_check in H1. + exploit (bisimu rs m bb ge fn); eauto. eapply trans_state_match. + rewrite H0; simpl. + intros (s2' & EXEC & MS). + exploit bisimu_par. 2: apply (trans_state_match (State rs m)). all: eauto. + intros (o2' & PRUN & MO). + exploit parallelizable_correct. apply is_para_correct_aux. eassumption. + intro. eapply H3 in PRUN. clear H3. destruct o2'. + - inv PRUN. inv H3. unfold exec in EXEC; unfold trans_state in H. + assert (x = s2') by congruence. subst. clear H. + assert (m0 = s2') by (apply functional_extensionality; auto). subst. clear H4. + destruct o; try discriminate. inv MO. inv H. assert (s2' = x) by congruence. subst. + exploit (state_equiv (State rs' m') (State rs0 m0)). + 2: eapply H4. eapply MS. intro H. inv H. reflexivity. + - unfold match_outcome in MO. destruct o. + + inv MO. inv H3. discriminate. + + clear MO. unfold exec in EXEC. + unfold trans_state in PRUN; rewrite EXEC in PRUN. discriminate. +Qed. + +End SECT_PAR. + +Section SECT_BBLOCK_EQUIV. + +Variable Ge: genv. + +Local Hint Resolve trans_state_match: core. + +Lemma bblock_simu_reduce: + forall p1 p2 ge fn, + Ge = Genv ge fn -> + L.bblock_simu Ge (trans_block p1) (trans_block p2) -> + Asmblockprops.bblock_simu ge fn p1 p2. +Proof. + unfold bblock_simu, res_eq; intros p1 p2 ge fn H1 H2 rs m DONTSTUCK. + generalize (H2 (trans_state (State rs m))); clear H2. + intro H2. + exploit (bisimu Ge rs m p1 ge fn (trans_state (State rs m))); eauto. + exploit (bisimu Ge rs m p2 ge fn (trans_state (State rs m))); eauto. + destruct (exec_bblock ge fn p1 rs m); try congruence. + intros H3 (s2' & exp2 & MS'). unfold exec in exp2, H3. rewrite exp2 in H2. + destruct H2 as (m2' & H2 & H4). discriminate. rewrite H2 in H3. + destruct (exec_bblock ge fn p2 rs m); simpl in H3. + * destruct H3 as (s' & H3 & H5 & H6). inv H3. inv MS'. + cutrewrite (rs0=rs1). + - cutrewrite (m0=m1); auto. congruence. + - apply functional_extensionality. intros r. + generalize (H0 r). intros Hr. congruence. + * discriminate. +Qed. + +(** Used for debug traces *) + +Definition gpreg_name (gpr: gpreg) := + match gpr with + | GPR0 => Str ("GPR0") | GPR1 => Str ("GPR1") | GPR2 => Str ("GPR2") | GPR3 => Str ("GPR3") | GPR4 => Str ("GPR4") + | GPR5 => Str ("GPR5") | GPR6 => Str ("GPR6") | GPR7 => Str ("GPR7") | GPR8 => Str ("GPR8") | GPR9 => Str ("GPR9") + | GPR10 => Str ("GPR10") | GPR11 => Str ("GPR11") | GPR12 => Str ("GPR12") | GPR13 => Str ("GPR13") | GPR14 => Str ("GPR14") + | GPR15 => Str ("GPR15") | GPR16 => Str ("GPR16") | GPR17 => Str ("GPR17") | GPR18 => Str ("GPR18") | GPR19 => Str ("GPR19") + | GPR20 => Str ("GPR20") | GPR21 => Str ("GPR21") | GPR22 => Str ("GPR22") | GPR23 => Str ("GPR23") | GPR24 => Str ("GPR24") + | GPR25 => Str ("GPR25") | GPR26 => Str ("GPR26") | GPR27 => Str ("GPR27") | GPR28 => Str ("GPR28") | GPR29 => Str ("GPR29") + | GPR30 => Str ("GPR30") | GPR31 => Str ("GPR31") | GPR32 => Str ("GPR32") | GPR33 => Str ("GPR33") | GPR34 => Str ("GPR34") + | GPR35 => Str ("GPR35") | GPR36 => Str ("GPR36") | GPR37 => Str ("GPR37") | GPR38 => Str ("GPR38") | GPR39 => Str ("GPR39") + | GPR40 => Str ("GPR40") | GPR41 => Str ("GPR41") | GPR42 => Str ("GPR42") | GPR43 => Str ("GPR43") | GPR44 => Str ("GPR44") + | GPR45 => Str ("GPR45") | GPR46 => Str ("GPR46") | GPR47 => Str ("GPR47") | GPR48 => Str ("GPR48") | GPR49 => Str ("GPR49") + | GPR50 => Str ("GPR50") | GPR51 => Str ("GPR51") | GPR52 => Str ("GPR52") | GPR53 => Str ("GPR53") | GPR54 => Str ("GPR54") + | GPR55 => Str ("GPR55") | GPR56 => Str ("GPR56") | GPR57 => Str ("GPR57") | GPR58 => Str ("GPR58") | GPR59 => Str ("GPR59") + | GPR60 => Str ("GPR60") | GPR61 => Str ("GPR61") | GPR62 => Str ("GPR62") | GPR63 => Str ("GPR63") + 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 RA => RET (Str ("RA")) + | Some PC => RET (Str ("PC")) + | Some (IR gpr) => RET (gpreg_name gpr) + | _ => RET (Str ("UNDEFINED")) + end. + +Definition string_of_name_r (n: arith_name_r): pstring := + match n with + | Ploadsymbol _ _ => "Ploadsymbol" + end. + +Definition string_of_name_rr (n: arith_name_rr): pstring := + match n with + Pmv => "Pmv" + | Pnegw => "Pnegw" + | Pnegl => "Pnegl" + | Pcvtl2w => "Pcvtl2w" + | Psxwd => "Psxwd" + | Pzxwd => "Pzxwd" + | Pextfz _ _ => "Pextfz" + | Pextfs _ _ => "Pextfs" + | Pextfzl _ _ => "Pextfzl" + | Pextfsl _ _ => "Pextfsl" + | Pfabsd => "Pfabsd" + | Pfabsw => "Pfabsw" + | Pfnegd => "Pfnegd" + | Pfnegw => "Pfnegw" + | Pfinvw => "Pfinvw" + | Pfnarrowdw => "Pfnarrowdw" + | Pfwidenlwd => "Pfwidenlwd" + | Pfloatwrnsz => "Pfloatwrnsz" + | Pfloatuwrnsz => "Pfloatuwrnsz" + | Pfloatudrnsz => "Pfloatudrnsz" + | Pfloatdrnsz => "Pfloatdrnsz" + | Pfixedwrzz => "Pfixedwrzz" + | Pfixeduwrzz => "Pfixeduwrzz" + | Pfixeddrzz => "Pfixeddrzz" + | Pfixedudrzz => "Pfixedudrzz" + | Pfixeddrzz_i32 => "Pfixeddrzz_i32" + | Pfixedudrzz_i32 => "Pfixedudrzz_i32" + end. + +Definition string_of_name_ri32 (n: arith_name_ri32): pstring := + match n with + | Pmake => "Pmake" + end. + +Definition string_of_name_ri64 (n: arith_name_ri64): pstring := + match n with + | Pmakel => "Pmakel" + end. + +Definition string_of_name_rf32 (n: arith_name_rf32): pstring := + match n with + | Pmakefs => "Pmakefs" + end. + +Definition string_of_name_rf64 (n: arith_name_rf64): pstring := + match n with + | Pmakef => "Pmakef" + end. + +Definition string_of_name_rrr (n: arith_name_rrr): pstring := + match n with + | Pcompw _ => "Pcompw" + | Pcompl _ => "Pcompl" + | Pfcompw _ => "Pfcompw" + | Pfcompl _ => "Pfcompl" + | Paddw => "Paddw" + | Paddxw _ => "Paddxw" + | Psubw => "Psubw" + | Prevsubxw _ => "Prevsubxw" + | Pmulw => "Pmulw" + | Pandw => "Pandw" + | Pnandw => "Pnandw" + | Porw => "Porw" + | Pnorw => "Pnorw" + | Pxorw => "Pxorw" + | Pnxorw => "Pnxorw" + | Pandnw => "Pandnw" + | Pornw => "Pornw" + | Psraw => "Psraw" + | Psrlw => "Psrlw" + | Psrxw => "Psrxw" + | Psllw => "Psllw" + | Paddl => "Paddl" + | Paddxl _ => "Paddxl" + | Psubl => "Psubl" + | Prevsubxl _ => "Prevsubxl" + | Pandl => "Pandl" + | Pnandl => "Pnandl" + | Porl => "Porl" + | Pnorl => "Pnorl" + | Pxorl => "Pxorl" + | Pnxorl => "Pnxorl" + | Pandnl => "Pandnl" + | Pornl => "Pornl" + | Pmull => "Pmull" + | Pslll => "Pslll" + | Psrll => "Psrll" + | Psrxl => "Psrxl" + | Psral => "Psral" + | Pfaddd => "Pfaddd" + | Pfaddw => "Pfaddw" + | Pfsbfd => "Pfsbfd" + | Pfsbfw => "Pfsbfw" + | Pfmuld => "Pfmuld" + | Pfmulw => "Pfmulw" + | Pfmind => "Pfmind" + | Pfminw => "Pfminw" + | Pfmaxd => "Pfmaxd" + | Pfmaxw => "Pfmaxw" + end. + +Definition string_of_name_rri32 (n: arith_name_rri32): pstring := + match n with + Pcompiw _ => "Pcompiw" + | Paddiw => "Paddiw" + | Paddxiw _ => "Paddxiw" + | Prevsubiw => "Prevsubiw" + | Prevsubxiw _ => "Prevsubxiw" + | Pmuliw => "Pmuliw" + | Pandiw => "Pandiw" + | Pnandiw => "Pnandiw" + | Poriw => "Poriw" + | Pnoriw => "Pnoriw" + | Pxoriw => "Pxoriw" + | Pnxoriw => "Pnxoriw" + | Pandniw => "Pandniw" + | Porniw => "Porniw" + | Psraiw => "Psraiw" + | Psrliw => "Psrliw" + | Psrxiw => "Psrxiw" + | Pslliw => "Pslliw" + | Proriw => "Proriw" + | Psllil => "Psllil" + | Psrlil => "Psrlil" + | Psrail => "Psrail" + | Psrxil => "Psrxil" + end. + +Definition string_of_name_rri64 (n: arith_name_rri64): pstring := + match n with + Pcompil _ => "Pcompil" + | Paddil => "Paddil" + | Prevsubil => "Prevsubil" + | Paddxil _ => "Paddxil" + | Prevsubxil _ => "Prevsubxil" + | Pmulil => "Pmulil" + | Pandil => "Pandil" + | Pnandil => "Pnandil" + | Poril => "Poril" + | Pnoril => "Pnoril" + | Pxoril => "Pxoril" + | Pnxoril => "Pnxoril" + | Pandnil => "Pandnil" + | Pornil => "Pornil" + end. + +Definition string_of_name_arrr (n: arith_name_arrr): pstring := + match n with + | Pmaddw => "Pmaddw" + | Pmaddl => "Pmaddl" + | Pmsubw => "Pmsubw" + | Pmsubl => "Pmsubl" + | Pcmove _ => "Pcmove" + | Pcmoveu _ => "Pcmoveu" + | Pfmaddfw => "Pfmaddfw" + | Pfmaddfl => "Pfmaddfl" + | Pfmsubfw => "Pfmsubfw" + | Pfmsubfl => "Pfmsubfl" + end. + +Definition string_of_name_arr (n: arith_name_arr): pstring := + match n with + | Pinsf _ _ => "Pinsf" + | Pinsfl _ _ => "Pinsfl" + end. + +Definition string_of_name_arri32 (n: arith_name_arri32): pstring := + match n with + | Pmaddiw => "Pmaddw" + | Pcmoveiw _ => "Pcmoveiw" + | Pcmoveuiw _ => "Pcmoveuiw" + end. + +Definition string_of_name_arri64 (n: arith_name_arri64): pstring := + match n with + | Pmaddil => "Pmaddl" + | Pcmoveil _ => "Pcmoveil" + | Pcmoveuil _ => "Pcmoveuil" + end. + +Definition string_of_arith (op: arith_op): pstring := + match op with + | OArithR n => string_of_name_r n + | OArithRR n => string_of_name_rr n + | OArithRI32 n _ => string_of_name_ri32 n + | OArithRI64 n _ => string_of_name_ri64 n + | OArithRF32 n _ => string_of_name_rf32 n + | OArithRF64 n _ => string_of_name_rf64 n + | OArithRRR n => string_of_name_rrr n + | OArithRRI32 n _ => string_of_name_rri32 n + | OArithRRI64 n _ => string_of_name_rri64 n + | OArithARRR n => string_of_name_arrr n + | OArithARR n => string_of_name_arr n + | OArithARRI32 n _ => string_of_name_arri32 n + | OArithARRI64 n _ => string_of_name_arri64 n + end. + +Definition string_of_load_name (n: load_name) : pstring := + match n with + Plb => "Plb" + | Plbu => "Plbu" + | Plh => "Plh" + | Plhu => "Plhu" + | Plw => "Plw" + | Plw_a => "Plw_a" + | Pld => "Pld" + | Pld_a => "Pld_a" + | Pfls => "Pfls" + | Pfld => "Pfld" + end. + +Definition string_of_load (op: load_op): pstring := + match op with + | OLoadRRO n _ _ => string_of_load_name n + | OLoadRRR n _ => string_of_load_name n + | OLoadRRRXS n _ => string_of_load_name n + end. + +Definition string_of_store_name (n: store_name) : pstring := + match n with + Psb => "Psb" + | Psh => "Psh" + | Psw => "Psw" + | Psw_a => "Psw_a" + | Psd => "Psd" + | Psd_a => "Psd_a" + | Pfss => "Pfss" + | Pfsd => "Pfsd" + end. + +Definition string_of_store (op: store_op) : pstring := + match op with + | OStoreRRO n _ => string_of_store_name n + | OStoreRRR n => string_of_store_name n + | OStoreRRRXS n => string_of_store_name n + end. + +Definition string_of_control (op: control_op) : pstring := + match op with + | Oj_l _ => "Oj_l" + | Ocb _ _ => "Ocb" + | Ocbu _ _ => "Ocbu" + | Odiv => "Odiv" + | Odivu => "Odivu" + | Ojumptable _ => "Ojumptable" + | OError => "OError" + | OIncremPC _ => "OIncremPC" + end. + +Definition string_of_op (op: P.op): ?? pstring := + match op with + | Arith op => RET (string_of_arith op) + | Load op => RET (string_of_load op) + | Store op => RET (string_of_store op) + | Control op => RET (string_of_control op) + | Allocframe _ _ => RET (Str "Allocframe") + | Allocframe2 _ _ => RET (Str "Allocframe2") + | Freeframe _ _ => RET (Str "Freeframe") + | Freeframe2 _ _ => RET (Str "Freeframe2") + | Constant _ => RET (Str "Constant") + | Fail => RET (Str "Fail") + end. + +End SECT_BBLOCK_EQUIV. + +(** REWRITE RULES *) + +Definition is_constant (o: op): bool := + match o with + | Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => 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 ao; simpl in * |- *; try congruence; + destruct n; simpl in * |- *; try congruence; + unfold arith_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: Asmvliw.bblock) : ?? bool := + 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 bblock_simu_reduce 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, Asmblockprops.bblock_simu ge fn p1 p2. +Proof. + wlp_simplify. +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: Asmvliw.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 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu 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: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true. + +Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2. +Proof. + eapply (pure_bblock_simu_test_correct true). +Qed.*) -- cgit