Global environments are a component of the dynamic semantics of all languages involved in the compiler. A global environment maps symbol names (names of functions and of global variables) to the corresponding memory addresses. It also maps memory addresses of functions to the corresponding function descriptions. Global environments, along with the initial memory state at the beginning of program execution, are built from the program of interest, as follows:

A distinct memory address is assigned to each function of the program. These function addresses use negative numbers to distinguish them from addresses of memory blocks. The associations of function name to function address and function address to function description are recorded in the global environment.
For each global variable, a memory block is allocated and associated to the name of the variable.

These operations reflect (at a high level of abstraction) what takes place during program linking and program loading in a real operating system.

Require Recdef.
Require Import Zwf.
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.

Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.

Local Open Scope pair_scope.
Local Open Scope error_monad_scope.

Set Implicit Arguments.

Auxiliary function for initialization of global variables.

Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
  if zle n 0 then Some m else
    match Mem.store Mint8unsigned m b p Vzero with
    | Some m' => store_zeros m' b (p + 1) (n - 1)
    | None => None
    end.

Proof.

intros. red. omega.
apply Zwf_well_founded.
Qed.

Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.

Symbol environments

Symbol environments are a restricted view of global environments, focusing on symbol names and their associated blocks. They do not contain mappings from blocks to function or variable definitions.

Module Senv.

Record t: Type := mksenv {

Operations

  find_symbol: ident -> option block;
  public_symbol: ident -> bool;
  invert_symbol: block -> option ident;
  block_is_volatile: block -> bool;
  nextblock: block;

Properties

  find_symbol_injective:
    forall id1 id2 b, find_symbol id1 = Some b -> find_symbol id2 = Some b -> id1 = id2;
  invert_find_symbol:
    forall id b, invert_symbol b = Some id -> find_symbol id = Some b;
  find_invert_symbol:
    forall id b, find_symbol id = Some b -> invert_symbol b = Some id;
  public_symbol_exists:
    forall id, public_symbol id = true -> exists b, find_symbol id = Some b;
  find_symbol_below:
    forall id b, find_symbol id = Some b -> Plt b nextblock;
  block_is_volatile_below:
    forall b, block_is_volatile b = true -> Plt b nextblock
}.

Definition symbol_address (ge: t) (id: ident) (ofs: int) : val :=
  match find_symbol ge id with
  | Some b => Vptr b ofs
  | None => Vundef
  end.

Theorem shift_symbol_address:
  forall ge id ofs n,
  symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).

Proof.

intros. unfold symbol_address. destruct (find_symbol ge id); auto.
Qed.

End Senv.

Module Genv.

Global environments

Section GENV.

Variable F: Type. (* The type of function descriptions *)
Variable V: Type. (* The type of information attached to variables *)

The type of global environments.

Record t: Type := mkgenv {
  genv_public: list ident; (* which symbol names are public *)
  genv_symb: PTree.t block; (* mapping symbol -> block *)
  genv_funs: PTree.t F; (* mapping function pointer -> definition *)
  genv_vars: PTree.t (globvar V); (* mapping variable pointer -> info *)
  genv_next: block; (* next symbol pointer *)
  genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> Plt b genv_next;
  genv_funs_range: forall b f, PTree.get b genv_funs = Some f -> Plt b genv_next;
  genv_vars_range: forall b v, PTree.get b genv_vars = Some v -> Plt b genv_next;
  genv_funs_vars: forall b1 b2 f v,
    PTree.get b1 genv_funs = Some f -> PTree.get b2 genv_vars = Some v -> b1 <> b2;
  genv_vars_inj: forall id1 id2 b,
    PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
}.

Lookup functions

find_symbol ge id returns the block associated with the given name, if any

Definition find_symbol (ge: t) (id: ident) : option block :=
PTree.get id ge.(genv_symb).

symbol_address ge id ofs returns a pointer into the block associated with id, at byte offset ofs. Vundef is returned if no block is associated to id.

Definition symbol_address (ge: t) (id: ident) (ofs: int) : val :=
  match find_symbol ge id with
  | Some b => Vptr b ofs
  | None => Vundef
  end.

