Changeset 961 for src/Clight/test


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

Location:
src/Clight/test
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/memorymodel.ma

    r717 r961  
    2727(* write a value *)
    2828definition store2 : mem.
    29   letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
     29  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));
    3030
    3131  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     
    3434(* overwrite the first byte of the value *)
    3535definition store3 : mem.
    36   letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
     36  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
    3737
    3838  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     
    4242example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
    4343
    44 (* The read is successful and returns a signed version of the value. *)
    45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
     44(* The read is successful and returns the value. *)
     45example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed.
    4646
    4747(* NB: Double frees are allowed by the memory model (although not necessarily
     
    6363definition storeIIblk := alloc storeA 0 4 Any.
    6464definition storeIII : mem.
    65  letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
     65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
    6666  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
    6767  | #rr #_ @rr ] qed.
  • src/Clight/test/search.ma

    r816 r961  
    88       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    99         (Expr (Ecast (Tint I8 Unsigned )
    10            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     10           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1111           (Tint I8 Unsigned )))
    1212       (Ssequence
     
    1717               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
    1818               (Tint I32 Signed  ))
    19              (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     19             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2020             (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    2121       (Ssequence
     
    3939                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    4040                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    41                (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     41               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    4242               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    4343         (Ssequence
     
    8080                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    8181                   (Tint I32 Signed  ))
    82                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     82                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    8383                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    8484           Sskip)
     
    103103                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    104104                   (Tint I32 Signed  ))
    105                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     105                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    106106                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    107107           Sskip)))))
    108108       Sskip)
    109109       (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
    110                              (Expr (Eunop Oneg (Expr (Econst_int (repr 1))
     110                             (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
    111111                                                 (Tint I32 Signed  )))
    112112                               (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
     
    122122                   (Expr (Evar (ident_of_nat 4))
    123123                     (Tarray Any (Tint I8 Unsigned ) 5))
    124                    (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    125                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    126         (Expr (Ecast (Tint I8 Unsigned )
    127           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    128           (Tint I8 Unsigned )))
    129       (Ssequence
    130       (Sassign (Expr (Ederef
    131                  (Expr (Ebinop Oadd
    132                    (Expr (Evar (ident_of_nat 4))
    133                      (Tarray Any (Tint I8 Unsigned ) 5))
    134                    (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    135                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    136         (Expr (Ecast (Tint I8 Unsigned )
    137           (Expr (Econst_int (repr 18)) (Tint I32 Signed  )))
    138           (Tint I8 Unsigned )))
    139       (Ssequence
    140       (Sassign (Expr (Ederef
    141                  (Expr (Ebinop Oadd
    142                    (Expr (Evar (ident_of_nat 4))
    143                      (Tarray Any (Tint I8 Unsigned ) 5))
    144                    (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    145                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    146         (Expr (Ecast (Tint I8 Unsigned )
    147           (Expr (Econst_int (repr 23)) (Tint I32 Signed  )))
    148           (Tint I8 Unsigned )))
    149       (Ssequence
    150       (Sassign (Expr (Ederef
    151                  (Expr (Ebinop Oadd
    152                    (Expr (Evar (ident_of_nat 4))
    153                      (Tarray Any (Tint I8 Unsigned ) 5))
    154                    (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
    155                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    156         (Expr (Ecast (Tint I8 Unsigned )
    157           (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
    158           (Tint I8 Unsigned )))
    159       (Ssequence
    160       (Sassign (Expr (Ederef
    161                  (Expr (Ebinop Oadd
    162                    (Expr (Evar (ident_of_nat 4))
    163                      (Tarray Any (Tint I8 Unsigned ) 5))
    164                    (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
    165                    (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
    166         (Expr (Ecast (Tint I8 Unsigned )
    167           (Expr (Econst_int (repr 120)) (Tint I32 Signed  )))
     124                   (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     125                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     126        (Expr (Ecast (Tint I8 Unsigned )
     127          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     128          (Tint I8 Unsigned )))
     129      (Ssequence
     130      (Sassign (Expr (Ederef
     131                 (Expr (Ebinop Oadd
     132                   (Expr (Evar (ident_of_nat 4))
     133                     (Tarray Any (Tint I8 Unsigned ) 5))
     134                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     135                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     136        (Expr (Ecast (Tint I8 Unsigned )
     137          (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
     138          (Tint I8 Unsigned )))
     139      (Ssequence
     140      (Sassign (Expr (Ederef
     141                 (Expr (Ebinop Oadd
     142                   (Expr (Evar (ident_of_nat 4))
     143                     (Tarray Any (Tint I8 Unsigned ) 5))
     144                   (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     145                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     146        (Expr (Ecast (Tint I8 Unsigned )
     147          (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
     148          (Tint I8 Unsigned )))
     149      (Ssequence
     150      (Sassign (Expr (Ederef
     151                 (Expr (Ebinop Oadd
     152                   (Expr (Evar (ident_of_nat 4))
     153                     (Tarray Any (Tint I8 Unsigned ) 5))
     154                   (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     155                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     156        (Expr (Ecast (Tint I8 Unsigned )
     157          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
     158          (Tint I8 Unsigned )))
     159      (Ssequence
     160      (Sassign (Expr (Ederef
     161                 (Expr (Ebinop Oadd
     162                   (Expr (Evar (ident_of_nat 4))
     163                     (Tarray Any (Tint I8 Unsigned ) 5))
     164                   (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
     165                   (Tarray Any (Tint I8 Unsigned ) 5))) (Tint I8 Unsigned ))
     166        (Expr (Ecast (Tint I8 Unsigned )
     167          (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
    168168          (Tint I8 Unsigned )))
    169169      (Ssequence
     
    173173        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
    174174        (Expr (Ecast (Tint I8 Unsigned )
    175           (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
     175          (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
    176176          (Tint I8 Unsigned ));
    177177        (Expr (Ecast (Tint I8 Unsigned )
    178           (Expr (Econst_int (repr 57)) (Tint I32 Signed  )))
     178          (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
    179179          (Tint I8 Unsigned ))])
    180180      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     
    189189.
    190190
    191 example exec: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     191example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    192192normalize  (* you can examine the result here *)
    193193@refl
     
    197197include "Cminor/semantics.ma".
    198198
    199 example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     199example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
    200200normalize
    201201@refl
  • src/Clight/test/sum.ma

    r881 r961  
    88       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    99         (Expr (Ecast (Tint I8 Unsigned )
    10            (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     10           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1111           (Tint I8 Unsigned )))
    1212       (Ssequence
    1313       (Ssequence
    1414       (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    15                (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     15               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1616         (Expr (Ebinop Olt
    1717           (Expr (Ecast (Tint I32 Unsigned)
     
    2323           (Expr (Ebinop Oadd
    2424             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    25              (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     25             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2626             (Tint I32 Signed  )))
    2727         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     
    5151  (ident_of_nat 0)
    5252  [〈〈〈ident_of_nat 3 (* src *),
    53      [(Init_int8 (repr 28)) ; (Init_int8 (repr 17)) ; (Init_int8 (repr 17)) ;
    54      (Init_int8 (repr 8)) ; (Init_int8 (repr 4)) ]〉, Any〉,
     53     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ;
     54     (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉,
    5555     (Tarray Any (Tint I8 Unsigned ) 5)〉]
    5656.
    5757
    58 example exec: finishes_with (repr 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     58example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    5959normalize  (* you can examine the result here *)
    6060@refl
Note: See TracChangeset for help on using the changeset viewer.