Module Cminor


Abstract syntax and semantics for the Cminor language.

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Events.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Switch.

Abstract syntax


Cminor is a low-level imperative language structured in expressions, statements, functions and programs. We first define the constants and operators that occur within expressions.

Inductive constant : Type :=
  | Ointconst: int -> constant (* integer constant *)
  | Ofloatconst: float -> constant (* double-precision floating-point constant *)
  | Osingleconst: float32 -> constant (* single-precision floating-point constant *)
  | Olongconst: int64 -> constant (* long integer constant *)
  | Oaddrsymbol: ident -> ptrofs -> constant (* address of the symbol plus the offset *)
  | Oaddrstack: ptrofs -> constant. (* stack pointer plus the given offset *)

Inductive unary_operation : Type :=
  | Ocast8unsigned: unary_operation (* 8-bit zero extension *)
  | Ocast8signed: unary_operation (* 8-bit sign extension *)
  | Ocast16unsigned: unary_operation (* 16-bit zero extension *)
  | Ocast16signed: unary_operation (* 16-bit sign extension *)
  | Onegint: unary_operation (* integer opposite *)
  | Onotint: unary_operation (* bitwise complement *)
  | Onegf: unary_operation (* float64 opposite *)
  | Oabsf: unary_operation (* float64 absolute value *)
  | Onegfs: unary_operation (* float32 opposite *)
  | Oabsfs: unary_operation (* float32 absolute value *)
  | Osingleoffloat: unary_operation (* float truncation to float32 *)
  | Ofloatofsingle: unary_operation (* float extension to float64 *)
  | Ointoffloat: unary_operation (* signed integer to float64 *)
  | Ointuoffloat: unary_operation (* unsigned integer to float64 *)
  | Ofloatofint: unary_operation (* float64 to signed integer *)
  | Ofloatofintu: unary_operation (* float64 to unsigned integer *)
  | Ointofsingle: unary_operation (* signed integer to float32 *)
  | Ointuofsingle: unary_operation (* unsigned integer to float32 *)
  | Osingleofint: unary_operation (* float32 to signed integer *)
  | Osingleofintu: unary_operation (* float32 to unsigned integer *)
  | Onegl: unary_operation (* long integer opposite *)
  | Onotl: unary_operation (* long bitwise complement *)
  | Ointoflong: unary_operation (* long to int *)
  | Olongofint: unary_operation (* signed int to long *)
  | Olongofintu: unary_operation (* unsigned int to long *)
  | Olongoffloat: unary_operation (* float64 to signed long *)
  | Olonguoffloat: unary_operation (* float64 to unsigned long *)
  | Ofloatoflong: unary_operation (* signed long to float64 *)
  | Ofloatoflongu: unary_operation (* unsigned long to float64 *)
  | Olongofsingle: unary_operation (* float32 to signed long *)
  | Olonguofsingle: unary_operation (* float32 to unsigned long *)
  | Osingleoflong: unary_operation (* signed long to float32 *)
  | Osingleoflongu: unary_operation. (* unsigned long to float32 *)

