Changeset 818 for Deliverables/D2.2/8051/src/clight/clightToCminor.ml
 Timestamp:
 May 19, 2011, 4:03:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051/src/clight/clightToCminor.ml
r740 r818 1 open AST 2 open Cminor 3 open Clight 4 5 6 let error_prefix = "Cminor to RTLabs" 1 2 3 let error_prefix = "Clight to Cminor" 7 4 let error = Error.global_error error_prefix 8 5 let error_float () = error "float not supported." 9 6 10 7 11 (*For internal use*) 12 type var_type = 8 (* General helpers *) 9 10 let clight_type_of (Clight.Expr (_, t)) = t 11 12 let cminor_type_of (Cminor.Expr (_, t)) = t 13 14 15 (* Translate types *) 16 17 let byte_size_of_intsize = function 18  Clight.I8 > 1 19  Clight.I16 > 2 20  Clight.I32 > 4 21 22 let sig_type_of_ctype = function 23  Clight.Tvoid > assert false (* do not use on this argument *) 24  Clight.Tint (intsize, sign) > 25 AST.Sig_int (byte_size_of_intsize intsize, sign) 26  Clight.Tfloat _ > error_float () 27  Clight.Tfunction _  Clight.Tstruct _  Clight.Tunion _ 28  Clight.Tpointer _  Clight.Tarray _  Clight.Tcomp_ptr _ > AST.Sig_ptr 29 30 let translate_args_types = List.map sig_type_of_ctype 31 32 let type_return_of_ctype = function 33  Clight.Tvoid > AST.Type_void 34  t > AST.Type_ret (sig_type_of_ctype t) 35 36 let quantity_of_sig_type = function 37  AST.Sig_int (size, _) > AST.QInt size 38  AST.Sig_float _ > error_float () 39  AST.Sig_offset > AST.QOffset 40  AST.Sig_ptr > AST.QPtr 41 42 let quantity_of_ctype t = quantity_of_sig_type (sig_type_of_ctype t) 43 44 let rec sizeof_ctype = function 45  Clight.Tvoid  Clight.Tfunction _ > AST.SQ (AST.QInt 1) 46  Clight.Tfloat _ > error_float () 47  Clight.Tint (size, _) > AST.SQ (AST.QInt (byte_size_of_intsize size)) 48  Clight.Tpointer _ 49  Clight.Tcomp_ptr _ > AST.SQ AST.QPtr 50  Clight.Tarray (t, n) > AST.SArray (n, sizeof_ctype t) 51  Clight.Tstruct (_, fields) > 52 AST.SProd (List.map sizeof_ctype (List.map snd fields)) 53  Clight.Tunion (_, fields) > 54 AST.SSum (List.map sizeof_ctype (List.map snd fields)) 55 56 let global_size_of_ctype = sizeof_ctype 57 58 59 (** Helpers on abstract sizes and offsets *) 60 61 let max_stacksize size1 size2 = match size1, size2 with 62  AST.SProd l1, AST.SProd l2 when List.length l1 > List.length l2 > size1 63  AST.SProd l1, AST.SProd l2 > size2 64  _ > raise (Failure "ClightToCminor.max_stacksize") 65 66 (** Hypothesis: [offset1] is a prefix of [offset2] or viceversa. *) 67 let max_offset offset1 offset2 = 68 if List.length offset1 > List.length offset2 then offset1 69 else offset2 70 71 let next_depth = function 72  AST.SProd l > List.length l 73  _ > raise (Failure "ClightToCminor.next_offset") 74 75 let add_stack offset = 76 let e1 = Cminor.Expr (Cminor.Cst AST.Cst_stack, AST.Sig_ptr) in 77 let e2 = Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), AST.Sig_offset) in 78 Cminor.Op2 (AST.Op_addp, e1, e2) 79 80 let add_stacksize t = function 81  AST.SProd l > AST.SProd (l @ [sizeof_ctype t]) 82  _ > raise (Failure "ClightToCminor.add_stacksize") 83 84 let struct_depth field fields = 85 let rec aux i = function 86  [] > error ("unknown field " ^ field ^ ".") 87  (field', t) :: _ when field' = field > i 88  (_, t) :: fields > aux (i+1) fields in 89 aux 0 fields 90 91 let struct_offset t field fields = 92 let size = sizeof_ctype t in 93 let depth = struct_depth field fields in 94 let offset = (size, depth) in 95 let t = AST.Sig_offset in 96 Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), t) 97 98 99 (** Sort variables: locals, parameters, globals, in stack. *) 100 101 type location = 102  Local 103  LocalStack of AST.abstract_offset 104  Param 105  ParamStack of AST.abstract_offset 13 106  Global 14  Stack of int (*Note: this is a constraint on the size of the stack.*) 15  Param 16  Local 17 18 (*Parametrisation by int and pointer size *) 19 let int_size = Driver.CminorMemory.int_size 20 let ptr_size = Driver.CminorMemory.ptr_size 21 let alignment = Driver.CminorMemory.alignment 22 23 let fresh_tmp variables = 24 let rec ft i = 25 let tmp = "tmp"^(string_of_int i) in 26 try (match Hashtbl.find variables tmp with _ > ft (i+1)) 27 with Not_found > tmp 28 in ft 0 29 30 let rec ctype_to_type_return t = match t with 31  Tvoid > Type_void 32  Tfloat _ > Type_ret Sig_float (*Not supported*) 33  Tpointer _  Tarray (_,_)  Tstruct (_,_)  Tunion (_,_) > Type_ret Sig_ptr 34  _ > Type_ret Sig_int 35 36 let rec ctype_to_sig_type t = match t with 37  Tfloat _ > 38 Sig_float (*Not supported but needed for external function from library*) 39  Tvoid > assert false 40  Tpointer _  Tstruct (_,_)  Tunion (_,_)  Tarray(_,_) > Sig_ptr 41  _ > Sig_int 42 43 let rec size_of_ty = function 44  Tvoid > assert false 45  Tfloat _ > assert false (*Not supported*) 46  Tfunction (_,_) > assert false (*Not supported*) 47  Tint (I8,Signed) > 1 48  Tint (I8,Unsigned) > 1 49  Tint (I16,Signed) > 2 50  Tint (I16,Unsigned) > 2 51 (*FIXME MQ_int32 : signed or unsigned ? *) 52  Tint (I32,Signed) > 4 53  Tint (I32,Unsigned) > 4 54  Tpointer _  Tarray (_,_)  Tstruct (_,_)  Tunion (_,_) 55  Tcomp_ptr _ > ptr_size 56 57 let size_of_intsize = function 58  I8 > 1 59  I16 > 2 60  I32 > 4 61 62 let quantity_of_ty = function 63  Tvoid > assert false (* do not use on this argument *) 64  Tint (size,_) > Memory.QInt (size_of_intsize size) 65  Tpointer _  Tarray (_,_)  Tstruct (_,_)  Tunion (_,_) 66  Tfunction (_,_) 67  Tcomp_ptr _ > Memory.QPtr 68  Tfloat _ > error_float () 69 70 let init_to_data l = List.map ( 107 108 (** Below are some helper definitions to ease the manipulation of a translation 109 environment for variables. *) 110 111 type var_locations = (location * Clight.ctype) StringTools.Map.t 112 113 let empty_var_locs : var_locations = StringTools.Map.empty 114 115 let add_var_locs : AST.ident > (location * Clight.ctype) > var_locations > 116 var_locations = 117 StringTools.Map.add 118 119 let mem_var_locs : AST.ident > var_locations > bool = StringTools.Map.mem 120 121 let find_var_locs : AST.ident > var_locations > (location * Clight.ctype) = 122 StringTools.Map.find 123 124 let fold_var_locs : (AST.ident > (location * Clight.ctype) > 'a > 'a) > 125 var_locations > 'a > 'a = 126 StringTools.Map.fold 127 128 129 let is_local_or_param id var_locs = match find_var_locs id var_locs with 130  (Local, _)  (Param, _) > true 131  _ > false 132 133 let get_locals var_locs = 134 let f id (location, ctype) locals = 135 let added = match location with 136  Local > [(id, sig_type_of_ctype ctype)] 137  _ > [] in 138 locals @ added in 139 fold_var_locs f var_locs [] 140 141 let get_stacksize var_locs = 142 let f _ (location, _) res = match location with 143  LocalStack (stacksize, _)  ParamStack (stacksize, _) > 144 max_stacksize res stacksize 145  _ > res in 146 fold_var_locs f var_locs (AST.SProd []) 147 148 149 (* Variables of a function that will go in stack: variables of a complex type 150 (array, structure or union) and variables whose address is evaluated. *) 151 152 let is_function_ctype = function 153  Clight.Tfunction _ > true 154  _ > false 155 156 let is_scalar_ctype : Clight.ctype > bool = function 157  Clight.Tint _  Clight.Tfloat _  Clight.Tpointer _ > true 158  _ > false 159 160 let is_complex_ctype : Clight.ctype > bool = function 161  Clight.Tarray _  Clight.Tstruct _  Clight.Tunion _  Clight.Tfunction _ > 162 true 163  _ > false 164 165 let complex_ctype_vars cfun = 166 let f set (x, t) = 167 if is_complex_ctype t then StringTools.Set.add x set else set in 168 (* Because of CIL, parameters should not have a complex type, but let's add 169 them just in case. *) 170 List.fold_left f StringTools.Set.empty 171 (cfun.Clight.fn_params @ cfun.Clight.fn_vars) 172 173 let union_list = List.fold_left StringTools.Set.union StringTools.Set.empty 174 175 let f_expr (Clight.Expr (ed, _)) sub_exprs_res = 176 let res_ed = match ed with 177  Clight.Eaddrof (Clight.Expr (Clight.Evar id, _)) > 178 StringTools.Set.singleton id 179  _ > StringTools.Set.empty in 180 union_list (res_ed :: sub_exprs_res) 181 182 let f_stmt _ sub_exprs_res sub_stmts_res = 183 union_list (sub_exprs_res @ sub_stmts_res) 184 185 let addr_vars_fun cfun = ClightFold.statement2 f_expr f_stmt cfun.Clight.fn_body 186 187 let stack_vars cfun = 188 StringTools.Set.union (complex_ctype_vars cfun) (addr_vars_fun cfun) 189 190 191 let sort_stacks stack_location vars var_locs = 192 let stacksize = get_stacksize var_locs in 193 let f (current_stacksize, var_locs) (id, t) = 194 let depth = next_depth current_stacksize in 195 let current_stacksize = add_stacksize t current_stacksize in 196 let offset = (current_stacksize, depth) in 197 let var_locs = add_var_locs id (stack_location offset, t) var_locs in 198 (current_stacksize, var_locs) in 199 snd (List.fold_left f (stacksize, var_locs) vars) 200 201 let sort_normals normal_location vars var_locs = 202 let f var_locs (id, ctype) = 203 add_var_locs id (normal_location, ctype) var_locs in 204 List.fold_left f var_locs vars 205 206 let sort_vars normal_location stack_location_opt stack_vars vars var_locs = 207 let f_stack (x, _) = StringTools.Set.mem x stack_vars in 208 let (f_normal, var_locs) = match stack_location_opt with 209  None > ((fun _ > true), var_locs) 210  Some stack_location > 211 ((fun var > not (f_stack var)), 212 sort_stacks stack_location (List.filter f_stack vars) var_locs) in 213 sort_normals normal_location (List.filter f_normal vars) var_locs 214 215 let sort_locals = sort_vars Local (Some (fun offset > LocalStack offset)) 216 217 let sort_params = sort_vars Param (Some (fun offset > ParamStack offset)) 218 219 let sort_globals stack_vars globals var_locs = 220 let globals = List.map (fun ((id, _), ctype) > (id, ctype)) globals in 221 sort_vars Global None stack_vars globals var_locs 222 223 (* The order of insertion in the sorting environment is important: it follows 224 the scope conventions of C. Local variables hide parameters that hide 225 globals. *) 226 227 let sort_variables globals cfun = 228 let stack_vars = stack_vars cfun in 229 let var_locs = empty_var_locs in 230 let var_locs = sort_globals stack_vars globals var_locs in 231 let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in 232 let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in 233 var_locs 234 235 236 (* Translate globals *) 237 238 let init_to_data = function 239  [Clight.Init_space _] > None 240  l > Some (List.map ( 71 241 function 72  Init_int8 i > Data_int8 i 73  Init_int16 i > Data_int16 i 74  Init_int32 i > Data_int32 i 75  Init_float32 _ 76  Init_float64 _ > assert false (*Not supported*) 77  Init_space n > Data_reserve n 78  Init_addrof (_,_) > assert false (*TODO*) 79 ) l 80 81 let rec size_of_ctype t = match t with 82  Tvoid > 0 83  Tint (I8,_) > 1 84  Tint (I16,_) > 2 85  Tint (I32,_) > 4 86  Tpointer _ > ptr_size 87  Tarray (c,s) > s*(size_of_ctype c) 88  Tstruct (_,lst) > 89 List.fold_left 90 (fun n (_,ty) > n+(size_of_ctype ty)) 0 lst 91  Tunion (_,lst) > 92 List.fold_left 93 (fun n (_,ty) > 94 let sz = (size_of_ctype ty) in (if n>sz then n else sz) 95 ) 0 lst 96  Tfloat _  Tfunction (_,_) > assert false (*Not supported*) 97  Tcomp_ptr _ > ptr_size 98 99 let translate_global_vars ((id,lst),_) = (id,init_to_data lst) 100 101 let translate_unop t = function 102  Onotbool > Op_notbool 103  Onotint > Op_notint 104  Oneg > (match t with 105  Tint (_,_) > Op_negint 106  Tfloat _ > assert false (*Not supported*) 107  _ > assert false (*Type error*) 108 ) 109 110 let translate_cmp t1 t2 cmp = 111 match (t1,t2) with 112  (Tint(_,Signed),Tint(_,Signed)) > Op_cmp cmp 113  (Tint(_,Unsigned),Tint(_,Unsigned)) > Op_cmpu cmp 114  (Tpointer _,Tpointer _) > Op_cmpp cmp 115  _ > Op_cmp cmp 116 117 let translate_add e1 e2 = function 118  (Tint(_,_),Tint(_,_)) > Op2 (Op_add,e1,e2) 119  (Tfloat _,Tfloat _) > assert false (*Not supported*) 120  (Tpointer t,Tint(_,_)) > 121 Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t)))) 122  (Tint(_,_),Tpointer t) > 123 Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t)))) 124  (Tarray (t,_),Tint(_,_)) > 125 Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 126  (Tint(_,_),Tarray(t,_)) > 127 Op2 (Op_addp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t))))) 128  _ > assert false (*Type error*) 129 130 let translate_sub e1 e2 = function 131  (Tint(_,_),Tint(_,_)) > Op2 (Op_sub,e1,e2) 132  (Tfloat _,Tfloat _) > assert false (*Not supported*) 133  (Tpointer t,Tint(_,_)) > 134 Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 135  (Tarray (t,_),Tint(_,_)) > 136 Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 137  _ > assert false (*Type error*) 138 139 let translate_mul e1 e2 = function 140  (Tint(_,_),Tint(_,_)) > Op2 (Op_mul,e1,e2) 141  (Tfloat _,Tfloat _) > assert false (*Not supported*) 142  _ > assert false (*Type error*) 143 144 let translate_div e1 e2 = function 145  (Tint(_,Signed),Tint(_,Signed)) > Op2 (Op_div,e1,e2) 146  (Tint(_,Unsigned),Tint(_,Unsigned)) > Op2 (Op_divu,e1,e2) 147  (Tfloat _,Tfloat _) > assert false (*Not supported*) 148  _ > assert false (*Type error*) 149 150 let translate_binop t1 e1 t2 e2 = function 151  Oadd > translate_add e1 e2 (t1,t2) 152  Osub > translate_sub e1 e2 (t1,t2) 153  Omul > translate_mul e1 e2 (t1,t2) 154  Odiv > translate_div e1 e2 (t1,t2) 155  Omod > Op2 (Op_mod,e1,e2) 156  Oand > Op2 (Op_and,e1,e2) 157  Oor > Op2 (Op_or,e1,e2) 158  Oxor > Op2 (Op_xor,e1,e2) 159  Oshl > Op2 (Op_shl,e1,e2) 160  Oshr > Op2 (Op_shr,e1,e2) 161  Oeq > Op2 (translate_cmp t1 t2 Cmp_eq,e1,e2) 162  One > Op2 (translate_cmp t1 t2 Cmp_ne,e1,e2) 163  Olt > Op2 (translate_cmp t1 t2 Cmp_lt,e1,e2) 164  Ogt > Op2 (translate_cmp t1 t2 Cmp_gt,e1,e2) 165  Ole > Op2 (translate_cmp t1 t2 Cmp_le,e1,e2) 166  Oge > Op2 (translate_cmp t1 t2 Cmp_ge,e1,e2) 167 168 let make_cast e = function 169  (Tint(I8,Signed),Tint(_,_)) > Op1 (Op_cast8signed,e) 170  (Tint(I8,Unsigned),Tint(_,_)) > Op1 (Op_cast8unsigned,e) 171  (Tint(I16,Signed),Tint(_,_)) > Op1 (Op_cast16signed,e) 172  (Tint(I16,Unsigned),Tint(_,_)) > Op1 (Op_cast16unsigned,e) 173  _ > e 174 175 let get_type (Expr (_,t)) = t 176 177 let rec get_offset_struct e id = function 178  [] > assert false (*Wrong id*) 179  (fi,_)::_ when fi=id > e 180  (_,ty)::ll > get_offset_struct (e+(size_of_ctype ty)) id ll 181 182 let is_struct = function 183  Tarray(_,_)  Tstruct (_,_)  Tunion(_,_) > true 242  Clight.Init_int8 i > AST.Data_int8 i 243  Clight.Init_int16 i > AST.Data_int16 i 244  Clight.Init_int32 i > AST.Data_int32 i 245  Clight.Init_float32 _ 246  Clight.Init_float64 _ > error_float () 247  Clight.Init_space n > error "bad global initialization style." 248  Clight.Init_addrof (_,_) > assert false (*TODO*) 249 ) l) 250 251 let translate_global ((id,lst),t) = (id,global_size_of_ctype t,init_to_data lst) 252 253 254 (* Translate expression *) 255 256 let translate_unop = function 257  Clight.Onotbool > AST.Op_notbool 258  Clight.Onotint > AST.Op_notint 259  Clight.Oneg > AST.Op_negint 260 261 let esizeof_ctype res_type t = 262 Cminor.Expr (Cminor.Cst (AST.Cst_sizeof (sizeof_ctype t)), res_type) 263 264 let translate_add res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with 265  Clight.Tint _, Clight.Tint _ > 266 Cminor.Expr (Cminor.Op2 (AST.Op_add, e1, e2), res_type) 267  Clight.Tfloat _, Clight.Tfloat _ > error_float () 268  Clight.Tpointer t, Clight.Tint _ 269  Clight.Tarray (t, _), Clight.Tint _ > 270 let t2 = cminor_type_of e2 in 271 let size = esizeof_ctype t2 t in 272 let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in 273 Cminor.Expr (Cminor.Op2 (AST.Op_addp, e1, index), res_type) 274  Clight.Tint _, Clight.Tpointer t 275  Clight.Tint _, Clight.Tarray (t, _) > 276 let t1 = cminor_type_of e1 in 277 let size = esizeof_ctype t1 t in 278 let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e1, size), t1) in 279 Cminor.Expr (Cminor.Op2 (AST.Op_addp, e2, index), res_type) 280  _ > error "type error." 281 282 let translate_sub res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with 283  Clight.Tint _, Clight.Tint _ > 284 Cminor.Expr (Cminor.Op2 (AST.Op_sub, e1, e2), res_type) 285  Clight.Tfloat _, Clight.Tfloat _ > error_float () 286  Clight.Tpointer t, Clight.Tint _ 287  Clight.Tarray (t, _), Clight.Tint _ > 288 let t2 = cminor_type_of e2 in 289 let size = esizeof_ctype t2 t in 290 let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in 291 Cminor.Expr (Cminor.Op2 (AST.Op_subp, e1, index), res_type) 292  Clight.Tpointer _, Clight.Tpointer _ 293  Clight.Tarray _, Clight.Tpointer _ 294  Clight.Tpointer _, Clight.Tarray _ 295  Clight.Tarray _, Clight.Tarray _ > 296 Cminor.Expr (Cminor.Op2 (AST.Op_subpp, e1, e2), res_type) 297  _ > error "type error." 298 299 let is_signed = function 300  Clight.Tint (_, AST.Signed) > true 184 301  _ > false 185 302 186 let is_ptr_to_struct = function 187  Tpointer t when is_struct t > true 188  _ > false 189 190 let is_function = function 191  Tfunction _ > true 303 let is_pointer = function 304  Clight.Tpointer _  Clight.Tarray _ > true 192 305  _ > false 193 306 194 let rec translate_expr variables expr = 195 let Expr(d,c) = expr in match d with 196  Econst_int i > Cst (Cst_int i) 197  Econst_float f > assert false (*Not supported*) 198  Evar id when is_function c > Cst (Cst_addrsymbol id) 199  Evar id > 200 (try (match Hashtbl.find variables id with 201  (Local,_) > Id id 202  (Stack o,ty) when is_struct ty > Cst (Cst_stackoffset o) 203  (Stack o,_) > 204 Mem (quantity_of_ty c,Cst (Cst_stackoffset o)) 205  (Param,_) > Id id 206  (Global,ty) when is_struct ty > Cst (Cst_addrsymbol id) 207  (Global,_) > 208 Mem (quantity_of_ty c,Cst (Cst_addrsymbol id)) 209 ) with Not_found > assert false) 210  Ederef e when is_ptr_to_struct (get_type e) > 211 translate_expr variables e 212  Ederef e > Mem (quantity_of_ty c,translate_expr variables e) 213  Eaddrof se > ( 214 match se with 215  Expr(Evar id,_) > 216 (try (match Hashtbl.find variables id with 217  (Local,_) > assert false (*Impossible: see sort_variables*) 218  (Stack o,_) > Cst (Cst_stackoffset o) 219  (Param,_) > Cst (Cst_addrsymbol id) 220  (Global,_) > Cst (Cst_addrsymbol id) 221 ) with Not_found > assert false) 222  Expr(Ederef ee,_) > 223 translate_expr variables ee 224  Expr(Efield (str,fi),_) > 225 (match str with 226  Expr(_,Tstruct(_,b)) > 227 Op2 (Op_add 228 ,translate_expr variables str 229 ,Cst (Cst_int (get_offset_struct 0 fi b))) 230  Expr(_,Tunion(_,_)) > 231 translate_expr variables str 232  _ > assert false (*Type Error*) 233 ) 234  _ > assert false (*Must be a lvalue*) 235 ) 236  Eunop (op,e) > 237 Op1 (translate_unop (get_type e) op ,translate_expr variables e) 238  Ebinop (op,e1,e2) > 239 translate_binop 240 (get_type e1) (translate_expr variables e1) 241 (get_type e2) (translate_expr variables e2) op 242  Ecast (ty,e) > make_cast (translate_expr variables e) (get_type e,ty) 243  Econdition (e1,e2,e3) > 244 Cond (translate_expr variables e1, 245 translate_expr variables e2, 246 translate_expr variables e3) 247  Eandbool (e1,e2) > 248 Cond ( 249 translate_expr variables e1, 250 Cond(translate_expr variables e2,Cst (Cst_int 1),Cst (Cst_int 0)), 251 Cst (Cst_int 0)) 252  Eorbool (e1,e2) > 253 Cond ( 254 translate_expr variables e1, 255 Cst (Cst_int 1), 256 Cond(translate_expr variables e2, Cst (Cst_int 1),Cst (Cst_int 0)) ) 257  Esizeof cc > Cst (Cst_int (size_of_ctype cc)) 258  Efield (e,id) > 259 (match get_type e with 260  Tstruct(_,lst) > 261 (try 262 Mem (quantity_of_ty (List.assoc id lst) 263 ,Op2(Op_add 264 ,translate_expr variables e 265 , Cst (Cst_int (get_offset_struct 0 id lst)) 266 ) 267 ) 268 with Not_found > assert false (*field does not exists*) 269 ) 270  Tunion(_,lst) > 271 (try 272 Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e) 273 with Not_found > assert false (*field does not exists*) 274 ) 275  _ > assert false (*Type error*) 276 ) 277  Ecost (lbl,e) > Exp_cost (lbl,translate_expr variables e) 278  Ecall _ > assert false (* Only for annotations *) 279 280 let translate_assign variables e = function 281  Expr (Evar v,t) > 282 (try (match Hashtbl.find variables v with 283  (Local,_) > St_assign (v,translate_expr variables e) 284  (Stack o,_) > St_store (quantity_of_ty t 285 ,Cst (Cst_stackoffset o) 286 ,translate_expr variables e) 287  (Param,_) > St_assign (v,translate_expr variables e) 288  (Global,_) > St_store (quantity_of_ty t 289 ,Cst (Cst_addrsymbol v) 290 ,translate_expr variables e) 291 ) with Not_found > assert false) 292  Expr (Ederef ee,t) > St_store (quantity_of_ty t 293 ,translate_expr variables ee 294 ,translate_expr variables e) 295  Expr (Efield (ee,id),t) > 296 (match ee with 297  Expr (_,Tstruct(_,lst)) > 298 St_store (quantity_of_ty t 299 ,Op2(Op_add,translate_expr variables ee 300 ,Cst(Cst_int (get_offset_struct 0 id lst ))) 301 ,translate_expr variables e) 302  Expr (_,Tunion(_,_)) > St_store (quantity_of_ty t 303 ,translate_expr variables ee 304 ,translate_expr variables e) 305  _ > assert false (*Type error*) 306 ) 307  _ > assert false (*lvalue error*) 308 309 let translate_call_name variables = function 310  Expr (Evar id,_) > Cst (Cst_addrsymbol id) 311  _ > assert false (*Not supported*) 312 313 let translate_call variables e1 e2 lst = 314 let st_call f_assign f_res = 315 St_call (f_assign 316 ,translate_expr variables e2 317 ,List.map (translate_expr variables) lst 318 ,{args=List.map (fun exp > 319 let Expr(_,t) = exp in ctype_to_sig_type t 320 )lst;res=f_res} 321 ) in 322 match e1 with 323  Some (Expr (se,tt)) > ( 324 match se with 325  Evar v > 326 (try (match Hashtbl.find variables v with 327  (Local,_)  (Param,_) > 328 st_call (Some v) (Type_ret (ctype_to_sig_type tt)) 329  (Stack o,_) > 330 let tmp = fresh_tmp variables in 331 St_seq ( 332 st_call (Some tmp) (Type_ret (ctype_to_sig_type tt)) 333 ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp) 334 ) 335  (Global,_) > 336 let tmp = fresh_tmp variables in 337 St_seq ( 338 st_call (Some tmp) (Type_ret (ctype_to_sig_type tt)) 339 ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp) 340 ) 341 ) with Not_found > assert false ) 342  Ederef ee > assert false (*Not supported*) 343  Efield (ee,id) > assert false (*Not supported*) 344  _ > assert false (*Should be a lvalue*) 345 ) 346  None > st_call None Type_void 347 348 (*TODO rewrite this buggy function*) 349 let translate_switch expr (cases,default) = 350 let sz = List.length cases in 351 let sw = St_block (St_switch ( 352 expr, MiscPottier.mapi (fun i (n,_) > (n,i)) cases, sz)) in 353 let rec add_block n e = function 354  [] > St_block (St_seq(e,default)) 355  (_,st)::l > 356 add_block (n1) (St_block (St_seq(e,St_seq(st,St_exit n)))) l 357 in add_block sz sw cases 358 359 let rec translate_stmt variables = function 360  Sskip > St_skip 361  Sassign (e1,e2) > translate_assign variables e2 e1 362  Scall (e1,e2,lst) > translate_call variables e1 e2 lst 363  Ssequence (s1,s2) > 364 St_seq (translate_stmt variables s1, 365 translate_stmt variables s2) 366  Sifthenelse (e,s1,s2) > 367 St_ifthenelse (translate_expr variables e, 368 translate_stmt variables s1, 369 translate_stmt variables s2) 370  Swhile (e,s) > 371 St_block(St_loop(St_seq ( 372 St_ifthenelse ( 373 Op1 (Op_notbool,translate_expr variables e), 374 St_exit 0,St_skip), 375 St_block (translate_stmt variables s) 376 ))) 377  Sdowhile (e,s) > 378 St_block(St_loop(St_seq ( 379 St_block (translate_stmt variables s), 380 St_ifthenelse ( 381 Op1(Op_notbool, translate_expr variables e), 382 St_exit 0,St_skip) 383 ))) 384  Sfor (s1,e,s2,s3) > 385 let b = St_block (St_loop (St_seq ( 386 St_ifthenelse ( 387 Op1(Op_notbool,translate_expr variables e), 388 St_exit 0,St_skip), 389 St_seq (St_block (translate_stmt variables s3), 390 translate_stmt variables s2 391 )))) in 392 (match (translate_stmt variables s1) with 393  St_skip > b  ss > St_seq (ss,b)) 394  Sbreak > St_exit(1) 395  Scontinue > St_exit(0) 396  Sreturn (Some e) > St_return (Some(translate_expr variables e)) 397  Sreturn None > St_return None 398  Sswitch (e,lbl) > 399 translate_switch (translate_expr variables e) (compute_lbl variables lbl) 400  Slabel (lbl,st) > 401 St_label(lbl,translate_stmt variables st) 402  Sgoto lbl > St_goto lbl 403  Scost (lbl,s) > St_cost(lbl,translate_stmt variables s) 404 405 and compute_lbl variables = function 406  LSdefault s > ([],translate_stmt variables s) 407  LScase (i,s,l) > 408 let (ll,def) = (compute_lbl variables l) in 409 ((i,translate_stmt variables s)::ll,def) 410 411 let rec get_stack_vars_expr (Expr (exp,_)) = match exp with 412  Econst_int _  Evar _  Esizeof _ > [] 413  Ederef e > (get_stack_vars_expr e) 414  Eaddrof Expr(e,_) > ( 415 match e with 416  Evar id > [id] 417  Ederef ee  Efield (ee,_) > (get_stack_vars_expr ee) 418  _ > assert false (*Should be a lvalue*) 419 ) 420  Eunop (_,e) > (get_stack_vars_expr e) 421  Ebinop (_,e1,e2) > (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 422  Ecast (_,e) > (get_stack_vars_expr e) 423  Econdition (e1,e2,e3) > 424 (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 425 @(get_stack_vars_expr e3) 426  Eandbool (e1,e2) > (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 427  Eorbool (e1,e2) > (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 428  Ecost (_,e) > (get_stack_vars_expr e) 429  Efield (e,_) > (get_stack_vars_expr e) 430  Econst_float _ > assert false (*Not supported*) 431  Ecall _ > assert false (* Should not happen *) 432 433 let rec get_stack_vars_stmt = function 434  Sskip  Sbreak  Scontinue  Sreturn None  Sgoto _ > [] 435  Sassign (e1,e2) > 436 (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 437  Scall (None,e,lst) > 438 (get_stack_vars_expr e) 439 @(List.fold_left (fun l e > l@(get_stack_vars_expr e)) [] lst) 440  Scall (Some e1,e2,lst) > 441 (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 442 @(List.fold_left (fun l e > l@(get_stack_vars_expr e)) [] lst) 443  Ssequence (s1,s2) > 444 (get_stack_vars_stmt s1)@(get_stack_vars_stmt s2) 445  Sifthenelse (e,s1,s2) > 446 (get_stack_vars_expr e)@(get_stack_vars_stmt s1)@(get_stack_vars_stmt s2) 447  Swhile (e,s) > 448 (get_stack_vars_expr e)@(get_stack_vars_stmt s) 449  Sdowhile (e,s) > 450 (get_stack_vars_expr e)@(get_stack_vars_stmt s) 451  Sfor (s1,e,s2,s3) > 452 (get_stack_vars_expr e)@(get_stack_vars_stmt s1)@(get_stack_vars_stmt s2) 453 @(get_stack_vars_stmt s3) 454  Sreturn (Some e) > 455 (get_stack_vars_expr e) 456  Sswitch (e,ls) > 457 (get_stack_vars_expr e)@(get_stack_vars_ls ls) 458  Slabel (_,s) > (get_stack_vars_stmt s) 459  Scost (_,s) > (get_stack_vars_stmt s) 460 and get_stack_vars_ls = function 461  LSdefault s > get_stack_vars_stmt s 462  LScase (_,s,ls) > (get_stack_vars_stmt s)@(get_stack_vars_ls ls) 463 464 let is_struct = function 465  Tarray (_,_)  Tstruct (_,_)  Tunion (_,_) > true 466  _ > false 467 468 let sort_variables globals f = 469 let variables = Hashtbl.create 47 and next_offset = ref 0 in 470 List.iter (fun (id,ty) > Hashtbl.add variables id (Global,ty)) globals; 471 List.iter (fun (id,ty) > Hashtbl.add variables id (Param,ty)) f.fn_params; 472 List.iter 473 (fun (id,ty) > 474 if is_struct ty then ( 475 Hashtbl.add variables id (Stack !next_offset,ty); 476 next_offset := !next_offset + (size_of_ctype ty) 477 ) else Hashtbl.add variables id (Local,ty) 478 ) f.fn_vars; 479 List.iter 480 (fun id > match 481 (try 482 Hashtbl.find variables id 483 with 484 Not_found > ( 485 Printf.eprintf "Error: Cannot find variable %s\n" id; 486 assert false) 487 ) with 488  (Local,ty) > 489 Hashtbl.add variables id (Stack !next_offset,ty); 490 next_offset:=!next_offset + (size_of_ctype ty) 491  (Global,_) > () 492  (Param,_) > () 493  (Stack _,_) > () 494 ) (get_stack_vars_stmt f.fn_body); 495 variables 496 497 let get_locals variables = 498 Hashtbl.fold 499 (fun id (v,_) l > match v with 500  Local > id::l 501  _ > l 502 ) variables [] 503 504 let get_stacksize variables = 505 Hashtbl.fold 506 (fun _ (v,t) c1 > let c2 = match v with 507  Stack o > o+(size_of_ctype t) 508  _ > c1 in if c1 > c2 then c1 else c2 509 ) variables 0 510 511 let translate_internal globals f = 512 let variables = sort_variables globals f in 513 { f_sig = 514 { 515 args = List.map (fun p > ctype_to_sig_type (snd p)) f.fn_params ; 516 res = ctype_to_type_return f.fn_return 517 }; 518 f_params = List.map fst f.fn_params ; 519 f_vars = (fresh_tmp variables)::(get_locals variables); 520 f_ptrs = [] (* will be filled in translate, 521 when calling CminorPointers.fill *); 522 f_stacksize = get_stacksize variables ; 523 f_body = translate_stmt variables f.fn_body 524 } 307 let cmp_of_clight_binop = function 308  Clight.Oeq > AST.Cmp_eq 309  Clight.One > AST.Cmp_ne 310  Clight.Olt > AST.Cmp_lt 311  Clight.Ole > AST.Cmp_le 312  Clight.Ogt > AST.Cmp_gt 313  Clight.Oge > AST.Cmp_ge 314  _ > assert false (* do not use on these arguments *) 315 316 let translate_simple_binop t = function 317  Clight.Omul > AST.Op_mul 318  Clight.Odiv when is_signed t > AST.Op_div 319  Clight.Odiv > AST.Op_divu 320  Clight.Omod when is_signed t > AST.Op_mod 321  Clight.Omod > AST.Op_modu 322  Clight.Oand > AST.Op_and 323  Clight.Oor > AST.Op_or 324  Clight.Oxor > AST.Op_xor 325  Clight.Oshl > AST.Op_shl 326  Clight.Oshr when is_signed t > AST.Op_shr 327  Clight.Oshr > AST.Op_shru 328  binop when is_pointer t > AST.Op_cmpp (cmp_of_clight_binop binop) 329  binop when is_signed t > AST.Op_cmp (cmp_of_clight_binop binop) 330  binop > AST.Op_cmpu (cmp_of_clight_binop binop) 331 332 let translate_binop res_type ctype1 ctype2 e1 e2 binop = 333 match binop with 334  Clight.Oadd > translate_add res_type ctype1 ctype2 e1 e2 335  Clight.Osub > translate_sub res_type ctype1 ctype2 e1 e2 336  _ > 337 let cminor_binop = translate_simple_binop ctype1 binop in 338 Cminor.Expr (Cminor.Op2 (cminor_binop, e1, e2), res_type) 339 340 let translate_ident var_locs res_type x = 341 let ed = match find_var_locs x var_locs with 342  (Local, _)  (Param, _) > Cminor.Id x 343  (LocalStack off, t)  (ParamStack off, t) when is_scalar_ctype t > 344 let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in 345 Cminor.Mem (quantity_of_ctype t, addr) 346  (LocalStack off, _)  (ParamStack off, _) > 347 add_stack off 348  (Global, t) when is_scalar_ctype t > 349 let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in 350 Cminor.Mem (quantity_of_ctype t, addr) 351  (Global, _) > Cminor.Cst (AST.Cst_addrsymbol x) in 352 Cminor.Expr (ed, res_type) 353 354 let translate_field res_type t e field = 355 let (fields, offset) = match t with 356  Clight.Tstruct (_, fields) > (fields, struct_offset t field fields) 357  Clight.Tunion (_, fields) > 358 (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset)) 359  _ > assert false (* type error *) in 360 let addr = Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), AST.Sig_ptr) in 361 let quantity = quantity_of_ctype (List.assoc field fields) in 362 Cminor.Expr (Cminor.Mem (quantity, addr), res_type) 363 364 let translate_cast e src_type dest_type = 365 let res_type = sig_type_of_ctype dest_type in 366 match src_type, dest_type with 367  Clight.Tint (size1, sign1), Clight.Tint (size2, _) > 368 let t1 = (byte_size_of_intsize size1, sign1) in 369 let t2 = byte_size_of_intsize size2 in 370 Cminor.Expr (Cminor.Op1 (AST.Op_cast (t1, t2), e), res_type) 371  Clight.Tint _, Clight.Tpointer _ 372  Clight.Tint _, Clight.Tarray _ > 373 Cminor.Expr (Cminor.Op1 (AST.Op_ptrofint, e), res_type) 374  Clight.Tpointer _, Clight.Tint _ 375  Clight.Tarray _, Clight.Tint _ > 376 Cminor.Expr (Cminor.Op1 (AST.Op_intofptr, e), res_type) 377  _ > e 378 379 let rec f_expr var_locs (Clight.Expr (ed, t)) sub_exprs_res = 380 let t_cminor = sig_type_of_ctype t in 381 let cst_int i t = Cminor.Expr (Cminor.Cst (AST.Cst_int i), t) in 382 match ed, sub_exprs_res with 383 384  Clight.Econst_int i, _ > 385 Cminor.Expr (Cminor.Cst (AST.Cst_int i), t_cminor) 386 387  Clight.Econst_float _, _ > error_float () 388 389  Clight.Evar x, _ when is_function_ctype t > 390 Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), t_cminor) 391 392  Clight.Evar x, _ > translate_ident var_locs t_cminor x 393 394  Clight.Ederef _, e :: _ when is_scalar_ctype t > 395 Cminor.Expr (Cminor.Mem (quantity_of_ctype t, e), t_cminor) 396 397  Clight.Ederef _, e :: _ > 398 (* When dereferencing something pointing to a struct for instance, the 399 result is the address of the struct. *) 400 e 401 402  Clight.Eaddrof e, _ > translate_addrof var_locs e 403 404  Clight.Eunop (unop, _), e :: _ > 405 Cminor.Expr (Cminor.Op1 (translate_unop unop, e), t_cminor) 406 407  Clight.Ebinop (binop, e1, e2), e1' :: e2' :: _ > 408 translate_binop t_cminor (clight_type_of e1) (clight_type_of e2) e1' e2' 409 binop 410 411  Clight.Ecast (t, Clight.Expr (_, t')), e :: _ > translate_cast e t' t 412 413  Clight.Econdition _, e1 :: e2 :: e3 :: _ > 414 Cminor.Expr (Cminor.Cond (e1, e2, e3), t_cminor) 415 416  Clight.Eandbool _, e1 :: e2 :: _ > 417 let zero = cst_int 0 t_cminor in 418 let one = cst_int 1 t_cminor in 419 let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in 420 Cminor.Expr (Cminor.Cond (e1, e2_cond, zero), t_cminor) 421 422  Clight.Eorbool _, e1 :: e2 :: _ > 423 let zero = cst_int 0 t_cminor in 424 let one = cst_int 1 t_cminor in 425 let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in 426 Cminor.Expr (Cminor.Cond (e1, one, e2_cond), t_cminor) 427 428  Clight.Esizeof t, _ > esizeof_ctype t_cminor t 429 430  Clight.Ecost (lbl, _), e :: _ > 431 Cminor.Expr (Cminor.Exp_cost (lbl, e), t_cminor) 432 433  Clight.Ecall _, _ > assert false (* only for annotations *) 434 435  Clight.Efield (Clight.Expr (_, t), field), e :: _ > 436 translate_field t_cminor t e field 437 438  _ > assert false (* wrong number of arguments *) 439 440 and translate_addrof_ident res_type var_locs id = 441 match find_var_locs id var_locs with 442  (Local, _)  (Param, _) > assert false (* type error *) 443  (LocalStack off, _)  (ParamStack off, _) > 444 Cminor.Expr (add_stack off, res_type) 445  (Global, _) > 446 Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol id), res_type) 447 448 and translate_addrof_field res_type t field e = 449 let (fields, offset) = match t with 450  Clight.Tstruct (_, fields) > (fields, struct_offset t field fields) 451  Clight.Tunion (_, fields) > 452 (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset)) 453  _ > assert false (* type error *) in 454 Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), res_type) 455 456 and translate_addrof var_locs (Clight.Expr (ed, _)) = 457 let res_type = AST.Sig_ptr in 458 match ed with 459 460  Clight.Evar id > translate_addrof_ident res_type var_locs id 461 462  Clight.Ederef e > translate_expr var_locs e 463 464  Clight.Efield ((Clight.Expr (_, t) as e), field) > 465 let e = translate_expr var_locs e in 466 translate_addrof_field res_type t field e 467 468  _ > assert false (* not a lvalue *) 469 470 and translate_expr var_locs e = ClightFold.expr2 (f_expr var_locs) e 471 472 473 (* Translate statement *) 474 475 let assign var_locs (Clight.Expr (ed, t) as e_res_clight) e_arg_cminor = 476 match ed with 477  Clight.Evar id when is_local_or_param id var_locs > 478 Cminor.St_assign (id, e_arg_cminor) 479  _ > 480 let quantity = quantity_of_ctype t in 481 let addr = translate_addrof var_locs e_res_clight in 482 Cminor.St_store (quantity, addr, e_arg_cminor) 483 484 let call_sig ret_type args = 485 { AST.args = List.map cminor_type_of args ; 486 AST.res = ret_type } 487 488 let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res = 489 let (tmps, sub_stmts_res) = List.split sub_stmts_res in 490 let tmps = List.flatten tmps in 491 492 let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with 493 494  Clight.Sskip, _, _ > ([], Cminor.St_skip) 495 496  Clight.Sassign (e1, _), _ :: e2 :: _, _ > 497 ([], assign var_locs e1 e2) 498 499  Clight.Scall (None, _, _), f :: args, _ > 500 ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args)) 501 502  Clight.Scall (Some e, _, _), _ :: f :: args, _ > 503 let t = sig_type_of_ctype (clight_type_of e) in 504 let tmp = fresh () in 505 let tmpe = Cminor.Expr (Cminor.Id tmp, t) in 506 let stmt_call = 507 Cminor.St_call (Some tmp, f, args, call_sig (AST.Type_ret t) args) in 508 let stmt_assign = assign var_locs e tmpe in 509 ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign)) 510 511  Clight.Swhile _, e :: _, stmt :: _ > 512 let econd = 513 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 514 let scond = 515 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 516 ([], 517 Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond, 518 Cminor.St_block stmt)))) 519 520  Clight.Sdowhile _, e :: _, stmt :: _ > 521 let econd = 522 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 523 let scond = 524 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 525 ([], 526 Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt, 527 scond)))) 528 529  Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ > 530 let econd = 531 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 532 let scond = 533 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 534 let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in 535 ([], 536 Cminor.St_seq (stmt1, 537 Cminor.St_block 538 (Cminor.St_loop (Cminor.St_seq (scond, body))))) 539 540  Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ > 541 ([], Cminor.St_ifthenelse (e, stmt1, stmt2)) 542 543  Clight.Ssequence _, _, stmt1 :: stmt2 :: _ > 544 ([], Cminor.St_seq (stmt1, stmt2)) 545 546  Clight.Sbreak, _, _ > ([], Cminor.St_exit 1) 547 548  Clight.Scontinue, _, _ > ([], Cminor.St_exit 0) 549 550  Clight.Sswitch _, _, _ > 551 (* Should not appear because of switch transformation performed 552 beforehand. *) 553 assert false 554 555  Clight.Sreturn None, _, _ > ([], Cminor.St_return None) 556 557  Clight.Sreturn (Some _), e :: _, _ > ([], Cminor.St_return (Some e)) 558 559  Clight.Slabel (lbl, _), _, stmt :: _ > ([], Cminor.St_label (lbl, stmt)) 560 561  Clight.Sgoto lbl, _, _ > ([], Cminor.St_goto lbl) 562 563  Clight.Scost (lbl, _), _, stmt :: _ > ([], Cminor.St_cost (lbl, stmt)) 564 565  _ > assert false (* type error *) in 566 567 (tmps @ added_tmps, stmt) 568 569 let translate_statement fresh var_locs = 570 ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs) 571 572 573 (* Translate functions and programs *) 574 575 let add_stack_parameter_initialization x t off body = 576 let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in 577 let e = Cminor.Expr (Cminor.Id x, sig_type_of_ctype t) in 578 let stmt = Cminor.St_store (quantity_of_ctype t, addr, e) in 579 Cminor.St_seq (stmt, body) 580 581 let add_stack_parameters_initialization var_locs body = 582 let f x (location, t) body = match location with 583  ParamStack offset > add_stack_parameter_initialization x t offset body 584  _ > body in 585 fold_var_locs f var_locs body 586 587 let translate_internal fresh globals cfun = 588 let var_locs = sort_variables globals cfun in 589 let params = 590 List.map (fun (x, t) > (x, sig_type_of_ctype t)) cfun.Clight.fn_params in 591 let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in 592 let body = add_stack_parameters_initialization var_locs body in 593 { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ; 594 Cminor.f_params = params ; 595 Cminor.f_vars = (get_locals var_locs) @ tmps ; 596 Cminor.f_stacksize = get_stacksize var_locs ; 597 Cminor.f_body = body } 525 598 526 599 let translate_external id params return = 527 { 528 ef_tag = id ; 529 ef_sig = { 530 args = List.map ctype_to_sig_type params ; 531 res = ctype_to_type_return return 532 } 533 } 534 535 let translate_funct globals = function 536  (id,Internal ff) > (id,F_int (translate_internal globals ff)) 537  (id,External (i,p,r)) > (id, F_ext (translate_external i p r)) 600 { AST.ef_tag = id ; 601 AST.ef_sig = { AST.args = translate_args_types params ; 602 AST.res = type_return_of_ctype return } } 603 604 let translate_funct fresh globals (id, def) = 605 let def = match def with 606  Clight.Internal ff > Cminor.F_int (translate_internal fresh globals ff) 607  Clight.External (i,p,r) > Cminor.F_ext (translate_external i p r) in 608 (id, def) 538 609 539 610 let translate p = 540 let p = Clight32ToClight8.translate p in 541 let globals = List.map (fun p > (fst (fst p),snd p) ) p.prog_vars in 542 let p = 543 {Cminor.vars = List.map translate_global_vars p.prog_vars; 544 Cminor.functs = List.map (translate_funct globals ) p.prog_funct; 545 Cminor.main = p.prog_main } in 546 (* TODO: find a better solution to get the pointers in the result. *) 547 CminorPointers.fill p 611 let fresh = ClightAnnotator.make_fresh "_tmp" p in 612 { Cminor.vars = List.map translate_global p.Clight.prog_vars ; 613 Cminor.functs = 614 List.map (translate_funct fresh p.Clight.prog_vars) p.Clight.prog_funct ; 615 Cminor.main = p.Clight.prog_main }
Note: See TracChangeset
for help on using the changeset viewer.