[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

@@ -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.
+      every (\(fname,dec). all_distinct (map fst dec.blocks)) p) ∧
-       alookup p fname = Some dec ⇒
-       all_distinct (map fst dec.blocks)) ∧
      (* 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

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:

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_tac std_ss [good_path_append, GSYM APPEND] >> rw []
-            rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >>
+            >- (rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >> metis_tac [])
-            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] >>

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 ();