Prove that Ret preserves the invariant

Summary:
Made progress on the sanity checking lemma (that the step relation
preserves some simple invariants on the state). Proved the Ret
instruction case of the state invariant lemma. To do this, I fixed a few
bugs in the definition, and strengthened the invariants.

Reviewed By: jberdine

Differential Revision: D16786900

fbshipit-source-id: 6fa8cb170

sledge/semantics/llvmScript.sml

@@ -239,7 +239,7 @@ Definition get_offset_def:
     | None => None
     | Some off => Some (i * sizeof t + off)) ∧
   (get_offset (StrT ts) (i::is) =
-    if i < length ts then 
+    if i < length ts then
       case get_offset (el i ts) is of
       | None => None
       | Some off => Some (sum (map sizeof (take i ts)) + off)
@@ -282,7 +282,7 @@ Definition eval_def:
   (eval s (Variable v) =
     case flookup s.locals v of
     | None => <| poison := F; value := W1V 0w |>
-    | Some v => v) ∧ 
+    | Some v => v) ∧
   (eval s (Constant c) = <| poison := F; value := eval_const s.globals c |>)
 End
 
@@ -308,14 +308,14 @@ Definition interval_to_set_def:
 End
 
 Definition interval_ok_def:
-  interval_ok (_, i1, i2) ⇔
+  interval_ok ((_:bool), i1, i2) ⇔
     i1 ≤ i2 ∧ i2 < 2 ** 64
 End
 
 Definition is_allocated_def:
   is_allocated b1 allocs ⇔
     interval_ok b1 ∧
-    ∃b2. b2 ∈ allocs ∧ interval_to_set b1 ⊆ interval_to_set b2
+    ∃b2. b2 ∈ allocs ∧ fst b1 = fst b2 ∧ interval_to_set b1 ⊆ interval_to_set b2
 End
 
 Definition is_free_def:
@@ -324,23 +324,29 @@ Definition is_free_def:
     ∀b2. b2 ∈ allocs ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
 End
 
+Definition set_bytes_def:
+  (set_bytes p [] n h = h) ∧
+  (set_bytes p (b::bs) n h =
+    set_bytes p bs (Suc n) (h |+ (A n, (p, b))))
+End
+
+(* Allocate a free chunk of memory, and write non-deterministic bytes into it *)
 Inductive allocate:
-  (v2n v.value = Some m ∧
+  v2n v.value = Some m ∧
    b = (T, w2n w, w2n w + m * len) ∧
-   is_free b s.allocations
+   is_free b s.allocations ∧
+   length bytes = m * len
    ⇒
    allocate s v len
      (<| poison := v.poison; value := PtrV w |>,
-      s with allocations := { b } ∪ s.allocations))
+         s with <| allocations := { b } ∪ s.allocations;
+                   heap := set_bytes v.poison bytes (w2n w) s.heap |>)
 End
 
 Definition deallocate_def:
-  (deallocate (A n) (Some allocs) =
-    if ∃m. (T,n,m) ∈ allocs then
-      Some { (b,start,stop) | (b,start,stop) ∈ allocs ∧ start ≠ n }
-    else
-      None) ∧
-  (deallocate _ None = None)
+  deallocate addrs allocs h =
+    let to_remove = { (T, n, stop) | A n ∈ set addrs ∧ (T, n, stop) ∈ allocs } in
+      (allocs DIFF to_remove, fdiff h (image A (bigunion (image interval_to_set to_remove))))
 End
 
 Definition get_bytes_def:
@@ -406,12 +412,6 @@ Termination
   decide_tac
 End
 
-Definition set_bytes_def:
-  (set_bytes p [] n h = h) ∧
-  (set_bytes p (b::bs) n h =
-    set_bytes p bs (Suc n) (h |+ (A n, (p, b))))
-End
-
 Definition do_sub_def:
   do_sub (nuw:bool) (nsw:bool) (v1:pv) (v2:pv) =
     let (diff, u_overflow, s_overflow) =
@@ -439,7 +439,7 @@ Definition do_icmp_def:
          | (W1V w1, W1V w2) => (get_comp c) w1 w2
          | (W8V w1, W8V w2) => (get_comp c) w1 w2
          | (W32V w1, W32V w2) => (get_comp c) w1 w2
