Module MIRexample

Require Import Coqlib Integers Maps.

Require Import MIR MIRlow.

Require Import Common INJECT.

Local Open Scope positive_scope.

Definition om : object_model :=
  Build_object_model
    3 10240
    (fun h n => zlt (Z_of_N n) (Int.unsigned h))
    (fun h f d => Sop (Op.Ocmp (Op.Ccompu Clt)) (f::h::nil) d)
   .

Definition putchar_sig : signature :=
  mksignature FInteger (FInteger::nil) true.

Section EX0.

  Variables main putchar : Ast.ident.

  Notation param := 1.
  Notation r := 2.

  Definition ex0_main_c : list (node * instruction) :=
    (1, Mop r (OpIntConst (Int.repr 64)) nil 2)
  ::(2, Mcall r putchar_sig putchar (r::nil) 3)
  ::(3, Mret r)
  ::nil.

  Definition ex0_main_f : function :=
    mkfunction
      (mksignature FInteger (FPointer::nil) false)
      (param::nil)
      1%N
      (of_pair_list ex0_main_c)
      1.


  Definition ex0 : program :=
    mk_program
      (of_pair_list
         ((main, Ast.Internal (lower_mir ex0_main_f))
        ::(putchar, Ast.External (Ast.mkextfun putchar (Ast.mksignature (Ast.Tint::nil) None)))
        ::nil))
      main
      (of_pair_list nil).

End EX0.

Section EX1.
  Variables main sleep putchar : Ast.ident.

  Notation param := 1.
  Notation root := 2.
  Notation rint := 3.
  Notation rone := 4.
  Notation res := 5.

  Definition ex1_main_c : list (node * instruction) :=
    (1, Mop rone (OpIntConst Int.one) nil 2)
  ::(2, Mop rint (OpIntConst (Int.repr 64)) nil 3)
  ::(3, Mnew root Int.zero 4)
  ::(4, Mcall res putchar_sig putchar (rint::nil) 5)
  ::(5, Mcall res putchar_sig sleep (rone::nil) 6)
  ::(6, Mop rint OpAdd (rint::rone::nil) 7)
  ::(7, Mif (Op.Ccompuimm Cge (Int.repr 91%Z)) (rint::nil) 8 3)
  ::(8, Mret res)
  ::nil.

  Definition ex1_main_f : function :=
    mkfunction
      (mksignature FInteger (FPointer::nil) false)
      (param::nil)
      2%N
      (of_pair_list ex1_main_c)
      1.

  Definition ex1 : program :=
    mk_program
      (of_pair_list
         ((main, Ast.Internal (lower_mir ex1_main_f))
        ::(putchar, Ast.External (Ast.mkextfun putchar (Ast.mksignature (Ast.Tint::nil) None)))
        ::(sleep, Ast.External (Ast.mkextfun sleep (Ast.mksignature (Ast.Tint::nil) (Some Ast.Tint))))
        ::nil))
      main
      (of_pair_list nil).

End EX1.

Section EX2.
  Variables main putchar : Ast.ident.

  Notation param := 1.
  Notation root := 2.
  Notation prev := 3.
  Notation rint := 4.
  Notation rone := 5.
  Notation res := 6.

  Notation next := (Field 0%N FNonVolatile FPointer).
  Notation value := (Field 1%N FNonVolatile FInteger).

  Definition ex2_main_c : list (node * instruction) :=
    ( 1, Mop rone (OpIntConst Int.one) nil 2)
  ::( 2, Mop prev OpNull nil 3)
  ::( 3, Mop rint (OpIntConst (Int.repr 64)) nil 4)
  ::( 4, Mnew root Int.one 5)
  ::( 5, Mput root next prev 6)
  ::( 6, Mput root value rint 7)
  ::( 7, Mop prev OpMov (root::nil) 8)
  ::( 8, Mop rint OpAdd (rint::rone::nil) 9)
  ::( 9, Mif (Op.Ccompuimm Cge (Int.repr 91%Z)) (rint::nil) 10 4)
  ::(10, Mif (Op.Ccompuimm Ceq Int.zero) (root::nil) 14 11)
  ::(11, Mget rint root value 12)
  ::(12, Mcall res putchar_sig putchar (rint::nil) 13)
  ::(13, Mget root root next 10)
  ::(14, Mop rint (OpIntConst (Int.repr 10)) nil 15)
  ::(15, Mcall res putchar_sig putchar (rint::nil) 16)
  ::(16, Mret res)
  ::nil.

  Definition ex2_main_f : function :=
    mkfunction
      (mksignature FInteger (FPointer::nil) false)
      (param::nil)
      3%N
      (of_pair_list ex2_main_c)
      1.

  Definition ex2 : program :=
    mk_program
      (of_pair_list
         ((main, Ast.Internal (lower_mir ex2_main_f))
        ::(putchar, Ast.External (Ast.mkextfun putchar (Ast.mksignature (Ast.Tint::nil) None)))
        ::nil))
      main
      (of_pair_list nil).

