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
  end.

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:

State cs f sp pc e m describes an execution point within a function. f is the current function. sp is the pointer to the stack block for its current activation (as in Cminor). pc is the current program point (CFG node) within the code c. e gives the current values for the local variables. m is the current memory state.
Callstate cs f args m is an intermediate state that appears during function calls. f is the function definition that we are calling. args (a list of values) are the arguments for this call. m is the current memory state.
Returnstate cs v m is an intermediate state that appears when a function terminates and returns to its caller. v is the return value and m the current memory state.

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 *)
      stackframe.

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 *)
      state
  | Callstate:
      forall (stack: list stackframe) (* call stack *)
             (f: fundef) (* function to call *)
             (args: list val) (* arguments to the call *)
             (m: mem), (* memory state *)
      state
  | Returnstate:
      forall (stack: list stackframe) (* call stack *)
             (v: val) (* return value for the call *)
             (m: mem), (* memory state *)
      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 Int.zero) e m fn vfn ->
      eval_exprlist ge (Vptr sp Int.zero) e m args vargs ->
      Genv.find_funct ge vfn = Some fd ->
      funsig fd = sig ->
      Mem.free m sp 0 f.(fn_stacksize) = Some m' ->
      step (State s f (Vptr sp Int.zero) 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) ->
      Mem.free m sp 0 f.(fn_stacksize) = Some m' ->
      step (State s f (Vptr sp Int.zero) 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 Int.zero) e m a v ->
      Mem.free m sp 0 f.(fn_stacksize) = Some m' ->
      step (State s f (Vptr sp Int.zero) 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 Int.zero) 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).

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

Module CFG

Abstract syntax

Operational semantics