-         | (W64V w1, W64V w2) => (get_comp c) w1 w2 
+         | (W64V w1, W64V w2) => (get_comp c) w1 w2
          | (PtrV w1, PtrV w2) => (get_comp c) w1 w2) |>
 End
 
@@ -476,16 +476,17 @@ End
 Inductive step_instr:
 
   (s.stack = fr::st ∧
-   FOLDR deallocate (Some s.allocations) fr.stack_allocs = Some new_allocs
+   deallocate fr.stack_allocs s.allocations s.heap = (new_allocs, new_h)
    ⇒
    step_instr prog s
      (Ret (t, a))
      (update_result fr.result_var (eval s a)
        <| ip := fr.ret;
+          globals := s.globals;
           locals := fr.saved_locals;
           stack := st;
           allocations := new_allocs;
-          heap := heap |>)) ∧
+          heap := new_h |>)) ∧
 
 (* Do the phi assignments in parallel. The manual says "For the purposes of the
  * SSA form, the use of each incoming value is deemed to occur on the edge from
@@ -500,7 +501,7 @@ Inductive step_instr:
  *)
   (eval s a = <| poison := p; value := W1V tf |> ∧
    l = Some (if tf = 1w then l1 else l2) ∧
-   flookup prog s.ip.f = Some d ∧ 
+   flookup prog s.ip.f = Some d ∧
    flookup d.blocks l = Some <| h := Head phis None; body := b |> ∧
    map (do_phi l s) phis = map Some updates
    ⇒
@@ -542,7 +543,7 @@ Inductive step_instr:
      (inc_pc (update_result r v2 s2))) ∧
 
   (eval s a1 = <| poison := p1; value := PtrV w |> ∧
-   interval = (b, w2n w, w2n w + sizeof t) ∧
+   interval = (freeable, w2n w, w2n w + sizeof t) ∧
    is_allocated interval s.allocations ∧
    pbytes = get_bytes s.heap interval
    ⇒
@@ -553,7 +554,7 @@ Inductive step_instr:
                             s))) ∧
 
   (eval s a2 = <| poison := p2; value := PtrV w |> ∧
-   interval = (b, w2n w, w2n w + sizeof t) ∧
+   interval = (freeable, w2n w, w2n w + sizeof t) ∧
    is_allocated interval s.allocations ∧
    bytes = value_to_bytes (eval s a1).value ∧
    length bytes = sizeof t
@@ -562,7 +563,7 @@ Inductive step_instr:
      (Store (t1, a1) (t2, a2))
      (inc_pc (s with heap := set_bytes p2 bytes (w2n w) s.heap))) ∧
 
