diff options
Diffstat (limited to 'backend/Machabstr.v')
| -rw-r--r-- | backend/Machabstr.v | 274 |
1 files changed, 155 insertions, 119 deletions
diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 25458dcc..8d5d72a9 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -7,6 +7,7 @@ Require Import Mem. Require Import Integers. Require Import Values. Require Import Mem. +Require Import Events. Require Import Globalenvs. Require Import Op. Require Import Locations. @@ -99,117 +100,132 @@ Variable ge: genv. Inductive exec_instr: function -> val -> frame -> - code -> regset -> frame -> mem -> + code -> regset -> frame -> mem -> trace -> code -> regset -> frame -> mem -> Prop := | exec_Mlabel: forall f sp parent lbl c rs fr m, exec_instr f sp parent (Mlabel lbl :: c) rs fr m - c rs fr m + E0 c rs fr m | exec_Mgetstack: forall f sp parent ofs ty dst c rs fr m v, get_slot fr ty (Int.signed ofs) v -> exec_instr f sp parent (Mgetstack ofs ty dst :: c) rs fr m - c (rs#dst <- v) fr m + E0 c (rs#dst <- v) fr m | exec_Msetstack: forall f sp parent src ofs ty c rs fr m fr', set_slot fr ty (Int.signed ofs) (rs src) fr' -> exec_instr f sp parent (Msetstack src ofs ty :: c) rs fr m - c rs fr' m + E0 c rs fr' m | exec_Mgetparam: forall f sp parent ofs ty dst c rs fr m v, get_slot parent ty (Int.signed ofs) v -> exec_instr f sp parent (Mgetparam ofs ty dst :: c) rs fr m - c (rs#dst <- v) fr m + E0 c (rs#dst <- v) fr m | exec_Mop: forall f sp parent op args res c rs fr m v, eval_operation ge sp op rs##args = Some v -> exec_instr f sp parent (Mop op args res :: c) rs fr m - c (rs#res <- v) fr m + E0 c (rs#res <- v) fr m | exec_Mload: forall f sp parent chunk addr args dst c rs fr m a v, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> exec_instr f sp parent (Mload chunk addr args dst :: c) rs fr m - c (rs#dst <- v) fr m + E0 c (rs#dst <- v) fr m | exec_Mstore: forall f sp parent chunk addr args src c rs fr m m' a, eval_addressing ge sp addr rs##args = Some a -> Mem.storev chunk m a (rs src) = Some m' -> exec_instr f sp parent (Mstore chunk addr args src :: c) rs fr m - c rs fr m' + E0 c rs fr m' | exec_Mcall: - forall f sp parent sig ros c rs fr m f' rs' m', + forall f sp parent sig ros c rs fr m t f' rs' m', find_function ge ros rs = Some f' -> - exec_function f' fr rs m rs' m' -> + exec_function f' fr rs m t rs' m' -> exec_instr f sp parent (Mcall sig ros :: c) rs fr m - c rs' fr m' + t c rs' fr m' + | exec_Malloc: + forall f sp parent c rs fr m sz m' blk, + rs (Conventions.loc_alloc_argument) = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', blk) -> + exec_instr f sp parent + (Malloc :: c) rs fr m + E0 c (rs#Conventions.loc_alloc_result <- + (Vptr blk Int.zero)) fr m' | exec_Mgoto: forall f sp parent lbl c rs fr m c', find_label lbl f.(fn_code) = Some c' -> exec_instr f sp parent (Mgoto lbl :: c) rs fr m - c' rs fr m + E0 c' rs fr m | exec_Mcond_true: forall f sp parent cond args lbl c rs fr m c', eval_condition cond rs##args = Some true -> find_label lbl f.(fn_code) = Some c' -> exec_instr f sp parent (Mcond cond args lbl :: c) rs fr m - c' rs fr m + E0 c' rs fr m | exec_Mcond_false: forall f sp parent cond args lbl c rs fr m, eval_condition cond rs##args = Some false -> exec_instr f sp parent (Mcond cond args lbl :: c) rs fr m - c rs fr m + E0 c rs fr m with exec_instrs: function -> val -> frame -> - code -> regset -> frame -> mem -> + code -> regset -> frame -> mem -> trace -> code -> regset -> frame -> mem -> Prop := | exec_refl: forall f sp parent c rs fr m, - exec_instrs f sp parent c rs fr m c rs fr m + exec_instrs f sp parent c rs fr m E0 c rs fr m | exec_one: - forall f sp parent c rs fr m c' rs' fr' m', - exec_instr f sp parent c rs fr m c' rs' fr' m' -> - exec_instrs f sp parent c rs fr m c' rs' fr' m' + forall f sp parent c rs fr m t c' rs' fr' m', + exec_instr f sp parent c rs fr m t c' rs' fr' m' -> + exec_instrs f sp parent c rs fr m t c' rs' fr' m' | exec_trans: - forall f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 c3 rs3 fr3 m3, - exec_instrs f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 -> - exec_instrs f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 -> - exec_instrs f sp parent c1 rs1 fr1 m1 c3 rs3 fr3 m3 + forall f sp parent c1 rs1 fr1 m1 t1 c2 rs2 fr2 m2 t2 c3 rs3 fr3 m3 t3, + exec_instrs f sp parent c1 rs1 fr1 m1 t1 c2 rs2 fr2 m2 -> + exec_instrs f sp parent c2 rs2 fr2 m2 t2 c3 rs3 fr3 m3 -> + t3 = t1 ** t2 -> + exec_instrs f sp parent c1 rs1 fr1 m1 t3 c3 rs3 fr3 m3 with exec_function_body: function -> frame -> val -> val -> - regset -> mem -> regset -> mem -> Prop := + regset -> mem -> trace -> regset -> mem -> Prop := | exec_funct_body: - forall f parent link ra rs m rs' m1 m2 stk fr1 fr2 fr3 c, + forall f parent link ra rs m t rs' m1 m2 stk fr1 fr2 fr3 c, Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> set_slot (init_frame f) Tint 0 link fr1 -> set_slot fr1 Tint 4 ra fr2 -> exec_instrs f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent f.(fn_code) rs fr2 m1 - (Mreturn :: c) rs' fr3 m2 -> - exec_function_body f parent link ra rs m rs' (Mem.free m2 stk) + t (Mreturn :: c) rs' fr3 m2 -> + exec_function_body f parent link ra rs m t rs' (Mem.free m2 stk) with exec_function: - function -> frame -> regset -> mem -> regset -> mem -> Prop := - | exec_funct: - forall f parent rs m rs' m', + fundef -> frame -> regset -> mem -> trace -> regset -> mem -> Prop := + | exec_funct_internal: + forall f parent rs m t rs' m', (forall link ra, Val.has_type link Tint -> Val.has_type ra Tint -> - exec_function_body f parent link ra rs m rs' m') -> - exec_function f parent rs m rs' m'. + exec_function_body f parent link ra rs m t rs' m') -> + exec_function (Internal f) parent rs m t rs' m' + | exec_funct_external: + forall ef parent args res rs1 rs2 m t, + event_match ef args t res -> + args = rs1##(Conventions.loc_external_arguments ef.(ef_sig)) -> + rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> + exec_function (External ef) parent rs1 m t rs2 m. Scheme exec_instr_ind4 := Minimality for exec_instr Sort Prop with exec_instrs_ind4 := Minimality for exec_instrs Sort Prop @@ -222,134 +238,155 @@ Scheme exec_instr_ind4 := Minimality for exec_instr Sort Prop by the [Scheme] command above. *) Lemma exec_mutual_induction: - forall (P + forall + (P P0 : function -> val -> frame -> code -> regset -> - frame -> mem -> code -> regset -> frame -> mem -> Prop) + frame -> + mem -> trace -> code -> regset -> frame -> mem -> Prop) (P1 : function -> - frame -> val -> val -> regset -> mem -> regset -> mem -> Prop) - (P2 : function -> frame -> regset -> mem -> regset -> mem -> Prop), + frame -> + val -> val -> regset -> mem -> trace -> regset -> mem -> Prop) + (P2 : fundef -> + frame -> regset -> mem -> trace -> regset -> mem -> Prop), (forall (f : function) (sp : val) (parent : frame) (lbl : label) (c : list instruction) (rs : regset) (fr : frame) (m : mem), - P f sp parent (Mlabel lbl :: c) rs fr m c rs fr m) -> - (forall (f : function) (sp : val) (parent : frame) (ofs : int) + P f sp parent (Mlabel lbl :: c) rs fr m E0 c rs fr m) -> + (forall (f0 : function) (sp : val) (parent : frame) (ofs : int) (ty : typ) (dst : mreg) (c : list instruction) (rs : regset) (fr : frame) (m : mem) (v : val), get_slot fr ty (Int.signed ofs) v -> - P f sp parent (Mgetstack ofs ty dst :: c) rs fr m c rs # dst <- v fr - m) -> - (forall (f : function) (sp : val) (parent : frame) (src : mreg) + P f0 sp parent (Mgetstack ofs ty dst :: c) rs fr m E0 c rs # dst <- v + fr m) -> + (forall (f1 : function) (sp : val) (parent : frame) (src : mreg) (ofs : int) (ty : typ) (c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem) (fr' : frame), set_slot fr ty (Int.signed ofs) (rs src) fr' -> - P f sp parent (Msetstack src ofs ty :: c) rs fr m c rs fr' m) -> - (forall (f : function) (sp : val) (parent : frame) (ofs : int) + P f1 sp parent (Msetstack src ofs ty :: c) rs fr m E0 c rs fr' m) -> + (forall (f2 : function) (sp : val) (parent : frame) (ofs : int) (ty : typ) (dst : mreg) (c : list instruction) (rs : regset) (fr : frame) (m : mem) (v : val), get_slot parent ty (Int.signed ofs) v -> - P f sp parent (Mgetparam ofs ty dst :: c) rs fr m c rs # dst <- v fr - m) -> - (forall (f : function) (sp : val) (parent : frame) (op : operation) + P f2 sp parent (Mgetparam ofs ty dst :: c) rs fr m E0 c rs # dst <- v + fr m) -> + (forall (f3 : function) (sp : val) (parent : frame) (op : operation) (args : list mreg) (res : mreg) (c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem) (v : val), eval_operation ge sp op rs ## args = Some v -> - P f sp parent (Mop op args res :: c) rs fr m c rs # res <- v fr m) -> - (forall (f : function) (sp : val) (parent : frame) + P f3 sp parent (Mop op args res :: c) rs fr m E0 c rs # res <- v fr m) -> + (forall (f4 : function) (sp : val) (parent : frame) (chunk : memory_chunk) (addr : addressing) (args : list mreg) (dst : mreg) (c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem) (a v : val), eval_addressing ge sp addr rs ## args = Some a -> loadv chunk m a = Some v -> - P f sp parent (Mload chunk addr args dst :: c) rs fr m c + P f4 sp parent (Mload chunk addr args dst :: c) rs fr m E0 c rs # dst <- v fr m) -> - (forall (f : function) (sp : val) (parent : frame) + (forall (f5 : function) (sp : val) (parent : frame) (chunk : memory_chunk) (addr : addressing) (args : list mreg) (src : mreg) (c : list instruction) (rs : mreg -> val) (fr : frame) (m m' : mem) (a : val), eval_addressing ge sp addr rs ## args = Some a -> storev chunk m a (rs src) = Some m' -> - P f sp parent (Mstore chunk addr args src :: c) rs fr m c rs fr m') -> - (forall (f : function) (sp : val) (parent : frame) (sig : signature) + P f5 sp parent (Mstore chunk addr args src :: c) rs fr m E0 c rs fr + m') -> + (forall (f6 : function) (sp : val) (parent : frame) (sig : signature) (ros : mreg + ident) (c : list instruction) (rs : regset) - (fr : frame) (m : mem) (f' : function) (rs' : regset) (m' : mem), + (fr : frame) (m : mem) (t : trace) (f' : fundef) (rs' : regset) + (m' : mem), find_function ge ros rs = Some f' -> - exec_function f' fr rs m rs' m' -> - P2 f' fr rs m rs' m' -> - P f sp parent (Mcall sig ros :: c) rs fr m c rs' fr m') -> - (forall (f : function) (sp : val) (parent : frame) (lbl : label) - (c : list instruction) (rs : regset) (fr : frame) (m : mem) - (c' : code), - find_label lbl (fn_code f) = Some c' -> - P f sp parent (Mgoto lbl :: c) rs fr m c' rs fr m) -> - (forall (f : function) (sp : val) (parent : frame) - (cond : condition) (args : list mreg) (lbl : label) + exec_function f' fr rs m t rs' m' -> + P2 f' fr rs m t rs' m' -> + P f6 sp parent (Mcall sig ros :: c) rs fr m t c rs' fr m') -> + (forall (f7 : function) (sp : val) (parent : frame) (c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem) + (sz : int) (m' : mem) (blk : block), + rs Conventions.loc_alloc_argument = Vint sz -> + alloc m 0 (Int.signed sz) = (m', blk) -> + P f7 sp parent (Malloc :: c) rs fr m E0 c + rs # Conventions.loc_alloc_result <- (Vptr blk Int.zero) fr m') -> + (forall (f7 : function) (sp : val) (parent : frame) (lbl : label) + (c : list instruction) (rs : regset) (fr : frame) (m : mem) (c' : code), + find_label lbl (fn_code f7) = Some c' -> + P f7 sp parent (Mgoto lbl :: c) rs fr m E0 c' rs fr m) -> + (forall (f8 : function) (sp : val) (parent : frame) (cond : condition) + (args : list mreg) (lbl : label) (c : list instruction) + (rs : mreg -> val) (fr : frame) (m : mem) (c' : code), eval_condition cond rs ## args = Some true -> - find_label lbl (fn_code f) = Some c' -> - P f sp parent (Mcond cond args lbl :: c) rs fr m c' rs fr m) -> - (forall (f : function) (sp : val) (parent : frame) - (cond : condition) (args : list mreg) (lbl : label) - (c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem), + find_label lbl (fn_code f8) = Some c' -> + P f8 sp parent (Mcond cond args lbl :: c) rs fr m E0 c' rs fr m) -> + (forall (f9 : function) (sp : val) (parent : frame) (cond : condition) + (args : list mreg) (lbl : label) (c : list instruction) + (rs : mreg -> val) (fr : frame) (m : mem), eval_condition cond rs ## args = Some false -> - P f sp parent (Mcond cond args lbl :: c) rs fr m c rs fr m) -> - (forall (f : function) (sp : val) (parent : frame) (c : code) + P f9 sp parent (Mcond cond args lbl :: c) rs fr m E0 c rs fr m) -> + (forall (f10 : function) (sp : val) (parent : frame) (c : code) (rs : regset) (fr : frame) (m : mem), - P0 f sp parent c rs fr m c rs fr m) -> - (forall (f : function) (sp : val) (parent : frame) (c : code) - (rs : regset) (fr : frame) (m : mem) (c' : code) (rs' : regset) - (fr' : frame) (m' : mem), - exec_instr f sp parent c rs fr m c' rs' fr' m' -> - P f sp parent c rs fr m c' rs' fr' m' -> - P0 f sp parent c rs fr m c' rs' fr' m') -> - (forall (f : function) (sp : val) (parent : frame) (c1 : code) - (rs1 : regset) (fr1 : frame) (m1 : mem) (c2 : code) (rs2 : regset) - (fr2 : frame) (m2 : mem) (c3 : code) (rs3 : regset) (fr3 : frame) - (m3 : mem), - exec_instrs f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 -> - P0 f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 -> - exec_instrs f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 -> - P0 f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 -> - P0 f sp parent c1 rs1 fr1 m1 c3 rs3 fr3 m3) -> - (forall (f : function) (parent : frame) (link ra : val) (rs : regset) - (m : mem) (rs' : regset) (m1 m2 : mem) (stk : block) - (fr1 fr2 fr3 : frame) (c : list instruction), - alloc m 0 (fn_stacksize f) = (m1, stk) -> - set_slot (init_frame f) Tint 0 link fr1 -> + P0 f10 sp parent c rs fr m E0 c rs fr m) -> + (forall (f11 : function) (sp : val) (parent : frame) (c : code) + (rs : regset) (fr : frame) (m : mem) (t : trace) (c' : code) + (rs' : regset) (fr' : frame) (m' : mem), + exec_instr f11 sp parent c rs fr m t c' rs' fr' m' -> + P f11 sp parent c rs fr m t c' rs' fr' m' -> + P0 f11 sp parent c rs fr m t c' rs' fr' m') -> + (forall (f12 : function) (sp : val) (parent : frame) (c1 : code) + (rs1 : regset) (fr1 : frame) (m1 : mem) (t1 : trace) (c2 : code) + (rs2 : regset) (fr2 : frame) (m2 : mem) (t2 : trace) (c3 : code) + (rs3 : regset) (fr3 : frame) (m3 : mem) (t3 : trace), + exec_instrs f12 sp parent c1 rs1 fr1 m1 t1 c2 rs2 fr2 m2 -> + P0 f12 sp parent c1 rs1 fr1 m1 t1 c2 rs2 fr2 m2 -> + exec_instrs f12 sp parent c2 rs2 fr2 m2 t2 c3 rs3 fr3 m3 -> + P0 f12 sp parent c2 rs2 fr2 m2 t2 c3 rs3 fr3 m3 -> + t3 = t1 ** t2 -> P0 f12 sp parent c1 rs1 fr1 m1 t3 c3 rs3 fr3 m3) -> + (forall (f13 : function) (parent : frame) (link ra : val) + (rs : regset) (m : mem) (t : trace) (rs' : regset) (m1 m2 : mem) + (stk : block) (fr1 fr2 fr3 : frame) (c : list instruction), + alloc m 0 (fn_stacksize f13) = (m1, stk) -> + set_slot (init_frame f13) Tint 0 link fr1 -> set_slot fr1 Tint 4 ra fr2 -> - exec_instrs f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent (fn_code f) rs fr2 m1 (Mreturn :: c) rs' fr3 - m2 -> - P0 f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent (fn_code f) rs fr2 m1 (Mreturn :: c) rs' fr3 m2 -> - P1 f parent link ra rs m rs' (free m2 stk)) -> - (forall (f : function) (parent : frame) (rs : regset) (m : mem) - (rs' : regset) (m' : mem), + exec_instrs f13 (Vptr stk (Int.repr (- fn_framesize f13))) parent + (fn_code f13) rs fr2 m1 t (Mreturn :: c) rs' fr3 m2 -> + P0 f13 (Vptr stk (Int.repr (- fn_framesize f13))) parent + (fn_code f13) rs fr2 m1 t (Mreturn :: c) rs' fr3 m2 -> + P1 f13 parent link ra rs m t rs' (free m2 stk)) -> + (forall (f14 : function) (parent : frame) (rs : regset) (m : mem) + (t : trace) (rs' : regset) (m' : mem), (forall link ra : val, Val.has_type link Tint -> Val.has_type ra Tint -> - exec_function_body f parent link ra rs m rs' m') -> + exec_function_body f14 parent link ra rs m t rs' m') -> (forall link ra : val, Val.has_type link Tint -> - Val.has_type ra Tint -> P1 f parent link ra rs m rs' m') -> - P2 f parent rs m rs' m') -> - (forall (f15 : function) (sp : val) (f16 : frame) (c : code) - (r : regset) (f17 : frame) (m : mem) (c0 : code) (r0 : regset) - (f18 : frame) (m0 : mem), - exec_instr f15 sp f16 c r f17 m c0 r0 f18 m0 -> - P f15 sp f16 c r f17 m c0 r0 f18 m0) - /\ (forall (f15 : function) (sp : val) (f16 : frame) (c : code) - (r : regset) (f17 : frame) (m : mem) (c0 : code) (r0 : regset) - (f18 : frame) (m0 : mem), - exec_instrs f15 sp f16 c r f17 m c0 r0 f18 m0 -> - P0 f15 sp f16 c r f17 m c0 r0 f18 m0) - /\ (forall (f15 : function) (f16 : frame) (v1 v2 : val) (r : regset) (m : mem) - (r0 : regset) (m0 : mem), - exec_function_body f15 f16 v1 v2 r m r0 m0 -> P1 f15 f16 v1 v2 r m r0 m0) - /\ (forall (f15 : function) (f16 : frame) (r : regset) (m : mem) + Val.has_type ra Tint -> P1 f14 parent link ra rs m t rs' m') -> + P2 (Internal f14) parent rs m t rs' m') -> + (forall (ef : external_function) (parent : frame) (args : list val) + (res : val) (rs1 : mreg -> val) (rs2 : RegEq.t -> val) (m : mem) + (t0 : trace), + event_match ef args t0 res -> + args = rs1 ## (Conventions.loc_external_arguments (ef_sig ef)) -> + rs2 = rs1 # (Conventions.loc_result (ef_sig ef)) <- res -> + P2 (External ef) parent rs1 m t0 rs2 m) -> + (forall (f16 : function) (v : val) (f17 : frame) (c : code) + (r : regset) (f18 : frame) (m : mem) (t : trace) (c0 : code) + (r0 : regset) (f19 : frame) (m0 : mem), + exec_instr f16 v f17 c r f18 m t c0 r0 f19 m0 -> + P f16 v f17 c r f18 m t c0 r0 f19 m0) + /\ (forall (f16 : function) (v : val) (f17 : frame) (c : code) + (r : regset) (f18 : frame) (m : mem) (t : trace) (c0 : code) + (r0 : regset) (f19 : frame) (m0 : mem), + exec_instrs f16 v f17 c r f18 m t c0 r0 f19 m0 -> + P0 f16 v f17 c r f18 m t c0 r0 f19 m0) + /\ (forall (f16 : function) (f17 : frame) (v v0 : val) (r : regset) + (m : mem) (t : trace) (r0 : regset) (m0 : mem), + exec_function_body f16 f17 v v0 r m t r0 m0 -> + P1 f16 f17 v v0 r m t r0 m0) + /\ (forall (f16 : fundef) (f17 : frame) (r : regset) (m : mem) (t : trace) (r0 : regset) (m0 : mem), - exec_function f15 f16 r m r0 m0 -> P2 f15 f16 r m r0 m0). + exec_function f16 f17 r m t r0 m0 -> P2 f16 f17 r m t r0 m0). Proof. intros. split. apply (exec_instr_ind4 P P0 P1 P2); assumption. split. apply (exec_instrs_ind4 P P0 P1 P2); assumption. @@ -359,13 +396,12 @@ Qed. End RELSEM. -Definition exec_program (p: program) (r: val) : Prop := +Definition exec_program (p: program) (t: trace) (r: val) : Prop := let ge := Genv.globalenv p in let m0 := Genv.init_mem p in exists b, exists f, exists rs, exists m, Genv.find_symbol ge p.(prog_main) = Some b /\ Genv.find_funct_ptr ge b = Some f /\ - f.(fn_sig) = mksignature nil (Some Tint) /\ - exec_function ge f empty_frame (Regmap.init Vundef) m0 rs m /\ - rs (Conventions.loc_result f.(fn_sig)) = r. + exec_function ge f empty_frame (Regmap.init Vundef) m0 t rs m /\ + rs R3 = r. |