Library compcert.backend.Linear


The Linear intermediate language: abstract syntax and semantcs
The Linear language is a variant of LTL where control-flow is not expressed as a graph of basic blocks, but as a linear list of instructions with explicit labels and ``goto'' instructions.

Require Import Coqlib.
Require Import AST Integers Values Memory Events Globalenvs Smallstep.
Require Import Op Locations LTL Conventions.

Abstract syntax

Operational semantics

Looking up labels in the instruction list.

Definition is_label (lbl: label) (instr: instruction) : bool :=
  match instr with
  | Llabel lbl'if peq lbl lbl' then true else false
  | _false
  end.

Lemma is_label_correct:
   lbl instr,
  if is_label lbl instr then instr = Llabel lbl else instr Llabel lbl.
Proof.
  intros. destruct instr; simpl; try discriminate.
  case (peq lbl l); intro; congruence.
Qed.

find_label lbl c returns a list of instruction, suffix of the code c, that immediately follows the Llabel lbl pseudo-instruction. If the label lbl is multiply-defined, the first occurrence is retained. If the label lbl is not defined, None is returned.

Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
  match c with
  | nilNone
  | i1 :: ilif is_label lbl i1 then Some il else find_label lbl il
  end.

Definition find_function (ge: genv) (ros: mreg + ident) (rs: locset) : option fundef :=
  match ros with
  | inl rGenv.find_funct ge (rs (R r))
  | inr symb
      match Genv.find_symbol ge symb with
      | NoneNone
      | Some bGenv.find_funct_ptr ge b
      end
  end.

Linear execution states.

Inductive stackframe: Type :=
  | Stackframe:
       (f: function)
             (sp: val)
             (rs: locset)
             (c: code),
      stackframe.

Inductive state `{memory_model_ops: Mem.MemoryModelOps}: Type :=
  | State:
       (stack: list stackframe)
             (f: function)
             (sp: val)
             (c: code)
             (rs: locset)
             (m: mem),
      state
  | Callstate:
       (stack: list stackframe)
             (f: fundef)
             (rs: locset)
             (m: mem),
      state
  | Returnstate:
       (stack: list stackframe)
             (rs: locset)
             (m: mem),
      state.

Section WITHEXTERNALCALLSOPS.
Context `{external_calls_prf: ExternalCalls}.

Section RELSEM.

parent_locset cs returns the mapping of values for locations of the caller function.

Variable parent_lm: locset.

Definition parent_locset (stack: list stackframe) : locset :=
  match stack with
  | nilparent_lm
  | Stackframe f sp ls c :: stack'ls
  end.

Variable ge: genv.