-  (map (eval s o snd) tindices = i1::indices ∧ 
+  (map (eval s o snd) tindices = i1::indices ∧
    (eval s a1).value = PtrV w1 ∧
    cast_num i1.value = Some n ∧
    map (λx. cast_num x.value) indices = map Some ns ∧
@@ -594,7 +595,7 @@ Inductive step_instr:
     (Icmp c t a1 a2)
     (inc_pc (update_result r (do_icmp c (eval s a1) (eval s a2)) s))) ∧
 
-  (flookup prog fname = Some d 
+  (flookup prog fname = Some d
    ⇒
    step_instr prog s
      (Call r t fname targs)
@@ -620,8 +621,8 @@ Inductive step_instr:
 End
 
 Inductive next_instr:
-  flookup p s.ip.f = Some d ∧ 
-  flookup d.blocks s.ip.b = Some b ∧ 
+  flookup p s.ip.f = Some d ∧
+  flookup d.blocks s.ip.b = Some b ∧
   s.ip.i < length b.body
   ⇒
   next_instr p s (el s.ip.i b.body)
@@ -642,13 +643,12 @@ Definition allocations_ok_def:
       i1 ∈ s.allocations ∧ i2 ∈ s.allocations
       ⇒
       interval_ok i1 ∧ interval_ok i2 ∧
-      (interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒
-       interval_to_set i1 = interval_to_set i2)
+      (interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2)
 End
 
 Definition heap_ok_def:
   heap_ok s ⇔
-    ∀i n. i ∈ s.allocations ∧ n ∈ interval_to_set i ⇒ flookup s.heap (A n) ≠ None
+    ∀n. flookup s.heap (A n) ≠ None ⇔ ∃i. i ∈ s.allocations ∧ n ∈ interval_to_set i
 End
 
 Definition globals_ok_def:
@@ -675,7 +675,7 @@ Definition is_init_state_def:
       flookup s.globals g = Some (n, w) ∧ flookup global_init g = Some (t,v) ⇒
       ∃bytes.
         get_bytes s.heap (F, w2n w, w2n w + sizeof t) = map (λb. (F,b)) bytes ∧
-        bytes_to_value t bytes = (v, []) 
+        bytes_to_value t bytes = (v, [])
 End
 
 (* ----- Invariants on state ----- *)
@@ -698,11 +698,12 @@ Definition frame_ok_def:
   frame_ok p s f ⇔
     ip_ok p f.ret ∧
     every (λn. ∃start stop. n = A start ∧ (T, start, stop) ∈ s.allocations) f.stack_allocs
-End    
+End
 
 Definition stack_ok_def:
   stack_ok p s ⇔
-    every (frame_ok p s) s.stack
+    every (frame_ok p s) s.stack ∧
+    all_distinct (flat (map (λf. f.stack_allocs) s.stack))
 End
 
 Definition state_invariant_def:

sledge/semantics/llvm_propScript.sml

@@ -9,6 +9,7 @@
 
 open HolKernel boolLib bossLib Parse;
 open pairTheory listTheory rich_listTheory arithmeticTheory wordsTheory;
+open pred_setTheory finite_mapTheory;
 open logrootTheory numposrepTheory;
 open settingsTheory llvmTheory;
 
@@ -76,13 +77,21 @@ Proof
   Induct >> rw [] >> Cases_on `l2` >> fs []
 QED
 
+Theorem flookup_fdiff:
+  ∀m s k.
+    flookup (fdiff m s) k =
+      if k ∈ s then None else flookup m k
+Proof
+  rw [FDIFF_def, FLOOKUP_DRESTRICT] >> fs []
+QED
+
 (* ----- Theorems about log ----- *)
 
 (* Could be upstreamed to HOL *)
 Theorem mul_div_bound:
   ∀m n. n ≠ 0 ⇒ m - (n - 1) ≤ n * (m DIV n) ∧ n * (m DIV n) ≤ m
 Proof
-  rw [] >> 
+  rw [] >>
   `0 < n` by decide_tac >>
   drule DIVISION >> disch_then (qspec_then `m` mp_tac) >>
   decide_tac
@@ -194,7 +203,7 @@ Theorem b2v_size:
     ∃vs. read_str ts bs = (vs, drop (sum (map sizeof ts)) bs))
 Proof
   ho_match_mp_tac bytes_to_value_ind >>
-  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >> 
+  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
   fs [first_class_type_def]
   >- (simp [PAIR_MAP] >> metis_tac [SND])
   >- (
@@ -220,22 +229,22 @@ Theorem b2v_append:
     ∃vs. read_str ts (bs ++ bs') = (I ## (λx. x ++ bs')) (read_str ts bs))
 Proof
   ho_match_mp_tac bytes_to_value_ind >>
-  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >> 
+  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
   fs [first_class_type_def, TAKE_APPEND, DROP_APPEND,
       DECIDE ``!x y. x ≤ y ⇒ x - y = 0n``, ETA_THM]
   >- (simp [PAIR_MAP] >> metis_tac [SND])
   >- (simp [PAIR_MAP] >> metis_tac [SND])
   >- (
-    rpt (pairarg_tac >> simp []) >> fs [ADD1] >> 
+    rpt (pairarg_tac >> simp []) >> fs [ADD1] >>
     BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
     first_x_assum irule >>
-    `sizeof t ≤ length bs` by decide_tac >> 
+    `sizeof t ≤ length bs` by decide_tac >>
     imp_res_tac b2v_smaller >> rfs [])
   >- (
-    rpt (pairarg_tac >> simp []) >> fs [ADD1] >> 
+    rpt (pairarg_tac >> simp []) >> fs [ADD1] >>
     BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
     first_x_assum irule >>
-    `sizeof t ≤ length bs` by decide_tac >> 
+    `sizeof t ≤ length bs` by decide_tac >>
     imp_res_tac b2v_smaller >> rfs [])
 QED
 
@@ -323,7 +332,7 @@ Proof
   simp [TAKE_TAKE_MIN] >>
   `length l = n` by simp [Abbr `l`] >>
   `length (dropWhile ($= 0) (reverse l)) ≤ n`
-  by metis_tac [LESS_EQ_TRANS, LENGTH_dropWhile_LESS_EQ, LENGTH_REVERSE] >> 
+  by metis_tac [LESS_EQ_TRANS, LENGTH_dropWhile_LESS_EQ, LENGTH_REVERSE] >>
   rw [MIN_DEF] >> fs []
   >- (
     simp [TAKE_APPEND, TAKE_TAKE_MIN, MIN_DEF, take_replicate] >>
@@ -345,7 +354,7 @@ Proof
     REWRITE_TAC [GSYM w2n_11, word_0_n2w] >>
     simp [])
   >- rw [TAKE_APPEND, TAKE_TAKE]
-QED 
+QED
 
 Theorem b2v_v2b:
   ∀v t bs. value_type t v ⇒ bytes_to_value t (value_to_bytes v ++ bs) = (v, bs)
@@ -427,7 +436,7 @@ Theorem extract_insertvalue:
     insert_value v1 v2 indices = Some v3
     ⇒
     extract_value v3 indices = Some v2
-Proof 
+Proof
   recInduct insert_value_ind >> rw [insert_value_def, extract_value_def] >>
   pop_assum mp_tac >> CASE_TAC >> fs [] >> rfs [] >>
   rw [] >> simp [extract_value_def, EL_LUPDATE]
@@ -439,7 +448,7 @@ Theorem extract_insertvalue_other:
     ¬(indices1 ≼ indices2) ∧ ¬(indices2 ≼ indices1)
     ⇒
     extract_value v3 indices2 = extract_value v1 indices2
-Proof 
+Proof
   recInduct insert_value_ind >> rw [insert_value_def, extract_value_def] >>
   qpat_x_assum `_ = SOME _` mp_tac >> CASE_TAC >> rw [] >> rfs [] >>
   qpat_x_assum `¬case _ of [] => F | h::t => P h t` mp_tac >>
@@ -452,7 +461,7 @@ Theorem insert_extractvalue:
     extract_value v1 indices = Some v2
     ⇒
     insert_value v1 v2 indices = Some v1
-Proof 
+Proof
   recInduct extract_value_ind >> rw [insert_value_def, extract_value_def] >> fs [] >>
   rw [LUPDATE_SAME]
 QED
@@ -476,7 +485,7 @@ Definition extract_type_def:
   (extract_type (StrT ts) (i::idx) =
     if i < length ts then
       extract_type (el i ts) idx
-    else 
+    else
       None) ∧
   (extract_type _ _ = None)
 End
@@ -621,11 +630,87 @@ Proof
       globals_ok_def, stack_ok_def, heap_ok_def, EVERY_EL, frame_ok_def]
 QED
 
