@ -33,7 +33,7 @@ Datatype `
label = Lab string ` ;
label = Lab string ` ;
Datatype `
Datatype `
loc_var = Loc string ` ;
reg = Reg string ` ;
Datatype `
Datatype `
glob_var = GlobName string ` ;
glob_var = GlobName string ` ;
@ -51,7 +51,7 @@ Datatype `
| UndefC ` ;
| UndefC ` ;
Datatype `
Datatype `
arg = Constant const | Variable loc_va r` ;
arg = Constant const | Variable reg ` ;
type_abbrev ( " t a r g " , ``: ty # arg `` ) ;
type_abbrev ( " t a r g " , ``: ty # arg `` ) ;
@ -63,29 +63,29 @@ Datatype `
(* T e r m i n a t o r s *)
(* T e r m i n a t o r s *)
| Ret targ
| Ret targ
| Br arg label label
| Br arg label label
| Invoke loc_va r ty arg ( targ list ) label label
| Invoke reg ty arg ( targ list ) label label
| Unreachable
| Unreachable
(* N o n - t e r m i n a t o r s *)
(* N o n - t e r m i n a t o r s *)
| Sub loc_va r bool bool ty arg arg
| Sub reg bool bool ty arg arg
| Extractvalue loc_va r targ ( const list )
| Extractvalue reg targ ( const list )
| Insertvalue loc_va r targ targ ( const list )
| Insertvalue reg targ targ ( const list )
| Alloca loc_va r ty targ
| Alloca reg ty targ
| Load loc_va r ty targ
| Load reg ty targ
| Store targ targ
| Store targ targ
| Gep loc_va r targ ( targ list )
| Gep reg targ ( targ list )
| Ptrtoint loc_va r targ ty
| Ptrtoint reg targ ty
| Inttoptr loc_va r targ ty
| Inttoptr reg targ ty
| Icmp cond ty arg arg
| Icmp cond ty arg arg
| Call loc_va r ty fun_name ( targ list )
| Call reg ty fun_name ( targ list )
(* C + + r u n t i m e f u n c t i o n s *)
(* C + + r u n t i m e f u n c t i o n s *)
| Cxa_allocate_exn loc_va r arg
| Cxa_allocate_exn reg arg
| Cxa_throw arg arg arg
| Cxa_throw arg arg arg
| Cxa_begin_catch loc_va r arg
| Cxa_begin_catch reg arg
| Cxa_end_catch
| Cxa_end_catch
| Cxa_get_exception_ptr loc_va r arg ` ;
| Cxa_get_exception_ptr reg arg ` ;
Datatype `
Datatype `
phi = Phi loc_va r ty ( label option |-> arg ) ` ;
phi = Phi reg ty ( label option |-> arg ) ` ;
Datatype `
Datatype `
clause = Catch targ ` ;
clause = Catch targ ` ;
@ -104,7 +104,7 @@ Datatype `
Datatype `
Datatype `
def =
def =
<| r : ty ;
<| r : ty ;
params : loc_va r list ;
params : reg list ;
(* N o n e - > e n t r y b l o c k , a n d S o m e n a m e - > n o n - e n t r y b l o c k *)
(* N o n e - > e n t r y b l o c k , a n d S o m e n a m e - > n o n - e n t r y b l o c k *)
blocks : label option |-> block |>` ;
blocks : label option |-> block |>` ;
@ -140,14 +140,14 @@ Datatype `
pc = <| f : fun_name ; b : label option ; i : num |>` ;
pc = <| f : fun_name ; b : label option ; i : num |>` ;
Datatype `
Datatype `
frame = <| ret : pc ; saved_locals : loc_va r |-> pv ; result_var : loc_va r; stack_allocs : addr list |>` ;
frame = <| ret : pc ; saved_locals : reg |-> pv ; result_var : reg ; stack_allocs : addr list |>` ;
Datatype `
Datatype `
state =
state =
<| ip : pc ;
<| ip : pc ;
(* K e e p t h e s i z e o f t h e g l o b a l w i t h i t s m e m o r y a d d r e s s *)
(* K e e p t h e s i z e o f t h e g l o b a l w i t h i t s m e m o r y a d d r e s s *)
globals : glob_var |-> ( num # word64 ) ;
globals : glob_var |-> ( num # word64 ) ;
locals : loc_va r |-> pv ;
locals : reg |-> pv ;
stack : frame list ;
stack : frame list ;
(* T h e s e t o f a l l o c a t e d r a n g e s . T h e b o o l i n d i c a t e s w h e t h e r t h e r a n g e i s
(* T h e s e t o f a l l o c a t e d r a n g e s . T h e b o o l i n d i c a t e s w h e t h e r t h e r a n g e i s
* free - able or not * )
* free - able or not * )