[ fix ] Fix issue with eager evaluation of crashing functions (fixes #…

…3003) (#3004)

* [ fix ] Fix issue with eager evaluation of crashing functions

* Mark functions that call unsafe builtins as non-constant

* Better detection of crash primop when deciding if functions can be constant

src/Compiler/Opts/ToplevelConstants.idr

@@ -15,7 +15,7 @@ import Libraries.Data.SortedMap
 --          Call Graph
 --------------------------------------------------------------------------------
 
--- direct calls from a top-level funtion's expression to other
+-- direct calls from a top-level function's expression to other
 -- top-level functions.
 0 CallGraph : Type
 CallGraph = SortedMap Name (SortedSet Name)
@@ -71,6 +71,7 @@ data SortTag : Type where
 record SortST where
   constructor SST
   processed : SortedSet Name
+  nonconst  : SortedSet Name
   triples   : SnocList (Name, FC, NamedDef)
   map       : SortedMap Name (Name, FC, NamedDef)
   graph     : CallGraph
@@ -94,6 +95,15 @@ markProcessed n = do
 isProcessed : Ref SortTag SortST => Name -> Core Bool
 isProcessed n = map (contains n . processed) (get SortTag)
 
+checkCrash : Ref SortTag SortST => (Name, FC, NamedDef) -> Core ()
+checkCrash (n, _, MkNmError _) = update SortTag $ { nonconst $= insert n }
+checkCrash (n, _, MkNmFun args (NmCrash _ _)) = update SortTag $ { nonconst $= insert n }
+checkCrash (n, _, MkNmFun args (NmOp _ Crash _)) = update SortTag $ { nonconst $= insert n }
+checkCrash (n, _, def) = do
+  st <- get SortTag
+  when (any (flip contains st.nonconst) !(getCalls n)) $
+    put SortTag $ { nonconst $= insert n } st
+
 sortDef : Ref SortTag SortST => Name -> Core ()
 sortDef n = do
   False  <- isProcessed n | True => pure ()
@@ -102,6 +112,7 @@ sortDef n = do
   traverse_ sortDef cs
   Just t <- getTriple n | Nothing => pure ()
   appendDef t
+  checkCrash t
 
 isConstant : (recursiveFunctions : SortedSet Name) -> (Name,FC,NamedDef) -> Bool
 isConstant rec (n, _, MkNmFun [] _) = not $ contains n rec
@@ -115,12 +126,15 @@ sortDefs ts =
       consts := map fst $ filter (isConstant rec) ts
       init   := SST {
                     processed = empty
+                  , nonconst  = empty
                   , triples   = Lin
                   , map       = fromList (map (\t => (fst t, t)) ts)
                   , graph     = graph
                   }
    in do
      s       <- newRef SortTag init
      traverse_ sortDef (map fst ts)
-     sorted  <- map ((<>> []) . triples) (get SortTag)
+     st <- get SortTag
+     let sorted = triples st <>> []
+     let consts = filter (not . flip contains (nonconst st)) consts
      pure (sorted, fromList consts)

tests/Main.idr

@@ -308,7 +308,7 @@ chezTests = MkTestPool "Chez backend" [] (Just Chez)
     , "chez013", "chez014", "chez015", "chez016", "chez017", "chez018"
     , "chez019", "chez020", "chez021", "chez022", "chez023", "chez024"
     , "chez025", "chez026", "chez027", "chez028", "chez029", "chez030"
-    , "chez031", "chez032", "chez033", "chez034", "chez035"
+    , "chez031", "chez032", "chez033", "chez034", "chez035", "chez036"
     , "futures001"
     , "bitops"
     , "casts"

tests/chez/chez036/Crash.idr

@@ -0,0 +1,14 @@
+-- no_clauses.idr
+%default total
+
+bad : (0 _ : Z = S Z) -> Void
+bad _ impossible
+
+data BadPrf = Ok | No (Z = S Z)
+
+Show BadPrf where
+    show Ok = "Ok"
+    show (No prf) = absurd $ bad prf
+
+main : IO ()
+main = printLn Ok

tests/chez/chez036/Crash2.idr

@@ -0,0 +1,15 @@
+%noinline
+foo : (0 _ : Z = S Z) -> Void
+foo _ impossible
+
+%noinline
+bah : (0 _ : Z = S Z) -> Void
+bah prf = foo prf
+data BadPrf = Ok | No (Z = S Z)
+
+Show BadPrf where
+    show Ok = "Ok"
+    show (No prf) = absurd $ bah prf
+
+main : IO ()
+main = printLn Ok

tests/chez/chez036/Crash3.idr

@@ -0,0 +1,9 @@
+import System
+partial
+unreachable : a
+unreachable = idris_crash "unreachable"
+
+main : IO Int
+main = do
+    exitSuccess
+    assert_total unreachable

tests/chez/chez036/expected

@@ -0,0 +1,2 @@
+Ok
+Ok

tests/chez/chez036/run

@@ -0,0 +1,5 @@
+$1 --no-banner --no-color --console-width 0 --exec main Crash.idr
+$1 --no-banner --no-color --console-width 0 --exec main Crash2.idr
+$1 --no-banner --no-color --console-width 0 --exec main Crash3.idr
+
+rm -rf build