[sledge sem] Improve and unify treatment of Exit

Summary: Add an argument to the Exit instruction. Update the LLVM semantics to execute the Exit instruction and store the result in an "exited" component of the state. (Previously it just noticed that it was stuck about to do an Exit.) With exiting treated uniformly, now in the proof that for every LLVM trace, there is a llair trace that simulates it, all of the cheats except for 1 are just cases that I haven't got to yet. However, the last cheat is for the situation where the LLVM program gets stuck and the llair program doesn't. For example, the following two line LLVM program gets stuck because r2 is not assigned (ignoring for the moment the static restriction that LLVM is in SSA form). r1 := r2 Exit(0) The compilation to llair omits the assignment and so we get a llair program that doesn't get stuck: Exit(0) The key question is whether the static restrictions are sufficient to ensure that no expression that might be omitted can get stuck. Reviewed By: jberdine Differential Revision: D17737589 fbshipit-source-id: bc6c01a1b
5 years ago · 14a8ae34b9
parent 5312b3d10c
commit 14a8ae34b9
7 changed files with 80 additions and 41 deletions
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@ -94,7 +94,7 @@ Datatype:
  | Return exp
  | Throw exp
  | Unreachable
-  | Exit
+  | Exit exp
 End

 Datatype:
@ -473,7 +473,10 @@ Inductive step_term:
        stack := rest;
        heap := s.heap |>) ∧

-  (∀prog s. step_term prog s Exit (s with status := Complete))
+  (∀prog s e i size.
+   eval_exp s e (FlatV (IntV i size))
+   ⇒
+   step_term prog s (Exit e) (s with status := Complete i))
  (* TODO Throw *)

 End
@ -487,7 +490,6 @@ Inductive step_block:
   ⇒
   step_block prog s1 [] [] t s2) ∧

