Changeset 717


Ignore:
Timestamp:
Mar 29, 2011, 5:54:36 PM (9 years ago)
Author:
campbell
Message:

Clean up Clight examples; better temporary definition of multiply.

Location:
src/Clight
Files:
5 added
4 deleted
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r700 r717  
    183183      match v1 with
    184184      [ Vint n1 ⇒ match v2 with
    185         [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))
     185          [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
     186(*        [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))*)
    186187        | _ ⇒ None ? ]
    187188      | _ ⇒ None ? ]
  • src/Clight/test/duff.ma

    r415 r717  
    1 include "Animation.ma".
     1include "Clight/Animation.ma".
    22
    3 (* This definition takes a long time to be accepted. *)
    4 
    5 ndefinition myprog := mk_program fundef type
    6   [mk_pair ?? (succ_pos_of_nat 132 (* copy *)) (Internal (
    7     mk_function Tvoid [mk_pair ?? (succ_pos_of_nat 151) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 152) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 153) (Tint I32 Signed  )] [mk_pair ?? (succ_pos_of_nat 133) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 135) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 136) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 137) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 138) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 139) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 140) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 141) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 142) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 143) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 144) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 145) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 146) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 147) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 148) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 149) (Tpointer Any (Tint I16 Signed  )); mk_pair ?? (succ_pos_of_nat 150) (Tpointer Any (Tint I16 Signed  ))]
    8       (Ssequence
    9       (Sassign (Expr (Evar (succ_pos_of_nat 133)) (Tint I32 Signed  ))
    10         (Expr (Ebinop Odiv
    11           (Expr (Ebinop Oadd
    12             (Expr (Evar (succ_pos_of_nat 153)) (Tint I32 Signed  ))
    13             (Expr (Econst_int (repr 7)) (Tint I32 Signed  )))
    14             (Tint I32 Signed  ))
    15           (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
    16           (Tint I32 Signed  )))
    17       (Sswitch (Expr (Ebinop Omod
    18                  (Expr (Evar (succ_pos_of_nat 153)) (Tint I32 Signed  ))
    19                  (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
    20                  (Tint I32 Signed  )) (
    21         (LScase (repr 0)
    22           (Slabel (succ_pos_of_nat 154)
    23           (Ssequence
    24           (Ssequence
    25           (Sassign (Expr (Evar (succ_pos_of_nat 149))
     3definition myprog := mk_program fundef type
     4  [〈succ_pos_of_nat 0 (* copy *), Internal (
     5     mk_function Tvoid [〈succ_pos_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 21, (Tint I32 Signed  )〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
     6       (Ssequence
     7       (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     8         (Expr (Ebinop Odiv
     9           (Expr (Ebinop Oadd
     10             (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed  ))
     11             (Expr (Econst_int (repr 7)) (Tint I32 Signed  )))
     12             (Tint I32 Signed  ))
     13           (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
     14           (Tint I32 Signed  )))
     15       (Sswitch (Expr (Ebinop Omod
     16                  (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed  ))
     17                  (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
     18                  (Tint I32 Signed  )) (
     19         (LScase (repr 0)
     20           (Slabel (succ_pos_of_nat 22)
     21           (Ssequence
     22           (Ssequence
     23           (Sassign (Expr (Evar (succ_pos_of_nat 17))
     24                      (Tpointer Any (Tint I16 Signed  )))
     25             (Expr (Evar (succ_pos_of_nat 19))
     26               (Tpointer Any (Tint I16 Signed  ))))
     27           (Sassign (Expr (Evar (succ_pos_of_nat 19))
     28                      (Tpointer Any (Tint I16 Signed  )))
     29             (Expr (Ebinop Oadd
     30               (Expr (Evar (succ_pos_of_nat 17))
     31                 (Tpointer Any (Tint I16 Signed  )))
     32               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     33               (Tpointer Any (Tint I16 Signed  )))))
     34           (Ssequence
     35           (Ssequence
     36           (Sassign (Expr (Evar (succ_pos_of_nat 18))
     37                      (Tpointer Any (Tint I16 Signed  )))
     38             (Expr (Evar (succ_pos_of_nat 20))
     39               (Tpointer Any (Tint I16 Signed  ))))
     40           (Sassign (Expr (Evar (succ_pos_of_nat 20))
     41                      (Tpointer Any (Tint I16 Signed  )))
     42             (Expr (Ebinop Oadd
     43               (Expr (Evar (succ_pos_of_nat 18))
     44                 (Tpointer Any (Tint I16 Signed  )))
     45               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     46               (Tpointer Any (Tint I16 Signed  )))))
     47           (Sassign (Expr (Ederef
     48                      (Expr (Evar (succ_pos_of_nat 17))
     49                        (Tpointer Any (Tint I16 Signed  ))))
     50                      (Tint I16 Signed  ))
     51             (Expr (Ederef
     52               (Expr (Evar (succ_pos_of_nat 18))
     53                 (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
     54           (LScase (repr 7)
     55             (Ssequence
     56             (Sassign (Expr (Evar (succ_pos_of_nat 15))
     57                        (Tpointer Any (Tint I16 Signed  )))
     58               (Expr (Evar (succ_pos_of_nat 19))
     59                 (Tpointer Any (Tint I16 Signed  ))))
     60             (Ssequence
     61             (Sassign (Expr (Evar (succ_pos_of_nat 19))
     62                        (Tpointer Any (Tint I16 Signed  )))
     63               (Expr (Ebinop Oadd
     64                 (Expr (Evar (succ_pos_of_nat 15))
     65                   (Tpointer Any (Tint I16 Signed  )))
     66                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     67                 (Tpointer Any (Tint I16 Signed  ))))
     68             (Ssequence
     69             (Sassign (Expr (Evar (succ_pos_of_nat 16))
     70                        (Tpointer Any (Tint I16 Signed  )))
     71               (Expr (Evar (succ_pos_of_nat 20))
     72                 (Tpointer Any (Tint I16 Signed  ))))
     73             (Ssequence
     74             (Sassign (Expr (Evar (succ_pos_of_nat 20))
     75                        (Tpointer Any (Tint I16 Signed  )))
     76               (Expr (Ebinop Oadd
     77                 (Expr (Evar (succ_pos_of_nat 16))
     78                   (Tpointer Any (Tint I16 Signed  )))
     79                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     80                 (Tpointer Any (Tint I16 Signed  ))))
     81             (Sassign (Expr (Ederef
     82                        (Expr (Evar (succ_pos_of_nat 15))
     83                          (Tpointer Any (Tint I16 Signed  ))))
     84                        (Tint I16 Signed  ))
     85               (Expr (Ederef
     86                 (Expr (Evar (succ_pos_of_nat 16))
     87                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
     88             (LScase (repr 6)
     89               (Ssequence
     90               (Sassign (Expr (Evar (succ_pos_of_nat 13))
     91                          (Tpointer Any (Tint I16 Signed  )))
     92                 (Expr (Evar (succ_pos_of_nat 19))
     93                   (Tpointer Any (Tint I16 Signed  ))))
     94               (Ssequence
     95               (Sassign (Expr (Evar (succ_pos_of_nat 19))
     96                          (Tpointer Any (Tint I16 Signed  )))
     97                 (Expr (Ebinop Oadd
     98                   (Expr (Evar (succ_pos_of_nat 13))
    2699                     (Tpointer Any (Tint I16 Signed  )))
    27             (Expr (Evar (succ_pos_of_nat 151))
    28               (Tpointer Any (Tint I16 Signed  ))))
    29           (Sassign (Expr (Evar (succ_pos_of_nat 151))
     100                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     101                   (Tpointer Any (Tint I16 Signed  ))))
     102               (Ssequence
     103               (Sassign (Expr (Evar (succ_pos_of_nat 14))
     104                          (Tpointer Any (Tint I16 Signed  )))
     105                 (Expr (Evar (succ_pos_of_nat 20))
     106                   (Tpointer Any (Tint I16 Signed  ))))
     107               (Ssequence
     108               (Sassign (Expr (Evar (succ_pos_of_nat 20))
     109                          (Tpointer Any (Tint I16 Signed  )))
     110                 (Expr (Ebinop Oadd
     111                   (Expr (Evar (succ_pos_of_nat 14))
    30112                     (Tpointer Any (Tint I16 Signed  )))
    31             (Expr (Ebinop Oadd
    32               (Expr (Evar (succ_pos_of_nat 149))
    33                 (Tpointer Any (Tint I16 Signed  )))
    34               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    35               (Tpointer Any (Tint I16 Signed  )))))
    36           (Ssequence
    37           (Ssequence
    38           (Sassign (Expr (Evar (succ_pos_of_nat 150))
    39                      (Tpointer Any (Tint I16 Signed  )))
    40             (Expr (Evar (succ_pos_of_nat 152))
    41               (Tpointer Any (Tint I16 Signed  ))))
    42           (Sassign (Expr (Evar (succ_pos_of_nat 152))
    43                      (Tpointer Any (Tint I16 Signed  )))
    44             (Expr (Ebinop Oadd
    45               (Expr (Evar (succ_pos_of_nat 150))
    46                 (Tpointer Any (Tint I16 Signed  )))
    47               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    48               (Tpointer Any (Tint I16 Signed  )))))
    49           (Sassign (Expr (Ederef
    50                      (Expr (Evar (succ_pos_of_nat 149))
     113                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     114                   (Tpointer Any (Tint I16 Signed  ))))
     115               (Sassign (Expr (Ederef
     116                          (Expr (Evar (succ_pos_of_nat 13))
     117                            (Tpointer Any (Tint I16 Signed  ))))
     118                          (Tint I16 Signed  ))
     119                 (Expr (Ederef
     120                   (Expr (Evar (succ_pos_of_nat 14))
     121                     (Tpointer Any (Tint I16 Signed  ))))
     122                   (Tint I16 Signed  )))))))
     123               (LScase (repr 5)
     124                 (Ssequence
     125                 (Sassign (Expr (Evar (succ_pos_of_nat 11))
     126                            (Tpointer Any (Tint I16 Signed  )))
     127                   (Expr (Evar (succ_pos_of_nat 19))
     128                     (Tpointer Any (Tint I16 Signed  ))))
     129                 (Ssequence
     130                 (Sassign (Expr (Evar (succ_pos_of_nat 19))
     131                            (Tpointer Any (Tint I16 Signed  )))
     132                   (Expr (Ebinop Oadd
     133                     (Expr (Evar (succ_pos_of_nat 11))
     134                       (Tpointer Any (Tint I16 Signed  )))
     135                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     136                     (Tpointer Any (Tint I16 Signed  ))))
     137                 (Ssequence
     138                 (Sassign (Expr (Evar (succ_pos_of_nat 12))
     139                            (Tpointer Any (Tint I16 Signed  )))
     140                   (Expr (Evar (succ_pos_of_nat 20))
     141                     (Tpointer Any (Tint I16 Signed  ))))
     142                 (Ssequence
     143                 (Sassign (Expr (Evar (succ_pos_of_nat 20))
     144                            (Tpointer Any (Tint I16 Signed  )))
     145                   (Expr (Ebinop Oadd
     146                     (Expr (Evar (succ_pos_of_nat 12))
     147                       (Tpointer Any (Tint I16 Signed  )))
     148                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     149                     (Tpointer Any (Tint I16 Signed  ))))
     150                 (Sassign (Expr (Ederef
     151                            (Expr (Evar (succ_pos_of_nat 11))
     152                              (Tpointer Any (Tint I16 Signed  ))))
     153                            (Tint I16 Signed  ))
     154                   (Expr (Ederef
     155                     (Expr (Evar (succ_pos_of_nat 12))
    51156                       (Tpointer Any (Tint I16 Signed  ))))
    52                      (Tint I16 Signed  ))
    53             (Expr (Ederef
    54               (Expr (Evar (succ_pos_of_nat 150))
    55                 (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
    56           (LScase (repr 7)
    57             (Ssequence
    58             (Sassign (Expr (Evar (succ_pos_of_nat 147))
    59                        (Tpointer Any (Tint I16 Signed  )))
    60               (Expr (Evar (succ_pos_of_nat 151))
    61                 (Tpointer Any (Tint I16 Signed  ))))
    62             (Ssequence
    63             (Sassign (Expr (Evar (succ_pos_of_nat 151))
    64                        (Tpointer Any (Tint I16 Signed  )))
    65               (Expr (Ebinop Oadd
    66                 (Expr (Evar (succ_pos_of_nat 147))
    67                   (Tpointer Any (Tint I16 Signed  )))
    68                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    69                 (Tpointer Any (Tint I16 Signed  ))))
    70             (Ssequence
    71             (Sassign (Expr (Evar (succ_pos_of_nat 148))
    72                        (Tpointer Any (Tint I16 Signed  )))
    73               (Expr (Evar (succ_pos_of_nat 152))
    74                 (Tpointer Any (Tint I16 Signed  ))))
    75             (Ssequence
    76             (Sassign (Expr (Evar (succ_pos_of_nat 152))
    77                        (Tpointer Any (Tint I16 Signed  )))
    78               (Expr (Ebinop Oadd
    79                 (Expr (Evar (succ_pos_of_nat 148))
    80                   (Tpointer Any (Tint I16 Signed  )))
    81                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    82                 (Tpointer Any (Tint I16 Signed  ))))
    83             (Sassign (Expr (Ederef
    84                        (Expr (Evar (succ_pos_of_nat 147))
     157                     (Tint I16 Signed  )))))))
     158                 (LScase (repr 4)
     159                   (Ssequence
     160                   (Sassign (Expr (Evar (succ_pos_of_nat 9))
     161                              (Tpointer Any (Tint I16 Signed  )))
     162                     (Expr (Evar (succ_pos_of_nat 19))
     163                       (Tpointer Any (Tint I16 Signed  ))))
     164                   (Ssequence
     165                   (Sassign (Expr (Evar (succ_pos_of_nat 19))
     166                              (Tpointer Any (Tint I16 Signed  )))
     167                     (Expr (Ebinop Oadd
     168                       (Expr (Evar (succ_pos_of_nat 9))
     169                         (Tpointer Any (Tint I16 Signed  )))
     170                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     171                       (Tpointer Any (Tint I16 Signed  ))))
     172                   (Ssequence
     173                   (Sassign (Expr (Evar (succ_pos_of_nat 10))
     174                              (Tpointer Any (Tint I16 Signed  )))
     175                     (Expr (Evar (succ_pos_of_nat 20))
     176                       (Tpointer Any (Tint I16 Signed  ))))
     177                   (Ssequence
     178                   (Sassign (Expr (Evar (succ_pos_of_nat 20))
     179                              (Tpointer Any (Tint I16 Signed  )))
     180                     (Expr (Ebinop Oadd
     181                       (Expr (Evar (succ_pos_of_nat 10))
     182                         (Tpointer Any (Tint I16 Signed  )))
     183                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     184                       (Tpointer Any (Tint I16 Signed  ))))
     185                   (Sassign (Expr (Ederef
     186                              (Expr (Evar (succ_pos_of_nat 9))
     187                                (Tpointer Any (Tint I16 Signed  ))))
     188                              (Tint I16 Signed  ))
     189                     (Expr (Ederef
     190                       (Expr (Evar (succ_pos_of_nat 10))
    85191                         (Tpointer Any (Tint I16 Signed  ))))
    86                        (Tint I16 Signed  ))
    87               (Expr (Ederef
    88                 (Expr (Evar (succ_pos_of_nat 148))
    89                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    90             (LScase (repr 6)
    91               (Ssequence
    92               (Sassign (Expr (Evar (succ_pos_of_nat 145))
    93                          (Tpointer Any (Tint I16 Signed  )))
    94                 (Expr (Evar (succ_pos_of_nat 151))
    95                   (Tpointer Any (Tint I16 Signed  ))))
    96               (Ssequence
    97               (Sassign (Expr (Evar (succ_pos_of_nat 151))
    98                          (Tpointer Any (Tint I16 Signed  )))
    99                 (Expr (Ebinop Oadd
    100                   (Expr (Evar (succ_pos_of_nat 145))
    101                     (Tpointer Any (Tint I16 Signed  )))
    102                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    103                   (Tpointer Any (Tint I16 Signed  ))))
    104               (Ssequence
    105               (Sassign (Expr (Evar (succ_pos_of_nat 146))
    106                          (Tpointer Any (Tint I16 Signed  )))
    107                 (Expr (Evar (succ_pos_of_nat 152))
    108                   (Tpointer Any (Tint I16 Signed  ))))
    109               (Ssequence
    110               (Sassign (Expr (Evar (succ_pos_of_nat 152))
    111                          (Tpointer Any (Tint I16 Signed  )))
    112                 (Expr (Ebinop Oadd
    113                   (Expr (Evar (succ_pos_of_nat 146))
    114                     (Tpointer Any (Tint I16 Signed  )))
    115                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    116                   (Tpointer Any (Tint I16 Signed  ))))
    117               (Sassign (Expr (Ederef
    118                          (Expr (Evar (succ_pos_of_nat 145))
     192                       (Tint I16 Signed  )))))))
     193                   (LScase (repr 3)
     194                     (Ssequence
     195                     (Sassign (Expr (Evar (succ_pos_of_nat 7))
     196                                (Tpointer Any (Tint I16 Signed  )))
     197                       (Expr (Evar (succ_pos_of_nat 19))
     198                         (Tpointer Any (Tint I16 Signed  ))))
     199                     (Ssequence
     200                     (Sassign (Expr (Evar (succ_pos_of_nat 19))
     201                                (Tpointer Any (Tint I16 Signed  )))
     202                       (Expr (Ebinop Oadd
     203                         (Expr (Evar (succ_pos_of_nat 7))
     204                           (Tpointer Any (Tint I16 Signed  )))
     205                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     206                         (Tpointer Any (Tint I16 Signed  ))))
     207                     (Ssequence
     208                     (Sassign (Expr (Evar (succ_pos_of_nat 8))
     209                                (Tpointer Any (Tint I16 Signed  )))
     210                       (Expr (Evar (succ_pos_of_nat 20))
     211                         (Tpointer Any (Tint I16 Signed  ))))
     212                     (Ssequence
     213                     (Sassign (Expr (Evar (succ_pos_of_nat 20))
     214                                (Tpointer Any (Tint I16 Signed  )))
     215                       (Expr (Ebinop Oadd
     216                         (Expr (Evar (succ_pos_of_nat 8))
     217                           (Tpointer Any (Tint I16 Signed  )))
     218                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     219                         (Tpointer Any (Tint I16 Signed  ))))
     220                     (Sassign (Expr (Ederef
     221                                (Expr (Evar (succ_pos_of_nat 7))
     222                                  (Tpointer Any (Tint I16 Signed  ))))
     223                                (Tint I16 Signed  ))
     224                       (Expr (Ederef
     225                         (Expr (Evar (succ_pos_of_nat 8))
    119226                           (Tpointer Any (Tint I16 Signed  ))))
    120                          (Tint I16 Signed  ))
    121                 (Expr (Ederef
    122                   (Expr (Evar (succ_pos_of_nat 146))
    123                     (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    124               (LScase (repr 5)
    125                 (Ssequence
    126                 (Sassign (Expr (Evar (succ_pos_of_nat 143))
    127                            (Tpointer Any (Tint I16 Signed  )))
    128                   (Expr (Evar (succ_pos_of_nat 151))
    129                     (Tpointer Any (Tint I16 Signed  ))))
    130                 (Ssequence
    131                 (Sassign (Expr (Evar (succ_pos_of_nat 151))
    132                            (Tpointer Any (Tint I16 Signed  )))
    133                   (Expr (Ebinop Oadd
    134                     (Expr (Evar (succ_pos_of_nat 143))
    135                       (Tpointer Any (Tint I16 Signed  )))
    136                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    137                     (Tpointer Any (Tint I16 Signed  ))))
    138                 (Ssequence
    139                 (Sassign (Expr (Evar (succ_pos_of_nat 144))
    140                            (Tpointer Any (Tint I16 Signed  )))
    141                   (Expr (Evar (succ_pos_of_nat 152))
    142                     (Tpointer Any (Tint I16 Signed  ))))
    143                 (Ssequence
    144                 (Sassign (Expr (Evar (succ_pos_of_nat 152))
    145                            (Tpointer Any (Tint I16 Signed  )))
    146                   (Expr (Ebinop Oadd
    147                     (Expr (Evar (succ_pos_of_nat 144))
    148                       (Tpointer Any (Tint I16 Signed  )))
    149                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    150                     (Tpointer Any (Tint I16 Signed  ))))
    151                 (Sassign (Expr (Ederef
    152                            (Expr (Evar (succ_pos_of_nat 143))
     227                         (Tint I16 Signed  )))))))
     228                     (LScase (repr 2)
     229                       (Ssequence
     230                       (Sassign (Expr (Evar (succ_pos_of_nat 5))
     231                                  (Tpointer Any (Tint I16 Signed  )))
     232                         (Expr (Evar (succ_pos_of_nat 19))
     233                           (Tpointer Any (Tint I16 Signed  ))))
     234                       (Ssequence
     235                       (Sassign (Expr (Evar (succ_pos_of_nat 19))
     236                                  (Tpointer Any (Tint I16 Signed  )))
     237                         (Expr (Ebinop Oadd
     238                           (Expr (Evar (succ_pos_of_nat 5))
     239                             (Tpointer Any (Tint I16 Signed  )))
     240                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     241                           (Tpointer Any (Tint I16 Signed  ))))
     242                       (Ssequence
     243                       (Sassign (Expr (Evar (succ_pos_of_nat 6))
     244                                  (Tpointer Any (Tint I16 Signed  )))
     245                         (Expr (Evar (succ_pos_of_nat 20))
     246                           (Tpointer Any (Tint I16 Signed  ))))
     247                       (Ssequence
     248                       (Sassign (Expr (Evar (succ_pos_of_nat 20))
     249                                  (Tpointer Any (Tint I16 Signed  )))
     250                         (Expr (Ebinop Oadd
     251                           (Expr (Evar (succ_pos_of_nat 6))
     252                             (Tpointer Any (Tint I16 Signed  )))
     253                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     254                           (Tpointer Any (Tint I16 Signed  ))))
     255                       (Sassign (Expr (Ederef
     256                                  (Expr (Evar (succ_pos_of_nat 5))
     257                                    (Tpointer Any (Tint I16 Signed  ))))
     258                                  (Tint I16 Signed  ))
     259                         (Expr (Ederef
     260                           (Expr (Evar (succ_pos_of_nat 6))
    153261                             (Tpointer Any (Tint I16 Signed  ))))
    154                            (Tint I16 Signed  ))
    155                   (Expr (Ederef
    156                     (Expr (Evar (succ_pos_of_nat 144))
    157                       (Tpointer Any (Tint I16 Signed  ))))
    158                     (Tint I16 Signed  )))))))
    159                 (LScase (repr 4)
    160                   (Ssequence
    161                   (Sassign (Expr (Evar (succ_pos_of_nat 141))
    162                              (Tpointer Any (Tint I16 Signed  )))
    163                     (Expr (Evar (succ_pos_of_nat 151))
    164                       (Tpointer Any (Tint I16 Signed  ))))
    165                   (Ssequence
    166                   (Sassign (Expr (Evar (succ_pos_of_nat 151))
    167                              (Tpointer Any (Tint I16 Signed  )))
    168                     (Expr (Ebinop Oadd
    169                       (Expr (Evar (succ_pos_of_nat 141))
    170                         (Tpointer Any (Tint I16 Signed  )))
    171                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    172                       (Tpointer Any (Tint I16 Signed  ))))
    173                   (Ssequence
    174                   (Sassign (Expr (Evar (succ_pos_of_nat 142))
    175                              (Tpointer Any (Tint I16 Signed  )))
    176                     (Expr (Evar (succ_pos_of_nat 152))
    177                       (Tpointer Any (Tint I16 Signed  ))))
    178                   (Ssequence
    179                   (Sassign (Expr (Evar (succ_pos_of_nat 152))
    180                              (Tpointer Any (Tint I16 Signed  )))
    181                     (Expr (Ebinop Oadd
    182                       (Expr (Evar (succ_pos_of_nat 142))
    183                         (Tpointer Any (Tint I16 Signed  )))
    184                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    185                       (Tpointer Any (Tint I16 Signed  ))))
    186                   (Sassign (Expr (Ederef
    187                              (Expr (Evar (succ_pos_of_nat 141))
     262                           (Tint I16 Signed  )))))))
     263                       (LScase (repr 1)
     264                         (Ssequence
     265                         (Sassign (Expr (Evar (succ_pos_of_nat 3))
     266                                    (Tpointer Any (Tint I16 Signed  )))
     267                           (Expr (Evar (succ_pos_of_nat 19))
     268                             (Tpointer Any (Tint I16 Signed  ))))
     269                         (Ssequence
     270                         (Sassign (Expr (Evar (succ_pos_of_nat 19))
     271                                    (Tpointer Any (Tint I16 Signed  )))
     272                           (Expr (Ebinop Oadd
     273                             (Expr (Evar (succ_pos_of_nat 3))
     274                               (Tpointer Any (Tint I16 Signed  )))
     275                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     276                             (Tpointer Any (Tint I16 Signed  ))))
     277                         (Ssequence
     278                         (Sassign (Expr (Evar (succ_pos_of_nat 4))
     279                                    (Tpointer Any (Tint I16 Signed  )))
     280                           (Expr (Evar (succ_pos_of_nat 20))
     281                             (Tpointer Any (Tint I16 Signed  ))))
     282                         (Ssequence
     283                         (Sassign (Expr (Evar (succ_pos_of_nat 20))
     284                                    (Tpointer Any (Tint I16 Signed  )))
     285                           (Expr (Ebinop Oadd
     286                             (Expr (Evar (succ_pos_of_nat 4))
     287                               (Tpointer Any (Tint I16 Signed  )))
     288                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     289                             (Tpointer Any (Tint I16 Signed  ))))
     290                         (Ssequence
     291                         (Sassign (Expr (Ederef
     292                                    (Expr (Evar (succ_pos_of_nat 3))
     293                                      (Tpointer Any (Tint I16 Signed  ))))
     294                                    (Tint I16 Signed  ))
     295                           (Expr (Ederef
     296                             (Expr (Evar (succ_pos_of_nat 4))
    188297                               (Tpointer Any (Tint I16 Signed  ))))
    189                              (Tint I16 Signed  ))
    190                     (Expr (Ederef
    191                       (Expr (Evar (succ_pos_of_nat 142))
    192                         (Tpointer Any (Tint I16 Signed  ))))
    193                       (Tint I16 Signed  )))))))
    194                   (LScase (repr 3)
    195                     (Ssequence
    196                     (Sassign (Expr (Evar (succ_pos_of_nat 139))
    197                                (Tpointer Any (Tint I16 Signed  )))
    198                       (Expr (Evar (succ_pos_of_nat 151))
    199                         (Tpointer Any (Tint I16 Signed  ))))
    200                     (Ssequence
    201                     (Sassign (Expr (Evar (succ_pos_of_nat 151))
    202                                (Tpointer Any (Tint I16 Signed  )))
    203                       (Expr (Ebinop Oadd
    204                         (Expr (Evar (succ_pos_of_nat 139))
    205                           (Tpointer Any (Tint I16 Signed  )))
    206                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    207                         (Tpointer Any (Tint I16 Signed  ))))
    208                     (Ssequence
    209                     (Sassign (Expr (Evar (succ_pos_of_nat 140))
    210                                (Tpointer Any (Tint I16 Signed  )))
    211                       (Expr (Evar (succ_pos_of_nat 152))
    212                         (Tpointer Any (Tint I16 Signed  ))))
    213                     (Ssequence
    214                     (Sassign (Expr (Evar (succ_pos_of_nat 152))
    215                                (Tpointer Any (Tint I16 Signed  )))
    216                       (Expr (Ebinop Oadd
    217                         (Expr (Evar (succ_pos_of_nat 140))
    218                           (Tpointer Any (Tint I16 Signed  )))
    219                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    220                         (Tpointer Any (Tint I16 Signed  ))))
    221                     (Sassign (Expr (Ederef
    222                                (Expr (Evar (succ_pos_of_nat 139))
    223                                  (Tpointer Any (Tint I16 Signed  ))))
    224                                (Tint I16 Signed  ))
    225                       (Expr (Ederef
    226                         (Expr (Evar (succ_pos_of_nat 140))
    227                           (Tpointer Any (Tint I16 Signed  ))))
    228                         (Tint I16 Signed  )))))))
    229                     (LScase (repr 2)
    230                       (Ssequence
    231                       (Sassign (Expr (Evar (succ_pos_of_nat 137))
    232                                  (Tpointer Any (Tint I16 Signed  )))
    233                         (Expr (Evar (succ_pos_of_nat 151))
    234                           (Tpointer Any (Tint I16 Signed  ))))
    235                       (Ssequence
    236                       (Sassign (Expr (Evar (succ_pos_of_nat 151))
    237                                  (Tpointer Any (Tint I16 Signed  )))
    238                         (Expr (Ebinop Oadd
    239                           (Expr (Evar (succ_pos_of_nat 137))
    240                             (Tpointer Any (Tint I16 Signed  )))
    241                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    242                           (Tpointer Any (Tint I16 Signed  ))))
    243                       (Ssequence
    244                       (Sassign (Expr (Evar (succ_pos_of_nat 138))
    245                                  (Tpointer Any (Tint I16 Signed  )))
    246                         (Expr (Evar (succ_pos_of_nat 152))
    247                           (Tpointer Any (Tint I16 Signed  ))))
    248                       (Ssequence
    249                       (Sassign (Expr (Evar (succ_pos_of_nat 152))
    250                                  (Tpointer Any (Tint I16 Signed  )))
    251                         (Expr (Ebinop Oadd
    252                           (Expr (Evar (succ_pos_of_nat 138))
    253                             (Tpointer Any (Tint I16 Signed  )))
    254                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    255                           (Tpointer Any (Tint I16 Signed  ))))
    256                       (Sassign (Expr (Ederef
    257                                  (Expr (Evar (succ_pos_of_nat 137))
    258                                    (Tpointer Any (Tint I16 Signed  ))))
    259                                  (Tint I16 Signed  ))
    260                         (Expr (Ederef
    261                           (Expr (Evar (succ_pos_of_nat 138))
    262                             (Tpointer Any (Tint I16 Signed  ))))
    263                           (Tint I16 Signed  )))))))
    264                       (LScase (repr 1)
    265                         (Ssequence
    266                         (Sassign (Expr (Evar (succ_pos_of_nat 135))
    267                                    (Tpointer Any (Tint I16 Signed  )))
    268                           (Expr (Evar (succ_pos_of_nat 151))
    269                             (Tpointer Any (Tint I16 Signed  ))))
    270                         (Ssequence
    271                         (Sassign (Expr (Evar (succ_pos_of_nat 151))
    272                                    (Tpointer Any (Tint I16 Signed  )))
    273                           (Expr (Ebinop Oadd
    274                             (Expr (Evar (succ_pos_of_nat 135))
    275                               (Tpointer Any (Tint I16 Signed  )))
    276                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    277                             (Tpointer Any (Tint I16 Signed  ))))
    278                         (Ssequence
    279                         (Sassign (Expr (Evar (succ_pos_of_nat 136))
    280                                    (Tpointer Any (Tint I16 Signed  )))
    281                           (Expr (Evar (succ_pos_of_nat 152))
    282                             (Tpointer Any (Tint I16 Signed  ))))
    283                         (Ssequence
    284                         (Sassign (Expr (Evar (succ_pos_of_nat 152))
    285                                    (Tpointer Any (Tint I16 Signed  )))
    286                           (Expr (Ebinop Oadd
    287                             (Expr (Evar (succ_pos_of_nat 136))
    288                               (Tpointer Any (Tint I16 Signed  )))
    289                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    290                             (Tpointer Any (Tint I16 Signed  ))))
    291                         (Ssequence
    292                         (Sassign (Expr (Ederef
    293                                    (Expr (Evar (succ_pos_of_nat 135))
    294                                      (Tpointer Any (Tint I16 Signed  ))))
    295                                    (Tint I16 Signed  ))
    296                           (Expr (Ederef
    297                             (Expr (Evar (succ_pos_of_nat 136))
    298                               (Tpointer Any (Tint I16 Signed  ))))
    299                             (Tint I16 Signed  )))
    300                         (Ssequence
    301                         (Sassign (Expr (Evar (succ_pos_of_nat 134))
    302                                    (Tint I32 Signed  ))
    303                           (Expr (Ebinop Osub
    304                             (Expr (Evar (succ_pos_of_nat 133))
    305                               (Tint I32 Signed  ))
    306                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    307                             (Tint I32 Signed  )))
    308                         (Ssequence
    309                         (Sassign (Expr (Evar (succ_pos_of_nat 133))
    310                                    (Tint I32 Signed  ))
    311                           (Expr (Evar (succ_pos_of_nat 134))
    312                             (Tint I32 Signed  )))
    313                         (Sifthenelse (Expr (Ebinop Ogt
    314                                        (Expr (Evar (succ_pos_of_nat 134))
    315                                          (Tint I32 Signed  ))
    316                                        (Expr (Econst_int (repr 0))
    317                                          (Tint I32 Signed  )))
    318                                        (Tint I32 Signed  ))
    319                           (Sgoto (succ_pos_of_nat 154))
    320                           Sskip))))))))
    321                         (LSdefault
    322                           Sskip)))))))))
    323       )))
    324    
    325    
    326    
    327   ));
    328   mk_pair ?? (succ_pos_of_nat 155 (* main *)) (Internal (
    329     mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 156) (Tarray Any (Tint I16 Signed  ) 3); mk_pair ?? (succ_pos_of_nat 157) (Tarray Any (Tint I16 Signed  ) 3)]
     298                             (Tint I16 Signed  )))
     299                         (Ssequence
     300                         (Sassign (Expr (Evar (succ_pos_of_nat 2))
     301                                    (Tint I32 Signed  ))
     302                           (Expr (Ebinop Osub
     303                             (Expr (Evar (succ_pos_of_nat 1))
     304                               (Tint I32 Signed  ))
     305                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     306                             (Tint I32 Signed  )))
     307                         (Ssequence
     308                         (Sassign (Expr (Evar (succ_pos_of_nat 1))
     309                                    (Tint I32 Signed  ))
     310                           (Expr (Evar (succ_pos_of_nat 2))
     311                             (Tint I32 Signed  )))
     312                         (Sifthenelse (Expr (Ebinop Ogt
     313                                        (Expr (Evar (succ_pos_of_nat 2))
     314                                          (Tint I32 Signed  ))
     315                                        (Expr (Econst_int (repr 0))
     316                                          (Tint I32 Signed  )))
     317                                        (Tint I32 Signed  ))
     318                           (Sgoto (succ_pos_of_nat 22))
     319                           Sskip))))))))
     320                         (LSdefault
     321                           Sskip)))))))))
     322       )))
     323     
     324     
     325     
     326   )〉;
     327  〈succ_pos_of_nat 23 (* main *), Internal (
     328    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 24, (Tarray Any (Tint I16 Signed  ) 3)〉 ; 〈succ_pos_of_nat 25, (Tarray Any (Tint I16 Signed  ) 3)〉 ]
    330329      (Ssequence
    331330      (Sassign (Expr (Ederef
    332331                 (Expr (Ebinop Oadd
    333                    (Expr (Evar (succ_pos_of_nat 156))
     332                   (Expr (Evar (succ_pos_of_nat 24))
    334333                     (Tarray Any (Tint I16 Signed  ) 3))
    335334                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     
    341340      (Sassign (Expr (Ederef
    342341                 (Expr (Ebinop Oadd
    343                    (Expr (Evar (succ_pos_of_nat 156))
     342                   (Expr (Evar (succ_pos_of_nat 24))
    344343                     (Tarray Any (Tint I16 Signed  ) 3))
    345344                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    351350      (Sassign (Expr (Ederef
    352351                 (Expr (Ebinop Oadd
    353                    (Expr (Evar (succ_pos_of_nat 156))
     352                   (Expr (Evar (succ_pos_of_nat 24))
    354353                     (Tarray Any (Tint I16 Signed  ) 3))
    355354                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     
    359358          (Tint I16 Signed  )))
    360359      (Ssequence
    361       (Scall (None ?) (Expr (Evar (succ_pos_of_nat 132))
    362                         (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
    363         [(Expr (Evar (succ_pos_of_nat 157))
     360      (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
     361                           (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
     362        [(Expr (Evar (succ_pos_of_nat 25))
    364363           (Tarray Any (Tint I16 Signed  ) 3));
    365         (Expr (Evar (succ_pos_of_nat 156))
    366           (Tarray Any (Tint I16 Signed  ) 3));
     364        (Expr (Evar (succ_pos_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
    367365        (Expr (Econst_int (repr 3)) (Tint I32 Signed  ))])
    368       (Sreturn (Some ? (Expr (Ebinop Oadd
    369                          (Expr (Ebinop Oadd
    370                            (Expr (Ecast (Tint I32 Signed  )
    371                              (Expr (Ederef
    372                                (Expr (Ebinop Oadd
    373                                  (Expr (Evar (succ_pos_of_nat 157))
    374                                    (Tarray Any (Tint I16 Signed  ) 3))
    375                                  (Expr (Econst_int (repr 0))
    376                                    (Tint I32 Signed  )))
    377                                  (Tarray Any (Tint I16 Signed  ) 3)))
    378                                (Tint I16 Signed  ))) (Tint I32 Signed  ))
    379                            (Expr (Ecast (Tint I32 Signed  )
    380                              (Expr (Ederef
    381                                (Expr (Ebinop Oadd
    382                                  (Expr (Evar (succ_pos_of_nat 157))
    383                                    (Tarray Any (Tint I16 Signed  ) 3))
    384                                  (Expr (Econst_int (repr 1))
    385                                    (Tint I32 Signed  )))
    386                                  (Tarray Any (Tint I16 Signed  ) 3)))
    387                                (Tint I16 Signed  ))) (Tint I32 Signed  )))
    388                            (Tint I32 Signed  ))
    389                          (Expr (Ecast (Tint I32 Signed  )
    390                            (Expr (Ederef
    391                              (Expr (Ebinop Oadd
    392                                (Expr (Evar (succ_pos_of_nat 157))
    393                                  (Tarray Any (Tint I16 Signed  ) 3))
    394                                (Expr (Econst_int (repr 2))
    395                                  (Tint I32 Signed  )))
    396                                (Tarray Any (Tint I16 Signed  ) 3)))
    397                              (Tint I16 Signed  ))) (Tint I32 Signed  )))
    398                          (Tint I32 Signed  ))))))))
     366      (Sreturn (Some expr (Expr (Ebinop Oadd
     367                            (Expr (Ebinop Oadd
     368                              (Expr (Ecast (Tint I32 Signed  )
     369                                (Expr (Ederef
     370                                  (Expr (Ebinop Oadd
     371                                    (Expr (Evar (succ_pos_of_nat 25))
     372                                      (Tarray Any (Tint I16 Signed  ) 3))
     373                                    (Expr (Econst_int (repr 0))
     374                                      (Tint I32 Signed  )))
     375                                    (Tarray Any (Tint I16 Signed  ) 3)))
     376                                  (Tint I16 Signed  ))) (Tint I32 Signed  ))
     377                              (Expr (Ecast (Tint I32 Signed  )
     378                                (Expr (Ederef
     379                                  (Expr (Ebinop Oadd
     380                                    (Expr (Evar (succ_pos_of_nat 25))
     381                                      (Tarray Any (Tint I16 Signed  ) 3))
     382                                    (Expr (Econst_int (repr 1))
     383                                      (Tint I32 Signed  )))
     384                                    (Tarray Any (Tint I16 Signed  ) 3)))
     385                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
     386                              (Tint I32 Signed  ))
     387                            (Expr (Ecast (Tint I32 Signed  )
     388                              (Expr (Ederef
     389                                (Expr (Ebinop Oadd
     390                                  (Expr (Evar (succ_pos_of_nat 25))
     391                                    (Tarray Any (Tint I16 Signed  ) 3))
     392                                  (Expr (Econst_int (repr 2))
     393                                    (Tint I32 Signed  )))
     394                                  (Tarray Any (Tint I16 Signed  ) 3)))
     395                                (Tint I16 Signed  ))) (Tint I32 Signed  )))
     396                            (Tint I32 Signed  ))))))))
    399397   
    400398   
    401399   
    402   ))]
    403   (succ_pos_of_nat 155)
     400  )]
     401  (succ_pos_of_nat 23)
    404402  []
    405403.
    406404
    407 nremark exec: result ? (exec_up_to myprog 80 []).
    408 nnormalize;  (* you can examine the result here *)
    409 @; nqed.
     405example exec:
     406  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0)]; OK ? (is_final s)) = OK ? (Some ? (repr 6)).
     407normalize @refl
     408qed.
  • src/Clight/test/factorial.ma

    r415 r717  
    1 include "Animation.ma".
     1include "Clight/Animation.ma".
    22
    3 ndefinition myprog := mk_program fundef type
    4  [mk_pair ?? (succ_pos_of_nat 132 (* get_input *)) (External (succ_pos_of_nat 132) Tnil (Tint I32 Signed  ));
    5   mk_pair ?? (succ_pos_of_nat 133 (* main *)) (Internal (
    6     mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 135) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 136) (Tint I32 Signed  )]
     3definition myprog := mk_program fundef type
     4  [〈succ_pos_of_nat 0 (* get_input *), External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
     5  〈succ_pos_of_nat 1 (* main *), Internal (
     6    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed  )〉 ]
    77      (Ssequence
    8       (Scall (Some ? (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed  )))
    9         (Expr (Evar (succ_pos_of_nat 132))
     8      (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
     9        (Expr (Evar (succ_pos_of_nat 0))
    1010          (Tfunction Tnil (Tint I32 Signed  )))
    1111        [])
    1212      (Ssequence
    13       (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
     13      (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
    1414        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    1515      (Ssequence
    16       (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
     16      (Ssequence
     17      (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    1718              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    1819        (Expr (Ebinop Ole
    19           (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
    20           (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed  )))
     20          (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     21          (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
    2122          (Tint I32 Signed  ))
    22         (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
     23        (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    2324          (Expr (Ebinop Oadd
    24             (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
     25            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    2526            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    2627            (Tint I32 Signed  )))
    27         (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
     28        (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
    2829          (Expr (Ebinop Omul
    29             (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
    30             (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  )))
     30            (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
     31            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  )))
    3132            (Tint I32 Signed  )))
    3233      )
    33       (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 135))
    34                          (Tint I32 Signed  )))))))
     34      Sskip)
     35      (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     36                            (Tint I32 Signed  )))))))
    3537   
    3638   
    3739   
    38   ))]
    39   (succ_pos_of_nat 133)
     40  )]
     41  (succ_pos_of_nat 1)
    4042  []
    4143.
    4244
    43 nremark exec: result ? (exec_up_to myprog 40 [EVint (repr 5)]).
    44 nnormalize;  (* you can examine the result here *)
    45 @; nqed.
     45example exec:
     46  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 5)]; OK ? (is_final s)) = OK ? (Some ? (repr 120)).
     47normalize  (* you can examine the result here *)
     48@refl qed.
  • src/Clight/test/memorymodel.ma

    r409 r717  
    1313(**************************************************************************)
    1414
    15 include "Mem.ma".
     15include "common/Mem.ma".
    1616
    1717
     
    2020   access, preventing you reading back more information than the memory can
    2121   store. *)
    22 ndefinition store0 := empty.
    23 ndefinition store1block : mem × block ≝ alloc store0 0 4 Any.
    24 ndefinition store1 : mem ≝ fst ?? store1block.
    25 ndefinition block := snd ?? store1block.
     22definition store0 := empty.
     23definition store1block : mem × block ≝ alloc store0 0 4 Any.
     24definition store1 : mem ≝ fst ?? store1block.
     25definition block := snd ?? store1block.
    2626
    2727(* write a value *)
    28 ndefinition store2 : mem.
    29   nletin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
     28definition store2 : mem.
     29  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
    3030
    31   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    32   ##| #rr; #_; napply rr ##] nqed.
     31  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     32  | #rr #_ @rr ] qed.
    3333
    3434(* overwrite the first byte of the value *)
    35 ndefinition store3 : mem.
    36   nletin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
     35definition store3 : mem.
     36  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
    3737
    38   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    39   ##| #rr; #_; napply rr ##] nqed.
     38  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     39  | #rr #_ @ rr ] qed.
    4040 
    4141(* The size checking rejects the read and gives us Some Vundef. *)
    42 nremark vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. //; nqed.
     42example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
    4343
    4444(* The read is successful and returns a signed version of the value. *)
    45 nremark vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
     45example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
    4646
    4747(* NB: Double frees are allowed by the memory model (although not necessarily
    4848       by the language). *)
    49 ndefinition store4 := free store3 block.
    50 ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.
     49definition store4 := free store3 block.
     50definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed.
    5151
    5252(* No ordering is imposed on deallocation (even though alloc and free are only used for
    5353   stack memory in the semantics. *)
    54 ndefinition storeA := empty.
    55 ndefinition storeBblkB := alloc storeA 0 4 Any.
    56 ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
    57 ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    58 ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)).
    59 nwhd in r; napply r; nqed.
     54definition storeA := empty.
     55definition storeBblkB := alloc storeA 0 4 Any.
     56definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
     57definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
     58definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
     59whd in r @r qed.
    6060
    6161(* Access to the "object representation" (as the C standard puts it) is not specified. *)
    62 ndefinition storeI := empty.
    63 ndefinition storeIIblk := alloc storeA 0 4 Any.
    64 ndefinition storeIII : mem.
    65  nletin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
    66   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    67   ##| #rr; #_; napply rr ##] nqed.
    68 ndefinition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
    69 nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)
     62definition storeI := empty.
     63definition storeIIblk := alloc storeA 0 4 Any.
     64definition storeIII : mem.
     65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
     66  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     67  | #rr #_ @rr ] qed.
     68definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
     69example byteundef: byte = Some ? Vundef. // qed. (* :( *)
  • src/Clight/test/transform1.ma

    r25 r717  
    1 
     1(*
    22include "Csyntax.ma".
    33include "AST.ma".
     
    131131         ##]
    132132       ##|
     133
     134*)
Note: See TracChangeset for help on using the changeset viewer.