Changeset 881 for src/Cminor


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

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

Location:
src/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r880 r881  
    2222   away. *)
    2323
    24 definition init_datum : ident → init_data → int (*offset?*) → stmt ≝
    25 λid,init,off.
     24definition init_datum : ident → region → init_data → int (*offset?*) → stmt ≝
     25λid,r,init,off.
    2626match init_expr init with
    2727[ None ⇒ St_skip
    2828| Some x ⇒
    2929    match x with [ dp chunk e ⇒
    30       St_store ? chunk (Cst ? (Oaddrsymbol id off)) e
     30      St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
    3131    ]
    3232].
    3333
    34 definition init_var : ident → list init_data → stmt ≝
    35 λid,init.
     34definition init_var : ident → region → list init_data → stmt ≝
     35λid,r,init.
    3636\snd (foldr ??
    3737  (λdatum,os.
    3838   let 〈off,s〉 ≝ os in
    39      〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id datum off) s〉)
     39     〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id r datum off) s〉)
    4040  〈zero, St_skip〉 init).
    4141
    4242definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
    4343λvars. foldr ??
    44   (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst (\fst var))))) St_skip vars.
     44  (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars.
    4545
    4646definition add_statement : ident → stmt →
  • src/Cminor/semantics.ma

    r880 r881  
    6767    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    6868    OK ? 〈tr1 ⧺ tr2, r〉
    69 | Mem ty chunk e ⇒
     69| Mem rg ty chunk e ⇒
    7070    do 〈tr,v〉 ← eval_expr ge ? e en sp m;
    7171    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
     
    169169        ! en' ← update ?? en id v;
    170170        ret ? 〈tr, State f St_skip en' m sp k〉
    171     | St_store _ chunk edst e ⇒
     171    | St_store _ _ chunk edst e ⇒
    172172        ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
    173173        ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
  • src/Cminor/syntax.ma

    r880 r881  
    1010| Op1 : ∀t,t'. unary_operation → expr t → expr t'
    1111| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
    12 | Mem : ∀t. memory_chunk → expr (ASTptr Any) → expr t
     12| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
    1313| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1414| Ecost : ∀t. costlabel → expr t → expr t.
     
    1717| St_skip : stmt
    1818| St_assign : ∀t. ident → expr t → stmt
    19 | St_store : ∀t. memory_chunk → expr (ASTptr Any) → expr t → stmt
     19| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
    2020(* ident for returned value, expression to identify fn, args. *)
    2121| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
  • src/Cminor/toRTLabs.ma

    r880 r881  
    8383    | _ ⇒ false
    8484    ]
    85 | Mem _ q e' ⇒
     85| Mem _ _ q e' ⇒
    8686    match q with
    8787    [ Mpointer _ ⇒ true
     
    133133    do f ← add_expr env ? e2 r2 ptrs f;
    134134    add_expr env ? e1 r1 ptrs f
    135 | Mem _ q e' ⇒
     135| Mem _ _ q e' ⇒
    136136    add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e')
    137137| Cond _ _ _ e' e1 e2 ⇒
     
    248248    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    249249    add_expr env ? e dst ptrs f
    250 | St_store _ q e1 e2 ⇒
     250| St_store _ _ q e1 e2 ⇒
    251251    do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f;
    252252    do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f;
Note: See TracChangeset for help on using the changeset viewer.