Module MutrecB

Require Import AST Coqlib.
Require Import Asm.
Require Import sflib.
Require Import AsmC Mod.
Require Import MutrecHeader Integers.

Definition _memoized : ident := 60%positive.
Definition lb0: label := 1%positive.
Definition lb1: label := 2%positive.
Definition lb2: label := 3%positive.

Definition v_memoized := {|
  gvar_info := tt;
  gvar_init := (Init_int32 (Int.zero) :: Init_int32 (Int.zero) :: nil);
  gvar_readonly := false;
  gvar_volatile := false
|}.

Definition code: list instruction :=
 [
   Pallocframe 24 (Ptrofs.repr 16) Ptrofs.zero ;
     Pmov_mr_a (Addrmode (Some RSP) None (inl 8)) RBX;

     Pmov_rr RBX RDI ;
     Ptestl_rr RBX RBX ;
     Pjcc Cond_ne lb0;
     Pxorl_r RAX;
     Pjmp_l lb1;

     Plabel lb0 ;
     Pmovl_rm RAX (Addrmode None None (inr (_memoized, Ptrofs.zero)));
     Pcmpl_rr RBX RAX;
     Pjcc Cond_e lb2;
     Pleal RDI (Addrmode (Some RBX) None (inl (- 1)));

     Pcall_s f_id (mksignature [Tint] (Some Tint) cc_default true);

     Pleal RAX (Addrmode (Some RAX) (Some (RBX, 1)) (inl 0));
     Pmovl_mr (Addrmode None None (inr (_memoized, Ptrofs.zero))) RBX;
     Pmovl_mr (Addrmode None None (inr (_memoized, Ptrofs.repr 4))) RAX;
     Pjmp_l lb1;

     Plabel lb2 ;
     Pmovl_rm RAX (Addrmode None None (inr (_memoized, Ptrofs.repr 4)));

     Plabel lb1 ;
     Pmov_rm_a RBX (Addrmode (Some RSP) None (inl 8));
     Pfreeframe 24 (Ptrofs.repr 16) Ptrofs.zero;
     Pret
 ].

Definition func_g: function :=
  mkfunction (mksignature [Tint] (Some Tint) cc_default true) code
.

Definition global_definitions : list (ident * globdef fundef unit) :=
((f_id,
   Gfun(External (EF_external "f"
                   (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default true)))) :: (_memoized, Gvar v_memoized) ::
 (g_id, Gfun(Internal func_g)) :: nil).

Definition public_idents : list ident :=
(f_id :: g_id :: nil).

Definition prog: program := mkprogram global_definitions public_idents main_id.

Definition md: Mod.t := AsmC.module prog.