Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
Require Import Clight.

Section WITHEXTCALLS.
Context `{external_calls_prf: ExternalCalls}.

Variable fn_stack_requirements: ident -> Z.

Section BIGSTEP.

Variable ge: genv.

Big-step semantics for terminating statements and functions

Inductive outcome: Type :=
   | Out_break: outcome (* terminated by break *)
   | Out_continue: outcome (* terminated by continue *)
   | Out_normal: outcome (* terminated normally *)
   | Out_return: option (val * type) -> outcome. (* terminated by return *)

Inductive out_normal_or_continue : outcome -> Prop :=
  | Out_normal_or_continue_N: out_normal_or_continue Out_normal
  | Out_normal_or_continue_C: out_normal_or_continue Out_continue.

Inductive out_break_or_return : outcome -> outcome -> Prop :=
  | Out_break_or_return_B: out_break_or_return Out_break Out_normal
  | Out_break_or_return_R: forall ov,
      out_break_or_return (Out_return ov) (Out_return ov).

Definition outcome_switch (out: outcome) : outcome :=
  match out with
  | Out_break => Out_normal
  | o => o
  end.

Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop :=
  match out, t with
  | Out_normal, Tvoid => v = Vundef
  | Out_return None, Tvoid => v = Vundef
  | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t m = Some v
  | _, _ => False
  end.


Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Z -> Prop.

Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop :=
  | exec_Sskip: forall e le m,
      exec_stmt e le m Sskip
               E0 le m Out_normal
  | exec_Sassign: forall e le m a1 a2 loc ofs v2 v m',
      eval_lvalue ge e le m a1 loc ofs ->
      eval_expr ge e le m a2 v2 ->
      sem_cast v2 (typeof a2) (typeof a1) m = Some v ->
      assign_loc ge (typeof a1) m loc ofs v m' ->
      exec_stmt e le m (Sassign a1 a2)
               E0 le m' Out_normal
  | exec_Sset: forall e le m id a v,
      eval_expr ge e le m a v ->
      exec_stmt e le m (Sset id a)
               E0 (PTree.set id v le) m Out_normal
  | exec_Scall: forall e le m optid a al tyargs tyres cconv vf vargs f t m' m'' vres id (IFI: is_function_ident ge vf id),
      classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
      eval_expr ge e le m a vf ->
      eval_exprlist ge e le m al tyargs vargs ->
      Genv.find_funct ge vf = Some f ->
      type_of_fundef f = Tfunction tyargs tyres cconv ->
      eval_funcall (Mem.push_new_stage m) f vargs t m' vres (fn_stack_requirements id) ->
      Mem.unrecord_stack_block m' = Some m'' ->
      exec_stmt e le m (Scall optid a al)
                t (set_opttemp optid vres le) m'' Out_normal
  | exec_Sbuiltin: forall e le m optid ef al tyargs vargs t m' vres m'',
      eval_exprlist ge e le m al tyargs 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,
      exec_stmt e le m (Sbuiltin optid ef tyargs al)
                t (set_opttemp optid vres le) m'' Out_normal
  | exec_Sseq_1: forall e le m s1 s2 t1 le1 m1 t2 le2 m2 out,
      exec_stmt e le m s1 t1 le1 m1 Out_normal ->
      exec_stmt e le1 m1 s2 t2 le2 m2 out ->
      exec_stmt e le m (Ssequence s1 s2)
                (t1 ** t2) le2 m2 out
  | exec_Sseq_2: forall e le m s1 s2 t1 le1 m1 out,
      exec_stmt e le m s1 t1 le1 m1 out ->
      out <> Out_normal ->
      exec_stmt e le m (Ssequence s1 s2)
                t1 le1 m1 out
  | exec_Sifthenelse: forall e le m a s1 s2 v1 b t le' m' out,
      eval_expr ge e le m a v1 ->
      bool_val v1 (typeof a) m = Some b ->
      exec_stmt e le m (if b then s1 else s2) t le' m' out ->
      exec_stmt e le m (Sifthenelse a s1 s2)
                t le' m' out
  | exec_Sreturn_none: forall e le m,
      exec_stmt e le m (Sreturn None)
               E0 le m (Out_return None)
  | exec_Sreturn_some: forall e le m a v,
      eval_expr ge e le m a v ->
      exec_stmt e le m (Sreturn (Some a))
                E0 le m (Out_return (Some (v, typeof a)))
  | exec_Sbreak: forall e le m,
      exec_stmt e le m Sbreak
               E0 le m Out_break
  | exec_Scontinue: forall e le m,
      exec_stmt e le m Scontinue
               E0 le m Out_continue
  | exec_Sloop_stop1: forall e le m s1 s2 t le' m' out' out,
      exec_stmt e le m s1 t le' m' out' ->
      out_break_or_return out' out ->
      exec_stmt e le m (Sloop s1 s2)
                t le' m' out
  | exec_Sloop_stop2: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 out2 out,
      exec_stmt e le m s1 t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      exec_stmt e le1 m1 s2 t2 le2 m2 out2 ->
      out_break_or_return out2 out ->
      exec_stmt e le m (Sloop s1 s2)
                (t1**t2) le2 m2 out
  | exec_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3 le3 m3 out,
      exec_stmt e le m s1 t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal ->
      exec_stmt e le2 m2 (Sloop s1 s2) t3 le3 m3 out ->
      exec_stmt e le m (Sloop s1 s2)
                (t1**t2**t3) le3 m3 out
  | exec_Sswitch: forall e le m a t v n sl le1 m1 out,
      eval_expr ge e le m a v ->
      sem_switch_arg v (typeof a) = Some n ->
      exec_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t le1 m1 out ->
      exec_stmt e le m (Sswitch a sl)
                t le1 m1 (outcome_switch out)


with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Z -> Prop :=
  | eval_funcall_internal: forall le m f vargs t e le' m2 m3 out vres m4 sz,
      function_entry ge f vargs m e le m2 sz ->
      exec_stmt e le m2 f.(fn_body) t le' m3 out ->
      outcome_result_value out f.(fn_return) vres m3 ->
      Mem.free_list m3 (blocks_of_env ge e) = Some m4 ->
      eval_funcall m (Internal f) vargs t m4 vres sz
  | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
      external_call ef ge vargs m t vres m' ->
      eval_funcall m (External ef targs tres cconv) vargs t m' vres 0.

Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
  with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
Combined Scheme exec_stmt_funcall_ind from exec_stmt_ind2, eval_funcall_ind2.

Big-step semantics for diverging statements and functions

CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop :=
  | execinf_Scall: forall e le m optid a al vf tyargs tyres cconv vargs f t id (IFI: is_function_ident ge vf id),
      classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
      eval_expr ge e le m a vf ->
      eval_exprlist ge e le m al tyargs vargs ->
      Genv.find_funct ge vf = Some f ->
      type_of_fundef f = Tfunction tyargs tyres cconv ->
      evalinf_funcall (Mem.push_new_stage m) f vargs t (fn_stack_requirements id) ->
      execinf_stmt e le m (Scall optid a al) t
  | execinf_Sseq_1: forall e le m s1 s2 t,
      execinf_stmt e le m s1 t ->
      execinf_stmt e le m (Ssequence s1 s2) t
  | execinf_Sseq_2: forall e le m s1 s2 t1 le1 m1 t2,
      exec_stmt e le m s1 t1 le1 m1 Out_normal ->
      execinf_stmt e le1 m1 s2 t2 ->
      execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2)
  | execinf_Sifthenelse: forall e le m a s1 s2 v1 b t,
      eval_expr ge e le m a v1 ->
      bool_val v1 (typeof a) m = Some b ->
      execinf_stmt e le m (if b then s1 else s2) t ->
      execinf_stmt e le m (Sifthenelse a s1 s2) t
  | execinf_Sloop_body1: forall e le m s1 s2 t,
      execinf_stmt e le m s1 t ->
      execinf_stmt e le m (Sloop s1 s2) t
  | execinf_Sloop_body2: forall e le m s1 s2 t1 le1 m1 out1 t2,
      exec_stmt e le m s1 t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      execinf_stmt e le1 m1 s2 t2 ->
      execinf_stmt e le m (Sloop s1 s2) (t1***t2)
  | execinf_Sloop_loop: forall e le m s1 s2 t1 le1 m1 out1 t2 le2 m2 t3,
      exec_stmt e le m s1 t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal ->
      execinf_stmt e le2 m2 (Sloop s1 s2) t3 ->
      execinf_stmt e le m (Sloop s1 s2) (t1***t2***t3)
  | execinf_Sswitch: forall e le m a t v n sl,
      eval_expr ge e le m a v ->
      sem_switch_arg v (typeof a) = Some n ->
      execinf_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t ->
      execinf_stmt e le m (Sswitch a sl) t


with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Z -> Prop :=
  | evalinf_funcall_internal: forall m f vargs t e le m2 sz,
      function_entry ge f vargs m e le m2 sz ->
      execinf_stmt e le m2 f.(fn_body) t ->
      evalinf_funcall m (Internal f) vargs t sz.

End BIGSTEP.


Section WHOLE_PROGRAM.

Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Z -> Prop.

Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
  | bigstep_program_terminates_intro: forall b f m0 m02 m1 t r,
      let ge := 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 ->
      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
      Mem.record_init_sp m0 = Some m02 ->
      eval_funcall ge function_entry (Mem.push_new_stage m02) f nil t m1 (Vint r) (fn_stack_requirements (prog_main p))->
      bigstep_program_terminates p t r.

Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
  | bigstep_program_diverges_intro: forall b f m0 t m02,
      let ge := 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 ->
      type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
      Mem.record_init_sp m0 = Some m02 ->
      evalinf_funcall ge function_entry (Mem.push_new_stage m02) f nil t (fn_stack_requirements (prog_main p)) ->
      bigstep_program_diverges p t.

Definition bigstep_semantics (p: program) :=
  Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p).

End WHOLE_PROGRAM.

Implication from big-step semantics to transition semantics

Section BIGSTEP_TO_TRANSITIONS.

Variable prog: program.
Let ge : genv := globalenv prog.

Inductive outcome_state_match
       (e: env) (le: temp_env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
  | osm_normal:
      outcome_state_match e le m f k Out_normal (State f Sskip k e le m)
  | osm_break:
      outcome_state_match e le m f k Out_break (State f Sbreak k e le m)
  | osm_continue:
      outcome_state_match e le m f k Out_continue (State f Scontinue k e le m)
  | osm_return_none: forall k',
      call_cont k' = call_cont k ->
      outcome_state_match e le m f k
        (Out_return None) (State f (Sreturn None) k' e le m)
  | osm_return_some: forall a v k',
      call_cont k' = call_cont k ->
      eval_expr ge e le m a v ->
      outcome_state_match e le m f k
        (Out_return (Some (v,typeof a))) (State f (Sreturn (Some a)) k' e le m).

Lemma is_call_cont_call_cont:
  forall k, is_call_cont k -> call_cont k = k.

Section WITHFUNCTIONENTRY.

Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Z -> Prop.

Lemma exec_stmt_eval_funcall_steps:
  (forall e le m s t le' m' out,
   exec_stmt ge function_entry e le m s t le' m' out ->
   forall f k, exists S,
   star (fun ge' => step fn_stack_requirements ge' function_entry) ge (State f s k e le m) t S
   /\ outcome_state_match e le' m' f k out S)
/\
  (forall m fd args t m' res sz,
   eval_funcall ge function_entry m fd args t m' res sz ->
   forall k,
   is_call_cont k ->
   star (fun ge' => step fn_stack_requirements ge' function_entry) ge (Callstate fd args k m sz) t (Returnstate res k m')).

Lemma exec_stmt_steps:
   forall e le m s t le' m' out,
   exec_stmt ge function_entry e le m s t le' m' out ->
   forall f k, exists S,
   star (fun ge' => step fn_stack_requirements ge' function_entry) ge (State f s k e le m) t S
   /\ outcome_state_match e le' m' f k out S.


Lemma eval_funcall_steps:
   forall m fd args t m' res sz,
   eval_funcall ge function_entry m fd args t m' res sz ->
   forall k,
   is_call_cont k ->
   star (fun ge' => step fn_stack_requirements ge' function_entry) ge (Callstate fd args k m sz) t (Returnstate res k m').

Definition order (x y: unit) := False.

Lemma evalinf_funcall_forever:
  forall m fd args T k sz,
  evalinf_funcall ge function_entry m fd args T sz ->
  forever_N (fun ge' => step fn_stack_requirements ge' function_entry) order ge tt (Callstate fd args k m sz) T.

End WITHFUNCTIONENTRY.


Theorem bigstep_semantics_sound:
  bigstep_sound (bigstep_semantics function_entry1 prog) (semantics1 fn_stack_requirements prog).

End BIGSTEP_TO_TRANSITIONS.

End WITHEXTCALLS.