4a5c677 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add 'idris_crash'

This is to abort immediately in the case of partial functions, and is primarily to allow partial functions on primitives to have more useful run time behaviour - an explicit crash is better than undefined behaviour (as we've had up to now) with an inevitable unpredictable crash or inexplicable behaviour. Now used in strHead, strTail and strIndex, which were the main culprits, and used for Debug.Error.error instead of an unsafePerformIO

commit4a5c6779e3992d8bb287f11c4adb2254916b32bd authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 8 Dec 2016, 19:15 (10 years ago) parent280810b

8 files changed+40−14

compare with master

unifiedsplit

libs/prelude/Builtins.idr+4 libs/prelude/Prelude/Strings.idr+19−14 rts/idris_rts.c+5 rts/idris_rts.h+3 src/IRTS/CodegenC.hs+1 src/IRTS/Compiler.hs+5 src/IRTS/Lang.hs+2 src/Idris/AbsSyntaxTree.hs+1

libs/prelude/Builtins.idr+4

@@ -178,6 +178,10 @@ assert_total x = x

178178assert_unreachable : a

179179-- compiled as primitive

180180

181+||| Abort immediately with an error message

182+idris_crash : String -> a

183+-- compiled as primitive

184+

181185||| Subvert the type checker. This function is abstract, so it will not reduce in

182186||| the type checker. Use it with care - it can result in segfaults or worse!

183187export

libs/prelude/Prelude/Strings.idr+19−14

@@ -45,7 +45,8 @@ foldl1 f (x::xs) = foldl f x xs

4545||| ```

4646partial

4747strHead : String -> Char

48−strHead = prim__strHead

48+strHead "" = idris_crash "Prelude.Strings: attempt to take the head of an empty string"

49+strHead x = prim__strHead x

4950

5051||| Returns the characters specified after the head of the string.

5152|||

@@ -59,7 +60,8 @@ strHead = prim__strHead

5960||| ```

6061partial

6162strTail : String -> String

62−strTail = prim__strTail

63+strTail "" = idris_crash "Prelude.Strings: attempt to take the tail of an empty string"

64+strTail xs = prim__strTail xs

6365

6466||| Adds a character to the front of the specified string.

6567|||

@@ -72,6 +74,18 @@ strTail = prim__strTail

7274strCons : Char -> String -> String

7375strCons = prim__strCons

7476

77+||| Returns the length of the string.

78+|||

79+||| ```idris example

80+||| length ""

81+||| ```

82+||| ```idris example

83+||| length "ABC"

84+||| ```

85+length : String -> Nat

86+length = fromInteger . prim__zextInt_BigInt . prim_lenString

87+

88+

7589||| Returns the nth character (starting from 0) of the specified string.

7690|||

7791||| Precondition: '0 < i < length s' for 'strIndex s i'.

@@ -81,7 +95,9 @@ strCons = prim__strCons

8195||| ```

8296partial

8397strIndex : String -> Int -> Char

84−strIndex = prim__strIndex

98+strIndex x i = if (i < 0 || i >= cast (length x))

99+ then idris_crash "Prelude.Strings: String index out of bounds"

100+ else prim__strIndex x i

85101

86102||| Reverses the elements within a String.

87103|||

@@ -297,17 +313,6 @@ unlines' (l::ls) = l ++ '\n' :: unlines' ls

297313unlines : List String -> String

298314unlines = pack . unlines' . map unpack

299315

300−||| Returns the length of the string.

301−|||

302−||| ```idris example

303−||| length ""

304−||| ```

305−||| ```idris example

306−||| length "ABC"

307−||| ```

308−length : String -> Nat

309−length = fromInteger . prim__zextInt_BigInt . prim_lenString

310−

311316||| Returns a substring of a given string

312317|||

313318||| @ index The (zero based) index of the string to extract. If this is

rts/idris_rts.c+5

@@ -595,6 +595,11 @@ VAL idris_readStr(VM* vm, FILE* h) {

595595 return ret;

596596}

597597

598+void idris_crash(char* msg) {

599+ fprintf(stderr, "%s\n", msg);

600+ exit(1);

601+}

602+

598603VAL idris_strHead(VM* vm, VAL str) {

599604 return idris_strIndex(vm, str, 0);

600605}

rts/idris_rts.h+3

@@ -364,6 +364,9 @@ VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data);

364364VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset);

365365VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data);

366366

367+// Crash with a message (used for partial primitives)

368+void idris_crash(char* msg);

369+

367370// String primitives

368371VAL idris_concat(VM* vm, VAL l, VAL r);

369372VAL idris_strlt(VM* vm, VAL l, VAL r);

src/IRTS/CodegenC.hs+1

@@ -617,6 +617,7 @@ doOp v (LIntCh ITNative) args = v ++ creg (last args)

617617doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args

618618

619619doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

620+doOp v LCrash [x] = "idris_crash(GETSTR(" ++ creg x ++ "))"

620621doOp v LNoOp args = v ++ creg (last args)

621622

622623-- Pointer primitives (declared as %extern in Builtins.idr)

src/IRTS/Compiler.hs+5

@@ -260,6 +260,11 @@ irTerm top vs env tm@(App _ f a) = do

260260 | u == txt "assert_unreachable"

261261 -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top

262262

263+ (P _ (UN u) _, [_, msg])

264+ | u == txt "idris_crash"

265+ -> do msg' <- irTerm top vs env msg

266+ return $ LOp LCrash [msg']

267+

263268 -- TMP HACK - until we get inlining.

264269 (P _ (UN r) _, [_, _, _, _, _, arg])

265270 | r == txt "replace"

src/IRTS/Lang.hs+2

@@ -92,6 +92,8 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

9292 | LPar -- evaluate argument anywhere, possibly on another

9393 -- core or another machine. 'id' is a valid implementation

9494 | LExternal Name

95+ | LCrash

96+

9597 | LNoOp

9698 deriving (Show, Eq, Generic)

9799

src/Idris/AbsSyntaxTree.hs+1

@@ -336,6 +336,7 @@ primDefs = [ sUN "unsafePerformPrimIO"

336336 , sUN "mkForeignPrim"

337337 , sUN "void"

338338 , sUN "assert_unreachable"

339+ , sUN "idris_crash"

339340 ]

340341

341342-- information that needs writing for the current module's .ibc file