diff options
| -rw-r--r-- | mips/mips_prelude.sail | 20 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 9 |
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 = |