Changeset 818 for Deliverables/D2.2/8051/src/cminor
- Timestamp:
- May 19, 2011, 4:03:04 PM (10 years ago)
- Location:
- Deliverables/D2.2/8051/src/cminor
- Files:
-
- 12 edited
-
cminor.mli (modified) (4 diffs)
-
cminorAnnotator.ml (modified) (7 diffs)
-
cminorAnnotator.mli (modified) (2 diffs)
-
cminorFold.ml (modified) (1 diff)
-
cminorFold.mli (modified) (1 diff)
-
cminorInterpret.ml (modified) (15 diffs)
-
cminorInterpret.mli (modified) (1 diff)
-
cminorLabelling.ml (modified) (1 diff)
-
cminorLexer.mll (modified) (1 diff)
-
cminorParser.mly (modified) (4 diffs)
-
cminorPrinter.ml (modified) (11 diffs)
-
cminorToRTLabs.ml (modified) (21 diffs)
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/cminor/cminor.mli
r740 r818 3 3 4 4 (* This file describes the abstract syntax of the Cminor language. 5 Only types are: int8, int16, int32 , float32, float64and void. *)5 Only types are: int8, int16, int32 and void. *) 6 6 7 type expression = 7 type etype = AST.sig_type 8 9 type expression = Expr of expr_descr * etype 10 and expr_descr = 8 11 | Id of AST.ident 9 12 | Cst of AST.cst 10 13 | Op1 of AST.op1 * expression 11 14 | Op2 of AST.op2 * expression * expression 12 | Mem of Memory.quantity * expression (* Memory read *)15 | Mem of AST.quantity * expression (* Memory read *) 13 16 | Cond of expression * expression * expression (* Ternary expression *) 14 17 | Exp_cost of CostLabel.t * expression (* Labelled expression *) … … 17 20 | St_skip 18 21 | St_assign of AST.ident * expression 19 | St_store of Memory.quantity * expression * expression22 | St_store of AST.quantity * expression * expression 20 23 21 24 (* Function call. Parameters are an optional variable to store the … … 47 50 48 51 type internal_function = 49 { f_sig : AST.signature ; 50 f_params : AST.ident list ; 51 f_vars : AST.ident list ; 52 f_ptrs : AST.ident list ; 53 f_stacksize : int ; 52 { f_return : AST.type_return ; 53 f_params : (AST.ident * etype) list ; 54 f_vars : (AST.ident * etype) list ; 55 f_stacksize : AST.abstract_size ; 54 56 f_body : statement } 55 57 … … 63 65 64 66 type program = 65 { vars : (AST.ident * (AST.data list)) list ;67 { vars : (AST.ident * AST.abstract_size * AST.data list option) list ; 66 68 functs : (AST.ident * function_def) list ; 67 69 main : AST.ident option } -
Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml
r740 r818 3 3 4 4 let funct_vars (id, fun_def) = match fun_def with 5 | Cminor.F_int def -> id :: (def.Cminor.f_params @ def.Cminor.f_vars) 5 | Cminor.F_int def -> 6 id :: (List.map fst (def.Cminor.f_params @ def.Cminor.f_vars)) 6 7 | _ -> [id] 7 8 8 9 let prog_idents p = 9 let vars = List.map fstp.Cminor.vars in10 let vars = List.map (fun (x, _, _) -> x) p.Cminor.vars in 10 11 let f vars funct = vars @ (funct_vars funct) in 11 12 let vars = List.fold_left f vars p.Cminor.functs in … … 18 19 19 20 21 (* 20 22 let increment cost_id incr = 21 let cost = Cminor.Cst (AST.Cst_addrsymbol cost_id) in 22 let load = Cminor.Mem (Memory.QInt 4, cost) in 23 let incr = Cminor.Op2 (AST.Op_add, load, Cminor.Cst (AST.Cst_int incr)) in 23 let cost = 24 Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol cost_id), AST.Sig_ptr) in 25 let load = Cminor.Expr (Cminor.Mem (Memory.QInt 4, cost), AST.Sig_int 4) in 26 let incr = Cminor.Expr (Cminor.Cst (AST.Cst_int incr), AST.Sig_int 4) in 27 let incr = Cminor.Expr (Cminor.Op2 (AST.Op_add, load, incr), AST.Sig_int 4) in 24 28 Cminor.St_store (Memory.QInt 4, cost, incr) 25 29 … … 35 39 36 40 let remove_cost_labels_exp e = 37 CminorFold.expression _leftf_remove_cost_labels_exp e41 CminorFold.expression f_remove_cost_labels_exp e 38 42 39 43 let remove_cost_labels_exps exps = … … 59 63 60 64 let update_cost_exp costs_mapping cost_id e = 61 CminorFold.expression _left(f_update_cost_exp costs_mapping cost_id) e65 CminorFold.expression (f_update_cost_exp costs_mapping cost_id) e 62 66 63 67 let update_cost_exps costs_mapping cost_id exps = … … 148 152 "" (* TODO *), 149 153 "" (* TODO *)) 154 *) 150 155 151 156 … … 168 173 List.fold_left f labels_empty l 169 174 170 let f_exp_labels esubexp_res =175 let f_exp_labels (Cminor.Expr (ed, _)) subexp_res = 171 176 let labels1 = labels_union_list subexp_res in 172 let labels2 = match e with177 let labels2 = match ed with 173 178 | Cminor.Exp_cost (lbl, _) -> add_cost_label lbl labels_empty 174 179 | _ -> labels_empty in … … 185 190 labels_union labels labels3 186 191 187 let body_labels stmt = CminorFold.statement _leftf_exp_labels f_body_labels stmt192 let body_labels stmt = CminorFold.statement f_exp_labels f_body_labels stmt 188 193 189 194 let prog_labels p = -
Deliverables/D2.2/8051/src/cminor/cminorAnnotator.mli
r640 r818 2 2 (** This module defines the instrumentation of a [Cminor] program. *) 3 3 4 (* 4 5 (** [instrument prog cost_map] instruments the program [prog]. First a fresh 5 6 global variable --- the so-called cost variable --- is added to the program. … … 10 11 val instrument : Cminor.program -> int CostLabel.Map.t -> 11 12 Cminor.program * string * string 13 *) 12 14 13 15 val cost_labels : Cminor.program -> CostLabel.Set.t -
Deliverables/D2.2/8051/src/cminor/cminorFold.ml
r486 r818 4 4 5 5 6 (* Left operators *) 6 let expression_subs (Cminor.Expr (ed, _)) = match ed with 7 | Cminor.Id _ | Cminor.Cst _ -> [] 8 | Cminor.Op1 (_, e) | Cminor.Mem (_, e) | Cminor.Exp_cost (_, e) -> [e] 9 | Cminor.Op2 (_, e1, e2) -> [e1 ; e2] 10 | Cminor.Cond (e1, e2, e3) -> [e1 ; e2 ; e3] 7 11 8 (* In [expression_left f e], [f]'s second argument is the list of 9 [expression_left]'s results on [e]'s sub-expressions. The results are 10 computed from left to right following their appearance order in the 11 [Cminor.expression] type. *) 12 13 let rec expression_left f_expr e = 14 let subexpr_res = match e with 15 | Cminor.Id _ | Cminor.Cst _ -> [] 16 | Cminor.Op1 (_, e) | Cminor.Mem (_, e) | Cminor.Exp_cost (_, e) -> 17 [expression_left f_expr e] 18 | Cminor.Op2 (_, e1, e2) -> 19 let res1 = expression_left f_expr e1 in 20 let res2 = expression_left f_expr e2 in 21 [res1 ; res2] 22 | Cminor.Cond (e1, e2, e3) -> 23 let res1 = expression_left f_expr e1 in 24 let res2 = expression_left f_expr e2 in 25 let res3 = expression_left f_expr e3 in 26 [res1 ; res2 ; res3] 27 in 28 f_expr e subexpr_res 29 30 let map_left f = 31 let rec aux = function 32 | [] -> [] 33 | e :: l -> let x = f e in x :: (aux l) 34 in 35 aux 36 37 (* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the 38 list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and 39 [f_stmt]'s third argument is the list of [statement_left]'s results 40 on [stmt]'s sub-statements. The results are computed from left to right 41 following their appearance order in the [Cminor.statement] type. *) 42 43 let rec statement_left f_expr f_stmt stmt = 44 let expr_res e = expression_left f_expr e in 45 let (subexpr_res, substmt_res) = match stmt with 46 | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_switch _ 47 | Cminor.St_return None | Cminor.St_goto _ -> ([], []) 48 | Cminor.St_assign (_, e) | Cminor.St_return (Some e) -> ([expr_res e], []) 49 | Cminor.St_store (_, e1, e2) -> 50 let res1 = expr_res e1 in 51 let res2 = expr_res e2 in 52 ([res1 ; res2], []) 53 | Cminor.St_call (_, f, args, _) | Cminor.St_tailcall (f, args, _) -> 54 let resf = expr_res f in 55 let resargs = map_left expr_res args in 56 (resf :: resargs, []) 57 | Cminor.St_seq (stmt1, stmt2) -> 58 let res1 = statement_left f_expr f_stmt stmt1 in 59 let res2 = statement_left f_expr f_stmt stmt2 in 60 ([], [res1 ; res2]) 61 | Cminor.St_ifthenelse (e, stmt1, stmt2) -> 62 let rese = expr_res e in 63 let res1 = statement_left f_expr f_stmt stmt1 in 64 let res2 = statement_left f_expr f_stmt stmt2 in 65 ([rese], [res1 ; res2]) 66 | Cminor.St_loop stmt | Cminor.St_block stmt 67 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) -> 68 ([], [statement_left f_expr f_stmt stmt]) 69 in 70 f_stmt stmt subexpr_res substmt_res 12 let expression_fill_subs (Cminor.Expr (ed, t)) subs = 13 let ed = match ed, subs with 14 | Cminor.Id _, _ | Cminor.Cst _, _ -> ed 15 | Cminor.Op1 (op1, _), e :: _ -> Cminor.Op1 (op1, e) 16 | Cminor.Op2 (op2, _, _), e1 :: e2 :: _ -> Cminor.Op2 (op2, e1, e2) 17 | Cminor.Mem (size, _), e :: _ -> Cminor.Mem (size, e) 18 | Cminor.Cond _, e1 :: e2 :: e3 :: _ -> Cminor.Cond (e1, e2, e3) 19 | Cminor.Exp_cost (lbl, _), e :: _ -> Cminor.Exp_cost (lbl, e) 20 | _ -> assert false (* wrong parameter size *) in 21 Cminor.Expr (ed, t) 71 22 72 23 73 (* Right operators *) 24 (* In [expression f e], [f]'s second argument is the list of 25 [expression]'s results on [e]'s sub-expressions. *) 74 26 75 (* In [expression_right f e], [f]'s second argument is the list of 76 [expression_right]'s results on [e]'s sub-expressions. The results are 77 computed from right to left following their appearance order in the 78 [Cminor.expression] type. *) 27 let rec expression f_expr e = 28 let sub_es_res = List.map (expression f_expr) (expression_subs e) in 29 f_expr e sub_es_res 79 30 80 let rec expression_right f_expr e =81 let subexpr_res = match e with82 | Cminor.Id _ | Cminor.Cst _ -> []83 | Cminor.Op1 (_, e) | Cminor.Mem (_, e) | Cminor.Exp_cost (_, e) ->84 [expression_right f_expr e]85 | Cminor.Op2 (_, e1, e2) ->86 let res2 = expression_right f_expr e2 in87 let res1 = expression_right f_expr e1 in88 [res2 ; res1]89 | Cminor.Cond (e1, e2, e3) ->90 let res3 = expression_right f_expr e3 in91 let res2 = expression_right f_expr e2 in92 let res1 = expression_right f_expr e1 in93 [res3 ; res2 ; res1]94 in95 f_expr subexpr_res e96 31 97 let map_right f = 98 let rec aux = function 99 | [] -> [] 100 | e :: l -> let res = (aux l) in (f e) :: res 101 in 102 aux 32 let statement_subs = function 33 | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None 34 | Cminor.St_goto _ -> ([], []) 35 | Cminor.St_assign (_, e) | Cminor.St_switch (e, _, _) 36 | Cminor.St_return (Some e) -> ([e], []) 37 | Cminor.St_store (_, e1, e2) -> 38 ([e1 ; e2], []) 39 | Cminor.St_call (_, f, args, _) | Cminor.St_tailcall (f, args, _) -> 40 (f :: args, []) 41 | Cminor.St_seq (stmt1, stmt2) -> 42 ([], [stmt1 ; stmt2]) 43 | Cminor.St_ifthenelse (e, stmt1, stmt2) -> 44 ([e], [stmt1 ; stmt2]) 45 | Cminor.St_loop stmt | Cminor.St_block stmt 46 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) -> 47 ([], [stmt]) 103 48 104 (* In [statement_right f_expr f_stmt stmt], [f_stmt]'s second argument is the 105 list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and 106 [f_stmt]'s third argument is the list of [statement_left]'s results 107 on [stmt]'s sub-statements. The results are computed from right to left 108 following their appearance order in the [Cminor.statement] type. *) 49 let statement_fill_subs stmt sub_es sub_stmts = 50 match stmt, sub_es, sub_stmts with 51 | ( Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None 52 | Cminor.St_goto _), _, _ -> stmt 53 | Cminor.St_assign (x, _), e :: _, _ -> 54 Cminor.St_assign (x, e) 55 | Cminor.St_switch (_, cases, dflt), e :: _, _ -> 56 Cminor.St_switch (e, cases, dflt) 57 | Cminor.St_return _, e :: _, _ -> 58 Cminor.St_return (Some e) 59 | Cminor.St_store (size, _, _), e1 :: e2 :: _, _ -> 60 Cminor.St_store (size, e1, e2) 61 | Cminor.St_call (x_opt, _, _, sg), f :: args, _ -> 62 Cminor.St_call (x_opt, f, args, sg) 63 | Cminor.St_tailcall (_, _, sg), f :: args, _ -> 64 Cminor.St_tailcall (f, args, sg) 65 | Cminor.St_seq _, _, stmt1 :: stmt2 :: _ -> 66 Cminor.St_seq (stmt1, stmt2) 67 | Cminor.St_ifthenelse _, e :: _, stmt1 :: stmt2 :: _ -> 68 Cminor.St_ifthenelse (e, stmt1, stmt2) 69 | Cminor.St_loop _, _, stmt :: _ -> 70 Cminor.St_loop stmt 71 | Cminor.St_block _, _, stmt :: _ -> 72 Cminor.St_block stmt 73 | Cminor.St_label (lbl, _), _, stmt :: _ -> 74 Cminor.St_label (lbl, stmt) 75 | Cminor.St_cost (lbl, _), _, stmt :: _ -> 76 Cminor.St_cost (lbl, stmt) 77 | _ -> assert false (* do not use on these arguments *) 109 78 110 let rec statement_right f_expr f_stmt stmt = 111 let expr_res e = expression_right f_expr e in 112 let (subexpr_res, substmt_res) = match stmt with 113 | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_switch _ 114 | Cminor.St_return None | Cminor.St_goto _ -> ([], []) 115 | Cminor.St_assign (_, e) | Cminor.St_return (Some e) -> ([expr_res e], []) 116 | Cminor.St_store (_, e1, e2) -> 117 let res2 = expr_res e2 in 118 let res1 = expr_res e1 in 119 ([res2 ; res1], []) 120 | Cminor.St_call (_, f, args, _) | Cminor.St_tailcall (f, args, _) -> 121 let resargs = map_right expr_res args in 122 let resf = expr_res f in 123 (resargs @ [resf], []) 124 | Cminor.St_seq (stmt1, stmt2) -> 125 let res2 = statement_right f_expr f_stmt stmt2 in 126 let res1 = statement_right f_expr f_stmt stmt1 in 127 ([], [res2 ; res1]) 128 | Cminor.St_ifthenelse (e, stmt1, stmt2) -> 129 let res2 = statement_right f_expr f_stmt stmt2 in 130 let res1 = statement_right f_expr f_stmt stmt1 in 131 let rese = expr_res e in 132 ([rese], [res2 ; res1]) 133 | Cminor.St_loop stmt | Cminor.St_block stmt 134 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) -> 135 ([], [statement_right f_expr f_stmt stmt]) 136 in 137 f_stmt subexpr_res substmt_res stmt 79 (* In [statement f_expr f_stmt stmt], [f_stmt]'s second argument is the 80 list of [expression f_expr]'s results on [stmt]'s sub-expressions, and 81 [f_stmt]'s third argument is the list of [statement]'s results 82 on [stmt]'s sub-statements. *) 83 84 let rec statement f_expr f_stmt stmt = 85 let (sub_es, sub_stmts) = statement_subs stmt in 86 let sub_es_res = List.map (expression f_expr) sub_es in 87 let sub_stmts_res = List.map (statement f_expr f_stmt) sub_stmts in 88 f_stmt stmt sub_es_res sub_stmts_res -
Deliverables/D2.2/8051/src/cminor/cminorFold.mli
r486 r818 3 3 [Cminor]'s AST. *) 4 4 5 (* In [expression_left f e], [f]'s second argument is the list of 6 [expression_left]'s results on [e]'s sub-expressions. The results are 7 computed from left to right following their appearance order in the 8 [Cminor.expression] type. *) 5 val expression_subs : Cminor.expression -> Cminor.expression list 9 6 10 val expression_left : (Cminor.expression -> 'a list -> 'a) -> 11 Cminor.expression -> 12 'a 7 val expression_fill_subs : Cminor.expression -> Cminor.expression list -> 8 Cminor.expression 13 9 14 (* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the 15 list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and 16 [f_stmt]'s third argument is the list of [statement_left]'s results 17 on [stmt]'s sub-statements. The results are computed from left to right 18 following their appearance order in the [Cminor.statement] type. *) 10 (* In [expression f e], [f]'s second argument is the list of 11 [expression]'s results on [e]'s sub-expressions. *) 19 12 20 val statement_left : (Cminor.expression -> 'a list -> 'a) -> 21 (Cminor.statement -> 'a list -> 'b list -> 'b) -> 22 Cminor.statement -> 23 'b 13 val expression : (Cminor.expression -> 'a list -> 'a) -> 14 Cminor.expression -> 15 'a 24 16 17 val statement_subs : Cminor.statement -> 18 (Cminor.expression list * Cminor.statement list) 25 19 26 (* In [expression_right f e], [f]'s second argument is the list of 27 [expression_right]'s results on [e]'s sub-expressions. The results are28 computed from right to left following their appearance order in the29 [Cminor.expression] type. *)20 val statement_fill_subs : Cminor.statement -> 21 Cminor.expression list -> 22 Cminor.statement list -> 23 Cminor.statement 30 24 31 val expression_right : ('a list -> Cminor.expression -> 'a) -> 32 Cminor.expression -> 33 'a 25 (* In [statement f_expr f_stmt stmt], [f_stmt]'s second argument is the 26 list of [expression f_expr]'s results on [stmt]'s sub-expressions, and 27 [f_stmt]'s third argument is the list of [statement]'s results 28 on [stmt]'s sub-statements. *) 34 29 35 (* In [statement_right f_expr f_stmt stmt], [f_stmt]'s second argument is the 36 list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and 37 [f_stmt]'s third argument is the list of [statement_left]'s results 38 on [stmt]'s sub-statements. The results are computed from right to left 39 following their appearance order in the [Cminor.statement] type. *) 40 41 val statement_right : ('a list -> Cminor.expression -> 'a) -> 42 ('a list -> 'b list -> Cminor.statement -> 'b) -> 43 Cminor.statement -> 44 'b 30 val statement : (Cminor.expression -> 'a list -> 'a) -> 31 (Cminor.statement -> 'a list -> 'b list -> 'b) -> 32 Cminor.statement -> 33 'b -
Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml
r740 r818 3 3 4 4 module Mem = Driver.CminorMemory 5 module Val ue= Mem.Value5 module Val = Mem.Value 6 6 module LocalEnv = Map.Make(String) 7 type local_env = Val ue.t LocalEnv.t7 type local_env = Val.t LocalEnv.t 8 8 type memory = Cminor.function_def Mem.memory 9 9 … … 28 28 | Ct_endblock of continuation 29 29 | Ct_returnto of 30 ident option*internal_function*Val ue.address*local_env*continuation30 ident option*internal_function*Val.address*local_env*continuation 31 31 32 32 type state = 33 33 State_regular of 34 internal_function*statement*continuation*Val ue.address*local_env*(function_def Mem.memory)35 | State_call of function_def*Val ue.t list*continuation*(function_def Mem.memory)36 | State_return of Val ue.t*continuation*(function_def Mem.memory)34 internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory) 35 | State_call of function_def*Val.t list*continuation*(function_def Mem.memory) 36 | State_return of Val.t*continuation*(function_def Mem.memory) 37 37 38 38 let string_of_local_env lenv = 39 let f x v s = s ^ x ^ " = " ^ (Val ue.to_string v) ^ " " in39 let f x v s = s ^ x ^ " = " ^ (Val.to_string v) ^ " " in 40 40 LocalEnv.fold f lenv "" 41 41 … … 72 72 (string_of_local_env lenv) 73 73 (Mem.to_string mem) 74 (Val ue.to_string (value_of_address sp))74 (Val.to_string (value_of_address sp)) 75 75 (string_of_statement stmt) 76 76 | State_call (_, args, _, mem) -> 77 77 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!" 78 78 (Mem.to_string mem) 79 (MiscPottier.string_of_list " " Val ue.to_string args)79 (MiscPottier.string_of_list " " Val.to_string args) 80 80 | State_return (v, _, mem) -> 81 81 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 82 82 (Mem.to_string mem) 83 (Val ue.to_string v)83 (Val.to_string v) 84 84 85 85 … … 87 87 88 88 let init_local_env args params vars = 89 let f_param lenv xv = LocalEnv.add x v lenv in90 let f_var lenv x = LocalEnv.add x Value.undef lenv in89 let f_param lenv (x, _) v = LocalEnv.add x v lenv in 90 let f_var lenv (x, _) = LocalEnv.add x Val.undef lenv in 91 91 let lenv = List.fold_left2 f_param LocalEnv.empty params args in 92 92 List.fold_left f_var lenv vars … … 99 99 (* Expression evaluation *) 100 100 101 let eval_constant stack m = function 102 | Cst_int i -> Value.of_int i 103 | Cst_float _ -> error_float () 104 | Cst_addrsymbol id when Mem.mem_global m id -> 105 value_of_address (Mem.find_global m id) 106 | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".") 107 | Cst_stackoffset o -> Value.add (value_of_address stack) (Value.of_int o) 108 109 let eval_unop = function 110 | Op_negf 111 | Op_absf 112 | Op_singleoffloat 113 | Op_intoffloat 114 | Op_intuoffloat 115 | Op_floatofint 116 | Op_floatofintu -> error_float () 117 | Op_cast8unsigned -> Value.cast8unsigned 118 | Op_cast8signed -> Value.cast8signed 119 | Op_cast16unsigned -> Value.cast16unsigned 120 | Op_cast16signed -> Value.cast16signed 121 | Op_negint -> Value.negint 122 | Op_notbool -> Value.notbool 123 | Op_notint -> Value.notint 124 | Op_id -> (fun v -> v) 125 | Op_ptrofint -> assert false (*Not supported yet*) 126 | Op_intofptr -> assert false (*Not supported yet*) 127 128 let eval_binop = function 129 | Op_add 130 | Op_addp -> Value.add 131 | Op_sub 132 | Op_subp -> Value.sub 133 | Op_mul -> Value.mul 134 | Op_div -> Value.div 135 | Op_divu -> Value.divu 136 | Op_mod -> Value.modulo 137 | Op_modu -> Value.modulou 138 | Op_and -> Value.and_op 139 | Op_or -> Value.or_op 140 | Op_xor -> Value.xor 141 | Op_shl -> Value.shl 142 | Op_shr -> Value.shr 143 | Op_shru -> Value.shru 144 | Op_addf 145 | Op_subf 146 | Op_mulf 147 | Op_divf 148 | Op_cmpf _ -> error_float () 149 | Op_cmp(Cmp_eq) 150 | Op_cmpp(Cmp_eq) -> Value.cmp_eq 151 | Op_cmp(Cmp_ne) 152 | Op_cmpp(Cmp_ne) -> Value.cmp_ne 153 | Op_cmp(Cmp_gt) 154 | Op_cmpp(Cmp_gt) -> Value.cmp_gt 155 | Op_cmp(Cmp_ge) 156 | Op_cmpp(Cmp_ge) -> Value.cmp_ge 157 | Op_cmp(Cmp_lt) 158 | Op_cmpp(Cmp_lt) -> Value.cmp_lt 159 | Op_cmp(Cmp_le) 160 | Op_cmpp(Cmp_le) -> Value.cmp_le 161 | Op_cmpu(Cmp_eq) -> Value.cmp_eq_u 162 | Op_cmpu(Cmp_ne) -> Value.cmp_ne_u 163 | Op_cmpu(Cmp_gt) -> Value.cmp_gt_u 164 | Op_cmpu(Cmp_ge) -> Value.cmp_ge_u 165 | Op_cmpu(Cmp_lt) -> Value.cmp_lt_u 166 | Op_cmpu(Cmp_le) -> Value.cmp_le_u 167 168 let rec eval_expression stack local_env memory = function 169 | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[]) 170 | Id x -> error ("unknown local variable " ^ x ^ ".") 171 | Cst(c) -> (eval_constant stack memory c,[]) 172 | Op1(op,arg) -> 173 let (v,l) = eval_expression stack local_env memory arg in 174 (eval_unop op v,l) 175 | Op2(op,arg1,arg2) -> 176 let (v1,l1) = eval_expression stack local_env memory arg1 in 177 let (v2,l2) = eval_expression stack local_env memory arg2 in 178 (eval_binop op v1 v2,l1@l2) 179 | Mem(q,a) -> 180 let (v,l) = eval_expression stack local_env memory a in 181 (Mem.loadq memory q (address_of_value v),l) 182 | Cond(a1,a2,a3) -> 183 let (v1,l1) = eval_expression stack local_env memory a1 in 184 if Value.is_true v1 then 185 let (v2,l2) = eval_expression stack local_env memory a2 in 186 (v2,l1@l2) 187 else 188 if Value.is_false v1 then 189 let (v3,l3) = eval_expression stack local_env memory a3 in 190 (v3,l1@l3) 191 else error "undefined conditional value." 192 | Exp_cost(lbl,e) -> 193 let (v,l) = eval_expression stack local_env memory e in 194 (v,l@[lbl]) 101 module Eval_op (M : Memory.S) = struct 102 103 let concrete_stacksize = M.concrete_size 104 105 let ext_fun_of_sign = function 106 | AST.Signed -> M.Value.sign_ext 107 | AST.Unsigned -> M.Value.zero_ext 108 109 let cast_to_std t v = match t with 110 | AST.Sig_int (size, sign) -> (ext_fun_of_sign sign) v size M.int_size 111 | AST.Sig_float _ -> error_float () 112 | AST.Sig_offset | AST.Sig_ptr -> v 113 114 let cast_from_std t v = match t with 115 | AST.Sig_int (size, _) -> (ext_fun_of_sign AST.Unsigned) v M.int_size size 116 | AST.Sig_float _ -> error_float () 117 | AST.Sig_offset | AST.Sig_ptr -> v 118 119 let cst mem sp t = function 120 | Cst_int i -> cast_to_std t (M.Value.of_int i) 121 | Cst_float _ -> error_float () 122 | Cst_addrsymbol id when M.mem_global mem id -> 123 value_of_address (M.find_global mem id) 124 | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".") 125 | Cst_stack -> value_of_address sp 126 | Cst_offset off -> M.Value.of_int (M.concrete_offset off) 127 | Cst_sizeof t' -> cast_to_std t (M.Value.of_int (M.concrete_size t')) 128 129 let fun_of_op1 = function 130 | Op_cast ((from_size, from_sign), to_size) -> 131 (fun v -> (ext_fun_of_sign from_sign) v from_size to_size) 132 | Op_negint -> M.Value.negint 133 | Op_notbool -> M.Value.notbool 134 | Op_notint -> M.Value.negint 135 | Op_id -> (fun v -> v) 136 | Op_ptrofint 137 | Op_intofptr -> 138 error "conversion between integers and pointers not supported yet." 139 140 let op1 ret_type t op v = 141 cast_from_std ret_type ((fun_of_op1 op) (cast_to_std t v)) 142 143 let fun_of_op2 = function 144 | Op_add | Op_addp -> M.Value.add 145 | Op_sub | Op_subp | Op_subpp -> M.Value.sub 146 | Op_mul -> M.Value.mul 147 | Op_div -> M.Value.div 148 | Op_divu -> M.Value.divu 149 | Op_mod -> M.Value.modulo 150 | Op_modu -> M.Value.modulou 151 | Op_and -> M.Value.and_op 152 | Op_or -> M.Value.or_op 153 | Op_xor -> M.Value.xor 154 | Op_shl -> M.Value.shl 155 | Op_shr -> M.Value.shr 156 | Op_shru -> M.Value.shru 157 | Op_cmp Cmp_eq | Op_cmpp Cmp_eq -> M.Value.cmp_eq 158 | Op_cmp Cmp_ne | Op_cmpp Cmp_ne -> M.Value.cmp_ne 159 | Op_cmp Cmp_gt | Op_cmpp Cmp_gt -> M.Value.cmp_gt 160 | Op_cmp Cmp_ge | Op_cmpp Cmp_ge -> M.Value.cmp_ge 161 | Op_cmp Cmp_lt | Op_cmpp Cmp_lt -> M.Value.cmp_lt 162 | Op_cmp Cmp_le | Op_cmpp Cmp_le -> M.Value.cmp_le 163 | Op_cmpu Cmp_eq -> M.Value.cmp_eq_u 164 | Op_cmpu Cmp_ne -> M.Value.cmp_ne_u 165 | Op_cmpu Cmp_gt -> M.Value.cmp_gt_u 166 | Op_cmpu Cmp_ge -> M.Value.cmp_ge_u 167 | Op_cmpu Cmp_lt -> M.Value.cmp_lt_u 168 | Op_cmpu Cmp_le -> M.Value.cmp_le_u 169 170 let op2 ret_type t1 t2 op2 v1 v2 = 171 let v1 = cast_to_std t1 v1 in 172 let v2 = cast_to_std t2 v2 in 173 cast_from_std ret_type ((fun_of_op2 op2) v1 v2) 174 end 175 176 module Eval = Eval_op (Mem) 177 178 let concrete_stacksize = Eval.concrete_stacksize 179 let eval_constant = Eval.cst 180 let eval_unop = Eval.op1 181 let eval_binop = Eval.op2 182 183 let type_of_expr (Cminor.Expr (_, t)) = t 184 185 let rec eval_expression stack local_env memory (Cminor.Expr (ed, t)) = 186 match ed with 187 | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[]) 188 | Id x -> error ("unknown local variable " ^ x ^ ".") 189 | Cst(c) -> (eval_constant memory stack t c,[]) 190 | Op1(op,arg) -> 191 let (v,l) = eval_expression stack local_env memory arg in 192 (eval_unop t (type_of_expr arg) op v,l) 193 | Op2(op, arg1, arg2) -> 194 let (v1,l1) = eval_expression stack local_env memory arg1 in 195 let (v2,l2) = eval_expression stack local_env memory arg2 in 196 (eval_binop t (type_of_expr arg1) (type_of_expr arg2) op v1 v2,l1@l2) 197 | Mem(q,a) -> 198 let (v,l) = eval_expression stack local_env memory a in 199 (Mem.loadq memory q (address_of_value v),l) 200 | Cond(a1,a2,a3) -> 201 let (v1,l1) = eval_expression stack local_env memory a1 in 202 if Val.is_true v1 then 203 let (v2,l2) = eval_expression stack local_env memory a2 in 204 (v2,l1@l2) 205 else 206 if Val.is_false v1 then 207 let (v3,l3) = eval_expression stack local_env memory a3 in 208 (v3,l1@l3) 209 else error "undefined conditional value." 210 | Exp_cost(lbl,e) -> 211 let (v,l) = eval_expression stack local_env memory e in 212 (v,l@[lbl]) 195 213 196 214 let eval_exprlist sp lenv mem es = … … 248 266 | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[]) 249 267 | St_skip, (Ct_returnto _ as k) -> 250 (State_return (Val ue.undef,k,Mem.free m sigma),[])268 (State_return (Val.undef,k,Mem.free m sigma),[]) 251 269 | St_skip,Ct_stop -> 252 (State_return (Val ue.undef,Ct_stop,Mem.free m sigma),[])270 (State_return (Val.undef,Ct_stop,Mem.free m sigma),[]) 253 271 | St_assign(x,exp),_ -> 254 272 let (v,l) = eval_expression sigma e m exp in … … 268 286 let (v,l) = eval_expression sigma e m exp in 269 287 let next_stmt = 270 if Val ue.is_true v then s1288 if Val.is_true v then s1 271 289 else 272 if Val ue.is_false v then s2290 if Val.is_false v then s2 273 291 else error "undefined conditional value." in 274 292 (State_regular(f,next_stmt,k,sigma,e,m),l) … … 285 303 | St_switch(exp,lst,def),_ -> 286 304 let (v,l) = eval_expression sigma e m exp in 287 if Val ue.is_int v then305 if Val.is_int v then 288 306 try 289 let i = Val ue.to_int v in307 let i = Val.to_int v in 290 308 let nb_exit = 291 309 if List.mem_assoc i lst then List.assoc i lst … … 295 313 else error "undefined switch value." 296 314 | St_return(None),_ -> 297 (State_return (Val ue.undef,callcont k,Mem.free m sigma),[])315 (State_return (Val.undef,callcont k,Mem.free m sigma),[]) 298 316 | St_return(Some(a)),_ -> 299 317 let (v,l) = eval_expression sigma e m a in … … 307 325 let interpret_external k mem f args = 308 326 let (mem', v) = match InterpretExternal.t mem f args with 309 | (mem', InterpretExternal.V v) -> (mem', v) 327 | (mem', InterpretExternal.V vs) -> 328 let v = if List.length vs = 0 then Val.undef else List.hd vs in 329 (mem', v) 310 330 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in 311 331 State_return (v, k, mem') … … 313 333 let step_call vargs k m = function 314 334 | F_int f -> 315 let (m, sp) = Mem.alloc m f.f_stacksizein335 let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in 316 336 let lenv = init_local_env vargs f.f_params f.f_vars in 317 337 State_regular(f,f.f_body,k,sp,lenv,m) … … 330 350 331 351 let init_mem prog = 332 let f_var mem (x, init_datas) = Mem.add_var mem xinit_datas in352 let f_var mem (x, size, init_datas) = Mem.add_var mem x size init_datas in 333 353 let mem = List.fold_left f_var Mem.empty prog.vars in 334 354 let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in … … 336 356 337 357 let compute_result v = 338 if Val ue.is_int v then IntValue.Int8.cast (Value.to_int_repr v)339 else IntValue.Int 8.zero358 if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v) 359 else IntValue.Int32.zero 340 360 341 361 let rec exec debug trace (state, l) = … … 343 363 let print_and_return_result res = 344 364 if debug then Printf.printf "Result = %s\n%!" 345 (IntValue.Int 8.to_string res) ;365 (IntValue.Int32.to_string res) ; 346 366 (res, cost_labels) in 347 367 if debug then print_state state ; … … 350 370 print_and_return_result (compute_result v) 351 371 | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *) 352 print_and_return_result IntValue.Int 8.zero372 print_and_return_result IntValue.Int32.zero 353 373 | state -> exec debug cost_labels (step state) 354 374 355 375 let interpret debug prog = 356 if debug then Printf.printf "*** Cminor ***\n\n%!" ;376 Printf.printf "*** Cminor interpret ***\n%!" ; 357 377 match prog.main with 358 | None -> (IntValue.Int 8.zero, [])378 | None -> (IntValue.Int32.zero, []) 359 379 | Some main -> 360 380 let mem = init_mem prog in -
Deliverables/D2.2/8051/src/cminor/cminorInterpret.mli
r486 r818 3 3 also print debug informations. *) 4 4 5 module Eval_op (M : Memory.S) : sig 6 val concrete_stacksize : AST.abstract_size -> int 7 val cst : 8 'a M.memory -> M.Value.address -> AST.sig_type -> AST.cst -> M.Value.t 9 val op1 : 10 AST.sig_type (* returned type *) -> AST.sig_type -> AST.op1 -> M.Value.t -> 11 M.Value.t 12 val op2 : 13 AST.sig_type (* returned type *) -> AST.sig_type -> AST.sig_type -> 14 AST.op2 -> M.Value.t -> M.Value.t -> M.Value.t 15 end 16 5 17 val interpret : bool -> Cminor.program -> AST.trace -
Deliverables/D2.2/8051/src/cminor/cminorLabelling.ml
r486 r818 73 73 74 74 let add_cost_labels_body cost_universe stmt = 75 CminorFold.statement _left75 CminorFold.statement 76 76 (f_add_cost_labels_exp cost_universe) 77 77 (f_add_cost_labels_body cost_universe) -
Deliverables/D2.2/8051/src/cminor/cminorLexer.mll
r740 r818 72 72 (* | "in" { IN } *) 73 73 | "int" { INT } 74 | "int8" { INT8 } 74 75 | "int16" { INT16 } 75 | "int16s" { INT16S }76 | "int16u" { INT16U }77 76 | "int32" { INT32 } 78 | "int8" { INT8 } 79 | "int8s" { INT8S } 80 | "int8u" { INT8U } 77 | "int8sto8" { INT8STO8 } 78 | "int8sto16" { INT8STO16 } 79 | "int8sto32" { INT8STO32 } 80 | "int8uto8" { INT8UTO8 } 81 | "int8uto16" { INT8UTO16 } 82 | "int8uto32" { INT8UTO32 } 83 | "int16sto8" { INT16STO8 } 84 | "int16sto16" { INT16STO16 } 85 | "int16sto32" { INT16STO32 } 86 | "int16uto8" { INT16UTO8 } 87 | "int16uto16" { INT16UTO16 } 88 | "int16uto32" { INT16UTO32 } 89 | "int32sto8" { INT32STO8 } 90 | "int32sto16" { INT32STO16 } 91 | "int32sto32" { INT32STO32 } 92 | "int32uto8" { INT32UTO8 } 93 | "int32uto16" { INT32UTO16 } 94 | "int32uto32" { INT32UTO32 } 81 95 | "intoffloat" { INTOFFLOAT } 82 96 | "intuoffloat" { INTUOFFLOAT } -
Deliverables/D2.2/8051/src/cminor/cminorParser.mly
r740 r818 25 25 open Cminor 26 26 open Memory 27 28 let error_prefix = "Cminor parser" 29 let error s = Error.global_error error_prefix s 30 let warning s = Error.warning error_prefix s 31 let error_float () = error "float not supported." 32 33 let uint32 = (4, Unsigned) 34 let int32 = (4, Signed) 27 35 28 36 (* Function calls are not allowed in the AST of expressions, but function … … 269 277 %token IF 270 278 %token INT 279 %token INT8 271 280 %token INT16 272 %token INT16S273 %token INT16U274 281 %token INT32 275 %token INT8 276 %token INT8S 277 %token INT8U 282 %token INT8STO8 283 %token INT8STO16 284 %token INT8STO32 285 %token INT8UTO8 286 %token INT8UTO16 287 %token INT8UTO32 288 %token INT16STO8 289 %token INT16STO16 290 %token INT16STO32 291 %token INT16UTO8 292 %token INT16UTO16 293 %token INT16UTO32 294 %token INT32STO8 295 %token INT32STO16 296 %token INT32STO32 297 %token INT32UTO8 298 %token INT32UTO16 299 %token INT32UTO32 278 300 %token <int> INTLIT 279 301 %token INTOFFLOAT … … 339 361 %left PLUS PLUSF MINUS MINUSF 340 362 %left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU 341 %nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16UFLOAT32 /* ALLOC */363 %nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU FLOAT32 /* ALLOC */ 342 364 %left LPAREN 343 365 … … 522 544 | STRINGLIT { RCst (Cst_addrsymbol $1) } 523 545 | AMPERSAND INTLIT { RCst (Cst_stackoffset $2) } 524 | MINUS expr %prec p_uminus { ROp1 (Op_negint , $2) }525 | MINUSF expr %prec p_uminus { ROp1 (Op_negf, $2) }526 | ABSF expr { ROp1 (Op_absf, $2) }527 | INTOFFLOAT expr { ROp1 (Op_intoffloat, $2) }528 | INTUOFFLOAT expr { ROp1 (Op_intuoffloat, $2) }529 | FLOATOFINT expr { ROp1 (Op_floatofint, $2) }530 | FLOATOFINTU expr { ROp1 (Op_floatofintu, $2) }531 | TILDE expr { ROp1 (Op_notint , $2) }546 | MINUS expr %prec p_uminus { ROp1 (Op_negint int32, $2) } 547 | MINUSF expr %prec p_uminus { error_float () } 548 | ABSF expr { error_float () } 549 | INTOFFLOAT expr { error_float () } 550 | INTUOFFLOAT expr { error_float () } 551 | FLOATOFINT expr { error_float () } 552 | FLOATOFINTU expr { error_float () } 553 | TILDE expr { ROp1 (Op_notint int32, $2) } 532 554 | BANG expr { ROp1 (Op_notbool, $2) } 533 | INT8S expr { ROp1 (Op_cast8signed, $2) } 534 | INT8U expr { ROp1 (Op_cast8unsigned, $2) } 535 | INT16S expr { ROp1 (Op_cast16signed, $2) } 536 | INT16U expr { ROp1 (Op_cast16unsigned, $2) } 537 | FLOAT32 expr { ROp1 (Op_singleoffloat, $2) } 538 | expr PLUS expr { ROp2 (Op_add, $1, $3) } 539 | expr MINUS expr { ROp2 (Op_sub, $1, $3) } 540 | expr STAR expr { ROp2 (Op_mul, $1, $3) } 541 | expr SLASH expr { ROp2 (Op_div, $1, $3) } 542 | expr PERCENT expr { ROp2 (Op_mod, $1, $3) } 543 | expr SLASHU expr { ROp2 (Op_divu, $1, $3) } 544 | expr PERCENTU expr { ROp2 (Op_modu, $1, $3) } 555 | INT8STO8 expr { ROp1 (Op_cast ((8, Signed), 8), $2) } 556 | INT8STO16 expr { ROp1 (Op_cast ((8, Signed), 16), $2) } 557 | INT8STO32 expr { ROp1 (Op_cast ((8, Signed), 32), $2) } 558 | INT8UTO8 expr { ROp1 (Op_cast ((8, Unsigned), 8), $2) } 559 | INT8UTO16 expr { ROp1 (Op_cast ((8, Unsigned), 16), $2) } 560 | INT8UTO32 expr { ROp1 (Op_cast ((8, Unsigned), 32), $2) } 561 | INT16STO8 expr { ROp1 (Op_cast ((16, Signed), 16), $2) } 562 | INT16STO16 expr { ROp1 (Op_cast ((16, Signed), 16), $2) } 563 | INT16STO32 expr { ROp1 (Op_cast ((16, Signed), 32), $2) } 564 | INT16UTO8 expr { ROp1 (Op_cast ((16, Unsigned), 8), $2) } 565 | INT16UTO16 expr { ROp1 (Op_cast ((16, Unsigned), 16), $2) } 566 | INT16UTO32 expr { ROp1 (Op_cast ((16, Unsigned), 32), $2) } 567 | INT32STO8 expr { ROp1 (Op_cast ((32, Signed), 8), $2) } 568 | INT32STO16 expr { ROp1 (Op_cast ((32, Signed), 16), $2) } 569 | INT32STO32 expr { ROp1 (Op_cast ((32, Signed), 32), $2) } 570 | INT32UTO8 expr { ROp1 (Op_cast ((32, Unsigned), 8), $2) } 571 | INT32UTO16 expr { ROp1 (Op_cast ((32, Unsigned), 16), $2) } 572 | INT32UTO32 expr { ROp1 (Op_cast ((32, Unsigned), 32), $2) } 573 | FLOAT32 expr { error_float () } 574 | expr PLUS expr { ROp2 (Op_add int32, $1, $3) } 575 | expr MINUS expr { ROp2 (Op_sub int32, $1, $3) } 576 | expr STAR expr { ROp2 (Op_mul int32, $1, $3) } 577 | expr SLASH expr { ROp2 (Op_div int32, $1, $3) } 578 | expr PERCENT expr { ROp2 (Op_mod int32, $1, $3) } 579 | expr SLASHU expr { ROp2 (Op_div uint32, $1, $3) } 580 | expr PERCENTU expr { ROp2 (Op_mod uint32, $1, $3) } 545 581 | expr AMPERSAND expr { ROp2 (Op_and, $1, $3) } 546 582 | expr BAR expr { ROp2 (Op_or, $1, $3) } 547 583 | expr CARET expr { ROp2 (Op_xor, $1, $3) } 548 | expr LESSLESS expr { ROp2 (Op_shl , $1, $3) }549 | expr GREATERGREATER expr { ROp2 (Op_shr , $1, $3) }550 | expr GREATERGREATERU expr { ROp2 (Op_shr u, $1, $3) }551 | expr PLUSF expr { ROp2 (Op_addf, $1, $3) }552 | expr MINUSF expr { ROp2 (Op_subf, $1, $3) }553 | expr STARF expr { ROp2 (Op_mulf, $1, $3) }554 | expr SLASHF expr { ROp2 (Op_divf, $1, $3) }555 | expr EQUALEQUAL expr { ROp2 (Op_cmp Cmp_eq, $1, $3) }556 | expr BANGEQUAL expr { ROp2 (Op_cmp Cmp_ne, $1, $3) }557 | expr LESS expr { ROp2 (Op_cmp Cmp_lt, $1, $3) }558 | expr LESSEQUAL expr { ROp2 (Op_cmp Cmp_le, $1, $3) }559 | expr GREATER expr { ROp2 (Op_cmp Cmp_gt, $1, $3) }560 | expr GREATEREQUAL expr { ROp2 (Op_cmp Cmp_ge, $1, $3) }561 | expr EQUALEQUALU expr { ROp2 (Op_cmpu Cmp_eq, $1, $3) }562 | expr BANGEQUALU expr { ROp2 (Op_cmpu Cmp_ne, $1, $3) }563 | expr LESSU expr { ROp2 (Op_cmpu Cmp_lt, $1, $3) }564 | expr LESSEQUALU expr { ROp2 (Op_cmpu Cmp_le, $1, $3) }565 | expr GREATERU expr { ROp2 (Op_cmpu Cmp_gt, $1, $3) }566 | expr GREATEREQUALU expr { ROp2 (Op_cmpu Cmp_ge, $1, $3) }567 | expr EQUALEQUALF expr { ROp2 (Op_cmpf Cmp_eq, $1, $3) }568 | expr BANGEQUALF expr { ROp2 (Op_cmpf Cmp_ne, $1, $3) }569 | expr LESSF expr { ROp2 (Op_cmpf Cmp_lt, $1, $3) }570 | expr LESSEQUALF expr { ROp2 (Op_cmpf Cmp_le, $1, $3) }571 | expr GREATERF expr { ROp2 (Op_cmpf Cmp_gt, $1, $3) }572 | expr GREATEREQUALF expr { ROp2 (Op_cmpf Cmp_ge, $1, $3) }584 | expr LESSLESS expr { ROp2 (Op_shl int32, $1, $3) } 585 | expr GREATERGREATER expr { ROp2 (Op_shr int32, $1, $3) } 586 | expr GREATERGREATERU expr { ROp2 (Op_shr uint32, $1, $3) } 587 | expr PLUSF expr { error_float () } 588 | expr MINUSF expr { error_float () } 589 | expr STARF expr { error_float () } 590 | expr SLASHF expr { error_float () } 591 | expr EQUALEQUAL expr { ROp2 (Op_cmp (Cmp_eq, int32), $1, $3) } 592 | expr BANGEQUAL expr { ROp2 (Op_cmp (Cmp_ne, int32), $1, $3) } 593 | expr LESS expr { ROp2 (Op_cmp (Cmp_lt, int32), $1, $3) } 594 | expr LESSEQUAL expr { ROp2 (Op_cmp (Cmp_le, int32), $1, $3) } 595 | expr GREATER expr { ROp2 (Op_cmp (Cmp_gt, int32), $1, $3) } 596 | expr GREATEREQUAL expr { ROp2 (Op_cmp (Cmp_ge, int32), $1, $3) } 597 | expr EQUALEQUALU expr { ROp2 (Op_cmp (Cmp_eq, uint32), $1, $3) } 598 | expr BANGEQUALU expr { ROp2 (Op_cmp (Cmp_ne, uint32), $1, $3) } 599 | expr LESSU expr { ROp2 (Op_cmp (Cmp_lt, uint32), $1, $3) } 600 | expr LESSEQUALU expr { ROp2 (Op_cmp (Cmp_le, uint32), $1, $3) } 601 | expr GREATERU expr { ROp2 (Op_cmp (Cmp_gt, uint32), $1, $3) } 602 | expr GREATEREQUALU expr { ROp2 (Op_cmp (Cmp_ge, uint32), $1, $3) } 603 | expr EQUALEQUALF expr { error_float () } 604 | expr BANGEQUALF expr { error_float () } 605 | expr LESSF expr { error_float () } 606 | expr LESSEQUALF expr { error_float () } 607 | expr GREATERF expr { error_float () } 608 | expr GREATEREQUALF expr { error_float () } 573 609 | quantity LBRACKET expr RBRACKET { RMem ($1, $3) } 574 610 | expr AMPERSANDAMPERSAND expr { RCond ($1, $3, RCst (Cst_int 0)) } -
Deliverables/D2.2/8051/src/cminor/cminorPrinter.ml
r740 r818 1 1 open AST 2 2 3 let print_type = function 4 | Sig_int -> "int" 5 | Sig_float -> "float" 6 | Sig_ptr -> "ptr" 7 8 let print_ret_type = function 9 | Type_ret t -> print_type t 10 | Type_void -> "void" 11 12 let print_sig sg = 13 let rec aux = function 14 | [] -> "" 15 | [t] -> (print_type t) ^ " -> " 16 | t :: sg -> (print_type t) ^ " -> " ^ (aux sg) 17 in 18 (aux sg.args) ^ (print_ret_type sg.res) 19 3 4 let rec print_size = function 5 | AST.SQ q -> Memory.string_of_quantity q 6 | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}" 7 | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}" 8 | AST.SArray (i, se) -> 9 (print_size se) ^ "[" ^ (string_of_int i) ^ "]" 10 and print_size_list l = 11 MiscPottier.string_of_list ", " print_size l 12 13 let print_stacksize = print_size 14 15 let print_offset (size, depth) = 16 "offset[" ^ (print_size size) ^ ", " ^ (string_of_int depth) ^ "]" 17 18 let print_sizeof = print_size 19 20 let print_global_size = print_size 20 21 21 22 let print_data = function 23 (* 22 24 | Data_reserve n -> Printf.sprintf "[%d]" n 25 *) 23 26 | Data_int8 i -> Printf.sprintf "(int8) %d" i 24 27 | Data_int16 i -> Printf.sprintf "(int16) %d" i … … 35 38 Printf.sprintf "{%s}" (aux init) 36 39 37 let print_var (id, init) = 38 Printf.sprintf "var \"%s\" %s\n" id (print_datas init) 40 let print_datas_opt = function 41 | None -> "" 42 | Some init -> " = " ^ (print_datas init) 43 44 let print_var (id, size, init_opt) = 45 Printf.sprintf "var \"%s\" : %s%s;\n" 46 id (print_global_size size) (print_datas_opt init_opt) 39 47 40 48 let print_vars = List.fold_left (fun s v -> s ^ (print_var v)) "" … … 44 52 | Cst_float f -> string_of_float f 45 53 | Cst_addrsymbol id -> "\"" ^ id ^ "\"" 46 | Cst_stackoffset off -> "&" ^ (string_of_int off) 54 | Cst_stack -> "&0" 55 | Cst_offset off -> "{" ^ (print_offset off) ^ "}" 56 | Cst_sizeof t -> "sizeof (" ^ (print_sizeof t) ^ ")" 47 57 48 58 let print_cmp = function … … 55 65 56 66 let print_op1 = function 57 | Op_cast8unsigned -> "int8u" 58 | Op_cast8signed -> "int8s" 59 | Op_cast16unsigned -> "int16u" 60 | Op_cast16signed -> "int16s" 67 | Op_cast ((src_size, sign), dest_size) -> 68 Printf.sprintf "int%s%sto%s" 69 (Primitive.print_size src_size) 70 (Primitive.print_signedness sign) 71 (Primitive.print_size dest_size) 61 72 | Op_negint -> "-" 62 73 | Op_notbool -> "!" 63 74 | Op_notint -> "~" 64 | Op_negf -> "-f"65 | Op_absf -> "absf"66 | Op_singleoffloat -> "float32"67 | Op_intoffloat -> "intoffloat"68 | Op_intuoffloat -> "intuoffloat"69 | Op_floatofint -> "floatofint"70 | Op_floatofintu -> "floatofintu"71 75 | Op_id -> "" 72 76 | Op_intofptr -> "intofptr" … … 87 91 | Op_shr -> ">>" 88 92 | Op_shru -> ">>u" 89 | Op_addf -> "+f"90 | Op_subf -> "-f"91 | Op_mulf -> "*f"92 | Op_divf -> "/f"93 93 | Op_cmp cmp -> print_cmp cmp 94 94 | Op_cmpu cmp -> (print_cmp cmp) ^ "u" 95 | Op_cmpf cmp -> (print_cmp cmp) ^ "f"96 95 | Op_addp -> "+p" 97 96 | Op_subp -> "-p" 97 | Op_subpp -> "-pp" 98 98 | Op_cmpp cmp -> (print_cmp cmp) ^ "p" 99 99 100 let rec print_expression = function100 let rec print_expression (Cminor.Expr (ed, _)) = match ed with 101 101 | Cminor.Id id -> id 102 102 | Cminor.Cst cst -> print_constant cst 103 103 | Cminor.Op1 (op1, e) -> 104 Printf.sprintf "%s %s" (print_op1 op1) (add_parenthesis e)104 Printf.sprintf "%s %s" (print_op1 op1) (add_parenthesis e) 105 105 | Cminor.Op2 (op2, e1, e2) -> 106 106 Printf.sprintf "%s %s %s" … … 117 117 | Cminor.Exp_cost (lab, e) -> 118 118 Printf.sprintf "/* %s */ %s" lab (print_expression e) 119 and add_parenthesis e = match ewith119 and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with 120 120 | Cminor.Id _ | Cminor.Cst _ | Cminor.Mem _ -> print_expression e 121 121 | _ -> Printf.sprintf "(%s)" (print_expression e) 122 122 123 123 124 let rec print_args = function 125 | [] -> "" 126 | [e] -> print_expression e 127 | e :: args -> (print_expression e) ^ ", " ^ (print_args args) 124 let print_args = 125 MiscPottier.string_of_list ", " print_expression 126 127 let print_decl (x, t) = (Primitive.print_type t) ^ " " ^ x 128 129 let print_decls vars = 130 MiscPottier.string_of_list ", " print_decl vars 128 131 129 132 130 133 let n_spaces n = String.make n ' ' 131 132 133 let print_locals vars =134 (MiscPottier.string_of_list ", " (fun x -> x) vars ^135 (if vars = [] then "" else ";"))136 134 137 135 … … 158 156 (print_expression f) 159 157 (print_args args) 160 ( print_sig sg)158 (Primitive.print_sig sg) 161 159 | Cminor.St_call (Some id, f, args, sg) -> 162 160 Printf.sprintf "%s%s = %s(%s) : %s;\n" … … 165 163 (print_expression f) 166 164 (print_args args) 167 ( print_sig sg)165 (Primitive.print_sig sg) 168 166 | Cminor.St_tailcall (f, args, sg) -> 169 167 Printf.sprintf "%stailcall %s(%s) : %s;\n" … … 171 169 (print_expression f) 172 170 (print_args args) 173 ( print_sig sg)171 (Primitive.print_sig sg) 174 172 | Cminor.St_seq (s1, s2) -> (print_body n s1) ^ (print_body n s2) 175 173 | Cminor.St_ifthenelse (e, s1, s2) -> … … 214 212 215 213 let print_internal f_name f_def = 216 Printf.sprintf "\"%s\" (%s) : %s {\n\n stack %d;\n\n vars: %s\n pointers: %s\n\n%s}\n\n\n"214 Printf.sprintf "\"%s\" (%s) : %s {\n\n stack: %s\n\n vars: %s;\n\n%s}\n\n\n" 217 215 f_name 218 (print_args (List.map (fun id -> Cminor.Id id) f_def.Cminor.f_params)) 219 (print_sig f_def.Cminor.f_sig) 220 f_def.Cminor.f_stacksize 221 (print_locals f_def.Cminor.f_vars) 222 (print_locals f_def.Cminor.f_ptrs) 216 (print_decls f_def.Cminor.f_params) 217 (Primitive.print_type_return f_def.Cminor.f_return) 218 (print_stacksize f_def.Cminor.f_stacksize) 219 (print_decls f_def.Cminor.f_vars) 223 220 (print_body 2 f_def.Cminor.f_body) 224 221 … … 227 224 Printf.sprintf "extern \"%s\" : %s\n\n\n" 228 225 f_name 229 ( print_sig f_def.ef_sig)226 (Primitive.print_sig f_def.ef_sig) 230 227 231 228 -
Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml
r740 r818 12 12 (* Helper functions *) 13 13 14 let is_pointer_op1 = function 15 | AST.Op_cast8unsigned | AST.Op_cast8signed | AST.Op_cast16unsigned 16 | AST.Op_cast16signed | AST.Op_negint | AST.Op_notbool | AST.Op_notint 17 | AST.Op_intoffloat | AST.Op_intuoffloat | AST.Op_intofptr 18 | AST.Op_negf | AST.Op_absf | AST.Op_singleoffloat | AST.Op_floatofint 19 | AST.Op_floatofintu -> 20 false 21 | AST.Op_ptrofint -> 22 true 23 | AST.Op_id -> 24 assert false (* Dependent on argument. Treated in type_of_expr. *) 25 26 let is_pointer_op2 = function 27 | AST.Op_add | AST.Op_sub | AST.Op_mul | AST.Op_div | AST.Op_divu | AST.Op_mod 28 | AST.Op_modu | AST.Op_and | AST.Op_or | AST.Op_xor | AST.Op_shl | AST.Op_shr 29 | AST.Op_shru 30 | AST.Op_addf | AST.Op_subf | AST.Op_mulf | AST.Op_divf 31 | AST.Op_cmp _ | AST.Op_cmpu _ | AST.Op_cmpf _ | AST.Op_cmpp _ -> 32 false 33 | AST.Op_addp | AST.Op_subp -> 34 true 35 36 let rec is_pointer ptrs = function 37 | Cminor.Id x -> List.mem x ptrs 38 | Cminor.Cst (AST.Cst_int _) 39 | Cminor.Cst (AST.Cst_float _) -> false 40 | Cminor.Cst (AST.Cst_addrsymbol _) 41 | Cminor.Cst (AST.Cst_stackoffset _) -> true 42 | Cminor.Op1 (AST.Op_id, e) -> is_pointer ptrs e 43 | Cminor.Op1 (op1, _) -> is_pointer_op1 op1 44 | Cminor.Op2 (op2, _, _) -> is_pointer_op2 op2 45 | Cminor.Mem (q, _) -> q = Memory.QPtr 46 | Cminor.Cond _ -> false 47 | Cminor.Exp_cost (_, e) -> is_pointer ptrs e 48 49 let allocate (rtlabs_fun : RTLabs.internal_function) (is_pointer : bool) 14 let allocate (rtlabs_fun : RTLabs.internal_function) (sig_type : AST.sig_type) 50 15 : RTLabs.internal_function * Register.t = 51 16 let r = Register.fresh rtlabs_fun.RTLabs.f_runiverse in 17 let locals = rtlabs_fun.RTLabs.f_locals @ [(r, sig_type)] in 52 18 let rtlabs_fun = 53 { rtlabs_fun with RTLabs.f_locals = rtlabs_fun.RTLabs.f_locals @ [r] } in 54 let rtlabs_fun = 55 if is_pointer then 56 { rtlabs_fun with RTLabs.f_ptrs = rtlabs_fun.RTLabs.f_ptrs @ [r] } 57 else rtlabs_fun in 19 { rtlabs_fun with RTLabs.f_locals = locals } in 58 20 (rtlabs_fun, r) 59 21 22 let type_of (Cminor.Expr (_, t)) = t 23 60 24 let allocate_expr 61 (ptrs : AST.ident list)62 25 (rtlabs_fun : RTLabs.internal_function) 63 26 (e : Cminor.expression) 64 27 : (RTLabs.internal_function * Register.t) = 65 allocate rtlabs_fun ( is_pointer ptrse)28 allocate rtlabs_fun (type_of e) 66 29 67 30 type local_env = Register.t StringTools.Map.t … … 71 34 else error ("Unknown local \"" ^ x ^ "\".") 72 35 73 let find_olocal 74 (rtlabs_fun : RTLabs.internal_function) 75 (lenv : local_env) 76 (ox : AST.ident option) 77 : RTLabs.internal_function * Register.t = 36 let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t option = 78 37 match ox with 79 | None -> allocate rtlabs_fun false80 | Some x -> (rtlabs_fun,find_local lenv x)38 | None -> None 39 | Some x -> Some (find_local lenv x) 81 40 82 41 let choose_destination 83 (ptrs : AST.ident list)84 42 (rtlabs_fun : RTLabs.internal_function) 85 43 (lenv : local_env) … … 87 45 : RTLabs.internal_function * Register.t = 88 46 match e with 89 | Cminor. Id x-> (rtlabs_fun, find_local lenv x)90 | _ -> allocate_expr ptrsrtlabs_fun e47 | Cminor.Expr (Cminor.Id x, _) -> (rtlabs_fun, find_local lenv x) 48 | _ -> allocate_expr rtlabs_fun e 91 49 92 50 let choose_destinations 93 (ptrs : AST.ident list)94 51 (rtlabs_fun : RTLabs.internal_function) 95 52 (lenv : local_env) … … 97 54 : RTLabs.internal_function * Register.t list = 98 55 let f (rtlabs_fun, regs) e = 99 let (rtlabs_fun, r) = choose_destination ptrsrtlabs_fun lenv e in56 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in 100 57 (rtlabs_fun, regs @ [r]) in 101 58 List.fold_left f (rtlabs_fun, []) args … … 131 88 132 89 90 (* 133 91 (* [addressing e] returns the type of address represented by [e], 134 92 along with its arguments *) 135 93 136 let addressing ( e: Cminor.expression)94 let addressing (Cminor.Expr (ed, t) : Cminor.expression) 137 95 : (RTLabs.addressing * Cminor.expression list) = 138 match e with96 match ed with 139 97 | Cminor.Cst (AST.Cst_addrsymbol id) -> (RTLabs.Aglobal (id, 0), []) 140 98 | Cminor.Cst (AST.Cst_stackoffset n) -> (RTLabs.Ainstack n, []) 141 | Cminor.Op2 (AST.Op_add ,99 | Cminor.Op2 (AST.Op_addp _, 142 100 Cminor.Cst (AST.Cst_addrsymbol id), 143 101 Cminor.Cst (AST.Cst_int n)) -> 144 145 | Cminor.Op2 (AST.Op_add , e1, Cminor.Cst (AST.Cst_int n)) ->146 147 | Cminor.Op2 (AST.Op_add ,102 (RTLabs.Aglobal (id, n), []) 103 | Cminor.Op2 (AST.Op_addp _, e1, Cminor.Cst (AST.Cst_int n)) -> 104 (RTLabs.Aindexed n, [e1]) 105 | Cminor.Op2 (AST.Op_addp _, 148 106 Cminor.Cst (AST.Cst_addrsymbol id), 149 107 e2) -> 150 151 | Cminor.Op2 (AST.Op_add , e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2])108 (RTLabs.Abased (id, 0), [e2]) 109 | Cminor.Op2 (AST.Op_addp _, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2]) 152 110 | _ -> (RTLabs.Aindexed 0, [e]) 153 154 155 (* Translating conditions 156 157 [ptrs] is used for typing purposes (differencing from integers and 158 pointers). [rtlabs_fun] is the function being constructed. [lenv] is the 159 environment associating a pseudo-register to the variables of the program 160 being translated. *) 111 *) 112 113 114 (* Translating conditions *) 161 115 162 116 let rec translate_branch 163 (ptrs : AST.ident list)164 117 (rtlabs_fun : RTLabs.internal_function) 165 118 (lenv : local_env) … … 168 121 (lbl_false : Label.t) 169 122 : RTLabs.internal_function = 170 match e with 123 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in 124 let stmt = RTLabs.St_cond (r, lbl_true, lbl_false) in 125 let rtlabs_fun = generate rtlabs_fun stmt in 126 translate_expr rtlabs_fun lenv r e 127 128 (* 129 let Cminor.Expr (ed, t) = e in 130 match ed with 171 131 172 132 | Cminor.Id x -> … … 176 136 177 137 | Cminor.Cst cst -> 178 generate rtlabs_fun (RTLabs.St_condcst (cst, lbl_true, lbl_false))138 generate rtlabs_fun (RTLabs.St_condcst (cst, t, lbl_true, lbl_false)) 179 139 180 140 | Cminor.Op1 (op1, e) -> 181 let (rtlabs_fun, r) = choose_destination ptrsrtlabs_fun lenv e in141 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in 182 142 let stmt = RTLabs.St_cond1 (op1, r, lbl_true, lbl_false) in 183 143 let rtlabs_fun = generate rtlabs_fun stmt in 184 translate_expr ptrsrtlabs_fun lenv r e144 translate_expr rtlabs_fun lenv r e 185 145 186 146 | Cminor.Op2 (op2, e1, e2) -> 187 let (rtlabs_fun, r1) = choose_destination ptrsrtlabs_fun lenv e1 in188 let (rtlabs_fun, r2) = choose_destination ptrsrtlabs_fun lenv e2 in147 let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in 148 let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in 189 149 let stmt = RTLabs.St_cond2 (op2, r1, r2, lbl_true, lbl_false) in 190 150 let rtlabs_fun = generate rtlabs_fun stmt in 191 translate_exprs ptrsrtlabs_fun lenv [r1 ; r2] [e1 ; e2]151 translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2] 192 152 193 153 | _ -> 194 let (rtlabs_fun, r) = choose_destination ptrsrtlabs_fun lenv e in154 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in 195 155 let stmt = RTLabs.St_cond1 (AST.Op_id, r, lbl_true, lbl_false) in 196 156 let rtlabs_fun = generate rtlabs_fun stmt in 197 translate_expr ptrs rtlabs_fun lenv r e 198 199 (* Translating expressions 200 201 [ptrs] is used for typing purposes (differencing from integers and 202 pointers). [rtlabs_fun] is the function being constructed. [lenv] is the 203 environment associating a pseudo-register to the variables of the program 204 being translated. [destr] is the destination register. *) 157 translate_expr rtlabs_fun lenv r e 158 *) 159 160 (* Translating expressions *) 205 161 206 162 and translate_expr 207 (ptrs : AST.ident list)208 163 (rtlabs_fun : RTLabs.internal_function) 209 164 (lenv : local_env) … … 211 166 (e : Cminor.expression) 212 167 : RTLabs.internal_function = 213 match e with 168 let Cminor.Expr (ed, t) = e in 169 match ed with 214 170 215 171 | Cminor.Id x -> … … 228 184 229 185 | Cminor.Op1 (op1, e) -> 230 let (rtlabs_fun, r) = choose_destination ptrsrtlabs_fun lenv e in186 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in 231 187 let old_entry = rtlabs_fun.RTLabs.f_entry in 232 188 let stmt = RTLabs.St_op1 (op1, destr, r, old_entry) in 233 189 let rtlabs_fun = generate rtlabs_fun stmt in 234 translate_expr ptrsrtlabs_fun lenv r e190 translate_expr rtlabs_fun lenv r e 235 191 236 192 | Cminor.Op2 (op2, e1, e2) -> 237 let (rtlabs_fun, r1) = choose_destination ptrsrtlabs_fun lenv e1 in238 let (rtlabs_fun, r2) = choose_destination ptrsrtlabs_fun lenv e2 in193 let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in 194 let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in 239 195 let old_entry = rtlabs_fun.RTLabs.f_entry in 240 196 let stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in 241 197 let rtlabs_fun = generate rtlabs_fun stmt in 242 translate_exprs ptrsrtlabs_fun lenv [r1 ; r2] [e1 ; e2]198 translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2] 243 199 244 200 | Cminor.Mem (chunk, e) -> 245 let (mode, args) = addressing e in 246 let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in 247 let old_entry = rtlabs_fun.RTLabs.f_entry in 248 let stmt = RTLabs.St_load (chunk, mode, regs, destr, old_entry) in 249 let rtlabs_fun = generate rtlabs_fun stmt in 250 translate_exprs ptrs rtlabs_fun lenv regs args 201 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in 202 let old_entry = rtlabs_fun.RTLabs.f_entry in 203 let stmt = RTLabs.St_load (chunk, r, destr, old_entry) in 204 let rtlabs_fun = generate rtlabs_fun stmt in 205 translate_expr rtlabs_fun lenv r e 251 206 252 207 | Cminor.Cond (e1, e2, e3) -> 253 208 let old_entry = rtlabs_fun.RTLabs.f_entry in 254 let rtlabs_fun = translate_expr ptrsrtlabs_fun lenv destr e3 in209 let rtlabs_fun = translate_expr rtlabs_fun lenv destr e3 in 255 210 let lbl_false = rtlabs_fun.RTLabs.f_entry in 256 211 let rtlabs_fun = change_entry rtlabs_fun old_entry in 257 let rtlabs_fun = translate_expr ptrsrtlabs_fun lenv destr e2 in212 let rtlabs_fun = translate_expr rtlabs_fun lenv destr e2 in 258 213 let lbl_true = rtlabs_fun.RTLabs.f_entry in 259 translate_branch ptrsrtlabs_fun lenv e1 lbl_true lbl_false214 translate_branch rtlabs_fun lenv e1 lbl_true lbl_false 260 215 261 216 | Cminor.Exp_cost (lbl, e) -> 262 let rtlabs_fun = translate_expr ptrsrtlabs_fun lenv destr e in217 let rtlabs_fun = translate_expr rtlabs_fun lenv destr e in 263 218 let old_entry = rtlabs_fun.RTLabs.f_entry in 264 219 generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) 265 220 266 221 and translate_exprs 267 (ptrs : AST.ident list)268 222 (rtlabs_fun : RTLabs.internal_function) 269 223 (lenv : local_env) … … 271 225 (args : Cminor.expression list) 272 226 : RTLabs.internal_function = 273 let f destr e rtlabs_fun = translate_expr ptrsrtlabs_fun lenv destr e in227 let f destr e rtlabs_fun = translate_expr rtlabs_fun lenv destr e in 274 228 List.fold_right2 f regs args rtlabs_fun 275 229 276 230 231 (* 277 232 (* Switch transformation 278 233 … … 298 253 | [] -> Cminor.St_skip 299 254 | (case, exit) :: cases -> 300 301 Cminor.Op2 (AST.Op_cmp AST.Cmp_eq,302 303 304 305 255 let c = 256 Cminor.Op2 (AST.Op_cmp (AST.Cmp_eq, uint), 257 e, Cminor.Cst (AST.Cst_int case)) in 258 let stmt = 259 Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in 260 Cminor.St_seq (stmt, aux cases) 306 261 in 307 262 Cminor.St_seq (aux cases, Cminor.St_exit dfl) 308 309 310 (* Translating statements 311 312 [ptrs] is used for typing purposes (differencing from integers and 313 pointers). [rtlabs_fun] is the function being constructed. [lenv] is the 314 environment associating a pseudo-register to each variable of the function 315 being translated. [exists] is the list of label to exit to. The leftmost 316 label in the list is used to exit the closest block. *) 263 *) 264 265 266 (* Translating statements *) 317 267 318 268 let rec translate_stmt 319 (ptrs : AST.ident list)320 269 (rtlabs_fun : RTLabs.internal_function) 321 270 (lenv : local_env) … … 328 277 329 278 | Cminor.St_assign (x, e) -> 330 translate_expr ptrsrtlabs_fun lenv (find_local lenv x) e279 translate_expr rtlabs_fun lenv (find_local lenv x) e 331 280 332 281 | Cminor.St_store (chunk, e1, e2) -> 333 let ( mode, args) = addressinge1 in334 let (rtlabs_fun, r egs) = choose_destinations ptrs rtlabs_fun lenv argsin335 let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e2in336 let old_entry = rtlabs_fun.RTLabs.f_entryin337 let stmt = RTLabs.St_store (chunk, mode, regs, r, old_entry)in338 let rtlabs_fun = generate rtlabs_fun stmt in339 let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv r e2 in 340 translate_exprs ptrs rtlabs_fun lenv regs args341 342 | Cminor.St_call (oret, Cminor.Cst (AST.Cst_addrsymbol f),args, sg) ->343 let (rtlabs_fun, regs) = choose_destinations ptrsrtlabs_fun lenv args in344 let (rtlabs_fun, retr) = find_olocal rtlabs_funlenv oret in345 let old_entry = rtlabs_fun.RTLabs.f_entry in 346 let stmt = RTLabs.St_call_id (f, regs, retr, sg, old_entry) in347 let rtlabs_fun = generate rtlabs_fun stmt in 348 translate_exprs ptrsrtlabs_fun lenv regs args282 let (rtlabs_fun, addr) = choose_destination rtlabs_fun lenv e1 in 283 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in 284 let old_entry = rtlabs_fun.RTLabs.f_entry in 285 let stmt = RTLabs.St_store (chunk, addr, r, old_entry) in 286 let rtlabs_fun = generate rtlabs_fun stmt in 287 translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2] 288 289 | Cminor.St_call (oret, 290 Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _), 291 args, sg) -> 292 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in 293 let oretr = find_olocal lenv oret in 294 let old_entry = rtlabs_fun.RTLabs.f_entry in 295 let stmt = RTLabs.St_call_id (f, regs, oretr, sg, old_entry) in 296 let rtlabs_fun = generate rtlabs_fun stmt in 297 translate_exprs rtlabs_fun lenv regs args 349 298 350 299 | Cminor.St_call (oret, f, args, sg) -> 351 let (rtlabs_fun, fr) = choose_destination ptrsrtlabs_fun lenv f in352 let (rtlabs_fun, regs) = choose_destinations ptrsrtlabs_fun lenv args in353 let (rtlabs_fun, retr) = find_olocal rtlabs_funlenv oret in354 let old_entry = rtlabs_fun.RTLabs.f_entry in 355 let stmt = RTLabs.St_call_ptr (fr, regs, retr, sg, old_entry) in356 let rtlabs_fun = generate rtlabs_fun stmt in 357 let rtlabs_fun = translate_exprs ptrs rtlabs_fun lenv regs args in358 translate_expr ptrs rtlabs_fun lenv fr f 359 360 | Cminor.St_tailcall (Cminor.Cst (AST.Cst_addrsymbol f),args, sg) ->361 let (rtlabs_fun, regs) = choose_destinations ptrsrtlabs_fun lenv args in300 let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in 301 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in 302 let oretr = find_olocal lenv oret in 303 let old_entry = rtlabs_fun.RTLabs.f_entry in 304 let stmt = RTLabs.St_call_ptr (fr, regs, oretr, sg, old_entry) in 305 let rtlabs_fun = generate rtlabs_fun stmt in 306 translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args) 307 308 | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _), 309 args, sg) -> 310 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in 362 311 let stmt = RTLabs.St_tailcall_id (f, regs, sg) in 363 312 let rtlabs_fun = generate rtlabs_fun stmt in 364 translate_exprs ptrsrtlabs_fun lenv regs args313 translate_exprs rtlabs_fun lenv regs args 365 314 366 315 | Cminor.St_tailcall (f, args, sg) -> 367 let (rtlabs_fun, fr) = choose_destination ptrsrtlabs_fun lenv f in368 let (rtlabs_fun, regs) = choose_destinations ptrsrtlabs_fun lenv args in316 let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in 317 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in 369 318 let stmt = RTLabs.St_tailcall_ptr (fr, regs, sg) in 370 319 let rtlabs_fun = generate rtlabs_fun stmt in 371 let rtlabs_fun = translate_exprs ptrs rtlabs_fun lenv regs args in 372 translate_expr ptrs rtlabs_fun lenv fr f 320 translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args) 373 321 374 322 | Cminor.St_seq (s1, s2) -> 375 let rtlabs_fun = translate_stmt ptrsrtlabs_fun lenv exits s2 in376 translate_stmt ptrsrtlabs_fun lenv exits s1323 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in 324 translate_stmt rtlabs_fun lenv exits s1 377 325 378 326 | Cminor.St_ifthenelse (e, s1, s2) -> 379 327 let old_entry = rtlabs_fun.RTLabs.f_entry in 380 let rtlabs_fun = translate_stmt ptrsrtlabs_fun lenv exits s2 in328 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in 381 329 let lbl_false = rtlabs_fun.RTLabs.f_entry in 382 330 let rtlabs_fun = change_entry rtlabs_fun old_entry in 383 let rtlabs_fun = translate_stmt ptrsrtlabs_fun lenv exits s1 in331 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s1 in 384 332 let lbl_true = rtlabs_fun.RTLabs.f_entry in 385 translate_branch ptrsrtlabs_fun lenv e lbl_true lbl_false333 translate_branch rtlabs_fun lenv e lbl_true lbl_false 386 334 387 335 | Cminor.St_loop s -> 388 336 let loop_start = fresh_label rtlabs_fun in 389 337 let rtlabs_fun = change_entry rtlabs_fun loop_start in 390 let rtlabs_fun = translate_stmt ptrsrtlabs_fun lenv exits s in338 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in 391 339 let old_entry = rtlabs_fun.RTLabs.f_entry in 392 340 add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry) … … 394 342 | Cminor.St_block s -> 395 343 let old_entry = rtlabs_fun.RTLabs.f_entry in 396 translate_stmt ptrsrtlabs_fun lenv (old_entry :: exits) s344 translate_stmt rtlabs_fun lenv (old_entry :: exits) s 397 345 398 346 | Cminor.St_exit n -> … … 402 350 let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in 403 351 (match eopt, rtlabs_fun.RTLabs.f_result with 404 | None, _ -> rtlabs_fun 405 | Some e, retr -> translate_expr ptrs rtlabs_fun lenv retr e) 352 | None, None -> rtlabs_fun 353 | Some e, Some (retr, _) -> translate_expr rtlabs_fun lenv retr e 354 | _ -> assert false (* should be impossible *)) 406 355 407 356 | Cminor.St_switch (e, cases, dfl) -> 357 assert false (* should have been simplified before *) 358 (* 408 359 let stmt = transform_switch e cases dfl in 409 translate_stmt ptrs rtlabs_fun lenv exits stmt 360 translate_stmt rtlabs_fun lenv exits stmt 361 *) 410 362 411 363 | Cminor.St_label (lbl, s) -> 412 let rtlabs_fun = translate_stmt ptrsrtlabs_fun lenv exits s in364 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in 413 365 let old_entry = rtlabs_fun.RTLabs.f_entry in 414 366 add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry) 415 367 416 368 | Cminor.St_cost (lbl, s) -> 417 let rtlabs_fun = translate_stmt ptrsrtlabs_fun lenv exits s in369 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in 418 370 let old_entry = rtlabs_fun.RTLabs.f_entry in 419 371 generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) … … 432 384 - Extract the registers representing the formal variables 433 385 - Extract the registers representing the local variables 386 - Allocate a fresh register to hold the result of the function 434 387 - Allocate a fresh label representing the exit point 435 - Allocate fresh registers holding the result of the function436 388 - Initialize the graph with a return instruction at the end 437 389 - Complete the graph according to the function's body. … … 448 400 449 401 (* Local environment *) 450 let add_local lenv x=402 let add_local lenv (x, _) = 451 403 StringTools.Map.add x (Register.fresh runiverse) lenv in 452 404 let lenv = StringTools.Map.empty in 453 405 let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in 454 406 let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in 455 let lenv = List.fold_left add_local lenv f_def.Cminor.f_ptrs in456 407 457 408 let extract vars = 458 List.fold_left (fun l x -> l @ [StringTools.Map.find x lenv]) [] vars in 409 let f l (x, t) = l @ [(find_local lenv x, t)] in 410 List.fold_left f [] vars in 459 411 460 412 (* Parameter registers *) 461 413 let params = extract f_def.Cminor.f_params in 462 463 (* Local registers *) 464 let locals = extract (f_def.Cminor.f_vars @ f_def.Cminor.f_ptrs) in 465 466 (* Pointer registers *) 467 let ptrs = extract f_def.Cminor.f_ptrs in 414 415 (* Local registers *) 416 let locals = extract f_def.Cminor.f_vars in 417 418 (* [result] is the result of the body, if any. *) 419 let result = match f_def.Cminor.f_return with 420 | AST.Type_void -> None 421 | AST.Type_ret t -> Some (Register.fresh runiverse, t) in 422 423 let locals = 424 locals @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in 468 425 469 426 (* Exit label of the graph *) 470 427 let exit = Label.Gen.fresh luniverse in 471 428 472 (* [retr] is the register that holds the return value of the body, if any. *)473 let retr = Register.fresh runiverse in474 475 let locals = locals @ [retr] in476 477 429 (* The control flow graph: for now, it is only a return instruction at the 478 430 end. *) 479 let graph = Label.Map.add exit (RTLabs.St_return retr) Label.Map.empty in 431 let return = match result with 432 | None -> None 433 | Some (retr, _) -> Some retr in 434 let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in 480 435 481 436 let rtlabs_fun = 482 437 { RTLabs.f_luniverse = luniverse ; 483 438 RTLabs.f_runiverse = runiverse ; 484 RTLabs.f_sig = f_def.Cminor.f_sig ; 485 RTLabs.f_result = retr ; 439 RTLabs.f_result = result ; 486 440 RTLabs.f_params = params ; 487 441 RTLabs.f_locals = locals ; 488 RTLabs.f_ptrs = ptrs ;489 442 RTLabs.f_stacksize = f_def.Cminor.f_stacksize ; 490 443 RTLabs.f_graph = graph ; … … 493 446 494 447 (* Complete the graph *) 495 translate_stmt f_def.Cminor.f_ptrsrtlabs_fun lenv [] f_def.Cminor.f_body448 translate_stmt rtlabs_fun lenv [] f_def.Cminor.f_body 496 449 497 450 498 451 let translate_functions lbls (f_id, f_def) = match f_def with 499 452 | Cminor.F_int int_def -> 500 501 502 453 let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in 454 let def = translate_internal lbl_prefix int_def in 455 (f_id, RTLabs.F_int def) 503 456 | Cminor.F_ext def -> (f_id, RTLabs.F_ext def) 504 457 … … 506 459 (* Initialization of globals *) 507 460 508 let quantity_of_data data = 461 let sum_offsets = 462 let f res off = 463 let cst_off = 464 Cminor.Expr (Cminor.Cst (AST.Cst_offset off), AST.Sig_offset) in 465 Cminor.Expr (Cminor.Op2 (AST.Op_add, res, cst_off), AST.Sig_offset) in 466 List.fold_left f (Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset)) 467 468 let quantity_sig_of_data data = 509 469 let i = match data with 510 470 | AST.Data_int8 _ -> 1 … … 512 472 | AST.Data_int32 _ -> 4 513 473 | _ -> assert false (* do not use on these arguments *) in 514 Memory.QInt i515 516 let assign_data x stmt ( data, off) =517 let e = Cminor.Op2 (AST.Op_add,518 Cminor.Cst (AST.Cst_addrsymbol x), 519 Cminor.Cst (AST.Cst_int off)) in474 (AST.QInt i, AST.Sig_int (i, AST.Unsigned)) 475 476 let assign_data x stmt (offsets, data) = 477 let off = sum_offsets offsets in 478 let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in 479 let e = Cminor.Expr (Cminor.Op2 (AST.Op_addp, addr, off), AST.Sig_ptr) in 520 480 let stmt' = match data with 481 (* 521 482 | AST.Data_reserve _ -> Cminor.St_skip 483 *) 522 484 | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> 523 Cminor.St_store (quantity_of_data data, e, Cminor.Cst (AST.Cst_int i)) 485 let (quantity, etype) = quantity_sig_of_data data in 486 let cst = Cminor.Expr (Cminor.Cst (AST.Cst_int i), etype) in 487 Cminor.St_store (quantity, e, cst) 524 488 | AST.Data_float32 f | AST.Data_float64 f -> error_float () in 525 489 Cminor.St_seq (stmt, stmt') 526 490 527 491 let add_global_initializations_body vars body = 528 let f stmt (x, datas) = 529 let offs_of_datas = RTLabsMemory.offsets_of_datas datas in 530 List.fold_left (assign_data x) stmt offs_of_datas in 492 let f stmt (x, size, datas_opt) = match datas_opt with 493 | None -> Cminor.St_skip 494 | Some datas -> 495 let offsets = Memory.all_offsets size in 496 if List.length offsets <> List.length datas then 497 error "bad global initialization style." 498 else 499 let offs_datas = List.combine offsets datas in 500 List.fold_left (assign_data x) stmt offs_datas in 531 501 Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body) 532 502 533 503 let add_global_initializations_funct vars = function 534 504 | Cminor.F_int def -> 535 536 505 let f_body = add_global_initializations_body vars def.Cminor.f_body in 506 Cminor.F_int { def with Cminor.f_body = f_body } 537 507 | def -> def 538 508 … … 547 517 MiscPottier.update_list_assoc main main_def p.Cminor.functs 548 518 549 550 519 (* Translation of a Cminor program to a RTLabs program. *) 551 520 552 521 let translate p = 553 554 (* Fetch the variables in the program that are pointers (whose value is an555 address). Some architectures have different sizes for pointers and556 integers. *)557 let p = CminorPointers.fill p in558 522 559 523 (* Fetch the labels already used in the program to create new ones. *) … … 564 528 565 529 (* The globals are associated their size. *) 566 let f (id, datas) = (id, RTLabsMemory.size_of_datas datas) in530 let f (id, size, _) = (id, size) in 567 531 568 532 (* Put all this together and translate each function. *)
Note: See TracChangeset
for help on using the changeset viewer.