+Theorem flookup_set_bytes:
+  ∀poison bytes n h n'.
+    flookup (set_bytes poison bytes n h) (A n') =
+      if n ≤ n' ∧ n' < n + length bytes then
+        Some (poison, el (n' - n) bytes)
+      else
+        flookup h (A n')
+Proof
+  Induct_on `bytes` >> rw [set_bytes_def, EL_CONS, PRE_SUB1] >>
+  fs [ADD1, FLOOKUP_UPDATE] >>
+  `n = n'` by decide_tac >>
+  rw []
+QED
+
+Theorem allocate_invariant:
+  ∀p s1 v1 t v2 s2.
+    state_invariant p s1 ∧ allocate s1 v1 t (v2,s2) ⇒ state_invariant p s2
+Proof
+  rw [allocate_cases, state_invariant_def, ip_ok_def, heap_ok_def,
+      globals_ok_def, stack_ok_def] >>
+  rw [] >> fs []
+  >- (
+    fs [allocations_ok_def] >> rpt gen_tac >> disch_tac >> fs [is_free_def] >> rw [] >>
+    metis_tac [INTER_COMM])
+  >- (
+    rw [flookup_set_bytes]
+    >- rw [RIGHT_AND_OVER_OR, EXISTS_OR_THM, interval_to_set_def] >>
+    eq_tac >> rw [] >> fs [interval_to_set_def] >>
+    metis_tac [])
+  >- (fs [is_allocated_def] >> metis_tac [])
+  >- (fs [EVERY_EL, frame_ok_def] >> rw [] >> metis_tac [])
+QED
+
+Theorem set_bytes_invariant:
+  ∀s poison bytes n prog b.
+    state_invariant prog s ∧ is_allocated (b, n, n + length bytes) s.allocations
+    ⇒
+    state_invariant prog (s with heap := set_bytes poison bytes n s.heap)
+Proof
+  rw [state_invariant_def]
+  >- (fs [allocations_ok_def] >> rw [] >> metis_tac [])
+  >- (
+    fs [heap_ok_def, flookup_set_bytes] >> rw [] >>
+    fs [is_allocated_def, interval_to_set_def, SUBSET_DEF] >>
+    metis_tac [LESS_EQ_REFL, DECIDE ``!x y. x < x + SUC y``])
+  >- (fs [globals_ok_def] >> metis_tac [])
+  >- (fs [stack_ok_def, EVERY_EL, frame_ok_def])
+QED
+
 Theorem step_instr_invariant:
-  ∀i s2. step_instr p s1 i s2 ⇒ prog_ok p ∧ next_instr p s1 i ∧ state_invariant p s1 ⇒ state_invariant p s2
+  ∀i s2.
+    step_instr p s1 i s2 ⇒ prog_ok p ∧ next_instr p s1 i ∧ state_invariant p s1
+    ⇒
+    state_invariant p s2
 Proof
   ho_match_mp_tac step_instr_ind >> rw []
-  >- cheat
+  >- (
+    rw [update_invariant] >> fs [state_invariant_def] >> rw []
+    >- (
+      fs [stack_ok_def] >> rfs [EVERY_EL, frame_ok_def] >>
+      first_x_assum (qspec_then `0` mp_tac) >> simp [])
+    >- (fs [deallocate_def, allocations_ok_def] >> rw [] >> metis_tac [])
+    >- (
+      fs [deallocate_def, heap_ok_def] >> rw [flookup_fdiff] >>
+      eq_tac >> rw []
+      >- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE]
+      >- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE] >>
+      fs [allocations_ok_def, stack_ok_def, EXTENSION] >> metis_tac [])
+    >- (
+      fs [globals_ok_def, deallocate_def] >> rw [] >>
+      first_x_assum drule >> rw [] >> fs [is_allocated_def] >>
+      qexists_tac `b2` >> rw [] >> CCONTR_TAC >> fs [])
+    >- (
+      fs [stack_ok_def, EVERY_MEM, frame_ok_def, deallocate_def] >> rfs [] >>
+      rw []
+      >- (
+        res_tac >> rw [] >> qexists_tac `stop` >> rw [] >>
+        fs [ALL_DISTINCT_APPEND, MEM_FLAT, MEM_MAP] >>
+        metis_tac [])
+      >- (
+        fs [ALL_DISTINCT_APPEND])))
   >- cheat
   >- cheat
   >- (
@@ -640,7 +725,7 @@ Proof
   >- (
     (* Allocation *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
-    >- cheat
+    >- metis_tac [allocate_invariant]
     >- (fs [next_instr_cases, allocate_cases] >> metis_tac [terminator_def]))
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
@@ -649,7 +734,7 @@ Proof
   >- (
     (* Store *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
-    >- cheat
+    >- (irule set_bytes_invariant >> rw [] >> metis_tac [])
     >- (fs [next_instr_cases] >> metis_tac [terminator_def]))
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>

sledge/semantics/settingsScript.sml

@@ -29,6 +29,7 @@ overload_on ("el", ``EL``);
 overload_on ("count_list", ``COUNT_LIST``);
 overload_on ("Suc", ``SUC``);
 overload_on ("flat", ``FLAT``);
+overload_on ("all_distinct", ``ALL_DISTINCT``);
 overload_on ("take", ``TAKE``);
 overload_on ("drop", ``DROP``);
 overload_on ("replicate", ``REPLICATE``);
@@ -42,5 +43,10 @@ overload_on ("option_join", ``OPTION_JOIN``);
 overload_on ("min", ``MIN``);
 overload_on ("list_update", ``LUPDATE``);
 overload_on ("last", ``LAST``);
+overload_on ("fdiff", ``FDIFF``);
+overload_on ("image", ``IMAGE``);
+overload_on ("bigunion", ``BIGUNION``);
+overload_on ("finite", ``FINITE``);
+overload_on ("card", ``CARD``);
 
 export_theory ();