Inductive binary_operation : Type :=
  | Oadd: binary_operation (* integer addition *)
  | Osub: binary_operation (* integer subtraction *)
  | Omul: binary_operation (* integer multiplication *)
  | Odiv: binary_operation (* integer signed division *)
  | Odivu: binary_operation (* integer unsigned division *)
  | Omod: binary_operation (* integer signed modulus *)
  | Omodu: binary_operation (* integer unsigned modulus *)
  | Oand: binary_operation (* integer bitwise ``and'' *)
  | Oor: binary_operation (* integer bitwise ``or'' *)
  | Oxor: binary_operation (* integer bitwise ``xor'' *)
  | Oshl: binary_operation (* integer left shift *)
  | Oshr: binary_operation (* integer right signed shift *)
  | Oshru: binary_operation (* integer right unsigned shift *)
  | Oaddf: binary_operation (* float64 addition *)
  | Osubf: binary_operation (* float64 subtraction *)
  | Omulf: binary_operation (* float64 multiplication *)
  | Odivf: binary_operation (* float64 division *)
  | Oaddfs: binary_operation (* float32 addition *)
  | Osubfs: binary_operation (* float32 subtraction *)
  | Omulfs: binary_operation (* float32 multiplication *)
  | Odivfs: binary_operation (* float32 division *)
  | Oaddl: binary_operation (* long addition *)
  | Osubl: binary_operation (* long subtraction *)
  | Omull: binary_operation (* long multiplication *)
  | Odivl: binary_operation (* long signed division *)
  | Odivlu: binary_operation (* long unsigned division *)
  | Omodl: binary_operation (* long signed modulus *)
  | Omodlu: binary_operation (* long unsigned modulus *)
  | Oandl: binary_operation (* long bitwise ``and'' *)
  | Oorl: binary_operation (* long bitwise ``or'' *)
  | Oxorl: binary_operation (* long bitwise ``xor'' *)
  | Oshll: binary_operation (* long left shift *)
  | Oshrl: binary_operation (* long right signed shift *)
  | Oshrlu: binary_operation (* long right unsigned shift *)
  | Ocmp: comparison -> binary_operation (* integer signed comparison *)
  | Ocmpu: comparison -> binary_operation (* integer unsigned comparison *)
  | Ocmpf: comparison -> binary_operation (* float64 comparison *)
  | Ocmpfs: comparison -> binary_operation (* float32 comparison *)
  | Ocmpl: comparison -> binary_operation (* long signed comparison *)
  | Ocmplu: comparison -> binary_operation. (* long unsigned comparison *)

Expressions include reading local variables, constants, arithmetic operations, and memory loads.

Inductive expr : Type :=
  | Evar : ident -> expr
  | Econst : constant -> expr
  | Eunop : unary_operation -> expr -> expr
  | Ebinop : binary_operation -> expr -> expr -> expr
  | Eload : memory_chunk -> expr -> expr.

Statements include expression evaluation, assignment to local variables, memory stores, function calls, an if/then/else conditional, infinite loops, blocks and early block exits, and early function returns. Sexit n terminates prematurely the execution of the n+1 enclosing Sblock statements.

Definition label := ident.

Inductive stmt : Type :=
  | Sskip: stmt
  | Sassign : ident -> expr -> stmt
  | Sstore : memory_chunk -> expr -> expr -> stmt
  | Scall : option ident -> signature -> expr -> list expr -> stmt
  | Stailcall: signature -> expr -> list expr -> stmt
  | Sbuiltin : option ident -> external_function -> list expr -> stmt
  | Sseq: stmt -> stmt -> stmt
  | Sifthenelse: expr -> stmt -> stmt -> stmt
  | Sloop: stmt -> stmt
  | Sblock: stmt -> stmt
  | Sexit: nat -> stmt
  | Sswitch: bool -> expr -> list (Z * nat) -> nat -> stmt
  | Sreturn: option expr -> stmt
  | Slabel: label -> stmt -> stmt
  | Sgoto: label -> stmt.

Functions are composed of a signature, a list of parameter names, a list of local variables, and a statement representing the function body. Each function can allocate a memory block of size fn_stackspace on entrance. This block will be deallocated automatically before the function returns. Pointers into this block can be taken with the Oaddrstack operator.

Record function : Type := mkfunction {
  fn_sig: signature;
  fn_params: list ident;
  fn_vars: list ident;
  fn_stackspace: Z;
  fn_body: stmt
}.

Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.

Definition funsig (fd: fundef) :=
  match fd with
  | Internal f => fn_sig f
  | External ef => ef_sig ef
  end.

Operational semantics (small-step)


Two kinds of evaluation environments are involved:

Definition genv := Genv.t fundef unit.
Definition env := PTree.t val.

The following functions build the initial local environment at function entry, binding parameters to the provided arguments and initializing local variables to Vundef.

Fixpoint set_params (vl: list val) (il: list ident) {struct il} : env :=
  match il, vl with
  | i1 :: is, v1 :: vs => PTree.set i1 v1 (set_params vs is)
  | i1 :: is, nil => PTree.set i1 Vundef (set_params nil is)
  | _, _ => PTree.empty val
  end.

