Module DemoTarget

Require Import AST Coqlib.
Require Import Asm.
Require Import sflib.
Require Import AsmC Mod.
Require Import DemoHeader.

Definition lb0: label := 1%positive.
Definition code: list instruction :=
  [
    Ptestq_rr RDI RDI ;
      Pjcc Cond_s lb0 ;
      Pxorpd_f XMM0 ;
      Pcvtsl2sd_fr XMM0 RDI ;
      Pret ;

      Plabel lb0 ;
      Pmov_rr RAX RDI ;
      Pshrq_ri RAX Integers.Int.one ;
      Pandq_ri RDI Integers.Int64.one ;
      Porq_rr RAX RDI ;
      Pxorpd_f XMM0 ;
      Pcvtsl2sd_fr XMM0 RAX ;
      Paddd_ff XMM0 XMM0 ;
      Pret
  ].

Definition func: function :=
  mkfunction (mksignature [Tlong] (Some Tfloat) cc_default true) code
.

Definition prog: program := mkprogram [(func_id, (Gfun (Internal func)))] [func_id ; main_id] main_id.

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

Hint Unfold md prog func code.