Inductive step: state trace state Prop :=
  | exec_Lgetstack:
       s f sp sl ofs ty dst b rs m rs',
      rs' = Locmap.set (R dst) (rs (S sl ofs ty)) (undef_regs (destroyed_by_getstack sl) rs)
      step (State s f sp (Lgetstack sl ofs ty dst :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lsetstack:
       s f sp src sl ofs ty b rs m rs',
      rs' = Locmap.set (S sl ofs ty) (rs (R src)) (undef_regs (destroyed_by_setstack ty) rs)
      step (State s f sp (Lsetstack src sl ofs ty :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lop:
       s f sp op args res b rs m v rs',
      eval_operation ge sp op (reglist rs args) m = Some v
      rs' = Locmap.set (R res) v (undef_regs (destroyed_by_op op) rs)
      step (State s f sp (Lop op args res :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lload:
       s f sp chunk addr args dst b rs m a v rs',
      eval_addressing ge sp addr (reglist rs args) = Some a
      Mem.loadv chunk m a = Some v
      rs' = Locmap.set (R dst) v (undef_regs (destroyed_by_load chunk addr) rs)
      step (State s f sp (Lload chunk addr args dst :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lstore:
       s f sp chunk addr args src b rs m m' a rs',
      eval_addressing ge sp addr (reglist rs args) = Some a
      Mem.storev chunk m a (rs (R src)) = Some m'
      rs' = undef_regs (destroyed_by_store chunk addr) rs
      step (State s f sp (Lstore chunk addr args src :: b) rs m)
        E0 (State s f sp b rs' m')
  | exec_Lcall:
       s f sp sig ros b rs m f',
      find_function ge ros rs = Some f'
      sig = funsig f'
      step (State s f sp (Lcall sig ros :: b) rs m)
        E0 (Callstate (Stackframe f sp rs b:: s) f' rs m)
  | exec_Ltailcall:
       s f stk sig ros b rs m rs' f' m',
      rs' = return_regs (parent_locset s) rs
      find_function ge ros rs' = Some f'
      sig = funsig f'
      Mem.free m stk 0 f.(fn_stacksize) = Some m'
      step (State s f (Vptr stk Ptrofs.zero) (Ltailcall sig ros :: b) rs m)
        E0 (Callstate s f' rs' m')
  | exec_Lbuiltin:
       s f sp rs m ef args res b vargs t vres rs' m',
      eval_builtin_args ge rs sp m args vargs
      external_call ef ge vargs m t vres m'
      rs' = Locmap.setres res vres (undef_regs (destroyed_by_builtin ef) rs)
       BUILTIN_ENABLED : builtin_enabled ef,
        step (State s f sp (Lbuiltin ef args res :: b) rs m)
             t (State s f sp b rs' m')
  | exec_Llabel:
       s f sp lbl b rs m,
      step (State s f sp (Llabel lbl :: b) rs m)
        E0 (State s f sp b rs m)
  | exec_Lgoto:
       s f sp lbl b rs m b',
      find_label lbl f.(fn_code) = Some b'
      step (State s f sp (Lgoto lbl :: b) rs m)
        E0 (State s f sp b' rs m)
  | exec_Lcond_true:
       s f sp cond args lbl b rs m rs' b',
      eval_condition cond (reglist rs args) m = Some true
      rs' = undef_regs (destroyed_by_cond cond) rs
      find_label lbl f.(fn_code) = Some b'
      step (State s f sp (Lcond cond args lbl :: b) rs m)
        E0 (State s f sp b' rs' m)
  | exec_Lcond_false:
       s f sp cond args lbl b rs m rs',
      eval_condition cond (reglist rs args) m = Some false
      rs' = undef_regs (destroyed_by_cond cond) rs
      step (State s f sp (Lcond cond args lbl :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Ljumptable:
       s f sp arg tbl b rs m n lbl b' rs',
      rs (R arg) = Vint n
      list_nth_z tbl (Int.unsigned n) = Some lbl
      find_label lbl f.(fn_code) = Some b'
      rs' = undef_regs (destroyed_by_jumptable) rs
      step (State s f sp (Ljumptable arg tbl :: b) rs m)
        E0 (State s f sp b' rs' m)
  | exec_Lreturn:
       s f stk b rs m m',
      Mem.free m stk 0 f.(fn_stacksize) = Some m'
      step (State s f (Vptr stk Ptrofs.zero) (Lreturn :: b) rs m)
        E0 (Returnstate s (return_regs (parent_locset s) rs) m')
  | exec_function_internal:
       s f rs m rs' m' stk,
      Mem.alloc m 0 f.(fn_stacksize) = (m', stk)
      rs' = undef_regs destroyed_at_function_entry (call_regs rs)
      step (Callstate s (Internal f) rs m)
        E0 (State s f (Vptr stk Ptrofs.zero) f.(fn_code) rs' m')
  | exec_function_external:
       s ef args res rs1 rs2 m t m',
      args = map (fun pLocmap.getpair p rs1) (loc_arguments (ef_sig ef))
      external_call ef ge args m t res m'
      rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1
      step (Callstate s (External ef) rs1 m)
         t (Returnstate s rs2 m')
  | exec_return:
       s f sp rs0 c rs m,
      step (Returnstate (Stackframe f sp rs0 c :: s) rs m)
        E0 (State s f sp c rs m).

End RELSEM.

Inductive initial_state (p: program): state Prop :=
  | initial_state_intro: 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 (Locmap.init Vundef) m0).

Inductive final_state: state int Prop :=
  | final_state_intro: rs m retcode,
      Locmap.getpair (map_rpair R (loc_result signature_main)) rs = Vint retcode
      final_state (Returnstate nil rs m) retcode.

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

End WITHEXTERNALCALLSOPS.