Changeset 2176 for src/Clight/Cexec.ma


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

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

File:
1 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].
Note: See TracChangeset for help on using the changeset viewer.