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

[sledge sem] Fix global variables

Browse Source 
Summary:
Add a field to LLAIR variables to indicate whether they are global or
local. Update the LLVM semantics for constant expression evaluation to
be relational, so that it doesn't have to have an answer for references
to undefined globals.

Reviewed By: jberdine

Differential Revision: D19446312

fbshipit-source-id: 9bbfd180e
master
Scott Owens 5 years ago committed by Facebook Github Bot
parent 63428e7b69
commit 8d95ef7e3c
7 changed files with 282 additions and 224 deletions
Show Stats Download Patch File Download Diff File

10
sledge/semantics/llairScript.sml
Unescape View File

@ -54,7 +54,8 @@ End
(* Based on the constructor functions in exp.mli rather than the type definition *) (* Based on the constructor functions in exp.mli rather than the type definition *)
Datatype: Datatype:
exp = exp =
| Var var (* Args: variable name, true for globals *)
| Var var bool
| Nondet | Nondet
(* Args: function name, block name *) (* Args: function name, block name *)
| Label label | Label label
@ -262,7 +263,12 @@ Inductive eval_exp:
(∀s v r. (∀s v r.
flookup s.locals v = Some r flookup s.locals v = Some r
⇒ ⇒
eval_exp s (Var v) r) ∧ eval_exp s (Var v F) r) ∧
(∀s v r.
flookup s.glob_addrs v = Some r
⇒
eval_exp s (Var v T) (FlatV (n2i r pointer_size))) ∧
(* TODO: Nondet I guess we need to know the type here *) (* TODO: Nondet I guess we need to know the type here *)
(* TODO: Label *) (* TODO: Label *)

16
sledge/semantics/llair_propScript.sml
Unescape View File

@ -124,7 +124,7 @@ Proof
QED QED
Theorem eval_exp_ignores_lem: Theorem eval_exp_ignores_lem:
∀s1 e v. eval_exp s1 e v ⇒ ∀s2. s1.locals = s2.locals ⇒ eval_exp s2 e v ∀s1 e v. eval_exp s1 e v ⇒ ∀s2. s1.locals = s2.locals ∧ s1.glob_addrs = s2.glob_addrs ⇒ eval_exp s2 e v
Proof Proof
ho_match_mp_tac eval_exp_ind >> ho_match_mp_tac eval_exp_ind >>
rw [] >> simp [Once eval_exp_cases] >> rw [] >> simp [Once eval_exp_cases] >>
@ -134,13 +134,14 @@ Proof
QED QED
Theorem eval_exp_ignores: Theorem eval_exp_ignores:
∀s1 e v s2. s1.locals = s2.locals ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v) ∀s1 e v s2. s1.locals = s2.locals ∧ s1.glob_addrs = s2.glob_addrs ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v)
Proof Proof
metis_tac [eval_exp_ignores_lem] metis_tac [eval_exp_ignores_lem]
QED QED
Definition exp_uses_def: Definition exp_uses_def:
(exp_uses (Var x) = {x}) ∧ (exp_uses (Var x T) = {}) ∧
(exp_uses (Var x F) = {x}) ∧
(exp_uses Nondet = {}) ∧ (exp_uses Nondet = {}) ∧
(exp_uses (Label _) = {}) ∧ (exp_uses (Label _) = {}) ∧
(exp_uses (Splat e1 e2) = exp_uses e1 ∪ exp_uses e2) ∧ (exp_uses (Splat e1 e2) = exp_uses e1 ∪ exp_uses e2) ∧
@ -164,7 +165,8 @@ End
Theorem eval_exp_ignores_unused_lem: Theorem eval_exp_ignores_unused_lem:
∀s1 e v. ∀s1 e v.
eval_exp s1 e v ⇒ eval_exp s1 e v ⇒
∀s2. DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ⇒ ∀s2. DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ∧
s1.glob_addrs = s2.glob_addrs ⇒
eval_exp s2 e v eval_exp s2 e v
Proof Proof
ho_match_mp_tac eval_exp_ind >> ho_match_mp_tac eval_exp_ind >>
@ -199,7 +201,11 @@ Proof
QED QED
Theorem eval_exp_ignores_unused: Theorem eval_exp_ignores_unused:
∀s1 e v s2. DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v) ∀s1 e v s2.
DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ∧
s1.glob_addrs = s2.glob_addrs
⇒
(eval_exp s1 e v ⇔ eval_exp s2 e v)
Proof Proof
metis_tac [eval_exp_ignores_unused_lem] metis_tac [eval_exp_ignores_unused_lem]
QED QED

123
sledge/semantics/llvmScript.sml
Unescape View File

