Changeset 888


Ignore:
Timestamp:
Jun 6, 2011, 4:28:07 PM (9 years ago)
Author:
campbell
Message:

Use simplified conditionals in RTLabs, following the prototype.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r887 r888  
    111111    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
    112112    do f ← add_expr env ? e1 dst f;
    113     add_branch_internal env ? e' (f_entry f) lfalse f (add_expr env ? e')
     113    do 〈r,f〉 ← choose_reg env ? e' f;
     114    do f ← add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f;
     115    add_expr env ? e' r f
    114116| Ecost _ l e' ⇒
    115117    do f ← add_expr env ? e' dst f;
    116118    add_fresh_to_graph (St_cost l) f
    117    
    118 (* Ugh, the termination checker isn't smart enough to notice that calling
    119    add_expr with e is OK, so we take it partially applied and define a proper
    120    add_<whatever> afterwards. *)
    121 ]
    122 and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (f:internal_function)
    123         (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝
    124 match e with
    125 [ Id _ i ⇒
    126     do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    127     add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
    128 | Cst _ c ⇒
    129     add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    130 | Op1 _ _ op e' ⇒
    131     do 〈r,f〉 ← choose_reg env ? e' f;
    132     do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
    133     add_expr env ? e' r f
    134 | Op2 _ _ _ op e1 e2 ⇒
    135     do 〈r1,f〉 ← choose_reg env ? e1 f;
    136     do 〈r2,f〉 ← choose_reg env ? e2 f;
    137     do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
    138     do f ← add_expr env ? e2 r2 f;
    139     add_expr env ? e1 r1 f
    140 | _ ⇒
    141     do 〈r,f〉 ← choose_reg env ? e f;
    142     do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
    143     termination_hack_add_expr r f
    144 ].
    145 
    146 (* See comment above. *)
    147 definition add_branch ≝
    148 λenv,ty,e,ltrue,lfalse,f. add_branch_internal env ty e ltrue lfalse f (add_expr env ty e).
     119].
    149120
    150121(* This shouldn't occur; maybe use vectors? *)
     
    214185    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
    215186    do f ← add_stmt env label_env s1 exits f;
    216     add_branch env ? e (f_entry f) l2 f
     187    do 〈r,f〉 ← choose_reg env ? e f;
     188    do f ← add_fresh_to_graph (λl1. St_cond r l1 l2) f;
     189    add_expr env ? e r f
    217190| St_loop s ⇒
    218191    do f ← add_loop_label_to_graph f;
     
    233206      let 〈i,n〉 ≝ cs in
    234207      do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);
     208      do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned);
    235209      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    236       do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
     210      do f ← add_fresh_to_graph (St_cond br l_case) f;
     211      do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
    237212      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
    238213    add_expr env ? e r f
  • src/RTLabs/semantics.ma

    r887 r888  
    140140      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    141141
    142   | St_condcst cst ltrue lfalse ⇒
    143       ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
     142  | St_cond src ltrue lfalse ⇒
     143      ! v ← reg_retrieve (locals f) src;
    144144      ! b ← eval_bool_of_val v;
    145       ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    146   | St_cond1 op src ltrue lfalse ⇒
    147       ! v ← reg_retrieve (locals f) src;
    148       ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
    149       ! b ← eval_bool_of_val v';
    150       ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    151   | St_cond2 op src1 src2 ltrue lfalse ⇒
    152       ! v1 ← reg_retrieve (locals f) src1;
    153       ! v2 ← reg_retrieve (locals f) src2;
    154       ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    155       ! b ← eval_bool_of_val v';
    156145      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    157146
  • src/RTLabs/syntax.ma

    r887 r888  
    2424| St_tailcall_id : ident → list register → statement
    2525| St_tailcall_ptr : register → list register → statement
    26 (* Um, what? *)
    27 | St_condcst : constant → label → label → statement
    28 | St_cond1 : unary_operation → register → label → label → statement
    29 | St_cond2 : binary_operation → register → register → label → label → statement
     26| St_cond : register → label → label → statement
    3027| St_jumptable : register → list label → statement
    3128| St_return : statement
Note: See TracChangeset for help on using the changeset viewer.