Changeset 1542 for Deliverables/D2.2
- Timestamp:
- Nov 23, 2011, 5:43:24 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051/src
- Files:
-
- 56 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/ASM/ASM.mli
r1462 r1542 102 102 type labelled_instruction = 103 103 [ instruction 104 | `Cost of string 104 | `Cost of CostLabel.t 105 | `Index of int 106 | `Inc of int 105 107 | `Label of string 106 108 | `Jmp of string … … 122 124 type program = 123 125 { code : BitVectors.byte list ; 124 cost_labels : string BitVectors.WordMap.t ; 126 inds : int BitVectors.WordMap.t ; (* loop index resets *) 127 incs : int BitVectors.WordMap.t ; (* loop index increments *) 128 cost_labels : CostLabel.t BitVectors.WordMap.t ; 125 129 labels : BitVectors.word StringTools.Map.t ; 130 126 131 exit_addr : BitVectors.word ; 127 132 has_main : bool } -
Deliverables/D2.2/8051/src/ASM/ASMCosts.ml
r643 r1542 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/src/ASM/ASMInterpret.ml
r1490 r1542 131 131 132 132 exit_addr : BitVectors.word; 133 cost_labels : string BitVectors.WordMap.t 133 134 (* 135 ind_0s : int BitVectors.WordMap.t; 136 ind_incs : int BitVectors.WordMap.t; 137 cost_labels : CostLabel.t BitVectors.WordMap.t 138 *) 134 139 } 135 140 … … 284 289 285 290 exit_addr = BitVectors.zero `Sixteen; 291 (* 292 ind_0s = BitVectors.WordMap.empty; 293 ind_incs = BitVectors.WordMap.empty; 286 294 cost_labels = BitVectors.WordMap.empty 295 *) 287 296 } 288 297 … … 950 959 ) (StringTools.Map.empty,0) p.ASM.ppreamble 951 960 in 952 let pc,exit_addr,labels, costs =961 let pc,exit_addr,labels,inds,incs,costs = 953 962 List.fold_left 954 (fun (pc,exit_addr,labels, costs) i ->963 (fun (pc,exit_addr,labels,inds,incs,costs) i -> 955 964 match i with 956 `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, costs 957 | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, costs 958 | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs 959 | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, costs 965 `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, inds, incs, costs 966 | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, inds, incs, costs 967 | `Cost s -> pc, exit_addr, labels, inds, incs, BitVectors.WordMap.add pc s costs 968 | `Index i -> pc, exit_addr, labels, BitVectors.WordMap.add pc i inds, incs, costs 969 | `Inc i -> pc, exit_addr, labels, inds, BitVectors.WordMap.add pc i incs, costs 970 | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs 971 960 972 | `Jmp _ 961 | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, costs973 | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs 962 974 (*CSC: very stupid: always expand to worst opcode *) 963 975 | `WithLabel i -> … … 967 979 assert (fake_jump = i'); 968 980 let pc' = snd (half_add pc' (vect_of_int 5 `Sixteen)) in 969 (snd (half_add pc pc'), exit_addr, labels, costs)981 (snd (half_add pc pc'), exit_addr, labels, inds, incs, costs) 970 982 | #instruction as i -> 971 983 let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in 972 984 assert (i = i'); 973 (snd (half_add pc pc'),exit_addr,labels, costs)985 (snd (half_add pc pc'),exit_addr,labels, inds, incs, costs) 974 986 ) 975 987 (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen, 976 StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode 988 StringTools.Map.empty, BitVectors.WordMap.empty, BitVectors.WordMap.empty, 989 BitVectors.WordMap.empty) p.ASM.pcode 977 990 in 978 991 let code = … … 980 993 (function 981 994 `Label _ 982 | `Cost _ -> [] 995 | `Cost _ 996 | `Index _ 997 | `Inc _ -> [] 983 998 | `WithLabel i -> 984 999 (* We need to expand a conditional jump to a label to a machine language … … 1032 1047 address, reconstructed 1033 1048 in 1034 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 1035 1051 let translation = [ translated_jump; sjmp; jmp ] in 1036 1052 List.flatten (List.map assembly1 translation) … … 1048 1064 assembly1 (`LCALL (`ADDR16 pc_offset )) 1049 1065 | #instruction as i -> assembly1 i) p.ASM.pcode) in 1050 { ASM.code = code ; ASM.cost_labels = costs ; 1066 { ASM.code = code ; 1067 ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ; 1051 1068 ASM.labels = StringTools.Map.empty ; 1052 1069 ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main } … … 1975 1992 let load_program p = 1976 1993 let st = load p.ASM.code initialize in 1977 { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels } 1978 1979 let observe_trace trace_ref st = 1980 let cost_label = 1981 if BitVectors.WordMap.mem st.pc st.cost_labels then 1982 [BitVectors.WordMap.find st.pc st.cost_labels] 1983 else [] in 1984 trace_ref := cost_label @ !trace_ref ; 1994 { st with exit_addr = p.ASM.exit_addr (* ; cost_labels = p.ASM.cost_labels *)} 1995 1996 type cost_trace = { 1997 mutable ct_labels : CostLabel.t list; 1998 mutable ct_inds : CostLabel.const_indexing list; 1999 } 2000 2001 (* FIXME: supposing only one index reset or increment per instruction *) 2002 let update_indexes trace p st = 2003 try 2004 let i = BitVectors.WordMap.find st.pc p.ASM.inds in 2005 CostLabel.enter_loop trace.ct_inds i 2006 with Not_found -> (); 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 | _ -> () 2018 2019 let update_labels trace p st = 2020 try 2021 let cost_label = BitVectors.WordMap.find st.pc p.cost_labels in 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 2025 with Not_found -> () 2026 2027 2028 2029 let update_trace trace p st = 2030 update_labels trace p st; 2031 update_indexes trace p st; 1985 2032 if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st 1986 2033 … … 2000 2047 if p.ASM.has_main then 2001 2048 let st = load_program p in 2002 let trace = ref []in2003 let callback = observe_trace tracein2049 let trace = {ct_labels = []; ct_inds = []} in 2050 let callback = update_trace trace p in 2004 2051 let st = execute callback st in 2005 2052 let res = result st in 2006 2053 if debug then 2007 2054 Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ; 2008 (res, List.rev !trace)2055 (res, List.rev trace.ct_labels) 2009 2056 else (IntValue.Int32.zero, []) 2010 2057 -
Deliverables/D2.2/8051/src/ASM/ASMInterpret.mli
r1488 r1542 98 98 99 99 exit_addr : BitVectors.word; 100 cost_labels : string BitVectors.WordMap.t 100 (* 101 ind_0s : int BitVectors.WordMap.t; 102 ind_incs : int BitVectors.WordMap.t; 103 cost_labels : CostLabel.t BitVectors.WordMap.t 104 *) 101 105 } 102 106 -
Deliverables/D2.2/8051/src/ASM/Pretty.ml
r818 r1542 43 43 function 44 44 `Label l -> l ^ ":" 45 | `Cost l -> l ^ ":" 45 | `Cost l -> CostLabel.string_of_cost_label ~pretty:true l ^ ":" 46 | `Index i -> "index " ^ string_of_int i ^ ":" 47 | `Inc i -> "increment " ^ string_of_int i ^ ":" 46 48 | `Jmp j -> "ljmp " ^ j 47 49 | `Call j -> "lcall " ^ j … … 96 98 | `XRL(`U2(a1,a2)) -> "xrl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 97 99 100 let find_comment p pc = 101 let s1 = 102 try 103 let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in 104 ", " ^ CostLabel.string_of_cost_label ~pretty:true lbl 105 with Not_found -> "" in 106 let s2 = 107 try 108 let i = BitVectors.WordMap.find pc p.ASM.inds in 109 ", index " ^ string_of_int i 110 with Not_found -> "" in 111 let s3 = 112 try 113 let i = BitVectors.WordMap.find pc p.ASM.incs in 114 ", inc " ^ string_of_int i 115 with Not_found -> "" in 116 s1 ^ s2 ^ s3 117 118 98 119 let print_program p = 99 120 let mem = ASMInterpret.load_code_memory p.ASM.code in 100 121 let f (s, pc) _ = 101 122 let (inst, new_pc, cost) = ASMInterpret.fetch mem pc in 102 (Printf.sprintf "%s% 6X: %- 18s ;; %d 123 (Printf.sprintf "%s% 6X: %- 18s ;; %d%s\n" 103 124 s 104 125 (BitVectors.int_of_vect pc) 105 126 (pp_instruction inst) 106 127 cost 107 (if BitVectors.WordMap.mem pc p.ASM.cost_labels then 108 (BitVectors.WordMap.find pc p.ASM.cost_labels) 109 else ""), 128 (find_comment p pc), 110 129 new_pc) in 111 130 fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code) -
Deliverables/D2.2/8051/src/ERTL/ERTL.mli
r1462 r1542 48 48 (* Emit a cost label. *) 49 49 | St_cost of CostLabel.t * Label.t 50 51 (* Reset to 0 a loop index *) 52 | St_ind_0 of CostLabel.index * Label.t 53 54 (* Increment a loop index *) 55 | St_ind_inc of CostLabel.index * Label.t 50 56 51 57 (* Assign the content of a hardware register to a pseudo register. Parameters -
Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml
r1462 r1542 32 32 33 33 type stack_frame = local_env 34 35 type indexing = CostLabel.const_indexing 34 36 35 37 (* Execution states. *) … … 44 46 renv : hdw_reg_env ; 45 47 mem : memory ; 48 inds : indexing list; 46 49 trace : CostLabel.t list } 47 50 … … 62 65 let change_trace st trace = { st with trace = trace } 63 66 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) 67 let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds) 68 let new_ind st = { st with inds = CostLabel.new_const_ind st.inds } 69 let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds } 70 let enter_loop st = CostLabel.enter_loop st.inds 71 let continue_loop st = CostLabel.continue_loop st.inds 64 72 65 73 let empty_state = … … 72 80 renv = I8051.RegisterMap.empty ; 73 81 mem = Mem.empty ; 82 inds = [] ; 74 83 trace = [] } 75 84 … … 118 127 let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in 119 128 let pc = entry_pc lbls_offs ptr def in 129 let st = new_ind st in 120 130 change_lenv (change_pc st pc) lenv 121 131 … … 231 241 232 242 let interpret_return lbls_offs st = 243 let st = forget_ind st in 233 244 let st = pop_st_frs st in 234 245 let (st, pch) = pop st in … … 254 265 255 266 | ERTL.St_cost (cost_lbl, lbl) -> 267 let cost_lbl = ev_label st cost_lbl in 256 268 let st = add_trace st cost_lbl in 269 next_pc st lbl 270 271 | ERTL.St_ind_0 (i, lbl) -> 272 enter_loop st i; 273 next_pc st lbl 274 275 | ERTL.St_ind_inc (i, lbl) -> 276 continue_loop st i; 257 277 next_pc st lbl 258 278 -
Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml
r1462 r1542 43 43 Printf.sprintf "*** %s *** --> %s" s lbl 44 44 | ERTL.St_cost (cost_lbl, lbl) -> 45 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 45 46 Printf.sprintf "emit %s --> %s" cost_lbl lbl 47 | ERTL.St_ind_0 (i, lbl) -> 48 Printf.sprintf "index %d --> %s" i lbl 49 | ERTL.St_ind_inc (i, lbl) -> 50 Printf.sprintf "increment %d --> %s" i lbl 46 51 | ERTL.St_get_hdw (r1, r2, lbl) -> 47 52 Printf.sprintf "move %s, %s --> %s" -
Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
r1488 r1542 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 167 | ERTL.St_ind_0 (i, l) -> 168 LTL.St_ind_0 (i, l) 169 170 | ERTL.St_ind_inc (i, l) -> 171 LTL.St_ind_inc (i, l) 166 172 167 173 | ERTL.St_get_hdw (destr, sourcehwr, l) -> -
Deliverables/D2.2/8051/src/ERTL/liveness.ml
r1462 r1542 18 18 | St_comment (_, l) 19 19 | St_cost (_, l) 20 | St_ind_0 (_, l) 21 | St_ind_inc (_, l) 20 22 | St_set_hdw (_, _, l) 21 23 | St_get_hdw (_, _, l) … … 83 85 end 84 86 85 module Label_ImperativeMap = struct 86 87 type key = 88 Label.Map.key 89 90 type 'data t = 91 'data Label.Map.t ref 92 93 let create () = 94 ref Label.Map.empty 95 96 let clear t = 97 t := Label.Map.empty 98 99 let add k d t = 100 t := Label.Map.add k d !t 101 102 let find k t = 103 Label.Map.find k !t 104 105 let iter f t = 106 Label.Map.iter f !t 107 108 end 109 110 module F = Fix.Make (Label_ImperativeMap) (L) 87 module F = Fix.Make (Label.ImpMap) (L) 111 88 112 89 (* These are the sets of variables defined at (written by) a statement. *) … … 117 94 | St_comment _ 118 95 | St_cost _ 96 | St_ind_0 _ 97 | St_ind_inc _ 119 98 | St_push _ 120 99 | St_store _ … … 169 148 | St_comment _ 170 149 | St_cost _ 150 | St_ind_0 _ 151 | St_ind_inc _ 171 152 | St_framesize _ 172 153 | St_pop _ … … 227 208 | St_comment _ 228 209 | St_cost _ 210 | St_ind_0 _ 211 | St_ind_inc _ 229 212 | St_newframe _ 230 213 | St_delframe _ -
Deliverables/D2.2/8051/src/ERTL/uses.ml
r1462 r1542 20 20 | St_comment _ 21 21 | St_cost _ 22 | St_ind_0 _ 23 | St_ind_inc _ 22 24 | St_hdw_to_hdw _ 23 25 | St_newframe _ -
Deliverables/D2.2/8051/src/LIN/LIN.mli
r1488 r1542 18 18 (* Emit a cost label. *) 19 19 | St_cost of CostLabel.t 20 21 (* Reset to 0 a loop index *) 22 | St_ind_0 of CostLabel.index 23 24 (* Increment a loop index *) 25 | St_ind_inc of CostLabel.index 20 26 21 27 (* Assign an integer constant to a register. Parameters are the destination -
Deliverables/D2.2/8051/src/LIN/LINInterpret.ml
r1488 r1542 21 21 22 22 type hdw_reg_env = Val.t I8051.RegisterMap.t 23 24 25 type indexing = CostLabel.const_indexing 23 26 24 27 (* Execution states. *) … … 31 34 renv : hdw_reg_env ; 32 35 mem : memory ; 36 inds : indexing list ; 33 37 trace : CostLabel.t list } 34 38 … … 44 48 let change_trace st trace = { st with trace = trace } 45 49 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) 50 let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds) 51 let new_ind st = { st with inds = CostLabel.new_const_ind st.inds } 52 let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds } 53 let enter_loop st = CostLabel.enter_loop st.inds 54 let continue_loop st = CostLabel.continue_loop st.inds 46 55 47 56 let empty_state = … … 52 61 renv = I8051.RegisterMap.empty ; 53 62 mem = Mem.empty ; 63 inds = [] ; 54 64 trace = [] } 55 65 … … 72 82 73 83 let init_fun_call st ptr = 84 let st = new_ind st in 74 85 change_pc st (Val.change_address_offset ptr Val.Offset.zero) 75 86 … … 176 187 177 188 let interpret_return st = 189 let st = forget_ind st in 178 190 let (st, pc) = return_pc st in 179 191 change_pc st pc … … 195 207 196 208 | LIN.St_cost cost_lbl -> 209 let cost_lbl = ev_label st cost_lbl in 197 210 let st = add_trace st cost_lbl in 211 next_pc st 212 213 | LIN.St_ind_0 i -> 214 enter_loop st i; 215 next_pc st 216 217 | LIN.St_ind_inc i -> 218 continue_loop st i; 198 219 next_pc st 199 220 -
Deliverables/D2.2/8051/src/LIN/LINPrinter.ml
r1488 r1542 26 26 Printf.sprintf "*** %s ***" s 27 27 | LIN.St_cost cost_lbl -> 28 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 28 29 Printf.sprintf "emit %s" cost_lbl 30 | LIN.St_ind_0 i -> 31 Printf.sprintf "index %d" i 32 | LIN.St_ind_inc i -> 33 Printf.sprintf "increment %d" i 29 34 | LIN.St_int (dstr, i) -> 30 35 Printf.sprintf "imm %s, %d" (print_reg dstr) i -
Deliverables/D2.2/8051/src/LIN/LINToASM.ml
r1525 r1542 25 25 | LIN.St_goto lbl 26 26 | LIN.St_label lbl 27 | LIN.St_cost lbl28 27 | LIN.St_condacc lbl -> Label.Set.singleton lbl 28 (* taking the atom as a fresh prefix will be generated *) 29 | LIN.St_cost lbl -> Label.Set.singleton (lbl.CostLabel.name) 29 30 | _ -> Label.Set.empty 30 31 … … 69 70 (* TODO: hack! Need to make the difference between cost labels and regular 70 71 labels. *) 71 [`Cost lbl ; `NOP] 72 [`Cost lbl ; `NOP ] 73 | LIN.St_ind_0 i -> [`Index i ; `NOP (* TODO: hack! *)] 74 | LIN.St_ind_inc i -> [`Inc i ; `NOP (* TODO: hack! *)] 72 75 | LIN.St_int (r, i) -> 73 76 [`MOV (`U3 (I8051.reg_addr r, data_of_int i))] -
Deliverables/D2.2/8051/src/LTL/LTL.mli
r1488 r1542 18 18 (* Emit a cost label. *) 19 19 | St_cost of CostLabel.t * Label.t 20 21 (* Reset to 0 a loop index *) 22 | St_ind_0 of CostLabel.index * Label.t 23 24 (* Increment a loop index *) 25 | St_ind_inc of CostLabel.index * Label.t 20 26 21 27 (* Assign an integer constant to a register. Parameters are the destination -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r1488 r1542 31 31 renv : hdw_reg_env ; 32 32 mem : memory ; 33 inds : CostLabel.const_indexing list ; 33 34 trace : CostLabel.t list } 34 35 … … 44 45 let change_trace st trace = { st with trace = trace } 45 46 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) 47 let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds) 48 let new_ind st = { st with inds = CostLabel.new_const_ind st.inds } 49 let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds } 50 let enter_loop st = CostLabel.enter_loop st.inds 51 let continue_loop st = CostLabel.continue_loop st.inds 46 52 47 53 let empty_state = … … 52 58 renv = I8051.RegisterMap.empty ; 53 59 mem = Mem.empty ; 60 inds = [] ; 54 61 trace = [] } 55 62 … … 95 102 let init_fun_call lbls_offs st ptr def = 96 103 let pc = entry_pc lbls_offs ptr def in 104 let st = new_ind st in 97 105 change_pc st pc 98 106 … … 207 215 208 216 let interpret_return lbls_offs st = 217 let st = forget_ind st in 209 218 let (st, pc) = return_pc st in 210 219 change_pc st pc … … 227 236 228 237 | LTL.St_cost (cost_lbl, lbl) -> 238 let cost_lbl = ev_label st cost_lbl in 229 239 let st = add_trace st cost_lbl in 240 next_pc st lbl 241 242 | LTL.St_ind_0 (i, lbl) -> 243 enter_loop st i; 244 next_pc st lbl 245 246 | LTL.St_ind_inc (i, lbl) -> 247 continue_loop st i; 230 248 next_pc st lbl 231 249 -
Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml
r1488 r1542 25 25 Printf.sprintf "*** %s *** --> %s" s lbl 26 26 | LTL.St_cost (cost_lbl, lbl) -> 27 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 27 28 Printf.sprintf "emit %s --> %s" cost_lbl lbl 29 | LTL.St_ind_0 (i, lbl) -> 30 Printf.sprintf "index %d --> %s" i lbl 31 | LTL.St_ind_inc (i, lbl) -> 32 Printf.sprintf "increment %d --> %s" i lbl 28 33 | LTL.St_int (dstr, i, lbl) -> 29 34 Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl -
Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml
r1488 r1542 22 22 | LTL.St_cost (lbl, _) -> 23 23 LIN.St_cost lbl 24 | LTL.St_ind_0 (i, _) -> 25 LIN.St_ind_0 i 26 | LTL.St_ind_inc (i, _) -> 27 LIN.St_ind_inc i 24 28 | LTL.St_int (r, i, _) -> 25 29 LIN.St_int (r, i) -
Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml
r1488 r1542 117 117 | LTL.St_comment (_, l) 118 118 | LTL.St_cost (_, l) 119 | LTL.St_ind_0 (_, l) 120 | LTL.St_ind_inc (_, l) 119 121 | LTL.St_int (_, _, l) 120 122 | LTL.St_pop l -
Deliverables/D2.2/8051/src/LTL/branch.ml
r1488 r1542 52 52 | LTL.St_cost (lbl, l) -> 53 53 LTL.St_cost (lbl, rep l) 54 | LTL.St_ind_0 (i, l) -> 55 LTL.St_ind_0 (i, rep l) 56 | LTL.St_ind_inc (i, l) -> 57 LTL.St_ind_inc (i, rep l) 54 58 | LTL.St_int (r, i, l) -> 55 59 LTL.St_int (r, i, rep l) -
Deliverables/D2.2/8051/src/RTL/RTL.mli
r818 r1542 16 16 (* Emit a cost label. *) 17 17 | St_cost of CostLabel.t * Label.t 18 19 (* Reset to 0 a loop index *) 20 | St_ind_0 of CostLabel.index * Label.t 21 22 (* Increment a loop index *) 23 | St_ind_inc of CostLabel.index * Label.t 18 24 19 25 (* Assign the address of a symbol to registers. Parameters are the destination -
Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
r818 r1542 34 34 carry : Val.t } 35 35 36 type indexing = CostLabel.const_indexing 37 36 38 (* Execution states. There are three possible states : 37 39 - The constructor [State] represents a state when executing a function … … 41 43 type state = 42 44 | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) * 43 local_env * Val.t (* carry *) * memory * CostLabel.t list 45 local_env * Val.t (* carry *) * memory * indexing list * 46 CostLabel.t list 44 47 | CallState of stack_frame list * RTL.function_def * 45 Val.t list (* args *) * memory* CostLabel.t list48 Val.t list (* args *) * memory * indexing list * CostLabel.t list 46 49 | ReturnState of stack_frame list * Val.t list (* return values *) * 47 memory * CostLabel.t list50 memory * indexing list * CostLabel.t list 48 51 49 52 let string_of_local_env lenv = … … 59 62 60 63 let print_state = function 61 | State (_, _, lbl, sp, lenv, carry, mem, _) ->62 Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\n Regular state: %s\n\n%!"64 | State (_, _, lbl, sp, lenv, carry, mem, ind, _) -> 65 Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:" 63 66 (Val.string_of_address sp) 64 67 (Val.to_string carry) 65 68 (string_of_local_env lenv) 66 (Mem.to_string mem) 69 (Mem.to_string mem); 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%!" 67 73 lbl 68 | CallState (_, _, args, mem, _ ) ->74 | CallState (_, _, args, mem, _, _) -> 69 75 Printf.printf "Memory:%s\nCall state: %s\n\n%!" 70 76 (Mem.to_string mem) 71 77 (string_of_args args) 72 | ReturnState (_, vs, mem, _ ) ->78 | ReturnState (_, vs, mem, _, _) -> 73 79 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 74 80 (Mem.to_string mem) … … 96 102 (* Assign a value to some destinations registers. *) 97 103 98 let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =104 let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs = 99 105 let lenv = adds destrs vs lenv in 100 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)106 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 101 107 102 108 (* Branch on a value. *) 103 109 104 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =110 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v = 105 111 let next_lbl = 106 112 if Val.is_true v then lbl_true … … 108 114 if Val.is_false v then lbl_false 109 115 else error "Undefined conditional value." in 110 State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace) 116 State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace) 117 118 let curr_ind = CostLabel.curr_const_ind 119 120 let forget_ind = CostLabel.forget_const_ind 121 122 let new_ind = CostLabel.new_const_ind 111 123 112 124 … … 120 132 (carry : Val.t) 121 133 (mem : memory) 134 (inds : indexing list) 122 135 (stmt : RTL.statement) 123 136 (trace : CostLabel.t list) : … … 125 138 126 139 | RTL.St_skip lbl -> 127 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)140 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 128 141 129 142 | RTL.St_cost (cost_lbl, lbl) -> 130 State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace) 143 let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in 144 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace) 145 146 | RTL.St_ind_0 (i, lbl) -> 147 CostLabel.enter_loop inds i; 148 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 149 150 | RTL.St_ind_inc (i, lbl) -> 151 CostLabel.continue_loop inds i; 152 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 131 153 132 154 | RTL.St_addr (r1, r2, x, lbl) -> 133 assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]155 assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] 134 156 (Mem.find_global mem x) 135 157 136 158 | RTL.St_stackaddr (r1, r2, lbl) -> 137 assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp159 assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp 138 160 139 161 | RTL.St_int (r, i, lbl) -> 140 assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]162 assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i] 141 163 142 164 | RTL.St_move (destr, srcr, lbl) -> 143 assign_state sfrs graph lbl sp lenv carry mem trace [destr]165 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] 144 166 [get_local_value lenv srcr] 145 167 … … 149 171 (get_local_value lenv srcr1) 150 172 (get_local_value lenv srcr2) in 151 assign_state sfrs graph lbl sp lenv carry mem trace173 assign_state sfrs graph lbl sp lenv carry mem inds trace 152 174 [destr1 ; destr2] [v1 ; v2] 153 175 154 176 | RTL.St_op1 (op1, destr, srcr, lbl) -> 155 177 let v = Eval.op1 op1 (get_local_value lenv srcr) in 156 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]178 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v] 157 179 158 180 | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) -> … … 161 183 (get_local_value lenv srcr1) 162 184 (get_local_value lenv srcr2) in 163 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]185 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v] 164 186 165 187 | RTL.St_clear_carry lbl -> 166 State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)188 State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace) 167 189 168 190 | RTL.St_set_carry lbl -> 169 State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)191 State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace) 170 192 171 193 | RTL.St_load (destr, addr1, addr2, lbl) -> 172 194 let addr = get_local_addr lenv addr1 addr2 in 173 195 let v = Mem.load mem chunk addr in 174 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]196 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v] 175 197 176 198 | RTL.St_store (addr1, addr2, srcr, lbl) -> 177 199 let addr = get_local_addr lenv addr1 addr2 in 178 200 let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in 179 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)201 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 180 202 181 203 | RTL.St_call_id (f, args, ret_regs, lbl) -> … … 186 208 sp = sp ; lenv = lenv ; carry = carry } 187 209 in 188 CallState (sf :: sfrs, f_def, args, mem, trace)210 CallState (sf :: sfrs, f_def, args, mem, inds, trace) 189 211 190 212 | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) -> … … 194 216 let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ; 195 217 sp = sp ; lenv = lenv ; carry = carry } in 196 CallState (sf :: sfrs, f_def, args, mem, trace)218 CallState (sf :: sfrs, f_def, args, mem, inds, trace) 197 219 198 220 | RTL.St_tailcall_id (f, args) -> … … 200 222 let args = get_arg_values lenv args in 201 223 let mem = Mem.free mem sp in 202 CallState (sfrs, f_def, args, mem, trace)224 CallState (sfrs, f_def, args, mem, inds, trace) 203 225 204 226 | RTL.St_tailcall_ptr (f1, f2, args) -> … … 207 229 let args = get_arg_values lenv args in 208 230 let mem = Mem.free mem sp in 209 CallState (sfrs, f_def, args, mem, trace)231 CallState (sfrs, f_def, args, mem, inds, trace) 210 232 211 233 | RTL.St_cond (srcr, lbl_true, lbl_false) -> 212 234 let v = get_local_value lenv srcr in 213 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v235 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v 214 236 215 237 | RTL.St_return rl -> 216 238 let vl = List.map (get_local_value lenv) rl in 217 239 let mem = Mem.free mem sp in 218 ReturnState (sfrs, vl, mem, trace)240 ReturnState (sfrs, vl, mem, inds, trace) 219 241 220 242 … … 240 262 (args : Val.t list) 241 263 (mem : memory) 264 (inds : indexing list) 242 265 (trace : CostLabel.t list) : 243 266 state = 244 267 match f_def with 245 268 | RTL.F_int def -> 269 let inds = new_ind inds in 246 270 let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in 247 271 State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp, 248 272 init_locals def.RTL.f_locals def.RTL.f_params args, 249 Val.undef, mem', trace)273 Val.undef, mem', inds, trace) 250 274 | RTL.F_ext def -> 251 275 let (mem', vs) = interpret_external mem def.AST.ef_tag args in 252 ReturnState (sfrs, vs, mem', trace)276 ReturnState (sfrs, vs, mem', inds, trace) 253 277 254 278 let state_after_return … … 257 281 (ret_vals : Val.t list) 258 282 (mem : memory) 283 (inds : indexing list) 259 284 (trace : CostLabel.t list) : 260 285 state = 261 286 let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in 262 287 let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in 263 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace) 288 let inds = forget_ind inds in 289 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace) 264 290 265 291 266 292 let small_step (st : state) : state = match st with 267 | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->293 | State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) -> 268 294 let stmt = Label.Map.find pc graph in 269 interpret_statement sfrs graph sp lenv carry mem stmt trace270 | CallState (sfrs, f_def, args, mem, trace) ->271 state_after_call sfrs f_def args mem trace272 | ReturnState ([], ret_vals, mem, trace) ->295 interpret_statement sfrs graph sp lenv carry mem inds stmt trace 296 | CallState (sfrs, f_def, args, mem, inds, trace) -> 297 state_after_call sfrs f_def args mem inds trace 298 | ReturnState ([], ret_vals, mem, inds, trace) -> 273 299 assert false (* End of execution; handled in iter_small_step. *) 274 | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->275 state_after_return sf sfrs ret_vals mem trace300 | ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) -> 301 state_after_return sf sfrs ret_vals mem inds trace 276 302 277 303 … … 292 318 if debug then print_state st ; 293 319 match small_step st with 294 | ReturnState ([], vs, mem, trace) ->320 | ReturnState ([], vs, mem, _, trace) -> 295 321 print_and_return_result (compute_result vs, List.rev trace) 296 322 | st' -> iter_small_step debug st' … … 321 347 let mem = init_mem p in 322 348 let main_def = find_function mem main in 323 let st = CallState ([], main_def, [], mem, [] ) in349 let st = CallState ([], main_def, [], mem, [], []) in 324 350 iter_small_step debug st -
Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml
r818 r1542 43 43 | RTL.St_skip lbl -> "--> " ^ lbl 44 44 | RTL.St_cost (cost_lbl, lbl) -> 45 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 45 46 Printf.sprintf "emit %s --> %s" cost_lbl lbl 47 | RTL.St_ind_0 (i, lbl) -> 48 Printf.sprintf "index %d --> %s" i lbl 49 | RTL.St_ind_inc (i, lbl) -> 50 Printf.sprintf "increment %d --> %s" i lbl 46 51 | RTL.St_addr (dstr1, dstr2, id, lbl) -> 47 52 Printf.sprintf "imm (%s, %s), %s --> %s" -
Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml
r1462 r1542 22 22 | ERTL.St_comment (s, _) -> ERTL.St_comment (s, lbl) 23 23 | ERTL.St_cost (cost_lbl, _) -> ERTL.St_cost (cost_lbl, lbl) 24 | ERTL.St_ind_0 (i, _) -> ERTL.St_ind_0 (i, lbl) 25 | ERTL.St_ind_inc (i, _) -> ERTL.St_ind_inc (i, lbl) 24 26 | ERTL.St_get_hdw (r1, r2, _) -> ERTL.St_get_hdw (r1, r2, lbl) 25 27 | ERTL.St_set_hdw (r1, r2, _) -> ERTL.St_set_hdw (r1, r2, lbl) … … 319 321 add_graph lbl (ERTL.St_cost (cost_lbl, lbl')) def 320 322 323 | RTL.St_ind_0 (i, lbl') -> 324 add_graph lbl (ERTL.St_ind_0 (i, lbl')) def 325 326 | RTL.St_ind_inc (i, lbl') -> 327 add_graph lbl (ERTL.St_ind_inc (i, lbl')) def 328 321 329 | RTL.St_addr (r1, r2, x, lbl') -> 322 330 adds_graph … … 432 440 let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in 433 441 (Some cost_label, { def with ERTL.f_graph = graph }) 442 | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl) 434 443 | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl) 435 444 | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl) -
Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli
r818 r1542 11 11 12 12 13 type argument = 14 | Reg of Register.t 15 | Imm of AST.cst*AST.sig_type 16 13 17 (* A function in RTLabs is a mapping from labels to 14 18 statements. Statements explicitely mention their successors. *) … … 22 26 | St_cost of CostLabel.t * Label.t 23 27 28 (* Reset to 0 a loop index *) 29 | St_ind_0 of CostLabel.index * Label.t 30 31 (* Increment a loop index *) 32 | St_ind_inc of CostLabel.index * Label.t 33 24 34 (* Assign a constant to registers. Parameters are the destination register, 25 35 the constant and the label of the next statement. *) … … 32 42 33 43 (* Application of a binary operation. Parameters are the operation, the 34 destination register, the two argument registers and the label of the next44 destination register, the two arguments and the label of the next 35 45 statement. *) 36 | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t46 | St_op2 of AST.op2 * Register.t * argument * argument * Label.t 37 47 38 48 (* Memory load. Parameters are the size in bytes of what to load, the 39 49 register containing the address, the destination register and the label 40 50 of the next statement. *) 41 | St_load of AST.quantity * Register.t * Register.t * Label.t51 | St_load of AST.quantity * argument * Register.t * Label.t 42 52 43 53 (* Memory store. Parameters are the size in bytes of what to store, the 44 54 register containing the address, the source register and the label of the 45 55 next statement. *) 46 | St_store of AST.quantity * Register.t * Register.t * Label.t56 | St_store of AST.quantity * argument * argument * Label.t 47 57 48 58 (* Call to a function given its name. Parameters are the name of the -
Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml
r818 r1542 33 33 lenv : local_env } 34 34 35 type indexing = CostLabel.const_indexing 36 35 37 (* Execution states. There are three possible states : 36 38 - The constructor [State] represents a state when executing a function … … 40 42 type state = 41 43 | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) * 42 Label.t * local_env * memory* CostLabel.t list44 Label.t * local_env * memory * indexing list * CostLabel.t list 43 45 | CallState of stack_frame list * RTLabs.function_def * 44 Val.t list (* args *) * memory* CostLabel.t list46 Val.t list (* args *) * memory * indexing list * CostLabel.t list 45 47 | ReturnState of stack_frame list * Val.t (* return value *) * 46 memory* CostLabel.t list48 memory * indexing list * CostLabel.t list 47 49 48 50 let string_of_local_env lenv = … … 57 59 List.fold_left f "" args 58 60 59 let print_state = function60 | State (_, _, sp, lbl, lenv, mem, _) ->61 Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\n Regular state: %s\n\n%!"61 let print_state state = match state with 62 | State (_, _, sp, lbl, lenv, mem, inds, _) -> 63 Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:" 62 64 (Val.string_of_address sp) 63 65 (string_of_local_env lenv) 64 (Mem.to_string mem) 66 (Mem.to_string mem); 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%!" 65 70 lbl 66 | CallState (_, _, args, mem, _ ) ->71 | CallState (_, _, args, mem, _, _) -> 67 72 Printf.printf "Memory:%s\nCall state: %s\n\n%!" 68 73 (Mem.to_string mem) 69 74 (string_of_args args) 70 | ReturnState (_, v, mem, _ ) ->75 | ReturnState (_, v, mem, _, _) -> 71 76 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 72 77 (Mem.to_string mem) … … 106 111 (* Assign a value to some destinations registers. *) 107 112 108 let assign_state sfrs graph sp lbl lenv mem trace destr v =113 let assign_state sfrs graph sp lbl lenv mem inds trace destr v = 109 114 let lenv = update_local destr v lenv in 110 State (sfrs, graph, sp, lbl, lenv, mem, trace)115 State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) 111 116 112 117 (* Branch on a value. *) 113 118 114 let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =119 let branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v = 115 120 let next_lbl = 116 121 if Val.is_true v then lbl_true … … 118 123 if Val.is_false v then lbl_false 119 124 else error "Undefined conditional value." in 120 State (sfrs, graph, sp, next_lbl, lenv, mem, trace) 121 125 State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace) 126 127 let curr_ind = CostLabel.curr_const_ind 128 129 let forget_ind = CostLabel.forget_const_ind 130 131 let new_ind = CostLabel.new_const_ind 132 133 let eval_arg lenv mem sp = function 134 | RTLabs.Reg r -> get_value lenv r 135 | RTLabs.Imm (c, t) -> Eval.cst mem sp t c 136 137 let get_type_arg lenv = function 138 | RTLabs.Reg r -> get_type lenv r 139 | RTLabs.Imm (_, typ) -> typ 122 140 123 141 (* Interpret statements. *) … … 130 148 (mem : memory) 131 149 (stmt : RTLabs.statement) 150 (inds : indexing list) 132 151 (trace : CostLabel.t list) : 133 152 state = match stmt with 134 153 135 154 | RTLabs.St_skip lbl -> 136 State (sfrs, graph, sp, lbl, lenv, mem, trace)155 State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) 137 156 138 157 | RTLabs.St_cost (cost_lbl, lbl) -> 139 State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace) 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) -> 164 CostLabel.enter_loop inds i; 165 State (sfrs, graph, sp, lbl, lenv, 166 mem, inds, trace) 167 168 | RTLabs.St_ind_inc (i, lbl) -> 169 CostLabel.continue_loop inds i; 170 State (sfrs, graph, sp, lbl, lenv, 171 mem, inds, trace) 140 172 141 173 | RTLabs.St_cst (destr, cst, lbl) -> 142 174 let v = Eval.cst mem sp (get_type lenv destr) cst in 143 assign_state sfrs graph sp lbl lenv mem trace destr v175 assign_state sfrs graph sp lbl lenv mem inds trace destr v 144 176 145 177 | RTLabs.St_op1 (op1, destr, srcr, lbl) -> … … 147 179 Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1 148 180 (get_value lenv srcr) in 149 assign_state sfrs graph sp lbl lenv mem trace destr v181 assign_state sfrs graph sp lbl lenv mem inds trace destr v 150 182 151 183 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) -> 152 184 let v = 153 185 Eval.op2 154 (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2) 186 (get_type lenv destr) 187 (get_type_arg lenv srcr1) 188 (get_type_arg lenv srcr2) 155 189 op2 156 ( get_value lenvsrcr1)157 ( get_value lenvsrcr2) in158 assign_state sfrs graph sp lbl lenv mem trace destr v190 (eval_arg lenv mem sp srcr1) 191 (eval_arg lenv mem sp srcr2) in 192 assign_state sfrs graph sp lbl lenv mem inds trace destr v 159 193 160 194 | RTLabs.St_load (q, addr, destr, lbl) -> 161 let addr = address_of_value ( get_value lenvaddr) in195 let addr = address_of_value (eval_arg lenv mem sp addr) in 162 196 let v = Mem.loadq mem q addr in 163 assign_state sfrs graph sp lbl lenv mem trace destr v197 assign_state sfrs graph sp lbl lenv mem inds trace destr v 164 198 165 199 | RTLabs.St_store (q, addr, srcr, lbl) -> 166 let addr = address_of_value (get_value lenvaddr) in167 let v = get_value lenvsrcr in200 let addr = address_of_value (eval_arg lenv mem sp addr) in 201 let v = eval_arg lenv mem sp srcr in 168 202 let mem = Mem.storeq mem q addr v in 169 State (sfrs, graph, sp, lbl, lenv, mem, trace)203 State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) 170 204 171 205 | RTLabs.St_call_id (f, args, destr, sg, lbl) -> … … 176 210 { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 177 211 in 178 CallState (sf :: sfrs, f_def, args, mem, trace)212 CallState (sf :: sfrs, f_def, args, mem, inds, trace) 179 213 180 214 | RTLabs.St_call_ptr (r, args, destr, sg, lbl) -> … … 186 220 { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 187 221 in 188 CallState (sf :: sfrs, f_def, args, mem, trace)222 CallState (sf :: sfrs, f_def, args, mem, inds, trace) 189 223 190 224 | RTLabs.St_tailcall_id (f, args, sg) -> … … 193 227 (* No need to save the stack frame. But free the stack. *) 194 228 let mem = Mem.free mem sp in 195 CallState (sfrs, f_def, args, mem, trace)229 CallState (sfrs, f_def, args, mem, inds, trace) 196 230 197 231 | RTLabs.St_tailcall_ptr (r, args, sg) -> … … 201 235 (* No need to save the stack frame. But free the stack. *) 202 236 let mem = Mem.free mem sp in 203 CallState (sfrs, f_def, args, mem, trace)237 CallState (sfrs, f_def, args, mem, inds, trace) 204 238 205 239 | RTLabs.St_cond (srcr, lbl_true, lbl_false) -> 206 240 let v = get_value lenv srcr in 207 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v241 branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v 208 242 209 243 (* … … 242 276 | RTLabs.St_return None -> 243 277 let mem = Mem.free mem sp in 244 ReturnState (sfrs, Val.undef, mem, trace)278 ReturnState (sfrs, Val.undef, mem, inds, trace) 245 279 246 280 | RTLabs.St_return (Some r) -> 247 281 let v = get_value lenv r in 248 282 let mem = Mem.free mem sp in 249 ReturnState (sfrs, v, mem, trace)283 ReturnState (sfrs, v, mem, inds, trace) 250 284 251 285 … … 274 308 (args : Val.t list) 275 309 (mem : memory) 310 (inds : indexing list) 276 311 (trace : CostLabel.t list) : 277 312 state = … … 281 316 Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in 282 317 let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in 283 State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, lenv, mem', 284 trace) 318 (* allocate new constant indexing *) 319 let graph = def.RTLabs.f_graph in 320 let inds = new_ind inds in 321 State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace) 285 322 | RTLabs.F_ext def -> 286 323 let (mem', v) = interpret_external mem def.AST.ef_tag args in 287 ReturnState (sfrs, v, mem', trace)324 ReturnState (sfrs, v, mem', inds, trace) 288 325 289 326 … … 293 330 (ret_val : Val.t) 294 331 (mem : memory) 332 (inds : indexing list) 295 333 (trace : CostLabel.t list) : 296 334 state = … … 298 336 | None -> sf.lenv 299 337 | Some ret_reg -> update_local ret_reg ret_val sf.lenv in 300 State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, 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) 301 342 302 343 303 344 let small_step (st : state) : state = match st with 304 | State (sfrs, graph, sp, pc, lenv, mem, trace) ->345 | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) -> 305 346 let stmt = Label.Map.find pc graph in 306 interpret_statement sfrs graph sp lenv mem stmt trace307 | CallState (sfrs, f_def, args, mem, trace) ->308 state_after_call sfrs f_def args mem trace309 | ReturnState ([], ret_val, mem, trace) ->347 interpret_statement sfrs graph sp lenv mem stmt inds trace 348 | CallState (sfrs, f_def, args, mem, inds, trace) -> 349 state_after_call sfrs f_def args mem inds trace 350 | ReturnState ([], ret_val, mem, inds, trace) -> 310 351 assert false (* End of execution; handled in iter_small_step. *) 311 | ReturnState (sf :: sfrs, ret_val, mem, trace) ->312 state_after_return sf sfrs ret_val mem trace352 | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) -> 353 state_after_return sf sfrs ret_val mem inds trace 313 354 314 355 … … 324 365 if debug then print_state st ; 325 366 match small_step st with 326 | ReturnState ([], v, mem, trace) ->367 | ReturnState ([], v, mem, inds, trace) -> 327 368 print_and_return_result (compute_result v, List.rev trace) 328 369 | st' -> iter_small_step debug st' … … 352 393 let mem = init_mem p in 353 394 let main_def = find_function mem main in 354 let st = CallState ([], main_def, [], mem, [] ) in395 let st = CallState ([], main_def, [], mem, [], []) in 355 396 iter_small_step debug st -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml
r818 r1542 45 45 46 46 let print_cmp = function 47 | AST.Cmp_eq -> " eq"48 | AST.Cmp_ne -> " ne"49 | AST.Cmp_gt -> " gt"50 | AST.Cmp_ge -> " ge"51 | AST.Cmp_lt -> " lt"52 | AST.Cmp_le -> " le"47 | AST.Cmp_eq -> "=" 48 | AST.Cmp_ne -> "!=" 49 | AST.Cmp_gt -> ">" 50 | AST.Cmp_ge -> ">=" 51 | AST.Cmp_lt -> "<" 52 | AST.Cmp_le -> "<=" 53 53 54 54 let rec print_size = function … … 83 83 Printf.sprintf "%d%s" size (string_of_signedness sign) 84 84 85 let print_op1 = function 85 let print_op1 op r = Printf.sprintf "%s %s" 86 (match op with 86 87 | AST.Op_cast (int_type, dest_size) -> 87 88 Printf.sprintf "int%sto%d" (string_of_int_type int_type) dest_size 88 | AST.Op_negint -> " negint"89 | AST.Op_notbool -> " notbool"90 | AST.Op_notint -> " notint"91 | AST.Op_id -> " id"89 | AST.Op_negint -> "-" 90 | AST.Op_notbool -> "!" 91 | AST.Op_notint -> "!i" 92 | AST.Op_id -> "" 92 93 | AST.Op_ptrofint -> "ptrofint" 93 | AST.Op_intofptr -> "intofptr" 94 95 let print_op2 = function 96 | AST.Op_add -> "add" 97 | AST.Op_sub -> "sub" 98 | AST.Op_mul -> "mul" 99 | AST.Op_div -> "div" 94 | AST.Op_intofptr -> "intofptr") 95 (print_reg r) 96 97 let print_arg = function 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 102 let print_op2 op r s = Printf.sprintf "%s %s %s" 103 (print_arg r) 104 (match op with 105 | AST.Op_add -> "+" 106 | AST.Op_sub -> "-" 107 | AST.Op_mul -> "*" 108 | AST.Op_div -> "/" 100 109 | AST.Op_divu -> "/u" 101 110 | AST.Op_mod -> "mod" … … 104 113 | AST.Op_or -> "or" 105 114 | AST.Op_xor -> "xor" 106 | AST.Op_shl -> " shl"107 | AST.Op_shr -> " shr"108 | AST.Op_shru -> " shru"115 | AST.Op_shl -> "<<" 116 | AST.Op_shr -> ">>" 117 | AST.Op_shru -> ">>u" 109 118 | AST.Op_cmp cmp -> print_cmp cmp 110 | AST.Op_addp -> " addp"111 | AST.Op_subp -> " subp"112 | AST.Op_subpp -> " subpp"119 | AST.Op_addp -> "+p" 120 | AST.Op_subp -> "-p" 121 | AST.Op_subpp -> "-pp" 113 122 | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p" 114 | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u" 123 | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u") 124 (print_arg s) 115 125 116 126 … … 136 146 | RTLabs.St_skip lbl -> "--> " ^ lbl 137 147 | RTLabs.St_cost (cost_lbl, lbl) -> 138 Printf.sprintf "emit %s --> %s" cost_lbl lbl 148 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 149 Printf.sprintf "emit %s --> %s" cost_lbl lbl 150 | RTLabs.St_ind_0 (i, lbl) -> 151 Printf.sprintf "index %d --> %s" i lbl 152 | RTLabs.St_ind_inc (i, lbl) -> 153 Printf.sprintf "increment %d --> %s" i lbl 139 154 | RTLabs.St_cst (destr, cst, lbl) -> 140 Printf.sprintf " imm %s,%s --> %s"155 Printf.sprintf "%s := %s --> %s" 141 156 (print_reg destr) 142 157 (print_cst cst) 143 158 lbl 144 159 | RTLabs.St_op1 (op1, destr, srcr, lbl) -> 145 Printf.sprintf "%s %s, %s --> %s" 146 (print_op1 op1) 160 Printf.sprintf "%s := %s --> %s" 147 161 (print_reg destr) 148 (print_regsrcr)162 (print_op1 op1 srcr) 149 163 lbl 150 164 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) -> 151 Printf.sprintf "%s %s, %s, %s --> %s" 152 (print_op2 op2) 165 Printf.sprintf "%s := %s --> %s" 153 166 (print_reg destr) 154 (print_reg srcr1) 155 (print_reg srcr2) 167 (print_op2 op2 srcr1 srcr2) 156 168 lbl 157 169 | RTLabs.St_load (q, addr, destr, lbl) -> 158 Printf.sprintf "load %s, %s, %s --> %s" 170 Printf.sprintf "%s := *(%s) %s --> %s" 171 (print_reg destr) 159 172 (Memory.string_of_quantity q) 160 (print_reg addr) 161 (print_reg destr) 173 (print_arg addr) 162 174 lbl 163 175 | RTLabs.St_store (q, addr, srcr, lbl) -> 164 Printf.sprintf "store %s, %s, %s --> %s" 165 (Memory.string_of_quantity q) 166 (print_reg addr) 167 (print_reg srcr) 168 lbl 169 | RTLabs.St_call_id (f, args, res, sg, lbl) -> 170 Printf.sprintf "call \"%s\", %s, %s: %s --> %s" 176 Printf.sprintf "*(%s)%s := %s --> %s" 177 (Memory.string_of_quantity q) 178 (print_arg addr) 179 (print_arg srcr) 180 lbl 181 | RTLabs.St_call_id (f, args, Some r, sg, lbl) -> 182 Printf.sprintf "%s := \"%s\"(%s) : %s --> %s" 183 (print_reg r) 171 184 f 172 185 (print_args args) 173 (print_oreg res) 174 (Primitive.print_sig sg) 175 lbl 176 | RTLabs.St_call_ptr (f, args, res, sg, lbl) -> 177 Printf.sprintf "call_ptr %s, %s, %s: %s --> %s" 186 (Primitive.print_sig sg) 187 lbl 188 | RTLabs.St_call_id (f, args, None, sg, lbl) -> 189 Printf.sprintf "\"%s\"(%s) : %s --> %s" 190 f 191 (print_args args) 192 (Primitive.print_sig sg) 193 lbl 194 | RTLabs.St_call_ptr (f, args, Some r, sg, lbl) -> 195 Printf.sprintf "%s := *%s (%s) : %s --> %s" 196 (print_reg r) 178 197 (print_reg f) 179 198 (print_args args) 180 (print_oreg res) 199 (Primitive.print_sig sg) 200 lbl 201 | RTLabs.St_call_ptr (f, args, None, sg, lbl) -> 202 Printf.sprintf "*%s (%s) : %s --> %s" 203 (print_reg f) 204 (print_args args) 181 205 (Primitive.print_sig sg) 182 206 lbl 183 207 | RTLabs.St_tailcall_id (f, args, sg) -> 184 Printf.sprintf "tailcall \"%s\" , %s: %s"208 Printf.sprintf "tailcall \"%s\" (%s) : %s" 185 209 f 186 210 (print_args args) 187 211 (Primitive.print_sig sg) 188 212 | RTLabs.St_tailcall_ptr (f, args, sg) -> 189 Printf.sprintf "tailcall _ptr \"%s\", %s: %s"213 Printf.sprintf "tailcall *%s (%s) : %s" 190 214 (print_reg f) 191 215 (print_args args) … … 225 249 226 250 227 let print_graph n c =251 let print_graph n c entry = 228 252 let f lbl stmt s = 229 253 Printf.sprintf "%s%s: %s\n%s" … … 232 256 (print_statement stmt) 233 257 s in 234 Label.Map.fold f c "" 235 236 258 let f' lbl stmt (reach, s) = 259 (Label.Set.add lbl reach, f lbl stmt s) in 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 237 268 let print_internal_decl n f def = 238 269 … … 252 283 (n_spaces (n+2)) 253 284 def.RTLabs.f_exit 254 (print_graph (n+2) def.RTLabs.f_graph )285 (print_graph (n+2) def.RTLabs.f_graph def.RTLabs.f_entry) 255 286 256 287 -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli
r740 r1542 4 4 val print_statement : RTLabs.statement -> string 5 5 6 val print_cst : AST.cst -> string 7 8 val print_op1 : AST.op1 -> Register.t -> string 9 10 val print_op2 : AST.op2 -> RTLabs.argument -> RTLabs.argument -> string 11 6 12 val print_program : RTLabs.program -> string -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r818 r1542 93 93 | RTL.St_skip _ -> RTL.St_skip lbl 94 94 | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl) 95 | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl) 96 | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl) 95 97 | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl) 96 98 | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl) … … 685 687 add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def 686 688 689 | RTLabs.St_ind_0 (i, lbl') -> 690 add_graph lbl (RTL.St_ind_0 (i, lbl')) def 691 692 | RTLabs.St_ind_inc (i, lbl') -> 693 add_graph lbl (RTL.St_ind_inc (i, lbl')) def 694 687 695 | RTLabs.St_cst (destr, cst, lbl') -> 688 696 translate_cst cst (find_local_env destr lenv) lbl lbl' def … … 692 700 lbl lbl' def 693 701 694 | RTLabs.St_op2 (op2, destr, srcr1,srcr2, lbl') ->702 | RTLabs.St_op2 (op2, destr, RTLabs.Reg srcr1, RTLabs.Reg srcr2, lbl') -> 695 703 translate_op2 op2 (find_local_env destr lenv) 696 704 (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def 697 705 698 | RTLabs.St_load (_, addr, destr, lbl') ->706 | RTLabs.St_load (_, RTLabs.Reg addr, destr, lbl') -> 699 707 translate_load (find_local_env addr lenv) (find_local_env destr lenv) 700 708 lbl lbl' def 701 709 702 | RTLabs.St_store (_, addr,srcr, lbl') ->710 | RTLabs.St_store (_, RTLabs.Reg addr, RTLabs.Reg srcr, lbl') -> 703 711 translate_store (find_local_env addr lenv) (find_local_env srcr lenv) 704 712 lbl lbl' def … … 739 747 | RTLabs.St_return (Some r) -> 740 748 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 741 742 749 750 | _ -> assert false (*not possible because of previous removal of immediates*) 751 752 let remove_immediates def = 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 let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in 757 let new_r = Register.fresh def.RTLabs.f_runiverse in 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 let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in 765 let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in 766 let g = Label.Map.add lbl' s g in 767 (g, rs) 768 | RTLabs.St_store(q, a1, a2, l) -> 769 let (lbl', g, rs, r1) = load_arg a1 lbl g rs in 770 let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in 771 let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in 772 let g = Label.Map.add lbl' s g in 773 (g, rs) 774 | RTLabs.St_load (q, a, r, l) -> 775 let (lbl', g, rs, r1) = load_arg a lbl g rs in 776 let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in 777 let g = Label.Map.add lbl' s g in 778 (g, rs) 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 743 785 let translate_internal def = 786 let def = remove_immediates def in 744 787 let runiverse = def.RTLabs.f_runiverse in 745 788 let lenv = -
Deliverables/D2.2/8051/src/acc.ml
r1462 r1542 44 44 the intermediate programs. *) 45 45 Languages.compile (Options.is_debug_enabled ()) 46 src_language tgt_language input_ast46 (Options.get_transformations ()) src_language tgt_language input_ast 47 47 in 48 48 let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in … … 51 51 begin 52 52 let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) = 53 Languages.annotate input_ast final_ast in ( 53 let cost_tern = Options.is_cost_ternary_enabled () in 54 Languages.annotate cost_tern input_ast final_ast in ( 54 55 save ~suffix:"-annotated" annotated_input_ast; 55 56 Languages.save_cost exact_output output_filename cost_id cost_incr 56 57 extern_cost_variables); 57 58 end; 58 59 if Options.is_debug_enabled () then 59 60 if Options.is_debug_enabled () then 60 61 List.iter save intermediate_asts; 61 62 … … 93 94 Languages.save 94 95 (Options.is_asm_pretty ()) exact_output output_filename "" ast in 95 let target_asts = Languages.compile false src_language tgt_language input_ast 96 let target_asts = 97 Languages.compile false (Options.get_transformations ()) 98 src_language tgt_language input_ast 96 99 in 97 100 let final_ast, _ = Misc.ListExt.cut_last target_asts in -
Deliverables/D2.2/8051/src/checker.ml
r619 r1542 14 14 in 15 15 let sentence (k, (v1, v2)) = 16 let k = CostLabel.string_of_cost_label ~pretty:true k in 16 17 Printf.sprintf " Label %s %s in language `%s' \ 17 18 whereas it %s in language `%s'." -
Deliverables/D2.2/8051/src/clight/clight.mli
r818 r1542 117 117 (** The following constructors are used by the annotation process only. *) 118 118 119 | Ecost of CostLabel.t *expr (**r cost label. *)119 | Ecost of CostLabel.t * expr (**r cost label. *) 120 120 | Ecall of ident * expr * expr 121 121 … … 130 130 type label = Label.t 131 131 132 type loop_index = CostLabel.index option 133 132 134 type statement = 133 135 | Sskip (**r do nothing *) … … 136 138 | Ssequence of statement*statement (**r sequence *) 137 139 | Sifthenelse of expr*statement*statement (**r conditional *) 138 | Swhile of expr*statement(**r [while] loop *)139 | Sdowhile of expr*statement(**r [do] loop *)140 | Sfor of statement*expr*statement*statement(**r [for] loop *)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 *) 141 143 | Sbreak (**r [break] statement *) 142 144 | Scontinue (**r [continue] statement *) -
Deliverables/D2.2/8051/src/clight/clightAnnotator.ml
r1462 r1542 10 10 let cost_id_prefix = "_cost" 11 11 let cost_incr_prefix = "_cost_incr" 12 let loop_id_prefix = "_i" 12 13 13 14 … … 70 71 let def_idents = function 71 72 | Clight.Internal def -> 72 73 74 75 76 77 73 let vars = 74 string_set_of_list 75 (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in 76 let (names, cost_labels, user_labels) = 77 body_idents def.Clight.fn_body in 78 (StringTools.Set.union vars names, cost_labels, user_labels) 78 79 | Clight.External (id, _, _) -> 79 80 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in 80 81 let fun_idents (id, f_def) = 81 82 let (names, cost_labels, user_labels) = def_idents f_def in … … 93 94 let all_labels p = 94 95 let (_, cost_labels, user_labels) = prog_idents p in 95 let all = 96 CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) 97 cost_labels StringTools.Set.empty in 98 Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all 96 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 97 let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 98 Label.Set.fold StringTools.Set.add user_labels all 99 99 100 100 let all_idents p = 101 101 let (names, cost_labels, user_labels) = prog_idents p in 102 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 103 let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 102 104 let to_string_set fold set = 103 105 fold (fun lbl idents -> StringTools.Set.add lbl idents) set 104 106 StringTools.Set.empty in 105 let cost_labels = to_string_set CostLabel.Set.fold cost_labels in106 107 let user_labels = to_string_set Label.Set.fold user_labels in 107 108 StringTools.Set.union names (StringTools.Set.union cost_labels user_labels) … … 125 126 let const_int i = Clight.Expr (Clight.Econst_int i, int_typ) 126 127 128 let expr_of_cost_cond var = function 129 | CostExpr.Ceq k -> 130 Clight.Expr(Clight.Ebinop(Clight.Oeq, var, const_int k),int_typ) 131 | CostExpr.Cgeq k -> 132 Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) 133 | CostExpr.Cmod (a, b) -> 134 let modulus = 135 Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in 136 Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) 137 | CostExpr.Cgeqmod (k, a, b) -> 138 let modulus = 139 Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in 140 let modulus_eq = 141 Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in 142 let greater = 143 Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in 144 Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ) 145 146 let rec expr_of_cost_gen_cond var gc = 147 assert (not (CostExpr.CondSet.is_empty gc)); 148 let c = CostExpr.CondSet.min_elt gc in 149 let c_expr = expr_of_cost_cond var c in 150 let rest = CostExpr.CondSet.remove c gc in 151 if CostExpr.CondSet.is_empty rest then c_expr else 152 let rest_expr = expr_of_cost_gen_cond var rest in 153 Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ) 154 155 let rec expr_of_cost_expr prefix = function 156 | CostExpr.Exact k -> const_int k 157 | CostExpr.Ternary(index, cond, if_true, if_false) -> 158 let id = CostLabel.make_id prefix index in 159 let var = Clight.Expr(Clight.Evar id, int_typ) in 160 let cond_e = expr_of_cost_gen_cond var cond in 161 let if_true_e = expr_of_cost_expr prefix if_true in 162 let if_false_e = expr_of_cost_expr prefix if_false in 163 Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ) 164 165 (* as long as Clight parser will be called at the end, this hack works *) 166 (* this will be called in case -no-cost-tern is active. *) 167 let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function 168 | CostExpr.Exact k -> 169 Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type) 170 | CostExpr.Ternary(index, cond, if_true, if_false) -> 171 let id = CostLabel.make_id prefix index in 172 let var = Clight.Expr(Clight.Evar id, int_typ) in 173 let cond_e = expr_of_cost_gen_cond var cond in 174 let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in 175 let if_true_e = rec_call if_true in 176 let if_false_e = rec_call if_false in 177 Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ) 178 179 let rec stmt_of_cost_expr prefix cost_incr = function 180 | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k]) 181 | CostExpr.Ternary(index, cond, if_true, if_false) -> 182 let id = CostLabel.make_id prefix index in 183 let var = Clight.Expr(Clight.Evar id, int_typ) in 184 let cond_e = expr_of_cost_gen_cond var cond in 185 let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in 186 let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in 187 Clight.Sifthenelse (cond_e, if_true_s, if_false_s) 188 127 189 (* Instrument an expression. *) 128 190 129 let rec instrument_expr cost_mapping cost_incr e = 130 let Clight.Expr (e, t) = e in 131 match e with 132 | Clight.Ecost (lbl, e) 133 when CostLabel.Map.mem lbl cost_mapping && 134 CostLabel.Map.find lbl cost_mapping = 0 -> 135 e 136 | _ -> 137 let e' = instrument_expr_descr cost_mapping cost_incr e in 138 Clight.Expr (e', t) 139 and instrument_expr_descr cost_mapping cost_incr e = match e with 140 | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _ 141 | Clight.Esizeof _ -> e 142 | Clight.Ederef e -> 143 let e' = instrument_expr cost_mapping cost_incr e in 144 Clight.Ederef e' 145 | Clight.Eaddrof e -> 146 let e' = instrument_expr cost_mapping cost_incr e in 147 Clight.Eaddrof e' 148 | Clight.Eunop (op, e) -> 149 let e' = instrument_expr cost_mapping cost_incr e in 150 Clight.Eunop (op, e') 151 | Clight.Ebinop (op, e1, e2) -> 152 let e1' = instrument_expr cost_mapping cost_incr e1 in 153 let e2' = instrument_expr cost_mapping cost_incr e2 in 154 Clight.Ebinop (op, e1', e2') 155 | Clight.Ecast (t, e) -> 156 let e' = instrument_expr cost_mapping cost_incr e in 157 Clight.Ecast (t, e') 158 | Clight.Econdition (e1, e2, e3) -> 159 let e1' = instrument_expr cost_mapping cost_incr e1 in 160 let e2' = instrument_expr cost_mapping cost_incr e2 in 161 let e3' = instrument_expr cost_mapping cost_incr e3 in 162 Clight.Econdition (e1', e2', e3') 163 | Clight.Eandbool (e1, e2) -> 164 let e1' = instrument_expr cost_mapping cost_incr e1 in 165 let e2' = instrument_expr cost_mapping cost_incr e2 in 166 Clight.Eandbool (e1', e2') 167 | Clight.Eorbool (e1, e2) -> 168 let e1' = instrument_expr cost_mapping cost_incr e1 in 169 let e2' = instrument_expr cost_mapping cost_incr e2 in 170 Clight.Eorbool (e1', e2') 171 | Clight.Efield (e, x) -> 172 let e' = instrument_expr cost_mapping cost_incr e in 173 Clight.Efield (e', x) 174 | Clight.Ecost (lbl, e) when CostLabel.Map.mem lbl cost_mapping -> 175 let e' = instrument_expr cost_mapping cost_incr e in 176 let incr = CostLabel.Map.find lbl cost_mapping in 177 if incr = 0 then let Clight.Expr (e'', _) = e' in e'' 178 else Clight.Ecall (cost_incr, const_int incr, e') 179 | Clight.Ecost (_, e) -> 180 let Clight.Expr (e', _) = instrument_expr cost_mapping cost_incr e in 181 e' 182 | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *) 191 (* FIXME: currently using a hack (reparsing) *) 192 let instrument_expr cost_tern l_ind cost_mapping cost_incr = 193 let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with 194 | Clight.Ecost (lbl, _), e' :: _ -> 195 let atom = lbl.CostLabel.name in 196 let cost = 197 try 198 CostLabel.Atom.Map.find atom cost_mapping 199 with (* if atom is not present, then map to 0 *) 200 | Not_found -> CostExpr.Exact 0 in 201 if cost = CostExpr.Exact 0 then e' else 202 if cost_tern then 203 let cost = expr_of_cost_expr l_ind cost in 204 Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et) 205 else 206 side_effect_expr_of_cost_expr l_ind cost_incr e' et cost 207 | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *) 208 | _ -> ClightFold.expr_fill_exprs e sub_res in 209 ClightFold.expr2 f_expr 210 211 let loop_increment prefix depth body = match depth with 212 | None -> body 213 | Some d -> 214 let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in 215 let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in 216 Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1))) 217 218 let loop_reset_index prefix depth loop = match depth with 219 | None -> loop 220 | Some d -> 221 let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in 222 Clight.Ssequence(Clight.Sassign(id, const_int 0), loop) 223 183 224 184 225 (* Instrument a statement. *) 185 226 186 let rec instrument_body cost_mapping cost_incr stmt = match stmt with 187 | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None 188 | Clight.Sgoto _ -> 189 stmt 190 | Clight.Sassign (e1, e2) -> 191 let e1' = instrument_expr cost_mapping cost_incr e1 in 192 let e2' = instrument_expr cost_mapping cost_incr e2 in 193 Clight.Sassign (e1', e2') 194 | Clight.Scall (eopt, f, args) -> 195 let eopt' = match eopt with 196 | None -> None 197 | Some e -> Some (instrument_expr cost_mapping cost_incr e) in 198 let f' = instrument_expr cost_mapping cost_incr f in 199 let args' = List.map (instrument_expr cost_mapping cost_incr) args in 200 Clight.Scall (eopt', f', args') 201 | Clight.Ssequence (s1, s2) -> 202 Clight.Ssequence (instrument_body cost_mapping cost_incr s1, 203 instrument_body cost_mapping cost_incr s2) 204 | Clight.Sifthenelse (e, s1, s2) -> 205 let e' = instrument_expr cost_mapping cost_incr e in 206 let s1' = instrument_body cost_mapping cost_incr s1 in 207 let s2' = instrument_body cost_mapping cost_incr s2 in 208 Clight.Sifthenelse (e', s1', s2') 209 | Clight.Swhile (e, s) -> 210 let e' = instrument_expr cost_mapping cost_incr e in 211 let s' = instrument_body cost_mapping cost_incr s in 212 Clight.Swhile (e', s') 213 | Clight.Sdowhile (e, s) -> 214 let e' = instrument_expr cost_mapping cost_incr e in 215 let s' = instrument_body cost_mapping cost_incr s in 216 Clight.Sdowhile (e', s') 217 | Clight.Sfor (s1, e, s2, s3) -> 218 let s1' = instrument_body cost_mapping cost_incr s1 in 219 let e' = instrument_expr cost_mapping cost_incr e in 220 let s2' = instrument_body cost_mapping cost_incr s2 in 221 let s3' = instrument_body cost_mapping cost_incr s3 in 222 Clight.Sfor (s1', e', s2', s3') 223 | Clight.Sreturn (Some e) -> 224 let e' = instrument_expr cost_mapping cost_incr e in 225 Clight.Sreturn (Some e') 226 | Clight.Sswitch (e, ls) -> 227 let e' = instrument_expr cost_mapping cost_incr e in 228 let ls' = instrument_ls cost_mapping cost_incr ls in 229 Clight.Sswitch (e', ls') 230 | Clight.Slabel (lbl, s) -> 231 let s' = instrument_body cost_mapping cost_incr s in 232 Clight.Slabel (lbl, s') 233 | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping -> 227 (* FIXME: use ClightFold, a much better option *) 228 let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt = 229 let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in 230 let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in 231 match stmt with 232 | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None 233 | Clight.Sgoto _ -> 234 stmt 235 | Clight.Sassign (e1, e2) -> 236 let e1' = instr_expr e1 in 237 let e2' = instr_expr e2 in 238 Clight.Sassign (e1', e2') 239 | Clight.Scall (eopt, f, args) -> 240 let eopt' = Option.map instr_expr eopt in 241 let f' = instr_expr f in 242 let args = List.map (instr_expr) args in 243 Clight.Scall (eopt', f', args) 244 | Clight.Ssequence (s1, s2) -> 245 Clight.Ssequence ( 246 instr_body s1, 247 instr_body s2) 248 | Clight.Sifthenelse (e, s1, s2) -> 249 let e' = instr_expr e in 250 let s1' = instr_body s1 in 251 let s2' = instr_body s2 in 252 Clight.Sifthenelse (e', s1', s2') 253 | Clight.Swhile (i, e, s) -> 254 let e' = instr_expr e in 255 let s' = instr_body s in 256 let s' = loop_increment l_ind i s' in 257 loop_reset_index l_ind i (Clight.Swhile (None, e', s')) 258 | Clight.Sdowhile (i, e, s) -> 259 let e' = instr_expr e in 260 let s' = instr_body s in 261 let s' = loop_increment l_ind i s' in 262 loop_reset_index l_ind i (Clight.Sdowhile (None, e', s')) 263 | Clight.Sfor (i, s1, e, s2, s3) -> 264 let s1' = instr_body s1 in 265 let e' = instr_expr e in 266 let s2' = instr_body s2 in 267 let s3' = instr_body s3 in 268 let s3' = loop_increment l_ind i s3' in 269 loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3')) 270 | Clight.Sreturn (Some e) -> 271 let e' = instr_expr e in 272 Clight.Sreturn (Some e') 273 | Clight.Sswitch (e, ls) -> 274 let e' = instr_expr e in 275 let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in 276 Clight.Sswitch (e', ls') 277 | Clight.Slabel (lbl, s) -> 278 let s' = instr_body s in 279 Clight.Slabel (lbl, s') 280 | Clight.Scost (lbl, s) -> 234 281 (* Keep the cost label in the code. *) 235 let s' = instrument_body cost_mapping cost_incr s in 236 let incr = CostLabel.Map.find lbl cost_mapping in 237 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 238 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 239 let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in 240 Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s')) 241 (* 242 let s' = instrument_body cost_mapping cost_incr s in 243 let incr = CostLabel.Map.find lbl cost_mapping in 244 if incr = 0 then s' 245 else 246 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 247 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 248 let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in 249 Clight.Ssequence (Clight.Scall (None, f, args), s') 250 *) 251 | Clight.Scost (lbl, s) -> 252 (* Keep the cost label in the code and show the increment of 0. *) 253 let s' = instrument_body cost_mapping cost_incr s in 254 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 255 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 256 let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in 257 Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s')) 258 (* 259 instrument_body cost_mapping cost_incr s 260 *) 261 and instrument_ls cost_mapping cost_incr = function 282 let s' = instr_body s in 283 let atom = lbl.CostLabel.name in 284 let cost = 285 try 286 CostLabel.Atom.Map.find atom cost_mapping 287 with (* if atom is not present, then map to 0 *) 288 | Not_found -> CostExpr.Exact 0 in 289 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 290 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 291 let cost_stmt = 292 if not cost_tern then stmt_of_cost_expr l_ind f cost else 293 let cost = expr_of_cost_expr l_ind cost in 294 Clight.Scall(None, f, [cost]) in 295 Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s')) 296 (* 297 let s' = instrument_body l_ind cost_mapping cost_incr s in 298 let incr = CostLabel.Map.find lbl cost_mapping in 299 if incr = 0 then s' 300 else 301 let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in 302 let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in 303 let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in 304 Clight.Ssequence (Clight.Scall (None, f, args), s') 305 *) 306 (* 307 instrument_body l_ind cost_mapping cost_incr s 308 *) 309 and instrument_ls cost_tern l_ind cost_mapping cost_incr = function 262 310 | Clight.LSdefault s -> 263 let s' = instrument_body cost_ mapping cost_incr s in311 let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in 264 312 Clight.LSdefault s' 265 313 | Clight.LScase (i, s, ls) -> 266 let s' = instrument_body cost_ mapping cost_incr s in267 let ls' = instrument_ls cost_ mapping cost_incr ls in314 let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in 315 let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in 268 316 Clight.LScase (i, s', ls') 317 318 let rec loop_indexes_defs prefix max_depth = 319 if max_depth = 0 then [] else 320 let max_depth = max_depth - 1 in 321 let id = CostLabel.make_id prefix max_depth in 322 (id, int_typ) :: loop_indexes_defs prefix max_depth 323 324 let max_depth = 325 let f_expr _ _ = () in 326 let f_stmt stmt _ res_stmts = 327 let curr_max = List.fold_left max 0 res_stmts in 328 if curr_max > 0 then curr_max else 329 match stmt with 330 | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_) 331 | Clight.Sfor(Some x,_,_,_,_) -> x + 1 332 | _ -> 0 in 333 ClightFold.statement2 f_expr f_stmt 269 334 270 335 (* Instrument a function. *) 271 336 272 let instrument_funct cost_ mapping cost_incr (id, def) =337 let instrument_funct cost_tern l_ind cost_mapping cost_incr (id, def) = 273 338 let def = match def with 274 339 | Clight.Internal def -> 275 let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in 276 Clight.Internal { def with Clight.fn_body = body } 340 let max_depth = max_depth def.Clight.fn_body in 341 let vars = loop_indexes_defs l_ind max_depth in 342 let vars = List.rev_append vars def.Clight.fn_vars in 343 let body = def.Clight.fn_body in 344 let body = 345 instrument_body cost_tern l_ind cost_mapping cost_incr body in 346 Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars} 277 347 | Clight.External _ -> def 278 348 in … … 326 396 name of the cost variable and the name of the cost increment function. *) 327 397 328 let instrument p cost_mapping =398 let instrument cost_tern p cost_mapping = 329 399 330 400 (* Create a fresh 'cost' variable. *) … … 334 404 let cost_decl = cost_decl cost_id in 335 405 406 (* Create a fresh loop index prefix *) 407 let names = StringTools.Set.add cost_id names in 408 let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in 409 336 410 (* Create a fresh uninitialized global variable for each extern function. *) 337 411 let (extern_cost_decls, extern_cost_variables) = … … 344 418 let cost_incr_def = cost_incr_def cost_id cost_incr in 345 419 420 (* Turn the mapping from indexed cost labels to integers into one from *) 421 (* cost atoms to cost expresisons *) 422 let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in 423 346 424 (* Instrument each function *) 425 let prog_funct = p.Clight.prog_funct in 347 426 let prog_funct = 348 List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in 427 let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in 428 List.map f prog_funct in 349 429 350 430 (* Glue all this together. *) -
Deliverables/D2.2/8051/src/clight/clightAnnotator.mli
r1462 r1542 2 2 (** This module defines the instrumentation of a [Clight] program. *) 3 3 4 (** [instrument prog cost_map] instruments the program [prog]. First a fresh 5 global variable --- the so-called cost variable --- is added to the program. 6 Then, each cost label in the program is replaced by an increment of the cost 7 variable, following the mapping [cost_map]. The function also returns the 8 name of the cost variable, the name of the cost increment function, and a 9 fresh uninitialized global (cost) variable associated to each extern 10 function. *) 11 12 val instrument : Clight.program -> int CostLabel.Map.t -> 4 (** [instrument cost_tern prog cost_map] instruments the program [prog]. First a 5 fresh global variable --- the so-called cost variable --- is added to the 6 program. Then, each cost label in the program is replaced by an increment of 7 the cost variable, following the mapping [cost_map]. The function also 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). *) 13 val instrument : bool -> Clight.program -> int CostLabel.Map.t -> 13 14 Clight.program * string * string * string StringTools.Map.t 14 15 -
Deliverables/D2.2/8051/src/clight/clightFold.ml
r818 r1542 116 116 | Clight.Ssequence (stmt1, stmt2) -> ([], [stmt1 ; stmt2]) 117 117 | Clight.Sifthenelse (e, stmt1, stmt2) -> ([e], [stmt1 ; stmt2]) 118 | Clight.Swhile ( e, stmt) | Clight.Sdowhile (e, stmt) -> ([e], [stmt])119 | Clight.Sfor ( stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3])118 | Clight.Swhile (_, e, stmt) | Clight.Sdowhile (_, e, stmt) -> ([e], [stmt]) 119 | Clight.Sfor (_, stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3]) 120 120 | Clight.Sreturn (Some e) -> ([e], []) 121 121 | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts) … … 145 145 | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ -> 146 146 Clight.Sifthenelse (e, stmt1, stmt2) 147 | Clight.Swhile _, e :: _, stmt :: _ ->148 Clight.Swhile ( e, stmt)149 | Clight.Sdowhile _, e :: _, stmt :: _ ->150 Clight.Sdowhile ( e, stmt)151 | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->152 Clight.Sfor ( stmt1, e, stmt2, stmt3)147 | Clight.Swhile (i, _, _), e :: _, stmt :: _ -> 148 Clight.Swhile (i, e, stmt) 149 | Clight.Sdowhile (i, _, _), e :: _, stmt :: _ -> 150 Clight.Sdowhile (i, e, stmt) 151 | Clight.Sfor (i, _, _, _, _), e :: _, stmt1 :: stmt2 :: stmt3 :: _ -> 152 Clight.Sfor (i, stmt1, e, stmt2, stmt3) 153 153 | Clight.Sreturn (Some _), e :: _, _ -> Clight.Sreturn (Some e) 154 154 | Clight.Sswitch (_, lbl_stmts), e :: _, _ -> -
Deliverables/D2.2/8051/src/clight/clightFromC.ml
r818 r1542 490 490 Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2) 491 491 | C.Swhile(e, s1) -> 492 Swhile( convertExpr env e, convertStmt env s1)492 Swhile(None, convertExpr env e, convertStmt env s1) 493 493 | C.Sdowhile(s1, e) -> 494 Sdowhile( convertExpr env e, convertStmt env s1)494 Sdowhile(None, convertExpr env e, convertStmt env s1) 495 495 | C.Sfor(s1, e, s2, s3) -> 496 Sfor( convertStmt env s1, convertExpr env e, convertStmt env s2,496 Sfor(None, convertStmt env s1, convertExpr env e, convertStmt env s2, 497 497 convertStmt env s3) 498 498 | C.Sbreak -> -
Deliverables/D2.2/8051/src/clight/clightInterpret.ml
r818 r1542 4 4 type localEnv = Value.address LocalEnv.t 5 5 type memory = Clight.fundef Mem.memory 6 type indexing = CostLabel.const_indexing 6 7 7 8 open Clight … … 26 27 | Kstop 27 28 | Kseq of statement*continuation 28 | Kwhile of expr*statement*continuation29 | Kdowhile of expr*statement*continuation30 | Kfor2 of expr*statement*statement*continuation31 | Kfor3 of expr*statement*statement*continuation29 | Kwhile of int option*expr*statement*continuation 30 | Kdowhile of int option*expr*statement*continuation 31 | Kfor2 of int option*expr*statement*statement*continuation 32 | Kfor3 of int option*expr*statement*statement*continuation 32 33 | Kswitch of continuation 33 34 | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation 34 35 35 36 type state = 36 | State of cfunction*statement*continuation*localEnv*memory 37 | Callstate of fundef*Value.t list*continuation*memory 38 | Returnstate of Value.t*continuation*memory 37 | State of cfunction*statement*continuation*localEnv*memory*indexing list 38 | Callstate of fundef*Value.t list*continuation*memory*indexing list 39 | Returnstate of Value.t*continuation*memory*indexing list 39 40 40 41 let string_of_unop = function … … 104 105 | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")" 105 106 | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field 106 | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e) 107 | Ecost (cost_lbl, e) -> 108 let cost_lbl = CostLabel.string_of_cost_label cost_lbl in 109 "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e) 107 110 | Ecall (f, arg, e) -> 108 111 "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")" … … 110 113 let string_of_args args = 111 114 "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")" 115 116 let string_of_loop_depth = function 117 | None -> "" 118 | Some d -> " at " ^ string_of_int d 112 119 113 120 let rec string_of_statement = function … … 119 126 | Ssequence _ -> "sequence" 120 127 | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")" 121 | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")" 122 | Sdowhile _ -> "dowhile" 123 | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)" 128 | Swhile (i, e, _) -> 129 let d = string_of_loop_depth i in 130 "while" ^ d ^ " (" ^ (string_of_expr e) ^ ")" 131 | Sdowhile (i, _, _) -> 132 let d = string_of_loop_depth i in 133 "dowhile" ^ d 134 | Sfor (i, s, _, _, _) -> 135 let d = string_of_loop_depth i in 136 "for" ^ d ^ " (" ^ (string_of_statement s) ^ "; ...)" 124 137 | Sbreak -> "break" 125 138 | Scontinue -> "continue" … … 129 142 | Slabel (lbl, _) -> "label " ^ lbl 130 143 | Sgoto lbl -> "goto " ^ lbl 131 | Scost (lbl, _) -> "cost " ^ lbl 144 | Scost (lbl, _) -> 145 let lbl = CostLabel.string_of_cost_label lbl in 146 "cost " ^ lbl 132 147 133 148 let string_of_local_env lenv = … … 136 151 LocalEnv.fold f lenv "" 137 152 138 let print_state = function139 | State (_, stmt, _, lenv, mem ) ->140 Printf.printf "Local environment:\n%s\n\nMemory:%s\n Regular state: %s\n\n%!"153 let print_state state = match state with 154 | State (_, stmt, _, lenv, mem, c) -> 155 Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: " 141 156 (string_of_local_env lenv) 142 (Mem.to_string mem) 157 (Mem.to_string mem); 158 let i = CostLabel.curr_const_ind c in 159 CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i; 160 Printf.printf "\nRegular state: %s\n\n%!" 143 161 (string_of_statement stmt) 144 | Callstate (_, args, _, mem ) ->162 | Callstate (_, args, _, mem, _) -> 145 163 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!" 146 164 (Mem.to_string mem) 147 165 (MiscPottier.string_of_list " " Value.to_string args) 148 | Returnstate (v, _, mem ) ->166 | Returnstate (v, _, mem, _) -> 149 167 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 150 168 (Mem.to_string mem) … … 155 173 156 174 let rec call_cont = function 157 | Kseq (_,k) | Kwhile (_, _,k) | Kdowhile (_,_,k)158 | Kfor2 (_, _,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k175 | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k) 176 | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k 159 177 | k -> k 160 178 … … 174 192 | None -> find_label1 lbl s2 k 175 193 ) 176 | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k)) 177 | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k)) 178 | Sfor (a1,a2,a3,s1) -> 179 (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with 194 | Swhile (i,a,s1) -> find_label1 lbl s1 (Kwhile(i,a,s1,k)) 195 | Sdowhile (i,a,s1) -> find_label1 lbl s1 (Kdowhile(i,a,s1,k)) 196 | Sfor (i,a1,a2,a3,s1) -> 197 (* doubt: should we search for labels in a1? *) 198 (match find_label1 lbl a1 (Kseq ((Sfor(i,Sskip,a2,a3,s1)),k)) with 180 199 | Some sk -> Some sk 181 200 | None -> 182 (match find_label1 lbl s1 (Kfor2( a2,a3,s1,k)) with201 (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with 183 202 | Some sk -> Some sk 184 | None -> find_label1 lbl a3 (Kfor3( a2,a3,s1,k))203 | None -> find_label1 lbl a3 (Kfor3(i,a2,a3,s1,k)) 185 204 )) 186 205 | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k) … … 355 374 let is_false (v, _) = Value.is_false v 356 375 357 let rec eval_expr localenv m (Expr (ee, tt)) =376 let rec eval_expr localenv m c (Expr (ee, tt)) = 358 377 match ee with 359 378 | Econst_int i -> … … 369 388 ((v, tt), []) 370 389 | Ederef e when is_function_type tt || is_big_type tt -> 371 let ((v1,_),l1) = eval_expr localenv m e in390 let ((v1,_),l1) = eval_expr localenv m c e in 372 391 ((v1,tt),l1) 373 392 | Ederef e -> 374 let ((v1,_),l1) = eval_expr localenv m e in393 let ((v1,_),l1) = eval_expr localenv m c e in 375 394 let addr = address_of_value v1 in 376 395 let v = Mem.load m (size_of_ctype tt) addr in 377 396 ((v,tt),l1) 378 397 | Eaddrof exp -> 379 let ((addr,_),l) = eval_lvalue localenv m exp in398 let ((addr,_),l) = eval_lvalue localenv m c exp in 380 399 ((value_of_address addr,tt),l) 381 400 | Ebinop (op,exp1,exp2) -> 382 let (v1,l1) = eval_expr localenv m exp1 in383 let (v2,l2) = eval_expr localenv m exp2 in401 let (v1,l1) = eval_expr localenv m c exp1 in 402 let (v2,l2) = eval_expr localenv m c exp2 in 384 403 ((eval_binop tt v1 v2 op,tt),l1@l2) 385 404 | Eunop (op,exp) -> 386 let (e1,l1) = eval_expr localenv m exp in405 let (e1,l1) = eval_expr localenv m c exp in 387 406 ((eval_unop tt e1 op,tt),l1) 388 407 | Econdition (e1,e2,e3) -> 389 let (v1,l1) = eval_expr localenv m e1 in390 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)408 let (v1,l1) = eval_expr localenv m c e1 in 409 if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2) 391 410 else 392 if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)411 if is_false v1 then let (v3,l3) = eval_expr localenv m c e3 in (v3,l1@l3) 393 412 else (v1,l1) 394 413 | Eandbool (e1,e2) -> 395 let (v1,l1) = eval_expr localenv m e1 in396 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)414 let (v1,l1) = eval_expr localenv m c e1 in 415 if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2) 397 416 else (v1,l1) 398 417 | Eorbool (e1,e2) -> 399 let (v1,l1) = eval_expr localenv m e1 in400 if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)418 let (v1,l1) = eval_expr localenv m c e1 in 419 if is_false v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2) 401 420 else (v1,l1) 402 421 | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[]) 403 422 | Efield (e1,id) -> 404 let ((v1,t1),l1) = eval_expr localenv m e1 in423 let ((v1,t1),l1) = eval_expr localenv m c e1 in 405 424 let addr = address_of_value (get_offset v1 id t1) in 406 425 ((Mem.load m (size_of_ctype tt) addr, tt), l1) 407 426 | Ecost (lbl,e1) -> 408 let (v1,l1) = eval_expr localenv m e1 in 427 (* applying current indexing on label *) 428 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in 429 let (v1,l1) = eval_expr localenv m c e1 in 409 430 (v1,lbl::l1) 410 431 | Ecall _ -> assert false (* only used by the annotation process *) 411 432 | Ecast (cty,exp) -> 412 let ((v,ty),l1) = eval_expr localenv m exp in433 let ((v,ty),l1) = eval_expr localenv m c exp in 413 434 ((eval_cast (v,ty,cty),tt),l1) 414 435 415 and eval_lvalue localenv m (Expr (e,t)) = match e with436 and eval_lvalue localenv m c (Expr (e,t)) = match e with 416 437 | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_) 417 438 | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_) | Eorbool (_,_) … … 419 440 | Evar id -> ((find_symbol localenv m id,t),[]) 420 441 | Ederef ee -> 421 let ((v,_),l1) = eval_expr localenv m ee in442 let ((v,_),l1) = eval_expr localenv m c ee in 422 443 ((address_of_value v,t),l1) 423 444 | Efield (ee,id) -> 424 let ((v,tt),l1) = eval_expr localenv m ee in445 let ((v,tt),l1) = eval_expr localenv m c ee in 425 446 let v' = get_offset v id tt in 426 447 ((address_of_value v', t), l1) 427 448 | Ecost (lbl,ee) -> 428 let (v,l) = eval_lvalue localenv m ee in449 let (v,l) = eval_lvalue localenv m c ee in 429 450 (v,lbl::l) 430 451 | Ecall _ -> assert false (* only used in the annotation process *) 431 452 432 let eval_exprlist lenv mem es =453 let eval_exprlist lenv mem c es = 433 454 let f (vs, cost_lbls) e = 434 let ((v, _), cost_lbls') = eval_expr lenv mem e in455 let ((v, _), cost_lbls') = eval_expr lenv mem c e in 435 456 (vs @ [v], cost_lbls @ cost_lbls') in 436 457 List.fold_left f ([], []) es … … 464 485 else error "undefined condition guard value." 465 486 466 let eval_stmt f k e m s = match s, k with 467 | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[]) 468 | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[]) 469 | Sskip, Kdowhile(a,s,k) -> 470 let ((v1, _),l1) = eval_expr e m a in 471 let a_false = (State(f,Sskip,k,e,m),l1) in 472 let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in 487 let eval_stmt f k e m s c = match s, k with 488 | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[]) 489 | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k') 490 | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') -> 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. *) 494 let ((v1,_),l1) = eval_expr e m c a in 495 let a_false = (State(f,Sskip,k',e,m,c),l1) in 496 let a_true = (State(f,s,k,e,m,c),l1) in 473 497 condition v1 a_true a_false 474 | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[]) 475 | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 476 | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[]) 498 | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) -> 499 CostLabel.continue_loop_opt c i; 500 let ((v1,_),l1) = eval_expr e m c a2 in 501 let a_false = (State(f,Sskip,k,e,m,c),l1) in 502 let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in 503 condition v1 a_true a_false 504 | Sskip, Kfor2(i,a2,a3,s,k) -> 505 (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[]) 506 | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[]) 477 507 | Sskip, Kcall _ -> 478 508 let m' = free_local_env m e in 479 (Returnstate(Value.undef,k,m' ),[])509 (Returnstate(Value.undef,k,m',c),[]) 480 510 | Sassign(a1, a2), _ -> 481 let ((v1,t1),l1) = (eval_lvalue e m a1) in482 let ((v2,t2),l2) = eval_expr e m a2 in483 (State(f,Sskip,k,e,assign m v2 t1 v1 ),l1@l2)511 let ((v1,t1),l1) = (eval_lvalue e m c a1) in 512 let ((v2,t2),l2) = eval_expr e m c a2 in 513 (State(f,Sskip,k,e,assign m v2 t1 v1,c),l1@l2) 484 514 | Scall(None,a,al), _ -> 485 let ((v1,_),l1) = eval_expr e m a in515 let ((v1,_),l1) = eval_expr e m c a in 486 516 let fd = Mem.find_fun_def m (address_of_value v1) in 487 let (vargs,l2) = eval_exprlist e m al in488 (Callstate(fd,vargs,Kcall(None,f,e,k),m ),l1@l2)517 let (vargs,l2) = eval_exprlist e m c al in 518 (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2) 489 519 | Scall(Some lhs,a,al), _ -> 490 let ((v1,_),l1) = eval_expr e m a in520 let ((v1,_),l1) = eval_expr e m c a in 491 521 let fd = Mem.find_fun_def m (address_of_value v1) in 492 let (vargs,l2) = eval_exprlist e m al in493 let (vt3,l3) = eval_lvalue e m lhs in494 (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m ),l1@l2@l3)495 | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m ),[])522 let (vargs,l2) = eval_exprlist e m c al in 523 let (vt3,l3) = eval_lvalue e m c lhs in 524 (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3) 525 | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[]) 496 526 | Sifthenelse(a,s1,s2), _ -> 497 let ((v1,_),l1) = eval_expr e m a in498 let a_true = (State(f,s1,k,e,m ),l1) in499 let a_false = (State(f,s2,k,e,m ),l1) in527 let ((v1,_),l1) = eval_expr e m c a in 528 let a_true = (State(f,s1,k,e,m,c),l1) in 529 let a_false = (State(f,s2,k,e,m,c),l1) in 500 530 condition v1 a_true a_false 501 | Swhile(a,s), _ -> 502 let ((v1,_),l1) = eval_expr e m a in 503 let a_false = (State(f,Sskip,k,e,m),l1) in 504 let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in 531 | Swhile(i,a,s), _ -> 532 CostLabel.enter_loop_opt c i; 533 let ((v1,_),l1) = eval_expr e m c a in 534 let a_false = (State(f,Sskip,k,e,m,c),l1) in 535 let a_true = (State(f,s,Kwhile(i,a,s,k),e,m,c),l1) in 505 536 condition v1 a_true a_false 506 | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[]) 507 | Sfor(Sskip,a2,a3,s), _ -> 508 let ((v1,_),l1) = eval_expr e m a2 in 509 let a_false = (State(f,Sskip,k,e,m),l1) in 510 let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in 537 | Sdowhile(i,a,s), _ -> 538 CostLabel.enter_loop_opt c i; 539 (State(f,s,Kdowhile(i,a,s,k),e,m,c),[]) 540 | Sfor(i,Sskip,a2,a3,s), _ -> 541 CostLabel.enter_loop_opt c i; 542 let ((v1,_),l1) = eval_expr e m c a2 in 543 let a_false = (State(f,Sskip,k,e,m,c),l1) in 544 let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in 511 545 condition v1 a_true a_false 512 | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[]) 513 | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[]) 514 | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[]) 515 | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[]) 516 | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[]) 517 | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[]) 518 | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[]) 519 | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[]) 520 | Scontinue, Kdowhile(a,s,k) -> 521 let ((v1,_),l1) = eval_expr e m a in 522 let a_false = (State(f,Sskip,k,e,m),l1) in 523 let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in 524 condition v1 a_true a_false 525 | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 526 | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[]) 546 | Sfor(i,a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(i,Sskip,a2,a3,s),k),e,m,c),[]) 547 | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[]) 548 | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k) 549 | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[]) 550 | Scontinue, Kseq(_,k) 551 | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[]) 527 552 | Sreturn None, _ -> 528 553 let m' = free_local_env m e in 529 (Returnstate(Value.undef,(call_cont k),m' ),[])554 (Returnstate(Value.undef,(call_cont k),m',c),[]) 530 555 | Sreturn (Some a), _ -> 531 let ((v1,_),l1) = eval_expr e m a in556 let ((v1,_),l1) = eval_expr e m c a in 532 557 let m' = free_local_env m e in 533 (Returnstate(v1,call_cont k,m' ),l1)558 (Returnstate(v1,call_cont k,m',c),l1) 534 559 | Sswitch(a,sl), _ -> 535 let ((v,_),l) = eval_expr e m a in560 let ((v,_),l) = eval_expr e m c a in 536 561 let n = Value.to_int v in 537 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l) 538 | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[]) 539 | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl]) 562 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l) 563 | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[]) 564 | Scost(lbl,s), _ -> 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]) 540 568 | Sgoto lbl, _ -> 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 *) 541 572 let (s', k') = find_label lbl f.fn_body (call_cont k) in 542 (State(f,s',k',e,m ),[])573 (State(f,s',k',e,m,c),[]) 543 574 | _ -> assert false (* should be impossible *) 544 575 … … 546 577 module InterpretExternal = Primitive.Interpret (Mem) 547 578 548 let interpret_external k mem f args =579 let interpret_external k mem c f args = 549 580 let (mem', v) = match InterpretExternal.t mem f args with 550 581 | (mem', InterpretExternal.V vs) -> … … 552 583 (mem', v) 553 584 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in 554 Returnstate (v, k, mem' )555 556 let step_call args cont mem = function585 Returnstate (v, k, mem',c) 586 587 let step_call args cont mem c = function 557 588 | Internal f -> 558 589 let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in 559 State (f, f.fn_body, cont, e, mem') 590 (* initializing loop indices *) 591 let c = CostLabel.new_const_ind c in 592 State (f, f.fn_body, cont, e, mem', c) 560 593 | External(id,targs,tres) when List.length targs = List.length args -> 561 interpret_external cont mem id args594 interpret_external cont mem c id args 562 595 | External(id,_,_) -> 563 596 error ("wrong size of arguments when calling external " ^ id ^ ".") 564 597 565 598 let step = function 566 | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt 567 | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[]) 568 | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[]) 569 | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) -> 599 | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c 600 | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[]) 601 | Returnstate(v,Kcall(None,f,e,k),m,c) -> 602 let c = CostLabel.forget_const_ind c in 603 (State(f,Sskip,k,e,m,c),[]) 604 | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) -> 605 let c = CostLabel.forget_const_ind c in 570 606 let m' = assign m v ty vv in 571 (State(f,Sskip,k,e,m' ),[])607 (State(f,Sskip,k,e,m',c),[]) 572 608 | _ -> error "state malformation." 573 609 … … 603 639 if debug then Printf.printf "Result = %s\n%!" 604 640 (IntValue.Int32.to_string res) ; 605 (res, cost_labels) in641 (res, List.rev cost_labels) in 606 642 if debug then print_state state ; 607 643 match state with 608 | Returnstate(v,Kstop,_ ) -> (* Explicit return in main *)644 | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *) 609 645 print_and_return_result (compute_result v) 610 | State(_,Sskip,Kstop,_,_ ) -> (* Implicit return in main *)646 | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *) 611 647 print_and_return_result IntValue.Int32.zero 612 648 | state -> exec debug cost_labels (step state) … … 618 654 | Some main -> 619 655 let mem = init_mem prog in 620 let first_state = (Callstate (find_fundef main mem,[],Kstop,mem ),[]) in656 let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in 621 657 exec debug [] first_state -
Deliverables/D2.2/8051/src/clight/clightLabelling.ml
r1504 r1542 1 1 2 2 (** This module defines the labelling of a [Clight] program. *) 3 4 module IntListSet = Set.Make(struct type t = int list let compare = compare end) 3 5 4 6 open Clight … … 6 8 7 9 8 (* Add a cost label in front of a statement . *)9 10 let add_starting_cost_label cost_universe stmt =11 Clight.Scost (CostLabel. Gen.freshcost_universe, stmt)10 (* Add a cost label in front of a statement with the current indexing. *) 11 12 let add_starting_cost_label indexing cost_universe stmt = 13 Clight.Scost (CostLabel.fresh indexing cost_universe, stmt) 12 14 13 15 (* Add a cost label at the end of a statement. *) 14 16 15 let add_ending_cost_label cost_universe stmt = 16 Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip) 17 let add_ending_cost_label indexing cost_universe stmt = 18 let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in 19 Clight.Ssequence (stmt, lbld_skip) 17 20 18 21 … … 24 27 25 28 26 let add_cost_label_e cost_universe e =27 Expr (Ecost (CostLabel. Gen.freshcost_universe, e), typeof e)29 let add_cost_label_e indexing cost_universe e = 30 Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e) 28 31 29 32 30 33 (* Add cost labels to an expression. *) 31 34 32 let rec add_cost_labels_e cost_universe = function33 | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)34 35 and add_cost_labels_expr cost_universe exp = match exp with35 let rec add_cost_labels_e ind cost_universe = function 36 | Expr (exp,cty) -> Expr (add_cost_labels_expr ind cost_universe exp,cty) 37 38 and add_cost_labels_expr ind cost_universe exp = match exp with 36 39 | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp 37 | Ederef e -> Ederef (add_cost_labels_e cost_universe e)38 | Eaddrof e -> Eaddrof (add_cost_labels_e cost_universe e)39 | Eunop (op,e) -> Eunop (op,(add_cost_labels_e cost_universe e))40 | Ederef e -> Ederef (add_cost_labels_e ind cost_universe e) 41 | Eaddrof e -> Eaddrof (add_cost_labels_e ind cost_universe e) 42 | Eunop (op,e) -> Eunop (op,(add_cost_labels_e ind cost_universe e)) 40 43 | Ebinop (op,e1,e2) -> 41 44 Ebinop (op, 42 add_cost_labels_e cost_universe e1,43 add_cost_labels_e cost_universe e2)44 | Ecast (t,e) -> Ecast (t, add_cost_labels_e cost_universe e)45 add_cost_labels_e ind cost_universe e1, 46 add_cost_labels_e ind cost_universe e2) 47 | Ecast (t,e) -> Ecast (t, add_cost_labels_e ind cost_universe e) 45 48 | Eandbool (e1,e2) -> 46 let e1' = add_cost_labels_e cost_universe e1 in47 let e2' = add_cost_labels_e cost_universe e2 in48 let b1 = add_cost_label_e cost_universe (const_int 1) in49 let b2 = add_cost_label_e cost_universe (const_int 0) in49 let e1' = add_cost_labels_e ind cost_universe e1 in 50 let e2' = add_cost_labels_e ind cost_universe e2 in 51 let b1 = add_cost_label_e ind cost_universe (const_int 1) in 52 let b2 = add_cost_label_e ind cost_universe (const_int 0) in 50 53 let e2' = Expr (Econdition (e2', b1, b2), int_type) in 51 let e2' = add_cost_label_e cost_universe e2' in52 let e3' = add_cost_label_e cost_universe (const_int 0) in54 let e2' = add_cost_label_e ind cost_universe e2' in 55 let e3' = add_cost_label_e ind cost_universe (const_int 0) in 53 56 Econdition (e1', e2', e3') 54 57 | Eorbool (e1,e2) -> 55 let e1' = add_cost_labels_e cost_universe e1 in56 let e2' = add_cost_label_e cost_universe (const_int 1) in57 let e3' = add_cost_labels_e cost_universe e2 in58 let b1 = add_cost_label_e cost_universe (const_int 1) in59 let b2 = add_cost_label_e cost_universe (const_int 0) in58 let e1' = add_cost_labels_e ind cost_universe e1 in 59 let e2' = add_cost_label_e ind cost_universe (const_int 1) in 60 let e3' = add_cost_labels_e ind cost_universe e2 in 61 let b1 = add_cost_label_e ind cost_universe (const_int 1) in 62 let b2 = add_cost_label_e ind cost_universe (const_int 0) in 60 63 let e3' = Expr (Econdition (e3', b1, b2), int_type) in 61 let e3' = add_cost_label_e cost_universe e3' in64 let e3' = add_cost_label_e ind cost_universe e3' in 62 65 Econdition (e1', e2', e3') 63 | Efield (e,id) -> Efield (add_cost_labels_e cost_universe e,id)66 | Efield (e,id) -> Efield (add_cost_labels_e ind cost_universe e,id) 64 67 | Econdition (e1,e2,e3) -> 65 let e1' = add_cost_labels_e cost_universe e1 in66 let e2' = add_cost_labels_e cost_universe e2 in67 let e2' = add_cost_label_e cost_universe e2' in68 let e3' = add_cost_labels_e cost_universe e3 in69 let e3' = add_cost_label_e cost_universe e3' in68 let e1' = add_cost_labels_e ind cost_universe e1 in 69 let e2' = add_cost_labels_e ind cost_universe e2 in 70 let e2' = add_cost_label_e ind cost_universe e2' in 71 let e3' = add_cost_labels_e ind cost_universe e3 in 72 let e3' = add_cost_label_e ind cost_universe e3' in 70 73 Econdition (e1', e2', e3') 71 74 | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *) 72 75 73 let add_cost_labels_opt cost_universe = function 74 | None -> None 75 | Some e -> Some (add_cost_labels_e cost_universe e) 76 77 let add_cost_labels_lst cost_universe l = 78 List.map (add_cost_labels_e cost_universe) l 76 let add_cost_labels_opt ind cost_universe = 77 Option.map (add_cost_labels_e ind cost_universe) 78 79 let add_cost_labels_lst ind cost_universe l = 80 List.map (add_cost_labels_e ind cost_universe) l 79 81 80 82 81 83 (* Add cost labels to a statement. *) 82 84 83 let rec add_cost_labels_st cost_universe = function 85 let update_ind i ind = 86 match i with 87 | None -> ind 88 | Some _ -> CostLabel.add_id_indexing ind 89 90 let rec add_cost_labels_st ind cost_universe = function 84 91 | Sskip -> Sskip 85 92 | Sassign (e1,e2) -> 86 Sassign (add_cost_labels_ecost_universe e1,87 add_cost_labels_ecost_universe e2)93 Sassign (add_cost_labels_e ind cost_universe e1, 94 add_cost_labels_e ind cost_universe e2) 88 95 | Scall (e1,e2,lst) -> 89 Scall (add_cost_labels_optcost_universe e1,90 add_cost_labels_ecost_universe e2,91 add_cost_labels_lstcost_universe lst)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) 92 99 | Ssequence (s1,s2) -> 93 Ssequence (add_cost_labels_stcost_universe s1,94 add_cost_labels_st cost_universe s2)100 Ssequence (add_cost_labels_st ind cost_universe s1, 101 add_cost_labels_st ind cost_universe s2) 95 102 | Sifthenelse (e,s1,s2) -> 96 let s1' = add_cost_labels_st cost_universe s1 in 97 let s1' = add_starting_cost_label cost_universe s1' in 98 let s2' = add_cost_labels_st cost_universe s2 in 99 let s2' = add_starting_cost_label cost_universe s2' in 100 Sifthenelse (add_cost_labels_e cost_universe e, s1', s2') 101 | Swhile (e,s) -> 102 let s' = add_cost_labels_st cost_universe s in 103 let s' = add_starting_cost_label cost_universe s' in 104 add_ending_cost_label cost_universe 105 (Swhile (add_cost_labels_e cost_universe e, s')) 106 | Sdowhile (e,s) -> 107 let s = add_cost_labels_st cost_universe s in 108 let s' = add_starting_cost_label cost_universe s in 109 add_ending_cost_label cost_universe 110 (Sdowhile (add_cost_labels_e cost_universe e, s')) 111 | Sfor (s1,e,s2,s3) -> 112 let s1' = add_cost_labels_st cost_universe s1 in 113 let s2' = add_cost_labels_st cost_universe s2 in 114 let s3' = add_cost_labels_st cost_universe s3 in 115 let s3' = add_starting_cost_label cost_universe s3' in 116 add_ending_cost_label cost_universe 117 (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3')) 118 | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e) 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') 108 | Swhile (i,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')) 115 | Sdowhile (i,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')) 121 | Sfor (i,s1,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')) 129 | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e) 119 130 | Sswitch (e,ls) -> 120 Sswitch (add_cost_labels_ecost_universe e,121 add_cost_labels_lscost_universe ls)131 Sswitch (add_cost_labels_e ind cost_universe e, 132 add_cost_labels_ls ind cost_universe ls) 122 133 | Slabel (lbl,s) -> 123 let s' = add_cost_labels_stcost_universe s in124 let s' = add_starting_cost_labelcost_universe s' in125 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') 126 137 | Scost (_,_) -> assert false 127 138 | _ as stmt -> stmt 128 139 129 and add_cost_labels_ls cost_universe = function140 and add_cost_labels_ls ind cost_universe = function 130 141 | LSdefault s -> 131 let s' = add_cost_labels_st cost_universe s in132 let s' = add_starting_cost_label cost_universe s' in142 let s' = add_cost_labels_st ind cost_universe s in 143 let s' = add_starting_cost_label ind cost_universe s' in 133 144 LSdefault s' 134 145 | LScase (i,s,ls) -> 135 let s' = add_cost_labels_st cost_universe s in 136 let s' = add_starting_cost_label cost_universe s' in 137 LScase (i, s', add_cost_labels_ls cost_universe ls) 138 139 140 (* Add cost labels to a function. *) 141 142 let add_cost_labels_f cost_universe = function 143 | (id,Internal fd) -> (id,Internal { 144 fn_return = fd.fn_return ; 145 fn_params = fd.fn_params ; 146 fn_vars = fd.fn_vars ; 147 fn_body = add_starting_cost_label cost_universe 148 (add_cost_labels_st cost_universe fd.fn_body) 149 }) 150 | (id,External (a,b,c)) -> (id,External (a,b,c)) 151 146 let s' = add_cost_labels_st ind cost_universe s in 147 let s' = add_starting_cost_label ind cost_universe s' in 148 LScase (i, s', add_cost_labels_ls ind cost_universe ls) 149 150 151 (* traversal of code assigning to every label the "loop address" of it. *) 152 (* A loop address like [2, 0, 1] means the corresponding label is in the *) 153 (* third loop inside the first loop inside the second loop of the body. *) 154 let rec assign_loop_addrs_s 155 (current : int list) 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 173 and assign_loop_addrs_ls current offset m = function 174 | LSdefault s -> assign_loop_addrs_s current offset m s 175 | LScase(_,s,ls) -> 176 let (offset, m) = assign_loop_addrs_s current offset m s in 177 assign_loop_addrs_ls current offset m ls 178 179 let rec is_prefix l1 l2 = match l1, l2 with 180 | [], _ -> true 181 | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2 182 | _ -> false 183 184 (* traversal of code which for every statement [s] returns the set of loop*) 185 (* addresses which are multi-entry due to a goto in [s]. *) 186 let rec find_multi_entry_loops_s 187 (m : int list Label.Map.t) 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) 210 211 and find_multi_entry_loops_ls m current offset = function 212 | LSdefault s -> find_multi_entry_loops_s m current offset s 213 | LScase(_,s,ls) -> 214 let (offset, set1) = find_multi_entry_loops_s m current offset s in 215 let (offset, set2) = find_multi_entry_loops_ls m current offset ls in 216 (offset, IntListSet.union set1 set2) 217 218 (* final pass where loops are indexed *) 219 let rec index_loops_s multi_entry current offset depth = function 220 (* I am supposing you cannot jump to the update statement of for loops... *) 221 | Swhile(_,b,s) -> 222 let current' = offset :: current in 223 let is_bad = IntListSet.mem current' multi_entry in 224 let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 225 let (_, s) = index_loops_s multi_entry current' 0 depth s in 226 (offset + 1, Swhile(i,b,s)) 227 | Sdowhile(_,b,s) -> 228 let current' = offset :: current in 229 let is_bad = IntListSet.mem current' multi_entry in 230 let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 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) -> 251 let (offset, s) = index_loops_ls multi_entry current offset depth ls in 252 (offset, Sswitch(v, ls)) 253 | _ as s -> (offset, s) 254 255 and index_loops_ls multi_entry current offset depth = function 256 | LSdefault s -> 257 let (offset, s) = 258 index_loops_s multi_entry current offset depth s in 259 (offset, LSdefault s) 260 | LScase(v,s,ls) -> 261 let (offset, s) = index_loops_s multi_entry current offset depth s in 262 let (offset, ls) = index_loops_ls multi_entry current offset depth ls in 263 (offset, LScase(v,s,ls)) 264 265 (* Index loops and introduce cost labels in functions *) 266 let process_f cost_universe = function 267 | (id,Internal fd) -> 268 let body = fd.fn_body in 269 (* assign loop addresses to labels *) 270 let (_, m) = assign_loop_addrs_s [] 0 Label.Map.empty body in 271 (* find which loops are potentially multi-entry *) 272 let (_, multi_entry) = find_multi_entry_loops_s m [] 0 body in 273 (* index loops accordingly *) 274 let (_, body) = index_loops_s multi_entry [] 0 0 body in 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}) 282 | _ as x -> x 283 284 152 285 153 286 (** [add_cost_labels prog] inserts some labels to enable … … 156 289 let add_cost_labels p = 157 290 let labs = ClightAnnotator.all_labels p in 158 let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in 159 let cost_prefix = CostLabel.Gen.fresh_prefix labs "_cost" in 160 let cost_universe = CostLabel.Gen.new_universe cost_prefix in 161 { 162 prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct; 163 prog_main = p.prog_main; 164 prog_vars = p.prog_vars 165 } 291 let add = CostLabel.Atom.Set.add in 292 let empty = CostLabel.Atom.Set.empty in 293 let labs = StringTools.Set.fold add labs empty in 294 let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in 295 let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in 296 {p with prog_funct = List.map (process_f cost_universe) p.prog_funct} -
Deliverables/D2.2/8051/src/clight/clightParser.mli
r1462 r1542 1 2 1 (** This module implements a parser for [C] based on [gcc] and 3 2 [CIL]. *) -
Deliverables/D2.2/8051/src/clight/clightPrinter.ml
r818 r1542 196 196 | Efield(e1, id) -> 197 197 fprintf p "%a.%s" print_expr_prec (level, e1) id 198 | Ecost (lbl,e1) -> 199 fprintf p "(/* %s */ %a)" lbl print_expr e1 200 | Ecall (f, arg, e) -> 198 | Ecost(lbl, e1) -> 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 | Ecall(f, arg, e) -> 201 203 fprintf p "(%s(%a), %a)" f print_expr arg print_expr e 202 204 … … 214 216 print_expr p e1; 215 217 print_expr_list p (false, et) 218 219 let print_loop_depth p = function 220 | None -> fprintf p "" 221 | Some x -> fprintf p "/* single entry loop depth: %d */@," x 216 222 217 223 let rec print_stmt p s = … … 241 247 print_stmt s1 242 248 print_stmt s2 243 | Swhile(e, s) -> 244 fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]" 245 print_expr e 246 print_stmt s 247 | Sdowhile(e, s) -> 248 fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]" 249 print_stmt s 250 print_expr e 251 | Sfor(s_init, e, s_iter, s_body) -> 252 fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]" 253 print_stmt_for s_init 254 print_expr e 255 print_stmt_for s_iter 256 print_stmt s_body 249 | Swhile(i, e, s) -> 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 | Sdowhile(i, e, s) -> 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 | Sfor(i, s_init, e, s_iter, s_body) -> 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 257 266 | Sbreak -> 258 267 fprintf p "break;" 259 268 | Scontinue -> 260 269 fprintf p "continue;" 261 270 | Sswitch(e, cases) -> 262 263 264 271 fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]" 272 print_expr e 273 print_cases cases 265 274 | Sreturn None -> 266 275 fprintf p "return;" 267 276 | Sreturn (Some e) -> 268 277 fprintf p "return %a;" print_expr e 269 278 | Slabel(lbl, s1) -> 270 279 fprintf p "%s:@ %a" lbl print_stmt s1 271 280 | Sgoto lbl -> 272 fprintf p "goto %s;" lbl 273 | Scost (lbl,s1) -> 281 fprintf p "goto %s;" lbl 282 | Scost (lbl,s1) -> 283 let lbl = CostLabel.string_of_cost_label lbl in 274 284 fprintf p "%s:@ %a" lbl print_stmt s1 275 285 … … 468 478 | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 469 479 | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 470 | Swhile( e, s) -> collect_expr e; collect_stmt s471 | Sdowhile( e, s) -> collect_stmt s; collect_expr e472 | Sfor( s_init, e, s_iter, s_body) ->473 474 480 | Swhile(_, e, s) -> collect_expr e; collect_stmt s 481 | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e 482 | Sfor(_, s_init, e, s_iter, s_body) -> 483 collect_stmt s_init; collect_expr e; 484 collect_stmt s_iter; collect_stmt s_body 475 485 | Sbreak -> () 476 486 | Scontinue -> () -
Deliverables/D2.2/8051/src/clight/clightToCminor.ml
r1462 r1542 495 495 AST.res = ret_type } 496 496 497 let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res = 498 let (tmps, sub_stmts_res) = List.split sub_stmts_res in 499 let tmps = List.flatten tmps in 500 501 let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with 502 503 | Clight.Sskip, _, _ -> ([], Cminor.St_skip) 504 505 | Clight.Sassign (e1, _), _ :: e2 :: _, _ -> 497 let ind_0 i stmt = match i with 498 | None -> stmt 499 | Some x -> Cminor.St_ind_0(x, stmt) 500 501 let ind_inc i stmt = match i with 502 | None -> stmt 503 | Some x -> Cminor.St_ind_inc(x, stmt) 504 505 let trans_for = 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) 526 527 let rec translate_stmt fresh var_locs cnt_lbl br_lbl = function 528 529 | Clight.Sskip -> ([], Cminor.St_skip) 530 531 | Clight.Sassign (e1, e2) -> 532 let e2 = translate_expr var_locs e2 in 506 533 ([], assign var_locs e1 e2) 507 534 508 | Clight.Scall (None, _, _), f :: args, _ -> 535 | Clight.Scall (None, f, args) -> 536 let f = translate_expr var_locs f in 537 let args = List.map (translate_expr var_locs) args in 509 538 ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args)) 510 539 511 | Clight.Scall (Some e, _, _), _ :: f :: args, _ -> 540 | Clight.Scall (Some e, f, args) -> 541 let f = translate_expr var_locs f in 542 let args = List.map (translate_expr var_locs) args in 512 543 let t = sig_type_of_ctype (clight_type_of e) in 513 544 let tmp = fresh () in … … 518 549 ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign)) 519 550 520 | Clight.Swhile _, e :: _, stmt :: _ -> 521 let econd = 522 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 551 | Clight.Swhile (i,e,stmt) -> 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 *) 523 560 let scond = 524 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 525 ([], 526 Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond, 527 Cminor.St_block stmt)))) 528 529 | Clight.Sdowhile _, e :: _, stmt :: _ -> 530 let econd = 531 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 561 Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in 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 565 (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip))) 566 567 | Clight.Sdowhile (i,e,stmt) -> 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 572 let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in 573 let e = translate_expr var_locs e in 574 let jmp lbl = Cminor.St_goto lbl in 532 575 let scond = 533 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 534 ([], 535 Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt, 536 scond)))) 537 538 | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ -> 539 let econd = 540 Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in 541 let scond = 542 Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in 543 let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in 544 ([], 545 Cminor.St_seq (stmt1, 546 Cminor.St_block 547 (Cminor.St_loop (Cminor.St_seq (scond, body))))) 548 549 | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ -> 550 ([], Cminor.St_ifthenelse (e, stmt1, stmt2)) 551 552 | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ -> 553 ([], Cminor.St_seq (stmt1, stmt2)) 554 555 | Clight.Sbreak, _, _ -> ([], Cminor.St_exit 1) 556 557 | Clight.Scontinue, _, _ -> ([], Cminor.St_exit 0) 558 559 | Clight.Sswitch _, _, _ -> 576 Cminor.St_ifthenelse (e, ind_inc i (jmp loop_lbl), Cminor.St_skip) in 577 let loop = 578 Cminor.St_seq (stmt, scond) in 579 let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in 580 (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip))) 581 582 | Clight.Sfor _ -> assert false (* transformed *) 583 584 | Clight.Sifthenelse (e, stmt1, stmt2) -> 585 let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in 586 let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in 587 let e = translate_expr var_locs e in 588 (tmps1 @ tmps2, Cminor.St_ifthenelse (e, stmt1, stmt2)) 589 590 | Clight.Ssequence(stmt1,stmt2) -> 591 let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in 592 let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in 593 (tmps1 @ tmps2, Cminor.St_seq (stmt1, stmt2)) 594 595 | Clight.Sbreak -> 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) 600 601 | Clight.Scontinue -> 602 let cnt_lbl = match cnt_lbl with 603 | Some x -> x 604 | None -> invalid_arg("continue without enclosing scope") in 605 ([], Cminor.St_goto cnt_lbl) 606 | Clight.Sswitch _ -> 560 607 (* Should not appear because of switch transformation performed 561 608 beforehand. *) 562 609 assert false 563 610 564 | Clight.Sreturn None, _, _ -> ([], Cminor.St_return None) 565 566 | Clight.Sreturn (Some _), e :: _, _ -> ([], Cminor.St_return (Some e)) 567 568 | Clight.Slabel (lbl, _), _, stmt :: _ -> ([], Cminor.St_label (lbl, stmt)) 569 570 | Clight.Sgoto lbl, _, _ -> ([], Cminor.St_goto lbl) 571 572 | Clight.Scost (lbl, _), _, stmt :: _ -> ([], Cminor.St_cost (lbl, stmt)) 573 574 | _ -> assert false (* type error *) in 575 576 (tmps @ added_tmps, stmt) 577 578 let translate_statement fresh var_locs = 579 ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs) 611 | Clight.Sreturn None -> ([], Cminor.St_return None) 612 613 | Clight.Sreturn (Some e) -> 614 let e = translate_expr var_locs e in 615 ([], Cminor.St_return (Some e)) 616 617 | Clight.Slabel (lbl, stmt) -> 618 let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in 619 (tmps, Cminor.St_label (lbl, stmt)) 620 621 | Clight.Sgoto lbl -> ([], Cminor.St_goto lbl) 622 623 | Clight.Scost (lbl, stmt) -> 624 let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in 625 (tmps, Cminor.St_cost (lbl, stmt)) 626 627 (* | _ -> assert false (* type error *) *) 580 628 581 629 … … 598 646 let params = 599 647 List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in 600 let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in 648 let body = cfun.Clight.fn_body in 649 let body = trans_for body in 650 let (tmps, body) = translate_stmt fresh var_locs None None body in 601 651 let body = add_stack_parameters_initialization var_locs body in 602 652 { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ; -
Deliverables/D2.2/8051/src/cminor/cminor.mli
r818 r1542 34 34 | St_seq of statement * statement 35 35 | St_ifthenelse of expression * statement * statement 36 | St_loop of statement36 (* | St_loop of statement 37 37 | St_block of statement 38 | St_exit of int 38 | St_exit of int *) 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. *)43 | St_switch of expression * (int* int) list * int41 table of cases and their corresponding labels to go to, 42 and the label to go to in the default case. *) 43 | St_switch of expression * (int*Label.t) list * Label.t 44 44 45 45 | St_return of expression option 46 46 | St_label of AST.ident * statement 47 | St_goto of string47 | St_goto of Label.t 48 48 | St_cost of CostLabel.t * statement 49 | St_ind_0 of CostLabel.index * statement 50 | St_ind_inc of CostLabel.index * statement 49 51 50 52 -
Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml
r818 r1542 204 204 let all_labels p = 205 205 let (cost_labels, user_labels) = prog_labels p in 206 let all = 207 CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) 208 cost_labels StringTools.Set.empty in 206 let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 207 let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in 209 208 Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all -
Deliverables/D2.2/8051/src/cminor/cminorFold.ml
r818 r1542 31 31 32 32 let statement_subs = function 33 | Cminor.St_skip | Cminor.St_exit _ |Cminor.St_return None33 | Cminor.St_skip | (*Cminor.St_exit _ |*) Cminor.St_return None 34 34 | Cminor.St_goto _ -> ([], []) 35 35 | Cminor.St_assign (_, e) | Cminor.St_switch (e, _, _) … … 43 43 | Cminor.St_ifthenelse (e, stmt1, stmt2) -> 44 44 ([e], [stmt1 ; stmt2]) 45 | Cminor.St_loop stmt | Cminor.St_block stmt 46 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) -> 45 (*| Cminor.St_loop stmt | Cminor.St_block stmt *) 46 | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) 47 | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (_, stmt) -> 47 48 ([], [stmt]) 48 49 49 50 let statement_fill_subs stmt sub_es sub_stmts = 50 51 match stmt, sub_es, sub_stmts with 51 | ( Cminor.St_skip | Cminor.St_exit _ |Cminor.St_return None52 | ( Cminor.St_skip | (*Cminor.St_exit _ |*) Cminor.St_return None 52 53 | Cminor.St_goto _), _, _ -> stmt 53 54 | Cminor.St_assign (x, _), e :: _, _ -> … … 67 68 | Cminor.St_ifthenelse _, e :: _, stmt1 :: stmt2 :: _ -> 68 69 Cminor.St_ifthenelse (e, stmt1, stmt2) 69 | Cminor.St_loop _, _, stmt :: _ ->70 (* | Cminor.St_loop _, _, stmt :: _ -> 70 71 Cminor.St_loop stmt 71 72 | Cminor.St_block _, _, stmt :: _ -> 72 Cminor.St_block stmt 73 Cminor.St_block stmt *) 73 74 | Cminor.St_label (lbl, _), _, stmt :: _ -> 74 75 Cminor.St_label (lbl, stmt) 75 76 | Cminor.St_cost (lbl, _), _, stmt :: _ -> 76 77 Cminor.St_cost (lbl, stmt) 78 | Cminor.St_ind_0 (i, _), _, stmt :: _ -> 79 Cminor.St_ind_0 (i, stmt) 80 | Cminor.St_ind_inc (i, _), _, stmt :: _ -> 81 Cminor.St_ind_inc (i, stmt) 77 82 | _ -> assert false (* do not use on these arguments *) 78 83 -
Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml
r1462 r1542 23 23 (* State of execution *) 24 24 25 type indexing = CostLabel.const_indexing 26 25 27 type continuation = 26 28 Ct_stop 27 29 | Ct_cont of statement*continuation 28 | Ct_endblock of continuation 30 (* | Ct_endblock of continuation *) 29 31 | Ct_returnto of 30 32 ident option*internal_function*Val.address*local_env*continuation … … 32 34 type state = 33 35 State_regular of 34 internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory) 35 | State_call of function_def*Val.t list*continuation*(function_def Mem.memory) 36 | State_return of Val.t*continuation*(function_def Mem.memory) 36 internal_function*statement*continuation*Val.address*local_env* 37 (function_def Mem.memory)*indexing list 38 | State_call of function_def*Val.t list*continuation* 39 (function_def Mem.memory)*indexing list 40 | State_return of Val.t*continuation*(function_def Mem.memory)*indexing list 37 41 38 42 let string_of_local_env lenv = … … 57 61 | St_seq _ -> "sequence" 58 62 | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")" 59 | St_loop _ -> "loop"63 (* | St_loop _ -> "loop" 60 64 | St_block _ -> "block" 61 | St_exit n -> "exit " ^ (string_of_int n) 65 | St_exit n -> "exit " ^ (string_of_int n) *) 62 66 | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")" 63 67 | St_return None -> "return" … … 65 69 | St_label (lbl, _) -> "label " ^ lbl 66 70 | St_goto lbl -> "goto " ^ lbl 67 | St_cost (lbl, _) -> "cost " ^ lbl 71 | St_cost (lbl, _) -> 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 68 76 69 77 let print_state = function 70 | State_regular (_, stmt, _, sp, lenv, mem ) ->71 Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n \nRegular state: %s\n\n%!"78 | State_regular (_, stmt, _, sp, lenv, mem, i) -> 79 Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\nIndexing:" 72 80 (string_of_local_env lenv) 73 81 (Mem.to_string mem) 74 (Val.to_string (value_of_address sp)) 82 (Val.to_string (value_of_address sp)); 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%!" 75 86 (string_of_statement stmt) 76 | State_call (_, args, _, mem ) ->87 | State_call (_, args, _, mem,_) -> 77 88 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!" 78 89 (Mem.to_string mem) 79 90 (MiscPottier.string_of_list " " Val.to_string args) 80 | State_return (v, _, mem ) ->91 | State_return (v, _, mem,_) -> 81 92 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 82 93 (Mem.to_string mem) … … 221 232 222 233 let rec callcont = function 223 Ct_stop -> Ct_stop 224 | Ct_cont(_,k) -> callcont k 225 | Ct_endblock(k) -> callcont k 226 | Ct_returnto(a,b,c,d,e) -> Ct_returnto(a,b,c,d,e) 234 | Ct_cont(_,k) (*| Ct_endblock k *) -> callcont k 235 | (Ct_stop | Ct_returnto _) as k -> k 227 236 228 237 let findlabel lbl st k = … … 243 252 | Some(v) -> Some(v) 244 253 ) 245 | St_loop(s) -> fdlbl (Ct_cont(St_loop(s),k)) s 246 | St_block(s) -> fdlbl (Ct_endblock(k)) s 247 | St_exit(_) -> None 248 | St_switch(_,_,_) -> None 249 | St_return(_) -> None 250 | St_label(l,s) when l = lbl -> Some((s,k)) 251 | St_goto(_) -> None 252 | St_cost (_,s) | St_label (_,s) -> fdlbl k s 254 (* | St_loop(s) -> fdlbl (Ct_cont(St_loop(s),k)) s 255 | St_block(s) -> fdlbl (Ct_endblock(k)) s 256 | St_exit(_) -> None *) 257 | St_switch(_,_,_) -> None 258 | St_return(_) -> None 259 | St_label(l,s) when l = lbl -> Some((s,k)) 260 | St_goto(_) -> None 261 | St_cost(_,s) | St_label(_,s) 262 | St_ind_0(_,s) | St_ind_inc(_,s) -> fdlbl k s 253 263 in match fdlbl k st with 254 264 None -> assert false (*Wrong label*) … … 256 266 257 267 258 let call_state sigma e m f params cont =268 let call_state sigma e m i f params cont = 259 269 let (addr,l1) = eval_expression sigma e m f in 260 270 let fun_def = Mem.find_fun_def m (address_of_value addr) in 261 271 let (args,l2) = eval_exprlist sigma e m params in 262 (State_call(fun_def,args,cont,m ),l1@l2)263 264 let eval_stmt f k sigma e m s = match s, k with265 | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m ),[])266 | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])272 (State_call(fun_def,args,cont,m,i),l1@l2) 273 274 let eval_stmt f k sigma e m i s = match s, k with 275 | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[]) 276 (* | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[]) *) 267 277 | St_skip, (Ct_returnto _ as k) -> 268 (State_return (Val.undef,k,Mem.free m sigma ),[])278 (State_return (Val.undef,k,Mem.free m sigma,i),[]) 269 279 | St_skip,Ct_stop -> 270 (State_return (Val.undef,Ct_stop,Mem.free m sigma ),[])280 (State_return (Val.undef,Ct_stop,Mem.free m sigma,i),[]) 271 281 | St_assign(x,exp),_ -> 272 282 let (v,l) = eval_expression sigma e m exp in 273 283 let e = LocalEnv.add x v e in 274 (State_regular(f, St_skip, k, sigma, e, m ),l)284 (State_regular(f, St_skip, k, sigma, e, m, i),l) 275 285 | St_store(q,a1,a2),_ -> 276 286 let (v1,l1) = eval_expression sigma e m a1 in 277 287 let (v2,l2) = eval_expression sigma e m a2 in 278 288 let m = Mem.storeq m q (address_of_value v1) v2 in 279 (State_regular(f, St_skip, k, sigma, e, m ),l1@l2)289 (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2) 280 290 | St_call(xopt,f',params,_),_ -> 281 call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))291 call_state sigma e m i f' params (Ct_returnto(xopt,f,sigma,e,k)) 282 292 | St_tailcall(f',params,_),_ -> 283 call_state sigma e m f' params (callcont k)284 | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m ),[])293 call_state sigma e m i f' params (callcont k) 294 | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[]) 285 295 | St_ifthenelse(exp,s1,s2),_ -> 286 296 let (v,l) = eval_expression sigma e m exp in … … 290 300 if Val.is_false v then s2 291 301 else error "undefined conditional value." in 292 (State_regular(f,next_stmt,k,sigma,e,m ),l)293 | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])294 | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m ),[])295 | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m ),[])296 | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m ),[])302 (State_regular(f,next_stmt,k,sigma,e,m,i),l) 303 (* | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[]) 304 | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[]) 305 | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[]) 306 | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[]) 297 307 | St_exit(n),Ct_endblock(k) -> 298 (State_regular(f,(St_exit (n-1)),k,sigma,e,m ),[])299 | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m ),[])300 | St_goto(lbl),_ -> 308 (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[]) *) 309 | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[]) 310 | St_goto(lbl),_ -> 301 311 let (s2,k2) = findlabel lbl f.f_body (callcont k) in 302 (State_regular(f,s2,k2,sigma,e,m ),[])312 (State_regular(f,s2,k2,sigma,e,m,i),[]) 303 313 | St_switch(exp,lst,def),_ -> 304 314 let (v,l) = eval_expression sigma e m exp in 305 315 if Val.is_int v then 306 316 try 307 let i = Val.to_int v in 308 let nb_exit = 309 if List.mem_assoc i lst then List.assoc i lst 310 else def in 311 (State_regular(f, St_exit nb_exit,k, sigma, e, m),l) 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 let (s',k') = findlabel lbl f.f_body (callcont k) in 324 (State_regular(f, s', k', sigma, e, m, i),l) 312 325 with _ -> error "int value too big." 313 326 else error "undefined switch value." 314 327 | St_return(None),_ -> 315 (State_return (Val.undef,callcont k,Mem.free m sigma ),[])328 (State_return (Val.undef,callcont k,Mem.free m sigma,i),[]) 316 329 | St_return(Some(a)),_ -> 317 330 let (v,l) = eval_expression sigma e m a in 318 (State_return (v,callcont k,Mem.free m sigma),l) 319 | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl]) 320 | _ -> error "state malformation." 331 (State_return (v,callcont k,Mem.free m sigma,i),l) 332 | St_cost(lbl,s),_ -> 333 (* applying current indexing on label *) 334 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind i) lbl in 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 (State_regular(f,s,k,sigma,e,m,i), []) 342 (* | _ -> error "state malformation." *) 321 343 322 344 323 345 module InterpretExternal = Primitive.Interpret (Mem) 324 346 325 let interpret_external k mem f args =347 let interpret_external k mem i f args = 326 348 let (mem', v) = match InterpretExternal.t mem f args with 327 349 | (mem', InterpretExternal.V vs) -> … … 329 351 (mem', v) 330 352 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in 331 State_return (v, k, mem' )332 333 let step_call vargs k m = function353 State_return (v, k, mem', i) 354 355 let step_call vargs k m i = function 334 356 | F_int f -> 335 357 let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in 336 358 let lenv = init_local_env vargs f.f_params f.f_vars in 337 State_regular(f,f.f_body,k,sp,lenv,m) 338 | F_ext f -> interpret_external k m f.ef_tag vargs 359 let i = CostLabel.new_const_ind i in 360 State_regular(f,f.f_body,k,sp,lenv,m,i) 361 | F_ext f -> interpret_external k m i f.ef_tag vargs 339 362 340 363 let step = function 341 | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt 342 | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[]) 343 | State_return(v,Ct_returnto(None,f,sigma,e,k),m) -> 344 (State_regular(f,St_skip,k,sigma,e,m),[]) 345 | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) -> 364 | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt 365 | State_call(fun_def,vargs,k,m,i) -> (step_call vargs k m i fun_def,[]) 366 | State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) -> 367 let i = CostLabel.forget_const_ind i in 368 (State_regular(f,St_skip,k,sigma,e,m,i),[]) 369 | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) -> 346 370 let e = LocalEnv.add x v e in 347 (State_regular(f,St_skip,k,sigma,e,m),[]) 371 let i = CostLabel.forget_const_ind i in 372 (State_regular(f,St_skip,k,sigma,e,m,i),[]) 348 373 | _ -> error "state malformation." 349 374 … … 364 389 if debug then Printf.printf "Result = %s\n%!" 365 390 (IntValue.Int32.to_string res) ; 366 (res, cost_labels) in391 (res, List.rev cost_labels) in 367 392 if debug then print_state state ; 368 393 match state with 369 | State_return(v,Ct_stop,_ ) -> (* Explicit return in main *)394 | State_return(v,Ct_stop,_,_) -> (* Explicit return in main *) 370 395 print_and_return_result (compute_result v) 371 | State_regular(_,St_skip,Ct_stop,_,_,_ ) -> (* Implicit return in main *)396 | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *) 372 397 print_and_return_result IntValue.Int32.zero 373 398 | state -> exec debug cost_labels (step state) … … 379 404 | Some main -> 380 405 let mem = init_mem prog in 381 let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in 406 let main = find_fundef main mem in 407 let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in 382 408 exec debug [] first_state -
Deliverables/D2.2/8051/src/cminor/cminorPrinter.ml
r818 r1542 116 116 (add_parenthesis e3) 117 117 | Cminor.Exp_cost (lab, e) -> 118 let lab = CostLabel.string_of_cost_label lab in 118 119 Printf.sprintf "/* %s */ %s" lab (print_expression e) 119 120 and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with … … 136 137 let print_table n = 137 138 let f s (case, exit) = 138 Printf.sprintf "%s%scase %d: exit %d;\n" s (n_spaces n) case exit139 Printf.sprintf "%s%scase %d: goto %s;\n" s (n_spaces n) case exit 139 140 in 140 141 List.fold_left f "" … … 171 172 (Primitive.print_sig sg) 172 173 | Cminor.St_seq (s1, s2) -> (print_body n s1) ^ (print_body n s2) 174 | Cminor.St_ifthenelse (e, s1, Cminor.St_skip) -> 175 Printf.sprintf "%sif (%s) {\n%s%s}\n" 176 (n_spaces n) 177 (print_expression e) 178 (print_body (n+2) s1) 179 (n_spaces n) 173 180 | Cminor.St_ifthenelse (e, s1, s2) -> 174 181 Printf.sprintf "%sif (%s) {\n%s%s}\n%selse {\n%s%s}\n" … … 180 187 (print_body (n+2) s2) 181 188 (n_spaces n) 182 | Cminor.St_loop s ->189 (* | Cminor.St_loop s -> 183 190 Printf.sprintf "%sloop {\n%s%s}\n" 184 191 (n_spaces n) … … 191 198 (n_spaces n) 192 199 | Cminor.St_exit i -> 193 Printf.sprintf "%sexit %d;\n" (n_spaces n) i 200 Printf.sprintf "%sexit %d;\n" (n_spaces n) i *) 194 201 | Cminor.St_switch (e, tbl, dflt) -> 195 Printf.sprintf "%sswitch (%s) {\n%s%sdefault: exit %d;\n%s}\n"202 Printf.sprintf "%sswitch (%s) {\n%s%sdefault: goto %s;\n%s}\n" 196 203 (n_spaces n) 197 204 (print_expression e) … … 208 215 Printf.sprintf "%sgoto %s;\n" (n_spaces n) lbl 209 216 | Cminor.St_cost (lbl, s) -> 210 Printf.sprintf "%s%s:\n%s" 211 (n_spaces n) lbl (print_body n s) 217 let lbl = CostLabel.string_of_cost_label lbl in 218 Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s) 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) 212 223 213 224 let print_internal f_name f_def = … … 246 257 | Cminor.St_seq(_,_) -> "seq" 247 258 | Cminor.St_ifthenelse(_,_,_) -> "ifthenelse" 248 | Cminor.St_loop(_) -> "loop"259 (* | Cminor.St_loop(_) -> "loop" 249 260 | Cminor.St_block(_) -> "block" 250 | Cminor.St_exit(_) -> "exit" 261 | Cminor.St_exit(_) -> "exit" *) 251 262 | Cminor.St_switch(_,_,_) -> "switch" 252 263 | Cminor.St_return(_) -> "return" … … 254 265 | Cminor.St_goto(_) -> "goto" 255 266 | Cminor.St_cost(_,_) -> "cost" 267 | Cminor.St_ind_0 _ -> "index" 268 | Cminor.St_ind_inc _ -> "increment" -
Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml
r818 r1542 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 let stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in 196 let r1_arg = RTLabs.Reg r1 in 197 let r2_arg = RTLabs.Reg r2 in 198 let stmt = RTLabs.St_op2 (op2, destr, r1_arg, r2_arg, old_entry) in 197 199 let rtlabs_fun = generate rtlabs_fun stmt in 198 200 translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2] … … 201 203 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in 202 204 let old_entry = rtlabs_fun.RTLabs.f_entry in 203 let stmt = RTLabs.St_load (chunk, r, destr, old_entry) in 205 let stmt = 206 RTLabs.St_load (chunk, RTLabs.Reg r, destr, old_entry) in 204 207 let rtlabs_fun = generate rtlabs_fun stmt in 205 208 translate_expr rtlabs_fun lenv r e … … 269 272 (rtlabs_fun : RTLabs.internal_function) 270 273 (lenv : local_env) 271 (exits : Label.t list)274 (* (exits : Label.t list) *) 272 275 (stmt : Cminor.statement) 273 276 : RTLabs.internal_function = … … 283 286 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in 284 287 let old_entry = rtlabs_fun.RTLabs.f_entry in 285 let stmt = RTLabs.St_store (chunk, addr, r, old_entry) in 288 let stmt = 289 RTLabs.St_store (chunk, RTLabs.Reg addr, RTLabs.Reg r, old_entry) in 286 290 let rtlabs_fun = generate rtlabs_fun stmt in 287 291 translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2] … … 321 325 322 326 | Cminor.St_seq (s1, s2) -> 323 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss2 in324 translate_stmt rtlabs_fun lenv exitss1327 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in 328 translate_stmt rtlabs_fun lenv (*exits*) s1 325 329 326 330 | Cminor.St_ifthenelse (e, s1, s2) -> 327 331 let old_entry = rtlabs_fun.RTLabs.f_entry in 328 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss2 in332 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in 329 333 let lbl_false = rtlabs_fun.RTLabs.f_entry in 330 334 let rtlabs_fun = change_entry rtlabs_fun old_entry in 331 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss1 in335 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s1 in 332 336 let lbl_true = rtlabs_fun.RTLabs.f_entry in 333 337 translate_branch rtlabs_fun lenv e lbl_true lbl_false 334 338 335 | Cminor.St_loop s ->339 (* | Cminor.St_loop s -> 336 340 let loop_start = fresh_label rtlabs_fun in 337 341 let rtlabs_fun = change_entry rtlabs_fun loop_start in … … 345 349 346 350 | Cminor.St_exit n -> 347 change_entry rtlabs_fun (List.nth exits n) 351 change_entry rtlabs_fun (List.nth exits n) *) 348 352 349 353 | Cminor.St_return eopt -> … … 362 366 363 367 | Cminor.St_label (lbl, s) -> 364 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss in368 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in 365 369 let old_entry = rtlabs_fun.RTLabs.f_entry in 366 370 add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry) 367 371 368 372 | Cminor.St_cost (lbl, s) -> 369 let rtlabs_fun = translate_stmt rtlabs_fun lenv exitss in373 let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in 370 374 let old_entry = rtlabs_fun.RTLabs.f_entry in 371 375 generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) 376 377 | Cminor.St_ind_0 (i, s) -> 378 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in 379 let old_entry = rtlabs_fun.RTLabs.f_entry in 380 generate rtlabs_fun (RTLabs.St_ind_0 (i, old_entry)) 381 382 | Cminor.St_ind_inc (i, s) -> 383 let rtlabs_fun = translate_stmt rtlabs_fun lenv s in 384 let old_entry = rtlabs_fun.RTLabs.f_entry in 385 generate rtlabs_fun (RTLabs.St_ind_inc (i, old_entry)) 372 386 373 387 | Cminor.St_goto lbl -> … … 446 460 447 461 (* Complete the graph *) 448 translate_stmt rtlabs_fun lenv []f_def.Cminor.f_body462 translate_stmt rtlabs_fun lenv (*[]*) f_def.Cminor.f_body 449 463 450 464 -
Deliverables/D2.2/8051/src/common/costLabel.ml
r486 r1542 1 module Atom = 2 struct 3 include StringTools 4 end 1 5 2 include StringTools 6 module StringMap = Map.Make(String) 7 8 (** Simple expressions are for now affine maps of the form a*_+b *) 9 type sexpr = 10 | Sexpr of int*int 11 12 let is_const_sexpr (Sexpr(a, _)) = (a = 0) 13 14 let sexpr_id = Sexpr(1, 0) 15 16 let const_sexpr n = Sexpr(0, n) 17 18 type index = int 19 20 let make_id prefix depth = prefix ^ string_of_int depth 21 22 type indexing = sexpr list 23 24 type const_indexing = int ExtArray.t 25 26 let const_ind_iter = ExtArray.iter 27 28 let curr_const_ind = function 29 | hd :: _ -> hd 30 | _ -> invalid_arg "curr_const_ind applied to non-empty list" 31 32 let init_const_indexing () = ExtArray.make ~buff:1 0 0 33 34 let enter_loop_single indexing n = ExtArray.set indexing n 0 35 36 let continue_loop_single indexing n = 37 try 38 ExtArray.set indexing n (ExtArray.get indexing n + 1) 39 with | _ -> 40 invalid_arg "uninitialized loop index" 41 42 let curr_ind = function 43 | hd :: _ -> hd 44 | _ -> invalid_arg "non-empty indexing stack" 45 46 let enter_loop inds = enter_loop_single (curr_ind inds) 47 48 let continue_loop inds = continue_loop_single (curr_ind inds) 49 50 let enter_loop_opt indexing = Option.iter (enter_loop indexing) 51 52 let continue_loop_opt indexing = Option.iter (continue_loop indexing) 53 54 let new_const_ind inds = init_const_indexing () :: inds 55 56 let forget_const_ind = function 57 | _ :: inds -> inds 58 | _ -> invalid_arg "non-empty indexing stack" 59 60 let sexpr_of i l = 61 try 62 List.nth l i 63 with 64 | Failure _ 65 | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of" 66 67 let empty_indexing = [] 68 69 let add_id_indexing ind = sexpr_id :: ind 70 71 (* a*_+b is composed with c*_+d by substitution: *) 72 (* namely a*_+b ° c*_+d = c*(a*_+b)+d *) 73 let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) = 74 Sexpr (a * c, b * c + d) 75 76 let ev_sexpr i (Sexpr(a, b)) = a*i+b 77 78 (* i|-->e ° I *) 79 let rec compose_index_indexing i s l = match i, l with 80 | 0, s' :: l' -> compose_sexpr s s' :: l' 81 | x, s' :: l' -> s' :: compose_index_indexing (i-1) s l' 82 | _ -> l 83 84 85 (* I°J applies every mapping in I to every mapping in J *) 86 let rec compose_indexing m n = match m, n with 87 | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2 88 | _ -> n 89 90 let rec compose_const_indexing_i i c = function 91 | [] -> [] 92 | s :: l -> 93 let head = 94 (* if s is constant leave it be. In particular, avoid raising the error *) 95 if is_const_sexpr s then s else 96 try 97 const_sexpr (ev_sexpr (ExtArray.get c i) s) 98 with 99 | Invalid_argument _ -> 100 invalid_arg "constant indexing not enough to be applied" in 101 head :: compose_const_indexing_i (i+1) c l 102 103 module IndexingSet = Set.Make(struct 104 type t = indexing 105 let compare = compare 106 end) 107 108 type t = { 109 name : Atom.t; 110 i : indexing 111 } 112 113 let comp_index i s lbl = 114 {lbl with i = compose_index_indexing i s lbl.i} 115 116 let ev_indexing c lbl = 117 {lbl with i = compose_const_indexing_i 0 c lbl.i} 118 119 120 (* if [pretty] is false then a name suitable for labels is given*) 121 (* ('P' replaces '+') *) 122 let string_of_sexpr pretty prefix i (Sexpr(a, b)) = 123 let plus = if pretty then "+" else "P" in 124 let id = prefix ^ string_of_int i in 125 let a_id_s = if a = 1 then id else string_of_int a ^ id in 126 let b_s = string_of_int b in 127 if a = 0 then b_s else 128 if b = 0 then a_id_s else a_id_s ^ plus ^ b_s 129 130 (* examples:*) 131 (* [pretty] true: (0,i1+1,2i2+2)*) 132 (* [pretty] false: _0_i1P1_2i2P2 *) 133 let rec string_of_indexing_tl pretty prefix i = function 134 | [] -> if pretty then ")" else "" 135 | hd :: tl -> 136 let sep = if pretty then "," else "_" in 137 let str = string_of_sexpr pretty prefix i hd in 138 sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl 139 140 let string_of_indexing pretty prefix = function 141 | [] -> "" 142 | hd :: tl -> 143 let start = if pretty then "(" else "_" in 144 let str = string_of_sexpr pretty prefix 0 hd in 145 start ^ str ^ string_of_indexing_tl pretty prefix 1 tl 146 147 let string_of_cost_label ?(pretty = false) lab = 148 lab.name ^ string_of_indexing pretty "i" lab.i 149 150 let fresh l universe = 151 {name = Atom.Gen.fresh universe; i = l} 152 153 (* TODO: urgh. Necessary? *) 154 type aux_t = t 155 156 (** labels are endowed with a lexicographical ordering *) 157 module T : Map.OrderedType with type t = aux_t = 158 struct 159 type t = aux_t 160 let compare = compare (* uses the built-in lexicographical comparison *) 161 end 162 163 module Map = Map.Make(T) 164 module Set = Set.Make(T) 165 (** [constant_map d x] produces a finite map which associates 166 [x] to every element of the set [d]. *) 167 168 let indexings_of atom s = 169 let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in 170 Set.fold f s IndexingSet.empty 3 171 4 172 let constant_map d x = -
Deliverables/D2.2/8051/src/common/costLabel.mli
r486 r1542 1 1 2 (** This module provides functions to manipulate and create freshcost2 (** This module provides functions to manipulate and create indexed cost 3 3 labels. *) 4 4 5 include StringSig.S 5 (** [Atom] provides functions for cost atoms, the root of indexed costs *) 6 module Atom : sig 7 include StringSig.S 8 end 9 10 (** Simple expressions corresponding to loop tranformations. 11 TODO: abstract or not? *) 12 type sexpr = Sexpr of int*int 13 14 (** The identity simple expression, used in initialization. *) 15 val sexpr_id : sexpr 16 17 (** Indexes are identified with (single-entry) loop depths. *) 18 type index = int 19 20 (** [make_id prefix index] produces an identifier out of a 21 prefix and a loop depth. *) 22 val make_id : string -> index -> string 23 24 type indexing = sexpr list 25 26 (** The type of constant indexings, to be used by interpreations *) 27 type const_indexing 28 29 (** [const_ind_iter f c] iterates [f] over the values of indexes in c *) 30 val const_ind_iter : (int -> unit) -> const_indexing -> unit 31 32 (** This is equivalent to [List.hd], but raises 33 [Invalid_argument "non-empty indexing stack"] if argument is empty *) 34 val curr_const_ind : const_indexing list -> const_indexing 35 36 (** [enter_loop inds n] is used to update the indexing stack [ind] when one 37 is entering a loop indexed by [n]. Raises [Invalid_argument 38 "non-empty indexing stack"] if [inds] is empty. *) 39 val enter_loop : const_indexing list -> index -> unit 40 41 (** [enter_loop_opt inds (Some n)] behaves like [enter_loop inds n], and does 42 nothing in case of [None]. 43 @see enter_loop *) 44 val enter_loop_opt : const_indexing list -> index option -> unit 45 46 (** [continue_loop inds n] is used to update the indexing stack [inds] when 47 one is continuing a loop indexed by [n]. 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]. *) 51 val continue_loop : const_indexing list -> index -> unit 52 53 (** [continue_loop_opt inds (Some n)] behaves like [continue_loop inds n], and 54 does nothing in case of [None]. 55 @see continue_loop *) 56 val continue_loop_opt : const_indexing list -> index option -> unit 57 58 (** [new_const_ind inds] pushes a new empty constant indexing on top of the 59 stack [inds]. *) 60 val new_const_ind : const_indexing list -> const_indexing list 61 62 (** [forget_const_ind inds] pops and discards the top constant indexing from the 63 stack [inds]. Raises [Invalid_argument "non-empty indexing stack"] if 64 [inds] is empty. *) 65 val forget_const_ind : const_indexing list -> const_indexing list 66 67 (** [empty_indexing] is the empty indexing *) 68 val empty_indexing : indexing 69 70 (** [add_id_indexing ind] adds an identity mapping in front of ind **) 71 val add_id_indexing : indexing -> indexing 72 73 module IndexingSet : Set.S with type elt = indexing 74 75 type t = { 76 name : Atom.t; 77 i : indexing 78 } 79 80 (** [comp_index i s lbl] gives back the label [lbl] where index [i] is remapped 81 to the simple expression [s]. *) 82 val comp_index : index -> sexpr -> t -> t 83 84 (** [ev_indexing ind lbl] returns [lbl] where its indexing has been 85 evaluated in the constant indexing [ind]. 86 @raise Invalid_argument "constant indexing not enough to be applied" if 87 [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *) 88 val ev_indexing : const_indexing -> t -> t 89 90 (** [string_of_cost_label pref t] converts an indexed label to a 91 string suitable for a label name in C source. 92 [string_of_cost_label ~pretty:true t] prints a more readable form *) 93 val string_of_cost_label : ?pretty : bool -> t -> string 94 95 (** [fresh i u] creates a fresh label using [u] as name universe, inside 96 the indexing [i] (which represents the nested loops containing the label) *) 97 val fresh : indexing -> Atom.Gen.universe -> t 98 99 module Set : Set.S with type elt = t 100 module Map : Map.S with type key = t 101 102 (** [indexings_of a s] produces the set of indexings of an atom [a] occurring 103 in the set of indexed labels [s]. *) 104 val indexings_of : Atom.t -> Set.t -> IndexingSet.t 6 105 7 106 (** [constant_map d x] produces a finite map which associates -
Deliverables/D2.2/8051/src/common/label.ml
r486 r1542 1 1 2 2 include StringTools 3 4 module ImpMap = struct 5 6 type key = 7 Map.key 8 9 type 'data t = 10 'data Map.t ref 11 12 let create () = 13 ref Map.empty 14 15 let clear t = 16 t := Map.empty 17 18 let add k d t = 19 t := Map.add k d !t 20 21 let find k t = 22 Map.find k !t 23 24 let iter f t = 25 Map.iter f !t 26 27 end -
Deliverables/D2.2/8051/src/common/label.mli
r486 r1542 4 4 5 5 include StringSig.S 6 7 (** Imperative label maps for use with Fix *) 8 module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t) -
Deliverables/D2.2/8051/src/languages.ml
r1462 r1542 35 35 | AstLIN of LIN.program 36 36 | AstASM of ASM.program 37 38 type transformation = name * (ast -> ast) 37 39 38 40 let language_of_ast = function … … 136 138 ] 137 139 138 let compile debug src tgt = 139 (* Find the maximal suffix of the chain that starts with the 140 language [src]. *) 141 let rec subchain = function 142 | [] -> 143 (* The chain is assumed to be well-formed: such a suffix 144 exists. *) 145 assert false 146 | ((l, _, _) :: _) as chain when l = src -> chain 147 | _ :: chain -> subchain chain 148 in 140 let insert_transformations ts chain = 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) 149 150 let compile debug ts src tgt = 151 (* insert intermediate transformations *) 152 let chain = insert_transformations ts compilation_chain in 153 (* erase transformations whose source is strictly before src *) 154 let chain = List.filter (function (l1, _, _) -> l1 >= src) chain in 155 (* erase transformations whose target is strictly after tgt *) 156 let chain = List.filter (function (_, l2, _) -> l2 <= tgt) chain in 149 157 (* Compose the atomic translations to build a compilation function 150 158 from [src] to [tgt]. Again, we assume that the compilation chain … … 153 161 translation from [src] to [tgt]. *) 154 162 let rec compose iprogs src tgt chains ast = 155 if src = tgt then List.rev (ast :: iprogs) 156 else 157 match chains with 158 | [] -> 163 match chains with 164 | [] when src = tgt -> List.rev (ast :: iprogs) 165 | [] -> 159 166 Error.global_error "During compilation configuration" 160 167 (Printf.sprintf "It is not possible to compile from `%s' to `%s'." … … 168 175 ast :: l2_to_tgt iprog 169 176 in 170 compose [] src tgt (subchain compilation_chain)177 compose [] src tgt chain 171 178 172 179 … … 210 217 211 218 (* FIXME *) 212 let instrument cost s_mapping = function219 let instrument cost_tern costs_mapping = function 213 220 | AstClight p -> 214 221 let (p', cost_id, cost_incr, extern_cost_variables) = 215 ClightAnnotator.instrument p costs_mapping in222 ClightAnnotator.instrument cost_tern p costs_mapping in 216 223 (AstClight p', cost_id, cost_incr, extern_cost_variables) 217 224 (* … … 227 234 (p, "", "", StringTools.Map.empty) 228 235 229 let annotate input_ast final =236 let annotate cost_tern input_ast final = 230 237 let costs_mapping = compute_costs final in 231 instrument cost s_mapping input_ast238 instrument cost_tern costs_mapping input_ast 232 239 233 240 let string_output asm_pretty = function -
Deliverables/D2.2/8051/src/languages.mli
r1488 r1542 30 30 | AstASM of ASM.program 31 31 32 33 (** The type of additional transfromations, with the language they take place 34 in and the actual transformation *) 35 type transformation = name * (ast -> ast) 36 32 37 (** [language_of_ast ast] returns the programming language of the 33 38 abstract syntax tree [ast]. *) … … 41 46 (** {2 Compilation} *) 42 47 43 (** [compile debug l1 l2] returns the compilation function that 44 translates the language [l1] to the language [l2]. This may be the 48 (** [compile debug ts l1 l2] returns the compilation function that 49 translates the language [l1] to the language [l2], employing the 50 transformations in [ts] along the way . This may be the 45 51 composition of several compilation functions. If [debug] is 46 52 [true], all the intermediate programs are inserted in the 47 53 output. *) 48 val compile : bool -> name -> name -> (ast -> ast list)54 val compile : bool -> transformation list -> name -> name -> (ast -> ast list) 49 55 50 56 (** [add_runtime ast] adds runtime functions for the operations not supported by … … 66 72 val labelize : ast -> ast 67 73 68 (** [annotate input_ast target_ast] inserts cost annotations into the input AST 69 from the (final) target AST. It also returns the name of the cost variable, 70 the name of the cost increment function, and a the name of a fresh 71 uninitialized global variable for each external function. *) 72 val annotate : ast -> ast -> (ast * string * string * string StringTools.Map.t) 74 (** [annotate cost_tern input_ast target_ast] inserts cost annotations into the 75 input AST from the (final) target AST. It also returns the name of the cost 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 78 rules whether cost increments are given by ternary expressions or branch 79 statements. *) 80 val annotate : bool -> ast -> ast -> (ast * string * string * string StringTools.Map.t) 73 81 74 82 (** [interpret debug ast] runs the program [ast] from the default initial -
Deliverables/D2.2/8051/src/options.ml
r1462 r1542 48 48 let is_debug_enabled () = !debug_flag 49 49 50 let transformations = ref [] 51 let add_transformation t () = transformations := !transformations @ [t] 52 let add_transformations ts () = transformations := !transformations @ ts 53 let get_transformations () = !transformations 54 55 let cost_ternary_flag = ref true 56 let set_cost_ternary = (:=) cost_ternary_flag 57 let is_cost_ternary_enabled () = !cost_ternary_flag 58 50 59 let asm_pretty_flag = ref false 51 60 let set_asm_pretty = (:=) asm_pretty_flag … … 79 88 let set_lustre_test_max_int = (:=) lustre_test_max_int 80 89 let get_lustre_test_max_int () = !lustre_test_max_int 90 81 91 82 92 (* … … 89 99 let set_dev_test = (:=) dev_test 90 100 let is_dev_test_enabled () = !dev_test 101 102 let help_specify_opt_stage (trans : Languages.transformation) = 103 Printf.sprintf "(done at the %s stage)." (Languages.to_string (fst trans)) 104 105 let basic_optimizations = 106 [ 107 LoopPeeling.trans; 108 ConstPropagation.trans; 109 CopyPropagation.trans; 110 RedundancyElimination.trans; 111 CopyPropagation.trans; 112 RedundancyElimination.trans 113 ] 114 91 115 92 116 let options = OptionsParsing.register [ … … 148 172 extra_doc " [default is 1000]"; 149 173 174 "-peel", Arg.Unit (add_transformation LoopPeeling.trans), 175 " Apply loop peeling " ^ 176 help_specify_opt_stage LoopPeeling.trans; 177 178 "-cst-prop", Arg.Unit (add_transformation ConstPropagation.trans), 179 " Apply constant propagation " ^ 180 help_specify_opt_stage ConstPropagation.trans; 181 182 "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans), 183 " Apply copy propagation " ^ 184 help_specify_opt_stage CopyPropagation.trans; 185 186 "-pre", Arg.Unit (add_transformation RedundancyElimination.trans), 187 " Apply partial redundancy elimination " ^ 188 help_specify_opt_stage RedundancyElimination.trans; 189 190 "-unroll-for", 191 Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()), 192 " Apply loop unrolling, specifying factor " ^ 193 help_specify_opt_stage (LoopUnrolling.trans ()); 194 195 "-unroll", Arg.Unit (add_transformation (LoopUnrolling.trans ())), 196 " Apply loop unrolling " ^ 197 help_specify_opt_stage (LoopUnrolling.trans ()); 198 199 "-O", Arg.Unit (add_transformations basic_optimizations), 200 " Apply some optimizations."; 201 202 "-no-cost-tern", Arg.Clear cost_ternary_flag, 203 " Replace cost ternary expressions with equivalent branch statements."; 204 150 205 (* 151 206 "-res", Arg.Set print_result_flag, -
Deliverables/D2.2/8051/src/options.mli
r1462 r1542 32 32 val is_debug_enabled : unit -> bool 33 33 34 (** {2 Cost ternary expressions} *) 35 val is_cost_ternary_enabled : unit -> bool 36 34 37 (** {2 Assembly pretty print} *) 35 38 val set_asm_pretty : bool -> unit … … 64 67 val get_lustre_test_max_int : unit -> int 65 68 69 70 (** {2 Intermediate transformations } *) 71 val get_transformations : unit -> Languages.transformation list 66 72 (* 67 73 (** {2 Print results requests} *)
Note: See TracChangeset
for help on using the changeset viewer.