Bugfixes and testing new checker on the MIPS spec

5 files changed, 60 insertions, 37 deletions

diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index d127f6db..d85ba0a5 100644
--- a/mips_new_tc/mips_insts.sail
+++ b/mips_new_tc/mips_insts.sail
@@ -1544,9 +1544,9 @@ function clause execute (MTC0(rt, rd, sel, double)) = {
       case _               -> (SignalException(ResI))
     }
 }
-
+(*
 function unit TLBWriteEntry((TLBIndexT) idx) = {
-  pagemask := EXTZ(TLBPageMask); (* XXX EXTZ here forces register read in ocaml shallow embedding *)
+  pagemask := (bit[16]) (EXTZ(TLBPageMask)); (* XXX EXTZ here forces register read in ocaml shallow embedding *)
   switch(pagemask) {
       case 0x0000 -> ()
       case 0x0003 -> ()
@@ -1578,7 +1578,7 @@ function unit TLBWriteEntry((TLBIndexT) idx) = {
   ((TLBEntries[idx]).d1      ) := TLBEntryLo1.D;
   ((TLBEntries[idx]).v1      ) := TLBEntryLo1.V;
 }
-
+*)
 union ast member TLBWI
 function clause decode (0b010000 : 0b10000000000000000000 : 0b000010) = Some(TLBWI)
 function clause execute (TLBWI) = {
diff --git a/mips_new_tc/mips_tlb.sail b/mips_new_tc/mips_tlb.sail
index 6a0cddd6..99e6eac5 100644
--- a/mips_new_tc/mips_tlb.sail
+++ b/mips_new_tc/mips_tlb.sail
@@ -46,10 +46,6 @@ function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
        ((vpn2 & ~((bit[27]) (EXTZ(entryMask)))) == ((entryVPN) & ~((bit[27]) (EXTZ(entryMask))))) &
        ((asid == (entryASID)) | (entryG)))
 
-val forall Type 'a. 'a -> option<'a> effect pure Some
-
-val forall Type 'a. unit -> option<'a> effect pure None
-
 function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
   let r    = (VAddr[63..62]) in
   let vpn2 = (VAddr[39..13]) in
@@ -58,7 +54,7 @@ function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
       if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then
 	return (Some ((TLBIndexT) (to_vec(idx))))
     };
-    None()
+    None
   }
 
 function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
@@ -68,7 +64,7 @@ function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessT
     let entry = (TLBEntries[idx]) in
     let entryMask = entry.pagemask in
 
