Mips TLB existential example

3 files changed, 110 insertions, 1 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index b4460992..fea94a90 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2514,7 +2514,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
 
   let nc_true = nc_eq (nconstant 0) (nconstant 0) in
   let typ_ret =
-    if existentials = []
+    if KidSet.is_empty (KidSet.inter (typ_frees typ_ret) (KidSet.of_list existentials))
     then typ_ret
     else mk_typ (Typ_exist (existentials, List.fold_left nc_and nc_true ex_constraints, typ_ret))
   in
diff --git a/test/typecheck/pass/exist_simple.sail b/test/typecheck/pass/exist_simple.sail
new file mode 100644
index 00000000..87e62b13
--- /dev/null
+++ b/test/typecheck/pass/exist_simple.sail
@@ -0,0 +1,15 @@
+
+register bool reg
+
+let (exist 'n, 0 <= 'n & 'n <= 4. [:'n:]) A = 4
+
+let ([|0:4|]) B = A
+
+val unit -> exist 'n, 'n in {0, 1}. [:'n:] effect {rreg} test
+
+function test () =
+{
+  if reg
+  then 0
+  else 1
+}
diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail
new file mode 100644
index 00000000..525d29c6
--- /dev/null
+++ b/test/typecheck/pass/exist_tlb.sail
@@ -0,0 +1,94 @@
+
+(* Minimal prelude *)
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
+
+overload EXTZ [extz]
+overload EXTS [exts]
+
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+
+overload (deinfix +) [add_vec]
+
+val bool -> bool effect pure bool_not
+overload ~ [bool_not]
+
+(* MIPS spec subset *)
+
+default Order dec
+
+register (bit[1])   CP0LLBit
+register (bit[64])  CP0LLAddr
+
+typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
+
+typedef regno = bit[5]                      (* a register number *)
+typedef imm16 = bit[16]                     (* 16-bit immediate *)
+
+typedef Exception = enumerate
+{
+   Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap;
+   XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck
+}
+
+typedef WordType = enumerate {B; H; W; D}
+
+val bit[5] -> bit[64] effect {rreg} rGPR
+val (bit[64], WordType) -> bool effect pure isAddressAligned
+val forall Type 'o. (Exception, bit[64]) -> 'o effect pure SignalExceptionBadAddr
+
+val WordType -> exist 'r, 'r in {1,2,4,8}. [:'r:] effect pure wordWidthBytes
+
+function wordWidthBytes w = switch w {
+  case B -> 1
+  case H -> 2
+  case W -> 4
+  case D -> 8
+}
+
+val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_reserve_wrapper
+val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_wrapper
+val (bit[5], bit[64]) -> unit effect {wreg} wGPR
+
+function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = addr
+
+function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = vAddr
+
+scattered typedef ast = const union
+
+val ast -> unit effect {rmem, rreg, wreg} execute
+
+scattered function unit execute
+
+union ast member (WordType, bool, bool, regno, regno, imm16) Load
+
+function clause execute (Load(width, signed, linked, base, rt, offset)) =
+  {
+    (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
+    if ~ (isAddressAligned(vAddr, width)) then
+      (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *)
+    else
+      let pAddr = (TLBTranslate(vAddr, LoadData)) in
+          {
+	    (exist 't, 't in {1,2,4,8}. bit[8 * 't]) memResult := if linked then
+                {
+                  CP0LLBit  := 0b1;
+                  CP0LLAddr := pAddr;
+                  MEMr_reserve_wrapper(pAddr, wordWidthBytes(width));
+                }
+              else
+                MEMr_wrapper(pAddr, wordWidthBytes(width));
+            if (signed) then
+              wGPR(rt) := EXTS(memResult)
+            else
+              wGPR(rt) := EXTZ(memResult)
+          }
+  }
+
+end ast
+end execute