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(-) (limited to 'src') 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(-) (limited to 'src') 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(-) (limited to 'src') 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 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(-) (limited to 'src') 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. --- src/Makefile | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'src') 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(-) (limited to 'src') 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