-
  (∀prog s1 i1 i2 l1 is t s2.
   step_inst s1 i1 l1 s2 ∧
   (¬?l2 s3. step_inst s2 i2 l2 s3)
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@ -90,7 +90,7 @@ Datatype:
  | Br arg label label
  | Invoke reg ty arg (targ list) label label
  | Unreachable
-  | Exit
+  | Exit arg
  (* Non-terminators *)
  | Sub reg bool bool ty arg arg
  | Extractvalue reg targ (const list)
@ -144,7 +144,7 @@ Definition terminator_def:
  (terminator (Br _ _ _) ⇔ T) ∧
  (terminator (Invoke _ _ _ _ _ _) ⇔ T) ∧
  (terminator Unreachable ⇔ T) ∧
-  (terminator Exit ⇔ T) ∧
+  (terminator (Exit _) ⇔ T) ∧
  (terminator (Cxa_throw _ _ _) ⇔ T) ∧
  (terminator _ ⇔ F)
 End
@ -196,7 +196,8 @@ Datatype:
       globals : glob_var |-> (num # word64);
       locals : reg |-> pv;
       stack : frame list;
-       heap : bool heap |>
+       heap : bool heap;
+       exited : int option |>
 End

 (* ----- Things about types ----- *)
@ -524,6 +525,13 @@ Inductive step_instr:
  (* TODO *)
  (step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧

+  (eval s a = Some v1 ∧
+  signed_v_to_int v1.value = Some exit_code
+   ⇒
+   step_instr prog s
+     (Exit a) Tau
+     (s with exited := Some (exit_code))) ∧
+
  (eval s a1 = Some v1 ∧
   eval s a2 = Some v2 ∧
   do_sub nuw nsw v1 v2 t = Some v3
@ -677,6 +685,7 @@ End

 Inductive step:
 (get_instr p s.ip (Inl i) ∧
+  s.exited = None ∧
  step_instr p s i l s'
  ⇒
  step p s l s') ∧
@ -693,6 +702,7 @@ Inductive step:
 * %r1 = phi [0, %l]
 *)
 (get_instr p s.ip (Inr (from_l, phis)) ∧
+  s.exited = None ∧
  map (do_phi from_l s) phis = map Some updates
  ⇒
  step p s Tau (inc_pc (s with locals := locals |++ updates)))
@ -701,8 +711,8 @@ End

 Definition get_observation_def:
  get_observation prog last_s =
-    if get_instr prog last_s.ip (Inl Exit) then
-      Complete
+    if last_s.exited ≠ None then
+      Complete (THE last_s.exited)
    else if ∃s l. step prog last_s l s then
      Partial
    else
@ -799,6 +809,7 @@ Definition is_init_state_def:
    s.ip.i = Offset 0 ∧
    s.locals = fempty ∧
    s.stack = [] ∧
+    s.exited = None ∧
    globals_ok s ∧
    heap_ok s.heap ∧
    fdom s.globals = fdom global_init ∧
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@ -427,6 +427,10 @@ Proof
      metis_tac [])
    >- (fs [globals_ok_def] >> metis_tac [])
    >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
+  >- (
+    fs [state_invariant_def, globals_ok_def, stack_ok_def, frame_ok_def,
+        EVERY_MEM] >>
+    metis_tac [])
  >- (
    irule inc_pc_invariant >> rw [get_instr_update, update_invariant]>>
    metis_tac [terminator_def])
@ -495,13 +499,9 @@ Proof
 QED

 Theorem exit_no_step:
-  !p s1. get_instr p s1.ip (Inl Exit) ⇒ ¬?l s2. step p s1 l s2
+  !p s1. s1.exited ≠ None ⇒ ¬?l s2. step p s1 l s2
 Proof
  rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``]
-  >- (
-    `i = Exit` by metis_tac [get_instr_func, sumTheory.INL_11] >>
-    rw [step_instr_cases]) >>
-  metis_tac [get_instr_func, sumTheory.sum_distinct]
 QED

 Definition is_call_def:
--- a/sledge/semantics/llvm_ssaScript.sml
+++ b/sledge/semantics/llvm_ssaScript.sml
@ -31,7 +31,7 @@ Definition instr_next_ips_def:
  (instr_next_ips (Invoke _ _ _ _ l1 l2) ip =
    { <| f := ip.f; b := Some l; i := Phi_ip ip.b |> | l | l ∈ {l1; l2} }) ∧
  (instr_next_ips Unreachable ip = {}) ∧
-  (instr_next_ips Exit ip = {}) ∧
+  (instr_next_ips (Exit _) ip = {}) ∧
  (instr_next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧
  (instr_next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧
  (instr_next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@ -219,7 +219,7 @@ Definition classify_instr_def:
  (classify_instr (Br _ _ _) = Term) ∧
  (classify_instr (Invoke _ _ _ _ _ _) = Term) ∧
  (classify_instr Unreachable = Term) ∧
-  (classify_instr Exit = Term) ∧
+  (classify_instr (Exit _) = Term) ∧
  (classify_instr (Load _ _ _) = Non_exp) ∧
  (classify_instr (Store _ _) = Non_exp) ∧
  (classify_instr (Cxa_throw _ _ _) = Non_exp) ∧
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@ -74,6 +74,12 @@ Definition untranslate_reg_def:
  untranslate_reg (Var_name x t) = Reg x
 End

+Inductive complete_trace_rel:
+  (∀i. complete_trace_rel (Some i) (Complete i)) ∧
+  (complete_trace_rel None Partial) ∧
+  (complete_trace_rel None Stuck)
+End
+
 (* Define when an LLVM state is related to a llair one.
 * Parameterised on a map for locals relating LLVM registers to llair
 * expressions that compute the value in that register. This corresponds to part
@ -94,7 +100,7 @@ Definition mem_state_rel_def:
          ∃ip2. untranslate_reg r' ∈ assigns prog ip2 ∧ dominates prog ip2 ip1))) ∧
    reachable prog s.ip ∧
    erase_tags s.heap = s'.heap ∧
-    s'.status = get_observation prog s
+    complete_trace_rel s.exited s'.status
 End

 (* Define when an LLVM state is related to a llair one
@ -105,7 +111,8 @@ End
 Definition state_rel_def:
  state_rel prog emap (s:llvm$state) (s':llair$state) ⇔
    pc_rel prog emap s.ip s'.bp ∧
-    mem_state_rel prog emap s s'
+    mem_state_rel prog emap s s' ∧
+    s'.status = get_observation prog s
 End

 Theorem mem_state_ignore_bp:
@ -132,7 +139,6 @@ Proof
    first_x_assum (qspec_then `r` mp_tac) >> simp [Once live_gen_kill, PULL_EXISTS] >>
    metis_tac [next_ips_same_func])
  >- metis_tac [next_ips_reachable]
-  >- cheat
 QED

 Theorem mem_state_rel_update:
@ -170,7 +176,6 @@ Proof
    simp [Once live_gen_kill, PULL_EXISTS, METIS_PROVE [] ``x ∨ y ⇔ (~y ⇒ x)``] >>
    metis_tac [])
  >- metis_tac [next_ips_reachable]
-  >- cheat
 QED

 Theorem mem_state_rel_update_keep:
@ -224,7 +229,6 @@ Proof
      first_x_assum irule >> rw [] >>
      metis_tac [next_ips_same_func]))
  >- metis_tac [next_ips_reachable]
-  >- cheat
 QED

 Theorem v_rel_bytes:
@ -267,6 +271,7 @@ Proof
    simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
    fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
    metis_tac [])
+  (* TODO: unimplemented stuff *)
  >- cheat
  >- cheat
  >- cheat
@ -290,6 +295,7 @@ Proof
  TRY pairarg_tac >> fs []
  >- metis_tac []
  >- metis_tac [] >>
+  (* TODO: unimplemented stuff *)
  cheat
 QED

@ -488,8 +494,7 @@ QED

 Theorem translate_instr_to_exp_correct:
  ∀emap instr r t s1 s1' s2 prog l.
-    is_ssa prog ∧
-    prog_ok prog ∧
+    is_ssa prog ∧ prog_ok prog ∧
    classify_instr instr = Exp r t ∧
    mem_state_rel prog emap s1 s1' ∧
    get_instr prog s1.ip (Inl instr) ∧
@ -528,17 +533,18 @@ Proof
    >- (
      simp [step_inst_cases, PULL_EXISTS] >>
      qexists_tac `res_v` >> rw []
-      >- simp [inc_pc_def, llvmTheory.inc_pc_def] >>
-      rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
-      simp [llvmTheory.inc_pc_def] >>
-      irule mem_state_rel_update_keep >> rw []
-      >- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
+      >- simp [inc_pc_def, llvmTheory.inc_pc_def]
      >- (
-        drule prog_ok_nonterm >>
-        simp [get_instr_cases, PULL_EXISTS] >>
-        ntac 3 (disch_then drule) >>
-        simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def])
-      >- fs [mem_state_rel_def])
+        rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
+        simp [llvmTheory.inc_pc_def] >>
+        irule mem_state_rel_update_keep >> rw []
+        >- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
+        >- (
+          drule prog_ok_nonterm >>
+          simp [get_instr_cases, PULL_EXISTS] >>
+          ntac 3 (disch_then drule) >>
+          simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def])
+        >- fs [mem_state_rel_def]))
    >- rw [inc_pc_def, llvmTheory.inc_pc_def]
    >- (
      simp [llvmTheory.inc_pc_def] >>
@ -580,6 +586,7 @@ Proof
      simp [step_inst_cases, PULL_EXISTS] >>
      qexists_tac `res_v` >> rw [] >>
      rw [update_results_def] >>
+      (* TODO: unfinished *)
      cheat)
    >- cheat) >>
  conj_tac