End EX2.

Section EX3.
  Variables producer consumer putchar : Ast.ident.

  Notation pval := (Field 0%N FNonVolatile FPointer).
  Notation flag := (Field 1%N FVolatile FInteger).
  Notation value:= (Field 0%N FNonVolatile FInteger).

  Definition sg := (mksignature FInteger (FPointer::nil) false).

  Section PRODUCER.
    Notation param := 1.
    Notation shared := 2.
    Notation obj := 3.

    Notation rone := 4.
    Notation rint := 5.
    Notation sign := 6.

    Definition producer_c : list (node * instruction) :=
      ( 1, Mop rone (OpIntConst Int.one) nil 2)
    ::( 2, Mop rint (OpIntConst (Int.repr 64)) nil 3)
    ::( 3, Mnew shared Int.one 4)
    ::( 4, Mspawn sg consumer shared 5)
    ::( 5, Mnew obj Int.zero 6)
    ::( 6, Mput obj value rint 7)
    ::( 7, Mget sign shared flag 8)
    ::( 8, Mif (Op.Ccompuimm Ceq Int.zero) (sign::nil) 9 7)
    ::( 9, Mput shared pval obj 10)
    ::(10, Mput shared flag rone 11)
    ::(11, Mop rint OpAdd (rint::rone::nil) 12)
    ::(12, Mif (Op.Ccompuimm Cge (Int.repr 91%Z)) (rint::nil) 13 5)
    ::(13, Mret rone)
    ::nil.

    Definition producer_f : function :=
      mkfunction
        sg
        (param::nil) 3%N
        (of_pair_list producer_c)
        1.

  End PRODUCER.

  Section CONSUMER.
    Notation shared := 1.
    Notation obj := 2.

    Notation rint := 3.
    Notation zero := 4.
    Notation res := 5.
    Notation sign := 6.

    Definition consumer_c : list (node * instruction) :=
      ( 1, Mop zero (OpIntConst Int.zero) nil 2)
    ::( 2, Mget sign shared flag 3)
    ::( 3, Mif (Op.Ccompuimm Ceq Int.one) (sign::nil) 4 2)
    ::( 4, Mget obj shared pval 5)
    ::( 5, Mput shared flag zero 6)
    ::( 6, Mget rint obj value 7)
    ::( 7, Mcall res putchar_sig putchar (rint::nil) 8)
    ::( 8, Mif (Op.Ccompuimm Cge (Int.repr 90%Z)) (rint::nil) 9 2)
    ::( 9, Mret zero)
    ::nil.

    Definition consumer_f : function :=
      mkfunction
        sg
        (shared::nil) 2%N
        (of_pair_list consumer_c)
        1.

  End CONSUMER.

  Definition ex3 : program :=
    mk_program
      (of_pair_list
         ((producer, Ast.Internal (lower_mir producer_f))
        ::(consumer, Ast.Internal (lower_mir consumer_f))
        ::(putchar, Ast.External (Ast.mkextfun putchar (Ast.mksignature (Ast.Tint::nil) None)))
        ::nil))
      producer
      (of_pair_list nil).

End EX3.

