vericert.hls.RTLBlock

Definition bb := list instr.

Definition bblock := @bblock bb.
Definition code := @code bb.
Definition function := @function bb.
Definition fundef := @fundef bb.
Definition program := @program bb.
Definition funsig := @funsig bb.
Definition stackframe := @stackframe bb.
Definition state := @state bb.
Definition genv := @genv bb.

Section RELSEM.

  Context (ge: genv).

  Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
    | exec_RBcons:
        forall state i state' state'' instrs sp,
        step_instr ge sp state i state' ->
        step_instr_list sp state' instrs state'' ->
        step_instr_list sp state (i :: instrs) state''
    | exec_RBnil:
        forall state sp,
        step_instr_list sp state nil state.

  Inductive step: state -> trace -> state -> Prop :=
  | exec_bblock:
    forall s f sp pc rs rs' m m' t s' bb pr pr',
      f.(fn_code)!pc = Some bb ->
      step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
      step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' ->
      step (State s f sp pc rs pr m) t s'
  | exec_function_internal:
    forall s f args m m' stk,
      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
      step (Callstate s (Internal f) args m)
        E0 (State s
                  f
                  (Vptr stk Ptrofs.zero)
                  f.(fn_entrypoint)
                  (init_regs args f.(fn_params))
                  (PMap.init false)
                  m')
  | exec_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')
  | exec_return:
    forall res f sp pc rs s vres m pr,
      step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
        E0 (State s f sp pc (rs#res <- vres) pr m).

End RELSEM.

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 = signature_main ->
      initial_state p (Callstate nil f nil m0).

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

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