diff options
Diffstat (limited to 'backend/Machabstr.v')
| -rw-r--r-- | backend/Machabstr.v | 371 |
1 files changed, 371 insertions, 0 deletions
diff --git a/backend/Machabstr.v b/backend/Machabstr.v new file mode 100644 index 00000000..25458dcc --- /dev/null +++ b/backend/Machabstr.v @@ -0,0 +1,371 @@ +(** Alternate semantics for the Mach intermediate language. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Mem. +Require Import Integers. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Conventions. +Require Import Mach. + +(** This file defines an alternate semantics for the Mach intermediate + language, which differ from the standard semantics given in file [Mach] + as follows: the stack access instructions [Mgetstack], [Msetstack] + and [Mgetparam] are interpreted not as memory accesses, but as + accesses in a frame environment, not resident in memory. The evaluation + relations take two such frame environments as parameters and results, + one for the current function and one for its caller. + + Not having the frame data in memory facilitates the proof of + the [Stacking] pass, which shows that the generated code executes + correctly with the alternate semantics. In file [Machabstr2mach], + we show an implication from this alternate semantics to + the standard semantics, thus establishing that the [Stacking] pass + generates code that behaves correctly against the standard [Mach] + semantics as well. *) + +(** * Structure of abstract stack frames *) + +(** A frame has the same structure as the contents of a memory block. *) + +Definition frame := block_contents. + +Definition empty_frame := empty_block 0 0. + +Definition mem_type (ty: typ) := + match ty with Tint => Size32 | Tfloat => Size64 end. + +(** [get_slot fr ty ofs v] holds if the frame [fr] contains value [v] + with type [ty] at word offset [ofs]. *) + +Inductive get_slot: frame -> typ -> Z -> val -> Prop := + | get_slot_intro: + forall fr ty ofs v, + 0 <= ofs -> + fr.(low) + ofs + 4 * typesize ty <= 0 -> + v = load_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) -> + get_slot fr ty ofs v. + +Remark size_mem_type: + forall ty, size_mem (mem_type ty) = 4 * typesize ty. +Proof. + destruct ty; reflexivity. +Qed. + +Remark set_slot_undef_outside: + forall fr ty ofs v, + fr.(high) = 0 -> + 0 <= ofs -> + fr.(low) + ofs + 4 * typesize ty <= 0 -> + (forall x, x < fr.(low) \/ x >= fr.(high) -> fr.(contents) x = Undef) -> + (forall x, x < fr.(low) \/ x >= fr.(high) -> + store_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) v x = Undef). +Proof. + intros. apply store_contents_undef_outside with fr.(low) fr.(high). + rewrite <- size_mem_type in H1. omega. assumption. assumption. +Qed. + +(** [set_slot fr ty ofs v fr'] holds if frame [fr'] is obtained from + frame [fr] by storing value [v] with type [ty] at word offset [ofs]. *) + +Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop := + | set_slot_intro: + forall fr ty ofs v + (A: fr.(high) = 0) + (B: 0 <= ofs) + (C: fr.(low) + ofs + 4 * typesize ty <= 0), + set_slot fr ty ofs v + (mkblock fr.(low) fr.(high) + (store_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) v) + (set_slot_undef_outside fr ty ofs v A B C fr.(undef_outside))). + +Definition init_frame (f: function) := + empty_block (- f.(fn_framesize)) 0. + +Section RELSEM. + +Variable ge: genv. + +(** Execution of one instruction has the form + [exec_instr ge f sp parent c rs fr m c' rs' fr' m'], + where [parent] is the caller's frame (read-only) + and [fr], [fr'] are the current frame, before and after execution + of one instruction. The other parameters are as in the Mach semantics. *) + +Inductive exec_instr: + function -> val -> frame -> + code -> regset -> frame -> mem -> + 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 + | 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 + | 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 + | 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 + | 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 + | 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 + | 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' + | exec_Mcall: + forall f sp parent sig ros c rs fr m f' rs' m', + find_function ge ros rs = Some f' -> + exec_function f' fr rs m rs' m' -> + exec_instr f sp parent + (Mcall sig ros :: c) rs fr m + c rs' 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 + | 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 + | 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 + +with exec_instrs: + function -> val -> frame -> + code -> regset -> frame -> mem -> + 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_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' + | 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 + +with exec_function_body: + function -> frame -> val -> val -> + regset -> mem -> regset -> mem -> Prop := + | exec_funct_body: + forall f parent link ra rs m 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) + +with exec_function: + function -> frame -> regset -> mem -> regset -> mem -> Prop := + | exec_funct: + forall f parent rs m 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'. + +Scheme exec_instr_ind4 := Minimality for exec_instr Sort Prop + with exec_instrs_ind4 := Minimality for exec_instrs Sort Prop + with exec_function_body_ind4 := Minimality for exec_function_body Sort Prop + with exec_function_ind4 := Minimality for exec_function Sort Prop. + +(** Ugly mutual induction principle over evaluation derivations. + Coq is not able to generate it directly, even though it is + an immediate consequence of the 4 induction principles generated + by the [Scheme] command above. *) + +Lemma exec_mutual_induction: + forall (P + P0 : function -> + val -> + frame -> + code -> + regset -> + frame -> mem -> code -> regset -> frame -> mem -> Prop) + (P1 : function -> + frame -> val -> val -> regset -> mem -> regset -> mem -> Prop) + (P2 : function -> frame -> regset -> mem -> 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) + (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) + (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) + (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) + (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) + (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 + rs # dst <- v fr m) -> + (forall (f : 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) + (ros : mreg + ident) (c : list instruction) (rs : regset) + (fr : frame) (m : mem) (f' : function) (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) + (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), + 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) + (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 -> + 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), + (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') -> + (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) + (r0 : regset) (m0 : mem), + exec_function f15 f16 r m r0 m0 -> P2 f15 f16 r m r0 m0). +Proof. + intros. split. apply (exec_instr_ind4 P P0 P1 P2); assumption. + split. apply (exec_instrs_ind4 P P0 P1 P2); assumption. + split. apply (exec_function_body_ind4 P P0 P1 P2); assumption. + apply (exec_function_ind4 P P0 P1 P2); assumption. +Qed. + +End RELSEM. + +Definition exec_program (p: program) (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. + |