Changeset 1539 for Deliverables/D2.2
- Timestamp:
- Nov 23, 2011, 1:55:12 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051-indexed-labels-branch/src
- Files:
-
- 60 edited
- 6 copied
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASM.mli
r1349 r1539 104 104 | `Cost of CostLabel.t 105 105 | `Index of int 106 | `Inc of int 106 | `Inc of int 107 107 | `Label of string 108 108 | `Jmp of string … … 127 127 incs : int BitVectors.WordMap.t ; (* loop index increments *) 128 128 cost_labels : CostLabel.t BitVectors.WordMap.t ; 129 labels : BitVectors.word StringTools.Map.t ; 130 129 131 exit_addr : BitVectors.word ; 130 132 has_main : bool } -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMCosts.ml
r643 r1539 50 50 warning 51 51 (Printf.sprintf 52 "Warning: branching to % s has cost %d, branching to %shas cost %d"53 ( string_of_int (BitVectors.int_of_vect pc1)) cost154 ( string_of_int (BitVectors.int_of_vect pc2)) cost2) ;52 "Warning: branching to %X has cost %d, branching to %X has cost %d" 53 (BitVectors.int_of_vect pc1) cost1 54 (BitVectors.int_of_vect pc2) cost2) ; 55 55 max cost1 (compare ((pc2, cost2) :: l)) 56 56 | _ :: l -> compare l -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.ml
r1357 r1539 133 133 134 134 (* 135 135 ind_0s : int BitVectors.WordMap.t; 136 136 ind_incs : int BitVectors.WordMap.t; 137 137 cost_labels : CostLabel.t BitVectors.WordMap.t … … 966 966 | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, inds, incs, costs 967 967 | `Cost s -> pc, exit_addr, labels, inds, incs, BitVectors.WordMap.add pc s costs 968 968 | `Index i -> pc, exit_addr, labels, BitVectors.WordMap.add pc i inds, incs, costs 969 969 | `Inc i -> pc, exit_addr, labels, inds, BitVectors.WordMap.add pc i incs, costs 970 | `Mov (_,_) -> (snd (half_add pc (vect_of_int 1 `Sixteen))), exit_addr, labels, inds, incs, costs 970 | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs 971 971 972 | `Jmp _ 972 973 | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs … … 986 987 (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen, 987 988 StringTools.Map.empty, BitVectors.WordMap.empty, BitVectors.WordMap.empty, 988 989 BitVectors.WordMap.empty) p.ASM.pcode 989 990 in 990 991 let code = … … 993 994 `Label _ 994 995 | `Cost _ 995 996 996 | `Index _ 997 | `Inc _ -> [] 997 998 | `WithLabel i -> 998 999 (* We need to expand a conditional jump to a label to a machine language … … 1046 1047 address, reconstructed 1047 1048 in 1048 let sjmp, jmp = `SJMP (`REL (vect_of_int 3 `Eight)), `LJMP (`ADDR16 jmp_address) in 1049 let sjmp = `SJMP (`REL (vect_of_int 3 `Eight)) in 1050 let jmp = `LJMP (`ADDR16 jmp_address) in 1049 1051 let translation = [ translated_jump; sjmp; jmp ] in 1050 1052 List.flatten (List.map assembly1 translation) 1051 1053 | `Mov (`DPTR,s) -> 1052 let addrr16 = StringTools.Map.find s datalabels in 1053 assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16))) 1054 (* let addr16 = StringTools.Map.find s datalabels in *) 1055 let addrr16 = 1056 try StringTools.Map.find s datalabels 1057 with Not_found -> StringTools.Map.find s labels in 1058 assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16))) 1054 1059 | `Jmp s -> 1055 1060 let pc_offset = StringTools.Map.find s labels in … … 1059 1064 assembly1 (`LCALL (`ADDR16 pc_offset )) 1060 1065 | #instruction as i -> assembly1 i) p.ASM.pcode) in 1061 { ASM.code = code ; ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ; 1066 { ASM.code = code ; 1067 ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ; 1068 ASM.labels = StringTools.Map.empty ; 1062 1069 ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main } 1063 1070 ;; … … 1988 1995 1989 1996 type cost_trace = { 1990 1991 1997 mutable ct_labels : CostLabel.t list; 1998 mutable ct_inds : CostLabel.const_indexing list; 1992 1999 } 1993 2000 1994 (* TODO: supposing only one index reset or increment per instruction *)2001 (* FIXME: supposing only one index reset or increment per instruction *) 1995 2002 let update_indexes trace p st = 1996 2003 try 1997 2004 let i = BitVectors.WordMap.find st.pc p.ASM.inds in 1998 2005 CostLabel.enter_loop trace.ct_inds i 1999 2006 with Not_found -> (); 2000 try2001 let i = BitVectors.WordMap.find st.pc p.ASM.incs in2002 CostLabel.continue_loop trace.ct_inds i2003 with Not_found -> ();2004 let instr,_,_ = fetch st.code_memory st.pc in2005 2006 2007 2008 2009 2010 2007 try 2008 let i = BitVectors.WordMap.find st.pc p.ASM.incs in 2009 CostLabel.continue_loop trace.ct_inds i 2010 with Not_found -> (); 2011 let instr,_,_ = fetch st.code_memory st.pc in 2012 match instr with 2013 | `ACALL _ | `LCALL _ -> 2014 trace.ct_inds <- CostLabel.new_const_ind trace.ct_inds 2015 | `RET -> 2016 trace.ct_inds <- CostLabel.forget_const_ind trace.ct_inds 2017 | _ -> () 2011 2018 2012 2019 let update_labels trace p st = 2013 2020 try 2014 2021 let cost_label = BitVectors.WordMap.find st.pc p.cost_labels in 2015 2016 2017 2022 let ind = CostLabel.curr_const_ind trace.ct_inds in 2023 let cost_label = CostLabel.ev_indexing ind cost_label in 2024 trace.ct_labels <- cost_label :: trace.ct_labels 2018 2025 with Not_found -> () 2019 2026 … … 2021 2028 2022 2029 let update_trace trace p st = 2023 2024 2030 update_labels trace p st; 2031 update_indexes trace p st; 2025 2032 if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st 2026 2033 … … 2048 2055 (res, List.rev trace.ct_labels) 2049 2056 else (IntValue.Int32.zero, []) 2057 2058 2059 let size_of_instr instr = 2060 let exit_lbl = "exit" in 2061 let p = { ASM.ppreamble = [] ; ASM.pexit_label = exit_lbl ; 2062 ASM.pcode = [instr ; `Label exit_lbl] ; ASM.phas_main = false } in 2063 let p = assembly p in 2064 let status = load_program p in 2065 let addr_zero = BitVectors.vect_of_int 0 `Sixteen in 2066 let (_, size, _) = fetch status.code_memory addr_zero in 2067 BitVectors.int_of_vect size 2068 2069 let size_of_instrs instrs = 2070 let f res instr = res + (size_of_instr instr) in 2071 List.fold_left f 0 instrs -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.mli
r1357 r1539 133 133 val load_program : ASM.program -> status 134 134 val interpret : bool -> ASM.program -> AST.trace 135 136 val size_of_instrs : ASM.labelled_instruction list -> int -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/I8051.ml
r818 r1539 170 170 let rets = [dpl ; dph ; r00 ; r01] 171 171 172 let spl_addr = spl 173 let spl_init = 255 174 let sph_addr = sph 175 let sph_init = 255 172 176 let isp_addr = 129 173 177 let isp_init = 47 -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/I8051.mli
r818 r1539 55 55 val carry : register (* only used for the liveness analysis *) 56 56 57 val spl_addr : int 58 val spl_init : int 59 val sph_addr : int 60 val sph_init : int 57 61 val isp_addr : int 58 62 val isp_init : int -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/Pretty.ml
r1357 r1539 44 44 `Label l -> l ^ ":" 45 45 | `Cost l -> CostLabel.string_of_cost_label ~pretty:true l ^ ":" 46 46 | `Index i -> "index " ^ string_of_int i ^ ":" 47 47 | `Inc i -> "increment " ^ string_of_int i ^ ":" 48 48 | `Jmp j -> "ljmp " ^ j … … 99 99 100 100 let find_comment p pc = 101 102 103 101 let s1 = 102 try 103 let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in 104 104 ", " ^ CostLabel.string_of_cost_label ~pretty:true lbl 105 105 with Not_found -> "" in 106 106 let s2 = 107 107 try 108 108 let i = BitVectors.WordMap.find pc p.ASM.inds in 109 109 ", index " ^ string_of_int i 110 110 with Not_found -> "" in 111 111 let s3 = 112 112 try 113 113 let i = BitVectors.WordMap.find pc p.ASM.incs in 114 114 ", inc " ^ string_of_int i 115 115 with Not_found -> "" in 116 116 s1 ^ s2 ^ s3 117 117 118 118 … … 126 126 (pp_instruction inst) 127 127 cost 128 128 (find_comment p pc), 129 129 new_pc) in 130 130 fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code) -
Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTL.mli
r1345 r1539 150 150 | St_call_id of AST.ident * int * Label.t 151 151 152 (* Call to a function given its address. Parameters are the registers holding 153 the address of the function, the number of arguments of the function, and 154 the label of the next statement. *) 155 | St_call_ptr of Register.t * Register.t * int * Label.t 156 152 157 (* 153 (* Call to a function given its address. Parameters are registers holding the154 address of the function, the arguments of the function, the destination155 registers, and the label of the next statement. *)156 | St_call_ptr of registers * register list * registers * Label.t157 158 158 (* Tail call to a function given its name. Parameters are the name of the 159 159 function, and the number of arguments of the function. *) 160 160 | St_tailcall_id of AST.ident * int 161 161 -
Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLInterpret.ml
r1357 r1539 46 46 renv : hdw_reg_env ; 47 47 mem : memory ; 48 48 inds : indexing list; 49 49 trace : CostLabel.t list } 50 50 … … 80 80 renv = I8051.RegisterMap.empty ; 81 81 mem = Mem.empty ; 82 82 inds = [] ; 83 83 trace = [] } 84 84 … … 127 127 let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in 128 128 let pc = entry_pc lbls_offs ptr def in 129 129 let st = new_ind st in 130 130 change_lenv (change_pc st pc) lenv 131 131 … … 203 203 st 204 204 205 let make_addr st r1 r2 = List.map (fun r -> get_reg (Psd r) st) [r1 ; r2] 206 205 207 206 208 module InterpretExternal = Primitive.Interpret (Mem) … … 226 228 change_pc st next_pc 227 229 228 let interpret_call lbls_offs st fra =229 let ptr = Mem.find_global st.mem f in230 let interpret_call lbls_offs st ptr ra = 231 (* let ptr = Mem.find_global st.mem f in *) 230 232 match Mem.find_fun_def st.mem ptr with 231 233 | ERTL.F_int def -> … … 239 241 240 242 let interpret_return lbls_offs st = 241 243 let st = forget_ind st in 242 244 let st = pop_st_frs st in 243 245 let (st, pch) = pop st in … … 263 265 264 266 | ERTL.St_cost (cost_lbl, lbl) -> 265 267 let cost_lbl = ev_label st cost_lbl in 266 268 let st = add_trace st cost_lbl in 267 269 next_pc st lbl 268 270 269 271 | ERTL.St_ind_0 (i, lbl) -> 270 271 272 enter_loop st i; 273 next_pc st lbl 272 274 273 275 | ERTL.St_ind_inc (i, lbl) -> … … 373 375 374 376 | ERTL.St_load (destr, addr1, addr2, lbl) -> 375 let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]in377 let addr = make_addr st addr1 addr2 in 376 378 let v = Mem.load st.mem chunk addr in 377 379 let st = add_reg (Psd destr) v st in … … 379 381 380 382 | ERTL.St_store (addr1, addr2, srcr, lbl) -> 381 let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]in383 let addr = make_addr st addr1 addr2 in 382 384 let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in 383 385 let st = change_mem st mem in … … 385 387 386 388 | ERTL.St_call_id (f, _, lbl) -> 387 interpret_call lbls_offs st f lbl 389 interpret_call lbls_offs st (Mem.find_global st.mem f) lbl 390 391 | ERTL.St_call_ptr (f1, f2, _, lbl) -> 392 interpret_call lbls_offs st (make_addr st f1 f2) lbl 388 393 389 394 | ERTL.St_cond (srcr, lbl_true, lbl_false) -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLPrinter.ml
r1345 r1539 43 43 Printf.sprintf "*** %s *** --> %s" s lbl 44 44 | ERTL.St_cost (cost_lbl, lbl) -> 45 45 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 46 46 Printf.sprintf "emit %s --> %s" cost_lbl lbl 47 47 | ERTL.St_ind_0 (i, lbl) -> … … 121 121 lbl 122 122 | ERTL.St_call_id (f, nb_args, lbl) -> 123 Printf.sprintf "call \"%s\", %d --> %s" 124 f 123 Printf.sprintf "call \"%s\", %d --> %s" f nb_args lbl 124 | ERTL.St_call_ptr (f1, f2, nb_args, lbl) -> 125 Printf.sprintf "call_ptr [%s ; %s], %d --> %s" 126 (Register.print f1) 127 (Register.print f2) 125 128 nb_args 126 129 lbl 127 130 (* 128 | ERTL.St_call_ptr (f, args, dstrs, lbl) ->129 Printf.sprintf "call_ptr %s, %s, %s --> %s"130 (print_ptr f)131 (print_args args)132 (print_return dstrs)133 lbl134 131 | ERTL.St_tailcall_id (f, nb_args) -> 135 132 Printf.sprintf "tailcall \"%s\", %d" -
Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLToLTLI.ml
r1345 r1539 163 163 164 164 | ERTL.St_cost (cost_lbl, l) -> 165 LTL.St_cost (cost_lbl, l)165 LTL.St_cost (cost_lbl, l) 166 166 167 167 | ERTL.St_ind_0 (i, l) -> 168 168 LTL.St_ind_0 (i, l) 169 169 170 170 | ERTL.St_ind_inc (i, l) -> 171 171 LTL.St_ind_inc (i, l) 172 172 173 173 | ERTL.St_get_hdw (destr, sourcehwr, l) -> … … 289 289 LTL.St_call_id (f, l) 290 290 291 | ERTL.St_call_ptr (f1, f2, _, l) -> 292 let l = generate (LTL.St_call_ptr l) in 293 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 294 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 295 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 296 let l = read f1 (fun hdw -> LTL.St_to_acc (hdw, l)) in 297 let l = generate (LTL.St_from_acc (I8051.st0, l)) in 298 let l = read f2 (fun hdw -> LTL.St_to_acc (hdw, l)) in 299 LTL.St_skip l 300 291 301 | ERTL.St_cond (srcr, lbl_true, lbl_false) -> 292 302 let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in -
Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/liveness.ml
r1468 r1539 40 40 | St_load (_, _, _, l) 41 41 | St_store (_, _, _, l) 42 | St_call_id (_, _, l) -> 42 | St_call_id (_, _, l) 43 | St_call_ptr (_, _, _, l) -> 43 44 Label.Set.singleton l 44 45 | St_cond (_, l1, l2) -> … … 93 94 | St_comment _ 94 95 | St_cost _ 95 96 96 | St_ind_0 _ 97 | St_ind_inc _ 97 98 | St_push _ 98 99 | St_store _ … … 124 125 | St_hdw_to_hdw (r, _, _) -> 125 126 L.hsingleton r 126 | St_call_id _ ->127 | St_call_id _ | St_call_ptr _ -> 127 128 (* Potentially destroys all caller-save hardware registers. *) 128 129 Register.Set.empty, I8051.caller_saved … … 160 161 (* Reads the hardware registers that are used to pass parameters. *) 161 162 Register.Set.empty, 163 set_of_list (MiscPottier.prefix nparams I8051.parameters) 164 | St_call_ptr (r1, r2, nparams, _) -> 165 (* Reads the hardware registers that are used to pass parameters. *) 166 Register.Set.of_list [r1 ; r2], 162 167 set_of_list (MiscPottier.prefix nparams I8051.parameters) 163 168 | St_get_hdw (_, r, _) … … 213 218 | St_store _ 214 219 | St_call_id _ 220 | St_call_ptr _ 215 221 | St_cond _ 216 222 | St_return _ -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/uses.ml
r1345 r1539 41 41 count r uses 42 42 | St_move (r1, r2, _) 43 | St_op1 (_, r1, r2, _) -> 43 | St_op1 (_, r1, r2, _) 44 | St_call_ptr (r1, r2, _, _) -> 44 45 count r1 (count r2 uses) 45 46 | St_opaccsA (_, r1, r2, r3, _) -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LIN.mli
r1349 r1539 73 73 | St_call_id of AST.ident 74 74 75 (* Call to a function given its address in DPTR. *) 76 | St_call_ptr 77 75 78 (* Branch on A accumulator. Parameter is the label to go to when the A 76 79 accumulator is not 0. *) -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINInterpret.ml
r1357 r1539 34 34 renv : hdw_reg_env ; 35 35 mem : memory ; 36 36 inds : indexing list ; 37 37 trace : CostLabel.t list } 38 38 … … 61 61 renv = I8051.RegisterMap.empty ; 62 62 mem = Mem.empty ; 63 63 inds = [] ; 64 64 trace = [] } 65 65 … … 81 81 else error msg 82 82 83 let init_fun_call st ptr def=84 83 let init_fun_call st ptr = 84 let st = new_ind st in 85 85 change_pc st (Val.change_address_offset ptr Val.Offset.zero) 86 86 … … 177 177 set_result st vs 178 178 179 let interpret_call st f = 180 let ptr = Mem.find_global st.mem f in 179 let interpret_call st ptr = 181 180 match Mem.find_fun_def st.mem ptr with 182 181 | LIN.F_int def -> 183 182 let st = save_ra st in 184 init_fun_call st ptr def183 init_fun_call st ptr 185 184 | LIN.F_ext def -> 186 185 let st = next_pc st in … … 188 187 189 188 let interpret_return st = 190 189 let st = forget_ind st in 191 190 let (st, pc) = return_pc st in 192 191 change_pc st pc … … 208 207 209 208 | LIN.St_cost cost_lbl -> 210 209 let cost_lbl = ev_label st cost_lbl in 211 210 let st = add_trace st cost_lbl in 212 211 next_pc st 213 214 215 216 212 213 | LIN.St_ind_0 i -> 214 enter_loop st i; 215 next_pc st 217 216 218 217 | LIN.St_ind_inc i -> 219 220 218 continue_loop st i; 219 next_pc st 221 220 222 221 | LIN.St_int (r, i) -> … … 292 291 293 292 | LIN.St_call_id f -> 294 interpret_call st f 293 interpret_call st (Mem.find_global st.mem f) 294 295 | LIN.St_call_ptr -> 296 interpret_call st (dptr st) 295 297 296 298 | LIN.St_condacc lbl_true -> … … 369 371 match Mem.find_fun_def st.mem ptr with 370 372 | LIN.F_int def -> 371 init_fun_call st ptr def373 init_fun_call st ptr 372 374 | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.") 373 375 -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINPrinter.ml
r1392 r1539 3 3 4 4 5 let n_spaces ?stmt n = 6 let n = match stmt with 7 | Some (LIN.St_label _) | Some (LIN.St_cost _) -> n - 2 8 | _ -> n in 9 String.make n ' ' 5 let n_spaces n = String.make n ' ' 10 6 11 7 … … 31 27 | LIN.St_cost cost_lbl -> 32 28 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 33 29 Printf.sprintf "emit %s" cost_lbl 34 30 | LIN.St_ind_0 i -> 35 31 Printf.sprintf "index %d" i … … 63 59 Printf.sprintf "movex @DPTR, %s" print_a 64 60 | LIN.St_call_id f -> Printf.sprintf "call \"%s\"" f 61 | LIN.St_call_ptr -> 62 Printf.sprintf "call_ptr DPTR" 65 63 | LIN.St_condacc lbl_true -> 66 64 Printf.sprintf "branch %s <> 0, %s" print_a lbl_true … … 70 68 let print_code n c = 71 69 let f s stmt = 72 Printf.sprintf "%s\n%s%s" s (n_spaces ~stmt:stmtn) (print_statement stmt) in70 Printf.sprintf "%s\n%s%s" s (n_spaces n) (print_statement stmt) in 73 71 List.fold_left f "" c 74 72 -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINToASM.ml
r1349 r1539 7 7 8 8 9 (* Translation environment *) 10 11 type env = 12 { externals : AST.ident list ; 13 exit_lbl : Label.t ; 14 fresh : unit -> string } 15 16 let make_env externals exit_lbl fresh = 17 { externals = externals ; 18 exit_lbl = exit_lbl ; 19 fresh = fresh } 20 21 9 22 (* Fetch the labels found in a LIN program. *) 10 23 … … 13 26 | LIN.St_label lbl 14 27 | LIN.St_condacc lbl -> Label.Set.singleton lbl 15 (* quite dubious about the following*)16 | LIN.St_cost lbl -> Label.Set.singleton ( CostLabel.string_of_cost_label lbl)28 (* taking the atom as a fresh prefix will be generated *) 29 | LIN.St_cost lbl -> Label.Set.singleton (lbl.CostLabel.name) 17 30 | _ -> Label.Set.empty 18 31 … … 44 57 let data16_of_int i = `DATA16 (vect_of_int i `Sixteen) 45 58 let acc_addr = I8051.reg_addr I8051.a 59 let dpl_addr = I8051.reg_addr I8051.dpl 60 let dph_addr = I8051.reg_addr I8051.dph 61 let st0_addr = I8051.reg_addr I8051.st0 62 let st1_addr = I8051.reg_addr I8051.st1 46 63 47 64 48 let translate_statement glbls_addr= function65 let translate_statement env = function 49 66 | LIN.St_goto lbl -> [`Jmp lbl] 50 67 | LIN.St_label lbl -> [`Label lbl] 51 68 | LIN.St_comment _ -> [] 52 | LIN.St_cost lbl -> [`Cost lbl ; `NOP (* TODO: hack! Need to make the difference between cost labels and regular labels. *)] 69 | LIN.St_cost lbl -> 70 (* TODO: hack! Need to make the difference between cost labels and regular 71 labels. *) 72 [`Cost lbl ; `NOP ] 53 73 | LIN.St_ind_0 i -> [`Index i ; `NOP (* TODO: hack! *)] 54 74 | LIN.St_ind_inc i -> [`Inc i ; `NOP (* TODO: hack! *)] … … 59 79 | LIN.St_push -> 60 80 [`PUSH acc_addr] 61 | LIN.St_addr x when List.mem _assoc x glbls_addr->62 [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))]81 | LIN.St_addr x when List.mem x env.externals -> 82 error ("Primitive or external " ^ x ^ " is not supported.") 63 83 | LIN.St_addr x -> 64 error ("unknown global " ^ x ^ ".")84 [`Mov (`DPTR, x)] 65 85 | LIN.St_from_acc r -> 66 86 [`MOV (`U3 (I8051.reg_addr r, `A))] … … 95 115 | LIN.St_store -> 96 116 [`MOVX (`U2 (`EXT_IND_DPTR, `A))] 117 | LIN.St_call_id x when List.mem x env.externals -> 118 error ("Primitive or external " ^ x ^ " is not supported.") 97 119 | LIN.St_call_id f -> 98 120 [`Call f] 121 | LIN.St_call_ptr -> 122 let lbl = env.fresh () in 123 [`MOV (`U3 (st0_addr, dpl_addr)) ; (* save DPL *) 124 `MOV (`U3 (st1_addr, dph_addr)) ; (* save DPH *) 125 `Mov (`DPTR, lbl) ; (* DPTR <- return address *) 126 `PUSH dpl_addr ; (* push DPL *) 127 `PUSH dph_addr ; (* push DPH *) 128 `MOV (`U3 (dpl_addr, st0_addr)) ; (* restore DPL *) 129 `MOV (`U3 (dph_addr, st1_addr)) ; (* restore DPH *) 130 `MOV (`U1 (`A, data_of_int 0)) ; (* A <- 0 *) 131 `JMP `IND_DPTR ; (* jump to A+DPTR *) 132 `Label lbl] (* return address *) 99 133 | LIN.St_condacc lbl -> 100 134 [`WithLabel (`JNZ (`Label lbl))] … … 102 136 [`RET] 103 137 104 let translate_code glbls_addrcode =105 List.flatten (List.map (translate_statement glbls_addr) code)138 let translate_code env code = 139 List.flatten (List.map (translate_statement env) code) 106 140 107 141 108 let translate_fun_def glbls_addr (id, def) = match def with 109 | LIN.F_int code -> (`Label id) :: (translate_code glbls_addr code) 110 | LIN.F_ext ext -> 111 error ("potential call to unsupported external " ^ ext.AST.ef_tag ^ ".") 142 let translate_fun_def env (id, def) = 143 let code = match def with 144 | LIN.F_int code -> translate_code env code 145 | LIN.F_ext ext -> [`NOP] in 146 ((`Label id) :: code) 112 147 113 let translate_functs glbls_addr exit_labelmain functs =148 let translate_functs env main functs = 114 149 let preamble = match main with 115 150 | None -> [] … … 117 152 [`MOV (`U3 (`DIRECT (byte_of_int I8051.isp_addr), 118 153 data_of_int I8051.isp_init)) ; 154 `MOV (`U3 (`DIRECT (byte_of_int I8051.spl_addr), 155 data_of_int I8051.spl_init)) ; 156 `MOV (`U3 (`DIRECT (byte_of_int I8051.sph_addr), 157 data_of_int I8051.sph_init)) ; 119 158 `Call main ; 120 `Label exit_label ; `Jmp exit_label] in 121 preamble @ 122 (List.flatten (List.map (translate_fun_def glbls_addr) functs)) 159 `Label env.exit_lbl ; `Jmp env.exit_lbl] in 160 preamble @ (List.flatten (List.map (translate_fun_def env) functs)) 123 161 124 162 125 let globals_addr l = 126 let f (res, offset) (x, size) = ((x, offset) :: res, offset + size) in 127 fst (List.fold_left f ([], 0) l) 163 let init_env p = 164 let f_externals (id, def) = match def with LIN.F_ext _ -> [id] | _ -> [] in 165 let externals = 166 List.fold_left (fun res def -> res @ (f_externals def)) [] p.LIN.functs in 167 let prog_lbls = prog_labels p in 168 let exit_lbl = Label.Gen.fresh_prefix prog_lbls "_exit" in 169 let fresh = Label.make_fresh prog_lbls "_call_ret" in 170 make_env externals exit_lbl fresh 128 171 129 172 … … 134 177 135 178 let translate p = 136 let prog_lbls = prog_labels p in 137 let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in 138 let glbls_addr = globals_addr p.LIN.vars in 179 let env = init_env p in 139 180 let p = 140 181 { ASM.ppreamble = p.LIN.vars ; 141 ASM.pexit_label = exit_label ; 142 ASM.pcode = 143 translate_functs glbls_addr exit_label p.LIN.main p.LIN.functs ; 182 ASM.pexit_label = env.exit_lbl ; 183 ASM.pcode = translate_functs env p.LIN.main p.LIN.functs ; 144 184 ASM.phas_main = p.LIN.main <> None } in 145 185 ASMInterpret.assembly p -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTL.mli
r1345 r1539 81 81 | St_call_id of AST.ident * Label.t 82 82 83 (* Call to a function given its address in DPTR. Parameter is the label of the 84 next statement. *) 85 | St_call_ptr of Label.t 86 83 87 (* Branch on A accumulator. Parameters are the label to go to when the A 84 88 accumulator is not 0, and the label to go to when the A accumulator is -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml
r1357 r1539 31 31 renv : hdw_reg_env ; 32 32 mem : memory ; 33 33 inds : CostLabel.const_indexing list ; 34 34 trace : CostLabel.t list } 35 35 … … 58 58 renv = I8051.RegisterMap.empty ; 59 59 mem = Mem.empty ; 60 60 inds = [] ; 61 61 trace = [] } 62 62 … … 102 102 let init_fun_call lbls_offs st ptr def = 103 103 let pc = entry_pc lbls_offs ptr def in 104 104 let st = new_ind st in 105 105 change_pc st pc 106 106 … … 204 204 change_pc st next_pc 205 205 206 let interpret_call lbls_offs st f ra = 207 let ptr = Mem.find_global st.mem f in 206 let interpret_call lbls_offs st ptr ra = 208 207 match Mem.find_fun_def st.mem ptr with 209 208 | LTL.F_int def -> … … 216 215 217 216 let interpret_return lbls_offs st = 218 217 let st = forget_ind st in 219 218 let (st, pc) = return_pc st in 220 219 change_pc st pc … … 237 236 238 237 | LTL.St_cost (cost_lbl, lbl) -> 239 238 let cost_lbl = ev_label st cost_lbl in 240 239 let st = add_trace st cost_lbl in 241 240 next_pc st lbl 242 241 243 242 | LTL.St_ind_0 (i, lbl) -> 244 245 243 enter_loop st i; 244 next_pc st lbl 246 245 247 246 | LTL.St_ind_inc (i, lbl) -> … … 249 248 next_pc st lbl 250 249 251 250 | LTL.St_int (r, i, lbl) -> 252 251 let st = add_reg r (Val.of_int i) st in 253 252 next_pc st lbl … … 321 320 322 321 | LTL.St_call_id (f, lbl) -> 323 interpret_call lbls_offs st f lbl 322 interpret_call lbls_offs st (Mem.find_global st.mem f) lbl 323 324 | LTL.St_call_ptr lbl -> 325 interpret_call lbls_offs st (dptr st) lbl 324 326 325 327 | LTL.St_condacc (lbl_true, lbl_false) -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLPrinter.ml
r1345 r1539 60 60 Printf.sprintf "movex @DPTR, %s --> %s" print_a lbl 61 61 | LTL.St_call_id (f, lbl) -> Printf.sprintf "call \"%s\" --> %s" f lbl 62 | LTL.St_call_ptr lbl -> 63 Printf.sprintf "call_ptr DPTR --> %s" lbl 62 64 | LTL.St_condacc (lbl_true, lbl_false) -> 63 65 Printf.sprintf "branch %s <> 0 --> %s, %s" print_a lbl_true lbl_false -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLIN.ml
r1349 r1539 22 22 | LTL.St_cost (lbl, _) -> 23 23 LIN.St_cost lbl 24 25 26 27 24 | LTL.St_ind_0 (i, _) -> 25 LIN.St_ind_0 i 26 | LTL.St_ind_inc (i, _) -> 27 LIN.St_ind_inc i 28 28 | LTL.St_int (r, i, _) -> 29 29 LIN.St_int (r, i) … … 54 54 | LTL.St_call_id (f, _) -> 55 55 LIN.St_call_id f 56 | LTL.St_call_ptr _ -> 57 LIN.St_call_ptr 56 58 57 59 (* Conditional branch statement. In [LIN], control implicitly -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLINI.ml
r1349 r1539 132 132 | LTL.St_load l 133 133 | LTL.St_store l 134 | LTL.St_call_id (_, l) -> 134 | LTL.St_call_id (_, l) 135 | LTL.St_call_ptr l -> 135 136 136 137 visit l -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/branch.ml
r1345 r1539 52 52 | LTL.St_cost (lbl, l) -> 53 53 LTL.St_cost (lbl, rep l) 54 55 54 | LTL.St_ind_0 (i, l) -> 55 LTL.St_ind_0 (i, rep l) 56 56 | LTL.St_ind_inc (i, l) -> 57 57 LTL.St_ind_inc (i, rep l) 58 58 | LTL.St_int (r, i, l) -> 59 59 LTL.St_int (r, i, rep l) … … 84 84 | LTL.St_call_id (f, l) -> 85 85 LTL.St_call_id (f, rep l) 86 | LTL.St_call_ptr l -> 87 LTL.St_call_ptr (rep l) 86 88 | LTL.St_condacc (lbl_true, lbl_false) -> 87 89 LTL.St_condacc (rep lbl_true, rep lbl_false) -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLInterpret.ml
r1357 r1539 68 68 (string_of_local_env lenv) 69 69 (Mem.to_string mem); 70 71 72 70 let i = CostLabel.curr_const_ind ind in 71 CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i; 72 Printf.printf "Regular state: %s\n\n%!" 73 73 lbl 74 74 | CallState (_, _, args, mem, _, _) -> … … 132 132 (carry : Val.t) 133 133 (mem : memory) 134 134 (inds : indexing list) 135 135 (stmt : RTL.statement) 136 136 (trace : CostLabel.t list) : … … 145 145 146 146 | RTL.St_ind_0 (i, lbl) -> 147 148 147 CostLabel.enter_loop inds i; 148 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 149 149 150 150 | RTL.St_ind_inc (i, lbl) -> 151 152 151 CostLabel.continue_loop inds i; 152 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 153 153 154 154 | RTL.St_addr (r1, r2, x, lbl) -> … … 262 262 (args : Val.t list) 263 263 (mem : memory) 264 264 (inds : indexing list) 265 265 (trace : CostLabel.t list) : 266 266 state = 267 267 match f_def with 268 268 | RTL.F_int def -> 269 269 let inds = new_ind inds in 270 270 let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in 271 271 State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp, … … 281 281 (ret_vals : Val.t list) 282 282 (mem : memory) 283 283 (inds : indexing list) 284 284 (trace : CostLabel.t list) : 285 285 state = 286 286 let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in 287 287 let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in 288 288 let inds = forget_ind inds in 289 289 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace) 290 290 -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLToERTL.ml
r1345 r1539 50 50 ERTL.St_store (addr1, addr2, srcrs, lbl) 51 51 | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl) 52 | ERTL.St_call_ptr (f1, f2, nb_args, _) -> 53 ERTL.St_call_ptr (f1, f2, nb_args, lbl) 52 54 | ERTL.St_cond _ as inst -> inst 53 55 | ERTL.St_return _ as inst -> inst … … 295 297 below. When the called function returns, we put the result where the calling 296 298 function expect it to be. *) 297 let translate_call _id fargs ret_regs start_lbl dest_lbl def =299 let translate_call stmt args ret_regs start_lbl dest_lbl def = 298 300 let nb_args = List.length args in 299 301 add_translates … … 301 303 adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @ 302 304 set_params args @ 303 [adds_graph [ ERTL.St_call_id (f, nb_args, start_lbl)] ;305 [adds_graph [stmt nb_args] ; 304 306 adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ; 305 307 fetch_result ret_regs ; … … 366 368 367 369 | RTL.St_call_id (f, args, ret_regs, lbl') -> 368 translate_call_id f args ret_regs lbl lbl' def 369 370 | RTL.St_call_ptr _ -> 371 assert false (* TODO *) 370 let stmt nb_args = ERTL.St_call_id (f, nb_args, lbl) in 371 translate_call stmt args ret_regs lbl lbl' def 372 373 | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl') -> 374 let stmt nb_args = ERTL.St_call_ptr (f1, f2, nb_args, lbl) in 375 translate_call stmt args ret_regs lbl lbl' def 372 376 373 377 (* … … 436 440 let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in 437 441 (Some cost_label, { def with ERTL.f_graph = graph }) 438 442 | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl) 439 443 | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl) 440 444 | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl) … … 447 451 | ERTL.St_load (_, _, _, lbl) 448 452 | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl) 453 | ERTL.St_call_ptr (_, _, _, lbl) 449 454 | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl) 450 455 -> -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabs.mli
r1477 r1539 12 12 13 13 type argument = 14 15 14 | Reg of Register.t 15 | Imm of AST.cst*AST.sig_type 16 16 17 17 (* A function in RTLabs is a mapping from labels to … … 27 27 28 28 (* Reset to 0 a loop index *) 29 29 | St_ind_0 of CostLabel.index * Label.t 30 30 31 31 (* Increment a loop index *) 32 32 | St_ind_inc of CostLabel.index * Label.t 33 33 34 34 (* Assign a constant to registers. Parameters are the destination register, -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsInterpret.ml
r1477 r1539 59 59 List.fold_left f "" args 60 60 61 let print_state state = (match state with61 let print_state state = match state with 62 62 | State (_, _, sp, lbl, lenv, mem, inds, _) -> 63 63 Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:" … … 65 65 (string_of_local_env lenv) 66 66 (Mem.to_string mem); 67 68 69 67 let i = CostLabel.curr_const_ind inds in 68 CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i; 69 Printf.printf "Regular state: %s\n\n%!" 70 70 lbl 71 71 | CallState (_, _, args, mem, _, _) -> … … 77 77 (Mem.to_string mem) 78 78 (Val.to_string v) 79 ); Printf.printf "-----------------------------------------------------\n\n%!"80 79 81 80 … … 133 132 134 133 let eval_arg lenv mem sp = function 135 136 134 | RTLabs.Reg r -> get_value lenv r 135 | RTLabs.Imm (c, t) -> Eval.cst mem sp t c 137 136 138 137 let get_type_arg lenv = function 139 140 138 | RTLabs.Reg r -> get_type lenv r 139 | RTLabs.Imm (_, typ) -> typ 141 140 142 141 (* Interpret statements. *) … … 149 148 (mem : memory) 150 149 (stmt : RTLabs.statement) 151 150 (inds : indexing list) 152 151 (trace : CostLabel.t list) : 153 152 state = match stmt with … … 157 156 158 157 | RTLabs.St_cost (cost_lbl, lbl) -> 159 let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in 160 State (sfrs, graph, sp, lbl, lenv, mem, inds, cost_lbl :: trace) 161 162 | RTLabs.St_ind_0 (i, lbl) -> 158 let cost_lbl = 159 CostLabel.ev_indexing (curr_ind inds) cost_lbl in 160 State (sfrs, graph, sp, lbl, lenv, 161 mem, inds, cost_lbl :: trace) 162 163 | RTLabs.St_ind_0 (i, lbl) -> 163 164 CostLabel.enter_loop inds i; 164 State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) 165 State (sfrs, graph, sp, lbl, lenv, 166 mem, inds, trace) 165 167 166 168 | RTLabs.St_ind_inc (i, lbl) -> 167 CostLabel.continue_loop inds i; 168 State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) 169 CostLabel.continue_loop inds i; 170 State (sfrs, graph, sp, lbl, lenv, 171 mem, inds, trace) 169 172 170 173 | RTLabs.St_cst (destr, cst, lbl) -> … … 181 184 let v = 182 185 Eval.op2 183 (get_type lenv destr) (get_type_arg lenv srcr1) (get_type_arg lenv srcr2) 186 (get_type lenv destr) 187 (get_type_arg lenv srcr1) 188 (get_type_arg lenv srcr2) 184 189 op2 185 190 (eval_arg lenv mem sp srcr1) … … 193 198 194 199 | RTLabs.St_store (q, addr, srcr, lbl) -> 195 let addr = address_of_value (eval_arg lenv mem sp addr) in200 let addr = address_of_value (eval_arg lenv mem sp addr) in 196 201 let v = eval_arg lenv mem sp srcr in 197 202 let mem = Mem.storeq mem q addr v in … … 203 208 (* Save the stack frame. *) 204 209 let sf = 205 {ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv} in 210 { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 211 in 206 212 CallState (sf :: sfrs, f_def, args, mem, inds, trace) 207 213 … … 302 308 (args : Val.t list) 303 309 (mem : memory) 304 310 (inds : indexing list) 305 311 (trace : CostLabel.t list) : 306 312 state = … … 310 316 Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in 311 317 let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in 312 313 314 318 (* allocate new constant indexing *) 319 let graph = def.RTLabs.f_graph in 320 let inds = new_ind inds in 315 321 State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace) 316 322 | RTLabs.F_ext def -> … … 324 330 (ret_val : Val.t) 325 331 (mem : memory) 326 332 (inds : indexing list) 327 333 (trace : CostLabel.t list) : 328 334 state = … … 330 336 | None -> sf.lenv 331 337 | Some ret_reg -> update_local ret_reg ret_val sf.lenv in 332 (* erase current indexing and revert to previous one *) 333 let inds = forget_ind inds in 334 State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, inds, trace) 338 (* erase current indexing and revert to previous one *) 339 let inds = forget_ind inds in 340 State (sfrs, sf.graph, sf.sp, sf.pc, lenv, 341 mem, inds, trace) 335 342 336 343 -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsPrinter.ml
r1477 r1539 96 96 97 97 let print_arg = function 98 99 100 98 | RTLabs.Reg r -> print_reg r 99 | RTLabs.Imm (c, t) -> 100 Printf.sprintf "(%s)%s" (Primitive.print_type t) (print_cst c) 101 101 102 102 let print_op2 op r s = Printf.sprintf "%s %s %s" … … 122 122 | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p" 123 123 | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u") 124 124 (print_arg s) 125 125 126 126 … … 169 169 | RTLabs.St_load (q, addr, destr, lbl) -> 170 170 Printf.sprintf "%s := *(%s) %s --> %s" 171 (print_reg destr)171 (print_reg destr) 172 172 (Memory.string_of_quantity q) 173 173 (print_arg addr) … … 175 175 | RTLabs.St_store (q, addr, srcr, lbl) -> 176 176 Printf.sprintf "*(%s)%s := %s --> %s" 177 (Memory.string_of_quantity q)177 (Memory.string_of_quantity q) 178 178 (print_arg addr) 179 179 (print_arg srcr) … … 181 181 | RTLabs.St_call_id (f, args, Some r, sg, lbl) -> 182 182 Printf.sprintf "%s := \"%s\"(%s) : %s --> %s" 183 184 183 (print_reg r) 184 f 185 185 (print_args args) 186 186 (Primitive.print_sig sg) 187 187 lbl 188 188 | RTLabs.St_call_id (f, args, None, sg, lbl) -> 189 Printf.sprintf "\"%s\"(%s) : %s --> %s"190 191 192 193 189 Printf.sprintf "\"%s\"(%s) : %s --> %s" 190 f 191 (print_args args) 192 (Primitive.print_sig sg) 193 lbl 194 194 | RTLabs.St_call_ptr (f, args, Some r, sg, lbl) -> 195 195 Printf.sprintf "%s := *%s (%s) : %s --> %s" 196 197 198 199 200 196 (print_reg r) 197 (print_reg f) 198 (print_args args) 199 (Primitive.print_sig sg) 200 lbl 201 201 | RTLabs.St_call_ptr (f, args, None, sg, lbl) -> 202 Printf.sprintf "*%s (%s) : %s --> %s"203 204 205 206 202 Printf.sprintf "*%s (%s) : %s --> %s" 203 (print_reg f) 204 (print_args args) 205 (Primitive.print_sig sg) 206 lbl 207 207 | RTLabs.St_tailcall_id (f, args, sg) -> 208 208 Printf.sprintf "tailcall \"%s\" (%s) : %s" … … 256 256 (print_statement stmt) 257 257 s in 258 258 let f' lbl stmt (reach, s) = 259 259 (Label.Set.add lbl reach, f lbl stmt s) in 260 261 262 263 264 265 266 260 let (reachable, str) = 261 RTLabsUtilities.dfs_fold f' c entry (Label.Set.empty, "") in 262 let filter lbl _ = not (Label.Set.mem lbl reachable) in 263 let c_rest = Label.Map.filter filter c in 264 if Label.Map.is_empty c_rest then str else 265 let str' = Label.Map.fold f c_rest "" in 266 str ^ "DEAD NODES:\n" ^ str' 267 267 268 268 let print_internal_decl n f def = -
Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsToRTL.ml
r1477 r1539 748 748 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 749 749 750 750 | _ -> assert false (*not possible because of previous removal of immediates*) 751 751 752 752 let remove_immediates def = 753 754 755 753 let load_arg a lbl g rs = match a with 754 | RTLabs.Reg r -> (lbl, g, rs, r) 755 | RTLabs.Imm (c, t) -> 756 756 let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in 757 757 let new_r = Register.fresh def.RTLabs.f_runiverse in 758 759 760 761 762 763 758 let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in 759 (new_l, g, (new_r, t) :: rs, new_r) in 760 let f lbl stmt (g, rs) = 761 match stmt with 762 | RTLabs.St_op2(op, r, a1, a2, l) -> 763 let (lbl', g, rs, r1) = load_arg a1 lbl g rs in 764 764 let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in 765 765 let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in 766 767 766 let g = Label.Map.add lbl' s g in 767 (g, rs) 768 768 | RTLabs.St_store(q, a1, a2, l) -> 769 769 let (lbl', g, rs, r1) = load_arg a1 lbl g rs in … … 772 772 let g = Label.Map.add lbl' s g in 773 773 (g, rs) 774 774 | RTLabs.St_load (q, a, r, l) -> 775 775 let (lbl', g, rs, r1) = load_arg a lbl g rs in 776 776 let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in 777 777 let g = Label.Map.add lbl' s g in 778 778 (g, rs) 779 780 781 782 783 779 | _ -> (g, rs) in 780 let g = def.RTLabs.f_graph in 781 let (g, rs) = Label.Map.fold f g (g, []) in 782 let locals = List.rev_append rs def.RTLabs.f_locals in 783 { def with RTLabs.f_graph = g; RTLabs.f_locals = locals } 784 784 785 785 let translate_internal def = 786 786 let def = remove_immediates def in 787 787 let runiverse = def.RTLabs.f_runiverse in 788 788 let lenv = -
Deliverables/D2.2/8051-indexed-labels-branch/src/acc.ml
r1507 r1539 23 23 *) 24 24 let process filename = 25 let _ = Printf.eprintf "Processing %s.\n%!" filename in 26 let src_language = Options.get_source_language () in 27 let tgt_language = Options.get_target_language () in 28 let input_ast = Languages.parse src_language filename in 29 let input_ast = Languages.add_runtime input_ast in 30 let input_ast = Languages.labelize input_ast in 25 let _ = Printf.printf "Processing %s.\n%!" filename in 26 let src_language = Options.get_source_language () in 27 let tgt_language = Options.get_target_language () in 28 let is_lustre_file = Options.is_lustre_file () in 29 let remove_lustre_externals = Options.is_remove_lustre_externals () in 30 let input_ast = 31 Languages.parse ~is_lustre_file ~remove_lustre_externals 32 src_language filename in 33 let input_ast = Languages.add_runtime input_ast in 34 let input_ast = Languages.labelize input_ast in 31 35 let (exact_output, output_filename) = match Options.get_output_files () with 32 36 | None -> (false, filename) 33 37 | Some filename' -> (true, filename') in 34 38 let save ?(suffix="") ast = 35 Languages.save exact_output output_filename suffix ast 39 Languages.save 40 (Options.is_asm_pretty ()) exact_output output_filename suffix ast 36 41 in 37 42 let target_asts = … … 45 50 if Options.annotation_requested () then 46 51 begin 47 let (annotated_input_ast, cost_id, cost_incr ) =52 let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) = 48 53 let cost_tern = Options.is_cost_ternary_enabled () in 49 54 Languages.annotate cost_tern input_ast final_ast in ( 50 55 save ~suffix:"-annotated" annotated_input_ast; 51 Languages.save_cost output_filename cost_id cost_incr); 56 Languages.save_cost exact_output output_filename cost_id cost_incr 57 extern_cost_variables); 52 58 end; 53 54 if Options.is_debug_enabled () then 59 60 if Options.is_debug_enabled () then 55 61 List.iter save intermediate_asts; 56 62 57 if Options.interpretation_requested () || Options.is_debug_enabled () || 58 Options.trace_requested () then 63 if Options.interpretations_requested () then 59 64 begin 60 65 let asts = target_asts in … … 62 67 let label_traces = List.map (Languages.interpret debug) asts in 63 68 Printf.eprintf "Checking execution traces...%!"; 64 if Options.trace_requested () then65 let print_l l =66 Printf.printf "%s, " (CostLabel.string_of_cost_label67 ~pretty:true l) in68 let print_ls ls = List.iter print_l ls in69 let print_trace (v, ls) =70 Printf.printf "%s | " (Big_int.string_of_big_int v);71 print_ls ls;72 Printf.printf "\n" in73 List.iter print_trace label_traces74 else ();75 69 Checker.same_traces (List.combine asts label_traces); 76 70 Printf.eprintf "OK.\n%!"; 77 end 71 end; 72 73 if Options.interpretation_requested () then 74 ignore (Languages.interpret (Options.is_debug_enabled ()) final_ast) 75 76 let lustre_test filename = 77 let lustre_test = match Options.get_lustre_test () with 78 | None -> assert false (* do not use on this argument *) 79 | Some lustre_test -> lustre_test in 80 let lustre_test_cases = Options.get_lustre_test_cases () in 81 let lustre_test_cycles = Options.get_lustre_test_cycles () in 82 let lustre_test_min_int = Options.get_lustre_test_min_int () in 83 let lustre_test_max_int = Options.get_lustre_test_max_int () in 84 let src_language = Languages.Clight in 85 let tgt_language = Languages.Clight in 86 let input_ast = Languages.parse src_language filename in 87 let input_ast = 88 Languages.add_lustre_main lustre_test lustre_test_cases lustre_test_cycles 89 lustre_test_min_int lustre_test_max_int input_ast in 90 let (exact_output, output_filename) = match Options.get_output_files () with 91 | None -> (false, filename) 92 | Some filename' -> (true, filename') in 93 let save ast = 94 Languages.save 95 (Options.is_asm_pretty ()) exact_output output_filename "" ast in 96 let target_asts = 97 Languages.compile false (Options.get_transformations ()) 98 src_language tgt_language input_ast 99 in 100 let final_ast, _ = Misc.ListExt.cut_last target_asts in 101 save input_ast ; 102 save final_ast 78 103 79 104 let _ = 80 105 if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files 81 else List.iter process input_files 106 else 107 if Options.get_lustre_test () <> None then List.iter lustre_test input_files 108 else List.iter process input_files -
Deliverables/D2.2/8051-indexed-labels-branch/src/checker.ml
r1291 r1539 14 14 in 15 15 let sentence (k, (v1, v2)) = 16 16 let k = CostLabel.string_of_cost_label ~pretty:true k in 17 17 Printf.sprintf " Label %s %s in language `%s' \ 18 18 whereas it %s in language `%s'." 19 19 k (string_of_value v1) lang1 (string_of_value v2) lang2 20 20 in 21 21 String.concat "\n" (List.map sentence ds) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clight.mli
r1305 r1539 113 113 | Eorbool of expr*expr (**r sequential or ([||]) *) 114 114 | Esizeof of ctype (**r size of a type *) 115 | Efield of expr*ident (**r access to a member of a struct or union *)115 | Efield of expr*ident (**r access to a member of a struct or union *) 116 116 117 117 (** The following constructors are used by the annotation process only. *) … … 138 138 | Ssequence of statement*statement (**r sequence *) 139 139 | Sifthenelse of expr*statement*statement (**r conditional *) 140 | Swhile of loop_index*expr*statement 141 | Sdowhile of loop_index*expr*statement 142 | Sfor of loop_index*statement*expr*statement*statement 140 | Swhile of loop_index*expr*statement (**r [while] loop *) 141 | Sdowhile of loop_index*expr*statement (**r [do] loop *) 142 | Sfor of loop_index*statement*expr*statement*statement (**r [for] loop *) 143 143 | Sbreak (**r [break] statement *) 144 144 | Scontinue (**r [continue] statement *) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml
r1507 r1539 26 26 Label.Set.union user_labels1 user_labels2) 27 27 28 let empty_triple = 29 (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty) 28 let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty) 30 29 31 30 let name_singleton id = 32 31 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) 33 32 34 let cost_label_singleton lbl =35 (StringTools.Set.empty, CostLabel.Set.singleton lbl, Label.Set.empty)33 let cost_label_singleton cost_lbl = 34 (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty) 36 35 37 36 let label_singleton lbl = … … 79 78 (StringTools.Set.union vars names, cost_labels, user_labels) 80 79 | Clight.External (id, _, _) -> 81 (StringTools.Set.singleton id, CostLabel.Set.empty, 82 Label.Set.empty) in 80 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in 83 81 let fun_idents (id, f_def) = 84 82 let (names, cost_labels, user_labels) = def_idents f_def in … … 191 189 (* Instrument an expression. *) 192 190 193 (* FIXME: follow cost_tern option*)191 (* FIXME: currently using a hack (reparsing) *) 194 192 let instrument_expr cost_tern l_ind cost_mapping cost_incr = 195 193 let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with … … 227 225 (* Instrument a statement. *) 228 226 229 (* not using ClightFold as l_ind changes through loops*)227 (* FIXME: use ClightFold, a much better option *) 230 228 let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt = 231 229 let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in … … 374 372 (cost_incr, Clight.Internal cfun) 375 373 374 (* Create a fresh uninitialized cost variable for each external function. This 375 will be used by the Cost plug-in of the Frama-C platform. *) 376 377 let extern_cost_variables make_unique functs = 378 let prefix = "_cost_of_" in 379 let f (decls, map) (_, def) = match def with 380 | Clight.Internal _ -> (decls, map) 381 | Clight.External (id, _, _) -> 382 let new_var = make_unique (prefix ^ id) in 383 (decls @ [cost_decl new_var], StringTools.Map.add id new_var map) in 384 List.fold_left f ([], StringTools.Map.empty) functs 385 376 386 let save_tmp tmp_file s = 377 387 let cout = open_out tmp_file in … … 379 389 flush cout ; 380 390 close_out cout 381 382 391 383 392 (** [instrument prog cost_map] instruments the program [prog]. First a fresh 384 393 global variable --- the so-called cost variable --- is added to the program. … … 391 400 (* Create a fresh 'cost' variable. *) 392 401 let names = names p in 393 let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in 402 let make_unique = StringTools.make_unique names in 403 let cost_id = make_unique cost_id_prefix in 394 404 let cost_decl = cost_decl cost_id in 395 405 … … 397 407 let names = StringTools.Set.add cost_id names in 398 408 let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in 409 410 (* Create a fresh uninitialized global variable for each extern function. *) 411 let (extern_cost_decls, extern_cost_variables) = 412 extern_cost_variables make_unique p.Clight.prog_funct in 399 413 400 414 (* Define an increment function for the cost variable. *) … … 415 429 416 430 (* Glue all this together. *) 417 let prog_vars = cost_decl :: p.Clight.prog_vars in431 let prog_vars = cost_decl :: extern_cost_decls @ p.Clight.prog_vars in 418 432 let prog_funct = cost_incr_def :: prog_funct in 419 433 let p' = … … 426 440 let tmp_file = Filename.temp_file "clight_instrument" ".c" in 427 441 save_tmp tmp_file (ClightPrinter.print_program p') ; 428 let p'= ClightParser.process tmp_file in442 let res = ClightParser.process tmp_file in 429 443 Misc.SysExt.safe_remove tmp_file ; 430 ( p', cost_id, cost_incr)444 (res, cost_id, cost_incr, extern_cost_variables) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.mli
r1507 r1539 6 6 program. Then, each cost label in the program is replaced by an increment of 7 7 the cost variable, following the mapping [cost_map]. The function also 8 returns the name of the cost variable and the name of the cost increment 9 function. [cost_tern] rules whether cost increments are given by ternary 10 expressions (more readable) or by branch statements (for frama-c 11 itegration). 12 13 TODO: int to expressions *) 8 returns the name of the cost variable, the name of the cost increment 9 function, and a fresh uninitialized global (cost) variable associated to each 10 extern function. [cost_tern] rules whether cost increments are given by 11 ternary expressions (more readable) or by branch statements (for frama-c 12 itegration). *) 14 13 val instrument : bool -> Clight.program -> int CostLabel.Map.t -> 15 Clight.program * string * string 14 Clight.program * string * string * string StringTools.Map.t 16 15 17 16 val cost_labels : Clight.program -> CostLabel.Set.t -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightFold.ml
r1392 r1539 170 170 let sub_stmts_res = List.map (statement2 f_expr f_statement) sub_stmts in 171 171 f_statement stmt sub_exprs_res sub_stmts_res 172 -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml
r1357 r1539 106 106 | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field 107 107 | Ecost (cost_lbl, e) -> 108 109 108 let cost_lbl = CostLabel.string_of_cost_label cost_lbl in 109 "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e) 110 110 | Ecall (f, arg, e) -> 111 111 "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")" … … 151 151 LocalEnv.fold f lenv "" 152 152 153 let print_state state = (match state with153 let print_state state = match state with 154 154 | State (_, stmt, _, lenv, mem, c) -> 155 155 Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: " 156 156 (string_of_local_env lenv) 157 157 (Mem.to_string mem); 158 159 158 let i = CostLabel.curr_const_ind c in 159 CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i; 160 160 Printf.printf "\nRegular state: %s\n\n%!" 161 161 (string_of_statement stmt) … … 168 168 (Mem.to_string mem) 169 169 (Value.to_string v) 170 ); Printf.printf "---------------------------------------------------------\n"171 170 172 171 … … 426 425 ((Mem.load m (size_of_ctype tt) addr, tt), l1) 427 426 | Ecost (lbl,e1) -> 428 429 427 (* applying current indexing on label *) 428 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in 430 429 let (v1,l1) = eval_expr localenv m c e1 in 431 430 (v1,lbl::l1) … … 486 485 else error "undefined condition guard value." 487 486 488 let eval_stmt f k e m s c = 489 match s, k with 487 let eval_stmt f k e m s c = match s, k with 490 488 | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[]) 491 489 | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k') 492 490 | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') -> 493 494 495 491 (* possibly continuing a loop *) 492 CostLabel.continue_loop_opt c i; (* if loop is not continued, this change 493 will have no effect in the following. *) 496 494 let ((v1,_),l1) = eval_expr e m c a in 497 495 let a_false = (State(f,Sskip,k',e,m,c),l1) in … … 504 502 let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in 505 503 condition v1 a_true a_false 506 | Sskip, Kfor2(i,a2,a3,s,k) -> (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[]) 504 | Sskip, Kfor2(i,a2,a3,s,k) -> 505 (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[]) 507 506 | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[]) 508 507 | Sskip, Kcall _ -> … … 531 530 condition v1 a_true a_false 532 531 | Swhile(i,a,s), _ -> 533 532 CostLabel.enter_loop_opt c i; 534 533 let ((v1,_),l1) = eval_expr e m c a in 535 534 let a_false = (State(f,Sskip,k,e,m,c),l1) in … … 537 536 condition v1 a_true a_false 538 537 | Sdowhile(i,a,s), _ -> 539 540 538 CostLabel.enter_loop_opt c i; 539 (State(f,s,Kdowhile(i,a,s,k),e,m,c),[]) 541 540 | Sfor(i,Sskip,a2,a3,s), _ -> 542 541 CostLabel.enter_loop_opt c i; 543 542 let ((v1,_),l1) = eval_expr e m c a2 in 544 543 let a_false = (State(f,Sskip,k,e,m,c),l1) in … … 548 547 | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[]) 549 548 | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k) 550 549 | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[]) 551 550 | Scontinue, Kseq(_,k) 552 551 | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[]) 553 552 | Sreturn None, _ -> 554 553 let m' = free_local_env m e in … … 561 560 let ((v,_),l) = eval_expr e m c a in 562 561 let n = Value.to_int v in 563 562 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l) 564 563 | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[]) 565 564 | Scost(lbl,s), _ -> 566 567 568 565 (* applying current indexing on label *) 566 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in 567 (State(f,s,k,e,m,c),[lbl]) 569 568 | Sgoto lbl, _ -> 570 (* if we exit an indexed loop, we don't care. It should not be possible to*)571 (* enter an indexed loop that is not the current one, so we do nothing*)572 569 (* if we exit an indexed loop, we don't care. It should not be possible to *) 570 (* enter an indexed loop that is not the current one, so we do nothing *) 571 (* to loop indexes *) 573 572 let (s', k') = find_label lbl f.fn_body (call_cont k) in 574 573 (State(f,s',k',e,m,c),[]) … … 589 588 | Internal f -> 590 589 let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in 591 592 590 (* initializing loop indices *) 591 let c = CostLabel.new_const_ind c in 593 592 State (f, f.fn_body, cont, e, mem', c) 594 593 | External(id,targs,tres) when List.length targs = List.length args -> … … 601 600 | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[]) 602 601 | Returnstate(v,Kcall(None,f,e,k),m,c) -> 603 604 602 let c = CostLabel.forget_const_ind c in 603 (State(f,Sskip,k,e,m,c),[]) 605 604 | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) -> 606 605 let c = CostLabel.forget_const_ind c in -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml
r1421 r1539 16 16 17 17 let add_ending_cost_label indexing cost_universe stmt = 18 18 let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in 19 19 Clight.Ssequence (stmt, lbld_skip) 20 20 … … 75 75 76 76 let add_cost_labels_opt ind cost_universe = 77 77 Option.map (add_cost_labels_e ind cost_universe) 78 78 79 79 let add_cost_labels_lst ind cost_universe l = … … 82 82 83 83 (* Add cost labels to a statement. *) 84 85 let update_ind i ind = 86 match i with 87 | None -> ind 88 | Some _ -> CostLabel.add_id_indexing ind 84 89 85 90 let rec add_cost_labels_st ind cost_universe = function 86 91 | Sskip -> Sskip 87 92 | Sassign (e1,e2) -> 88 89 93 Sassign (add_cost_labels_e ind cost_universe e1, 94 add_cost_labels_e ind cost_universe e2) 90 95 | Scall (e1,e2,lst) -> 91 92 93 96 Scall (add_cost_labels_opt ind cost_universe e1, 97 add_cost_labels_e ind cost_universe e2, 98 add_cost_labels_lst ind cost_universe lst) 94 99 | Ssequence (s1,s2) -> 95 96 add_cost_labels_st ind cost_universe s2)100 Ssequence (add_cost_labels_st ind cost_universe s1, 101 add_cost_labels_st ind cost_universe s2) 97 102 | Sifthenelse (e,s1,s2) -> 98 99 100 101 102 103 let s1' = add_cost_labels_st ind cost_universe s1 in 104 let s1' = add_starting_cost_label ind cost_universe s1' in 105 let s2' = add_cost_labels_st ind cost_universe s2 in 106 let s2' = add_starting_cost_label ind cost_universe s2' in 107 Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2') 103 108 | Swhile (i,e,s) -> 104 let ind' = match i with 105 | None -> ind 106 | Some _ -> CostLabel.add_id_indexing ind in 107 let s' = add_cost_labels_st ind' cost_universe s in 108 let s' = add_starting_cost_label ind' cost_universe s' in 109 (* exit label indexed with outside indexing *) 110 add_ending_cost_label ind cost_universe 111 (Swhile (i,add_cost_labels_e ind cost_universe e, s')) 109 let ind' = update_ind i ind in 110 let s' = add_cost_labels_st ind' cost_universe s in 111 let s' = add_starting_cost_label ind' cost_universe s' in 112 (* exit label indexed with outside indexing *) 113 add_ending_cost_label ind cost_universe 114 (Swhile (i,add_cost_labels_e ind cost_universe e, s')) 112 115 | Sdowhile (i,e,s) -> 113 let ind' = match i with 114 | None -> ind 115 | Some _ -> CostLabel.add_id_indexing ind in 116 let s' = add_cost_labels_st ind' cost_universe s in 117 let s' = add_starting_cost_label ind' cost_universe s' in 118 add_ending_cost_label ind cost_universe 119 (Sdowhile (i,add_cost_labels_e ind cost_universe e, s')) 116 let ind' = update_ind i ind in 117 let s' = add_cost_labels_st ind' cost_universe s in 118 let s' = add_starting_cost_label ind' cost_universe s' in 119 add_ending_cost_label ind cost_universe 120 (Sdowhile (i,add_cost_labels_e ind cost_universe e, s')) 120 121 | Sfor (i,s1,e,s2,s3) -> 121 let s1' = add_cost_labels_st ind cost_universe s1 in 122 let ind' = match i with 123 | None -> ind 124 | Some _ -> CostLabel.add_id_indexing ind in 125 let s2' = add_cost_labels_st ind' cost_universe s2 in 126 let s3' = add_cost_labels_st ind' cost_universe s3 in 127 let s3' = add_starting_cost_label ind' cost_universe s3' in 128 add_ending_cost_label ind cost_universe 129 (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3')) 122 let s1' = add_cost_labels_st ind cost_universe s1 in 123 let ind' = update_ind i ind in 124 let s2' = add_cost_labels_st ind' cost_universe s2 in 125 let s3' = add_cost_labels_st ind' cost_universe s3 in 126 let s3' = add_starting_cost_label ind' cost_universe s3' in 127 add_ending_cost_label ind cost_universe 128 (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3')) 130 129 | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e) 131 130 | Sswitch (e,ls) -> 132 133 131 Sswitch (add_cost_labels_e ind cost_universe e, 132 add_cost_labels_ls ind cost_universe ls) 134 133 | Slabel (lbl,s) -> 135 136 137 134 let s' = add_cost_labels_st ind cost_universe s in 135 let s' = add_starting_cost_label ind cost_universe s' in 136 Slabel (lbl,s') 138 137 | Scost (_,_) -> assert false 139 138 | _ as stmt -> stmt … … 152 151 (* traversal of code assigning to every label the "loop address" of it. *) 153 152 (* A loop address like [2, 0, 1] means the corresponding label is in the *) 154 (* third loop inside the first loop inside the second loop of the body. The*)153 (* third loop inside the first loop inside the second loop of the body. *) 155 154 let rec assign_loop_addrs_s 156 155 (current : int list) 157 (offset : int) 158 (m : int list Label.Map.t) 159 : Clight.statement -> int*int list Label.Map.t = function 160 (* I am supposing you cannot jump to the update statement of for loops... *) 161 | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) -> 162 let (_, m) = assign_loop_addrs_s (offset :: current) 0 m s in 163 (offset + 1, m) 164 | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) -> 165 let (offset, m) = assign_loop_addrs_s current offset m s1 in 166 assign_loop_addrs_s current offset m s2 167 | Slabel(l,s) -> 168 let (offset, m) = assign_loop_addrs_s current offset m s in 169 (offset, Label.Map.add l current m) 170 | Sswitch(_,ls) -> assign_loop_addrs_ls current offset m ls 171 | _ -> (offset, m) 156 (offset : int) 157 (m : int list Label.Map.t) 158 : Clight.statement -> int*int list Label.Map.t = 159 function 160 (* I am supposing you cannot jump to the update statement of for loops... *) 161 | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) -> 162 let (_, m) = assign_loop_addrs_s (offset :: current) 0 m s in 163 (offset + 1, m) 164 | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) -> 165 let (offset, m) = assign_loop_addrs_s current offset m s1 in 166 assign_loop_addrs_s current offset m s2 167 | Slabel(l,s) -> 168 let (offset, m) = assign_loop_addrs_s current offset m s in 169 (offset, Label.Map.add l current m) 170 | Sswitch(_,ls) -> assign_loop_addrs_ls current offset m ls 171 | _ -> (offset, m) 172 172 173 173 and assign_loop_addrs_ls current offset m = function 174 174 | LSdefault s -> assign_loop_addrs_s current offset m s 175 175 | LScase(_,s,ls) -> 176 177 176 let (offset, m) = assign_loop_addrs_s current offset m s in 177 assign_loop_addrs_ls current offset m ls 178 178 179 179 let rec is_prefix l1 l2 = match l1, l2 with 180 181 182 180 | [], _ -> true 181 | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2 182 | _ -> false 183 183 184 184 (* traversal of code which for every statement [s] returns the set of loop*) … … 186 186 let rec find_multi_entry_loops_s 187 187 (m : int list Label.Map.t) 188 (current : int list) 189 (offset : int) 190 : Clight.statement -> int*IntListSet.t = function 191 (* I am supposing you cannot jump to the update statement of for loops... *) 192 | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) -> 193 let current' = offset :: current in 194 let (_, set) = find_multi_entry_loops_s m current' 0 s in 195 (offset + 1, set) 196 | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) -> 197 let (offset, set1) = find_multi_entry_loops_s m current offset s1 in 198 let (offset, set2) = find_multi_entry_loops_s m current offset s2 in 199 (offset, IntListSet.union set1 set2) 200 | Slabel(_,s) -> find_multi_entry_loops_s m current offset s 201 | Sgoto l -> 202 (* all labels should have a binding in m *) 203 let addr = Label.Map.find l m in 204 let cond = is_prefix addr current in 205 let set = if cond then IntListSet.empty else IntListSet.singleton addr in 206 (offset, set) 207 | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls 208 | _ -> (offset, IntListSet.empty) 188 (current : int list) 189 (offset : int) 190 : Clight.statement -> int*IntListSet.t = 191 function 192 (* I am supposing you cannot jump to the update statement of for loops... *) 193 | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) -> 194 let current' = offset :: current in 195 let (_, set) = find_multi_entry_loops_s m current' 0 s in 196 (offset + 1, set) 197 | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) -> 198 let (offset, set1) = find_multi_entry_loops_s m current offset s1 in 199 let (offset, set2) = find_multi_entry_loops_s m current offset s2 in 200 (offset, IntListSet.union set1 set2) 201 | Slabel(_,s) -> find_multi_entry_loops_s m current offset s 202 | Sgoto l -> 203 (* all labels should have a binding in m *) 204 let addr = Label.Map.find l m in 205 let cond = is_prefix addr current in 206 let set = if cond then IntListSet.empty else IntListSet.singleton addr in 207 (offset, set) 208 | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls 209 | _ -> (offset, IntListSet.empty) 209 210 210 211 and find_multi_entry_loops_ls m current offset = function … … 214 215 let (offset, set2) = find_multi_entry_loops_ls m current offset ls in 215 216 (offset, IntListSet.union set1 set2) 216 217 217 218 (* final pass where loops are indexed *) 218 219 let rec index_loops_s multi_entry current offset depth = function 219 (* I am supposing you cannot jump to the update statement of for loops... *) 220 | Swhile(_,b,s) -> 221 let current' = offset :: current in 222 let is_bad = IntListSet.mem current' multi_entry in 223 let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 224 let (_, s) = index_loops_s multi_entry current' 0 depth s in 225 (offset + 1, Swhile(i,b,s)) 226 | Sdowhile(_,b,s) -> 220 (* I am supposing you cannot jump to the update statement of for loops... *) 221 | Swhile(_,b,s) -> 227 222 let current' = offset :: current in 228 223 let is_bad = IntListSet.mem current' multi_entry in 229 224 let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 230 231 (offset + 1, Sdowhile(i,b,s))232 | Sfor(_,a1,a2,a3,s) ->225 let (_, s) = index_loops_s multi_entry current' 0 depth s in 226 (offset + 1, Swhile(i,b,s)) 227 | Sdowhile(_,b,s) -> 233 228 let current' = offset :: current in 234 229 let is_bad = IntListSet.mem current' multi_entry in 235 230 let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 236 let (_, s) = index_loops_s multi_entry current' 0 depth s in 237 (offset + 1, Sfor(i,a1,a2,a3,s)) 238 | Ssequence(s1,s2) -> 239 let (offset, s1) = index_loops_s multi_entry current offset depth s1 in 240 let (offset, s2) = index_loops_s multi_entry current offset depth s2 in 241 (offset, Ssequence(s1,s2)) 242 | Sifthenelse(b,s1,s2) -> 243 let (offset, s1) = index_loops_s multi_entry current offset depth s1 in 244 let (offset, s2) = index_loops_s multi_entry current offset depth s2 in 245 (offset, Sifthenelse(b,s1,s2)) 246 | Slabel(l,s) -> 247 let (offset, s) = index_loops_s multi_entry current offset depth s in 248 (offset, Slabel(l, s)) 249 | Sswitch(v,ls) -> 231 let (_, s) = index_loops_s multi_entry current' 0 depth s in 232 (offset + 1, Sdowhile(i,b,s)) 233 | Sfor(_,a1,a2,a3,s) -> 234 let current' = offset :: current in 235 let is_bad = IntListSet.mem current' multi_entry in 236 let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 237 let (_, s) = index_loops_s multi_entry current' 0 depth s in 238 (offset + 1, Sfor(i,a1,a2,a3,s)) 239 | Ssequence(s1,s2) -> 240 let (offset, s1) = index_loops_s multi_entry current offset depth s1 in 241 let (offset, s2) = index_loops_s multi_entry current offset depth s2 in 242 (offset, Ssequence(s1,s2)) 243 | Sifthenelse(b,s1,s2) -> 244 let (offset, s1) = index_loops_s multi_entry current offset depth s1 in 245 let (offset, s2) = index_loops_s multi_entry current offset depth s2 in 246 (offset, Sifthenelse(b,s1,s2)) 247 | Slabel(l,s) -> 248 let (offset, s) = index_loops_s multi_entry current offset depth s in 249 (offset, Slabel(l, s)) 250 | Sswitch(v,ls) -> 250 251 let (offset, s) = index_loops_ls multi_entry current offset depth ls in 251 252 252 (offset, Sswitch(v, ls)) 253 | _ as s -> (offset, s) 253 254 254 255 and index_loops_ls multi_entry current offset depth = function 255 256 | LSdefault s -> 256 let (offset, s) = index_loops_s multi_entry current offset depth s in 257 (offset, LSdefault s) 257 let (offset, s) = 258 index_loops_s multi_entry current offset depth s in 259 (offset, LSdefault s) 258 260 | LScase(v,s,ls) -> 259 261 let (offset, s) = index_loops_s multi_entry current offset depth s in 260 262 let (offset, ls) = index_loops_ls multi_entry current offset depth ls in 261 263 (offset, LScase(v,s,ls)) 262 264 263 265 (* Index loops and introduce cost labels in functions *) … … 271 273 (* index loops accordingly *) 272 274 let (_, body) = index_loops_s multi_entry [] 0 0 body in 273 274 275 276 277 278 279 275 (* initialize indexing *) 276 let ind = CostLabel.empty_indexing in 277 (* add cost labels inside *) 278 let body = add_cost_labels_st ind cost_universe body in 279 (* add cost label in front *) 280 let body = add_starting_cost_label ind cost_universe body in 281 (id,Internal {fd with fn_body = body}) 280 282 | _ as x -> x 281 283 … … 287 289 let add_cost_labels p = 288 290 let labs = ClightAnnotator.all_labels p in 289 290 291 let add = CostLabel.Atom.Set.add in 292 let empty = CostLabel.Atom.Set.empty in 291 293 let labs = StringTools.Set.fold add labs empty in 292 294 let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in 293 295 let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in 294 296 {p with prog_funct = List.map (process_f cost_universe) p.prog_funct} 295 -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightParser.ml
r818 r1539 1 let process file = 2 let tmp_file1 = Filename.temp_file "cparser1" ".c" 3 and tmp_file2 = Filename.temp_file "cparser2" ".i" 1 2 let process ?is_lustre_file ?remove_lustre_externals file = 3 let temp_dir = Filename.dirname file in 4 let tmp_file1 = Filename.temp_file ~temp_dir "cparser1" ".c" 5 and tmp_file2 = Filename.temp_file ~temp_dir "cparser2" ".i" 4 6 and prepro_opts = [] in 5 7 … … 8 10 try 9 11 let oc = open_out tmp_file1 in 12 if is_lustre_file = Some true || remove_lustre_externals = Some true then 13 output_string oc "#include<string.h>"; 10 14 output_string oc Primitive.prototypes ; 11 15 close_out oc … … 15 19 (Filename.quote file) (Filename.quote tmp_file1)) in 16 20 if rc <> 0 then ( 21 (* 17 22 Misc.SysExt.safe_remove tmp_file1; 23 *) 18 24 failwith "Error adding primitive prototypes." 19 25 ); … … 26 32 (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in 27 33 if rc <> 0 then ( 34 (* 28 35 Misc.SysExt.safe_remove tmp_file1; 29 36 Misc.SysExt.safe_remove tmp_file2; 37 *) 30 38 failwith "Error calling gcc." 31 39 ); … … 33 41 (* C to Cil *) 34 42 let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in 35 Misc.SysExt.safe_remove tmp_file1;36 Misc.SysExt.safe_remove tmp_file2;37 43 match r with 38 44 | None -> failwith "Error during C parsing." … … 41 47 (match ClightFromC.convertProgram p with 42 48 | None -> failwith "Error during C to Clight pass." 43 | Some(pp) -> pp 44 ) 49 | Some(pp) -> 50 Misc.SysExt.safe_remove tmp_file1; 51 Misc.SysExt.safe_remove tmp_file2; 52 if remove_lustre_externals = Some true then ClightLustre.simplify pp 53 else pp) -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightParser.mli
r486 r1539 2 2 [CIL]. *) 3 3 4 (** [process filename] parses the contents of [filename] to obtain 5 an abstract syntax tree that represents a Clight program. *) 6 val process : string -> Clight.program 4 (** [process ?is_lustre_file ?remove_lustre_externals filename] parses the 5 contents of [filename] to obtain an abstract syntax tree that represents a 6 Clight program. *) 7 val process : 8 ?is_lustre_file:bool -> ?remove_lustre_externals:bool -> 9 string -> Clight.program -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightPrinter.ml
r1392 r1539 197 197 fprintf p "%a.%s" print_expr_prec (level, e1) id 198 198 | Ecost(lbl, e1) -> 199 200 201 199 (* printing label uglily even if in comment for consistence *) 200 let lbl = CostLabel.string_of_cost_label lbl in 201 fprintf p "(/* %s */ %a)" lbl print_expr e1 202 202 | Ecall(f, arg, e) -> 203 203 fprintf p "(%s(%a), %a)" f print_expr arg print_expr e … … 218 218 219 219 let print_loop_depth p = function 220 221 220 | None -> fprintf p "" 221 | Some x -> fprintf p "/* single entry loop depth: %d */@," x 222 222 223 223 let rec print_stmt p s = … … 248 248 print_stmt s2 249 249 | Swhile(i, e, s) -> 250 251 252 253 250 fprintf p "@[<v 0>%a@[<v 2>while (%a) {@ %a@;<0 -2>}@]@]" 251 print_loop_depth i 252 print_expr e 253 print_stmt s 254 254 | Sdowhile(i, e, s) -> 255 256 257 258 255 fprintf p "@[<v 0>%a@[<v 2>do {@ %a@;<0 -2>} while(%a);@]@]" 256 print_loop_depth i 257 print_stmt s 258 print_expr e 259 259 | Sfor(i, s_init, e, s_iter, s_body) -> 260 261 262 263 264 265 260 fprintf p "@[<v 0>%a@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]@]" 261 print_loop_depth i 262 print_stmt_for s_init 263 print_expr e 264 print_stmt_for s_iter 265 print_stmt s_body 266 266 | Sbreak -> 267 267 fprintf p "break;" 268 268 | Scontinue -> 269 269 fprintf p "continue;" 270 270 | Sswitch(e, cases) -> 271 272 273 271 fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]" 272 print_expr e 273 print_cases cases 274 274 | Sreturn None -> 275 275 fprintf p "return;" 276 276 | Sreturn (Some e) -> 277 277 fprintf p "return %a;" print_expr e 278 278 | Slabel(lbl, s1) -> 279 279 fprintf p "%s:@ %a" lbl print_stmt s1 280 280 | Sgoto lbl -> 281 282 | Scost (lbl,s1) ->283 281 fprintf p "goto %s;" lbl 282 | Scost (lbl,s1) -> 283 let lbl = CostLabel.string_of_cost_label lbl in 284 284 fprintf p "%s:@ %a" lbl print_stmt s1 285 285 … … 481 481 | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e 482 482 | Sfor(_, s_init, e, s_iter, s_body) -> 483 484 483 collect_stmt s_init; collect_expr e; 484 collect_stmt s_iter; collect_stmt s_body 485 485 | Sbreak -> () 486 486 | Scontinue -> () -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightSwitch.ml
r818 r1539 6 6 let type_of (Clight.Expr (_, t)) = t 7 7 8 let rec simplify_switch e cases stmts = match cases, stmts with9 | Clight.LSdefault _, stmt :: _ -> stmt10 | Clight.LScase (i, _, lbl_stmts), stmt :: stmts ->11 let next_cases = simplify_switch e lbl_stmts stmts in12 let ret_type = Clight.Tint (Clight.I32, AST.Signed) in13 let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in14 let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in15 Clight.Sifthenelse (test, stmt, next_cases)16 | _ -> assert false (* do not use on these arguments *)17 8 18 9 let f_expr e _ = e 19 10 20 let f_stmt stmt sub_exprs_res sub_stmts_res = match stmt, sub_stmts_res with 21 | Clight.Sswitch (e, cases), sub_stmts -> simplify_switch e cases sub_stmts 22 | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res 11 let f_stmt lbl stmt sub_exprs_res sub_stmts_res = 12 match stmt, sub_stmts_res with 13 | Clight.Sbreak, _ -> Clight.Sgoto lbl 14 | Clight.Swhile _, _ | Clight.Sdowhile _, _ 15 | Clight.Sfor _, _ | Clight.Sswitch _, _ -> stmt 16 | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res 23 17 24 let simplify_statement = ClightFold.statement2 f_expr f_stmt18 let replace_undeep_break lbl = ClightFold.statement2 f_expr (f_stmt lbl) 25 19 26 let simplify_fundef = function 20 21 let add_starting_lbl fresh stmt = 22 let lbl = fresh () in 23 (lbl, Clight.Slabel (lbl, stmt)) 24 25 let add_starting_lbl_list fresh stmts = List.map (add_starting_lbl fresh) stmts 26 27 let add_ending_goto lbl stmt = 28 Clight.Ssequence (stmt, Clight.Slabel (lbl, Clight.Sskip)) 29 30 let make_sequence stmts = 31 let f sequence stmt = Clight.Ssequence (sequence, stmt) in 32 List.fold_left f Clight.Sskip stmts 33 34 let simplify_switch fresh e cases stmts = 35 let exit_lbl = fresh () in 36 let (lbls, stmts) = List.split (add_starting_lbl_list fresh stmts) in 37 let stmts = List.map (replace_undeep_break exit_lbl) stmts in 38 let rec aux cases lbls = match cases, lbls with 39 | Clight.LSdefault _, lbl :: _ -> [Clight.Sgoto lbl] 40 | Clight.LScase (i, _, cases), lbl :: lbls -> 41 let next_cases = aux cases lbls in 42 let ret_type = Clight.Tint (Clight.I32, AST.Signed) in 43 let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in 44 let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in 45 Clight.Sifthenelse (test, Clight.Sgoto lbl, Clight.Sskip) :: next_cases 46 | _ -> 47 (* Do not use on these arguments: wrong list size. *) 48 assert false in 49 add_ending_goto exit_lbl (make_sequence ((aux cases lbls) @ stmts)) 50 51 let f_expr e _ = e 52 53 let f_stmt fresh stmt sub_exprs_res sub_stmts_res = 54 match stmt, sub_stmts_res with 55 | Clight.Sswitch (e, cases), sub_stmts -> 56 simplify_switch fresh e cases sub_stmts 57 | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res 58 59 let simplify_statement fresh = ClightFold.statement2 f_expr (f_stmt fresh) 60 61 let simplify_fundef fresh = function 27 62 | Clight.Internal cfun -> 28 let cfun = 29 { cfun with Clight.fn_body = simplify_statement cfun.Clight.fn_body } in 30 Clight.Internal cfun 63 let fn_body = simplify_statement fresh cfun.Clight.fn_body in 64 Clight.Internal { cfun with Clight.fn_body = fn_body } 31 65 | fundef -> fundef 32 66 33 67 let simplify p = 34 let f (id, fundef) = (id, simplify_fundef fundef) in 68 let labels = ClightAnnotator.all_labels p in 69 let fresh = StringTools.make_fresh labels "_tmp_switch" in 70 let f (id, fundef) = (id, simplify_fundef fresh fundef) in 35 71 { p with Clight.prog_funct = List.map f p.Clight.prog_funct } -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightToCminor.ml
r1473 r1539 217 217 let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset)) 218 218 219 let sort_globals stack_vars globals var_locs =219 let sort_globals stack_vars globals functs var_locs = 220 220 let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in 221 let f_functs (id, fundef) = 222 let (params, return) = match fundef with 223 | Clight.Internal cfun -> 224 (List.map snd cfun.Clight.fn_params, cfun.Clight.fn_return) 225 | Clight.External (_, params, return) -> (params, return) in 226 (id, Clight.Tfunction (params, return)) in 227 let functs = List.map f_functs functs in 228 let globals = globals @ functs in 221 229 sort_vars Global None stack_vars globals var_locs 222 230 … … 225 233 globals. *) 226 234 227 let sort_variables globals cfun =235 let sort_variables globals functs cfun = 228 236 let stack_vars = stack_vars cfun in 229 237 let var_locs = empty_var_locs in 230 let var_locs = sort_globals stack_vars globals var_locs in238 let var_locs = sort_globals stack_vars globals functs var_locs in 231 239 let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in 232 240 let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in … … 439 447 440 448 and translate_addrof_ident res_type var_locs id = 449 assert (mem_var_locs id var_locs) ; 441 450 match find_var_locs id var_locs with 442 | (Local, _) | (Param, _) -> assert false (* typeerror *)451 | (Local, _) | (Param, _) -> assert false (* location error *) 443 452 | (LocalStack off, _) | (ParamStack off, _) -> 444 453 Cminor.Expr (add_stack off, res_type) … … 487 496 488 497 let ind_0 i stmt = match i with 489 490 498 | None -> stmt 499 | Some x -> Cminor.St_ind_0(x, stmt) 491 500 492 501 let ind_inc i stmt = match i with 493 494 502 | None -> stmt 503 | Some x -> Cminor.St_ind_inc(x, stmt) 495 504 496 505 let trans_for = 497 let f_expr e _ = e in 498 let f_stmt stmt expr_res stmt_res = match expr_res, stmt_res, stmt with 499 | e::_, s1::s2::s3::_, Clight.Sfor(i,_,_,_,_) -> 500 Clight.Ssequence(s1,Clight.Swhile(i,e, 501 Clight.Ssequence(s3, s2))) 502 | exprs, sub_sts, stm -> ClightFold.statement_fill_subs stm exprs sub_sts in 503 ClightFold.statement2 f_expr f_stmt 506 let f_expr e _ = e in 507 let f_stmt stmt expr_res stmt_res = match expr_res, stmt_res, stmt with 508 | e::_, s1::s2::s3::_, Clight.Sfor(i,_,_,_,_) -> 509 Clight.Ssequence(s1,Clight.Swhile(i,e, 510 Clight.Ssequence(s3, s2))) 511 | exprs, sub_sts, stm -> 512 ClightFold.statement_fill_subs stm exprs sub_sts in 513 ClightFold.statement2 f_expr f_stmt 514 515 let cmp_complement = function 516 | AST.Cmp_eq -> AST.Cmp_ne 517 | AST.Cmp_ne -> AST.Cmp_eq 518 | AST.Cmp_gt -> AST.Cmp_le 519 | AST.Cmp_ge -> AST.Cmp_lt 520 | AST.Cmp_lt -> AST.Cmp_ge 521 | AST.Cmp_le -> AST.Cmp_gt 522 523 let negate_expr (Cminor.Expr (_, et) as e) = 524 let ed' = Cminor.Op1 (AST.Op_notbool, e) in 525 Cminor.Expr(ed', et) 504 526 505 527 let rec translate_stmt fresh var_locs cnt_lbl br_lbl = function … … 508 530 509 531 | Clight.Sassign (e1, e2) -> 510 532 let e2 = translate_expr var_locs e2 in 511 533 ([], assign var_locs e1 e2) 512 534 513 535 | Clight.Scall (None, f, args) -> 514 515 536 let f = translate_expr var_locs f in 537 let args = List.map (translate_expr var_locs) args in 516 538 ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args)) 517 539 518 540 | Clight.Scall (Some e, f, args) -> 519 520 541 let f = translate_expr var_locs f in 542 let args = List.map (translate_expr var_locs) args in 521 543 let t = sig_type_of_ctype (clight_type_of e) in 522 544 let tmp = fresh () in … … 528 550 529 551 | Clight.Swhile (i,e,stmt) -> 530 let loop_lbl = fresh () in 531 let llbl_opt = Some loop_lbl in 532 let exit_lbl = fresh () in 533 let elbl_opt = Some exit_lbl in 534 let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in 535 let e = translate_expr var_locs e in 536 let jmp lbl = Cminor.St_goto lbl in 552 let loop_lbl = fresh () in 553 let llbl_opt = Some loop_lbl in 554 let exit_lbl = fresh () in 555 let elbl_opt = Some exit_lbl in 556 let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in 557 let e = translate_expr var_locs e in 558 let jmp lbl = Cminor.St_goto lbl in 559 (* let econd = negate_expr e in *) 537 560 let scond = 538 561 Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in 539 540 541 562 let loop = 563 Cminor.St_seq(scond,Cminor.St_seq (stmt, ind_inc i (jmp loop_lbl))) in 564 let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in 542 565 (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip))) 543 566 544 567 | Clight.Sdowhile (i,e,stmt) -> 545 546 547 548 568 let loop_lbl = fresh () in 569 let llbl_opt = Some loop_lbl in 570 let exit_lbl = fresh () in 571 let elbl_opt = Some exit_lbl in 549 572 let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in 550 573 let e = translate_expr var_locs e in … … 552 575 let scond = 553 576 Cminor.St_ifthenelse (e, ind_inc i (jmp loop_lbl), Cminor.St_skip) in 554 577 let loop = 555 578 Cminor.St_seq (stmt, scond) in 556 579 let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in 557 580 (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip))) 558 581 559 582 | Clight.Sfor _ -> assert false (* transformed *) 560 583 … … 571 594 572 595 | Clight.Sbreak -> 573 574 575 576 596 let br_lbl = match br_lbl with 597 | Some x -> x 598 | None -> invalid_arg("break without enclosing scope") in 599 ([], Cminor.St_goto br_lbl) 577 600 578 601 | Clight.Scontinue -> 579 580 581 602 let cnt_lbl = match cnt_lbl with 603 | Some x -> x 604 | None -> invalid_arg("continue without enclosing scope") in 582 605 ([], Cminor.St_goto cnt_lbl) 583 606 | Clight.Sswitch _ -> … … 589 612 590 613 | Clight.Sreturn (Some e) -> 591 592 614 let e = translate_expr var_locs e in 615 ([], Cminor.St_return (Some e)) 593 616 594 617 | Clight.Slabel (lbl, stmt) -> 595 596 618 let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in 619 (tmps, Cminor.St_label (lbl, stmt)) 597 620 598 621 | Clight.Sgoto lbl -> ([], Cminor.St_goto lbl) 599 622 600 623 | Clight.Scost (lbl, stmt) -> 601 602 624 let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in 625 (tmps, Cminor.St_cost (lbl, stmt)) 603 626 604 627 (* | _ -> assert false (* type error *) *) … … 619 642 fold_var_locs f var_locs body 620 643 621 let translate_internal fresh globals cfun =622 let var_locs = sort_variables globals cfun in644 let translate_internal fresh globals functs cfun = 645 let var_locs = sort_variables globals functs cfun in 623 646 let params = 624 647 List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in 625 626 648 let body = cfun.Clight.fn_body in 649 let body = trans_for body in 627 650 let (tmps, body) = translate_stmt fresh var_locs None None body in 628 651 let body = add_stack_parameters_initialization var_locs body in … … 638 661 AST.res = type_return_of_ctype return } } 639 662 640 let translate_funct fresh globals (id, def) =663 let translate_funct fresh globals functs (id, def) = 641 664 let def = match def with 642 | Clight.Internal ff -> Cminor.F_int (translate_internal fresh globals ff) 665 | Clight.Internal ff -> 666 Cminor.F_int (translate_internal fresh globals functs ff) 643 667 | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in 644 668 (id, def) … … 646 670 let translate p = 647 671 let fresh = ClightAnnotator.make_fresh "_tmp" p in 672 let translate_funct = 673 translate_funct fresh p.Clight.prog_vars p.Clight.prog_funct in 648 674 { Cminor.vars = List.map translate_global p.Clight.prog_vars ; 649 Cminor.functs = 650 List.map (translate_funct fresh p.Clight.prog_vars) p.Clight.prog_funct ; 675 Cminor.functs = List.map translate_funct p.Clight.prog_funct ; 651 676 Cminor.main = p.Clight.prog_main } -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/runtime.ml
r818 r1539 36 36 function *) 37 37 (string -> string) * 38 (* dependenc es *)38 (* dependencies *) 39 39 operation list 40 40 -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminor.mli
r1392 r1539 39 39 40 40 (* Switch. Parameters are the expression whose value is switch, a 41 table of cases and their corresponding number of blocks to exit,42 and the number of block to exitin the default case. *)41 table of cases and their corresponding labels to go to, 42 and the label to go to in the default case. *) 43 43 | St_switch of expression * (int*Label.t) list * Label.t 44 44 … … 47 47 | St_goto of Label.t 48 48 | St_cost of CostLabel.t * statement 49 49 | St_ind_0 of CostLabel.index * statement 50 50 | St_ind_inc of CostLabel.index * statement 51 51 -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorAnnotator.ml
r1291 r1539 204 204 let all_labels p = 205 205 let (cost_labels, user_labels) = prog_labels p in 206 206 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 207 207 let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 208 208 Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorFold.ml
r1392 r1539 45 45 (*| Cminor.St_loop stmt | Cminor.St_block stmt *) 46 46 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) 47 48 47 | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (_, stmt) -> 48 ([], [stmt]) 49 49 50 50 let statement_fill_subs stmt sub_es sub_stmts = -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml
r1392 r1539 70 70 | St_goto lbl -> "goto " ^ lbl 71 71 | St_cost (lbl, _) -> 72 73 74 75 72 let lbl = CostLabel.string_of_cost_label lbl in 73 "cost " ^ lbl 74 | St_ind_0 (i, _) -> "reset " ^ string_of_int i ^ " to 0" 75 | St_ind_inc (i, _) -> "post-increment " ^ string_of_int i 76 76 77 77 let print_state = function … … 81 81 (Mem.to_string mem) 82 82 (Val.to_string (value_of_address sp)); 83 84 85 83 let ind = CostLabel.curr_const_ind i in 84 CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) ind; 85 Printf.printf "\nRegular state: %s\n\n%!" 86 86 (string_of_statement stmt) 87 87 | State_call (_, args, _, mem,_) -> … … 233 233 let rec callcont = function 234 234 | Ct_cont(_,k) (*| Ct_endblock k *) -> callcont k 235 235 | (Ct_stop | Ct_returnto _) as k -> k 236 236 237 237 let findlabel lbl st k = … … 244 244 | St_seq(s1,s2) -> 245 245 (match fdlbl (Ct_cont(s2,k)) s1 with 246 247 246 None -> fdlbl k s2 247 | Some(v) -> Some(v) 248 248 ) 249 249 | St_ifthenelse(_,s1,s2) -> 250 250 (match fdlbl k s1 with 251 252 251 None -> fdlbl k s2 252 | Some(v) -> Some(v) 253 253 ) 254 254 (* | St_loop(s) -> fdlbl (Ct_cont(St_loop(s),k)) s … … 260 260 | St_goto(_) -> None 261 261 | St_cost(_,s) | St_label(_,s) 262 262 | St_ind_0(_,s) | St_ind_inc(_,s) -> fdlbl k s 263 263 in match fdlbl k st with 264 264 None -> assert false (*Wrong label*) … … 315 315 if Val.is_int v then 316 316 try 317 318 319 320 321 322 317 let v = Val.to_int v in 318 let lbl = 319 try 320 List.assoc v lst 321 with 322 | Not_found -> def in 323 323 let (s',k') = findlabel lbl f.f_body (callcont k) in 324 324 (State_regular(f, s', k', sigma, e, m, i),l) 325 325 with _ -> error "int value too big." 326 326 else error "undefined switch value." … … 333 333 (* applying current indexing on label *) 334 334 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind i) lbl in 335 336 337 338 339 340 335 (State_regular(f,s,k,sigma,e,m,i),[lbl]) 336 | St_ind_0(ind,s),_ -> 337 CostLabel.enter_loop i ind; 338 (State_regular(f,s,k,sigma,e,m,i), []) 339 | St_ind_inc(ind,s),_ -> 340 CostLabel.continue_loop i ind; 341 341 (State_regular(f,s,k,sigma,e,m,i), []) 342 342 (* | _ -> error "state malformation." *) … … 357 357 let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in 358 358 let lenv = init_local_env vargs f.f_params f.f_vars in 359 359 let i = CostLabel.new_const_ind i in 360 360 State_regular(f,f.f_body,k,sp,lenv,m,i) 361 361 | F_ext f -> interpret_external k m i f.ef_tag vargs … … 365 365 | State_call(fun_def,vargs,k,m,i) -> (step_call vargs k m i fun_def,[]) 366 366 | State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) -> 367 367 let i = CostLabel.forget_const_ind i in 368 368 (State_regular(f,St_skip,k,sigma,e,m,i),[]) 369 369 | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) -> … … 404 404 | Some main -> 405 405 let mem = init_mem prog in 406 406 let main = find_fundef main mem in 407 407 let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in 408 408 exec debug [] first_state -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorPrinter.ml
r1392 r1539 116 116 (add_parenthesis e3) 117 117 | Cminor.Exp_cost (lab, e) -> 118 118 let lab = CostLabel.string_of_cost_label lab in 119 119 Printf.sprintf "/* %s */ %s" lab (print_expression e) 120 120 and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with … … 215 215 Printf.sprintf "%sgoto %s;\n" (n_spaces n) lbl 216 216 | Cminor.St_cost (lbl, s) -> 217 217 let lbl = CostLabel.string_of_cost_label lbl in 218 218 Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s) 219 220 221 222 219 | Cminor.St_ind_0 (i, s) -> 220 Printf.sprintf "%sindex %d:\n%s" (n_spaces n) i (print_body n s) 221 | Cminor.St_ind_inc (i,s) -> 222 Printf.sprintf "%sincrement %d:\n%s\n" (n_spaces n) i (print_body n s) 223 223 224 224 let print_internal f_name f_def = … … 265 265 | Cminor.St_goto(_) -> "goto" 266 266 | Cminor.St_cost(_,_) -> "cost" 267 268 267 | Cminor.St_ind_0 _ -> "index" 268 | Cminor.St_ind_inc _ -> "increment" -
Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorToRTLabs.ml
r1477 r1539 194 194 let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in 195 195 let old_entry = rtlabs_fun.RTLabs.f_entry in 196 197 196 let r1_arg = RTLabs.Reg r1 in 197 let r2_arg = RTLabs.Reg r2 in 198 198 let stmt = RTLabs.St_op2 (op2, destr, r1_arg, r2_arg, old_entry) in 199 199 let rtlabs_fun = generate rtlabs_fun stmt in … … 204 204 let old_entry = rtlabs_fun.RTLabs.f_entry in 205 205 let stmt = 206 206 RTLabs.St_load (chunk, RTLabs.Reg r, destr, old_entry) in 207 207 let rtlabs_fun = generate rtlabs_fun stmt in 208 208 translate_expr rtlabs_fun lenv r e … … 287 287 let old_entry = rtlabs_fun.RTLabs.f_entry in 288 288 let stmt = 289 289 RTLabs.St_store (chunk, RTLabs.Reg addr, RTLabs.Reg r, old_entry) in 290 290 let rtlabs_fun = generate rtlabs_fun stmt in 291 291 translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2] … … 325 325 326 326 | Cminor.St_seq (s1, s2) -> 327 let rtlabs_fun = translate_stmt rtlabs_fun lenv s2 in328 translate_stmt rtlabs_fun lenv (* exits*) s1327 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in 328 translate_stmt rtlabs_fun lenv (*exits*) s1 329 329 330 330 | Cminor.St_ifthenelse (e, s1, s2) -> 331 331 let old_entry = rtlabs_fun.RTLabs.f_entry in 332 let rtlabs_fun = translate_stmt rtlabs_fun lenv s2 in332 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in 333 333 let lbl_false = rtlabs_fun.RTLabs.f_entry in 334 334 let rtlabs_fun = change_entry rtlabs_fun old_entry in 335 let rtlabs_fun = translate_stmt rtlabs_fun lenv s1 in335 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s1 in 336 336 let lbl_true = rtlabs_fun.RTLabs.f_entry in 337 337 translate_branch rtlabs_fun lenv e lbl_true lbl_false … … 366 366 367 367 | Cminor.St_label (lbl, s) -> 368 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in368 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in 369 369 let old_entry = rtlabs_fun.RTLabs.f_entry in 370 370 add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry) 371 371 372 372 | Cminor.St_cost (lbl, s) -> 373 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in373 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in 374 374 let old_entry = rtlabs_fun.RTLabs.f_entry in 375 375 generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) … … 460 460 461 461 (* Complete the graph *) 462 translate_stmt rtlabs_fun lenv f_def.Cminor.f_body462 translate_stmt rtlabs_fun lenv (*[]*) f_def.Cminor.f_body 463 463 464 464 -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml
r1433 r1539 1 1 module Atom = 2 3 4 2 struct 3 include StringTools 4 end 5 5 6 6 module StringMap = Map.Make(String) … … 35 35 36 36 let continue_loop_single indexing n = 37 38 39 40 37 try 38 ExtArray.set indexing n (ExtArray.get indexing n + 1) 39 with | _ -> 40 invalid_arg "uninitialized loop index" 41 41 42 42 let curr_ind = function … … 172 172 let constant_map d x = 173 173 Set.fold (fun k accu -> Map.add k x accu) d Map.empty 174 175 176 (** **) -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli
r1433 r1539 2 2 (** This module provides functions to manipulate and create indexed cost 3 3 labels. *) 4 4 5 5 (** [Atom] provides functions for cost atoms, the root of indexed costs *) 6 6 module Atom : sig 7 7 include StringSig.S 8 8 end 9 9 … … 12 12 type sexpr = Sexpr of int*int 13 13 14 (** The identity simple expression, used in initialization. *) 14 15 val sexpr_id : sexpr 15 16 16 (* trying a nameless approach*)17 (** Indexes are identified with (single-entry) loop depths. *) 17 18 type index = int 18 19 20 (** [make_id prefix index] produces an identifier out of a 21 prefix and a loop depth. *) 19 22 val make_id : string -> index -> string 20 23 21 24 type indexing = sexpr list 22 25 26 (** The type of constant indexings, to be used by interpreations *) 23 27 type const_indexing 24 28 29 (** [const_ind_iter f c] iterates [f] over the values of indexes in c *) 25 30 val const_ind_iter : (int -> unit) -> const_indexing -> unit 26 31 27 (** T op of the stack.28 @raise[Invalid_argument "non-empty indexing stack"] if argument is empty *)32 (** This is equivalent to [List.hd], but raises 33 [Invalid_argument "non-empty indexing stack"] if argument is empty *) 29 34 val curr_const_ind : const_indexing list -> const_indexing 30 35 31 36 (** [enter_loop inds n] is used to update the indexing stack [ind] when one 32 37 is entering a loop indexed by [n]. Raises [Invalid_argument 33 38 "non-empty indexing stack"] if [inds] is empty. *) 34 39 val enter_loop : const_indexing list -> index -> unit 35 40 36 41 (** [enter_loop_opt inds (Some n)] behaves like [enter_loop inds n], and does 37 42 nothing in case of [None]. 38 43 @see enter_loop *) 39 44 val enter_loop_opt : const_indexing list -> index option -> unit 40 45 41 46 (** [continue_loop inds n] is used to update the indexing stack [inds] when 42 47 one is continuing a loop indexed by [n]. 43 44 45 48 @raise [Invalid_argument "non-empty indexing stack"] if [inds] is empty. 49 @raise [Invalid_argument "uninitialized loop index"] if the head of 50 [inds] has no value for [index]. *) 46 51 val continue_loop : const_indexing list -> index -> unit 47 52 … … 57 62 (** [forget_const_ind inds] pops and discards the top constant indexing from the 58 63 stack [inds]. Raises [Invalid_argument "non-empty indexing stack"] if 59 64 [inds] is empty. *) 60 65 val forget_const_ind : const_indexing list -> const_indexing list 61 66 62 63 64 65 (** [empty_indexing] generates an empty indexing *) 67 (** [empty_indexing] is the empty indexing *) 66 68 val empty_indexing : indexing 67 69 … … 72 74 73 75 type t = { 74 75 76 name : Atom.t; 77 i : indexing 76 78 } 77 79 … … 80 82 val comp_index : index -> sexpr -> t -> t 81 83 82 83 84 (** [ev_indexing ind lbl] returns [lbl] where its indexing has been 84 85 evaluated in the constant indexing [ind]. 85 86 86 @raise Invalid_argument "constant indexing not enough to be applied" if 87 [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *) 87 88 val ev_indexing : const_indexing -> t -> t 88 89 89 90 (** [string_of_cost_label pref t] converts an indexed label to a 90 string suitable for a label name in source91 91 string suitable for a label name in C source. 92 [string_of_cost_label ~pretty:true t] prints a more readable form *) 92 93 val string_of_cost_label : ?pretty : bool -> t -> string 93 94 … … 106 107 [x] to every element of the set [d]. *) 107 108 val constant_map : Set.t -> 'a -> 'a Map.t 108 109 -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/label.ml
r1468 r1539 26 26 27 27 end 28 -
Deliverables/D2.2/8051-indexed-labels-branch/src/common/label.mli
r1468 r1539 7 7 (** Imperative label maps for use with Fix *) 8 8 module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t) 9 -
Deliverables/D2.2/8051-indexed-labels-branch/src/dev_test.ml
r1433 r1539 8 8 let do_dev_test (filenames : string list) : unit = 9 9 10 let main_lbl = "main" in 11 let exit_lbl = "exit" in 12 let lbl = "label" in 13 14 let code = 15 [(* Prelude *) 16 `Call main_lbl ; (* call main *) 17 `Label exit_lbl ; (* when coming back from main, do an infinite 18 jump here *) 19 `Jmp exit_lbl ; 20 (* Main *) 21 `Label main_lbl ; 22 `Mov (`DPTR, lbl) ; (* fetch the address of lbl in DPTR *) 23 (* Push the address of lbl on the stack. *) 24 `PUSH (I8051.reg_addr I8051.dpl) ; (* low bytes first *) 25 `PUSH (I8051.reg_addr I8051.dph) ; (* then high bytes *) 26 `RET ; (* this should jump to lbl, i.e. right below *) 27 `Label lbl ; 28 `RET (* jump to the exit label *)] in 29 30 (* Create a labelled ASM program with the code. *) 31 let prog = 32 { ASM.ppreamble = [] ; 33 ASM.pexit_label = exit_lbl ; 34 ASM.pcode = code ; 35 ASM.phas_main = true } in 36 37 (* Assemble it. *) 38 let prog = Languages.AstASM (ASMInterpret.assembly prog) in 39 40 (* Save the result in a fresh file prefixed by "yop" and whose extension is 41 "hex". *) 42 Languages.save false false "yop" "" prog 43 44 (* 10 45 let f filename = 11 12 13 14 15 16 17 18 19 let ps = Languages.compile false []Languages.Clight target p in20 21 22 23 24 25 [(print, Languages.save false filename "") ;26 27 46 Printf.printf "Processing %s...\n%!" filename ; 47 let target = Languages.RTL in 48 let print = false in 49 let debug = true in 50 let interpret = true in 51 let p = Languages.parse Languages.Clight filename in 52 let p = Languages.add_runtime p in 53 let p = Languages.labelize p in 54 let ps = Languages.compile false Languages.Clight target p in 55 let f f' p = match Languages.language_of_ast p with 56 | l when l = target -> f' p 57 | _ -> () 58 in 59 let actions = 60 [(print, Languages.save false false filename "") ; 61 (interpret, (fun p -> ignore (Languages.interpret debug p)))] in 62 List.iter (fun (b, f') -> if b then List.iter (f f') ps else ()) actions 28 63 in 29 64 30 65 List.iter f filenames 66 *) -
Deliverables/D2.2/8051-indexed-labels-branch/src/languages.ml
r1507 r1539 53 53 | language -> [to_string language] 54 54 55 let parse = function55 let parse ?is_lustre_file ?remove_lustre_externals = function 56 56 | Clight -> 57 fun filename -> AstClight (ClightParser.process filename) 57 fun filename -> 58 AstClight 59 (ClightParser.process ?is_lustre_file ?remove_lustre_externals filename) 58 60 59 61 (* … … 113 115 114 116 let ltl_to_lin = function 115 | AstLTL p -> 117 | AstLTL p -> 116 118 AstLIN (LTLToLIN.translate p) 117 119 | _ -> assert false 118 120 119 121 let lin_to_asm = function 120 | AstLIN p -> 122 | AstLIN p -> 121 123 AstASM (LINToASM.translate p) 122 124 | _ -> assert false … … 137 139 138 140 let insert_transformations ts chain = 139 140 141 142 143 144 145 146 141 (* turn transformation into elements of the compilation chain *) 142 let trans_to_comp (n, t) = (n, n, t) in 143 let ts = List.map trans_to_comp ts in 144 (* ts and chain are merged, and then sorted so that the resulting list is *) 145 (* still a well formed compilation chain. Stable sort preserves order *) 146 (* between transformations on the same language as appearing in ts *) 147 let compare (n1, n2, s) (m1, m2, t) = compare (n1, n2) (m1, m2) in 148 List.stable_sort compare (ts @ chain) 147 149 148 150 let compile debug ts src tgt = 149 151 (* insert intermediate transformations *) 150 152 let chain = insert_transformations ts compilation_chain in 151 152 153 (* erase transformations whose source is strictly before src *) 154 let chain = List.filter (function (l1, _, _) -> l1 >= src) chain in 153 155 (* erase transformations whose target is strictly after tgt *) 154 156 let chain = List.filter (function (_, l2, _) -> l2 <= tgt) chain in 155 157 (* Compose the atomic translations to build a compilation function 156 158 from [src] to [tgt]. Again, we assume that the compilation chain … … 217 219 let instrument cost_tern costs_mapping = function 218 220 | AstClight p -> 219 let (p', cost_id, cost_incr ) =221 let (p', cost_id, cost_incr, extern_cost_variables) = 220 222 ClightAnnotator.instrument cost_tern p costs_mapping in 221 (AstClight p', cost_id, cost_incr )223 (AstClight p', cost_id, cost_incr, extern_cost_variables) 222 224 (* 223 225 | AstCminor p -> … … 230 232 "Instrumentation is not implemented for source language `%s'." 231 233 (to_string (language_of_ast p))); 232 (p, "", "" )234 (p, "", "", StringTools.Map.empty) 233 235 234 236 let annotate cost_tern input_ast final = … … 236 238 instrument cost_tern costs_mapping input_ast 237 239 238 let string_output = function240 let string_output asm_pretty = function 239 241 | AstClight p -> 240 242 [ClightPrinter.print_program p] … … 252 254 [LINPrinter.print_program p] 253 255 | AstASM p -> 254 [Pretty.print_program p ; ASMPrinter.print_program p] 255 256 let save exact_output filename suffix ast = 256 (if asm_pretty then [Pretty.print_program p] 257 else ["Pretty print not requested"]) @ 258 [ASMPrinter.print_program p] 259 260 let save asm_pretty exact_output filename suffix ast = 257 261 let ext_chopped_filename = 258 262 if exact_output then filename … … 267 271 if exact_output then ext_filenames 268 272 else List.map Misc.SysExt.alternative ext_filenames in 269 let output_strings = string_output as t in273 let output_strings = string_output asm_pretty ast in 270 274 let f filename s = 271 275 let cout = open_out filename in … … 275 279 List.iter2 f output_filenames output_strings 276 280 277 let save_cost filename cost_id cost_incr = 281 let save_cost exact_name filename cost_id cost_incr extern_cost_variables = 282 let filename = 283 if exact_name then filename 284 else 285 try Filename.chop_extension filename 286 with Invalid_argument ("Filename.chop_extension") -> filename in 278 287 let cout = open_out (filename ^ ".cerco") in 288 let f fun_name cost_var = 289 output_string cout (fun_name ^ " " ^ cost_var ^ "\n") in 279 290 output_string cout (cost_id ^ "\n"); 280 291 output_string cout (cost_incr ^ "\n"); 292 StringTools.Map.iter f extern_cost_variables; 281 293 flush cout; 282 294 close_out cout … … 299 311 | AstASM p -> 300 312 ASMInterpret.interpret debug p 313 314 let add_lustre_main 315 lustre_test lustre_test_cases lustre_test_cycles 316 lustre_test_min_int lustre_test_max_int = function 317 | AstClight p -> 318 AstClight 319 (ClightLustreMain.add lustre_test lustre_test_cases lustre_test_cycles 320 lustre_test_min_int lustre_test_max_int p) 321 | _ -> 322 Error.global_error "during main generation" 323 "Lustre testing is only available with C programs." -
Deliverables/D2.2/8051-indexed-labels-branch/src/languages.mli
r1507 r1539 39 39 val language_of_ast : ast -> name 40 40 41 (** [parse name] returns the parsing function of the language 42 [name]. *) 43 val parse : name -> (string -> ast) 41 (** [parse ?is_lustre_file ?remove_lustre_externals name] returns the parsing 42 function of the language [name]. *) 43 val parse : ?is_lustre_file:bool -> ?remove_lustre_externals:bool -> 44 name -> (string -> ast) 44 45 45 46 (** {2 Compilation} *) … … 47 48 (** [compile debug ts l1 l2] returns the compilation function that 48 49 translates the language [l1] to the language [l2], employing the 49 50 transformations in [ts] along the way . This may be the 50 51 composition of several compilation functions. If [debug] is 51 52 [true], all the intermediate programs are inserted in the … … 73 74 (** [annotate cost_tern input_ast target_ast] inserts cost annotations into the 74 75 input AST from the (final) target AST. It also returns the name of the cost 75 variable and the name of the cost increment function. The [cost_tern] flag 76 variable and the name of the cost increment function, and a the name of a fresh 77 uninitialized global variable for each external function. The [cost_tern] flag 76 78 rules whether cost increments are given by ternary expressions or branch 77 79 statements. *) 78 val annotate : bool -> ast -> ast -> (ast * string * string )80 val annotate : bool -> ast -> ast -> (ast * string * string * string StringTools.Map.t) 79 81 80 82 (** [interpret debug ast] runs the program [ast] from the default initial … … 84 86 (** {2 Serialization} *) 85 87 86 (** [save exact_output filename input_ast] pretty prints [input_ast] in a file 87 whose name is prefixed by [filename] and whose extension is deduced from the 88 language of the AST. If [exact_output] is false then the written file will 89 be fresh. *) 90 val save : bool -> string -> string -> ast -> unit 88 (** [save asm_pretty exact_output filename suffix input_ast] prints [input_ast] 89 in a file whose name is prefixed by [filename], suffixed by [suffix] and 90 whose extension is deduced from the language of the AST. If [exact_output] 91 is false then the written file will be fresh. If [asm_pretty] is true, then 92 an additional pretty-printed assembly file is output. *) 93 val save : bool -> bool -> string -> string -> ast -> unit 91 94 92 (** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the 93 cost variable and then the name [cost_incr] of the cost increment function 94 in a seperate line in the file prefixed by [filename] and extended with 95 (** [save_cost exact_name filename cost_id cost_incr extern_cost_variables] 96 prints the name [cost_id] of the cost variable, then the name [cost_incr] of 97 the cost increment function, and the entries of the mapping 98 [extern_cost_variables] (key first, then binding, seperated by a space) in a 99 seperate line in the file prefixed by [filename] and extended with 95 100 ".cost". If the file already exists, it is overwritten. *) 96 val save_cost : string -> string -> string -> unit 101 val save_cost : bool -> string -> string -> string -> 102 string StringTools.Map.t -> unit 97 103 98 104 (** [from_string s] parses [s] as an intermediate language name. *) … … 101 107 (** [to_string n] prints [n] as a string. *) 102 108 val to_string : name -> string 109 110 (** [add_lustre_main lustre_test lustre_test_cases lustre_test_cycles 111 lustre_test_min_int lustre_test_max_int ast] adds a main function that tests 112 a Lustre step function to a Clight AST. The file [lustre_test] contains 113 CerCo information (e.g. the name of the cost variable). The integer 114 [lustre_test_cases] is the number of test cases that are performed, and the 115 integer [lustre_test_cycles] is the number of cycles per test 116 case. [lustre_test_min_int] (resp. [lustre_test_max_int]) is the minimum 117 (resp. maximum) integer value randomly generated during testing, and. *) 118 val add_lustre_main : string -> int -> int -> int -> int -> ast -> ast -
Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml
r1507 r1539 40 40 let interpretation_requested () = !interpretation_flag 41 41 42 let trace_flag = ref false43 let request_ trace = (:=) trace_flag44 let trace_requested () = !trace_flag42 let interpretations_flag = ref false 43 let request_interpretations = (:=) interpretations_flag 44 let interpretations_requested () = !interpretations_flag 45 45 46 46 let debug_flag = ref false … … 56 56 let set_cost_ternary = (:=) cost_ternary_flag 57 57 let is_cost_ternary_enabled () = !cost_ternary_flag 58 59 let asm_pretty_flag = ref false 60 let set_asm_pretty = (:=) asm_pretty_flag 61 let is_asm_pretty () = !asm_pretty_flag 62 63 let lustre_flag = ref false 64 let set_lustre_file = (:=) lustre_flag 65 let is_lustre_file () = !lustre_flag 66 67 let remove_lustre_externals = ref false 68 let set_remove_lustre_externals = (:=) remove_lustre_externals 69 let is_remove_lustre_externals () = !remove_lustre_externals 70 71 let lustre_test = ref None 72 let set_lustre_test s = lustre_test := Some s 73 let get_lustre_test () = !lustre_test 74 75 let lustre_test_cases = ref 100 76 let set_lustre_test_cases = (:=) lustre_test_cases 77 let get_lustre_test_cases () = !lustre_test_cases 78 79 let lustre_test_cycles = ref 100 80 let set_lustre_test_cycles = (:=) lustre_test_cycles 81 let get_lustre_test_cycles () = !lustre_test_cycles 82 83 let lustre_test_min_int = ref (-1000) 84 let set_lustre_test_min_int = (:=) lustre_test_min_int 85 let get_lustre_test_min_int () = !lustre_test_min_int 86 87 let lustre_test_max_int = ref 1000 88 let set_lustre_test_max_int = (:=) lustre_test_max_int 89 let get_lustre_test_max_int () = !lustre_test_max_int 90 58 91 59 92 (* … … 71 104 72 105 let basic_optimizations = 73 74 75 76 77 106 [ 107 LoopPeeling.trans; 108 ConstPropagation.trans; 109 CopyPropagation.trans; 110 RedundancyElimination.trans; 78 111 CopyPropagation.trans; 79 112 RedundancyElimination.trans 80 113 ] 81 114 82 115 83 116 let options = OptionsParsing.register [ 117 (* 84 118 "-s", Arg.String set_source_language, 85 119 " Choose the source language between:"; 86 120 extra_doc " Clight, Cminor"; 87 121 extra_doc " [default is C]"; 122 *) 88 123 89 124 "-l", Arg.String set_target_language, … … 98 133 " Interpret the compiled code."; 99 134 100 "- t", Arg.Set trace_flag,101 " Interpret the compiled code and print all label traces.";135 "-is", Arg.Set interpretations_flag, 136 " Interpret all the compilation passes."; 102 137 103 138 "-d", Arg.Set debug_flag, … … 106 141 "-o", Arg.String set_output_files, 107 142 " Prefix of the output files."; 143 144 "-asm-pretty", Arg.Set asm_pretty_flag, 145 " Output a pretty-printed assembly file."; 146 147 "-lustre", Arg.Set lustre_flag, 148 " Input file is a Lustre file."; 149 150 "-remove-lustre-externals", Arg.Set remove_lustre_externals, 151 " Remove Lustre externals."; 152 153 "-lustre-test", Arg.String set_lustre_test, 154 " Input file is a Lustre file, testing requested."; 155 156 "-lustre-test-cases", Arg.Int set_lustre_test_cases, 157 " Set the number of test cases when testing a Lustre"; 158 extra_doc " file."; 159 extra_doc " [default is 100]"; 160 161 "-lustre-test-cycles", Arg.Int set_lustre_test_cycles, 162 " Set the number of cycles for each case when testing"; 163 extra_doc " a Lustre file."; 164 extra_doc " [default is 100]"; 165 166 "-lustre-test-min-int", Arg.Int set_lustre_test_min_int, 167 " Random int minimum value when testing a Lustre file."; 168 extra_doc " [default is -1000]"; 169 170 "-lustre-test-max-int", Arg.Int set_lustre_test_max_int, 171 " Random int maximum value when testing a Lustre file."; 172 extra_doc " [default is 1000]"; 108 173 109 174 "-peel", Arg.Unit (add_transformation LoopPeeling.trans), -
Deliverables/D2.2/8051-indexed-labels-branch/src/options.mli
r1507 r1539 9 9 val get_target_language : unit -> Languages.name 10 10 11 (** {2 Interpretation request s} *)11 (** {2 Interpretation request} *) 12 12 val request_interpretation : bool -> unit 13 13 val interpretation_requested : unit -> bool 14 14 15 (** {2 Tracerequests} *)16 val request_ trace: bool -> unit17 val trace_requested : unit -> bool15 (** {2 Interpretation requests} *) 16 val request_interpretations : bool -> unit 17 val interpretations_requested : unit -> bool 18 18 19 19 (** {2 Annotation requests} *) … … 35 35 val is_cost_ternary_enabled : unit -> bool 36 36 37 (** {2 Assembly pretty print} *) 38 val set_asm_pretty : bool -> unit 39 val is_asm_pretty : unit -> bool 40 41 (** {2 Lustre file} *) 42 val set_lustre_file : bool -> unit 43 val is_lustre_file : unit -> bool 44 45 (** {2 Remove Lustre externals} *) 46 val set_remove_lustre_externals : bool -> unit 47 val is_remove_lustre_externals : unit -> bool 48 49 (** {2 Lustre file and test requested} *) 50 val set_lustre_test : string -> unit 51 val get_lustre_test : unit -> string option 52 53 (** {2 Lustre file: number of test cases} *) 54 val set_lustre_test_cases : int -> unit 55 val get_lustre_test_cases : unit -> int 56 57 (** {2 Lustre file: number of cycles for each case} *) 58 val set_lustre_test_cycles : int -> unit 59 val get_lustre_test_cycles : unit -> int 60 61 (** {2 Lustre file: random int minimum value} *) 62 val set_lustre_test_min_int : int -> unit 63 val get_lustre_test_min_int : unit -> int 64 65 (** {2 Lustre file: random int maximum value} *) 66 val set_lustre_test_max_int : int -> unit 67 val get_lustre_test_max_int : unit -> int 68 69 37 70 (** {2 Intermediate transformations } *) 38 71 val get_transformations : unit -> Languages.transformation list -
Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/stringSig.mli
r818 r1539 9 9 val compare : t -> t -> int 10 10 11 module Set : Set.S with type elt = t 11 module Set : sig 12 include Set.S with type elt = t 13 val of_list : elt list -> t 14 val unionl : t list -> t 15 end 12 16 13 17 module Map : Map.S with type key = t … … 21 25 22 26 val make_unique : Set.t -> (string -> string) 27 val make_fresh : Set.t -> string -> (unit -> string) 23 28 24 29 end -
Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/stringTools.ml
r818 r1539 7 7 8 8 9 module Set = Set.Make (String) 9 module Set = struct 10 include Set.Make (String) 11 let of_list l = 12 let f res e = add e res in 13 List.fold_left f empty l 14 let unionl l = List.fold_left union empty l 15 end 10 16 11 17 … … 50 56 res in 51 57 unique 58 59 let make_fresh set prefix = 60 let fresh_prefix = Gen.fresh_prefix set prefix in 61 let universe = Gen.new_universe fresh_prefix in 62 (fun () -> Gen.fresh universe)
Note: See TracChangeset
for help on using the changeset viewer.