Changeset 124 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (10 years ago)
Author:
campbell
Message:

Initial work on Clight semantics with 8051 memory spaces.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • C-semantics/Csyntax.ma

    r24 r124  
    4646  | F32: floatsize
    4747  | F64: floatsize.
     48
     49(* Pointers can point to particular memory spaces. *)
     50ninductive mem_space : Type ≝
     51  | Generic : mem_space
     52  | Data : mem_space
     53  | IData : mem_space
     54  | XData : mem_space
     55  | Code : mem_space.
    4856
    4957(* * The syntax of type expressions.  Some points to note:
    … …  
    8694  | Tint: intsize → signedness → type   (**r integer types *)
    8795  | Tfloat: floatsize → type            (**r floating-point types *)
    88   | Tpointer: type → type               (**r pointer types ([*ty]) *)
    89   | Tarray: type → Z → type            (**r array types ([ty[len]]) *)
     96  | Tpointer: mem_space → type → type   (**r pointer types ([*ty]) *)
     97  | Tarray: mem_space → type → Z → type (**r array types ([ty[len]]) *)
    9098  | Tfunction: typelist → type → type   (**r function types *)
    9199  | Tstruct: ident → fieldlist → type   (**r struct types *)
    … …  
    107115  (it:∀i,s. P (Tint i s))
    108116  (fl:∀f. P (Tfloat f))
    109   (pt:∀t. P t → P (Tpointer t))
    110   (ar:∀t,n. P t → P (Tarray t n))
     117  (pt:∀s,t. P t → P (Tpointer s t))
     118  (ar:∀s,t,n. P t → P (Tarray s t n))
    111119  (fn:∀tl,t. P t → P (Tfunction tl t))
    112120  (st:∀i,fl. P (Tstruct i fl))
    … …  
    118126  | Tint i s ⇒ it i s
    119127  | Tfloat s ⇒ fl s
    120   | Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t')
    121   | Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t')
     128  | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t')
     129  | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t')
    122130  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
    123131  | Tstruct i fs ⇒ st i fs
    … …  
    357365  | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    358366  | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    359   | Tpointer _ ⇒ 4
    360   | Tarray t' n ⇒ alignof t'
     367  | Tpointer _ _ ⇒ 4
     368  | Tarray _ t' n ⇒ alignof t'
    361369  | Tfunction _ _ ⇒ 1
    362370  | Tstruct _ fld ⇒ alignof_fields fld
    … …  
    382390  (it:∀i,s. P (Tint i s))
    383391  (fl:∀f. P (Tfloat f))
    384   (pt:∀t. P t → P (Tpointer t))
    385   (ar:∀t,n. P t → P (Tarray t n))
     392  (pt:∀s,t. P t → P (Tpointer s t))
     393  (ar:∀s,t,n. P t → P (Tarray s t n))
    386394  (fn:∀tl,t. P t → P (Tfunction tl t))
    387395  (st:∀i,fl. Q fl → P (Tstruct i fl))
    … …  
    395403  | Tint i s ⇒ it i s
    396404  | Tfloat s ⇒ fl s
    397   | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    398   | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     405  | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     406  | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    399407  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    400408  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    … …  
    407415  (it:∀i,s. P (Tint i s))
    408416  (fl:∀f. P (Tfloat f))
    409   (pt:∀t. P t → P (Tpointer t))
    410   (ar:∀t,n. P t → P (Tarray t n))
     417  (pt:∀s,t. P t → P (Tpointer s t))
     418  (ar:∀s,t,n. P t → P (Tarray s t n))
    411419  (fn:∀tl,t. P t → P (Tfunction tl t))
    412420  (st:∀i,fl. Q fl → P (Tstruct i fl))
    … …  
    442450  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    443451  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    444   | Tpointer _ ⇒ 4
    445   | Tarray t' n ⇒ sizeof t' * Zmax 1 n
     452  | Tpointer _ _ ⇒ 4
     453  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
    446454  | Tfunction _ _ ⇒ 1
    447455  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
    … …  
    631639                            | F64 ⇒ By_value Mfloat64 ]
    632640  | Tvoid ⇒ By_nothing
    633   | Tpointer _ ⇒ By_value Mint32
    634   | Tarray _ _ ⇒ By_reference
     641  | Tpointer _ _ ⇒ By_value Mint32
     642  | Tarray _ _ _ ⇒ By_reference
    635643  | Tfunction _ _ ⇒ By_reference
    636644  | Tstruct _ fList ⇒ By_nothing
    … …  
    672680    match ty2 with
    673681    [ Tint _ _ ⇒ add_case_ii
    674     | Tpointer ty ⇒ add_case_ip ty
    675     | Tarray ty _ ⇒ add_case_ip ty
     682    | Tpointer _ ty ⇒ add_case_ip ty
     683    | Tarray _ ty _ ⇒ add_case_ip ty
    676684    | _ ⇒ add_default ]
    677685  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
    678   | Tpointer ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
    679   | Tarray ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
     686  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
     687  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
    680688  | _ ⇒ add_default
    681689  ].
    … …  
    704712  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
    705713  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
    706   | Tpointer ty ⇒
     714  | Tpointer _ ty ⇒
    707715    match ty2 with
    708716    [ Tint _ _ ⇒ sub_case_pi ty
    709     | Tpointer _ ⇒ sub_case_pp ty
    710     | Tarray _ _ ⇒ sub_case_pp ty
     717    | Tpointer _ _ ⇒ sub_case_pp ty
     718    | Tarray _ _ _ ⇒ sub_case_pp ty
    711719    | _ ⇒ sub_default ]
    712   | Tarray ty _ ⇒
     720  | Tarray _ ty _ ⇒
    713721    match ty2 with
    714722    [ Tint _ _ ⇒ sub_case_pi ty
    715     | Tpointer _ ⇒ sub_case_pp ty
    716     | Tarray _ _ ⇒ sub_case_pp ty
     723    | Tpointer _ _ ⇒ sub_case_pp ty
     724    | Tarray _ _ _ ⇒ sub_case_pp ty
    717725    | _ ⇒ sub_default ]
    718726  | _ ⇒ sub_default
    … …  
    831839    | _ ⇒ cmp_default ]
    832840  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
    833   | Tpointer _ ⇒
     841  | Tpointer _ _ ⇒
    834842    match ty2 with
    835843    [ Tint _ _ ⇒ cmp_case_ipip
    836     | Tpointer _ ⇒ cmp_case_ipip
    837     | Tarray _ _ ⇒ cmp_case_ipip
     844    | Tpointer _ _ ⇒ cmp_case_ipip
     845    | Tarray _ _ _ ⇒ cmp_case_ipip
    838846    | _ ⇒ cmp_default ]
    839   | Tarray _ _ ⇒
     847  | Tarray _ _ _ ⇒
    840848    match ty2 with
    841849    [ Tint _ _ ⇒ cmp_case_ipip
    842     | Tpointer _ ⇒ cmp_case_ipip
    843     | Tarray _ _ ⇒ cmp_case_ipip
     850    | Tpointer _ _ ⇒ cmp_case_ipip
     851    | Tarray _ _ _ ⇒ cmp_case_ipip
    844852    | _ ⇒ cmp_default ]
    845853  | _ ⇒ cmp_default
    … …  
    869877  match ty with
    870878  [ Tfunction args res ⇒ fun_case_f args res
    871   | Tpointer ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
    872                                   | _ ⇒ fun_default
    873                                   ]
     879  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
     880                                    | _ ⇒ fun_default
     881                                    ]
    874882  | _ ⇒ fun_default
    875883  ].
Note: See TracChangeset for help on using the changeset viewer.