(** 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 Mem.
Require Import Op.
Require Import Globalenvs.

(** * Abstract syntax *)

(** Cminor is a low-level imperative language structured in expressions,
  statements, functions and programs.  Expressions include
  reading local variables, reading and writing store locations,
  arithmetic operations, function calls, and conditional expressions
  (similar to [e1 ? e2 : e3] in C).  The [Elet] and [Eletvar] constructs
  enable sharing the computations of subexpressions.  De Bruijn notation
  is used: [Eletvar n] refers to the value bound by then [n+1]-th enclosing
  [Elet] construct.

  A variant [condexpr] of [expr] is used to represent expressions
  which are evaluated for their boolean value only and not their exact value.
*)

Inductive expr : Set :=
  | Evar : ident -> expr
  | Eop : operation -> exprlist -> expr
  | Eload : memory_chunk -> addressing -> exprlist -> expr
  | Estore : memory_chunk -> addressing -> exprlist -> expr -> expr
  | Ecall : signature -> expr -> exprlist -> expr
  | Econdition : condexpr -> expr -> expr -> expr
  | Elet : expr -> expr -> expr
  | Eletvar : nat -> expr
  | Ealloc : expr -> expr

with condexpr : Set :=
  | CEtrue: condexpr
  | CEfalse: condexpr
  | CEcond: condition -> exprlist -> condexpr
  | CEcondition : condexpr -> condexpr -> condexpr -> condexpr

with exprlist : Set :=
  | Enil: exprlist
  | Econs: expr -> exprlist -> exprlist.

(** Statements include expression evaluation, assignment to local variables,
  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. *)

Inductive stmt : Set :=
  | Sskip: stmt
  | Sexpr: expr -> stmt
  | Sassign : ident -> expr -> stmt
  | Sseq: stmt -> stmt -> stmt
  | Sifthenelse: condexpr -> stmt -> stmt -> stmt
  | Sloop: stmt -> stmt
  | Sblock: stmt -> stmt
  | Sexit: nat -> stmt
  | Sswitch: expr -> list (int * nat) -> nat -> stmt
  | Sreturn: option expr -> 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 : Set := 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 => f.(fn_sig)
  | External ef => ef.(ef_sig)
  end.

(** * Operational semantics *)

(** The operational semantics for Cminor is given in big-step operational
  style.  Expressions evaluate to values, and statements evaluate to
  ``outcomes'' indicating how execution should proceed afterwards. *)

Inductive outcome: Set :=
  | Out_normal: outcome                (**r continue in sequence *)
  | Out_exit: nat -> outcome           (**r terminate [n+1] enclosing blocks *)
  | Out_return: option val -> outcome. (**r return immediately to caller *)

Definition outcome_result_value
                 (out: outcome) (ot: option typ) (v: val) : Prop :=
  match out, ot with
  | Out_normal, None => v = Vundef
  | Out_return None, None => v = Vundef
  | Out_return (Some v'), Some ty => v = v'
  | _, _ => False
  end.

Definition outcome_block (out: outcome) : outcome :=
  match out with
  | Out_normal => Out_normal
  | Out_exit O => Out_normal
  | Out_exit (S n) => Out_exit n
  | Out_return optv => Out_return optv
  end.

Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat))
                       {struct cases} : nat :=
  match cases with
  | nil => dfl
  | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem
  end.

(** Three kinds of evaluation environments are involved:
- [genv]: global environments, define symbols and functions;
- [env]: local environments, map local variables to values;
- [lenv]: let environments, map de Bruijn indices to values.
*)

Definition genv := Genv.t fundef.
Definition env := PTree.t val.
Definition letenv := list 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.

Section RELSEM.

Variable ge: genv.

