Check sizes of buffers and strings in TTCs

They need to be positive or we can't make the buffer, which causes a
segfault. This happened when loading old TTCs with a different format.
Fixes #1503

libs/base/Data/Buffer.idr

@@ -34,8 +34,10 @@ prim__newBuffer : Int -> PrimIO Buffer
 export
 newBuffer : HasIO io => Int -> io (Maybe Buffer)
 newBuffer size
-    = do buf <- primIO (prim__newBuffer size)
-         pure $ Just buf
+    = if size >= 0
+            then do buf <- primIO (prim__newBuffer size)
+                    pure $ Just buf
+                 else pure Nothing
 --          if prim__nullAnyPtr buf /= 0
 --             then pure Nothing
 --             else pure $ Just $ MkBuffer buf size 0

src/Libraries/Utils/Binary.idr

@@ -222,6 +222,7 @@ TTC String where
   fromBuf b
       = do len <- fromBuf {a = Int} b
            chunk <- get Bin
+           when (len < 0) $ corrupt "String"
            if toRead chunk >= len
               then
                 do val <- coreLift $ getString (buf chunk) (loc chunk) len
@@ -252,7 +253,7 @@ TTC Binary where
          if toRead chunk >= len
             then
               do Just newbuf <- coreLift $ newBuffer len
-                      | Nothing => throw (InternalError "Can't create buffer")
+                      | Nothing => corrupt "Binary"
                  coreLift $ copyData (buf chunk) (loc chunk) len
                                      newbuf 0
                  put Bin (incLoc len chunk)

tests/Main.idr

@@ -123,7 +123,8 @@ idrisTestsRegression = MkTestPool "Various regressions" [] Nothing
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
        "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
-       "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042"]
+       "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042",
+       "reg043"]
 
 idrisTestsData : TestPool
 idrisTestsData = MkTestPool "Data and record types" [] Nothing

tests/idris2/reg043/TestFake.idr

@@ -0,0 +1 @@
+import Fake

tests/idris2/reg043/expected

@@ -0,0 +1,2 @@
+1/1: Building TestFake (TestFake.idr)
+Error: Error in TTC file: Corrupt TTC data for String (the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files)

tests/idris2/reg043/run

@@ -0,0 +1,6 @@
+mkdir -p build/ttc
+echo "TT2This Is A Fake TTC" > build/ttc/Fake.ttc
+
+$1 --no-color --console-width 0 --check TestFake.idr
+
+rm -rf build