From 89c3da4510910fd0d386ac8a90ca578e006dd605 Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Wed, 14 Aug 2019 06:58:09 -0700 Subject: [PATCH] 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 | 71 ++++++++-------- sledge/semantics/llvm_propScript.sml | 119 +++++++++++++++++++++++---- sledge/semantics/settingsScript.sml | 6 ++ 3 files changed, 144 insertions(+), 52 deletions(-) diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml index 4d101c27a..48006eed2 100644 --- a/sledge/semantics/llvmScript.sml +++ b/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: diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml index 5d6fff5c0..3c58d1b2e 100644 --- a/sledge/semantics/llvm_propScript.sml +++ b/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] >> diff --git a/sledge/semantics/settingsScript.sml b/sledge/semantics/settingsScript.sml index d22722c9e..af03c3ef6 100644 --- a/sledge/semantics/settingsScript.sml +++ b/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 ();