@ -341,39 +341,43 @@ Definition unsigned_v_to_num_def:
(unsigned_v_to_num _ = None) (unsigned_v_to_num _ = None)
End End
Definition eval_const_def: Inductive eval_const:
(eval_const g (IntC W1 i) = FlatV (W1V (i2w i))) ∧ (∀g i. eval_const g (IntC W1 i) (FlatV (W1V (i2w i)))) ∧
(eval_const g (IntC W8 i) = FlatV (W8V (i2w i))) ∧ (∀g i. eval_const g (IntC W8 i) (FlatV (W8V (i2w i)))) ∧
(eval_const g (IntC W32 i) = FlatV (W32V (i2w i))) ∧ (∀g i. eval_const g (IntC W32 i) (FlatV (W32V (i2w i)))) ∧
(eval_const g (IntC W64 i) = FlatV (W64V (i2w i))) ∧ (∀g i. eval_const g (IntC W64 i) (FlatV (W64V (i2w i)))) ∧
(eval_const g (StrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧ (∀g tconsts rs.
(eval_const g (ArrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧ list_rel (eval_const g) (map snd tconsts) rs
(eval_const g (GepC ty ptr (t, idx) indices) = ⇒
case (eval_const g ptr, signed_v_to_num (eval_const g idx)) of eval_const g (StrC tconsts) (AggV rs)) ∧
| (FlatV (PtrV ptr), Some n) => (∀g tconsts rs.
let ns = map (λ(t,ci). case signed_v_to_num (eval_const g ci) of None => 0 | Some n => n) indices in list_rel (eval_const g) (map snd tconsts) rs
(case get_offset ty ns of ⇒
| None => FlatV UndefV eval_const g (ArrC tconsts) (AggV rs)) ∧
| Some off => FlatV (PtrV (n2w ((w2n ptr) + (sizeof ty) * n + off)))) (∀g ty ptr t idx indices ptr' n ns off vs v.
| _ => FlatV UndefV) ∧ eval_const g ptr (FlatV (PtrV ptr')) ∧
(eval_const g (GlobalC var) = eval_const g idx v ∧
case flookup g var of signed_v_to_num v = Some n ∧
| None => FlatV (PtrV 0w) list_rel (λ(t, ci) v. eval_const g ci v) indices vs ∧
| Some (s,w) => FlatV (PtrV w)) ∧ map signed_v_to_num vs = map Some ns ∧
(eval_const g UndefC = FlatV UndefV) get_offset ty ns = Some off
Termination ⇒
WF_REL_TAC `measure (const_size o snd)` >> rw [listTheory.MEM_MAP] >> eval_const g (GepC ty ptr (t, idx) indices) (FlatV (PtrV (n2w ((w2n ptr') + (sizeof ty) * n + off))))) ∧
TRY (∀g var s w.
(TRY (PairCases_on `y`) >> simp [] >> flookup g var = Some (s, w)
Induct_on `tconsts` >> rw [] >> rw [definition "const_size_def"] >> ⇒
res_tac >> fs [] >> NO_TAC) >> eval_const g (GlobalC var) (FlatV (PtrV w)))
Induct_on `indices` >> rw [] >> rw [definition "const_size_def"] >>
fs []
End End
Definition eval_def: Inductive eval:
(eval s (Variable v) = flookup s.locals v) ∧ (∀s x v.
(eval s (Constant c) = Some <| poison := F; value := eval_const s.globals c |>) flookup s.locals x = Some v
⇒
eval s (Variable x) v) ∧
(∀s c v.
eval_const s.globals c v
⇒
eval s (Constant c) <| poison := F; value := v |>)
End End
(* BEGIN Functions to interface to the generic memory model *) (* BEGIN Functions to interface to the generic memory model *)
@ -483,9 +487,12 @@ Definition do_icmp_def:
| _ => None) | _ => None)
End End
Definition do_phi_def: Inductive do_phi:
do_phi from_l s (Phi id _ entries) = (∀from_l s id lands entries e v.
option_join (option_map (λarg. option_map (\v. (id, v)) (eval s arg)) (alookup entries from_l)) alookup entries from_l = Some e ∧
eval s e v
⇒
do_phi from_l s (Phi id lands entries) (id, v))
End End
Definition extract_value_def: Definition extract_value_def:
@ -536,7 +543,7 @@ Inductive step_instr:
(∀prog s t a fr v st new_h. (∀prog s t a fr v st new_h.
s.stack = fr::st ∧ s.stack = fr::st ∧
deallocate fr.stack_allocs s.heap = new_h ∧ deallocate fr.stack_allocs s.heap = new_h ∧
eval s a = Some v eval s a v
⇒ ⇒
step_instr prog s step_instr prog s
(Ret (t, a)) Tau (Ret (t, a)) Tau
@ -549,7 +556,7 @@ Inductive step_instr:
status := s.status |>)) ∧ status := s.status |>)) ∧
(∀prog s a l1 l2 tf l p. (∀prog s a l1 l2 tf l p.
eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧ eval s a <| poison := p; value := FlatV (W1V tf) |> ∧
l = Some (if tf = 0w then l2 else l1) l = Some (if tf = 0w then l2 else l1)
⇒ ⇒
step_instr prog s step_instr prog s
@ -560,7 +567,7 @@ Inductive step_instr:
(∀prog s r t a args l1 l2. step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧ (∀prog s r t a args l1 l2. step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧
(∀prog s a exit_code v1. (∀prog s a exit_code v1.
eval s a = Some v1 ∧ eval s a v1 ∧
signed_v_to_int v1.value = Some exit_code signed_v_to_int v1.value = Some exit_code
⇒ ⇒
step_instr prog s step_instr prog s
@ -568,31 +575,33 @@ Inductive step_instr:
(s with status := Complete exit_code)) ∧ (s with status := Complete exit_code)) ∧
(∀prog s r nuw nsw t a1 a2 v3 v1 v2. (∀prog s r nuw nsw t a1 a2 v3 v1 v2.
eval s a1 = Some v1 ∧ eval s a1 v1 ∧
eval s a2 = Some v2 ∧ eval s a2 v2 ∧
do_sub nuw nsw v1 v2 t = Some v3 do_sub nuw nsw v1 v2 t = Some v3
⇒ ⇒
step_instr prog s step_instr prog s
(Sub r nuw nsw t a1 a2) Tau (Sub r nuw nsw t a1 a2) Tau
(inc_pc (update_result r v3 s))) ∧ (inc_pc (update_result r v3 s))) ∧
(∀prog s r t a const_indices v ns result. (∀prog s r t a const_indices v vs ns result.
eval s a = Some v ∧ eval s a v ∧
list_rel (eval_const s.globals) const_indices vs ∧
(* The manual implies (but does not explicitly state) that the indices are (* The manual implies (but does not explicitly state) that the indices are
* interpreted as signed numbers *) * interpreted as signed numbers *)
map (λci. signed_v_to_num (eval_const s.globals ci)) const_indices = map Some ns ∧ map signed_v_to_num vs = map Some ns ∧
extract_value v.value ns = Some result extract_value v.value ns = Some result
⇒ ⇒
step_instr prog s step_instr prog s
(Extractvalue r (t, a) const_indices) Tau (Extractvalue r (t, a) const_indices) Tau
(inc_pc (update_result r <| poison := v.poison; value := result |> s))) ∧ (inc_pc (update_result r <| poison := v.poison; value := result |> s))) ∧
(∀prog s r t1 a1 t2 a2 const_indices result v1 v2 ns. (∀prog s r t1 a1 t2 a2 const_indices result v1 v2 ns vs.
eval s a1 = Some v1 ∧ eval s a1 v1 ∧
eval s a2 = Some v2 ∧ eval s a2 v2 ∧
list_rel (eval_const s.globals) const_indices vs ∧
(* The manual implies (but does not explicitly state) that the indices are (* The manual implies (but does not explicitly state) that the indices are
* interpreted as signed numbers *) * interpreted as signed numbers *)
map (λci. signed_v_to_num (eval_const s.globals ci)) const_indices = map Some ns ∧ map signed_v_to_num vs = map Some ns ∧
insert_value v1.value v2.value ns = Some result insert_value v1.value v2.value ns = Some result
⇒ ⇒
step_instr prog s step_instr prog s
@ -601,7 +610,7 @@ Inductive step_instr:
<| poison := (v1.poison ∨ v2.poison); value := result |> s))) ∧ <| poison := (v1.poison ∨ v2.poison); value := result |> s))) ∧
(∀prog s r t t1 a1 ptr new_h v n n2. (∀prog s r t t1 a1 ptr new_h v n n2.
eval s a1 = Some v ∧ eval s a1 v ∧
(* TODO Question is the number to allocate interpreted as a signed or (* TODO Question is the number to allocate interpreted as a signed or
* unsigned quantity. E.g., if we allocate i8 0xFF does that do 255 or -1? *) * unsigned quantity. E.g., if we allocate i8 0xFF does that do 255 or -1? *)
signed_v_to_num v.value = Some n ∧ signed_v_to_num v.value = Some n ∧
@ -614,7 +623,7 @@ Inductive step_instr:
(s with heap := new_h)))) ∧ (s with heap := new_h)))) ∧
(∀prog s r t t1 a1 pbytes w interval freeable p1. (∀prog s r t t1 a1 pbytes w interval freeable p1.
eval s a1 = Some <| poison := p1; value := FlatV (PtrV w) |> ∧ eval s a1 <| poison := p1; value := FlatV (PtrV w) |> ∧
interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧ interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
is_allocated interval s.heap ∧ is_allocated interval s.heap ∧
pbytes = get_bytes s.heap interval ∧ pbytes = get_bytes s.heap interval ∧
@ -627,8 +636,8 @@ Inductive step_instr:
s))) ∧ s))) ∧
(∀prog s t1 a1 t2 a2 obs p2 bytes w v1 freeable interval. (∀prog s t1 a1 t2 a2 obs p2 bytes w v1 freeable interval.
eval s a2 = Some <| poison := p2; value := FlatV (PtrV w) |> ∧ eval s a2 <| poison := p2; value := FlatV (PtrV w) |> ∧
eval s a1 = Some v1 ∧ eval s a1 v1 ∧
interval = Interval freeable (w2n w) (w2n w + sizeof t1) ∧ interval = Interval freeable (w2n w) (w2n w + sizeof t1) ∧
is_allocated interval s.heap ∧ is_allocated interval s.heap ∧
bytes = llvm_value_to_bytes v1.value ∧ bytes = llvm_value_to_bytes v1.value ∧
@ -640,8 +649,8 @@ Inductive step_instr:
(inc_pc (s with heap := set_bytes p2 bytes (w2n w) s.heap))) ∧ (inc_pc (s with heap := set_bytes p2 bytes (w2n w) s.heap))) ∧
(∀prog s r t t1 a1 tindices v1 i1 indices v w1 i is off ptr. (∀prog s r t t1 a1 tindices v1 i1 indices v w1 i is off ptr.
map (eval s o snd) tindices = map Some (i1::indices) ∧ list_rel (eval s o snd) tindices (i1::indices) ∧
eval s a1 = Some v ∧ eval s a1 v ∧
v.value = FlatV (PtrV w1) ∧ v.value = FlatV (PtrV w1) ∧
(* The manual states that the indices are interpreted as signed numbers *) (* The manual states that the indices are interpreted as signed numbers *)
signed_v_to_num i1.value = Some i ∧ signed_v_to_num i1.value = Some i ∧
@ -657,7 +666,7 @@ Inductive step_instr:
s))) ∧ s))) ∧
(∀prog s cop r t1 a1 t v1 v2. (∀prog s cop r t1 a1 t v1 v2.
eval s a1 = Some v1 ∧ eval s a1 v1 ∧
do_cast cop v1.value t = Some v2 do_cast cop v1.value t = Some v2
⇒ ⇒
step_instr prog s step_instr prog s
@ -665,8 +674,8 @@ Inductive step_instr:
(inc_pc (update_result r <| poison := v1.poison; value := v2 |> s))) ∧ (inc_pc (update_result r <| poison := v1.poison; value := v2 |> s))) ∧
(∀prog s r c t a1 a2 v3 v1 v2. (∀prog s r c t a1 a2 v3 v1 v2.
eval s a1 = Some v1 ∧ eval s a1 v1 ∧
eval s a2 = Some v2 ∧ eval s a2 v2 ∧
do_icmp c v1 v2 = Some v3 do_icmp c v1 v2 = Some v3
⇒ ⇒
step_instr prog s step_instr prog s
@ -675,7 +684,7 @@ Inductive step_instr:
(∀prog s r t fname targs d vs. (∀prog s r t fname targs d vs.
alookup prog fname = Some d ∧ alookup prog fname = Some d ∧
map (eval s o snd) targs = map Some vs list_rel (eval s o snd) targs vs
⇒ ⇒
step_instr prog s step_instr prog s
(Call r t fname targs) Tau (Call r t fname targs) Tau
@ -741,7 +750,7 @@ Inductive step:
*) *)
(∀p s updates from_l phis. (∀p s updates from_l phis.
get_instr p s.ip (Inr (from_l, phis)) ∧ get_instr p s.ip (Inr (from_l, phis)) ∧
map (do_phi from_l s) phis = map Some updates list_rel (do_phi from_l s) phis updates
⇒ ⇒
step p s Tau (inc_pc (s with locals := s.locals |++ updates))) step p s Tau (inc_pc (s with locals := s.locals |++ updates)))
End End

12
sledge/semantics/llvm_to_llairScript.sml
Unescape View File

@ -95,7 +95,7 @@ Definition translate_const_def:
Record (map (λ(ty, c). translate_const gmap c) tcs)) ∧ Record (map (λ(ty, c). translate_const gmap c) tcs)) ∧
(translate_const gmap (ArrC tcs) = (translate_const gmap (ArrC tcs) =
Record (map (λ(ty, c). translate_const gmap c) tcs)) ∧ Record (map (λ(ty, c). translate_const gmap c) tcs)) ∧
(translate_const gmap (GlobalC g) = Var (translate_glob_var gmap g)) ∧ (translate_const gmap (GlobalC g) = Var (translate_glob_var gmap g) T) ∧
(* TODO *) (* TODO *)
(translate_const gmap (GepC _ _ _ _) = ARB) ∧ (translate_const gmap (GepC _ _ _ _) = ARB) ∧
(translate_const gmap UndefC = Nondet) (translate_const gmap UndefC = Nondet)
@ -112,7 +112,7 @@ Definition translate_arg_def:
(* With the current strategy of threading the emap through the whole (* With the current strategy of threading the emap through the whole
* function, we should never get a None here. * function, we should never get a None here.
*) *)
| None => Var (translate_reg r (IntT W64)) | None => Var (translate_reg r (IntT W64)) F
| Some e => e) | Some e => e)
End End
@ -271,8 +271,8 @@ Definition classify_instr_def:
End End
Definition extend_emap_non_exp_def: Definition extend_emap_non_exp_def:
(extend_emap_non_exp emap (Load r t _) = emap |+ (r, Var (translate_reg r t))) ∧ (extend_emap_non_exp emap (Load r t _) = emap |+ (r, Var (translate_reg r t) F)) ∧
(extend_emap_non_exp emap (Call r t _ _) = emap |+ (r, Var (translate_reg r t))) ∧ (extend_emap_non_exp emap (Call r t _ _) = emap |+ (r, Var (translate_reg r t) F)) ∧
(extend_emap_non_exp emap _ = emap) (extend_emap_non_exp emap _ = emap)
End End
@ -317,7 +317,7 @@ Definition translate_instrs_def:
let x = translate_reg r t in let x = translate_reg r t in
let e = translate_instr_to_exp gmap emap i in let e = translate_instr_to_exp gmap emap i in
if r ∈ reg_to_keep then if r ∈ reg_to_keep then
let (bs, emap') = translate_instrs l gmap (emap |+ (r, Var x)) reg_to_keep is in let (bs, emap') = translate_instrs l gmap (emap |+ (r, Var x F)) reg_to_keep is in
(add_to_first_block (Move [(x, e)]) bs, emap') (add_to_first_block (Move [(x, e)]) bs, emap')
else else
translate_instrs l gmap (emap |+ (r, e)) reg_to_keep is translate_instrs l gmap (emap |+ (r, e)) reg_to_keep is
@ -367,7 +367,7 @@ End
Definition header_to_emap_upd_def: Definition header_to_emap_upd_def:
(header_to_emap_upd Entry = []) ∧ (header_to_emap_upd Entry = []) ∧
(header_to_emap_upd (Head phis _) = (header_to_emap_upd (Head phis _) =
map (λx. case x of Phi r t largs => (r, Var (translate_reg r t))) phis) map (λx. case x of Phi r t largs => (r, Var (translate_reg r t) F)) phis)
End End
Definition translate_block_def: Definition translate_block_def:

