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

2 files changed, 15 insertions, 14 deletions

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 4710167e..5847cecb 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -368,8 +368,8 @@ function unit incrementCP0Count() = {
   (* XXX Sail does not allow reading fields here :-( *)
   let (bit[32])status = CP0Status in
   let (bit[32])cause  = CP0Cause in
-  let (bit[8]) ims = (status[15..8]) in
-  let (bit[8]) ips = (cause[15..8]) in
+  let (bit[8]) ims = status[15..8] in
+  let (bit[8]) ips = cause[15..8] in
   let ie           = status[0] in
   let exl          = status[1] in
   let erl          = status[2] in
@@ -379,14 +379,14 @@ function unit incrementCP0Count() = {
 
 function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = 
       let entryVal   = (bit[117]) entry in
-      let entryValid = (entryVal[62]) in
-      let entryR     = (entryVal[100..99]) in
-      let entryMask  = (entryVal[116..101]) in
-      let entryVPN   = (entryVal[98..72]) in
-      let entryASID  = (entryVal[71..64]) in
-      let entryG     = (entryVal[63]) in
-      ((entryValid) &
-       (r == (entryR)) & 
+      let entryValid = entryVal[62] in
+      let entryR     = entryVal[100..99] in
+      let entryMask  = entryVal[116..101] in
+      let entryVPN   = entryVal[98..72] in
+      let entryASID  = entryVal[71..64] in
+      let entryG     = entryVal[63] in
+      (entryValid &
+       (r == entryR) & 
        ((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) &
        ((asid == (entryASID)) | (entryG)))
 
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index dccbe090..0abc6220 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -13,6 +13,9 @@ open import Instruction_extractor
 
 type tannot = Interp_utilities.tannot
 
+val debug_print : string -> unit
+declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
+
 val intern_annot : tannot -> tannot
 let intern_annot annot =
   match annot with
@@ -579,7 +582,8 @@ let access_vector v n =
     | V_lit (L_aux L_undef _) -> v
     | V_lit (L_aux L_zero _) -> v
     | V_lit (L_aux L_one _ ) -> v
-    | V_vector m dir vs -> 
+    | V_vector m dir vs ->
+      (*let _ = debug_print ("access_vector given " ^ string_of_value v ^ " where dir was " ^ (if is_inc(dir) then "increasing" else "decreaseing") ^ " and start is " ^ show m ^ " and index is " ^ show n ^ "\n") in*)
       list_nth vs (if is_inc(dir) then (n - m) else (m - n))
     | V_vector_sparse _ _ _ vs d ->
       match (List.lookup n vs) with
@@ -1054,9 +1058,6 @@ let fix_up_nondet typ branches annot =
       (fun e -> E_aux (E_assign (LEXP_aux (LEXP_id redex_id) annot) e) annot) branches), Just "0")
 end
 
-val debug_print : string -> unit
-declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
-
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv
 let rec match_pattern t_level (P_aux p (_, annot)) value_whole =