Changeset 2176 for src/Clight


Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

Location:
src/Clight
Files:
17 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2019 r2176  
    2424    ]
    2525  | Vptr _ ⇒ match ty with
    26     [ Tpointer _ _ ⇒ OK ? true
     26    [ Tpointer _ ⇒ OK ? true
    2727    | _ ⇒ Error ? (msg TypeMismatch)
    2828    ]
    29   | Vnull _ ⇒ match ty with
    30     [ Tpointer _ _ ⇒ OK ? false
     29  | Vnull ⇒ match ty with
     30    [ Tpointer _ ⇒ OK ? false
    3131    | _ ⇒ Error ? (msg TypeMismatch)
    3232    ]
     
    3737#v #ty #r #H elim H; #v #t #H' elim H';
    3838  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    39   | #ptr #r #ty %{ true} % //
     39  | #ptr #ty %{ true} % //
    4040  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
    4141  | * #sg %{ false} % //
    42   | #r #r' #t %{ false} % //;
     42  | #t %{ false} % //;
    4343  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
    4444  ]
     
    8181    if eq_intsize sz sz' then
    8282      match ty' with
    83       [ Tpointer r _ ⇒ OK ? (Vnull r)
    84       | Tarray r _ _ ⇒ OK ? (Vnull r)
    85       | Tfunction _ _ ⇒ OK ? (Vnull Code)
     83      [ Tpointer _ ⇒ OK ? Vnull
     84      | Tarray _ _ ⇒ OK ? Vnull
     85      | Tfunction _ _ ⇒ OK ? Vnull
    8686      | _ ⇒ Error ? (msg BadCast)
    8787      ]
     
    9090  ]
    9191| false ⇒ Error ? (msg BadCast)
     92].
     93
     94definition ptr_like_type : type → bool ≝
     95λt. match t with
     96[ Tpointer _ ⇒ true
     97| Tarray _ _ ⇒ true
     98| Tfunction _ _ ⇒ true
     99| _ ⇒ false
    92100].
    93101
     
    103111      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
    104112      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
    105       | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    106       | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     113      | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     114      | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    107115      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    108116      | _ ⇒ Error ? (msg BadCast)
    109117      ])
    110118    (Error ? (msg BadCast))
    111   | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    112   | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     119  | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
     120  | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    113121  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
    114122  | _ ⇒ Error ? (msg TypeMismatch)
     
    125133  ]
    126134| Vptr ptr ⇒
    127     do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
     135(*    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
    128136    do u ← match eq_region_dec (ptype ptr) s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
    129137    do s' ← match ty' with
     
    133141    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
    134142    | inr _ ⇒ Error ? (msg BadCast)
    135     ]
    136 | Vnull r ⇒
     143    ]*)
     144    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? (Vptr ptr) else Error ? (msg BadCast)
     145| Vnull ⇒
     146(*
    137147    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
    138148    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
     
    140150         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    141151         | _ ⇒ Error ? (msg BadCast) ];
    142     OK ? (Vnull s')
     152    OK ? (Vnull s')*)
     153    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? Vnull else Error ? (msg BadCast)
    143154| _ ⇒ Error ? (msg BadCast)
    144155].
     
    184195      do 〈lo,tr〉 ← exec_lvalue ge en m a;
    185196      match ty with
    186       [ Tpointer r _ ⇒
     197      [ Tpointer _ ⇒
    187198        let 〈loc,ofs〉 ≝ lo in
    188           match pointer_compat_dec loc r with
     199(*          match pointer_compat_dec loc r with
    189200          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
    190201          | inr _ ⇒ Error ? (msg TypeMismatch)
    191           ]
     202          ]*)  OK ? 〈Vptr (mk_pointer loc ofs), tr〉
    192203      | _ ⇒ Error ? (msg BadlyTypedTerm)
    193204      ]
     
    285296| cons h vars ⇒
    286297  let 〈id,ty〉 ≝ h in
    287   let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
     298  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) XData in
    288299      exec_alloc_variables (add ?? en id b1) m1 vars
    289300].
  • src/Clight/CexecComplete.ma

    r2120 r2176  
    3939] qed.
    4040
     41(*
    4142lemma is_pointer_compat_true: ∀b,sp.
    4243  pointer_compat b sp →
     
    4647[ //
    4748| #H' @False_ind @(absurd … H H')
    48 ] qed.
     49] qed.*)
    4950
    5051theorem is_det: ∀p,s,s'.
     
    9293| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    9394| #m #f #sz #sz' @refl
     95| #m #ty0 #ty0' #ptr #H1 #H2 cases H1 cases H2 //
     96| #m #sz #sg #ty' #H' cases H' [ #ty'' | #ty'' #n | #tys #ty'' ] whd in ⊢ (??%?);
     97  >intsize_eq_elim_true whd in ⊢ (??%?); cases sz //
     98| #m #ty0 #ty0' #H1 #H2 cases H1 cases H2 //
     99(*
    94100| #m #ty #ty' * #r #b #pc #ofs #r' #H1 #H2 #pc'
    95101    elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
     
    103109| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
    104110    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
     111*)
    105112] qed.
    106113
     
    122129  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true
    123130    >(eq_bv_false … ne) //
    124   | * #r #b #pc #i #i0 #s %{ true} % //
     131  | *  #b #i #i0 %{ true} % //
    125132  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    126133  | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //
    127   | #r #r' #t %{ false} % //;
     134  | #t %{ false} % //;
    128135  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
    129136  ]
     
    133140#v #ty #H elim H;
    134141  [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //;
    135   | * #p #b #i #i0 #s //
     142  | #s //
    136143  | #f #s #ne whd; >(Feq_zero_false … ne) //;
    137144  ]
     
    141148#v #ty #H elim H;
    142149  [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //;
    143   | #r #r' #t //;
     150  | #t //;
    144151  | #s whd; >(Feq_zero_true …) //;
    145152  ]
     
    165172    whd in ⊢ (??%?); change with (load_value_of_type' ty m 〈l,off〉) in H2:(??%?);
    166173    >H2 @refl
    167 | #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
     174| #e #ty #l #off #tr #H1 #H2 whd in ⊢ (??%?);
    168175    >(yields_eq ??? H2) whd in ⊢ (??%?);
    169     @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
     176(*    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd*)
    170177    @refl
    171178| #ty' #sz #sg @refl
     
    221228| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
    222229    >e2 @refl
    223 | #e #ty #r #l #pc #ofs #tr #H1 #H2 whd in ⊢ (??%?);
     230| #e #ty #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
    224231    >(yields_eq ??? H2)
    225232    @refl
     
    262269  (it:∀i,s. P (Tint i s))
    263270  (fl:∀f. P (Tfloat f))
    264   (pt:∀s,t. P t → P (Tpointer s t))
    265   (ar:∀s,t,n. P t → P (Tarray s t n))
     271  (pt:∀t. P t → P (Tpointer t))
     272  (ar:∀t,n. P t → P (Tarray t n))
    266273  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
    267274  (st:∀i,fl. P (Tstruct i fl))
    268275  (un:∀i,fl. P (Tunion i fl))
    269   (cp:∀r,i. P (Tcomp_ptr r i))
     276  (cp:∀i. P (Tcomp_ptr i))
    270277  (nl:Q Tnil)
    271278  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
     
    275282  | Tint i s ⇒ it i s
    276283  | Tfloat s ⇒ fl s
    277   | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    278   | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     284  | Tpointer t' ⇒ pt t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     285  | Tarray t' n ⇒ ar t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    279286  | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
    280287  | Tstruct i fs ⇒ st i fs
    281288  | Tunion i fs ⇒ un i fs
    282   | Tcomp_ptr r i ⇒ cp r i
     289  | Tcomp_ptr i ⇒ cp i
    283290  ]
    284291and typelist_ind2l
     
    287294  (it:∀i,s. P (Tint i s))
    288295  (fl:∀f. P (Tfloat f))
    289   (pt:∀s,t. P t → P (Tpointer s t))
    290   (ar:∀s,t,n. P t → P (Tarray s t n))
     296  (pt:∀t. P t → P (Tpointer t))
     297  (ar:∀t,n. P t → P (Tarray t n))
    291298  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
    292299  (st:∀i,fl. P (Tstruct i fl))
    293300  (un:∀i,fl. P (Tunion i fl))
    294   (cp:∀r,i. P (Tcomp_ptr r i))
     301  (cp:∀i. P (Tcomp_ptr i))
    295302  (nl:Q Tnil)
    296303  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
  • src/Clight/CexecSound.ma

    r2106 r2176  
    55 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    66#v #ty #r
    7 cases v; [ | #sz #i | #f | #r1 | #ptr ]
    8 cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
     7cases v; [ | #sz #i | #f | | #ptr ]
     8cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: (*#rg*) #ty | 5,14,23,32,41: (*#r*) #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: (*#r*) #id ]
    99whd in ⊢ (??%? → ?);
    1010[ 2: @intsize_eq_elim_elim
     
    3939@eq_bv_elim
    4040[ #e >e
    41     cases ty; [ | #sz' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     41    cases ty; [ | #sz' #sg | #fs | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
    4242    whd in ⊢ (??%? → ?); #H [ 2: | *: destruct ]
    43     cases ty' in H ⊢ %; [ | #sz'' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     43    cases ty' in H ⊢ %; [ | #sz'' #sg | #fs | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
    4444    try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z //
    4545| #_ whd in ⊢ (??%? → ?); #H destruct
     
    5454  [ #H whd in H:(??%?); destruct;
    5555  | 3: #a #H whd in H:(??%?); destruct;
    56   | 7,8,9: #a #b #H whd in H:(??%?); destruct;
     56  | 7,8,9: #a [ 1,2: #b ] #H whd in H:(??%?); destruct;
    5757  | #sz1 #si1 cases ty';
    5858    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
     
    6464      | *; whd #H whd in H:(??%?); destruct; @cast_if
    6565      ]
    66     | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
     66    | 2,7,8,9: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6767      [ 1,3,5,7: #NE #H destruct
    6868      | *: *; whd #H whd in H:(??%?); destruct; //
    6969      ]
    70     | 4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
    71                  | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    72                  | #args #rty letin t ≝ (Tfunction args rty) ]
     70    | 4,5,6: [ #ty'' letin t ≝ (Tpointer ty'')
     71             | #ty'' #n letin t ≝ (Tarray ty'' n)
     72             | #args #rty letin t ≝ (Tfunction args rty) ]
    7373        whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    7474        [ 1,3,5: #NE #H destruct
     
    8181        ]
    8282    ]
    83   | *: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
    84            | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    85            | #args #rty letin t ≝ (Tfunction args rty) ]
     83  | *: [ #ty'' letin t ≝ (Tpointer ty'')
     84       | #ty'' #n letin t ≝ (Tarray ty'' n)
     85       | #args #rty letin t ≝ (Tfunction args rty) ]
    8686        whd in ⊢ (??%? → ?);
    8787        lapply (try_cast_null_sound m sz i t ty' v');
     
    9191        ]
    9292  ]
    93 | #f cases ty;  [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
    94                     [ cases ty'; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
     93| #f cases ty;  [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     94                    [ cases ty'; [ #e | 3,4,9: #a #e | 2,6,7,8: #a #b #e | #a #b #e ]
    9595                        whd in e:(??%?); destruct; //;
    9696                    | *: #e whd in e:(??%?); destruct
    9797                    ]
    98 | #r cases ty; [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
    99     whd in ⊢ (??%? → ?); #H destruct; cases (eq_region_dec r ?) in H;
    100     whd in ⊢ (? → ??%? → ?); #H1 #H2 destruct;
    101     cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
     98| cases ty; [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     99    whd in ⊢ (??%? → ?); #H destruct
     100    cases ty' in H; normalize; try #a try #b try #c try #d destruct;
    102101    @cast_pp_z //;
     102(*
    103103| #ptr whd in ⊢ (??%? → ?); #e
    104104    elim (bind_inversion ????? e) #s * #es #e'
     
    119119        ]
    120120    ]
     121*)
     122| #ptr
     123  cases ty; [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     124  #E whd in E:(??%?); destruct
     125  cases ty' in E ⊢ %; normalize #A try #B try #C try #D destruct /2/
    121126] qed.
    122127
     
    142147    ]
    143148| #ty #e #He whd in ⊢ (???%);
    144     @bind2_OK #v cases v / by / * #r #l #pc #ofs #tr #Hv whd
     149    @bind2_OK #v cases v / by / * #l #ofs #tr #Hv whd
    145150    >Hv in He; #He
    146     @eval_Ederef [ 3: @He | *: skip ]
     151    @eval_Ederef @He
    147152| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
    148   cases ty try (try #a try #b try #c @I) * #pty
    149   cases loc in H ⊢ %; * #loc' #H
    150   whd try @I
     153  cases ty try (try #a try #b try #c @I)
     154  #ty' whd
    151155  @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He''
    152156| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
     
    210214] qed.
    211215
    212 lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,pc,off,tr,ty.
    213 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer r loc pc off)) tr →
     216lemma addrof_eval_lvalue: ∀ge,en,m,e,loc,off,tr,ty.
     217eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer loc off)) tr →
    214218eval_lvalue ge en m e loc off tr.
    215 #ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
     219#ge #en #m #e #loc #off #tr #ty #H inversion H;
    216220[ 1,2,5: #a #b #c #H @False_ind destruct (H);
    217221| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
     
    219223    [ #a #b #c #d #bad destruct (bad);
    220224    | #a #b #c #d #e #bad destruct (bad);
    221     | #a #b #c #d #e #f #g #h #bad destruct (bad);
     225    | #a #b #c #d #e #f #bad destruct (bad);
    222226    | #a #b #c #d #e #f #g #h #i #j #k #l #bad @False_ind destruct (bad);
    223227    | #a #b #c #d #e #f #g #h #i #j #bad destruct (bad);
    224228    ]
    225 | #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
     229| #e' #ty' #loc' #ofs' #tr' #H' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
    226230| #a #b #c #d #e #f #g #h #bad destruct (bad);
    227231| #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
     
    238242lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
    239243exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    240 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr (mk_pointer r (mk_block r loc) (same_compat ??) off), tr〉.
     244exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block r loc) off), tr〉.
    241245#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
    242246>H whd in ⊢ (??%?); cases r @refl
     
    248252cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    249253[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
    250     @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
     254    @(addrof_eval_lvalue … (Tpointer Tvoid))
    251255    lapply (addrof_exec_lvalue … H) #H'
    252     lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
     256    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer Tvoid)))
    253257    >H' #H'' @H''
    254258| #msg #_ whd @I
     
    284288[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    285289| * #id #ty #t #IH #en #m #en' #m'
    286   lapply (refl ? (alloc m O (sizeof ty) Any)) whd in ⊢ (? → ??%? → ?);
     290  lapply (refl ? (alloc m O (sizeof ty) XData)) whd in ⊢ (? → ??%? → ?);
    287291  cases (alloc ????) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
    288292 @(alloc_variables_cons … ALLOC)
     
    314318  [ //
    315319  | #ty #tys whd in ⊢ (???%);
    316     cases ty [ #sz #sg | #sz | #r ] cases v //
     320    cases ty [ #sz #sg | | #sz ] cases v //
    317321    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
    318322      @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
  • src/Clight/ClassifyOp.ma

    r1872 r2176  
    1414*)
    1515
    16 definition ptr_type ≝ λr,ty,n. match n with [ None ⇒ Tpointer r ty | Some n' ⇒ Tarray r ty n' ].
     16definition ptr_type ≝ λty,n. match n with [ None ⇒ Tpointer  ty | Some n' ⇒ Tarray ty n' ].
    1717
    1818inductive classify_add_cases : type → type → Type[0] ≝
    1919  (* integer addition is always done on a single type, the parser will insert any
    2020     necessary casts *)
    21   | add_case_ii: ∀sz,sg.          classify_add_cases (Tint sz sg)      (Tint sz sg)      (*Tint sz sg*)
    22   | add_case_ff: ∀sz.             classify_add_cases (Tfloat sz)       (Tfloat sz)       (*Tfloat sz*)
    23   | add_case_pi: ∀n,r,ty,sz,sg.   classify_add_cases (ptr_type r ty n) (Tint sz sg)      (*ptr_type r ty n*)
    24   | add_case_ip: ∀n,sz,sg,r,ty.   classify_add_cases (Tint sz sg)      (ptr_type r ty n) (*ptr_type r ty n*)
    25   | add_default: ∀ty1,ty2.        classify_add_cases ty1 ty2 (*ty'*).
     21  | add_case_ii: ∀sz,sg.      classify_add_cases (Tint sz sg)     (Tint sz sg)     (*Tint sz sg*)
     22  | add_case_ff: ∀sz.         classify_add_cases (Tfloat sz)      (Tfloat sz)      (*Tfloat sz*)
     23  | add_case_pi: ∀n,ty,sz,sg. classify_add_cases (ptr_type  ty n) (Tint sz sg)     (*ptr_type r ty n*)
     24  | add_case_ip: ∀n,sz,sg,ty. classify_add_cases (Tint sz sg)     (ptr_type ty n) (*ptr_type r ty n*)
     25  | add_default: ∀ty1,ty2.    classify_add_cases ty1 ty2 (*ty'*).
    2626
    2727definition classify_add : ∀ty1,ty2. classify_add_cases ty1 ty2 ≝ λty1: type. λty2: type.
     
    3030    match ty2 return λty2. classify_add_cases ? ty2 with
    3131    [ Tint sz2 sg2 ⇒ inttyp_eq_elim' sz1 sz2 sg1 sg2 (λsz1,sg1,sz2,sg2. classify_add_cases (Tint sz1 sg1) (Tint sz2 sg2)) (add_case_ii sz1 ?) (add_default ??)
    32     | Tpointer _ ty ⇒ add_case_ip (None ?) …
    33     | Tarray _ ty n ⇒ add_case_ip (Some ? n) …
     32    | Tpointer ty ⇒ add_case_ip (None ?) …
     33    | Tarray ty n ⇒ add_case_ip (Some ? n) …
    3434    | _ ⇒ add_default … ]
    3535  | Tfloat sz1 ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [ Tfloat sz2 ⇒ floatsize_eq_elim sz1 sz2 (λsz1,sz2. classify_add_cases (Tfloat sz1) (Tfloat sz2)) (add_case_ff sz1) (add_default …) | _ ⇒ add_default … ]
    36   | Tpointer _ ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
    37   | Tarray _ ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
     36  | Tpointer ty ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (None ?) … | _ ⇒ add_default … ]
     37  | Tarray ty n ⇒ match ty2 return λty2. classify_add_cases ? ty2 with [Tint _ _ ⇒ add_case_pi (Some ? n) … | _ ⇒ add_default … ]
    3838  | _ ⇒ add_default …
    3939  ].
    4040
    4141inductive classify_sub_cases : type → type → Type[0] ≝
    42   | sub_case_ii: ∀sz,sg.        classify_sub_cases (Tint sz sg)      (Tint sz sg)
    43   | sub_case_ff: ∀sz.           classify_sub_cases (Tfloat sz)       (Tfloat sz)
    44   | sub_case_pi: ∀n,r,ty,sz,sg. classify_sub_cases (ptr_type r ty n) (Tint sz sg)
    45   | sub_case_pp: ∀n1,n2,r1,ty1,r2,ty2. classify_sub_cases (ptr_type r1 ty1 n1) (ptr_type r2 ty2 n2)
     42  | sub_case_ii: ∀sz,sg.         classify_sub_cases (Tint sz sg)       (Tint sz sg)
     43  | sub_case_ff: ∀sz.            classify_sub_cases (Tfloat sz)        (Tfloat sz)
     44  | sub_case_pi: ∀n,ty,sz,sg.    classify_sub_cases (ptr_type  ty n)  (Tint sz sg)
     45  | sub_case_pp: ∀n1,n2,ty1,ty2. classify_sub_cases (ptr_type  ty1 n1) (ptr_type ty2 n2)
    4646  | sub_default: ∀ty1,ty2. classify_sub_cases ty1 ty2.
    4747
     
    5050  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_sub_cases ty1 ty2) (sub_case_ii sz1 sg1) (sub_default …)
    5151  | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_sub_cases ty1 ty2) (sub_case_ff sz1) (sub_default …)
    52   | Tpointer _ ty ⇒
     52  | Tpointer ty ⇒
    5353    match ty2 return λty2. classify_sub_cases ? ty2 with
    5454    [ Tint sz sg ⇒ sub_case_pi …
    55     | Tpointer _ _ ⇒ sub_case_pp (None ?) (None ?) …
    56     | Tarray _ _ n2 ⇒ sub_case_pp (None ?) (Some ? n2) …
     55    | Tpointer _ ⇒ sub_case_pp (None ?) (None ?) …
     56    | Tarray _ n2 ⇒ sub_case_pp (None ?) (Some ? n2) …
    5757    | _ ⇒ sub_default …]
    58   | Tarray _ ty n1 ⇒
     58  | Tarray ty n1 ⇒
    5959    match ty2 return λty2. classify_sub_cases ? ty2 with
    6060    [ Tint _ _ ⇒ sub_case_pi …
    61     | Tpointer _ _ ⇒ sub_case_pp (Some ? n1) (None ?) …
    62     | Tarray _ _ n2 ⇒ sub_case_pp (Some ? n1) (Some ? n2) …
     61    | Tpointer _ ⇒ sub_case_pp (Some ? n1) (None ?) …
     62    | Tarray _ n2 ⇒ sub_case_pp (Some ? n1) (Some ? n2) …
    6363    | _ ⇒ sub_default … ]
    6464  | _ ⇒ sub_default …
     
    8484inductive classify_cmp_cases : type → type → Type[0] ≝
    8585  | cmp_case_ii: ∀sz,sg.  classify_cmp_cases (Tint sz sg)      (Tint sz sg)
    86   | cmp_case_pp: ∀n,r,ty. classify_cmp_cases (ptr_type r ty n) (ptr_type r ty n)
     86  | cmp_case_pp: ∀n,ty.   classify_cmp_cases (ptr_type  ty n)  (ptr_type ty n)
    8787  | cmp_case_ff: ∀sz.     classify_cmp_cases (Tfloat sz)       (Tfloat sz)
    8888  | cmp_default: ∀ty,ty'. classify_cmp_cases ty ty'.
     
    9292  [ Tint sz1 sg1 ⇒ if_type_eq (Tint sz1 sg1) ty2 (λty1, ty2. classify_cmp_cases ty1 ty2) (cmp_case_ii sz1 sg1) (cmp_default …)
    9393  | Tfloat sz1 ⇒ if_type_eq (Tfloat sz1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_ff sz1) (cmp_default …)
    94   | Tpointer r1 ty1' ⇒ if_type_eq (Tpointer r1 ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
    95   | Tarray r1 ty1' n1 ⇒ if_type_eq (Tarray r1 ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
     94  | Tpointer  ty1' ⇒ if_type_eq (Tpointer ty1') ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (None ?) …) (cmp_default …)
     95  | Tarray  ty1' n1 ⇒ if_type_eq (Tarray ty1' n1) ty2 (λty1,ty2. classify_cmp_cases ty1 ty2) (cmp_case_pp (Some ? n1) …) (cmp_default …)
    9696  | _ ⇒ cmp_default …
    9797  ].
     
    104104  match ty with
    105105  [ Tfunction args res ⇒ fun_case_f args res
    106   | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
    107                                     | _ ⇒ fun_default
    108                                     ]
     106  | Tpointer ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
     107                                  | _ ⇒ fun_default
     108                                  ]
    109109  | _ ⇒ fun_default
    110110  ].
  • src/Clight/Csem.ma

    r2032 r2176  
    3939  | is_false_int: ∀sz,sg.
    4040      is_false (Vint sz (zero ?)) (Tint sz sg)
    41   | is_false_pointer: ∀r,r',t.
    42       is_false (Vnull r) (Tpointer r' t)
     41  | is_false_pointer: ∀t.
     42      is_false Vnull (Tpointer t)
    4343 | is_false_float: ∀sz.
    4444      is_false (Vfloat Fzero) (Tfloat sz).
     
    4848      n ≠ (zero ?) →
    4949      is_true (Vint sz n) (Tint sz sg)
    50   | is_true_pointer_pointer: ∀ptr,s,t.
    51       is_true (Vptr ptr) (Tpointer s t)
     50  | is_true_pointer_pointer: ∀ptr,t.
     51      is_true (Vptr ptr) (Tpointer t)
    5252  | is_true_float: ∀f,sz.
    5353      f ≠ Fzero →
     
    102102      | _ ⇒ None ?
    103103      ]
    104   | Tpointer _ _
     104  | Tpointer _
    105105      match v with
    106106      [ Vptr _ ⇒ Some ? Vfalse
    107       | Vnull _ ⇒ Some ? Vtrue
     107      | Vnull ⇒ Some ? Vtrue
    108108      | _ ⇒ None ?
    109109      ]
     
    131131        | _ ⇒ None ? ]
    132132      | _ ⇒ None ? ]
    133   | add_case_pi _ _ ty _ _ ⇒                    (**r pointer plus integer *)
     133  | add_case_pi _ ty _ _ ⇒                    (**r pointer plus integer *)
    134134      match v1 with
    135135      [ Vptr ptr1 ⇒ match v2 with
    136136        [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2))
    137137        | _ ⇒ None ? ]
    138       | Vnull r ⇒ match v2 with
    139         [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    140         | _ ⇒ None ? ]
    141       | _ ⇒ None ? ]
    142   | add_case_ip _ _ _ _ ty ⇒                    (**r integer plus pointer *)
     138      | Vnull ⇒ match v2 with
     139        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
     140        | _ ⇒ None ? ]
     141      | _ ⇒ None ? ]
     142  | add_case_ip _ _ _ ty ⇒                    (**r integer plus pointer *)
    143143      match v1 with
    144144      [ Vint sz1 n1 ⇒ match v2 with
    145145        [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1))
    146         | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?
     146        | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ?
    147147        | _ ⇒ None ? ]
    148148      | _ ⇒ None ? ]
     
    165165        | _ ⇒ None ? ]
    166166      | _ ⇒ None ? ]
    167   | sub_case_pi _ _ ty _ _ ⇒             (**r pointer minus integer *)
     167  | sub_case_pi _ ty _ _ ⇒             (**r pointer minus integer *)
    168168      match v1 with
    169169      [ Vptr ptr1 ⇒ match v2 with
    170170        [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2))
    171171        | _ ⇒ None ? ]
    172       | Vnull r ⇒ match v2 with
    173         [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    174         | _ ⇒ None ? ]
    175       | _ ⇒ None ? ]
    176   | sub_case_pp _ _ _ ty _ _ ⇒             (**r pointer minus pointer *)
     172      | Vnull ⇒ match v2 with
     173        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
     174        | _ ⇒ None ? ]
     175      | _ ⇒ None ? ]
     176  | sub_case_pp _ _ ty _ ⇒             (**r pointer minus pointer *)
    177177      match v1 with
    178178      [ Vptr ptr1 ⇒ match v2 with
     
    186186          else None ?
    187187        | _ ⇒ None ? ]
    188       | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
     188      | Vnull ⇒ match v2 with [ Vnull ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
    189189      | _ ⇒ None ? ]
    190190  | sub_default _ _ ⇒ None ?
     
    343343      | _ ⇒ None ?     
    344344      ]
    345   | cmp_case_pp _ _ _
     345  | cmp_case_pp _ _
    346346      match v1 with
    347347      [ Vptr ptr1 ⇒
     
    354354            else sem_cmp_mismatch c
    355355          else None ?
    356         | Vnull r2 ⇒ sem_cmp_mismatch c
    357         | _ ⇒ None ? ]
    358       | Vnull r1
     356        | Vnull ⇒ sem_cmp_mismatch c
     357        | _ ⇒ None ? ]
     358      | Vnull
    359359        match v2 with
    360360        [ Vptr ptr2 ⇒ sem_cmp_mismatch c
    361         | Vnull r2 ⇒ sem_cmp_match c
     361        | Vnull ⇒ sem_cmp_match c
    362362        | _ ⇒ None ?
    363363        ]
     
    430430  ].
    431431
     432(* Only for full 8051 memory spaces
    432433inductive type_region : type → region → Prop ≝
    433434| type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s
    434435| type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s
    435 (* XXX Is the following necessary? *)
     436(* Is the following necessary? *)
    436437| type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code.
     438*)
     439
     440inductive type_ptr : type → Prop ≝
     441| type_pointer : ∀t. type_ptr (Tpointer t)
     442| type_array : ∀t,n. type_ptr (Tarray t n)
     443| type_fun : ∀tys,ty. type_ptr (Tfunction tys ty).
    437444
    438445inductive cast : mem → val → type → type → val → Prop ≝
     
    449456      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    450457           (Vfloat (cast_float_float sz2 f))
    451   | cast_pp: ∀m,ty,ty',ptr,r'.
    452       type_region ty (ptype ptr) →
     458  | cast_pp: ∀m,ty,ty',ptr.
     459(*      type_region ty (ptype ptr) →
    453460      type_region ty' r' →
    454461      ∀pc':pointer_compat (pblock ptr) r'.
    455       cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))
    456   | cast_ip_z: ∀m,sz,sg,ty',r.
    457       type_region ty' r →
    458       cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r)
    459   | cast_pp_z: ∀m,ty,ty',r,r'.
    460       type_region ty r →
    461       type_region ty' r' →
    462       cast m (Vnull r) ty ty' (Vnull r').
     462      cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))*)
     463      type_ptr ty →
     464      type_ptr ty' →
     465      cast m (Vptr ptr) ty ty' (Vptr ptr)
     466  | cast_ip_z: ∀m,sz,sg,ty'.
     467(*     type_region ty' r →*)
     468      type_ptr ty' →
     469      cast m (Vint sz (zero ?)) (Tint sz sg) ty' Vnull
     470  | cast_pp_z: ∀m,ty,ty'.
     471(*      type_region ty r →
     472      type_region ty' r' →*)
     473      type_ptr ty →
     474      type_ptr ty' →
     475      cast m Vnull ty ty' Vnull.
    463476
    464477(* * * Operational semantics *)
     
    486499let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝
    487500  match access_mode ty with
    488   [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer Any b ? ofs))
    489   | By_reference r ⇒
    490     match pointer_compat_dec b r with
     501  [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer b ofs))
     502  | By_reference  ⇒ Some ? (Vptr (mk_pointer b ofs))
     503(*    match pointer_compat_dec b r with
    491504    [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs))
    492505    | inr _ ⇒ None ?
    493     ]
     506    ]*)
    494507  | By_nothing _ ⇒ None ?
    495508  ].
    496 cases b //
    497 qed.
     509(*cases b //
     510qed.*)
    498511
    499512(* * Symmetrically, [store_value_of_type ty m b ofs v] returns the
     
    504517let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝
    505518  match access_mode ty_dest with
    506   [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v
    507   | By_reference _ ⇒ None ?
     519  [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer loc ofs)) v
     520  | By_reference ⇒ None ?
    508521  | By_nothing _ ⇒ None ?
    509522  ].
    510 cases loc //
    511 qed.
     523(*cases loc //
     524qed.*)
    512525
    513526(* * Allocation of function-local variables.
     
    526539  | alloc_variables_cons:
    527540      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    528       alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
     541      alloc m 0 (sizeof ty) XData = 〈m1, b1〉 →
    529542      alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
    530543      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
     
    598611      load_value_of_type ty m loc ofs = Some ? v →
    599612      eval_expr ge e m (Expr a ty) v tr
    600   | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
     613  | eval_Eaddrof: ∀a,ty,loc,ofs,tr.
    601614      eval_lvalue ge e m a loc ofs tr →
    602       ∀pc:pointer_compat loc r.
    603       eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr (mk_pointer r loc pc ofs)) tr
     615(*      ∀pc:pointer_compat loc r.*)
     616      eval_expr ge e m (Expr (Eaddrof a) (Tpointer ty)) (Vptr (mk_pointer loc ofs)) tr
    604617  | eval_Esizeof: ∀ty',sz,sg.
    605618      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
     
    664677      find_symbol … ge id = Some ? l →
    665678      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
    666   | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
    667       eval_expr ge e m a (Vptr (mk_pointer r l p ofs)) tr →
     679  | eval_Ederef: ∀a,ty,l,ofs,tr.
     680      eval_expr ge e m a (Vptr (mk_pointer  l ofs)) tr →
    668681      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
    669682    (* Aside: note that each block of memory is entirely contained within one
     
    685698  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    686699  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    687   (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
     700  (ead:∀a,ty,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
    688701  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    689702  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    702715  | eval_Econst_float f ty ⇒ ecF f ty
    703716  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    704   | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
     717  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H
    705718  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    706719  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
     
    722735  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
    723736  (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2))
    724   (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
     737  (lde:∀a,ty,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty l ofs tr H))
    725738  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
    726739  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     
    729742  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    730743  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    731   | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H
     744  | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H
    732745  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
    733746  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
     
    793806  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    794807  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    795   (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
     808  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
    796809  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    797810  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    807820  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    808821  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    809   (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
     822  (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H))
    810823  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
    811824  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     
    816829  | eval_Econst_float f ty ⇒ ecF f ty
    817830  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
    818   | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
     831  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
    819832  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    820833  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
     
    835848  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    836849  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    837   (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
     850  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
    838851  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    839852  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    849862  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    850863  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    851   (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
     864  (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H))
    852865  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
    853866  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     
    856869  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    857870  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    858   | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer r l pc ofs)) tr H)
     871  | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer l ofs)) tr H)
    859872  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
    860873  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
     
    10141027| Tint a b ⇒ Tint a b
    10151028| Tfloat a ⇒ Tfloat a
    1016 | Tpointer _ ty ⇒ ty
    1017 | Tarray a b c ⇒ Tarray a b c
     1029| Tpointer ty ⇒ ty
     1030| Tarray a b ⇒ Tarray a b
    10181031| Tfunction a b ⇒ Tfunction a b
    10191032| Tstruct a b ⇒ Tstruct a b
    10201033| Tunion a b ⇒ Tunion a b
    1021 | Tcomp_ptr a b ⇒ Tcomp_ptr a b
     1034| Tcomp_ptr a ⇒ Tcomp_ptr a
    10221035].
    10231036
  • src/Clight/Csyntax.ma

    r1920 r2176  
    6565  | Tint: intsize → signedness → type   (**r integer types *)
    6666  | Tfloat: floatsize → type            (**r floating-point types *)
    67   | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
    68   | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *)
     67  | Tpointer: (*region →*) type → type      (**r pointer types ([*ty]) *)
     68  | Tarray: (*region →*) type → nat → type  (**r array types ([ty[len]]) *)
    6969  | Tfunction: typelist → type → type   (**r function types *)
    7070  | Tstruct: ident → fieldlist → type   (**r struct types *)
    7171  | Tunion: ident → fieldlist → type    (**r union types *)
    72   | Tcomp_ptr: region → ident → type    (**r pointer to named struct or union *)
     72  | Tcomp_ptr: (*region →*) ident → type    (**r pointer to named struct or union *)
    7373
    7474with typelist : Type[0] ≝
     
    8686  (it:∀i,s. P (Tint i s))
    8787  (fl:∀f. P (Tfloat f))
    88   (pt:∀s,t. P t → P (Tpointer s t))
    89   (ar:∀s,t,n. P t → P (Tarray s t n))
     88  (pt:∀t. P t → P (Tpointer t))
     89  (ar:∀t,n. P t → P (Tarray t n))
    9090  (fn:∀tl,t. P t → P (Tfunction tl t))
    9191  (st:∀i,fl. P (Tstruct i fl))
    9292  (un:∀i,fl. P (Tunion i fl))
    93   (cp:∀rg,i. P (Tcomp_ptr rg i))
     93  (cp:∀i. P (Tcomp_ptr i))
    9494  (t:type) on t : P t ≝
    9595  match t return λt'.P t' with
     
    9797  | Tint i s ⇒ it i s
    9898  | Tfloat s ⇒ fl s
    99   | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t')
    100   | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t')
     99  | Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t')
     100  | Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t')
    101101  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
    102102  | Tstruct i fs ⇒ st i fs
    103103  | Tunion i fs ⇒ un i fs
    104   | Tcomp_ptr rg i ⇒ cp rg i
     104  | Tcomp_ptr i ⇒ cp i
    105105  ].
    106106 
     
    350350
    351351(* * Natural alignment of a type, in bytes. *)
    352 (* FIXME: these are old values for 32 bit machines *)
    353 let rec alignof (t: type) : nat ≝
     352let rec alignof (t: type) : nat ≝ (*1*)
     353(* these are old values for 32 bit machines *)
    354354  match t with
    355355  [ Tvoid ⇒ 1
    356356  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    357357  | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    358   | Tpointer _ _ ⇒ 4
    359   | Tarray _ t' n ⇒ alignof t'
     358  | Tpointer _ ⇒ 4
     359  | Tarray t' n ⇒ alignof t'
    360360  | Tfunction _ _ ⇒ 1
    361361  | Tstruct _ fld ⇒ alignof_fields fld
    362362  | Tunion _ fld ⇒ alignof_fields fld
    363   | Tcomp_ptr _ _ ⇒ 4
     363  | Tcomp_ptr _ ⇒ 4
    364364  ]
    365365
     
    381381  (it:∀i,s. P (Tint i s))
    382382  (fl:∀f. P (Tfloat f))
    383   (pt:∀s,t. P t → P (Tpointer s t))
    384   (ar:∀s,t,n. P t → P (Tarray s t n))
     383  (pt:∀t. P t → P (Tpointer t))
     384  (ar:∀t,n. P t → P (Tarray t n))
    385385  (fn:∀tl,t. P t → P (Tfunction tl t))
    386386  (st:∀i,fl. Q fl → P (Tstruct i fl))
    387387  (un:∀i,fl. Q fl → P (Tunion i fl))
    388   (cp:∀r,i. P (Tcomp_ptr r i))
     388  (cp:∀i. P (Tcomp_ptr i))
    389389  (nl:Q Fnil)
    390390  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
     
    394394  | Tint i s ⇒ it i s
    395395  | Tfloat s ⇒ fl s
    396   | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    397   | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     396  | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     397  | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    398398  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    399399  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    400400  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    401   | Tcomp_ptr r i ⇒ cp r i
     401  | Tcomp_ptr i ⇒ cp i
    402402  ]
    403403and fieldlist_ind2
     
    406406  (it:∀i,s. P (Tint i s))
    407407  (fl:∀f. P (Tfloat f))
    408   (pt:∀s,t. P t → P (Tpointer s t))
    409   (ar:∀s,t,n. P t → P (Tarray s t n))
     408  (pt:∀t. P t → P (Tpointer t))
     409  (ar:∀t,n. P t → P (Tarray t n))
    410410  (fn:∀tl,t. P t → P (Tfunction tl t))
    411411  (st:∀i,fl. Q fl → P (Tstruct i fl))
    412412  (un:∀i,fl. Q fl → P (Tunion i fl))
    413   (cp:∀r,i. P (Tcomp_ptr r i))
     413  (cp:∀i. P (Tcomp_ptr i))
    414414  (nl:Q Fnil)
    415415  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
     
    440440  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    441441  | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    442   | Tpointer r _ ⇒ size_pointer r
    443   | Tarray _ t' n ⇒ sizeof t' * max 1 n
     442  | Tpointer _ ⇒ size_pointer
     443  | Tarray t' n ⇒ sizeof t' * max 1 n
    444444  | Tfunction _ _ ⇒ 1
    445445  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
    446446  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
    447   | Tcomp_ptr r _ ⇒ size_pointer r
     447  | Tcomp_ptr _ ⇒ size_pointer
    448448  ]
    449449
     
    611611  | Tint sz sg ⇒ ASTint sz sg
    612612  | Tfloat sz ⇒ ASTfloat sz
    613   | Tpointer r _ ⇒ ASTptr r
    614   | Tarray r _ _ ⇒ ASTptr r
    615   | Tfunction _ _ ⇒ ASTptr Code
    616   | Tcomp_ptr r _ ⇒ ASTptr r
     613  | Tpointer _ ⇒ ASTptr
     614  | Tarray _ _ ⇒ ASTptr
     615  | Tfunction _ _ ⇒ ASTptr
     616  | Tcomp_ptr _ ⇒ ASTptr
    617617  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
    618618  ].
     
    623623  | Tint sz sg ⇒ Some ? (ASTint sz sg)
    624624  | Tfloat sz ⇒ Some ? (ASTfloat sz)
    625   | Tpointer r _ ⇒ Some ? (ASTptr r)
    626   | Tarray r _ _ ⇒ Some ? (ASTptr r)
    627   | Tfunction _ _ ⇒ Some ? (ASTptr Code)
    628   | Tcomp_ptr r _ ⇒ Some ? (ASTptr r)
     625  | Tpointer _ ⇒ Some ? ASTptr
     626  | Tarray _ _ ⇒ Some ? ASTptr
     627  | Tfunction _ _ ⇒ Some ? ASTptr
     628  | Tcomp_ptr _ ⇒ Some ? ASTptr
    629629  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
    630630  ].
     
    651651inductive mode: typ → Type[0] ≝
    652652  | By_value: ∀t:typ. mode t
    653   | By_reference: ∀r:region. mode (ASTptr r)
     653  | By_reference: (*∀r:region.*) mode ASTptr
    654654  | By_nothing: ∀t. mode t.
    655655
     
    659659  | Tfloat sz ⇒ By_value (ASTfloat sz)
    660660  | Tvoid ⇒ By_nothing …
    661   | Tpointer r _ ⇒ By_value (ASTptr r)
    662   | Tarray r _ _ ⇒ By_reference r
    663   | Tfunction _ _ ⇒ By_reference Code
     661  | Tpointer _ ⇒ By_value ASTptr
     662  | Tarray _ _ ⇒ By_reference
     663  | Tfunction _ _ ⇒ By_reference
    664664  | Tstruct _ fList ⇒ By_nothing …
    665665  | Tunion _ fList ⇒ By_nothing …
    666   | Tcomp_ptr r _ ⇒ By_value (ASTptr r)
     666  | Tcomp_ptr _ ⇒ By_value ASTptr
    667667  ].
    668668
  • src/Clight/SimplifyCasts.ma

    r2103 r2176  
    719719#castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result
    720720elim castee_val
    721 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     721[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    722722[ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ]
    723723whd in ⊢ ((??%?) → ?);
     
    750750#sz #sg #v1 #v2 #m #r
    751751elim v1
    752 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     752[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    753753whd in ⊢ ((??%?) → ?); normalize nodelta
    754754>classify_add_int normalize nodelta #H destruct
    755755elim v2 in H;
    756 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     756[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    757757whd in ⊢ ((??%?) → ?); #H destruct
    758758elim (sz_eq_dec sz' sz'')
     
    766766#sz #sg #v1 #v2 #m #r
    767767elim v1
    768 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     768[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    769769whd in ⊢ ((??%?) → ?); normalize nodelta
    770770>classify_sub_int normalize nodelta #H destruct
    771771elim v2 in H;
    772 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     772[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    773773whd in ⊢ ((??%?) → ?); #H destruct
    774774elim (sz_eq_dec sz' sz'')
     
    789789#sz #sg #v1 #v2 #m
    790790elim v1
    791 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     791[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    792792[ 2: | *: #_ %1 %1 % #H @H ]
    793793elim v2
    794 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     794[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    795795[ 2: | *: #_ %1 %2 % #H @H ]
    796796whd in ⊢ ((??%?) → ?); normalize nodelta
     
    808808#sz #sg #v1 #v2 #m
    809809elim v1
    810 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     810[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    811811[ 2: | *: #_ %1 %1 % #H @H ]
    812812elim v2
    813 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     813[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    814814[ 2: | *: #_ %1 %2 % #H @H ]
    815815whd in ⊢ ((??%?) → ?); normalize nodelta
     
    827827elim op normalize in match (binop_simplifiable ?); #H destruct
    828828elim v1 in H;
    829 [ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: #r | 5,10: #ptr ]
     829[ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: | 5,10: #ptr ]
    830830#_
    831831whd in match (sem_binary_operation ??????); normalize nodelta
     
    11861186      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    11871187        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
    1188         cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
    1189                                  (pointer_compat_dec block r = inl ?? pc) ∧
    1190                                  (ty = Tpointer r ptype) ∧
    1191                                   val = Vptr (mk_pointer r block pc offset))
     1188        cut (∃block,offset,ptype. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
     1189                                 (ty = Tpointer ptype) ∧
     1190                                  val = Vptr (mk_pointer block offset))
    11921191        [ 1: lapply Hstep -Hstep
    11931192             cases (exec_lvalue ge en m e1)
    11941193             [ 1: * * #block #offset #trace' normalize nodelta
    11951194                  cases ty
    1196                   [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
    1197                   | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
     1195                  [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1196                  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
    11981197                  normalize nodelta try (#Heq destruct)
    1199                   @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty)
    1200                   cases (pointer_compat_dec block rg) in Heq; normalize
    1201                   [ 2: #Hnotcompat #Hcontr destruct
    1202                   | 1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ]
     1198                  @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty)
     1199                  try @conj try @conj destruct //
    12031200             | 2: normalize nodelta #errmesg #Hcontr destruct
    12041201             ]
    1205         | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq
     1202        | 2: * #block * #offset * #ptype * * #Hexec_lvalue #Hty_eq #Hval_eq
    12061203             whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
    1207              >Hptr_compat //
     1204             //
    12081205        ]
    12091206     ]
     
    16441641           >Htype_eq
    16451642           cases (typeof rec_expr1) normalize nodelta
    1646            [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
     1643           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    16471644           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
    16481645           | 6,7: cases Hsim_lvalue
     
    16591656           >Htype_eq
    16601657           cases (typeof rec_expr1) normalize nodelta
    1661            [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
     1658           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    16621659           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
    16631660           | 6,7: cases Hsim_lvalue
     
    19311928   whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); 
    19321929   [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta
    1933        [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
    1934        | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     1930       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
     1931       | 7: #id #fl | 8: #id #fl | 9: #id ]
    19351932       try (@SimFail /2 by ex_intro/)
    19361933       cases Hsim_lvalue
     
    19431940   | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *)
    19441941       >Htype_eq cases (typeof rec_expr1) normalize nodelta
    1945        [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
    1946        | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     1942       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
     1943       | 7: #id #fl | 8: #id #fl | 9: #id ]
    19471944       try (@SimFail /2 by ex_intro/)
    19481945       cases Hsim_lvalue
     
    22042201      normalize in match (typeof (Expr ??));
    22052202      cases ty' in Hsim_lvalue; normalize nodelta
    2206       [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
    2207       | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
     2203      [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     2204      | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
    22082205      #Hsim_lvalue
    22092206      try (@SimFail /2 by ex_intro/)
     
    26092606                    | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
    26102607                    | 4: #r #Habsurd destruct (Habsurd) ]                   
    2611                | 3: #irrelevant #Habsurd destruct
    2612                | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct
     2608               | 3,4,9: #irrelevant #Habsurd destruct
    26132609               | *: #irrelevant1 #irrelevant2 #Habsurd destruct ]
    26142610          | 2: (* Kseq stm' k' *)
     
    26752671                                  (free_list m (blocks_of_env en)))} @conj
    26762672                    [ 1: // | 2: %3 @cc_call // ]                                 
    2677                | 3: #irrelevant #Habsurd destruct (Habsurd)
    2678                | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct (Habsurd)
     2673               | 3,4,9: #irrelevant #Habsurd destruct (Habsurd)
    26792674               | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ]
    26802675           ]
     
    29042899          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
    29052900               whd in match (ret ??) in ⊢ (% → %);
    2906                [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
    2907                | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     2901               [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
     2902               | 7: #id #fl | 8: #id #fl | 9: #id ]
    29082903               #H destruct (H)
    29092904               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
  • src/Clight/TypeComparison.ma

    r1872 r2176  
    2525    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    2626    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     27| Tpointer t ⇒ match t2 return λt'. Sum (Tpointer ? = t') (Tpointer ? ≠ t')  with [ Tpointer t' ⇒
     28      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
     29      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
     30    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     31| Tarray t n ⇒ match t2 return λt'. Sum (Tarray ?? = t') (Tarray ?? ≠ t')  with [ Tarray t' n' ⇒
     32      match type_eq_dec t t' with [ inl e2 ⇒
     33        match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
     34        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     35        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     36        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     37(*
    2738| Tpointer s t ⇒ match t2 return λt'. Sum (Tpointer ?? = t') (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
    2839    match eq_region_dec s s' with [ inl e1 ⇒
     
    3849        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    3950        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     51*)
    4052| Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
    4153    match typelist_eq_dec tl tl' with [ inl e1 ⇒
     
    5870    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    5971    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
     72| Tcomp_ptr i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? = t') (Tcomp_ptr ? ≠ t')  with [ Tcomp_ptr i' ⇒
     73      match ident_eq i i' with [ inl e2 ⇒ inl ???
     74      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
     75    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     76(*
    6077| Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
    6178    match eq_region_dec r r' with [ inl e1 ⇒
     
    6481    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    6582    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     83*)
    6684]
    6785and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝
  • src/Clight/clightPrintMatita.ml

    r1633 r2176  
    151151  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
    152152  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
    153   | Tpointer t -> "(Tpointer Any " ^ stype t ^ ")"
    154   | Tarray(t, n) -> "(Tarray Any " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
     153  | Tpointer t -> "(Tpointer " ^ stype t ^ ")"
     154  | Tarray(t, n) -> "(Tarray " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
    155155  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
    156156  | Tstruct(name, fld) ->
     
    159159      fieldlist "(Tunion (ident_of_nat " name fld
    160160  | Tcomp_ptr (name) ->
    161       "(Tcomp_ptr Any (ident_of_nat " ^ id_s name ^ "))"
     161      "(Tcomp_ptr (ident_of_nat " ^ id_s name ^ "))"
    162162 and typelist l =
    163163    let b = Buffer.create 20 in
     
    357357  | Init_int8 n -> fprintf p "(Init_int8 (repr I8 %d))@ " n
    358358  | Init_int16 n -> fprintf p "(Init_int16 (repr I16 %d))@ " n
    359   (*| Init_null r -> fprintf p "(Init_null Any)@"*)
     359  (*| Init_null r -> fprintf p "(Init_null)@"*)
    360360  | Init_int32 n -> fprintf p "(Init_int32 (repr I32 %d))@ " n
    361361  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
    362362  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
    363363  | Init_space n -> fprintf p "(Init_space %d)@ " n
    364   | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof Any (ident_of_nat %i) %d)" (id_i symb) ofs
     364  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof (ident_of_nat %i) %d)" (id_i symb) ofs
    365365
    366366let re_string_literal = Str.regexp "__stringlit_[0-9]+"
    367367
    368368let print_globvar p (((id, init), ty)) =
    369   fprintf p "@[<hov 2>〈〈ident_of_nat %i (* %s *),@ Any〉,@ 〈%a,@ %s〉〉@]"
     369  fprintf p "@[<hov 2>〈〈ident_of_nat %i (* %s *),@ XData〉,@ 〈%a,@ %s〉〉@]"
    370370    (id_i id)
    371371    id
  • src/Clight/labelSimulation.ma

    r2145 r2176  
    103103  whd in ⊢ (?(??%?)?);
    104104  cases ty' in EX1rem ⊢ %;
    105   [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
    106        #pc normalize #E destruct /2/
     105  [ 4: #ty' normalize #E destruct /2/
    107106  | *: normalize #A try #B try #C try #D destruct
    108107  ]
     
    672671        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
    673672        | // ] | /3/ ]
    674       | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
     673      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    675674      ]
    676675    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
     
    720719        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
    721720        @refl | // ] | /4/ ] | skip ]
    722       | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
     721      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    723722      ]
    724723    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
  • src/Clight/test/duff.c.ma

    r1513 r2176  
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    55  [][〈ident_of_nat 0 (* copy *), CL_Internal (
    6        mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
     6       mk_function Tvoid [〈ident_of_nat 19, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer (Tint I16 Signed  ))〉 ]
    77         (Ssequence
    88         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     
    2323             (Ssequence
    2424             (Sassign (Expr (Evar (ident_of_nat 17))
    25                         (Tpointer Any (Tint I16 Signed  )))
    26                (Expr (Evar (ident_of_nat 19))
    27                  (Tpointer Any (Tint I16 Signed  ))))
     25                        (Tpointer (Tint I16 Signed  )))
     26               (Expr (Evar (ident_of_nat 19)) (Tpointer (Tint I16 Signed  ))))
    2827             (Sassign (Expr (Evar (ident_of_nat 19))
    29                         (Tpointer Any (Tint I16 Signed  )))
     28                        (Tpointer (Tint I16 Signed  )))
    3029               (Expr (Ebinop Oadd
    3130                 (Expr (Evar (ident_of_nat 17))
    32                    (Tpointer Any (Tint I16 Signed  )))
     31                   (Tpointer (Tint I16 Signed  )))
    3332                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    34                  (Tpointer Any (Tint I16 Signed  )))))
     33                 (Tpointer (Tint I16 Signed  )))))
    3534             (Ssequence
    3635             (Ssequence
    3736             (Sassign (Expr (Evar (ident_of_nat 18))
    38                         (Tpointer Any (Tint I16 Signed  )))
    39                (Expr (Evar (ident_of_nat 20))
    40                  (Tpointer Any (Tint I16 Signed  ))))
     37                        (Tpointer (Tint I16 Signed  )))
     38               (Expr (Evar (ident_of_nat 20)) (Tpointer (Tint I16 Signed  ))))
    4139             (Sassign (Expr (Evar (ident_of_nat 20))
    42                         (Tpointer Any (Tint I16 Signed  )))
     40                        (Tpointer (Tint I16 Signed  )))
    4341               (Expr (Ebinop Oadd
    4442                 (Expr (Evar (ident_of_nat 18))
    45                    (Tpointer Any (Tint I16 Signed  )))
     43                   (Tpointer (Tint I16 Signed  )))
    4644                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    47                  (Tpointer Any (Tint I16 Signed  )))))
     45                 (Tpointer (Tint I16 Signed  )))))
    4846             (Sassign (Expr (Ederef
    4947                        (Expr (Evar (ident_of_nat 17))
    50                           (Tpointer Any (Tint I16 Signed  ))))
     48                          (Tpointer (Tint I16 Signed  ))))
    5149                        (Tint I16 Signed  ))
    5250               (Expr (Ederef
    5351                 (Expr (Evar (ident_of_nat 18))
    54                    (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
     52                   (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
    5553             (LScase I32 (repr ? 7)
    5654               (Ssequence
    5755               (Sassign (Expr (Evar (ident_of_nat 15))
    58                           (Tpointer Any (Tint I16 Signed  )))
     56                          (Tpointer (Tint I16 Signed  )))
    5957                 (Expr (Evar (ident_of_nat 19))
    60                    (Tpointer Any (Tint I16 Signed  ))))
     58                   (Tpointer (Tint I16 Signed  ))))
    6159               (Ssequence
    6260               (Sassign (Expr (Evar (ident_of_nat 19))
    63                           (Tpointer Any (Tint I16 Signed  )))
     61                          (Tpointer (Tint I16 Signed  )))
    6462                 (Expr (Ebinop Oadd
    6563                   (Expr (Evar (ident_of_nat 15))
    66                      (Tpointer Any (Tint I16 Signed  )))
     64                     (Tpointer (Tint I16 Signed  )))
    6765                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    68                    (Tpointer Any (Tint I16 Signed  ))))
     66                   (Tpointer (Tint I16 Signed  ))))
    6967               (Ssequence
    7068               (Sassign (Expr (Evar (ident_of_nat 16))
    71                           (Tpointer Any (Tint I16 Signed  )))
     69                          (Tpointer (Tint I16 Signed  )))
    7270                 (Expr (Evar (ident_of_nat 20))
    73                    (Tpointer Any (Tint I16 Signed  ))))
     71                   (Tpointer (Tint I16 Signed  ))))
    7472               (Ssequence
    7573               (Sassign (Expr (Evar (ident_of_nat 20))
    76                           (Tpointer Any (Tint I16 Signed  )))
     74                          (Tpointer (Tint I16 Signed  )))
    7775                 (Expr (Ebinop Oadd
    7876                   (Expr (Evar (ident_of_nat 16))
    79                      (Tpointer Any (Tint I16 Signed  )))
     77                     (Tpointer (Tint I16 Signed  )))
    8078                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    81                    (Tpointer Any (Tint I16 Signed  ))))
     79                   (Tpointer (Tint I16 Signed  ))))
    8280               (Sassign (Expr (Ederef
    8381                          (Expr (Evar (ident_of_nat 15))
    84                             (Tpointer Any (Tint I16 Signed  ))))
     82                            (Tpointer (Tint I16 Signed  ))))
    8583                          (Tint I16 Signed  ))
    8684                 (Expr (Ederef
    8785                   (Expr (Evar (ident_of_nat 16))
    88                      (Tpointer Any (Tint I16 Signed  ))))
    89                    (Tint I16 Signed  )))))))
     86                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    9087               (LScase I32 (repr ? 6)
    9188                 (Ssequence
    9289                 (Sassign (Expr (Evar (ident_of_nat 13))
    93                             (Tpointer Any (Tint I16 Signed  )))
     90                            (Tpointer (Tint I16 Signed  )))
    9491                   (Expr (Evar (ident_of_nat 19))
    95                      (Tpointer Any (Tint I16 Signed  ))))
     92                     (Tpointer (Tint I16 Signed  ))))
    9693                 (Ssequence
    9794                 (Sassign (Expr (Evar (ident_of_nat 19))
    98                             (Tpointer Any (Tint I16 Signed  )))
     95                            (Tpointer (Tint I16 Signed  )))
    9996                   (Expr (Ebinop Oadd
    10097                     (Expr (Evar (ident_of_nat 13))
    101                        (Tpointer Any (Tint I16 Signed  )))
     98                       (Tpointer (Tint I16 Signed  )))
    10299                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    103                      (Tpointer Any (Tint I16 Signed  ))))
     100                     (Tpointer (Tint I16 Signed  ))))
    104101                 (Ssequence
    105102                 (Sassign (Expr (Evar (ident_of_nat 14))
    106                             (Tpointer Any (Tint I16 Signed  )))
     103                            (Tpointer (Tint I16 Signed  )))
    107104                   (Expr (Evar (ident_of_nat 20))
    108                      (Tpointer Any (Tint I16 Signed  ))))
     105                     (Tpointer (Tint I16 Signed  ))))
    109106                 (Ssequence
    110107                 (Sassign (Expr (Evar (ident_of_nat 20))
    111                             (Tpointer Any (Tint I16 Signed  )))
     108                            (Tpointer (Tint I16 Signed  )))
    112109                   (Expr (Ebinop Oadd
    113110                     (Expr (Evar (ident_of_nat 14))
    114                        (Tpointer Any (Tint I16 Signed  )))
     111                       (Tpointer (Tint I16 Signed  )))
    115112                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    116                      (Tpointer Any (Tint I16 Signed  ))))
     113                     (Tpointer (Tint I16 Signed  ))))
    117114                 (Sassign (Expr (Ederef
    118115                            (Expr (Evar (ident_of_nat 13))
    119                               (Tpointer Any (Tint I16 Signed  ))))
     116                              (Tpointer (Tint I16 Signed  ))))
    120117                            (Tint I16 Signed  ))
    121118                   (Expr (Ederef
    122119                     (Expr (Evar (ident_of_nat 14))
    123                        (Tpointer Any (Tint I16 Signed  ))))
    124                      (Tint I16 Signed  )))))))
     120                       (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    125121                 (LScase I32 (repr ? 5)
    126122                   (Ssequence
    127123                   (Sassign (Expr (Evar (ident_of_nat 11))
    128                               (Tpointer Any (Tint I16 Signed  )))
     124                              (Tpointer (Tint I16 Signed  )))
    129125                     (Expr (Evar (ident_of_nat 19))
    130                        (Tpointer Any (Tint I16 Signed  ))))
     126                       (Tpointer (Tint I16 Signed  ))))
    131127                   (Ssequence
    132128                   (Sassign (Expr (Evar (ident_of_nat 19))
    133                               (Tpointer Any (Tint I16 Signed  )))
     129                              (Tpointer (Tint I16 Signed  )))
    134130                     (Expr (Ebinop Oadd
    135131                       (Expr (Evar (ident_of_nat 11))
    136                          (Tpointer Any (Tint I16 Signed  )))
     132                         (Tpointer (Tint I16 Signed  )))
    137133                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    138                        (Tpointer Any (Tint I16 Signed  ))))
     134                       (Tpointer (Tint I16 Signed  ))))
    139135                   (Ssequence
    140136                   (Sassign (Expr (Evar (ident_of_nat 12))
    141                               (Tpointer Any (Tint I16 Signed  )))
     137                              (Tpointer (Tint I16 Signed  )))
    142138                     (Expr (Evar (ident_of_nat 20))
    143                        (Tpointer Any (Tint I16 Signed  ))))
     139                       (Tpointer (Tint I16 Signed  ))))
    144140                   (Ssequence
    145141                   (Sassign (Expr (Evar (ident_of_nat 20))
    146                               (Tpointer Any (Tint I16 Signed  )))
     142                              (Tpointer (Tint I16 Signed  )))
    147143                     (Expr (Ebinop Oadd
    148144                       (Expr (Evar (ident_of_nat 12))
    149                          (Tpointer Any (Tint I16 Signed  )))
     145                         (Tpointer (Tint I16 Signed  )))
    150146                       (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    151                        (Tpointer Any (Tint I16 Signed  ))))
     147                       (Tpointer (Tint I16 Signed  ))))
    152148                   (Sassign (Expr (Ederef
    153149                              (Expr (Evar (ident_of_nat 11))
    154                                 (Tpointer Any (Tint I16 Signed  ))))
     150                                (Tpointer (Tint I16 Signed  ))))
    155151                              (Tint I16 Signed  ))
    156152                     (Expr (Ederef
    157153                       (Expr (Evar (ident_of_nat 12))
    158                          (Tpointer Any (Tint I16 Signed  ))))
     154                         (Tpointer (Tint I16 Signed  ))))
    159155                       (Tint I16 Signed  )))))))
    160156                   (LScase I32 (repr ? 4)
    161157                     (Ssequence
    162158                     (Sassign (Expr (Evar (ident_of_nat 9))
    163                                 (Tpointer Any (Tint I16 Signed  )))
     159                                (Tpointer (Tint I16 Signed  )))
    164160                       (Expr (Evar (ident_of_nat 19))
    165                          (Tpointer Any (Tint I16 Signed  ))))
     161                         (Tpointer (Tint I16 Signed  ))))
    166162                     (Ssequence
    167163                     (Sassign (Expr (Evar (ident_of_nat 19))
    168                                 (Tpointer Any (Tint I16 Signed  )))
     164                                (Tpointer (Tint I16 Signed  )))
    169165                       (Expr (Ebinop Oadd
    170166                         (Expr (Evar (ident_of_nat 9))
    171                            (Tpointer Any (Tint I16 Signed  )))
     167                           (Tpointer (Tint I16 Signed  )))
    172168                         (Expr (Econst_int I32 (repr ? 1))
    173169                           (Tint I32 Signed  )))
    174                          (Tpointer Any (Tint I16 Signed  ))))
     170                         (Tpointer (Tint I16 Signed  ))))
    175171                     (Ssequence
    176172                     (Sassign (Expr (Evar (ident_of_nat 10))
    177                                 (Tpointer Any (Tint I16 Signed  )))
     173                                (Tpointer (Tint I16 Signed  )))
    178174                       (Expr (Evar (ident_of_nat 20))
    179                          (Tpointer Any (Tint I16 Signed  ))))
     175                         (Tpointer (Tint I16 Signed  ))))
    180176                     (Ssequence
    181177                     (Sassign (Expr (Evar (ident_of_nat 20))
    182                                 (Tpointer Any (Tint I16 Signed  )))
     178                                (Tpointer (Tint I16 Signed  )))
    183179                       (Expr (Ebinop Oadd
    184180                         (Expr (Evar (ident_of_nat 10))
    185                            (Tpointer Any (Tint I16 Signed  )))
     181                           (Tpointer (Tint I16 Signed  )))
    186182                         (Expr (Econst_int I32 (repr ? 1))
    187183                           (Tint I32 Signed  )))
    188                          (Tpointer Any (Tint I16 Signed  ))))
     184                         (Tpointer (Tint I16 Signed  ))))
    189185                     (Sassign (Expr (Ederef
    190186                                (Expr (Evar (ident_of_nat 9))
    191                                   (Tpointer Any (Tint I16 Signed  ))))
     187                                  (Tpointer (Tint I16 Signed  ))))
    192188                                (Tint I16 Signed  ))
    193189                       (Expr (Ederef
    194190                         (Expr (Evar (ident_of_nat 10))
    195                            (Tpointer Any (Tint I16 Signed  ))))
     191                           (Tpointer (Tint I16 Signed  ))))
    196192                         (Tint I16 Signed  )))))))
    197193                     (LScase I32 (repr ? 3)
    198194                       (Ssequence
    199195                       (Sassign (Expr (Evar (ident_of_nat 7))
    200                                   (Tpointer Any (Tint I16 Signed  )))
     196                                  (Tpointer (Tint I16 Signed  )))
    201197                         (Expr (Evar (ident_of_nat 19))
    202                            (Tpointer Any (Tint I16 Signed  ))))
     198                           (Tpointer (Tint I16 Signed  ))))
    203199                       (Ssequence
    204200                       (Sassign (Expr (Evar (ident_of_nat 19))
    205                                   (Tpointer Any (Tint I16 Signed  )))
     201                                  (Tpointer (Tint I16 Signed  )))
    206202                         (Expr (Ebinop Oadd
    207203                           (Expr (Evar (ident_of_nat 7))
    208                              (Tpointer Any (Tint I16 Signed  )))
     204                             (Tpointer (Tint I16 Signed  )))
    209205                           (Expr (Econst_int I32 (repr ? 1))
    210206                             (Tint I32 Signed  )))
    211                            (Tpointer Any (Tint I16 Signed  ))))
     207                           (Tpointer (Tint I16 Signed  ))))
    212208                       (Ssequence
    213209                       (Sassign (Expr (Evar (ident_of_nat 8))
    214                                   (Tpointer Any (Tint I16 Signed  )))
     210                                  (Tpointer (Tint I16 Signed  )))
    215211                         (Expr (Evar (ident_of_nat 20))
    216                            (Tpointer Any (Tint I16 Signed  ))))
     212                           (Tpointer (Tint I16 Signed  ))))
    217213                       (Ssequence
    218214                       (Sassign (Expr (Evar (ident_of_nat 20))
    219                                   (Tpointer Any (Tint I16 Signed  )))
     215                                  (Tpointer (Tint I16 Signed  )))
    220216                         (Expr (Ebinop Oadd
    221217                           (Expr (Evar (ident_of_nat 8))
    222                              (Tpointer Any (Tint I16 Signed  )))
     218                             (Tpointer (Tint I16 Signed  )))
    223219                           (Expr (Econst_int I32 (repr ? 1))
    224220                             (Tint I32 Signed  )))
    225                            (Tpointer Any (Tint I16 Signed  ))))
     221                           (Tpointer (Tint I16 Signed  ))))
    226222                       (Sassign (Expr (Ederef
    227223                                  (Expr (Evar (ident_of_nat 7))
    228                                     (Tpointer Any (Tint I16 Signed  ))))
     224                                    (Tpointer (Tint I16 Signed  ))))
    229225                                  (Tint I16 Signed  ))
    230226                         (Expr (Ederef
    231227                           (Expr (Evar (ident_of_nat 8))
    232                              (Tpointer Any (Tint I16 Signed  ))))
     228                             (Tpointer (Tint I16 Signed  ))))
    233229                           (Tint I16 Signed  )))))))
    234230                       (LScase I32 (repr ? 2)
    235231                         (Ssequence
    236232                         (Sassign (Expr (Evar (ident_of_nat 5))
    237                                     (Tpointer Any (Tint I16 Signed  )))
     233                                    (Tpointer (Tint I16 Signed  )))
    238234                           (Expr (Evar (ident_of_nat 19))
    239                              (Tpointer Any (Tint I16 Signed  ))))
     235                             (Tpointer (Tint I16 Signed  ))))
    240236                         (Ssequence
    241237                         (Sassign (Expr (Evar (ident_of_nat 19))
    242                                     (Tpointer Any (Tint I16 Signed  )))
     238                                    (Tpointer (Tint I16 Signed  )))
    243239                           (Expr (Ebinop Oadd
    244240                             (Expr (Evar (ident_of_nat 5))
    245                                (Tpointer Any (Tint I16 Signed  )))
     241                               (Tpointer (Tint I16 Signed  )))
    246242                             (Expr (Econst_int I32 (repr ? 1))
    247243                               (Tint I32 Signed  )))
    248                              (Tpointer Any (Tint I16 Signed  ))))
     244                             (Tpointer (Tint I16 Signed  ))))
    249245                         (Ssequence
    250246                         (Sassign (Expr (Evar (ident_of_nat 6))
    251                                     (Tpointer Any (Tint I16 Signed  )))
     247                                    (Tpointer (Tint I16 Signed  )))
    252248                           (Expr (Evar (ident_of_nat 20))
    253                              (Tpointer Any (Tint I16 Signed  ))))
     249                             (Tpointer (Tint I16 Signed  ))))
    254250                         (Ssequence
    255251                         (Sassign (Expr (Evar (ident_of_nat 20))
    256                                     (Tpointer Any (Tint I16 Signed  )))
     252                                    (Tpointer (Tint I16 Signed  )))
    257253                           (Expr (Ebinop Oadd
    258254                             (Expr (Evar (ident_of_nat 6))
    259                                (Tpointer Any (Tint I16 Signed  )))
     255                               (Tpointer (Tint I16 Signed  )))
    260256                             (Expr (Econst_int I32 (repr ? 1))
    261257                               (Tint I32 Signed  )))
    262                              (Tpointer Any (Tint I16 Signed  ))))
     258                             (Tpointer (Tint I16 Signed  ))))
    263259                         (Sassign (Expr (Ederef
    264260                                    (Expr (Evar (ident_of_nat 5))
    265                                       (Tpointer Any (Tint I16 Signed  ))))
     261                                      (Tpointer (Tint I16 Signed  ))))
    266262                                    (Tint I16 Signed  ))
    267263                           (Expr (Ederef
    268264                             (Expr (Evar (ident_of_nat 6))
    269                                (Tpointer Any (Tint I16 Signed  ))))
     265                               (Tpointer (Tint I16 Signed  ))))
    270266                             (Tint I16 Signed  )))))))
    271267                         (LScase I32 (repr ? 1)
    272268                           (Ssequence
    273269                           (Sassign (Expr (Evar (ident_of_nat 3))
    274                                       (Tpointer Any (Tint I16 Signed  )))
     270                                      (Tpointer (Tint I16 Signed  )))
    275271                             (Expr (Evar (ident_of_nat 19))
    276                                (Tpointer Any (Tint I16 Signed  ))))
     272                               (Tpointer (Tint I16 Signed  ))))
    277273                           (Ssequence
    278274                           (Sassign (Expr (Evar (ident_of_nat 19))
    279                                       (Tpointer Any (Tint I16 Signed  )))
     275                                      (Tpointer (Tint I16 Signed  )))
    280276                             (Expr (Ebinop Oadd
    281277                               (Expr (Evar (ident_of_nat 3))
    282                                  (Tpointer Any (Tint I16 Signed  )))
     278                                 (Tpointer (Tint I16 Signed  )))
    283279                               (Expr (Econst_int I32 (repr ? 1))
    284280                                 (Tint I32 Signed  )))
    285                                (Tpointer Any (Tint I16 Signed  ))))
     281                               (Tpointer (Tint I16 Signed  ))))
    286282                           (Ssequence
    287283                           (Sassign (Expr (Evar (ident_of_nat 4))
    288                                       (Tpointer Any (Tint I16 Signed  )))
     284                                      (Tpointer (Tint I16 Signed  )))
    289285                             (Expr (Evar (ident_of_nat 20))
    290                                (Tpointer Any (Tint I16 Signed  ))))
     286                               (Tpointer (Tint I16 Signed  ))))
    291287                           (Ssequence
    292288                           (Sassign (Expr (Evar (ident_of_nat 20))
    293                                       (Tpointer Any (Tint I16 Signed  )))
     289                                      (Tpointer (Tint I16 Signed  )))
    294290                             (Expr (Ebinop Oadd
    295291                               (Expr (Evar (ident_of_nat 4))
    296                                  (Tpointer Any (Tint I16 Signed  )))
     292                                 (Tpointer (Tint I16 Signed  )))
    297293                               (Expr (Econst_int I32 (repr ? 1))
    298294                                 (Tint I32 Signed  )))
    299                                (Tpointer Any (Tint I16 Signed  ))))
     295                               (Tpointer (Tint I16 Signed  ))))
    300296                           (Ssequence
    301297                           (Sassign (Expr (Ederef
    302298                                      (Expr (Evar (ident_of_nat 3))
    303                                         (Tpointer Any (Tint I16 Signed  ))))
     299                                        (Tpointer (Tint I16 Signed  ))))
    304300                                      (Tint I16 Signed  ))
    305301                             (Expr (Ederef
    306302                               (Expr (Evar (ident_of_nat 4))
    307                                  (Tpointer Any (Tint I16 Signed  ))))
     303                                 (Tpointer (Tint I16 Signed  ))))
    308304                               (Tint I16 Signed  )))
    309305                           (Ssequence
     
    336332     )〉;
    337333    〈ident_of_nat 23 (* main *), CL_Internal (
    338       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed  ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed  ) 3)〉 ]
     334      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 24, (Tarray (Tint I16 Signed  ) 3)〉 ; 〈ident_of_nat 25, (Tarray (Tint I16 Signed  ) 3)〉 ]
    339335        (Ssequence
    340336        (Sassign (Expr (Ederef
    341337                   (Expr (Ebinop Oadd
    342338                     (Expr (Evar (ident_of_nat 24))
    343                        (Tarray Any (Tint I16 Signed  ) 3))
     339                       (Tarray (Tint I16 Signed  ) 3))
    344340                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    345                      (Tpointer Any (Tint I16 Signed  ))))
    346                    (Tint I16 Signed  ))
     341                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
    347342          (Expr (Ecast (Tint I16 Signed  )
    348343            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     
    352347                   (Expr (Ebinop Oadd
    353348                     (Expr (Evar (ident_of_nat 24))
    354                        (Tarray Any (Tint I16 Signed  ) 3))
     349                       (Tarray (Tint I16 Signed  ) 3))
    355350                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    356                      (Tpointer Any (Tint I16 Signed  ))))
    357                    (Tint I16 Signed  ))
     351                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
    358352          (Expr (Ecast (Tint I16 Signed  )
    359353            (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     
    363357                   (Expr (Ebinop Oadd
    364358                     (Expr (Evar (ident_of_nat 24))
    365                        (Tarray Any (Tint I16 Signed  ) 3))
     359                       (Tarray (Tint I16 Signed  ) 3))
    366360                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    367                      (Tpointer Any (Tint I16 Signed  ))))
    368                    (Tint I16 Signed  ))
     361                     (Tpointer (Tint I16 Signed  )))) (Tint I16 Signed  ))
    369362          (Expr (Ecast (Tint I16 Signed  )
    370363            (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     
    372365        (Ssequence
    373366        (Scall (None expr) (Expr (Evar (ident_of_nat 0))
    374                              (Tfunction (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tpointer Any (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
    375           [(Expr (Evar (ident_of_nat 25)) (Tarray Any (Tint I16 Signed  ) 3));
    376           (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed  ) 3));
     367                             (Tfunction (Tcons (Tpointer (Tint I16 Signed  )) (Tcons (Tpointer (Tint I16 Signed  )) (Tcons (Tint I32 Signed  ) Tnil))) Tvoid))
     368          [(Expr (Evar (ident_of_nat 25)) (Tarray (Tint I16 Signed  ) 3));
     369          (Expr (Evar (ident_of_nat 24)) (Tarray (Tint I16 Signed  ) 3));
    377370          (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  ))])
    378371        (Sreturn (Some expr (Expr (Ebinop Oadd
     
    382375                                    (Expr (Ebinop Oadd
    383376                                      (Expr (Evar (ident_of_nat 25))
    384                                         (Tarray Any (Tint I16 Signed  ) 3))
     377                                        (Tarray (Tint I16 Signed  ) 3))
    385378                                      (Expr (Econst_int I32 (repr ? 0))
    386379                                        (Tint I32 Signed  )))
    387                                       (Tpointer Any (Tint I16 Signed  ))))
     380                                      (Tpointer (Tint I16 Signed  ))))
    388381                                    (Tint I16 Signed  )))
    389382                                  (Tint I32 Signed  ))
     
    392385                                    (Expr (Ebinop Oadd
    393386                                      (Expr (Evar (ident_of_nat 25))
    394                                         (Tarray Any (Tint I16 Signed  ) 3))
     387                                        (Tarray (Tint I16 Signed  ) 3))
    395388                                      (Expr (Econst_int I32 (repr ? 1))
    396389                                        (Tint I32 Signed  )))
    397                                       (Tpointer Any (Tint I16 Signed  ))))
     390                                      (Tpointer (Tint I16 Signed  ))))
    398391                                    (Tint I16 Signed  )))
    399392                                  (Tint I32 Signed  ))) (Tint I32 Signed  ))
     
    402395                                  (Expr (Ebinop Oadd
    403396                                    (Expr (Evar (ident_of_nat 25))
    404                                       (Tarray Any (Tint I16 Signed  ) 3))
     397                                      (Tarray (Tint I16 Signed  ) 3))
    405398                                    (Expr (Econst_int I32 (repr ? 2))
    406399                                      (Tint I32 Signed  )))
    407                                     (Tpointer Any (Tint I16 Signed  ))))
     400                                    (Tpointer (Tint I16 Signed  ))))
    408401                                  (Tint I16 Signed  ))) (Tint I32 Signed  )))
    409402                              (Tint I32 Signed  ))))))))
  • src/Clight/test/insertsort.c.ma

    r1513 r2176  
    66
    77definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    8   [〈〈ident_of_nat 3 (* l6 *), Any〉,
     8  [〈〈ident_of_nat 3 (* l6 *), XData〉,
    99     〈[(Init_int8 (repr I8 69)) ; (Init_space 3) ;
    10         (Init_null Any) ],
    11      (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    12   〈〈ident_of_nat 4 (* l5 *), Any〉,
     10        (Init_null) ],
     11     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     12  〈〈ident_of_nat 4 (* l5 *), XData〉,
    1313    〈[(Init_int8 (repr I8 36)) ; (Init_space 3) ;
    14        (Init_addrof Any (ident_of_nat 3) 0)],
    15     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    16   〈〈ident_of_nat 5 (* l4 *), Any〉,
     14       (Init_addrof (ident_of_nat 3) 0)],
     15    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     16  〈〈ident_of_nat 5 (* l4 *), XData〉,
    1717    〈[(Init_int8 (repr I8 136)) ; (Init_space 3) ;
    18        (Init_addrof Any (ident_of_nat 4) 0)],
    19     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    20   〈〈ident_of_nat 6 (* l3 *), Any〉,
     18       (Init_addrof (ident_of_nat 4) 0)],
     19    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     20  〈〈ident_of_nat 6 (* l3 *), XData〉,
    2121    〈[(Init_int8 (repr I8 105)) ; (Init_space 3) ;
    22        (Init_addrof Any (ident_of_nat 5) 0)],
    23     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    24   〈〈ident_of_nat 7 (* l2 *), Any〉,
     22       (Init_addrof (ident_of_nat 5) 0)],
     23    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     24  〈〈ident_of_nat 7 (* l2 *), XData〉,
    2525    〈[(Init_int8 (repr I8 234)) ; (Init_space 3) ;
    26        (Init_addrof Any (ident_of_nat 6) 0)],
    27     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    28   〈〈ident_of_nat 8 (* l1 *), Any〉,
     26       (Init_addrof (ident_of_nat 6) 0)],
     27    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     28  〈〈ident_of_nat 8 (* l1 *), XData〉,
    2929    〈[(Init_int8 (repr I8 240)) ; (Init_space 3) ;
    30        (Init_addrof Any (ident_of_nat 7) 0)],
    31     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉;
    32   〈〈ident_of_nat 9 (* l0 *), Any〉,
     30       (Init_addrof (ident_of_nat 7) 0)],
     31    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉;
     32  〈〈ident_of_nat 9 (* l0 *), XData〉,
    3333    〈[(Init_int8 (repr I8 102)) ; (Init_space 3) ;
    34        (Init_addrof Any (ident_of_nat 8) 0)],
    35     (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))〉〉]
     34       (Init_addrof (ident_of_nat 8) 0)],
     35    (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))〉〉]
    3636  [〈ident_of_nat 10 (* insert *), CL_Internal (
    37      mk_function Tvoid [〈ident_of_nat 12, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed  )〉 ]
     37     mk_function Tvoid [〈ident_of_nat 12, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 13, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 11, (Tint I32 Signed  )〉 ]
    3838       (Ssequence
    3939       (Sifthenelse (Expr (Ebinop Oeq
    4040                      (Expr (Ederef
    4141                        (Expr (Evar (ident_of_nat 13))
    42                           (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    43                         (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    44                       (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))
    45                         (Expr (Ecast (Tpointer Any Tvoid)
     42                          (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     43                        (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     44                      (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))
     45                        (Expr (Ecast (Tpointer Tvoid)
    4646                          (Expr (Econst_int I8 (repr ? 0))
    47                             (Tint I8 Unsigned ))) (Tpointer Any Tvoid)))
    48                         (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     47                            (Tint I8 Unsigned ))) (Tpointer Tvoid)))
     48                        (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    4949                      (Tint I32 Signed  ))
    5050         (Sassign (Expr (Evar (ident_of_nat 11)) (Tint I32 Signed  ))
     
    5757                                 (Expr (Ederef
    5858                                   (Expr (Evar (ident_of_nat 13))
    59                                      (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    60                                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    61                                  (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
     59                                     (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     60                                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     61                                 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    6262                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    6363               (Expr (Ecast (Tint I32 Signed  )
    6464                 (Expr (Efield (Expr (Ederef
    6565                                 (Expr (Evar (ident_of_nat 12))
    66                                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    67                                  (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
     66                                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     67                                 (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    6868                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    6969               (Tint I32 Signed  ))
     
    7474         (Sassign (Expr (Efield (Expr (Ederef
    7575                                  (Expr (Evar (ident_of_nat 12))
    76                                     (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    77                                   (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    78                     (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     76                                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     77                                  (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     78                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    7979           (Expr (Ederef
    8080             (Expr (Evar (ident_of_nat 13))
    81                (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    82              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     81               (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     82             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    8383         (Sassign (Expr (Ederef
    8484                    (Expr (Evar (ident_of_nat 13))
    85                       (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    86                     (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     85                      (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     86                    (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    8787           (Expr (Evar (ident_of_nat 12))
    88              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
     88             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
    8989         (Scall (None expr) (Expr (Evar (ident_of_nat 10))
    90                               (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
     90                              (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
    9191           [(Expr (Evar (ident_of_nat 12))
    92               (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))));
     92              (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))));
    9393           (Expr (Eaddrof
    9494             (Expr (Efield (Expr (Ederef
    9595                             (Expr (Ederef
    9696                               (Expr (Evar (ident_of_nat 13))
    97                                  (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    98                                (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    99                              (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    100                (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    101              (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))])))
     97                                 (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     98                               (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     99                             (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     100               (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     101             (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])))
    102102     
    103103     
     
    105105   )〉;
    106106  〈ident_of_nat 14 (* sort *), CL_Internal (
    107     mk_function Tvoid [〈ident_of_nat 17, (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ]
     107    mk_function Tvoid [〈ident_of_nat 17, (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))〉 ] [〈ident_of_nat 15, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 2, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ; 〈ident_of_nat 16, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ]
    108108      (Ssequence
    109109      (Sassign (Expr (Evar (ident_of_nat 2))
    110                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     110                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    111111        (Expr (Ederef
    112112          (Expr (Evar (ident_of_nat 17))
    113             (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    114           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     113            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     114          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    115115      (Ssequence
    116116      (Sassign (Expr (Evar (ident_of_nat 16))
    117                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    118         (Expr (Ecast (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))
     117                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     118        (Expr (Ecast (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))
    119119          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    120           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     120          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    121121      (Ssequence
    122122      (Swhile (Expr (Evar (ident_of_nat 2))
    123                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     123                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    124124        (Ssequence
    125125        (Sassign (Expr (Evar (ident_of_nat 15))
    126                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     126                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    127127          (Expr (Evar (ident_of_nat 2))
    128             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     128            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    129129        (Ssequence
    130130        (Sassign (Expr (Evar (ident_of_nat 2))
    131                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     131                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    132132          (Expr (Efield (Expr (Ederef
    133133                          (Expr (Evar (ident_of_nat 2))
    134                             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    135                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    136             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     134                            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     135                          (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     136            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    137137        (Scall (None expr) (Expr (Evar (ident_of_nat 10))
    138                              (Tfunction (Tcons (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
     138                             (Tfunction (Tcons (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil)) Tvoid))
    139139          [(Expr (Evar (ident_of_nat 15))
    140              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))));
     140             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))));
    141141          (Expr (Eaddrof
    142142            (Expr (Evar (ident_of_nat 16))
    143               (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    144             (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))]))))
     143              (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     144            (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))]))))
    145145      (Sassign (Expr (Ederef
    146146                 (Expr (Evar (ident_of_nat 17))
    147                    (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))
    148                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     147                   (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))
     148                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    149149        (Expr (Evar (ident_of_nat 16))
    150           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))))))
     150          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))))))
    151151   
    152152   
     
    155155  〈ident_of_nat 18 (* out *), CL_External (ident_of_nat 18) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
    156156  〈ident_of_nat 19 (* main *), CL_Internal (
    157     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 20, (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))〉 ]
     157    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 20, (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))〉 ]
    158158      (Ssequence
    159159      (Sassign (Expr (Evar (ident_of_nat 20))
    160                  (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     160                 (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    161161        (Expr (Eaddrof
    162162          (Expr (Evar (ident_of_nat 9))
    163             (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
    164           (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
     163            (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
     164          (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
    165165      (Ssequence
    166166      (Scall (None expr) (Expr (Evar (ident_of_nat 14))
    167                            (Tfunction (Tcons (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))) Tnil) Tvoid))
     167                           (Tfunction (Tcons (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))) Tnil) Tvoid))
    168168        [(Expr (Eaddrof
    169169           (Expr (Evar (ident_of_nat 20))
    170              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    171            (Tpointer Any (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))])
     170             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     171           (Tpointer (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))])
    172172      (Ssequence
    173173      (Swhile (Expr (Evar (ident_of_nat 20))
    174                 (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     174                (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    175175        (Ssequence
    176176        (Scall (None expr) (Expr (Evar (ident_of_nat 18))
     
    178178          [(Expr (Efield (Expr (Ederef
    179179                           (Expr (Evar (ident_of_nat 20))
    180                              (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    181                            (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
     180                             (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     181                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 1))
    182182             (Tint I8 Unsigned ))])
    183183        (Sassign (Expr (Evar (ident_of_nat 20))
    184                    (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))))
     184                   (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))))
    185185          (Expr (Efield (Expr (Ederef
    186186                          (Expr (Evar (ident_of_nat 20))
    187                             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))
    188                           (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
    189             (Tpointer Any (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr Any (ident_of_nat 0)) Fnil))))))))
     187                            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))
     188                          (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil)))) (ident_of_nat 2))
     189            (Tpointer (Tstruct (ident_of_nat 0) (Fcons (ident_of_nat 1) (Tint I8 Unsigned ) (Fcons (ident_of_nat 2) (Tcomp_ptr (ident_of_nat 0)) Fnil))))))))
    190190      (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
    191191                            (Tint I32 Signed  )))))))
  • src/Clight/test/memorymodel.ma

    r1993 r2176  
    2121   store. *)
    2222definition store0 := empty.
    23 definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 Any.
     23definition store1block : mem × Σb:block.? ≝ alloc store0 0 4 XData.
    2424definition store1 : mem ≝ fst ?? store1block.
    2525definition block :block := pi1 … (snd ?? store1block).
     
    2727(* write a value *)
    2828definition store2 : mem.
    29   letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer Any block (same_compat …) zero_offset) (Vint I16 (repr ? 1)));
     29  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer block zero_offset) (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 (ASTint I8 Unsigned) store2 (mk_pointer Any block (same_compat …) zero_offset) (Vint I8 (repr ? 1)));
     36  letin r ≝ (store (ASTint I8 Unsigned) store2 (mk_pointer block zero_offset) (Vint I8 (repr ? 1)))
    3737
    3838  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
     
    4141(* This is what happened under the original CompCert 1.6 ported memory model:
    4242   The size checking rejects the read and gives us Some Vundef.
    43 example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? Vundef. @refl qed.
     43example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? Vundef. @refl qed.
    4444*)
    4545(* Now we do byte-wise values and get to see the altered integer. *)
    46 example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
     46example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.
    4747
    4848(* The read is successful and returns the value. *)
    49 example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer Any block (same_compat …) zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
     49example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer block zero_offset) = Some ? (Vint I8 (repr ? 1)). // qed.
    5050
    5151(* NB: Double frees are allowed by the memory model (although not necessarily
     
    5757   stack memory in the semantics. *)
    5858definition storeA := empty.
    59 definition storeBblkB := alloc storeA 0 4 Any.
    60 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
     59definition storeBblkB := alloc storeA 0 4 XData.
     60definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData.
    6161definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    6262definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
     
    6767   doesn't currently expose parts of pointers. *)
    6868definition storeI := empty.
    69 definition storeIIblk := alloc storeI 0 4 Any.
     69definition storeIIblk := alloc storeI 0 4 XData.
    7070definition storeIII : mem.
    71  letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset) (Vint I32 (repr ? 1)));
     71 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer (snd ?? storeIIblk) zero_offset) (Vint I32 (repr ? 1)));
    7272  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
    7373  | #rr #_ @rr ] qed.
    74 definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer Any (snd ?? storeIIblk) (same_compat …) zero_offset).
     74definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer (snd ?? storeIIblk) zero_offset).
    7575example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)
     76
  • src/Clight/test/null-op.c.ma

    r1513 r2176  
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    55  [][〈ident_of_nat 0 (* main *), CL_Internal (
    6        mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I8 Unsigned ))〉 ]
     6       mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 3, (Tpointer (Tint I8 Unsigned ))〉 ]
    77         (Ssequence
    88         (Sassign (Expr (Evar (ident_of_nat 2))
    9                     (Tpointer Any (Tint I8 Unsigned )))
    10            (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
     9                    (Tpointer (Tint I8 Unsigned )))
     10           (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
    1111             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12              (Tpointer Any (Tint I8 Unsigned ))))
     12             (Tpointer (Tint I8 Unsigned ))))
    1313         (Ssequence
    1414         (Sassign (Expr (Evar (ident_of_nat 3))
    15                     (Tpointer Any (Tint I8 Unsigned )))
     15                    (Tpointer (Tint I8 Unsigned )))
    1616           (Expr (Eaddrof (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    17              (Tpointer Any (Tint I8 Unsigned ))))
     17             (Tpointer (Tint I8 Unsigned ))))
    1818         (Ssequence
    1919         (Sifthenelse (Expr (Ebinop Oeq
    2020                        (Expr (Evar (ident_of_nat 2))
    21                           (Tpointer Any (Tint I8 Unsigned )))
     21                          (Tpointer (Tint I8 Unsigned )))
    2222                        (Expr (Evar (ident_of_nat 3))
    23                           (Tpointer Any (Tint I8 Unsigned ))))
     23                          (Tpointer (Tint I8 Unsigned ))))
    2424                        (Tint I32 Signed  ))
    2525           (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
     
    3030                        (Expr (Ebinop Osub
    3131                          (Expr (Evar (ident_of_nat 2))
    32                             (Tpointer Any (Tint I8 Unsigned )))
     32                            (Tpointer (Tint I8 Unsigned )))
    3333                          (Expr (Evar (ident_of_nat 2))
    34                             (Tpointer Any (Tint I8 Unsigned ))))
     34                            (Tpointer (Tint I8 Unsigned ))))
    3535                          (Tint I32 Signed  ))
    3636                        (Expr (Econst_int I32 (repr ? 0))
     
    4141         (Ssequence
    4242         (Sassign (Expr (Evar (ident_of_nat 2))
    43                     (Tpointer Any (Tint I8 Unsigned )))
     43                    (Tpointer (Tint I8 Unsigned )))
    4444           (Expr (Ebinop Oadd
    45              (Expr (Evar (ident_of_nat 2))
    46                (Tpointer Any (Tint I8 Unsigned )))
     45             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
    4746             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    48              (Tpointer Any (Tint I8 Unsigned ))))
     47             (Tpointer (Tint I8 Unsigned ))))
    4948         (Ssequence
    5049         (Sassign (Expr (Evar (ident_of_nat 2))
    51                     (Tpointer Any (Tint I8 Unsigned )))
     50                    (Tpointer (Tint I8 Unsigned )))
    5251           (Expr (Ebinop Oadd
    5352             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
    54              (Expr (Evar (ident_of_nat 2))
    55                (Tpointer Any (Tint I8 Unsigned ))))
    56              (Tpointer Any (Tint I8 Unsigned ))))
     53             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned ))))
     54             (Tpointer (Tint I8 Unsigned ))))
    5755         (Ssequence
    5856         (Sassign (Expr (Evar (ident_of_nat 2))
    59                     (Tpointer Any (Tint I8 Unsigned )))
     57                    (Tpointer (Tint I8 Unsigned )))
    6058           (Expr (Ebinop Osub
    61              (Expr (Evar (ident_of_nat 2))
    62                (Tpointer Any (Tint I8 Unsigned )))
     59             (Expr (Evar (ident_of_nat 2)) (Tpointer (Tint I8 Unsigned )))
    6360             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    64              (Tpointer Any (Tint I8 Unsigned ))))
     61             (Tpointer (Tint I8 Unsigned ))))
    6562         (Sreturn (Some expr (Expr (Ebinop Oeq
    6663                               (Expr (Evar (ident_of_nat 2))
    67                                  (Tpointer Any (Tint I8 Unsigned )))
    68                                (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
    69                                  (Expr (Ecast (Tpointer Any Tvoid)
     64                                 (Tpointer (Tint I8 Unsigned )))
     65                               (Expr (Ecast (Tpointer (Tint I8 Unsigned ))
     66                                 (Expr (Ecast (Tpointer Tvoid)
    7067                                   (Expr (Econst_int I8 (repr ? 0))
    71                                      (Tint I8 Unsigned )))
    72                                    (Tpointer Any Tvoid)))
    73                                  (Tpointer Any (Tint I8 Unsigned ))))
     68                                     (Tint I8 Unsigned ))) (Tpointer Tvoid)))
     69                                 (Tpointer (Tint I8 Unsigned ))))
    7470                               (Tint I32 Signed  )))))))))))
    7571       
  • src/Clight/test/search.c.ma

    r1991 r2176  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program (λ_.clight_fundef) ((list init_data) × type)
    5   []
    6   [〈ident_of_nat 0 (* search *), CL_Internal (
    7      mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    8        (Ssequence
    9        (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    10          (Expr (Ecast (Tint I8 Unsigned )
    11            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    12            (Tint I8 Unsigned )))
    13        (Ssequence
    14        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    15          (Expr (Ecast (Tint I8 Unsigned )
    16            (Expr (Ebinop Osub
    17              (Expr (Ecast (Tint I32 Signed  )
    18                (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
    19                (Tint I32 Signed  ))
    20              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    21              (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    22        (Ssequence
    23        (Swhile (Expr (Ebinop Oge
    24                  (Expr (Ecast (Tint I32 Signed  )
    25                    (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    26                    (Tint I32 Signed  ))
    27                  (Expr (Ecast (Tint I32 Signed  )
    28                    (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    29                    (Tint I32 Signed  ))) (Tint I32 Signed  ))
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* search *), CL_Internal (
     6       mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    307         (Ssequence
    31          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
     8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    329           (Expr (Ecast (Tint I8 Unsigned )
    33              (Expr (Ebinop Odiv
    34                (Expr (Ebinop Oadd
    35                  (Expr (Ecast (Tint I32 Signed  )
    36                    (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    37                    (Tint I32 Signed  ))
    38                  (Expr (Ecast (Tint I32 Signed  )
    39                    (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    40                    (Tint I32 Signed  ))) (Tint I32 Signed  ))
    41                (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     10             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     11             (Tint I8 Unsigned )))
     12         (Ssequence
     13         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     14           (Expr (Ecast (Tint I8 Unsigned )
     15             (Expr (Ebinop Osub
     16               (Expr (Ecast (Tint I32 Signed  )
     17                 (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
     18                 (Tint I32 Signed  ))
     19               (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    4220               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    4321         (Ssequence
    44          (Sifthenelse (Expr (Ebinop Oeq
    45                         (Expr (Ecast (Tint I32 Signed  )
    46                           (Expr (Ederef
    47                             (Expr (Ebinop Oadd
    48                               (Expr (Evar (ident_of_nat 4))
    49                                 (Tpointer Any (Tint I8 Unsigned )))
    50                               (Expr (Evar (ident_of_nat 3))
    51                                 (Tint I8 Unsigned )))
    52                               (Tpointer Any (Tint I8 Unsigned ))))
    53                             (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    54                         (Expr (Ecast (Tint I32 Signed  )
    55                           (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
    56                           (Tint I32 Signed  ))) (Tint I32 Signed  ))
    57            (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    58                                  (Tint I8 Unsigned ))))
    59            Sskip)
    60          (Ssequence
    61          (Sifthenelse (Expr (Ebinop Ogt
    62                         (Expr (Ecast (Tint I32 Signed  )
    63                           (Expr (Ederef
    64                             (Expr (Ebinop Oadd
    65                               (Expr (Evar (ident_of_nat 4))
    66                                 (Tpointer Any (Tint I8 Unsigned )))
    67                               (Expr (Evar (ident_of_nat 3))
    68                                 (Tint I8 Unsigned )))
    69                               (Tpointer Any (Tint I8 Unsigned ))))
    70                             (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    71                         (Expr (Ecast (Tint I32 Signed  )
    72                           (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
    73                           (Tint I32 Signed  ))) (Tint I32 Signed  ))
    74            (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     22         (Swhile (Expr (Ebinop Oge
     23                   (Expr (Ecast (Tint I32 Signed  )
     24                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     25                     (Tint I32 Signed  ))
     26                   (Expr (Ecast (Tint I32 Signed  )
     27                     (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     28                     (Tint I32 Signed  ))) (Tint I32 Signed  ))
     29           (Ssequence
     30           (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    7531             (Expr (Ecast (Tint I8 Unsigned )
    76                (Expr (Ebinop Osub
    77                  (Expr (Ecast (Tint I32 Signed  )
    78                    (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    79                    (Tint I32 Signed  ))
    80                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     32               (Expr (Ebinop Odiv
     33                 (Expr (Ebinop Oadd
     34                   (Expr (Ecast (Tint I32 Signed  )
     35                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     36                     (Tint I32 Signed  ))
     37                   (Expr (Ecast (Tint I32 Signed  )
     38                     (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
     39                     (Tint I32 Signed  ))) (Tint I32 Signed  ))
     40                 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    8141                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    82            Sskip)
    83          (Sifthenelse (Expr (Ebinop Olt
    84                         (Expr (Ecast (Tint I32 Signed  )
    85                           (Expr (Ederef
    86                             (Expr (Ebinop Oadd
    87                               (Expr (Evar (ident_of_nat 4))
    88                                 (Tpointer Any (Tint I8 Unsigned )))
    89                               (Expr (Evar (ident_of_nat 3))
    90                                 (Tint I8 Unsigned )))
    91                               (Tpointer Any (Tint I8 Unsigned ))))
    92                             (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    93                         (Expr (Ecast (Tint I32 Signed  )
    94                           (Expr (Evar (ident_of_nat 6)) (Tint I8 Unsigned )))
    95                           (Tint I32 Signed  ))) (Tint I32 Signed  ))
    96            (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    97              (Expr (Ecast (Tint I8 Unsigned )
    98                (Expr (Ebinop Oadd
    99                  (Expr (Ecast (Tint I32 Signed  )
    100                    (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    101                    (Tint I32 Signed  ))
    102                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    103                  (Tint I32 Signed  ))) (Tint I8 Unsigned )))
    104            Sskip)))))
    105        (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
    106                              (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
    107                                                  (Tint I32 Signed  )))
    108                                (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
    109      
    110      
    111      
    112    )〉;
    113   〈ident_of_nat 7 (* main *), CL_Internal (
    114     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
    115       (Ssequence
    116       (Sassign (Expr (Ederef
     42           (Ssequence
     43           (Sifthenelse (Expr (Ebinop Oeq
     44                          (Expr (Ecast (Tint I32 Signed  )
     45                            (Expr (Ederef
     46                              (Expr (Ebinop Oadd
     47                                (Expr (Evar (ident_of_nat 4))
     48                                  (Tpointer (Tint I8 Unsigned )))
     49                                (Expr (Evar (ident_of_nat 3))
     50                                  (Tint I8 Unsigned )))
     51                                (Tpointer (Tint I8 Unsigned ))))
     52                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     53                          (Expr (Ecast (Tint I32 Signed  )
     54                            (Expr (Evar (ident_of_nat 6))
     55                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     56                          (Tint I32 Signed  ))
     57             (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
     58                                   (Tint I8 Unsigned ))))
     59             Sskip)
     60           (Ssequence
     61           (Sifthenelse (Expr (Ebinop Ogt
     62                          (Expr (Ecast (Tint I32 Signed  )
     63                            (Expr (Ederef
     64                              (Expr (Ebinop Oadd
     65                                (Expr (Evar (ident_of_nat 4))
     66                                  (Tpointer (Tint I8 Unsigned )))
     67                                (Expr (Evar (ident_of_nat 3))
     68                                  (Tint I8 Unsigned )))
     69                                (Tpointer (Tint I8 Unsigned ))))
     70                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     71                          (Expr (Ecast (Tint I32 Signed  )
     72                            (Expr (Evar (ident_of_nat 6))
     73                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     74                          (Tint I32 Signed  ))
     75             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     76               (Expr (Ecast (Tint I8 Unsigned )
     77                 (Expr (Ebinop Osub
     78                   (Expr (Ecast (Tint I32 Signed  )
     79                     (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
     80                     (Tint I32 Signed  ))
     81                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     82                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
     83             Sskip)
     84           (Sifthenelse (Expr (Ebinop Olt
     85                          (Expr (Ecast (Tint I32 Signed  )
     86                            (Expr (Ederef
     87                              (Expr (Ebinop Oadd
     88                                (Expr (Evar (ident_of_nat 4))
     89                                  (Tpointer (Tint I8 Unsigned )))
     90                                (Expr (Evar (ident_of_nat 3))
     91                                  (Tint I8 Unsigned )))
     92                                (Tpointer (Tint I8 Unsigned ))))
     93                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))
     94                          (Expr (Ecast (Tint I32 Signed  )
     95                            (Expr (Evar (ident_of_nat 6))
     96                              (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     97                          (Tint I32 Signed  ))
     98             (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
     99               (Expr (Ecast (Tint I8 Unsigned )
    117100                 (Expr (Ebinop Oadd
    118                    (Expr (Evar (ident_of_nat 4))
    119                      (Tarray Any (Tint I8 Unsigned ) 5))
    120                    (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    121                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    122         (Expr (Ecast (Tint I8 Unsigned )
    123           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    124           (Tint I8 Unsigned )))
    125       (Ssequence
    126       (Sassign (Expr (Ederef
    127                  (Expr (Ebinop Oadd
    128                    (Expr (Evar (ident_of_nat 4))
    129                      (Tarray Any (Tint I8 Unsigned ) 5))
     101                   (Expr (Ecast (Tint I32 Signed  )
     102                     (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
     103                     (Tint I32 Signed  ))
    130104                   (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    131                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    132         (Expr (Ecast (Tint I8 Unsigned )
    133           (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
    134           (Tint I8 Unsigned )))
    135       (Ssequence
    136       (Sassign (Expr (Ederef
    137                  (Expr (Ebinop Oadd
    138                    (Expr (Evar (ident_of_nat 4))
    139                      (Tarray Any (Tint I8 Unsigned ) 5))
    140                    (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    141                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    142         (Expr (Ecast (Tint I8 Unsigned )
    143           (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
    144           (Tint I8 Unsigned )))
    145       (Ssequence
    146       (Sassign (Expr (Ederef
    147                  (Expr (Ebinop Oadd
    148                    (Expr (Evar (ident_of_nat 4))
    149                      (Tarray Any (Tint I8 Unsigned ) 5))
    150                    (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
    151                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    152         (Expr (Ecast (Tint I8 Unsigned )
    153           (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
    154           (Tint I8 Unsigned )))
    155       (Ssequence
    156       (Sassign (Expr (Ederef
    157                  (Expr (Ebinop Oadd
    158                    (Expr (Evar (ident_of_nat 4))
    159                      (Tarray Any (Tint I8 Unsigned ) 5))
    160                    (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
    161                    (Tpointer Any (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
    162         (Expr (Ecast (Tint I8 Unsigned )
    163           (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
    164           (Tint I8 Unsigned )))
    165       (Ssequence
    166       (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
    167         (Expr (Evar (ident_of_nat 0))
    168           (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
    169         [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
    170         (Expr (Ecast (Tint I8 Unsigned )
    171           (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
    172           (Tint I8 Unsigned ));
    173         (Expr (Ecast (Tint I8 Unsigned )
    174           (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
    175           (Tint I8 Unsigned ))])
    176       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    177                             (Expr (Evar (ident_of_nat 8))
    178                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
    179    
    180    
    181    
    182   )〉]
     105                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
     106             Sskip)))))
     107         (Sreturn (Some expr (Expr (Ecast (Tint I8 Unsigned )
     108                               (Expr (Eunop Oneg (Expr (Econst_int I32 (repr ? 1))
     109                                                   (Tint I32 Signed  )))
     110                                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))))))
     111       
     112       
     113       
     114     )〉;
     115    〈ident_of_nat 7 (* main *), CL_Internal (
     116      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
     117        (Ssequence
     118        (Sassign (Expr (Ederef
     119                   (Expr (Ebinop Oadd
     120                     (Expr (Evar (ident_of_nat 4))
     121                       (Tarray (Tint I8 Unsigned ) 5))
     122                     (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     123                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     124          (Expr (Ecast (Tint I8 Unsigned )
     125            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
     126            (Tint I8 Unsigned )))
     127        (Ssequence
     128        (Sassign (Expr (Ederef
     129                   (Expr (Ebinop Oadd
     130                     (Expr (Evar (ident_of_nat 4))
     131                       (Tarray (Tint I8 Unsigned ) 5))
     132                     (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     133                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     134          (Expr (Ecast (Tint I8 Unsigned )
     135            (Expr (Econst_int I32 (repr ? 18)) (Tint I32 Signed  )))
     136            (Tint I8 Unsigned )))
     137        (Ssequence
     138        (Sassign (Expr (Ederef
     139                   (Expr (Ebinop Oadd
     140                     (Expr (Evar (ident_of_nat 4))
     141                       (Tarray (Tint I8 Unsigned ) 5))
     142                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     143                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     144          (Expr (Ecast (Tint I8 Unsigned )
     145            (Expr (Econst_int I32 (repr ? 23)) (Tint I32 Signed  )))
     146            (Tint I8 Unsigned )))
     147        (Ssequence
     148        (Sassign (Expr (Ederef
     149                   (Expr (Ebinop Oadd
     150                     (Expr (Evar (ident_of_nat 4))
     151                       (Tarray (Tint I8 Unsigned ) 5))
     152                     (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
     153                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     154          (Expr (Ecast (Tint I8 Unsigned )
     155            (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
     156            (Tint I8 Unsigned )))
     157        (Ssequence
     158        (Sassign (Expr (Ederef
     159                   (Expr (Ebinop Oadd
     160                     (Expr (Evar (ident_of_nat 4))
     161                       (Tarray (Tint I8 Unsigned ) 5))
     162                     (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
     163                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
     164          (Expr (Ecast (Tint I8 Unsigned )
     165            (Expr (Econst_int I32 (repr ? 120)) (Tint I32 Signed  )))
     166            (Tint I8 Unsigned )))
     167        (Ssequence
     168        (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
     169          (Expr (Evar (ident_of_nat 0))
     170            (Tfunction (Tcons (Tpointer (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
     171          [(Expr (Evar (ident_of_nat 4)) (Tarray (Tint I8 Unsigned ) 5));
     172          (Expr (Ecast (Tint I8 Unsigned )
     173            (Expr (Econst_int I32 (repr ? 5)) (Tint I32 Signed  )))
     174            (Tint I8 Unsigned ));
     175          (Expr (Ecast (Tint I8 Unsigned )
     176            (Expr (Econst_int I32 (repr ? 57)) (Tint I32 Signed  )))
     177            (Tint I8 Unsigned ))])
     178        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
     179                              (Expr (Evar (ident_of_nat 8))
     180                                (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
     181     
     182     
     183     
     184    )〉]
    183185  (ident_of_nat 7)
     186 
    184187.
    185188
     189(*
     190example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
     191normalize  (* you can examine the result here *)
     192*)
  • src/Clight/test/sum.c.ma

    r1226 r2176  
    33
    44definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
    5   [〈〈ident_of_nat 0 (* src *), Any〉,
     5  [〈〈ident_of_nat 0 (* src *), XData〉,
    66     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    77        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    8         (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     8        (Init_int8 (repr I8 4)) ], (Tarray (Tint I8 Unsigned ) 5)〉〉]
    99  [〈ident_of_nat 1 (* main *), CL_Internal (
    1010     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
     
    2121             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    2222             (Tint I32 Unsigned))
    23            (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
     23           (Expr (Esizeof (Tarray (Tint I8 Unsigned ) 5))
    2424             (Tint I32 Unsigned))) (Tint I32 Signed  ))
    2525         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
     
    3838                   (Expr (Ebinop Oadd
    3939                     (Expr (Evar (ident_of_nat 0))
    40                        (Tarray Any (Tint I8 Unsigned ) 5))
     40                       (Tarray (Tint I8 Unsigned ) 5))
    4141                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    42                      (Tpointer Any (Tint I8 Unsigned ))))
    43                    (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    44                (Tint I32 Signed  ))) (Tint I8 Unsigned )))
     42                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned )))
     43                 (Tint I32 Signed ))) (Tint I32 Signed  )))
     44             (Tint I8 Unsigned )))
    4545       )
    4646       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
  • src/Clight/toCminor.ma

    r1884 r2176  
    102102definition always_alloc : type → bool ≝
    103103λt. match t with
    104 [ Tarray _ _ _ ⇒ true
     104[ Tarray _ _ ⇒ true
    105105| Tstruct _ _ ⇒ true
    106106| Tunion _ _ ⇒ true
     
    268268(* same gig for AST typs *)
    269269definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
    270 * [ #sz1 #sg1 | #r1 | #sz1 ]
    271 * [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
     270* [ #sz1 #sg1 | | #sz1 ]
     271* [ 1,5,9: | *: #a #b try #c try #d @(Error ? (msg TypeMismatch)) ]
    272272[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
    273273  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    274 | *; #P #p @(region_should_eq r1 ?? p)
     274| #P #p @(OK ? p)
    275275| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    276276] qed.
     
    294294          | _ ⇒ Error ? (msg TypeMismatch)
    295295          ]
    296       | ASTptr r
     296      | ASTptr
    297297          match t' return λt'. res (CMunop ? t') with
    298298          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
     
    323323
    324324(* First, how to get rid of a abstract-away pointer or array type *)
    325 definition fix_ptr_type : ∀r,ty,n. expr (typ_of_type (ptr_type r ty n)) → expr (ASTptr r)
    326 λr,ty,n,e. e⌈expr (typ_of_type (ptr_type r ty n)) ↦ expr (ASTptr r)⌉.
     325definition fix_ptr_type : ∀ty,n. expr (typ_of_type (ptr_type ty n)) → expr ASTptr
     326λty,n,e. e⌈expr (typ_of_type (ptr_type ty n)) ↦ expr ASTptr⌉.
    327327cases n //
    328328qed.
     
    336336| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2)
    337337(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    338 | add_case_pi n r ty sz sg ⇒
    339     λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    340 | add_case_ip n sz sg r ty ⇒
    341     λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     338| add_case_pi n ty sz sg ⇒
     339    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     340| add_case_ip n sz sg ty ⇒
     341    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    342342| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    343343].
     
    352352| sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2)
    353353(* XXX could optimise cast as above *)
    354 | sub_case_pi n r ty sz sg ⇒
    355     λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     354| sub_case_pi n ty sz sg ⇒
     355    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    356356(* XXX check in detail? *)
    357 | sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒
     357| sub_case_pp n1 n2 ty1 ty2 ⇒
    358358    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
    359     [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16 r1 r2) (fix_ptr_type … e1) (fix_ptr_type ??? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2))))))
     359    [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2))))))
    360360    | _ ⇒ Error ? (msg TypeMismatch)
    361361    ]
     
    432432    | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2)
    433433    ]
    434 | cmp_case_pp n r ty ⇒
     434| cmp_case_pp n ty ⇒
    435435    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
    436436| cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2)
     
    473473  P t1 v1 →
    474474  P t2 v2.
    475 * [ * * | * | * ]
     475* [ * * | | * ]
    476476* try * try *
    477477#P #v1 #v2 #E whd in E:(??%?); destruct
     
    479479qed.
    480480
    481 lemma unfix_ptr_type : ∀r,ty,n,e.∀P:∀t. expr t → Prop.
    482   P (typ_of_type (ptr_type r ty n)) e →
    483   P (ASTptr r) (fix_ptr_type r ty n e).
    484 #r #ty * [ 2: #n ] #e #P #H @H
     481lemma unfix_ptr_type : ∀ty,n,e.∀P:∀t. expr t → Prop.
     482  P (typ_of_type (ptr_type ty n)) e →
     483  P ASTptr (fix_ptr_type ty n e).
     484#ty * [ 2: #n ] #e #P #H @H
    485485qed.
    486486
     
    503503  | #sz #E1 #E2 #E3 destruct >E3 #E4
    504504    @(typ_equals … E4) % //
    505   | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    506     @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
    507   | #n #sz #sg #r #ty0 #E1 #E2 #E3 destruct >E3 #E4
    508     @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)| % // ]
     505  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     506    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
     507  | #n #sz #sg #ty0 #E1 #E2 #E3 destruct >E3 #E4
     508    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)| % // ]
    509509  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    510510  ]
     
    514514  | #sz #E1 #E2 #E3 destruct >E3 #E4
    515515    @(typ_equals … E4) % //
    516   | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    517     @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
    518   | #n1 #n2 #r1 #ty1' #r2 #ty2' #E1 #E2 #E3 destruct >E3
     516  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     517    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
     518  | #n1 #n2 #ty1' #ty2' #E1 #E2 #E3 destruct >E3
    519519    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
    520     [ 2: #sz #sg #e #E4 | 4: #r #ty #e #E4 | 5: #r #ty' #n' #e #E4
     520    [ 2: #sz #sg #e #E4 | 4: #ty #e #E4 | 5: #ty' #n' #e #E4
    521521    | *: normalize #X1 #X2 try #X3 try #X4 destruct
    522522    ] whd in E4:(??%?); destruct % // %
    523     [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) ]
     523    [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) ]
    524524  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    525525  ]
     
    535535| 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?;
    536536  [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3
    537   | 2,6,10,14,18,22: #n #r #ty' #E1 #E2 #E3 destruct >E3
     537  | 2,6,10,14,18,22: #n #ty' #E1 #E2 #E3 destruct >E3
    538538  | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3
    539539  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
     
    542542  #sz #sg #e #E4
    543543  whd in E4:(??%?); destruct %
    544   [ 25,27,29,31,33,35: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)
    545   | 26,28,30,32,34,36: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)
     544  [ 25,27,29,31,33,35: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)
     545  | 26,28,30,32,34,36: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)
    546546  | *: //
    547547  ]
     
    550550
    551551(* We'll need to implement proper translation of pointers if we really do memory
    552    spaces. *)
     552   spaces.
    553553(* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *)
    554554definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
     
    566566definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
    567567λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
    568 
     568*)
    569569axiom FIXME : String.
    570570
     
    577577    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
    578578    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)
    579     | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
    580     | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
     579    | Tpointer _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
     580    | Tarray _ _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
    581581    | _ ⇒ Error ? (msg TypeMismatch)
    582582    ]
     
    587587    | _ ⇒ Error ? (msg TypeMismatch)
    588588    ]
    589 | Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
     589| Tpointer _ ⇒ λe. (* will need changed for memory regions *)
    590590    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
    591     [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?»
    592     | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
    593     | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
     591    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ?) e, ?»
     592    | Tarray _ _ ⇒ (*translate_ptr ? r1 r2 e*) OK ? e
     593    | Tpointer _ ⇒ OK ? e
    594594    | _ ⇒ Error ? (msg TypeMismatch)
    595595    ]
    596 | Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
     596| Tarray _ _ ⇒ λe. (* will need changed for memory regions *)
    597597    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    598     [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?»
    599     | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
    600     | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
     598    [ Tint sz2 sg2 ⇒ OK ? «Op1 ASTptr (ASTint sz2 sg2) (Ointofptr sz2 ?) e, ?»
     599    | Tarray _ _ ⇒ OK ? e
     600    | Tpointer _ ⇒ OK ? e
    601601    | _ ⇒ Error ? (msg TypeMismatch)
    602602    ]
     
    642642           *)
    643643          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    644           [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol r id 0)), ?» (* Mem is "load" in compcert *)
    645           | By_reference r ⇒ OK ? «Cst ? (Oaddrsymbol r id 0), ?»
     644          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
     645          | By_reference ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    646646          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    647647          ]
     
    650650           * because its adress was taken somewhere or becauste it's a structured data. *)
    651651          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    652           [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?»
    653           | By_reference r ⇒ match r return λr. res (Σe':CMexpr (ASTptr r). ?) with
    654                              [ Any ⇒ OK ? «Cst ? (Oaddrstack n), ?»
     652          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrstack n)), ?»
     653          | By_reference ⇒ (*match r return λr. res (Σe':CMexpr (ASTptr r). ?) with
     654                             [ Any ⇒*) OK ? «Cst ? (Oaddrstack n), ?» (*
    655655                             | _ ⇒ Error  ? [MSG BadlyTypedAccess; CTX ? id]
    656                              ]
     656                             ]*)
    657657          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    658658          ]
     
    669669      *)
    670670      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    671       [ ASTptr r ⇒ λe1'.
     671      [ ASTptr ⇒ λe1'.
    672672          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    673           [ By_value t ⇒ OK ? «Mem t ? (pi1 … e1'), ?»
    674           | By_reference r' ⇒ region_should_eq r r' ? e1'
     673          [ By_value t ⇒ OK ? «Mem t (pi1 … e1'), ?»
     674          | By_reference ⇒ OK ? e1'
    675675          | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    676676          ]
     
    680680      do e1' ← translate_addr vars e1;
    681681      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
    682       [ ASTptr r ⇒
    683           match e1' with
     682      [ ASTptr ⇒ OK ? e1'
     683(*          match e1' with
    684684          [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1'
    685           ]
     685          ]*)
    686686      | _ ⇒ Error ? (msg TypeMismatch)
    687687      ]
     
    743743      [ Tstruct _ fl ⇒
    744744          do e1' ← translate_addr vars e1;
    745           match e1' with
    746           [ mk_DPair r e1' ⇒
     745(*          match e1' with
     746          [ mk_DPair r e1' ⇒*)
    747747            do off ← field_offset id fl;
    748748            match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    749749            [ By_value t ⇒
    750                 OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
     750                OK ? «Mem t (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
    751751                                   (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»
    752             | By_reference r'
    753                 do e1' ← region_should_eq r r' ? e1';
    754                 OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r')
     752            | By_reference
     753(*                do e1' ← region_should_eq r r' ? e1';*)
     754                OK ? «Op2 ASTptr (ASTint I16 Signed (* XXX efficiency? *)) ASTptr
    755755                        (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»
    756756            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    757757            ]
    758           ]
    759758      | Tunion _ _ ⇒
    760759          do e1' ← translate_addr vars e1;
    761           match e1' with
    762           [ mk_DPair r e1' ⇒
    763760            match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with
    764             [ By_value t ⇒ OK ? «Mem t ? e1', ?»
    765             | By_reference r' ⇒ region_should_eq r r' ? e1'
     761            [ By_value t ⇒ OK ? «Mem t e1', ?»
     762            | By_reference ⇒ OK ? e1'
    766763            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    767764            ]
    768           ]
    769765      | _ ⇒ Error ? (msg BadlyTypedAccess)
    770766      ]
     
    777773
    778774(* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1].   *)
    779 and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
     775and translate_addr (vars:var_types) (e:expr) on e : res ((*𝚺r.*) Σe':CMexpr ASTptr. expr_vars ? e' (local_id vars)) ≝
    780776match e with
    781777[ Expr ed _ ⇒
     
    783779  [ Evar id ⇒
    784780      do 〈c,t〉 ← lookup' vars id;
    785       match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
    786       [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol r id 0), ?»❭
    787       | Stack n ⇒ OK ? ❬Any, «Cst ? (Oaddrstack n), ?»❭
     781      match c return λ_. res (Σz:CMexpr ASTptr.?) with
     782      [ Global r ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
     783      | Stack n ⇒ OK ? «Cst ? (Oaddrstack n), ?»
    788784      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
    789785      ]
    790786  | Ederef e1 ⇒
    791787      do e1' ← translate_expr vars e1;
    792       match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (𝚺r. Σz:CMexpr (ASTptr r). ?) with
    793       [ ASTptr r ⇒ λe1'.OK ? ❬r, e1'❭
     788      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σz:CMexpr ASTptr. expr_vars ? z (local_id vars)) with
     789      [ ASTptr ⇒ λe1'.OK ? e1'
    794790      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
    795791      ] e1'
     
    799795          do e1' ← translate_addr vars e1;
    800796          do off ← field_offset id fl;
    801           match e1' with
    802           [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)
    803              (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r)
    804                      (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 Signed (repr ? off))), ?» ❭)
    805           ]
     797(*          match e1' with
     798          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)*)
     799             OK ? «Op2 ASTptr (ASTint I16 Signed (* FIXME inefficient?*)) ASTptr
     800                   (Oaddp I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?»
    806801      | Tunion _ _ ⇒ translate_addr vars e1
    807802      | _ ⇒ Error ? (msg BadlyTypedAccess)
     
    832827inductive destination (vars:var_types) : Type[0] ≝
    833828| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
    834 | MemDest : ∀r:region. (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
     829| MemDest : (Σe:CMexpr ASTptr.expr_vars ? e (local_id vars)) → destination vars.
    835830
    836831(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
     
    858853          match c return λx.? → ? with
    859854          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
    860           | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol r id 0)))
    861           | Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n)))
     855          | Global r ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrsymbol id 0)))
     856          | Stack n ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrstack n)))
    862857          ] E
    863858      | _ ⇒
    864859          do e1' ← translate_addr vars e1;
    865           match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r e1') ]
     860          OK ? (MemDest ? e1')
    866861      ]
    867862  ].
     
    968963    do e2' ← type_should_eq (typeof e2) ty ? e2';
    969964    OK ? «St_assign ? id e2', ?»
    970 | MemDest r e1' ⇒ OK ? «St_store ? r e1' e2', ?»
     965| MemDest e1' ⇒ OK ? «St_store ? e1' e2', ?»
    971966].
    972967% try (//)  try (elim e2' //) elim e1' //
     
    11301125       do e2' ← type_should_eq (typeof e2) ty ? e2';
    11311126       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    1132     | MemDest r e1' ⇒
    1133        OK ? «〈uv, ul, St_store ? r e1' e2'〉, ?»
     1127    | MemDest e1' ⇒
     1128       OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
    11341129    ]
    11351130| Scall ret ef args ⇒
    11361131    do ef' ← translate_expr vars ef;
    1137     do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
     1132    do ef' ← typ_should_eq (typ_of_type (typeof ef)) ASTptr ? ef';
    11381133    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
    11391134    match ret with
     
    11431138        match dest with
    11441139        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
    1145         | MemDest r e1' ⇒
     1140        | MemDest e1' ⇒
    11461141            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
    1147             OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r e1' (Id ? tmp))〉, ?»
     1142            OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))〉, ?»
    11481143        ]
    11491144    ]
     
    12661261try (#l #H elim H)
    12671262try (#size #sign #H assumption)
    1268 try (#region #H assumption)
     1263try (#H1 try #H2 assumption)
    12691264[ 1,5: @(tmp_preserved … p) ]
    12701265[ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ]
     
    12841279       | 2: elim args' // ]
    12851280| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
    1286 [ 1: #size #sign | 2: #reg | 3: #fsize ]
     1281[ 1: #size #sign | 2: | 3: #fsize ]
    12871282[ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
    12881283try @(match fgens1 return λx.x=fgens1 → ? with
     
    14421437  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
    14431438  | Stack n ⇒ λE.
    1444       OK ? «〈fgens1, St_seq (St_store ? Any (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
     1439      OK ? «〈fgens1, St_seq (St_store ? (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
    14451440  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    14461441  ] E) (OK ? s) params.
Note: See TracChangeset for help on using the changeset viewer.