define some big_int literals in sail_values.ml to avoid lots of calls to bit_int_of_int. Likely very little performance benefit but slightly more readable.

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.  *)