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

[sledge sem] Add top-level llair semantics

Browse Source 
Summary:
Give the llair semantics observable side effects (writes to global
variables) and a semantic function mirroring the LLVM semantics. Start
sketching out the LLVM/llair translation equivalence proof in a top-down
way from the obvious statement of equality of the semantics.

Reviewed By: jberdine

Differential Revision: D17399654

fbshipit-source-id: 2170678a8
master
Scott Owens 5 years ago committed by Facebook Github Bot
parent 30c301a3e8
commit 17b3c7a49f
9 changed files with 385 additions and 108 deletions
Show Stats Download Patch File Download Diff File

2
sledge/semantics/Holmakefile
Unescape View File

@ -7,7 +7,7 @@ all: $(DEFAULT_TARGETS)
HOLHEAP = heap HOLHEAP = heap
EXTRA_CLEANS = heap EXTRA_CLEANS = heap
OBJNAMES = wordsLib.uo intLib.uo stringLib.uo integer_wordLib.uo finite_mapLib.uo alistLib.uo OBJNAMES = wordsLib.uo intLib.uo stringLib.uo integer_wordLib.uo finite_mapLib.uo alistLib.uo pathTheory.uo
DEPS = $(patsubst %,$(dprot $(SIGOBJ)/%),$(OBJNAMES)) DEPS = $(patsubst %,$(dprot $(SIGOBJ)/%),$(OBJNAMES))
$(HOLHEAP): $(DEPS) $(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $@ $(OBJNAMES) $(protect $(HOLDIR)/bin/buildheap) -o $@ $(OBJNAMES)

83
sledge/semantics/llairScript.sml
Unescape View File

@ -94,6 +94,7 @@ Datatype:
| Return exp | Return exp
| Throw exp | Throw exp
| Unreachable | Unreachable
| Exit
End End
Datatype: Datatype:
@ -116,7 +117,7 @@ Datatype:
End End
Datatype: Datatype:
llair = <| globals : global list; functions : (string, func) alist |> llair = <| glob_init : global list; functions : (string, func) alist |>
End End
(* ----- Semantic states ----- *) (* ----- Semantic states ----- *)
@ -139,10 +140,11 @@ End
Datatype: Datatype:
state = state =
<| bp : label; (* Pointer to the next block to execute *) <| bp : label; (* Pointer to the next block to execute *)
globals : var |-> word64; glob_addrs : var |-> num;
locals : var |-> v; locals : var |-> v;
stack : frame list; stack : frame list;
heap : unit heap |> heap : unit heap;
status : trace_type |>
End End
(* Assume that all pointers can fit in 64 bits *) (* Assume that all pointers can fit in 64 bits *)
@ -344,12 +346,17 @@ Definition update_results_def:
update_results xvs s = s with locals := s.locals |++ xvs update_results xvs s = s with locals := s.locals |++ xvs
End End
Inductive get_obs:
(∀s ptr bytes x. flookup s.glob_addrs x = Some ptr ⇒ get_obs s ptr bytes (W x bytes)) ∧
(∀s ptr bytes. ptr ∉ FRANGE s.glob_addrs ⇒ get_obs s ptr bytes Tau)
End
Inductive step_inst: Inductive step_inst:
(∀s ves rs. (∀s ves rs.
list_rel (eval_exp s) (map snd ves) rs list_rel (eval_exp s) (map snd ves) rs
⇒ ⇒
step_inst s step_inst s
(Move ves) (Move ves) Tau
(update_results (map (λ(v,r). (v, r)) (zip (map fst ves, rs))) s)) ∧ (update_results (map (λ(v,r). (v, r)) (zip (map fst ves, rs))) s)) ∧
(∀s x t e size ptr freeable interval bytes. (∀s x t e size ptr freeable interval bytes.
@ -359,19 +366,20 @@ Inductive step_inst:
bytes = map snd (get_bytes s.heap interval) bytes = map snd (get_bytes s.heap interval)
⇒ ⇒
step_inst s step_inst s
(Load (Var_name x t) e size) (Load (Var_name x t) e size) Tau
(update_results [(Var_name x t, fst (bytes_to_llair_value t bytes))] s)) ∧ (update_results [(Var_name x t, fst (bytes_to_llair_value t bytes))] s)) ∧
(∀s e1 e2 size ptr bytes freeable interval r. (∀s e1 e2 size ptr bytes freeable interval r obs.
eval_exp s e1 (FlatV ptr) ∧ eval_exp s e1 (FlatV ptr) ∧
eval_exp s e2 r ∧ eval_exp s e2 r ∧
interval = Interval freeable (i2n ptr) (i2n ptr + size) ∧ interval = Interval freeable (i2n ptr) (i2n ptr + size) ∧
is_allocated interval s.heap ∧ is_allocated interval s.heap ∧
bytes = llair_value_to_bytes r ∧ bytes = llair_value_to_bytes r ∧
length bytes = size length bytes = size ∧
get_obs s (i2n ptr) bytes obs
⇒ ⇒
step_inst s step_inst s
(Store e1 e2 size) (Store e1 e2 size) obs
(s with heap := set_bytes () bytes (i2n ptr) s.heap)) ∧ (s with heap := set_bytes () bytes (i2n ptr) s.heap)) ∧
(* TODO memset *) (* TODO memset *)
@ -387,7 +395,7 @@ Inductive step_inst:
bytes = map snd (get_bytes s.heap src_interval) bytes = map snd (get_bytes s.heap src_interval)
⇒ ⇒
step_inst s step_inst s
(Memcpy e1 e2 e3) (Memcpy e1 e2 e3) Tau
(s with heap := set_bytes () bytes (i2n dest_ptr) s.heap)) ∧ (s with heap := set_bytes () bytes (i2n dest_ptr) s.heap)) ∧
(* TODO memmove *) (* TODO memmove *)
@ -399,21 +407,21 @@ Inductive step_inst:
nfits ptr pointer_size nfits ptr pointer_size
⇒ ⇒
step_inst s step_inst s
(Alloc v e1 e2) (Alloc v e1 e2) Tau
(update_results [(v, FlatV (n2i ptr pointer_size))] (s with heap := new_h))) ∧ (update_results [(v, FlatV (n2i ptr pointer_size))] (s with heap := new_h))) ∧
(∀s e ptr. (∀s e ptr.
eval_exp s e (FlatV ptr) eval_exp s e (FlatV ptr)
⇒ ⇒
step_inst s step_inst s
(Free e) (Free e) Tau
(s with heap := deallocate [A (i2n ptr)] s.heap)) ∧ (s with heap := deallocate [A (i2n ptr)] s.heap)) ∧
(∀s x t nondet. (∀s x t nondet.
value_type t nondet value_type t nondet
⇒ ⇒
step_inst s step_inst s
(NondetI (Var_name x t)) (NondetI (Var_name x t)) Tau
(update_results [(Var_name x t, nondet)] s)) (update_results [(Var_name x t, nondet)] s))
End End
@ -445,7 +453,7 @@ Inductive step_term:
step_term prog s step_term prog s
(Call v (Lab_name fname bname) es t ret1 ret2) (Call v (Lab_name fname bname) es t ret1 ret2)
<| bp := Lab_name fname bname; <| bp := Lab_name fname bname;
globals := s.globals; glob_addrs := s.glob_addrs;
locals := alist_to_fmap (zip (f.params, vals)); locals := alist_to_fmap (zip (f.params, vals));
stack := stack :=
<| ret := ret1; <| ret := ret1;
@ -461,11 +469,12 @@ Inductive step_term:
step_term prog s step_term prog s
(Return e) (Return e)
<| bp := top.ret; <| bp := top.ret;
globals := s.globals; glob_addrs := s.glob_addrs;
locals := top.saved_locals |+ (top.ret_var, r); locals := top.saved_locals |+ (top.ret_var, r);
stack := rest; stack := rest;
heap := s.heap |>) heap := s.heap |>) ∧
(∀prog s. step_term prog s Exit (s with status := Complete))
(* TODO Throw *) (* TODO Throw *)
End End
@ -477,24 +486,46 @@ Inductive step_block:
(∀prog s1 t s2. (∀prog s1 t s2.
step_term prog s1 t s2 step_term prog s1 t s2
⇒ ⇒
step_block prog s1 [] t s2) ∧ step_block prog s1 [] [] t s2) ∧
(∀prog s1 i is t s2 s3. (∀prog s1 i1 i2 l1 is t s2.
step_inst s1 i s2 ∧ step_inst s1 i1 l1 s2 ∧
step_block prog s2 is t s3 (¬?l2 s3. step_inst s2 i2 l2 s3)
⇒ ⇒
step_block prog s1 (i::is) t s3) step_block prog s1 (i1::i2::is) [l1] t (s2 with status := Stuck)) ∧
(∀prog s1 i l is ls t s2 s3.
step_inst s1 i l s2 ∧
step_block prog s2 is ls t s3
⇒
step_block prog s1 (i::is) (l::ls) t s3)
End End
Inductive step: Inductive get_block:
(∀prog s fname bname f b s'. ∀prog bp fname bname f b.
s.bp = Lab_name fname bname ∧ bp = Lab_name fname bname ∧
alookup prog.functions fname = Some f ∧ alookup prog.functions fname = Some f ∧
alookup f.cfg s.bp = Some b ∧ alookup f.cfg bp = Some b
step_block prog s b.cmnd b.term s'
⇒ ⇒
step prog s s') get_block prog bp b
End
Inductive step:
∀prog s b ls s'.
get_block prog s.bp b ∧
step_block prog s b.cmnd ls b.term s' ∧
s.status = Partial
⇒
step prog s ls s'
End
Definition sem_def:
sem p s1 =
{ l1 | ∃path l2. l1 ∈ observation_prefixes ((last path).status, flat l2) ∧
toList (labels path) = Some l2 ∧
finite path ∧ okpath (step p) path ∧ first path = s1 }
End End
export_theory (); export_theory ();

18
sledge/semantics/llair_propScript.sml
Unescape View File

@ -8,7 +8,7 @@
(* Properties of the llair model *) (* Properties of the llair model *)
open HolKernel boolLib bossLib Parse; open HolKernel boolLib bossLib Parse;
open arithmeticTheory integerTheory integer_wordTheory wordsTheory; open arithmeticTheory integerTheory integer_wordTheory wordsTheory listTheory;
open settingsTheory miscTheory llairTheory; open settingsTheory miscTheory llairTheory;
new_theory "llair_prop"; new_theory "llair_prop";
@ -138,4 +138,20 @@ Proof
rw [w2i_n2w_pos]) rw [w2i_n2w_pos])
QED QED
Theorem eval_exp_ignores_lem:
∀s1 e v. eval_exp s1 e v ⇒ ∀s2. s1.locals = s2.locals ⇒ eval_exp s2 e v
Proof
ho_match_mp_tac eval_exp_ind >>
rw [] >> simp [Once eval_exp_cases] >>
TRY (qexists_tac `vals` >> rw [] >> fs [LIST_REL_EL_EQN] >> NO_TAC) >>
TRY (fs [LIST_REL_EL_EQN] >> NO_TAC) >>
metis_tac []
QED
Theorem eval_exp_ignores:
∀s1 e v s2. s1.locals = s2.locals ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v)
Proof
metis_tac [eval_exp_ignores_lem]
QED
export_theory (); export_theory ();

