Merge branch 'master' of bitbucket.org:Peter_Sewell/sail

3 files changed, 49 insertions, 14 deletions

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
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index d287b2cd..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
@@ -13,6 +14,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"
@@ -23,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
@@ -37,7 +40,7 @@ let is_one i =
   else Vzero
 
 
-let exit _ = failwith "called exit"
+let exit _ = raise Sail_exit
 
 
 let is_one_int i =
@@ -157,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 =
@@ -532,11 +535,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
@@ -1121,7 +1147,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)
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)