diff options
Diffstat (limited to 'backend/RTLbigstep.v')
| -rw-r--r-- | backend/RTLbigstep.v | 400 |
1 files changed, 400 insertions, 0 deletions
diff --git a/backend/RTLbigstep.v b/backend/RTLbigstep.v new file mode 100644 index 0000000..0ad6e68 --- /dev/null +++ b/backend/RTLbigstep.v @@ -0,0 +1,400 @@ +(** An alternate, mixed-step semantics for the RTL intermediate language. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Events. +Require Import Mem. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Op. +Require Import Registers. +Require Import RTL. + +Section BIGSTEP. + +Variable ge: genv. + +(** 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 -> trace -> + 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 E0 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 m = Some v -> + exec_instr c sp pc rs m E0 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 E0 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 E0 pc' rs m' + | exec_Icall: + forall c sp pc rs m sig ros args res pc' f vres m' t, + c!pc = Some(Icall sig ros args res pc') -> + find_function ge ros rs = Some f -> + funsig f = sig -> + exec_function f rs##args m t vres m' -> + exec_instr c sp pc rs m t pc' (rs#res <- vres) m' + | exec_Ialloc: + forall c sp pc rs m pc' arg res sz m' b, + c!pc = Some(Ialloc arg res pc') -> + rs#arg = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', b) -> + exec_instr c sp pc rs m E0 pc' (rs#res <- (Vptr b Int.zero)) 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 m = Some true -> + exec_instr c sp pc rs m E0 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 m = Some false -> + exec_instr c sp pc rs m E0 ifnot rs m + +(** [exec_body ge c sp pc rs m res m'] repeatedly executes + instructions starting at [pc] in [c], until it + reaches a return or tailcall instruction. It performs + that instruction and sets [res] to the return value + and [m'] to the final memory state. *) + +with exec_body: code -> val -> + node -> regset -> mem -> trace -> + val -> mem -> Prop := + | exec_body_step: forall c sp pc rs m t1 pc1 rs1 m1 t2 t res m2, + exec_instr c sp pc rs m t1 pc1 rs1 m1 -> + exec_body c sp pc1 rs1 m1 t2 res m2 -> + t = t1 ** t2 -> + exec_body c sp pc rs m t res m2 + | exec_Ireturn: forall c stk pc rs m or res, + c!pc = Some(Ireturn or) -> + res = regmap_optget or Vundef rs -> + exec_body c (Vptr stk Int.zero) pc rs m E0 res (Mem.free m stk) + | exec_Itailcall: forall c stk pc rs m sig ros args f t res m', + c!pc = Some(Itailcall sig ros args) -> + find_function ge ros rs = Some f -> + funsig f = sig -> + exec_function f rs##args (Mem.free m stk) t res m' -> + exec_body c (Vptr stk Int.zero) pc rs m t res m' + +(** [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: fundef -> list val -> mem -> trace -> + val -> mem -> Prop := + | exec_funct_internal: + forall f m m1 stk args t m2 vres, + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + exec_body f.(fn_code) (Vptr stk Int.zero) + f.(fn_entrypoint) (init_regs args f.(fn_params)) m1 + t vres m2 -> + exec_function (Internal f) args m t vres m2 + | exec_funct_external: + forall ef args m t res, + event_match ef args t res -> + exec_function (External ef) args m t res m. + +Scheme exec_instr_ind_3 := Minimality for exec_instr Sort Prop + with exec_body_ind_3 := Minimality for exec_body Sort Prop + with exec_function_ind_3 := Minimality for exec_function Sort Prop. + +(** The reflexive transitive closure of [exec_instr]. *) + +Inductive exec_instrs: code -> val -> + node -> regset -> mem -> trace -> + node -> regset -> mem -> Prop := + | exec_refl: + forall c sp pc rs m, + exec_instrs c sp pc rs m E0 pc rs m + | exec_one: + forall c sp pc rs m t pc' rs' m', + exec_instr c sp pc rs m t pc' rs' m' -> + exec_instrs c sp pc rs m t pc' rs' m' + | exec_trans: + forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3, + exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> + exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> + t3 = t1 ** t2 -> + exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3. + +(** Some derived execution rules. *) + +Lemma exec_instrs_exec_body: + forall c sp pc1 rs1 m1 t1 pc2 rs2 m2, + exec_instrs c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> + forall res t2 m3 t3, + exec_body c sp pc2 rs2 m2 t2 res m3 -> + t3 = t1 ** t2 -> + exec_body c sp pc1 rs1 m1 t3 res m3. +Proof. + induction 1; intros. + subst t3. rewrite E0_left. auto. + eapply exec_body_step; eauto. + eapply IHexec_instrs1. eapply IHexec_instrs2. eauto. + eauto. traceEq. +Qed. + +Lemma exec_step: + forall c sp pc1 rs1 m1 t1 pc2 rs2 m2 t2 pc3 rs3 m3 t3, + exec_instr c sp pc1 rs1 m1 t1 pc2 rs2 m2 -> + exec_instrs c sp pc2 rs2 m2 t2 pc3 rs3 m3 -> + t3 = t1 ** t2 -> + exec_instrs c sp pc1 rs1 m1 t3 pc3 rs3 m3. +Proof. + intros. eapply exec_trans. apply exec_one. eauto. eauto. auto. +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 m = Some v -> + rs' = (rs#res <- v) -> + exec_instr c sp pc rs m E0 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 E0 pc' rs' m. +Proof. + intros. subst rs'. eapply exec_Iload; eauto. +Qed. + +(** Experimental: coinductive big-step semantics for divergence. *) + +CoInductive diverge_body: + code -> val -> node -> regset -> mem -> traceinf -> Prop := + | diverge_step: forall c sp pc rs m t1 pc1 rs1 m1 T2 T, + exec_instr c sp pc rs m t1 pc1 rs1 m1 -> + diverge_body c sp pc1 rs1 m1 T2 -> + T = t1 *** T2 -> + diverge_body c sp pc rs m T + | diverge_Icall: + forall c sp pc rs m sig ros args res pc' f T, + c!pc = Some(Icall sig ros args res pc') -> + find_function ge ros rs = Some f -> + funsig f = sig -> + diverge_function f rs##args m T -> + diverge_body c sp pc rs m T + | diverge_Itailcall: forall c stk pc rs m sig ros args f T, + c!pc = Some(Itailcall sig ros args) -> + find_function ge ros rs = Some f -> + funsig f = sig -> + diverge_function f rs##args (Mem.free m stk) T -> + diverge_body c (Vptr stk Int.zero) pc rs m T + +with diverge_function: fundef -> list val -> mem -> traceinf -> Prop := + | diverge_funct_internal: + forall f m m1 stk args T, + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + diverge_body f.(fn_code) (Vptr stk Int.zero) + f.(fn_entrypoint) (init_regs args f.(fn_params)) m1 + T -> + diverge_function (Internal f) args m T. + +End BIGSTEP. + +(** Execution of whole programs. *) + +Inductive exec_program (p: program): program_behavior -> Prop := + | exec_program_terminates: forall b f t r m, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = mksignature nil (Some Tint) -> + exec_function ge f nil m0 t (Vint r) m -> + exec_program p (Terminates t r) + | exec_program_diverges: forall b f T, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = mksignature nil (Some Tint) -> + diverge_function ge f nil m0 T -> + exec_program p (Diverges T). + +(** * Equivalence with the transition semantics. *) + +Section EQUIVALENCE. + +Variable ge: genv. + +Definition exec_instr_prop + (c: code) (sp: val) (pc1: node) (rs1: regset) (m1: mem) + (t: trace) (pc2: node) (rs2: regset) (m2: mem) : Prop := + forall s, + plus step ge (State s c sp pc1 rs1 m1) + t (State s c sp pc2 rs2 m2). + +Definition exec_body_prop + (c: code) (sp: val) (pc1: node) (rs1: regset) (m1: mem) + (t: trace) (res: val) (m2: mem) : Prop := + forall s, + plus step ge (State s c sp pc1 rs1 m1) + t (Returnstate s res m2). + +Definition exec_function_prop + (f: fundef) (args: list val) (m1: mem) + (t: trace) (res: val) (m2: mem) : Prop := + forall s, + plus step ge (Callstate s f args m1) + t (Returnstate s res m2). + +Lemma exec_steps: + (forall c sp pc1 rs1 m1 t pc2 rs2 m2, + exec_instr ge c sp pc1 rs1 m1 t pc2 rs2 m2 -> + exec_instr_prop c sp pc1 rs1 m1 t pc2 rs2 m2) /\ + (forall c sp pc1 rs1 m1 t res m2, + exec_body ge c sp pc1 rs1 m1 t res m2 -> + exec_body_prop c sp pc1 rs1 m1 t res m2) /\ + (forall f args m1 t res m2, + exec_function ge f args m1 t res m2 -> + exec_function_prop f args m1 t res m2). +Proof. + set (IND := fun a b c d e f g h i j k l m => + conj (exec_instr_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m) + (conj (exec_body_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m) + (exec_function_ind_3 ge exec_instr_prop exec_body_prop exec_function_prop a b c d e f g h i j k l m))). + apply IND; clear IND; + intros; red; intros. + (* nop *) + apply plus_one. eapply RTL.exec_Inop; eauto. + (* op *) + apply plus_one. eapply RTL.exec_Iop'; eauto. + (* load *) + apply plus_one. eapply RTL.exec_Iload'; eauto. + (* store *) + apply plus_one. eapply RTL.exec_Istore; eauto. + (* call *) + eapply plus_left'. eapply RTL.exec_Icall; eauto. + eapply plus_right'. apply H3. apply RTL.exec_return. + eauto. traceEq. + (* alloc *) + apply plus_one. eapply RTL.exec_Ialloc; eauto. + (* cond true *) + apply plus_one. eapply RTL.exec_Icond_true; eauto. + (* cond false *) + apply plus_one. eapply RTL.exec_Icond_false; eauto. + (* body step *) + eapply plus_trans. apply H0. apply H2. auto. + (* body return *) + apply plus_one. rewrite H0. eapply RTL.exec_Ireturn; eauto. + (* body tailcall *) + eapply plus_left'. eapply RTL.exec_Itailcall; eauto. + apply H3. traceEq. + (* internal function *) + eapply plus_left'. eapply RTL.exec_function_internal; eauto. + apply H1. traceEq. + (* external function *) + apply plus_one. eapply RTL.exec_function_external; eauto. +Qed. + +Lemma diverge_function_steps: + forall fd args m T s, + diverge_function ge fd args m T -> + forever step ge (Callstate s fd args m) T. +Proof. + assert (diverge_function_steps': + forall fd args m T s, + diverge_function ge fd args m T -> + forever_N step ge O (Callstate s fd args m) T). + cofix COINDHYP1. + assert (diverge_body_steps: forall c sp pc rs m T s, + diverge_body ge c sp pc rs m T -> + forever_N step ge O (State s c sp pc rs m) T). + cofix COINDHYP2; intros. + inv H. + (* step *) + apply forever_N_plus with (State s c sp pc1 rs1 m1) O. + destruct exec_steps as [E [F G]]. + apply E. assumption. + apply COINDHYP2. assumption. + (* call *) + change T with (E0 *** T). + apply forever_N_plus with (Callstate (Stackframe res c sp pc' rs :: s) + f rs##args m) O. + apply plus_one. eapply RTL.exec_Icall; eauto. + apply COINDHYP1. assumption. + (* tailcall *) + change T with (E0 *** T). + apply forever_N_plus with (Callstate s f rs##args (free m stk)) O. + apply plus_one. eapply RTL.exec_Itailcall; eauto. + apply COINDHYP1. assumption. + (* internal function *) + intros. inv H. + change T with (E0 *** T). + apply forever_N_plus with + (State s f.(fn_code) (Vptr stk Int.zero) + f.(fn_entrypoint) (init_regs args f.(fn_params)) m1) O. + apply plus_one. eapply RTL.exec_function_internal; eauto. + apply diverge_body_steps. assumption. + (* conclusion *) + intros. eapply forever_N_forever. eauto. +Qed. + +End EQUIVALENCE. + +Theorem exec_program_bigstep_smallstep: + forall p beh, + exec_program p beh -> + RTL.exec_program p beh. +Proof. + intros. unfold RTL.exec_program. inv H. + econstructor. + econstructor; eauto. + apply plus_star. + destruct (exec_steps (Genv.globalenv p)) as [E [F G]]. + apply (G _ _ _ _ _ _ H3). + constructor. + econstructor. + econstructor; eauto. + apply diverge_function_steps. auto. +Qed. + |