334
sledge/semantics/llvm_to_llair_propScript.sml
Unescape View File

@ -48,19 +48,6 @@ Definition num_calls_def:
num_calls is = length (filter is_call is) num_calls is = length (filter is_call is)
End End
(* TODO: remove?
Definition build_phi_block_def:
build_phi_block gmap emap f entry from_l to_l phis =
generate_move_block [(to_l, (translate_header (dest_fn f) gmap emap entry (Head phis ARB), (ARB:block)))]
(translate_label_opt (dest_fn f) entry from_l) to_l
End
Definition build_phi_emap_def:
build_phi_emap phis =
map (\x. case x of Phi r t _ => (r, Var (translate_reg r t))) phis
End
*)
Inductive pc_rel: Inductive pc_rel:
(* LLVM side points to a normal instruction *) (* LLVM side points to a normal instruction *)
(∀prog emap ip bp d b idx b' prev_i gmap rest. (∀prog emap ip bp d b idx b' prev_i gmap rest.
@ -105,31 +92,37 @@ End
*) *)
Definition emap_invariant_def: Definition emap_invariant_def:
emap_invariant prog emap ip locals locals' r = emap_invariant prog emap s s' r =
∃v v' e. ∃v v' e.
v_rel v.value v' ∧ v_rel v.value v' ∧
flookup locals r = Some v ∧ flookup s.locals r = Some v ∧
flookup emap r = Some e ∧ eval_exp <| locals := locals' |> e v' ∧ flookup emap r = Some e ∧ eval_exp s' e v' ∧
(* Each register used in e is dominated by an assignment to that (* Each register used in e is dominated by an assignment to that
* register for the entire live range of r. *) * register for the entire live range of r. *)
(∀ip1 r'. ip1.f = ip.f ∧ r ∈ live prog ip1 ∧ r' ∈ exp_uses e ⇒ (∀ip1 r'. ip1.f = s.ip.f ∧ r ∈ live prog ip1 ∧ r' ∈ exp_uses e ⇒
∃ip2. untranslate_reg r' ∈ assigns prog ip2 ∧ dominates prog ip2 ip1) ∃ip2. untranslate_reg r' ∈ assigns prog ip2 ∧ dominates prog ip2 ip1)
End End
Definition local_state_rel_def: Definition local_state_rel_def:
local_state_rel prog emap ip locals locals' ⇔ local_state_rel prog emap s s' ⇔
(* Live LLVM registers are mapped and have a related value in the emap (* Live LLVM registers are mapped and have a related value in the emap
* (after evaluating) *) * (after evaluating) *)
(∀r. r ∈ live prog ip ⇒ emap_invariant prog emap ip locals locals' r) (∀r. r ∈ live prog s.ip ⇒ emap_invariant prog emap s s' r)
End
Definition globals_rel_def:
globals_rel gmap gl gl' ⇔
BIJ (translate_glob_var gmap) (fdom gl) (fdom gl') ∧
∀k. k ∈ fdom gl ⇒
nfits (w2n (snd (gl ' k))) llair$pointer_size ∧
w2n (snd (gl ' k)) = gl' ' (translate_glob_var gmap k)
End End
Definition mem_state_rel_def: Definition mem_state_rel_def:
mem_state_rel prog gmap emap (s:llvm$state) (s':llair$state) ⇔ mem_state_rel prog gmap emap (s:llvm$state) (s':llair$state) ⇔
local_state_rel prog emap s.ip s.locals s'.locals ∧ local_state_rel prog emap s s' ∧
reachable prog s.ip ∧ reachable prog s.ip ∧
fmap_rel (\(_,n) n'. w2n n = n') globals_rel gmap s.globals s'.glob_addrs ∧
s.globals
(s'.glob_addrs f_o translate_glob_var gmap) ∧
heap_ok s.heap ∧ heap_ok s.heap ∧
erase_tags s.heap = s'.heap ∧ erase_tags s.heap = s'.heap ∧
s.status = s'.status s.status = s'.status
@ -159,7 +152,8 @@ Proof
QED QED
Triviality lemma: Triviality lemma:
((s:llair$state) with status := Complete code).locals = s.locals ((s:llair$state) with status := Complete code).locals = s.locals ∧
((s:llair$state) with status := Complete code).glob_addrs = s.glob_addrs
Proof Proof
rw [] rw []
QED QED
@ -189,12 +183,6 @@ Proof
>- metis_tac [next_ips_reachable] >- metis_tac [next_ips_reachable]
QED QED
Triviality record_lemma:
(<|locals := x|> :llair$state).locals = x
Proof
rw []
QED
Theorem mem_state_rel_update: Theorem mem_state_rel_update:
∀prog gmap emap s1 s1' v res_v r e i. ∀prog gmap emap s1 s1' v res_v r e i.
is_ssa prog ∧ is_ssa prog ∧
@ -214,8 +202,7 @@ Proof
>- ( >- (
rw [FLOOKUP_UPDATE] rw [FLOOKUP_UPDATE]
>- ( >- (
HINT_EXISTS_TAC >> rw [] HINT_EXISTS_TAC >> rw [] >>
>- metis_tac [eval_exp_ignores, record_lemma] >>
first_x_assum drule >> rw [] >> first_x_assum drule >> rw [] >>
first_x_assum drule >> rw [] >> first_x_assum drule >> rw [] >>
fs [exp_uses_def, translate_arg_def] >> fs [exp_uses_def, translate_arg_def] >>
@ -234,15 +221,15 @@ Proof
QED QED
Theorem emap_inv_updates_keep_same_ip1: Theorem emap_inv_updates_keep_same_ip1:
∀prog emap ip locals locals' vs res_vs rtys r. ∀prog emap ip s s' vs res_vs rtys r.
is_ssa prog ∧ is_ssa prog ∧
list_rel v_rel (map (\v. v.value) vs) res_vs ∧ list_rel v_rel (map (\v. v.value) vs) res_vs ∧
length rtys = length vs ∧ length rtys = length vs ∧
r ∈ set (map fst rtys) r ∈ set (map fst rtys)
⇒ ⇒
emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty))) rtys) ip emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty) F)) rtys)
(locals |++ zip (map fst rtys, vs)) (s with locals := s.locals |++ zip (map fst rtys, vs))
(locals' |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs)) (s' with locals := s'.locals |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
r r
Proof Proof
rw [emap_invariant_def, flookup_fupdate_list] >> rw [emap_invariant_def, flookup_fupdate_list] >>
@ -308,9 +295,10 @@ Proof
>- ( >- (
fs [exp_uses_def] >> rw [] >> fs [exp_uses_def] >> rw [] >>
Cases_on `fst rty` >> simp [translate_reg_def, untranslate_reg_def] >> Cases_on `fst rty` >> simp [translate_reg_def, untranslate_reg_def] >>
`∃ip. ip.f = ip1.f ∧ Reg s ∈ uses prog ip` rename1 `Reg r ∈ assigns _ _` >>
`∃ip. ip.f = ip1.f ∧ Reg r ∈ uses prog ip`
by ( by (
qabbrev_tac `x = (ip1.f = ip.f)` >> qabbrev_tac `x = (ip1.f = s.ip.f)` >>
fs [live_def] >> qexists_tac `last (ip1::path)` >> rw [] >> fs [live_def] >> qexists_tac `last (ip1::path)` >> rw [] >>
irule good_path_same_func >> irule good_path_same_func >>
qexists_tac `ip1::path` >> rw [MEM_LAST] >> qexists_tac `ip1::path` >> rw [MEM_LAST] >>
@ -319,19 +307,19 @@ Proof
QED QED
Theorem emap_inv_updates_keep_same_ip2: Theorem emap_inv_updates_keep_same_ip2:
∀prog emap ip locals locals' vs res_vs rtys r. ∀prog emap s s' vs res_vs rtys r.
is_ssa prog ∧ is_ssa prog ∧
r ∈ live prog ip ∧ r ∈ live prog s.ip ∧
assigns prog ip = set (map fst rtys) ∧ assigns prog s.ip = set (map fst rtys) ∧
emap_invariant prog emap ip locals locals' r ∧ emap_invariant prog emap s s' r ∧
list_rel v_rel (map (\v. v.value) vs) res_vs ∧ list_rel v_rel (map (\v. v.value) vs) res_vs ∧
length rtys = length vs ∧ length rtys = length vs ∧
reachable prog ip ∧ reachable prog s.ip ∧
¬mem r (map fst rtys) ¬mem r (map fst rtys)
⇒ ⇒
emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty))) rtys) ip emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty) F)) rtys)
(locals |++ zip (map fst rtys, vs)) (s with locals := s.locals |++ zip (map fst rtys, vs))
(locals' |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs)) (s' with locals := s'.locals |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
r r
Proof Proof
rw [emap_invariant_def, alistTheory.flookup_fupdate_list] >> rw [] >> rw [emap_invariant_def, alistTheory.flookup_fupdate_list] >> rw [] >>
@ -340,10 +328,11 @@ Proof
CASE_TAC >> rw [] CASE_TAC >> rw []
>- ( >- (
qexists_tac `v'` >> rw [] >> qexists_tac `v'` >> rw [] >>
`DRESTRICT (locals' |++ zip (map (λ(r,ty). translate_reg r ty) rtys, res_vs)) (exp_uses e) = qmatch_goalsub_abbrev_tac `eval_exp s_upd _ _` >>
DRESTRICT locals' (exp_uses e)` `DRESTRICT s_upd.locals (exp_uses e) = DRESTRICT s'.locals (exp_uses e) ∧
suffices_by metis_tac [eval_exp_ignores_unused, record_lemma] >> s_upd.glob_addrs = s'.glob_addrs`
rw [] >> suffices_by metis_tac [eval_exp_ignores_unused] >>
rw [Abbr `s_upd`] >>
qmatch_goalsub_abbrev_tac `_ |++ l = _` >> qmatch_goalsub_abbrev_tac `_ |++ l = _` >>
`l = []` suffices_by rw [FUPDATE_LIST_THM] >> `l = []` suffices_by rw [FUPDATE_LIST_THM] >>
rw [Abbr `l`, FILTER_EQ_NIL, LAMBDA_PROD] >> rw [Abbr `l`, FILTER_EQ_NIL, LAMBDA_PROD] >>
@ -353,13 +342,14 @@ Proof
rw [every_zip_fst, EVERY_MAP] >> rw [LAMBDA_PROD] >> rw [every_zip_fst, EVERY_MAP] >> rw [LAMBDA_PROD] >>
rw [EVERY_EL] >> pairarg_tac >> rw [] >> rw [EVERY_EL] >> pairarg_tac >> rw [] >>
qmatch_goalsub_rename_tac `translate_reg r1 ty1 ∉ exp_uses _` >> qmatch_goalsub_rename_tac `translate_reg r1 ty1 ∉ exp_uses _` >>
first_x_assum (qspecl_then [`ip`, `translate_reg r1 ty1`] mp_tac) >> rw [] >> first_x_assum (qspecl_then [`s.ip`, `translate_reg r1 ty1`] mp_tac) >> rw [] >>
CCONTR_TAC >> fs [] >> CCONTR_TAC >> fs [] >>
`ip2 = ip` `ip2 = s.ip`
by ( by (
fs [is_ssa_def, EXTENSION, IN_DEF] >> fs [is_ssa_def, EXTENSION, IN_DEF] >>
Cases_on `r1` >> fs [translate_reg_def, untranslate_reg_def] >> Cases_on `r1` >> fs [translate_reg_def, untranslate_reg_def] >>
`assigns prog ip (Reg s)` suffices_by metis_tac [reachable_dominates_same_func] >> rename1 `Reg reg` >>
`assigns prog s.ip (Reg reg)` suffices_by metis_tac [reachable_dominates_same_func] >>
rw [LIST_TO_SET_MAP, MEM_EL] >> rw [LIST_TO_SET_MAP, MEM_EL] >>
metis_tac [FST]) >> metis_tac [FST]) >>
metis_tac [dominates_irrefl]) >> metis_tac [dominates_irrefl]) >>
@ -371,15 +361,15 @@ Proof
QED QED
Theorem local_state_rel_next_ip: Theorem local_state_rel_next_ip:
∀prog emap ip1 ip2 locals locals'. ∀prog emap ip2 s s'.
local_state_rel prog emap ip1 locals locals' ∧ local_state_rel prog emap s s' ∧
ip2 ∈ next_ips prog ip1 ∧ ip2 ∈ next_ips prog s.ip ∧
(∀r. r ∈ assigns prog ip1 ⇒ emap_invariant prog emap ip1 locals locals' r) (∀r. r ∈ assigns prog s.ip ⇒ emap_invariant prog emap s s' r)
⇒ ⇒
local_state_rel prog emap ip2 locals locals' local_state_rel prog emap (s with ip := ip2) s'
Proof Proof
rw [local_state_rel_def, emap_invariant_def] >> rw [local_state_rel_def, emap_invariant_def] >>
Cases_on `r ∈ live prog ip1` >> fs [] Cases_on `r ∈ live prog s.ip` >> fs []
>- ( >- (
last_x_assum drule >> rw [] >> last_x_assum drule >> rw [] >>
ntac 3 HINT_EXISTS_TAC >> rw [] >> ntac 3 HINT_EXISTS_TAC >> rw [] >>
@ -394,44 +384,43 @@ Proof
QED QED
Theorem local_state_rel_updates_keep: Theorem local_state_rel_updates_keep:
∀rtys prog emap ip locals locals' vs res_vs i. ∀rtys prog emap s s' vs res_vs i.
is_ssa prog ∧ is_ssa prog ∧
set (map fst rtys) = assigns prog ip ∧ set (map fst rtys) = assigns prog s.ip ∧
local_state_rel prog emap ip locals locals' ∧ local_state_rel prog emap s s' ∧
length vs = length rtys ∧ length vs = length rtys ∧
list_rel v_rel (map (\v. v.value) vs) res_vs ∧ list_rel v_rel (map (\v. v.value) vs) res_vs ∧
i ∈ next_ips prog ip ∧ i ∈ next_ips prog s.ip ∧
reachable prog ip reachable prog s.ip
⇒ ⇒
local_state_rel prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty))) rtys) i local_state_rel prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty) F)) rtys)
(locals |++ zip (map fst rtys, vs)) (s with <| ip := i; locals := s.locals |++ zip (map fst rtys, vs) |>)
(locals' |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs)) (s' with locals := s'.locals |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
Proof Proof
rw [] >> irule local_state_rel_next_ip >> rw [] >> irule local_state_rel_next_ip >>
qexists_tac `ip` >> rw [] >>
fs [local_state_rel_def] >> rw [] fs [local_state_rel_def] >> rw []
>- (irule emap_inv_updates_keep_same_ip1 >> rw []) >> >- (irule emap_inv_updates_keep_same_ip1 >> rw []) >>
fs [local_state_rel_def] >> rw [] >>
Cases_on `mem r (map fst rtys)` Cases_on `mem r (map fst rtys)`
>- (irule emap_inv_updates_keep_same_ip1 >> rw []) >> >- (irule emap_inv_updates_keep_same_ip1 >> rw []) >>
irule emap_inv_updates_keep_same_ip2 >> rw [] irule emap_inv_updates_keep_same_ip2 >> rw []
QED QED
Theorem local_state_rel_update_keep: Theorem local_state_rel_update_keep:
∀prog emap ip locals locals' v res_v r i ty. ∀prog emap s s' v res_v r i ty.
is_ssa prog ∧ is_ssa prog ∧
assigns prog ip = {r} ∧ assigns prog s.ip = {r} ∧
local_state_rel prog emap ip locals locals' ∧ local_state_rel prog emap s s' ∧
v_rel v.value res_v ∧ v_rel v.value res_v ∧
reachable prog ip ∧ reachable prog s.ip ∧
i ∈ next_ips prog ip i ∈ next_ips prog s.ip
⇒ ⇒
local_state_rel prog (emap |+ (r, Var (translate_reg r ty))) local_state_rel prog (emap |+ (r, Var (translate_reg r ty) F))
i (locals |+ (r, v)) (locals' |+ (translate_reg r ty, res_v)) (s with <| ip := i; locals := s.locals |+ (r, v) |>)
(s' with locals := s'.locals |+ (translate_reg r ty, res_v))
Proof Proof
rw [] >> rw [] >>
drule local_state_rel_updates_keep >> drule local_state_rel_updates_keep >>
disch_then (qspecl_then [`[(r,ty)]`, `emap`, `ip`] mp_tac) >> disch_then (qspecl_then [`[(r,ty)]`, `emap`, `s`] mp_tac) >>
simp [] >> disch_then drule >> simp [] >> disch_then drule >>
disch_then (qspecl_then [`[v]`, `[res_v]`] mp_tac) >> disch_then (qspecl_then [`[v]`, `[res_v]`] mp_tac) >>
simp [] >> disch_then drule >> simp [] >> disch_then drule >>
@ -447,7 +436,7 @@ Theorem mem_state_rel_update_keep:
reachable prog s.ip ∧ reachable prog s.ip ∧
i ∈ next_ips prog s.ip i ∈ next_ips prog s.ip
⇒ ⇒
mem_state_rel prog gmap (emap |+ (r, Var (translate_reg r ty))) mem_state_rel prog gmap (emap |+ (r, Var (translate_reg r ty) F))
(s with <| ip := i; locals := s.locals |+ (r, v) |>) (s with <| ip := i; locals := s.locals |+ (r, v) |>)
(s' with locals := s'.locals |+ (translate_reg r ty, res_v)) (s' with locals := s'.locals |+ (translate_reg r ty, res_v))
Proof Proof
@ -457,7 +446,8 @@ Proof
QED QED
Triviality lemma: Triviality lemma:
((s:llair$state) with heap := h).locals = s.locals ((s:llair$state) with heap := h).locals = s.locals ∧
((s:llair$state) with heap := h).glob_addrs = s.glob_addrs
Proof Proof
rw [] rw []
QED QED
@ -475,6 +465,9 @@ Proof
fs [fmap_eq_flookup, FLOOKUP_o_f] >> rw [] >> fs [fmap_eq_flookup, FLOOKUP_o_f] >> rw [] >>
first_x_assum (qspec_then `x` mp_tac) >> first_x_assum (qspec_then `x` mp_tac) >>
BasicProvers.EVERY_CASE_TAC >> rw [] >> BasicProvers.EVERY_CASE_TAC >> rw [] >>
fs [emap_invariant_def]
>- metis_tac [eval_exp_ignores, lemma]
>- metis_tac [eval_exp_ignores, lemma] >>
Cases_on `x'` >> Cases_on `x''` >> fs [] Cases_on `x'` >> Cases_on `x''` >> fs []
QED QED
@ -988,57 +981,82 @@ Proof
pairarg_tac >> fs [] pairarg_tac >> fs []
QED QED
Triviality n2i_lem:
∀n. nfits n llair$pointer_size ⇒
n2i n llair$pointer_size = IntV (w2i (n2w n : word64)) llair$pointer_size
Proof
rw [pointer_size_def] >>
`2 ** 64 = dimword (:64)` by rw [dimword_64] >>
full_simp_tac bool_ss [nfits_def] >>
drule w2i_n2w >> rw []
QED
Theorem translate_constant_correct_lem: Theorem translate_constant_correct_lem:
(∀c s prog gmap emap s'. (∀c s prog gmap emap s' v.
mem_state_rel prog gmap emap s s' mem_state_rel prog gmap emap s s' ∧
eval_const s.globals c v
⇒ ⇒
∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel (eval_const s.globals c) v') ∧ ∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel v v') ∧
(∀(cs : (ty # const) list) s prog gmap emap s'. (∀(cs : (ty # const) list) s prog gmap emap s' vs.
mem_state_rel prog gmap emap s s' mem_state_rel prog gmap emap s s' ∧
list_rel (eval_const s.globals o snd) cs vs
⇒ ⇒
∃v'. list_rel (eval_exp s') (map (translate_const gmap o snd) cs) v' ∧ list_rel v_rel (map (eval_const s.globals o snd) cs) v') ∧ ∃v'. list_rel (eval_exp s') (map (translate_const gmap o snd) cs) v' ∧ list_rel v_rel vs v') ∧
(∀(tc : ty # const) s prog gmap emap s'. (∀(tc : ty # const) s prog gmap emap s' v.
mem_state_rel prog gmap emap s s' mem_state_rel prog gmap emap s s' ∧
eval_const s.globals (snd tc) v
⇒ ⇒
∃v'. eval_exp s' (translate_const gmap (snd tc)) v' ∧ v_rel (eval_const s.globals (snd tc)) v') ∃v'. eval_exp s' (translate_const gmap (snd tc)) v' ∧ v_rel v v')
Proof Proof
ho_match_mp_tac const_induction >> rw [translate_const_def] >> ho_match_mp_tac const_induction >> rw [translate_const_def] >>
simp [Once eval_exp_cases, eval_const_def] pop_assum mp_tac >> simp [Once eval_const_cases]
>- ( >- (
Cases_on `s` >> simp [eval_const_def, translate_size_def, v_rel_cases] >> rw [Once eval_exp_cases] >>
simp [Once eval_const_cases, translate_size_def, v_rel_cases] >>
metis_tac [truncate_2comp_i2w_w2i, dimindex_1, dimindex_8, dimindex_32, dimindex_64]) metis_tac [truncate_2comp_i2w_w2i, dimindex_1, dimindex_8, dimindex_32, dimindex_64])
>- ( >- (
rw [Once eval_exp_cases] >>
simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >> simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
fs [combinTheory.o_DEF, LAMBDA_PROD] >> fs [combinTheory.o_DEF, LAMBDA_PROD] >> rw [] >>
metis_tac []) first_x_assum drule >> disch_then irule >>
fs [LIST_REL_EL_EQN] >> rw [] >> rfs [] >>
first_x_assum drule >>
simp [EL_MAP] >>
Cases_on `el n cs` >> simp [])
>- ( >- (
rw [Once eval_exp_cases] >>
simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >> simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
fs [combinTheory.o_DEF, LAMBDA_PROD] >> fs [combinTheory.o_DEF, LAMBDA_PROD] >> rw [] >>
metis_tac []) first_x_assum drule >> disch_then irule >>
(* TODO: unimplemented stuff *) fs [LIST_REL_EL_EQN] >> rw [] >> rfs [] >>
first_x_assum drule >>
simp [EL_MAP] >>
Cases_on `el n cs` >> simp [])
(* TODO: unimplemented GEP stuff *)
>- cheat >- cheat
>- ( >- (
fs [mem_state_rel_def, fmap_rel_OPTREL_FLOOKUP] >> rw [Once eval_exp_cases] >> simp [v_rel_cases] >>
CASE_TAC >> fs [] >> first_x_assum (qspec_then `g` mp_tac) >> rw [] >> fs [mem_state_rel_def, globals_rel_def] >>
rename1 `option_rel _ _ opt` >> Cases_on `opt` >> fs [OPTREL_def] >> first_x_assum (qspec_then `g` mp_tac) >> rw [] >>
(* TODO: false at the moment, need to work out the llair story on globals *) qexists_tac `w2n w` >> rw [] >> fs [FLOOKUP_DEF]
cheat) >- (
(* TODO: unimplemented stuff *) rfs [] >>
>- cheat qpat_x_assum `w2n _ = _` (mp_tac o GSYM) >> rw [] >>
>- cheat simp [n2i_lem])
>- rfs [BIJ_DEF, INJ_DEF, SURJ_DEF])
>- metis_tac []
QED QED
Theorem translate_constant_correct: Theorem translate_constant_correct:
∀c s prog gmap emap s' g. ∀c s prog gmap emap s' g v.
mem_state_rel prog gmap emap s s' mem_state_rel prog gmap emap s s' ∧
eval_const s.globals c v
⇒ ⇒
∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel (eval_const s.globals c) v' ∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel v v'
Proof Proof
metis_tac [translate_constant_correct_lem] metis_tac [translate_constant_correct_lem]
QED QED
(* TODO: This isn't true, since the translation turns LLVM globals into llair
* locals *)
Theorem translate_const_no_reg[simp]: Theorem translate_const_no_reg[simp]:
∀gmap c. r ∉ exp_uses (translate_const gmap c) ∀gmap c. r ∉ exp_uses (translate_const gmap c)
Proof Proof
@ -1046,22 +1064,22 @@ Proof
rw [translate_const_def, exp_uses_def, MEM_MAP, METIS_PROVE [] ``x ∨ y ⇔ (~x ⇒ y)``] rw [translate_const_def, exp_uses_def, MEM_MAP, METIS_PROVE [] ``x ∨ y ⇔ (~x ⇒ y)``]
>- (pairarg_tac >> fs [] >> metis_tac []) >- (pairarg_tac >> fs [] >> metis_tac [])
>- (pairarg_tac >> fs [] >> metis_tac []) >- (pairarg_tac >> fs [] >> metis_tac [])
>- cheat (* TODO: unimplemented GEP stuff *)
>- cheat >- cheat
QED QED
Theorem translate_arg_correct: Theorem translate_arg_correct:
∀s a v prog gmap emap s'. ∀s a v prog gmap emap s'.
mem_state_rel prog gmap emap s s' ∧ mem_state_rel prog gmap emap s s' ∧
eval s a = Some v ∧ eval s a v ∧
arg_to_regs a ⊆ live prog s.ip arg_to_regs a ⊆ live prog s.ip
⇒ ⇒
∃v'. eval_exp s' (translate_arg gmap emap a) v' ∧ v_rel v.value v' ∃v'. eval_exp s' (translate_arg gmap emap a) v' ∧ v_rel v.value v'
Proof Proof
Cases_on `a` >> rw [eval_def, translate_arg_def] >> rw [] Cases_on `a` >> rw [eval_cases, translate_arg_def] >> rw []
>- metis_tac [translate_constant_correct] >> >- metis_tac [translate_constant_correct] >>
CASE_TAC >> fs [PULL_EXISTS, mem_state_rel_def, local_state_rel_def, emap_invariant_def, arg_to_regs_def] >> CASE_TAC >> fs [PULL_EXISTS, mem_state_rel_def, local_state_rel_def, emap_invariant_def, arg_to_regs_def] >>
res_tac >> rfs [] >> metis_tac [eval_exp_ignores, record_lemma] res_tac >> rfs [] >> metis_tac [eval_exp_ignores]
QED QED
Theorem is_allocated_mem_state_rel: Theorem is_allocated_mem_state_rel:
@ -1154,9 +1172,10 @@ Proof
QED QED
Theorem translate_extract_correct: Theorem translate_extract_correct:
∀prog gmap emap s1 s1' a v v1' e1' cs ns result. ∀prog gmap emap s1 s1' a v v1' e1' cs vs ns result.
mem_state_rel prog gmap emap s1 s1' ∧ mem_state_rel prog gmap emap s1 s1' ∧
map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧ list_rel (eval_const s1.globals) cs vs ∧
map signed_v_to_num vs = map Some ns ∧
extract_value v ns = Some result ∧ extract_value v ns = Some result ∧
eval_exp s1' e1' v1' ∧ eval_exp s1' e1' v1' ∧
v_rel v v1' v_rel v v1'
@ -1165,12 +1184,13 @@ Theorem translate_extract_correct:
eval_exp s1' (foldl (λe c. Select e (translate_const gmap c)) e1' cs) v2' ∧ eval_exp s1' (foldl (λe c. Select e (translate_const gmap c)) e1' cs) v2' ∧
v_rel result v2' v_rel result v2'
Proof Proof
Induct_on `cs` >> rw [] >> fs [extract_value_def] Induct_on `cs` >> rw [] >> rfs [] >> fs [extract_value_def]
>- metis_tac [] >> >- metis_tac [] >>
first_x_assum irule >> first_x_assum irule >>
Cases_on `ns` >> fs [] >> Cases_on `ns` >> fs [] >>
qmatch_goalsub_rename_tac `translate_const gmap c` >> qmatch_goalsub_rename_tac `translate_const gmap c` >>
`∃v2'. eval_exp s1' (translate_const gmap c) v2' ∧ v_rel (eval_const s1.globals c) v2'` qmatch_assum_rename_tac `eval_const _ _ v3` >>
`∃v2'. eval_exp s1' (translate_const gmap c) v2' ∧ v_rel v3 v2'`
by metis_tac [translate_constant_correct] >> by metis_tac [translate_constant_correct] >>
Cases_on `v` >> fs [extract_value_def] >> Cases_on `v` >> fs [extract_value_def] >>
qpat_x_assum `v_rel (AggV _) _` mp_tac >> qpat_x_assum `v_rel (AggV _) _` mp_tac >>
@ -1178,7 +1198,7 @@ Proof
simp [Once eval_exp_cases, PULL_EXISTS] >> simp [Once eval_exp_cases, PULL_EXISTS] >>
fs [LIST_REL_EL_EQN] >> fs [LIST_REL_EL_EQN] >>
qmatch_assum_rename_tac `_ = map Some is` >> qmatch_assum_rename_tac `_ = map Some is` >>
Cases_on `eval_const s1.globals c` >> fs [signed_v_to_num_def, signed_v_to_int_def] >> rw [] >> Cases_on `v3` >> fs [signed_v_to_num_def, signed_v_to_int_def] >> rw [] >>
`∃i. v2' = FlatV i` by fs [v_rel_cases] >> fs [] >> `∃i. v2' = FlatV i` by fs [v_rel_cases] >> fs [] >>
qmatch_assum_rename_tac `option_join _ = Some x` >> qmatch_assum_rename_tac `option_join _ = Some x` >>
`∃size. i = IntV (&x) size` suffices_by metis_tac [] >> rw [] >> `∃size. i = IntV (&x) size` suffices_by metis_tac [] >> rw [] >>
@ -1188,9 +1208,10 @@ Proof
QED QED
Theorem translate_update_correct: Theorem translate_update_correct:
∀prog gmap emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result. ∀prog gmap emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs vs ns result.
mem_state_rel prog gmap emap s1 s1' ∧ mem_state_rel prog gmap emap s1 s1' ∧
map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧ list_rel (eval_const s1.globals) cs vs ∧
map signed_v_to_num vs = map Some ns ∧
insert_value v1 v2 ns = Some result ∧ insert_value v1 v2 ns = Some result ∧
eval_exp s1' e1' v1' ∧ eval_exp s1' e1' v1' ∧
v_rel v1 v1' ∧ v_rel v1 v1' ∧
@ -1201,7 +1222,7 @@ Theorem translate_update_correct:
eval_exp s1' (translate_updatevalue gmap e1' e2' cs) v3' ∧ eval_exp s1' (translate_updatevalue gmap e1' e2' cs) v3' ∧
v_rel result v3' v_rel result v3'
Proof Proof
Induct_on `cs` >> rw [] >> fs [insert_value_def, translate_updatevalue_def] Induct_on `cs` >> rw [] >> rfs [] >> fs [insert_value_def, translate_updatevalue_def]
>- metis_tac [] >> >- metis_tac [] >>
simp [Once eval_exp_cases, PULL_EXISTS] >> simp [Once eval_exp_cases, PULL_EXISTS] >>
Cases_on `ns` >> fs [] >> Cases_on `ns` >> fs [] >>
@ -1212,7 +1233,8 @@ Proof
simp [v_rel_cases] >> simp [v_rel_cases] >>
qmatch_goalsub_rename_tac `translate_const gmap c` >> qmatch_goalsub_rename_tac `translate_const gmap c` >>
qexists_tac `vs2` >> simp [] >> qexists_tac `vs2` >> simp [] >>
`∃v4'. eval_exp s1' (translate_const gmap c) v4' ∧ v_rel (eval_const s1.globals c) v4'` qmatch_assum_rename_tac `eval_const _ _ v3` >>
`∃v4'. eval_exp s1' (translate_const gmap c) v4' ∧ v_rel v3 v4'`
by metis_tac [translate_constant_correct] >> by metis_tac [translate_constant_correct] >>
`∃idx_size. v4' = FlatV (IntV (&x) idx_size)` `∃idx_size. v4' = FlatV (IntV (&x) idx_size)`
by ( by (
@ -1222,6 +1244,7 @@ Proof
first_x_assum drule >> first_x_assum drule >>
disch_then drule >> disch_then drule >>
disch_then drule >> disch_then drule >>
disch_then drule >>
disch_then (qspecl_then [`el x vs2`, `v2'`, `e2'`, `Select e1' (translate_const gmap c)`] mp_tac) >> disch_then (qspecl_then [`el x vs2`, `v2'`, `e2'`, `Select e1' (translate_const gmap c)`] mp_tac) >>
simp [Once eval_exp_cases] >> simp [Once eval_exp_cases] >>
metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN] metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
@ -1344,8 +1367,7 @@ Theorem const_idx_uses[simp]:
∀cs gmap e. ∀cs gmap e.
exp_uses (foldl (λe c. Select e (translate_const gmap c)) e cs) = exp_uses e exp_uses (foldl (λe c. Select e (translate_const gmap c)) e cs) = exp_uses e
Proof Proof
Induct_on `cs` >> rw [exp_uses_def] >> Induct_on `cs` >> rw [exp_uses_def] >> rw [EXTENSION]
rw [translate_const_no_reg, EXTENSION]
QED QED
Theorem exp_uses_trans_upd_val[simp]: Theorem exp_uses_trans_upd_val[simp]:
@ -1353,7 +1375,7 @@ Theorem exp_uses_trans_upd_val[simp]:
(if cs = [] then {} else exp_uses e1) ∪ exp_uses e2 (if cs = [] then {} else exp_uses e1) ∪ exp_uses e2
Proof Proof
Induct_on `cs` >> rw [exp_uses_def, translate_updatevalue_def] >> Induct_on `cs` >> rw [exp_uses_def, translate_updatevalue_def] >>
rw [translate_const_no_reg, EXTENSION] >> rw [EXTENSION] >>
metis_tac [] metis_tac []
QED QED
@ -1372,7 +1394,7 @@ Theorem translate_instr_to_exp_correct:
mem_state_rel prog gmap emap' s2 s2' ∧ mem_state_rel prog gmap emap' s2 s2' ∧
(r ∉ regs_to_keep ⇒ s1' = s2' ∧ emap' = emap |+ (r, translate_instr_to_exp gmap emap instr)) ∧ (r ∉ regs_to_keep ⇒ s1' = s2' ∧ emap' = emap |+ (r, translate_instr_to_exp gmap emap instr)) ∧
(r ∈ regs_to_keep ⇒ (r ∈ regs_to_keep ⇒
emap' = emap |+ (r,Var (translate_reg r t)) ∧ emap' = emap |+ (r,Var (translate_reg r t) F) ∧
step_inst s1' (Move [(translate_reg r t, translate_instr_to_exp gmap emap instr)]) Tau s2') step_inst s1' (Move [(translate_reg r t, translate_instr_to_exp gmap emap instr)]) Tau s2')
Proof Proof
recInduct translate_instr_to_exp_ind >> recInduct translate_instr_to_exp_ind >>
@ -1476,9 +1498,9 @@ Proof
instr_uses_def]) >> instr_uses_def]) >>
drule translate_update_correct >> rpt (disch_then drule) >> drule translate_update_correct >> rpt (disch_then drule) >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >> first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >> disch_then drule >> disch_then drule >>
first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >> first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
disch_then drule >> disch_then drule >> disch_then drule >>
simp [] >> strip_tac >> strip_tac >> simp [] >> strip_tac >> strip_tac >>
disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >> disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >>
disch_then drule >> disch_then drule >> disch_then drule >> disch_then drule >>
@ -1658,15 +1680,25 @@ Proof
fs [is_allocated_def, heap_component_equality, erase_tags_def] >> fs [is_allocated_def, heap_component_equality, erase_tags_def] >>
metis_tac []) metis_tac [])
>- ( >- (
(* TODO: mem_state_rel needs to relate the globals *)
fs [get_obs_cases, llvmTheory.get_obs_cases] >> rw [translate_trace_def] >> fs [get_obs_cases, llvmTheory.get_obs_cases] >> rw [translate_trace_def] >>
fs [mem_state_rel_def, fmap_rel_OPTREL_FLOOKUP] fs [mem_state_rel_def, globals_rel_def]
>- ( >- (
first_x_assum (qspec_then `x` mp_tac) >> rw [] >> fs [FLOOKUP_DEF] >>
rename1 `option_rel _ _ opt` >> Cases_on `opt` >> first_x_assum drule >> rw []
fs [OPTREL_def] >> >- metis_tac [BIJ_DEF, SURJ_DEF] >>
cheat) >> pop_assum (mp_tac o GSYM) >> rw [w2n_i2n])
cheat)) >- (
CCONTR_TAC >> fs [FRANGE_DEF] >>
fs [BIJ_DEF, SURJ_DEF, INJ_DEF] >>
first_x_assum drule >> rw [] >>
CCONTR_TAC >> fs [] >> rw [] >>
first_x_assum drule >> rw [] >>
CCONTR_TAC >> fs [] >> rw [] >>
`i2n (IntV (w2i w) (dimindex (:64))) = w2n w` by metis_tac [w2n_i2n, dimindex_64] >>
fs [] >> rw [] >>
fs [METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
first_x_assum drule >> rw [] >>
metis_tac [pair_CASES, SND])))
QED QED
Theorem classify_instr_term_call: Theorem classify_instr_term_call:
@ -1949,7 +1981,7 @@ QED
Theorem do_phi_vals: Theorem do_phi_vals:
∀prog gmap emap from_l s s' phis updates. ∀prog gmap emap from_l s s' phis updates.
mem_state_rel prog gmap emap s s' ∧ mem_state_rel prog gmap emap s s' ∧
map (do_phi from_l s) phis = map Some updates ∧ list_rel (do_phi from_l s) phis updates ∧
BIGUNION (set (map (phi_uses from_l) phis)) ⊆ live prog s.ip BIGUNION (set (map (phi_uses from_l) phis)) ⊆ live prog s.ip
⇒ ⇒
∃es vs. ∃es vs.
@ -1963,9 +1995,9 @@ Theorem do_phi_vals:
phis phis
= map2 (\p. λe. case p of Phi r t largs => (translate_reg r t, e)) phis es = map2 (\p. λe. case p of Phi r t largs => (translate_reg r t, e)) phis es
Proof Proof
Induct_on `phis` >> rw [] >> Cases_on `updates` >> fs [] >> Induct_on `phis` >> rw [] >> fs [] >>
first_x_assum drule >> disch_then drule >> rw [] >> first_x_assum drule >> disch_then drule >> rw [PULL_EXISTS] >>
Cases_on `h` >> fs [do_phi_def, OPTION_JOIN_EQ_SOME] >> Cases_on `h` >> fs [do_phi_cases] >>
drule translate_arg_correct >> drule translate_arg_correct >>
disch_then drule >> disch_then drule >>
impl_tac impl_tac
@ -2009,7 +2041,7 @@ Theorem build_phi_block_correct:
∀prog s1 s1' to_l from_l phis updates f gmap emap entry bloc. ∀prog s1 s1' to_l from_l phis updates f gmap emap entry bloc.
prog_ok prog ∧ is_ssa prog ∧ prog_ok prog ∧ is_ssa prog ∧
get_instr prog s1.ip (Inr (from_l,phis)) ∧ get_instr prog s1.ip (Inr (from_l,phis)) ∧
map (do_phi from_l s1) phis = map Some updates ∧ list_rel (do_phi from_l s1) phis updates ∧
mem_state_rel prog gmap emap s1 s1' ∧ mem_state_rel prog gmap emap s1 s1' ∧
BIGUNION (set (map (phi_uses from_l) phis)) ⊆ live prog s1.ip ∧ BIGUNION (set (map (phi_uses from_l) phis)) ⊆ live prog s1.ip ∧
bloc = generate_move_block f gmap emap phis from_l to_l bloc = generate_move_block f gmap emap phis from_l to_l
@ -2069,7 +2101,7 @@ Proof
by ( by (
qpat_x_assum `map fst _ = map phi_assigns _` mp_tac >> qpat_x_assum `map fst _ = map phi_assigns _` mp_tac >>
simp [LIST_EQ_REWRITE, EL_MAP] >> simp [LIST_EQ_REWRITE, EL_MAP] >>
`length phis = length updates` by metis_tac [LENGTH_MAP] >> `length phis = length updates` by metis_tac [LIST_REL_LENGTH] >>
rw [EL_ZIP, LENGTH_MAP, EL_MAP] >> rw [EL_ZIP, LENGTH_MAP, EL_MAP] >>
rename1 `_ = el n updates` >> rename1 `_ = el n updates` >>
first_x_assum drule >> first_x_assum drule >>
@ -2138,6 +2170,7 @@ Theorem multi_step_to_step_block:
filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace (get_gmap prog)) tr) ∧ filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace (get_gmap prog)) tr) ∧
state_rel prog (get_gmap prog) emap2 s2 s2' state_rel prog (get_gmap prog) emap2 s2 s2'
Proof Proof
rw [] >> pop_assum mp_tac >> simp [Once state_rel_def] >> rw [Once pc_rel_cases] rw [] >> pop_assum mp_tac >> simp [Once state_rel_def] >> rw [Once pc_rel_cases]
>- ( >- (
(* Non-phi instruction *) (* Non-phi instruction *)
@ -2153,6 +2186,7 @@ Proof
qpat_x_assum `last_step _ _ _ _` mp_tac >> qpat_x_assum `last_step _ _ _ _` mp_tac >>
simp [last_step_cases] >> strip_tac simp [last_step_cases] >> strip_tac
>- ( >- (
fs [llvmTheory.step_cases] fs [llvmTheory.step_cases]
>- metis_tac [get_instr_func, sum_distinct] >> >- metis_tac [get_instr_func, sum_distinct] >>
fs [translate_trace_def] >> rw [] >> fs [translate_trace_def] >> rw [] >>
@ -2170,6 +2204,12 @@ Proof
fs [get_instr_cases] >> fs [get_instr_cases] >>
rfs [] >> rw [] >> fs []) >> rfs [] >> rw [] >> fs []) >>
first_x_assum drule >> rw [] >> first_x_assum drule >> rw [] >>
rename1 `generate_move_block _ _ emap1` >>
`mem_state_rel prog (get_gmap prog) emap1 s1 s1'`
by (
fs [mem_state_rel_def, local_state_rel_def] >>
cheat) >>
qmatch_assum_abbrev_tac `get_block _ _ bloc` >> qmatch_assum_abbrev_tac `get_block _ _ bloc` >>
GEN_EXISTS_TAC "b" `bloc` >> GEN_EXISTS_TAC "b" `bloc` >>
rw [] >> rw [] >>
@ -2182,13 +2222,8 @@ Proof
drule get_instr_live >> rw [SUBSET_DEF, uses_cases, IN_DEF] >> drule get_instr_live >> rw [SUBSET_DEF, uses_cases, IN_DEF] >>
first_x_assum irule >> disj2_tac >> metis_tac []) >> first_x_assum irule >> disj2_tac >> metis_tac []) >>
rw [] >> rw [] >>
qexists_tac `s2'` >> qexists_tac `emap |++ header_to_emap_upd (Head phis None)` >> qexists_tac `s2'` >> qexists_tac `emap1 |++ header_to_emap_upd (Head phis None)` >>
qexists_tac `[Tau; Tau]` >> rw [] qexists_tac `[Tau; Tau]` >> rw [] >>
>- (
(* TODO: This isn't true and will require a more subtle treatment of the
* emap in this proof overall *)
`emap = emap'` by cheat >>
metis_tac []) >>
fs [state_rel_def] >> rw [] >> fs [state_rel_def] >> rw [] >>
fs [llvmTheory.inc_pc_def] >> fs [llvmTheory.inc_pc_def] >>
fs [pc_rel_cases, get_instr_cases, PULL_EXISTS, translate_label_def, fs [pc_rel_cases, get_instr_cases, PULL_EXISTS, translate_label_def,
@ -2206,16 +2241,17 @@ Proof
by ( by (
fs [prog_ok_def] >> res_tac >> fs [] >> fs [prog_ok_def] >> res_tac >> fs [] >>
fs [EVERY_MEM]) >> fs [EVERY_MEM]) >>
drule alookup_translate_blocks >> rpt (disch_then drule) >> drule alookup_translate_blocks >> rpt (disch_then drule) >>
simp [translate_label_def] >> simp [translate_label_def] >>
disch_then (qspecl_then [`s`, `get_gmap prog`, `fempty`, `get_regs_to_keep d`, disch_then (qspecl_then [`s`, `get_gmap prog`, `fempty`, `get_regs_to_keep d`,
`map (λ(l,b). (l,get_from_ls l d.blocks)) d.blocks`] `map (λ(l,b). (l,get_from_ls l d.blocks)) d.blocks`]
mp_tac) >> mp_tac) >>
rw [] >> rw [dest_label_def, num_calls_def] >> rw [] >> rw [dest_label_def, num_calls_def] >>
rename1 `alookup _ _ = Some (snd (HD (fst (translate_instrs _ _ emap1 _ _))))` >> rename1 `alookup _ _ = Some (snd (HD (fst (translate_instrs _ _ emap2 _ _))))` >>
(* TODO: This isn't true and will require a more subtle treatment of the (* TODO: This isn't true and will require a more subtle treatment of the
* emap in this proof overall *) * emap in this proof overall *)
`emap1 = emap |++ header_to_emap_upd (Head phis None)` by cheat >> `emap2 = emap1 |++ header_to_emap_upd (Head phis None)` by cheat >>
rw [translate_instrs_take_to_call] >> rw [translate_instrs_take_to_call] >>
qexists_tac `get_regs_to_keep d` >> rw [] >> qexists_tac `get_regs_to_keep d` >> rw [] >>
qmatch_goalsub_abbrev_tac `_ = HD (fst (translate_instrs a1 b1 c1 d1 e1))` >> qmatch_goalsub_abbrev_tac `_ = HD (fst (translate_instrs a1 b1 c1 d1 e1))` >>

5
sledge/semantics/memory_modelScript.sml
Unescape View File

@ -361,7 +361,7 @@ Proof
`take size (le_write_num size n ⧺ bs) = le_write_num size n` `take size (le_write_num size n ⧺ bs) = le_write_num size n`
by metis_tac [le_write_num_length, TAKE_LENGTH_APPEND] >> by metis_tac [le_write_num_length, TAKE_LENGTH_APPEND] >>
simp [le_write_num_def, w2l_def, l2w_def] >> simp [le_write_num_def, w2l_def, l2w_def] >>
fs [l2n_padding, TAKE_APPEND, take_replicate] >> fs [SIMP_RULE (srw_ss()) [map_replicate] l2n_padding, TAKE_APPEND, take_replicate] >>
simp [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, mod_n2l] >> simp [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, mod_n2l] >>
rename1 `n2l 256 m` >> rename1 `n2l 256 m` >>
Cases_on `size = 0` >> fs [] >> Cases_on `size = 0` >> fs [] >>
@ -383,7 +383,8 @@ Proof
fs [EXP_EXP_MULT] >> fs [EXP_EXP_MULT] >>
`2 ** log 2 m ≤ m` by rw [exp_log_bound] >> `2 ** log 2 m ≤ m` by rw [exp_log_bound] >>
decide_tac) >> decide_tac) >>
simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG]) simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG]
)
>- metis_tac [le_write_num_length, DROP_LENGTH_APPEND] >- metis_tac [le_write_num_length, DROP_LENGTH_APPEND]
QED QED

2
sledge/semantics/miscScript.sml
Unescape View File

@ -361,7 +361,7 @@ QED
Theorem l2n_padding: Theorem l2n_padding:
∀ws n. l2n 256 (ws ++ map w2n (replicate n 0w)) = l2n 256 ws ∀ws n. l2n 256 (ws ++ map w2n (replicate n 0w)) = l2n 256 ws
Proof Proof
Induct >> rw [l2n_def] >> Induct >> rw [l2n_def] >> fs [map_replicate] >>
Induct_on `n` >> rw [l2n_def] Induct_on `n` >> rw [l2n_def]
QED QED

Write Preview
Loading…
Cancel
Save