Section BINTREE.

  Variables main new_tree_node bottom_up item_check print_it print_int putchar : Ast.ident.
  Variable alloc_count : option Ast.ident.

  Notation n_left := (Field 0%N FNonVolatile FPointer).
  Notation n_right := (Field 1%N FNonVolatile FPointer).
  Notation n_item := (Field 2%N FNonVolatile FInteger).
  Notation n_hdr := (Int.repr 2).

  Section NEWNODE.
    Notation a_left := 1.
    Notation a_right:= 2.
    Notation r_new := 3.

    Notation a_item := 4.
    Notation r_cnt := 5.
    Notation r_one := 6.

    Definition new_tree_node_c :=
      (1, Mnew r_new n_hdr 2)
    ::(2, Mput r_new n_left a_left 3)
    ::(3, Mput r_new n_right a_right 4)
    ::(4, Mput r_new n_item a_item 5)
    ::(match alloc_count with
         | Some alloc_count =>
             (5, Mop r_one (OpIntConst Int.one) nil 6)
           ::(6, Mget_global r_cnt alloc_count 7)
           ::(7, Mop r_cnt OpAdd (r_cnt::r_one::nil) 8)
           ::(8, Mput_global alloc_count r_cnt 9)
           ::(9, Mret r_new)
           ::nil
         | None => (5, Mret r_new)::nil
      end).

    Definition new_tree_node_sig := mksignature FPointer (FPointer::FPointer::FInteger::nil) false.

    Definition new_tree_node_f : fundef :=
      Ast.Internal (lower_mir (mkfunction
       new_tree_node_sig
       (a_left::a_right::a_item::nil) 3%N
       (of_pair_list new_tree_node_c) 1)).

  End NEWNODE.

  Section ITEMCHECK.
    Notation a_tree := 1.
    Notation r_child := 2.

    Notation r_item := 3.
    Notation r_resl := 4.
    Notation r_resr := 5.
    Notation r_res := 6.

    Definition item_check_sig := mksignature FInteger (FPointer::nil) false.

    Definition item_check_c :=
      (1, Mget r_child a_tree n_left 2)
    ::(2, Mget r_item a_tree n_item 3)
    ::(3, Mif (Op.Ccompuimm Ceq Int.zero) (r_child::nil) 4 5)
    ::(4, Mret r_item)
    ::(5, Mcall r_resl item_check_sig item_check (r_child::nil) 6)
    ::(6, Mget r_child a_tree n_right 7)
    ::(7, Mcall r_resr item_check_sig item_check (r_child::nil) 8)
    ::(8, Mop r_res OpAdd (r_item::r_resl::nil) 9)
    ::(9, Mop r_resr OpNeg (r_resr::nil) 10)
    ::(10, Mop r_res OpAdd (r_res::r_resr::nil) 11)
    ::(11, Mret r_res)
    ::nil.

    Definition item_check_f :=
      Ast.Internal (lower_mir (mkfunction
        item_check_sig
        (a_tree::nil) 2%N
        (of_pair_list item_check_c) 1)).

  End ITEMCHECK.

  Section BOTTOMUP.
    Notation r_left := 1.
    Notation r_right:= 2.
    Notation r_new := 3.

    Notation a_item := 4.
    Notation a_depth := 5.
    Notation r_item := 6.
    Notation r_mone := 7.

    Definition bottom_up_sig :=
      mksignature FPointer (FInteger::FInteger::nil) false.

    Definition bottom_up_c :=
      ( 1, Mif (Op.Ccompuimm Cgt Int.zero) (a_depth::nil) 2 8)
    ::( 2, Mop r_mone (OpIntConst Int.mone) nil 3)
    ::( 3, Mop a_depth OpAdd (a_depth::r_mone::nil) 4)
    ::( 4, Mop r_item OpAdd (a_item::a_item::nil) 5)
    ::( 5, Mcall r_right bottom_up_sig bottom_up (r_item::a_depth::nil) 6)
    ::( 6, Mop r_item OpAdd (r_item::r_mone::nil) 7)
    ::( 7, Mcall r_left bottom_up_sig bottom_up (r_item::a_depth::nil) 10)
    ::( 8, Mop r_left OpNull nil 9)
    ::( 9, Mop r_right OpNull nil 10)
    ::(10, Mcall r_new new_tree_node_sig new_tree_node (r_left::r_right::a_item::nil) 11)
    ::(11, Mret r_new)
    ::nil.

    Definition bottom_up_f : fundef :=
      Ast.Internal (lower_mir (mkfunction
        bottom_up_sig
        (a_item::a_depth::nil) 3%N
        (of_pair_list bottom_up_c) 1)).

  End BOTTOMUP.

  Section PRINTIT.
    Notation a_depth := 1.
    Notation a_sum := 2.
    Notation r_dummy := 3.

    Definition print_it_c :=
      (1, Mcall r_dummy putchar_sig print_int (a_depth::nil) 2)
    ::(2, Mop r_dummy (OpIntConst (Int.repr 9)) nil 3)
    ::(3, Mcall r_dummy putchar_sig putchar (r_dummy::nil) 4)
    ::(4, Mcall r_dummy putchar_sig print_int (a_sum::nil) 5)
    ::(5, Mop r_dummy (OpIntConst (Int.repr 10)) nil 6)
    ::(6, Mcall r_dummy putchar_sig putchar (r_dummy::nil) 7)
    ::(7, Mret r_dummy)
    ::nil.

    Definition print_it_sig := mksignature FInteger (FInteger::FInteger::nil) false.

    Definition print_it_f :=
      Ast.Internal (lower_mir (mkfunction
        print_it_sig
        (a_depth::a_sum::nil) 0%N
        (of_pair_list print_it_c) 1)).

  End PRINTIT.

  Section MAIN.
    Notation param := 1.
    Notation r_tree := 2.
    Notation r_lltr := 3.

    Notation r_zero := 10.
    Notation r_dep := 11.
    Notation r_res := 12.
    Notation r_maxdepth := 13.
    Notation r_iter := 14.
    Notation r_two := 15.
    Notation r_check := 16.
    Notation r_i := 17.
    Notation r_mi := 18.

    Definition bintree_c depth :=
      ( 1, Mop r_zero (OpIntConst Int.zero) nil 2)
    ::( 2, Mop r_dep (OpIntConst (Int.repr (depth+1))) nil 3)
    ::( 3, Mcall r_tree bottom_up_sig bottom_up (r_zero::r_dep::nil) 4)
    ::( 4, Mcall r_res item_check_sig item_check (r_tree::nil) 5)
    ::( 5, Mcall r_res print_it_sig print_it (r_dep::r_res::nil) 6)
    ::( 6, Mop r_maxdepth (OpIntConst (Int.repr depth)) nil 7)
    ::( 7, Mcall r_lltr bottom_up_sig bottom_up (r_zero::r_maxdepth::nil) 8)
    ::( 8, Mop r_dep (OpIntConst (Int.repr 4)) nil 9)
    ::( 9, Mop r_iter (OpIntConst (Int.shl Int.one (Int.repr depth))) nil 10)
    ::(10, Mif (Op.Ccompuimm Cle (Int.repr depth)) (r_dep::nil) 11 27)
    ::(11, Mop r_check (OpIntConst Int.zero) nil 12)
    ::(12, Mop r_i (OpIntConst Int.one) nil 13)
    ::(13, Mif (Op.Ccompu Cle) (r_i::r_iter::nil) 14 23)
    ::(14, Mcall r_tree bottom_up_sig bottom_up (r_i::r_dep::nil) 15)
    ::(15, Mcall r_res item_check_sig item_check (r_tree::nil) 16)
    ::(16, Mop r_check OpAdd (r_check::r_res::nil) 17)
    ::(17, Mop r_mi OpNeg (r_i::nil) 18)
    ::(18, Mcall r_tree bottom_up_sig bottom_up (r_mi::r_dep::nil) 19)
    ::(19, Mcall r_res item_check_sig item_check (r_tree::nil) 20)
    ::(20, Mop r_check OpAdd (r_check::r_res::nil) 21)
    ::(21, Mop r_two (OpIntConst Int.one) nil 22)
    ::(22, Mop r_i OpAdd (r_i::r_two::nil) 13)
    ::(23, Mcall r_res print_it_sig print_it (r_dep::r_check::nil) 24)
    ::(24, Mop r_two (OpIntConst (Int.repr 2)) nil 25)
    ::(25, Mop r_dep OpAdd (r_dep::r_two::nil) 26)
    ::(26, Mop r_iter (OpShri (Int.repr 2)) (r_iter::nil) 10)
    ::(27, Mcall r_res item_check_sig item_check (r_lltr::nil) 28)
    ::(28, Mcall r_res print_it_sig print_it (r_maxdepth::r_res::nil) 29)
    ::(match alloc_count with
         | Some alloc_count =>
               (29, Mget_global r_check alloc_count 30)
             ::(30, Mcall r_res putchar_sig print_int (r_check::nil) 31)
             ::(31, Mop r_i (OpIntConst (Int.repr 10)) nil 32)
             ::(32, Mcall r_res putchar_sig putchar (r_i::nil) 33)
             ::(33, Mret param)
             ::nil
         | None => (29, Mret param)::nil
       end).

  Definition bintree_f depth :=
    Ast.Internal (lower_mir (mkfunction
      (mksignature FPointer (FPointer::nil) false)
      (param::nil) 3%N
      (of_pair_list (bintree_c depth)) 1)).

  End MAIN.

  Definition bintree (depth: Z) : program :=
    mk_program
      (of_pair_list
         ((new_tree_node, new_tree_node_f)
        ::(item_check, item_check_f)
        ::(bottom_up, bottom_up_f)
        ::(print_it, print_it_f)
        ::(main, bintree_f depth)
        ::(print_int, Ast.External (Ast.mkextfun print_int (Ast.mksignature (Ast.Tint::nil) None)))
        ::(putchar, Ast.External (Ast.mkextfun putchar (Ast.mksignature (Ast.Tint::nil) None)))
        ::nil))
      main
      (of_pair_list (match alloc_count with
                       | Some alloc_count => (alloc_count, (FNonVolatile, FInteger))::nil
                       | None => nil
                     end)).