16
sledge/semantics/llvmScript.sml
Unescape View File

@ -178,15 +178,6 @@ Datatype:
heap : bool heap |> heap : bool heap |>
End End
(* Labels for the transitions to make externally observable behaviours apparent.
* For now, we'll consider this to be writes to global variables.
* *)
Datatype:
obs =
| Tau
| W glob_var (word8 list)
End
(* ----- Things about types ----- *) (* ----- Things about types ----- *)
(* Given a number n that fits into pointer_size number of bytes, create the (* Given a number n that fits into pointer_size number of bytes, create the
@ -671,13 +662,6 @@ Inductive step:
step p s l s' step p s l s'
End End
Datatype:
trace_type =
| Stuck
| Complete
| Partial
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 Exit then

2
sledge/semantics/llvm_liveScript.sml
Unescape View File

@ -20,7 +20,7 @@ Definition inc_pc_def:
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, withing a function *) * immediately reach, within a function *)
Definition next_ips_def: Definition next_ips_def:
(next_ips (Ret _) ip = {}) ∧ (next_ips (Ret _) ip = {}) ∧
(next_ips (Br _ l1 l2) ip = (next_ips (Br _ l1 l2) ip =

12
sledge/semantics/llvm_propScript.sml
Unescape View File

@ -483,9 +483,6 @@ QED
(* ----- A bigger-step semantics ----- *) (* ----- A bigger-step semantics ----- *)
Definition stuck_def:
stuck p s1 ⇔ ¬get_instr p s1.ip Exit ∧ ¬∃l s2. step p s1 l s2
End
Definition last_step_def: Definition last_step_def:
last_step p s1 l s2 ⇔ last_step p s1 l s2 ⇔
@ -512,15 +509,6 @@ Inductive multi_step:
multi_step p s1 (l::ls) s3) multi_step p s1 (l::ls) s3)
End End
Inductive observation_prefixes:
(∀l. observation_prefixes (Complete, l) (Complete, filter (\x. x ≠ Tau) l)) ∧
(∀l. observation_prefixes (Stuck, l) (Stuck, filter (\x. x ≠ Tau) l)) ∧
(∀l1 l2 x.
l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)
⇒
observation_prefixes (x, l1) (Partial, filter (\x. x ≠ Tau) l2))
End
Definition multi_step_sem_def: Definition multi_step_sem_def:
multi_step_sem p s1 = multi_step_sem p s1 =
{ l1 | ∃path l2. l1 ∈ observation_prefixes (get_observation p (last path), flat l2) ∧ { l1 | ∃path l2. l1 ∈ observation_prefixes (get_observation p (last path), flat l2) ∧

4
sledge/semantics/llvm_to_llairScript.sml
Unescape View File

@ -180,7 +180,7 @@ End
(* TODO *) (* TODO *)
Definition translate_instr_to_inst_def: Definition translate_instr_to_inst_def:
(translate_instr_to_inst emap (llvm$Store (t1, a1) (t2, a2)) = (translate_instr_to_inst emap (llvm$Store (t1, a1) (t2, a2)) =
llair$Store (translate_arg emap a1) (translate_arg emap a2) (sizeof t2)) ∧ llair$Store (translate_arg emap a2) (translate_arg emap a1) (sizeof t1)) ∧
(translate_instr_to_inst emap (Load r t (t1, a1)) = (translate_instr_to_inst emap (Load r t (t1, a1)) =
Load (translate_reg r t) (translate_arg emap a1) (sizeof t)) Load (translate_reg r t) (translate_arg emap a1) (sizeof t))
End End
@ -402,7 +402,7 @@ End
Definition translate_prog_def: Definition translate_prog_def:
translate_prog p = translate_prog p =
<| globals := ARB; <| glob_init := ARB;
functions := map (\(fname, d). (dest_fn fname, translate_def (dest_fn fname) d)) p |> functions := map (\(fname, d). (dest_fn fname, translate_def (dest_fn fname) d)) p |>
End End

302
sledge/semantics/llvm_to_llair_propScript.sml
Unescape View File

@ -9,14 +9,18 @@
open HolKernel boolLib bossLib Parse; open HolKernel boolLib bossLib Parse;
open listTheory arithmeticTheory pred_setTheory finite_mapTheory wordsTheory integer_wordTheory; open listTheory arithmeticTheory pred_setTheory finite_mapTheory wordsTheory integer_wordTheory;
open settingsTheory miscTheory llvmTheory llairTheory llair_propTheory llvm_to_llairTheory; open rich_listTheory pathTheory;
open settingsTheory miscTheory memory_modelTheory;
open llvmTheory llvm_propTheory llvm_liveTheory llairTheory llair_propTheory llvm_to_llairTheory;
new_theory "llvm_to_llair_prop"; new_theory "llvm_to_llair_prop";
set_grammar_ancestry ["llvm", "llair", "llvm_to_llair", "llvm_live"];
numLib.prefer_num (); numLib.prefer_num ();
Inductive v_rel: Inductive v_rel:
(∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) pointer_size))) ∧ (∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) llair$pointer_size))) ∧
(∀w. v_rel (FlatV (W1V w)) (FlatV (IntV (w2i w) 1))) ∧ (∀w. v_rel (FlatV (W1V w)) (FlatV (IntV (w2i w) 1))) ∧
(∀w. v_rel (FlatV (W8V w)) (FlatV (IntV (w2i w) 8))) ∧ (∀w. v_rel (FlatV (W8V w)) (FlatV (IntV (w2i w) 8))) ∧
(∀w. v_rel (FlatV (W32V w)) (FlatV (IntV (w2i w) 32))) ∧ (∀w. v_rel (FlatV (W32V w)) (FlatV (IntV (w2i w) 32))) ∧
@ -28,52 +32,52 @@ Inductive v_rel:
End End
(* Define when an LLVM state is related to a llair one. Parameterised over a (* Define when an LLVM state is related to a llair one. Parameterised over a
* relation on program counters, which chould be generated by the * relation on program counters, which should be generated by the
* transformation. It is not trivial because the translation cuts up blocks at * transformation. It is not trivial because the translation cuts up blocks at
* function calls and for remiving phi nodes. * function calls and adds blocks for removing phi nodes.
* *
* Also parameterised on a map for locals relating LLVM registers to llair * Also parameterised on a map for locals relating LLVM registers to llair
* expressions that compute the value in that register. This corresponds to part * expressions that compute the value in that register. This corresponds to part
* of the translation's state. * of the translation's state.
*) *)
Definition state_rel_def: Definition state_rel_def:
state_rel pc_rel emap (s:llvm$state) (s':llair$state) ⇔ state_rel prog pc_rel emap (s:llvm$state) (s':llair$state) ⇔
pc_rel s.ip s'.bp ∧ pc_rel s.ip s'.bp ∧
(* Unmapped registers in LLVM are unmapped in llair too *) (* Live LLVM registers are mapped and have a related value in the emap
(∀r. flookup s.locals r = None ⇒ flookup emap r = None) ∧ * (after evaluating) *)
(* Mapped LLVM registers have a related value in the emap (after (∀r. r ∈ live prog s.ip ⇒
* evaluating) *) ∃v v' e.
(∀r v. flookup s.locals r = Some v ⇒
∃v' e.
v_rel v.value v' ∧ v_rel v.value v' ∧
flookup s.locals r = Some v ∧
flookup emap r = Some e ∧ eval_exp s' e v') ∧ flookup emap r = Some e ∧ eval_exp s' e v') ∧
erase_tags s.heap = s'.heap erase_tags s.heap = s'.heap ∧
s'.status = get_observation prog s
End End
Theorem translate_arg_correct: Theorem v_rel_bytes:
∀s a v pc_rel emap s'. ∀v v'. v_rel v v' ⇒ llvm_value_to_bytes v = llair_value_to_bytes v'
state_rel pc_rel emap s s' ∧
eval s a = Some v
⇒
∃v'. eval_exp s' (translate_arg emap a) v' ∧ v_rel v.value v'
Proof Proof
Cases_on `a` >> rw [eval_def, translate_arg_def] ho_match_mp_tac v_rel_ind >>
>- cheat >> rw [v_rel_cases, llvm_value_to_bytes_def, llair_value_to_bytes_def] >>
CASE_TAC >> fs [PULL_EXISTS, state_rel_def] >> rw [value_to_bytes_def, llvmTheory.unconvert_value_def, w2n_i2n,
res_tac >> rfs [] >> metis_tac [] llairTheory.unconvert_value_def, llairTheory.pointer_size_def,
llvmTheory.pointer_size_def] >>
pop_assum mp_tac >>
qid_spec_tac `vs1` >>
Induct_on `vs2` >> rw [] >> rw []
QED QED
Theorem translate_constant_correct_lem: Theorem translate_constant_correct_lem:
(∀c s pc_rel emap s' (g : glob_var |-> β # word64). (∀c s prog pc_rel emap s' (g : glob_var |-> β # word64).
state_rel pc_rel emap s s' state_rel prog pc_rel emap s s'
⇒ ⇒
∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v') ∧ ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v') ∧
(∀(cs : (ty # const) list) s pc_rel emap s' (g : glob_var |-> β # word64). (∀(cs : (ty # const) list) s prog pc_rel emap s' (g : glob_var |-> β # word64).
state_rel pc_rel emap s s' state_rel prog pc_rel emap s s'
⇒ ⇒
∃v'. list_rel (eval_exp s') (map (translate_const o snd) cs) v' ∧ list_rel v_rel (map (eval_const g o snd) cs) v') ∧ ∃v'. list_rel (eval_exp s') (map (translate_const o snd) cs) v' ∧ list_rel v_rel (map (eval_const g o snd) cs) v') ∧
(∀(tc : ty # const) s pc_rel emap s' (g : glob_var |-> β # word64). (∀(tc : ty # const) s prog pc_rel emap s' (g : glob_var |-> β # word64).
state_rel pc_rel emap s s' state_rel prog pc_rel emap s s'
⇒ ⇒
∃v'. eval_exp s' (translate_const (snd tc)) v' ∧ v_rel (eval_const g (snd tc)) v') ∃v'. eval_exp s' (translate_const (snd tc)) v' ∧ v_rel (eval_const g (snd tc)) v')
Proof Proof
@ -97,14 +101,38 @@ Proof
QED QED
Theorem translate_constant_correct: Theorem translate_constant_correct:
∀c s pc_rel emap s' g. ∀c s prog pc_rel emap s' g.
state_rel pc_rel emap s s' state_rel prog pc_rel emap s s'
⇒ ⇒
∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v' ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v'
Proof Proof
metis_tac [translate_constant_correct_lem] metis_tac [translate_constant_correct_lem]
QED QED
Theorem translate_arg_correct:
∀s a v prog pc_rel emap s'.
state_rel prog pc_rel emap s s' ∧
eval s a = Some v ∧
arg_to_regs a ⊆ live prog s.ip
⇒
∃v'. eval_exp s' (translate_arg emap a) v' ∧ v_rel v.value v'
Proof
Cases_on `a` >> rw [eval_def, translate_arg_def] >> rw []
>- metis_tac [translate_constant_correct] >>
CASE_TAC >> fs [PULL_EXISTS, state_rel_def, arg_to_regs_def] >>
res_tac >> rfs [] >> metis_tac []
QED
Theorem is_allocated_state_rel:
∀prog pc_rel emap s1 s1'.
state_rel prog pc_rel emap s1 s1'
⇒
(∀i. is_allocated i s1.heap ⇔ is_allocated i s1'.heap)
Proof
rw [state_rel_def, is_allocated_def, erase_tags_def] >>
pop_assum mp_tac >> pop_assum (mp_tac o GSYM) >> rw []
QED
Theorem restricted_i2w_11: Theorem restricted_i2w_11:
∀i (w:'a word). INT_MIN (:'a) ≤ i ∧ i ≤ INT_MAX (:'a) ⇒ (i2w i : 'a word) = i2w (w2i w) ⇒ i = w2i w ∀i (w:'a word). INT_MIN (:'a) ≤ i ∧ i ≤ INT_MAX (:'a) ⇒ (i2w i : 'a word) = i2w (w2i w) ⇒ i = w2i w
Proof Proof
@ -132,8 +160,8 @@ Proof
QED QED
Theorem translate_extract_correct: Theorem translate_extract_correct:
∀pc_rel emap s1 s1' a v v1' e1' cs ns result. ∀prog pc_rel emap s1 s1' a v v1' e1' cs ns result.
state_rel pc_rel emap s1 s1' ∧ state_rel prog pc_rel emap s1 s1' ∧
map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧ map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = 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' ∧
@ -166,8 +194,8 @@ Proof
QED QED
Theorem translate_update_correct: Theorem translate_update_correct:
∀pc_rel emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result. ∀prog pc_rel emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
state_rel pc_rel emap s1 s1' ∧ state_rel prog pc_rel emap s1 s1' ∧
map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧ map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = 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' ∧
@ -205,26 +233,29 @@ Proof
metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN] metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
QED QED
(*
Theorem translate_instr_to_exp_correct: Theorem translate_instr_to_exp_correct:
∀emap instr r t s1 s1'. ∀emap instr r t s1 s1' s2 prog pc_rel.
classify_instr instr = Exp r t ∧ classify_instr instr = Exp r t ∧
state_rel pc_rel emap s1 s1' state_rel prog pc_rel emap s1 s1' ∧
⇒ get_instr prog s1.ip instr ∧
(∀s2. step_instr prog s1 instr s2 ⇒ step_instr prog s1 instr s2 ⇒
(∃v pv. eval_exp s1' (translate_instr_to_exp emap instr) v ∧ ∃v pv.
flookup s2.locals r = Some pv ∧ v_rel pv.value v)) eval_exp s1' (translate_instr_to_exp emap instr) v ∧
flookup s2.locals r = Some pv ∧ v_rel pv.value v
Proof Proof
recInduct translate_instr_to_exp_ind >> recInduct translate_instr_to_exp_ind >>
simp [translate_instr_to_exp_def, classify_instr_def] >> simp [translate_instr_to_exp_def, classify_instr_def] >>
conj_tac conj_tac
>- ( (* Sub *) >- ( (* Sub *)
rw [step_instr_cases, Once eval_exp_cases, do_sub_def, PULL_EXISTS] >> rw [step_instr_cases, Once eval_exp_cases, do_sub_def, PULL_EXISTS] >>
simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >> simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
simp [v_rel_cases, PULL_EXISTS] >> simp [v_rel_cases, PULL_EXISTS] >>
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 >>
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 >>
drule get_instr_live >> simp [uses_def] >> strip_tac >>
BasicProvers.EVERY_CASE_TAC >> fs [translate_ty_def, translate_size_def] >> BasicProvers.EVERY_CASE_TAC >> fs [translate_ty_def, translate_size_def] >>
rfs [v_rel_cases] >> rfs [v_rel_cases] >>
pairarg_tac >> fs [] >> pairarg_tac >> fs [] >>
@ -263,16 +294,193 @@ Proof
metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:64)``, metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:64)``,
SIMP_CONV (srw_ss()) [] ``INT_MAX (:64)``])) >> SIMP_CONV (srw_ss()) [] ``INT_MAX (:64)``])) >>
conj_tac conj_tac
>- ( >- ( (* Extractvalue *)
rw [step_instr_cases] >> rw [step_instr_cases] >>
simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >> simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
metis_tac [translate_arg_correct, translate_extract_correct]) >> metis_tac [uses_def, get_instr_live, translate_arg_correct, translate_extract_correct]) >>
conj_tac conj_tac
>- ( >- ( (* Updatevalue *)
rw [step_instr_cases] >> rw [step_instr_cases] >>
simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >> simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
metis_tac [translate_arg_correct, translate_update_correct]) >> drule get_instr_live >> simp [uses_def] >>
metis_tac [get_instr_live, translate_arg_correct, translate_update_correct]) >>
cheat cheat
QED QED
Triviality eval_exp_help:
(s1 with heap := h).locals = s1.locals
Proof
rw []
QED
Theorem erase_tags_set_bytes:
∀p v l h. erase_tags (set_bytes p v l h) = set_bytes () v l (erase_tags h)
Proof
Induct_on `v` >> rw [set_bytes_def] >>
irule (METIS_PROVE [] ``x = y ⇒ f a b c x = f a b c y``) >>
rw [erase_tags_def]
QED
Theorem translate_instr_to_inst_correct:
∀prog pc_rel emap instr s1 s1' s2.
classify_instr instr = Non_exp ∧
state_rel prog pc_rel emap s1 s1' ∧
get_instr prog s1.ip instr ∧
step_instr prog s1 instr s2 ⇒
∃s2'.
step_inst s1' (translate_instr_to_inst emap instr) s2' ∧
state_rel prog pc_rel emap s2 s2'
Proof
rw [step_instr_cases] >>
fs [classify_instr_def, translate_instr_to_inst_def]
>- ( (* Load *)
cheat)
>- ( (* Store *)
simp [step_inst_cases, PULL_EXISTS] >>
drule get_instr_live >> rw [uses_def] >>
drule translate_arg_correct >> disch_then drule >> disch_then drule >>
qpat_x_assum `eval _ _ = Some _` mp_tac >>
drule translate_arg_correct >> disch_then drule >> disch_then drule >>
rw [] >>
qpat_x_assum `v_rel (FlatV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
HINT_EXISTS_TAC >> rw [] >>
qexists_tac `freeable` >> rw [] >>
HINT_EXISTS_TAC >> rw []
>- metis_tac [v_rel_bytes]
>- (
fs [w2n_i2n, pointer_size_def] >>
metis_tac [v_rel_bytes, is_allocated_state_rel, ADD_COMM]) >>
fs [state_rel_def] >>
rw []
>- cheat
>- (
fs [llvmTheory.inc_pc_def] >>
`r ∈ live prog s1.ip`
by (
drule live_gen_kill >>
rw [next_ips_def, assigns_def, uses_def, inc_pc_def]) >>
first_x_assum drule >> rw [] >>
metis_tac [eval_exp_ignores, eval_exp_help])
>- (
rw [llvmTheory.inc_pc_def, w2n_i2n, pointer_size_def, erase_tags_set_bytes] >>
metis_tac[v_rel_bytes]))
>- cheat
>- cheat
>- cheat
QED
simp [step_inst_cases, PULL_EXISTS] >>
Cases_on `r` >> simp [translate_reg_def] >>
drule get_instr_live >> rw [uses_def] >>
drule translate_arg_correct >> disch_then drule >> disch_then drule >>
simp [Once v_rel_cases] >> rw [] >>
qexists_tac `IntV (w2i w) pointer_size` >> rw [] >>
qexists_tac `freeable` >> rw []
>- (fs [w2n_i2n, pointer_size_def] >> metis_tac [is_allocated_state_rel]) >>
fs [state_rel_def] >> rw []
>- cheat
>- (
fs [llvmTheory.inc_pc_def, update_results_def, update_result_def] >>
rw [] >> fs [FLOOKUP_UPDATE] >> rw []
>- (
cheat)
>- (
`r ∈ live prog s1.ip`
by (
drule live_gen_kill >>
rw [next_ips_def, assigns_def, uses_def, inc_pc_def]) >>
first_x_assum drule >> rw [] >>
qexists_tac `v` >>
qexists_tac `v'` >>
qexists_tac `e` >>
rw []
metis_tac [eval_exp_ignores, eval_exp_help])
>- fs [update_results_def, llvmTheory.inc_pc_def, update_result_def]
*)
Definition translate_trace_def:
(translate_trace types Tau = Tau ) ∧
(translate_trace types (W gv bytes) = W (translate_glob_var gv (types gv)) bytes)
End
Theorem multi_step_to_step_block:
∀prog s1 s1' tr s2.
state_rel prog pc_rel emap s1 s1' ∧
multi_step prog s1 tr s2
⇒
∃s2' b.
get_block (translate_prog prog) s1'.bp b ∧
step_block (translate_prog prog) s1' b.cmnd (map (translate_trace types) tr) b.term s2' ∧
state_rel prog pc_rel emap s2 s2'
Proof
cheat
QED
Theorem trans_trace_not_tau:
∀types. (λx. x ≠ Tau) ∘ translate_trace types = (λx. x ≠ Tau)
Proof
rw [FUN_EQ_THM] >> eq_tac >> rw [translate_trace_def] >>
Cases_on `x` >> fs [translate_trace_def]
QED
Theorem translate_prog_correct_lem1:
∀path.
okpath (multi_step prog) path ∧ finite path
⇒
∀s1'.
state_rel prog pc_rel emap (first path) s1'
⇒
∃path'.
finite path' ∧
okpath (step (translate_prog prog)) path' ∧
first path' = s1' ∧
labels path' = LMAP (map (translate_trace types)) (labels path) ∧
state_rel prog pc_rel emap (last path) (last path')
Proof
ho_match_mp_tac finite_okpath_ind >> rw []
>- (qexists_tac `stopped_at s1'` >> rw []) >>
drule multi_step_to_step_block >> disch_then drule >>
disch_then (qspec_then `types` mp_tac) >> rw [] >>
first_x_assum drule >> rw [] >>
qexists_tac `pcons s1' (map (translate_trace types) r) path'` >> rw [] >>
simp [step_cases] >> qexists_tac `b` >> simp [] >>
fs [state_rel_def] >> simp [get_observation_def] >>
fs [Once multi_step_cases, last_step_def] >> rw [] >>
metis_tac [get_instr_func, exit_no_step]
QED
Theorem translate_prog_correct:
∀prog s1 s1'.
state_rel prog pc_rel emap s1 s1'
⇒
image (I ## map (translate_trace types)) (multi_step_sem prog s1) = sem (translate_prog prog) s1'
Proof
rw [sem_def, multi_step_sem_def, EXTENSION] >> eq_tac >> rw []
>- (
drule translate_prog_correct_lem1 >> disch_then drule >> disch_then drule >>
disch_then (qspec_then `types` mp_tac) >> rw [] >>
qexists_tac `path'` >> rw [] >>
fs [IN_DEF, observation_prefixes_cases, toList_some] >> rw [] >>
rfs [lmap_fromList] >>
rw [GSYM MAP_FLAT, FILTER_MAP, trans_trace_not_tau]
>- fs [state_rel_def]
>- fs [state_rel_def] >>
qexists_tac `map (translate_trace types) l2'` >>
simp [GSYM MAP_FLAT, FILTER_MAP, trans_trace_not_tau] >>
`INJ (translate_trace types) (set l2' ∪ set (flat l2)) UNIV`
by (
simp [INJ_DEF] >> rpt gen_tac >>
Cases_on `x` >> Cases_on `y` >> simp [translate_trace_def] >>
Cases_on `a` >> Cases_on `a'` >> simp [translate_glob_var_def]) >>
fs [INJ_MAP_EQ_IFF, inj_map_prefix_iff] >> rw [] >>
fs [state_rel_def])
>- cheat
QED
export_theory (); export_theory ();

52
sledge/semantics/miscScript.sml
Unescape View File

@ -10,7 +10,7 @@
open HolKernel boolLib bossLib Parse; open HolKernel boolLib bossLib Parse;
open listTheory rich_listTheory arithmeticTheory integerTheory llistTheory pathTheory; open listTheory rich_listTheory arithmeticTheory integerTheory llistTheory pathTheory;
open integer_wordTheory wordsTheory; open integer_wordTheory wordsTheory pred_setTheory;
open finite_mapTheory open logrootTheory numposrepTheory; open finite_mapTheory open logrootTheory numposrepTheory;
open settingsTheory; open settingsTheory;
@ -18,6 +18,31 @@ new_theory "misc";
numLib.prefer_num (); numLib.prefer_num ();
(* Labels for the transitions to make externally observable behaviours apparent.
* For now, we'll consider this to be writes to global variables.
* *)
Datatype:
obs =
| Tau
| W 'a (word8 list)
End
Datatype:
trace_type =
| Stuck
| Complete
| Partial
End
Inductive observation_prefixes:
(∀l. observation_prefixes (Complete, l) (Complete, filter (\x. x ≠ Tau) l)) ∧
(∀l. observation_prefixes (Stuck, l) (Stuck, filter (\x. x ≠ Tau) l)) ∧
(∀l1 l2 x.
l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)
⇒
observation_prefixes (x, l1) (Partial, filter (\x. x ≠ Tau) l2))
End
(* ----- Theorems about list library functions ----- *) (* ----- Theorems about list library functions ----- *)
Theorem dropWhile_map: Theorem dropWhile_map:
@ -85,6 +110,19 @@ Proof
rw [FDIFF_def, FLOOKUP_DRESTRICT] >> fs [] rw [FDIFF_def, FLOOKUP_DRESTRICT] >> fs []
QED QED
Theorem inj_map_prefix_iff:
∀f l1 l2. INJ f (set l1 ∪ set l2) UNIV ⇒ (map f l1 ≼ map f l2 ⇔ l1 ≼ l2)
Proof
Induct_on `l1` >> rw [] >>
Cases_on `l2` >> rw [] >>
`INJ f (set l1 ∪ set t) UNIV`
by (
irule INJ_SUBSET >> qexists_tac `(h INSERT set l1) ∪ (set (h'::t))` >>
simp [SUBSET_DEF] >> fs [] >>
metis_tac []) >>
fs [INJ_IFF] >> metis_tac []
QED
(* ----- Theorems about log ----- *) (* ----- Theorems about log ----- *)
Theorem mul_div_bound: Theorem mul_div_bound:
@ -251,6 +289,18 @@ Proof
metis_tac [] metis_tac []
QED QED
Theorem lmap_fromList:
!f l. LMAP f (fromList l) = fromList (map f l)
Proof
Induct_on `l` >> rw []
QED
Theorem fromList_11[simp]:
!l1 l2. fromList l1 = fromList l2 ⇔ l1 = l2
Proof
Induct >> rw [] >>
Cases_on `l2` >> fs []
QED
(* ----- Theorems about labelled transition system paths ----- *) (* ----- Theorems about labelled transition system paths ----- *)

Write Preview
Loading…
Cancel
Save