Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (8 years ago)
Author:
campbell
Message:

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r879 r880  
    5050axiom FailedLoad : String.
    5151
    52 let rec eval_expr (ge:genv) (e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
     52let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
    5353match e with
    54 [ Id i ⇒
     54[ Id _ i ⇒
    5555    do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i);
    5656    OK ? 〈E0, r〉
    57 | Cst c ⇒
     57| Cst _ c ⇒
    5858    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    5959    OK ? 〈E0, r〉
    60 | Op1 op e' ⇒
    61     do 〈tr,v〉 ← eval_expr ge e' en sp m;
     60| Op1 ty ty' op e' ⇒
     61    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    6262    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
    6363    OK ? 〈tr, r〉
    64 | Op2 op e1 e2 ⇒
    65     do 〈tr1,v1〉 ← eval_expr ge e1 en sp m;
    66     do 〈tr2,v2〉 ← eval_expr ge e2 en sp m;
     64| Op2 ty1 ty2 ty' op e1 e2 ⇒
     65    do 〈tr1,v1〉 ← eval_expr ge ? e1 en sp m;
     66    do 〈tr2,v2〉 ← eval_expr ge ? e2 en sp m;
    6767    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    6868    OK ? 〈tr1 ⧺ tr2, r〉
    69 | Mem chunk e ⇒
    70     do 〈tr,v〉 ← eval_expr ge e en sp m;
     69| Mem ty chunk e ⇒
     70    do 〈tr,v〉 ← eval_expr ge ? e en sp m;
    7171    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    7272    OK ? 〈tr, r〉
    73 | Cond e' e1 e2 ⇒
    74     do 〈tr,v〉 ← eval_expr ge e' en sp m;
     73| Cond sz sg ty e' e1 e2 ⇒
     74    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    7575    do b ← eval_bool_of_val v;
    76     do 〈tr',r〉 ← eval_expr ge (if b then e1 else e2) en sp m;
     76    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en sp m;
    7777    OK ? 〈tr ⧺ tr', r〉
    78 | Ecost l e' ⇒
    79     do 〈tr,r〉 ← eval_expr ge e' en sp m;
     78| Ecost ty l e' ⇒
     79    do 〈tr,r〉 ← eval_expr ge ty e' en sp m;
    8080    OK ? 〈Echarge l ⧺ tr, r〉
    8181].
     
    113113    | Some sk ⇒ Some ? sk
    114114    ]
    115 | St_ifthenelse _ s1 s2 ⇒
     115| St_ifthenelse _ _ _ s1 s2 ⇒
    116116    match find_label l s1 k with
    117117    [ None ⇒ find_label l s2 k
     
    165165        | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉
    166166        ]
    167     | St_assign id e ⇒
    168         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     167    | St_assign _ id e ⇒
     168        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    169169        ! en' ← update ?? en id v;
    170170        ret ? 〈tr, State f St_skip en' m sp k〉
    171     | St_store chunk edst e ⇒
    172         ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
    173         ! 〈tr',v〉 ← eval_expr ge e en sp m;
     171    | St_store _ chunk edst e ⇒
     172        ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
     173        ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
    174174        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    175175        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
    176176
    177177    | St_call dst ef args ⇒
    178         ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
     178        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
    179179        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    180         ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
     180        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    181181        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    182182    | St_tailcall ef args ⇒
    183         ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
     183        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
    184184        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    185         ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
     185        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    186186        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉
    187187       
    188188    | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
    189     | St_ifthenelse e strue sfalse ⇒
    190         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     189    | St_ifthenelse _ _ e strue sfalse ⇒
     190        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    191191        ! b ← eval_bool_of_val v;
    192192        ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
     
    196196        ! k' ← k_exit n k;
    197197        ret ? 〈E0, State f St_skip en m sp k'〉
    198     | St_switch e cs default ⇒
    199         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     198    | St_switch _ _ e cs default ⇒
     199        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    200200        match v with
    201201        [ Vint i ⇒
     
    208208        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
    209209        | Some e ⇒
    210             ! 〈tr,v〉 ← eval_expr ge e en sp m;
    211             ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
     210            match e with [ dp ty e ⇒
     211              ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
     212              ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
     213            ]
    212214        ]
    213215    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
Note: See TracChangeset for help on using the changeset viewer.