From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/LTL.v | 357 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 357 insertions(+) create mode 100644 backend/LTL.v (limited to 'backend/LTL.v') diff --git a/backend/LTL.v b/backend/LTL.v new file mode 100644 index 00000000..2c36cba9 --- /dev/null +++ b/backend/LTL.v @@ -0,0 +1,357 @@ +(** The LTL intermediate language: abstract syntax and semantics. + + LTL (``Location Transfer Language'') is the target language + for register allocation and the source language for linearization. *) + +Require Import Relations. +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Conventions. + +(** * Abstract syntax *) + +(** LTL is close to RTL, but uses locations instead of pseudo-registers, + and basic blocks instead of single instructions as nodes of its + control-flow graph. *) + +Definition node := positive. + +(** A basic block is a sequence of instructions terminated by + a [Bgoto], [Bcond] or [Breturn] instruction. (This invariant + is enforced by the following inductive type definition.) + The instructions behave like the similarly-named instructions + of RTL. They take machine registers (type [mreg]) as arguments + and results. Two new instructions are added: [Bgetstack] + and [Bsetstack], which are ``move'' instructions between + a machine register and a stack slot. *) + +Inductive block: Set := + | Bgetstack: slot -> mreg -> block -> block + | Bsetstack: mreg -> slot -> block -> block + | Bop: operation -> list mreg -> mreg -> block -> block + | Bload: memory_chunk -> addressing -> list mreg -> mreg -> block -> block + | Bstore: memory_chunk -> addressing -> list mreg -> mreg -> block -> block + | Bcall: signature -> mreg + ident -> block -> block + | Bgoto: node -> block + | Bcond: condition -> list mreg -> node -> node -> block + | Breturn: block. + +Definition code: Set := PTree.t block. + +(** Unlike in RTL, parameter passing (passing values of the arguments + to a function call to the parameters of the called function) is done + via conventional locations (machine registers and stack slots). + Consequently, the [Bcall] instruction has no list of argument registers, + and function descriptions have no list of parameter registers. *) + +Record function: Set := mkfunction { + fn_sig: signature; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node; + fn_code_wf: + forall (pc: node), Plt pc (Psucc fn_entrypoint) \/ fn_code!pc = None +}. + +Definition program := AST.program function. + +(** * Operational semantics *) + +Definition genv := Genv.t function. +Definition locset := Locmap.t. + +Section RELSEM. + +(** Calling conventions are reflected at the level of location sets + (environments mapping locations to values) by the following two + functions. + + [call_regs caller] returns the location set at function entry, + as a function of the location set [caller] of the calling function. +- Machine registers have the same values as in the caller. +- Incoming stack slots (used for parameter passing) have the same + values as the corresponding outgoing stack slots (used for argument + passing) in the caller. +- Local and outgoing stack slots are initialized to undefined values. +*) + +Definition call_regs (caller: locset) : locset := + fun (l: loc) => + match l with + | R r => caller (R r) + | S (Local ofs ty) => Vundef + | S (Incoming ofs ty) => caller (S (Outgoing ofs ty)) + | S (Outgoing ofs ty) => Vundef + end. + +(** [return_regs caller callee] returns the location set after + a call instruction, as a function of the location set [caller] + of the caller before the call instruction and of the location + set [callee] of the callee at the return instruction. +- Callee-save machine registers have the same values as in the caller + before the call. +- Caller-save and temporary machine registers have the same values + as in the callee at the return point. +- Stack slots have the same values as in the caller before the call. +*) + +Definition return_regs (caller callee: locset) : locset := + fun (l: loc) => + match l with + | R r => + if In_dec Loc.eq (R r) Conventions.temporaries then + callee (R r) + else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + callee (R r) + else + caller (R r) + | S s => caller (S s) + end. + +Variable ge: genv. + +Definition find_function (ros: mreg + ident) (rs: locset) : option function := + match ros with + | inl r => Genv.find_funct ge (rs (R r)) + | inr symb => + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + +Definition reglist (rl: list mreg) (rs: locset) : list val := + List.map (fun r => rs (R r)) rl. + +(** The dynamic semantics of LTL, like that of RTL, is a combination + of small-step transition semantics and big-step semantics. + Function calls are treated in big-step style so that they appear + as a single transition in the caller function. Other instructions + are treated in purely small-step style, as a single transition. + + The introduction of basic blocks increases the number of inductive + predicates needed to express the semantics: +- [exec_instr ge sp b ls m b' ls' m'] is the execution of the first + instruction of block [b]. [b'] is the remainder of the block. +- [exec_instrs ge sp b ls m b' ls' m'] is similar, but executes + zero, one or several instructions at the beginning of block [b]. +- [exec_block ge sp b ls m out ls' m'] executes all instructions + of block [b]. The outcome [out] is either [Cont s], indicating + that the block terminates by branching to block labeled [s], + or [Return], indicating that the block terminates by returning + from the current function. +- [exec_blocks ge code sp pc ls m out ls' m'] executes a sequence + of zero, one or several blocks, starting at the block labeled [pc]. + [code] is the control-flow graph for the current function. + The outcome [out] indicates how the last block in this sequence + terminates: by branching to another block or by returning from the + function. +- [exec_function ge f ls m ls' m'] executes the body of function [f], + from its entry point to the first [Lreturn] instruction encountered. + + In all these predicates, [ls] and [ls'] are the location sets + (values of locations) at the beginning and end of the transitions, + respectively. +*) + +Inductive outcome: Set := + | Cont: node -> outcome + | Return: outcome. + +Inductive exec_instr: val -> + block -> locset -> mem -> + block -> locset -> mem -> Prop := + | exec_Bgetstack: + forall sp sl r b rs m, + exec_instr sp (Bgetstack sl r b) rs m + b (Locmap.set (R r) (rs (S sl)) rs) m + | exec_Bsetstack: + forall sp r sl b rs m, + exec_instr sp (Bsetstack r sl b) rs m + b (Locmap.set (S sl) (rs (R r)) rs) m + | exec_Bop: + forall sp op args res b rs m v, + eval_operation ge sp op (reglist args rs) = Some v -> + exec_instr sp (Bop op args res b) rs m + b (Locmap.set (R res) v rs) m + | exec_Bload: + forall sp chunk addr args dst b rs m a v, + eval_addressing ge sp addr (reglist args rs) = Some a -> + loadv chunk m a = Some v -> + exec_instr sp (Bload chunk addr args dst b) rs m + b (Locmap.set (R dst) v rs) m + | exec_Bstore: + forall sp chunk addr args src b rs m m' a, + eval_addressing ge sp addr (reglist args rs) = Some a -> + storev chunk m a (rs (R src)) = Some m' -> + exec_instr sp (Bstore chunk addr args src b) rs m + b rs m' + | exec_Bcall: + forall sp sig ros b rs m f rs' m', + find_function ros rs = Some f -> + sig = f.(fn_sig) -> + exec_function f rs m rs' m' -> + exec_instr sp (Bcall sig ros b) rs m + b (return_regs rs rs') m' + +with exec_instrs: val -> + block -> locset -> mem -> + block -> locset -> mem -> Prop := + | exec_refl: + forall sp b rs m, + exec_instrs sp b rs m b rs m + | exec_one: + forall sp b1 rs1 m1 b2 rs2 m2, + exec_instr sp b1 rs1 m1 b2 rs2 m2 -> + exec_instrs sp b1 rs1 m1 b2 rs2 m2 + | exec_trans: + forall sp b1 rs1 m1 b2 rs2 m2 b3 rs3 m3, + exec_instrs sp b1 rs1 m1 b2 rs2 m2 -> + exec_instrs sp b2 rs2 m2 b3 rs3 m3 -> + exec_instrs sp b1 rs1 m1 b3 rs3 m3 + +with exec_block: val -> + block -> locset -> mem -> + outcome -> locset -> mem -> Prop := + | exec_Bgoto: + forall sp b rs m s rs' m', + exec_instrs sp b rs m (Bgoto s) rs' m' -> + exec_block sp b rs m (Cont s) rs' m' + | exec_Bcond_true: + forall sp b rs m cond args ifso ifnot rs' m', + exec_instrs sp b rs m (Bcond cond args ifso ifnot) rs' m' -> + eval_condition cond (reglist args rs') = Some true -> + exec_block sp b rs m (Cont ifso) rs' m' + | exec_Bcond_false: + forall sp b rs m cond args ifso ifnot rs' m', + exec_instrs sp b rs m (Bcond cond args ifso ifnot) rs' m' -> + eval_condition cond (reglist args rs') = Some false -> + exec_block sp b rs m (Cont ifnot) rs' m' + | exec_Breturn: + forall sp b rs m rs' m', + exec_instrs sp b rs m Breturn rs' m' -> + exec_block sp b rs m Return rs' m' + +with exec_blocks: code -> val -> + node -> locset -> mem -> + outcome -> locset -> mem -> Prop := + | exec_blocks_refl: + forall c sp pc rs m, + exec_blocks c sp pc rs m (Cont pc) rs m + | exec_blocks_one: + forall c sp pc b m rs out rs' m', + c!pc = Some b -> + exec_block sp b rs m out rs' m' -> + exec_blocks c sp pc rs m out rs' m' + | exec_blocks_trans: + forall c sp pc1 rs1 m1 pc2 rs2 m2 out rs3 m3, + exec_blocks c sp pc1 rs1 m1 (Cont pc2) rs2 m2 -> + exec_blocks c sp pc2 rs2 m2 out rs3 m3 -> + exec_blocks c sp pc1 rs1 m1 out rs3 m3 + +with exec_function: function -> locset -> mem -> + locset -> mem -> Prop := + | exec_funct: + forall f rs m m1 stk rs2 m2, + alloc m 0 f.(fn_stacksize) = (m1, stk) -> + exec_blocks f.(fn_code) (Vptr stk Int.zero) + f.(fn_entrypoint) (call_regs rs) m1 Return rs2 m2 -> + exec_function f rs m rs2 (free m2 stk). + +End RELSEM. + +(** Execution of a whole program boils down to invoking its main + function. The result of the program is the return value of the + main function, to be found in the machine register dictated + by the calling conventions. *) + +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 (Locmap.init Vundef) m0 rs m /\ + rs (R (Conventions.loc_result f.(fn_sig))) = r. + +(** We remark that the [exec_blocks] relation is stable if + the control-flow graph is extended by adding new basic blocks + at previously unused graph nodes. *) + +Section EXEC_BLOCKS_EXTENDS. + +Variable ge: genv. +Variable c1 c2: code. +Hypothesis EXT: forall pc, c2!pc = c1!pc \/ c1!pc = None. + +Lemma exec_blocks_extends: + forall sp pc1 rs1 m1 out rs2 m2, + exec_blocks ge c1 sp pc1 rs1 m1 out rs2 m2 -> + exec_blocks ge c2 sp pc1 rs1 m1 out rs2 m2. +Proof. + induction 1. + apply exec_blocks_refl. + apply exec_blocks_one with b. + elim (EXT pc); intro; congruence. assumption. + eapply exec_blocks_trans; eauto. +Qed. + +End EXEC_BLOCKS_EXTENDS. + +(** * Operations over LTL *) + +(** Computation of the possible successors of a basic block. + This is used for dataflow analyses. *) + +Fixpoint successors_aux (b: block) : list node := + match b with + | Bgetstack s r b => successors_aux b + | Bsetstack r s b => successors_aux b + | Bop op args res b => successors_aux b + | Bload chunk addr args dst b => successors_aux b + | Bstore chunk addr args src b => successors_aux b + | Bcall sig ros b => successors_aux b + | Bgoto n => n :: nil + | Bcond cond args ifso ifnot => ifso :: ifnot :: nil + | Breturn => nil + end. + +Definition successors (f: function) (pc: node) : list node := + match f.(fn_code)!pc with + | None => nil + | Some b => successors_aux b + end. + +Lemma successors_aux_invariant: + forall ge sp b rs m b' rs' m', + exec_instrs ge sp b rs m b' rs' m' -> + successors_aux b = successors_aux b'. +Proof. + induction 1; simpl; intros. + reflexivity. + inversion H; reflexivity. + transitivity (successors_aux b2); auto. +Qed. + +Lemma successors_correct: + forall ge f sp pc rs m pc' rs' m' b, + f.(fn_code)!pc = Some b -> + exec_block ge sp b rs m (Cont pc') rs' m' -> + In pc' (successors f pc). +Proof. + intros. unfold successors. rewrite H. inversion H0. + rewrite (successors_aux_invariant _ _ _ _ _ _ _ _ H6); simpl. + tauto. + rewrite (successors_aux_invariant _ _ _ _ _ _ _ _ H2); simpl. + tauto. + rewrite (successors_aux_invariant _ _ _ _ _ _ _ _ H2); simpl. + tauto. +Qed. -- cgit