diff options
| -rw-r--r-- | mips/run_embed.ml | 20 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.ml | 261 | ||||
| -rw-r--r-- | src/pretty_print_ocaml.ml | 7 |
3 files changed, 277 insertions, 11 deletions
diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 8ddbd8d1..183e2ff1 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -142,7 +142,7 @@ module MIPS_model : ISA_model = struct type ast = Mips_embed._ast let init_model () = - let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x9000000040000000")) in + let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in set_register Mips_embed._nextPC start_addr; set_register_field_bit Mips_embed._CP0Status "BEV" Vone @@ -155,7 +155,7 @@ module MIPS_model : ISA_model = struct | 0 -> let pc_vaddr = unsigned_big(Mips_embed._PC) in let npc_addr = add_int_big_int 4 pc_vaddr in - let npc_vec = to_vec_dec_big (big_int_of_int 64, npc_addr) in + let npc_vec = to_vec_dec_big (bi64, npc_addr) in set_register Mips_embed._nextPC npc_vec; | 1 -> set_register Mips_embed._nextPC Mips_embed._delayedPC; @@ -168,7 +168,7 @@ module MIPS_model : ISA_model = struct Some (unsigned_big(Mips_embed._TranslatePC(Mips_embed._PC))) with Sail_exit -> None - let get_opcode pc_a = Mips_embed._reverse_endianness(_MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4)) + let get_opcode pc_a = Mips_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4)) let decode = Mips_embed._decode @@ -185,7 +185,7 @@ module CHERI_model : ISA_model = struct type ast = Cheri_embed._ast let init_model () = - let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x9000000040000000")) in + let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in set_register Cheri_embed._nextPC start_addr; set_register_field_bit Cheri_embed._CP0Status "BEV" Vone; let initial_cap_val_int = big_int_of_string "0x100000000fffffffe00000000000000000000000000000000ffffffffffffffff" in @@ -207,7 +207,7 @@ module CHERI_model : ISA_model = struct | 0 -> let pc_vaddr = unsigned_big(Cheri_embed._PC) in let npc_addr = add_int_big_int 4 pc_vaddr in - let npc_vec = to_vec_dec_big (big_int_of_int 64, npc_addr) in + let npc_vec = to_vec_dec_big (bi64, npc_addr) in set_register Cheri_embed._nextPC npc_vec; | 1 -> begin @@ -223,7 +223,7 @@ module CHERI_model : ISA_model = struct Some (unsigned_big(Cheri_embed._TranslatePC(Cheri_embed._PC))) with Sail_exit -> None - let get_opcode pc_a = Cheri_embed._reverse_endianness(_MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4)) + let get_opcode pc_a = Cheri_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4)) let decode = Cheri_embed._decode @@ -242,11 +242,11 @@ module CHERI128_model : ISA_model = struct type ast = Cheri128_embed._ast let init_model () = - let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x9000000040000000")) in + let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in set_register Cheri128_embed._nextPC start_addr; set_register_field_bit Cheri128_embed._CP0Status "BEV" Vone; let initial_cap_val_int = big_int_of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *) - let initial_cap_vec = to_vec_dec ((big_int_of_int 129), initial_cap_val_int) in + let initial_cap_vec = to_vec_dec ((bi129), initial_cap_val_int) in set_register Cheri128_embed._PCC initial_cap_vec; set_register Cheri128_embed._nextPCC initial_cap_vec; set_register Cheri128_embed._delayedPCC initial_cap_vec; @@ -264,7 +264,7 @@ module CHERI128_model : ISA_model = struct | 0 -> let pc_vaddr = unsigned_big(Cheri128_embed._PC) in let npc_addr = add_int_big_int 4 pc_vaddr in - let npc_vec = to_vec_dec_big (big_int_of_int 64, npc_addr) in + let npc_vec = to_vec_dec_big (bi64, npc_addr) in set_register Cheri128_embed._nextPC npc_vec; | 1 -> begin @@ -280,7 +280,7 @@ module CHERI128_model : ISA_model = struct Some (unsigned_big(Cheri128_embed._TranslatePC(Cheri128_embed._PC))) with Sail_exit -> None - let get_opcode pc_a = Cheri128_embed._reverse_endianness(_MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4)) + let get_opcode pc_a = Cheri128_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4)) let decode = Cheri128_embed._decode diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 41c1fd6a..9b394d3a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -1236,3 +1236,264 @@ let slice_raw (v, i, j) = Vvector (bits, (if is_inc then 0 else len - 1), is_inc) | _ -> failwith "slice_raw only implemented for VVector" let _slice_raw = slice_raw + +(* enough literal big ints to account for most literals found in specs *) +(* for i = 0 to 257 do Printf.printf "let bi%d = big_int_of_int %d\n" i i done;; *) +let bi0 = zero_big_int +let bi1 = unit_big_int +let bi2 = big_int_of_int 2 +let bi3 = big_int_of_int 3 +let bi4 = big_int_of_int 4 +let bi5 = big_int_of_int 5 +let bi6 = big_int_of_int 6 +let bi7 = big_int_of_int 7 +let bi8 = big_int_of_int 8 +let bi9 = big_int_of_int 9 +let bi10 = big_int_of_int 10 +let bi11 = big_int_of_int 11 +let bi12 = big_int_of_int 12 +let bi13 = big_int_of_int 13 +let bi14 = big_int_of_int 14 +let bi15 = big_int_of_int 15 +let bi16 = big_int_of_int 16 +let bi17 = big_int_of_int 17 +let bi18 = big_int_of_int 18 +let bi19 = big_int_of_int 19 +let bi20 = big_int_of_int 20 +let bi21 = big_int_of_int 21 +let bi22 = big_int_of_int 22 +let bi23 = big_int_of_int 23 +let bi24 = big_int_of_int 24 +let bi25 = big_int_of_int 25 +let bi26 = big_int_of_int 26 +let bi27 = big_int_of_int 27 +let bi28 = big_int_of_int 28 +let bi29 = big_int_of_int 29 +let bi30 = big_int_of_int 30 +let bi31 = big_int_of_int 31 +let bi32 = big_int_of_int 32 +let bi33 = big_int_of_int 33 +let bi34 = big_int_of_int 34 +let bi35 = big_int_of_int 35 +let bi36 = big_int_of_int 36 +let bi37 = big_int_of_int 37 +let bi38 = big_int_of_int 38 +let bi39 = big_int_of_int 39 +let bi40 = big_int_of_int 40 +let bi41 = big_int_of_int 41 +let bi42 = big_int_of_int 42 +let bi43 = big_int_of_int 43 +let bi44 = big_int_of_int 44 +let bi45 = big_int_of_int 45 +let bi46 = big_int_of_int 46 +let bi47 = big_int_of_int 47 +let bi48 = big_int_of_int 48 +let bi49 = big_int_of_int 49 +let bi50 = big_int_of_int 50 +let bi51 = big_int_of_int 51 +let bi52 = big_int_of_int 52 +let bi53 = big_int_of_int 53 +let bi54 = big_int_of_int 54 +let bi55 = big_int_of_int 55 +let bi56 = big_int_of_int 56 +let bi57 = big_int_of_int 57 +let bi58 = big_int_of_int 58 +let bi59 = big_int_of_int 59 +let bi60 = big_int_of_int 60 +let bi61 = big_int_of_int 61 +let bi62 = big_int_of_int 62 +let bi63 = big_int_of_int 63 +let bi64 = big_int_of_int 64 +let bi65 = big_int_of_int 65 +let bi66 = big_int_of_int 66 +let bi67 = big_int_of_int 67 +let bi68 = big_int_of_int 68 +let bi69 = big_int_of_int 69 +let bi70 = big_int_of_int 70 +let bi71 = big_int_of_int 71 +let bi72 = big_int_of_int 72 +let bi73 = big_int_of_int 73 +let bi74 = big_int_of_int 74 +let bi75 = big_int_of_int 75 +let bi76 = big_int_of_int 76 +let bi77 = big_int_of_int 77 +let bi78 = big_int_of_int 78 +let bi79 = big_int_of_int 79 +let bi80 = big_int_of_int 80 +let bi81 = big_int_of_int 81 +let bi82 = big_int_of_int 82 +let bi83 = big_int_of_int 83 +let bi84 = big_int_of_int 84 +let bi85 = big_int_of_int 85 +let bi86 = big_int_of_int 86 +let bi87 = big_int_of_int 87 +let bi88 = big_int_of_int 88 +let bi89 = big_int_of_int 89 +let bi90 = big_int_of_int 90 +let bi91 = big_int_of_int 91 +let bi92 = big_int_of_int 92 +let bi93 = big_int_of_int 93 +let bi94 = big_int_of_int 94 +let bi95 = big_int_of_int 95 +let bi96 = big_int_of_int 96 +let bi97 = big_int_of_int 97 +let bi98 = big_int_of_int 98 +let bi99 = big_int_of_int 99 +let bi100 = big_int_of_int 100 +let bi101 = big_int_of_int 101 +let bi102 = big_int_of_int 102 +let bi103 = big_int_of_int 103 +let bi104 = big_int_of_int 104 +let bi105 = big_int_of_int 105 +let bi106 = big_int_of_int 106 +let bi107 = big_int_of_int 107 +let bi108 = big_int_of_int 108 +let bi109 = big_int_of_int 109 +let bi110 = big_int_of_int 110 +let bi111 = big_int_of_int 111 +let bi112 = big_int_of_int 112 +let bi113 = big_int_of_int 113 +let bi114 = big_int_of_int 114 +let bi115 = big_int_of_int 115 +let bi116 = big_int_of_int 116 +let bi117 = big_int_of_int 117 +let bi118 = big_int_of_int 118 +let bi119 = big_int_of_int 119 +let bi120 = big_int_of_int 120 +let bi121 = big_int_of_int 121 +let bi122 = big_int_of_int 122 +let bi123 = big_int_of_int 123 +let bi124 = big_int_of_int 124 +let bi125 = big_int_of_int 125 +let bi126 = big_int_of_int 126 +let bi127 = big_int_of_int 127 +let bi128 = big_int_of_int 128 +let bi129 = big_int_of_int 129 +let bi130 = big_int_of_int 130 +let bi131 = big_int_of_int 131 +let bi132 = big_int_of_int 132 +let bi133 = big_int_of_int 133 +let bi134 = big_int_of_int 134 +let bi135 = big_int_of_int 135 +let bi136 = big_int_of_int 136 +let bi137 = big_int_of_int 137 +let bi138 = big_int_of_int 138 +let bi139 = big_int_of_int 139 +let bi140 = big_int_of_int 140 +let bi141 = big_int_of_int 141 +let bi142 = big_int_of_int 142 +let bi143 = big_int_of_int 143 +let bi144 = big_int_of_int 144 +let bi145 = big_int_of_int 145 +let bi146 = big_int_of_int 146 +let bi147 = big_int_of_int 147 +let bi148 = big_int_of_int 148 +let bi149 = big_int_of_int 149 +let bi150 = big_int_of_int 150 +let bi151 = big_int_of_int 151 +let bi152 = big_int_of_int 152 +let bi153 = big_int_of_int 153 +let bi154 = big_int_of_int 154 +let bi155 = big_int_of_int 155 +let bi156 = big_int_of_int 156 +let bi157 = big_int_of_int 157 +let bi158 = big_int_of_int 158 +let bi159 = big_int_of_int 159 +let bi160 = big_int_of_int 160 +let bi161 = big_int_of_int 161 +let bi162 = big_int_of_int 162 +let bi163 = big_int_of_int 163 +let bi164 = big_int_of_int 164 +let bi165 = big_int_of_int 165 +let bi166 = big_int_of_int 166 +let bi167 = big_int_of_int 167 +let bi168 = big_int_of_int 168 +let bi169 = big_int_of_int 169 +let bi170 = big_int_of_int 170 +let bi171 = big_int_of_int 171 +let bi172 = big_int_of_int 172 +let bi173 = big_int_of_int 173 +let bi174 = big_int_of_int 174 +let bi175 = big_int_of_int 175 +let bi176 = big_int_of_int 176 +let bi177 = big_int_of_int 177 +let bi178 = big_int_of_int 178 +let bi179 = big_int_of_int 179 +let bi180 = big_int_of_int 180 +let bi181 = big_int_of_int 181 +let bi182 = big_int_of_int 182 +let bi183 = big_int_of_int 183 +let bi184 = big_int_of_int 184 +let bi185 = big_int_of_int 185 +let bi186 = big_int_of_int 186 +let bi187 = big_int_of_int 187 +let bi188 = big_int_of_int 188 +let bi189 = big_int_of_int 189 +let bi190 = big_int_of_int 190 +let bi191 = big_int_of_int 191 +let bi192 = big_int_of_int 192 +let bi193 = big_int_of_int 193 +let bi194 = big_int_of_int 194 +let bi195 = big_int_of_int 195 +let bi196 = big_int_of_int 196 +let bi197 = big_int_of_int 197 +let bi198 = big_int_of_int 198 +let bi199 = big_int_of_int 199 +let bi200 = big_int_of_int 200 +let bi201 = big_int_of_int 201 +let bi202 = big_int_of_int 202 +let bi203 = big_int_of_int 203 +let bi204 = big_int_of_int 204 +let bi205 = big_int_of_int 205 +let bi206 = big_int_of_int 206 +let bi207 = big_int_of_int 207 +let bi208 = big_int_of_int 208 +let bi209 = big_int_of_int 209 +let bi210 = big_int_of_int 210 +let bi211 = big_int_of_int 211 +let bi212 = big_int_of_int 212 +let bi213 = big_int_of_int 213 +let bi214 = big_int_of_int 214 +let bi215 = big_int_of_int 215 +let bi216 = big_int_of_int 216 +let bi217 = big_int_of_int 217 +let bi218 = big_int_of_int 218 +let bi219 = big_int_of_int 219 +let bi220 = big_int_of_int 220 +let bi221 = big_int_of_int 221 +let bi222 = big_int_of_int 222 +let bi223 = big_int_of_int 223 +let bi224 = big_int_of_int 224 +let bi225 = big_int_of_int 225 +let bi226 = big_int_of_int 226 +let bi227 = big_int_of_int 227 +let bi228 = big_int_of_int 228 +let bi229 = big_int_of_int 229 +let bi230 = big_int_of_int 230 +let bi231 = big_int_of_int 231 +let bi232 = big_int_of_int 232 +let bi233 = big_int_of_int 233 +let bi234 = big_int_of_int 234 +let bi235 = big_int_of_int 235 +let bi236 = big_int_of_int 236 +let bi237 = big_int_of_int 237 +let bi238 = big_int_of_int 238 +let bi239 = big_int_of_int 239 +let bi240 = big_int_of_int 240 +let bi241 = big_int_of_int 241 +let bi242 = big_int_of_int 242 +let bi243 = big_int_of_int 243 +let bi244 = big_int_of_int 244 +let bi245 = big_int_of_int 245 +let bi246 = big_int_of_int 246 +let bi247 = big_int_of_int 247 +let bi248 = big_int_of_int 248 +let bi249 = big_int_of_int 249 +let bi250 = big_int_of_int 250 +let bi251 = big_int_of_int 251 +let bi252 = big_int_of_int 252 +let bi253 = big_int_of_int 253 +let bi254 = big_int_of_int 254 +let bi255 = big_int_of_int 255 +let bi256 = big_int_of_int 256 +let bi257 = big_int_of_int 257 diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index fb6dd99f..c8c0bb86 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -127,7 +127,12 @@ let doc_lit_ocaml in_pat (L_aux(l,_)) = | L_one -> "Vone" | L_true -> "Vone" | L_false -> "Vzero" - | L_num i -> "(big_int_of_int (" ^ (string_of_int i) ^ "))" + | L_num i -> + let s = string_of_int i in + if (i >= 0) && (i <= 257) then + "bi" ^ s + else + "(big_int_of_int (" ^ s ^ "))" | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) | L_undef -> "failwith \"undef literal not supported\"" (* XXX Undef vectors get handled with to_vec_undef. We could support undef bit but would need to check type. For the moment treat as runtime error. *) |