Module Common
Require
Import
Utf8
Coqlib
Registers
Integers
.
Require
Import
MIR
INJECT
.
Object model.
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
omifpr
h
f
d
is an instruction that computes in register
d
if according to the header in register
h
, field
f
is a pointer.
}.
Information needed to compile a MIR program.
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
).