Ignore:
Timestamp:
Jul 19, 2011, 12:39:01 PM (8 years ago)
Author:
campbell
Message:

Implement stack allocation for parameters whose address is taken.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r962 r1078  
    177177                           then 〈Stack stack_high,stack_high + sizeof ty〉
    178178                           else 〈Local, stack_high〉 in
    179       〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_vars f) in
     179      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
    180180  〈m,stacksize〉.
    181181
     
    538538      [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
    539539      | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
    540       | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *)
     540      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
    541541      ]
    542542  | Ederef e1 ⇒
     
    724724].
    725725
     726axiom ParamGlobalMixup : String.
     727
     728definition alloc_params : var_types → list (ident×type) → stmt → res stmt ≝
     729λvars,params,s. foldl ?? (λs,it.
     730  let 〈id,ty〉 ≝ it in
     731  do s ← s;
     732  do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
     733  match t with
     734  [ Local ⇒ OK ? s
     735  | Stack n ⇒
     736      do q ← match access_mode ty with
     737      [ By_value q ⇒ OK ? q
     738      | By_reference r ⇒ OK ? (Mpointer r)
     739      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
     740      ];
     741      OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s)
     742  | Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id]
     743  ]) (OK ? s) params.
    726744
    727745definition bigid1 ≝ an_identifier SymbolTag [[
     
    743761  let tmpp ≝ bigid2 in (* FIXME *)
    744762  do s ← translate_statement vartypes tmp tmpp (fn_body f);
     763  do s ← alloc_params vartypes (fn_params f) s;
    745764  OK ? (mk_internal_function
    746765    (opttyp_of_type (fn_return f))
Note: See TracChangeset for help on using the changeset viewer.