Fixpoint set_locals (il: list ident) (e: env) {struct il} : env :=
  match il with
  | nil => e
  | i1 :: is => PTree.set i1 Vundef (set_locals is e)
  end.

Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=
  match optid with
  | None => e
  | Some id => PTree.set id v e
  end.

Continuations

Inductive cont: Type :=
  | Kstop: cont (* stop program execution *)
  | Kseq: stmt -> cont -> cont (* execute stmt, then cont *)
  | Kblock: cont -> cont (* exit a block, then do cont *)
  | Kcall: option ident -> function -> val -> env -> cont -> cont.

States

Inductive state `{memory_model_ops: Mem.MemoryModelOps}: Type :=
  | State: (* Execution within a function *)
      forall (f: function) (* currently executing function *)
             (s: stmt) (* statement under consideration *)
             (k: cont) (* its continuation -- what to do next *)
             (sp: val) (* current stack pointer *)
             (e: env) (* current local environment *)
             (m: mem), (* current memory state *)
      state
  | Callstate: (* Invocation of a function *)
      forall (f: fundef) (* function to invoke *)
             (args: list val) (* arguments provided by caller *)
             (k: cont) (* what to do next *)
             (m: mem) (sz: Z), (* memory state *)
      state
  | Returnstate: (* Return from a function *)
      forall (v: val) (* Return value *)
             (k: cont) (* what to do next *)
             (m: mem), (* memory state *)
      state.

Section WITHEXTCALLS.
Context `{external_calls_prf: ExternalCalls}.

Variable fn_stack_requirements : ident -> Z.

Section RELSEM.

Variable ge: genv.

Evaluation of constants and operator applications. None is returned when the computation is undefined, e.g. if arguments are of the wrong types, or in case of an integer division by zero.

Definition eval_constant (sp: val) (cst: constant) : option val :=
  match cst with
  | Ointconst n => Some (Vint n)
  | Ofloatconst n => Some (Vfloat n)
  | Osingleconst n => Some (Vsingle n)
  | Olongconst n => Some (Vlong n)
  | Oaddrsymbol s ofs => Some (Genv.symbol_address ge s ofs)
  | Oaddrstack ofs => Some (Val.offset_ptr sp ofs)
  end.

Definition eval_unop (op: unary_operation) (arg: val) : option val :=
  match op with
  | Ocast8unsigned => Some (Val.zero_ext 8 arg)
  | Ocast8signed => Some (Val.sign_ext 8 arg)
  | Ocast16unsigned => Some (Val.zero_ext 16 arg)
  | Ocast16signed => Some (Val.sign_ext 16 arg)
  | Onegint => Some (Val.negint arg)
  | Onotint => Some (Val.notint arg)
  | Onegf => Some (Val.negf arg)
  | Oabsf => Some (Val.absf arg)
  | Onegfs => Some (Val.negfs arg)
  | Oabsfs => Some (Val.absfs arg)
  | Osingleoffloat => Some (Val.singleoffloat arg)
  | Ofloatofsingle => Some (Val.floatofsingle arg)
  | Ointoffloat => Val.intoffloat arg
  | Ointuoffloat => Val.intuoffloat arg
  | Ofloatofint => Val.floatofint arg
  | Ofloatofintu => Val.floatofintu arg
  | Ointofsingle => Val.intofsingle arg
  | Ointuofsingle => Val.intuofsingle arg
  | Osingleofint => Val.singleofint arg
  | Osingleofintu => Val.singleofintu arg
  | Onegl => Some (Val.negl arg)
  | Onotl => Some (Val.notl arg)
  | Ointoflong => Some (Val.loword arg)
  | Olongofint => Some (Val.longofint arg)
  | Olongofintu => Some (Val.longofintu arg)
  | Olongoffloat => Val.longoffloat arg
  | Olonguoffloat => Val.longuoffloat arg
  | Ofloatoflong => Val.floatoflong arg
  | Ofloatoflongu => Val.floatoflongu arg
  | Olongofsingle => Val.longofsingle arg
  | Olonguofsingle => Val.longuofsingle arg
  | Osingleoflong => Val.singleoflong arg
  | Osingleoflongu => Val.singleoflongu arg
  end.

