Changeset 2775 for extracted/csem.ml


Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2773 r2775  
    778778let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    779779| Kstop -> h_Kstop
    780 | Kseq (x_3726, x_3725) ->
    781   h_Kseq x_3726 x_3725
     780| Kseq (x_8557, x_8556) ->
     781  h_Kseq x_8557 x_8556
    782782    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    783       h_Kswitch h_Kcall x_3725)
    784 | Kwhile (x_3729, x_3728, x_3727) ->
    785   h_Kwhile x_3729 x_3728 x_3727
     783      h_Kswitch h_Kcall x_8556)
     784| Kwhile (x_8560, x_8559, x_8558) ->
     785  h_Kwhile x_8560 x_8559 x_8558
    786786    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    787       h_Kswitch h_Kcall x_3727)
    788 | Kdowhile (x_3732, x_3731, x_3730) ->
    789   h_Kdowhile x_3732 x_3731 x_3730
     787      h_Kswitch h_Kcall x_8558)
     788| Kdowhile (x_8563, x_8562, x_8561) ->
     789  h_Kdowhile x_8563 x_8562 x_8561
    790790    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    791       h_Kswitch h_Kcall x_3730)
    792 | Kfor2 (x_3736, x_3735, x_3734, x_3733) ->
    793   h_Kfor2 x_3736 x_3735 x_3734 x_3733
     791      h_Kswitch h_Kcall x_8561)
     792| Kfor2 (x_8567, x_8566, x_8565, x_8564) ->
     793  h_Kfor2 x_8567 x_8566 x_8565 x_8564
    794794    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    795       h_Kswitch h_Kcall x_3733)
    796 | Kfor3 (x_3740, x_3739, x_3738, x_3737) ->
    797   h_Kfor3 x_3740 x_3739 x_3738 x_3737
     795      h_Kswitch h_Kcall x_8564)
     796| Kfor3 (x_8571, x_8570, x_8569, x_8568) ->
     797  h_Kfor3 x_8571 x_8570 x_8569 x_8568
    798798    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    799       h_Kswitch h_Kcall x_3737)
    800 | Kswitch x_3741 ->
    801   h_Kswitch x_3741
     799      h_Kswitch h_Kcall x_8568)
     800| Kswitch x_8572 ->
     801  h_Kswitch x_8572
    802802    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    803       h_Kswitch h_Kcall x_3741)
    804 | Kcall (x_3745, x_3744, x_3743, x_3742) ->
    805   h_Kcall x_3745 x_3744 x_3743 x_3742
     803      h_Kswitch h_Kcall x_8572)
     804| Kcall (x_8576, x_8575, x_8574, x_8573) ->
     805  h_Kcall x_8576 x_8575 x_8574 x_8573
    806806    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    807       h_Kswitch h_Kcall x_3742)
     807      h_Kswitch h_Kcall x_8573)
    808808
    809809(** val cont_rect_Type3 :
     
    818818let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    819819| Kstop -> h_Kstop
    820 | Kseq (x_3786, x_3785) ->
    821   h_Kseq x_3786 x_3785
     820| Kseq (x_8617, x_8616) ->
     821  h_Kseq x_8617 x_8616
    822822    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    823       h_Kswitch h_Kcall x_3785)
    824 | Kwhile (x_3789, x_3788, x_3787) ->
    825   h_Kwhile x_3789 x_3788 x_3787
     823      h_Kswitch h_Kcall x_8616)
     824| Kwhile (x_8620, x_8619, x_8618) ->
     825  h_Kwhile x_8620 x_8619 x_8618
    826826    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    827       h_Kswitch h_Kcall x_3787)
    828 | Kdowhile (x_3792, x_3791, x_3790) ->
    829   h_Kdowhile x_3792 x_3791 x_3790
     827      h_Kswitch h_Kcall x_8618)
     828| Kdowhile (x_8623, x_8622, x_8621) ->
     829  h_Kdowhile x_8623 x_8622 x_8621
    830830    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    831       h_Kswitch h_Kcall x_3790)
    832 | Kfor2 (x_3796, x_3795, x_3794, x_3793) ->
    833   h_Kfor2 x_3796 x_3795 x_3794 x_3793
     831      h_Kswitch h_Kcall x_8621)
     832| Kfor2 (x_8627, x_8626, x_8625, x_8624) ->
     833  h_Kfor2 x_8627 x_8626 x_8625 x_8624
    834834    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    835       h_Kswitch h_Kcall x_3793)
    836 | Kfor3 (x_3800, x_3799, x_3798, x_3797) ->
    837   h_Kfor3 x_3800 x_3799 x_3798 x_3797
     835      h_Kswitch h_Kcall x_8624)
     836| Kfor3 (x_8631, x_8630, x_8629, x_8628) ->
     837  h_Kfor3 x_8631 x_8630 x_8629 x_8628
    838838    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    839       h_Kswitch h_Kcall x_3797)
    840 | Kswitch x_3801 ->
    841   h_Kswitch x_3801
     839      h_Kswitch h_Kcall x_8628)
     840| Kswitch x_8632 ->
     841  h_Kswitch x_8632
    842842    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    843       h_Kswitch h_Kcall x_3801)
    844 | Kcall (x_3805, x_3804, x_3803, x_3802) ->
    845   h_Kcall x_3805 x_3804 x_3803 x_3802
     843      h_Kswitch h_Kcall x_8632)
     844| Kcall (x_8636, x_8635, x_8634, x_8633) ->
     845  h_Kcall x_8636 x_8635 x_8634 x_8633
    846846    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    847       h_Kswitch h_Kcall x_3802)
     847      h_Kswitch h_Kcall x_8633)
    848848
    849849(** val cont_rect_Type2 :
     
    858858let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    859859| Kstop -> h_Kstop
    860 | Kseq (x_3816, x_3815) ->
    861   h_Kseq x_3816 x_3815
     860| Kseq (x_8647, x_8646) ->
     861  h_Kseq x_8647 x_8646
    862862    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    863       h_Kswitch h_Kcall x_3815)
    864 | Kwhile (x_3819, x_3818, x_3817) ->
    865   h_Kwhile x_3819 x_3818 x_3817
     863      h_Kswitch h_Kcall x_8646)
     864| Kwhile (x_8650, x_8649, x_8648) ->
     865  h_Kwhile x_8650 x_8649 x_8648
    866866    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    867       h_Kswitch h_Kcall x_3817)
    868 | Kdowhile (x_3822, x_3821, x_3820) ->
    869   h_Kdowhile x_3822 x_3821 x_3820
     867      h_Kswitch h_Kcall x_8648)
     868| Kdowhile (x_8653, x_8652, x_8651) ->
     869  h_Kdowhile x_8653 x_8652 x_8651
    870870    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    871       h_Kswitch h_Kcall x_3820)
    872 | Kfor2 (x_3826, x_3825, x_3824, x_3823) ->
    873   h_Kfor2 x_3826 x_3825 x_3824 x_3823
     871      h_Kswitch h_Kcall x_8651)
     872| Kfor2 (x_8657, x_8656, x_8655, x_8654) ->
     873  h_Kfor2 x_8657 x_8656 x_8655 x_8654
    874874    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    875       h_Kswitch h_Kcall x_3823)
    876 | Kfor3 (x_3830, x_3829, x_3828, x_3827) ->
    877   h_Kfor3 x_3830 x_3829 x_3828 x_3827
     875      h_Kswitch h_Kcall x_8654)
     876| Kfor3 (x_8661, x_8660, x_8659, x_8658) ->
     877  h_Kfor3 x_8661 x_8660 x_8659 x_8658
    878878    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    879       h_Kswitch h_Kcall x_3827)
    880 | Kswitch x_3831 ->
    881   h_Kswitch x_3831
     879      h_Kswitch h_Kcall x_8658)
     880| Kswitch x_8662 ->
     881  h_Kswitch x_8662
    882882    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    883       h_Kswitch h_Kcall x_3831)
    884 | Kcall (x_3835, x_3834, x_3833, x_3832) ->
    885   h_Kcall x_3835 x_3834 x_3833 x_3832
     883      h_Kswitch h_Kcall x_8662)
     884| Kcall (x_8666, x_8665, x_8664, x_8663) ->
     885  h_Kcall x_8666 x_8665 x_8664 x_8663
    886886    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    887       h_Kswitch h_Kcall x_3832)
     887      h_Kswitch h_Kcall x_8663)
    888888
    889889(** val cont_rect_Type1 :
     
    898898let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    899899| Kstop -> h_Kstop
    900 | Kseq (x_3846, x_3845) ->
    901   h_Kseq x_3846 x_3845
     900| Kseq (x_8677, x_8676) ->
     901  h_Kseq x_8677 x_8676
    902902    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    903       h_Kswitch h_Kcall x_3845)
    904 | Kwhile (x_3849, x_3848, x_3847) ->
    905   h_Kwhile x_3849 x_3848 x_3847
     903      h_Kswitch h_Kcall x_8676)
     904| Kwhile (x_8680, x_8679, x_8678) ->
     905  h_Kwhile x_8680 x_8679 x_8678
    906906    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    907       h_Kswitch h_Kcall x_3847)
    908 | Kdowhile (x_3852, x_3851, x_3850) ->
    909   h_Kdowhile x_3852 x_3851 x_3850
     907      h_Kswitch h_Kcall x_8678)
     908| Kdowhile (x_8683, x_8682, x_8681) ->
     909  h_Kdowhile x_8683 x_8682 x_8681
    910910    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    911       h_Kswitch h_Kcall x_3850)
    912 | Kfor2 (x_3856, x_3855, x_3854, x_3853) ->
    913   h_Kfor2 x_3856 x_3855 x_3854 x_3853
     911      h_Kswitch h_Kcall x_8681)
     912| Kfor2 (x_8687, x_8686, x_8685, x_8684) ->
     913  h_Kfor2 x_8687 x_8686 x_8685 x_8684
    914914    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    915       h_Kswitch h_Kcall x_3853)
    916 | Kfor3 (x_3860, x_3859, x_3858, x_3857) ->
    917   h_Kfor3 x_3860 x_3859 x_3858 x_3857
     915      h_Kswitch h_Kcall x_8684)
     916| Kfor3 (x_8691, x_8690, x_8689, x_8688) ->
     917  h_Kfor3 x_8691 x_8690 x_8689 x_8688
    918918    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    919       h_Kswitch h_Kcall x_3857)
    920 | Kswitch x_3861 ->
    921   h_Kswitch x_3861
     919      h_Kswitch h_Kcall x_8688)
     920| Kswitch x_8692 ->
     921  h_Kswitch x_8692
    922922    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    923       h_Kswitch h_Kcall x_3861)
    924 | Kcall (x_3865, x_3864, x_3863, x_3862) ->
    925   h_Kcall x_3865 x_3864 x_3863 x_3862
     923      h_Kswitch h_Kcall x_8692)
     924| Kcall (x_8696, x_8695, x_8694, x_8693) ->
     925  h_Kcall x_8696 x_8695 x_8694 x_8693
    926926    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    927       h_Kswitch h_Kcall x_3862)
     927      h_Kswitch h_Kcall x_8693)
    928928
    929929(** val cont_rect_Type0 :
     
    938938let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    939939| Kstop -> h_Kstop
    940 | Kseq (x_3876, x_3875) ->
    941   h_Kseq x_3876 x_3875
     940| Kseq (x_8707, x_8706) ->
     941  h_Kseq x_8707 x_8706
    942942    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    943       h_Kswitch h_Kcall x_3875)
    944 | Kwhile (x_3879, x_3878, x_3877) ->
    945   h_Kwhile x_3879 x_3878 x_3877
     943      h_Kswitch h_Kcall x_8706)
     944| Kwhile (x_8710, x_8709, x_8708) ->
     945  h_Kwhile x_8710 x_8709 x_8708
    946946    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    947       h_Kswitch h_Kcall x_3877)
    948 | Kdowhile (x_3882, x_3881, x_3880) ->
    949   h_Kdowhile x_3882 x_3881 x_3880
     947      h_Kswitch h_Kcall x_8708)
     948| Kdowhile (x_8713, x_8712, x_8711) ->
     949  h_Kdowhile x_8713 x_8712 x_8711
    950950    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    951       h_Kswitch h_Kcall x_3880)
    952 | Kfor2 (x_3886, x_3885, x_3884, x_3883) ->
    953   h_Kfor2 x_3886 x_3885 x_3884 x_3883
     951      h_Kswitch h_Kcall x_8711)
     952| Kfor2 (x_8717, x_8716, x_8715, x_8714) ->
     953  h_Kfor2 x_8717 x_8716 x_8715 x_8714
    954954    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    955       h_Kswitch h_Kcall x_3883)
    956 | Kfor3 (x_3890, x_3889, x_3888, x_3887) ->
    957   h_Kfor3 x_3890 x_3889 x_3888 x_3887
     955      h_Kswitch h_Kcall x_8714)
     956| Kfor3 (x_8721, x_8720, x_8719, x_8718) ->
     957  h_Kfor3 x_8721 x_8720 x_8719 x_8718
    958958    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    959       h_Kswitch h_Kcall x_3887)
    960 | Kswitch x_3891 ->
    961   h_Kswitch x_3891
     959      h_Kswitch h_Kcall x_8718)
     960| Kswitch x_8722 ->
     961  h_Kswitch x_8722
    962962    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    963       h_Kswitch h_Kcall x_3891)
    964 | Kcall (x_3895, x_3894, x_3893, x_3892) ->
    965   h_Kcall x_3895 x_3894 x_3893 x_3892
     963      h_Kswitch h_Kcall x_8722)
     964| Kcall (x_8726, x_8725, x_8724, x_8723) ->
     965  h_Kcall x_8726 x_8725 x_8724 x_8723
    966966    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    967       h_Kswitch h_Kcall x_3892)
     967      h_Kswitch h_Kcall x_8723)
    968968
    969969(** val cont_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.