Changeset 880 for src/Cminor
 Timestamp:
 Jun 3, 2011, 5:35:31 PM (10 years ago)
 Location:
 src/Cminor
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/initialisation.ma
r758 r880 5 5 include "common/Globalenvs.ma". 6 6 7 definition init_expr : init_data → option (memory_chunk × expr) ≝ 7 (* XXX having to specify the return type in the match is annoying. *) 8 definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝ 8 9 λinit. 9 match init with10 [ Init_int8 i ⇒ Some ? 〈Mint8unsigned, Cst (Ointconst i)〉11  Init_int16 i ⇒ Some ? 〈Mint16unsigned, Cst (Ointconst i)〉12  Init_int32 i ⇒ Some ? 〈Mint32, Cst (Ointconst i)〉13  Init_float32 f ⇒ Some ? 〈Mfloat32, Cst (Ofloatconst f)〉14  Init_float64 f ⇒ Some ? 〈Mfloat64, Cst (Ofloatconst f)〉10 match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with 11 [ Init_int8 i ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i))) 12  Init_int16 i ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i))) 13  Init_int32 i ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i))) 14  Init_float32 f ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f))) 15  Init_float64 f ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f))) 15 16  Init_space n ⇒ None ? 16  Init_null r ⇒ Some ? 〈Mpointer r, Op1 (Optrofint r) (Cst (Ointconst zero))〉17  Init_addrof r id off ⇒ Some ? 〈Mpointer r, Cst (Oaddrsymbol id off)〉17  Init_null r ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero)))) 18  Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off))) 18 19 ]. 19 20 … … 26 27 [ None ⇒ St_skip 27 28  Some x ⇒ 28 let 〈chunk, e〉 ≝ x in 29 St_store chunk (Cst (Oaddrsymbol id off)) e 29 match x with [ dp chunk e ⇒ 30 St_store ? chunk (Cst ? (Oaddrsymbol id off)) e 31 ] 30 32 ]. 31 33 
src/Cminor/semantics.ma
r879 r880 50 50 axiom FailedLoad : String. 51 51 52 let rec eval_expr (ge:genv) ( e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝52 let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝ 53 53 match e with 54 [ Id i ⇒54 [ Id _ i ⇒ 55 55 do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i); 56 56 OK ? 〈E0, r〉 57  Cst c ⇒57  Cst _ c ⇒ 58 58 do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c); 59 59 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; 62 62 do r ← opt_to_res … (msg FailedOp) (eval_unop op v); 63 63 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; 67 67 do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2); 68 68 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; 71 71 do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v); 72 72 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; 75 75 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; 77 77 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; 80 80 OK ? 〈Echarge l ⧺ tr, r〉 81 81 ]. … … 113 113  Some sk ⇒ Some ? sk 114 114 ] 115  St_ifthenelse _ s1 s2 ⇒115  St_ifthenelse _ _ _ s1 s2 ⇒ 116 116 match find_label l s1 k with 117 117 [ None ⇒ find_label l s2 k … … 165 165  Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉 166 166 ] 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; 169 169 ! en' ← update ?? en id v; 170 170 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; 174 174 ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v); 175 175 ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉 176 176 177 177  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; 179 179 ! 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; 181 181 ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉 182 182  St_tailcall ef args ⇒ 183 ! 〈tr,vf〉 ← eval_expr ge ef en sp m;183 ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m; 184 184 ! 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; 186 186 ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉 187 187 188 188  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; 191 191 ! b ← eval_bool_of_val v; 192 192 ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉 … … 196 196 ! k' ← k_exit n k; 197 197 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; 200 200 match v with 201 201 [ Vint i ⇒ … … 208 208 [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉 209 209  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 ] 212 214 ] 213 215  St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉 
src/Cminor/syntax.ma
r878 r880 3 3 include "common/CostLabel.ma". 4 4 5 inductive expr : Type[0] ≝ 6  Id : ident → expr 7  Cst : constant → expr 8  Op1 : unary_operation → expr → expr 9  Op2 : binary_operation → expr → expr → expr 10  Mem : memory_chunk → expr → expr 11  Cond : expr → expr → expr → expr 12  Ecost : costlabel → expr → expr. 5 (* TODO: consider making the typing stricter. *) 6 7 inductive expr : typ → Type[0] ≝ 8  Id : ∀t. ident → expr t 9  Cst : ∀t. constant → expr t 10  Op1 : ∀t,t'. unary_operation → expr t → expr t' 11  Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t' 12  Mem : ∀t. memory_chunk → expr (ASTptr Any) → expr t 13  Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t 14  Ecost : ∀t. costlabel → expr t → expr t. 13 15 14 16 inductive stmt : Type[0] ≝ 15 17  St_skip : stmt 16  St_assign : ident → expr→ stmt17  St_store : memory_chunk → expr → expr→ stmt18  St_assign : ∀t. ident → expr t → stmt 19  St_store : ∀t. memory_chunk → expr (ASTptr Any) → expr t → stmt 18 20 (* ident for returned value, expression to identify fn, args. *) 19  St_call : option ident → expr → list expr→ stmt20  St_tailcall : expr → list expr→ stmt21  St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt 22  St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt 21 23  St_seq : stmt → stmt → stmt 22  St_ifthenelse : expr→ stmt → stmt → stmt24  St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt 23 25  St_loop : stmt → stmt 24 26  St_block : stmt → stmt 25 27  St_exit : nat → stmt 26 28 (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *) 27  St_switch : expr→ list (int × nat) → nat → stmt28  St_return : option expr→ stmt29  St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt 30  St_return : option (Σt. expr t) → stmt 29 31  St_label : ident → stmt → stmt 30 32  St_goto : ident → stmt 
src/Cminor/toRTLabs.ma
r816 r880 67 67 (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 68 68 69 let rec expr_yields_pointer ( e:expr) (ptrs:list ident): bool ≝69 let rec expr_yields_pointer (ty:typ) (e:expr ty) (ptrs:list ident) on e : bool ≝ 70 70 match e with 71 [ Id i ⇒ exists ? (eq_identifier ? i) ptrs72  Cst c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true  Oaddrstack _ ⇒ true  _ ⇒ false ]73  Op1 op e' ⇒71 [ Id _ i ⇒ exists ? (eq_identifier ? i) ptrs 72  Cst _ c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true  Oaddrstack _ ⇒ true  _ ⇒ false ] 73  Op1 _ _ op e' ⇒ 74 74 match op with 75 [ Oid ⇒ expr_yields_pointer e' ptrs75 [ Oid ⇒ expr_yields_pointer ? e' ptrs 76 76  Optrofint _ ⇒ true 77 77  _ ⇒ false 78 78 ] 79  Op2 op e1 e2 ⇒79  Op2 _ _ _ op e1 e2 ⇒ 80 80 match op with 81 81 [ Oaddp ⇒ true … … 83 83  _ ⇒ false 84 84 ] 85  Mem q e' ⇒85  Mem _ q e' ⇒ 86 86 match q with 87 87 [ Mpointer _ ⇒ true … … 89 89 ] 90 90 (* Both branches ought to be the same? *) 91  Cond e' e1 e2 ⇒ (expr_yields_pointer e1 ptrs) ∨ (expr_yields_pointere2 ptrs)92  Ecost _ e' ⇒ expr_yields_pointere' ptrs91  Cond _ _ _ e' e1 e2 ⇒ (expr_yields_pointer ? e1 ptrs) ∨ (expr_yields_pointer ? e2 ptrs) 92  Ecost _ _ e' ⇒ expr_yields_pointer ? e' ptrs 93 93 ]. 94 94 95 95 axiom UnknownVariable : String. 96 96 97 definition choose_reg : env → expr→ list ident → internal_function → res (register × internal_function) ≝98 λenv, e,ptrs,f.97 definition choose_reg : env → ∀t.expr t → list ident → internal_function → res (register × internal_function) ≝ 98 λenv,ty,e,ptrs,f. 99 99 match e with 100 [ Id i ⇒100 [ Id _ i ⇒ 101 101 do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i); 102 102 OK ? 〈r, f〉 103 103  _ ⇒ 104 if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f104 if expr_yields_pointer ? e ptrs then fresh_ptr_reg f else fresh_reg f 105 105 ]. 106 106 107 definition choose_regs : env → list expr→ list ident → internal_function → res (list register × internal_function) ≝107 definition choose_regs : env → list (Σt:typ.expr t) → list ident → internal_function → res (list register × internal_function) ≝ 108 108 λenv,es,ptrs,f. 109 foldr ?? (λe,acc. do 〈rs,f〉 ← acc; 110 do 〈r,f'〉 ← choose_reg env e ptrs f; 111 OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. 109 foldr (Σt:typ.expr t) ? 110 (λe,acc. do 〈rs,f〉 ← acc; 111 do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e ptrs f ]; 112 OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. 112 113 113 114 axiom BadCminorProgram : String. 114 115 115 let rec add_expr (env:env) ( e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝116 let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝ 116 117 match e with 117 [ Id i ⇒118 [ Id _ i ⇒ 118 119 do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i); 119 120 match register_eq r dst with … … 121 122  inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f 122 123 ] 123  Cst c ⇒ add_fresh_to_graph (St_const dst c) f124  Op1 op e' ⇒125 do 〈r,f〉 ← choose_reg env e' ptrs f;124  Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f 125  Op1 _ _ op e' ⇒ 126 do 〈r,f〉 ← choose_reg env ? e' ptrs f; 126 127 do f ← add_fresh_to_graph (St_op1 op dst r) f; 127 add_expr env e' r ptrs f128  Op2 op e1 e2 ⇒129 do 〈r1,f〉 ← choose_reg env e1 ptrs f;130 do 〈r2,f〉 ← choose_reg env e2 ptrs f;128 add_expr env ? e' r ptrs f 129  Op2 _ _ _ op e1 e2 ⇒ 130 do 〈r1,f〉 ← choose_reg env ? e1 ptrs f; 131 do 〈r2,f〉 ← choose_reg env ? e2 ptrs f; 131 132 do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f; 132 do f ← add_expr env e2 r2 ptrs f;133 add_expr env e1 r1 ptrs f134  Mem q e' ⇒135 add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr enve')136  Cond e' e1 e2 ⇒133 do f ← add_expr env ? e2 r2 ptrs f; 134 add_expr env ? e1 r1 ptrs f 135  Mem _ q e' ⇒ 136 add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e') 137  Cond _ _ _ e' e1 e2 ⇒ 137 138 let resume_at ≝ f_entry f in 138 do f ← add_expr env e2 dst ptrs f;139 do f ← add_expr env ? e2 dst ptrs f; 139 140 let lfalse ≝ f_entry f in 140 141 do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; 141 do f ← add_expr env e1 dst ptrs f;142 add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr enve')143  Ecost l e' ⇒144 do f ← add_expr env e' dst ptrs f;142 do f ← add_expr env ? e1 dst ptrs f; 143 add_branch_internal env ? e' (f_entry f) lfalse ptrs f (add_expr env ? e') 144  Ecost _ l e' ⇒ 145 do f ← add_expr env ? e' dst ptrs f; 145 146 add_fresh_to_graph (St_cost l) f 146 147 … … 149 150 add_<whatever> afterwards. *) 150 151 ] 151 and add_with_addressing_internal (env:env) ( e:expr)152 and add_with_addressing_internal (env:env) (ty:typ) (e:expr ty) 152 153 (s:∀m:addressing. addr m → label → statement) 153 154 (ptrs:list ident) … … 156 157 on e : res internal_function ≝ 157 158 let add_default : unit → res internal_function ≝ λ_. 158 do 〈r, f〉 ← choose_reg env e ptrs f;159 do 〈r, f〉 ← choose_reg env ? e ptrs f; 159 160 do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f; 160 161 termination_hack r ptrs f 161 162 in 162 163 match e with 163 [ Cst c ⇒164 [ Cst _ c ⇒ 164 165 match c with 165 166 [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f … … 167 168  _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *) 168 169 ] 169  Op2 op e1 e2 ⇒170  Op2 _ _ _ op e1 e2 ⇒ 170 171 match op with 171 172 [ Oaddp ⇒ 172 173 let add_generic_addp : unit → res internal_function ≝ λ_. 173 do 〈r1, f〉 ← choose_reg env e1 ptrs f;174 do 〈r2, f〉 ← choose_reg env e2 ptrs f;174 do 〈r1, f〉 ← choose_reg env ? e1 ptrs f; 175 do 〈r2, f〉 ← choose_reg env ? e2 ptrs f; 175 176 do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f; 176 do f ← add_expr env e2 r2 ptrs f;177 add_expr env e1 r1 ptrs f177 do f ← add_expr env ? e2 r2 ptrs f; 178 add_expr env ? e1 r1 ptrs f 178 179 in 179 180 match e1 with 180 [ Cst c ⇒181 [ Cst _ c ⇒ 181 182 match c with 182 183 [ Oaddrsymbol id i ⇒ 183 do 〈r, f〉 ← choose_reg env e ptrs f;184 do 〈r, f〉 ← choose_reg env ? e ptrs f; 184 185 do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f; 185 add_expr env e2 r ptrs f186 add_expr env ? e2 r ptrs f 186 187  _ ⇒ add_generic_addp it 187 188 ] … … 193 194 ] 194 195 (* and again *) 195 and add_branch_internal (env:env) ( e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)196 and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function) 196 197 (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝ 197 198 match e with 198 [ Id i ⇒199 [ Id _ i ⇒ 199 200 do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i); 200 201 add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f 201  Cst c ⇒202  Cst _ c ⇒ 202 203 add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f 203  Op1 op e' ⇒204 do 〈r,f〉 ← choose_reg env e' ptrs f;204  Op1 _ _ op e' ⇒ 205 do 〈r,f〉 ← choose_reg env ? e' ptrs f; 205 206 do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f; 206 add_expr env e' r ptrs f207  Op2 op e1 e2 ⇒208 do 〈r1,f〉 ← choose_reg env e1 ptrs f;209 do 〈r2,f〉 ← choose_reg env e2 ptrs f;207 add_expr env ? e' r ptrs f 208  Op2 _ _ _ op e1 e2 ⇒ 209 do 〈r1,f〉 ← choose_reg env ? e1 ptrs f; 210 do 〈r2,f〉 ← choose_reg env ? e2 ptrs f; 210 211 do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f; 211 do f ← add_expr env e2 r2 ptrs f;212 add_expr env e1 r1 ptrs f212 do f ← add_expr env ? e2 r2 ptrs f; 213 add_expr env ? e1 r1 ptrs f 213 214  _ ⇒ 214 do 〈r,f〉 ← choose_reg env e ptrs f;215 do 〈r,f〉 ← choose_reg env ? e ptrs f; 215 216 do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f; 216 217 termination_hack_add_expr r ptrs f … … 219 220 (* See comment above. *) 220 221 definition add_with_addressing ≝ 221 λenv, e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr enve).222 λenv,ty,e,s,ptrs,f. add_with_addressing_internal env ty e s ptrs f (add_expr env ty e). 222 223 definition add_branch ≝ 223 λenv, e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr enve).224 λenv,ty,e,ltrue,lfalse,ptrs,f. add_branch_internal env ty e ltrue lfalse ptrs f (add_expr env ty e). 224 225 225 226 (* This shouldn't occur; maybe use vectors? *) 226 227 axiom WrongNumberOfArguments : String. 227 228 228 let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝229 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝ 229 230 match es with 230 231 [ nil ⇒ match dsts with [ nil ⇒ OK ? f  cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ] … … 234 235  cons r rt ⇒ 235 236 do f ← add_exprs env et rt ptrs f; 236 add_expr env e r ptrs f237 match e with [ dp ty e ⇒ add_expr env ty e r ptrs f ] 237 238 ] 238 239 ]. … … 244 245 match s with 245 246 [ St_skip ⇒ OK ? f 246  St_assign x e ⇒247  St_assign _ x e ⇒ 247 248 do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x); 248 add_expr env e dst ptrs f249  St_store q e1 e2 ⇒250 do 〈val_reg, f〉 ← choose_reg env e2 ptrs f;251 do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;252 add_expr env e2 val_reg ptrs f249 add_expr env ? e dst ptrs f 250  St_store _ q e1 e2 ⇒ 251 do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f; 252 do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f; 253 add_expr env ? e2 val_reg ptrs f 253 254  St_call return_opt_id e args ⇒ 254 255 do return_opt_reg ← … … 260 261 do f ← 261 262 match e with 262 [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f263 [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f 263 264  _ ⇒ 264 do 〈fnr, f〉 ← choose_reg env e ptrs f;265 do 〈fnr, f〉 ← choose_reg env ? e ptrs f; 265 266 do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f; 266 add_expr env e fnr ptrs f267 add_expr env ? e fnr ptrs f 267 268 ]; 268 269 add_exprs env args args_regs ptrs f … … 271 272 do f ← 272 273 match e with 273 [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f274 [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f 274 275  _ ⇒ 275 do 〈fnr, f〉 ← choose_reg env e ptrs f;276 do 〈fnr, f〉 ← choose_reg env ? e ptrs f; 276 277 do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f; 277 add_expr env e fnr ptrs f278 add_expr env ? e fnr ptrs f 278 279 ]; 279 280 add_exprs env args args_regs ptrs f … … 281 282 do f ← add_stmt env label_env s2 exits ptrs f; 282 283 add_stmt env label_env s1 exits ptrs f 283  St_ifthenelse e s1 s2 ⇒284  St_ifthenelse _ _ e s1 s2 ⇒ 284 285 let l_next ≝ f_entry f in 285 286 do f ← add_stmt env label_env s2 exits ptrs f; … … 287 288 do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; 288 289 do f ← add_stmt env label_env s1 exits ptrs f; 289 add_branch env e (f_entry f) l2 ptrs f290 add_branch env ? e (f_entry f) l2 ptrs f 290 291  St_loop s ⇒ 291 292 do f ← add_loop_label_to_graph f; … … 298 299 do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 299 300 add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f 300  St_switch e tab n ⇒301 do 〈r,f〉 ← choose_reg env e ptrs f;301  St_switch _ _ e tab n ⇒ 302 do 〈r,f〉 ← choose_reg env ? e ptrs f; 302 303 do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); 303 304 do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f; … … 309 310 do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f; 310 311 add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab; 311 add_expr env e r ptrs f312 add_expr env ? e r ptrs f 312 313  St_return opt_e ⇒ 313 314 do f ← add_fresh_to_graph (λ_. St_return) f; … … 317 318 match f_result f with 318 319 [ None ⇒ Error ? (msg ReturnMismatch) 319  Some r ⇒ add_expr env e r ptrs f320  Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e r ptrs f ] 320 321 ] 321 322 ] … … 343 344 match s with 344 345 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 345  St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)346  St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 346 347  St_loop s ⇒ labels_of s 347 348  St_block s ⇒ labels_of s
Note: See TracChangeset
for help on using the changeset viewer.