(** Evaluation of an expression: [eval_expr ge sp le e m a m' v]
  states that expression [a], in initial local environment [e] and
  memory state [m], evaluates to value [v].  [m'] is the final
  memory state, reflecting memory stores possibly performed by [a].
  Expressions do not assign variables, therefore the local environment
  [e] is unchanged.  [ge] and [le] are the global environment and let
  environment respectively, and are unchanged during evaluation.  [sp]
  is the pointer to the memory block allocated for this function
  (stack frame).
*)

Inductive eval_expr:
         val -> letenv -> env ->
         mem -> expr -> trace -> mem -> val -> Prop :=
  | eval_Evar:
      forall sp le e m id v,
      PTree.get id e = Some v ->
      eval_expr sp le e m (Evar id) E0 m v
  | eval_Eop:
      forall sp le e m op al t m1 vl v,
      eval_exprlist sp le e m al t m1 vl ->
      eval_operation ge sp op vl = Some v ->
      eval_expr sp le e m (Eop op al) t m1 v
  | eval_Eload:
      forall sp le e m chunk addr al t m1 v vl a,
      eval_exprlist sp le e m al t m1 vl ->
      eval_addressing ge sp addr vl = Some a ->
      Mem.loadv chunk m1 a = Some v ->
      eval_expr sp le e m (Eload chunk addr al) t m1 v
  | eval_Estore:
      forall sp le e m chunk addr al b t t1 m1 vl t2 m2 m3 v a,
      eval_exprlist sp le e m al t1 m1 vl ->
      eval_expr sp le e m1 b t2 m2 v ->
      eval_addressing ge sp addr vl = Some a ->
      Mem.storev chunk m2 a v = Some m3 ->
      t = t1 ** t2 ->
      eval_expr sp le e m (Estore chunk addr al b) t m3 v
  | eval_Ecall:
      forall sp le e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f,
      eval_expr sp le e m a t1 m1 vf ->
      eval_exprlist sp le e m1 bl t2 m2 vargs ->
      Genv.find_funct ge vf = Some f ->
      funsig f = sig ->
      eval_funcall m2 f vargs t3 m3 vres ->
      t = t1 ** t2 ** t3 ->
      eval_expr sp le e m (Ecall sig a bl) t m3 vres
  | eval_Econdition:
      forall sp le e m a b c t t1 m1 v1 t2 m2 v2,
      eval_condexpr sp le e m a t1 m1 v1 ->
      eval_expr sp le e m1 (if v1 then b else c) t2 m2 v2 ->
      t = t1 ** t2 ->
      eval_expr sp le e m (Econdition a b c) t m2 v2
  | eval_Elet:
      forall sp le e m a b t t1 m1 v1 t2 m2 v2,
      eval_expr sp le e m a t1 m1 v1 ->
      eval_expr sp (v1::le) e m1 b t2 m2 v2 ->
      t = t1 ** t2 ->
      eval_expr sp le e m (Elet a b) t m2 v2
  | eval_Eletvar:
      forall sp le e m n v,
      nth_error le n = Some v ->
      eval_expr sp le e m (Eletvar n) E0 m v
  | eval_Ealloc:
      forall sp le e m a t m1 n m2 b,
      eval_expr sp le e m a t m1 (Vint n) ->
      Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
      eval_expr sp le e m (Ealloc a) t m2 (Vptr b Int.zero)

(** Evaluation of a condition expression:
  [eval_condexpr ge sp le e m a m' b]
  states that condition expression [a] evaluates to the boolean value [b].
  The other parameters are as in [eval_expr].
*)

with eval_condexpr:
         val -> letenv -> env ->
         mem -> condexpr -> trace -> mem -> bool -> Prop :=
  | eval_CEtrue:
      forall sp le e m,
      eval_condexpr sp le e m CEtrue E0 m true
  | eval_CEfalse:
      forall sp le e m,
      eval_condexpr sp le e m CEfalse E0 m false
  | eval_CEcond:
      forall sp le e m cond al t1 m1 vl b,
      eval_exprlist sp le e m al t1 m1 vl ->
      eval_condition cond vl = Some b ->
      eval_condexpr sp le e m (CEcond cond al) t1 m1 b
  | eval_CEcondition:
      forall sp le e m a b c t t1 m1 vb1 t2 m2 vb2,
      eval_condexpr sp le e m a t1 m1 vb1 ->
      eval_condexpr sp le e m1 (if vb1 then b else c) t2 m2 vb2 ->
      t = t1 ** t2 ->
      eval_condexpr sp le e m (CEcondition a b c) t m2 vb2

(** Evaluation of a list of expressions:
  [eval_exprlist ge sp le al m a m' vl]
  states that the list [al] of expressions evaluate 
  to the list [vl] of values.
  The other parameters are as in [eval_expr].
*)

with eval_exprlist:
         val -> letenv -> env ->
         mem -> exprlist -> trace -> mem -> list val -> Prop :=
  | eval_Enil:
      forall sp le e m,
      eval_exprlist sp le e m Enil E0 m nil
  | eval_Econs:
      forall sp le e m a bl t t1 m1 v t2 m2 vl,
      eval_expr sp le e m a t1 m1 v ->
      eval_exprlist sp le e m1 bl t2 m2 vl ->
      t = t1 ** t2 ->
      eval_exprlist sp le e m (Econs a bl) t m2 (v :: vl)

(** Evaluation of a function invocation: [eval_funcall ge m f args m' res]
  means that the function [f], applied to the arguments [args] in
  memory state [m], returns the value [res] in modified memory state [m'].
*)

with eval_funcall:
        mem -> fundef -> list val -> trace ->
        mem -> val -> Prop :=
  | eval_funcall_internal:
      forall m f vargs m1 sp e t e2 m2 out vres,
      Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
      exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out ->
      outcome_result_value out f.(fn_sig).(sig_res) vres ->
      eval_funcall m (Internal f) vargs t (Mem.free m2 sp) vres
  | eval_funcall_external:
      forall ef m args t res,
      event_match ef args t res ->
      eval_funcall m (External ef) args t m res

(** Execution of a statement: [exec_stmt ge sp e m s e' m' out]
  means that statement [s] executes with outcome [out].
  The other parameters are as in [eval_expr]. *)

with exec_stmt:
         val ->
         env -> mem -> stmt -> trace ->
         env -> mem -> outcome -> Prop :=
  | exec_Sskip:
      forall sp e m,
      exec_stmt sp e m Sskip E0 e m Out_normal
  | exec_Sexpr:
      forall sp e m a t m1 v,
      eval_expr sp nil e m a t m1 v ->
      exec_stmt sp e m (Sexpr a) t e m1 Out_normal
  | exec_Sassign:
      forall sp e m id a t m1 v,
      eval_expr sp nil e m a t m1 v ->
      exec_stmt sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal
  | exec_Sifthenelse:
      forall sp e m a s1 s2 t t1 m1 v1 t2 e2 m2 out,
      eval_condexpr sp nil e m a t1 m1 v1 ->
      exec_stmt sp e m1 (if v1 then s1 else s2) t2 e2 m2 out ->
      t = t1 ** t2 ->
      exec_stmt sp e m (Sifthenelse a s1 s2) t e2 m2 out
  | exec_Sseq_continue:
      forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out,
      exec_stmt sp e m s1 t1 e1 m1 Out_normal ->
      exec_stmt sp e1 m1 s2 t2 e2 m2 out ->
      t = t1 ** t2 ->
      exec_stmt sp e m (Sseq s1 s2) t e2 m2 out
  | exec_Sseq_stop:
      forall sp e m t s1 s2 e1 m1 out,
      exec_stmt sp e m s1 t e1 m1 out ->
      out <> Out_normal ->
      exec_stmt sp e m (Sseq s1 s2) t e1 m1 out
  | exec_Sloop_loop:
      forall sp e m s t t1 e1 m1 t2 e2 m2 out,
      exec_stmt sp e m s t1 e1 m1 Out_normal ->
      exec_stmt sp e1 m1 (Sloop s) t2 e2 m2 out ->
      t = t1 ** t2 ->
      exec_stmt sp e m (Sloop s) t e2 m2 out
  | exec_Sloop_stop:
      forall sp e m t s e1 m1 out,
      exec_stmt sp e m s t e1 m1 out ->
      out <> Out_normal ->
      exec_stmt sp e m (Sloop s) t e1 m1 out
  | exec_Sblock:
      forall sp e m s t e1 m1 out,
      exec_stmt sp e m s t e1 m1 out ->
      exec_stmt sp e m (Sblock s) t e1 m1 (outcome_block out)
  | exec_Sexit:
      forall sp e m n,
      exec_stmt sp e m (Sexit n) E0 e m (Out_exit n)
  | exec_Sswitch:
      forall sp e m a cases default t1 m1 n,
      eval_expr sp nil e m a t1 m1 (Vint n) ->
      exec_stmt sp e m (Sswitch a cases default)
                t1 e m1 (Out_exit (switch_target n default cases))
  | exec_Sreturn_none:
      forall sp e m,
      exec_stmt sp e m (Sreturn None) E0 e m (Out_return None)
  | exec_Sreturn_some:
      forall sp e m a t m1 v,
      eval_expr sp nil e m a t m1 v ->
      exec_stmt sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)).

End RELSEM.

(** Execution of a whole program: [exec_program p r]
  holds if the application of [p]'s main function to no arguments
  in the initial memory state for [p] eventually returns value [r]. *)

Definition exec_program (p: program) (t: trace) (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 /\
  funsig f = mksignature nil (Some Tint) /\
  eval_funcall ge m0 f nil t m r.