-    let evenOddBit = switch(entryMask) {
+    let evenOddBit = ([|12:28|]) switch((bit[16])(entryMask)) {
       case 0x0000 -> 12
       case 0x0003 -> 14
       case 0x000f -> 16
@@ -81,43 +77,64 @@ function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessT
       case _      -> undefined
     } in
     let isOdd = (vAddr[evenOddBit]) in
-    let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then
-        (entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1)
+    let (caps, capl, pfn, d, v) = if (isOdd) then
+	((bit[1]) (entry.caps1), (bit[1]) (entry.capl1), (bit[24]) (entry.pfn1), (bit[1]) (entry.d1), (bit[1]) (entry.v1))
       else
-        (entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in
+	((bit[1]) (entry.caps0), (bit[1]) (entry.capl0), (bit[24]) (entry.pfn0), (bit[1]) (entry.d0), (bit[1]) (entry.v0)) in
     if (~(v)) then
       (SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
     else if ((accessType == StoreData) & ~(d)) then
       (SignalExceptionTLB(TLBMod, vAddr))
     else
-      (EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]), 
-       if (accessType == StoreData) then caps else capl)
+      let res = (bit[64]) switch evenOddBit {
+	case ([:12:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:14:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:16:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:18:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:20:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:22:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:24:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:26:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:28:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+      } in
+      (res, (bool) (if (accessType == StoreData) then caps else capl)) (* FIXME: get rid of explicit cast here *)
     case None ->  (SignalExceptionTLB(
       if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
   }
 }
 
+val cast AccessLevel -> [|0:2|] effect pure cast_AccessLevel
+
+function [|0:2|] cast_AccessLevel level =
+{
+  switch level {
+    case User -> 0
+    case Supervisor -> 1
+    case Kernel -> 2
+  }
+}
+
 (* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag *)
 function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) = 
   {
     let currentAccessLevel = getAccessLevel() in
     let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
-    let (requiredLevel, addr) = switch(vAddr[63..62]) {
-      case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *)
-        case (true, 0b11) -> (Kernel, None)               (* kseg3 mapped 32-bit compat *)
-        case (true, 0b10) -> (Supervisor, None)           (* sseg  mapped 32-bit compat *)
-        case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
-        case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
-        case (_, _) -> (Kernel, None) (* xkseg mapped *)
+    let (requiredLevel, addr) = ((AccessLevel, option<bit[64]>)) switch((bit[2]) (vAddr[63..62])) {
+      case 0b11 -> switch(compat32, (bit[2]) (vAddr[30..29])) { (* xkseg *)
+	case (true, 0b11) -> (Kernel, (option<bit[64]>) None)               (* kseg3 mapped 32-bit compat *)
+	case (true, 0b10) -> (Supervisor, (option<bit[64]>) None)           (* sseg  mapped 32-bit compat *)
+	case (true, 0b01) -> (Kernel, Some((bit[64]) (EXTZ(vAddr[28..0])))) (* kseg1 unmapped uncached 32-bit compat *)
+	case (true, 0b00) -> (Kernel, Some((bit[64]) (EXTZ(vAddr[28..0])))) (* kseg0 unmapped cached 32-bit compat *)
+	case (_, _) -> (Kernel, (option<bit[64]>) None) (* xkseg mapped *)
       }
-      case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0])))       (* xkphys bits 61-59 are cache mode (ignored) *)
-      case 0b01 -> (Supervisor, None)                       (* xsseg - supervisor mapped *)
-      case 0b00 -> (User, None) (* xuseg - user mapped *)
+      case 0b10 -> (Kernel, Some((bit[64]) (EXTZ(vAddr[58..0]))))       (* xkphys bits 61-59 are cache mode (ignored) *)
+      case 0b01 -> (Supervisor, (option<bit[64]>) None)                       (* xsseg - supervisor mapped *)
+      case 0b00 -> (User, (option<bit[64]>) None) (* xuseg - user mapped *)
     } in
     if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
       (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
-    else 
-      let (pa, c) = switch(addr) {
+    else
+      let (pa, c) = ((bit[64], bool)) switch(addr) {
       case (Some(a)) -> (a, false)
       case None      -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
           (SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
diff --git a/src/process_file.ml b/src/process_file.ml
index 42d1402b..2425a9bb 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -92,7 +92,7 @@ let opt_new_typecheck = ref false
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
 let opt_dno_cast = ref false
-                                        
+
 let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs =
   let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
                 Type_internal.nabbrevs = Envmap.empty;
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index e87a6bd2..d60d8280 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -1317,13 +1317,16 @@ let rec instantiate_quants quants kid uvar = match quants with
        | _ -> (QI_aux (QI_const nc, l)) :: instantiate_quants quants kid uvar
      end
 
-let destructure_vec_typ l = function
-  | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _);
-                           Typ_arg_aux (Typ_arg_nexp n2, _);
-                           Typ_arg_aux (Typ_arg_order o, _);
-                           Typ_arg_aux (Typ_arg_typ vtyp, _)]
-                     ), _) when string_of_id id = "vector" -> (n1, n2, o, vtyp)
-  | typ -> typ_error l ("Expected vector type, got " ^ string_of_typ typ)
+let destructure_vec_typ l env typ =
+  let destructure_vec_typ' l = function
+    | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _);
+                             Typ_arg_aux (Typ_arg_nexp n2, _);
+                             Typ_arg_aux (Typ_arg_order o, _);
+                             Typ_arg_aux (Typ_arg_typ vtyp, _)]
+                       ), _) when string_of_id id = "vector" -> (n1, n2, o, vtyp)
+    | typ -> typ_error l ("Expected vector type, got " ^ string_of_typ typ)
+  in
+  destructure_vec_typ' l (Env.expand_synonyms env typ)
 
 let typ_of (E_aux (_, (_, tannot))) = match tannot with
   | Some (_, typ, _) -> typ
@@ -1536,7 +1539,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      annot_exp_effect (E_exit checked_exp) typ (mk_effect [BE_escape])
   | E_vector vec, _ ->
      begin
-       let (start, len, ord, vtyp) = destructure_vec_typ l typ in
+       let (start, len, ord, vtyp) = destructure_vec_typ l env typ in
        let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
        match len with
        | Nexp_aux (Nexp_constant lenc, _) ->
@@ -1720,9 +1723,9 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
        pats @ [inferred_pat], env
      in
      let (inferred_pat :: inferred_pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in
-     let (_, len, _, vtyp) = destructure_vec_typ l (pat_typ_of inferred_pat) in
+     let (_, len, _, vtyp) = destructure_vec_typ l env (pat_typ_of inferred_pat) in
      let fold_len len pat =
-       let (_, len', _, vtyp') = destructure_vec_typ l (pat_typ_of pat) in
+       let (_, len', _, vtyp') = destructure_vec_typ l env (pat_typ_of pat) in
        typ_equality l env vtyp vtyp';
        nsum len len'
      in
@@ -1849,6 +1852,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | Local (_, typ) | Enum typ -> annot_exp (E_id v) typ
        | Register typ -> annot_exp_effect (E_id v) typ (mk_effect [BE_rreg])
        | Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
+       | Union _ -> typ_error l ("Cannot infer the type of polymorphic union indentifier " ^ string_of_id v)
      end
   | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
   | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)])))
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index a7f02f6e..5172142d 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -16,6 +16,8 @@ mkdir -p $DIR/rtfail
 rm -f $DIR/tests.xml
 
 cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail > $DIR/pass/mips_prelude.sail
+cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail $SAILDIR/mips_new_tc/mips_tlb.sail > $DIR/pass/mips_tlb.sail
+cat $SAILDIR/lib/prelude.sail $SAILDIR/mips_new_tc/mips_prelude.sail $SAILDIR/mips_new_tc/mips_tlb.sail $SAILDIR/mips_new_tc/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail
 
 pass=0
 fail=0