Definition eval_binop
            (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
  match op with
  | Oadd => Some (Val.add arg1 arg2)
  | Osub => Some (Val.sub arg1 arg2)
  | Omul => Some (Val.mul arg1 arg2)
  | Odiv => Val.divs arg1 arg2
  | Odivu => Val.divu arg1 arg2
  | Omod => Val.mods arg1 arg2
  | Omodu => Val.modu arg1 arg2
  | Oand => Some (Val.and arg1 arg2)
  | Oor => Some (Val.or arg1 arg2)
  | Oxor => Some (Val.xor arg1 arg2)
  | Oshl => Some (Val.shl arg1 arg2)
  | Oshr => Some (Val.shr arg1 arg2)
  | Oshru => Some (Val.shru arg1 arg2)
  | Oaddf => Some (Val.addf arg1 arg2)
  | Osubf => Some (Val.subf arg1 arg2)
  | Omulf => Some (Val.mulf arg1 arg2)
  | Odivf => Some (Val.divf arg1 arg2)
  | Oaddfs => Some (Val.addfs arg1 arg2)
  | Osubfs => Some (Val.subfs arg1 arg2)
  | Omulfs => Some (Val.mulfs arg1 arg2)
  | Odivfs => Some (Val.divfs arg1 arg2)
  | Oaddl => Some (Val.addl arg1 arg2)
  | Osubl => Some (Val.subl arg1 arg2)
  | Omull => Some (Val.mull arg1 arg2)
  | Odivl => Val.divls arg1 arg2
  | Odivlu => Val.divlu arg1 arg2
  | Omodl => Val.modls arg1 arg2
  | Omodlu => Val.modlu arg1 arg2
  | Oandl => Some (Val.andl arg1 arg2)
  | Oorl => Some (Val.orl arg1 arg2)
  | Oxorl => Some (Val.xorl arg1 arg2)
  | Oshll => Some (Val.shll arg1 arg2)
  | Oshrl => Some (Val.shrl arg1 arg2)
  | Oshrlu => Some (Val.shrlu arg1 arg2)
  | Ocmp c => Some (Val.cmp c arg1 arg2)
  | Ocmpu c => Some (Val.cmpu (Mem.valid_pointer m) c arg1 arg2)
  | Ocmpf c => Some (Val.cmpf c arg1 arg2)
  | Ocmpfs c => Some (Val.cmpfs c arg1 arg2)
  | Ocmpl c => Val.cmpl c arg1 arg2
  | Ocmplu c => Val.cmplu (Mem.valid_pointer m) c arg1 arg2
  end.

Evaluation of an expression: eval_expr ge sp e m a v states that expression a evaluates to value v. ge is the global environment, e the local environment, and m the current memory state. They are unchanged during evaluation. sp is the pointer to the memory block allocated for this function (stack frame).

Section EVAL_EXPR.

Variable sp: val.
Variable e: env.
Variable m: mem.

Inductive eval_expr: expr -> val -> Prop :=
  | eval_Evar: forall id v,
      PTree.get id e = Some v ->
      eval_expr (Evar id) v
  | eval_Econst: forall cst v,
      eval_constant sp cst = Some v ->
      eval_expr (Econst cst) v
  | eval_Eunop: forall op a1 v1 v,
      eval_expr a1 v1 ->
      eval_unop op v1 = Some v ->
      eval_expr (Eunop op a1) v
  | eval_Ebinop: forall op a1 a2 v1 v2 v,
      eval_expr a1 v1 ->
      eval_expr a2 v2 ->
      eval_binop op v1 v2 m = Some v ->
      eval_expr (Ebinop op a1 a2) v
  | eval_Eload: forall chunk addr vaddr v,
      eval_expr addr vaddr ->
      Mem.loadv chunk m vaddr = Some v ->
      eval_expr (Eload chunk addr) v.

Inductive eval_exprlist: list expr -> list val -> Prop :=
  | eval_Enil:
      eval_exprlist nil nil
  | eval_Econs: forall a1 al v1 vl,
      eval_expr a1 v1 -> eval_exprlist al vl ->
      eval_exprlist (a1 :: al) (v1 :: vl).

End EVAL_EXPR.

Pop continuation until a call or stop

Fixpoint call_cont (k: cont) : cont :=
  match k with
  | Kseq s k => call_cont k
  | Kblock k => call_cont k
  | _ => k
  end.

Definition is_call_cont (k: cont) : Prop :=
  match k with
  | Kstop => True
  | Kcall _ _ _ _ _ => True
  | _ => False
  end.

Find the statement and manufacture the continuation corresponding to a label

Fixpoint find_label (lbl: label) (s: stmt) (k: cont)
                    {struct s}: option (stmt * cont) :=
  match s with
  | Sseq s1 s2 =>
      match find_label lbl s1 (Kseq s2 k) with
      | Some sk => Some sk
      | None => find_label lbl s2 k
      end
  | Sifthenelse a s1 s2 =>
      match find_label lbl s1 k with
      | Some sk => Some sk
      | None => find_label lbl s2 k
      end
  | Sloop s1 =>
      find_label lbl s1 (Kseq (Sloop s1) k)
  | Sblock s1 =>
      find_label lbl s1 (Kblock k)
  | Slabel lbl' s' =>
      if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
  | _ => None
  end.

One step of execution



Inductive step: state -> trace -> state -> Prop :=

  | step_skip_seq: forall f s k sp e m,
      step (State f Sskip (Kseq s k) sp e m)
        E0 (State f s k sp e m)
  | step_skip_block: forall f k sp e m,
      step (State f Sskip (Kblock k) sp e m)
        E0 (State f Sskip k sp e m)
  | step_skip_call: forall f k sp e m m',
      is_call_cont k ->
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      step (State f Sskip k (Vptr sp Ptrofs.zero) e m)
        E0 (Returnstate Vundef k m')

  | step_assign: forall f id a k sp e m v,
      eval_expr sp e m a v ->
      step (State f (Sassign id a) k sp e m)
        E0 (State f Sskip k sp (PTree.set id v e) m)

  | step_store: forall f chunk addr a k sp e m vaddr v m',
      eval_expr sp e m addr vaddr ->
      eval_expr sp e m a v ->
      Mem.storev chunk m vaddr v = Some m' ->
      step (State f (Sstore chunk addr a) k sp e m)
        E0 (State f Sskip k sp e m')

  | step_call: forall f optid sig a bl k sp e m vf vargs fd id (IFI: is_function_ident ge vf id),
      eval_expr sp e m a vf ->
      eval_exprlist sp e m bl vargs ->
      Genv.find_funct ge vf = Some fd ->
      funsig fd = sig ->
      step (State f (Scall optid sig a bl) k sp e m)
        E0 (Callstate fd vargs (Kcall optid f sp e k) (Mem.push_new_stage m) (fn_stack_requirements id))

  | step_tailcall: forall f sig a bl k sp e m vf vargs fd m' m'' id (IFI: is_function_ident ge vf id),
      eval_expr (Vptr sp Ptrofs.zero) e m a vf ->
      eval_exprlist (Vptr sp Ptrofs.zero) e m bl vargs ->
      Genv.find_funct ge vf = Some fd ->
      funsig fd = sig ->
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      Mem.tailcall_stage m' = Some m'' ->
      step (State f (Stailcall sig a bl) k (Vptr sp Ptrofs.zero) e m)
        E0 (Callstate fd vargs (call_cont k) m'' (fn_stack_requirements id))

  | step_builtin: forall f optid ef bl k sp e m vargs t vres m' m'',
      eval_exprlist sp e m bl vargs ->
      external_call ef ge vargs (Mem.push_new_stage m) t vres m' ->
      Mem.unrecord_stack_block m' = Some m'' ->
      forall BUILTIN_ENABLED : builtin_enabled ef,
      step (State f (Sbuiltin optid ef bl) k sp e m)
         t (State f Sskip k sp (set_optvar optid vres e) m'')

  | step_seq: forall f s1 s2 k sp e m,
      step (State f (Sseq s1 s2) k sp e m)
        E0 (State f s1 (Kseq s2 k) sp e m)

  | step_ifthenelse: forall f a s1 s2 k sp e m v b,
      eval_expr sp e m a v ->
      Val.bool_of_val v b ->
      step (State f (Sifthenelse a s1 s2) k sp e m)
        E0 (State f (if b then s1 else s2) k sp e m)

  | step_loop: forall f s k sp e m,
      step (State f (Sloop s) k sp e m)
        E0 (State f s (Kseq (Sloop s) k) sp e m)

  | step_block: forall f s k sp e m,
      step (State f (Sblock s) k sp e m)
        E0 (State f s (Kblock k) sp e m)

  | step_exit_seq: forall f n s k sp e m,
      step (State f (Sexit n) (Kseq s k) sp e m)
        E0 (State f (Sexit n) k sp e m)
  | step_exit_block_0: forall f k sp e m,
      step (State f (Sexit O) (Kblock k) sp e m)
        E0 (State f Sskip k sp e m)
  | step_exit_block_S: forall f n k sp e m,
      step (State f (Sexit (S n)) (Kblock k) sp e m)
        E0 (State f (Sexit n) k sp e m)

  | step_switch: forall f islong a cases default k sp e m v n,
      eval_expr sp e m a v ->
      switch_argument islong v n ->
      step (State f (Sswitch islong a cases default) k sp e m)
        E0 (State f (Sexit (switch_target n default cases)) k sp e m)

  | step_return_0: forall f k sp e m m',
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      step (State f (Sreturn None) k (Vptr sp Ptrofs.zero) e m)
        E0 (Returnstate Vundef (call_cont k) m')
  | step_return_1: forall f a k sp e m v m',
      eval_expr (Vptr sp Ptrofs.zero) e m a v ->
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      step (State f (Sreturn (Some a)) k (Vptr sp Ptrofs.zero) e m)
        E0 (Returnstate v (call_cont k) m')

  | step_label: forall f lbl s k sp e m,
      step (State f (Slabel lbl s) k sp e m)
        E0 (State f s k sp e m)

  | step_goto: forall f lbl k sp e m s' k',
      find_label lbl f.(fn_body) (call_cont k) = Some(s', k') ->
      step (State f (Sgoto lbl) k sp e m)
        E0 (State f s' k' sp e m)

  | step_internal_function: forall f vargs k m m' sp e m'' sz,
      Mem.alloc m 0 f.(fn_stackspace) = (m', sp) ->
      Mem.record_stack_blocks m' (make_singleton_frame_adt sp (fn_stackspace f) sz) = Some m'' ->
      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
      step (Callstate (Internal f) vargs k m sz)
        E0 (State f f.(fn_body) k (Vptr sp Ptrofs.zero) e m'')
  | step_external_function: forall ef vargs k m t vres m' sz,
      external_call ef ge vargs m t vres m' ->
      step (Callstate (External ef) vargs k m sz)
         t (Returnstate vres k m')

  | step_return: forall v optid f sp e k m m',
      Mem.unrecord_stack_block m = Some m' ->
      step (Returnstate v (Kcall optid f sp e k) m)
        E0 (State f Sskip k sp (set_optvar optid v e) m').




Fixpoint funs_of_cont k : list (option (block * Z)) :=
  match k with
  | Kstop => nil
  | Kseq s k => funs_of_cont k
  | Kblock k => funs_of_cont k
  | Kcall oi f (Vptr sp _) e k => Some (sp, fn_stackspace f):: funs_of_cont k
  | Kcall oi f _ e k => None :: funs_of_cont k
  end.

  Inductive stack_inv : state -> Prop :=
  | stack_inv_regular: forall k f s sp m o e
                         (MSA1: match_stack (Some (sp, fn_stackspace f)::funs_of_cont k) (Mem.stack m)),
      stack_inv (State f s k (Vptr sp o) e m)
  | stack_inv_call: forall k fd args m sz
                      (TOPNOPERM: top_tframe_tc (Mem.stack m))
                      (MSA1: match_stack (funs_of_cont k) (tl (Mem.stack m))),
      stack_inv (Callstate fd args k m sz)
  | stack_inv_return: forall k res m
                        (MSA1: match_stack (funs_of_cont k) (tl (Mem.stack m))),
      stack_inv (Returnstate res k m).

  Lemma funs_of_call_cont:
    forall k,
      funs_of_cont (call_cont k) = funs_of_cont k.
Proof.
    induction k; simpl; intros; eauto.
  Qed.

  Lemma find_label_funs_of_cont:
    forall lbl s k s' k',
      find_label lbl s k = Some (s', k') ->
      funs_of_cont k' = funs_of_cont k.
Proof.
    induction s; simpl; intros; try congruence.
    - destr_in H; eauto. inv H. apply IHs1 in Heqo. simpl in Heqo. auto.
    - destr_in H; inv H; eauto.
    - apply IHs in H. simpl in H; auto.
    - apply IHs in H. simpl in H; auto.
    - destr_in H; eauto.
  Qed.

  Lemma stack_inv_inv:
    forall S1 t S2,
      step S1 t S2 ->
      stack_inv S1 -> stack_inv S2.
Proof.
    destruct 1; simpl; intros SI;
      inv SI; try econstructor; repeat rewrite_stack_blocks; eauto;
        try solve [inv MSA1; simpl; rewrite ?funs_of_call_cont; eauto].
    - constructor. reflexivity.
    - intros; constructor. reflexivity.
    - simpl. inv MSA1. inversion 1; subst.
      rewrite funs_of_call_cont. auto.
    - erewrite find_label_funs_of_cont by eauto.
      rewrite funs_of_call_cont. auto.
    - intros EQ; rewrite EQ in *. simpl in *.
      econstructor; eauto; reflexivity.
    - simpl in MSA1. repeat destr_in MSA1. econstructor. rewrite_stack_blocks.
      rewrite <- H4. econstructor; eauto.
  Qed.
  
End RELSEM.

Execution of whole programs are described as sequences of transitions from an initial state to a final state. An initial state is a Callstate corresponding to the invocation of the ``main'' function of the program without arguments and with an empty continuation.

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall b f m0 m2,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      funsig f = signature_main ->
      Mem.record_init_sp m0 = Some m2 ->
      initial_state p (Callstate f nil Kstop (Mem.push_new_stage m2) (fn_stack_requirements (prog_main p))).


Lemma stack_inv_initial:
  forall p S
    (INIT: initial_state p S),
    stack_inv S.
Proof.
  intros; inv INIT; econstructor.
  rewrite_stack_blocks; constructor. reflexivity.
  constructor.
Qed.

A final state is a Returnstate with an empty continuation.

Inductive final_state: state -> int -> Prop :=
  | final_state_intro: forall r m,
      final_state (Returnstate (Vint r) Kstop m) r.

The corresponding small-step semantics.

Definition semantics (p: program) :=
  Semantics step (initial_state p) final_state (Genv.globalenv p).

This semantics is receptive to changes in events.

Lemma semantics_receptive:
  forall (p: program), receptive (semantics p).
Proof.
  intros. constructor; simpl; intros.
 receptiveness *)  assert (t1 = E0 -> exists s2, step (Genv.globalenv p) s t2 s2).
    intros. subst. inv H0. exists s1; auto.
  inversion H; subst; auto.
  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
  destruct (Mem.unrecord_stack _ _ H4) as (b & EQ).
  edestruct (Mem.unrecord_stack_block_succeeds m2) as (m2' & USB & STK).
  apply external_call_stack_blocks in EC2.
  repeat rewrite_stack_blocks.
  eauto.
  eexists. econstructor; eauto.
  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
  exists (Returnstate vres2 k m2). econstructor; eauto.
 trace length *)  red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto.
Qed.
End WITHEXTCALLS.
Generated by coq2html