Module Common

Require Import Utf8 Coqlib Registers Integers.

Require Import MIR INJECT.

Record object_model : Type :=
{ om_object_size : positive
; om_heap_size : positive
; om_is_field_pointer : header -> N -> bool
; om_is_field_pointer_stmt : reg -> reg -> reg -> INJECT.statement
}.

Record backend_info :=
{ bi_abort: Ast.ident
; bi_main: Ast.ident
; bi_thread_main: Ast.ident
; bi_translate_abort_msg : abort_msg -> int
; bi_leak : Ast.ident
; bi_translate_leak : INJECT.leak -> int
; bi_show_leak: bool

; bi_max_mutators: int
; bi_bucket_size: int

; bi_mutator_lock: Ast.ident
; bi_mutator_data : Ast.ident

; bi_free_list: Ast.ident

; bi_heap: Ast.ident

; bi_collector: Ast.ident
; bi_collector_stack: Ast.ident
; bi_collector_stack_size: int

; bi_ptr_globals: Ast.ident
; bi_int_globals: Ast.ident

; bi_enforce_sc: bool

}.

Definition ok_bi : backend_info → Prop :=
  fun b => ¬ b.(bi_show_leak).