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

[sledge sem] Refactor the way LLVM sem. does phis

Browse Source 
Summary:
Previously the LLVM semantics did the phi instructions at the head of a
block as part of executing the branch into that block. This looked a bit
weird, but had the advantage that the semantics knew which block was
being jumped from, which is necessary to run the phi instructions.
However, it meant that the rules for doing phi instructions would need
to show up with each branching construct. It was also annoying for the
LLVM->llair proof, since the phis are removed and their effect happens as
a distinct step from the branch.

Here we add a distinct Phi_ip instruction pointer to indicate that the
phi instructions at the start of the block should execute next, and then
be incremented to the usual numeric instruction pointer that points to
the non-phi instructions. The Phi_ip contains the identity of the
previous block.

Reviewed By: jberdine

Differential Revision: D17452416

fbshipit-source-id: 78fef7cca
master
Scott Owens 5 years ago committed by Facebook Github Bot
parent 17b3c7a49f
commit ab7233c5b8
5 changed files with 328 additions and 154 deletions
Show Stats Download Patch File Download Diff File

133
sledge/semantics/llvmScript.sml
Unescape View File

@ -68,6 +68,21 @@ Datatype:
cond = Eq | Ult | Slt cond = Eq | Ult | Slt
End End
Datatype:
phi = Phi reg ty ((label option, arg) alist)
End
(*
* The Exit instruction below models a system/libc call to exit the program. The
* semantics needs some way to tell the difference between normally terminated
* programs and stuck states, and this lets it do that. From a C++ perspective,
* a program could call this directly, in which case it's good to model, or it
* might simply return from main and then the code in libc that called main will
* call exit. However, adding special handling for main in the semantics will
* cruft things up a bit, and it's not very satisfying, because it's not really
* an LLVM concept.
*)
Datatype: Datatype:
instr = instr =
(* Terminators *) (* Terminators *)
@ -96,10 +111,6 @@ Datatype:
| Cxa_get_exception_ptr reg arg | Cxa_get_exception_ptr reg arg
End End
Datatype:
phi = Phi reg ty ((label option, arg) alist)
End
Datatype: Datatype:
clause = Catch targ clause = Catch targ
End End
@ -160,8 +171,17 @@ Datatype:
pv = <| poison : bool; value : v |> pv = <| poison : bool; value : v |>
End End
(* Instruction pointer into a block. Phi_ip indicates to do the phi instruction,
* coming from the given label. Offset points to a normal (non-phi) instruction.
* *)
Datatype:
bip =
| Phi_ip (label option)
| Offset num
End
Datatype: Datatype:
pc = <| f : fun_name; b : label option; i : num |> pc = <| f : fun_name; b : label option; i : bip |>
End End
Datatype: Datatype:
@ -461,8 +481,13 @@ Definition update_result_def:
update_result x v s = s with locals := s.locals |+ (x, v) update_result x v s = s with locals := s.locals |+ (x, v)
End End
Definition inc_bip_def:
(inc_bip (Phi_ip _) = Offset 0) ∧
(inc_bip (Offset i) = Offset (i + 1))
End
Definition inc_pc_def: Definition inc_pc_def:
inc_pc s = s with ip := (s.ip with i := s.ip.i + 1) inc_pc s = s with ip := (s.ip with i := inc_bip s.ip.i)
End End
Inductive get_obs: Inductive get_obs:
@ -488,27 +513,12 @@ Inductive step_instr:
stack := st; stack := st;
heap := new_h |>)) ∧ heap := new_h |>)) ∧
(* Do the phi assignments in parallel. The manual says "For the purposes of the
* SSA form, the use of each incoming value is deemed to occur on the edge from
* the corresponding predecessor block to the current block (but after any
* definition of an 'invoke' instruction's return value on the same edge)".
* So treat these two as equivalent
* %r1 = phi [0, %l]
* %r2 = phi [%r1, %l]
* and
* %r2 = phi [%r1, %l]
* %r1 = phi [0, %l]
*)
(eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧ (eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
l = Some (if tf = 1w then l1 else l2) ∧ 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 |> ∧
map (do_phi l s) phis = map Some updates
⇒ ⇒
step_instr prog s step_instr prog s
(Br a l1 l2) Tau (Br a l1 l2) Tau
(s with <| ip := <| f := s.ip.f; b := l; i := 0 |>; (s with ip := <| f := s.ip.f; b := l; i := Phi_ip s.ip.b |>)) ∧
locals := s.locals |++ updates |>)) ∧
(* TODO *) (* TODO *)
(step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧ (step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧
@ -623,11 +633,12 @@ Inductive step_instr:
⇒ ⇒
step_instr prog s step_instr prog s
(Call r t fname targs) Tau (Call r t fname targs) Tau
<| ip := <| f := fname; b := None; i := 0 |>; (* Jump to the entry block of the function which has no phis *)
<| ip := <| f := fname; b := None; i := Offset 0 |>;
locals := alist_to_fmap (zip (map snd d.params, vs)); locals := alist_to_fmap (zip (map snd d.params, vs));
globals := s.globals; globals := s.globals;
stack := stack :=
<| ret := s.ip with i := s.ip.i + 1; <| ret := s.ip with i := inc_bip s.ip.i;
saved_locals := s.locals; saved_locals := s.locals;
result_var := r; result_var := r;
stack_allocs := [] |> :: s.stack; stack_allocs := [] |> :: s.stack;
@ -647,24 +658,49 @@ Inductive step_instr:
End End
Inductive get_instr: Inductive get_instr:
(∀prog ip. (∀prog ip.
alookup prog ip.f = Some d ∧ alookup prog ip.f = Some d ∧
alookup d.blocks ip.b = Some b ∧ alookup d.blocks ip.b = Some b ∧
ip.i < length b.body ip.i = Offset idx ∧
⇒ idx < length b.body
get_instr prog ip (el ip.i b.body)) ⇒
get_instr prog ip (Inl (el idx b.body))) ∧
(∀prog ip.
alookup prog ip.f = Some d ∧
alookup d.blocks ip.b = Some b ∧
ip.i = Phi_ip from_l ∧
b.h = Head phis landing
⇒
get_instr prog ip (Inr (from_l, phis)))
End End
Inductive step: Inductive step:
get_instr p s.ip i ∧ (get_instr p s.ip (Inl i) ∧
step_instr p s i l s' step_instr p s i l s'
⇒ ⇒
step p s l s' step p s l s') ∧
(* Do the phi assignments in parallel. The manual says "For the purposes of the
* SSA form, the use of each incoming value is deemed to occur on the edge from
* the corresponding predecessor block to the current block (but after any
* definition of an 'invoke' instruction's return value on the same edge)".
* So treat these two as equivalent
* %r1 = phi [0, %l]
* %r2 = phi [%r1, %l]
* and
* %r2 = phi [%r1, %l]
* %r1 = phi [0, %l]
*)
(get_instr p s.ip (Inr (from_l, phis)) ∧
map (do_phi from_l s) phis = map Some updates
⇒
step p s Tau (inc_pc (s with locals := locals |++ updates)))
End End
Definition get_observation_def: Definition get_observation_def:
get_observation prog last_s = get_observation prog last_s =
if get_instr prog last_s.ip Exit then if get_instr prog last_s.ip (Inl Exit) then
Complete Complete
else if ∃s l. step prog last_s l s then else if ∃s l. step prog last_s l s then
Partial Partial
@ -695,20 +731,39 @@ End
(* Instruction pointer points to an instruction *) (* Instruction pointer points to an instruction *)
Definition ip_ok_def: Definition ip_ok_def:
ip_ok p ip ⇔ ip_ok p ip ⇔
∃dec block. alookup p ip.f = Some dec ∧ alookup dec.blocks ip.b = Some block ∧ ip.i < length block.body ∃dec block.
alookup p ip.f = Some dec ∧ alookup dec.blocks ip.b = Some block ∧
((∃idx. ip.i = Offset idx ∧ idx < length block.body) ∨
(∃from_l. ip.i = Phi_ip from_l ∧ block.h ≠ Entry ∧ alookup dec.blocks from_l ≠ None))
End
Definition instr_to_labs_def:
(instr_to_labs (Br _ l1 l2) = [l1; l2]) ∧
(instr_to_labs _ = [])
End End
Definition prog_ok_def: Definition prog_ok_def:
prog_ok p ⇔ prog_ok p ⇔
((* All blocks end with terminators *) ((* All blocks end with terminators and terminators only appear at the end.
* All labels mentioned in instructions actually exist *)
∀fname dec bname block. ∀fname dec bname block.
alookup p fname = Some dec ∧ alookup p fname = Some dec ∧
alookup dec.blocks bname = Some block alookup dec.blocks bname = Some block
⇒ ⇒
block.body ≠ [] ∧ terminator (last block.body)) ∧ block.body ≠ [] ∧ terminator (last block.body) ∧
every (λi. ¬terminator i) (front block.body) ∧
every (λlab. alookup dec.blocks (Some lab) ≠ None)
(instr_to_labs (last block.body)) ∧
(∀phis lands. block.h = Head phis lands ⇒
every (λx. case x of Phi _ _ l => every (λ(lab, _). alookup dec.blocks lab ≠ None) l) phis)) ∧
((* All functions have an entry block *) ((* All functions have an entry block *)
∀fname dec. ∀fname dec.
alookup p fname = Some dec ⇒ ∃block. alookup dec.blocks None = Some block) ∧ alookup p fname = Some dec ⇒
∃block. alookup dec.blocks None = Some block ∧ block.h = Entry) ∧
((* All non-entry blocks have a proper header *)
∀fname dec l b.
alookup p fname = Some dec ∧ alookup dec.blocks (Some l) = Some b ⇒
b.h ≠ Entry) ∧
(* There is a main function *) (* There is a main function *)
∃dec. alookup p (Fn "main") = Some dec ∃dec. alookup p (Fn "main") = Some dec
End End
@ -740,7 +795,7 @@ Definition is_init_state_def:
is_init_state s (global_init : glob_var |-> ty # v) ⇔ is_init_state s (global_init : glob_var |-> ty # v) ⇔
s.ip.f = Fn "main" ∧ s.ip.f = Fn "main" ∧
s.ip.b = None ∧ s.ip.b = None ∧
s.ip.i = 0 ∧ s.ip.i = Offset 0 ∧
s.locals = fempty ∧ s.locals = fempty ∧
s.stack = [] ∧ s.stack = [] ∧
globals_ok s ∧ globals_ok s ∧

213
sledge/semantics/llvm_liveScript.sml
Unescape View File

@ -16,35 +16,47 @@ new_theory "llvm_live";
numLib.prefer_num (); numLib.prefer_num ();
Definition inc_pc_def: Definition inc_pc_def:
inc_pc ip = ip with i := ip.i + 1 inc_pc ip = ip with i := inc_bip ip.i
End End
(* The set of program counters the given instruction and starting point can (* The set of program counters the given instruction and starting point can
* immediately reach, within a function *) * immediately reach, within a function *)
Definition next_ips_def: Definition instr_next_ips_def:
(next_ips (Ret _) ip = {}) ∧ (instr_next_ips (Ret _) ip = {}) ∧
(next_ips (Br _ l1 l2) ip = (instr_next_ips (Br _ l1 l2) ip =
{ <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧ { <| f := ip.f; b := Some l; i := Phi_ip ip.b |> | l | l ∈ {l1; l2} }) ∧
(next_ips (Invoke _ _ _ _ l1 l2) ip = (instr_next_ips (Invoke _ _ _ _ l1 l2) ip =
{ <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧ { <| f := ip.f; b := Some l; i := Phi_ip ip.b |> | l | l ∈ {l1; l2} }) ∧
(next_ips Unreachable ip = {}) ∧ (instr_next_ips Unreachable ip = {}) ∧
(next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Alloca _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Alloca _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Load _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Load _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Store _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Store _ _) ip = { inc_pc ip }) ∧
(next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧
(next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧
(* TODO: revisit throw when dealing with exceptions *) (* TODO: revisit throw when dealing with exceptions *)
(next_ips (Cxa_throw _ _ _) ip = { }) ∧ (instr_next_ips (Cxa_throw _ _ _) ip = { }) ∧
(next_ips (Cxa_begin_catch _ _) ip = { inc_pc ip }) ∧ (instr_next_ips (Cxa_begin_catch _ _) ip = { inc_pc ip }) ∧
(next_ips (Cxa_end_catch) ip = { inc_pc ip }) ∧ (instr_next_ips (Cxa_end_catch) ip = { inc_pc ip }) ∧
(next_ips (Cxa_get_exception_ptr _ _) ip = { inc_pc ip }) (instr_next_ips (Cxa_get_exception_ptr _ _) ip = { inc_pc ip })
End
Inductive next_ips:
(∀prog ip i l.
get_instr prog ip (Inl i) ∧
l ∈ instr_next_ips i ip
⇒
next_ips prog ip l) ∧
(∀prog ip from_l phis.
get_instr prog ip (Inr (from_l, phis))
⇒
next_ips prog ip (inc_pc ip))
End End
(* The path is a list of program counters that represent a statically feasible (* The path is a list of program counters that represent a statically feasible
@ -52,14 +64,13 @@ End
Inductive good_path: Inductive good_path:
(∀prog. good_path prog []) ∧ (∀prog. good_path prog []) ∧
(∀ip i. (∀prog ip i.
get_instr prog ip i get_instr prog ip i
⇒ ⇒
good_path prog [ip]) ∧ good_path prog [ip]) ∧
(∀prog path ip1 i1 ip2. (∀prog path ip1 ip2.
get_instr prog ip1 i1 ∧ ip2 ∈ next_ips prog ip1 ∧
ip2 ∈ next_ips i1 ip1 ∧
good_path prog (ip2::path) good_path prog (ip2::path)
⇒ ⇒
good_path prog (ip1::ip2::path)) good_path prog (ip1::ip2::path))
@ -71,65 +82,102 @@ Definition arg_to_regs_def:
End End
(* The registers that an instruction uses *) (* The registers that an instruction uses *)
Definition uses_def: Definition instr_uses_def:
(uses (Ret (_, a)) = arg_to_regs a) ∧ (instr_uses (Ret (_, a)) = arg_to_regs a) ∧
(uses (Br a _ _) = arg_to_regs a) ∧ (instr_uses (Br a _ _) = arg_to_regs a) ∧
(uses (Invoke _ _ a targs _ _) = (instr_uses (Invoke _ _ a targs _ _) =
arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧ arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
(uses Unreachable = {}) ∧ (instr_uses Unreachable = {}) ∧
(uses (Sub _ _ _ _ a1 a2) = (instr_uses (Sub _ _ _ _ a1 a2) =
arg_to_regs a1 ∪ arg_to_regs a2) ∧ arg_to_regs a1 ∪ arg_to_regs a2) ∧
(uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧ (instr_uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧
(uses (Insertvalue _ (_, a1) (_, a2) _) = (instr_uses (Insertvalue _ (_, a1) (_, a2) _) =
arg_to_regs a1 ∪ arg_to_regs a2) ∧ arg_to_regs a1 ∪ arg_to_regs a2) ∧
(uses (Alloca _ _ (_, a)) = arg_to_regs a) ∧ (instr_uses (Alloca _ _ (_, a)) = arg_to_regs a) ∧
(uses (Load _ _ (_, a)) = arg_to_regs a) ∧ (instr_uses (Load _ _ (_, a)) = arg_to_regs a) ∧
(uses (Store (_, a1) (_, a2)) = (instr_uses (Store (_, a1) (_, a2)) =
arg_to_regs a1 ∪ arg_to_regs a2) ∧ arg_to_regs a1 ∪ arg_to_regs a2) ∧
(uses (Gep _ _ (_, a) targs) = (instr_uses (Gep _ _ (_, a) targs) =
arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧ arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
(uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧ (instr_uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧
(uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧ (instr_uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧
(uses (Icmp _ _ _ a1 a2) = (instr_uses (Icmp _ _ _ a1 a2) =
arg_to_regs a1 ∪ arg_to_regs a2) ∧ arg_to_regs a1 ∪ arg_to_regs a2) ∧
(uses (Call _ _ _ targs) = (instr_uses (Call _ _ _ targs) =
BIGUNION (set (map (arg_to_regs o snd) targs))) ∧ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
(uses (Cxa_allocate_exn _ a) = arg_to_regs a) ∧ (instr_uses (Cxa_allocate_exn _ a) = arg_to_regs a) ∧
(uses (Cxa_throw a1 a2 a3) = (instr_uses (Cxa_throw a1 a2 a3) =
arg_to_regs a1 ∪ arg_to_regs a2 ∪ arg_to_regs a3) ∧ arg_to_regs a1 ∪ arg_to_regs a2 ∪ arg_to_regs a3) ∧
(uses (Cxa_begin_catch _ a) = arg_to_regs a) ∧ (instr_uses (Cxa_begin_catch _ a) = arg_to_regs a) ∧
(uses (Cxa_end_catch) = { }) ∧ (instr_uses (Cxa_end_catch) = { }) ∧
(uses (Cxa_get_exception_ptr _ a) = arg_to_regs a) (instr_uses (Cxa_get_exception_ptr _ a) = arg_to_regs a)
End
Definition phi_uses_def:
phi_uses from_l (Phi _ _ entries) =
case alookup entries from_l of
| None => {}
| Some a => arg_to_regs a
End
Inductive uses:
(∀prog ip i r.
get_instr prog ip (Inl i) ∧
r ∈ instr_uses i
⇒
uses prog ip r) ∧
(∀prog ip from_l phis r.
get_instr prog ip (Inr (from_l, phis)) ∧
r ∈ BIGUNION (set (map (phi_uses from_l) phis))
⇒
uses prog ip r)
End End
(* The registers that an instruction assigns *) (* The registers that an instruction assigns *)
Definition assigns_def: Definition instr_assigns_def:
(assigns (Invoke r _ _ _ _ _) = {r}) ∧ (instr_assigns (Invoke r _ _ _ _ _) = {r}) ∧
(assigns (Sub r _ _ _ _ _) = {r}) ∧ (instr_assigns (Sub r _ _ _ _ _) = {r}) ∧
(assigns (Extractvalue r _ _) = {r}) ∧ (instr_assigns (Extractvalue r _ _) = {r}) ∧
(assigns (Insertvalue r _ _ _) = {r}) ∧ (instr_assigns (Insertvalue r _ _ _) = {r}) ∧
(assigns (Alloca r _ _) = {r}) ∧ (instr_assigns (Alloca r _ _) = {r}) ∧
(assigns (Load r _ _) = {r}) ∧ (instr_assigns (Load r _ _) = {r}) ∧
(assigns (Gep r _ _ _) = {r}) ∧ (instr_assigns (Gep r _ _ _) = {r}) ∧
(assigns (Ptrtoint r _ _) = {r}) ∧ (instr_assigns (Ptrtoint r _ _) = {r}) ∧
(assigns (Inttoptr r _ _) = {r}) ∧ (instr_assigns (Inttoptr r _ _) = {r}) ∧
(assigns (Icmp r _ _ _ _) = {r}) ∧ (instr_assigns (Icmp r _ _ _ _) = {r}) ∧
(assigns (Call r _ _ _) = {r}) ∧ (instr_assigns (Call r _ _ _) = {r}) ∧
(assigns (Cxa_allocate_exn r _) = {r}) ∧ (instr_assigns (Cxa_allocate_exn r _) = {r}) ∧
(assigns (Cxa_begin_catch r _) = {r}) ∧ (instr_assigns (Cxa_begin_catch r _) = {r}) ∧
(assigns (Cxa_get_exception_ptr r _) = {r}) ∧ (instr_assigns (Cxa_get_exception_ptr r _) = {r}) ∧
(assigns _ = {}) (instr_assigns _ = {})
End
Definition phi_assigns_def:
phi_assigns (Phi r _ _) = {r}
End
Inductive assigns:
(∀prog ip i r.
get_instr prog ip (Inl i) ∧
r ∈ instr_assigns i
⇒
assigns prog ip r) ∧
(∀prog ip from_l phis r.
get_instr prog ip (Inr (from_l, phis)) ∧
r ∈ BIGUNION (set (map phi_assigns phis))
⇒
assigns prog ip r)
End End
Definition live_def: Definition live_def:
live prog ip ⇔ live prog ip =
{ r | ∃path instr. { r | ∃path.
good_path prog (ip::path) ∧ good_path prog (ip::path) ∧
get_instr prog (last (ip::path)) instr ∧ r ∈ uses prog (last (ip::path)) ∧
r ∈ uses instr ∧ ∀ip2. ip2 ∈ set (front (ip::path)) ⇒ r ∉ assigns prog ip2 }
∀ip2 instr2. ip2 ∈ set (front (ip::path)) ∧ get_instr prog ip2 instr2 ⇒ r ∉ assigns instr2 }
End End
(*
Theorem get_instr_live: Theorem get_instr_live:
∀prog ip instr. ∀prog ip instr.
get_instr prog ip instr get_instr prog ip instr
@ -140,6 +188,7 @@ Proof
qexists_tac `[]` >> rw [Once good_path_cases] >> qexists_tac `[]` >> rw [Once good_path_cases] >>
qexists_tac `instr` >> simp [] >> metis_tac [IN_DEF] qexists_tac `instr` >> simp [] >> metis_tac [IN_DEF]
QED QED
*)
Triviality set_rw: Triviality set_rw:
!s P. (!x. x ∈ s ⇔ P x) ⇔ s = P !s P. (!x. x ∈ s ⇔ P x) ⇔ s = P
@ -148,28 +197,24 @@ Proof
QED QED
Theorem live_gen_kill: Theorem live_gen_kill:
∀prog ip instr ip'. ∀prog ip ip'.
get_instr prog ip instr live prog ip =
⇒ BIGUNION {live prog ip' | ip' | ip' ∈ next_ips prog ip} DIFF assigns prog ip ∪ uses prog ip
live prog ip = BIGUNION {live prog ip' | ip' ∈ next_ips instr ip} DIFF assigns instr ∪ uses instr
Proof Proof
rw [live_def, EXTENSION] >> eq_tac >> rw [] rw [live_def, EXTENSION] >> eq_tac >> rw []
>- ( >- (
Cases_on `path` >> fs [] Cases_on `path` >> fs [] >>
>- metis_tac [get_instr_func] >>
rename1 `ip::ip2::path` >> rename1 `ip::ip2::path` >>
qpat_x_assum `good_path _ _` mp_tac >> simp [Once good_path_cases] >> rw [] >> qpat_x_assum `good_path _ _` mp_tac >> simp [Once good_path_cases] >> rw [] >>
Cases_on `x ∈ uses instr` >> fs [] >> simp [set_rw, PULL_EXISTS] >> Cases_on `x ∈ uses prog ip` >> fs [] >> simp [set_rw, PULL_EXISTS] >>
qexists_tac `ip2` >> qexists_tac `path` >> qexists_tac `instr'` >> rw [] >> qexists_tac `ip2` >> qexists_tac `path` >> rw [])
metis_tac [get_instr_func])
>- ( >- (
fs [] >> fs [] >>
qexists_tac `ip'::path` >> qexists_tac `instr'` >> rw [] qexists_tac `ip'::path` >> rw [] >>
>- (simp [Once good_path_cases] >> metis_tac []) >> simp [Once good_path_cases])
metis_tac [get_instr_func])
>- ( >- (
qexists_tac `[]` >> qexists_tac `instr` >> rw [] >> qexists_tac `[]` >> rw [] >>
simp [Once good_path_cases] >> fs [Once good_path_cases, uses_cases, IN_DEF] >>
metis_tac []) metis_tac [])
QED QED

120
sledge/semantics/llvm_propScript.sml
Unescape View File

@ -293,19 +293,20 @@ QED
Theorem get_instr_func: Theorem get_instr_func:
∀p ip i1 i2. get_instr p ip i1 ∧ get_instr p ip i2 ⇒ i1 = i2 ∀p ip i1 i2. get_instr p ip i1 ∧ get_instr p ip i2 ⇒ i1 = i2
Proof Proof
rw [get_instr_cases] >> rw [get_instr_cases] >> fs [] >> rw [] >> fs [] >> rw [] >> fs []
metis_tac [optionTheory.SOME_11]
QED QED
Theorem inc_pc_invariant: Theorem inc_pc_invariant:
∀p s i. prog_ok p ∧ get_instr p s.ip i ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s) ∀p s i. prog_ok p ∧ get_instr p s.ip (Inl i) ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s)
Proof Proof
rw [state_invariant_def, inc_pc_def, allocations_ok_def, globals_ok_def, rw [state_invariant_def, inc_pc_def, allocations_ok_def, globals_ok_def,
stack_ok_def, frame_ok_def, heap_ok_def, EVERY_EL, ip_ok_def] stack_ok_def, frame_ok_def, heap_ok_def, EVERY_EL, ip_ok_def, inc_bip_def,
METIS_PROVE [] ``x ∨ y ⇔ ~x ⇒ y``]
>- ( >- (
qexists_tac `dec` >> qexists_tac `block'` >> rw [] >> qexists_tac `dec` >> qexists_tac `block'` >> rw [] >>
fs [prog_ok_def, get_instr_cases] >> res_tac >> rw [] >> fs [prog_ok_def, get_instr_cases] >> res_tac >> rw [] >>
`s.ip.i ≠ length block'.body - 1` suffices_by decide_tac >> Cases_on `s.ip.i` >> fs [] >> rw [] >> fs [inc_bip_def] >>
`idx ≠ length block'.body - 1` suffices_by decide_tac >>
CCONTR_TAC >> fs [] >> rfs [LAST_EL, PRE_SUB1]) >> CCONTR_TAC >> fs [] >> rfs [LAST_EL, PRE_SUB1]) >>
metis_tac [] metis_tac []
QED QED
@ -327,7 +328,8 @@ Theorem allocate_invariant:
∀p s1 v1 t v2 h2. ∀p s1 v1 t v2 h2.
state_invariant p s1 ∧ allocate s1.heap v1 t (v2,h2) ⇒ state_invariant p (s1 with heap := h2) state_invariant p s1 ∧ allocate s1.heap v1 t (v2,h2) ⇒ state_invariant p (s1 with heap := h2)
Proof Proof
rw [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def] rw [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def,
METIS_PROVE [] ``x ∨ y ⇔ ~x ⇒ y``]
>- metis_tac [allocate_heap_ok] >- metis_tac [allocate_heap_ok]
>- (fs [is_allocated_def] >> metis_tac [allocate_unchanged, SUBSET_DEF]) >- (fs [is_allocated_def] >> metis_tac [allocate_unchanged, SUBSET_DEF])
>- ( >- (
@ -347,9 +349,15 @@ Proof
>- (fs [stack_ok_def, EVERY_EL, frame_ok_def, set_bytes_unchanged]) >- (fs [stack_ok_def, EVERY_EL, frame_ok_def, set_bytes_unchanged])
QED QED
Triviality not_none_eq:
!x. x ≠ None ⇔ ?y. x = Some y
Proof
Cases >> rw []
QED
Theorem step_instr_invariant: Theorem step_instr_invariant:
∀i l s2. ∀i l s2.
step_instr p s1 i l s2 ⇒ prog_ok p ∧ get_instr p s1.ip i ∧ state_invariant p s1 step_instr p s1 i l s2 ⇒ prog_ok p ∧ get_instr p s1.ip (Inl i) ∧ state_invariant p s1
⇒ ⇒
state_invariant p s2 state_invariant p s2
Proof Proof
@ -384,17 +392,39 @@ Proof
>- ( (* Br *) >- ( (* Br *)
fs [state_invariant_def] >> rw [] fs [state_invariant_def] >> rw []
>- ( >- (
rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >> rw [ip_ok_def] >> fs [prog_ok_def] >>
qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >> qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
last_x_assum drule >> disch_then drule >> fs []) fs [get_instr_cases] >>
last_x_assum drule >> disch_then drule >> fs [] >> rw [] >>
`terminator (el idx b.body)` by metis_tac [terminator_def] >>
`last b.body = el idx b.body`
by (
Cases_on `idx = PRE (length b.body)` >> fs [EL_PRE_LENGTH] >>
`Suc idx < length b.body` by decide_tac >>
drule mem_el_front >> rw [] >> fs [EVERY_MEM] >>
metis_tac []) >>
qpat_x_assum `Br _ _ _ = _` (assume_tac o GSYM) >> fs [] >>
fs [instr_to_labs_def, not_none_eq] >>
metis_tac [])
>- (fs [globals_ok_def] >> metis_tac []) >- (fs [globals_ok_def] >> metis_tac [])
>- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac [])) >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
>- ( (* Br *) >- ( (* Br *)
fs [state_invariant_def] >> rw [] fs [state_invariant_def] >> rw []
>- ( >- (
rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >> rw [ip_ok_def] >> fs [prog_ok_def] >>
qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >> qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
last_x_assum drule >> disch_then drule >> fs []) fs [get_instr_cases] >>
last_x_assum drule >> disch_then drule >> fs [] >> rw [] >>
`terminator (el idx b.body)` by metis_tac [terminator_def] >>
`last b.body = el idx b.body`
by (
Cases_on `idx = PRE (length b.body)` >> fs [EL_PRE_LENGTH] >>
`Suc idx < length b.body` by decide_tac >>
drule mem_el_front >> rw [] >> fs [EVERY_MEM] >>
metis_tac []) >>
qpat_x_assum `Br _ _ _ = _` (assume_tac o GSYM) >> fs [] >>
fs [instr_to_labs_def, not_none_eq] >>
metis_tac [])
>- (fs [globals_ok_def] >> metis_tac []) >- (fs [globals_ok_def] >> metis_tac [])
>- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac [])) >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
>- ( >- (
@ -438,21 +468,40 @@ Proof
>- ( >- (
fs [state_invariant_def, stack_ok_def] >> rw [] fs [state_invariant_def, stack_ok_def] >> rw []
>- ( >- (
rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def] >> rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def, inc_bip_def] >>
last_x_assum drule >> disch_then drule >> rw [] >> last_x_assum drule >> disch_then drule >> rw [] >>
CCONTR_TAC >> fs [] >> rfs [LAST_EL] >> CCONTR_TAC >> fs [] >> rfs [LAST_EL] >>
Cases_on `length block'.body = s1.ip.i + 1` >> fs [PRE_SUB1] >> Cases_on `length block'.body = idx + 1` >> fs [PRE_SUB1] >>
fs [get_instr_cases] >> fs [get_instr_cases] >>
metis_tac [terminator_def]) metis_tac [terminator_def])
>- (fs [EVERY_MEM, frame_ok_def] >> metis_tac []))) >- (fs [EVERY_MEM, frame_ok_def] >> metis_tac [])))
QED QED
Theorem step_invariant:
∀p s1 l s2.
prog_ok p ∧ step p s1 l s2 ∧ state_invariant p s1
⇒
state_invariant p s2
Proof
rw [step_cases]
>- metis_tac [step_instr_invariant] >>
fs [get_instr_cases, inc_pc_def, inc_bip_def, state_invariant_def] >>
rw []
>- (
fs [ip_ok_def, prog_ok_def] >>
metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
>- (fs [globals_ok_def] >> metis_tac [])
>- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac [])
QED
Theorem exit_no_step: Theorem exit_no_step:
!p s1. get_instr p s1.ip Exit ⇒ ¬?l s2. step p s1 l s2 !p s1. get_instr p s1.ip (Inl Exit) ⇒ ¬?l s2. step p s1 l s2
Proof Proof
rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >> rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``]
`i = Exit` by metis_tac [get_instr_func] >> >- (
rw [step_instr_cases] `i = Exit` by metis_tac [get_instr_func, sumTheory.INL_11] >>
rw [step_instr_cases]) >>
metis_tac [get_instr_func, sumTheory.sum_distinct]
QED QED
Definition is_call_def: Definition is_call_def:
@ -461,13 +510,17 @@ Definition is_call_def:
End End
Theorem step_same_block: Theorem step_same_block:
∀p s1 l s2 i. ∀p s1 l s2.
get_instr p s1.ip i ∧ step_instr p s1 i l s2 ∧ ¬terminator i ∧ ~is_call i⇒ get_instr p s1.ip i ∧ step p s1 l s2 ∧
(∀i'. i = Inl i' ⇒ ¬terminator i' ∧ ¬is_call i') ⇒
s1.ip.f = s2.ip.f ∧ s1.ip.f = s2.ip.f ∧
s1.ip.b = s2.ip.b ∧ s1.ip.b = s2.ip.b ∧
s2.ip.i = s1.ip.i + 1 s2.ip.i = inc_bip s1.ip.i
Proof Proof
rw [step_instr_cases] >> simp [step_cases] >>
rpt gen_tac >> disch_tac >> fs [inc_pc_def] >>
`i = Inl i'` by metis_tac [get_instr_func] >>
fs [step_instr_cases] >> rfs [] >>
fs [terminator_def, is_call_def, inc_pc_def, update_result_def] fs [terminator_def, is_call_def, inc_pc_def, update_result_def]
QED QED
@ -488,10 +541,13 @@ Definition last_step_def:
last_step p s1 l s2 ⇔ last_step p s1 l s2 ⇔
∃i. ∃i.
step p s1 l s2 ∧ get_instr p s1.ip i ∧ step p s1 l s2 ∧ get_instr p s1.ip i ∧
(terminator i ∨ is_call i ∨ ¬∃l s3. step p s2 l s3) ((∃x. i = Inr x) ∨
(∃i'. i = Inl i' ∧ (terminator i' ∨ is_call i')) ∨
¬∃l s3. step p s2 l s3)
End End
(* Run all of the instructions up-to-and-including the next Call or terminator (* Run all of the instructions up-to-and-including the next Call or terminator.
* Stop after the phis too.
* *) * *)
Inductive multi_step: Inductive multi_step:
@ -502,7 +558,7 @@ Inductive multi_step:
(∀p s1 s2 s3 i l ls. (∀p s1 s2 s3 i l ls.
step p s1 l s2 ∧ step p s1 l s2 ∧
get_instr p s1.ip i ∧ get_instr p s1.ip (Inl i) ∧
¬(terminator i ∨ is_call i) ∧ ¬(terminator i ∨ is_call i) ∧
multi_step p s2 ls s3 multi_step p s2 ls s3
⇒ ⇒
@ -598,7 +654,10 @@ Definition instrs_left_def:
| Some d => | Some d =>
case alookup d.blocks s.ip.b of case alookup d.blocks s.ip.b of
| None => 0 | None => 0
| Some b => length b.body - s.ip.i | Some b =>
case s.ip.i of
| Phi_ip _ => length b.body + 1
| Offset idx => length b.body - idx
End End
Theorem extend_step_path: Theorem extend_step_path:
@ -635,8 +694,8 @@ Proof
fs [finite_length] >> fs [finite_length] >>
qexists_tac `n` >> rw [] qexists_tac `n` >> rw []
>- ( >- (
rw [last_step_def] >> fs [step_cases] >> qpat_x_assum `step _ _ _ _` mp_tac >>
metis_tac []) >> rw [last_step_def, step_cases] >> metis_tac []) >>
`length (plink p' (pcons (last p') l (stopped_at s))) = Some (n + Suc 1 - 1)` `length (plink p' (pcons (last p') l (stopped_at s))) = Some (n + Suc 1 - 1)`
by metis_tac [length_plink, alt_length_thm, optionTheory.OPTION_MAP_DEF] >> by metis_tac [length_plink, alt_length_thm, optionTheory.OPTION_MAP_DEF] >>
rw [] rw []
@ -668,11 +727,10 @@ Proof
pop_assum mp_tac >> simp [] >> pop_assum mp_tac >> simp [] >>
`?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >> `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
disch_then (qspec_then `i` mp_tac) >> simp [] >> disch_then (qspec_then `i` mp_tac) >> simp [] >>
pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
rw [] >>
`i' = i` by metis_tac [get_instr_func] >> rw [] >>
drule step_same_block >> disch_then drule >> simp [] >> drule step_same_block >> disch_then drule >> simp [] >>
rw [] >> fs [step_cases, get_instr_cases]) >> pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
rw [] >> fs [get_instr_cases, inc_bip_def] >> rw [] >> fs [] >>
rw [inc_bip_def] >> fs []) >>
`last path = first path1` `last path = first path1`
by ( by (
unabbrev_all_tac >> simp [Once unfold_thm] >> unabbrev_all_tac >> simp [Once unfold_thm] >>

13
sledge/semantics/miscScript.sml
Unescape View File

@ -123,6 +123,19 @@ Proof
fs [INJ_IFF] >> metis_tac [] fs [INJ_IFF] >> metis_tac []
QED QED
Theorem is_prefix_subset:
∀l1 l2. l1 ≼ l2 ⇒ set l1 ⊆ set l2
Proof
Induct_on `l1` >> rw [] >>
Cases_on `l2` >> fs [SUBSET_DEF]
QED
Theorem mem_el_front:
∀n l. Suc n < length l ⇒ mem (el n l) (front l)
Proof
Induct >> rw [] >> Cases_on `l` >> fs [FRONT_DEF] >> rw [] >> fs []
QED
(* ----- Theorems about log ----- *) (* ----- Theorems about log ----- *)
Theorem mul_div_bound: Theorem mul_div_bound:

3
sledge/semantics/settingsScript.sml
Unescape View File

@ -56,5 +56,8 @@ overload_on ("foldl", ``FOLDL``);
overload_on ("foldr", ``FOLDR``); overload_on ("foldr", ``FOLDR``);
overload_on ("option_rel", ``OPTREL``); overload_on ("option_rel", ``OPTREL``);
overload_on ("front", ``FRONT``); overload_on ("front", ``FRONT``);
overload_on ("Inl", ``INL``);
overload_on ("Inr", ``INR``);
overload_on ("mem", ``MEM``);
export_theory (); export_theory ();

Write Preview
Loading…
Cancel
Save