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/RTL.v | 349 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 349 insertions(+) create mode 100644 backend/RTL.v (limited to 'backend/RTL.v') diff --git a/backend/RTL.v b/backend/RTL.v new file mode 100644 index 0000000..ac9a415 --- /dev/null +++ b/backend/RTL.v @@ -0,0 +1,349 @@ +(** The RTL intermediate language: abstract syntax and semantics. + + RTL (``Register Transfer Language'' is the first intermediate language + after Cminor. +*) + +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 Registers. + +(** * Abstract syntax *) + +(** RTL is organized as instructions, functions and programs. + Instructions correspond roughly to elementary instructions of the + target processor, but take their arguments and leave their results + in pseudo-registers (also called temporaries in textbooks). + Infinitely many pseudo-registers are available, and each function + has its own set of pseudo-registers, unaffected by function calls. + + Instructions are organized as a control-flow graph: a function is + a finite map from ``nodes'' (abstract program points) to instructions, + and each instruction lists explicitly the nodes of its successors. +*) + +Definition node := positive. + +Inductive instruction: Set := + | Inop: node -> instruction + (** No operation -- just branch to the successor. *) + | Iop: operation -> list reg -> reg -> node -> instruction + (** [Iop op args dest succ] performs the arithmetic operation [op] + over the values of registers [args], stores the result in [dest], + and branches to [succ]. *) + | Iload: memory_chunk -> addressing -> list reg -> reg -> node -> instruction + (** [Iload chunk addr args dest succ] loads a [chunk] quantity from + the address determined by the addressing mode [addr] and the + values of the [args] registers, stores the quantity just read + into [dest], and branches to [succ]. *) + | Istore: memory_chunk -> addressing -> list reg -> reg -> node -> instruction + (** [Istore chunk addr args src succ] stores the value of register + [src] in the [chunk] quantity at the + the address determined by the addressing mode [addr] and the + values of the [args] registers, then branches to [succ]. *) + | Icall: signature -> reg + ident -> list reg -> reg -> node -> instruction + (** [Icall sig fn args dest succ] invokes the function determined by + [fn] (either a function pointer found in a register or a + function name), giving it the values of registers [args] + as arguments. It stores the return value in [dest] and branches + to [succ]. *) + | Icond: condition -> list reg -> node -> node -> instruction + (** [Icond cond args ifso ifnot] evaluates the boolean condition + [cond] over the values of registers [args]. If the condition + is true, it transitions to [ifso]. If the condition is false, + it transitions to [ifnot]. *) + | Ireturn: option reg -> instruction. + (** [Ireturn] terminates the execution of the current function + (it has no successor). It returns the value of the given + register, or [Vundef] if none is given. *) + +Definition code: Set := PTree.t instruction. + +Record function: Set := mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node; + fn_nextpc: node; + fn_code_wf: forall (pc: node), Plt pc fn_nextpc \/ fn_code!pc = None +}. + +(** A function description comprises a control-flow graph (CFG) [fn_code] + (a partial finite mapping from nodes to instructions). As in Cminor, + [fn_sig] is the function signature and [fn_stacksize] the number of bytes + for its stack-allocated activation record. [fn_params] is the list + of registers that are bound to the values of arguments at call time. + [fn_entrypoint] is the node of the first instruction of the function + in the CFG. [fn_code_wf] asserts that all instructions of the function + have nodes no greater than [fn_nextpc]. *) + +Definition program := AST.program function. + +(** * Operational semantics *) + +Definition genv := Genv.t function. +Definition regset := Regmap.t val. + +Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := + match rl, vl with + | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) + | _, _ => Regmap.init Vundef + end. + +Section RELSEM. + +Variable ge: genv. + +Definition find_function (ros: reg + ident) (rs: regset) : option function := + match ros with + | inl r => Genv.find_funct ge rs#r + | inr symb => + match Genv.find_symbol ge symb with + | None => None + | Some b => Genv.find_funct_ptr ge b + end + end. + +(** The dynamic semantics of RTL is a combination of small-step (transition) + semantics and big-step semantics. Execution of an instruction performs + a single transition to the next instruction (small-step), except if + the instruction is a function call. In this case, the whole body of + the called function is executed at once and the transition terminates + on the instruction immediately following the call in the caller function. + Such ``mixed-step'' semantics is convenient for reasoning over + intra-procedural analyses and transformations. It also dispenses us + from making the call stack explicit in the semantics. + + The semantics is organized in three mutually inductive predicates. + The first is [exec_instr ge c sp pc rs m pc' rs' m']. [ge] is the + global environment (see module [Genv]), [c] the CFG for the current + function, and [sp] the pointer to the stack block for its + current activation (as in Cminor). [pc], [rs] and [m] is the + initial state of the transition: program point (CFG node) [pc], + register state (mapping of pseudo-registers to values) [rs], + and memory state [m]. The final state is [pc'], [rs'] and [m']. *) + +Inductive exec_instr: code -> val -> + node -> regset -> mem -> + node -> regset -> mem -> Prop := + | exec_Inop: + forall c sp pc rs m pc', + c!pc = Some(Inop pc') -> + exec_instr c sp pc rs m pc' rs m + | exec_Iop: + forall c sp pc rs m op args res pc' v, + c!pc = Some(Iop op args res pc') -> + eval_operation ge sp op rs##args = Some v -> + exec_instr c sp pc rs m pc' (rs#res <- v) m + | exec_Iload: + forall c sp pc rs m chunk addr args dst pc' a v, + c!pc = Some(Iload chunk addr args dst pc') -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + exec_instr c sp pc rs m pc' (rs#dst <- v) m + | exec_Istore: + forall c sp pc rs m chunk addr args src pc' a m', + c!pc = Some(Istore chunk addr args src pc') -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + exec_instr c sp pc rs m pc' rs m' + | exec_Icall: + forall c sp pc rs m sig ros args res pc' f vres m', + c!pc = Some(Icall sig ros args res pc') -> + find_function ros rs = Some f -> + sig = f.(fn_sig) -> + exec_function f rs##args m vres m' -> + exec_instr c sp pc rs m pc' (rs#res <- vres) m' + | exec_Icond_true: + forall c sp pc rs m cond args ifso ifnot, + c!pc = Some(Icond cond args ifso ifnot) -> + eval_condition cond rs##args = Some true -> + exec_instr c sp pc rs m ifso rs m + | exec_Icond_false: + forall c sp pc rs m cond args ifso ifnot, + c!pc = Some(Icond cond args ifso ifnot) -> + eval_condition cond rs##args = Some false -> + exec_instr c sp pc rs m ifnot rs m + +(** [exec_instrs ge c sp pc rs m pc' rs' m'] is the reflexive + transitive closure of [exec_instr]. It corresponds to the execution + of zero, one or finitely many transitions. *) + +with exec_instrs: code -> val -> + node -> regset -> mem -> + node -> regset -> mem -> Prop := + | exec_refl: + forall c sp pc rs m, + exec_instrs c sp pc rs m pc rs m + | exec_one: + forall c sp pc rs m pc' rs' m', + exec_instr c sp pc rs m pc' rs' m' -> + exec_instrs c sp pc rs m pc' rs' m' + | exec_trans: + forall c sp pc1 rs1 m1 pc2 rs2 m2 pc3 rs3 m3, + exec_instrs c sp pc1 rs1 m1 pc2 rs2 m2 -> + exec_instrs c sp pc2 rs2 m2 pc3 rs3 m3 -> + exec_instrs c sp pc1 rs1 m1 pc3 rs3 m3 + +(** [exec_function ge f args m res m'] executes a function application. + [f] is the called function, [args] the values of its arguments, + and [m] the memory state at the beginning of the call. [res] is + the returned value: the value of [r] if the function terminates with + a [Ireturn (Some r)], or [Vundef] if it terminates with [Ireturn None]. + Evaluation proceeds by executing transitions from the function's entry + point to the first [Ireturn] instruction encountered. It is preceeded + by the allocation of the stack activation block and the binding + of register parameters to the provided arguments. + (Non-parameter registers are initialized to [Vundef].) Before returning, + the stack activation block is freed. *) + +with exec_function: function -> list val -> mem -> + val -> mem -> Prop := + | exec_funct: + forall f m m1 stk args pc rs m2 or vres, + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + exec_instrs f.(fn_code) (Vptr stk Int.zero) + f.(fn_entrypoint) (init_regs args f.(fn_params)) m1 + pc rs m2 -> + f.(fn_code)!pc = Some(Ireturn or) -> + vres = regmap_optget or Vundef rs -> + exec_function f args m vres (Mem.free m2 stk). + +Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop + with exec_instrs_ind_3 := Minimality for exec_instrs Sort Prop + with exec_function_ind_3 := Minimality for exec_function Sort Prop. + +(** Some derived execution rules. *) + +Lemma exec_step: + forall c sp pc1 rs1 m1 pc2 rs2 m2 pc3 rs3 m3, + exec_instr c sp pc1 rs1 m1 pc2 rs2 m2 -> + exec_instrs c sp pc2 rs2 m2 pc3 rs3 m3 -> + exec_instrs c sp pc1 rs1 m1 pc3 rs3 m3. +Proof. + intros. eapply exec_trans. apply exec_one. eauto. eauto. +Qed. + +Lemma exec_Iop': + forall c sp pc rs m op args res pc' rs' v, + c!pc = Some(Iop op args res pc') -> + eval_operation ge sp op rs##args = Some v -> + rs' = (rs#res <- v) -> + exec_instr c sp pc rs m pc' rs' m. +Proof. + intros. subst rs'. eapply exec_Iop; eauto. +Qed. + +Lemma exec_Iload': + forall c sp pc rs m chunk addr args dst pc' rs' a v, + c!pc = Some(Iload chunk addr args dst pc') -> + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + rs' = (rs#dst <- v) -> + exec_instr c sp pc rs m pc' rs' m. +Proof. + intros. subst rs'. eapply exec_Iload; eauto. +Qed. + +(** If a transition can take place from [pc], the instruction at [pc] + is defined in the CFG. *) + +Lemma exec_instr_present: + forall c sp pc rs m pc' rs' m', + exec_instr c sp pc rs m pc' rs' m' -> + c!pc <> None. +Proof. + induction 1; congruence. +Qed. + +Lemma exec_instrs_present: + forall c sp pc rs m pc' rs' m', + exec_instrs c sp pc rs m pc' rs' m' -> + c!pc' <> None -> c!pc <> None. +Proof. + induction 1; intros. + auto. + eapply exec_instr_present; eauto. + eauto. +Qed. + +End RELSEM. + +(** Execution of whole programs. As in Cminor, we call the ``main'' function + with no arguments and observe its return value. *) + +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 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 nil m0 r m. + +(** * Operations on RTL abstract syntax *) + +(** Computation of the possible successors of an instruction. + This is used in particular for dataflow analyses. *) + +Definition successors (f: function) (pc: node) : list node := + match f.(fn_code)!pc with + | None => nil + | Some i => + match i with + | Inop s => s :: nil + | Iop op args res s => s :: nil + | Iload chunk addr args dst s => s :: nil + | Istore chunk addr args src s => s :: nil + | Icall sig ros args res s => s :: nil + | Icond cond args ifso ifnot => ifso :: ifnot :: nil + | Ireturn optarg => nil + end + end. + +Lemma successors_correct: + forall ge f sp pc rs m pc' rs' m', + exec_instr ge f.(fn_code) sp pc rs m pc' rs' m' -> + In pc' (successors f pc). +Proof. + intros ge f. unfold successors. generalize (fn_code f). + induction 1; rewrite H; simpl; tauto. +Qed. + +(** Transformation of a RTL function instruction by instruction. + This applies a given transformation function to all instructions + of a function and constructs a transformed function from that. *) + +Section TRANSF. + +Variable transf: node -> instruction -> instruction. + +Lemma transf_code_wf: + forall (c: code) (nextpc: node), + (forall (pc: node), Plt pc nextpc \/ c!pc = None) -> + (forall (pc: node), Plt pc nextpc \/ (PTree.map transf c)!pc = None). +Proof. + intros. elim (H pc); intro. + left; assumption. + right. rewrite PTree.gmap. rewrite H0. reflexivity. +Qed. + +Definition transf_function (f: function) : function := + mkfunction + f.(fn_sig) + f.(fn_params) + f.(fn_stacksize) + (PTree.map transf f.(fn_code)) + f.(fn_entrypoint) + f.(fn_nextpc) + (transf_code_wf f.(fn_code) f.(fn_nextpc) f.(fn_code_wf)). + +End TRANSF. -- cgit v1.2.3