From 49d95f40a205eb0075537c1e4351556c8e6302dd Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Fri, 17 Apr 2020 05:18:41 -0700 Subject: [PATCH] [sledge sem] Adds a theorem about block processing order Summary: Show that the SSA restrictions imply that the blocks can be topologically sorted so that any use of a variable follows its definition in the list of blocks. This showed a slight flaw in my definition of SSA form. It used to treat program counters up to equality. However, PCs that point to a block header contain the location that control came from (so that the Phi instructions can be executed), but the SSA restrictions shouldn't pay attention to that, so now the definition of SSA introduces a equivalence on PCs that ignores that additional information. Reviewed By: jberdine Differential Revision: D21066873 fbshipit-source-id: 735575a1f --- sledge/semantics/llvmScript.sml | 8 +- sledge/semantics/llvm_ssaScript.sml | 1142 ++++++++++++++++- sledge/semantics/llvm_to_llair_propScript.sml | 12 +- .../llvm_to_llair_sem_propScript.sml | 17 +- sledge/semantics/miscScript.sml | 61 +- 5 files changed, 1177 insertions(+), 63 deletions(-) diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml index 176db21b0..b76e07d0c 100644 --- a/sledge/semantics/llvmScript.sml +++ b/sledge/semantics/llvmScript.sml @@ -830,15 +830,15 @@ Definition prog_ok_def: alookup p fname = Some dec ⇒ every (\b. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ∧ ((* The blocks in a definition have distinct labels.*) - ∀fname dec. - alookup p fname = Some dec ⇒ - all_distinct (map fst dec.blocks)) ∧ + every (\(fname,dec). all_distinct (map fst dec.blocks)) p) ∧ (* There is a main function *) (∃dec. alookup p (Fn "main") = Some dec) ∧ (* No phi instruction assigns the same register twice *) (∀ip from_l phis. get_instr p ip (Inr (from_l, phis)) ⇒ - all_distinct (map (λp. case p of Phi r _ _ => r) phis)) + all_distinct (map (λp. case p of Phi r _ _ => r) phis)) ∧ + (* No duplicate function names *) + (all_distinct (map fst p)) End (* All call frames have a good return address, and the stack allocations of the diff --git a/sledge/semantics/llvm_ssaScript.sml b/sledge/semantics/llvm_ssaScript.sml index 5803018ed..c45c9b7a7 100644 --- a/sledge/semantics/llvm_ssaScript.sml +++ b/sledge/semantics/llvm_ssaScript.sml @@ -10,12 +10,28 @@ open HolKernel boolLib bossLib Parse; open pred_setTheory listTheory rich_listTheory pairTheory arithmeticTheory; +open alistTheory set_relationTheory; open settingsTheory miscTheory llvmTheory llvm_propTheory; new_theory "llvm_ssa"; numLib.prefer_num (); +(* ----- The syntactic things we need to know about a program, just for this file ---- *) + +Definition loc_prog_ok_def: + loc_prog_ok p ⇔ + (∀fname dec bname block. + alookup p fname = Some dec ∧ + alookup dec.blocks bname = Some block ⇒ + block.body ≠ [] ∧ terminator (last block.body) ∧ + every (λi. ~terminator i) (front block.body)) ∧ + (∀fname dec. + alookup p fname = Some dec ⇒ + every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ∧ + (every (\(fname, dec). all_distinct (map fst dec.blocks)) p) +End + (* ----- Static paths through a program ----- *) Definition inc_pc_def: @@ -250,9 +266,17 @@ Definition entry_ip_def: entry_ip fname = <| f := fname; b := None; i := Offset 0 |> End +(* Equivalent instruction pointers, since we don't want to distinguish pointers + * to headers that have different from labels *) +Definition ip_equiv_def: + ip_equiv ip1 ip2 ⇔ + ip1.f = ip2.f ∧ ip1.b = ip2.b ∧ + (ip1.i ≠ ip2.i ⇒ ∃l1 l2. ip1.i = Phi_ip l1 ∧ ip2.i = Phi_ip l2) +End + Definition reachable_def: reachable prog ip ⇔ - ∃path. good_path prog (entry_ip ip.f :: path) ∧ last (entry_ip ip.f :: path) = ip + ∃path. good_path prog (entry_ip ip.f :: path) ∧ ip_equiv (last (entry_ip ip.f :: path)) ip End (* To get to ip2 from the entry, you must go through ip1 *) @@ -260,8 +284,8 @@ Definition dominates_def: dominates prog ip1 ip2 ⇔ ∀path. good_path prog (entry_ip ip2.f :: path) ∧ - last (entry_ip ip2.f :: path) = ip2 ⇒ - mem ip1 (front (entry_ip ip2.f :: path)) + ip_equiv (last (entry_ip ip2.f :: path)) ip2 ⇒ + ∃ip1'. ip_equiv ip1 ip1' ∧ mem ip1' (front (entry_ip ip2.f :: path)) End Definition is_ssa_def: @@ -273,12 +297,94 @@ Definition is_ssa_def: r ∈ image fst (assigns prog ip1) ∧ r ∈ image fst (assigns prog ip2) ∧ ip1.f = fname ∧ ip2.f = fname ⇒ - ip1 = ip2)) ∧ + ip_equiv ip1 ip2)) ∧ (* Each use is dominated by its assignment *) (∀ip1 r. r ∈ uses prog ip1 ⇒ - ∃ip2. ip2.f = ip1.f ∧ r ∈ image fst (assigns prog ip2) ∧ dominates prog ip2 ip1) + ∃ip2. ip2.f = ip1.f ∧ r ∈ image fst (assigns prog ip2) ∧ dominates prog ip2 ip1) ∧ + (* All of the blocks are reachable. Otherwise, we could have dead code that + * violates SSA, and this will wreck our treatment of a function body as a + * list of blocks in dominator tree order *) + (∀ip i. get_instr prog ip i ⇒ reachable prog ip) End +Theorem ip_equiv_sym: + ∀ip1 ip2. ip_equiv ip1 ip2 ⇔ ip_equiv ip2 ip1 +Proof + rw [ip_equiv_def] >> metis_tac [] +QED + +Theorem ip_equiv_refl: + ∀ip. ip_equiv ip ip +Proof + rw [ip_equiv_def] +QED + +Theorem ip_equiv_trans: + ∀ip1 ip2 ip3. ip_equiv ip1 ip2 ∧ ip_equiv ip2 ip3 ⇒ ip_equiv ip1 ip3 +Proof + rw [ip_equiv_def] >> metis_tac [] +QED + +Theorem ip_equiv_assigns: + ∀prog ip1 ip2 rt. + ip_equiv ip1 ip2 ∧ rt ∈ assigns prog ip1 ⇒ rt ∈ assigns prog ip2 +Proof + rw [ip_equiv_def, assigns_cases, IN_DEF] >> + Cases_on `ip1 = ip2` >> rw [] + >- metis_tac [] + >- (fs [pc_component_equality] >> fs [get_instr_cases] >> fs []) + >- metis_tac [] + >- ( + fs [pc_component_equality] >> + fs [get_instr_cases, inc_pc_def, inc_bip_def, PULL_EXISTS] >> + rw [] >> rfs [inc_bip_def] >> + metis_tac [optionTheory.SOME_11]) +QED + +Theorem ip_equiv_next: + ∀prog ip1 ip2 ip3. + ip_equiv ip1 ip2 ∧ ip3 ∈ next_ips prog ip1 ⇒ + ip3 ∈ next_ips prog ip2 +Proof + rw [ip_equiv_def, next_ips_cases, IN_DEF] >> + Cases_on `ip1 = ip2` >> rw [] + >- metis_tac [] + >- (fs [pc_component_equality] >> fs [get_instr_cases] >> fs []) + >- metis_tac [] + >- ( + fs [pc_component_equality] >> + fs [get_instr_cases, inc_pc_def, inc_bip_def, PULL_EXISTS] >> + rw [] >> rfs [inc_bip_def] >> + metis_tac [optionTheory.SOME_11]) +QED + +Theorem ip_equiv_dominates: + ∀prog ip1 ip2 ip3. + dominates prog ip1 ip2 ∧ ip_equiv ip2 ip3 ⇒ dominates prog ip1 ip3 +Proof + rw [dominates_def] >> metis_tac [ip_equiv_def] +QED + +Theorem ip_equiv_dominates2: + ∀prog ip1 ip2 ip3. + dominates prog ip1 ip2 ∧ ip_equiv ip1 ip3 ⇒ dominates prog ip3 ip2 +Proof + rw [dominates_def] >> metis_tac [ip_equiv_def] +QED + +Theorem ip_equiv_next_ips: + ∀p i ip1 ip2. ip_equiv ip1 ip2 ∧ i ∈ next_ips p ip1 ⇒ i ∈ next_ips p ip2 +Proof + rw [ip_equiv_def] >> + Cases_on `ip1.i = ip2.i` + >- metis_tac [pc_component_equality] >> + fs [] >> rw [] >> rfs [] >> + fs [next_ips_cases, IN_DEF, inc_pc_def, inc_bip_def] >> + fs [get_instr_cases] >> rw [] >> fs [] >> + rw [pc_component_equality, PULL_EXISTS] >> + rfs [] >> rw [] >> fs [inc_bip_def] +QED + Theorem dominates_trans: ∀prog ip1 ip2 ip3. dominates prog ip1 ip2 ∧ dominates prog ip2 ip3 ⇒ dominates prog ip1 ip3 @@ -289,24 +395,33 @@ Proof qpat_x_assum `mem _ (front _)` mp_tac >> simp [Once MEM_EL] >> rw [] >> fs [EL_FRONT] >> first_x_assum (qspec_then `take n path` mp_tac) >> simp [LAST_DEF] >> + simp [Once ip_equiv_sym] >> rw [] >> fs [entry_ip_def] - >- (fs [Once good_path_cases] >> rw [] >> fs [next_ips_cases, IN_DEF]) >> + >- ( + fs [Once good_path_cases, ip_equiv_def] >> rw [] >> + fs [next_ips_cases, IN_DEF] >> metis_tac []) + >- ( + fs [Once good_path_cases, ip_equiv_def] >> rw [] >> + fs [next_ips_cases, IN_DEF] >> metis_tac []) >> rfs [EL_CONS] >> `?m. n = Suc m` by (Cases_on `n` >> rw []) >> rw [] >> rfs [] >> - `(el m path).f = ip3.f` + `(el m path).f = (last (<|f := ip3.f; b := None; i := Offset 0|> ::path)).f` by ( irule good_path_same_func >> qexists_tac `<| f:= ip3.f; b := NONE; i := Offset 0|> :: path` >> qexists_tac `prog` >> conj_tac >- rw [EL_MEM] >> metis_tac [MEM_LAST]) >> + `(el m path).f = ip3.f` by metis_tac [ip_equiv_def] >> fs [] >> qpat_x_assum `_ ⇒ _` mp_tac >> impl_tac >- ( irule good_path_prefix >> HINT_EXISTS_TAC >> rw [] >> - metis_tac [take_is_prefix]) >> - rw [] >> drule MEM_FRONT >> rw [] >> + metis_tac [take_is_prefix, ip_equiv_def]) >> + rw [] >> drule MEM_FRONT >> rw [] + >- (qexists_tac `<|f := ip3.f; b := None; i := Offset 0|>` >> fs [ip_equiv_def]) >> fs [MEM_EL, LENGTH_FRONT] >> rfs [EL_TAKE] >> rw [] >> + HINT_EXISTS_TAC >> rw [] >> disj2_tac >> qexists_tac `n'` >> rw [] >> irule (GSYM EL_FRONT) >> rw [NULL_EQ, LENGTH_FRONT] @@ -323,59 +438,68 @@ Theorem dominates_antisym_lem: ∀prog ip1 ip2. dominates prog ip1 ip2 ∧ dominates prog ip2 ip1 ⇒ ¬reachable prog ip1 Proof rw [dominates_def, reachable_def] >> CCONTR_TAC >> fs [] >> - Cases_on `ip1 = entry_ip ip1.f` >> fs [] + Cases_on `ip_equiv ip1 (entry_ip ip1.f)` >> fs [] >- ( first_x_assum (qspec_then `[]` mp_tac) >> rw [] >> fs [Once good_path_cases, IN_DEF, next_ips_cases] >> - metis_tac []) >> - `path ≠ []` by (Cases_on `path` >> fs []) >> - `(OLEAST n. n < length path ∧ el n path = ip1) ≠ None` + metis_tac [ip_equiv_sym]) >> + `path ≠ []` by (Cases_on `path` >> fs [] >> metis_tac [ip_equiv_sym]) >> + `(OLEAST n. n < length path ∧ ip_equiv (el n path) ip1) ≠ None` by ( rw [whileTheory.OLEAST_EQ_NONE] >> qexists_tac `PRE (length path)` >> rw [] >> fs [LAST_DEF, LAST_EL] >> Cases_on `path` >> fs []) >> - qabbrev_tac `path1 = splitAtPki (\n ip. ip = ip1) (\x y. x) path` >> - first_x_assum (qspec_then `path1 ++ [ip1]` mp_tac) >> + qabbrev_tac `path1 = splitAtPki (\n ip. ip_equiv ip ip1) (\x y. x++[HD y]) path` >> + first_x_assum (qspec_then `path1` mp_tac) >> simp [] >> + `IS_PREFIX path path1` + by ( + unabbrev_all_tac >> rw [splitAtPki_EQN] >> + CASE_TAC >> rw [] >> + fs [whileTheory.OLEAST_EQ_SOME] >> + rw [GSYM SNOC_APPEND, SNOC_EL_TAKE, HD_DROP] >> + metis_tac [take_is_prefix]) >> conj_asm1_tac >> rw [] + >- (irule good_path_prefix >> HINT_EXISTS_TAC >> rw []) >- ( - irule good_path_prefix >> - HINT_EXISTS_TAC >> rw [] >> unabbrev_all_tac >> rw [splitAtPki_EQN] >> CASE_TAC >> rw [] >> fs [whileTheory.OLEAST_EQ_SOME] >> - rw [GSYM SNOC_APPEND, SNOC_EL_TAKE] >> - metis_tac [take_is_prefix]) - >- rw [LAST_DEF] >> + rw [LAST_DEF, HD_DROP]) >> + `path1 ≠ []` + by (fs [Abbr `path1`, splitAtPki_EQN] >> CASE_TAC >> rw []) >> simp [GSYM SNOC_APPEND, FRONT_SNOC, FRONT_DEF] >> CCONTR_TAC >> fs [MEM_EL] >- ( first_x_assum (qspec_then `[]` mp_tac) >> fs [entry_ip_def, Once good_path_cases, IN_DEF, next_ips_cases] >> + fs [ip_equiv_def] >> metis_tac []) >> - rw [] >> - rename [`n1 < length _`, `last _ = el n path`] >> + rw [] >> rfs [] >> + rename [`n1 < length (front _)`, `ip_equiv (el n _) _`, + `ip_equiv _ (el n1 (front _))`] >> first_x_assum (qspec_then `take (Suc n1) path1` mp_tac) >> rw [] >- ( irule good_path_prefix >> HINT_EXISTS_TAC >> rw [entry_ip_def] >- ( + `(el n1 (front path1)).f = (entry_ip ip1.f).f` suffices_by fs [ip_equiv_def, entry_ip_def] >> irule good_path_same_func >> - qexists_tac `entry_ip (el n path).f::(path1 ++ [el n path])` >> - qexists_tac `prog` >> rw [EL_MEM]) >> + qexists_tac `entry_ip ip1.f::path1` >> + qexists_tac `prog` >> rw [EL_MEM, entry_ip_def] >> + rw [MEM_EL] >> disj2_tac >> + qexists_tac `n1` >> rw [] >> rfs [LENGTH_FRONT] >> + irule EL_FRONT >> rw [NULL_EQ, LENGTH_FRONT]) >> metis_tac [IS_PREFIX_APPEND3, take_is_prefix, IS_PREFIX_TRANS]) - >- (rw [LAST_DEF] >> fs []) >> + >- ( + rfs [LENGTH_FRONT] >> rw [LAST_DEF] >> + metis_tac [EL_FRONT, NULL_EQ, ip_equiv_sym, LENGTH_FRONT]) >> rw [METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >> simp [EL_FRONT] >> + rfs [LENGTH_TAKE, LENGTH_FRONT] >> rename [`n2 < Suc _`] >> Cases_on `¬(0 < n2)` >> rw [EL_CONS] - >- ( - fs [entry_ip_def] >> - `(el n path).f = (el n1 path1).f` suffices_by metis_tac [] >> - irule good_path_same_func >> - qexists_tac `<|f := (el n path).f; b := None; i := Offset 0|> ::(path1 ++ [el n path])` >> - qexists_tac `prog` >> - rw [EL_MEM]) >> + >- (fs [entry_ip_def] >> CCONTR_TAC >> fs [] >> fs [ip_equiv_def]) >> fs [EL_TAKE, Abbr `path1`, splitAtPki_EQN] >> CASE_TAC >> rw [] >> fs [] >- metis_tac [] >> @@ -383,7 +507,9 @@ Proof rfs [LENGTH_TAKE] >> `PRE n2 < x` by decide_tac >> first_x_assum drule >> - rw [EL_TAKE] + rfs [HD_DROP, LAST_DEF] >> + rw [EL_TAKE, EL_APPEND_EQN] >> + metis_tac [ip_equiv_sym] QED Theorem dominates_antisym: @@ -398,6 +524,274 @@ Proof metis_tac [dominates_antisym] QED +Definition bip_less_def: + (bip_less (Phi_ip _) (Offset _) ⇔ T) ∧ + (bip_less (Offset m) (Offset n) ⇔ m < n) ∧ + (bip_less _ _ ⇔ F) +End + +Theorem bip_less_tri: + ∀ip1 ip2. ip1.f = ip2.f ∧ ip1.b = ip2.b ⇒ bip_less ip1.i ip2.i ∨ bip_less ip2.i ip1.i ∨ ip_equiv ip1 ip2 +Proof + rw [] >> Cases_on `ip1.i` >> Cases_on `ip2.i`>> rw [bip_less_def, ip_equiv_def] +QED + +Theorem ip_equiv_less: + ∀ip1 ip2 ip3. + ip_equiv ip2 ip3 ∧ + bip_less ip1.i ip2.i + ⇒ + bip_less ip1.i ip3.i +Proof + rw [ip_equiv_def] >> + Cases_on `ip1.i` >> Cases_on `ip2.i` >> Cases_on `ip3.i` >> fs [bip_less_def] +QED + +Theorem ip_equiv_less2: + ∀ip1 ip2 ip3. + ip_equiv ip2 ip3 ∧ + bip_less ip2.i ip1.i + ⇒ + bip_less ip3.i ip1.i +Proof + rw [ip_equiv_def] >> + Cases_on `ip1.i` >> Cases_on `ip2.i` >> Cases_on `ip3.i` >> fs [bip_less_def] +QED + + +Triviality front_cons_snoc: + ∀x y z. front (x::SNOC y z) = x::z +Proof + Induct_on `z` >> fs [SNOC_APPEND] +QED + +Triviality last_cons_snoc: + ∀x y z. last (x::SNOC y z) = y +Proof + Induct_on `z` >> fs [] +QED + +Triviality prefix_snoc: + ∀x y. x ≼ SNOC y x +Proof + Induct_on `x` >> fs [] +QED + +Triviality bip_lem: + bip_less i1 i2 ⇒ ?n. i2 = Offset n +Proof + Cases_on `i1` >> Cases_on `i2` >> fs [bip_less_def] +QED + +Theorem next_ips_prev_entry: + ∀prog ip1 ip2 ip3 f. + (∀fname dec. + alookup prog fname = Some dec ⇒ + every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ⇒ + ip3 ∈ next_ips prog (entry_ip f) ∧ + (∃i. get_instr prog ip1 i) ∧ + ip1.f = ip2.f ∧ + ip1.b = ip2.b ∧ + bip_less ip1.i ip2.i ∧ + ip_equiv ip3 ip2 + ⇒ + ip1 = entry_ip f +Proof + rw [IN_DEF, next_ips_cases, get_instr_cases, entry_ip_def, ip_equiv_def] >> + rw [] >> + Cases_on `HD b.body` >> fs [instr_next_ips_def] >> + rw [] >> fs [inc_pc_def, inc_bip_def] >> rw [] >> + fs [] >> rw [pc_component_equality] >> + rfs [bip_less_def] >> rw [] >> + res_tac >> + fs [EVERY_MEM] >> + metis_tac [blockHeader_distinct, FST, ALOOKUP_MEM, SND, EVERY_MEM, bip_lem, bip_distinct] +QED + +Theorem next_ips_prev_less: + ip2 ∈ next_ips prog ip3 ∧ + (∃i. get_instr prog ip1 i) ∧ + ip1.f = ip2.f ∧ + ip1.b = ip2.b ∧ + ~ip_equiv ip1 ip3 ∧ + bip_less ip1.i ip2.i + ⇒ + ip3.b = ip2.b ∧ bip_less ip1.i ip3.i +Proof + rw [IN_DEF, next_ips_cases, get_instr_cases, ip_equiv_def] >> + rw [] >> + Cases_on `el idx b.body` >> fs [instr_next_ips_def] >> + rw [] >> fs [inc_pc_def, inc_bip_def] >> rw [bip_less_def] >> + imp_res_tac bip_lem >> + fs [] >> + rfs [bip_less_def, inc_bip_def] >> rw [] >> + fs [pc_component_equality] >> rfs [] +QED + +Theorem good_path_end_step: + good_path prog (entry_ip f::SNOC ip2 (p1 ++ [ip3])) + ⇒ + ip2 ∈ next_ips prog ip3 +Proof + rw [Once good_path_cases] >> + qpat_x_assum `_ = _` (mp_tac o GSYM) >> + rw [] >> fs [good_path_append] >> + Cases_on `p1` >> fs [Once good_path_cases] +QED + +Theorem same_block_dominates: + ∀prog. + (∀fname dec. + alookup prog fname = Some dec ⇒ + every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ⇒ + ∀ip1 ip2. + ip1.f = ip2.f ∧ ip1.b = ip2.b ∧ (∃i. get_instr prog ip1 i) ⇒ bip_less ip1.i ip2.i ⇒ dominates prog ip1 ip2 +Proof + ntac 2 strip_tac >> + simp [dominates_def, PULL_FORALL] >> + ntac 3 gen_tac >> + Q.ID_SPEC_TAC `ip2` >> + Q.ID_SPEC_TAC `path` >> + ho_match_mp_tac SNOC_INDUCT >> rw [] + >- ( + simp [Once good_path_cases, ip_equiv_def] >> + Cases_on `ip1.i` >> Cases_on `ip2.i` >> fs [bip_less_def] >> + rw [entry_ip_def, pc_component_equality] >> + CCONTR_TAC >> fs [] >> rw [] >> fs [get_instr_cases] >> rw [] >> + first_x_assum drule >> simp [EXISTS_MEM] >> + qexists_tac `(ip1.b, b)` >> rw [] >> + metis_tac [optionTheory.SOME_11, ALOOKUP_MEM]) >> + simp [front_cons_snoc] >> fs [last_cons_snoc] >> rw [] >> + `good_path prog (entry_ip ip2.f::path)` + by (irule good_path_prefix >> HINT_EXISTS_TAC >> rw [prefix_snoc]) >> + Cases_on `path = []` >> rw [] + >- ( + fs [Once good_path_cases] >> + fs [Once good_path_cases] >> + metis_tac [next_ips_prev_entry, ip_equiv_refl]) >> + `?p1 ip3. path = p1 ++ [ip3]` by metis_tac [SNOC_CASES, SNOC_APPEND] >> + fs [] >> rw [] >> + rename1 `ip_equiv ip2' _` >> + `ip3.f = ip2'.f` + by ( + irule good_path_same_func >> + qexists_tac `entry_ip ip2.f::SNOC ip2' (p1 ++ [ip3])` >> + rw [] >> metis_tac []) >> + Cases_on `ip_equiv ip1 ip3` >> rw [] + >- metis_tac [] >> + `ip3.b = ip2'.b ∧ bip_less ip1.i ip3.i` + by ( + drule good_path_end_step >> strip_tac >> + irule next_ips_prev_less >> + fs [] >> rw [] + >- fs [ip_equiv_def] + >- fs [ip_equiv_def] + >- metis_tac [] + >- metis_tac [ip_equiv_less, ip_equiv_sym]) >> + first_x_assum (qspec_then `ip3` mp_tac) >> simp [] >> + impl_tac + >- metis_tac [ip_equiv_def] >> + impl_tac >> rw [] + >- fs [ip_equiv_def] + >- rw [LAST_DEF, ip_equiv_def] >> + qexists_tac `ip1'` >> rw [] >> + drule MEM_FRONT >> fs [ip_equiv_def] +QED + +Theorem next_ips_still_leq: + ip2 ∈ next_ips prog ip1 ∧ + ip2.f = ip1.f ∧ + ip2.f = ip3.f ∧ + ip1.b = ip3.b ∧ + (∀inst. get_instr prog ip1 (Inl inst) ⇒ ~terminator inst) ∧ + bip_less ip1.i ip3.i + ⇒ + bip_less ip2.i ip3.i ∧ ip2.b = ip1.b ∨ ip2 = ip3 +Proof + rw [IN_DEF, next_ips_cases] >> rfs [] + >- ( + fs [get_instr_cases] >> rw [] >> rfs [] >> rw [] >> fs [] >> + Cases_on `el idx b.body` >> fs [instr_next_ips_def] >> rw [] >> fs [inc_pc_def] >> + rw [] >> rfs [inc_bip_def] >> + Cases_on `ip3.i` >> fs [bip_less_def, pc_component_equality] >> + rw [] >> fs [terminator_def]) + >- ( + fs [get_instr_cases, inc_pc_def] >> rw [] >> rfs [inc_bip_def] >> rw [pc_component_equality] >> + Cases_on `ip3.i` >> fs [bip_less_def]) +QED + +Theorem good_path_find_ip: + ∀prog path. + good_path prog path ⇒ + ∀ip. + loc_prog_ok prog ∧ + path ≠ [] ∧ + (last path).b ≠ ip.b ∧ + ip.f = (HD path).f ∧ ip.b = (HD path).b ∧ bip_less (HD path).i ip.i ∧ + (∃inst. get_instr prog ip inst) + ⇒ + mem ip (front path) +Proof + ho_match_mp_tac good_path_ind >> rw [] + >- metis_tac [] >> + drule next_ips_same_func >> rw [] >> + drule next_ips_still_leq >> simp [] >> + disch_then (qspec_then `ip` mp_tac) >> simp [] >> + impl_tac + >- ( + rw [get_instr_cases] >> + `every (λi. ~terminator i) (front b.body) ∧ b.body ≠ []` by metis_tac [loc_prog_ok_def] >> + fs [EVERY_MEM, MEM_EL] >> + first_x_assum (qspec_then `el idx b.body` mp_tac) >> + impl_tac + >- ( + qexists_tac `idx` >> conj_asm1_tac + >- ( + Cases_on `ip.i` >> fs [bip_less_def, LENGTH_FRONT] >> + fs [get_instr_cases] >> + rw [] >> rfs [] >> rw [] >> fs []) >> + metis_tac [EL_FRONT, NULL_EQ]) >> + metis_tac []) >> + rw [] + >- metis_tac [next_ips_same_func] >> + Cases_on `path` >> fs [] +QED + +Theorem dominates_same_block: + ∀ip1 ip2 ip3. + loc_prog_ok prog ∧ dominates prog ip1 ip3 ∧ ip1.f = ip2.f ∧ ip1.b = ip2.b ∧ + ip3.b ≠ ip1.b ∧ bip_less ip1.i ip2.i ∧ (∃inst. get_instr prog ip2 instr) + ⇒ + dominates prog ip2 ip3 +Proof + rw [dominates_def] >> + first_x_assum drule >> rw [] >> + drule MEM_FRONT >> + REWRITE_TAC [Once MEM_SPLIT] >> strip_tac >> + `good_path prog (ip1'::l2)` + by ( + full_simp_tac std_ss [GSYM APPEND_ASSOC] >> + full_simp_tac std_ss [Once good_path_append]) >> + full_simp_tac std_ss [LAST_APPEND] >> + drule good_path_find_ip >> + disch_then (qspec_then `ip2` mp_tac) >> + impl_tac >> rw [] + >- (fs [ip_equiv_def] >> metis_tac []) + >- ( + `ip1'.f = (entry_ip ip3.f).f` suffices_by (fs [ip_equiv_def]) >> + irule good_path_same_func >> + qexists_tac `entry_ip ip3.f::path` >> + qexists_tac `prog` >> rw_tac std_ss [] + >- rw [] + >- metis_tac [MEM]) + >- fs [ip_equiv_def] + >- metis_tac [ip_equiv_less2] + >- metis_tac [] + >- ( + qexists_tac `ip2` >> rw [ip_equiv_refl] >> + rw [FRONT_APPEND]) +QED + (* ----- Liveness ----- *) Definition live_def: @@ -476,10 +870,11 @@ Proof qpat_x_assum `good_path _ (_::_)` mp_tac >> qpat_x_assum `good_path _ (_::_)` mp_tac >> simp [Once good_path_cases] >> - rw [] >> rw [])) - >- (Cases_on `path` >> fs [])) >> + rw [] >> rw [] >> + metis_tac [ip_equiv_next, ip_equiv_sym])) + >- (Cases_on `path` >> fs [] >> metis_tac [ip_equiv_refl])) >> rw [] >> - `ip2'.f = ip2.f` + `ip1'.f = (last (entry_ip ip2.f::path')).f` by ( irule good_path_same_func >> qexists_tac `entry_ip ip2.f::path'` >> @@ -489,19 +884,23 @@ Proof Cases_on `path` >> full_simp_tac std_ss [GSYM APPEND, FRONT_APPEND, APPEND_NIL, LAST_CONS] >- metis_tac [MEM_FRONT] >> - fs [] >> metis_tac []) + full_simp_tac std_ss [GSYM APPEND, FRONT_APPEND] >> fs [] >> rw [FRONT_DEF] >> fs [] >> + metis_tac [ip_equiv_assigns]) >- metis_tac [MEM_LAST]) >> - `ip2' = ip1` by metis_tac [] >> + `ip2'.f = ip1.f` by fs [ip_equiv_def] >> + `ip_equiv ip2' ip1` by metis_tac [] >> rw [] >> Cases_on `path` >> fs [] >> full_simp_tac std_ss [GSYM APPEND, FRONT_APPEND] >> fs [] >> rw [FRONT_DEF] >> fs [] - >- metis_tac [] + >- (fs [FRONT_DEF] >> metis_tac [ip_equiv_sym, ip_equiv_trans]) + >- (fs [ip_equiv_def, entry_ip_def] >> metis_tac [pc_component_equality]) + >- (fs [FRONT_DEF] >> metis_tac [ip_equiv_sym, ip_equiv_trans]) >- ( - `mem ip1 path' = mem ip1 (front path' ++ [last path'])` by metis_tac [APPEND_FRONT_LAST] >> + `mem ip1' path' = mem ip1' (front path' ++ [last path'])` by metis_tac [APPEND_FRONT_LAST] >> fs [LAST_DEF] >> - metis_tac []) - >- metis_tac [] - >- metis_tac [] + metis_tac [ip_equiv_trans, ip_equiv_assigns]) + >- metis_tac [ip_equiv_assigns] + >- metis_tac [ip_equiv_assigns] QED Theorem ssa_dominates_live_range: @@ -521,6 +920,7 @@ Theorem reachable_dominates_same_func: ∀prog ip1 ip2. reachable prog ip2 ∧ dominates prog ip1 ip2 ⇒ ip1.f = ip2.f Proof rw [reachable_def, dominates_def] >> res_tac >> + `ip1'.f = (last (entry_ip ip2.f::path)).f` suffices_by fs [ip_equiv_def] >> irule good_path_same_func >> metis_tac [MEM_LAST, MEM_FRONT] QED @@ -533,9 +933,10 @@ Proof qexists_tac `path ++ [ip2]` >> simp_tac std_ss [GSYM APPEND, LAST_APPEND_CONS, LAST_CONS] >> simp [good_path_append] >> - simp [Once good_path_cases] >> - fs [next_ips_cases, IN_DEF] >> - metis_tac [] + simp [Once good_path_cases, ip_equiv_refl] >> + rw [] + >- (fs [next_ips_cases, IN_DEF] >> metis_tac []) + >- metis_tac [ip_equiv_next, ip_equiv_sym] QED (* ----- A theory of *dominator ordered* programs ------ *) @@ -570,11 +971,6 @@ Definition linear_live_def: let (gen,kill) = instrs_live b.body in header_uses b.h ∪ (gen ∪ (linear_live bs DIFF kill) DIFF header_assigns b.h)) End -Definition bip_less_def: - (bip_less (Phi_ip _) (Offset _) ⇔ T) ∧ - (bip_less (Offset m) (Offset n) ⇔ m < n) ∧ - (bip_less _ _ ⇔ F) -End Definition linear_pc_less_def: linear_pc_less = $< LEX bip_less @@ -834,4 +1230,648 @@ Proof metis_tac [] QED +Definition block_assigns_def: + block_assigns (l, b) = + header_assigns b.h ∪ image fst (bigunion (image instr_assigns (set b.body))) +End + +Definition block_uses_def: + block_uses (l, b) = + header_uses b.h ∪ bigunion (image instr_uses (set b.body)) +End + +Definition block_order_def: + block_order bs = + tc { (b1, b2) | + fst b1 ≠ fst b2 ∧ mem b1 bs ∧ mem b2 bs ∧ (∃r. r ∈ block_assigns b1 ∧ r ∈ block_uses b2) } +End + +Theorem prog_ok_distinct_lem: + loc_prog_ok p ∧ alookup p f = Some d ⇒ all_distinct (map fst d.blocks) +Proof + rw [loc_prog_ok_def, EVERY_MEM] >> + drule ALOOKUP_MEM >> rw [] >> + res_tac >> fs [] +QED + +Theorem block_order_dominates: + ∀b1 b2. + (b1,b2) ∈ block_order d.blocks ⇒ + loc_prog_ok prog ∧ + is_ssa prog ∧ + alookup prog f = Some d ⇒ + ∃ip1 ip2. + dominates prog ip1 ip2 ∧ + ip1.f = f ∧ + ip2.f = f ∧ + ip1.b = fst b1 ∧ + ip2.b = fst b2 ∧ + fst b1 ≠ fst b2 ∧ + (∃i2. get_instr prog ip2 i2) +Proof + simp [block_order_def] >> + ho_match_mp_tac tc_ind >> rw [] + >- ( + fs [is_ssa_def] >> + `∃ip1. r ∈ uses prog ip1 ∧ ip1.f = f ∧ ip1.b = fst b2` + by ( + simp [Once IN_DEF, uses_cases] >> Cases_on `b2` >> fs [block_uses_def] >> + fs [get_instr_cases, PULL_EXISTS] + >- ( + rename1 `_ ∈ header_uses b.h` >> + Cases_on `b.h` >> fs [header_uses_def] >> rw [] >> + rename1 `mem (l1, _) _` >> + qexists_tac `<| f := f; b := l1; i := Phi_ip from_l |>` >> rw [] >> + qexists_tac `l` >> qexists_tac `phi_uses from_l p` >> qexists_tac `b` >> + rw [MEM_MAP] >> + metis_tac [ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, prog_ok_distinct_lem]) + >- ( + fs [MEM_EL] >> rw [] >> + rename [`n1 < length b.body`, `(l1, _) = el _ _`] >> + qexists_tac `<| f := f; b := l1; i := Offset n1 |>` >> rw [] >> + metis_tac [ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, EL_MEM, prog_ok_distinct_lem])) >> + first_x_assum drule >> rw [] >> + qexists_tac `ip2` >> qexists_tac `ip1` >> rw [] + >- ( + rename1 `rt ∈ assigns _ _` >> + `∃ip3 t. (fst rt, t) ∈ assigns prog ip3 ∧ ip3.f = ip1.f ∧ ip3.b = fst b1` + by ( + simp [Once IN_DEF, assigns_cases] >> Cases_on `b1` >> fs [block_assigns_def] >> + fs [get_instr_cases, PULL_EXISTS] + >- ( + rename1 `_ ∈ header_assigns b.h` >> + Cases_on `b.h` >> fs [header_assigns_def] >> rw [] >> + rename1 `mem (l1, _) _` >> + fs [MEM_MAP] >> + qexists_tac `<| f := ip1.f; b := l1; i := Phi_ip from_l |>` >> rw [] >> + qexists_tac `SND (phi_assigns y)` >> qexists_tac `l` >> qexists_tac `b` >> + qexists_tac `o'` >> rw [] >> + metis_tac [FST, ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, SND, prog_ok_distinct_lem]) + >- ( + fs [MEM_EL] >> rw [] >> + rename [`n1 < length b.body`, `(l1, _) = el _ _`] >> + qexists_tac `<| f := ip1.f; b := l1; i := Offset n1 |>` >> rw [] >> + qexists_tac `snd x` >> + rw [] >> + metis_tac [ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, EL_MEM, FST, SND, prog_ok_distinct_lem])) >> + metis_tac [ip_equiv_def, FST]) + >- (fs [uses_cases, IN_DEF] >> metis_tac [])) + >- ( + first_x_assum drule >> first_x_assum drule >> rw [] >> + Cases_on `ip1.b = ip2.b ∨ ip1'.b = ip2'.b` + >- metis_tac [] >> + qexists_tac `ip1` >> qexists_tac `ip2'` >> + Cases_on `bip_less ip2.i ip1'.i` + >- ( + `dominates prog ip2 ip1'` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + rw [] + >- metis_tac [dominates_trans] + >- ( + CCONTR_TAC >> fs [] >> + Cases_on `bip_less ip2'.i ip1.i` + >- ( + `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >> + Cases_on `bip_less ip1.i ip2'.i` + >- ( + `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def]) + >- ( + `dominates prog ip1' ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def])) + >- metis_tac []) >> + Cases_on `bip_less ip1'.i ip2.i` + >- ( + `dominates prog ip2 ip2'` by metis_tac [dominates_same_block] >> + rw [] + >- metis_tac [dominates_trans] + >- ( + CCONTR_TAC >> fs [] >> + Cases_on `bip_less ip2'.i ip1.i` + >- ( + `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >> + Cases_on `bip_less ip1.i ip2'.i` + >- ( + `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def]) + >- ( + `dominates prog ip2 ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def])) + >- metis_tac []) + >- ( + `ip_equiv ip1' ip2` by metis_tac [bip_less_tri] >> + `dominates prog ip1 ip2'` by metis_tac [dominates_trans, ip_equiv_sym, ip_equiv_dominates] >> + rw [] + >- ( + CCONTR_TAC >> fs [] >> + Cases_on `bip_less ip2'.i ip1.i` + >- ( + `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >> + Cases_on `bip_less ip1.i ip2'.i` + >- ( + `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >> + `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, ip_equiv_sym] >> + metis_tac [dominates_antisym, is_ssa_def]) + >- ( + `dominates prog ip2' ip2` by metis_tac [ip_equiv_dominates2, bip_less_tri] >> + `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, bip_less_tri] >> + metis_tac [dominates_antisym, is_ssa_def])) + >- metis_tac [])) +QED + +Theorem block_order_po: + ∀prog f d. + loc_prog_ok prog ∧ is_ssa prog ∧ + alookup prog f = Some d + ⇒ + partial_order (rc (block_order d.blocks) (set d.blocks)) (set d.blocks) +Proof + rw [partial_order_def] + >- (rw [block_order_def, domain_def, SUBSET_DEF, rc_def] >> drule tc_domain_range >> rw [domain_def]) + >- (rw [block_order_def, range_def, SUBSET_DEF, rc_def] >> rw [] >> drule tc_domain_range >> rw [range_def]) + >- metis_tac [block_order_def, transitive_rc, tc_transitive] + >- metis_tac [rc_is_reflexive] + >- ( + simp [antisym_rc] >> rw [antisym_def] >> + pop_assum mp_tac >> + drule block_order_dominates >> + disch_then drule >> simp [] >> disch_then drule >> rw [] >> + drule block_order_dominates >> + disch_then drule >> simp [] >> disch_then drule >> rw [] >> + CCONTR_TAC >> + Cases_on `bip_less ip2.i ip1'.i` + >- ( + `dominates prog ip2 ip1'` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + Cases_on `bip_less ip2'.i ip1.i` + >- ( + `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >> + Cases_on `bip_less ip1.i ip2'.i` + >- ( + `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def]) + >- ( + `dominates prog ip1' ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def])) >> + Cases_on `bip_less ip1'.i ip2.i` + >- ( + `dominates prog ip2 ip2'` by metis_tac [dominates_same_block] >> + Cases_on `bip_less ip2'.i ip1.i` + >- ( + `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >> + Cases_on `bip_less ip1.i ip2'.i` + >- ( + `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def]) + >- ( + `dominates prog ip2 ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >> + metis_tac [dominates_antisym, dominates_trans, is_ssa_def])) + >- ( + `ip_equiv ip1' ip2` by metis_tac [bip_less_tri] >> + `dominates prog ip1 ip2'` by metis_tac [dominates_trans, ip_equiv_sym, ip_equiv_dominates] >> + Cases_on `bip_less ip2'.i ip1.i` + >- ( + `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >> + metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >> + Cases_on `bip_less ip1.i ip2'.i` + >- ( + `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >> + `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, ip_equiv_sym] >> + metis_tac [dominates_antisym, is_ssa_def]) + >- ( + `dominates prog ip2' ip2` by metis_tac [ip_equiv_dominates2, bip_less_tri] >> + `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, bip_less_tri] >> + metis_tac [dominates_antisym, is_ssa_def]))) +QED + +Theorem assigns_weak: + ∀l d p ip r. ~mem l (map fst p) ∧ r ∈ assigns p ip ⇒ r ∈ assigns ((l,d)::p) ip +Proof + rw [assigns_cases, IN_DEF, get_instr_cases, PULL_EXISTS] >> + imp_res_tac ALOOKUP_MEM >> + fs [LIST_TO_SET_MAP] >> metis_tac [FST] +QED + +Theorem uses_weak: + ∀l d p ip r. ip.f ≠ l ⇒ uses ((l,d)::p) ip = uses p ip +Proof + rw [uses_cases, EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS] +QED + +Theorem assigns_weak2: + ∀l d p ip r. ip.f ≠ l ⇒ assigns ((l,d)::p) ip = assigns p ip +Proof + rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS] +QED + +Theorem good_path_weak: + ∀l d p ip path. ip.f ≠ l ⇒ good_path ((l,d)::p) (ip::path) = good_path p (ip::path) +Proof + Induct_on `path` >> rw [] >> + ONCE_REWRITE_TAC [good_path_cases] >> rw [] + >- rw [EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS] >> + rename1 `good_path _ (p1::_)` >> + Cases_on `p1.f ≠ l` + >- ( + first_x_assum drule >> rw [] >> + eq_tac >> rw [] >> + fs [next_ips_cases, EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS] >> rw [] >> + metis_tac []) + >- metis_tac [next_ips_same_func] +QED + +Theorem dominates_weak: + ∀l d p ip1 ip2. ip1.f ≠ l ⇒ dominates ((l,d)::p) ip2 ip1 = dominates p ip2 ip1 +Proof + rw [dominates_def, EXTENSION, IN_DEF] >> + `(entry_ip ip1.f).f = ip1.f` by rw [entry_ip_def] >> + metis_tac [good_path_weak] +QED + +Theorem uses_good_ip: + ∀r prog ip. r ∈ uses prog ip ⇒ mem ip.f (map fst prog) +Proof + rw [uses_cases, IN_DEF, get_instr_cases] >> + imp_res_tac ALOOKUP_MEM >> + fs [LIST_TO_SET_MAP] >> + metis_tac [FST] +QED + +Theorem is_ssa_weak: + ∀l d p. ~mem l (map fst p) ∧ is_ssa ((l,d)::p) ⇒ is_ssa p +Proof + rw [is_ssa_def] + >- (first_x_assum irule >> rw [PULL_EXISTS] >> metis_tac [assigns_weak]) + >- ( + drule uses_good_ip >> rw [] >> + last_x_assum (qspec_then `ip1` mp_tac) >> rw [] >> + `ip1.f ≠ l` by metis_tac [MEM_MAP] >> + fs [uses_weak, assigns_weak2] >> + first_x_assum drule >> rw [] >> + qexists_tac `ip2` >> rw [] >> rfs [] >> + metis_tac [assigns_weak2, dominates_weak]) + >- ( + `get_instr ((l,d)::p) ip i` + by (fs [get_instr_cases, MEM_MAP] >> rw [] >> metis_tac [ALOOKUP_MEM, FST]) >> + first_x_assum drule >> rw [reachable_def] >> + qexists_tac `path` >> rw [] >> + `(entry_ip ip.f).f ≠ l` suffices_by metis_tac [good_path_weak] >> + rw [entry_ip_def] >> fs [get_instr_cases, MEM_MAP] >> + CCONTR_TAC >> fs [] >> rw [] >> + metis_tac [FST, ALOOKUP_MEM]) +QED + +Theorem loc_prog_ok_weak: + ∀l d p. ~mem l (map fst p) ∧ loc_prog_ok ((l,d)::p) ⇒ loc_prog_ok p +Proof + rw [loc_prog_ok_def, MEM_MAP] >> + metis_tac [ALOOKUP_MEM, FST] +QED + +Triviality in_uncurry: + (x,y) ∈ UNCURRY R ⇔ R x y +Proof + rw [IN_DEF, UNCURRY_DEF] +QED + +Theorem sorted_all_distinct_idx: + ∀R l. all_distinct l ∧ transitive R ∧ reflexive R ∧ antisym (rrestrict (UNCURRY R) (set l)) ⇒ + (SORTED R l ⇔ (∀i j. i < length l ∧ j < length l ⇒ (R (el i l) (el j l) ⇔ i ≤ j))) +Proof + Induct_on `l` >> rw [sortingTheory.SORTED_EQ] >> + `antisym (rrestrict (UNCURRY R) (set l))` + by (fs [antisym_def] >> rw [in_rrestrict]) >> + eq_tac >> rw [] + >- ( + Cases_on `i` >> Cases_on `j` >> rw [] >> fs [] + >- fs [relationTheory.reflexive_def] + >- (first_x_assum irule >> rw [MEM_EL] >> metis_tac []) + >- ( + fs [antisym_def] >> + last_x_assum (qspecl_then [`h`, `el n l`] mp_tac) >> + simp [in_rrestrict, in_uncurry] >> metis_tac [MEM_EL])) + >- (first_x_assum (qspecl_then [`Suc i`, `Suc j`] mp_tac) >> rw []) + >- ( + fs [MEM_EL] >> rw [] >> + first_x_assum (qspecl_then [`0`, `Suc n`] mp_tac) >> rw []) +QED + +Theorem lpc_uses_to_uses: + ∀r bs lip prog f d. + r ∈ lpc_uses (map snd bs) lip ∧ + alookup prog (Fn f) = Some d ∧ + PERM d.blocks bs ∧ + all_distinct (map fst (d.blocks)) + ⇒ + r ∈ uses prog <| f := Fn f; b := fst (el (fst lip) bs); i := snd lip |> ∧ + fst lip < length bs +Proof + rw [IN_DEF, uses_cases, lpc_uses_cases, get_instr_cases, PULL_EXISTS, + lpc_get_instr_cases] >> + rw [] + >- ( + qexists_tac `el i' (map snd bs)` >> rw [] >> + irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >> + drule sortingTheory.MEM_PERM >> rw [MEM_EL, EL_MAP] >> + metis_tac [pair_CASES, FST, SND]) + >- ( + qexists_tac `phis` >> + qexists_tac `el i (map snd bs)` >> rw [] >> + qexists_tac `s` >> rw [] >> + irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >> + drule sortingTheory.MEM_PERM >> rw [MEM_EL, EL_MAP] >> + metis_tac [pair_CASES, FST, SND]) +QED + +Theorem assigns_to_block_assigns: + ∀prog ip d b r l. + r ∈ assigns prog ip ∧ + alookup prog ip.f = Some d ∧ + alookup d.blocks ip.b = Some b + ⇒ + fst r ∈ block_assigns (l:label option, b) +Proof + rw [] >> + qpat_x_assum `_ ∈ assigns _ _` mp_tac >> + simp [Once IN_DEF] >> + rw [assigns_cases, get_instr_cases, PULL_EXISTS, block_assigns_def] + >- ( + disj2_tac >> + qexists_tac `r` >> HINT_EXISTS_TAC >> + metis_tac [MEM_EL]) + >- ( + rw [header_assigns_def, MEM_MAP] >> + disj1_tac >> + fs [MEM_MAP] >> rw [] >> + metis_tac []) +QED + +Theorem assigns_to_lpc_assigns: + ∀prog ip d r idx (bs : (label option # block) list). + r ∈ assigns prog ip ∧ + alookup prog ip.f = Some d ∧ + alookup d.blocks ip.b = Some (snd (el idx bs)) ∧ + idx < length bs + ⇒ + r ∈ lpc_assigns (map snd bs) (idx, ip.i) +Proof + rw [assigns_cases, get_instr_cases, PULL_EXISTS, block_assigns_def, + lpc_assigns_cases, IN_DEF, lpc_get_instr_cases] >> + fs [] >> rw [] >> fs [] >> rw [EL_MAP] +QED + +Theorem uses_to_block_uses: + ∀prog ip d b r l. + r ∈ uses prog ip ∧ + alookup prog ip.f = Some d ∧ + alookup d.blocks ip.b = Some b + ⇒ + r ∈ block_uses (l:label option, b) +Proof + rw [] >> + qpat_x_assum `_ ∈ uses _ _` mp_tac >> + simp [Once IN_DEF] >> + rw [uses_cases, get_instr_cases, PULL_EXISTS, block_uses_def] + >- ( + disj2_tac >> + metis_tac [MEM_EL]) + >- ( + rw [header_uses_def, MEM_MAP] >> + disj1_tac >> + fs [MEM_MAP] >> rw [] >> + metis_tac []) +QED + +Theorem same_block_assigns_less_uses: + reachable prog ip1 ∧ + dominates prog ip2 ip1 ∧ + ip1.b = ip2.b ∧ + (?i. get_instr prog ip1 i) ∧ + (∀fname dec. + alookup prog fname = Some dec ⇒ + every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks) + ⇒ + bip_less ip2.i ip1.i +Proof + rw [] >> CCONTR_TAC >> fs [] >> + `ip1.f = ip2.f` by metis_tac [reachable_dominates_same_func] >> + `ip_equiv ip1 ip2 ∨ bip_less ip1.i ip2.i` by metis_tac [bip_less_tri] + >- metis_tac [ip_equiv_dominates2, dominates_irrefl, ip_equiv_sym] >> + metis_tac [dominates_antisym, same_block_dominates] +QED + +Theorem ssa_to_dominator_ordered_lem: + ∀p1. loc_prog_ok p1 ∧ is_ssa p1 ∧ all_distinct (map fst p1) ∧ every (λ(l,d). all_distinct (map fst d.blocks)) p1 ⇒ + ∃p2. list_rel (\(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 ∧ + dominator_ordered p2 +Proof + Induct_on `p1` >> rw [] + >- rw [dominator_ordered_def] >> + `is_ssa p1` by metis_tac [is_ssa_weak, pair_CASES, FST] >> + `loc_prog_ok p1` by metis_tac [loc_prog_ok_weak, pair_CASES, FST] >> + fs [PULL_EXISTS] >> + rename1 `is_ssa (x::_)` >> + `?l d. x = (l,d)` by metis_tac [pair_CASES] >> + `partial_order (rc (block_order d.blocks) (set d.blocks)) (set d.blocks)` + by metis_tac [block_order_po, ALOOKUP_def] >> + rw [] >> + `finite (set d.blocks)` by rw [] >> + drule finite_linear_order_of_finite_po >> + disch_then drule >> rw [] >> + drule finite_linear_order_to_list >> + disch_then drule >> rw [] >> + rename1 `set _ = set bs` >> + qexists_tac `(l, d with blocks := bs)` >> + qexists_tac `p2` >> + conj_asm1_tac >> rw [] >> + fs [] + >- (irule sortingTheory.PERM_ALL_DISTINCT >> rw [] >> metis_tac [ALL_DISTINCT_MAP]) >> + qmatch_assum_abbrev_tac `SORTED R _` >> + `transitive R ∧ reflexive R ∧ antisym (rrestrict (UNCURRY R) (set bs))` + by ( + fs [linear_order_def, transitive_def, reflexive_def, SUBSET_DEF, + antisym_def, domain_def, range_def, in_rrestrict] >> + rw [Abbr `R`, relationTheory.transitive_def, relationTheory.reflexive_def] >> + fs [IN_DEF] >> metis_tac []) >> + drule sorted_all_distinct_idx >> + disch_then drule >> rw [] >> + fs [dominator_ordered_def] >> rw [PULL_EXISTS] >> fs [] + >- ( + drule lpc_uses_to_uses >> + disch_then (qspecl_then [`(Fn f,d)::p1`, `f`, `d`] mp_tac) >> + rw [] >> + qmatch_assum_abbrev_tac `_ ∈ uses prog ip1` >> + `?ip2. ip2.f = Fn f ∧ r ∈ image fst (assigns prog ip2) ∧ dominates prog ip2 ip1` + by (fs [is_ssa_def] >> last_x_assum drule >> rw [Abbr `ip1`]) >> + `?idx. idx < length bs ∧ alookup d.blocks ip2.b = Some (snd (el idx bs)) ∧ + fst (el idx bs) = ip2.b` + by ( + fs [assigns_cases, IN_DEF, get_instr_cases, Abbr `prog`] >> + rfs [] >> + drule ALOOKUP_MEM >> + drule sortingTheory.MEM_PERM >> + rw [MEM_EL] >> + metis_tac [FST, SND]) >> + `?t. (r, t) ∈ assigns prog ip2` by metis_tac [IN_IMAGE, pair_CASES, FST] >> + drule assigns_to_block_assigns >> rw [Abbr `prog`] >> + qexists_tac `(idx, ip2.i)` >> + qexists_tac `(r, t)` >> + rw [] + >- ( + `(el idx bs, el (fst lip1) bs) ∈ rc (block_order d.blocks) (set d.blocks)` + by ( + simp [rc_def, block_order_def, EL_MEM] >> + drule uses_to_block_uses >> simp [Abbr `ip1`] >> + `alookup d.blocks (fst (el (fst lip1) bs)) = Some (snd (el (fst lip1) bs))` + by ( + qmatch_goalsub_abbrev_tac `(fst b)` >> + `mem b bs` by (rw [Abbr `b`, MEM_EL] >> metis_tac []) >> + metis_tac [ALOOKUP_ALL_DISTINCT_MEM, PAIR]) >> + rw [METIS_PROVE [] ``a ∨ b ⇔ ~b ⇒ a``] >> + simp [Once tc_cases] >> + disj1_tac >> rw [MEM_EL] + >- ( + `all_distinct (map fst bs)` + by ( + irule ALL_DISTINCT_MAP_INJ >> rw [] >> + `mem x d.blocks ∧ mem y d.blocks` by metis_tac [sortingTheory.MEM_PERM] >> + metis_tac [PAIR, ALOOKUP_ALL_DISTINCT_MEM, optionTheory.SOME_11]) >> + metis_tac [PAIR, optionTheory.SOME_11]) >> + metis_tac [PAIR, FST]) >> + rw [] >> + `idx ≤ fst lip1` + by ( + `R (el idx bs) (el (fst lip1) bs)` suffices_by metis_tac [] >> + fs [Abbr `R`, SUBSET_DEF, rc_def] >> metis_tac []) >> + PairCases_on `lip1` >> + rw [linear_pc_less_def, LEX_DEF_THM] >> fs [LESS_OR_EQ] >> + rw [] >> + `reachable ((Fn f,d)::p1) ip1` + by ( + fs [is_ssa_def] >> first_x_assum irule >> + fs [uses_cases, IN_DEF] >> metis_tac []) >> + drule same_block_assigns_less_uses >> + disch_then drule >> simp [Abbr `ip1`] >> + disch_then irule >> rw [] >> + fs [uses_cases, IN_DEF, loc_prog_ok_def] >> + metis_tac []) + >- (drule assigns_to_lpc_assigns >> simp [])) + >- metis_tac [] +QED + +Theorem prog_ok_to_loc_prog_ok: + ∀p. prog_ok p ⇒ loc_prog_ok p +Proof + rw [prog_ok_def, loc_prog_ok_def] >> metis_tac [] +QED + +Theorem alookup_perm_blocks: + ∀p1 p2. + list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 + ⇒ + (∀l d. alookup p2 l = Some d ⇒ ?d'. alookup p1 l = Some d' ∧ PERM d'.blocks d.blocks) ∧ + (∀l d. alookup p1 l = Some d ⇒ ?d'. alookup p2 l = Some d' ∧ PERM d.blocks d'.blocks) ∧ + (map fst p1 = map fst p2) +Proof + Induct_on `p1` >> rw [] >> + pairarg_tac >> fs [] >> pairarg_tac >> fs [] >> rw [] >> rw [] >> fs [] >> + metis_tac [] +QED + +Theorem alookup_perm: + ∀b1 b2. PERM b1 b2 ∧ all_distinct (map fst b1) ⇒ alookup b1 = alookup b2 +Proof + rw [] >> + irule ALOOKUP_ALL_DISTINCT_PERM_same >> + rw [sortingTheory.PERM_MAP, sortingTheory.PERM_LIST_TO_SET] +QED + +Theorem get_instr_perm_blocks: + every (\(l,d). all_distinct (map fst d.blocks)) p1 ∧ + list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 + ⇒ + get_instr p1 = get_instr p2 +Proof + rw [get_instr_cases, FUN_EQ_THM] >> + eq_tac >> rw [] >> + drule alookup_perm_blocks >> rw [] >> + first_x_assum drule >> rw [] >> rw [] >> + `all_distinct (map fst d.blocks)` + by ( + fs [EVERY_MEM] >> + imp_res_tac ALOOKUP_MEM >> + res_tac >> fs [] >> + metis_tac [sortingTheory.ALL_DISTINCT_PERM, sortingTheory.PERM_MAP]) >> + metis_tac [alookup_perm, sortingTheory.PERM_SYM] +QED + +Theorem next_ips_perm_blocks: + every (\(l,d). all_distinct (map fst d.blocks)) p1 ∧ + list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 + ⇒ + next_ips p1 = next_ips p2 +Proof + rw [FUN_EQ_THM, next_ips_cases] >> metis_tac [get_instr_perm_blocks] +QED + +Theorem good_path_perm_blocks: + ∀p1 p2. + every (\(l,d). all_distinct (map fst d.blocks)) p1 ∧ + list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 + ⇒ + good_path p1 = good_path p2 +Proof + rw [] >> simp [FUN_EQ_THM] >> + Induct >> rw [] >> + ONCE_REWRITE_TAC [good_path_cases] >> rw [] >> + metis_tac [next_ips_perm_blocks, get_instr_perm_blocks] +QED + +Theorem ssa_to_dominator_ordered: + ∀p1. + prog_ok p1 ∧ is_ssa p1 + ⇒ + ∃p2. list_rel (\(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 ∧ + dominator_ordered p2 ∧ prog_ok p2 ∧ is_ssa p2 +Proof + rw [] >> + drule prog_ok_to_loc_prog_ok >> rw [] >> + drule ssa_to_dominator_ordered_lem >> simp [] >> + impl_tac + >- ( + fs [prog_ok_def] >> rw [EVERY_MEM] >> + pairarg_tac >> fs [] >> rw [] >> metis_tac [ALOOKUP_ALL_DISTINCT_MEM]) >> + rw [] >> + qexists_tac `p2` >> rw [] >> + `every (λ(l,d). all_distinct (map fst d.blocks)) p1` + by fs [prog_ok_def] >> + drule get_instr_perm_blocks >> disch_then drule >> rw [] >> + drule good_path_perm_blocks >> disch_then drule >> rw [] + >- ( + drule alookup_perm_blocks >> rw [] >> + fs [prog_ok_def] >> + conj_tac + >- ( + rw [] >> rpt (last_x_assum (qspec_then `fname` mp_tac)) >> rw [] >> + metis_tac [alookup_perm, sortingTheory.MEM_PERM, prog_ok_distinct_lem]) >> + conj_tac >- metis_tac [alookup_perm, sortingTheory.MEM_PERM, prog_ok_distinct_lem] >> + conj_tac >- (fs [EVERY_MEM] >> metis_tac [alookup_perm, sortingTheory.MEM_PERM]) >> + conj_tac + >- ( + rfs [LIST_REL_EL_EQN, EVERY_EL] >> rw [] >> + pairarg_tac >> fs [] >> + rpt (first_x_assum (qspec_then `n` mp_tac)) >> rw [] >> + pairarg_tac >> fs [] >> + metis_tac [sortingTheory.ALL_DISTINCT_PERM, sortingTheory.PERM_MAP]) >> + conj_tac >- metis_tac [alookup_perm, sortingTheory.MEM_PERM] + >- metis_tac [alookup_perm, sortingTheory.MEM_PERM]) + >- ( + fs [is_ssa_def, IN_DEF, uses_cases, assigns_cases, reachable_def, dominates_def] >> + rw [] >> + first_x_assum irule >> metis_tac []) +QED + export_theory (); diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml index 65cc82f9e..9c5f36932 100644 --- a/sledge/semantics/llvm_to_llair_propScript.sml +++ b/sledge/semantics/llvm_to_llair_propScript.sml @@ -31,6 +31,8 @@ Proof rw [prog_ok_def] >> rpt (first_x_assum drule) >> rw [] >> fs [EVERY_MEM] >> rw [] >> pairarg_tac >> rw [] >> + `mem (Fn f,d) prog` by metis_tac [ALOOKUP_MEM] >> + last_x_assum drule >> rw [] >> fs [] >> `alookup d.blocks l = Some b` by metis_tac [ALOOKUP_ALL_DISTINCT_MEM] >> last_x_assum drule >> rw [] >> CCONTR_TAC >> fs [] >> @@ -42,6 +44,7 @@ Proof `~mem (el i b.body) (front b.body)` by metis_tac [] >> metis_tac [mem_el_front] QED + Theorem prog_ok_nonterm: ∀prog i ip. prog_ok prog ∧ get_instr prog ip (Inl i) ∧ ¬terminator i ⇒ inc_pc ip ∈ next_ips prog ip @@ -935,7 +938,14 @@ Proof imp_res_tac ALOOKUP_MEM >> fs [MEM_MAP] >> metis_tac [FST]) - >- metis_tac [ALOOKUP_ALL_DISTINCT_MEM, prog_ok_def] + >- ( + fs [prog_ok_def] >> + qexists_tac `prog` >> rw [] >> + irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >> + fs [EVERY_MEM] >> + `(λ(fname,dec). all_distinct (map fst dec.blocks)) (Fn f, d)` + by metis_tac [ALOOKUP_MEM] >> + fs []) QED Theorem alookup_translate_header_lab: diff --git a/sledge/semantics/llvm_to_llair_sem_propScript.sml b/sledge/semantics/llvm_to_llair_sem_propScript.sml index 30396d0be..c1ed339b7 100644 --- a/sledge/semantics/llvm_to_llair_sem_propScript.sml +++ b/sledge/semantics/llvm_to_llair_sem_propScript.sml @@ -328,7 +328,7 @@ Proof first_x_assum drule >> simp [] >> disch_then (qspec_then `translate_reg r1 ty1` mp_tac) >> rw [] >> CCONTR_TAC >> fs [] >> - `ip2 = s.ip` + `ip_equiv ip2 s.ip` by ( fs [is_ssa_def, EXTENSION, IN_DEF] >> Cases_on `r1` >> fs [translate_reg_def, untranslate_reg_def] >> @@ -337,7 +337,7 @@ Proof `assigns prog s.ip (Reg reg, ty1)` suffices_by metis_tac [reachable_dominates_same_func, FST] >> metis_tac [EL_MEM, IN_DEF]) >> - metis_tac [dominates_irrefl]) >> + metis_tac [dominates_irrefl, ip_equiv_dominates2]) >> drule ALOOKUP_MEM >> rw [MEM_MAP, MEM_ZIP] >> metis_tac [EL_MEM, LIST_REL_LENGTH, LENGTH_MAP] QED @@ -1493,9 +1493,10 @@ Proof >- ( fs [reachable_def] >> qexists_tac `path ++ [<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>]` >> - rw_tac std_ss [good_path_append, GSYM APPEND] >> rw [] >> - rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >> - metis_tac []))) + rw_tac std_ss [good_path_append, GSYM APPEND] >> rw [] + >- (rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >> metis_tac []) + >- metis_tac [ip_equiv_next_ips, ip_equiv_sym] + >- metis_tac [ip_equiv_refl]))) >- fs [is_implemented_def] >- fs [is_implemented_def] >- ( (* Exit *) @@ -1923,7 +1924,11 @@ Proof rw [] >> drule alookup_translate_blocks >> rpt (disch_then drule) >> impl_tac - >- metis_tac [ALOOKUP_ALL_DISTINCT_MEM, prog_ok_def] >> + >- ( + fs [prog_ok_def, EVERY_MEM] >> rw [] >> + irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >> + imp_res_tac ALOOKUP_MEM >> + res_tac >> fs []) >> simp [translate_label_def] >> rw [] >> rw [dest_label_def, num_calls_def] >> rw [translate_instrs_take_to_call] >> diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml index b890398e0..1dcb0efca 100644 --- a/sledge/semantics/miscScript.sml +++ b/sledge/semantics/miscScript.sml @@ -11,7 +11,8 @@ open HolKernel boolLib bossLib Parse; open listTheory rich_listTheory arithmeticTheory integerTheory llistTheory pathTheory; open integer_wordTheory wordsTheory pred_setTheory alistTheory; -open finite_mapTheory open logrootTheory numposrepTheory; +open finite_mapTheory open logrootTheory numposrepTheory set_relationTheory; +open sortingTheory; open settingsTheory; new_theory "misc"; @@ -965,4 +966,62 @@ Proof rw [] QED +(* ---- set_relation theorems ---- *) + +Theorem finite_imp_finite_prefixes: + ∀r s. finite s ∧ domain r ⊆ s ⇒ finite_prefixes r s +Proof + rw [finite_prefixes_def] >> + irule SUBSET_FINITE_I >> fs [SUBSET_DEF, domain_def] >> metis_tac [] +QED + +Theorem finite_linear_order_of_finite_po: + ∀r s. finite s ∧ partial_order r s ⇒ ∃r'. linear_order r' s ∧ r ⊆ r' +Proof + rw [] >> + `countable s` by metis_tac [finite_countable] >> + `finite_prefixes r s` by metis_tac [finite_imp_finite_prefixes, partial_order_def] >> + metis_tac [linear_order_of_countable_po] +QED + +Theorem finite_linear_order_to_list: + ∀lo X. finite X ∧ linear_order lo X ⇒ + ∃l. X = set l ∧ SORTED (λx y. (x, y) ∈ lo ∨ y ∉ X) l ∧ all_distinct l +Proof + rw [] >> + qmatch_goalsub_abbrev_tac `SORTED R _` >> + qexists_tac `QSORT R (SET_TO_LIST X)` >> rw [SET_TO_LIST_INV] + >- rw [EXTENSION, QSORT_MEM] + >- ( + irule QSORT_SORTED >> + rw [Abbr `R`, relationTheory.total_def] + >- (fs [linear_order_def] >> metis_tac []) >> + fs [linear_order_def, transitive_def, relationTheory.transitive_def, + domain_def, range_def, SUBSET_DEF] >> + rw [] >> metis_tac []) + >- metis_tac [ALL_DISTINCT_SET_TO_LIST, ALL_DISTINCT_PERM, QSORT_PERM] +QED + +Definition rc_def: + rc R s = R ∪ {(x,x) | x ∈ s} +End + +Theorem rc_is_reflexive: + ∀R s. reflexive (rc R s) s +Proof + rw [rc_def, reflexive_def] +QED + +Theorem transitive_rc: + ∀R s. transitive R ⇒ transitive (rc R s) +Proof + rw [rc_def, transitive_def] >> metis_tac [] +QED + +Theorem antisym_rc: + ∀R s. antisym (rc R s) ⇔ antisym R +Proof + rw [rc_def, antisym_def] >> metis_tac [] +QED + export_theory ();