Module DataStructures

Require Import Coqlib Integers.

Require Import MIR Common.

Section DATASTRUCTURES.

  Variable bi : backend_info.

Definition color_BW := Int.repr (15 * 16 * 16).
Definition color_mask := Int.repr ((15 * 16 + 15) * 16).
Definition color_blue := Int.mone.

Definition ms_available := Int.repr 0.
Definition ms_quick := Int.repr 1.
Definition ms_running := Int.repr 2.

Definition ms_async := Int.repr 0.
Definition ms_sync1 := Int.repr 1.
Definition ms_sync2 := Int.repr 2.

Definition cs_resting := Int.repr 0.
Definition cs_clear_or_marking := Int.repr 1.
Definition cs_tracing := Int.repr 2.
Definition cs_sweeping := Int.repr 3.

Definition hf_next := Int.repr 0.
Definition hf_size := Int.repr 4.
Definition hf_roots := Int.repr 8.

Definition blk_hdr := Int.repr 0.
Definition blk_color:= Int.repr 4.
Definition blk_mon := Int.repr 8.
Definition blk_next := Int.repr 12.
Definition blk_first_field := Int.repr 16.

Definition object_byte_size om : int :=
  Int.add blk_first_field
  (Int.repr (Zpos om.(om_object_size) * 4)).

Definition offset_of_field (f:field) : int :=
  match f with
    | Field i _ _ => Int.add blk_first_field (Int.repr (Z_of_N i * 4))
  end.

Definition heap_byte_size om : int :=
  Int.mul
  (Int.repr (Zpos om.(om_heap_size)))
  (object_byte_size om).

Definition md_status := Int.repr 0.
Definition md_phase := Int.repr 4.
Definition md_alloc_c:= Int.repr 12.
Definition md_shadow := Int.repr 16.
Definition md_fp := Int.repr 20.
Definition md_arg := Int.repr 24.
Definition md_next_write := Int.repr 28.
Definition md_next_read := Int.repr 32.
Definition md_bucket := Int.repr 36.

Definition sizeof_md := Int.add md_bucket bi.(bi_bucket_size).

Definition md_size : int :=
  Int.mul bi.(bi_max_mutators) sizeof_md.

Definition cd_phase := Int.repr 0.
Definition cd_mark_c := Int.repr 4.

Definition sizeof_cd : int := Int.repr 8.

End DATASTRUCTURES.