public_symbol ge id says whether the name id is public and defined.

Definition public_symbol (ge: t) (id: ident) : bool :=
  match find_symbol ge id with
  | None => false
  | Some _ => In_dec ident_eq id ge.(genv_public)
  end.

find_funct_ptr ge b returns the function description associated with the given address.

Definition find_funct_ptr (ge: t) (b: block) : option F :=
PTree.get b ge.(genv_funs).

find_funct is similar to find_funct_ptr, but the function address is given as a value, which must be a pointer with offset 0.

Definition find_funct (ge: t) (v: val) : option F :=
  match v with
  | Vptr b ofs => if Int.eq_dec ofs Int.zero then find_funct_ptr ge b else None
  | _ => None
  end.

invert_symbol ge b returns the name associated with the given block, if any

Definition invert_symbol (ge: t) (b: block) : option ident :=
  PTree.fold
    (fun res id b' => if eq_block b b' then Some id else res)
    ge.(genv_symb) None.

find_var_info ge b returns the information attached to the variable at address b.

Definition find_var_info (ge: t) (b: block) : option (globvar V) :=
PTree.get b ge.(genv_vars).

block_is_volatile ge b returns true if b points to a global variable of volatile type, false otherwise.

Definition block_is_volatile (ge: t) (b: block) : bool :=
  match find_var_info ge b with
  | None => false
  | Some gv => gv.(gvar_volatile)
  end.

Constructing the global environment

Program Definition add_global (ge: t) (idg: ident * globdef F V) : t :=
  @mkgenv
    ge.(genv_public)
    (PTree.set idg#1 ge.(genv_next) ge.(genv_symb))
    (match idg#2 with
     | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs)
     | Gvar v => ge.(genv_funs)
     end)
    (match idg#2 with
     | Gfun f => ge.(genv_vars)
     | Gvar v => PTree.set ge.(genv_next) v ge.(genv_vars)
     end)
    (Psucc ge.(genv_next))
    _ _ _ _ _.

Next Obligation.

  destruct ge; simpl in *.
  rewrite PTree.gsspec in H. destruct (peq id i). inv H. apply Plt_succ.
  apply Plt_trans_succ; eauto.
Qed.

Next Obligation.

  destruct ge; simpl in *.
  destruct g.
  rewrite PTree.gsspec in H.
  destruct (peq b genv_next0). inv H. apply Plt_succ.
  apply Plt_trans_succ; eauto.
  apply Plt_trans_succ; eauto.
Qed.

Next Obligation.

  destruct ge; simpl in *.
  destruct g.
  apply Plt_trans_succ; eauto.
  rewrite PTree.gsspec in H.
  destruct (peq b genv_next0). inv H. apply Plt_succ.
  apply Plt_trans_succ; eauto.
Qed.

Next Obligation.

  destruct ge; simpl in *.
  destruct g.
  rewrite PTree.gsspec in H.
  destruct (peq b1 genv_next0). inv H.
  apply sym_not_equal; apply Plt_ne; eauto.
  eauto.
  rewrite PTree.gsspec in H0.
  destruct (peq b2 genv_next0). inv H0.
  apply Plt_ne; eauto.
  eauto.
Qed.

Next Obligation.

  destruct ge; simpl in *.
  rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0.
  destruct (peq id1 i); destruct (peq id2 i).
  congruence.
  inv H. eelim Plt_strict. eapply genv_symb_range0; eauto.
  inv H0. eelim Plt_strict. eapply genv_symb_range0; eauto.
  eauto.
Qed.

Definition add_globals (ge: t) (gl: list (ident * globdef F V)) : t :=
  List.fold_left add_global gl ge.

Lemma add_globals_app:
  forall gl2 gl1 ge,
  add_globals ge (gl1 ++ gl2) = add_globals (add_globals ge gl1) gl2.

Proof.

induction gl1; simpl; intros. auto. rewrite IHgl1; auto.
Qed.

Program Definition empty_genv (pub: list ident): t :=
@mkgenv pub (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _.

Next Obligation.