Module CFG

Abstract syntax and semantics for the CFG 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.
Require Import Cminor.

Abstract syntax

RTL is organized as statements, functions and programs. Statements are organized as a control-flow graph: a function is a finite map from ``nodes'' (abstract program points) to statements and each instruction lists explicitly the nodes of its successors. Statements involve structured, pure expressions that are identical to those of Cminor.

Definition node := positive.

Inductive instruction : Type :=
  | Iskip: node -> instruction
  | Iassign: ident -> expr -> node -> instruction
  | Istore: memory_chunk -> expr -> expr -> node -> instruction
  | Icall: option ident -> signature -> expr -> list expr -> node -> instruction
  | Itailcall: signature -> expr -> list expr -> instruction
  | Ibuiltin : option ident -> external_function -> list expr -> node -> instruction
  | Iifthenelse: expr -> node -> node -> instruction
  | Iswitch: expr -> list (int * node) -> node -> instruction
  | Ireturn: option expr -> instruction.

Definition code: Type := PTree.t instruction.

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_stacksize: Z;
  fn_code: code;
  fn_entrypoint: node

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

Operational semantics

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

The dynamic semantics of CFG is given in small-step style, as a set of transitions between states. A state captures the current point in the execution. Three kinds of states appear in the transitions: In all three kinds of states, the cs parameter represents the call stack. It is a list of frames Stackframe res f sp pc e. Each frame represents a function call in progress. res is the variable that will receive the result of the call. f is the calling function. sp is its stack pointer. pc is the program point for the instruction that follows the call. e is the state of local variables in the calling function.

Inductive stackframe : Type :=
  | Stackframe:
      forall (res: option ident) (* where to store the result *)
             (f: function) (* calling function *)
             (sp: val) (* stack pointer in calling function *)
             (pc: node) (* program point in calling function *)
             (e: env), (* local variables in calling function *)

Inductive state : Type :=
  | State:
      forall (stack: list stackframe) (* call stack *)
             (f: function) (* current function *)
             (sp: val) (* stack pointer *)
             (pc: node) (* current program point *)
             (e: env) (* local variable state *)
             (m: mem), (* memory state *)
  | Callstate:
      forall (stack: list stackframe) (* call stack *)
             (f: fundef) (* function to call *)
             (args: list val) (* arguments to the call *)
             (m: mem), (* memory state *)
  | Returnstate:
      forall (stack: list stackframe) (* call stack *)
             (v: val) (* return value for the call *)
             (m: mem), (* memory state *)

Section RELSEM.

Variable ge: genv.

The transitions are presented as an inductive predicate step ge st1 t st2, where ge is the global environment, st1 the initial state, st2 the final state, and t the trace of system calls performed during this transition.

Inductive step: state -> trace -> state -> Prop :=
  | step_skip:
      forall s f sp pc e m pc',
      (fn_code f)!pc = Some(Iskip pc') ->
      step (State s f sp pc e m)
        E0 (State s f sp pc' e m)
  | step_assign:
      forall s f sp pc e m id a pc' v,
      (fn_code f)!pc = Some(Iassign id a pc') ->
      eval_expr ge sp e m a v ->
      step (State s f sp pc e m)
        E0 (State s f sp pc' (PTree.set id v e) m)
  | step_store:
      forall s f sp pc e m chunk addr src pc' vaddr vsrc m',
      (fn_code f)!pc = Some(Istore chunk addr src pc') ->
      eval_expr ge sp e m addr vaddr ->
      eval_expr ge sp e m src vsrc ->
      Mem.storev chunk m vaddr vsrc = Some m' ->
      step (State s f sp pc e m)
        E0 (State s f sp pc' e m')
  | step_call:
      forall s f sp pc e m res sig fn args pc' vfn vargs fd,
      (fn_code f)!pc = Some(Icall res sig fn args pc') ->
      eval_expr ge sp e m fn vfn ->
      eval_exprlist ge sp e m args vargs ->
      Genv.find_funct ge vfn = Some fd ->
      funsig fd = sig ->
      step (State s f sp pc e m)
        E0 (Callstate (Stackframe res f sp pc' e :: s) fd vargs m)
  | step_tailcall:
      forall s f sp pc e m sig fn args vfn vargs fd m',
      (fn_code f)!pc = Some(Itailcall sig fn args) ->
      eval_expr ge (Vptr sp e m fn vfn ->
      eval_exprlist ge (Vptr sp e m args vargs ->
      Genv.find_funct ge vfn = Some fd ->
      funsig fd = sig -> m sp 0 f.(fn_stacksize) = Some m' ->
      step (State s f (Vptr sp pc e m)
        E0 (Callstate s fd vargs m')
  | step_builtin:
      forall s f sp pc e m res ef args pc' vargs t vres m',
      (fn_code f)!pc = Some(Ibuiltin res ef args pc') ->
      eval_exprlist ge sp e m args vargs ->
      external_call ef ge vargs m t vres m' ->
      step (State s f sp pc e m)
         t (State s f sp pc' (set_optvar res vres e) m')
  | step_ifthenelse:
      forall s f sp pc e m a ifso ifnot v b pc',
      (fn_code f)!pc = Some(Iifthenelse a ifso ifnot) ->
      eval_expr ge sp e m a v ->
      Val.bool_of_val v b ->
      pc' = (if b then ifso else ifnot) ->
      step (State s f sp pc e m)
        E0 (State s f sp pc' e m)
  | step_switch:
      forall s f sp pc e m a cases default n pc',
      (fn_code f)!pc = Some(Iswitch a cases default) ->
      eval_expr ge sp e m a (Vint n) ->
      pc' = switch_target n default cases ->
      step (State s f sp pc e m)
        E0 (State s f sp pc' e m)
  | step_return_0:
      forall s f sp pc e m m',
      (fn_code f)!pc = Some(Ireturn None) -> m sp 0 f.(fn_stacksize) = Some m' ->
      step (State s f (Vptr sp pc e m)
        E0 (Returnstate s Vundef m')
  | step_return_1:
      forall s f sp pc a e m v m',
      (fn_code f)!pc = Some(Ireturn (Some a)) ->
      eval_expr ge (Vptr sp e m a v -> m sp 0 f.(fn_stacksize) = Some m' ->
      step (State s f (Vptr sp pc e m)
        E0 (Returnstate s v m')
  | step_function_internal:
      forall s f args m m' sp e,
      Mem.alloc m 0 f.(fn_stacksize) = (m', sp) ->
      set_locals f.(fn_vars) (set_params args f.(fn_params)) = e ->
      step (Callstate s (Internal f) args m)
        E0 (State s f (Vptr sp f.(fn_entrypoint) e m')
  | step_function_external:
      forall s ef args res t m m',
      external_call ef ge args m t res m' ->
      step (Callstate s (External ef) args m)
         t (Returnstate s res m')
  | step_return:
      forall res f sp pc e s v m,
      step (Returnstate (Stackframe res f sp pc e :: s) v m)
        E0 (State s f sp pc (set_optvar res v e) m).


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 call stack.

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall b f m0,
      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 = mksignature nil (Some Tint) ->
      initial_state p (Callstate nil f nil m0).

A final state is a Returnstate with an call stack.

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

The corresponding small-step semantics.

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

The set of reachable states

Inductive Reach (p:program): state -> Prop :=
| Reach_init: forall s0,
  initial_state p s0 -> Reach p s0
| Reach_next: forall s1 tr s2,
  Reach p s1 -> step (Genv.globalenv p) s1 tr s2 -> Reach p s2.