From edff4ba336735bcd1c244a4bd7fc8f5c4464e91b Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 4 Apr 2017 10:34:42 +0100 Subject: Implement exit by raising Sail_exit exception --- src/gen_lib/sail_values.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index d287b2cd..86f8934a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -13,6 +13,8 @@ type value = | Vregister of vbit array ref * int * bool * (string * (int * int)) list | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*) +exception Sail_exit + let string_of_bit = function | Vone -> "1" | Vzero -> "0" @@ -37,7 +39,7 @@ let is_one i = else Vzero -let exit _ = failwith "called exit" +let exit _ = raise Sail_exit let is_one_int i = -- cgit v1.2.3 From 9c51012bc47d0a66ff898ae53359764f59816a02 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 4 Apr 2017 10:36:15 +0100 Subject: implement exts and extz as manipulations on bit vectors rather than converting to integers, allowing them to work on vectors containing undef. --- src/gen_lib/sail_values.ml | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 86f8934a..a2f1286a 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -534,11 +534,34 @@ let to_vec_dec_undef_big len = to_vec_undef_big false len let to_vec_inc_undef = to_vec_inc_undef_big let to_vec_dec_undef = to_vec_dec_undef_big -let exts_int (len, vec) = to_vec_int (get_ord vec) len (signed_int vec) -let extz_int (len, vec) = to_vec_int (get_ord vec) len (unsigned_int vec) +let exts_int (len, vec) = + let barray = get_barray(vec) in + let vlen = Array.length barray in + let arr = + if (vlen < len) then + (* copy most significant bit into new bits *) + Array.append (Array.make (len - vlen) barray.(0)) barray + else + (* truncate to least significant bits *) + Array.sub barray (vlen - len) len in + let inc = get_ord vec in + Vvector(arr, (if inc then 0 else (len - 1)), inc) + +let extz_int (len, vec) = + let barray = get_barray(vec) in + let vlen = Array.length barray in + let arr = + if (vlen < len) then + (* fill new bits with zero *) + Array.append (Array.make (len - vlen) Vzero) barray + else + (* truncate to least significant bits *) + Array.sub barray (vlen - len) len in + let inc = get_ord vec in + Vvector(arr, (if inc then 0 else (len - 1)), inc) -let exts_big (len,vec) = to_vec_big (get_ord vec) len (signed_big vec) -let extz_big (len,vec) = to_vec_big (get_ord vec) len (unsigned_big vec) +let exts_big (len,vec) = exts_int (int_of_big_int len, vec) +let extz_big (len,vec) = extz_int (int_of_big_int len, vec) let exts = exts_big let extz = extz_big -- cgit v1.2.3 From c7b9060464ead8fac71824b151c25a968cb25302 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 4 Apr 2017 10:37:10 +0100 Subject: fix incorrect use of == in eq --- src/gen_lib/sail_values.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index a2f1286a..21aa48c3 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -1146,7 +1146,7 @@ let gt_range_vec = gt_range_vec_big let lteq_range_vec = lteq_range_vec_big let gteq_range_vec = gteq_range_vec_big -let eq (l,r) = if l == r then Vone else Vzero +let eq (l,r) = if l = r then Vone else Vzero let eq_vec_vec (l,r) = eq (to_num_big true l, to_num_big true r) let eq_vec (l,r) = eq_vec_vec(l,r) let eq_vec_range (l,r) = eq (to_num_big false l,r) -- cgit v1.2.3 From b50cf34a6e700b70b12f9c4bfe81a6c0b703198b Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 5 Apr 2017 11:36:12 +0100 Subject: Print registers in test suite compatible way. --- mips/run_embed.ml | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/mips/run_embed.ml b/mips/run_embed.ml index b65f74d9..d4b46747 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -64,7 +64,23 @@ let rec foldli f acc ?(i=0) = function | x::xs -> foldli f (f i acc x) ~i:(i+1) xs;; let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;; -let big_int_to_hex i = Uint64.to_string_hex (Uint64.of_string (string_of_big_int i)) +let big_int_to_hex i = + (* annoyingly Uint64.to_string_hex prefixes the string with 0x UNLESS it is zero... *) + if i = zero_big_int then + "0" + else + let s = Uint64.to_string_hex (Uint64.of_string (string_of_big_int i)) in + let len = String.length s in + String.sub s 2 (len - 2) + +let big_int_to_hex64 i = + let hex = big_int_to_hex i in + let len = String.length hex in + if (len < 16) then + (String.make (16-len) '0') ^ hex + else + hex + let input_buf = (ref [] : int list ref);; let add_mem byte addr mem = begin @@ -295,7 +311,7 @@ let time_it action arg = (finish_time -. start_time, ret) let rec debug_print_gprs start stop = - resultf "DEBUG MIPS REG %.2d %s\n" start (big_int_to_hex (unsigned_big(vector_access Mips_model._GPR (big_int_of_int start)))); + resultf "DEBUG MIPS REG %.2d 0x%s\n" start (big_int_to_hex64 (unsigned_big(vector_access Mips_model._GPR (big_int_of_int start)))); if start < stop then debug_print_gprs (start + 1) stop else () @@ -337,6 +353,7 @@ let rec fde_loop count = if (i == Mips_model.HCF) then begin + resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex pc_vaddr); debug_print_gprs 0 31; resultf "\nSUCCESS program terminated after %d instructions\n" count; count -- cgit v1.2.3 From 83ba712a9897c1b375c1ae4cfb744f718b91c482 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 5 Apr 2017 17:31:44 +0100 Subject: Model now assumes memory is little endian so adjust extras file accordingly. --- mips/mips_extras_ml.ml | 4 ++-- mips/run_embed.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml index 1565c7c6..29f4a13d 100644 --- a/mips/mips_extras_ml.ml +++ b/mips/mips_extras_ml.ml @@ -23,7 +23,7 @@ let _MEMval (addr, size, data) = for i = 0 to (s - 1) do let bit_idx = i * 8 in let byte = unsigned_int(slice_raw (data, big_int_of_int bit_idx, big_int_of_int (bit_idx + 7))) in - let byte_addr = add_int_big_int i a in + let byte_addr = add_int_big_int (s-1-i) a in begin (*printf "MEM [%s] <- %x\n" (big_int_to_hex byte_addr) byte;*) mips_mem := Mem.add byte_addr byte !mips_mem; @@ -42,7 +42,7 @@ let _MEMr (addr, size) = begin let byte_addr = add_int_big_int i a in let byte = Mem.find byte_addr !mips_mem in let byte_vec = to_vec_dec_int (8, byte) in - ret := vector_concat (!ret) byte_vec; + ret := vector_concat byte_vec (!ret); (*printf "MEM [%s] -> %x %s %s\n" (big_int_to_hex byte_addr) byte (string_of_value byte_vec) (string_of_value !ret);*) done; ret := set_start_to_length (!ret); diff --git a/mips/run_embed.ml b/mips/run_embed.ml index d4b46747..76b1b222 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -316,7 +316,7 @@ let rec debug_print_gprs start stop = then debug_print_gprs (start + 1) stop else () -let get_opcode pc_a = _MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4) +let get_opcode pc_a = Mips_model._reverse_endianness(_MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4)) let rec fde_loop count = if !max_cut_off && count = !max_instr -- cgit v1.2.3 From 1e1b869f5c66976685901d694959dd3432597264 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 6 Apr 2017 12:25:58 +0100 Subject: minor changes in sail_values.ml to aid debugging --- src/gen_lib/sail_values.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 21aa48c3..ebde00a7 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -1,4 +1,5 @@ open Big_int_Z +open Printf (* only expected to be 0, 1, 2; 2 represents undef *) type vbit = Vone | Vzero | Vundef @@ -25,7 +26,7 @@ let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) let string_of_value = function | Vvector(bits, start, inc) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array bits) | VvectorR(values, start, inc) -> "" - | Vregister(bits, start, inc, fields) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits) + | Vregister(bits, start, inc, fields) -> "reg" ^ (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits) | Vbit(b) -> string_of_bit b let to_bool = function @@ -159,7 +160,7 @@ let set_register register value = match register,value with a := !new_v | Vregister(a,_,_,_), Vvector(new_v,_,_) -> a := new_v - | _ -> () + | _ -> failwith "set_register of non-register" let set_vector_subrange_vec_int v n m new_v = let walker array length offset new_values = -- cgit v1.2.3 From 22a5dd79b302a7da4170f58d0c54115c1d4a69ac Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 6 Apr 2017 12:28:15 +0100 Subject: add support for address translation and exit handling in mips ocaml shallow embedding test setup. --- mips/run_embed.ml | 98 ++++++++++++++++++++++++++++++------------------------- src/Makefile | 10 ++++-- 2 files changed, 62 insertions(+), 46 deletions(-) diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 76b1b222..42e36a6e 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -47,7 +47,7 @@ open Mips_extras_ml;; (* The linksem ELF interface *) open Sail_interface ;; -module Mips_model=Mips_notlb_embed;; +module Mips_model=Mips_embed;; let interact_print = ref true let result_print = ref true @@ -294,14 +294,14 @@ let initial_system_state_of_elf_file name = let max_cut_off = ref false let max_instr = ref 0 let raw_file = ref "" -let raw_at = ref 0 +let raw_at = ref "" let elf_file = ref "" let args = [ ("--file", Arg.Set_string elf_file, "filename of elf binary to load in memory"); ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop"); ("--raw", Arg.Set_string raw_file, "filename of raw file to load in memory"); - ("--at", Arg.Set_int raw_at, "address to load raw file in memory"); + ("--at", Arg.Set_string raw_at, "address to load raw file in memory"); ] let time_it action arg = @@ -318,6 +318,13 @@ let rec debug_print_gprs start stop = let get_opcode pc_a = Mips_model._reverse_endianness(_MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4)) +let get_pc () = begin + try + Some (unsigned_big(Mips_model._TranslatePC(Mips_model._PC))) + with Sail_exit -> None + end + + let rec fde_loop count = if !max_cut_off && count = !max_instr then begin @@ -327,8 +334,8 @@ let rec fde_loop count = else begin let pc_vaddr = unsigned_big(Mips_model._PC) in interactf "\n**** instruction %d from address %s ****\n" - count (big_int_to_hex pc_vaddr); - let m_paddr = Some pc_vaddr in (* XXX should be address translate *) + count (big_int_to_hex64 pc_vaddr); + let m_paddr = get_pc () in match m_paddr with | Some pc -> let inBranchDelay = Some(unsigned_int(Mips_model._inBranchDelay)) in @@ -360,43 +367,13 @@ let rec fde_loop count = end else begin - Mips_model._execute(i); - - (* - (try - let (pending, _, _) = (Unix.select [(Unix.stdin)] [] [] 0.0) in - (if (pending != []) then - let char = (input_byte stdin) in ( - errorf "Input %x\n" char; - input_buf := (!input_buf) @ [char])); - with - | _ -> ()); - - let uart_rvalid = option_int_of_reg "UART_RVALID" in - (match uart_rvalid with - | Some 0 -> - (match !input_buf with - | x :: xs -> ( - reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Sail_impl_base.D_decreasing (Nat_big_num.of_int x)) !reg; - reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg; - input_buf := xs; - ) - | [] -> ()) - | _-> ()); - - let uart_written = option_int_of_reg "UART_WRITTEN" in - (match uart_written with - | Some 1 -> - (let uart_data = option_int_of_reg "UART_WDATA" in - match uart_data with - | Some b -> (printf "%c" (Char.chr b); printf "%!") - | None -> (errorf "UART_WDATA was undef" ; exit 1)) - | _ -> ()); - reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;*) - set_register Mips_model._inBranchDelay Mips_model._branchPending; - set_register Mips_model._branchPending (to_vec_dec_int (1, 0)); - set_register Mips_model._PC Mips_model._nextPC; - fde_loop (count + 1) + (try + Mips_model._execute(i) + with Sail_exit -> ()); + set_register Mips_model._inBranchDelay Mips_model._branchPending; + set_register Mips_model._branchPending (to_vec_dec_int (1, 0)); + set_register Mips_model._PC Mips_model._nextPC; + fde_loop (count + 1) end | None -> begin (* Exception during PC translation *) set_register Mips_model._inBranchDelay Mips_model._branchPending; @@ -406,6 +383,39 @@ let rec fde_loop count = end end + + (* + (try + let (pending, _, _) = (Unix.select [(Unix.stdin)] [] [] 0.0) in + (if (pending != []) then + let char = (input_byte stdin) in ( + errorf "Input %x\n" char; + input_buf := (!input_buf) @ [char])); + with + | _ -> ()); + + let uart_rvalid = option_int_of_reg "UART_RVALID" in + (match uart_rvalid with + | Some 0 -> + (match !input_buf with + | x :: xs -> ( + reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Sail_impl_base.D_decreasing (Nat_big_num.of_int x)) !reg; + reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg; + input_buf := xs; + ) + | [] -> ()) + | _-> ()); + + let uart_written = option_int_of_reg "UART_WRITTEN" in + (match uart_written with + | Some 1 -> + (let uart_data = option_int_of_reg "UART_WDATA" in + match uart_data with + | Some b -> (printf "%c" (Char.chr b); printf "%!") + | None -> (errorf "UART_WDATA was undef" ; exit 1)) + | _ -> ()); + reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;*) + let rec load_raw_file' mem addr chan = let byte = input_byte chan in (add_mem byte addr mem; @@ -434,10 +444,10 @@ let run () = startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in *) if String.length(!raw_file) != 0 then - load_raw_file mips_mem (big_int_of_int !raw_at) (open_in_bin !raw_file); + load_raw_file mips_mem (big_int_of_string !raw_at) (open_in_bin !raw_file); set_register_field_bit Mips_model._CP0Status "BEV" Vone; printf "CP0Status: %s\n" (string_of_value Mips_model._CP0Status); - let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x40000000")) in + let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x9000000040000000")) in set_register Mips_model._PC start_addr; let name = Filename.basename !raw_file in let (t, count) = time_it fde_loop 0 in diff --git a/src/Makefile b/src/Makefile index acdd0075..e98b896b 100644 --- a/src/Makefile +++ b/src/Makefile @@ -133,6 +133,12 @@ _build/mips_notlb_embed.ml: $(MIPS_NOTLB_SAILS_PRE) ./sail.native cd _build ; \ ../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_notlb_embed $(MIPS_NOTLB_SAILS_PRE) +_build/mips_embed.ml: $(MIPS_SAILS_PRE) ./sail.native + mkdir -p _build + cd _build ; \ + ../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_embed $(MIPS_SAILS_PRE) + + _build/cheri.lem: $(CHERI_SAILS) ./sail.native mkdir -p _build cd _build ;\ @@ -175,8 +181,8 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native -run_mips_embed.native: _build/mips_notlb_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_notlb_embed.ml _build/run_embed.ml -o run_mips_embed.native +run_mips_embed.native: _build/mips_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_embed.ml _build/run_embed.ml -o run_mips_embed.native run_mips_embed.bytes: _build/mips_notlb_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml env OCAMLRUNPARAM=l=100M ocamlfind ocamlc -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cma $(LEMLIBOCAML)/extract.cma $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cma $(ELFDIR)/src/linksem.cma _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_notlb_embed.ml _build/run_embed.ml -o run_mips_embed.bytes -- cgit v1.2.3 From d716893e137a41638b449162dc8b5c682eb7f4d4 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 6 Apr 2017 12:34:49 +0100 Subject: use set_register when writing element of vector of registers to avoid accidentally replacing Vregister with Vvalue or Vregister... Seems to work for MIPS but not sure if might encounter vector of something other than bit or register. A more specific value type would have made this a compile-time error rather than run-time. --- src/pretty_print_ocaml.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index 47aacf0c..5df8691e 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -479,10 +479,13 @@ let doc_exp_ocaml, doc_let_ocaml = | _ -> (false,false) in match lexp with | LEXP_vector(v,e) -> - doc_op (string "<-") - (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml false v)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) - (exp e_new_v) + if is_bit then + doc_op (string "<-") (group (parens (string "get_barray" ^^ space ^^ doc_lexp_ocaml false v)) ^^ + dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) (exp e_new_v) + else (* XXX Check whether vector of reg? *) + parens ((string "set_register") ^^ space ^^ + ((group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v)) ^^ + dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) ^^ space ^^ (exp e_new_v))) | LEXP_vector_range(v,e1,e2) -> parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) -- cgit v1.2.3