Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 357 insertions, 0 deletions

diff --git a/backend/LTL.v b/backend/LTL.v
new file mode 100644
index 00000000..2c36cba9
--- /dev/null
+++ b/backend/LTL.v
@@ -0,0 +1,357 @@
+(** The LTL intermediate language: abstract syntax and semantics.
+
+  LTL (``Location Transfer Language'') is the target language
+  for register allocation and the source language for linearization. *)
+
+Require Import Relations.
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Locations.
+Require Conventions.
+
+(** * Abstract syntax *)
+
+(** LTL is close to RTL, but uses locations instead of pseudo-registers,
+   and basic blocks instead of single instructions as nodes of its
+   control-flow graph. *)
+
+Definition node := positive.
+
+(** A basic block is a sequence of instructions terminated by
+    a [Bgoto], [Bcond] or [Breturn] instruction.  (This invariant
+    is enforced by the following inductive type definition.)
+    The instructions behave like the similarly-named instructions
+    of RTL.  They take machine registers (type [mreg]) as arguments
+    and results.  Two new instructions are added: [Bgetstack]
+    and [Bsetstack], which are ``move'' instructions between
+    a machine register and a stack slot. *)
+
+Inductive block: Set :=
+  | Bgetstack: slot -> mreg -> block -> block
+  | Bsetstack: mreg -> slot -> block -> block
+  | Bop: operation -> list mreg -> mreg -> block -> block
+  | Bload: memory_chunk -> addressing -> list mreg -> mreg -> block -> block
+  | Bstore: memory_chunk -> addressing -> list mreg -> mreg -> block -> block
+  | Bcall: signature -> mreg + ident -> block -> block
+  | Bgoto: node -> block
+  | Bcond: condition -> list mreg -> node -> node -> block
+  | Breturn: block.
+
+Definition code: Set := PTree.t block.
+
+(** Unlike in RTL, parameter passing (passing values of the arguments
+  to a function call to the parameters of the called function) is done
+  via conventional locations (machine registers and stack slots).
+  Consequently, the [Bcall] instruction has no list of argument registers,
+  and function descriptions have no list of parameter registers. *)
+
+Record function: Set := mkfunction {
+  fn_sig: signature;
+  fn_stacksize: Z;
+  fn_code: code;
+  fn_entrypoint: node;
+  fn_code_wf:
+    forall (pc: node), Plt pc (Psucc fn_entrypoint) \/ fn_code!pc = None
+}.
+
+Definition program := AST.program function.
+
+(** * Operational semantics *)
+
+Definition genv := Genv.t function.
+Definition locset := Locmap.t.
+
+Section RELSEM.
+
+(** Calling conventions are reflected at the level of location sets
+  (environments mapping locations to values) by the following two 
+  functions.  
+
+  [call_regs caller] returns the location set at function entry,
+  as a function of the location set [caller] of the calling function.
+- Machine registers have the same values as in the caller.
+- Incoming stack slots (used for parameter passing) have the same
+  values as the corresponding outgoing stack slots (used for argument
+  passing) in the caller.
+- Local and outgoing stack slots are initialized to undefined values.
+*) 
+
+Definition call_regs (caller: locset) : locset :=
+  fun (l: loc) =>
+    match l with
+    | R r => caller (R r)
+    | S (Local ofs ty) => Vundef
+    | S (Incoming ofs ty) => caller (S (Outgoing ofs ty))
+    | S (Outgoing ofs ty) => Vundef
+    end.
+
+(** [return_regs caller callee] returns the location set after
+  a call instruction, as a function of the location set [caller]
+  of the caller before the call instruction and of the location
+  set [callee] of the callee at the return instruction.
+- Callee-save machine registers have the same values as in the caller
+  before the call.
+- Caller-save and temporary machine registers have the same values
+  as in the callee at the return point.
+- Stack slots have the same values as in the caller before the call.
+*)
+
+Definition return_regs (caller callee: locset) : locset :=
+  fun (l: loc) =>
+    match l with
+    | R r =>
+        if In_dec Loc.eq (R r) Conventions.temporaries then
+          callee (R r)
+        else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
+          callee (R r)
+        else
+          caller (R r)
+    | S s => caller (S s)
+    end.
+
+Variable ge: genv.
+
+Definition find_function (ros: mreg + ident) (rs: locset) : option function :=
+  match ros with
+  | inl r => Genv.find_funct ge (rs (R r))
+  | inr symb =>
+      match Genv.find_symbol ge symb with
+      | None => None
+      | Some b => Genv.find_funct_ptr ge b
+      end
+  end.
+
+Definition reglist (rl: list mreg) (rs: locset) : list val :=
+  List.map (fun r => rs (R r)) rl.
+
+(** The dynamic semantics of LTL, like that of RTL, is a combination
+  of small-step transition semantics and big-step semantics.
+  Function calls are treated in big-step style so that they appear
+  as a single transition in the caller function.  Other instructions
+  are treated in purely small-step style, as a single transition.
+
+  The introduction of basic blocks increases the number of inductive
+  predicates needed to express the semantics:
+- [exec_instr ge sp b ls m b' ls' m'] is the execution of the first
+  instruction of block [b].  [b'] is the remainder of the block.
+- [exec_instrs ge sp b ls m b' ls' m'] is similar, but executes
+  zero, one or several instructions at the beginning of block [b].
+- [exec_block ge sp b ls m out ls' m'] executes all instructions
+  of block [b].  The outcome [out] is either [Cont s], indicating
+  that the block terminates by branching to block labeled [s],
+  or [Return], indicating that the block terminates by returning
+  from the current function.
+- [exec_blocks ge code sp pc ls m out ls' m'] executes a sequence
+  of zero, one or several blocks, starting at the block labeled [pc].
+  [code] is the control-flow graph for the current function.
+  The outcome [out] indicates how the last block in this sequence
+  terminates: by branching to another block or by returning from the
+  function.
+- [exec_function ge f ls m ls' m'] executes the body of function [f],
+  from its entry point to the first [Lreturn] instruction encountered.
+
+  In all these predicates, [ls] and [ls'] are the location sets
+  (values of locations) at the beginning and end of the transitions,
+  respectively.
+*)
+
+Inductive outcome: Set :=
+  | Cont: node -> outcome
+  | Return: outcome.
+
+Inductive exec_instr: val ->
+                      block -> locset -> mem ->
+                      block -> locset -> mem -> Prop :=
+  | exec_Bgetstack:
+      forall sp sl r b rs m,
+      exec_instr sp (Bgetstack sl r b) rs m
+                    b (Locmap.set (R r) (rs (S sl)) rs) m
+  | exec_Bsetstack:
+      forall sp r sl b rs m,
+      exec_instr sp (Bsetstack r sl b) rs m
+                    b (Locmap.set (S sl) (rs (R r)) rs) m
+  | exec_Bop:
+      forall sp op args res b rs m v,
+      eval_operation ge sp op (reglist args rs) = Some v ->
+      exec_instr sp (Bop op args res b) rs m
+                    b (Locmap.set (R res) v rs) m
+  | exec_Bload:
+      forall sp chunk addr args dst b rs m a v,
+      eval_addressing ge sp addr (reglist args rs) = Some a ->
+      loadv chunk m a = Some v ->
+      exec_instr sp (Bload chunk addr args dst b) rs m
+                    b (Locmap.set (R dst) v rs) m
+  | exec_Bstore:
+      forall sp chunk addr args src b rs m m' a,
+      eval_addressing ge sp addr (reglist args rs) = Some a ->
+      storev chunk m a (rs (R src)) = Some m' ->
+      exec_instr sp (Bstore chunk addr args src b) rs m
+                    b rs m'
+  | exec_Bcall:
+      forall sp sig ros b rs m f rs' m',
+      find_function ros rs = Some f ->
+      sig = f.(fn_sig) ->
+      exec_function f rs m rs' m' ->
+      exec_instr sp (Bcall sig ros b) rs m
+                    b (return_regs rs rs') m'
+
+with exec_instrs: val ->
+                  block -> locset -> mem ->
+                  block -> locset -> mem -> Prop :=
+  | exec_refl:
+      forall sp b rs m,
+      exec_instrs sp b rs m b rs m
+  | exec_one:
+      forall sp b1 rs1 m1 b2 rs2 m2,
+      exec_instr sp b1 rs1 m1 b2 rs2 m2 ->
+      exec_instrs sp b1 rs1 m1 b2 rs2 m2
+  | exec_trans:
+      forall sp b1 rs1 m1 b2 rs2 m2 b3 rs3 m3,
+      exec_instrs sp b1 rs1 m1 b2 rs2 m2 ->
+      exec_instrs sp b2 rs2 m2 b3 rs3 m3 ->
+      exec_instrs sp b1 rs1 m1 b3 rs3 m3
+
+with exec_block: val ->
+                 block -> locset -> mem ->
+                 outcome -> locset -> mem -> Prop :=
+  | exec_Bgoto:
+      forall sp b rs m s rs' m',
+      exec_instrs sp b rs m (Bgoto s) rs' m' ->
+      exec_block sp b rs m (Cont s) rs' m'
+  | exec_Bcond_true:
+      forall sp b rs m cond args ifso ifnot rs' m',
+      exec_instrs sp b rs m (Bcond cond args ifso ifnot) rs' m' ->
+      eval_condition cond (reglist args rs') = Some true ->
+      exec_block sp b rs m (Cont ifso) rs' m'
+  | exec_Bcond_false:
+      forall sp b rs m cond args ifso ifnot rs' m',
+      exec_instrs sp b rs m (Bcond cond args ifso ifnot) rs' m' ->
+      eval_condition cond (reglist args rs') = Some false ->
+      exec_block sp b rs m (Cont ifnot) rs' m'
+  | exec_Breturn:
+      forall sp b rs m rs' m',
+      exec_instrs sp b rs m Breturn rs' m' ->
+      exec_block sp b rs m Return rs' m'
+
+with exec_blocks: code -> val ->
+                  node -> locset -> mem ->
+                  outcome -> locset -> mem -> Prop :=
+  | exec_blocks_refl:
+      forall c sp pc rs m,
+      exec_blocks c sp pc rs m (Cont pc) rs m
+  | exec_blocks_one:
+      forall c sp pc b m rs out rs' m',
+      c!pc = Some b ->
+      exec_block sp b rs m out rs' m' ->
+      exec_blocks c sp pc rs m out rs' m'
+  | exec_blocks_trans:
+      forall c sp pc1 rs1 m1 pc2 rs2 m2 out rs3 m3,
+      exec_blocks c sp pc1 rs1 m1 (Cont pc2) rs2 m2 ->
+      exec_blocks c sp pc2 rs2 m2 out rs3 m3 ->
+      exec_blocks c sp pc1 rs1 m1 out rs3 m3
+
+with exec_function: function -> locset -> mem ->
+                                locset -> mem -> Prop :=
+  | exec_funct:
+      forall f rs m m1 stk rs2 m2,
+      alloc m 0 f.(fn_stacksize) = (m1, stk) ->
+      exec_blocks f.(fn_code) (Vptr stk Int.zero)
+                  f.(fn_entrypoint) (call_regs rs) m1 Return rs2 m2 ->
+      exec_function f rs m rs2 (free m2 stk).
+
+End RELSEM.
+
+(** Execution of a whole program boils down to invoking its main
+  function.  The result of the program is the return value of the
+  main function, to be found in the machine register dictated
+  by the calling conventions. *)
+
+Definition exec_program (p: program) (r: val) : Prop :=
+  let ge := Genv.globalenv p in
+  let m0 := Genv.init_mem p in
+  exists b, exists f, exists rs, exists m,
+  Genv.find_symbol ge p.(prog_main) = Some b /\
+  Genv.find_funct_ptr ge b  = Some f /\
+  f.(fn_sig) = mksignature nil (Some Tint) /\
+  exec_function ge f (Locmap.init Vundef) m0 rs m /\
+  rs (R (Conventions.loc_result f.(fn_sig))) = r.
+
+(** We remark that the [exec_blocks] relation is stable if
+  the control-flow graph is extended by adding new basic blocks
+  at previously unused graph nodes. *)
+
+Section EXEC_BLOCKS_EXTENDS.
+
+Variable ge: genv.
+Variable c1 c2: code.
+Hypothesis EXT: forall pc, c2!pc = c1!pc \/ c1!pc = None.
+
+Lemma exec_blocks_extends:
+  forall sp pc1 rs1 m1 out rs2 m2,
+  exec_blocks ge c1 sp pc1 rs1 m1 out rs2 m2 ->
+  exec_blocks ge c2 sp pc1 rs1 m1 out rs2 m2.
+Proof.
+  induction 1. 
+  apply exec_blocks_refl.
+  apply exec_blocks_one with b. 
+    elim (EXT pc); intro; congruence. assumption.
+  eapply exec_blocks_trans; eauto.
+Qed.
+
+End EXEC_BLOCKS_EXTENDS.
+
+(** * Operations over LTL *)
+
+(** Computation of the possible successors of a basic block.
+  This is used for dataflow analyses. *)
+
+Fixpoint successors_aux (b: block) : list node :=
+  match b with
+  | Bgetstack s r b => successors_aux b
+  | Bsetstack r s b => successors_aux b
+  | Bop op args res b => successors_aux b
+  | Bload chunk addr args dst b => successors_aux b
+  | Bstore chunk addr args src b => successors_aux b
+  | Bcall sig ros b => successors_aux b
+  | Bgoto n => n :: nil
+  | Bcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Breturn => nil
+  end.
+
+Definition successors (f: function) (pc: node) : list node :=
+  match f.(fn_code)!pc with
+  | None => nil
+  | Some b => successors_aux b
+  end.
+
+Lemma successors_aux_invariant:
+  forall ge sp b rs m b' rs' m',
+  exec_instrs ge sp b rs m b' rs' m' ->
+  successors_aux b = successors_aux b'.
+Proof.
+  induction 1; simpl; intros.
+  reflexivity.
+  inversion H; reflexivity.
+  transitivity (successors_aux b2); auto.
+Qed.
+
+Lemma successors_correct:
+  forall ge f sp pc rs m pc' rs' m' b,
+  f.(fn_code)!pc = Some b ->
+  exec_block ge sp b rs m (Cont pc') rs' m' ->
+  In pc' (successors f pc).
+Proof.
+  intros. unfold successors. rewrite H. inversion H0.
+  rewrite (successors_aux_invariant _ _ _ _ _ _ _ _ H6); simpl.
+  tauto.
+  rewrite (successors_aux_invariant _ _ _ _ _ _ _ _ H2); simpl.
+  tauto.
+  rewrite (successors_aux_invariant _ _ _ _ _ _ _ _ H2); simpl.
+  tauto.
+Qed.