End BINTREE.

Section MUTEX.

  Variables main client putchar sleep : Ast.ident.
  Variable global : Ast.ident.

  Variable nb_clients : positive.

  Notation expect := (Int.repr ((Zpos ((nb_clients * Psucc nb_clients))) / 2)).

  Notation counter := (Field N0 FNonVolatile FInteger).

  Section MAIN.
  Notation rnew := 1.

  Notation rcpt := 2.
  Notation rmone := 3.

  Definition mutex_main_c :=
    (1, Mnew rnew Int.zero 2)
  ::(2, Mput_global global rnew 3)
  ::(3, Mop rnew OpNull nil 4)
  ::(4, Mop rcpt (OpIntConst (Int.repr (Zpos nb_clients))) nil 5)
  ::(5, Mspawn (mksignature FInteger (FInteger::nil) false) client rcpt 6)
  ::(6, Mop rmone (OpIntConst Int.mone) nil 7)
  ::(7, Mop rcpt OpAdd (rcpt::rmone::nil) 8)
  ::(8, Mif (Op.Ccompuimm Cgt Int.zero) (rcpt::nil) 5 9)
  ::(9, Mget_global rnew global 10)
  ::(10, Mget rcpt rnew counter 11)
  ::(11, Mif (Op.Ccompuimm Cne expect) (rcpt::nil) 10 12)
  ::(12, Mret rnew)
  ::nil.

  Definition mutex_main_f :=
    Ast.Internal (lower_mir (mkfunction
      (mksignature FPointer (FPointer::nil) false)
      (rnew::nil) 1%N
      (of_pair_list mutex_main_c) 1)).

  End MAIN.

  Section CLIENT.
    Notation rglob := 1.
    Notation a_tid := 2.
    Notation curr := 3.
    Notation r_tid := 4.
    Notation garb := 5.

    Definition mutex_client_c :=
      (1, Mget_global rglob global 2)
    ::(2, Mlock rglob 3)
    ::(3, Mop r_tid (OpIntConst (Int.repr 64)) nil 4)
    ::(4, Mop r_tid OpAdd (r_tid::a_tid::nil) 5)
    ::(5, Mcall curr putchar_sig putchar (r_tid::nil) 6)
    ::(6, Mget curr rglob counter 7)
    ::(7, Mcall garb putchar_sig sleep (a_tid::nil) 8)
    ::(8, Mop curr OpAdd (curr::a_tid::nil) 9)
    ::(9, Mput rglob counter curr 10)
    ::(10, Mcall curr putchar_sig putchar (r_tid::nil) 11)
    ::(11, Munlock rglob 12)
    ::(12, Mret a_tid)
    ::nil.

    Definition mutex_client_f :=
      Ast.Internal (lower_mir (mkfunction
        (mksignature FInteger (FInteger::nil) false)
        (a_tid::nil) 1%N
        (of_pair_list mutex_client_c) 1)).

  End CLIENT.

  Definition mutex :=
    mk_program
      (of_pair_list
        ((main, mutex_main_f)
       ::(client, mutex_client_f)
       ::(putchar, Ast.External (Ast.mkextfun putchar (Ast.mksignature (Ast.Tint::nil) None)))
       ::(sleep, Ast.External (Ast.mkextfun sleep (Ast.mksignature (Ast.Tint::nil) (Some Ast.Tint))))
       ::nil))
      main
      (of_pair_list ((global, (FNonVolatile, FPointer))::nil)).

End MUTEX.