pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge semantics] Refactor the memory model

Browse Source 
Summary:
LLVM and llair have similar memory models, and we don't want to
duplicate any definitions or theorems. This adds a new memory model
theory which should be understandable in its own right. A heap is a
mapping from addresses to bytes, alongside a set of valid addresses, and
intervals that have been allocated already. Primitives are defined for
allocating and de-allocating as well as reading and writing chuncks of
bytes.

There is also a generic type of structured values, and functions for
converting them to/from byte arrays.

Reviewed By: jberdine

Differential Revision: D17074470

fbshipit-source-id: bdab6089f
master
Scott Owens 5 years ago committed by Facebook Github Bot
parent 28e84f275e
commit 9f44bbc264
6 changed files with 973 additions and 671 deletions
Show Stats Download Patch File Download Diff File

24
sledge/semantics/llairScript.sml
Unescape View File

@ -8,7 +8,7 @@
(* A mini-LLAIR model, based on the files in sledge/src/llair *)
open HolKernel boolLib bossLib Parse;
open settingsTheory;
open settingsTheory memory_modelTheory;
new_theory "llair";
@ -120,25 +120,19 @@ End
(* ----- Semantic states ----- *)
(* TODO Given the similarities with LLVM, consider moving some definitions into
* a common predecessor theory *)
Datatype:
addr = A num
End
(* These are the values that can be stored in registers. The implementation uses
* integers with a bit-width to represent numbers, and keeps locations and sizes
* separate.
*)
Datatype:
v =
flat_v =
| LocV num
| SizeV num
| IntV int num
| AggV (v list)
End
Type v = ``:flat_v reg_v``
Datatype:
pc = <| l : label; i : num |>
End
@ -153,15 +147,7 @@ Datatype:
globals : var |-> word64;
locals : var |-> v;
stack : frame list;
(* The set of allocated ranges.
* The llvm model had a bool to indicate whether the range is free-able
* or not, since the memory that the globals is in should never be freed.
* llair does not currently catch this error, so we won't either. If
* llair wants to catch the error in the future, then we can adapt the
* semantics. *)
allocations : (num # num) set;
(* A byte addressed heap *)
heap : addr |-> word8 |>
heap : unit heap |>
End
(* ----- Semantic transitions ----- *)

353
sledge/semantics/llvmScript.sml
Unescape View File

@ -9,7 +9,7 @@
* are relevant for the LLVM -> LLAIR translation, especially exceptions. *)
open HolKernel boolLib bossLib Parse;
open settingsTheory;
open settingsTheory memory_modelTheory;
new_theory "llvm";
@ -137,20 +137,17 @@ End
(* ----- Semantic states ----- *)
Datatype:
addr = A num
End
Datatype:
v =
flat_v =
| W1V word1
| W8V word8
| W32V word32
| W64V word64
| AggV (v list)
| PtrV word64
| UndefV
End
Type v = ``:flat_v reg_v``
Datatype:
pv = <| poison : bool; value : v |>
End
@ -170,11 +167,7 @@ Datatype:
globals : glob_var |-> (num # word64);
locals : reg |-> pv;
stack : frame list;
(* The set of allocated ranges. The bool indicates whether the range is
* free-able or not *)
allocations : (bool # num # num) set;
(* A byte addressed heap, with a poison tag *)
heap : addr |-> bool # word8 |>
heap : bool heap |>
End
(* ----- Things about types ----- *)
@ -217,11 +210,11 @@ Definition indices_ok_def:
End
Inductive value_type:
(value_type (IntT W1) (W1V w1)) ∧
(value_type (IntT W8) (W8V w8)) ∧
(value_type (IntT W32) (W32V w32)) ∧
(value_type (IntT W64) (W64V w64)) ∧
(value_type (PtrT _) (PtrV w64)) ∧
(value_type (IntT W1) (FlatV (W1V w1))) ∧
(value_type (IntT W8) (FlatV (W8V w8))) ∧
(value_type (IntT W32) (FlatV (W32V w32))) ∧
(value_type (IntT W64) (FlatV (W64V w64))) ∧
(value_type (PtrT _) (FlatV (PtrV w64))) ∧
(every (value_type t) vs ∧ length vs = n ∧ first_class_type t
⇒
value_type (ArrT n t) (AggV vs)) ∧
@ -230,30 +223,19 @@ Inductive value_type:
value_type (StrT ts) (AggV vs))
End
(* ----- Semantic transitions ----- *)
Definition w64_cast_def:
(w64_cast w (IntT W1) = Some (W1V (w2w w))) ∧
(w64_cast w (IntT W8) = Some (W8V (w2w w))) ∧
(w64_cast w (IntT W32) = Some (W32V (w2w w))) ∧
(w64_cast w (IntT W64) = Some (W64V w)) ∧
(w64_cast _ _ = None)
End
Definition cast_w64_def:
(cast_w64 (W1V w) = Some (w2w w)) ∧
(cast_w64 (W8V w) = Some (w2w w)) ∧
(cast_w64 (W32V w) = Some (w2w w)) ∧
(cast_w64 (W64V w) = Some w) ∧
(cast_w64 _ = None)
End
Definition cast_num_def:
cast_num v = option_map w2n (cast_w64 v)
End
Definition bool_to_v_def:
bool_to_v b = if b then W1V 1w else W1V 0w
Definition extract_type_def:
(extract_type t [] = Some t) ∧
(extract_type (ArrT n t) (i::idx) =
if i < n then
extract_type t idx
else
None) ∧
(extract_type (StrT ts) (i::idx) =
if i < length ts then
extract_type (el i ts) idx
else
None) ∧
(extract_type _ _ = None)
End
(* Calculate the offset given by a list of indices *)
@ -273,26 +255,52 @@ Definition get_offset_def:
(get_offset _ _ = Some 0)
End
(* ----- Semantic transitions ----- *)
Definition w64_cast_def:
(w64_cast w (IntT W1) = Some (FlatV (W1V (w2w w)))) ∧
(w64_cast w (IntT W8) = Some (FlatV (W8V (w2w w)))) ∧
(w64_cast w (IntT W32) = Some (FlatV (W32V (w2w w)))) ∧
(w64_cast w (IntT W64) = Some (FlatV (W64V w))) ∧
(w64_cast _ _ = None)
End
Definition cast_w64_def:
(cast_w64 (FlatV (W1V w)) = Some (w2w w)) ∧
(cast_w64 (FlatV (W8V w)) = Some (w2w w)) ∧
(cast_w64 (FlatV (W32V w)) = Some (w2w w)) ∧
(cast_w64 (FlatV (W64V w)) = Some w) ∧
(cast_w64 _ = None)
End
Definition cast_num_def:
cast_num v = option_map w2n (cast_w64 v)
End
Definition bool_to_v_def:
bool_to_v b = if b then FlatV (W1V 1w) else FlatV (W1V 0w)
End
Definition eval_const_def:
(eval_const g (IntC W1 i) = W1V (i2w i)) ∧
(eval_const g (IntC W8 i) = W8V (i2w i)) ∧
(eval_const g (IntC W32 i) = W32V (i2w i)) ∧
(eval_const g (IntC W64 i) = W64V (i2w i)) ∧
(eval_const g (IntC W1 i) = FlatV (W1V (i2w i))) ∧
(eval_const g (IntC W8 i) = FlatV (W8V (i2w i))) ∧
(eval_const g (IntC W32 i) = FlatV (W32V (i2w i))) ∧
(eval_const g (IntC W64 i) = FlatV (W64V (i2w i))) ∧
(eval_const g (StrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
(eval_const g (ArrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
(eval_const g (GepC ty ptr (t, idx) indices) =
case (eval_const g ptr, cast_num (eval_const g idx)) of
| (PtrV w, Some n) =>
| (FlatV (PtrV w), Some n) =>
let ns = map (λ(t,ci). case cast_num (eval_const g ci) of None => 0 | Some n => n) indices in
(case get_offset ty ns of
| None => UndefV
| Some off => PtrV (n2w (w2n w + sizeof ty * n + off)))
| _ => UndefV) ∧
| None => FlatV UndefV
| Some off => FlatV (PtrV (n2w (w2n w + sizeof ty * n + off))))
| _ => FlatV UndefV) ∧
(eval_const g (GlobalC var) =
case flookup g var of
| None => PtrV 0w
| Some (s,w) => PtrV w) ∧
(eval_const g UndefC = UndefV)
| None => FlatV (PtrV 0w)
| Some (s,w) => FlatV (PtrV w)) ∧
(eval_const g UndefC = FlatV UndefV)
Termination
WF_REL_TAC `measure (const_size o snd)` >> rw [listTheory.MEM_MAP] >>
TRY
@ -306,140 +314,64 @@ End
Definition eval_def:
(eval s (Variable v) =
case flookup s.locals v of
| None => <| poison := F; value := W1V 0w |>
| None => <| poison := F; value := FlatV (W1V 0w) |>
| Some v => v) ∧
(eval s (Constant c) = <| poison := F; value := eval_const s.globals c |>)
End
Definition v2n_def:
(v2n (W1V b) = Some (if T then 1 else 0)) ∧
(v2n (W8V w8) = Some (w2n w8)) ∧
(v2n (W32V w32) = Some (w2n w32)) ∧
(v2n (W64V w64) = Some (w2n w64)) ∧
(v2n (FlatV (W1V b)) = Some (if T then 1 else 0)) ∧
(v2n (FlatV (W8V w8)) = Some (w2n w8)) ∧
(v2n (FlatV (W32V w32)) = Some (w2n w32)) ∧
(v2n (FlatV (W64V w64)) = Some (w2n w64)) ∧
(v2n _ = None)
End
Definition interval_to_set_def:
interval_to_set (_, start,stop) =
{ n | start ≤ n ∧ n < stop }
End
Definition interval_ok_def:
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 ∧ fst b1 = fst b2 ∧ interval_to_set b1 ⊆ interval_to_set b2
End
Definition is_free_def:
is_free b1 allocs ⇔
interval_ok b1 ∧
∀b2. b2 ∈ allocs ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
End
Definition get_bytes_def:
get_bytes h (_, start, stop) =
map
(λoff.
case flookup h (A (start + off)) of
| None => (F, 0w)
| Some w => w)
(count_list (stop - start))
Definition type_to_shape_def:
(type_to_shape (IntT s) = Flat (sizeof (IntT s)) (IntT s)) ∧
(type_to_shape (PtrT t) = Flat (sizeof (PtrT t)) (PtrT t)) ∧
(type_to_shape (ArrT n t) = Array (type_to_shape t) n) ∧
(type_to_shape (StrT ts) = Tuple (map type_to_shape ts))
Termination
WF_REL_TAC `measure ty_size` >> rw [] >>
Induct_on `ts` >> rw [definition "ty_size_def"] >>
res_tac >> simp []
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))))
Definition convert_value_def:
(convert_value (IntT W1) w = W1V (w2w w)) ∧
(convert_value (IntT W8) w = W8V (w2w w)) ∧
(convert_value (IntT W32) w = W32V (w2w w)) ∧
(convert_value (IntT W64) w = W64V w) ∧
(convert_value (PtrT _) w = PtrV w)
End
(* Allocate a free chunk of memory, and write non-deterministic bytes into it *)
Inductive allocate:
v2n v.value = Some m ∧
b = (T, w2n w, w2n w + m * len) ∧
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;
heap := set_bytes v.poison bytes (w2n w) s.heap |>)
Definition bytes_to_llvm_value_def:
bytes_to_llvm_value t bs =
(bytes_to_value (λn t w. convert_value t w) (type_to_shape t) bs)
End
Definition deallocate_def:
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))))
Definition unconvert_value_def:
(unconvert_value (W1V w) = (1, w2w w)) ∧
(unconvert_value (W8V w) = (1, w2w w)) ∧
(unconvert_value (W32V w) = (4, w2w w)) ∧
(unconvert_value (W64V w) = (8, w)) ∧
(unconvert_value (PtrV w) = (8, w))
End
(* Read len bytes from the list of bytes, and convert it into a word value,
* little-endian encoding *)
Definition le_read_w_def:
le_read_w len (bs : word8 list) =
if length bs < len then
(l2w 256 (map w2n bs), [])
else
(l2w 256 (map w2n (take len bs)), drop len bs)
End
(* Return len bytes that are the little-endian encoding of the argument word *)
Definition le_write_w_def:
le_write_w len w =
let (l : word8 list) = map n2w (w2l 256 w) in
take len (l ++ replicate (len - length l) 0w)
End
Definition bytes_to_value_def:
(bytes_to_value (IntT W1) (b::bs) = (W1V (w2w b), bs)) ∧
(bytes_to_value (IntT W8) (b::bs) = (W8V b, bs)) ∧
(bytes_to_value (IntT W32) bs = (W32V ## I) (le_read_w 4 bs)) ∧
(bytes_to_value (IntT W64) bs = (W64V ## I) (le_read_w 8 bs)) ∧
(bytes_to_value (PtrT _) bs = (PtrV ## I) (le_read_w 8 bs)) ∧
(bytes_to_value (ArrT n t) bs = (AggV ## I) (read_array n t bs)) ∧
(bytes_to_value (StrT ts) bs = (AggV ## I) (read_str ts bs)) ∧
(read_array 0 t bs = ([], bs)) ∧
(read_array (Suc n) t bs =
let (v, bs) = bytes_to_value t bs in
let (rest, bs) = read_array n t bs in
(v::rest, bs)) ∧
(read_str [] bs = ([], bs)) ∧
(read_str (t::ts) bs =
let (v, bs) = bytes_to_value t bs in
let (rest, bs) = read_str ts bs in
(v::rest, bs))
Termination
WF_REL_TAC `measure (λx. case x of
| INL (t, bs) => ty_size t
| INR (INL (n, t, bs)) => n + ty_size t
| INR (INR (ts, bs)) => ty1_size ts)`
End
Definition value_to_bytes_def:
(value_to_bytes (W1V w) = [w2w w]) ∧
(value_to_bytes (W8V w) = [w]) ∧
(value_to_bytes (W32V w) = le_write_w 4 w) ∧
(value_to_bytes (W64V w) = le_write_w 8 w) ∧
(value_to_bytes (PtrV n) = le_write_w 8 n) ∧
(value_to_bytes (AggV vs) = flat (map value_to_bytes vs))
Termination
WF_REL_TAC `measure v_size` >>
Induct >> rw [definition "v_size_def"] >>
TRY (first_x_assum drule) >>
decide_tac
Definition llvm_value_to_bytes_def:
llvm_value_to_bytes v =
value_to_bytes unconvert_value v
End
Definition do_sub_def:
do_sub (nuw:bool) (nsw:bool) (v1:pv) (v2:pv) =
let (diff, u_overflow, s_overflow) =
case (v1.value, v2.value) of
| (W1V w1, W1V w2) => (W1V ## I) (add_with_carry (w1, ¬w2, T))
| (W8V w1, W8V w2) => (W8V ## I) (add_with_carry (w1, ¬w2, T))
| (W32V w1, W32V w2) => (W32V ## I) (add_with_carry (w1, ¬w2, T))
| (W64V w1, W64V w2) => (W64V ## I) (add_with_carry (w1, ¬w2, T))
| (FlatV (W1V w1), FlatV (W1V w2)) => (FlatV o W1V ## I) (add_with_carry (w1, ¬w2, T))
| (FlatV (W8V w1), FlatV (W8V w2)) => (FlatV o W8V ## I) (add_with_carry (w1, ¬w2, T))
| (FlatV (W32V w1), FlatV (W32V w2)) => (FlatV o W32V ## I) (add_with_carry (w1, ¬w2, T))
| (FlatV (W64V w1), FlatV (W64V w2)) => (FlatV o W64V ## I) (add_with_carry (w1, ¬w2, T))
in
let p = ((nuw ∧ u_overflow) ∨ (nsw ∧ s_overflow) ∨ v1.poison ∨ v2.poison) in
<| poison := p; value := diff |>
@ -456,11 +388,11 @@ Definition do_icmp_def:
<| poison := (v1.poison ∨ v2.poison);
value := bool_to_v (
case (v1.value, v2.value) of
| (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
| (PtrV w1, PtrV w2) => (get_comp c) w1 w2) |>
| (FlatV (W1V w1), FlatV (W1V w2)) => (get_comp c) w1 w2
| (FlatV (W8V w1), FlatV (W8V w2)) => (get_comp c) w1 w2
| (FlatV (W32V w1), FlatV (W32V w2)) => (get_comp c) w1 w2
| (FlatV (W64V w1), FlatV (W64V w2)) => (get_comp c) w1 w2
| (FlatV (PtrV w1), FlatV (PtrV w2)) => (get_comp c) w1 w2) |>
End
Definition do_phi_def:
@ -468,21 +400,6 @@ Definition do_phi_def:
option_map (λarg. (id, eval s arg)) (alookup entries from_l)
End
Definition extract_type_def:
(extract_type t [] = Some t) ∧
(extract_type (ArrT n t) (i::idx) =
if i < n then
extract_type t idx
else
None) ∧
(extract_type (StrT ts) (i::idx) =
if i < length ts then
extract_type (el i ts) idx
else
None) ∧
(extract_type _ _ = None)
End
Definition extract_value_def:
(extract_value v [] = Some v) ∧
(extract_value (AggV vs) (i::indices) =
@ -519,7 +436,7 @@ End
Inductive step_instr:
(s.stack = fr::st ∧
deallocate fr.stack_allocs s.allocations s.heap = (new_allocs, new_h)
deallocate fr.stack_allocs s.heap = new_h
⇒
step_instr prog s
(Ret (t, a))
@ -528,7 +445,6 @@ Inductive step_instr:
globals := s.globals;
locals := fr.saved_locals;
stack := st;
allocations := new_allocs;
heap := new_h |>)) ∧
(* Do the phi assignments in parallel. The manual says "For the purposes of the
@ -542,7 +458,7 @@ Inductive step_instr:
* %r2 = phi [%r1, %l]
* %r1 = phi [0, %l]
*)
(eval s a = <| poison := p; value := W1V tf |> ∧
(eval s a = <| poison := p; value := FlatV (W1V tf) |> ∧
l = Some (if tf = 1w then l1 else l2) ∧
alookup prog s.ip.f = Some d ∧
alookup d.blocks l = Some <| h := Head phis None; body := b |> ∧
@ -579,27 +495,29 @@ Inductive step_instr:
(inc_pc (update_result r
<| poison := (v1.poison ∨ v2.poison); value := result |> s))) ∧
(allocate s (eval s a1) (sizeof t) (v2, s2)
(eval s a1 = v ∧
v2n v.value = Some n ∧
allocate s.heap (n * sizeof t) v.poison (v2, new_h)
⇒
step_instr prog s
(Alloca r t (t1, a1))
(inc_pc (update_result r v2 s2))) ∧
(inc_pc (update_result r v2 (s with heap := new_h)))) ∧
(eval s a1 = <| poison := p1; value := PtrV w |> ∧
interval = (freeable, w2n w, w2n w + sizeof t) ∧
is_allocated interval s.allocations ∧
(eval s a1 = <| poison := p1; value := FlatV (PtrV w) |> ∧
interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
is_allocated interval s.heap ∧
pbytes = get_bytes s.heap interval
⇒
step_instr prog s
(Load r t (t1, a1))
(inc_pc (update_result r <| poison := (T ∈ set (map fst pbytes));
value := fst (bytes_to_value t (map snd pbytes)) |>
value := fst (bytes_to_llvm_value t (map snd pbytes)) |>
s))) ∧
(eval s a2 = <| poison := p2; value := PtrV w |> ∧
interval = (freeable, w2n w, w2n w + sizeof t) ∧
is_allocated interval s.allocations ∧
bytes = value_to_bytes (eval s a1).value ∧
(eval s a2 = <| poison := p2; value := FlatV (PtrV w) |> ∧
interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
is_allocated interval s.heap ∧
bytes = llvm_value_to_bytes (eval s a1).value ∧
length bytes = sizeof t
⇒
step_instr prog s
@ -607,7 +525,7 @@ Inductive step_instr:
(inc_pc (s with heap := set_bytes p2 bytes (w2n w) s.heap))) ∧
(map (eval s o snd) tindices = i1::indices ∧
(eval s a1).value = PtrV w1 ∧
(eval s a1).value = FlatV (PtrV w1) ∧
cast_num i1.value = Some n ∧
map (λx. cast_num x.value) indices = map Some ns ∧
get_offset t1 ns = Some off
@ -616,11 +534,11 @@ Inductive step_instr:
(Gep r t ((PtrT t1), a1) tindices)
(inc_pc (update_result r
<| poison := (v1.poison ∨ i1.poison ∨ exists (λv. v.poison) indices);
value := PtrV (n2w (w2n w1 + sizeof t1 * n + off)) |>
value := FlatV (PtrV (n2w (w2n w1 + sizeof t1 * n + off))) |>
s))) ∧
(eval s a1 = v1 ∧
v1.value = PtrV w ∧
v1.value = FlatV (PtrV w) ∧
w64_cast w t = Some int_v
⇒
step_instr prog s
@ -632,7 +550,7 @@ Inductive step_instr:
⇒
step_instr prog s
(Inttoptr r (t1, a1) t)
(inc_pc (update_result r <| poison := v1.poison; value := PtrV w |> s))) ∧
(inc_pc (update_result r <| poison := v1.poison; value := FlatV (PtrV w) |> s))) ∧
(step_instr prog s
(Icmp r c t a1 a2)
@ -645,7 +563,6 @@ Inductive step_instr:
<| ip := <| f := fname; b := None; i := 0 |>;
locals := alist_to_fmap (zip (map snd d.params, map (eval s o snd) targs));
globals := s.globals;
allocations:= s.allocations;
stack :=
<| ret := s.ip with i := s.ip.i + 1;
saved_locals := s.locals;
@ -682,29 +599,13 @@ End
(* ----- Invariants on state ----- *)
(* The allocations are of intervals that don't overlap *)
Definition allocations_ok_def:
allocations_ok s ⇔
∀i1 i2.
i1 ∈ s.allocations ∧ i2 ∈ s.allocations
⇒
interval_ok i1 ∧ interval_ok i2 ∧
(interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2)
End
(* The heap maps exactly the address in the allocations *)
Definition heap_ok_def:
heap_ok s ⇔
∀n. flookup s.heap (A n) ≠ None ⇔ ∃i. i ∈ s.allocations ∧ n ∈ interval_to_set i
End
(* All global variables are allocated in non-freeable memory *)
Definition globals_ok_def:
globals_ok s ⇔
∀g n w.
flookup s.globals g = Some (n, w)
⇒
is_allocated (F, w2n w, w2n w + n) s.allocations
is_allocated (Interval F (w2n w) (w2n w + n)) s.heap
End
(* Instruction pointer points to an instruction *)
@ -733,7 +634,7 @@ End
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
every (λn. ∃start stop. n = A start ∧ Interval T start stop ∈ s.heap.allocations) f.stack_allocs
End
(* The frames are all of, and no two stack allocations have the same address *)
@ -745,7 +646,7 @@ End
Definition state_invariant_def:
state_invariant p s ⇔
ip_ok p s.ip ∧ allocations_ok s ∧ heap_ok s ∧ globals_ok s ∧ stack_ok p s
ip_ok p s.ip ∧ heap_ok s.heap ∧ globals_ok s ∧ stack_ok p s
End
(* ----- Initial state ----- *)
@ -758,19 +659,19 @@ Definition is_init_state_def:
s.ip.i = 0 ∧
s.locals = fempty ∧
s.stack = [] ∧
allocations_ok s ∧
globals_ok s ∧
heap_ok s ∧
heap_ok s.heap ∧
fdom s.globals = fdom global_init ∧
s.heap.valid_addresses = { A n | n < dimword (:64) } ∧
(* The initial allocations for globals are not freeable *)
s.allocations ⊆ { (F, start, stop) | T } ∧
s.heap.allocations ⊆ { Interval F start stop | T } ∧
(* The heap starts with the initial values of the globals written to their
* addresses *)
∀g w t v n.
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, [])
get_bytes s.heap (Interval F (w2n w) (w2n w + sizeof t)) = map (λb. (F,b)) bytes ∧
bytes_to_llvm_value t bytes = (v, [])
End
export_theory();

521
sledge/semantics/llvm_propScript.sml
Unescape View File

@ -11,393 +11,95 @@ open HolKernel boolLib bossLib Parse;
open pairTheory listTheory rich_listTheory arithmeticTheory wordsTheory;
open pred_setTheory finite_mapTheory;
open logrootTheory numposrepTheory;
open settingsTheory llvmTheory;
open settingsTheory miscTheory llvmTheory memory_modelTheory;
new_theory "llvm_prop";
numLib.prefer_num();
(* ----- Theorems about list library functions ----- *)
(* Could be upstreamed to HOL *)
Theorem dropWhile_map:
∀P f l. dropWhile P (map f l) = map f (dropWhile (P o f) l)
Proof
Induct_on `l` >> rw []
QED
Theorem dropWhile_prop:
∀P l x. x < length l - length (dropWhile P l) ⇒ P (el x l)
Proof
Induct_on `l` >> rw [] >>
Cases_on `x` >> fs []
QED
Theorem dropWhile_rev_take:
∀P n l x.
let len = length (dropWhile P (reverse (take n l))) in
x + len < n ∧ n ≤ length l ⇒ P (el (x + len) l)
Proof
rw [] >>
`P (el ((n - 1 - x - length (dropWhile P (reverse (take n l))))) (reverse (take n l)))`
by (irule dropWhile_prop >> simp [LENGTH_REVERSE]) >>
rfs [EL_REVERSE, EL_TAKE, PRE_SUB1]
QED
Theorem take_replicate:
∀m n x. take m (replicate n x) = replicate (min m n) x
Proof
Induct_on `n` >> rw [TAKE_def, MIN_DEF] >> fs [] >>
Cases_on `m` >> rw []
QED
Theorem length_take_less_eq:
∀n l. length (take n l) ≤ n
Proof
Induct_on `l` >> rw [TAKE_def] >>
Cases_on `n` >> fs []
QED
Theorem flat_drop:
∀n m ls. flat (drop m ls) = drop (length (flat (take m ls))) (flat ls)
Proof
Induct_on `ls` >> rw [DROP_def, DROP_APPEND] >>
irule (GSYM DROP_LENGTH_TOO_LONG) >> simp []
QED
Theorem take_is_prefix:
∀n l. take n l ≼ l
Proof
Induct_on `l` >> rw [TAKE_def]
QED
Theorem sum_prefix:
∀l1 l2. l1 ≼ l2 ⇒ sum l1 ≤ sum l2
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 [] >>
`0 < n` by decide_tac >>
drule DIVISION >> disch_then (qspec_then `m` mp_tac) >>
decide_tac
QED
Theorem exp_log_bound:
∀b n. 1 < b ∧ n ≠ 0 ⇒ n DIV b + 1 ≤ b ** (log b n) ∧ b ** (log b n) ≤ n
Proof
rw [] >> `0 < n` by decide_tac >>
drule LOG >> disch_then drule >> rw [] >>
fs [ADD1, EXP_ADD] >>
simp [DECIDE ``∀x y. x + 1 ≤ y ⇔ x < y``] >>
`∃x. b = Suc x` by intLib.COOPER_TAC >>
`b * (n DIV b) < b * b ** log b n` suffices_by metis_tac [LESS_MULT_MONO] >>
pop_assum kall_tac >>
`b ≠ 0` by decide_tac >>
drule mul_div_bound >> disch_then (qspec_then `n` mp_tac) >>
decide_tac
QED
Theorem log_base_power:
∀n b. 1 < b ⇒ log b (b ** n) = n
Proof
Induct >> rw [EXP, LOG_1] >>
Cases_on `n` >> rw [LOG_BASE] >>
first_x_assum drule >> rw [] >>
simp [Once EXP, LOG_MULT]
QED
Theorem log_change_base_power:
∀m n b. 1 < b ∧ m ≠ 0 ∧ n ≠ 0 ⇒ log (b ** n) m = log b m DIV n
Proof
rw [] >> irule LOG_UNIQUE >>
rw [ADD1, EXP_MUL, LEFT_ADD_DISTRIB] >>
qmatch_goalsub_abbrev_tac `x DIV _` >>
drule mul_div_bound >> disch_then (qspec_then `x` mp_tac) >> rw []
>- (
irule LESS_LESS_EQ_TRANS >>
qexists_tac `b ** (x+1)` >> rw [] >>
unabbrev_all_tac >>
simp [EXP_ADD] >>
`b * (m DIV b + 1) ≤ b * b ** log b m`
by metis_tac [exp_log_bound, LESS_MONO_MULT, MULT_COMM] >>
`m < b * (m DIV b + 1)` suffices_by decide_tac >>
simp [LEFT_ADD_DISTRIB] >>
`b ≠ 0` by decide_tac >>
`m - (b - 1) ≤ b * (m DIV b)` by metis_tac [mul_div_bound] >>
fs [])
>- (
irule LESS_EQ_TRANS >>
qexists_tac `b ** (log b m)` >> rw [] >>
unabbrev_all_tac >>
metis_tac [exp_log_bound])
QED
(* ----- Theorems about word stuff ----- *)
Theorem l2n_padding:
∀ws n. l2n 256 (ws ++ map w2n (replicate n 0w)) = l2n 256 ws
Proof
Induct >> rw [l2n_def] >>
Induct_on `n` >> rw [l2n_def]
QED
Theorem l2n_0:
∀l b. b ≠ 0 ∧ every ($> b) l⇒ (l2n b l = 0 ⇔ every ($= 0) l)
Proof
Induct >> rw [l2n_def] >>
eq_tac >> rw []
QED
(* ----- Theorems about converting between values and byte lists ----- *)
Theorem mod_n2l:
∀d n. 0 < d ⇒ map (\x. x MOD d) (n2l d n) = n2l d n
Theorem value_type_is_fc:
∀t v. value_type t v ⇒ first_class_type t
Proof
rw [] >> drule n2l_BOUND >> disch_then (qspec_then `n` mp_tac) >>
qspec_tac (`n2l d n`, `l`) >>
Induct >> rw []
ho_match_mp_tac value_type_ind >> rw [first_class_type_def] >>
fs [LIST_REL_EL_EQN, EVERY_EL]
QED
(* ----- Theorems about converting between values and byte lists ----- *)
Theorem le_write_w_length:
∀l x. length (le_write_w l w) = l
Theorem sizeof_type_to_shape:
∀t. first_class_type t ⇒ sizeof (type_to_shape t) = sizeof t
Proof
rw [le_write_w_def]
recInduct type_to_shape_ind >>
rw [type_to_shape_def, memory_modelTheory.sizeof_def, llvmTheory.sizeof_def,
first_class_type_def, EVERY_MEM] >>
qid_spec_tac `vs` >> Induct_on `ts` >> rw [] >> fs []
QED
Theorem v2b_size:
∀t v. value_type t v ⇒ length (value_to_bytes v) = sizeof t
Theorem value_type_to_shape:
∀t v.
value_type t v ⇒
∀s.
value_shape (\n t x. n = fst (unconvert_value x) ∧ value_type t (FlatV x)) (type_to_shape t) v
Proof
ho_match_mp_tac value_type_ind >>
rw [value_to_bytes_def, sizeof_def]
>- metis_tac [le_write_w_length]
>- metis_tac [le_write_w_length]
>- metis_tac [le_write_w_length]
>- (Induct_on `vs` >> rw [ADD1] >> fs [])
>- (
pop_assum mp_tac >>
qid_spec_tac `vs` >> qid_spec_tac `ts` >>
ho_match_mp_tac LIST_REL_ind >> rw [])
rw [memory_modelTheory.sizeof_def, llvmTheory.sizeof_def, type_to_shape_def,
unconvert_value_def, value_shape_def] >>
fs [value_shapes_list_rel, LIST_REL_CONJ, ETA_THM, EVERY2_MAP] >>
metis_tac [value_type_rules]
QED
Theorem b2v_size:
(∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
∃v. bytes_to_value t bs = (v, drop (sizeof t) bs)) ∧
(∀n t bs. first_class_type t ∧ n * sizeof t ≤ length bs ⇒
∃vs. read_array n t bs = (vs, drop (n * sizeof t) bs)) ∧
(∀ts bs. every first_class_type ts ∧ sum (map sizeof ts) ≤ length bs ⇒
∃vs. read_str ts bs = (vs, drop (sum (map sizeof ts)) bs))
Theorem llvm_v2b_size:
∀t v. value_type t v ⇒ length (llvm_value_to_bytes v) = sizeof t
Proof
ho_match_mp_tac bytes_to_value_ind >>
rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
fs [first_class_type_def]
>- (simp [PAIR_MAP] >> metis_tac [SND])
>- (
pairarg_tac >> rw [] >> pairarg_tac >> rw [] >>
fs [ADD1] >> rw [] >> fs [DROP_DROP_T, LEFT_ADD_DISTRIB])
>- fs [DROP_DROP_T, LEFT_ADD_DISTRIB]
rw [llvm_value_to_bytes_def] >>
drule value_type_to_shape >> rw [] >>
drule value_type_is_fc >> rw [] >>
drule sizeof_type_to_shape >>
disch_then (mp_tac o GSYM) >> rw [] >>
irule v2b_size >> rw [] >>
qmatch_assum_abbrev_tac `value_shape f _ _` >>
qexists_tac `f` >> rw [] >>
unabbrev_all_tac >> fs []
QED
Theorem b2v_smaller:
Theorem b2llvm_v_size:
∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
length (snd (bytes_to_value t bs)) = length bs - sizeof t
∃v. bytes_to_llvm_value t bs = (v, drop (sizeof t) bs)
Proof
rw [] >> imp_res_tac b2v_size >>
Cases_on `bytes_to_value t bs` >> fs []
rw [bytes_to_llvm_value_def] >>
drule sizeof_type_to_shape >> disch_then (mp_tac o GSYM) >> rw [] >>
fs [PAIR_MAP] >>
metis_tac [SND, b2v_size]
QED
Theorem b2v_append:
(∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
bytes_to_value t (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_value t bs)) ∧
(∀n t bs. first_class_type t ∧ n * sizeof t ≤ length bs ⇒
∃vs. read_array n t (bs ++ bs') = (I ## (λx. x ++ bs')) (read_array n t bs)) ∧
(∀ts bs. every first_class_type ts ∧ sum (map sizeof ts) ≤ length bs ⇒
∃vs. read_str ts (bs ++ bs') = (I ## (λx. x ++ bs')) (read_str ts bs))
Theorem b2llvm_v_smaller:
∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
length (snd (bytes_to_llvm_value t bs)) = length bs - sizeof t
Proof
ho_match_mp_tac bytes_to_value_ind >>
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] >>
BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
first_x_assum irule >>
`sizeof t ≤ length bs` by decide_tac >>
imp_res_tac b2v_smaller >> rfs [])
>- (
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 >>
imp_res_tac b2v_smaller >> rfs [])
rw [bytes_to_llvm_value_def] >>
metis_tac [b2v_smaller, sizeof_type_to_shape]
QED
Theorem le_read_write:
∀n w bs.
n ≠ 0 ∧ dimword (:'a) ≤ 256 ** n ⇒ le_read_w n (le_write_w n (w :'a word) ⧺ bs) = (w, bs)
Theorem b2llvm_v_append:
∀t bs bs'. first_class_type t ∧ sizeof t ≤ length bs ⇒
bytes_to_llvm_value t (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_llvm_value t bs)
Proof
rw [le_read_w_def, le_write_w_length]
>- (
`take n (le_write_w n w ⧺ bs) = le_write_w n w`
by metis_tac [le_write_w_length, TAKE_LENGTH_APPEND] >>
simp [le_write_w_def, w2l_def, l2w_def] >>
Cases_on `w` >> simp [] >> fs [l2n_padding, TAKE_APPEND, take_replicate] >>
simp [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, mod_n2l] >>
rename1 `n2l 256 m` >>
`length (n2l 256 m) ≤ n`
by (
rw [LENGTH_n2l] >>
`256 = 2 ** 8` by EVAL_TAC >>
ASM_REWRITE_TAC [] >> simp [log_change_base_power, GSYM LESS_EQ] >>
`n2w m ≠ 0w` by simp [] >>
drule LOG2_w2n_lt >> rw [] >> fs [bitTheory.LOG2_def, dimword_def] >>
`8 * (log 2 m DIV 8) ≤ log 2 m` by metis_tac [mul_div_bound, EVAL ``8 ≠ 0n``] >>
`LOG 2 (2 ** dimindex (:'a)) ≤ LOG 2 (256 ** n)` by simp [LOG_LE_MONO] >>
pop_assum mp_tac >>
`256 = 2 ** 8` by EVAL_TAC >>
ASM_REWRITE_TAC [EXP_MUL] >> simp [log_base_power]) >>
simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG])
>- metis_tac [le_write_w_length, DROP_LENGTH_APPEND]
rw [bytes_to_llvm_value_def] >>
drule sizeof_type_to_shape >> disch_then (mp_tac o GSYM) >> rw [] >> fs [] >>
rw [PAIR_MAP, b2v_append]
QED
Theorem le_write_read:
∀n w bs bs'.
256 ** n ≤ dimword (:'a) ∧
n ≤ length bs ∧
le_read_w n bs = (w:'a word, bs')
⇒
le_write_w n w ++ bs' = bs
Theorem b2v_llvm_v2b:
∀v t bs. value_type t v ⇒ bytes_to_llvm_value t (llvm_value_to_bytes v ++ bs) = (v, bs)
Proof
rw [le_read_w_def] >>
qmatch_goalsub_abbrev_tac `l2w _ l` >>
`le_write_w n (l2w 256 l) = take n bs` suffices_by metis_tac [TAKE_DROP] >>
simp [le_write_w_def, w2l_l2w] >>
`l2n 256 l < 256 ** n`
by (
`n ≤ length bs` by decide_tac >>
metis_tac [l2n_lt, LENGTH_TAKE, LENGTH_MAP, EVAL ``0n < 256``]) >>
fs [] >>
`every ($> 256) l`
by (
simp [EVERY_MAP, Abbr `l`] >> irule EVERY_TAKE >> simp [] >>
rpt (pop_assum kall_tac) >>
Induct_on `bs` >> rw [] >>
Cases_on `h` >> fs []) >>
rw [n2l_l2n]
>- (
rw [TAKE_def, take_replicate] >>
Cases_on `n` >> fs [] >>
rfs [l2n_0] >> unabbrev_all_tac >> fs [EVERY_MAP] >>
ONCE_REWRITE_TAC [GSYM REPLICATE] >>
qmatch_goalsub_abbrev_tac `take n _` >>
qpat_assum `¬(_ < _)` mp_tac >>
qpat_assum `every (\x. 0 = w2n x) _` mp_tac >>
rpt (pop_assum kall_tac) >>
qid_spec_tac `bs` >>
Induct_on `n` >> rw [] >>
Cases_on `bs` >> rw [] >> fs [] >>
Cases_on `h` >> fs [] >>
first_x_assum irule >> rw [] >>
irule MONO_EVERY >>
qexists_tac `(λx. 0 = w2n x)` >> rw []) >>
fs [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
`exists (\y. 0 ≠ y) l`
by (
fs [l2n_eq_0, combinTheory.o_DEF] >> fs [EXISTS_MEM, EVERY_MEM] >>
qexists_tac `x` >> rfs [MOD_MOD, GREATER_DEF]) >>
simp [LOG_l2n_dropWhile] >>
`length (dropWhile ($= 0) (reverse l)) ≠ 0`
by (
Cases_on `l` >> fs [dropWhile_eq_nil, combinTheory.o_DEF, EXISTS_REVERSE]) >>
`0 < length (dropWhile ($= 0) (reverse l))` by decide_tac >>
fs [SUC_PRE] >>
`map n2w l = take n bs`
by (simp [Abbr `l`, MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, n2w_w2n]) >>
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] >>
rw [MIN_DEF] >> fs []
>- (
simp [TAKE_APPEND, TAKE_TAKE_MIN, MIN_DEF, take_replicate] >>
`replicate (length l − length (dropWhile ($= 0) (reverse l))) 0w =
take (length l − (length (dropWhile ($= 0) (reverse l)))) (drop (length (dropWhile ($= 0) (reverse l))) bs)`
suffices_by (rw [] >> irule take_drop_partition >> simp []) >>
rw [LIST_EQ_REWRITE, EL_REPLICATE, EL_TAKE, EL_DROP] >>
`length (dropWhile ($= 0) (reverse l)) =
length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs)))`
by (
`reverse l = reverse (take (length l) (map w2n bs))` by metis_tac [] >>
ONCE_ASM_REWRITE_TAC [] >>
qpat_x_assum `Abbrev (l = _)` kall_tac >>
simp [GSYM MAP_TAKE, GSYM MAP_REVERSE, dropWhile_map, combinTheory.o_DEF]) >>
fs [] >>
`x + length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs))) < length l` by decide_tac >>
drule (SIMP_RULE std_ss [LET_THM] dropWhile_rev_take) >>
rw [] >>
REWRITE_TAC [GSYM w2n_11, word_0_n2w] >>
simp [])
>- rw [TAKE_APPEND, TAKE_TAKE]
QED
Theorem b2v_v2b:
∀v t bs. value_type t v ⇒ bytes_to_value t (value_to_bytes v ++ bs) = (v, bs)
Proof
gen_tac >> completeInduct_on `v_size v` >>
rw [] >>
pop_assum mp_tac >> simp [value_type_cases] >>
rw [] >>
rw [bytes_to_value_def, value_to_bytes_def, le_read_write]
>- wordsLib.WORD_DECIDE_TAC
>- (
qmatch_abbrev_tac `_ x = _` >>
`x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
unabbrev_all_tac >>
qid_spec_tac `bs` >> Induct_on `vs` >> simp [bytes_to_value_def] >>
rw [] >> fs [v_size_def] >>
pairarg_tac >> fs [] >>
pairarg_tac >> fs [] >>
rename1 `value_type t v1` >>
first_x_assum (qspec_then `v_size v1` mp_tac) >> simp [] >>
disch_then (qspec_then `v1` mp_tac) >> simp [] >>
disch_then (qspec_then `t` mp_tac) >> simp [] >>
qmatch_assum_abbrev_tac `bytes_to_value _ (_ ++ bs1 ++ _) = _` >>
disch_then (qspec_then `bs1++bs` mp_tac) >> simp [] >>
unabbrev_all_tac >> strip_tac >> fs [] >>
first_x_assum (qspec_then `bs` mp_tac) >> rw [])
>- (
qmatch_abbrev_tac `_ x = _` >>
`x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
unabbrev_all_tac >>
pop_assum mp_tac >>
qid_spec_tac `bs` >> qid_spec_tac `ts` >> Induct_on `vs` >> simp [bytes_to_value_def] >>
rw [] >> fs [v_size_def, bytes_to_value_def] >>
pairarg_tac >> fs [] >>
pairarg_tac >> fs [] >>
rename1 `value_type t v1` >>
first_x_assum (qspec_then `v_size v1` mp_tac) >> simp [] >>
disch_then (qspec_then `v1` mp_tac) >> simp [] >>
disch_then (qspec_then `t` mp_tac) >> simp [] >>
qmatch_assum_abbrev_tac `bytes_to_value _ (_ ++ bs1 ++ _) = _` >>
disch_then (qspec_then `bs1++bs` mp_tac) >> simp [] >>
unabbrev_all_tac >> strip_tac >> fs [] >>
first_x_assum drule >> metis_tac [PAIR_EQ])
rw [bytes_to_llvm_value_def, llvm_value_to_bytes_def] >>
drule value_type_to_shape >> rw [] >>
qmatch_assum_abbrev_tac `value_shape f _ _` >>
irule b2v_v2b >>
qexists_tac `f` >> rw [] >>
unabbrev_all_tac >> fs [] >>
fs [unconvert_value_def, convert_value_def, value_type_cases] >>
wordsLib.WORD_DECIDE_TAC
QED
(* ----- Theorems about insert/extract value and get_offset ----- *)
@ -482,7 +184,7 @@ Theorem offset_size_leq:
⇒
n ≤ sizeof t
Proof
recInduct get_offset_ind >> rw [get_offset_def, sizeof_def, indices_in_range_def] >>
recInduct get_offset_ind >> rw [get_offset_def, llvmTheory.sizeof_def, indices_in_range_def] >>
BasicProvers.EVERY_CASE_TAC >> fs [] >> rw [] >> rfs []
>- (
`x + i * sizeof t ≤ (i + 1) * sizeof t` by decide_tac >>
@ -495,13 +197,6 @@ Proof
drule sum_prefix >> rw [SUM_APPEND]
QED
Theorem value_type_is_fc:
∀t v. value_type t v ⇒ first_class_type t
Proof
ho_match_mp_tac value_type_ind >> rw [first_class_type_def] >>
fs [LIST_REL_EL_EQN, EVERY_EL]
QED
Theorem extract_type_fc:
∀t is t'. extract_type t is = Some t' ∧ first_class_type t ⇒ first_class_type t'
Proof
@ -517,7 +212,7 @@ Theorem extract_offset_size:
sizeof t' ≤ sizeof t - n
Proof
recInduct get_offset_ind >> rw [get_offset_def, extract_type_def] >>
BasicProvers.EVERY_CASE_TAC >> fs [sizeof_def] >> rfs [] >> rw [ETA_THM]
BasicProvers.EVERY_CASE_TAC >> fs [llvmTheory.sizeof_def] >> rfs [] >> rw [ETA_THM]
>- (
`sizeof t ≤ (v1 − i) * sizeof t` suffices_by decide_tac >>
`1 ≤ v1 - i` by decide_tac >>
@ -529,6 +224,12 @@ Proof
Induct_on `ts` >> rw [TAKE_def, EL_CONS, PRE_SUB1]
QED
Theorem llvm_value_to_bytes_agg:
∀vs. llvm_value_to_bytes (AggV vs) = flat (map llvm_value_to_bytes vs)
Proof
Induct >> rw [] >> fs [llvm_value_to_bytes_def, value_to_bytes_def]
QED
Theorem read_from_offset_extract:
∀t indices n v t'.
indices_in_range t indices ∧
@ -536,55 +237,55 @@ Theorem read_from_offset_extract:
value_type t v ∧
extract_type t indices = Some t'
⇒
extract_value v indices = Some (fst (bytes_to_value t' (drop n (value_to_bytes v))))
extract_value v indices = Some (fst (bytes_to_llvm_value t' (drop n (llvm_value_to_bytes v))))
Proof
recInduct get_offset_ind >>
rw [extract_value_def, get_offset_def, extract_type_def, indices_in_range_def] >>
simp [DROP_0]
>- metis_tac [APPEND_NIL, FST, b2v_v2b] >>
>- metis_tac [APPEND_NIL, FST, b2v_llvm_v2b] >>
qpat_x_assum `value_type _ _` mp_tac >>
simp [Once value_type_cases] >> rw [] >> simp [extract_value_def] >>
qpat_x_assum `_ = Some n` mp_tac >> CASE_TAC >> rw [] >> rfs [] >>
simp [value_to_bytes_def]
simp [llvm_value_to_bytes_agg]
>- (
`value_type t (el i vs)` by metis_tac [EVERY_EL] >>
first_x_assum drule >>
rw [] >> simp [GSYM DROP_DROP_T, ETA_THM] >>
`i * sizeof t = length (flat (take i (map value_to_bytes vs)))`
`i * sizeof t = length (flat (take i (map llvm_value_to_bytes vs)))`
by (
simp [LENGTH_FLAT, MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
`map (λx. length (value_to_bytes x)) vs = replicate (length vs) (sizeof t)`
`map (λx. length (llvm_value_to_bytes x)) vs = replicate (length vs) (sizeof t)`
by (
qpat_x_assum `every _ _` mp_tac >> rpt (pop_assum kall_tac) >>
Induct_on `vs` >> rw [v2b_size]) >>
Induct_on `vs` >> rw [llvm_v2b_size]) >>
rw [take_replicate, MIN_DEF]) >>
rw [GSYM flat_drop, GSYM MAP_DROP] >>
drule DROP_CONS_EL >> simp [DROP_APPEND] >> disch_then kall_tac >>
`first_class_type t'` by metis_tac [value_type_is_fc, extract_type_fc] >>
`sizeof t' ≤ length (drop x (value_to_bytes (el i vs)))`
by (simp [LENGTH_DROP] >> drule v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
simp [b2v_append])
`sizeof t' ≤ length (drop x (llvm_value_to_bytes (el i vs)))`
by (simp [LENGTH_DROP] >> drule llvm_v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
simp [b2llvm_v_append])
>- metis_tac [LIST_REL_LENGTH]
>- (
`value_type (el i ts) (el i vs)` by metis_tac [LIST_REL_EL_EQN] >>
first_x_assum drule >>
rw [] >> simp [GSYM DROP_DROP_T, ETA_THM] >>
`sum (map sizeof (take i ts)) = length (flat (take i (map value_to_bytes vs)))`
`sum (map sizeof (take i ts)) = length (flat (take i (map llvm_value_to_bytes vs)))`
by (
simp [LENGTH_FLAT, MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
`map sizeof ts = map (\x. length (value_to_bytes x)) vs`
`map sizeof ts = map (\x. length (llvm_value_to_bytes x)) vs`
by (
qpat_x_assum `list_rel _ _ _` mp_tac >> rpt (pop_assum kall_tac) >>
qid_spec_tac `ts` >>
Induct_on `vs` >> rw [] >> rw [v2b_size]) >>
Induct_on `vs` >> rw [] >> rw [llvm_v2b_size]) >>
rw []) >>
rw [GSYM flat_drop, GSYM MAP_DROP] >>
`i < length vs` by metis_tac [LIST_REL_LENGTH] >>
drule DROP_CONS_EL >> simp [DROP_APPEND] >> disch_then kall_tac >>
`first_class_type t'` by metis_tac [value_type_is_fc, extract_type_fc] >>
`sizeof t' ≤ length (drop x (value_to_bytes (el i vs)))`
by (simp [LENGTH_DROP] >> drule v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
simp [b2v_append])
`sizeof t' ≤ length (drop x (llvm_value_to_bytes (el i vs)))`
by (simp [LENGTH_DROP] >> drule llvm_v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
simp [b2llvm_v_append])
QED
(* ----- Theorems about the step function ----- *)
@ -615,53 +316,28 @@ 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
∀p s1 v1 t v2 h2.
state_invariant p s1 ∧ allocate s1.heap v1 t (v2,h2) ⇒ state_invariant p (s1 with heap := h2)
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 [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def]
>- metis_tac [allocate_heap_ok]
>- (fs [is_allocated_def] >> metis_tac [allocate_unchanged, SUBSET_DEF])
>- (
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 [])
fs [EVERY_EL, frame_ok_def, allocate_unchanged] >> rw [] >>
metis_tac [allocate_unchanged, SUBSET_DEF])
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 ∧ is_allocated (Interval b n (n + length bytes)) s.heap
⇒
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])
>- metis_tac [set_bytes_heap_ok]
>- (fs [globals_ok_def, is_allocated_def, set_bytes_unchanged] >> metis_tac [])
>- (fs [stack_ok_def, EVERY_EL, frame_ok_def, set_bytes_unchanged])
QED
Theorem step_instr_invariant:
@ -676,8 +352,10 @@ Proof
>- (
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 [heap_ok_def, deallocate_def, allocations_ok_def] >> rw []
>- metis_tac []
>- metis_tac [] >>
fs [deallocate_def, heap_ok_def] >> rw [flookup_fdiff] >>
eq_tac >> rw []
>- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE]
@ -686,7 +364,7 @@ Proof
>- (
fs [globals_ok_def, deallocate_def] >> rw [] >>
first_x_assum drule >> rw [] >> fs [is_allocated_def] >>
qexists_tac `b2` >> rw [] >> CCONTR_TAC >> fs [])
qexists_tac `b2` >> rw [] >> CCONTR_TAC >> fs [interval_freeable_def])
>- (
fs [stack_ok_def, EVERY_MEM, frame_ok_def, deallocate_def] >> rfs [] >>
rw []
@ -702,8 +380,6 @@ Proof
rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
last_x_assum drule >> disch_then drule >> fs [])
>- (fs [allocations_ok_def] >> metis_tac [])
>- (fs [heap_ok_def] >> metis_tac [])
>- (fs [globals_ok_def] >> metis_tac [])
>- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
>- ( (* Br *)
@ -712,8 +388,6 @@ Proof
rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
last_x_assum drule >> disch_then drule >> fs [])
>- (fs [allocations_ok_def] >> metis_tac [])
>- (fs [heap_ok_def] >> metis_tac [])
>- (fs [globals_ok_def] >> metis_tac [])
>- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
>- (
@ -752,7 +426,6 @@ Proof
>- ( (* Call *)
rw [state_invariant_def]
>- (fs [prog_ok_def, ip_ok_def] >> metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
>- (fs [state_invariant_def, allocations_ok_def] >> metis_tac [])
>- (fs [state_invariant_def, heap_ok_def] >> metis_tac [])
>- (fs [state_invariant_def, globals_ok_def] >> metis_tac [])
>- (

2
sledge/semantics/llvm_to_llairScript.sml
Unescape View File

@ -344,7 +344,7 @@ Definition generate_move_blocks_list_def:
(used_names, new_blocks :: new_blocks2))
End
(* Givel an association list of labels and phi-block pairs, remove the phi's,
(* Given an association list of labels and phi-block pairs, remove the phi's,
* by generating an extra block along each control flow edge that does the move
* corresponding to the relevant phis. *)
Definition remove_phis_def:

570
sledge/semantics/memory_modelScript.sml
Unescape View File

@ -0,0 +1,570 @@
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
(* A simple, concrete memory model where the heap is an array of bytes. This is
* how llair views memory, and how we give semantics to llvm. Although LLVM's
* real memory model is still a subject of research, this is mostly to do with
* enabling the right collection of compiler optimisations. Since we only want to
* think about LLVM semantics after optimisation, the concrete model is likely to
* be sufficient. *)
open HolKernel boolLib bossLib Parse;
open arithmeticTheory listTheory rich_listTheory pairTheory;
open logrootTheory numposrepTheory wordsTheory pred_setTheory finite_mapTheory;
open settingsTheory miscTheory;
new_theory "memory_model";
numLib.prefer_num ();
(* Heap addresses *)
Datatype:
addr = A num
End
(* Values that fit in registers *)
Datatype:
reg_v =
| FlatV 'a
| AggV (reg_v list)
End
(* An interval of allocated memory.
* Args: whether it's freeable, the starting address (inclusive), and the ending address
* (exclusive)
*)
Datatype:
interval = Interval bool num num
End
Datatype:
heap = <| memory : addr |-> 'a # word8;
allocations : interval set;
valid_addresses : addr set|>
End
(* shapes statically describe the shape of a value in a register. Flat shapes
* take a given number of bytes, Array shapes are replicated a certain number of
* times
*)
Datatype:
shape =
| Flat num 'a
| Array shape num
| Tuple (shape list)
End
(* Does a value have a given shape. The function argument answers the question
* for flat values/shapes.
* We use mutual recursion instead of list_rel to work around a HOL bug. *)
Definition value_shape_def:
(value_shape f (Flat n t) (FlatV x) ⇔ f n t x) ∧
(value_shape f (Array s n) (AggV vs) ⇔
every (value_shape f s) vs ∧ length vs = n) ∧
(value_shape f (Tuple ss) (AggV vs) ⇔
value_shapes f ss vs) ∧
(value_shape _ _ _ ⇔ F) ∧
(value_shapes f [] [] ⇔ T) ∧
(value_shapes f (s::ss) (v::vs) ⇔
value_shape f s v ∧ value_shapes f ss vs) ∧
(value_shapes _ _ _ ⇔ F)
Termination
WF_REL_TAC `measure (\x. case x of | INL (_, x, _) => shape_size (\x.0) x | INR (_, y, _) => shape1_size (\x.0) y)`
End
Theorem value_shapes_list_rel:
∀f ss vs. value_shapes f ss vs ⇔ list_rel (value_shape f) ss vs
Proof
Induct_on `ss` >> Cases_on `vs` >> rw [value_shape_def]
QED
Theorem value_shape_cases:
∀f s v.
value_shape f s v ⇔
(∃n t x. s = Flat n t ∧ v = FlatV x ∧ f n t x) ∨
(∃s2 n vs. s = Array s2 n ∧ v = AggV vs ∧
every (value_shape f s2) vs ∧ length vs = n) ∨
(∃ss vs. s = Tuple ss ∧ v = AggV vs ∧ value_shapes f ss vs)
Proof
rw [] >>
Cases_on `s` >> Cases_on `v` >> rw [value_shape_def] >> metis_tac []
QED
Definition sizeof_def:
(sizeof (Flat n t) = n) ∧
(sizeof (Array s n) = n * sizeof s) ∧
(sizeof (Tuple ss) = sum (map sizeof ss))
Termination
WF_REL_TAC `measure (shape_size (\x.0))` >> rw [] >>
Induct_on `ss` >> rw [definition "shape_size_def"] >>
res_tac >> decide_tac
End
Definition interval_to_set_def:
interval_to_set (Interval _ start stop) =
{ n | start ≤ n ∧ n < stop }
End
Definition interval_ok_def:
interval_ok (Interval b i1 i2) valid_addresses ⇔
i1 ≤ i2 ∧ image A (interval_to_set (Interval b i1 i2)) ⊆ valid_addresses
End
Definition interval_freeable_def:
interval_freeable (Interval b _ _) ⇔ b
End
Definition is_allocated_def:
is_allocated b1 h ⇔
interval_ok b1 h.valid_addresses ∧
∃b2. b2 ∈ h.allocations ∧ (interval_freeable b1 ⇔ interval_freeable b2) ∧
interval_to_set b1 ⊆ interval_to_set b2
End
Definition is_free_def:
is_free b1 h ⇔
interval_ok b1 h.valid_addresses ∧
∀b2. b2 ∈ h.allocations ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
End
(* The allocations are of intervals that don't overlap *)
Definition allocations_ok_def:
allocations_ok h ⇔
∀i1 i2.
i1 ∈ h.allocations ∧ i2 ∈ h.allocations
⇒
interval_ok i1 h.valid_addresses ∧ interval_ok i2 h.valid_addresses ∧
(interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2)
End
(* The heap maps exactly the address in the allocations *)
Definition heap_ok_def:
heap_ok h ⇔
allocations_ok h ∧
∀n. flookup h.memory (A n) ≠ None ⇔ ∃i. i ∈ h.allocations ∧ n ∈ interval_to_set i
End
Definition get_bytes_def:
get_bytes h (Interval _ start stop) =
map
(λoff.
case flookup h.memory (A (start + off)) of
| None => (F, 0w)
| Some w => w)
(count_list (stop - start))
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 with memory := h.memory |+ (A n, (p, b))))
End
(* Allocate a free chunk of memory, and write non-deterministic bytes into it *)
Inductive allocate:
b = Interval T p (p + size) ∧
is_free b h ∧
length bytes = size
⇒
allocate h size tag (w, set_bytes tag bytes p
<| memory := h.memory;
allocations := { b } ∪ h.allocations;
valid_addresses := h.valid_addresses |>)
End
Definition deallocate_def:
deallocate addrs h =
let to_remove = { Interval T n stop | A n ∈ set addrs ∧ Interval T n stop ∈ h.allocations } in
<| memory := fdiff h.memory (image A (bigunion (image interval_to_set to_remove)));
allocations := h.allocations DIFF to_remove;
valid_addresses := h.valid_addresses |>
End
(* Read len bytes from the list of bytes, and convert it into a word value,
* little-endian encoding *)
Definition le_read_w_def:
le_read_w len (bs : word8 list) =
if length bs < len then
(l2w 256 (map w2n bs), [])
else
(l2w 256 (map w2n (take len bs)), drop len bs)
End
(* Return len bytes that are the little-endian encoding of the argument word *)
Definition le_write_w_def:
le_write_w len w =
let (l : word8 list) = map n2w (w2l 256 w) in
take len (l ++ replicate (len - length l) 0w)
End
(* Read a from a list of bytes bs to build a register value described by a
* shape. The function f is applied to the word read from a flat list of bytes
* in little-endian order. *)
Definition bytes_to_value_def:
(bytes_to_value f (Flat n t) bs = (FlatV o f n t ## I) (le_read_w n bs)) ∧
(bytes_to_value f (Array s n) bs = (AggV ## I) (read_array f n s bs)) ∧
(bytes_to_value f (Tuple ts) bs = (AggV ## I) (read_str f ts bs)) ∧
(read_array f 0 s bs = ([], bs)) ∧
(read_array f (Suc n) s bs =
let (v, bs) = bytes_to_value f s bs in
let (rest, bs) = read_array f n s bs in
(v::rest, bs)) ∧
(read_str f [] bs = ([], bs)) ∧
(read_str f (s::ss) bs =
let (v, bs) = bytes_to_value f s bs in
let (rest, bs) = read_str f ss bs in
(v::rest, bs))
Termination
WF_REL_TAC `measure (λx. case x of
| INL (_, t, bs) => shape_size (\x.0) t
| INR (INL (_, n, t, bs)) => n + shape_size (\x.0) t
| INR (INR (_, ts, bs)) => shape1_size (\x.0) ts)`
End
(* Convert the given value to a list of bytes, the function gives the size, and
* a machine word for a flat value *)
Definition value_to_bytes_def:
(value_to_bytes f (FlatV x) =
let (size, word) = f x in
le_write_w size word) ∧
(value_to_bytes f (AggV vs) = flat (map (value_to_bytes f) vs))
Termination
WF_REL_TAC `measure (reg_v_size (\x. 0) o snd)` >>
Induct >> rw [definition "reg_v_size_def"] >>
TRY (first_x_assum drule) >>
decide_tac
End
(* ----- Theorems about converting between values and byte lists ----- *)
Theorem le_write_w_length:
∀l x. length (le_write_w l w) = l
Proof
rw [le_write_w_def]
QED
Theorem v2b_size_lem:
(∀(f:num->'a->'b->bool) s v. (∀n t x. f n t x ⇒ fst (g x) = n) ∧ value_shape f s v ⇒ length (value_to_bytes g v) = sizeof s) ∧
(∀(f:num->'a->'b->bool) ss vs. (∀n t x. f n t x ⇒ fst (g x) = n) ∧ value_shapes f ss vs ⇒ sum (map (length o value_to_bytes g) vs) = sum (map sizeof ss))
Proof
ho_match_mp_tac value_shape_ind >>
rw [value_to_bytes_def, sizeof_def, value_shape_def]
>- (
pairarg_tac >> simp [] >>
metis_tac [FST, le_write_w_length])
>- (
simp [LENGTH_FLAT, MAP_MAP_o, combinTheory.o_DEF] >>
Induct_on `vs` >> rw [ADD1] >> fs [LEFT_ADD_DISTRIB] >>
metis_tac [])
>- (fs [LENGTH_FLAT, ETA_THM, MAP_MAP_o, combinTheory.o_DEF] >> metis_tac [])
>- metis_tac [ADD_COMM]
QED
Theorem v2b_size:
∀f s v g. (∀n t x. f n t x ⇒ fst (g x) = n) ∧ value_shape f s v ⇒ length (value_to_bytes g v) = sizeof s
Proof
metis_tac [v2b_size_lem]
QED
Theorem b2v_size_lem:
(∀(f:num->'c ->'a word -> 'b) s bs. sizeof s ≤ length bs ⇒
∃v. bytes_to_value f s bs = (v, drop (sizeof s) bs)) ∧
(∀(f:num->'c ->'a word -> 'b) n s bs. n * sizeof s ≤ length bs ⇒
∃vs. read_array f n s bs = (vs, drop (n * sizeof s) bs)) ∧
(∀(f:num->'c ->'a word -> 'b) ss bs. sum (map sizeof ss) ≤ length bs ⇒
∃vs. read_str f ss bs = (vs, drop (sum (map sizeof ss)) bs))
Proof
ho_match_mp_tac bytes_to_value_ind >>
rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
fs []
>- (simp [PAIR_MAP] >> metis_tac [SND])
>- (
pairarg_tac >> rw [] >> pairarg_tac >> rw [] >>
fs [ADD1] >> rw [] >> fs [DROP_DROP_T, LEFT_ADD_DISTRIB])
>- fs [DROP_DROP_T, LEFT_ADD_DISTRIB]
QED
Theorem b2v_size:
∀f s bs. sizeof s ≤ length bs ⇒
∃v. bytes_to_value f s bs = (v, drop (sizeof s) bs)
Proof
metis_tac [b2v_size_lem]
QED
Theorem b2v_smaller:
∀f s bs. sizeof s ≤ length bs ⇒
length (snd (bytes_to_value f s bs)) = length bs - sizeof s
Proof
rw [] >> imp_res_tac b2v_size >>
Cases_on `bytes_to_value f s bs` >> fs [] >>
first_x_assum (qspec_then `f` mp_tac) >> rw []
QED
Theorem b2v_append_lem:
(∀(f:num->'c->'a word -> 'b) s bs. sizeof s ≤ length bs ⇒
bytes_to_value f s (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_value f s bs)) ∧
(∀(f:num->'c->'a word -> 'b) n s bs. n * sizeof s ≤ length bs ⇒
∃vs. read_array f n s (bs ++ bs') = (I ## (λx. x ++ bs')) (read_array f n s bs)) ∧
(∀(f:num->'c->'a word -> 'b) ss bs. sum (map sizeof ss) ≤ length bs ⇒
∃vs. read_str f ss (bs ++ bs') = (I ## (λx. x ++ bs')) (read_str f ss bs))
Proof
ho_match_mp_tac bytes_to_value_ind >>
rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
fs [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] >>
BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
first_x_assum irule >>
`sizeof s ≤ length bs` by decide_tac >>
qspec_then `f` drule b2v_smaller >>
disch_then (qspec_then `f` mp_tac) >>
rw [])
>- (
rpt (pairarg_tac >> simp []) >> fs [ADD1] >>
BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
first_x_assum irule >>
`sizeof s ≤ length bs` by decide_tac >>
qspec_then `f` drule b2v_smaller >>
disch_then (qspec_then `f` mp_tac) >>
rw [])
QED
Theorem b2v_append:
∀f s bs bs'. sizeof s ≤ length bs ⇒
bytes_to_value f s (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_value f s bs)
Proof
metis_tac [b2v_append_lem]
QED
Theorem le_read_write:
∀n w bs.
w2n w < 256 ** n ⇒ le_read_w n (le_write_w n w ⧺ bs) = (w, bs)
Proof
rw [le_read_w_def, le_write_w_length]
>- (
`take n (le_write_w n w ⧺ bs) = le_write_w n w`
by metis_tac [le_write_w_length, TAKE_LENGTH_APPEND] >>
simp [le_write_w_def, w2l_def, l2w_def] >>
Cases_on `w` >> simp [] >> fs [l2n_padding, TAKE_APPEND, take_replicate] >>
simp [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, mod_n2l] >>
rename1 `n2l 256 m` >>
Cases_on `n = 0` >> fs [] >>
`length (n2l 256 m) ≤ n`
by (
rw [LENGTH_n2l] >>
`256 = 2 ** 8` by EVAL_TAC >>
ASM_REWRITE_TAC [] >> simp [log_change_base_power, GSYM LESS_EQ] >>
`n2w m ≠ 0w` by simp [] >>
rw [] >> fs [bitTheory.LOG2_def, dimword_def] >>
`8 * (log 2 m DIV 8) ≤ log 2 m` by metis_tac [mul_div_bound, EVAL ``8 ≠ 0n``] >>
`LOG 2 m ≤ LOG 2 (256 ** n)` by simp [LOG_LE_MONO] >>
pop_assum mp_tac >>
`256 = 2 ** 8` by EVAL_TAC >>
ASM_REWRITE_TAC [EXP_MUL] >> simp [log_base_power] >>
Cases_on `log 2 m DIV 8 = n` >> rw [] >>
CCONTR_TAC >> fs [] >>
`log 2 m = (8 * (log 2 m DIV 8))` by intLib.COOPER_TAC >> fs [] >>
`2 ** log 2 m = 2 ** (8 * (log 2 m DIV 8))` by rw [] >>
fs [EXP_EXP_MULT] >>
`2 ** log 2 m ≤ m` by rw [exp_log_bound] >>
decide_tac) >>
simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG])
>- metis_tac [le_write_w_length, DROP_LENGTH_APPEND]
QED
Theorem le_write_read:
∀n w bs bs'.
256 ** n ≤ dimword (:'a) ∧
n ≤ length bs ∧
le_read_w n bs = (w:'a word, bs')
⇒
le_write_w n w ++ bs' = bs
Proof
rw [le_read_w_def] >>
qmatch_goalsub_abbrev_tac `l2w _ l` >>
`le_write_w n (l2w 256 l) = take n bs` suffices_by metis_tac [TAKE_DROP] >>
simp [le_write_w_def, w2l_l2w] >>
`l2n 256 l < 256 ** n`
by (
`n ≤ length bs` by decide_tac >>
metis_tac [l2n_lt, LENGTH_TAKE, LENGTH_MAP, EVAL ``0n < 256``]) >>
fs [] >>
`every ($> 256) l`
by (
simp [EVERY_MAP, Abbr `l`] >> irule EVERY_TAKE >> simp [] >>
rpt (pop_assum kall_tac) >>
Induct_on `bs` >> rw [] >>
Cases_on `h` >> fs []) >>
rw [n2l_l2n]
>- (
rw [TAKE_def, take_replicate] >>
Cases_on `n` >> fs [] >>
rfs [l2n_0] >> unabbrev_all_tac >> fs [EVERY_MAP] >>
ONCE_REWRITE_TAC [GSYM REPLICATE] >>
qmatch_goalsub_abbrev_tac `take n _` >>
qpat_assum `¬(_ < _)` mp_tac >>
qpat_assum `every (\x. 0 = w2n x) _` mp_tac >>
rpt (pop_assum kall_tac) >>
qid_spec_tac `bs` >>
Induct_on `n` >> rw [] >>
Cases_on `bs` >> rw [] >> fs [] >>
Cases_on `h` >> fs [] >>
first_x_assum irule >> rw [] >>
irule MONO_EVERY >>
qexists_tac `(λx. 0 = w2n x)` >> rw []) >>
fs [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
`exists (\y. 0 ≠ y) l`
by (
fs [l2n_eq_0, combinTheory.o_DEF] >> fs [EXISTS_MEM, EVERY_MEM] >>
qexists_tac `x` >> rfs [MOD_MOD, GREATER_DEF]) >>
simp [LOG_l2n_dropWhile] >>
`length (dropWhile ($= 0) (reverse l)) ≠ 0`
by (
Cases_on `l` >> fs [dropWhile_eq_nil, combinTheory.o_DEF, EXISTS_REVERSE]) >>
`0 < length (dropWhile ($= 0) (reverse l))` by decide_tac >>
fs [SUC_PRE] >>
`map n2w l = take n bs`
by (simp [Abbr `l`, MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, n2w_w2n]) >>
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] >>
rw [MIN_DEF] >> fs []
>- (
simp [TAKE_APPEND, TAKE_TAKE_MIN, MIN_DEF, take_replicate] >>
`replicate (length l − length (dropWhile ($= 0) (reverse l))) 0w =
take (length l − (length (dropWhile ($= 0) (reverse l)))) (drop (length (dropWhile ($= 0) (reverse l))) bs)`
suffices_by (rw [] >> irule take_drop_partition >> simp []) >>
rw [LIST_EQ_REWRITE, EL_REPLICATE, EL_TAKE, EL_DROP] >>
`length (dropWhile ($= 0) (reverse l)) =
length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs)))`
by (
`reverse l = reverse (take (length l) (map w2n bs))` by metis_tac [] >>
ONCE_ASM_REWRITE_TAC [] >>
qpat_x_assum `Abbrev (l = _)` kall_tac >>
simp [GSYM MAP_TAKE, GSYM MAP_REVERSE, dropWhile_map, combinTheory.o_DEF]) >>
fs [] >>
`x + length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs))) < length l` by decide_tac >>
drule (SIMP_RULE std_ss [LET_THM] dropWhile_rev_take) >>
rw [] >>
REWRITE_TAC [GSYM w2n_11, word_0_n2w] >>
simp [])
>- rw [TAKE_APPEND, TAKE_TAKE]
QED
Theorem b2v_v2b_lem:
(∀f s v.
value_shape f s v ⇒
(∀x t n. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ w2n (snd (h x)) < 256 ** n) ⇒
∀bs.
bytes_to_value (g:num -> 'c -> 'a word -> 'b) s (value_to_bytes h v ++ bs) = (v, bs)) ∧
(∀f ss vs.
value_shapes f ss vs ⇒
(∀x t n. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ w2n (snd (h x)) < 256 ** n) ⇒
∀bs.
read_str (g:num -> 'c -> 'a word -> 'b) ss (flat (map (value_to_bytes h) vs) ++ bs) = (vs, bs))
Proof
ho_match_mp_tac value_shape_ind >> rw [value_shape_def] >>
fs [bytes_to_value_def, value_to_bytes_def] >> rw []
>- (
pairarg_tac >> fs [] >>
first_x_assum drule >> simp [] >> rw [] >>
simp [le_read_write])
>- (
qmatch_abbrev_tac `_ x = _` >>
`x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
unabbrev_all_tac >>
qid_spec_tac `bs` >> Induct_on `vs` >> simp [bytes_to_value_def] >>
rw [] >> fs [definition "reg_v_size_def"] >>
pairarg_tac >> fs [] >>
pairarg_tac >> fs [] >>
rename1 `value_shape _ s v1` >>
qpat_x_assum `_ ⇒ !bs. P bs` mp_tac >> impl_tac >> simp [] >>
metis_tac [APPEND_ASSOC, PAIR_EQ])
>- (
qmatch_abbrev_tac `_ x = _` >>
`x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
metis_tac [])
>- (
pairarg_tac >> fs [] >>
pairarg_tac >> fs [] >>
metis_tac [APPEND_ASSOC, PAIR_EQ])
QED
Theorem b2v_v2b:
∀f g h s v bs.
value_shape f s v ⇒
(∀x n t. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ w2n (snd (h x)) < 256 ** n) ⇒
bytes_to_value g s (value_to_bytes h v ++ bs) = (v, bs)
Proof
metis_tac [b2v_v2b_lem]
QED
Theorem flookup_set_bytes:
∀tag bytes n h n'.
flookup ((set_bytes tag bytes n h).memory) (A n') =
if n ≤ n' ∧ n' < n + length bytes then
Some (tag, el (n' - n) bytes)
else
flookup h.memory (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 set_bytes_unchanged:
∀t bs p h. (set_bytes t bs p h).valid_addresses = h.valid_addresses ∧
(set_bytes t bs p h).allocations = h.allocations
Proof
Induct_on `bs` >> rw [set_bytes_def]
QED
Theorem allocate_unchanged:
∀h1 v1 t h2 v2.
allocate h1 v1 t (v2, h2)
⇒
h1.valid_addresses = h2.valid_addresses ∧
h1.allocations ⊆ h2.allocations
Proof
rw [allocate_cases] >> rw [set_bytes_unchanged]
QED
Theorem allocate_heap_ok:
∀h1 v1 t v2 h2. heap_ok h1 ∧ allocate h1 v1 t (v2,h2) ⇒ heap_ok h2
Proof
rw [allocate_cases, heap_ok_def]
>- (
fs [allocations_ok_def] >> rpt gen_tac >> disch_tac >> fs [is_free_def] >> rw [] >>
fs [set_bytes_unchanged] >> metis_tac [INTER_COMM])
>- (
rw [flookup_set_bytes, set_bytes_unchanged]
>- rw [RIGHT_AND_OVER_OR, EXISTS_OR_THM, interval_to_set_def] >>
eq_tac >> rw [] >> fs [interval_to_set_def] >>
metis_tac [])
QED
Theorem set_bytes_heap_ok:
∀h tag bytes n b.
heap_ok h ∧ is_allocated (Interval b n (n + length bytes)) h
⇒
heap_ok (set_bytes tag bytes n h)
Proof
rw [heap_ok_def]
>- (fs [allocations_ok_def] >> rw [set_bytes_unchanged] >> metis_tac [])
>- (
fs [flookup_set_bytes, set_bytes_unchanged] >> rw [] >>
fs [is_allocated_def, interval_to_set_def, SUBSET_DEF] >>
metis_tac [LESS_EQ_REFL, DECIDE ``!x y. x < x + SUC y``])
QED
export_theory ();

172
sledge/semantics/miscScript.sml
Unescape View File

@ -0,0 +1,172 @@
(*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
(* Misc. theorems that aren't specific to the semantics of LLVM or Sledge. These
* could be upstreamed to HOL, and should eventually. *)
open HolKernel boolLib bossLib Parse;
open listTheory rich_listTheory arithmeticTheory wordsTheory;
open finite_mapTheory open logrootTheory numposrepTheory;
open settingsTheory;
new_theory "misc";
numLib.prefer_num ();
(* ----- Theorems about list library functions ----- *)
Theorem dropWhile_map:
∀P f l. dropWhile P (map f l) = map f (dropWhile (P o f) l)
Proof
Induct_on `l` >> rw []
QED
Theorem dropWhile_prop:
∀P l x. x < length l - length (dropWhile P l) ⇒ P (el x l)
Proof
Induct_on `l` >> rw [] >>
Cases_on `x` >> fs []
QED
Theorem dropWhile_rev_take:
∀P n l x.
let len = length (dropWhile P (reverse (take n l))) in
x + len < n ∧ n ≤ length l ⇒ P (el (x + len) l)
Proof
rw [] >>
`P (el ((n - 1 - x - length (dropWhile P (reverse (take n l))))) (reverse (take n l)))`
by (irule dropWhile_prop >> simp [LENGTH_REVERSE]) >>
rfs [EL_REVERSE, EL_TAKE, PRE_SUB1]
QED
Theorem take_replicate:
∀m n x. take m (replicate n x) = replicate (min m n) x
Proof
Induct_on `n` >> rw [TAKE_def, MIN_DEF] >> fs [] >>
Cases_on `m` >> rw []
QED
Theorem length_take_less_eq:
∀n l. length (take n l) ≤ n
Proof
Induct_on `l` >> rw [TAKE_def] >>
Cases_on `n` >> fs []
QED
Theorem flat_drop:
∀n m ls. flat (drop m ls) = drop (length (flat (take m ls))) (flat ls)
Proof
Induct_on `ls` >> rw [DROP_def, DROP_APPEND] >>
irule (GSYM DROP_LENGTH_TOO_LONG) >> simp []
QED
Theorem take_is_prefix:
∀n l. take n l ≼ l
Proof
Induct_on `l` >> rw [TAKE_def]
QED
Theorem sum_prefix:
∀l1 l2. l1 ≼ l2 ⇒ sum l1 ≤ sum l2
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 ----- *)
Theorem mul_div_bound:
∀m n. n ≠ 0 ⇒ m - (n - 1) ≤ n * (m DIV n) ∧ n * (m DIV n) ≤ m
Proof
rw [] >>
`0 < n` by decide_tac >>
drule DIVISION >> disch_then (qspec_then `m` mp_tac) >>
decide_tac
QED
Theorem exp_log_bound:
∀b n. 1 < b ∧ n ≠ 0 ⇒ n DIV b + 1 ≤ b ** (log b n) ∧ b ** (log b n) ≤ n
Proof
rw [] >> `0 < n` by decide_tac >>
drule LOG >> disch_then drule >> rw [] >>
fs [ADD1, EXP_ADD] >>
simp [DECIDE ``∀x y. x + 1 ≤ y ⇔ x < y``] >>
`∃x. b = Suc x` by intLib.COOPER_TAC >>
`b * (n DIV b) < b * b ** log b n` suffices_by metis_tac [LESS_MULT_MONO] >>
pop_assum kall_tac >>
`b ≠ 0` by decide_tac >>
drule mul_div_bound >> disch_then (qspec_then `n` mp_tac) >>
decide_tac
QED
Theorem log_base_power:
∀n b. 1 < b ⇒ log b (b ** n) = n
Proof
Induct >> rw [EXP, LOG_1] >>
Cases_on `n` >> rw [LOG_BASE] >>
first_x_assum drule >> rw [] >>
simp [Once EXP, LOG_MULT]
QED
Theorem log_change_base_power:
∀m n b. 1 < b ∧ m ≠ 0 ∧ n ≠ 0 ⇒ log (b ** n) m = log b m DIV n
Proof
rw [] >> irule LOG_UNIQUE >>
rw [ADD1, EXP_MUL, LEFT_ADD_DISTRIB] >>
qmatch_goalsub_abbrev_tac `x DIV _` >>
drule mul_div_bound >> disch_then (qspec_then `x` mp_tac) >> rw []
>- (
irule LESS_LESS_EQ_TRANS >>
qexists_tac `b ** (x+1)` >> rw [] >>
unabbrev_all_tac >>
simp [EXP_ADD] >>
`b * (m DIV b + 1) ≤ b * b ** log b m`
by metis_tac [exp_log_bound, LESS_MONO_MULT, MULT_COMM] >>
`m < b * (m DIV b + 1)` suffices_by decide_tac >>
simp [LEFT_ADD_DISTRIB] >>
`b ≠ 0` by decide_tac >>
`m - (b - 1) ≤ b * (m DIV b)` by metis_tac [mul_div_bound] >>
fs [])
>- (
irule LESS_EQ_TRANS >>
qexists_tac `b ** (log b m)` >> rw [] >>
unabbrev_all_tac >>
metis_tac [exp_log_bound])
QED
(* ----- Theorems about word stuff ----- *)
Theorem l2n_padding:
∀ws n. l2n 256 (ws ++ map w2n (replicate n 0w)) = l2n 256 ws
Proof
Induct >> rw [l2n_def] >>
Induct_on `n` >> rw [l2n_def]
QED
Theorem l2n_0:
∀l b. b ≠ 0 ∧ every ($> b) l⇒ (l2n b l = 0 ⇔ every ($= 0) l)
Proof
Induct >> rw [l2n_def] >>
eq_tac >> rw []
QED
Theorem mod_n2l:
∀d n. 0 < d ⇒ map (\x. x MOD d) (n2l d n) = n2l d n
Proof
rw [] >> drule n2l_BOUND >> disch_then (qspec_then `n` mp_tac) >>
qspec_tac (`n2l d n`, `l`) >>
Induct >> rw []
QED
export_theory ();
Write Preview
Loading…
Cancel
Save