Changeset 125 for C-semantics/CexecIO.ma


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

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r124 r125  
    223223    p ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
    224224    s' ← match ty' with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];:
    225     if is_class_compat (blockclass m b) (ptr_spc_cls s')
    226     then OK ? (Vptr (ptr_spc_cls s') b ofs)
     225    if is_pointer_compat (block_space m b) s'
     226    then OK ? (Vptr s' b ofs)
    227227    else Error ?)
    228228  (* XXX: maybe should allow some Tint? *)
     
    239239          nwhd in e:(??%?); ndestruct; //;
    240240      ##| #Hty' Hty;
    241           nwhd in match (is_class_compat ??) in ⊢ %;
    242           ncases (class_compat_dec (blockclass m c1) (ptr_spc_cls s')); #Hcompat;
     241          nwhd in match (is_pointer_compat ??) in ⊢ %;
     242          ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat;
    243243          nwhd; /2/;
    244244      ##]
     
    247247
    248248ndefinition load_value_of_type' ≝
    249 λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒
    250   load_value_of_type ty m pcl loc ofs ] ].
     249λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒
     250  load_value_of_type ty m psp loc ofs ] ].
    251251
    252252(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    305305  ]
    306306]
    307 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:ptr_class × block × int. eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
     307and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int. eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
    308308  match e' with
    309309  [ Evar id ⇒
    310310      match (get … id en) with
    311       [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈Universal (* XXX *),l〉,zero〉) (* global *)
    312       | Some bl ⇒ match bl with [ mk_pair bcl loc ⇒ Some ? (OK ? 〈〈blk_ptr_cls bcl,loc〉,zero〉) ] (* local *)
     311      [ None ⇒ Some ? (〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈sp,l〉,zero〉) (* global *)
     312      | Some loc ⇒ Some ? (OK ? 〈〈Any,loc〉,zero〉) (* local *)
    313313      ]
    314314  | Ederef a ⇒ Some ? (
    315315      v ← exec_expr ge en m a;:
    316316      match v with
    317       [ Vptr pcl l ofs ⇒ OK ? 〈〈pcl,l〉,ofs〉
     317      [ Vptr sp l ofs ⇒ OK ? 〈〈sp,l〉,ofs〉
    318318      | _ ⇒ Error ?
    319319      ])
     
    331331  | _ ⇒ Some ? (Error ?)
    332332  ]
    333 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:ptr_class × block × int. eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
     333and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int. eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
    334334match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    335335nwhd;
    336 ##[ //
    337 ##| //
     336##[ ##1,2: //
    338337##| ##3,4:
    339     napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #pcl loc ofs H;
     338    napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs H;
    340339    napply opt_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
    341 ##| napply sig_bind2_OK; #x; ncases x; #pcl loc ofs H;
     340##| napply sig_bind2_OK; #x; ncases x; #sp loc ofs H;
    342341    nwhd; napply eval_Eaddrof; //;
    343342##| napply sig_bind_OK; #v1 Hv1;
     
    374373    ##]
    375374##| //
    376 ##| napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #pcl l ofs H;
     375##| napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs H;
    377376    napply opt_OK; #v ev; napply (eval_Elvalue … H ev);
    378377##| //
    379378##| //
    380 ##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
    381 ##| napply eval_Evar_local; nrewrite < c6; /2/
    382 ##| napply sig_bind_OK; #v; ncases v; //; #pcl l ofs Hv; nwhd;
     379##| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/;
     380##| napply (eval_Evar_local … c3);
     381##| napply sig_bind_OK; #v; ncases v; //; #sp l ofs Hv; nwhd;
    383382    napply eval_Ederef; //
    384383##| ##19,20,21,22,23,24,25,26,27,28,29,30,31,32: //
    385 ##| napply sig_bind2_OK; #x; ncases x; #pcl l ofs H;
     384##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    386385    napply bind_OK; #delta Hdelta;
    387386    napply (eval_Efield_struct … H c5 Hdelta);
    388 ##| napply sig_bind2_OK; #x; ncases x; #pcl l ofs H;
     387##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    389388    napply (eval_Efield_union … H c5);
    390389##| //
     
    414413| cons h vars ⇒
    415414  match h with [ mk_pair id ty ⇒
    416     match alloc m 0 (sizeof ty) UnspecifiedB with [ mk_pair m1 b1 ⇒
    417       match exec_alloc_variables (set … id 〈UnspecifiedB,b1〉 en) m1 vars with
     415    match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒
     416      match exec_alloc_variables (set … id b1 en) m1 vars with
    418417      [ sig_intro r p ⇒ r ]
    419 ]]]. nwhd; //;
    420 nelim (exec_alloc_variables (set ident ? ? c3 〈UnspecifiedB,c7〉 en) c6 c1);
    421 #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
     418]]]. nwhd;
     419##[ //;
     420##| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1);
     421    #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
    422422napply (alloc_variables_cons … IH); /2/;
    423423nqed.
     
    431431      [ nil ⇒ Some ? (Error ?)
    432432      | cons v1 vl ⇒ Some ? (
    433           〈bcl,b〉 ← opt_to_res ? (get … id e);:
    434           m1 ← opt_to_res ? (store_value_of_type ty m (blk_ptr_cls bcl) b zero v1);:
     433          b ← opt_to_res ? (get … id e);:
     434          m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);:
    435435          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
    436436      ]
    437437  ] ].
    438438nwhd; //;
    439 napply opt_bind_OK; #x; ncases x; #bcl b eb;
     439napply opt_bind_OK; #b eb;
    440440napply opt_bind_OK; #m1 em1;
    441441napply reinject; #m2 em2 Hm2;
     
    474474ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    475475#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    476 ndefinition ms_eq_dec : ∀s1,s2:mem_space. (s1 = s2) + (s1 ≠ s2).
     476ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
    477477#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    478478
     
    823823  let m0 ≝ init_mem Genv ?? p in
    824824  Some ? (
    825     ! b ← find_symbol ? ? ge (prog_main ?? p);:
     825    ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p);:
     826    ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);:
    826827    ! f ← find_funct_ptr ? ? ge b;:
    827828    ret ? (Callstate f (nil ?) Kstop m0)).
    828829nwhd;
    829 napply opt_bindIO_OK; #b eb;
     830napply opt_bindIO2_OK; #sp b esb;
     831napply opt_bindIO_OK; #u ecode;
    830832napply opt_bindIO_OK; #f ef;
    831 nwhd; napply (initial_state_intro … eb ef);
     833ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4: ndestruct (ecode); ##]
     834nwhd; napply (initial_state_intro … esb ef);
    832835nqed.
    833836
Note: See TracChangeset for help on using the changeset viewer.