@ -611,6 +618,7 @@ Proof
      simp [step_inst_cases, PULL_EXISTS] >>
      qexists_tac `res_v` >> rw [] >>
      rw [update_results_def] >>
+      (* TODO: unfinished *)
      cheat)
    >- cheat) >>
  cheat
@ -741,6 +749,17 @@ Proof
  metis_tac [un_translate_glob_inv]
 QED

+Theorem take_to_call_lem:
+  ∀i idx body.
+    idx < length body ∧ el idx body = i ∧ ¬terminator i ∧ ¬is_call i ⇒
+    take_to_call (drop idx body) = i :: take_to_call (drop (idx + 1) body)
+Proof
+  Induct_on `idx` >> rw []
+  >- (Cases_on `body` >> fs [take_to_call_def] >> rw []) >>
+  Cases_on `body` >> fs [] >>
+  first_x_assum drule >> simp [ADD1]
+QED
+
 Theorem translate_instrs_correct1:
  ∀prog s1 tr s2.
    multi_step prog s1 tr s2 ⇒
@ -839,8 +858,9 @@ Proof
              `s1'.locals = s3.locals` by fs [Abbr `s3`] >>
              metis_tac [eval_exp_ignores]))
          >- cheat
-          >- (
-            cheat)))
+          >- cheat)
+        >- (
+          cheat))
      >- ( (* Invoke *)
        cheat)
      >- ( (* Unreachable *)
@ -872,7 +892,9 @@ Proof
      rename1 `state_rel prog emap3 s3 s3'` >>
      qexists_tac `emap3` >> qexists_tac `s3'` >> rw [] >>
      `take_to_call (drop idx b.body) = i :: take_to_call (drop (idx + 1) b.body)`
-      by cheat >>
+      by (
+        irule take_to_call_lem >> simp [] >>
+        fs [get_instr_cases]) >>
      simp [translate_instrs_def] >>
      Cases_on `r ∉ regs_to_keep` >> fs [] >> rw []
      >- metis_tac [] >>
@ -898,6 +920,7 @@ Theorem multi_step_to_step_block:
 Proof
  rw [] >> pop_assum mp_tac >> simp [Once state_rel_def] >> rw [pc_rel_cases]
  >- (
+    (* Non-phi instruction *)
    drule translate_instrs_correct1 >> simp [] >>
    disch_then drule >>
    disch_then (qspecl_then [`regs_to_keep`, `types`] mp_tac) >> simp [] >>
@ -905,13 +928,14 @@ Proof
    qexists_tac `s2'` >> simp [] >>
    ntac 3 HINT_EXISTS_TAC >>
    rw [] >> fs [dest_fn_def]) >>
-  (* Phi nodes *)
+  (* Phi instruction *)
  reverse (fs [Once multi_step_cases])
  >- metis_tac [get_instr_func, sumTheory.sum_distinct] >>
  qpat_x_assum `last_step _ _ _ _` mp_tac >>
  simp [last_step_def] >> simp [Once llvmTheory.step_cases] >>
  rw [] >> imp_res_tac get_instr_func >> fs [] >> rw [] >>
  fs [translate_trace_def] >>
+  (* TODO: unfinished *)
  cheat
 QED

@ -1027,7 +1051,11 @@ Proof
    >- rw [MAP_MAP_o, combinTheory.o_DEF, un_translate_trace_inv] >>
    qexists_tac `path'` >> rw [] >>
    fs [IN_DEF, observation_prefixes_cases, toList_some] >> rw [] >>
-    `?labs. labels path' = fromList labs` by cheat >>
+    `?labs. labels path' = fromList labs`
+    by (
+      fs [GSYM finite_labels] >>
+      imp_res_tac llistTheory.LFINITE_toList >>
+      fs [toList_some]) >>
    fs [] >>
    rfs [lmap_fromList, combinTheory.o_DEF, MAP_MAP_o] >>
    simp [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF, FILTER_MAP]
@ -1035,8 +1063,6 @@ Proof
    >- fs [state_rel_def, mem_state_rel_def] >>
    rename [`labels path' = fromList l'`, `labels path = fromList l`,
            `state_rel _ _ (last path) (last path')`, `lsub ≼ flat l`] >>
-    qexists_tac `map (translate_trace types) lsub` >>
-    fs [FILTER_MAP, trans_trace_not_tau] >>
    cheat)
 (*
    `INJ (translate_trace types) (set l2' ∪ set (flat l2)) UNIV`
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@ -30,12 +30,12 @@ End
 Datatype:
  trace_type =
  | Stuck
-  | Complete
+  | Complete int
  | Partial
 End

 Inductive observation_prefixes:
-  (∀l. observation_prefixes (Complete, l) (Complete, filter ($≠ Tau) l)) ∧
+  (∀l i. observation_prefixes (Complete i, l) (Complete i, filter ($≠ Tau) l)) ∧
  (∀l. observation_prefixes (Stuck, l) (Stuck, filter ($≠ Tau) l)) ∧
  (∀l1 l2 x.
    l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)