Require Export Memory.
Require Export Cminor.
Require Export Globalenvs.

Load param.

(*
Definition independent (block1 : Z) off1 (block2 : Z) off2 :=
block1 <> block2 \/ 
signed off1 + 4 <= signed off2 \/
signed off2 + 4 <= signed off1.
*)

Module Type Common_variables.

Parameters heap_start heap_end freelist_head : ident.

End Common_variables.

Module Type Common_hypotheses.

Declare Module CV : Common_variables.
Export CV.

(* The global environment contains all the global variables
   required for both garbage collectors. *)

Parameter genv : genv.

(* Two blocks and two constant pointers to them are required. In those blocks, 
   indeed, will be stored the pointers to the beginning and to the end of the heap.
*)

Parameters heap_start_block heap_end_block freelist_head_block : block. 

Axiom heap_start_heap_end_indep : heap_start_block <> heap_end_block.


Axiom freelist_head_heap_end_indep :
  freelist_head_block <> heap_end_block.
Axiom freelist_head_heap_start_indep : 
  freelist_head_block <> heap_start_block.


Axiom genv_heap_start : Genv.find_symbol genv heap_start = Some heap_start_block.
Axiom genv_heap_end : Genv.find_symbol genv heap_end = Some heap_end_block.
Axiom genv_freelist_head : Genv.find_symbol genv freelist_head = Some freelist_head_block.

Hint Resolve heap_start_heap_end_indep freelist_head_heap_end_indep freelist_head_heap_start_indep.


Record gc_invariants_param : Set := make_gc_invariants_param {
 freelist_head_value : val
}.

Record gc_invariants 
 (m : mem) (mp : memory_param) (up : used_abstraction_param) (p : gc_invariants_param) : Prop := gc_invariants_intro {

 (* these two might change because of pointer comparison rules *)
 gc_heap_start : Some (Vptr (memory_heap mp) (memory_hs mp)) = load Mint32 m heap_start_block 0;
 gc_heap_end : Some (Vptr (memory_heap mp) (memory_he mp)) = load Mint32 m heap_end_block 0;

 gc_used_hyp : used_abstraction m mp up;

 (* further hypotheses on the heap *)
(* gc_good_pointers : good_pointers_from_to m (memory_heap mp) (memory_hs mp) (memory_he mp);
   useless, consequence of gc_used_hyp *)
 gc_heap_valid : valid_block m (memory_heap mp); (* necessary, if hs = he *)
(*
  gc_heap_bounded : 
   min_signed <= low_bound m (memory_heap mp) /\
   high_bound m (memory_heap mp) <= max_signed ;
 *)

 heap_start_not_in_heap : heap_start_block <> (memory_heap mp);
 heap_end_not_in_heap : heap_end_block <> (memory_heap mp);

 rootpos_heap_start_indep : forall b i, member (b, i) (flatten (used_rootpos up)) -> b <> heap_start_block;
 rootpos_heap_end_indep : forall b i, member (b, i) (flatten (used_rootpos up)) -> b <> heap_end_block;
 rootpos_freelist_head_indep : forall b i, member (b, i) (flatten (used_rootpos up)) -> b <> freelist_head_block;

 freelist_head_not_in_heap : freelist_head_block <> memory_heap mp;
 freelist_head_defined : Some (freelist_head_value p) = load Mint32 m freelist_head_block 0;
 freelist_head_pointer_or_dumb : val_is_pointer_or_dumb_desc (freelist_head_value p)

}.

Hint Resolve gc_heap_start gc_heap_end gc_used_hyp gc_heap_valid heap_start_not_in_heap heap_end_not_in_heap 
 rootpos_heap_start_indep rootpos_heap_end_indep rootpos_freelist_head_indep 
freelist_head_not_in_heap freelist_head_defined freelist_head_pointer_or_dumb.

End Common_hypotheses.