Ignore:
Timestamp:
Feb 11, 2011, 4:45:36 PM (9 years ago)
Author:
campbell
Message:

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r496 r498  
    184184
    185185definition load_value_of_type' ≝
    186 λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair r loc ⇒
    187   load_value_of_type ty m r loc ofs ] ].
     186λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
    188187
    189188(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    210209      OK ? 〈v,tr〉
    211210  | Eaddrof a ⇒
    212       do 〈plo,tr〉 ← exec_lvalue ge en m a;
    213       OK ? 〈match plo with [ pair pl ofs ⇒ match pl with [ pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉
     211      do 〈lo,tr〉 ← exec_lvalue ge en m a;
     212      match ty with
     213      [ Tpointer r _ ⇒ OK ? 〈match lo with [ pair loc ofs ⇒  Vptr r loc ofs ], tr〉
     214      | _ ⇒ Error ?
     215      ]
    214216  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
    215217  | Eunop op a ⇒
     
    254256  ]
    255257]
    256 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (region × block × int × trace) ≝
     258and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × int × trace) ≝
    257259  match e' with
    258260  [ Evar id ⇒
    259261      match (get … id en) with
    260       [ None ⇒ do 〈r,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈r,〈r,l〉〉,zero〉,E0〉 (* global *)
    261       | Some loc ⇒ OK ? 〈〈〈Any,loc〉,zero〉,E0〉 (* local *)
     262      [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero〉,E0〉 (* global *)
     263      | Some loc ⇒ OK ? 〈〈loc,zero〉,E0〉 (* local *)
    262264      ]
    263265  | Ederef a ⇒
    264266      do 〈v,tr〉 ← exec_expr ge en m a;
    265267      match v with
    266       [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉
     268      [ Vptr _ l ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
    267269      | _ ⇒ Error ?
    268270      ]
     
    270272      match (typeof a) with
    271273      [ Tstruct id fList ⇒
    272           do 〈plofs,tr〉 ← exec_lvalue ge en m a;
     274          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    273275          do delta ← field_offset i fList;
    274           OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉
     276          OK ? 〈〈\fst lofs,add (\snd lofs) (repr delta)〉,tr〉
    275277      | Tunion id fList ⇒
    276           do 〈plofs,tr〉 ← exec_lvalue ge en m a;
    277           OK ? 〈plofs,tr〉
     278          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
     279          OK ? 〈lofs,tr〉
    278280      | _ ⇒ Error ?
    279281      ]
    280282  | _ ⇒ Error ?
    281283  ]
    282 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (region × block × int × trace) ≝
     284and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × int × trace) ≝
    283285match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    284286
     
    323325      | cons v1 vl ⇒
    324326          do b ← opt_to_res ? (get … id e);
    325           do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);
     327          do m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);
    326328          exec_bind_parameters e m1 params' vl
    327329      ]
     
    495497definition store_value_of_type' ≝
    496498λty,m,l,v.
    497 match l with [ pair pl ofs ⇒
    498   match pl with [ pair pcl loc ⇒
    499     store_value_of_type ty m pcl loc ofs v ] ].
     499match l with [ pair loc ofs ⇒
     500  store_value_of_type ty m loc ofs v ].
    500501
    501502let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
     
    518519         | Some lhs' ⇒
    519520           ! locofs ← exec_lvalue ge e m lhs';
    520            ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
     521           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
    521522         ];
    522523    ret ? 〈E0, Callstate fd vargs k' m〉)
Note: See TracChangeset for help on using the changeset viewer.