Changeset 619 for Deliverables/D2.2/8051
- Timestamp:
- Mar 2, 2011, 3:27:41 PM (10 years ago)
- Location:
- Deliverables/D2.2/8051
- Files:
-
- 8 added
- 54 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/README
r530 r619 5 5 the CIL parser[1], Xavier Leroy's translation from C to Clight, and 6 6 an existing back-end compiler for a register transfer language to a 7 subset of the MIPS assembly language[2] or the 8051 microprocessor 8 family. The current version is configured to output 8051 code. 7 subset of the MIPS assembly language[2]. 9 8 10 9 We wrote 3 compiler passes: one from Clight to Cminor, another from 11 10 Cminor to an abstract register transfer language (RTLabs), and a 12 last one from RTLabs to an RTL that uses either MIPS or 8051 instructions.13 Weextended interpreters for the intermediate languages to output a11 last one from RTLabs to an RTL that uses MIPS instructions. We 12 extended interpreters for the intermediate languages to output a 14 13 list of labels which denote key control points of the program that 15 14 have been crossed during the interpretation. These labels are the -
Deliverables/D2.2/8051/distributed_files
r486 r619 854 854 ./src/ASM/printOps.ml 855 855 ./src/ASM/printOps.mli 856 ./src/ASM/Pretty.ml 857 ./src/ASM/Pretty.mli 856 858 ./src/ASM/Util.ml 857 859 ./src/clight -
Deliverables/D2.2/8051/myocamlbuild_config.ml
r486 r619 1 let parser_lib = "/home/ayache/ Work/Source/CerCo/experiments/compiler/branches/8051/lib"1 let parser_lib = "/home/ayache/Downloads/Bol/Deliverables/D2.2/8051/lib" -
Deliverables/D2.2/8051/src/ASM/ASM.mli
r486 r619 113 113 type preamble = (string * int) list 114 114 115 (* has_main currently unused *) 116 type 'a pretty_program = 117 { ppreamble : preamble ; 118 pexit_label : string ; 119 pcode : 'a list ; 120 phas_main : bool } 121 115 122 type program = 116 { preamble : preamble;117 exit_label : Label.t ;118 code : labelled_instruction list;119 has_main : bool }123 { code : BitVectors.byte list ; 124 cost_labels : string BitVectors.WordMap.t ; 125 exit_addr : BitVectors.word ; 126 has_main : bool } -
Deliverables/D2.2/8051/src/ASM/ASMCosts.ml
r486 r619 1 1 2 2 let error_prefix = "ASMCosts" 3 let error s = Error.global_error error_prefix s 4 let warning s = Error.warning error_prefix s 3 let warning s = prerr_endline (error_prefix ^ s) 5 4 6 5 7 6 type instruction_nature = 8 | Cost of CostLabel.t 9 | Goto of Label.t | Branch of Label.t 10 | Direct_fun_call of Label.t | Return 7 | Goto of BitVectors.word | Branch of BitVectors.word 8 | Direct_fun_call of BitVectors.word | Return 11 9 | Other 12 10 13 let inst_nature = function 14 | `Cost lbl -> Cost lbl 15 | `Call lbl -> Direct_fun_call lbl 16 | `Jmp lbl -> Goto lbl 17 | `WithLabel (`JC (`Label lbl)) 18 | `WithLabel (`JNC (`Label lbl)) 19 | `WithLabel (`JB (_, `Label lbl)) 20 | `WithLabel (`JNB (_, `Label lbl)) 21 | `WithLabel (`JBC (_, `Label lbl)) 22 | `WithLabel (`JZ (`Label lbl)) 23 | `WithLabel (`JNZ (`Label lbl)) 24 | `WithLabel (`CJNE (_, `Label lbl)) 25 | `WithLabel (`DJNZ (_, `Label lbl)) -> Branch lbl 11 let inst_nature pc = function 12 | `LCALL (`ADDR16 addr16) -> Direct_fun_call addr16 13 | `ACALL (`ADDR11 addr11) -> 14 Direct_fun_call (Physical.addr16_of_addr11 pc addr11) 15 | `LJMP (`ADDR16 addr16) -> Goto addr16 16 | `AJMP (`ADDR11 addr11) -> Goto (Physical.addr16_of_addr11 pc addr11) 17 | `SJMP (`REL addr) -> 18 let _, addr = BitVectors.half_add pc (BitVectors.sign_extension addr) in 19 Goto addr 20 | `JMP idptr -> Other (* Indirect jump; precondition: every possible 21 destination should start with its own label *) 22 | `JC addr 23 | `JNC addr 24 | `JB (_,addr) 25 | `JNB (_,addr) 26 | `JBC (_,addr) 27 | `JZ addr 28 | `JNZ addr 29 | `CJNE (_,addr) 30 | `DJNZ (_,addr) -> 31 let `REL addr = addr in 32 let _, addr = BitVectors.half_add pc (BitVectors.sign_extension addr) in 33 Branch addr 26 34 | `RET -> Return 27 35 | _ -> Other 28 36 29 37 30 let pc_of_label p = 31 let f pc map = function 32 | `Label lab -> StringTools.Map.add lab pc map 33 | _ -> map 34 in 35 MiscPottier.foldi f StringTools.Map.empty p.ASM.code 36 37 38 let inst_cost = function 39 | `Cost _ | `Label _ -> 0 40 | _ -> 1 41 42 43 let block_cost pc_of_label p = 44 let rec aux pc = 45 if pc >= List.length p.ASM.code then 0 38 (* TODO: do not consider the very first instruction as ending the block since it 39 contains the cost label whose cost we are trying to compute! *) 40 let block_cost mem costs = 41 let rec aux oldpc = 42 if BitVectors.WordMap.mem oldpc costs then 0 46 43 else 47 let inst = List.nth p.ASM.code pc in 48 let cost = match inst_nature inst with 49 | Cost _ | Return -> 0 50 | Goto lbl -> 51 let pc = StringTools.Map.find lbl pc_of_label in 52 aux pc 53 | Branch lbl -> 54 let pc1 = pc + 1 in 55 let pc2 = StringTools.Map.find lbl pc_of_label in 56 let cost1 = aux pc1 in 57 let cost2 = aux pc2 in 58 let cost = max cost1 cost2 in 59 if cost1 <> cost2 then 60 warning 61 (Printf.sprintf 44 let inst,pc,inst_cost = ASMInterpret.fetch mem oldpc in 45 let cost = match inst_nature oldpc inst with 46 | Return -> 0 47 | Goto pc -> aux pc 48 | Branch pc2 -> 49 let pc1 = 50 snd (BitVectors.half_add pc (BitVectors.vect_of_int 1 `Sixteen)) in 51 let cost1 = aux pc1 in 52 let cost2 = aux pc2 in 53 if cost1 <> cost2 then 54 warning 55 (Printf.sprintf 62 56 "Warning: branching to %s has cost %d; continuing has cost %d.\n" 63 lblcost2 cost1) ;64 cost65 | _ -> aux (pc+1) 57 "*fixme*"(*pc2*) cost2 cost1) ; 58 max cost1 cost2 59 | _ -> aux pc 66 60 in 67 cost + inst_cost inst61 cost + inst_cost 68 62 in 69 63 aux 70 64 71 65 72 let rec init_function p pc = 73 let inst = List.nth p.ASM.code pc in 74 match inst_nature inst with 75 | Cost lbl -> (lbl, 0, pc+1) 76 | _ -> 77 let (lbl, cost, pc) = init_function p (pc+1) in 78 (lbl, cost + (inst_cost inst), pc) 66 let traverse_code mem p = 67 let rec aux pc code = 68 let _,newpc,_ = ASMInterpret.fetch mem pc in 69 match code with 70 | [] -> CostLabel.Map.empty 71 | _::tl when BitVectors.WordMap.mem pc p.ASM.cost_labels -> 72 let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in 73 let cost = block_cost mem p.ASM.cost_labels pc in 74 let costs_mapping = aux newpc tl in 75 CostLabel.Map.add lbl cost costs_mapping 76 | _::tl -> aux newpc tl 77 in 78 aux (BitVectors.zero `Sixteen) p.ASM.code 79 79 80 80 81 let traverse_code pc_of_label p = 82 let rec aux pc = 83 if pc >= List.length p.ASM.code then CostLabel.Map.empty 84 else 85 match inst_nature (List.nth p.ASM.code pc) with 86 | Cost lbl -> 87 let cost = block_cost pc_of_label p (pc+1) in 88 let costs_mapping = aux (pc+1) in 89 CostLabel.Map.add lbl cost costs_mapping 90 | _ -> aux (pc+1) 81 let first_cost_label mem costs = 82 let rec aux oldpc = 83 try (BitVectors.WordMap.find oldpc costs, 0) 84 with 85 | Not_found -> 86 let inst,pc,inst_cost = ASMInterpret.fetch mem oldpc in 87 match inst_nature oldpc inst with 88 | Direct_fun_call pc -> 89 let (lbl, cost) = aux pc in 90 (lbl, inst_cost + cost) 91 | Return 92 | Goto _ 93 | Branch _ -> 94 assert false (* no such instructions before calling main *) 95 | Other -> 96 let (lbl, cost) = aux pc in 97 (lbl, inst_cost + cost) 91 98 in 92 aux 099 aux (BitVectors.zero `Sixteen) 93 100 94 101 95 let first_cost_label pc_of_label p = 96 let rec aux pc = 97 if pc >= List.length p.ASM.code then assert false (* should not happen *) 98 else 99 match inst_nature (List.nth p.ASM.code pc) with 100 | Cost lbl -> lbl 101 | Direct_fun_call lbl -> aux (StringTools.Map.find lbl pc_of_label) 102 | _ -> aux (pc+1) 103 in 104 aux 0 105 106 let initialize_cost pc_of_label p costs_mapping = 107 let lbl = first_cost_label pc_of_label p in 102 let initialize_cost mem costs costs_mapping = 103 let (lbl, cost) = first_cost_label mem costs in 108 104 let old_cost = 109 if CostLabel.Map.mem lbl costs_mapping then 110 CostLabel.Map.find lbl costs_mapping 111 else 0 in 112 let init = 1 (* cost of the preamble *) in 113 let new_cost = old_cost + init in 105 assert (CostLabel.Map.mem lbl costs_mapping) ; 106 CostLabel.Map.find lbl costs_mapping in 107 let new_cost = old_cost + cost in 114 108 CostLabel.Map.add lbl new_cost costs_mapping 115 109 116 110 117 111 let compute p = 118 let pc_of_label = pc_of_label pin119 let costs_mapping = traverse_code pc_of_labelp in120 if p.ASM.has_main then initialize_cost pc_of_label pcosts_mapping112 let mem = ASMInterpret.load_code_memory p.ASM.code in 113 let costs_mapping = traverse_code mem p in 114 if p.ASM.has_main then initialize_cost mem p.ASM.cost_labels costs_mapping 121 115 else costs_mapping -
Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml
r486 r619 2 2 open Physical;; 3 3 open ASM;; 4 open ASMPrinter;;5 4 open IntelHex;; 6 5 open Util;; … … 56 55 (* let _ = prerr_endline <*> string_of_line $ line in *) 57 56 (time + 1),debug_continuation) 58 59 module IntMap = Map.Make(struct type t = int let compare = compare end);; 60 type costs = CostLabel.t IntMap.t 61 57 62 58 (* no differentiation between internal and external code memory *) 63 59 type status = 64 60 { 65 61 (* Memory *) 66 code_memory: WordMap.map; (* can be reduced *)62 code_memory: Physical.WordMap.map; (* can be reduced *) 67 63 low_internal_ram: Byte7Map.map; 68 64 high_internal_ram: Byte7Map.map; 69 external_ram: WordMap.map;65 external_ram: Physical.WordMap.map; 70 66 71 67 (* Program counter *) … … 134 130 es_running: bool; 135 131 136 exit_ pc: word option;137 cost s: costs;132 exit_addr : BitVectors.word; 133 cost_labels : string BitVectors.WordMap.t 138 134 } 139 135 … … 225 221 226 222 let initialize = { 227 code_memory = WordMap.empty;223 code_memory = Physical.WordMap.empty; 228 224 low_internal_ram = Byte7Map.empty; 229 225 high_internal_ram = Byte7Map.empty; 230 external_ram = WordMap.empty;226 external_ram = Physical.WordMap.empty; 231 227 232 228 pc = zero `Sixteen; … … 287 283 es_running = false; 288 284 289 costs = IntMap.empty;290 exit_pc = None;285 exit_addr = BitVectors.zero `Sixteen; 286 cost_labels = BitVectors.WordMap.empty 291 287 } 292 288 … … 387 383 let next pc = 388 384 let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in 389 res, WordMap.find pc pmem385 res, Physical.WordMap.find pc pmem 390 386 in 391 387 let pc,instr = next pc in … … 693 689 let pc,b2 = next pc in 694 690 `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2 695 | _,_ -> assert false 691 | (true,false,true,false),(false,true,false,true) -> 692 (* undefined opcode *) assert false 696 693 ;; 697 694 … … 927 924 ;; 928 925 929 let fold_lefti f = 930 let rec aux i acc = 931 function 932 [] -> acc 933 | he::tl -> aux (i+1) (f i acc he) tl 934 in 935 aux 0 936 ;; 937 938 let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty 939 940 let load_mem mem exit_pc costs status = 941 { status with code_memory = mem ; 942 exit_pc = exit_pc ; 943 costs = costs } 944 let load l exit_pc costs = load_mem (load_code_memory l) exit_pc costs 945 946 module StringMap = Map.Make(String);; 947 926 let load_code_memory = MiscPottier.foldi (fun i mem v -> Physical.WordMap.add (vect_of_int i `Sixteen) v mem) Physical.WordMap.empty 927 928 let load_mem mem status = { status with code_memory = mem } 929 let load l = load_mem (load_code_memory l) 948 930 949 931 let assembly_jump addr_of = … … 965 947 (fun (datalabels,addr) (name,size) -> 966 948 let addr16 = vect_of_int addr `Sixteen in 967 String Map.add name addr16 datalabels, addr+size968 ) (String Map.empty,0) p.ASM.preamble949 StringTools.Map.add name addr16 datalabels, addr+size 950 ) (StringTools.Map.empty,0) p.ASM.ppreamble 969 951 in 970 let pc, labels,costs =952 let pc,exit_addr,labels,costs = 971 953 List.fold_left 972 (fun (pc, labels,costs) i ->954 (fun (pc,exit_addr,labels,costs) i -> 973 955 match i with 974 `Label s -> pc, StringMap.add s pc labels, costs 975 | `Cost s -> pc, labels, IntMap.add pc s costs 976 | `Mov (_,_) -> pc, labels, costs 956 `Label s when s = p.ASM.pexit_label -> 957 pc, pc, StringTools.Map.add s pc labels, costs 958 | `Label s -> 959 pc, exit_addr, StringTools.Map.add s pc labels, costs 960 | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs 961 | `Mov (_,_) -> pc, exit_addr, labels, costs 977 962 | `Jmp _ 978 | `Call _ -> pc + 3, labels, costs (*CSC: very stupid: always expand to worst opcode *) 963 | `Call _ -> 964 (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), 965 exit_addr, labels, costs 966 (*CSC: very stupid: always expand to worst opcode *) 979 967 | `WithLabel i -> 980 981 982 983 984 (pc + int_of_vect pc',labels, costs)968 let fake_addr _ = `REL (zero `Eight) in 969 let fake_jump = assembly_jump fake_addr i in 970 let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in 971 assert (fake_jump = i'); 972 (snd (half_add pc pc'), exit_addr, labels, costs) 985 973 | #instruction as i -> 986 974 let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in 987 975 assert (i = i'); 988 (pc + int_of_vect pc',labels, costs) 989 ) (0,StringMap.empty,IntMap.empty) p.ASM.code 976 (snd (half_add pc pc'),exit_addr,labels, costs) 977 ) 978 (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen, 979 StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode 990 980 in 991 if pc >= 65536 then 992 raise CodeTooLarge 993 else 994 List.flatten (List.map 995 (function 996 `Label _ 997 | `Cost _ -> [] 998 | `WithLabel i -> 999 let addr_of (`Label s) = 1000 let addr = StringMap.find s labels in 1001 (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *) 1002 assert (addr < 256); 1003 `REL (vect_of_int addr `Eight) 1004 in 1005 assembly1 (assembly_jump addr_of i) 1006 | `Mov (`DPTR,s) -> 1007 let addrr16 = StringMap.find s datalabels in 1008 assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16))) 1009 | `Jmp s -> 1010 let pc_offset = StringMap.find s labels in 1011 assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen))) 1012 | `Call s -> 1013 let pc_offset = StringMap.find s labels in 1014 assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen))) 1015 | #instruction as i -> assembly1 i) p.ASM.code), 1016 vect_of_int (StringMap.find p.ASM.exit_label labels) `Sixteen, 1017 costs 981 let code = 982 List.flatten (List.map 983 (function 984 `Label _ 985 | `Cost _ -> [] 986 | `WithLabel i -> 987 let addr_of (`Label s) = 988 let addr = StringTools.Map.find s labels in 989 (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *) 990 `REL (assert false) (*addr*) 991 in 992 assembly1 (assembly_jump addr_of i) 993 | `Mov (`DPTR,s) -> 994 let addrr16 = StringTools.Map.find s datalabels in 995 assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16))) 996 | `Jmp s -> 997 let pc_offset = StringTools.Map.find s labels in 998 assembly1 (`LJMP (`ADDR16 pc_offset)) 999 | `Call s -> 1000 let pc_offset = StringTools.Map.find s labels in 1001 assembly1 (`LCALL (`ADDR16 pc_offset )) 1002 | #instruction as i -> assembly1 i) p.ASM.pcode) in 1003 { ASM.code = code ; ASM.cost_labels = costs ; 1004 ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main } 1018 1005 ;; 1019 1006 … … 1048 1035 assert false for now. Try to understand what DEC really does *) 1049 1036 let cry,addr = half_add dpr (mk_word (vect_of_int 0 `Eight) status.acc) in 1050 WordMap.find addr status.external_ram1037 Physical.WordMap.find addr status.external_ram 1051 1038 | `A_PC -> 1052 1039 (* CSC: what is the right behaviour in case of overflow? 1053 1040 assert false for now *) 1054 1041 let cry,addr = half_add status.pc (mk_word (vect_of_int 0 `Eight) status.acc) in 1055 WordMap.find addr status.external_ram1042 Physical.WordMap.find addr status.external_ram 1056 1043 | `EXT_INDIRECT b -> 1057 1044 let addr = get_register status (false,false,b) in 1058 WordMap.find (mk_word (zero `Eight) addr) status.external_ram1045 Physical.WordMap.find (mk_word (zero `Eight) addr) status.external_ram 1059 1046 | `EXT_IND_DPTR -> 1060 1047 let dpr = mk_word status.dph status.dpl in 1061 WordMap.find dpr status.external_ram1048 Physical.WordMap.find dpr status.external_ram 1062 1049 ;; 1063 1050 … … 1131 1118 let dpr = mk_word status.dph status.dpl in 1132 1119 { status with external_ram = 1133 WordMap.add dpr v status.external_ram }1120 Physical.WordMap.add dpr v status.external_ram } 1134 1121 | `EXT_INDIRECT b -> 1135 1122 let addr = get_register status (false,false,b) in 1136 1123 { status with external_ram = 1137 WordMap.add (mk_word (zero `Eight) addr) v status.external_ram }1124 Physical.WordMap.add (mk_word (zero `Eight) addr) v status.external_ram } 1138 1125 ;; 1139 1126 … … 1741 1728 let dptr = mk_word status.dph status.dpl in 1742 1729 let cry, addr = half_add dptr big_acc in 1743 let lookup = WordMap.find addr status.code_memory in1730 let lookup = Physical.WordMap.find addr status.code_memory in 1744 1731 { status with acc = lookup } 1745 1732 | `MOVC (`A, `A_PC) -> … … 1750 1737 let status = { status with pc = inc_pc } in 1751 1738 let cry,addr = half_add inc_pc big_acc in 1752 let lookup = WordMap.find addr status.code_memory in1739 let lookup = Physical.WordMap.find addr status.code_memory in 1753 1740 { status with acc = lookup } 1754 1741 (* data transfer *) … … 1813 1800 status 1814 1801 | `RET -> 1815 let high_bits = read_at_sp status in1816 let new_sp,cy,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in1817 let status = { status with sp = new_sp } in1818 let low_bits = read_at_sp status in1819 let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) cy in1820 let status = { status with sp = new_sp } in1821 { status with pc = mk_word high_bits low_bits }1822 (*1823 1802 (* DPM: What happens when we underflow? *) 1824 1803 let high_bits = read_at_sp status in … … 1829 1808 let status = { status with sp = new_sp } in 1830 1809 { status with pc = mk_word high_bits low_bits } 1831 *)1832 1810 | `RETI -> 1833 1811 let high_bits = read_at_sp status in … … 1846 1824 let status = { status with sp = new_sp } in 1847 1825 let status = write_at_sp status pc_upper_byte in 1848 let n1, n2 = from_byte pc_upper_byte in 1849 let (b1,b2,b3,_) = from_word11 a in 1850 let (p1,p2,p3,p4),(p5,_,_,_) = from_nibble n1, from_nibble n2 in 1851 let addr = mk_word (mk_byte (mk_nibble p1 p2 p3 p4) (mk_nibble p5 b1 b2 b3)) pc_lower_byte in 1826 let addr = addr16_of_addr11 status.pc a in 1852 1827 { status with pc = addr } 1853 1828 | `LCALL (`ADDR16 addr) -> … … 1861 1836 { status with pc = addr } 1862 1837 | `AJMP (`ADDR11 a) -> 1863 let pc_upper_byte, pc_lower_byte = from_word status.pc in 1864 let n1, n2 = from_byte pc_upper_byte in 1865 let (p1,p2,p3,p4),(p5,_,_,_) = from_nibble n1, from_nibble n2 in 1866 let (b1,b2,b3,b) = from_word11 a in 1867 let addr = mk_word (mk_byte (mk_nibble p1 p2 p3 p4) (mk_nibble p5 b1 b2 b3)) b in 1868 let cry, new_pc = half_add status.pc addr in 1869 { status with pc = new_pc } 1838 let addr = addr16_of_addr11 status.pc a in 1839 { status with pc = addr } 1870 1840 | `LJMP (`ADDR16 a) -> 1871 1841 { status with pc = a } … … 1954 1924 ;; 1955 1925 1956 let eq_pc pc1 pc2 = 1957 let to_int = BitVectors.int_of_vect in 1958 to_int pc1 = to_int pc2 1959 1960 let end_of_program st = match st.exit_pc with 1961 | None -> false 1962 | Some exit_pc -> eq_pc st.pc exit_pc 1963 1964 let print_result st = 1965 Printf.printf "Result : DPL = %d DPH = %d\n%!" 1966 (BitVectors.int_of_vect st.dpl) (BitVectors.int_of_vect st.dph) 1967 1968 let print_instr instr = 1969 Printf.printf "%s\n%!" (ASMPrinter.pp_instruction instr) 1926 1927 let load_program p = 1928 let st = load p.ASM.code initialize in 1929 { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels } 1970 1930 1971 1931 let observe_trace trace_ref st = 1972 let pc = st.pc in1973 let (instr, _, _) = fetch st.code_memory pc in1974 let ipc = BitVectors.int_of_vect pc in1975 (* <DEBUG> *)1976 print_result st ;1977 Printf.printf "%d: %!" ipc ;1978 print_instr instr ;1979 (* </DEBUG> *)1980 1932 let cost_label = 1981 if IntMap.mem ipc st.costs then [IntMap.find ipc st.costs] 1933 if BitVectors.WordMap.mem st.pc st.cost_labels then 1934 [BitVectors.WordMap.find st.pc st.cost_labels] 1982 1935 else [] in 1983 1936 trace_ref := cost_label @ !trace_ref ; 1984 if end_of_program st then raise Halt else st 1985 1986 let interpret p = 1937 if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st 1938 1939 let result st = 1940 let i = BitVectors.int_of_vect st.dpl in 1941 IntValue.Int8.of_int i 1942 1943 let interpret print_result p = 1987 1944 if p.ASM.has_main then 1988 let (insts, exit_pc, costs) = assembly p in 1989 let st = load insts (Some exit_pc) costs initialize in 1945 let st = load_program p in 1990 1946 let trace = ref [] in 1991 1947 let callback = observe_trace trace in 1992 1948 let st = execute callback st in 1993 (* <DEBUG> *) 1994 print_result st ; 1995 (* </DEBUG> *) 1996 List.rev !trace 1997 else [] 1998 1999 let parse_and_interpret_hex file = 2000 let intel_hex = IntelHex.intel_hex_of_file file in 2001 let physical = IntelHex.process_intel_hex intel_hex in 2002 let st = load_mem physical None IntMap.empty initialize in 2003 let callback = observe_trace (ref []) in 2004 ignore (execute callback st) 1949 let res = result st in 1950 if print_result then 1951 Printf.printf "8051: %s\n%!" (IntValue.Int8.to_string res) ; 1952 (res, List.rev !trace) 1953 else (IntValue.Int8.zero, []) -
Deliverables/D2.2/8051/src/ASM/ASMInterpret.mli
r486 r619 3 3 4 4 exception CodeTooLarge 5 5 6 6 type time = int;; 7 7 type line = [ `P1 of byte … … 18 18 (* In: reception time, line of input, new continuation, 19 19 Out: transmission time, output line, expected duration until reply, 20 20 new continuation. 21 21 *) 22 22 type continuation = 23 23 [`In of time * line * epsilon * continuation] option * 24 [`Out of (time -> line -> time * continuation) ];; 25 26 module IntMap: Map.S with type key = int 27 type costs = CostLabel.t IntMap.t 24 [`Out of (time -> line -> time * continuation) ];; 28 25 29 26 type status = 30 { 31 (* Memory *) 32 code_memory: WordMap.map; (* can be reduced *) 33 low_internal_ram: Byte7Map.map; 34 high_internal_ram: Byte7Map.map; 35 external_ram: WordMap.map; 27 { 28 (* Memory *) 29 code_memory: WordMap.map; (* can be reduced *) 30 low_internal_ram: Byte7Map.map; 31 high_internal_ram: Byte7Map.map; 32 external_ram: WordMap.map; 33 34 (* Program counter *) 35 pc: word; 36 37 (* SFRs *) 38 sp: byte; 39 dpl: byte; 40 dph: byte; 41 pcon: byte; 42 tcon: byte; 43 tmod: byte; 44 tl0: byte; 45 tl1: byte; 46 th0: byte; 47 th1: byte; 48 p1: byte; 49 scon: byte; 50 sbuf: byte; 51 ie: byte; 52 p3: byte; 53 ip: byte; 54 psw: byte; 55 acc: byte; 56 b: byte; 57 t2con: byte; (* 8052 only *) 58 rcap2l: byte; (* 8052 only *) 59 rcap2h: byte; (* 8052 only *) 60 tl2: byte; (* 8052 only *) 61 th2: byte; (* 8052 only *) 62 63 (* Latches for the output lines *) 64 p1_latch: byte; 65 p3_latch: byte; 66 67 (* Fields for tracking the state of the processor. *) 68 69 (* IO specific *) 70 previous_p1_val: bool; 71 previous_p3_val: bool; 72 73 serial_epsilon_out: epsilon option; 74 serial_epsilon_in: epsilon option; 75 76 io_epsilon: epsilon; 77 78 serial_v_in: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option; 79 serial_v_out: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option; 80 81 serial_k_out: continuation option; 82 83 io: continuation; 84 expected_out_time: [ `None | `Now | `At of time ]; 85 86 (* Timer and clock specific *) 87 clock: time; 88 timer0: word; 89 timer1: word; 90 timer2: word; (* can be missing *) 91 92 esi_running: bool; 93 t0i_running: bool; 94 t1i_running: bool; 95 e0i_running: bool; 96 e1i_running: bool; 97 es_running: bool; 36 98 37 (* Program counter *) 38 pc: word; 39 40 (* SFRs *) 41 sp: byte; 42 dpl: byte; 43 dph: byte; 44 pcon: byte; 45 tcon: byte; 46 tmod: byte; 47 tl0: byte; 48 tl1: byte; 49 th0: byte; 50 th1: byte; 51 p1: byte; 52 scon: byte; 53 sbuf: byte; 54 ie: byte; 55 p3: byte; 56 ip: byte; 57 psw: byte; 58 acc: byte; 59 b: byte; 60 t2con: byte; (* 8052 only *) 61 rcap2l: byte; (* 8052 only *) 62 rcap2h: byte; (* 8052 only *) 63 tl2: byte; (* 8052 only *) 64 th2: byte; (* 8052 only *) 65 66 (* Latches for the output lines *) 67 p1_latch: byte; 68 p3_latch: byte; 69 70 (* Fields for tracking the state of the processor. *) 71 72 (* IO specific *) 73 previous_p1_val: bool; 74 previous_p3_val: bool; 75 76 serial_epsilon_out: epsilon option; 77 serial_epsilon_in: epsilon option; 78 79 io_epsilon: epsilon; 80 81 serial_v_in: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option; 82 serial_v_out: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option; 83 84 serial_k_out: continuation option; 85 86 io: continuation; 87 expected_out_time: [ `None | `Now | `At of time ]; 88 89 (* Timer and clock specific *) 90 clock: time; 91 timer0: word; 92 timer1: word; 93 timer2: word; (* can be missing *) 94 95 esi_running: bool; 96 t0i_running: bool; 97 t1i_running: bool; 98 e0i_running: bool; 99 e1i_running: bool; 100 es_running: bool; 101 102 exit_pc: word option; 103 costs: costs; 104 } 105 99 exit_addr : BitVectors.word; 100 cost_labels : string BitVectors.WordMap.t 101 } 102 106 103 val string_of_status: status -> string 107 104 108 val assembly: ASM.program -> BitVectors.byte list (*ASM.instruction list * symbol_table *) * word (* exit pc *) * string IntMap.t 105 106 val assembly: 107 [< ASM.labelled_instruction] ASM.pretty_program -> ASM.program 109 108 110 109 (* 111 val link:112 (ASM.instruction list * symbol_table * cost_map) list -> BitVectors.byte list110 val link: 111 (ASM.instruction list * symbol_table * cost_map) list -> BitVectors.byte list 113 112 *) 114 113 115 114 val initialize: status 116 117 val load_mem: Physical.WordMap.map -> word option -> costs -> status -> status 118 val load: BitVectors.byte list -> word option -> costs -> status -> status 119 115 116 val load_code_memory: BitVectors.byte list -> Physical.WordMap.map 117 val load_mem: Physical.WordMap.map -> status -> status 118 val load: BitVectors.byte list -> status -> status 119 120 120 exception Halt (* to be raised to stop execution *) 121 121 122 122 (* the callback function is used to observe the execution 123 123 trace; it can raise Hold to stop execution. Otherwise 124 124 the processor never halts. *) 125 125 val execute: (status -> unit) -> status -> status 126 126 127 127 val fetch: Physical.WordMap.map -> word -> ASM.instruction * word * int 128 128 129 val interpret : ASM.program -> AST.trace 130 131 val parse_and_interpret_hex : string -> unit 129 val load_program : ASM.program -> status 130 val interpret : bool -> ASM.program -> AST.trace -
Deliverables/D2.2/8051/src/ASM/ASMPrinter.ml
r486 r619 1 open BitVectors;;2 open ASM;;3 1 4 let pp_arg = 5 function 6 `A -> "A" 7 | `B -> "B" 8 | `C -> "C" 9 | `DPTR -> "DPTR" 10 | `ADDR11 x -> hex_string_of_vect x 11 | `ADDR16 x -> hex_string_of_vect x 12 | `DATA x -> "#0" ^ hex_string_of_vect x ^ "h" 13 | `DATA16 x -> "#0" ^ hex_string_of_vect x ^ "h" 14 | `BIT x -> "bit " ^ hex_string_of_vect (x: byte) 15 | `NBIT x -> "nbit " ^ hex_string_of_vect (x: byte) 16 | `REG (r1, r2, r3) -> "R" ^ string_of_int (int_of_vect (mk_nibble false r1 r2 r3)) 17 | `REL x -> hex_string_of_vect x 18 | `A_DPTR -> "@DPTR" 19 | `A_PC -> "@PC" 20 | `DIRECT x -> "0" ^ (hex_string_of_vect (x: byte)) ^ "h" 21 | `EXT_INDIRECT x -> "ext_indirect " ^ string_of_bool x 22 | `EXT_IND_DPTR -> "@DPTR" 23 (* DPM: weird: this seems to be reversed in mcu8051ide: change made. *) 24 | `INDIRECT x -> if not x then "@R0" else "@R1" 25 | `IND_DPTR -> "@DPTR" 26 | `Label s -> s 27 ;; 28 29 let pp_jump = 30 function 31 `CJNE (`U1 (a1,a2),a3) -> "cjne " ^ pp_arg a1 ^ ", " ^ pp_arg a2 ^ ", " ^ pp_arg a3 32 | `CJNE (`U2 (a1,a2),a3) -> "cjne " ^ pp_arg a1 ^ ", " ^ pp_arg a2 ^ ", " ^ pp_arg a3 33 | `DJNZ (a1,a2) -> "djnz " ^ pp_arg a1 ^ ", " ^ pp_arg a2 34 | `JB (a1,a2) -> "jb " ^ pp_arg a1 ^ ", " ^ pp_arg a2 35 | `JBC (a1,a2) -> "jbc " ^ pp_arg a1 ^ ", " ^ pp_arg a2 36 | `JC a1 -> "jc " ^ pp_arg a1 37 | `JNB (a1,a2) -> "jnb " ^ pp_arg a1 ^ ", " ^ pp_arg a2 38 | `JNC a1 -> "jnc " ^ pp_arg a1 39 | `JNZ a1 -> "jnz " ^ pp_arg a1 40 | `JZ a1 -> "jz " ^ pp_arg a1 41 42 let pp_instruction = 43 function 44 `Label l -> l ^ ":" 45 | `Cost l -> l ^ ":" 46 | `Jmp j -> "ljmp " ^ j 47 | `Call j -> "lcall " ^ j 48 | `WithLabel i -> pp_jump i 49 | `Begin_fun -> "\n; Begin function" 50 | `End_fun -> "; End function\n" 51 | (#jump as i) -> pp_jump i 52 | `Mov (a1,a2) -> "mov " ^ pp_arg a1 ^ ", " ^ a2 53 | `ACALL a1 -> "acall " ^ pp_arg a1 54 | `ADD (a1,a2) -> "add " ^ pp_arg a1 ^ ", " ^ pp_arg a2 55 | `ADDC (a1,a2) -> "addc " ^ pp_arg a1 ^ ", " ^ pp_arg a2 56 | `AJMP a1 -> "ajmp " ^ pp_arg a1 57 | `ANL (`U1 (a1,a2)) -> "anl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 58 | `ANL (`U2 (a1,a2)) -> "anl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 59 | `ANL (`U3 (a1,a2)) -> "anl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 60 | `CLR a1 -> "clr " ^ pp_arg a1 61 | `CPL a1 -> "cpl " ^ pp_arg a1 62 | `DA a1 -> "da " ^ pp_arg a1 63 | `DEC a1 -> "dec " ^ pp_arg a1 64 | `DIV (a1,a2) -> "div AB" 65 | `INC a1 -> "inc " ^ pp_arg a1 66 | `JMP a1 -> "jmp " ^ pp_arg a1 67 | `LCALL a1 -> "lcall " ^ pp_arg a1 68 | `LJMP a1 -> "ljmp " ^ pp_arg a1 69 | `MOV (`U1 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2 70 | `MOV (`U2 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2 71 | `MOV (`U3 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2 72 | `MOV (`U4 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2 73 | `MOV (`U5 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2 74 | `MOV (`U6 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2 75 | `MOVC (a1,a2) -> "movc " ^ pp_arg a1 ^ ", " ^ pp_arg a2 76 | `MOVX (`U1 (a1,a2)) -> "movx " ^ pp_arg a1 ^ ", " ^ pp_arg a2 77 | `MOVX (`U2 (a1,a2)) -> "movx " ^ pp_arg a1 ^ ", " ^ pp_arg a2 78 | `MUL(a1, a2) -> "mul AB" 79 | `NOP -> "nop" 80 | `ORL (`U1(a1,a2)) -> "orl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 81 | `ORL (`U2(a1,a2)) -> "orl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 82 | `ORL (`U3(a1,a2)) -> "orl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 83 | `POP a1 -> "pop " ^ pp_arg a1 84 | `PUSH a1 -> "push " ^ pp_arg a1 85 | `RET -> "ret" 86 | `RETI -> "reti" 87 | `RL a1 -> "rl " ^ pp_arg a1 88 | `RLC a1 -> "rlc " ^ pp_arg a1 89 | `RR a1 -> "rr " ^ pp_arg a1 90 | `RRC a1 -> "rrc " ^ pp_arg a1 91 | `SETB a1 -> "setb " ^ pp_arg a1 92 | `SJMP a1 -> "sjmp " ^ pp_arg a1 93 | `SUBB (a1,a2) -> "subb " ^ pp_arg a1 ^ ", " ^ pp_arg a2 94 | `SWAP a1 -> "swap " ^ pp_arg a1 95 | `XCH (a1,a2) -> "xch " ^ pp_arg a1 ^ ", " ^ pp_arg a2 96 | `XCHD(a1,a2) -> "xchd " ^ pp_arg a1 ^ ", " ^ pp_arg a2 97 | `XRL(`U1(a1,a2)) -> "xrl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 98 | `XRL(`U2(a1,a2)) -> "xrl " ^ pp_arg a1 ^ ", " ^ pp_arg a2 2 (** This module provides a function to print [ASM] programs. *) 99 3 100 4 let print_program p = 101 let f s i = Printf.sprintf "%s%s\n" s (pp_instruction i) in 102 "Org 0\n\n" ^ (List.fold_left f "" p.ASM.code) ^ "\nEND\n" 5 let code_memory = ASMInterpret.load_code_memory p.ASM.code in 6 let intel_hex = IntelHex.pack_exported_code_memory 16 65536 code_memory in 7 IntelHex.string_of_intel_hex_format intel_hex -
Deliverables/D2.2/8051/src/ASM/ASMPrinter.mli
r486 r619 1 val pp_arg: 2 [< `A 3 | `ADDR11 of 'a BitVectors.vect 4 | `ADDR16 of 'b BitVectors.vect 5 | `A_DPTR 6 | `A_PC 7 | `B 8 | `BIT of BitVectors.byte 9 | `C 10 | `DATA of 'c BitVectors.vect 11 | `DATA16 of 'd BitVectors.vect 12 | `DIRECT of BitVectors.byte 13 | `DPTR 14 | `EXT_INDIRECT of bool 15 | `EXT_IND_DPTR 16 | `INDIRECT of bool 17 | `IND_DPTR 18 | `NBIT of BitVectors.byte 19 | `REG of BitVectors.bit * BitVectors.bit * BitVectors.bit 20 | `REL of 'e BitVectors.vect ] -> string 21 val pp_instruction: [< ASM.labelled_instruction] -> string 1 2 (** This module provides a function to print [ASM] programs. *) 22 3 23 4 val print_program : ASM.program -> string -
Deliverables/D2.2/8051/src/ASM/BitVectors.ml
r486 r619 155 155 (* CSC: only works properly with bytes!!! *) 156 156 let hex_string_of_vect v = Printf.sprintf "%0 2X" (int_of_vect v);; 157 158 module WordMap = 159 Map.Make (struct type t = word let compare = compare end);; -
Deliverables/D2.2/8051/src/ASM/BitVectors.mli
r486 r619 54 54 val shift_right : 'a vect -> 'a vect 55 55 val shift_left : 'a vect -> 'a vect 56 57 module WordMap: Map.S with type key = word -
Deliverables/D2.2/8051/src/ASM/I8051.ml
r486 r619 44 44 | Mul -> Val.mul 45 45 | Divu -> Val.divu 46 | Modu -> Val.modu 46 | Modu -> Val.modulou 47 47 48 48 let op1 = function … … 57 57 (res2, Val.or_op of1 of2) 58 58 | Sub -> 59 let (res1, uf1) = Val.sub_and_ of v1 v2 in60 let (res2, uf2) = Val.sub_and_ of res1 carry in59 let (res1, uf1) = Val.sub_and_uf v1 v2 in 60 let (res2, uf2) = Val.sub_and_uf res1 carry in 61 61 (res2, Val.or_op uf1 uf2) 62 62 | And -> (Val.and_op v1 v2, carry) -
Deliverables/D2.2/8051/src/ASM/IntelHex.ml
r486 r619 3 3 open Util;; 4 4 open Parser;; 5 open Printf;; 5 6 6 7 exception WrongFormat of string … … 32 33 | '9' -> 9 | 'A' -> 10 | 'B' -> 11 33 34 | 'C' -> 12 | 'D' -> 13 | 'E' -> 14 34 | 'F' -> 15 | _ -> assert false 35 | 'F' -> 15 | 'a' -> 10 | 'b' -> 11 36 | 'c' -> 12 | 'd' -> 13 | 'e' -> 14 37 | 'f' -> 15 | _ -> assert false 35 38 36 39 let intel_hex_entry_type_of_int = … … 93 96 aux (false, (vect_of_int 0 `Eight)) r 94 97 95 let c hecksum_validhex_entry =98 let calculate_checksum hex_entry = 96 99 let ty = (flip vect_of_int $ `Eight) $ int_of_intel_hex_entry_type hex_entry.record_type in 97 100 let addr1,addr2 = from_word hex_entry.record_addr in 98 101 let _, total = add_bytes (hex_entry.record_length :: addr1 :: addr2 :: ty :: hex_entry.data_field) in 99 102 let _,total = half_add (vect_of_int 1 `Eight) $ complement total in 100 hex_entry.data_checksum = total 101 103 total 104 105 let checksum_valid hex_entry = 106 let total = calculate_checksum hex_entry in 107 hex_entry.data_checksum = total 102 108 103 109 let prs_intel_hex_record = … … 135 141 let string_of_intel_hex_entry entry = 136 142 let length_string = hex_string_of_vect entry.record_length in 137 let addr_string = hex_string_of_vect entry.record_addrin138 let checksum_string = hex_string_of_vect entry.data_checksumin139 let type_string = Printf.sprintf "%0 143 let addr_string = Printf.sprintf "%04X" (int_of_vect entry.record_addr) in 144 let checksum_string = Printf.sprintf "%02X" (int_of_vect entry.data_checksum) in 145 let type_string = Printf.sprintf "%02d" (int_of_intel_hex_entry_type entry.record_type) in 140 146 let data_string = String.concat "" (List.map hex_string_of_vect entry.data_field) in 141 147 ":" ^ length_string ^ addr_string ^ type_string ^ data_string ^ checksum_string … … 188 194 aux Physical.WordMap.empty 189 195 ;; 196 197 (* DPM: this needs some comment: 198 We aim to extract code memory into segmented lists of bytes, with a maximum 199 length (chunk_size). The code memory map has a fixed size (max_addressable) 200 on the 8051. Further, the chunks we extract get segmented when we find an 201 unitialized zone in the code memory. 202 *) 203 let export_code_memory chunk_size max_addressable code_mem = 204 let rec aux chunk address start_address rbuff lbuff = 205 if address = max_addressable then 206 (start_address, List.rev rbuff)::lbuff 207 else if chunk = 0 then 208 aux chunk_size address address [] ((start_address, List.rev rbuff)::lbuff) 209 else 210 let code = Physical.WordMap.find (vect_of_int address `Sixteen) code_mem in 211 aux (chunk - 1) (address + 1) start_address (code::rbuff) lbuff 212 in 213 List.rev (aux chunk_size 0 0 [] []) 214 ;; 215 216 let clean_exported_code_memory = List.filter (fun x -> snd x <> []) 217 ;; 218 219 let calculate_data_checksum (record_length, record_addr, record_type, data_field) = 220 let ty = (flip vect_of_int $ `Eight) $ int_of_intel_hex_entry_type record_type in 221 let addr1,addr2 = from_word record_addr in 222 let _, total = add_bytes (record_length :: addr1 :: addr2 :: ty :: data_field) in 223 let _,total = half_add (vect_of_int 0 `Eight) $ complement total in 224 total 225 ;; 226 227 let process_exported_code_memory = 228 List.map (fun x -> 229 let record_length = vect_of_int (List.length (snd x)) `Eight in 230 let record_addr = vect_of_int (fst x) `Sixteen in 231 let record_type = Data in 232 let data_field = snd x in 233 let temp_record = 234 { record_length = record_length; 235 record_addr = record_addr; 236 record_type = record_type; 237 data_field = data_field; 238 data_checksum = zero `Eight 239 } in 240 { temp_record with data_checksum = calculate_checksum temp_record }) 241 ;; 242 243 let pack_exported_code_memory chunk_size max_addressable code_mem = 244 let export = export_code_memory chunk_size max_addressable code_mem in 245 let cleaned = clean_exported_code_memory export in 246 let processed = process_exported_code_memory cleaned in 247 let end_buffer = 248 [{ record_length = zero `Eight; 249 record_addr = zero `Sixteen; 250 record_type = End; 251 data_field = []; 252 data_checksum = vect_of_int 255 `Eight 253 }] in 254 processed @ end_buffer 255 ;; 256 257 let file_of_intel_hex path fmt = 258 let str_fmt = string_of_intel_hex_format fmt in 259 let channel = open_out path in 260 fprintf channel "%s\n" str_fmt; 261 close_out channel 262 ;; -
Deliverables/D2.2/8051/src/ASM/IntelHex.mli
r486 r619 11 11 12 12 val intel_hex_of_file: string -> intel_hex_format 13 val file_of_intel_hex: string -> intel_hex_format -> unit 13 14 val process_intel_hex: intel_hex_format -> Physical.WordMap.map 15 16 val pack_exported_code_memory: int -> int -> Physical.WordMap.map -> intel_hex_format 17 val file_of_intel_hex: string -> intel_hex_format -> unit -
Deliverables/D2.2/8051/src/ASM/Parser.ml
r486 r619 84 84 x = '4' || x = '5' || x = '6' || x = '7' || 85 85 x = '8' || x = '9' || x = 'A' || x = 'B' || 86 x = 'C' || x = 'D' || x = 'E' || x = 'F') 86 x = 'C' || x = 'D' || x = 'E' || x = 'F' || 87 x = 'a' || x = 'b' || x = 'c' || x = 'd' || 88 x = 'e' || x = 'f') 87 89 -
Deliverables/D2.2/8051/src/ASM/Physical.ml
r486 r619 10 10 val find : key -> map -> byte 11 11 val add : key -> byte -> map -> map 12 val fold : (key -> byte -> 'b -> 'b) -> map -> 'b -> 'b 13 val equal: (byte -> byte -> bool) -> map -> map -> bool 12 14 end 13 15 ;; … … 21 23 find k m 22 24 with Not_found -> zero `Eight 25 let fold = fold 26 let equal = equal 23 27 end;; 24 28 … … 31 35 find k m 32 36 with Not_found -> zero `Eight 37 let fold = fold 38 let equal = equal 33 39 end;; 34 40 … … 97 103 | _ -> assert false 98 104 ;; 105 106 let addr16_of_addr11 pc a = 107 let pc_upper, _ = from_word pc in 108 let n1, n2 = from_byte pc_upper in 109 let (b1,b2,b3,b) = from_word11 a in 110 let (p1,p2,p3,p4),(p5,_,_,_) = from_nibble n1, from_nibble n2 in 111 mk_word (mk_byte (mk_nibble p1 p2 p3 p4) (mk_nibble p5 b1 b2 b3)) b 112 ;; -
Deliverables/D2.2/8051/src/ASM/Physical.mli
r486 r619 10 10 val find : key -> map -> byte 11 11 val add : key -> byte -> map -> map 12 val fold : (key -> byte -> 'b -> 'b) -> map -> 'b -> 'b 13 val equal: (byte -> byte -> bool) -> map -> map -> bool 12 14 end 13 15 ;; … … 26 28 val dec: byte -> byte (* with roll-over *) 27 29 val inc: byte -> byte (* with roll-over *) 30 31 val addr16_of_addr11: word -> word11 -> word -
Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml
r486 r619 55 55 renv : hdw_reg_env ; 56 56 mem : memory ; 57 trace : AST.trace}57 trace : CostLabel.t list } 58 58 59 59 … … 448 448 (Val.to_string st.pc) (current_label lbls_offs st) ; 449 449 Printf.printf "SP: %s\n%!" 450 (Val.to_string (Val.merge [ I8051.RegisterMap.find I8051.sph st.renv;451 I8051.RegisterMap.find I8051.spl st.renv])) ;450 (Val.to_string (Val.merge [get_reg (Hdw I8051.sph) st ; 451 get_reg (Hdw I8051.spl) st])) ; 452 452 Printf.printf "ISP: %s%!" (Val.to_string st.isp) ; 453 453 print_lenv st.lenv ; … … 456 456 Printf.printf "\n%!" 457 457 458 let rec iter_small_step lbls_offs st = match fetch_stmt lbls_offs st with 459 | ERTL.St_return ret_regs when st.st_frs = [] -> 460 (* 461 print_state lbls_offs st ; 462 let res = fetch_result st.renv ret_regs in 463 Printf.printf "Return: %s\n%!" (Val.to_string res) ; 464 *) 465 List.rev st.trace 466 | stmt -> 467 (* 468 print_state lbls_offs st ; 469 *) 470 let st' = interpret_stmt lbls_offs st stmt in 471 iter_small_step lbls_offs st' 458 let compute_result st ret_regs = 459 try 460 let v = get_reg (Psd (MiscPottier.last ret_regs)) st in 461 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 462 else IntValue.Int8.zero 463 with Not_found -> IntValue.Int8.zero 464 465 let rec iter_small_step print_result lbls_offs st = 466 match fetch_stmt lbls_offs st with 467 | ERTL.St_return ret_regs when st.st_frs = [] -> 468 let (res, cost_labels) as trace = 469 (compute_result st ret_regs, List.rev st.trace) in 470 if print_result then 471 Printf.printf "ERTL: %s\n%!" (IntValue.Int8.to_string res) ; 472 trace 473 | stmt -> 474 (* 475 print_state lbls_offs st ; 476 *) 477 let st' = interpret_stmt lbls_offs st stmt in 478 iter_small_step print_result lbls_offs st' 472 479 473 480 … … 530 537 - Initialize the carry flag to 0. *) 531 538 532 let interpret p = match p.ERTL.main with533 | None -> []539 let interpret print_result p = match p.ERTL.main with 540 | None -> (IntValue.Int8.zero (* TODO *), []) 534 541 | Some main -> 535 542 let lbls_offs = labels_offsets p in … … 541 548 let st = init_main_call lbls_offs st main in 542 549 let st = change_carry st Val.zero in 543 iter_small_step lbls_offs st550 iter_small_step print_result lbls_offs st -
Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.mli
r486 r619 2 2 (** This module provides an interpreter for the [ERTL] language. *) 3 3 4 val interpret : ERTL.program -> AST.trace4 val interpret : bool -> ERTL.program -> AST.trace -
Deliverables/D2.2/8051/src/LIN/LINInterpret.ml
r486 r619 42 42 renv : hdw_reg_env ; 43 43 mem : memory ; 44 trace : AST.trace}44 trace : CostLabel.t list } 45 45 46 46 … … 195 195 match Mem.find_fun_def st.mem ptr with 196 196 | LIN.F_int def -> 197 (*198 Printf.printf "Pushing return address in IRAM: %s\n%!"199 (Val.to_string (next_pc st).pc) ;200 *)201 197 let st = save_ra st in 202 198 init_fun_call st ptr … … 205 201 let interpret_return st = 206 202 let pc = return_pc st in 207 (*208 Printf.printf "Returning to %s\n%!" (Val.to_string pc) ;209 *)210 203 change_pc st pc 211 204 … … 328 321 Printf.printf "\n%!" 329 322 330 let print_result st =331 let string_of_reg r = Val.to_string (get_reg r st)in332 Printf.printf "DPH: %s - DPL: %s\n%!"333 (string_of_reg I8051.dph) (string_of_reg I8051.dpl)334 335 let rec iter_small_step st =323 let compute_result st = 324 let v = get_reg I8051.dpl st in 325 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 326 else IntValue.Int8.zero 327 328 let rec iter_small_step print_result st = 336 329 (* 330 (* <DEBUG> *) 337 331 print_state st ; 332 (* </DEBUG> *) 338 333 *) 339 334 match fetch_stmt st with 340 335 | LIN.St_return when Val.eq (return_pc st) Val.zero -> 341 (* 342 print_state st ; 343 print_result st ;344 *) 345 List.rev st.trace336 let (res, cost_labels) as trace = 337 (compute_result st, List.rev st.trace) in 338 if print_result then 339 Printf.printf "LIN: %s\n%!" (IntValue.Int8.to_string res) ; 340 trace 346 341 | stmt -> 347 342 let st' = interpret_stmt st stmt in 348 iter_small_step st'343 iter_small_step print_result st' 349 344 350 345 … … 406 401 - Initialize the carry flag to 0. *) 407 402 408 let interpret p = match p.LIN.main with409 | None -> []403 let interpret print_result p = match p.LIN.main with 404 | None -> (IntValue.Int8.zero, []) 410 405 | Some main -> 411 406 let st = empty_state in … … 416 411 let st = init_main_call st main in 417 412 let st = change_carry st Val.zero in 418 iter_small_step st413 iter_small_step print_result st -
Deliverables/D2.2/8051/src/LIN/LINInterpret.mli
r486 r619 3 3 return the trace of cost labels encountered. *) 4 4 5 val interpret: LIN.program -> AST.trace5 val interpret: bool -> LIN.program -> AST.trace -
Deliverables/D2.2/8051/src/LIN/LINToASM.ml
r486 r619 129 129 130 130 131 (* Move the first cost label of each function at the beginning of the132 function. Indeed, some preamble instructions (such as frame creation) might133 get in the way. *)134 135 let move_first_cost_label_up_code =136 let rec aux preamble = function137 | [] -> preamble138 | LIN.St_cost lbl :: code -> LIN.St_cost lbl :: preamble @ code139 | inst :: code -> aux (preamble @ [inst]) code140 in aux []141 142 let move_first_cost_label_up_funct (id, def) =143 let def' = match def with144 | LIN.F_int int_def -> LIN.F_int (move_first_cost_label_up_code int_def)145 | _ -> def in146 (id, def')147 148 let move_first_cost_label_up p =149 { p with LIN.functs = List.map move_first_cost_label_up_funct p.LIN.functs }150 151 152 131 (* Translating programs. 153 132 … … 165 144 let tmp_universe = Label.Gen.new_universe fresh_tmp in 166 145 let glbls_addr = globals_addr p.LIN.vars in 167 { ASM.preamble = p.LIN.vars ; 168 ASM.exit_label = exit_label ; 169 ASM.code = 170 translate_functs tmp_universe glbls_addr exit_label p.LIN.main 171 p.LIN.functs ; 172 ASM.has_main = p.LIN.main <> None } 146 let p = 147 { ASM.ppreamble = p.LIN.vars ; 148 ASM.pexit_label = exit_label ; 149 ASM.pcode = 150 translate_functs tmp_universe glbls_addr exit_label p.LIN.main 151 p.LIN.functs ; 152 ASM.phas_main = p.LIN.main <> None } in 153 ASMInterpret.assembly p -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r486 r619 45 45 renv : hdw_reg_env ; 46 46 mem : memory ; 47 trace : AST.trace}47 trace : CostLabel.t list } 48 48 49 49 … … 371 371 (string_of_reg I8051.dph) (string_of_reg I8051.dpl) 372 372 373 let rec iter_small_step lbls_offs st = 373 let compute_result st = 374 let v = get_reg I8051.dpl st in 375 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 376 else IntValue.Int8.zero 377 378 let rec iter_small_step print_result lbls_offs st = 374 379 (* 375 380 print_state lbls_offs st ; … … 377 382 match fetch_stmt lbls_offs st with 378 383 | LTL.St_return when Val.eq (return_pc st) Val.zero -> 379 (* 380 print_state lbls_offs st ; 381 print_result st ;382 *) 383 List.rev st.trace384 let (res, cost_labels) as trace = 385 (compute_result st, List.rev st.trace) in 386 if print_result then 387 Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ; 388 trace 384 389 | stmt -> 385 390 let st' = interpret_stmt lbls_offs st stmt in 386 iter_small_step lbls_offs st'391 iter_small_step print_result lbls_offs st' 387 392 388 393 … … 446 451 - Initialize the carry flag to 0. *) 447 452 448 let interpret p = match p.LTL.main with449 | None -> []453 let interpret print_result p = match p.LTL.main with 454 | None -> (IntValue.Int8.zero, []) 450 455 | Some main -> 451 456 let lbls_offs = labels_offsets p in … … 457 462 let st = init_main_call lbls_offs st main in 458 463 let st = change_carry st Val.zero in 459 iter_small_step lbls_offs st464 iter_small_step print_result lbls_offs st -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.mli
r486 r619 3 3 return the trace of cost labels encountered. *) 4 4 5 val interpret: LTL.program -> AST.trace5 val interpret: bool -> LTL.program -> AST.trace -
Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
r486 r619 41 41 type state = 42 42 | State of stack_frame list * RTL.graph * Label.t * Val.t (* sp *) * 43 local_env * Val.t (* carry *) * memory * AST.trace43 local_env * Val.t (* carry *) * memory * CostLabel.t list 44 44 | CallState of stack_frame list * RTL.function_def * 45 Val.t list (* args *) * memory * AST.trace45 Val.t list (* args *) * memory * CostLabel.t list 46 46 | ReturnState of stack_frame list * Val.t list (* return values *) * 47 memory * AST.trace47 memory * CostLabel.t list 48 48 49 49 … … 101 101 (mem : memory) 102 102 (stmt : RTL.statement) 103 (t : AST.trace) :103 (t : CostLabel.t list) : 104 104 state = match stmt with 105 105 … … 269 269 (args : Val.t list) 270 270 (mem : memory) 271 (t : AST.trace) :271 (t : CostLabel.t list) : 272 272 state = 273 273 match f_def with … … 286 286 (ret_vals : Val.t list) 287 287 (mem : memory) 288 (t : AST.trace) :288 (t : CostLabel.t list) : 289 289 state = 290 290 let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in … … 311 311 (Register.print r) (Val.to_string v)) 312 312 313 let rec iter_small_step st = match small_step st with 313 let compute_result vs = 314 try 315 let v = MiscPottier.last vs in 316 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 317 else IntValue.Int8.zero 318 with Not_found -> IntValue.Int8.zero 319 320 let rec iter_small_step print_result st = match small_step st with 314 321 (* 322 (* <DEBUG> *) 315 323 | ReturnState ([], vs, mem, t) -> 316 324 Mem.print mem ; … … 331 339 Printf.printf "Carry = %s\n\n%!" (Val.to_string carry) ; 332 340 iter_small_step st' 341 (* </DEBUG> *) 333 342 *) 334 343 | ReturnState ([], vs, mem, t) -> 335 (* 336 Printf.printf "Return: %s\n%!" (print_ret_vals vs) ;337 *) 338 List.rev t339 | st' -> iter_small_step st'344 let (res, cost_labels) as trace = (compute_result vs, List.rev t) in 345 if print_result then 346 Printf.printf "RTL: %s\n%!" (IntValue.Int8.to_string res) ; 347 trace 348 | st' -> iter_small_step print_result st' 340 349 341 350 … … 357 366 (* Interpret the program only if it has a main. *) 358 367 359 let interpret p = match p.RTL.main with360 | None -> []368 let interpret print_result p = match p.RTL.main with 369 | None -> (IntValue.Int8.zero, []) 361 370 | Some main -> 362 371 let mem = init_mem p in 363 372 let main_def = find_function mem main in 364 373 let st = CallState ([], main_def, [], mem, []) in 365 iter_small_step st374 iter_small_step print_result st -
Deliverables/D2.2/8051/src/RTL/RTLInterpret.mli
r486 r619 3 3 and return the trace of cost labels encountered. *) 4 4 5 val interpret : RTL.program -> AST.trace5 val interpret : bool -> RTL.program -> AST.trace -
Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml
r486 r619 171 171 | [] -> [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl] 172 172 | [r] -> 173 [fun start_lbl -> 174 adds_graph [ERTL.St_set_hdw (I8051.st0, r, start_lbl)] start_lbl] 173 [fun start_lbl dest_lbl def -> 174 let (def, r_tmp) = fresh_reg def in 175 adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ; 176 ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl) ; 177 ERTL.St_set_hdw (I8051.st0, r, start_lbl)] 178 start_lbl dest_lbl def] 175 179 | r1 :: r2 :: _ -> 176 180 [(fun start_lbl -> 177 adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl)] start_lbl) ; 178 (fun start_lbl -> 179 adds_graph [ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)] 181 adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl) ; 182 ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)] 180 183 181 184 let add_epilogue ret_regs srah sral sregs def = … … 267 270 268 271 (* Fetching the result depends on the type of the function, or say, the number 269 of registers that are waiting for a value. *) 272 of registers that are waiting for a value. Temporary non allocatable 273 registers are used. Indeed, moving directly from DPL to a pseudo-register may 274 cause a bug: DPL might be used to compute the address of the 275 pseudo-register. *) 270 276 271 277 let fetch_result ret_regs start_lbl = match ret_regs with 272 278 | [] -> adds_graph [ERTL.St_skip start_lbl] start_lbl 273 279 | [r] -> 274 adds_graph280 adds_graph 275 281 [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ; 276 282 ERTL.St_get_hdw (r, I8051.st0, start_lbl)] … … 401 407 402 408 409 (* Move the first cost label of each function at the beginning of the 410 function. Indeed, the instructions for calling conventions (stack allocation 411 for example) are added at the very beginning of the function, thus before the 412 first cost label. *) 413 414 let generate stmt def = 415 let entry = Label.Gen.fresh def.ERTL.f_luniverse in 416 let def = 417 { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in 418 { def with ERTL.f_entry = entry } 419 420 let find_and_remove_first_cost_label def = 421 let rec aux lbl = match Label.Map.find lbl def.ERTL.f_graph with 422 | ERTL.St_cost (cost_label, next_lbl) -> 423 let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in 424 (cost_label, { def with ERTL.f_graph = graph }) 425 | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl) 426 | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl) 427 | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl) 428 | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl) 429 | ERTL.St_move (_, _, lbl) | ERTL.St_opaccs (_, _, _, _, lbl) 430 | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl) 431 | ERTL.St_clear_carry lbl | ERTL.St_load (_, _, _, lbl) 432 | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl) 433 | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl) 434 -> 435 aux lbl 436 | ERTL.St_condacc _ | ERTL.St_return _ -> 437 (* Should be impossible: the first cost label is found after some linear 438 instructions. *) 439 assert false in 440 aux def.ERTL.f_entry 441 442 let move_first_cost_label_up_internal def = 443 let (cost_label, def) = find_and_remove_first_cost_label def in 444 generate (ERTL.St_cost (cost_label, def.ERTL.f_entry)) def 445 446 let move_first_cost_label_up (id, def) = 447 let def' = match def with 448 | ERTL.F_int int_fun -> 449 ERTL.F_int (move_first_cost_label_up_internal int_fun) 450 | _ -> def in 451 (id, def') 452 453 403 454 let translate p = 404 455 (* We simplify tail calls as regular calls for now. *) 405 456 let p = RTLtailcall.simplify p in 457 (* The tranformation on each RTL function: create an ERTL function and move 458 its first cost label at the very beginning. *) 459 let f funct = move_first_cost_label_up (translate_funct funct) in 406 460 { ERTL.vars = p.RTL.vars ; 407 ERTL.functs = List.map translate_functp.RTL.functs ;461 ERTL.functs = List.map f p.RTL.functs ; 408 462 ERTL.main = p.RTL.main } -
Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml
r486 r619 38 38 type state = 39 39 | State of stack_frame list * RTLabs.graph * Val.t (* stack pointer *) * 40 Label.t * local_env * memory * AST.trace40 Label.t * local_env * memory * CostLabel.t list 41 41 | CallState of stack_frame list * RTLabs.function_def * 42 Val.t list (* args *) * memory * AST.trace42 Val.t list (* args *) * memory * CostLabel.t list 43 43 | ReturnState of stack_frame list * Val.t (* return value *) * 44 memory * AST.trace44 memory * CostLabel.t list 45 45 46 46 … … 135 135 | AST.Op_divu -> Val.divu 136 136 | AST.Op_mod -> Val.modulo 137 | AST.Op_modu -> Val.modu 137 | AST.Op_modu -> Val.modulou 138 138 | AST.Op_and -> Val.and_op 139 139 | AST.Op_or -> Val.or_op … … 192 192 (mem : memory) 193 193 (stmt : RTLabs.statement) 194 (t : AST.trace) :194 (t : CostLabel.t list) : 195 195 state = match stmt with 196 196 … … 364 364 (args : Val.t list) 365 365 (mem : memory) 366 (t : AST.trace) :366 (t : CostLabel.t list) : 367 367 state = 368 368 match f_def with … … 382 382 (ret_val : Val.t) 383 383 (mem : memory) 384 (t : AST.trace) :384 (t : CostLabel.t list) : 385 385 state = 386 386 let lenv = adds sf.ret_regs ret_val sf.lenv in … … 400 400 401 401 402 let rec iter_small_step st = match small_step st with 402 let compute_result v = 403 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 404 else IntValue.Int8.zero 405 406 let rec iter_small_step print_result st = match small_step st with 403 407 (* 408 (* <DEBUG> *) 404 409 | ReturnState ([], v, mem, t) -> 405 410 Mem.print mem ; … … 409 414 | ReturnState (_, _, mem, _) 410 415 | State (_, _, _, _, _, mem, _) as st' -> Mem.print mem ; iter_small_step st' 416 (* </DEBUG> *) 411 417 *) 412 | ReturnState ([], v, mem, t) -> List.rev t 413 | st' -> iter_small_step st' 418 | ReturnState ([], v, mem, t) -> 419 let (res, cost_labels) as trace = (compute_result v, List.rev t) in 420 if print_result then 421 Printf.printf "RTLabs: %s\n%!" (IntValue.Int8.to_string res) ; 422 trace 423 | st' -> iter_small_step print_result st' 414 424 415 425 … … 431 441 (* Interpret the program only if it has a main. *) 432 442 433 let interpret p = match p.RTLabs.main with434 | None -> []443 let interpret print_result p = match p.RTLabs.main with 444 | None -> (IntValue.Int8.zero, []) 435 445 | Some main -> 436 446 let mem = init_mem p in 437 447 let main_def = find_function mem main in 438 448 let st = CallState ([], main_def, [], mem, []) in 439 iter_small_step st449 iter_small_step print_result st -
Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.mli
r486 r619 3 3 and return the trace of cost labels encountered. *) 4 4 5 val interpret : RTLabs.program -> AST.trace5 val interpret : bool -> RTLabs.program -> AST.trace -
Deliverables/D2.2/8051/src/acc.ml
r486 r619 22 22 *) 23 23 let process filename = 24 let _ = Printf.eprintf "Processing %s :\n" filename in 25 let src_language = Options.get_source_language () in 26 let tgt_language = Options.get_target_language () in 27 let input_ast = Languages.parse src_language filename in 28 let input_ast = Languages.labelize input_ast in 24 let _ = Printf.eprintf "Processing %s.\n%!" filename in 25 let src_language = Options.get_source_language () in 26 let tgt_language = Options.get_target_language () in 27 let input_ast = Languages.parse src_language filename in 28 let input_ast = Languages.labelize input_ast in 29 let (exact_output, output_filename) = match Options.get_output_files () with 30 | None -> (false, filename) 31 | Some filename' -> (true, filename') in 32 let save = Languages.save exact_output output_filename in 29 33 let target_asts = 30 34 (** If debugging is enabled, the compilation function returns all … … 34 38 in 35 39 let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in 36 Languages.save filename final_ast;40 save final_ast; 37 41 (if Options.annotation_requested () then 38 let annotated_input_ast = Languages.annotate input_ast final_ast in 39 Languages.save filename annotated_input_ast); 42 let (annotated_input_ast, cost_incr) = 43 Languages.annotate input_ast final_ast in 44 save annotated_input_ast; 45 Languages.save_cost_incr output_filename cost_incr); 40 46 (if Options.is_debug_enabled () then 41 List.iter (Languages.save filename)intermediate_asts);47 List.iter save intermediate_asts); 42 48 if Options.interpretation_requested () || Options.is_debug_enabled () then 43 49 begin 44 50 let asts = input_ast :: target_asts in 45 let label_traces = List.map Languages.interpret asts in 46 Printf.eprintf "Checking execution traces..."; 47 Checker.same_traces (List.combine asts label_traces); 48 Printf.eprintf "OK.\n%!"; 51 let print_result = Options.is_print_result_enabled () in 52 let label_traces = List.map (Languages.interpret print_result) asts in 53 Printf.eprintf "Checking execution traces...%!"; 54 Checker.same_traces (List.combine asts label_traces); 55 Printf.eprintf "OK.\n%!"; 49 56 end 50 57 51 58 let _ = 52 59 if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files 53 else List.iter process input_files 60 else List.iter process input_files -
Deliverables/D2.2/8051/src/checker.ml
r486 r619 1 let same_traces (traces : ((Languages.ast * (Label.t list)) list)) =1 let same_traces (traces : ((Languages.ast * AST.trace) list)) = 2 2 let compare_trace trace1 trace2 = 3 3 let occs_trace1 = Misc.ListExt.multi_set_of_list trace1 … … 5 5 Misc.ListExt.assoc_diff occs_trace1 occs_trace2 6 6 in 7 let check_trace (_, trace1) (_, trace2) =7 let check_trace (_, (_, trace1)) (_, (_, trace2)) = 8 8 compare_trace trace1 trace2 = [] 9 9 in … … 22 22 match Misc.ListExt.transitive_forall2 check_trace traces with 23 23 | None -> () 24 | Some ((ast1, trace1), (ast2, trace2)) ->24 | Some ((ast1, (res1, trace1)), (ast2, (res2, trace2))) -> 25 25 let lang1 = Languages.to_string (Languages.language_of_ast ast1) 26 26 and lang2 = Languages.to_string (Languages.language_of_ast ast2) in -
Deliverables/D2.2/8051/src/checker.mli
r486 r619 3 3 (** [same_traces ts] checks that the collected execution traces are 4 4 identical (modulo permutation). *) 5 val same_traces : (Languages.ast * (Label.t list)) list -> unit 6 7 8 5 val same_traces : (Languages.ast * AST.trace) list -> unit -
Deliverables/D2.2/8051/src/clight/clightAnnotator.ml
r486 r619 12 12 13 13 14 (* Program var names, cost labels and labels *)14 (* Program var and fun names, cost labels and labels *) 15 15 16 16 let string_set_of_list l = … … 312 312 let res = ClightParser.process tmp_file in 313 313 Misc.SysExt.safe_remove tmp_file ; 314 res 315 316 314 (res, cost_incr) -
Deliverables/D2.2/8051/src/clight/clightAnnotator.mli
r486 r619 5 5 global variable --- the so-called cost variable --- is added to the program. 6 6 Then, each cost label in the program is replaced by an increment of the cost 7 variable, following the mapping [cost_map]. *) 7 variable, following the mapping [cost_map]. The returned string is the name 8 of the cost increment function. *) 8 9 9 val instrument : Clight.program -> int CostLabel.Map.t -> Clight.program 10 val instrument : Clight.program -> int CostLabel.Map.t -> 11 Clight.program * string 10 12 11 13 val cost_labels : Clight.program -> CostLabel.Set.t -
Deliverables/D2.2/8051/src/clight/clightInterpret.ml
r486 r619 248 248 (*Pointer*) 249 249 | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 -> 250 Value.add v1 (Value. of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))250 Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1)))) 251 251 | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 -> 252 Value.add v1 (Value. of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))252 Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1)))) 253 253 (*Error*) 254 254 | _ -> assert false (*Type error*) … … 271 271 (*Pointer*) 272 272 | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 -> 273 Value.sub v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1)))) 274 | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 -> 275 Value.sub v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1)))) 273 Value.sub v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1)))) 276 274 (*Error*) 277 275 | _ -> assert false (*Type error*) … … 611 609 | State(f,Sswitch(a,sl),k,e,m) -> 612 610 let (n,l) = (match eval_expr globalenv e m a with 613 | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll) 611 | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll) 614 612 | _ -> assert false (*Wrong switch index*) 615 613 ) in … … 682 680 (m,(g2,f)) 683 681 682 let compute_result v = 683 if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v) 684 else IntValue.Int8.zero 685 684 686 let interpret debug prog = match prog.prog_main with 685 | None -> []687 | None -> (IntValue.Int8.zero, []) 686 688 | Some main -> 687 689 let (m,g) = initmem_clight prog in … … 689 691 let rec exec trace = function 690 692 | (Returnstate(v,Kstop,m),l) -> 693 (* 691 694 if debug then ( 692 695 print_string ("Result: "^(Value.to_string v)); … … 694 697 Mem.print m 695 698 ); 696 l@trace 699 *) 700 let (res, cost_labels) as trace = (compute_result v, l@trace) in 701 if debug then 702 Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ; 703 trace 697 704 | (State(_,Sskip,Kstop,_,m),l) -> (*Implicit return in main*) 705 (* 698 706 if debug then ( 699 707 print_string ("Result: (implicit return)"); … … 701 709 Mem.print m 702 710 ); 703 l@trace 711 *) 712 let (res, cost_labels) as trace = (IntValue.Int8.zero, l@trace) in 713 if debug then 714 Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ; 715 trace 704 716 | (state,l) -> 717 (* 705 718 if debug then print_string ((string_of_state state)^"\n"); 719 *) 706 720 exec (l@trace) (next_step g state) 707 721 in 722 (* 708 723 if debug then print_string "> --- Interpret Clight --- <\n"; 709 exec [] first_state 724 *) 725 exec [] first_state -
Deliverables/D2.2/8051/src/clight/clightToCminor.ml
r486 r619 154 154 let make_cast e = function 155 155 | (Tint(_,_),Tint(I8,Signed)) when int_size>8 -> Op1 (Op_cast8signed,e) 156 | (Tint(_,_),Tint(I8,Unsigned)) when int_size>8 -> Op1 (Op_cast8 signed,e)156 | (Tint(_,_),Tint(I8,Unsigned)) when int_size>8 -> Op1 (Op_cast8unsigned,e) 157 157 | (Tint(_,_),Tint(I16,Signed)) when int_size>16 -> Op1 (Op_cast16signed,e) 158 158 | (Tint(_,_),Tint(I16,Unsigned)) when int_size>16 -> Op1 (Op_cast16unsigned,e) … … 521 521 | (id,External (i,p,r)) -> (id, F_ext (translate_external i p r)) 522 522 523 let translate p = 523 let translate p = 524 (* TODO: Clight32ToClight8 transformation *) 525 (* 526 let p = Clight32ToClight8.translate p in 527 *) 528 (* <DEBUG> *) 529 (* 530 Printf.printf "%s\n%!" (ClightPrinter.print_program p) ; 531 *) 532 (* </DEBUG> *) 524 533 let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in 525 534 let p = -
Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml
r486 r619 137 137 (f_name, instrument_function costs_mapping cost_id f_def) in 138 138 let functs = List.map f p.Cminor.functs in 139 { Cminor.vars = vars ; 140 Cminor.functs = functs ; 141 Cminor.main = p.Cminor.main } 139 ({ Cminor.vars = vars ; 140 Cminor.functs = functs ; 141 Cminor.main = p.Cminor.main }, 142 "" (* TODO *)) 142 143 143 144 -
Deliverables/D2.2/8051/src/cminor/cminorAnnotator.mli
r486 r619 5 5 global variable --- the so-called cost variable --- is added to the program. 6 6 Then, each cost label in the program is replaced by an increment of the cost 7 variable, following the mapping [cost_map]. *) 7 variable, following the mapping [cost_map]. The returned string is the name 8 of the cost increment function. *) 8 9 9 val instrument : Cminor.program -> int CostLabel.Map.t -> Cminor.program 10 val instrument : Cminor.program -> int CostLabel.Map.t -> 11 Cminor.program * string 10 12 11 13 val cost_labels : Cminor.program -> CostLabel.Set.t -
Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml
r486 r619 128 128 | Op_divu -> Value.divu arg1 arg2 129 129 | Op_mod -> Value.modulo arg1 arg2 130 | Op_modu -> Value.modu arg1 arg2130 | Op_modu -> Value.modulou arg1 arg2 131 131 | Op_and -> Value.and_op arg1 arg2 132 132 | Op_or -> Value.or_op arg1 arg2 … … 405 405 (m,(g2,f)) 406 406 407 let compute_result v = 408 if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v) 409 else IntValue.Int8.zero 410 407 411 let interpret debug prog = match prog.main with 408 | None -> []412 | None -> (IntValue.Int8.zero, []) 409 413 | Some main -> 410 414 let (m,global_env) = initmem_cminor prog in … … 413 417 [], Ct_stop,m),[]) in 414 418 let rec exec l = function 415 | (State_return(v,Ct_stop,m),lbl) -> 419 | (State_return(v,Ct_stop,m),lbl) -> 420 (* 416 421 if debug then ( 417 422 print_string ("Result: "^(Value.to_string v)); … … 419 424 Mem.print m 420 425 ); 421 lbl@l 426 *) 427 let (res, cost_labels) as trace = (compute_result v, lbl@l) in 428 if debug then 429 Printf.printf "Cminor: %s\n%!" (IntValue.Int8.to_string res) ; 430 trace 422 431 | (State_regular(_,St_skip,Ct_stop,_,_,m),lbl) -> 432 (* 423 433 if debug then ( 424 434 print_string ("Result: (implicit return)\n"); … … 426 436 Mem.print m 427 437 ); 428 lbl@l 438 *) 439 let (res, cost_labels) as trace = (IntValue.Int8.zero, lbl@l) in 440 if debug then 441 Printf.printf "Cminor: %s\n%!" (IntValue.Int8.to_string res) ; 442 trace 429 443 | (state,lbl) -> 444 (* 430 445 if debug then print_string ((string_of_state state)^"\n"); 446 *) 431 447 exec (lbl@l) (state_transition state global_env) 432 448 in 449 (* 433 450 if debug then print_string ">------------------- Interpret Cminor -------------------<\n"; 451 *) 434 452 (exec [] first_state) -
Deliverables/D2.2/8051/src/common/AST.mli
r486 r619 92 92 93 93 94 (* Traces returned by interpreters: only cost labels are observed. *) 94 (* Traces returned by interpreters: result and cost labels are observed. The 95 result is interpreted as an 8 bits integer for coherence between 96 languages. *) 95 97 96 type trace = CostLabel.t list98 type trace = IntValue.int8 * CostLabel.t list -
Deliverables/D2.2/8051/src/common/intValue.ml
r486 r619 1 2 (** This module defines functions to manipulate bounded integers. They can be 3 used to represent sequences of bits. *) 1 4 2 5 open Big_int 3 6 4 7 8 (* Integers, whatever their size, will be represented using the Big_int 9 module. This allows immediate conversion, and allows the representation of 10 any integer (that fits into memory). *) 11 5 12 type int_repr = Big_int.big_int 6 13 14 (* The parameter module. Bounded integers are characterized by the number of 15 bits used to represent them. *) 16 7 17 module type INTTYPE = 8 18 sig 9 val size : int (* in bytes *) 10 val is_signed : bool 19 val size : int (* in bytes *) 11 20 end 21 22 (* The signature provided to manipulate bounded integers. *) 12 23 13 24 module type S = sig … … 20 31 val one : t 21 32 22 val succ : t -> t 23 val pred : t -> t 24 val add : t -> t -> t 25 (** [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the 26 unsigned value of [i2] overflows. *) 27 val add_of : t -> t -> bool 28 val sub : t -> t -> t 29 (** [sub_of i1 i2] returns true iff substracting the unsigned value of [i1] 30 and the unsigned value of [i2] underflows. *) 31 val sub_of : t -> t -> bool 32 val mul : t -> t -> t 33 val div : t -> t -> t 34 val modulo : t -> t -> t 35 val eq : t -> t -> bool 36 val neq : t -> t -> bool 37 val lt : t -> t -> bool 38 val le : t -> t -> bool 39 val gt : t -> t -> bool 40 val ge : t -> t -> bool 41 val neg : t -> t 42 val lognot : t -> t 43 val logand : t -> t -> t 44 val logor : t -> t -> t 45 val logxor : t -> t -> t 46 val shl : t -> t -> t 47 val shr : t -> t -> t 48 val shrl : t -> t -> t 49 val max : t -> t -> t 50 val min : t -> t -> t 51 val cast : int_repr -> t 52 val of_int : int -> t 53 val to_int : t -> int 33 val succ : t -> t 34 val pred : t -> t 35 val add : t -> t -> t 36 (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *) 37 val add_of : t -> t -> bool 38 val sub : t -> t -> t 39 (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] 40 underflows. *) 41 val sub_uf : t -> t -> bool 42 val mul : t -> t -> t 43 val div : t -> t -> t 44 val divu : t -> t -> t 45 val modulo : t -> t -> t 46 val modulou : t -> t -> t 47 val eq : t -> t -> bool 48 val neq : t -> t -> bool 49 val lt : t -> t -> bool 50 val ltu : t -> t -> bool 51 val le : t -> t -> bool 52 val leu : t -> t -> bool 53 val gt : t -> t -> bool 54 val gtu : t -> t -> bool 55 val ge : t -> t -> bool 56 val geu : t -> t -> bool 57 val neg : t -> t 58 val lognot : t -> t 59 val logand : t -> t -> t 60 val logor : t -> t -> t 61 val logxor : t -> t -> t 62 val shl : t -> t -> t 63 val shr : t -> t -> t 64 val shrl : t -> t -> t 65 val max : t -> t -> t 66 val maxu : t -> t -> t 67 val min : t -> t -> t 68 val minu : t -> t -> t 69 val cast : int_repr -> t 70 val of_int : int -> t 71 val to_int : t -> int 72 73 (** [zero_ext n a] performs zero extension on [a] where [n] bits are 74 significant. *) 75 val zero_ext : int -> t -> t 76 (** [sign_ext n a] performs sign extension on [a] where [n] bits are 77 significant. *) 78 val sign_ext : int -> t -> t 54 79 55 80 (** [break i n] cuts [i] in [n] parts. In the resulting list, the first 56 81 element is the high bits, and the last is the low bits. *) 57 82 val break : t -> int -> t list 58 (** [merge l] creates anthe integer where the first element of [l] is its83 (** [merge l] creates the integer where the first element of [l] is its 59 84 high bits, etc, and the last element of [l] is its low bits. *) 60 85 val merge : t list -> t … … 63 88 64 89 65 (* First, we use a parameter module and a functor where integers may be 66 unbounded. This will allow to create the Integer module (unbounded integers) 67 as well as bounded integers. *) 68 69 module type INTTYPE_ARB = 70 sig 71 val size : int 72 val is_signed : bool 73 val arbitrary : bool 74 end 75 76 (* The following functor works for unbounded integers as well as for bounded 77 intergers. *) 78 79 module Make_Arb (IntType: INTTYPE_ARB) : S = 90 module Make (IntType: INTTYPE) : S = 80 91 struct 81 92 … … 90 101 let two = succ_big_int unit_big_int 91 102 92 let half_bound = power_int_positive_int 2 (size-1) 93 94 (* The upper bound of signed integers. *) 95 let shbound = half_bound 96 (* The lower bound of signed integers. *) 97 let slbound = minus_big_int half_bound 98 99 (* The upper bound of unsigned integers. *) 100 let uhbound = mult_int_big_int 2 half_bound 101 (* The lower bound of unsigned integers. *) 102 let ulbound = zero 103 104 (* [unsign a] returns the unsigned value of [a]. *) 105 let unsign a = 106 if lt_big_int a zero_big_int then add_big_int uhbound a 107 else a 108 109 (* [is_in_repr a] returns true iff [a] is a value comprised in the interval of 110 representation. *) 111 let is_in_repr a = 112 if IntType.is_signed then (le_big_int slbound a) && (lt_big_int a shbound) 113 else (le_big_int ulbound a) && (lt_big_int a uhbound) 103 (* Integers will all be taken modulo the following value. *) 104 let _mod = power_int_positive_int 2 size 105 106 (* The lower bound (inclusive). *) 107 let lower_bound = zero 108 (* The upper bound (inclusive). *) 109 let upper_bound = pred_big_int _mod 114 110 115 111 (* [cast a] returns a modulo of [a] such that the result fits in the interval 116 112 of representation. *) 117 let cast a = 118 if IntType.arbitrary then a 119 else 120 if is_in_repr a then a 121 else 122 if IntType.is_signed then 123 sub_big_int 124 (mod_big_int (add_big_int a half_bound) uhbound) 125 half_bound 126 else mod_big_int a uhbound 113 let cast a = mod_big_int a _mod 114 115 (* Half bound (exclusive), i.e. upper bound of signed integers. *) 116 let half_bound = power_int_positive_int 2 (size-1) 117 118 (* Signed value of [a]. *) 119 let signed a = sub_big_int (cast a) half_bound 120 121 let signed_op op a b = op (signed a) (signed b) 127 122 128 123 let succ a = cast (succ_big_int a) … … 130 125 let add a b = cast (add_big_int a b) 131 126 132 (* [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the 133 unsigned value of [i2] overflows. *) 134 let add_of a b = 135 let u1 = unsign a in 136 let u2 = unsign b in 137 let i = add_big_int u1 u2 in 138 ge_big_int i uhbound 127 (* [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *) 128 let add_of a b = gt_big_int (add_big_int a b) upper_bound 139 129 140 130 let sub a b = cast (sub_big_int a b) 141 131 142 (* [sub_of i1 i2] returns true iff substracting the unsigned value of [i1] and 143 the unsigned value of [i2] underflows. *) 144 let sub_of a b = 145 let u1 = unsign a in 146 let u2 = unsign b in 147 let i = sub_big_int u1 u2 in 148 lt_big_int i zero_big_int 132 let cast_op op a b = op (cast a) (cast b) 149 133 150 134 let mul a b = cast (mult_big_int a b) 151 let div a b = cast (div_big_int a b) 152 let modulo a b = cast (mod_big_int a b) 135 let div a b = cast (signed_op div_big_int a b) 136 let divu a b = cast_op div_big_int a b 137 let modulo a b = cast (signed_op mod_big_int a b) 138 let modulou a b = cast_op mod_big_int a b 139 153 140 let eq = eq_big_int 154 141 let neq a b = not (eq a b) 155 let lt a b = lt_big_int (cast a) (cast b) 156 let le a b = le_big_int (cast a) (cast b) 157 let gt a b = gt_big_int (cast a) (cast b) 158 let ge a b = ge_big_int (cast a) (cast b) 142 let lt a b = signed_op lt_big_int a b 143 let le a b = signed_op le_big_int a b 144 let gt a b = signed_op gt_big_int a b 145 let ge a b = signed_op ge_big_int a b 146 let ltu a b = cast_op lt_big_int a b 147 let leu a b = cast_op le_big_int a b 148 let gtu a b = cast_op gt_big_int a b 149 let geu a b = cast_op ge_big_int a b 150 151 (* [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] underflows. *) 152 let sub_uf a b = lt_big_int (sub_big_int a b) zero 153 159 154 let of_int i = cast (big_int_of_int i) 160 let to_int i = int_of_big_int i 155 let to_int i = int_of_big_int (cast i) 156 161 157 let neg a = cast (minus_big_int a) 162 158 163 let lognot a = 164 let mone = minus_big_int unit_big_int in 165 if IntType.is_signed then sub mone a 166 else sub (pred uhbound) a 159 let lognot = sub upper_bound 167 160 168 161 let shl a b = 169 let pow = power_int_positive_big_int 2 bin162 let pow = power_int_positive_big_int 2 (cast b) in 170 163 cast (mult_big_int a pow) 171 164 172 165 let shr a b = 173 let pow = power_int_positive_big_int 2 b in 174 cast (div_big_int a pow) 175 176 let shrl a b = 166 let a = cast a in 167 let b = cast b in 177 168 let added = 178 if IntType.is_signed || (lt_big_int b half_bound) then zero_big_int169 if lt_big_int a half_bound then zero 179 170 else half_bound in 180 171 let rec aux acc b = 181 if eq _big_int b zero_big_intthen acc172 if eq b zero then acc 182 173 else 183 let cont_acc = add _big_int added (div_big_intacc two) in184 let cont_b = pred _big_intb in174 let cont_acc = add added (divu acc two) in 175 let cont_b = pred b in 185 176 aux cont_acc cont_b 186 177 in 187 178 cast (aux a b) 179 180 let shrl a b = 181 let pow = power_int_positive_big_int 2 (cast b) in 182 cast (div_big_int (cast a) pow) 188 183 189 184 let max a b = if lt a b then b else a 190 185 let min a b = if gt a b then b else a 191 192 let is_odd a = eq_big_int (mod_big_int a two) unit_big_int 193 (* [to_bits a] returns the list of bits (0 or 1) that a represents. Signed 194 integers are represented using the 2-complement representation. *) 186 let maxu a b = if ltu a b then b else a 187 let minu a b = if gtu a b then b else a 188 189 let is_odd a = eq (modulou a two) one 190 (* [to_bits a] returns the list of bits (0 or 1) that [a] represents. *) 195 191 let to_bits a = 196 192 let rec aux acc a i = 197 193 if i >= size then acc 198 else aux ((is_odd a) :: acc) (div _big_inta two) (i+1)199 in 200 aux [] a0194 else aux ((is_odd a) :: acc) (divu a two) (i+1) 195 in 196 aux [] (cast a) 0 201 197 202 198 (* [from_bits bits] returns the integer that the list of bits [bits] 203 represents. Signed integers are represented using the 2-complement 204 representation. *) 199 represents. *) 205 200 let from_bits bits = 206 201 let rec aux acc = function 207 202 | [] -> acc 208 203 | b :: bits -> 209 let next_acc = mul t_int_big_int 2 accin210 let next_acc = if b then succ _big_intnext_acc else next_acc in204 let next_acc = mul acc two in 205 let next_acc = if b then succ next_acc else next_acc in 211 206 aux next_acc bits 212 207 in 213 cast (aux zero_big_int bits)208 aux zero bits 214 209 215 210 (* [binary_log_op f a b] applies the binary boolean operation [f] … … 224 219 let logxor = binary_log_op xor 225 220 221 222 (* [zero_ext n a] performs zero extension on [a] where [n] bits are 223 significant. *) 224 let zero_ext n a = 225 let pow2 = power_int_positive_int 2 n in 226 cast (mod_big_int a pow2) 227 228 (* [sign_ext n a] performs sign extension on [a] where [n] bits are 229 significant. *) 230 let sign_ext n a = 231 let a' = zero_ext n a in 232 let pow2 = power_int_positive_int 2 (n-1) in 233 let sign = divu a pow2 in 234 if is_odd sign then 235 let added = shr half_bound (of_int (n-1)) in 236 add a' added 237 else a' 238 239 226 240 (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element 227 241 is the high bits, and the last is the low bits. *) 228 242 let break a n = 229 let chunk_size = (8 * IntType.size)/ n in243 let chunk_size = size / n in 230 244 let pow2_chunk_size = power_int_positive_int 2 chunk_size in 231 245 let rec aux acc a i = 232 246 if i = 0 then acc 233 247 else 234 let (next, chunk) = Big_int.quomod_big_int a pow2_chunk_size in248 let (next, chunk) = quomod_big_int a pow2_chunk_size in 235 249 aux ((cast chunk) :: acc) next (i-1) 236 250 in 237 aux [] an251 aux [] (cast a) n 238 252 239 253 (* [merge l] creates the integer where the first element of [l] is its high … … 244 258 let al = List.rev al in 245 259 let nb_chunks = List.length al in 246 let chunk_size = (8 * IntType.size)/ nb_chunks in260 let chunk_size = size / nb_chunks in 247 261 let pow2_chunk_size = power_int_positive_int 2 chunk_size in 248 262 let rec aux pow2 = function … … 255 269 256 270 257 module Make (IntType : INTTYPE) = 258 Make_Arb (struct include IntType let arbitrary = false end) 259 260 261 module Int8s : S = Make 262 (struct 263 let size = 1 264 let is_signed = true 265 end) 266 267 module Int8u : S = Make 268 (struct 269 let size = 1 270 let is_signed = false 271 end) 272 273 module Int16s : S = Make 274 (struct 275 let size = 2 276 let is_signed = true 277 end) 278 279 module Int16u : S = Make 280 (struct 281 let size = 2 282 let is_signed = false 283 end) 284 285 module Int32 : S = Make 286 (struct 287 let size = 4 288 let is_signed = true 289 end) 290 291 module Integer : S = Make_Arb 292 (struct 293 let size = 1 294 let is_signed = true 295 let arbitrary = true 296 end) 297 298 299 type int8s = Int8s.t 300 type int8u = Int8u.t 301 type int16s = Int16s.t 302 type int16u = Int16u.t 303 type int32 = Int32.t 304 type integer = Integer.t 271 module Int8 : S = Make (struct let size = 1 end) 272 module Int16 : S = Make (struct let size = 2 end) 273 module Int32 : S = Make (struct let size = 4 end) 274 275 type int8 = Int8.t 276 type int16 = Int16.t 277 type int32 = Int32.t -
Deliverables/D2.2/8051/src/common/intValue.mli
r486 r619 1 1 2 (** This module defines functions to manipulate integers coded on various number3 of bits (sized integers). *)2 (** This module defines functions to manipulate bounded integers. They can be 3 used to represent sequences of bits. *) 4 4 5 5 (* Integers, whatever their size, will be represented using the Big_int … … 9 9 type int_repr = Big_int.big_int 10 10 11 (* The parameter module. Sized integers are characterized by the number of bits12 used to represent them, and the fact that they are signed or not. *)11 (* The parameter module. Bounded integers are characterized by the number of 12 bits used to represent them. *) 13 13 14 14 module type INTTYPE = 15 15 sig 16 val size : int (* in bytes *) 17 val is_signed : bool 16 val size : int (* in bytes *) 18 17 end 19 18 20 (* The signature provided to manipulate sized integers. *)19 (* The signature provided to manipulate bounded integers. *) 21 20 22 21 module type S = sig … … 29 28 val one : t 30 29 31 val succ : t -> t 32 val pred : t -> t 33 val add : t -> t -> t 34 (** [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the 35 unsigned value of [i2] overflows. *) 36 val add_of : t -> t -> bool 37 val sub : t -> t -> t 38 (** [sub_of i1 i2] returns true iff substracting the unsigned value of [i1] 39 and the unsigned value of [i2] overflows. *) 40 val sub_of : t -> t -> bool 41 val mul : t -> t -> t 42 val div : t -> t -> t 43 val modulo : t -> t -> t 44 val eq : t -> t -> bool 45 val neq : t -> t -> bool 46 val lt : t -> t -> bool 47 val le : t -> t -> bool 48 val gt : t -> t -> bool 49 val ge : t -> t -> bool 50 val neg : t -> t 51 val lognot : t -> t 52 val logand : t -> t -> t 53 val logor : t -> t -> t 54 val logxor : t -> t -> t 55 val shl : t -> t -> t 56 val shr : t -> t -> t 57 val shrl : t -> t -> t 58 val max : t -> t -> t 59 val min : t -> t -> t 60 val cast : int_repr -> t 61 val of_int : int -> t 62 val to_int : t -> int 30 val succ : t -> t 31 val pred : t -> t 32 val add : t -> t -> t 33 (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *) 34 val add_of : t -> t -> bool 35 val sub : t -> t -> t 36 (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] 37 underflows. *) 38 val sub_uf : t -> t -> bool 39 val mul : t -> t -> t 40 val div : t -> t -> t 41 val divu : t -> t -> t 42 val modulo : t -> t -> t 43 val modulou : t -> t -> t 44 val eq : t -> t -> bool 45 val neq : t -> t -> bool 46 val lt : t -> t -> bool 47 val ltu : t -> t -> bool 48 val le : t -> t -> bool 49 val leu : t -> t -> bool 50 val gt : t -> t -> bool 51 val gtu : t -> t -> bool 52 val ge : t -> t -> bool 53 val geu : t -> t -> bool 54 val neg : t -> t 55 val lognot : t -> t 56 val logand : t -> t -> t 57 val logor : t -> t -> t 58 val logxor : t -> t -> t 59 val shl : t -> t -> t 60 val shr : t -> t -> t 61 val shrl : t -> t -> t 62 val max : t -> t -> t 63 val maxu : t -> t -> t 64 val min : t -> t -> t 65 val minu : t -> t -> t 66 val cast : int_repr -> t 67 val of_int : int -> t 68 val to_int : t -> int 69 70 (** [zero_ext n a] performs zero extension on [a] where [n] bits are 71 significant. *) 72 val zero_ext : int -> t -> t 73 (** [sign_ext n a] performs sign extension on [a] where [n] bits are 74 significant. *) 75 val sign_ext : int -> t -> t 63 76 64 77 (** [break i n] cuts [i] in [n] parts. In the resulting list, the first … … 71 84 end 72 85 73 (** The functor to create bounded integers from a size and a signedness. *)86 (** The functor to create bounded integers from a size. *) 74 87 75 88 module Make: functor (IntType: INTTYPE) -> S 76 89 90 module Int8 : S 91 module Int16 : S 92 module Int32 : S 93 94 type int8 = Int8.t 95 type int16 = Int16.t 96 type int32 = Int32.t 97 98 99 (* 77 100 module Int8s : S 78 101 module Int8u : S … … 90 113 type int32 = Int32.t 91 114 type integer = Integer.t 115 *) -
Deliverables/D2.2/8051/src/common/memory.ml
r486 r619 192 192 | Some alignment when (size <= alignment) && (is_multiple size alignment) -> 193 193 let size = Offset.of_int size in 194 let rem = Offset.modulo off size in194 let rem = Offset.modulou off size in 195 195 if Offset.eq rem Offset.zero then off 196 196 else Offset.add off (Offset.sub size rem) 197 197 | Some alignment -> 198 198 let size = Offset.of_int alignment in 199 let rem = Offset.modulo off size in199 let rem = Offset.modulou off size in 200 200 if Offset.eq rem Offset.zero then off 201 201 else Offset.add off (Offset.sub size rem) … … 263 263 (* Pretty printing *) 264 264 265 let print mem =265 let print mem = 266 266 let print_cells off = function 267 267 | Datum (size, v) when Value.eq v Value.undef -> … … 275 275 match content with 276 276 | Contents contents -> 277 278 279 277 Printf.printf "(%s -> %s)%!" 278 (Offset.to_string contents.low) (Offset.to_string contents.high) ; 279 OffsetMap.iter print_cells contents.cells 280 280 | Fun_def _ -> Printf.printf "function definition%!" ; 281 281 in 282 282 BlockMap.iter print_block mem.blocks ; 283 283 Printf.printf "\n%!" 284 285 286 284 287 285 … … 405 403 all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont] 406 404 405 let string_of_alignment = function 406 | None -> "none" 407 | Some alignment -> string_of_int alignment 408 407 409 (** [write_value msg mem b off size v size'] store the value [v] at the offset 408 410 [off] of the block [b] in the memory [mem]. [size] is the size of the -
Deliverables/D2.2/8051/src/common/memory.mli
r486 r619 108 108 (int list (* resulting offsets *) * int (* full size *)) 109 109 110 val size_of_datas 110 val size_of_datas : AST.data list -> int 111 111 112 112 (** [offsets_of_datas datas] returns the aligned offsets for the datas … … 114 114 val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list 115 115 116 val alloc_datas 117 116 val alloc_datas : 'fun_def memory -> AST.data list -> 117 ('fun_def memory * Value.t) 118 118 119 119 val print : 'fun_def memory -> unit -
Deliverables/D2.2/8051/src/common/value.ml
r486 r619 103 103 val add_and_of : t -> t -> (t * t) 104 104 val add : t -> t -> t 105 (** [add_of v1 v2] returns the 1value if the sum of [v1] and [v2]106 overflows, and 0otherwise. *)105 (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2] 106 overflows, and [0] otherwise. *) 107 107 val add_of : t -> t -> t 108 108 (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether 109 this substraction overflows. *)110 val sub_and_ of : t -> t -> (t * t)109 this substraction underflows. *) 110 val sub_and_uf : t -> t -> (t * t) 111 111 val sub : t -> t -> t 112 (** [sub_of v1 v2] returns the 1value if the substraction of [v1] and [v2]113 overflows, and 0otherwise. *)114 val sub_ of : t -> t -> t112 (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2] 113 underflows, and [0] otherwise. *) 114 val sub_uf : t -> t -> t 115 115 val mul : t -> t -> t 116 116 val div : t -> t -> t 117 117 val divu : t -> t -> t 118 118 val modulo : t -> t -> t 119 val modu 119 val modulou : t -> t -> t 120 120 val and_op : t -> t -> t 121 121 val or_op : t -> t -> t … … 166 166 (* This module will be used to represent integer values. *) 167 167 module Int = 168 IntValue.Make (struct let size = D.int_size let is_signed = true end) 169 170 (* This module will be used to define unsigned operations on integer 171 values. *) 172 module Intu = 173 IntValue.Make (struct let size = D.int_size let is_signed = false end) 168 IntValue.Make (struct let size = D.int_size end) 174 169 175 170 (* Addresses are represented by a block, i.e. a base address, and an offset … … 183 178 184 179 module Block = 185 IntValue.Make (struct let size = D.ptr_size let is_signed = trueend)180 IntValue.Make (struct let size = D.ptr_size end) 186 181 module Offset = (* Block *) 187 IntValue.Make (struct let size = D.ptr_size let is_signed = trueend)182 IntValue.Make (struct let size = D.ptr_size end) 188 183 189 184 (* We want to be able to put an address into registers, and we want to be able … … 226 221 | _, Val_ptrl _ -> -1 227 222 223 (* 228 224 let hash = function 229 225 | Val_int i -> Int.to_int i … … 232 228 | Val_ptr (b,o) 233 229 | Val_ptrh (b,o) 234 | Val_ptrl (b,o) -> Integer.to_int (Integer.add b o) 230 | Val_ptrl (b,o) -> Int.to_int (Int.add b o) 231 *) 232 233 let hash = Hashtbl.hash 235 234 236 235 let equal a b = compare a b = 0 … … 315 314 | _ -> Val_undef 316 315 317 (** [cast8unsigned v] returns undefined for non-integer values. For integer 318 values, it supposes that the value is a 8 bit unsigned integer. It will 319 return the integer value that represents the same quantity, but using 320 every bits (2-completement representation). The other cast operations 321 behave the same way. *) 322 323 let cast8unsigned = cast Int8u.cast 324 let cast8signed = cast Int8s.cast 325 let cast16unsigned = cast Int16u.cast 326 let cast16signed = cast Int16s.cast 327 let cast32 = cast Int32.cast 316 (** Sign or 0 extensions from various bounded integers. *) 317 let cast8unsigned = cast (Int.zero_ext 8) 318 let cast8signed = cast (Int.sign_ext 8) 319 let cast16unsigned = cast (Int.zero_ext 16) 320 let cast16signed = cast (Int.sign_ext 16) 321 let cast32 = cast (Int.zero_ext 32) 328 322 329 323 … … 335 329 | Val_int i1, Val_int i2 -> Val_int (f i1 i2) 336 330 | _ -> Val_undef 337 338 let binary_intu_op f v1 v2 = match v1, v2 with339 | Val_int i1, Val_int i2 ->340 Val_int (Int.cast (f (Intu.cast i1) (Intu.cast i2)))341 | _, _ -> Val_undef342 343 let binary_int_cmp f v1 v2 = match v1, v2 with344 | Val_int i1, Val_int i2 -> of_bool (f i1 i2)345 | _, _ -> Val_undef346 347 let binary_intu_cmp f v1 v2 = match v1, v2 with348 | Val_int i1, Val_int i2 ->349 of_bool (f (Intu.cast i1) (Intu.cast i2))350 | _, _ -> Val_undef351 331 352 332 let unary_float_op f = function … … 431 411 let succ v = add v (Val_int Int.one) 432 412 433 (** [sub_and_ of v1 v2] returns the substraction of [v1] and [v2], and whether434 this substraction overflows. *)435 let sub_and_ of v1 v2 = match v1, v2 with413 (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether 414 this substraction underflows. *) 415 let sub_and_uf v1 v2 = match v1, v2 with 436 416 | Val_int i1, Val_int i2 -> 437 (Val_int (Int.sub i1 i2), of_bool (Int.sub_ of i1 i2))417 (Val_int (Int.sub i1 i2), of_bool (Int.sub_uf i1 i2)) 438 418 | Val_ptr (b, off), Val_int i -> 439 419 (Val_ptr (b, Offset.sub off i), 440 of_bool (Offset.sub_ of off (Offset.cast i)))420 of_bool (Offset.sub_uf off (Offset.cast i))) 441 421 | Val_ptrh (b, off), Val_int i -> 442 422 (Val_ptrh (b, Offset.sub off i), 443 of_bool (Offset.sub_ of off (Offset.cast i)))423 of_bool (Offset.sub_uf off (Offset.cast i))) 444 424 | Val_ptrl (b, off), Val_int i -> 445 425 (Val_ptrl (b, Offset.sub off i), 446 of_bool (Offset.sub_ of off (Offset.cast i)))426 of_bool (Offset.sub_uf off (Offset.cast i))) 447 427 | Val_ptr (b1, off1), Val_ptr (b2, off2) 448 428 | Val_ptrh (b1, off1), Val_ptrh (b2, off2) 449 429 | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 -> 450 430 (Val_int (Int.cast (Offset.sub off1 off2)), 451 of_bool (Offset.sub_ of off1 off2))431 of_bool (Offset.sub_uf off1 off2)) 452 432 | _, _ -> (Val_undef, Val_undef) 453 433 454 let sub v1 v2 = fst (sub_and_ of v1 v2)455 let sub_ of v1 v2 = snd (sub_and_of v1 v2)434 let sub v1 v2 = fst (sub_and_uf v1 v2) 435 let sub_uf v1 v2 = snd (sub_and_uf v1 v2) 456 436 457 437 let pred v = sub v (Val_int Int.one) … … 471 451 let divu v1 v2 = 472 452 if is_zero v2 then Val_undef 473 else binary_int u_op Intu.divv1 v2453 else binary_int_op Int.divu v1 v2 474 454 475 455 let modulo v1 v2 = … … 477 457 else binary_int_op Int.modulo v1 v2 478 458 479 let modu v1 v2 =459 let modulou v1 v2 = 480 460 if is_zero v2 then Val_undef 481 else binary_int u_op Intu.modulov1 v2461 else binary_int_op Int.modulou v1 v2 482 462 483 463 let and_op = binary_int_op Int.logand … … 503 483 | _ -> Val_undef 504 484 505 let cmp p_eq f_intv1 v2 = match v1, v2 with485 let cmp f_int f_ptr v1 v2 = match v1, v2 with 506 486 | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2) 507 487 | Val_ptr (b1, off1), Val_ptr (b2, off2) 508 488 | Val_ptrh (b1, off1), Val_ptrh (b2, off2) 509 | Val_ptrl (b1, off1), Val_ptrl (b2, off2) -> 510 of_bool ((Block.eq b1 b2) && (Offset.eq off1 off2)) 511 | _ -> Val_undef 512 513 let cmpp_ne cmp_eq v1 v2 = notbool (cmp_eq v1 v2) 514 515 let cmpp_lt f_int v1 v2 = match v1, v2 with 516 | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2) 517 | Val_ptr (b1, off1), Val_ptr (b2, off2) 518 | Val_ptrh (b1, off1), Val_ptrh (b2, off2) 519 | Val_ptrl (b1, off1), Val_ptrl (b2, off2) -> 520 of_bool ((Block.lt b1 b2) || 521 ((Block.eq b1 b2) && (Offset.lt off1 off2))) 522 | _ -> Val_undef 523 524 let cmpp_ge cmp_lt v1 v2 = notbool (cmp_lt v1 v2) 525 let cmpp_le cmp_lt cmp_eq v1 v2 = orbool (cmp_lt v1 v2) (cmp_eq v1 v2) 526 let cmpp_gt cmp_le v1 v2 = notbool (cmp_le v1 v2) 527 528 let cmp_eq = cmpp_eq Int.eq 529 let cmp_ne = cmpp_ne cmp_eq 530 let cmp_lt = cmpp_lt Int.lt 531 let cmp_ge = cmpp_ge cmp_lt 532 let cmp_le = cmpp_le cmp_lt cmp_eq 533 let cmp_gt = cmpp_gt cmp_le 534 535 let cmp_eq_u = cmpp_eq Intu.eq 536 let cmp_ne_u = cmpp_ne cmp_eq_u 537 let cmp_lt_u = cmpp_lt Intu.lt 538 let cmp_ge_u = cmpp_ge cmp_lt_u 539 let cmp_le_u = cmpp_le cmp_lt_u cmp_eq_u 540 let cmp_gt_u = cmpp_gt cmp_le_u 489 | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 -> 490 of_bool (f_ptr off1 off2) 491 | _ -> Val_undef 492 493 let cmp_eq = cmp Int.eq Offset.eq 494 let cmp_ne = cmp Int.neq Offset.neq 495 let cmp_lt = cmp Int.lt Offset.lt 496 let cmp_ge = cmp Int.ge Offset.ge 497 let cmp_le = cmp Int.le Offset.le 498 let cmp_gt = cmp Int.gt Offset.gt 499 500 let cmp_eq_u = cmp Int.eq Offset.eq 501 let cmp_ne_u = cmp Int.neq Offset.neq 502 let cmp_lt_u = cmp Int.ltu Offset.ltu 503 let cmp_ge_u = cmp Int.geu Offset.geu 504 let cmp_le_u = cmp Int.leu Offset.leu 505 let cmp_gt_u = cmp Int.gtu Offset.gtu 541 506 542 507 let cmp_eq_f = binary_float_cmp (=) -
Deliverables/D2.2/8051/src/common/value.mli
r486 r619 64 64 val undef : t 65 65 66 (** [cast8unsigned v] returns undefined for non-integer values. For integer 67 values, it supposes that the value is a 8 bit unsigned integer. It will 68 return the integer value that represents the same quantity, but using 69 every bits. The other cast operations behave the same way. *) 66 67 (** Sign or 0 extensions from various bounded integers. *) 70 68 val cast8unsigned : t -> t 71 69 val cast8signed : t -> t … … 96 94 val add_and_of : t -> t -> (t * t) 97 95 val add : t -> t -> t 98 (** [add_of v1 v2] returns the 1value if the sum of [v1] and [v2]99 overflows, and 0otherwise. *)96 (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2] 97 overflows, and [0] otherwise. *) 100 98 val add_of : t -> t -> t 101 99 (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether 102 this substraction overflows. *)103 val sub_and_ of : t -> t -> (t * t)100 this substraction underflows. *) 101 val sub_and_uf : t -> t -> (t * t) 104 102 val sub : t -> t -> t 105 (** [sub_of v1 v2] returns the 1value if the substraction of [v1] and [v2]106 overflows, and 0otherwise. *)107 val sub_ of : t -> t -> t103 (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2] 104 underflows, and [0] otherwise. *) 105 val sub_uf : t -> t -> t 108 106 val mul : t -> t -> t 109 107 val div : t -> t -> t 110 108 val divu : t -> t -> t 111 109 val modulo : t -> t -> t 112 val modu 110 val modulou : t -> t -> t 113 111 val and_op : t -> t -> t 114 112 val or_op : t -> t -> t -
Deliverables/D2.2/8051/src/dev_test.ml
r486 r619 9 9 10 10 let f filename = 11 12 ASMInterpret.parse_and_interpret_hex filename 13 14 (* 11 let target = Languages.Clight in 15 12 let print = false in 16 let interpret = false in 17 let labelize = false in 18 let target = Languages.ASM in 13 let interpret = true in 19 14 let p = Languages.parse Languages.Clight filename in 20 let p = if labelize then Languages.labelize p else p in15 let p = Languages.labelize p in 21 16 let ps = Languages.compile false Languages.Clight target p in 22 17 let f f' p = match Languages.language_of_ast p with … … 24 19 | _ -> () 25 20 in 26 if print then List.iter (f (Languages.save f ilename)) ps ;27 if interpret then List.iter (f (fun p -> ignore (Languages.interpret p))) ps28 *) 21 if print then List.iter (f (Languages.save false filename)) ps ; 22 if interpret then 23 List.iter (f (fun p -> ignore (Languages.interpret true p))) ps 29 24 in 30 25 -
Deliverables/D2.2/8051/src/languages.ml
r486 r619 199 199 (* FIXME *) 200 200 let instrument costs_mapping = function 201 | AstClight p -> 202 AstClight (ClightAnnotator.instrument p costs_mapping) 201 | AstClight p -> 202 let (p', cost_incr) = ClightAnnotator.instrument p costs_mapping in 203 (AstClight p', cost_incr) 203 204 | AstCminor p -> 204 AstCminor (CminorAnnotator.instrument p costs_mapping) 205 let (p', cost_incr) = CminorAnnotator.instrument p costs_mapping in 206 (AstCminor p', cost_incr) 205 207 | p -> 206 208 Error.warning "during instrumentation" … … 208 210 "Instrumentation is not implemented for source language `%s'." 209 211 (to_string (language_of_ast p))); 210 p212 (p, "") 211 213 212 214 let annotate input_ast final = … … 232 234 ASMPrinter.print_program p 233 235 234 let save filename ast = 235 let output_filename = 236 Misc.SysExt.alternative 237 (Filename.chop_extension filename 238 ^ "." ^ extension (language_of_ast ast)) 239 in 236 let save exact_output filename ast = 237 let ext_chopped_filename = 238 if exact_output then filename 239 else 240 try Filename.chop_extension filename 241 with Invalid_argument ("Filename.chop_extension") -> filename in 242 let ext_filename = 243 ext_chopped_filename ^ "." ^ extension (language_of_ast ast) in 244 let output_filename = 245 if exact_output then ext_filename 246 else Misc.SysExt.alternative ext_filename in 240 247 let cout = open_out output_filename in 241 248 output_string cout (string_output ast); … … 243 250 close_out cout 244 251 245 let interpret = function 252 let save_cost_incr filename cost_incr = 253 let cout = open_out (filename ^ ".cerco") in 254 output_string cout cost_incr; 255 flush cout; 256 close_out cout 257 258 let interpret print_result = function 246 259 | AstClight p -> 247 ClightInterpret.interpret falsep260 ClightInterpret.interpret print_result p 248 261 | AstCminor p -> 249 CminorInterpret.interpret falsep262 CminorInterpret.interpret print_result p 250 263 | AstRTLabs p -> 251 RTLabsInterpret.interpret p 264 RTLabsInterpret.interpret print_result p 252 265 | AstRTL p -> 253 RTLInterpret.interpret p 266 RTLInterpret.interpret print_result p 254 267 | AstERTL p -> 255 ERTLInterpret.interpret p 268 ERTLInterpret.interpret print_result p 256 269 | AstLTL p -> 257 LTLInterpret.interpret p 270 LTLInterpret.interpret print_result p 258 271 | AstLIN p -> 259 LINInterpret.interpret p 272 LINInterpret.interpret print_result p 260 273 | AstASM p -> 261 ASMInterpret.interpret p 274 ASMInterpret.interpret print_result p -
Deliverables/D2.2/8051/src/languages.mli
r486 r619 61 61 val labelize : ast -> ast 62 62 63 (** [annotate input_ast target_ast] inserts cost annotations into the 64 input AST from the (final) target AST. *) 65 val annotate : ast -> ast -> ast 63 (** [annotate input_ast target_ast] inserts cost annotations into the input AST 64 from the (final) target AST. It also returns the name of the cost increment 65 function *) 66 val annotate : ast -> ast -> (ast * string) 66 67 67 (** [interpret ast] runs the program [ast] from the default initial 68 configuration. This interpretation may emit some cost labels. *) 69 val interpret : ast -> CostLabel.t list 68 (** [interpret print_result ast] runs the program [ast] from the default initial 69 configuration. This interpretation may emit some cost labels. If 70 [print_result] is [true], then the result of the interpretations is 71 output. *) 72 val interpret : bool -> ast -> AST.trace 70 73 71 74 (** {2 Serialization} *) 72 75 73 (** [save filename input_ast] pretty prints [input_ast] in a fresh 74 file whose name is prefixed by [filename] and whose extension 75 is deduced from the language of the AST. *) 76 val save : string -> ast -> unit 76 (** [save exact_output filename input_ast] pretty prints [input_ast] in a file 77 whose name is prefixed by [filename] and whose extension is deduced from the 78 language of the AST. If [exact_output] is false then the written file will 79 be fresh. *) 80 val save : bool -> string -> ast -> unit 81 82 (** [save_cost_incr filename cost_incr] prints the name of the cost increment 83 function [cost_incr] in the file prefixed by [filename] and extended with 84 ".cost". If the file already exists, it is overwritten. *) 85 val save_cost_incr : string -> string -> unit 77 86 78 87 (** [from_string s] parses [s] as an intermediate language name. *) -
Deliverables/D2.2/8051/src/options.ml
r486 r619 28 28 let input_files () = !input_files 29 29 30 let output_files = ref None 31 let set_output_files s = output_files := Some s 32 let get_output_files () = !output_files 33 30 34 let annotation_flag = ref false 31 35 let request_annotation = (:=) annotation_flag … … 39 43 let set_debug = (:=) debug_flag 40 44 let is_debug_enabled () = !debug_flag 45 46 let print_result_flag = ref false 47 let set_print_result = (:=) print_result_flag 48 let is_print_result_enabled () = !print_result_flag 41 49 42 50 let dev_test = ref false … … 64 72 " Debugging mode."; 65 73 74 "-o", Arg.String set_output_files, 75 " Prefix of the output files."; 76 77 "-res", Arg.Set print_result_flag, 78 " Print the result of interpretations."; 79 66 80 "-dev", Arg.Set dev_test, 67 81 " Playground for developers."; -
Deliverables/D2.2/8051/src/options.mli
r486 r619 21 21 val input_files : unit -> string list 22 22 23 (** {2 Output files} *) 24 val set_output_files : string -> unit 25 val get_output_files : unit -> string option 26 23 27 (** {2 Verbose mode} *) 24 28 val is_debug_enabled : unit -> bool 25 29 30 (** {2 Print results requests} *) 31 val is_print_result_enabled : unit -> bool 32 26 33 (** {2 Developers' playground} *) 27 34 val is_dev_test_enabled : unit -> bool -
Deliverables/D2.2/8051/src/utilities/miscPottier.ml
r486 r619 32 32 aux 0 l 33 33 34 let rec last = function 35 | [] -> raise Not_found 36 | [a] -> a 37 | _ :: l -> last l 38 34 39 (* [split a i] splits the list a in two lists: one with the elements 35 40 up until the [i]th (exclusive) and one with the rest. *) … … 40 45 let (l1, l2) = split (List.tl l) (i-1) in 41 46 ((List.hd l) :: l1, l2) 47 48 (* [split_last l] returns the list [l] without its last element and its last 49 element. Raises Invalid_argument "MiscPottier.split_last" if the list is 50 empty. *) 51 52 let split_last l = match split l ((List.length l) - 1) with 53 | l', last :: _ -> (l', last) 54 | _ -> raise (Invalid_argument "MiscPottier.split_last") 42 55 43 56 let rec update_list_assoc a b = function -
Deliverables/D2.2/8051/src/utilities/miscPottier.mli
r486 r619 6 6 val index_of : 'a -> 'a list -> int 7 7 8 val foldi : (int -> 'a -> 'b -> 'a) -> 'a -> 'b list -> 'a8 val foldi : (int -> 'a -> 'b -> 'a) -> 'a -> 'b list -> 'a 9 9 10 val iteri : (int -> 'a -> unit) -> 'a list -> unit10 val iteri : (int -> 'a -> unit) -> 'a list -> unit 11 11 12 val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list12 val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list 13 13 14 (* [split a i] splits the list a in two lists: one with the elements 14 (* Raises Not_found if the list is empty. *) 15 val last : 'a list -> 'a 16 17 (* [split l i] splits the list [l] in two lists: one with the elements 15 18 up until the [i]th (exclusive) and one with the rest. *) 16 19 17 20 val split: 'a list -> int -> ('a list * 'a list) 21 22 (* [split_last l] returns the list [l] without its last element and its last 23 element. Raises Invalid_argument "MiscPottier.split_last" if the list is 24 empty. *) 25 26 val split_last : 'a list -> ('a list * 'a) 18 27 19 28 val update_list_assoc: 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list -
Deliverables/D2.2/8051/tests/clight/array.c
r486 r619 39 39 } 40 40 41 main(){41 int main(){ 42 42 int t[10] = {1,2,3,4,5,6,7,8,9,0}; 43 43 int a = array_local(); … … 45 45 int c = array_param(t,2,3); 46 46 return a+b+c; //19 47 // return b;47 // return b; 48 48 }
Note: See TracChangeset
for help on using the changeset viewer.